From df1de9c2c802c0192eb10ddb1e9165f5ee2896e6 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Wed, 12 May 2021 09:46:53 -0700 Subject: [PATCH 1/7] Set and use writability permissions on JVM instance fields and arrays. Adapt to GaloisInc/crucible#735. --- deps/crucible | 2 +- intTests/test_jvm_unsound/test.saw | 5 ++-- src/SAWScript/Crucible/JVM/Builtins.hs | 40 +++++++++++++++----------- src/SAWScript/Crucible/JVM/Override.hs | 7 +++-- 4 files changed, 33 insertions(+), 21 deletions(-) diff --git a/deps/crucible b/deps/crucible index 9d0347a5d6..31e3976444 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 9d0347a5d644ef5c916a4f483e7822990743ab72 +Subproject commit 31e397644411598b1fee7f6145ef9bf9d46a438f diff --git a/intTests/test_jvm_unsound/test.saw b/intTests/test_jvm_unsound/test.saw index 21a598202b..636fa2a8f8 100644 --- a/intTests/test_jvm_unsound/test.saw +++ b/intTests/test_jvm_unsound/test.saw @@ -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."; diff --git a/src/SAWScript/Crucible/JVM/Builtins.hs b/src/SAWScript/Crucible/JVM/Builtins.hs index 547aed569b..ee6a8a8a80 100644 --- a/src/SAWScript/Crucible/JVM/Builtins.hs +++ b/src/SAWScript/Crucible/JVM/Builtins.hs @@ -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 diff --git a/src/SAWScript/Crucible/JVM/Override.hs b/src/SAWScript/Crucible/JVM/Override.hs index 10766d77de..e50344c078 100644 --- a/src/SAWScript/Crucible/JVM/Override.hs +++ b/src/SAWScript/Crucible/JVM/Override.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 From 3926fecccba4c9b32affe78aef73e953020da30d Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Wed, 12 May 2021 10:56:58 -0700 Subject: [PATCH 2/7] Update examples/java/get.saw to use jvm_modifies declarations. --- examples/java/get.saw | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/examples/java/get.saw b/examples/java/get.saw index 868de2ba7b..f07adfa42e 100644 --- a/examples/java/get.saw +++ b/examples/java/get.saw @@ -9,7 +9,11 @@ jvm_verify c "get" [] false j <- jvm_fresh_var "j" java_int; jvm_precond {{ j <= 3 }}; jvm_execute_func [this, a, jvm_term j]; - // TODO: Update spec to say `a` is modified but not specified + // TODO: Add declaration to say that the entire array is modified. + jvm_modifies_elem a 0; + jvm_modifies_elem a 1; + jvm_modifies_elem a 2; + jvm_modifies_elem a 3; jvm_return (jvm_term {{ j }}); } abc; From c7271f5156e9d4e74cfe7fb7f9c36b018c7df894 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Wed, 12 May 2021 14:34:44 -0700 Subject: [PATCH 3/7] Add `jvm_modifies_array` primitive. --- examples/java/get.saw | 6 +-- src/SAWScript/Crucible/JVM/Builtins.hs | 44 +++++++++++++++------- src/SAWScript/Crucible/JVM/MethodSpecIR.hs | 4 +- src/SAWScript/Crucible/JVM/Override.hs | 13 ++++++- src/SAWScript/Interpreter.hs | 12 ++++++ 5 files changed, 57 insertions(+), 22 deletions(-) diff --git a/examples/java/get.saw b/examples/java/get.saw index f07adfa42e..aaae7633a6 100644 --- a/examples/java/get.saw +++ b/examples/java/get.saw @@ -9,11 +9,7 @@ jvm_verify c "get" [] false j <- jvm_fresh_var "j" java_int; jvm_precond {{ j <= 3 }}; jvm_execute_func [this, a, jvm_term j]; - // TODO: Add declaration to say that the entire array is modified. - jvm_modifies_elem a 0; - jvm_modifies_elem a 1; - jvm_modifies_elem a 2; - jvm_modifies_elem a 3; + jvm_modifies_array a; jvm_return (jvm_term {{ j }}); } abc; diff --git a/src/SAWScript/Crucible/JVM/Builtins.hs b/src/SAWScript/Crucible/JVM/Builtins.hs index ee6a8a8a80..c846c12c8f 100644 --- a/src/SAWScript/Crucible/JVM/Builtins.hs +++ b/src/SAWScript/Crucible/JVM/Builtins.hs @@ -34,6 +34,7 @@ module SAWScript.Crucible.JVM.Builtins , jvm_modifies_field , jvm_modifies_static_field , jvm_modifies_elem + , jvm_modifies_array , jvm_field_is , jvm_static_field_is , jvm_elem_is @@ -476,7 +477,7 @@ setupPrePointsTos mspec cc env pts mem0 = foldM doPointsTo mem0 pts do let lhs' = lookupAllocIndex env lhs rhs' <- maybe (pure CJ.unassignedJVMValue) injectSetupVal rhs CJ.doArrayStore sym mem lhs' idx rhs' - JVMPointsToArray _loc lhs rhs -> + JVMPointsToArray _loc lhs (Just rhs) -> do sc <- saw_ctx <$> sawCoreState sym let lhs' = lookupAllocIndex env lhs (_ety, tts) <- @@ -486,6 +487,8 @@ setupPrePointsTos mspec cc env pts mem0 = foldM doPointsTo mem0 pts Just x -> pure x rhs' <- traverse (injectSetupVal . MS.SetupTerm) tts doEntireArrayStore sym mem lhs' rhs' + JVMPointsToArray _loc _lhs Nothing -> + pure mem -- This should probably never occur in the prestate section. -- | Collects boolean terms that should be assumed to be true. setupPrestateConditions :: @@ -1146,11 +1149,22 @@ generic_elem_is ptr idx mval = X.throwM $ JVMElemMultiple ptr' idx Setup.addPointsTo pt +jvm_modifies_array :: + SetupValue {- ^ array reference -} -> + JVMSetupM () +jvm_modifies_array ptr = generic_array_is ptr Nothing + jvm_array_is :: SetupValue {- ^ array reference -} -> TypedTerm {- ^ array value -} -> JVMSetupM () -jvm_array_is ptr val = +jvm_array_is ptr val = generic_array_is ptr (Just val) + +generic_array_is :: + SetupValue {- ^ array reference -} -> + Maybe TypedTerm {- ^ array value -} -> + JVMSetupM () +generic_array_is ptr mval = JVMSetupM $ do loc <- SS.toW4Loc "jvm_array_is" <$> lift getPosition ptr' <- @@ -1163,17 +1177,21 @@ jvm_array_is ptr val = case snd (lookupAllocIndex env ptr') of AllocObject cname -> X.throwM $ JVMElemNonArray (J.ClassType cname) AllocArray len elTy -> pure (len, elTy) - let schema = ttSchema val - let checkVal = - do ty <- Cryptol.isMono schema - (n, a) <- Cryptol.tIsSeq ty - guard (Cryptol.tIsNum n == Just (toInteger len)) - jty <- toJVMType (Cryptol.evalValType mempty a) - guard (registerCompatible elTy jty) - case checkVal of - Nothing -> X.throwM (JVMArrayTypeMismatch len elTy schema) - Just () -> pure () - let pt = JVMPointsToArray loc ptr' val + case mval of + Nothing -> pure () + Just val -> + case checkVal of + Nothing -> X.throwM (JVMArrayTypeMismatch len elTy schema) + Just () -> pure () + where + schema = ttSchema val + checkVal = + do ty <- Cryptol.isMono schema + (n, a) <- Cryptol.tIsSeq ty + guard (Cryptol.tIsNum n == Just (toInteger len)) + jty <- toJVMType (Cryptol.evalValType mempty a) + guard (registerCompatible elTy jty) + let pt = JVMPointsToArray loc ptr' mval let pts = st ^. Setup.csMethodSpec . MS.csPreState . MS.csPointsTos when (st ^. Setup.csPrePost == PreState && any (overlapPointsTo pt) pts) $ X.throwM $ JVMArrayMultiple ptr' diff --git a/src/SAWScript/Crucible/JVM/MethodSpecIR.hs b/src/SAWScript/Crucible/JVM/MethodSpecIR.hs index a30ace1901..b57a111b39 100644 --- a/src/SAWScript/Crucible/JVM/MethodSpecIR.hs +++ b/src/SAWScript/Crucible/JVM/MethodSpecIR.hs @@ -123,7 +123,7 @@ data JVMPointsTo = JVMPointsToField ProgramLoc MS.AllocIndex J.FieldId (Maybe (MS.SetupValue CJ.JVM)) | JVMPointsToStatic ProgramLoc J.FieldId (Maybe (MS.SetupValue CJ.JVM)) | JVMPointsToElem ProgramLoc MS.AllocIndex Int (Maybe (MS.SetupValue CJ.JVM)) - | JVMPointsToArray ProgramLoc MS.AllocIndex TypedTerm + | JVMPointsToArray ProgramLoc MS.AllocIndex (Maybe TypedTerm) overlapPointsTo :: JVMPointsTo -> JVMPointsTo -> Bool overlapPointsTo = @@ -165,7 +165,7 @@ ppPointsTo = JVMPointsToArray _loc ptr val -> MS.ppAllocIndex ptr PPL.<+> PPL.pretty "points to" - PPL.<+> MS.ppTypedTerm val + PPL.<+> opt MS.ppTypedTerm val where opt = maybe (PPL.pretty "") diff --git a/src/SAWScript/Crucible/JVM/Override.hs b/src/SAWScript/Crucible/JVM/Override.hs index e50344c078..5b65315a3d 100644 --- a/src/SAWScript/Crucible/JVM/Override.hs +++ b/src/SAWScript/Crucible/JVM/Override.hs @@ -692,7 +692,7 @@ learnPointsTo opts sc cc spec prepost pt = do v <- liftIO $ projectJVMVal sym ty ("array load " ++ show idx ++ ", " ++ show loc) dyn matchArg opts sc cc spec prepost v ty val - JVMPointsToArray loc ptr tt -> + JVMPointsToArray loc ptr (Just tt) -> do (len, ety) <- case Cryptol.isMono (ttSchema tt) of Nothing -> fail "jvm_array_is: invalid polymorphic value" @@ -846,7 +846,7 @@ executePointsTo opts sc cc spec pt = do globals' <- liftIO $ CJ.doArrayStore sym globals rval idx dyn OM (overrideGlobals .= globals') - JVMPointsToArray _loc ptr tt -> + JVMPointsToArray _loc ptr (Just tt) -> do (_ety, tts) <- liftIO (destVecTypedTerm sc tt) >>= \case @@ -857,6 +857,15 @@ executePointsTo opts sc cc spec pt = do globals' <- liftIO $ doEntireArrayStore sym globals rval vs OM (overrideGlobals .= globals') + JVMPointsToArray _loc ptr Nothing -> + case Map.lookup ptr (MS.csAllocations spec) of + Just (_, AllocArray len _) -> + do let vs = replicate len CJ.unassignedJVMValue + rval <- resolveAllocIndexJVM ptr + globals' <- liftIO $ doEntireArrayStore sym globals rval vs + OM (overrideGlobals .= globals') + _ -> panic "JVMSetup" ["executePointsTo", "expected array allocation"] + injectSetupValueJVM :: Sym -> Options -> diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 66f84344c2..d9c33d7e26 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -2731,6 +2731,18 @@ primitives = Map.fromList , "nothing about the new value." ] + , prim "jvm_modifies_array" "JVMValue -> JVMSetup ()" + (pureVal jvm_modifies_array) + Experimental + [ "Declare that the indicated array's elements contain unspecified" + , "values." + , "" + , "This lets users write partial specifications of JVM methods." + , "In the post-state section (after `jvm_execute_func`), it" + , "states that the method may modify the array elements, but says" + , "nothing about the new values." + ] + , prim "jvm_field_is" "JVMValue -> String -> JVMValue -> JVMSetup ()" (pureVal jvm_field_is) Experimental From 4188a46bb3d5989b6efc70a1b7751c0c02319053 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Mon, 17 May 2021 11:34:53 -0700 Subject: [PATCH 4/7] Generate errors for `jvm_modifies` declarations in pre-state section. --- src/SAWScript/Crucible/JVM/Builtins.hs | 39 ++++++++++++++++++++------ 1 file changed, 30 insertions(+), 9 deletions(-) diff --git a/src/SAWScript/Crucible/JVM/Builtins.hs b/src/SAWScript/Crucible/JVM/Builtins.hs index c846c12c8f..cd55c40edf 100644 --- a/src/SAWScript/Crucible/JVM/Builtins.hs +++ b/src/SAWScript/Crucible/JVM/Builtins.hs @@ -56,7 +56,7 @@ import Data.Function import Data.List import Data.Map (Map) import qualified Data.Map as Map -import Data.Maybe (fromMaybe) +import Data.Maybe (fromMaybe, isNothing) import Data.Set (Set) import qualified Data.Set as Set import qualified Data.Sequence as Seq @@ -107,6 +107,7 @@ import Verifier.SAW.TypedTerm import Verifier.SAW.Simulator.What4.ReturnTrip import SAWScript.Exceptions +import SAWScript.Panic import SAWScript.Proof import SAWScript.Prover.SolverStats import SAWScript.TopLevel @@ -466,16 +467,16 @@ setupPrePointsTos mspec cc env pts mem0 = foldM doPointsTo mem0 pts doPointsTo :: Crucible.SymGlobalState Sym -> JVMPointsTo -> IO (Crucible.SymGlobalState Sym) doPointsTo mem pt = case pt of - JVMPointsToField _loc lhs fid rhs -> + JVMPointsToField _loc lhs fid (Just rhs) -> do let lhs' = lookupAllocIndex env lhs - rhs' <- maybe (pure CJ.unassignedJVMValue) injectSetupVal rhs + rhs' <- injectSetupVal rhs CJ.doFieldStore sym mem lhs' fid rhs' - JVMPointsToStatic _loc fid rhs -> - do rhs' <- maybe (pure CJ.unassignedJVMValue) injectSetupVal rhs + JVMPointsToStatic _loc fid (Just rhs) -> + do rhs' <- injectSetupVal rhs CJ.doStaticFieldStore sym jc mem fid rhs' - JVMPointsToElem _loc lhs idx rhs -> + JVMPointsToElem _loc lhs idx (Just rhs) -> do let lhs' = lookupAllocIndex env lhs - rhs' <- maybe (pure CJ.unassignedJVMValue) injectSetupVal rhs + rhs' <- injectSetupVal rhs CJ.doArrayStore sym mem lhs' idx rhs' JVMPointsToArray _loc lhs (Just rhs) -> do sc <- saw_ctx <$> sawCoreState sym @@ -487,8 +488,8 @@ setupPrePointsTos mspec cc env pts mem0 = foldM doPointsTo mem0 pts Just x -> pure x rhs' <- traverse (injectSetupVal . MS.SetupTerm) tts doEntireArrayStore sym mem lhs' rhs' - JVMPointsToArray _loc _lhs Nothing -> - pure mem -- This should probably never occur in the prestate section. + _ -> + panic "setupPrePointsTo" ["invalid invariant", "jvm_modifies in pre-state"] -- | Collects boolean terms that should be assumed to be true. setupPrestateConditions :: @@ -829,17 +830,21 @@ data JVMSetupError | JVMFieldMultiple AllocIndex J.FieldId | JVMFieldFailure String -- TODO: switch to a more structured type | JVMFieldTypeMismatch J.FieldId J.Type + | JVMFieldModifyPrestate AllocIndex J.FieldId | JVMStaticMultiple J.FieldId | JVMStaticFailure String -- TODO: switch to a more structured type | JVMStaticTypeMismatch J.FieldId J.Type + | JVMStaticModifyPrestate J.FieldId | JVMElemNonReference SetupValue Int | JVMElemNonArray J.Type | JVMElemInvalidIndex J.Type Int Int -- element type, length, index | JVMElemTypeMismatch Int J.Type J.Type -- index, expected, found | JVMElemMultiple AllocIndex Int -- reference and array index + | JVMElemModifyPrestate AllocIndex Int | JVMArrayNonReference SetupValue | JVMArrayTypeMismatch Int J.Type Cryptol.Schema | JVMArrayMultiple AllocIndex + | JVMArrayModifyPrestate AllocIndex | JVMArgTypeMismatch Int J.Type J.Type -- argument position, expected, found | JVMArgNumberWrong Int Int -- number expected, number found | JVMReturnUnexpected J.Type -- found @@ -871,6 +876,8 @@ instance Show JVMSetupError where , "Expected type: " ++ show (J.fieldIdType fid) , "Given type: " ++ show found ] + JVMFieldModifyPrestate _ptr fid -> + "jvm_modifies_field: Invalid use before jvm_execute_func (" ++ J.fieldIdName fid ++ ")" JVMStaticMultiple fid -> "jvm_static_field_is: Multiple specifications for the same static field (" ++ J.fieldIdName fid ++ ")" JVMStaticFailure msg -> @@ -882,6 +889,8 @@ instance Show JVMSetupError where , "Expected type: " ++ show (J.fieldIdType fid) , "Given type: " ++ show found ] + JVMStaticModifyPrestate fid -> + "jvm_modifies_static_field: Invalid use before jvm_execute_func (" ++ J.fieldIdName fid ++ ")" JVMElemNonReference ptr idx -> unlines [ "jvm_elem_is: Left-hand side is not a valid object reference" @@ -905,6 +914,8 @@ instance Show JVMSetupError where ] JVMElemMultiple _ptr idx -> "jvm_elem_is: Multiple specifications for the same array index (" ++ show idx ++ ")" + JVMElemModifyPrestate _ptr idx -> + "jvm_modifies_elem: Invalid use before jvm_execute_func (" ++ show idx ++ ")" JVMArrayNonReference ptr -> unlines [ "jvm_array_is: Left-hand side is not a valid object reference" @@ -919,6 +930,8 @@ instance Show JVMSetupError where ] JVMArrayMultiple _ptr -> "jvm_array_is: Multiple specifications for the same array reference" + JVMArrayModifyPrestate _ptr -> + "jvm_modifies_array: Invalid use before jvm_execute_func" JVMArgTypeMismatch i expected found -> unlines [ "jvm_execute_func: Argument type mismatch" @@ -1055,6 +1068,8 @@ generic_field_is ptr fname mval = let pts = st ^. Setup.csMethodSpec . MS.csPreState . MS.csPointsTos when (st ^. Setup.csPrePost == PreState && any (overlapPointsTo pt) pts) $ X.throwM $ JVMFieldMultiple ptr' fid + when (st ^. Setup.csPrePost == PreState && isNothing mval) $ + X.throwM $ JVMFieldModifyPrestate ptr' fid Setup.addPointsTo pt jvm_modifies_static_field :: @@ -1100,6 +1115,8 @@ generic_static_field_is fname mval = let pts = st ^. Setup.csMethodSpec . MS.csPreState . MS.csPointsTos when (st ^. Setup.csPrePost == PreState && any (overlapPointsTo pt) pts) $ X.throwM $ JVMStaticMultiple fid + when (st ^. Setup.csPrePost == PreState && isNothing mval) $ + X.throwM $ JVMStaticModifyPrestate fid Setup.addPointsTo pt jvm_modifies_elem :: @@ -1147,6 +1164,8 @@ generic_elem_is ptr idx mval = let pts = st ^. Setup.csMethodSpec . MS.csPreState . MS.csPointsTos when (st ^. Setup.csPrePost == PreState && any (overlapPointsTo pt) pts) $ X.throwM $ JVMElemMultiple ptr' idx + when (st ^. Setup.csPrePost == PreState && isNothing mval) $ + X.throwM $ JVMElemModifyPrestate ptr' idx Setup.addPointsTo pt jvm_modifies_array :: @@ -1195,6 +1214,8 @@ generic_array_is ptr mval = let pts = st ^. Setup.csMethodSpec . MS.csPreState . MS.csPointsTos when (st ^. Setup.csPrePost == PreState && any (overlapPointsTo pt) pts) $ X.throwM $ JVMArrayMultiple ptr' + when (st ^. Setup.csPrePost == PreState && isNothing mval) $ + X.throwM $ JVMArrayModifyPrestate ptr' Setup.addPointsTo pt jvm_precond :: TypedTerm -> JVMSetupM () From f9f4e15c529754a4f92d820c971ddc5825a143b8 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Mon, 17 May 2021 16:10:50 -0700 Subject: [PATCH 5/7] Extend `test_jvm_setup_errors` to include new `jvm_modifies` errors. --- intTests/test_jvm_setup_errors/Test.class | Bin 678 -> 767 bytes intTests/test_jvm_setup_errors/Test.java | 5 ++ intTests/test_jvm_setup_errors/test.saw | 54 ++++++++++++++++++++++ 3 files changed, 59 insertions(+) diff --git a/intTests/test_jvm_setup_errors/Test.class b/intTests/test_jvm_setup_errors/Test.class index 9458edd4fcdd06da31eded64a49dae353796086b..ce089f1f21165bf3f85fb59d4f3c166666a3e144 100644 GIT binary patch literal 767 zcmZvZOK;Oa6ot>&PMo+dP2Ex+1zMnh6C|=>fds0MkdPV$5Ngx~T}|9k>(10RevFz)h zQy#j7P8HhWRMCCK6szX9OC23O)5kTp znPl0~Vk{Y}@iyzB5wnS0wAQULfao6XpI5&FVpgwY8!LN!W zNEaOaX#vh*fjgjsMMkD#s}_HO^?|8bvHM?ffTdcz37apw>#co-_4jD6>REpGTt!%^ zJ^VSoiDmkb_ReFaX1%0aaT@g4$X$MK-oka>!Li>nYR_1jpJ4`PmI7R$IfaX?Zouk1 z=C8#iT(0pC2p7E5TkZdAvoiy9u!<|JVoQ(u>`m{gkMQ1k; zx0m_J)hHK)=lR|J?sYcKECS3~_%KCB+KHwIAbhNpKb(M-u(*)cW5k*%`+|AKw$fTG zFas9Ra9Tz~sA(^KgL+{>;TJal!c8ny@DZ=jWK7z9hkBjSdl79wf1hS N1Y4v9ZDv}b^8?n#9y0&{ diff --git a/intTests/test_jvm_setup_errors/Test.java b/intTests/test_jvm_setup_errors/Test.java index 4e46e8df4c..5f832c9976 100644 --- a/intTests/test_jvm_setup_errors/Test.java +++ b/intTests/test_jvm_setup_errors/Test.java @@ -1,6 +1,7 @@ class Test { long val; + static long counter; long get () { return val; @@ -14,4 +15,8 @@ boolean lessThan (Test t) { static long lookup (long arr[], int idx) { return arr[idx]; } + static long next () { + counter = counter + 1; + return counter; + } } diff --git a/intTests/test_jvm_setup_errors/test.saw b/intTests/test_jvm_setup_errors/test.saw index eadafce504..9627779cc2 100644 --- a/intTests/test_jvm_setup_errors/test.saw +++ b/intTests/test_jvm_setup_errors/test.saw @@ -120,6 +120,38 @@ check_fails test "get" jvm_return (jvm_term val); }; +print "jvm_modifies_field in pre-state section"; +check_fails test "get" + do { + this <- jvm_alloc_object "Test"; + val <- jvm_fresh_var "val" java_long; + jvm_modifies_field this "val"; + jvm_execute_func [this]; + jvm_return (jvm_term val); + }; + +print "Working spec for method 'next'"; +jvm_verify test "next" [] false + do { + ctr <- jvm_fresh_var "ctr" java_long; + jvm_static_field_is "counter" (jvm_term ctr); + jvm_execute_func []; + let ctr' = {{ ctr + 1 }}; + jvm_static_field_is "counter" (jvm_term ctr'); + jvm_return (jvm_term ctr'); + } z3; + +print "jvm_modifies_static_field in pre-state section"; +check_fails test "next" + do { + ctr <- jvm_fresh_var "ctr" java_long; + jvm_modifies_static_field "counter"; + jvm_execute_func []; + let ctr' = {{ ctr + 1 }}; + jvm_static_field_is "counter" (jvm_term ctr'); + jvm_return (jvm_term ctr'); + }; + print "Working spec for method 'lookup'"; jvm_verify test "lookup" [] false do { @@ -233,6 +265,17 @@ check_fails test "lookup" jvm_return (jvm_term x); }; +print "jvm_modifies_elem in pre-state section"; +check_fails test "lookup" + do { + arr <- jvm_alloc_array 8 java_long; + let idx = {{ 2 : [32] }}; + x <- jvm_fresh_var "x" java_long; + jvm_modifies_elem arr 2; + jvm_execute_func [arr, jvm_term idx]; + jvm_return (jvm_term x); + }; + print "Working spec for method 'lookup' (jvm_array_is)"; jvm_verify test "lookup" [] false do { @@ -356,6 +399,17 @@ check_fails test "lookup" jvm_return (jvm_term {{ xs @ idx }}); }; +print "jvm_modifies_array in pre-state section"; +check_fails test "lookup" + do { + arr <- jvm_alloc_array 8 java_long; + let idx = {{ 2 : [32] }}; + x <- jvm_fresh_var "x" java_long; + jvm_modifies_array arr; + jvm_execute_func [arr, jvm_term idx]; + jvm_return (jvm_term x); + }; + print "Working spec for method 'set'"; jvm_verify test "set" [] false do { From e6a0fb6df58174cd6323c1faf9ae647db345d3a5 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Mon, 17 May 2021 16:24:13 -0700 Subject: [PATCH 6/7] Add missing tests about `jvm_static_field_is` to `test_jvm_setup_errors`. --- intTests/test_jvm_setup_errors/test.saw | 56 +++++++++++++++++++++++++ 1 file changed, 56 insertions(+) diff --git a/intTests/test_jvm_setup_errors/test.saw b/intTests/test_jvm_setup_errors/test.saw index 9627779cc2..d92bae4392 100644 --- a/intTests/test_jvm_setup_errors/test.saw +++ b/intTests/test_jvm_setup_errors/test.saw @@ -141,6 +141,62 @@ jvm_verify test "next" [] false jvm_return (jvm_term ctr'); } z3; +print "jvm_static_field_is with non-monomorphic type"; +check_fails test "next" + do { + let ctr = {{ 0 }}; + jvm_static_field_is "counter" (jvm_term ctr); + jvm_execute_func []; + let ctr' = {{ 1 }}; + jvm_static_field_is "counter" (jvm_term ctr'); + jvm_return (jvm_term ctr'); + }; + +print "jvm_static_field_is with non-jvm type"; +check_fails test "next" + do { + let ctr = {{ 0 : Integer }}; + jvm_static_field_is "counter" (jvm_term ctr); + jvm_execute_func []; + let ctr' = {{ ctr + 1 }}; + jvm_static_field_is "counter" (jvm_term ctr'); + jvm_return (jvm_term ctr'); + }; + +print "jvm_static_field_is with wrong type"; +check_fails test "next" + do { + let ctr = {{ 0 : [32] }}; + jvm_static_field_is "counter" (jvm_term ctr); + jvm_execute_func []; + let ctr' = {{ ctr + 1 }}; + jvm_static_field_is "counter" (jvm_term ctr'); + jvm_return (jvm_term ctr'); + }; + +print "jvm_static_field_is with non-existent field name"; +check_fails test "next" + do { + ctr <- jvm_fresh_var "ctr" java_long; + jvm_static_field_is "count" (jvm_term ctr); + jvm_execute_func []; + let ctr' = {{ ctr + 1 }}; + jvm_static_field_is "count" (jvm_term ctr'); + jvm_return (jvm_term ctr'); + }; + +print "jvm_static_field_is with previous jvm_static_field_is on same field"; +check_fails test "next" + do { + ctr <- jvm_fresh_var "ctr" java_long; + jvm_static_field_is "counter" (jvm_term ctr); + jvm_static_field_is "counter" (jvm_term ctr); + jvm_execute_func []; + let ctr' = {{ ctr + 1 }}; + jvm_static_field_is "counter" (jvm_term ctr'); + jvm_return (jvm_term ctr'); + }; + print "jvm_modifies_static_field in pre-state section"; check_fails test "next" do { From ed814c8c5168b86628b6a5eef66c0ca8c1ba97aa Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Tue, 18 May 2021 18:06:01 -0700 Subject: [PATCH 7/7] Add new regression test for jvm_modifies declarations. --- intTests/test_jvm_modifies/Makefile | 2 + intTests/test_jvm_modifies/Test.class | Bin 0 -> 920 bytes intTests/test_jvm_modifies/Test.java | 31 +++++ intTests/test_jvm_modifies/test.saw | 170 ++++++++++++++++++++++++++ intTests/test_jvm_modifies/test.sh | 1 + 5 files changed, 204 insertions(+) create mode 100644 intTests/test_jvm_modifies/Makefile create mode 100644 intTests/test_jvm_modifies/Test.class create mode 100644 intTests/test_jvm_modifies/Test.java create mode 100644 intTests/test_jvm_modifies/test.saw create mode 100644 intTests/test_jvm_modifies/test.sh diff --git a/intTests/test_jvm_modifies/Makefile b/intTests/test_jvm_modifies/Makefile new file mode 100644 index 0000000000..94675b9b1f --- /dev/null +++ b/intTests/test_jvm_modifies/Makefile @@ -0,0 +1,2 @@ +%.class: %.java + javac -g $< diff --git a/intTests/test_jvm_modifies/Test.class b/intTests/test_jvm_modifies/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..e01192f456b0baa996f7499ccc28810a6afd9354 GIT binary patch literal 920 zcma)&OHUJF6o%igop!EVENFo#SV6R%g^ib;gbjhDSYZKSlp^|{+!#<3 z7yJNzl<_^xvr$)2 zn%1PXX&r^!Cnm*}q@Rpd74o(Eo`SVD=*9{Yt)w4sogB5};jV7?SShsz9o^g0!$k6| zXpIh%V=`L1@$u+AU+Zr7wL+oRY}RGaH`@2K{3dm8`SokE6nY4VYSTCY3Xd2y=oNh-`UCZoK@KHq@v5jW#W+YCFpbB|Agiz