Merge pull request #2151 from GaloisInc/T1998-jvm_mir_equal

Add `{jvm,mir}_equal` commands

CHANGES.md

@@ -1,5 +1,10 @@
 # next -- TBA
 
+## New Features
+
+* Add `mir_equal` and `jvm_equal` commands, which mirror the `llvm_equal`
+  command for the MIR and JVM backends, respectively.
+
 ## Bug fixes
 
 * Counterexamples including SMT arrays are now printed with the array

doc/manual/manual.md

@@ -3710,16 +3710,18 @@ values in scope at the time.
 * `mir_postcond : Term -> MIRSetup ()`
 * `mir_assert : Term -> MIRSetup ()`
 
-These commands take `Term` arguments, and therefore cannot describe
-the values of pointers. The "assert" variants will work in either pre-
-or post-conditions, and are useful when defining helper functions
-that, e.g., state datastructure invariants that make sense in both
-phases.  The `llvm_equal` command states that two `SetupValue`s should
-be equal, and can be used in either the initial or the final state.
+These commands take `Term` arguments, and therefore cannot describe the values
+of pointers. The "assert" variants will work in either pre- or post-conditions,
+and are useful when defining helper functions that, e.g., provide datastructure
+invariants that make sense in both phases.  The `{llvm,jvm,mir}_equal` commands
+state that two values should be equal, and can be used in either the initial or
+the final state.
 
 * `llvm_equal : SetupValue -> SetupValue -> LLVMSetup ()`
+* `jvm_equal : JVMValue -> JVMValue -> JVMSetup ()`
+* `mir_equal : MIRValue -> MIRValue -> MIRSetup ()`
 
-The use of `llvm_equal` can also sometimes lead to more efficient
+The use of `{llvm,jvm,mir}_equal` can also sometimes lead to more efficient
 symbolic execution when the predicate of interest is an equality.
 
 ## Assuming specifications

intTests/test1998_jvm/Makefile

@@ -0,0 +1,2 @@
+%.class: %.java
+	javac -g $<

intTests/test1998_jvm/Test.java

@@ -0,0 +1,5 @@
+class Test {
+    static boolean f(int x, int y) {
+        return x == y;
+    }
+}

intTests/test1998_jvm/test.saw

@@ -0,0 +1,12 @@
+let f_spec = do {
+    x <- jvm_fresh_var "x" java_int;
+    y <- jvm_fresh_var "y" java_int;
+    jvm_equal (jvm_term x) (jvm_term y);
+
+    jvm_execute_func [jvm_term x, jvm_term y];
+
+    jvm_return (jvm_term {{ True }});
+};
+
+c <- java_load_class "Test";
+jvm_verify c "f" [] false f_spec z3;

intTests/test1998_jvm/test.sh

@@ -0,0 +1 @@
+$SAW test.saw

intTests/test1998_mir/Makefile

@@ -0,0 +1,17 @@
+# The current checked-in linked-mir.json file was generated by:
+#    rustc 1.69.0-nightly (5e37043d6 2023-01-22)
+#    mir-json c52b16bf26af2f5b98157ebf9975aa0021982bbc from 2024-09-11
+
+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/test1998_mir/test.rs

@@ -0,0 +1,7 @@
+pub fn f(x: [u16; 32], y: [u16; 32]) -> bool {
+    let mut eq: bool = true;
+    for i in 0..32 {
+        eq &= x[i] == y[i];
+    }
+    eq
+}

intTests/test1998_mir/test.saw

@@ -0,0 +1,14 @@
+enable_experimental;
+
+let f_spec = do {
+    x <- mir_fresh_expanded_value "x" (mir_array 32 mir_u16);
+    y <- mir_fresh_expanded_value "y" (mir_array 32 mir_u16);
+    mir_equal x y;
+
+    mir_execute_func [x, y];
+
+    mir_return (mir_term {{ True }});
+};
+
+m <- mir_load_module "test.linked-mir.json";
+mir_verify m "test::f" [] false f_spec z3;

intTests/test1998_mir/test.sh

@@ -0,0 +1 @@
+$SAW test.saw

src/SAWScript/Crucible/Common/Setup/Builtins.hs

@@ -9,7 +9,14 @@ Stability   : provisional
 {-# LANGUAGE DeriveTraversable #-}
 {-# LANGUAGE ParallelListComp #-}
 
-module SAWScript.Crucible.Common.Setup.Builtins where
+module SAWScript.Crucible.Common.Setup.Builtins
+  ( crucible_precond
+  , crucible_postcond
+  , crucible_return
+  , crucible_execute_func
+  , crucible_equal
+  , CheckPointsToType(..)
+  ) where
 
 import           Control.Lens
 import           Control.Monad (when)
@@ -85,6 +92,21 @@ crucible_execute_func args = do
                                                   | t <- tps
                                                   ]
 
+crucible_equal ::
+  W4.ProgramLoc ->
+  MS.SetupValue ext ->
+  MS.SetupValue ext ->
+  CrucibleSetup ext ()
+crucible_equal loc val1 val2 = do
+  tags <- view croTags
+  let md = MS.ConditionMetadata
+           { MS.conditionLoc = loc
+           , MS.conditionTags = tags
+           , MS.conditionType = "equality specification"
+           , MS.conditionContext = ""
+           }
+  addCondition (MS.SetupCond_Equal md val1 val2)
+
 --------------------------------------------------------------------------------
 -- ** Shared data types
 

src/SAWScript/Crucible/JVM/Builtins.hs

@@ -45,6 +45,7 @@ module SAWScript.Crucible.JVM.Builtins
     , jvm_alloc_array
     , jvm_setup_with_tag
     , jvm_ghost_value
+    , jvm_equal
     ) where
 
 import           Control.Lens
@@ -1449,6 +1450,25 @@ jvm_ghost_value ::
 jvm_ghost_value ghost val = JVMSetupM $
   ghost_value ghost val
 
+jvm_equal :: SetupValue -> SetupValue -> JVMSetupM ()
+jvm_equal val1 val2 =
+  JVMSetupM $
+  do loc <- getW4Position "jvm_equal"
+     st <- get
+     let cc = st ^. Setup.csCrucibleContext
+         env = MS.csAllocations (st ^. Setup.csMethodSpec)
+         nameEnv = MS.csTypeNames (st ^. Setup.csMethodSpec)
+     ty1 <- typeOfSetupValue cc env nameEnv val1
+     ty2 <- typeOfSetupValue cc env nameEnv val2
+
+     let b = registerCompatible ty1 ty2
+     unless b $ throwCrucibleSetup loc $ unlines
+       [ "Incompatible types when asserting equality:"
+       , show ty1
+       , show ty2
+       ]
+     Setup.crucible_equal loc val1 val2
+
 --------------------------------------------------------------------------------
 
 -- | Sort a list of things and group them into equivalence classes.

src/SAWScript/Crucible/LLVM/Builtins.hs

@@ -2824,14 +2824,7 @@ llvm_equal (getAllLLVM -> val1) (getAllLLVM -> val2) =
        , show ty1
        , show ty2
        ]
-     tags <- view Setup.croTags
-     let md = MS.ConditionMetadata
-              { MS.conditionLoc = loc
-              , MS.conditionTags = tags
-              , MS.conditionType = "equality specification"
-              , MS.conditionContext = ""
-              }
-     Setup.addCondition (MS.SetupCond_Equal md val1 val2)
+     Setup.crucible_equal loc val1 val2
 
 llvm_ghost_value ::
   MS.GhostGlobal ->

src/SAWScript/Crucible/MIR/Builtins.hs

@@ -14,6 +14,7 @@ module SAWScript.Crucible.MIR.Builtins
   , mir_alloc_mut
   , mir_assert
   , mir_execute_func
+  , mir_equal
   , mir_find_adt
   , mir_fresh_cryptol_var
   , mir_fresh_expanded_value
@@ -237,6 +238,25 @@ mir_execute_func args =
      checkArgs 0 argTys args
      Setup.crucible_execute_func args
 
+mir_equal :: SetupValue -> SetupValue -> MIRSetupM ()
+mir_equal val1 val2 =
+  MIRSetupM $
+  do cc <- getMIRCrucibleContext
+     loc <- getW4Position "mir_equal"
+     st <- get
+     let env = MS.csAllocations (st ^. Setup.csMethodSpec)
+         nameEnv = MS.csTypeNames (st ^. Setup.csMethodSpec)
+     ty1 <- typeOfSetupValue cc env nameEnv val1
+     ty2 <- typeOfSetupValue cc env nameEnv val2
+
+     let b = checkCompatibleTys ty1 ty2
+     unless b $ throwCrucibleSetup loc $ unlines
+       [ "Incompatible types when asserting equality:"
+       , show ty1
+       , show ty2
+       ]
+     Setup.crucible_equal loc val1 val2
+
 -- | Consult the given 'Mir.RustModule' to find an 'Mir.Adt'" with the given
 -- 'String' as an identifier and the given 'Mir.Ty's as the types used to
 -- instantiate the type parameters. If such a 'Mir.Adt' cannot be found in the

src/SAWScript/Interpreter.hs

@@ -3922,6 +3922,15 @@ primitives = Map.fromList
     , "method being verified."
     ]
 
+  , prim "jvm_equal" "JVMValue -> JVMValue -> JVMSetup ()"
+    (pureVal jvm_equal)
+    Current
+    [ "State that two JVM values should be equal. Can be used as either a"
+    , "pre-condition or a post-condition. It is semantically equivalent to"
+    , "an `jvm_precond` or `jvm_postcond` statement which is an equality"
+    , "predicate, but potentially more efficient."
+    ]
+
   , prim "jvm_execute_func" "[JVMValue] -> JVMSetup ()"
     (pureVal jvm_execute_func)
     Current
@@ -4037,6 +4046,15 @@ primitives = Map.fromList
     , "String argument represents the variant name."
     ]
 
+  , prim "mir_equal" "MIRValue -> MIRValue -> MIRSetup ()"
+    (pureVal mir_equal)
+    Experimental
+    [ "State that two MIR values should be equal. Can be used as either a"
+    , "pre-condition or a post-condition. It is semantically equivalent to"
+    , "an `mir_precond` or `mir_postcond` statement which is an equality"
+    , "predicate, but potentially more efficient."
+    ]
+
   , prim "mir_execute_func" "[MIRValue] -> MIRSetup ()"
     (pureVal mir_execute_func)
     Experimental