Merge pull request #981 from GaloisInc/bh-jvm

Add `jvm_static_field_is` command for specifying static fields in JVM.

intTests/test_jvm_static_fields/Makefile

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

intTests/test_jvm_static_fields/Test.java

@@ -0,0 +1,29 @@
+class A
+{
+    static long x;
+    static long y;
+    static void setX(long v) {
+        x = v;
+    }
+    static void setY(long v) {
+        y = v;
+    }
+    static long getSum() {
+        return x + y;
+    }
+}
+
+class B extends A
+{
+    static long y;
+    static void setY(long v) {
+        y = v;
+    }
+}
+
+class C extends B
+{
+    static long getSum() {
+        return x + y;
+    }
+}

intTests/test_jvm_static_fields/test.saw

@@ -0,0 +1,130 @@
+enable_experimental;
+a <- java_load_class "A";
+print a;
+b <- java_load_class "B";
+c <- java_load_class "C";
+
+print "Verifying class A";
+
+a_setX <-
+  jvm_verify a "setX" [] false
+    do {
+      x <- jvm_fresh_var "x" java_long;
+      v <- jvm_fresh_var "v" java_long;
+      jvm_static_field_is "x" (jvm_term x);
+      jvm_execute_func [jvm_term v];
+      jvm_static_field_is "x" (jvm_term v);
+    }
+    z3;
+
+a_setY <-
+  jvm_verify a "setY" [] false
+    do {
+      y <- jvm_fresh_var "y" java_long;
+      v <- jvm_fresh_var "v" java_long;
+      jvm_static_field_is "y" (jvm_term y);
+      jvm_execute_func [jvm_term v];
+      jvm_static_field_is "y" (jvm_term v);
+    }
+    z3;
+
+a_getSum <-
+  jvm_verify a "getSum" [] false
+    do {
+      x <- jvm_fresh_var "x" java_long;
+      y <- jvm_fresh_var "y" java_long;
+      jvm_static_field_is "x" (jvm_term x);
+      jvm_static_field_is "y" (jvm_term y);
+      jvm_execute_func [];
+      jvm_return (jvm_term {{ x + y }});
+    }
+    z3;
+
+print "Verifying class B";
+
+b_setX <-
+  jvm_verify b "setX" [] false
+    do {
+      x <- jvm_fresh_var "x" java_long;
+      v <- jvm_fresh_var "v" java_long;
+      jvm_static_field_is "x" (jvm_term x);
+      jvm_execute_func [jvm_term v];
+      jvm_static_field_is "x" (jvm_term v);
+    }
+    z3;
+
+b_setY <-
+  jvm_verify b "setY" [] false
+    do {
+      y <- jvm_fresh_var "y" java_long;
+      v <- jvm_fresh_var "v" java_long;
+      jvm_static_field_is "y" (jvm_term y);
+      jvm_execute_func [jvm_term v];
+      jvm_static_field_is "y" (jvm_term v);
+    }
+    z3;
+
+fails (
+  jvm_verify b "getSum" [] false
+    do {
+      x <- jvm_fresh_var "x" java_long;
+      y <- jvm_fresh_var "y" java_long;
+      jvm_static_field_is "x" (jvm_term x);
+      // This fails because "getSum" is inherited from class A,
+      // which has its own static field called "y", which in turn
+      // is shadowed by field "y" from class B.
+      jvm_static_field_is "y" (jvm_term y);
+      jvm_execute_func [];
+      jvm_return (jvm_term {{ x + y }});
+    }
+    z3);
+
+b_getSum <-
+  jvm_verify b "getSum" [] false
+    do {
+      x <- jvm_fresh_var "x" java_long;
+      y <- jvm_fresh_var "y" java_long;
+      jvm_static_field_is "x" (jvm_term x);
+      // Because field "A.y" is shadowed by another field named "y"
+      // in class "B", we must use the qualified field name.
+      jvm_static_field_is "A.y" (jvm_term y);
+      jvm_execute_func [];
+      jvm_return (jvm_term {{ x + y }});
+    }
+    z3;
+
+print "Verifying class C";
+
+c_setX <-
+  jvm_verify c "setX" [] false
+    do {
+      x <- jvm_fresh_var "x" java_long;
+      v <- jvm_fresh_var "v" java_long;
+      jvm_static_field_is "x" (jvm_term x);
+      jvm_execute_func [jvm_term v];
+      jvm_static_field_is "x" (jvm_term v);
+    }
+    z3;
+
+c_setY <-
+  jvm_verify c "setY" [] false
+    do {
+      y <- jvm_fresh_var "y" java_long;
+      v <- jvm_fresh_var "v" java_long;
+      jvm_static_field_is "y" (jvm_term y);
+      jvm_execute_func [jvm_term v];
+      jvm_static_field_is "y" (jvm_term v);
+    }
+    z3;
+
+c_getSum <-
+  jvm_verify c "getSum" [] false
+    do {
+      x <- jvm_fresh_var "x" java_long;
+      y <- jvm_fresh_var "y" java_long;
+      jvm_static_field_is "x" (jvm_term x);
+      jvm_static_field_is "y" (jvm_term y);
+      jvm_execute_func [];
+      jvm_return (jvm_term {{ x + y }});
+    }
+    z3;

intTests/test_jvm_static_fields/test.sh

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

src/SAWScript/Crucible/JVM/Builtins.hs

@@ -32,6 +32,7 @@ module SAWScript.Crucible.JVM.Builtins
     , jvm_postcond
     , jvm_precond
     , jvm_field_is
+    , jvm_static_field_is
     , jvm_elem_is
     , jvm_array_is
     , jvm_fresh_var
@@ -418,6 +419,7 @@ setupPrePointsTos ::
 setupPrePointsTos mspec cc env pts mem0 = foldM doPointsTo mem0 pts
   where
     sym = cc^.jccBackend
+    jc = cc ^. jccJVMContext
     tyenv = MS.csAllocations mspec
     nameEnv = mspec ^. MS.csPreState . MS.csVarTypeNames
 
@@ -436,6 +438,9 @@ setupPrePointsTos mspec cc env pts mem0 = foldM doPointsTo mem0 pts
           do lhs' <- resolveJVMRefVal lhs
              rhs' <- resolveSetupVal cc env tyenv nameEnv rhs
              CJ.doFieldStore sym mem lhs' fid (injectJVMVal sym rhs')
+        JVMPointsToStatic _loc fid rhs ->
+          do rhs' <- resolveSetupVal cc env tyenv nameEnv rhs
+             CJ.doStaticFieldStore sym jc mem fid (injectJVMVal sym rhs')
         JVMPointsToElem _loc lhs idx rhs ->
           do lhs' <- resolveJVMRefVal lhs
              rhs' <- resolveSetupVal cc env tyenv nameEnv rhs
@@ -755,7 +760,11 @@ setupDynamicClassTable sym jc = foldM addClass Map.empty (Map.assocs (CJ.classTa
     setupClass cls =
       do let cname = J.className cls
          name <- W4.stringLit sym (W4S.UnicodeLiteral $ CJ.classNameText (J.className cls))
-         status <- W4.bvLit sym knownRepr (BV.zero knownRepr)
+         -- Set every class to status 2 (initialized). In the absence
+         -- of JVMSetup commands for specifying initialization status,
+         -- this will allow verifications to proceed without the
+         -- interference of any static initializers.
+         status <- W4.bvLit sym knownRepr (BV.mkBV knownRepr 2)
          super <-
            case J.superClass cls of
              Nothing -> return W4.Unassigned
@@ -795,6 +804,8 @@ data JVMSetupError
   | JVMFieldMultiple SetupValue String -- reference and field name
   | JVMFieldFailure String -- TODO: switch to a more structured type
   | JVMFieldTypeMismatch String J.Type J.Type -- field name, expected, found
+  | JVMStaticFailure String -- TODO: switch to a more structured type
+  | JVMStaticTypeMismatch String J.Type J.Type -- field name, expected, found
   | JVMElemNonReference SetupValue Int
   | JVMElemNonArray J.Type
   | JVMElemInvalidIndex J.Type Int Int -- element type, length, index
@@ -832,6 +843,15 @@ instance Show JVMSetupError where
         , "Expected type: " ++ show expected
         , "Given type: " ++ show found
         ]
+      JVMStaticFailure msg ->
+        "jvm_static_field_is: JVM field resolution failed:\n" ++ msg
+      JVMStaticTypeMismatch fname expected found ->
+         -- FIXME: use a pretty printing function for J.Type instead of show
+        unlines
+        [ "jvm_static_field_is: Incompatible types for field " ++ show fname
+        , "Expected type: " ++ show expected
+        , "Given type: " ++ show found
+        ]
       JVMElemNonReference ptr idx ->
         unlines
         [ "jvm_elem_is: Left-hand side is not a valid object reference"
@@ -992,6 +1012,36 @@ jvm_field_is ptr fname val =
        X.throwM $ JVMFieldTypeMismatch fname (J.fieldIdType fid) valTy
      Setup.addPointsTo (JVMPointsToField loc ptr' fid val)
 
+jvm_static_field_is ::
+  BuiltinContext ->
+  Options        ->
+  String     {- ^ field name -} ->
+  SetupValue {- ^ field value -} ->
+  JVMSetupM ()
+jvm_static_field_is _bic _opt fname val =
+  JVMSetupM $
+  do pos <- lift getPosition
+     loc <- SS.toW4Loc "jvm_static_field_is" <$> lift getPosition
+     st <- get
+     let cc = st ^. Setup.csCrucibleContext
+     let cb = cc ^. jccCodebase
+     let env = MS.csAllocations (st ^. Setup.csMethodSpec)
+     let nameEnv = MS.csTypeNames (st ^. Setup.csMethodSpec)
+     let cname =
+           case dropWhileEnd (/= '.') fname of
+             "" -> J.className (cc ^. jccJVMClass)
+             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 fname (J.fieldIdType fid) valTy
+     -- let name = J.unClassName (J.fieldIdClass fid) ++ "." ++ J.fieldIdName fid
+     -- liftIO $ putStrLn $ "resolved to: " ++ name
+     -- TODO: test for multiple points-to conditions on same static field
+     Setup.addPointsTo (JVMPointsToStatic loc fid val)
+
 jvm_elem_is ::
   SetupValue {- ^ array -} ->
   Int        {- ^ index -} ->

src/SAWScript/Crucible/JVM/MethodSpecIR.hs

@@ -128,6 +128,7 @@ 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)
   | JVMPointsToArray ProgramLoc MS.AllocIndex TypedTerm
 
@@ -138,6 +139,10 @@ ppPointsTo =
       MS.ppAllocIndex ptr <> PPL.pretty "." <> PPL.pretty (J.fieldIdName fid)
       PPL.<+> PPL.pretty "points to"
       PPL.<+> 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
     JVMPointsToElem _loc ptr idx val ->
       MS.ppAllocIndex ptr <> PPL.pretty "[" <> PPL.pretty idx <> PPL.pretty "]"
       PPL.<+> PPL.pretty "points to"

src/SAWScript/Crucible/JVM/Override.hs

@@ -451,6 +451,7 @@ matchPointsTos opts sc cc spec prepost = go False []
     -- determine if a precondition is ready to be checked
     checkPointsTo :: JVMPointsTo -> OverrideMatcher CJ.JVM w Bool
     checkPointsTo (JVMPointsToField _loc p _ _) = checkAllocIndex p
+    checkPointsTo (JVMPointsToStatic _loc _ _) = pure True
     checkPointsTo (JVMPointsToElem _loc p _ _) = checkAllocIndex p
     checkPointsTo (JVMPointsToArray _loc p _) = checkAllocIndex p
 
@@ -656,6 +657,7 @@ learnPointsTo ::
 learnPointsTo opts sc cc spec prepost pt = do
   let tyenv = MS.csAllocations spec
   let nameEnv = MS.csTypeNames spec
+  let jc = cc ^. jccJVMContext
   sym <- Ov.getSymInterface
   globals <- OM (use overrideGlobals)
   case pt of
@@ -667,6 +669,12 @@ learnPointsTo opts sc cc spec prepost pt = do
          v <- liftIO $ projectJVMVal sym ty ("field load " ++ J.fieldIdName fid ++ ", " ++ show loc) dyn
          matchArg opts sc cc spec prepost v ty val
 
+    JVMPointsToStatic loc fid val ->
+      do ty <- typeOfSetupValue cc tyenv nameEnv val
+         dyn <- liftIO $ CJ.doStaticFieldLoad sym jc globals fid
+         v <- liftIO $ projectJVMVal sym ty ("static field load " ++ J.fieldIdName fid ++ ", " ++ show loc) dyn
+         matchArg opts sc cc spec prepost v ty val
+
     JVMPointsToElem loc ptr idx val ->
       do ty <- typeOfSetupValue cc tyenv nameEnv val
          rval <- resolveAllocIndexJVM ptr
@@ -801,6 +809,7 @@ executePointsTo ::
 executePointsTo opts sc cc spec pt = do
   sym <- Ov.getSymInterface
   globals <- OM (use overrideGlobals)
+  let jc = cc ^. jccJVMContext
   case pt of
 
     JVMPointsToField _loc ptr fid val ->
@@ -810,6 +819,12 @@ executePointsTo opts sc cc spec pt = do
          globals' <- liftIO $ CJ.doFieldStore sym globals rval fid dyn
          OM (overrideGlobals .= globals')
 
+    JVMPointsToStatic _loc fid val ->
+      do (_, val') <- resolveSetupValueJVM opts cc sc spec val
+         let dyn = injectJVMVal sym val'
+         globals' <- liftIO $ CJ.doStaticFieldStore sym jc globals fid dyn
+         OM (overrideGlobals .= globals')
+
     JVMPointsToElem _loc ptr idx val ->
       do (_, val') <- resolveSetupValueJVM opts cc sc spec val
          rval <- resolveAllocIndexJVM ptr

src/SAWScript/Interpreter.hs

@@ -2713,6 +2713,21 @@ primitives = Map.fromList
     , "about the final memory state after running the function."
     ]
 
+  , prim "jvm_static_field_is" "String -> JVMValue -> JVMSetup ()"
+    (bicVal jvm_static_field_is)
+    Experimental
+    [ "Declare that the named static field contains the given value."
+    , "By default the field name is assumed to belong to the same class"
+    , "as the method being specified. Static fields belonging to other"
+    , "classes can be selected using the \"<classname>.<fieldname>\""
+    , "syntax in the string argument."
+    , ""
+    , "In the pre-state section (before jvm_execute_func) this specifies"
+    , "the initial memory layout before function execution. In the post-state"
+    , "section (after jvm_execute_func), this specifies an assertion"
+    , "about the final memory state after running the function."
+    ]
+
   , prim "jvm_elem_is" "JVMValue -> Int -> JVMValue -> JVMSetup ()"
     (pureVal jvm_elem_is)
     Experimental