Skeleton and initial support for proof-carrying code. (#7165)

* WIP veriwasm 2.0

Co-Authored-By: Chris Fallin <cfallin@fastly.com>

* PCC: successfully parse some simple facts.

Co-authored-by: Nick Fitzgerald <fitzgen@gmail.com>

* PCC: plumb facts through VCode and add framework on LowerBackend to check them.

Co-authored-by: Nick Fitzgerald <fitzgen@gmail.com>

* PCC: code is carrying some proofs! Very simple test-case.

Co-authored-by: Nick Fitzgerald <fitzgen@gmail.com>

* PCC: add a `safe` flag for checked memory accesses.

* PCC: add pretty-printing of facts to CLIF output.

* PCC: misc. cleanups.

* PCC: lots of cleanup.

* Post-rebase fixups and some misc. fixes.

* Add serde traits to facts.

* PCC: add succeed and fail tests.

* Review feedback: rename `safe` memflag to `checked`.

* Review feedback.

---------

Co-authored-by: Nick Fitzgerald <fitzgen@gmail.com>

Author: cfallin

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

@@ -63,6 +63,15 @@ 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. TODO ADD MORE
+        "#,
+        false,
+    );
+
     // Note that Cranelift doesn't currently need an is_pie flag, because PIE is
     // just PIC where symbols can't be pre-empted, which can be expressed with the
     // `colocated` flag on external functions and global values.

cranelift/codegen/src/context.rs

@@ -237,6 +237,8 @@ impl Context {
     /// Run the verifier on the function.
     ///
     /// Also check that the dominator tree and control flow graph are consistent with the function.
+    ///
+    /// TODO: rename to "CLIF validate" or similar.
     pub fn verify<'a, FOI: Into<FlagsOrIsa<'a>>>(&self, fisa: FOI) -> VerifierResult<()> {
         let mut errors = VerifierErrors::default();
         let _ = verify_context(&self.func, &self.cfg, &self.domtree, fisa, &mut errors);

cranelift/codegen/src/ir/dfg.rs

@@ -5,6 +5,7 @@ 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::{
     types, Block, BlockCall, ConstantData, ConstantPool, DynamicType, ExtFuncData, FuncRef,
     Immediate, Inst, JumpTables, RelSourceLoc, SigRef, Signature, Type, Value,
@@ -125,6 +126,9 @@ 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>,
@@ -158,6 +162,7 @@ impl DataFlowGraph {
             dynamic_types: DynamicTypes::new(),
             value_lists: ValueListPool::new(),
             values: PrimaryMap::new(),
+            facts: SecondaryMap::new(),
             signatures: PrimaryMap::new(),
             old_signatures: SecondaryMap::new(),
             ext_funcs: PrimaryMap::new(),

cranelift/codegen/src/ir/memflags.rs

@@ -6,10 +6,19 @@ use core::fmt;
 use serde_derive::{Deserialize, Serialize};
 
 enum FlagBit {
+    /// Guaranteed not to trap. This may enable additional
+    /// optimizations to be performed.
     Notrap,
+    /// Guaranteed to use "natural alignment" for the given type. This
+    /// may enable better instruction selection.
     Aligned,
+    /// A load that reads data in memory that does not change for the
+    /// duration of the function's execution. This may enable
+    /// additional optimizations to be performed.
     Readonly,
+    /// Load multi-byte values from memory in a little-endian format.
     LittleEndian,
+    /// Load multi-byte values from memory in a big-endian format.
     BigEndian,
     /// Accesses only the "heap" part of abstract state. Used for
     /// alias analysis. Mutually exclusive with "table" and "vmctx".
@@ -20,10 +29,15 @@ enum FlagBit {
     /// Accesses only the "vmctx" part of abstract state. Used for
     /// alias analysis. Mutually exclusive with "heap" and "table".
     Vmctx,
+    /// Check this load or store for safety when using the
+    /// proof-carrying-code framework. The address must have a
+    /// `PointsTo` fact attached with a sufficiently large valid range
+    /// for the accessed size.
+    Checked,
 }
 
-const NAMES: [&str; 8] = [
-    "notrap", "aligned", "readonly", "little", "big", "heap", "table", "vmctx",
+const NAMES: [&str; 9] = [
+    "notrap", "aligned", "readonly", "little", "big", "heap", "table", "vmctx", "checked",
 ];
 
 /// Endianness of a memory access.
@@ -48,7 +62,7 @@ pub enum Endianness {
 #[derive(Clone, Copy, Debug, Hash, PartialEq, Eq)]
 #[cfg_attr(feature = "enable-serde", derive(Serialize, Deserialize))]
 pub struct MemFlags {
-    bits: u8,
+    bits: u16,
 }
 
 impl MemFlags {
@@ -265,6 +279,32 @@ impl MemFlags {
         self.set_vmctx();
         self
     }
+
+    /// Test if the `checked` bit is set.
+    ///
+    /// Loads and stores with this flag are verified to access
+    /// pointers only with a validated `PointsTo` fact attached, and
+    /// with that fact validated, when using the proof-carrying-code
+    /// framework. If initial facts on program inputs are correct
+    /// (i.e., correctly denote the shape and types of data structures
+    /// in memory), and if PCC validates the compiled output, then all
+    /// `checked`-marked memory accesses are guaranteed (up to the
+    /// checker's correctness) to access valid memory. This can be
+    /// used to ensure memory safety and sandboxing.
+    pub fn checked(self) -> bool {
+        self.read(FlagBit::Checked)
+    }
+
+    /// Set the `checked` bit.
+    pub fn set_checked(&mut self) {
+        self.set(FlagBit::Checked);
+    }
+
+    /// Set the `checked` bit, returning new flags.
+    pub fn with_checked(mut self) -> Self {
+        self.set_checked();
+        self
+    }
 }
 
 impl fmt::Display for MemFlags {

cranelift/codegen/src/ir/mod.rs

@@ -18,6 +18,7 @@ pub(crate) mod known_symbol;
 pub mod layout;
 pub(crate) mod libcall;
 mod memflags;
+pub mod pcc;
 mod progpoint;
 mod sourceloc;
 pub mod stackslot;