PCC: remove proof-carrying code (for now?). (#12800)

In late 2023, we built out an experimental feature called
Proof-Carrying Code (PCC), where we attached "facts" to values in the
CLIF IR and built verification of these facts after lowering to
machine instructions. We also added "memory types" describing layout
of memory and a "checked" flag on memory operations such that we could
verify that any checked memory operation accessed valid memory (as
defined by memory types attached to pointer values via
facts). Wasmtime's Cranelift backend then put appropriate memory types
and facts in its IR such that all accesses to memory (aspirationally)
could be checked, taking the whole mid-end and lowering backend of
Cranelift out of the trusted core that enforces SFI.

This basically worked, at the time, for static memories; but never for
dynamic memories, and then work on the feature lost
prioritization (aka I had to work on other things) and I wasn't able
to complete it and put it in fuzzing/enable it as a production option.

Unfortunately since then it has bit-rotted significantly -- as we add
new backend optimizations and instruction lowerings we haven't kept
the PCC framework up to date.

Inspired by the discussion in #12497 I think it's time to delete
it (hopefully just "for now"?) unless/until we can build it again. And
when we do that, we should probably get it to the point of validating
robust operation on all combinations of memory configurations before
merging. (That implies a big experiment branch rather than a bunch of
eager PRs in-tree, but so it goes.) I still believe it is possible to
build this (and I have ideas on how to do it!) but not right now.

Author: cfallin

cranelift/codegen/meta/src/shared/settings.rs

@@ -77,20 +77,6 @@ pub(crate) fn define() -> SettingGroup {
         true,
     );
 
-    settings.add_bool(
-        "enable_pcc",
-        "Enable proof-carrying code translation validation.",
-        r#"
-            This adds a proof-carrying-code mode. Proof-carrying code (PCC) is a strategy to verify
-            that the compiler preserves certain properties or invariants in the compiled code.
-            For example, a frontend that translates WebAssembly to CLIF can embed PCC facts in
-            the CLIF, and Cranelift will verify that the final machine code satisfies the stated
-            facts at each intermediate computed value. Loads and stores can be marked as "checked"
-            and their memory effects can be verified as safe.
-        "#,
-        false,
-    );
-
     // Note that Cranelift doesn't currently need an is_pie flag, because PIE is
     // just PIC where symbols can't be preempted, which can be expressed with the
     // `colocated` flag on external functions and global values.

cranelift/codegen/src/context.rs

@@ -381,7 +381,6 @@ impl Context {
             &self.domtree,
             &self.loop_analysis,
             &mut alias_analysis,
-            &fisa.flags,
             ctrl_plane,
         );
         pass.run();

cranelift/codegen/src/egraph/mod.rs

@@ -7,16 +7,13 @@ use crate::cursor::{Cursor, CursorPosition, FuncCursor};
 use crate::dominator_tree::DominatorTree;
 use crate::egraph::elaborate::Elaborator;
 use crate::inst_predicates::{is_mergeable_for_egraph, is_pure_for_egraph};
-use crate::ir::pcc::Fact;
 use crate::ir::{
-    Block, DataFlowGraph, Function, Inst, InstructionData, Opcode, Type, Value, ValueDef,
-    ValueListPool,
+    Block, DataFlowGraph, Function, Inst, InstructionData, Type, Value, ValueDef, ValueListPool,
 };
 use crate::loop_analysis::LoopAnalysis;
 use crate::opts::IsleContext;
 use crate::opts::generated_code::SkeletonInstSimplification;
 use crate::scoped_hash_map::{Entry as ScopedEntry, ScopedHashMap};
-use crate::settings::Flags;
 use crate::take_and_replace::TakeAndReplace;
 use crate::trace;
 use alloc::vec::Vec;
@@ -60,8 +57,6 @@ pub struct EgraphPass<'a> {
     /// Loop analysis results, used for built-in LICM during
     /// elaboration.
     loop_analysis: &'a LoopAnalysis,
-    /// Compiler flags.
-    flags: &'a Flags,
     /// Chaos-mode control-plane so we can test that we still get
     /// correct results when our heuristics make bad decisions.
     ctrl_plane: &'a mut ControlPlane,
@@ -95,7 +90,6 @@ where
     domtree: &'opt DominatorTree,
     pub(crate) alias_analysis: &'opt mut AliasAnalysis<'analysis>,
     pub(crate) alias_analysis_state: &'opt mut LastStores,
-    flags: &'opt Flags,
     ctrl_plane: &'opt mut ControlPlane,
     // Held locally during optimization of one node (recursively):
     pub(crate) rewrite_depth: usize,
@@ -170,7 +164,6 @@ where
                 let result = self.func.dfg.first_result(inst);
                 self.value_to_opt_value[result] = orig_result;
                 self.available_block[result] = self.available_block[orig_result];
-                self.func.dfg.merge_facts(result, orig_result);
             }
             orig_result
         } else {
@@ -194,8 +187,6 @@ where
                 }
             };
 
-            self.attach_constant_fact(inst, result, ty);
-
             self.available_block[result] = self.get_available_block(inst);
             let opt_value = self.optimize_pure_enode(inst);
             log::trace!("optimizing inst {inst} orig result {result} gave {opt_value}");
@@ -387,7 +378,6 @@ where
                 ctx.eclass_size[union_value] = eclass_size - 1;
                 ctx.stats.union += 1;
                 trace!(" -> union: now {}", union_value);
-                ctx.func.dfg.merge_facts(old_union_value, optimized_value);
                 ctx.available_block[union_value] =
                     ctx.merge_availability(old_union_value, optimized_value);
             }
@@ -503,7 +493,6 @@ where
             );
             self.value_to_opt_value[result] = new_result;
             self.available_block[result] = self.available_block[new_result];
-            self.func.dfg.merge_facts(result, new_result);
             Some(SkeletonInstSimplification::Remove)
         }
         // Otherwise, generic side-effecting op -- always keep it, and
@@ -695,23 +684,6 @@ where
         // Return the best simplification!
         best
     }
-
-    /// Helper to propagate facts on constant values: if PCC is
-    /// enabled, then unconditionally add a fact attesting to the
-    /// Value's concrete value.
-    fn attach_constant_fact(&mut self, inst: Inst, value: Value, ty: Type) {
-        if self.flags.enable_pcc() {
-            if let InstructionData::UnaryImm {
-                opcode: Opcode::Iconst,
-                imm,
-            } = self.func.dfg.insts[inst]
-            {
-                let imm: i64 = imm.into();
-                self.func.dfg.facts[value] =
-                    Some(Fact::constant(ty.bits().try_into().unwrap(), imm as u64));
-            }
-        }
-    }
 }
 
 impl<'a> EgraphPass<'a> {
@@ -721,15 +693,13 @@ impl<'a> EgraphPass<'a> {
         domtree: &'a DominatorTree,
         loop_analysis: &'a LoopAnalysis,
         alias_analysis: &'a mut AliasAnalysis<'a>,
-        flags: &'a Flags,
         ctrl_plane: &'a mut ControlPlane,
     ) -> Self {
         Self {
             func,
             domtree,
             loop_analysis,
             alias_analysis,
-            flags,
             ctrl_plane,
             stats: Stats::default(),
             remat_values: FxHashSet::default(),
@@ -897,7 +867,6 @@ impl<'a> EgraphPass<'a> {
                             domtree: &self.domtree,
                             alias_analysis: self.alias_analysis,
                             alias_analysis_state: &mut alias_analysis_state,
-                            flags: self.flags,
                             ctrl_plane: self.ctrl_plane,
                             optimized_values: Default::default(),
                             optimized_insts: Default::default(),

cranelift/codegen/src/ir/dfg.rs

@@ -5,7 +5,6 @@ use crate::ir;
 use crate::ir::builder::ReplaceBuilder;
 use crate::ir::dynamic_type::{DynamicTypeData, DynamicTypes};
 use crate::ir::instructions::{CallInfo, InstructionData};
-use crate::ir::pcc::Fact;
 use crate::ir::user_stack_maps::{UserStackMapEntry, UserStackMapEntryVec};
 use crate::ir::{
     Block, BlockArg, BlockCall, ConstantData, ConstantPool, DynamicType, ExceptionTables,
@@ -144,9 +143,6 @@ pub struct DataFlowGraph {
     /// Primary value table with entries for all values.
     values: PrimaryMap<Value, ValueDataPacked>,
 
-    /// Facts: proof-carrying-code assertions about values.
-    pub facts: SecondaryMap<Value, Option<Fact>>,
-
     /// Function signature table. These signatures are referenced by indirect call instructions as
     /// well as the external function references.
     pub signatures: PrimaryMap<SigRef, Signature>,
@@ -181,7 +177,6 @@ impl DataFlowGraph {
             dynamic_types: DynamicTypes::new(),
             value_lists: ValueListPool::new(),
             values: PrimaryMap::new(),
-            facts: SecondaryMap::new(),
             signatures: PrimaryMap::new(),
             ext_funcs: PrimaryMap::new(),
             values_labels: None,
@@ -207,7 +202,6 @@ impl DataFlowGraph {
         self.constants.clear();
         self.immediates.clear();
         self.jump_tables.clear();
-        self.facts.clear();
     }
 
     /// Get the total number of instructions created in this function, whether they are currently
@@ -489,21 +483,6 @@ impl DataFlowGraph {
         //   removed), and unions (but the egraph pass ensures there are no
         //   aliases before creating unions).
 
-        // Merge `facts` from any alias onto the aliased value. Note that if
-        // there was a chain of aliases, at this point every alias that was in
-        // the chain points to the same final value, so their facts will all be
-        // merged together.
-        for value in self.facts.keys() {
-            if let ValueData::Alias { original, .. } = self.values[value].into() {
-                if let Some(new_fact) = self.facts[value].take() {
-                    match &mut self.facts[original] {
-                        Some(old_fact) => *old_fact = Fact::intersect(old_fact, &new_fact),
-                        old_fact => *old_fact = Some(new_fact),
-                    }
-                }
-            }
-        }
-
         // - `signatures` and `ext_funcs` have no values.
 
         if let Some(values_labels) = &mut self.values_labels {
@@ -1075,13 +1054,7 @@ impl DataFlowGraph {
         // Get the controlling type variable.
         let ctrl_typevar = self.ctrl_typevar(inst);
         // Create new result values.
-        let num_results = self.make_inst_results(new_inst, ctrl_typevar);
-        // Copy over PCC facts, if any.
-        for i in 0..num_results {
-            let old_result = self.inst_results(inst)[i];
-            let new_result = self.inst_results(new_inst)[i];
-            self.facts[new_result] = self.facts[old_result].clone();
-        }
+        self.make_inst_results(new_inst, ctrl_typevar);
         new_inst
     }
 
@@ -1416,38 +1389,6 @@ impl DataFlowGraph {
     pub fn detach_inst_results(&mut self, inst: Inst) {
         self.results[inst].clear(&mut self.value_lists);
     }
-
-    /// Merge the facts for two values. If both values have facts and
-    /// they differ, both values get a special "conflict" fact that is
-    /// never satisfied.
-    pub fn merge_facts(&mut self, a: Value, b: Value) {
-        let a = self.resolve_aliases(a);
-        let b = self.resolve_aliases(b);
-        match (&self.facts[a], &self.facts[b]) {
-            (Some(a), Some(b)) if a == b => { /* nothing */ }
-            (None, None) => { /* nothing */ }
-            (Some(a), None) => {
-                self.facts[b] = Some(a.clone());
-            }
-            (None, Some(b)) => {
-                self.facts[a] = Some(b.clone());
-            }
-            (Some(a_fact), Some(b_fact)) => {
-                assert_eq!(self.value_type(a), self.value_type(b));
-                let merged = Fact::intersect(a_fact, b_fact);
-                crate::trace!(
-                    "facts merge on {} and {}: {:?}, {:?} -> {:?}",
-                    a,
-                    b,
-                    a_fact,
-                    b_fact,
-                    merged,
-                );
-                self.facts[a] = Some(merged.clone());
-                self.facts[b] = Some(merged);
-            }
-        }
-    }
 }
 
 /// Contents of a basic block.

cranelift/codegen/src/ir/entities.rs

@@ -187,25 +187,6 @@ impl GlobalValue {
     }
 }
 
-/// An opaque reference to a memory type.
-///
-/// A `MemoryType` is a descriptor of a struct layout in memory, with
-/// types and proof-carrying-code facts optionally attached to the
-/// fields.
-#[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
-#[cfg_attr(feature = "enable-serde", derive(Serialize, Deserialize))]
-pub struct MemoryType(u32);
-entity_impl!(MemoryType, "mt");
-
-impl MemoryType {
-    /// Create a new memory type reference from its number.
-    ///
-    /// This method is for use by the parser.
-    pub fn with_number(n: u32) -> Option<Self> {
-        if n < u32::MAX { Some(Self(n)) } else { None }
-    }
-}
-
 /// An opaque reference to a constant.
 ///
 /// You can store [`ConstantData`](super::ConstantData) in a
@@ -400,8 +381,6 @@ pub enum AnyEntity {
     DynamicType(DynamicType),
     /// A Global value.
     GlobalValue(GlobalValue),
-    /// A memory type.
-    MemoryType(MemoryType),
     /// A jump table.
     JumpTable(JumpTable),
     /// A constant.
@@ -427,7 +406,6 @@ impl fmt::Display for AnyEntity {
             Self::DynamicStackSlot(r) => r.fmt(f),
             Self::DynamicType(r) => r.fmt(f),
             Self::GlobalValue(r) => r.fmt(f),
-            Self::MemoryType(r) => r.fmt(f),
             Self::JumpTable(r) => r.fmt(f),
             Self::Constant(r) => r.fmt(f),
             Self::FuncRef(r) => r.fmt(f),
@@ -486,12 +464,6 @@ impl From<GlobalValue> for AnyEntity {
     }
 }
 
-impl From<MemoryType> for AnyEntity {
-    fn from(r: MemoryType) -> Self {
-        Self::MemoryType(r)
-    }
-}
-
 impl From<JumpTable> for AnyEntity {
     fn from(r: JumpTable) -> Self {
         Self::JumpTable(r)

cranelift/codegen/src/ir/function.rs

@@ -9,8 +9,8 @@ use crate::ir::DebugTags;
 use crate::ir::{
     self, Block, DataFlowGraph, DynamicStackSlot, DynamicStackSlotData, DynamicStackSlots,
     DynamicType, ExtFuncData, FuncRef, GlobalValue, GlobalValueData, Inst, JumpTable,
-    JumpTableData, Layout, MemoryType, MemoryTypeData, SigRef, Signature, SourceLocs, StackSlot,
-    StackSlotData, StackSlots, Type, pcc::Fact,
+    JumpTableData, Layout, SigRef, Signature, SourceLocs, StackSlot, StackSlotData, StackSlots,
+    Type,
 };
 use crate::isa::CallConv;
 use crate::write::{write_function, write_function_spec};
@@ -173,12 +173,6 @@ pub struct FunctionStencil {
     /// Global values referenced.
     pub global_values: PrimaryMap<ir::GlobalValue, ir::GlobalValueData>,
 
-    /// Global value proof-carrying-code facts.
-    pub global_value_facts: SecondaryMap<ir::GlobalValue, Option<Fact>>,
-
-    /// Memory types for proof-carrying code.
-    pub memory_types: PrimaryMap<ir::MemoryType, ir::MemoryTypeData>,
-
     /// Data flow graph containing the primary definition of all instructions, blocks and values.
     pub dfg: DataFlowGraph,
 
@@ -221,8 +215,6 @@ impl FunctionStencil {
         self.sized_stack_slots.clear();
         self.dynamic_stack_slots.clear();
         self.global_values.clear();
-        self.global_value_facts.clear();
-        self.memory_types.clear();
         self.dfg.clear();
         self.layout.clear();
         self.srclocs.clear();
@@ -257,11 +249,6 @@ impl FunctionStencil {
         self.global_values.push(data)
     }
 
-    /// Declares a memory type for use by the function.
-    pub fn create_memory_type(&mut self, data: MemoryTypeData) -> MemoryType {
-        self.memory_types.push(data)
-    }
-
     /// Find the global dyn_scale value associated with given DynamicType.
     pub fn get_dyn_scale(&self, ty: DynamicType) -> GlobalValue {
         self.dfg.dynamic_types.get(ty).unwrap().dynamic_scale
@@ -420,8 +407,6 @@ impl Function {
                 sized_stack_slots: StackSlots::new(),
                 dynamic_stack_slots: DynamicStackSlots::new(),
                 global_values: PrimaryMap::new(),
-                global_value_facts: SecondaryMap::new(),
-                memory_types: PrimaryMap::new(),
                 dfg: DataFlowGraph::new(),
                 layout: Layout::new(),
                 srclocs: SecondaryMap::new(),