Compositional crux-mir support

crux-mir/crux-mir.cabal

@@ -65,13 +65,12 @@ library
                    Mir.PP
                    Mir.Generate
                    Mir.DefId
-  other-modules:
-                 Mir.FancyMuxTree
-                 Mir.Intrinsics
-                 Mir.Overrides
-                 Mir.TransTy
-                 Mir.Trans
-                 Mir.TransCustom
+                   Mir.FancyMuxTree
+                   Mir.Intrinsics
+                   Mir.Overrides
+                   Mir.TransTy
+                   Mir.Trans
+                   Mir.TransCustom
 
 
 executable crux-mir

crux-mir/lib/crucible/lib.rs

@@ -1,8 +1,10 @@
 #![no_std]
 #![feature(core_intrinsics)]
 #![feature(crucible_intrinsics)]
+#![feature(unboxed_closures)]
 
 pub mod bitvector;
+pub mod method_spec;
 pub mod sym_bytes;
 pub mod symbolic;
 

crux-mir/lib/crucible/method_spec/mod.rs

@@ -0,0 +1,83 @@
+//! Provides the `MethodSpec` type, used for compositional reasoning.  Also provides
+//! `MethodSpecBuilder`, which is used internally by the compositional reasoning macros to
+//! construct a `MethodSpec` from a symbolic test.
+//!
+//! Note that these types work only when running under `crux-mir-comp`.  Trying to use them under
+//! ordinary `crux-mir` will produce an error.
+use core::fmt;
+
+mod raw;
+
+pub use self::raw::clobber_globals;
+
+
+/// The specification of a function.  This can be used when verifying callers of the function to
+/// avoid simulating the entire function itself.
+#[derive(Clone, Copy)]
+pub struct MethodSpec {
+    raw: raw::MethodSpec,
+}
+
+impl MethodSpec {
+    /// Enable this `MethodSpec` to be used as an override for its subject function.
+    pub fn enable(&self) {
+        raw::spec_enable(self.raw);
+    }
+}
+
+impl fmt::Debug for MethodSpec {
+    fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result {
+        let s = raw::spec_pretty_print(self.raw);
+        fmt.write_str("MethodSpec {")?;
+        for (i, chunk) in s.split("\n").enumerate() {
+            if i > 0 {
+                fmt.write_str(", ")?;
+            }
+            fmt.write_str(chunk);
+        }
+        fmt.write_str("}")?;
+        Ok(())
+    }
+}
+
+
+/// Helper type used to incrementally construct a `MethodSpec` for a function.
+pub struct MethodSpecBuilder {
+    raw: raw::MethodSpecBuilder,
+}
+
+impl fmt::Debug for MethodSpecBuilder {
+    fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result {
+        write!(fmt, "MethodSpecBuilder {{ .. }}")
+    }
+}
+
+impl MethodSpecBuilder {
+    pub fn new<Args, F: Fn<Args>>(f: F) -> MethodSpecBuilder {
+        MethodSpecBuilder {
+            raw: raw::builder_new::<F>(),
+        }
+    }
+
+    pub fn add_arg<T>(&mut self, x: &T) {
+        self.raw = raw::builder_add_arg(self.raw, x);
+    }
+
+    pub fn gather_assumes(&mut self) {
+        self.raw = raw::builder_gather_assumes(self.raw);
+    }
+
+    pub fn set_return<T>(&mut self, x: &T) {
+        self.raw = raw::builder_set_return(self.raw, x);
+    }
+
+    pub fn gather_asserts(&mut self) {
+        self.raw = raw::builder_gather_asserts(self.raw);
+    }
+
+    pub fn finish(self) -> MethodSpec {
+        MethodSpec {
+            raw: raw::builder_finish(self.raw),
+        }
+    }
+}

crux-mir/lib/crucible/method_spec/raw.rs

@@ -0,0 +1,73 @@
+//! Bindings for low-level MethodSpec APIs.
+//!
+//! Like most functions in the `crucible` crate, these functions are left unimplemented in Rust
+//! and are replaced by a real implementation via the Crucible override mechanism.  However, unlike
+//! most other functions, the necessary overrides are not provided by `crux-mir`; instead, they are
+//! provided by the `crux-mir-comp` package in the `saw-script` repository, which extends ordinary
+//! `crux-mir` with additional overrides using `crux-mir`'s new `mainWithExtraOverrides` entry
+//! point.  Trying to use these APIs under ordinary `crux-mir` will produce an error.
+
+/// Crucible `MethodSpecType`, exposed to Rust.
+///
+/// As usual for Crucible types, this implements `Copy`, since it's backed by a boxed,
+/// garbage-collected Haskell value.  It contains a dummy field to ensure the Rust compiler sees it
+/// as having non-zero size.  The representation is overridden within `crux-mir`, so the field
+/// should not be accessed when running symbolically.
+#[derive(Clone, Copy)]
+pub struct MethodSpec(u8);
+
+// We only have `libcore` available, so we can't return `String` here.  Instead, the override for
+// this function within `crux-mir` will construct and leak a `str`.
+pub fn spec_pretty_print(ms: MethodSpec) -> &'static str {
+    "(unknown MethodSpec)"
+}
+
+/// Enable using `ms` in place of calls to the actual function.  The function to override is
+/// determined by the `F` type parameter of `builder_new` during the construction of the
+/// `MethodSpec`.
+pub fn spec_enable(ms: MethodSpec) {
+}
+
+
+/// Crucible `MethodSpecBuilderType`, exposed to Rust.
+#[derive(Clone, Copy)]
+pub struct MethodSpecBuilder(u8);
+
+pub fn builder_new<F>() -> MethodSpecBuilder {
+    // If the program is running under ordinary `crux-mir` instead of `crux-mir-comp`, then the
+    // override for this function will be missing.  We could provide a dummy implementation for
+    // that case, but it's better to fail early.  Otherwise users will get cryptic errors when
+    // invoking their spec functions, as `builder_finish` won't have its usual effect of discarding
+    // any new goals added by the spec function.
+    unimplemented!("MethodSpecBuilder is not supported on this version of crux-mir")
+}
+
+pub fn builder_add_arg<T>(msb: MethodSpecBuilder, x: &T) -> MethodSpecBuilder {
+    let _ = x;
+    msb
+}
+
+pub fn builder_gather_assumes(msb: MethodSpecBuilder) -> MethodSpecBuilder {
+    msb
+}
+
+pub fn builder_set_return<T>(msb: MethodSpecBuilder, x: &T) -> MethodSpecBuilder {
+    let _ = x;
+    msb
+}
+
+pub fn builder_gather_asserts(msb: MethodSpecBuilder) -> MethodSpecBuilder {
+    msb
+}
+
+pub fn builder_finish(msb: MethodSpecBuilder) -> MethodSpec {
+    let _ = msb;
+    MethodSpec(0)
+}
+
+
+/// Replace all mutable global data with arbitrary values.  This is used at the start of tests to
+/// ensure that the property holds in any context.
+pub fn clobber_globals() {
+    unimplemented!("MethodSpecBuilder is not supported on this version of crux-mir")
+}

crux-mir/src/Mir/Generate.hs

@@ -77,10 +77,10 @@ needsRebuild output inputs = do
 mirJsonOutFile :: FilePath -> FilePath
 mirJsonOutFile rustFile = rustFile -<.> "mir"
 
-getRlibsDir :: IO FilePath
-getRlibsDir = maybe "rlibs" id <$> lookupEnv "CRUX_RUST_LIBRARY_PATH"
+getRlibsDir :: (?defaultRlibsDir :: FilePath) => IO FilePath
+getRlibsDir = maybe ?defaultRlibsDir id <$> lookupEnv "CRUX_RUST_LIBRARY_PATH"
 
-compileMirJson :: Bool -> Bool -> FilePath -> IO ()
+compileMirJson :: (?defaultRlibsDir :: FilePath) => Bool -> Bool -> FilePath -> IO ()
 compileMirJson keepRlib quiet rustFile = do
     let outFile = rustFile -<.> "bin"
 
@@ -103,7 +103,7 @@ compileMirJson keepRlib quiet rustFile = do
             True  -> removeFile outFile
             False -> return ()
 
-maybeCompileMirJson :: Bool -> Bool -> FilePath -> IO ()
+maybeCompileMirJson :: (?defaultRlibsDir :: FilePath) => Bool -> Bool -> FilePath -> IO ()
 maybeCompileMirJson keepRlib quiet rustFile = do
     build <- needsRebuild (mirJsonOutFile rustFile) [rustFile]
     when build $ compileMirJson keepRlib quiet rustFile
@@ -159,7 +159,7 @@ libJsonFiles =
 -- NOTE: If the rust file has not been modified since the
 -- last .mir file was created, this function does nothing
 -- This function uses 'failIO' if any error occurs
-generateMIR :: (HasCallStack, ?debug::Int) =>
+generateMIR :: (HasCallStack, ?debug::Int, ?defaultRlibsDir :: FilePath) =>
                FilePath          -- ^ location of input file
             -> Bool              -- ^ `True` to keep the generated .rlib
             -> IO Collection