Draft: mir_unsafe_assume_spec

This implements supports for overrides in the SAW MIR backend, largely inspired
by the existing implementation in the LLVM backend. I've added a
`test_mir_unsafe_assume_spec` integration test to kick the tires and ensure the
basics work as expected.

Checks off one box in #1859.

Still TODO:

* Resolve the TODOs in the `test_mir_unsafe_assume_spec` test case (and the
  related code in `executeCond`) involving mutable allocations/statics in
  the postconditions of overrides.
* Add a SAW remote API test case

doc/manual/manual.md

@@ -2122,8 +2122,6 @@ some parts of `mir_verify` are not currently implemented, so it is possible
 that using `mir_verify` on some programs will fail. Features that are not yet
 implemented include the following:
 
-* MIR specifications that use overrides (i.e., the `[MIRSpec]` argument to
-  `mir_verify` must always be the empty list at present)
 * The ability to construct MIR `enum` values in specifications
 
 The `String` supplied as an argument to `mir_verify` is expected to be a
@@ -3086,18 +3084,18 @@ the target code. However, in some cases, it can be useful to use a
 `MethodSpec` to specify some code that either doesn't exist or is hard
 to prove. The previously-mentioned [`assume_unsat`
 tactic](#miscellaneous-tactics) omits proof but does not prevent
-simulation of the function. To skip simulation altogether, one can use:
+simulation of the function. To skip simulation altogether, one can use
+one of the following commands:
 
 ~~~
 llvm_unsafe_assume_spec :
   LLVMModule -> String -> LLVMSetup () -> TopLevel CrucibleMethodSpec
-~~~
-
-Or, in the experimental JVM implementation:
 
-~~~
 jvm_unsafe_assume_spec :
   JavaClass -> String -> JVMSetup () -> TopLevel JVMMethodSpec
+
+mir_unsafe_assume_spec :
+  MIRModule -> String -> MIRSetup () -> TopLevel MIRSpec
 ~~~
 
 ## A Heap-Based Example

intTests/test_mir_unsafe_assume_spec/Makefile

@@ -0,0 +1,13 @@
+all: test.linked-mir.json
+
+test.linked-mir.json: test.rs
+	saw-rustc $<
+	$(MAKE) remove-unused-build-artifacts
+
+.PHONY: remove-unused-build-artifacts
+remove-unused-build-artifacts:
+	rm -f test libtest.mir libtest.rlib
+
+.PHONY: clean
+clean: remove-unused-build-artifacts
+	rm -f test.linked-mir.json

intTests/test_mir_unsafe_assume_spec/test.rs

@@ -0,0 +1,35 @@
+pub fn f(_x: u32) -> u32 {
+    unimplemented!("f should be overridden");
+}
+
+pub fn g(x: u32) -> u32 {
+    f(x).wrapping_add(1)
+}
+
+pub fn h(x: u32) -> u32 {
+    x.wrapping_add(1)
+}
+
+pub fn g2() -> u32 {
+    f(2).wrapping_add(1)
+}
+
+pub fn p(_x: &u32, _y: &u32) -> u32 {
+    unimplemented!("p should be overriden");
+}
+
+pub fn q(x: &u32, y: &u32) -> u32 {
+    p(x, y)
+}
+
+pub fn side_effect(a: &mut u32) -> u32 {
+    let v: u32 = *a;
+    *a = 0;
+    v
+}
+
+pub fn foo(x: u32) -> u32 {
+    let mut b: u32 = x;
+    side_effect(&mut b);
+    side_effect(&mut b)
+}

intTests/test_mir_unsafe_assume_spec/test.saw

@@ -0,0 +1,158 @@
+enable_experimental;
+
+let f_generic_spec (x : Term) = do {
+  mir_execute_func [mir_term x];
+
+  mir_return (mir_term x);
+};
+
+let f_spec = do {
+  x <- mir_fresh_var "x" mir_u32;
+  f_generic_spec x;
+};
+
+let f2_spec = do {
+  let x = {{ 2 : [32] }};
+  f_generic_spec x;
+};
+
+let f3_spec = do {
+  let x = {{ 3 : [32] }};
+  f_generic_spec x;
+};
+
+let g_spec = do {
+  x <- mir_fresh_var "x" mir_u32;
+
+  mir_execute_func [mir_term x];
+
+  mir_return (mir_term {{ x + 1 }});
+};
+
+let g2_spec = do {
+  mir_execute_func [];
+
+  mir_return (mir_term {{ 3 : [32] }});
+};
+
+let h_spec = g_spec;
+
+let p_spec_1 = do {
+  x_ptr <- mir_alloc mir_u32;
+  x <- mir_fresh_var "x" mir_u32;
+  mir_points_to x_ptr (mir_term x);
+
+  y_ptr <- mir_alloc mir_u32;
+  y <- mir_fresh_var "y" mir_u32;
+  mir_points_to y_ptr (mir_term y);
+
+  mir_execute_func [x_ptr, y_ptr];
+
+  mir_return (mir_term {{ x + y }});
+};
+
+let p_spec_2 = do {
+  x_ptr <- mir_alloc mir_u32;
+  x <- mir_fresh_var "x" mir_u32;
+  mir_points_to x_ptr (mir_term x);
+
+  mir_execute_func [x_ptr, x_ptr];
+
+  mir_return (mir_term {{ 2 * x }});
+};
+
+let q_spec = p_spec_1;
+
+let side_spec_1 = do {
+  a_ptr <- mir_alloc_mut mir_u32;
+  a <- mir_fresh_var "a" mir_u32;
+  mir_points_to a_ptr (mir_term a);
+
+  mir_execute_func [a_ptr];
+
+  mir_points_to a_ptr (mir_term {{ 0 : [32] }});
+  mir_return (mir_term a);
+};
+
+let side_spec_2 = do {
+  a_ptr <- mir_alloc_mut mir_u32;
+  a <- mir_fresh_var "a" mir_u32;
+  mir_points_to a_ptr (mir_term a);
+
+  mir_execute_func [a_ptr];
+
+  mir_return (mir_term a);
+};
+
+let foo_spec = do {
+  x <- mir_fresh_var "x" mir_u32;
+
+  mir_execute_func [mir_term x];
+
+  mir_return (mir_term {{ x }});
+};
+
+m <- mir_load_module "test.linked-mir.json";
+
+////////////
+// Basics //
+////////////
+
+f_ov  <- mir_unsafe_assume_spec m "test::f" f_spec;
+f2_ov <- mir_unsafe_assume_spec m "test::f" f2_spec;
+f3_ov <- mir_unsafe_assume_spec m "test::f" f3_spec;
+
+// `g` should fail without an override for `f`...
+fails (
+  mir_verify m "test::g" [] false g_spec z3
+);
+// ...but should succeed with an `f` override.
+mir_verify m "test::g" [f_ov] false g_spec z3;
+// `h` never calls `f`, but it's still fine to redundantly pass an `f` override
+mir_verify m "test::h" [f_ov] false h_spec z3;
+
+// `g2` will succeed with both a generic `f` override as well as a specialized
+// one where the argument and result values are concrete.
+mir_verify m "test::g2" [f_ov] false g2_spec z3;
+mir_verify m "test::g2" [f2_ov] false g2_spec z3;
+mir_verify m "test::g2" [f_ov, f2_ov] false g2_spec z3;
+
+// Overrides that fail to match.
+fails (
+  mir_verify m "test::g" [f3_ov] false g_spec z3
+);
+fails (
+  mir_verify m "test::g2" [f3_ov] false g2_spec z3
+);
+
+//////////////
+// Pointers //
+//////////////
+
+p_ov_1 <- mir_unsafe_assume_spec m "test::p" p_spec_1;
+p_ov_2 <- mir_unsafe_assume_spec m "test::p" p_spec_2;
+
+mir_verify m "test::q" [p_ov_1] false q_spec z3;
+fails (
+  mir_verify m "test::q" [p_ov_2] false q_spec z3
+);
+
+///////////////////////
+// Avoid unsoundness //
+///////////////////////
+
+// https://github.com/GaloisInc/saw-script/issues/30
+
+side_ov_1 <- mir_verify m "test::side_effect" [] false side_spec_1 z3;
+side_ov_2 <- mir_verify m "test::side_effect" [] false side_spec_2 z3;
+
+fails (
+  mir_verify m "test::foo" [side_ov_1] false foo_spec z3
+);
+// TODO: This should not verify, as side_spec_2 underspecifies the mutable
+// allocation `a_ptr`. We need to implement a check that catches this.
+// fails (
+//   mir_verify m "test::foo" [side_ov_2] false foo_spec z3
+// );
+
+// TODO: Add similar tests for mutable statics.

intTests/test_mir_unsafe_assume_spec/test.sh

@@ -0,0 +1,3 @@
+set -e
+
+$SAW test.saw

saw-remote-api/CHANGELOG.md

@@ -8,6 +8,8 @@
   * The `SAW/MIR/verify` command performs verification of a MIR function.
   * The `SAW/MIR/find ADT` command looks up an algebraic data type (ADT) name in
     a MIR module.
+  * The `SAW/MIR/assume` command assumes a specification for a MIR function
+    without performing any verification.
 
   See the [remote API
   documentation](https://github.com/GaloisInc/saw-script/blob/master/saw-remote-api/docs/SAW.rst#sawmirload-module-command)

saw-remote-api/python/CHANGELOG.md

@@ -8,7 +8,8 @@
   * The `mir_verify` function performs verification of a MIR function.
   * The `mir_find_adt` function looks up an algebraic data type (ADT) name in a
     MIR module.
-
+  * The `mir_assume` function assumes a specification for a MIR function without
+    performing any verification.
   * The `saw_client.mir` module contains utility functions for constructing
     MIR types.
 

saw-remote-api/src/SAWServer/MIRVerify.hs

@@ -11,7 +11,7 @@ import Prelude hiding (mod)
 import Control.Lens
 
 import SAWScript.Crucible.MIR.Builtins
-    ( mir_verify )
+    ( mir_unsafe_assume_spec, mir_verify )
 import SAWScript.Value (rwCryptol)
 
 import qualified Argo
@@ -61,7 +61,7 @@ mirVerifyAssume mode (VerifyParams modName fun lemmaNames checkSat contract scri
                 proofScript <- interpretProofScript script
                 tl $ mir_verify rm fun lemmas checkSat setup proofScript
               AssumeContract ->
-                tl $ error "mir_unsafe_assume_spec not yet supported"
+                tl $ mir_unsafe_assume_spec rm fun setup
             dropTask
             setServerVal lemmaName res
             ok

src/SAWScript/Crucible/Common/Override.hs

@@ -78,10 +78,10 @@ import qualified Control.Monad.Fail as Fail
 import           Control.Monad.Trans.Except
 import           Control.Monad.Trans.Class
 import           Control.Monad.IO.Class
-import           Data.Proxy (Proxy(..))
 import qualified Data.Map as Map
 import           Data.Map (Map)
 import           Data.Maybe (fromMaybe)
+import           Data.Proxy (Proxy(..))
 import           Data.Set (Set)
 import           Data.Typeable (Typeable)
 import           Data.Void