Merge pull request #733 from GaloisInc/jvm-static-field-writable

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

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,19 +31,26 @@ import Lang.Crucible.JVM.Types
 -- * JVMContext
 
 
-type StaticFieldTable = Map J.FieldId (GlobalVar JVMValueType)
+type StaticFieldTable = Map J.FieldId StaticFieldInfo
 type MethodHandleTable = Map (J.ClassName, J.MethodKey) JVMHandleInfo
 
 data JVMHandleInfo where
  JVMHandleInfo :: J.MethodKey -> FnHandle init ret -> JVMHandleInfo
 
+data StaticFieldInfo =
+ StaticFieldInfo
+ { staticFieldValue :: GlobalVar JVMValueType
+ , staticFieldWritable :: GlobalVar BoolType
+ }
+
 -- | Contains information about crucible function handles and global variables
 -- that is statically known during the class translation.
 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 StaticFieldInfo
  -- ^ 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

@@ -12,6 +12,7 @@ Stability : provisional
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
@@ -343,8 +344,10 @@ declareStaticField halloc c m f = do
  let fn = J.fieldName f
  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
+ let varname = globalVarName cn str
+ gvar <- C.freshGlobalVar halloc varname (knownRepr :: TypeRepr JVMValueType)
+ pvar <- C.freshGlobalVar halloc (varname <> ".W") (knownRepr :: TypeRepr BoolType)
+ return $ Map.insert fieldId (StaticFieldInfo gvar pvar) m
 
 
 -- | Create the initial 'JVMContext'.
@@ -470,11 +473,14 @@ 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 -> StaticFieldInfo -> IO (C.SymGlobalState sym) -> IO (C.SymGlobalState sym)
+ initField fi info 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
+ let gs1 = C.insertGlobal (staticFieldValue info) z gs
+ let gs2 = C.insertGlobal (staticFieldWritable info) writable gs1
+ pure gs2
 
  simctx = jvmSimContext sym halloc stdout ctx verbosity p
  globals0 = C.insertGlobal (dynamicClassTable ctx) Map.empty C.emptyGlobals
@@ -829,7 +835,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,12 +848,29 @@ doStaticFieldStore ::
 doStaticFieldStore sym jc globals fid val =
  case Map.lookup fid (staticFields jc) of
  Nothing -> C.addFailedAssertion sym msg
- Just gvar ->
- do putStrLn $ "doStaticFieldStore " ++ fname
- pure (C.insertGlobal gvar val globals)
+ Just info -> pure (C.insertGlobal (staticFieldValue info) val globals)
  where
- fname = J.unClassName (J.fieldIdClass fid) ++ "." ++ J.fieldIdName fid
- msg = C.GenericSimError $ "Static field store: field not found: " ++ fname
+ msg = C.GenericSimError $ "Static field store: field not found: " ++ ppFieldId fid
+
+-- | 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 info -> pure (C.insertGlobal (staticFieldWritable info) val globals)
+ where
+ msg = C.GenericSimError $ "Static field writable: field not found: " ++ ppFieldId fid
+
+ppFieldId :: J.FieldId -> String
+ppFieldId fid = J.unClassName (J.fieldIdClass fid) ++ "." ++ J.fieldIdName fid
 
 -- | Write a value at an index of an array reference.
 doArrayStore ::
@@ -901,13 +925,12 @@ doStaticFieldLoad ::
 doStaticFieldLoad sym jc globals fid =
  case Map.lookup fid (staticFields jc) of
  Nothing -> C.addFailedAssertion sym msg
- Just gvar ->
- case C.lookupGlobal gvar globals of
+ Just info ->
+ case C.lookupGlobal (staticFieldValue info) globals of
  Nothing -> C.addFailedAssertion sym msg
  Just v -> pure v
  where
- fname = J.unClassName (J.fieldIdClass fid) ++ "." ++ J.fieldIdName fid
- msg = C.GenericSimError $ "Static field load: field not found: " ++ fname
+ msg = C.GenericSimError $ "Static field load: field not found: " ++ ppFieldId fid
 
 -- | Read a value at an index of an array reference.
 doArrayLoad ::

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

@@ -364,8 +364,8 @@ getStaticFieldValue rawFieldId =
  initializeClass (J.fieldIdClass fieldId)
  ctx <- gets jsContext
  case Map.lookup fieldId (staticFields ctx) of
- Just glob ->
- do r <- readGlobal glob
+ Just info ->
+ do r <- readGlobal (staticFieldValue info)
  fromJVMDynamic ("getstatic " <> fieldIdText fieldId) (J.fieldIdType fieldId) r
  Nothing ->
  jvmFail $ "getstatic: field " ++ show (fieldIdText fieldId) ++ " not found"
@@ -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 info ->
+ do writable <- readGlobal (staticFieldWritable info)
+ let msg = "putstatic: field " ++ show (fieldIdText fieldId) ++ " not writable"
+ assertExpr writable $ fromString msg
+ writeGlobal (staticFieldValue info) (valueToExpr val)
  Nothing ->
  jvmFail $ "putstatic: field " ++ show (fieldIdText fieldId) ++ " not found"