Set and use writability permissions on JVM instance fields and arrays.

Adapt to GaloisInc/crucible#735.

Author: Brian Huffman

deps/crucible

@@ -86,5 +86,6 @@ jvm_verify c "test_b" [set_ov_2] false
 fails (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;
+fails (jvm_verify c "set" [] false set_spec_2 z3);
+
+print "Done.";

intTests/test_jvm_unsound/test.saw

@@ -55,6 +55,7 @@ import           Data.Function
 import           Data.List
 import           Data.Map (Map)
 import qualified Data.Map as Map
+import           Data.Maybe (fromMaybe)
 import           Data.Set (Set)
 import qualified Data.Set as Set
 import qualified Data.Sequence as Seq
@@ -322,6 +323,7 @@ verifyPrestate ::
 verifyPrestate cc mspec globals0 =
   do let sym = cc^.jccBackend
      let jc = cc^.jccJVMContext
+     let halloc = cc^.jccHandleAllocator
      let preallocs = mspec ^. MS.csPreState . MS.csAllocs
      let tyenv = MS.csAllocations mspec
      let nameEnv = mspec ^. MS.csPreState . MS.csVarTypeNames
@@ -338,8 +340,29 @@ verifyPrestate cc mspec globals0 =
      let makeWritable gs fid = CJ.doStaticFieldWritable sym jc gs fid (W4.truePred sym)
      globals0' <- liftIO $ foldM makeWritable globals0 updatedStaticFields
 
+     -- determine which arrays and instance fields need to be writable
+     let addUpdates pt (as, es, fs) =
+           case pt of
+             JVMPointsToField _ a fid _ -> (as, es, Map.insertWith (++) a [fid] fs)
+             JVMPointsToStatic{} -> (as, es, fs)
+             JVMPointsToElem _ a i _ -> (as, Map.insertWith (++) a [i] es, fs)
+             JVMPointsToArray _ a _ -> (Set.insert a as, es, fs)
+     let (updatedArrays, updatedElems, updatedFields) =
+           foldr addUpdates (Set.empty, Map.empty, Map.empty) postPointsTos
+
      -- Allocate objects in memory for each 'jvm_alloc'
-     (env, globals1) <- runStateT (traverse (doAlloc cc . snd) preallocs) globals0'
+     let doAlloc a (_loc, alloc) =
+           case alloc of
+             AllocObject cname ->
+               StateT (CJ.doAllocateObject sym halloc jc cname (flip elem fids))
+               where fids = fromMaybe [] (Map.lookup a updatedFields)
+             AllocArray len ty ->
+               StateT (CJ.doAllocateArray sym halloc jc len ty writable)
+               where
+                 writable
+                   | Set.member a updatedArrays = const True
+                   | otherwise = maybe (const False) (flip elem) (Map.lookup a updatedElems)
+     (env, globals1) <- runStateT (Map.traverseWithKey doAlloc preallocs) globals0'
 
      globals2 <- setupPrePointsTos mspec cc env (mspec ^. MS.csPreState . MS.csPointsTos) globals1
      cs <- setupPrestateConditions mspec cc env (mspec ^. MS.csPreState . MS.csConditions)
@@ -506,21 +529,6 @@ assertEqualVals cc v1 v2 =
 
 --------------------------------------------------------------------------------
 
-doAlloc ::
-  JVMCrucibleContext ->
-  Allocation ->
-  StateT (Crucible.SymGlobalState Sym) IO JVMRefVal
-doAlloc cc alloc =
-  case alloc of
-    AllocObject cname -> StateT (CJ.doAllocateObject sym halloc jc cname)
-    AllocArray len ty -> StateT (CJ.doAllocateArray sym halloc jc len ty)
-  where
-    sym = cc^.jccBackend
-    halloc = cc^.jccHandleAllocator
-    jc = cc^.jccJVMContext
-
---------------------------------------------------------------------------------
-
 getMethodHandle :: CJ.JVMContext -> JVMMethodId -> IO CJ.JVMHandleInfo
 getMethodHandle jc (JVMMethodId mkey cname) =
   case Map.lookup (cname, mkey) (CJ.methodHandles jc) of

src/SAWScript/Crucible/JVM/Builtins.hs

@@ -786,10 +786,13 @@ executeAllocation opts cc (var, (loc, alloc)) =
      let halloc = cc^.jccHandleAllocator
      sym <- Ov.getSymInterface
      globals <- OM (use overrideGlobals)
+     let mut = True -- allocate objects/arrays from post-state as mutable
      (ptr, globals') <-
        case alloc of
-         AllocObject cname -> liftIO $ CJ.doAllocateObject sym halloc jc cname globals
-         AllocArray len elemTy -> liftIO $ CJ.doAllocateArray sym halloc jc len elemTy globals
+         AllocObject cname ->
+           liftIO $ CJ.doAllocateObject sym halloc jc cname (const mut) globals
+         AllocArray len elemTy ->
+           liftIO $ CJ.doAllocateArray sym halloc jc len elemTy (const mut) globals
      OM (overrideGlobals .= globals')
      assignVar cc loc var ptr