From f20ac29aca804e0ed7d03d2269c9dbe78eb64238 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Wed, 12 May 2021 14:34:44 -0700 Subject: [PATCH] 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