Add jvm_modifies_array primitive.

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;

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'

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 "<unspecified>")
 

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              ->

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