crucible-jvm: Add permission bit for writability to each static field.

The permission bit is asserted to be true on every putstatic instruction.

This feature will allow SAW to use method specs that do not explicitly
specify a final value for each static field; by making those fields
read-only, we can be sure that the values did not change, without having
to explicitly check that the final value is equal to the initial value.

crucible-jvm/src/Lang/Crucible/JVM/Context.hs

@@ -22,6 +22,7 @@ import qualified Language.JVM.Parser as J
 -- crucible
 import Lang.Crucible.CFG.Generator
 import Lang.Crucible.FunctionHandle
+import Lang.Crucible.Types
 
 -- crucible-jvm
 import Lang.Crucible.JVM.Types
@@ -30,7 +31,7 @@ import Lang.Crucible.JVM.Types
 -- * JVMContext
 
 
-type StaticFieldTable = Map J.FieldId (GlobalVar JVMValueType)
+type StaticFieldTable = Map J.FieldId (GlobalVar JVMValueType, GlobalVar BoolType)
 type MethodHandleTable = Map (J.ClassName, J.MethodKey) JVMHandleInfo
 
 data JVMHandleInfo where
@@ -41,8 +42,9 @@ data JVMHandleInfo where
 data JVMContext = JVMContext
  { methodHandles :: Map (J.ClassName, J.MethodKey) JVMHandleInfo
  -- ^ Map from static and dynamic methods to Crucible function handles.
- , staticFields :: Map J.FieldId (GlobalVar JVMValueType)
+ , staticFields :: Map J.FieldId (GlobalVar JVMValueType, GlobalVar BoolType)
  -- ^ Map from static field names to Crucible global variables.
+ -- Each static field is paired with a permission bit for writability.
  -- We know about these fields at translation time so we can allocate
  -- global variables to store them.
  , classTable :: Map J.ClassName J.Class

crucible-jvm/src/Lang/Crucible/JVM/Simulate.hs

@@ -344,7 +344,8 @@ declareStaticField halloc c m f = do
  let fieldId = J.FieldId cn fn (J.fieldType f)
  let str = fn ++ show (J.fieldType f)
  gvar <- C.freshGlobalVar halloc (globalVarName cn str) (knownRepr :: TypeRepr JVMValueType)
- return $ Map.insert fieldId gvar m
+ pvar <- C.freshGlobalVar halloc (globalVarName cn str) (knownRepr :: TypeRepr BoolType)
+ return $ Map.insert fieldId (gvar, pvar) m
 
 
 -- | Create the initial 'JVMContext'.
@@ -470,11 +471,12 @@ mkSimSt sym p halloc ctx verbosity ret k =
  do globals <- Map.foldrWithKey initField (return globals0) (staticFields ctx)
  return $ C.InitialState simctx globals C.defaultAbortHandler ret k
  where
- initField :: J.FieldId -> GlobalVar JVMValueType -> IO (C.SymGlobalState sym) -> IO (C.SymGlobalState sym)
- initField fi var m =
+ initField :: J.FieldId -> (GlobalVar JVMValueType, GlobalVar BoolType) -> IO (C.SymGlobalState sym) -> IO (C.SymGlobalState sym)
+ initField fi (var, perm) m =
  do gs <- m
  z <- zeroValue sym (J.fieldIdType fi)
- return (C.insertGlobal var z gs)
+ let writable = W4.truePred sym -- For crux, default all static fields to writable
+ return (C.insertGlobal perm writable (C.insertGlobal var z gs))
 
  simctx = jvmSimContext sym halloc stdout ctx verbosity p
  globals0 = C.insertGlobal (dynamicClassTable ctx) Map.empty C.emptyGlobals
@@ -829,7 +831,8 @@ doFieldStore sym globals ref fid val =
  EvalStmt.alterRef sym jvmIntrinsicTypes objectRepr ref' (W4.justPartExpr sym obj') globals
 
 -- | Write a value to a static field of a class. The 'FieldId' must
--- have already been resolved (see §5.4.3.2 of the JVM spec).
+-- have already been resolved (see §5.4.3.2 of the JVM spec). Note
+-- that the writability permission of the field is not checked.
 doStaticFieldStore ::
  IsSymInterface sym =>
  sym ->
@@ -841,13 +844,33 @@ doStaticFieldStore ::
 doStaticFieldStore sym jc globals fid val =
  case Map.lookup fid (staticFields jc) of
  Nothing -> C.addFailedAssertion sym msg
- Just gvar ->
+ Just (gvar, _pvar) ->
  do putStrLn $ "doStaticFieldStore " ++ fname
  pure (C.insertGlobal gvar val globals)
  where
  fname = J.unClassName (J.fieldIdClass fid) ++ "." ++ J.fieldIdName fid
  msg = C.GenericSimError $ "Static field store: field not found: " ++ fname
 
+-- | Set the write permission on a static field. The 'FieldId' must
+-- have already been resolved (see §5.4.3.2 of the JVM spec).
+doStaticFieldWritable ::
+ IsSymInterface sym =>
+ sym ->
+ JVMContext ->
+ C.SymGlobalState sym ->
+ J.FieldId ->
+ W4.Pred sym ->
+ IO (C.SymGlobalState sym)
+doStaticFieldWritable sym jc globals fid val =
+ case Map.lookup fid (staticFields jc) of
+ Nothing -> C.addFailedAssertion sym msg
+ Just (_gvar, pvar) ->
+ do putStrLn $ "doStaticFieldWritable " ++ fname
+ pure (C.insertGlobal pvar val globals)
+ where
+ fname = J.unClassName (J.fieldIdClass fid) ++ "." ++ J.fieldIdName fid
+ msg = C.GenericSimError $ "Static field writable: field not found: " ++ fname
+
 -- | Write a value at an index of an array reference.
 doArrayStore ::
  IsSymInterface sym =>
@@ -901,7 +924,7 @@ doStaticFieldLoad ::
 doStaticFieldLoad sym jc globals fid =
  case Map.lookup fid (staticFields jc) of
  Nothing -> C.addFailedAssertion sym msg
- Just gvar ->
+ Just (gvar, _pvar) ->
  case C.lookupGlobal gvar globals of
  Nothing -> C.addFailedAssertion sym msg
  Just v -> pure v

crucible-jvm/src/Lang/Crucible/JVM/Translation/Class.hs

@@ -364,7 +364,7 @@ getStaticFieldValue rawFieldId =
  initializeClass (J.fieldIdClass fieldId)
  ctx <- gets jsContext
  case Map.lookup fieldId (staticFields ctx) of
- Just glob ->
+ Just (glob, _) ->
  do r <- readGlobal glob
  fromJVMDynamic ("getstatic " <> fieldIdText fieldId) (J.fieldIdType fieldId) r
  Nothing ->
@@ -387,8 +387,11 @@ setStaticFieldValue :: J.FieldId -> JVMValue s -> JVMGenerator s ret ()
 setStaticFieldValue fieldId val =
  do ctx <- gets jsContext
  case Map.lookup fieldId (staticFields ctx) of
- Just glob ->
- writeGlobal glob (valueToExpr val)
+ Just (glob, perm) ->
+ do writable <- readGlobal perm
+ let msg = "putstatic: field " ++ show (fieldIdText fieldId) ++ " not writable"
+ assertExpr writable $ fromString msg
+ writeGlobal glob (valueToExpr val)
  Nothing ->
  jvmFail $ "putstatic: field " ++ show (fieldIdText fieldId) ++ " not found"