Set and use writability permission bits on JVM static fields

intTests/test_jvm_unsound/Makefile

@@ -0,0 +1,2 @@
+%.class: %.java
+	javac -g $<

intTests/test_jvm_unsound/Test.java

@@ -0,0 +1,18 @@
+class Test
+{
+    static int a;
+    int b;
+
+    public void set(int x) {
+        a = x;
+        b = x;
+    }
+    public int test_a(int x) {
+        set(x);
+        return a;
+    }
+    public int test_b(int x) {
+        set(x);
+        return b;
+    }
+}

intTests/test_jvm_unsound/test.saw

@@ -0,0 +1,90 @@
+// This is a regression test for saw-script issue #900; it tests whether
+// `jvm_verify` will successfully verify a spec that does not specify a
+// new value for a field, when the method actually does modify that
+// field. For soundness of compositional verification, it is required
+// that such a verification will fail.
+// https://github.com/GaloisInc/saw-script/issues/900
+
+enable_experimental;
+c <- java_load_class "Test";
+
+let set_spec_1 =
+  do {
+    this <- jvm_alloc_object "Test";
+    x <- jvm_fresh_var "x" java_int;
+    jvm_execute_func [this, jvm_term x];
+    jvm_field_is this "b" (jvm_term x);
+  };
+
+let set_spec_2 =
+  do {
+    this <- jvm_alloc_object "Test";
+    x <- jvm_fresh_var "x" java_int;
+    jvm_execute_func [this, jvm_term x];
+    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;
+
+let one = jvm_term {{ 1:[32] }};
+let two = jvm_term {{ 2:[32] }};
+
+// A correct spec for test_a.
+jvm_verify c "test_a" [] false
+  do {
+    this <- jvm_alloc_object "Test";
+    jvm_static_field_is "a" one;
+    jvm_execute_func [this, two];
+    jvm_static_field_is "a" two;
+    jvm_field_is this "b" two;
+    jvm_return two;
+  }
+  z3;
+
+// An incorrect spec for test_a, which can be proven using the bogus
+// spec set_ov_1.
+jvm_verify c "test_a" [set_ov_1] false
+  do {
+    this <- jvm_alloc_object "Test";
+    jvm_static_field_is "a" one;
+    jvm_execute_func [this, two];
+    jvm_static_field_is "a" one;
+    jvm_field_is this "b" two;
+    jvm_return one;
+  }
+  z3;
+
+// A correct spec for test_b.
+jvm_verify c "test_b" [] false
+  do {
+    this <- jvm_alloc_object "Test";
+    jvm_static_field_is "a" one;
+    jvm_field_is this "b" one;
+    jvm_execute_func [this, two];
+    jvm_static_field_is "a" two;
+    jvm_field_is this "b" two;
+    jvm_return two;
+  }
+  z3;
+
+// An incorrect spec for test_b, which can be proven using the bogus
+// spec set_ov_2.
+jvm_verify c "test_b" [set_ov_2] false
+  do {
+    this <- jvm_alloc_object "Test";
+    jvm_static_field_is "a" one;
+    jvm_field_is this "b" one;
+    jvm_execute_func [this, two];
+    jvm_static_field_is "a" two;
+    jvm_field_is this "b" one;
+    jvm_return one;
+  }
+  z3;
+
+// It should be impossible to verify the bogus set_spec_1.
+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;

intTests/test_jvm_unsound/test.sh

@@ -0,0 +1 @@
+$SAW test.saw

src/SAWScript/Crucible/JVM/Builtins.hs

@@ -31,6 +31,9 @@ module SAWScript.Crucible.JVM.Builtins
     , jvm_execute_func
     , jvm_postcond
     , jvm_precond
+    , jvm_modifies_field
+    , jvm_modifies_static_field
+    , jvm_modifies_elem
     , jvm_field_is
     , jvm_static_field_is
     , jvm_elem_is
@@ -318,6 +321,7 @@ verifyPrestate ::
       Crucible.SymGlobalState Sym)
 verifyPrestate cc mspec globals0 =
   do let sym = cc^.jccBackend
+     let jc = cc^.jccJVMContext
      let preallocs = mspec ^. MS.csPreState . MS.csAllocs
      let tyenv = MS.csAllocations mspec
      let nameEnv = mspec ^. MS.csPreState . MS.csVarTypeNames
@@ -327,9 +331,15 @@ verifyPrestate cc mspec globals0 =
 
      --let cvar = CJ.dynamicClassTable (cc^.jccJVMContext)
      --let Just mem = Crucible.lookupGlobal lvar globals
+     let postPointsTos = mspec ^. MS.csPostState . MS.csPointsTos
+
+     -- make static fields mentioned in post-state section writable
+     let updatedStaticFields = [ fid | JVMPointsToStatic _ fid _ <- postPointsTos ]
+     let makeWritable gs fid = CJ.doStaticFieldWritable sym jc gs fid (W4.truePred sym)
+     globals0' <- liftIO $ foldM makeWritable globals0 updatedStaticFields
 
      -- Allocate objects in memory for each 'jvm_alloc'
-     (env, globals1) <- runStateT (traverse (doAlloc cc . snd) preallocs) globals0
+     (env, globals1) <- runStateT (traverse (doAlloc cc . snd) preallocs) globals0'
 
      globals2 <- setupPrePointsTos mspec cc env (mspec ^. MS.csPreState . MS.csPointsTos) globals1
      cs <- setupPrestateConditions mspec cc env (mspec ^. MS.csPreState . MS.csConditions)
@@ -434,14 +444,14 @@ setupPrePointsTos mspec cc env pts mem0 = foldM doPointsTo mem0 pts
       case pt of
         JVMPointsToField _loc lhs fid rhs ->
           do let lhs' = lookupAllocIndex env lhs
-             rhs' <- injectSetupVal rhs
+             rhs' <- maybe (pure CJ.unassignedJVMValue) injectSetupVal rhs
              CJ.doFieldStore sym mem lhs' fid rhs'
         JVMPointsToStatic _loc fid rhs ->
-          do rhs' <- injectSetupVal rhs
+          do rhs' <- maybe (pure CJ.unassignedJVMValue) injectSetupVal rhs
              CJ.doStaticFieldStore sym jc mem fid rhs'
         JVMPointsToElem _loc lhs idx rhs ->
           do let lhs' = lookupAllocIndex env lhs
-             rhs' <- injectSetupVal rhs
+             rhs' <- maybe (pure CJ.unassignedJVMValue) injectSetupVal rhs
              CJ.doArrayStore sym mem lhs' idx rhs'
         JVMPointsToArray _loc lhs rhs ->
           do sc <- saw_ctx <$> sawCoreState sym
@@ -743,7 +753,10 @@ setupGlobalState sym jc =
   do classTab <- setupDynamicClassTable sym jc
      let classTabVar = CJ.dynamicClassTable jc
      let globals0 = Crucible.insertGlobal classTabVar classTab Crucible.emptyGlobals
-     let declareGlobal var = Crucible.insertGlobal var CJ.unassignedJVMValue
+     let writable = W4.falsePred sym -- static fields default to read-only
+     let declareGlobal info =
+           Crucible.insertGlobal (CJ.staticFieldWritable info) writable .
+           Crucible.insertGlobal (CJ.staticFieldValue info) CJ.unassignedJVMValue
      return $ foldr declareGlobal globals0 (Map.elems (CJ.staticFields jc))
 
 setupDynamicClassTable :: Sym -> CJ.JVMContext -> IO (Crucible.RegValue Sym CJ.JVMClassTableType)
@@ -988,12 +1001,25 @@ jvm_alloc_array len ety =
      Setup.currentState . MS.csAllocs . at n ?= (loc, AllocArray len (typeOfJavaType ety))
      return (MS.SetupVar n)
 
+jvm_modifies_field ::
+  SetupValue {- ^ object -} ->
+  String     {- ^ field name -} ->
+  JVMSetupM ()
+jvm_modifies_field ptr fname = generic_field_is ptr fname Nothing
+
 jvm_field_is ::
   SetupValue {- ^ object -} ->
   String     {- ^ field name -} ->
   SetupValue {- ^ field value -} ->
   JVMSetupM ()
-jvm_field_is ptr fname val =
+jvm_field_is ptr fname val = generic_field_is ptr fname (Just val)
+
+generic_field_is ::
+  SetupValue {- ^ object -} ->
+  String {- ^ field name -} ->
+  Maybe SetupValue {- ^ field value -} ->
+  JVMSetupM ()
+generic_field_is ptr fname mval =
   JVMSetupM $
   do pos <- lift getPosition
      loc <- SS.toW4Loc "jvm_field_is" <$> lift getPosition
@@ -1007,21 +1033,35 @@ jvm_field_is ptr fname val =
      let env = MS.csAllocations (st ^. Setup.csMethodSpec)
      let nameEnv = MS.csTypeNames (st ^. Setup.csMethodSpec)
      ptrTy <- typeOfSetupValue cc env nameEnv ptr
-     valTy <- typeOfSetupValue cc env nameEnv val
      fid <- either (X.throwM . JVMFieldFailure) pure =<< (liftIO $ runExceptT $ findField cb pos ptrTy fname)
-     unless (registerCompatible (J.fieldIdType fid) valTy) $
-       X.throwM $ JVMFieldTypeMismatch fid valTy
-     let pt = JVMPointsToField loc ptr' fid val
+     case mval of
+       Nothing -> pure ()
+       Just val ->
+         do valTy <- typeOfSetupValue cc env nameEnv val
+            unless (registerCompatible (J.fieldIdType fid) valTy) $
+              X.throwM $ JVMFieldTypeMismatch fid valTy
+     let pt = JVMPointsToField loc ptr' fid mval
      let pts = st ^. Setup.csMethodSpec . MS.csPreState . MS.csPointsTos
      when (st ^. Setup.csPrePost == PreState && any (overlapPointsTo pt) pts) $
        X.throwM $ JVMFieldMultiple ptr' fid
      Setup.addPointsTo pt
 
+jvm_modifies_static_field ::
+  String {- ^ field name -} ->
+  JVMSetupM ()
+jvm_modifies_static_field fname = generic_static_field_is fname Nothing
+
 jvm_static_field_is ::
   String     {- ^ field name -} ->
   SetupValue {- ^ field value -} ->
   JVMSetupM ()
-jvm_static_field_is fname val =
+jvm_static_field_is fname val = generic_static_field_is fname (Just val)
+
+generic_static_field_is ::
+  String {- ^ field name -} ->
+  Maybe SetupValue {- ^ field value -} ->
+  JVMSetupM ()
+generic_static_field_is fname mval =
   JVMSetupM $
   do pos <- lift getPosition
      loc <- SS.toW4Loc "jvm_static_field_is" <$> lift getPosition
@@ -1036,24 +1076,40 @@ jvm_static_field_is fname val =
              s -> J.mkClassName (init s)
      -- liftIO $ putStrLn $ "jvm_static_field_is " ++ J.unClassName cname ++ " " ++ fname
      let ptrTy = J.ClassType cname
-     valTy <- typeOfSetupValue cc env nameEnv val
      fid <- either (X.throwM . JVMStaticFailure) pure =<< (liftIO $ runExceptT $ findField cb pos ptrTy fname)
-     unless (registerCompatible (J.fieldIdType fid) valTy) $
-       X.throwM $ JVMStaticTypeMismatch fid valTy
+     case mval of
+       Nothing -> pure ()
+       Just val ->
+         do valTy <- typeOfSetupValue cc env nameEnv val
+            unless (registerCompatible (J.fieldIdType fid) valTy) $
+              X.throwM $ JVMStaticTypeMismatch fid valTy
      -- let name = J.unClassName (J.fieldIdClass fid) ++ "." ++ J.fieldIdName fid
      -- liftIO $ putStrLn $ "resolved to: " ++ name
-     let pt = JVMPointsToStatic loc fid val
+     let pt = JVMPointsToStatic loc fid mval
      let pts = st ^. Setup.csMethodSpec . MS.csPreState . MS.csPointsTos
      when (st ^. Setup.csPrePost == PreState && any (overlapPointsTo pt) pts) $
        X.throwM $ JVMStaticMultiple fid
      Setup.addPointsTo pt
 
+jvm_modifies_elem ::
+  SetupValue {- ^ array -} ->
+  Int        {- ^ index -} ->
+  JVMSetupM ()
+jvm_modifies_elem ptr idx = generic_elem_is ptr idx Nothing
+
 jvm_elem_is ::
   SetupValue {- ^ array -} ->
   Int        {- ^ index -} ->
   SetupValue {- ^ element value -} ->
   JVMSetupM ()
-jvm_elem_is ptr idx val =
+jvm_elem_is ptr idx val = generic_elem_is ptr idx (Just val)
+
+generic_elem_is ::
+  SetupValue {- ^ array -} ->
+  Int {- ^ index -} ->
+  Maybe SetupValue {- ^ element value -} ->
+  JVMSetupM ()
+generic_elem_is ptr idx mval =
   JVMSetupM $
   do loc <- SS.toW4Loc "jvm_elem_is" <$> lift getPosition
      ptr' <-
@@ -1068,12 +1124,15 @@ jvm_elem_is ptr idx val =
        case snd (lookupAllocIndex env ptr') of
          AllocObject cname -> X.throwM $ JVMElemNonArray (J.ClassType cname)
          AllocArray len elTy -> pure (len, elTy)
-     valTy <- typeOfSetupValue cc env nameEnv val
      unless (0 <= idx && idx < len) $
        X.throwM $ JVMElemInvalidIndex elTy len idx
-     unless (registerCompatible elTy valTy) $
-       X.throwM $ JVMElemTypeMismatch idx elTy valTy
-     let pt = JVMPointsToElem loc ptr' idx val
+     case mval of
+       Nothing -> pure ()
+       Just val ->
+         do valTy <- typeOfSetupValue cc env nameEnv val
+            unless (registerCompatible elTy valTy) $
+              X.throwM $ JVMElemTypeMismatch idx elTy valTy
+     let pt = JVMPointsToElem loc 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

src/SAWScript/Crucible/JVM/MethodSpecIR.hs

@@ -120,9 +120,9 @@ type instance MS.AllocSpec CJ.JVM = (ProgramLoc, Allocation)
 type instance MS.PointsTo CJ.JVM = JVMPointsTo
 
 data JVMPointsTo
-  = JVMPointsToField ProgramLoc MS.AllocIndex J.FieldId (MS.SetupValue CJ.JVM)
-  | JVMPointsToStatic ProgramLoc J.FieldId (MS.SetupValue CJ.JVM)
-  | JVMPointsToElem ProgramLoc MS.AllocIndex Int (MS.SetupValue CJ.JVM)
+  = 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
 
 overlapPointsTo :: JVMPointsTo -> JVMPointsTo -> Bool
@@ -153,19 +153,21 @@ ppPointsTo =
     JVMPointsToField _loc ptr fid val ->
       MS.ppAllocIndex ptr <> PPL.pretty "." <> PPL.pretty (J.fieldIdName fid)
       PPL.<+> PPL.pretty "points to"
-      PPL.<+> MS.ppSetupValue val
+      PPL.<+> opt MS.ppSetupValue val
     JVMPointsToStatic _loc fid val ->
       PPL.pretty (J.unClassName (J.fieldIdClass fid)) <> PPL.pretty "." <> PPL.pretty (J.fieldIdName fid)
       PPL.<+> PPL.pretty "points to"
-      PPL.<+> MS.ppSetupValue val
+      PPL.<+> opt MS.ppSetupValue val
     JVMPointsToElem _loc ptr idx val ->
       MS.ppAllocIndex ptr <> PPL.pretty "[" <> PPL.pretty idx <> PPL.pretty "]"
       PPL.<+> PPL.pretty "points to"
-      PPL.<+> MS.ppSetupValue val
+      PPL.<+> opt MS.ppSetupValue val
     JVMPointsToArray _loc ptr val ->
       MS.ppAllocIndex ptr
       PPL.<+> PPL.pretty "points to"
       PPL.<+> MS.ppTypedTerm val
+  where
+    opt = maybe (PPL.pretty "<unspecified>")
 
 instance PPL.Pretty JVMPointsTo where
   pretty = ppPointsTo