Add a invalidation pass for pre-state allocations in jvm_verify.

This ensures that executing an incomplete override, which omits
some field modifications that are not mentioned in the override
spec, will not lead to unsoundness.

Fixes #900.

intTests/test_jvm_unsound/test.saw

@@ -8,6 +8,7 @@
 enable_experimental;
 c <- java_load_class "Test";
 
+// An incomplete spec for method "set".
 let set_spec_1 =
   do {
     this <- jvm_alloc_object "Test";
@@ -16,6 +17,7 @@ let set_spec_1 =
     jvm_field_is this "b" (jvm_term x);
   };
 
+// Another incomplete spec for method "set".
 let set_spec_2 =
   do {
     this <- jvm_alloc_object "Test";
@@ -24,8 +26,8 @@ let set_spec_2 =
     jvm_static_field_is "a" (jvm_term x);
   };
 
-set_ov_1 <- jvm_unsafe_assume_spec c "set" set_spec_1;
-set_ov_2 <- jvm_unsafe_assume_spec c "set" set_spec_2;
+set_ov_1 <- jvm_verify c "set" [] false set_spec_1 z3;
+set_ov_2 <- jvm_verify c "set" [] false set_spec_2 z3;
 
 let one = jvm_term {{ 1:[32] }};
 let two = jvm_term {{ 2:[32] }};
@@ -44,6 +46,7 @@ jvm_verify c "test_a" [] false
 
 // An incorrect spec for test_a, which can be proven using the bogus
 // spec set_ov_1.
+// FIXME: this should fail
 jvm_verify c "test_a" [set_ov_1] false
   do {
     this <- jvm_alloc_object "Test";
@@ -68,8 +71,9 @@ jvm_verify c "test_b" [] false
   }
   z3;
 
-// An incorrect spec for test_b, which can be proven using the bogus
-// spec set_ov_2.
+// An incorrect spec for test_b, which would be provable using the
+// incomplete spec set_ov_2, if not for the memory invalidation pass.
+fails (
 jvm_verify c "test_b" [set_ov_2] false
   do {
     this <- jvm_alloc_object "Test";
@@ -80,12 +84,5 @@ jvm_verify c "test_b" [set_ov_2] false
     jvm_field_is this "b" one;
     jvm_return one;
   }
-  z3;
-
-// It should be impossible to verify the bogus set_spec_1.
-// FIXME: this should fail
-jvm_verify c "set" [] false set_spec_1 z3;
-
-// It should be impossible to verify the bogus set_spec_2.
-// FIXME: this should fail
-jvm_verify c "set" [] false set_spec_2 z3;
+  z3
+);

src/SAWScript/Crucible/JVM/Override.hs

@@ -308,13 +308,13 @@ methodSpecHandler_prestate opts sc cc args cs =
 --   which involves writing values into memory, computing the return value,
 --   and computing postcondition predicates.
 methodSpecHandler_poststate ::
-  forall ret w.
+  forall ret.
   Options                  {- ^ output/verbosity options                     -} ->
   SharedContext            {- ^ context for constructing SAW terms           -} ->
   JVMCrucibleContext          {- ^ context for interacting with Crucible        -} ->
   Crucible.TypeRepr ret    {- ^ type representation of function return value -} ->
   CrucibleMethodSpecIR     {- ^ specification for current function override  -} ->
-  OverrideMatcher CJ.JVM w (Crucible.RegValue Sym ret)
+  OverrideMatcher CJ.JVM RW (Crucible.RegValue Sym ret)
 methodSpecHandler_poststate opts sc cc retTy cs =
   do executeCond opts sc cc cs (cs ^. MS.csPostState)
      computeReturnValue opts cc sc cs retTy (cs ^. MS.csRetValue)
@@ -354,16 +354,17 @@ enforceCompleteSubstitution loc ss =
      unless (null missing) (failure loc (AmbiguousVars missing))
 
 
--- execute a pre/post condition
+-- | Execute a post condition.
 executeCond ::
   Options ->
   SharedContext ->
   JVMCrucibleContext ->
   CrucibleMethodSpecIR ->
   StateSpec ->
-  OverrideMatcher CJ.JVM w ()
+  OverrideMatcher CJ.JVM RW ()
 executeCond opts sc cc cs ss =
   do refreshTerms sc ss
+     invalidateAllocs cc cs
      traverse_ (executeAllocation opts cc) (Map.assocs (ss ^. MS.csAllocs))
      traverse_ (executePointsTo opts sc cc cs) (ss ^. MS.csPointsTos)
      traverse_ (executeSetupCondition opts sc cc cs) (ss ^. MS.csConditions)
@@ -764,6 +765,38 @@ learnPred sc cc loc prepost t =
 
 ------------------------------------------------------------------------
 
+-- | Invalidate all memory that was allocated in the method spec
+-- precondition using either @jvm_alloc_object@ or @jvm_alloc_array@.
+invalidateAllocs ::
+  JVMCrucibleContext ->
+  MS.CrucibleMethodSpecIR CJ.JVM ->
+  OverrideMatcher CJ.JVM RW ()
+invalidateAllocs cc cs =
+  do let allocs = cs ^. MS.csPreState . MS.csAllocs
+     void $ Map.traverseWithKey invalidateAlloc allocs
+  where
+    invalidateAlloc :: AllocIndex -> (W4.ProgramLoc, Allocation) -> OverrideMatcher CJ.JVM RW ()
+    invalidateAlloc i (_loc, alloc) =
+      do sym <- Ov.getSymInterface
+         globals <- OM (use overrideGlobals)
+         ref <- resolveAllocIndexJVM i
+         -- TODO: annotate the value with a descriptive error message.
+         let val = CJ.unassignedJVMValue
+         case alloc of
+           AllocObject cName ->
+             do let jc = cc ^. jccJVMContext
+                let fids = CJ.fieldsOfClassName jc cName
+                let clear g fid = liftIO $ CJ.doFieldStore sym g ref fid val
+                globals' <- foldM clear globals fids
+                OM (overrideGlobals .= globals')
+           AllocArray len _ty ->
+             do let idxs = take len [0..]
+                let clear g idx = liftIO $ CJ.doArrayStore sym g ref idx val
+                globals' <- foldM clear globals idxs
+                OM (overrideGlobals .= globals')
+
+------------------------------------------------------------------------
+
 -- TODO: replace (W4.ProgramLoc, J.Type) by some allocation datatype
 -- that includes constructors for object allocations and array
 -- allocations (with length).