Invalidate memory before executing override postcondition (#549)

* Invalidate memory before executing postcondition
* Do not implicitly allocate mutable global variables. Instead, use a new crucible_alloc_global function.
* Refactor unwieldy additions to verifyPrestate and executeCond
* Update integration test suite
* Add some integration tests for issue #30
* Add source location for global allocations
* Bump crucible submodule

Fixes #30.

examples/llvm/global.saw

@@ -11,11 +11,13 @@ let ptr_to_fresh n ty = do {
 };
 
 let clear_setup = do {
+    crucible_alloc_global "g";
     crucible_execute_func [];
     crucible_points_to (crucible_global "g") (crucible_term {{ 0 : [32] }});
 };
 
 let set_setup = do {
+    crucible_alloc_global "g";
     x <- crucible_fresh_var "x" (llvm_int 32);
     crucible_execute_func [crucible_term x];
     crucible_points_to (crucible_global "g") (crucible_term x);
@@ -26,4 +28,4 @@ let main : TopLevel () = do {
     crucible_llvm_verify m "clear" [] false clear_setup abc;
     crucible_llvm_verify m "set" [] false set_setup abc;
     print "Done.";
-};
+};

examples/multi-override/multi-override.saw

@@ -27,6 +27,7 @@ let sum_spec n : CrucibleSetup() = do {
 
   crucible_execute_func[arrp, crucible_term {{ `n:[32]}}];
   crucible_return (crucible_term {{ mysum arr }});
+  crucible_points_to arrp (crucible_term arr);
 };
 
 let example_sums : CrucibleSetup() = do {
@@ -35,6 +36,7 @@ let example_sums : CrucibleSetup() = do {
 };
 
 let set_myglobal n : CrucibleSetup() = do {
+  crucible_alloc_global "myglobal";
   old <- crucible_fresh_var "old" (llvm_int 32);
   crucible_precond {{ old < 1000 }};
   crucible_points_to (crucible_global "myglobal") (crucible_term old);
@@ -44,8 +46,11 @@ let set_myglobal n : CrucibleSetup() = do {
 };
 
 let myglobal_example : CrucibleSetup() = do {
+  crucible_alloc_global "myglobal";
   crucible_execute_func[];
   crucible_return (crucible_term {{ 120 : [32] }});
+  crucible_points_to (crucible_global "myglobal")
+                     (crucible_term {{ 120 : [32] }});
 };
 
 let main : TopLevel () = do {

examples/salsa20/salsa.saw

@@ -60,8 +60,14 @@ let salsa20_djb_setup = do {
 };
 
 let salsa20_expansion_32 = do {
-    (k, pk) <- ptr_to_fresh "k" (llvm_array 32 (llvm_int 8));
-    (n, pn) <- ptr_to_fresh "n" (llvm_array 16 (llvm_int 8));
+    // (k, pk) <- ptr_to_fresh "k" (llvm_array 32 (llvm_int 8));
+    // (n, pn) <- ptr_to_fresh "n" (llvm_array 16 (llvm_int 8));
+    k <- crucible_fresh_var "k" (llvm_array 32 (llvm_int 8));
+    pk <- crucible_alloc_readonly (llvm_array 32 (llvm_int 8));
+    crucible_points_to pk (crucible_term k);
+    n <- crucible_fresh_var "n" (llvm_array 16 (llvm_int 8));
+    pn <- crucible_alloc_readonly (llvm_array 16 (llvm_int 8));
+    crucible_points_to pn (crucible_term n);
     pks <- crucible_alloc (llvm_array 64 (llvm_int 8));
     crucible_execute_func [pk, pn, pks];
     let rks = {{ Salsa20_expansion`{a=2}(k, n)}};

intTests/test0036_global/test.saw

@@ -1,6 +1,7 @@
 m <- llvm_load_module "./test.bc";
 
 let init_global name = do {
+  crucible_alloc_global name;
   crucible_points_to (crucible_global name)
                      (crucible_global_initializer name);
 };

intTests/test_boilerplate/test.c

@@ -4,14 +4,14 @@
 #include <string.h>
 #include <inttypes.h>
 
-uint64_t GLOBAL = 0;
+const uint64_t GLOBAL = 1;
 
 uint64_t test0(uint64_t x, uint64_t y) {
 	return x + y;
 }
 
-void test1() {
-	GLOBAL += test0(GLOBAL, GLOBAL);
+uint64_t test1() {
+	return test0(GLOBAL, GLOBAL);
 }
 
 uint64_t test2(uint64_t *buf) {

intTests/test_llvm_unsound_alloc/test.sh

@@ -0,0 +1,7 @@
+#!/bin/sh
+
+if ! $SAW unsound_alloc.saw ; then
+    exit 0
+else
+    exit 1
+fi

intTests/test_llvm_unsound_alloc/unsound_alloc.c

@@ -0,0 +1,12 @@
+#include <stdint.h>
+
+uint32_t foo(uint32_t *x) {
+	uint32_t tmp = *x + 1;
+	*x += 42;
+	return tmp;
+};
+
+uint32_t bar() {
+	uint32_t val = 1;
+	return foo(&val) + val;
+};

intTests/test_llvm_unsound_alloc/unsound_alloc.saw

@@ -0,0 +1,23 @@
+MODULE <- llvm_load_module "unsound_alloc.bc";
+
+let foo_setup = do {
+  x <- crucible_alloc (llvm_int 32);
+  x_star <- crucible_fresh_var "x" (llvm_int 32);
+  crucible_points_to x (crucible_term x_star);
+  crucible_execute_func [x];
+  crucible_return (crucible_term {{ x_star + 1 : [32] }});
+};
+foo_spec <- crucible_llvm_verify MODULE "foo" [] false foo_setup z3;
+
+let bar_setup = do {
+  crucible_execute_func [];
+  crucible_return (crucible_term {{ 3 : [32] }});
+};
+
+// the below line (without override) correctly fails
+// crucible_llvm_verify MODULE "bar" [] false bar_setup z3;
+
+// works, but shouldn't
+crucible_llvm_verify MODULE "bar" [foo_spec] false bar_setup z3;
+
+print "Should not have succeeded - unsound!";

intTests/test_llvm_unsound_global/test.sh

@@ -0,0 +1,7 @@
+#!/bin/sh
+
+if ! $SAW unsound_global.saw ; then
+    exit 0
+else
+    exit 1
+fi

intTests/test_llvm_unsound_global/unsound_global.c

@@ -0,0 +1,22 @@
+// unsound_global.c
+
+#include <stdint.h>
+#include <stdio.h>
+
+uint32_t TEST;
+
+uint32_t GLOBAL[2];
+
+uint32_t foo(uint32_t x) {
+	GLOBAL[1] = x;
+	return x + 1;
+};
+
+uint32_t bar() {
+	TEST = 42;
+	GLOBAL[1] = 0;
+	uint32_t val = foo(1);
+	printf("%u\n", TEST);
+	// GLOBAL[1] = 0;
+	return val + GLOBAL[1];
+};

intTests/test_llvm_unsound_global/unsound_global.saw

@@ -0,0 +1,25 @@
+MODULE <- llvm_load_module "unsound_global.bc";
+
+let foo_setup = do {
+  crucible_alloc_global "GLOBAL";
+  x <- crucible_fresh_var "x" (llvm_int 32);
+  crucible_execute_func [crucible_term x];
+  crucible_return (crucible_term {{ x + 1 : [32] }});
+  // crucible_points_to (crucible_elem (crucible_global "GLOBAL") 1) (crucible_term x);
+};
+foo_spec <- crucible_llvm_verify MODULE "foo" [] false foo_setup z3;
+
+let bar_setup = do {
+  crucible_alloc_global "GLOBAL";
+  crucible_alloc_global "TEST";
+  crucible_execute_func [];
+  crucible_return (crucible_term {{ 2 : [32] }});
+};
+
+// the below line (without override) correctly fails
+// crucible_llvm_verify MODULE "bar" [] false bar_setup z3;
+
+// works, but shouldn't
+crucible_llvm_verify MODULE "bar" [foo_spec] false bar_setup z3;
+
+print "Should not have succeeded - unsound!";

src/SAWScript/Crucible/Common/MethodSpec.hs

@@ -298,6 +298,9 @@ type family ExtType ext :: Type
 -- | The type of points-to assertions
 type family PointsTo ext :: Type
 
+-- | The type of global allocations
+type family AllocGlobal ext :: Type
+
 --------------------------------------------------------------------------------
 -- *** StateSpec
 
@@ -362,6 +365,7 @@ data CrucibleMethodSpecIR ext =
   , _csPostState       :: StateSpec ext -- ^ state after the function runs
   , _csArgBindings     :: Map Integer (ExtType ext, SetupValue ext) -- ^ function arguments
   , _csRetValue        :: Maybe (SetupValue ext) -- ^ function return value
+  , _csGlobalAllocs    :: [AllocGlobal ext] -- ^ globals allocated
   , _csSolverStats     :: SolverStats -- ^ statistics about the proof that produced this
   , _csCodebase        :: Codebase ext -- ^ the codebase this spec was verified against
   , _csLoc             :: ProgramLoc -- ^ where in the SAWscript was this spec?
@@ -410,6 +414,7 @@ makeCrucibleMethodSpecIR meth args ret loc code = do
     ,_csPostState       = initialStateSpec
     ,_csArgBindings     = Map.empty
     ,_csRetValue        = Nothing
+    ,_csGlobalAllocs    = []
     ,_csSolverStats     = mempty
     ,_csLoc             = loc
     ,_csCodebase        = code

src/SAWScript/Crucible/Common/Override.hs

@@ -124,7 +124,7 @@ makeLenses ''OverrideState
 initialState ::
   Sym                           {- ^ simulator                      -} ->
   Crucible.SymGlobalState Sym   {- ^ initial global variables       -} ->
-  Map AllocIndex (Pointer ext) {- ^ initial allocation substituion -} ->
+  Map AllocIndex (Pointer ext)  {- ^ initial allocation substituion -} ->
   Map VarIndex Term             {- ^ initial term substituion       -} ->
   Set VarIndex                  {- ^ initial free terms             -} ->
   W4.ProgramLoc                 {- ^ location information for the override -} ->

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

@@ -26,6 +26,7 @@ module SAWScript.Crucible.Common.Setup.Type
   , CrucibleSetupT
   , currentState
   , addPointsTo
+  , addAllocGlobal
   , addCondition
   , freshVariable
   ) where
@@ -86,6 +87,9 @@ currentState f x = case x^. csPrePost of
 addPointsTo :: Monad m => MS.PointsTo ext -> CrucibleSetupT ext m ()
 addPointsTo pt = currentState . MS.csPointsTos %= (pt : )
 
+addAllocGlobal :: Monad m => MS.AllocGlobal ext -> CrucibleSetupT ext m ()
+addAllocGlobal ag = csMethodSpec . MS.csGlobalAllocs %= (ag : )
+
 addCondition :: Monad m => MS.SetupCondition ext -> CrucibleSetupT ext m ()
 addCondition cond = currentState . MS.csConditions %= (cond : )