PCC: initial end-to-end integration with Wasmtime's static memories.

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

@@ -67,7 +67,12 @@ pub(crate) fn define() -> SettingGroup {
         "enable_pcc",
         "Enable proof-carrying code translation validation.",
         r#"
-            This adds a proof-carrying code mode. TODO ADD MORE
+            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,
     );

cranelift/codegen/src/ir/function.rs

@@ -5,10 +5,10 @@
 
 use crate::entity::{PrimaryMap, SecondaryMap};
 use crate::ir::{
-    self, Block, DataFlowGraph, DynamicStackSlot, DynamicStackSlotData, DynamicStackSlots,
-    DynamicType, ExtFuncData, FuncRef, GlobalValue, GlobalValueData, Inst, JumpTable,
-    JumpTableData, Layout, MemoryType, MemoryTypeData, Opcode, SigRef, Signature, SourceLocs,
-    StackSlot, StackSlotData, StackSlots, Table, TableData, Type,
+    self, pcc::Fact, Block, DataFlowGraph, DynamicStackSlot, DynamicStackSlotData,
+    DynamicStackSlots, DynamicType, ExtFuncData, FuncRef, GlobalValue, GlobalValueData, Inst,
+    JumpTable, JumpTableData, Layout, MemoryType, MemoryTypeData, Opcode, SigRef, Signature,
+    SourceLocs, StackSlot, StackSlotData, StackSlots, Table, TableData, Type,
 };
 use crate::isa::CallConv;
 use crate::write::write_function;
@@ -172,6 +172,9 @@ 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>,
 
@@ -204,6 +207,7 @@ 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.tables.clear();
         self.dfg.clear();
@@ -417,6 +421,7 @@ 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(),
                 tables: PrimaryMap::new(),
                 dfg: DataFlowGraph::new(),

cranelift/codegen/src/ir/globalvalue.rs

@@ -1,7 +1,7 @@
 //! Global values.
 
 use crate::ir::immediates::{Imm64, Offset32};
-use crate::ir::{ExternalName, GlobalValue, Type};
+use crate::ir::{ExternalName, GlobalValue, MemFlags, Type};
 use crate::isa::TargetIsa;
 use core::fmt;
 
@@ -31,9 +31,8 @@ pub enum GlobalValueData {
         /// Type of the loaded value.
         global_type: Type,
 
-        /// Specifies whether the memory that this refers to is readonly, allowing for the
-        /// elimination of redundant loads.
-        readonly: bool,
+        /// Specifies the memory flags to be used by the load. Guaranteed to be notrap and aligned.
+        flags: MemFlags,
     },
 
     /// Value is an offset from another global value.
@@ -111,15 +110,8 @@ impl fmt::Display for GlobalValueData {
                 base,
                 offset,
                 global_type,
-                readonly,
-            } => write!(
-                f,
-                "load.{} notrap aligned {}{}{}",
-                global_type,
-                if readonly { "readonly " } else { "" },
-                base,
-                offset
-            ),
+                flags,
+            } => write!(f, "load.{}{} {}{}", global_type, flags, base, offset),
             Self::IAddImm {
                 global_type,
                 base,

cranelift/codegen/src/ir/pcc.rs

@@ -53,6 +53,10 @@
 //! - Support bounds-checking-type operations for dynamic memories and
 //!   tables.
 //!
+//! More checks:
+//! - Check that facts on `vmctx` GVs are subsumed by the actual facts
+//!   on the vmctx arg in block0 (function arg).
+//!
 //! Generality:
 //! - facts on outputs (in func signature)?
 //! - Implement checking at the CLIF level as well.
@@ -79,6 +83,7 @@ use crate::ir;
 use crate::ir::types::*;
 use crate::isa::TargetIsa;
 use crate::machinst::{BlockIndex, LowerBackend, MachInst, VCode};
+use crate::trace;
 use regalloc2::Function as _;
 use std::fmt;
 
@@ -440,6 +445,13 @@ impl<'a> FactContext<'a> {
         // support positive offsets.
         let offset = u64::try_from(offset).ok()?;
 
+        trace!(
+            "FactContext::offset: {:?} + {} in width {}",
+            fact,
+            offset,
+            width
+        );
+
         match fact {
             Fact::Range {
                 bit_width,
@@ -460,8 +472,8 @@ impl<'a> FactContext<'a> {
                 min_offset: mem_min_offset,
                 max_offset: mem_max_offset,
             } => {
-                let min_offset = mem_min_offset.checked_sub(offset)?;
-                let max_offset = mem_max_offset.checked_sub(offset)?;
+                let min_offset = mem_min_offset.checked_add(offset)?;
+                let max_offset = mem_max_offset.checked_add(offset)?;
                 Some(Fact::Mem {
                     ty: *ty,
                     min_offset,

cranelift/codegen/src/isa/aarch64/pcc.rs

@@ -346,9 +346,7 @@ fn check_addr<'a>(
             let rm = get_fact_or_default(vcode, rm)?;
             let rm_extended = fail_if_missing(extend_fact(ctx, rm, extendop))?;
             let sum = fail_if_missing(ctx.add(&rn, &rm_extended, 64))?;
-            trace!("rn = {rn:?} rm = {rm:?} rm_extended = {rm_extended:?} sum = {sum:?}");
             check(&sum, ty)?;
-            trace!(" -> checks out!");
             Ok(())
         }
         &AMode::Unscaled { rn, simm9 } => {
@@ -358,11 +356,13 @@ fn check_addr<'a>(
         }
         &AMode::UnsignedOffset { rn, uimm12 } => {
             let rn = get_fact_or_default(vcode, rn)?;
-            // Safety: this will not overflow: `size` should be at
-            // most 32 or 64 for large vector ops, and the `uimm12`'s
-            // value is at most 4095.
-            let uimm12: u64 = uimm12.value.into();
-            let offset: u64 = uimm12.checked_mul(ty.bytes().into()).unwrap();
+            // N.B.: the architecture scales the immediate in the
+            // encoded instruction by the size of the loaded type, so
+            // e.g. an offset field of 4095 can mean a load of offset
+            // 32760 (= 4095 * 8) for I64s. The `UImm12Scaled` type
+            // stores the *scaled* value, so we don't need to multiply
+            // (again) by the type's size here.
+            let offset: u64 = uimm12.value.into();
             // This `unwrap()` will always succeed because the value
             // will always be positive and much smaller than
             // `i64::MAX` (see above).

cranelift/codegen/src/legalizer/globalvalue.rs

@@ -21,7 +21,7 @@ pub fn expand_global_value(
     );
 
     match func.global_values[global_value] {
-        ir::GlobalValueData::VMContext => vmctx_addr(inst, func),
+        ir::GlobalValueData::VMContext => vmctx_addr(global_value, inst, func),
         ir::GlobalValueData::IAddImm {
             base,
             offset,
@@ -31,8 +31,8 @@ pub fn expand_global_value(
             base,
             offset,
             global_type,
-            readonly,
-        } => load_addr(inst, func, base, offset, global_type, readonly, isa),
+            flags,
+        } => load_addr(inst, func, base, offset, global_type, flags, isa),
         ir::GlobalValueData::Symbol { tls, .. } => symbol(inst, func, global_value, isa, tls),
         ir::GlobalValueData::DynScaleTargetConst { vector_type } => {
             const_vector_scale(inst, func, vector_type, isa)
@@ -52,7 +52,7 @@ fn const_vector_scale(inst: ir::Inst, func: &mut ir::Function, ty: ir::Type, isa
 }
 
 /// Expand a `global_value` instruction for a vmctx global.
-fn vmctx_addr(inst: ir::Inst, func: &mut ir::Function) {
+fn vmctx_addr(global_value: ir::GlobalValue, inst: ir::Inst, func: &mut ir::Function) {
     // Get the value representing the `vmctx` argument.
     let vmctx = func
         .special_param(ir::ArgumentPurpose::VMContext)
@@ -63,6 +63,15 @@ fn vmctx_addr(inst: ir::Inst, func: &mut ir::Function) {
     func.dfg.clear_results(inst);
     func.dfg.change_to_alias(result, vmctx);
     func.layout.remove_inst(inst);
+
+    // If there was a fact on the GV, then copy it to the vmctx arg
+    // blockparam def.
+    if let Some(fact) = &func.global_value_facts[global_value] {
+        if func.dfg.facts[vmctx].is_none() {
+            let fact = fact.clone();
+            func.dfg.facts[vmctx] = Some(fact);
+        }
+    }
 }
 
 /// Expand a `global_value` instruction for an iadd_imm global.
@@ -75,15 +84,11 @@ fn iadd_imm_addr(
 ) {
     let mut pos = FuncCursor::new(func).at_inst(inst);
 
-    // Get the value for the lhs. For tidiness, expand VMContext here so that we avoid
-    // `vmctx_addr` which creates an otherwise unneeded value alias.
-    let lhs = if let ir::GlobalValueData::VMContext = pos.func.global_values[base] {
-        pos.func
-            .special_param(ir::ArgumentPurpose::VMContext)
-            .expect("Missing vmctx parameter")
-    } else {
-        pos.ins().global_value(global_type, base)
-    };
+    // Get the value for the lhs.
+    let lhs = pos.ins().global_value(global_type, base);
+    if let Some(fact) = &pos.func.global_value_facts[base] {
+        pos.func.dfg.facts[lhs] = Some(fact.clone());
+    }
 
     // Simply replace the `global_value` instruction with an `iadd_imm`, reusing the result value.
     pos.func.dfg.replace(inst).iadd_imm(lhs, offset);
@@ -96,7 +101,7 @@ fn load_addr(
     base: ir::GlobalValue,
     offset: ir::immediates::Offset32,
     global_type: ir::Type,
-    readonly: bool,
+    flags: ir::MemFlags,
     isa: &dyn TargetIsa,
 ) {
     // We need to load a pointer from the `base` global value, so insert a new `global_value`
@@ -106,27 +111,17 @@ fn load_addr(
     let mut pos = FuncCursor::new(func).at_inst(inst);
     pos.use_srcloc(inst);
 
-    // Get the value for the base. For tidiness, expand VMContext here so that we avoid
-    // `vmctx_addr` which creates an otherwise unneeded value alias.
-    let base_addr = if let ir::GlobalValueData::VMContext = pos.func.global_values[base] {
-        pos.func
-            .special_param(ir::ArgumentPurpose::VMContext)
-            .expect("Missing vmctx parameter")
-    } else {
-        pos.ins().global_value(ptr_ty, base)
-    };
-
-    // Global-value loads are always notrap and aligned. They may be readonly.
-    let mut mflags = ir::MemFlags::trusted();
-    if readonly {
-        mflags.set_readonly();
+    // Get the value for the base.
+    let base_addr = pos.ins().global_value(ptr_ty, base);
+    if let Some(fact) = &pos.func.global_value_facts[base] {
+        pos.func.dfg.facts[base_addr] = Some(fact.clone());
     }
 
     // Perform the load.
     pos.func
         .dfg
         .replace(inst)
-        .load(global_type, mflags, base_addr, offset);
+        .load(global_type, flags, base_addr, offset);
 }
 
 /// Expand a `global_value` instruction for a symbolic name global.

cranelift/codegen/src/machinst/abi.rs

@@ -1319,7 +1319,7 @@ fn generate_gv<M: ABIMachineSpec>(
             base,
             offset,
             global_type: _,
-            readonly: _,
+            flags: _,
         } => {
             let base = generate_gv::<M>(f, sigs, sig, base, insts);
             let into_reg = Writable::from_reg(M::get_stacklimit_reg(f.stencil.signature.call_conv));

cranelift/codegen/src/print_errors.rs

@@ -4,6 +4,7 @@ use crate::entity::SecondaryMap;
 use crate::ir;
 use crate::ir::entities::{AnyEntity, Block, Inst, Value};
 use crate::ir::function::Function;
+use crate::ir::pcc::Fact;
 use crate::result::CodegenError;
 use crate::verifier::{VerifierError, VerifierErrors};
 use crate::write::{decorate_function, FuncWriter, PlainWriter};
@@ -71,8 +72,9 @@ impl<'a> FuncWriter for PrettyVerifierError<'a> {
         func: &Function,
         entity: AnyEntity,
         value: &dyn fmt::Display,
+        maybe_fact: Option<&Fact>,
     ) -> fmt::Result {
-        pretty_preamble_error(w, func, entity, value, &mut *self.0, self.1)
+        pretty_preamble_error(w, func, entity, value, maybe_fact, &mut *self.0, self.1)
     }
 }
 
@@ -156,11 +158,12 @@ fn pretty_preamble_error(
     func: &Function,
     entity: AnyEntity,
     value: &dyn fmt::Display,
+    maybe_fact: Option<&Fact>,
     func_w: &mut dyn FuncWriter,
     errors: &mut Vec<VerifierError>,
 ) -> fmt::Result {
     let mut s = String::new();
-    func_w.write_entity_definition(&mut s, func, entity, value)?;
+    func_w.write_entity_definition(&mut s, func, entity, value, maybe_fact)?;
     write!(w, "{}", s)?;
 
     // TODO: Use drain_filter here when it gets stabilized