Merge pull request #589 from GaloisInc/bh-jvm

Changes to crucible-jvm field operations

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

@@ -30,7 +30,7 @@ import Lang.Crucible.JVM.Types
 -- * JVMContext
 
 
-type StaticFieldTable = Map (J.ClassName, J.FieldId) (GlobalVar JVMValueType)
+type StaticFieldTable = Map J.FieldId (GlobalVar JVMValueType)
 type MethodHandleTable = Map (J.ClassName, J.MethodKey) JVMHandleInfo
 
 data JVMHandleInfo where
@@ -41,7 +41,7 @@ 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.ClassName, J.FieldId) (GlobalVar JVMValueType)
+ , staticFields :: Map J.FieldId (GlobalVar JVMValueType)
  -- ^ Map from static field names to Crucible global variables.
  -- We know about these fields at translation time so we can allocate
  -- global variables to store them.

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

@@ -34,7 +34,6 @@ import Data.Maybe (fromMaybe)
 import qualified Data.Set as Set
 import Data.String (fromString)
 import Data.List (isPrefixOf)
-import qualified Data.Text as Text
 import qualified Data.Vector as V
 
 import System.IO
@@ -345,7 +344,7 @@ 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 (cn,fieldId) gvar m)
+ return $ Map.insert fieldId gvar m
 
 
 -- | Create the initial 'JVMContext'.
@@ -457,7 +456,7 @@ jvmSimContext sym halloc handle ctx verbosity p =
 -- | Make the initial state for the simulator, binding the function handles so that
 -- they translate method bodies when they are accessed.
 mkSimSt ::
- -- forall sym .
+ forall sym p ret.
  (IsSymInterface sym) =>
  sym ->
  p ->
@@ -471,8 +470,8 @@ 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.ClassName, J.FieldId) -> GlobalVar JVMValueType -> IO (C.SymGlobalState sym) -> IO (C.SymGlobalState sym)
- initField (_, fi) var m =
+ initField :: J.FieldId -> GlobalVar JVMValueType -> IO (C.SymGlobalState sym) -> IO (C.SymGlobalState sym)
+ initField fi var m =
  do gs <- m
  z <- zeroValue sym (J.fieldIdType fi)
  return (C.insertGlobal var z gs)
@@ -807,27 +806,48 @@ doAppJVM sym =
  where
  out _verbosity _msg = return () --putStrLn
 
--- | Write a value to a field of an object reference.
+-- | Write a value to a field of an object reference. The 'FieldId'
+-- must have already been resolved (see §5.4.3.2 of the JVM spec).
 doFieldStore ::
  IsSymInterface sym =>
  sym ->
  C.SymGlobalState sym ->
  C.RegValue sym JVMRefType ->
- String {- ^ field name -} ->
+ J.FieldId ->
  C.RegValue sym JVMValueType ->
  IO (C.SymGlobalState sym)
-doFieldStore sym globals ref fname val =
+doFieldStore sym globals ref fid val =
  do let msg1 = C.GenericSimError "Field store: null reference"
  ref' <- C.readPartExpr sym ref msg1
  obj <- EvalStmt.readRef sym jvmIntrinsicTypes objectRepr ref' globals
  let msg2 = C.GenericSimError "Field store: object is not a class instance"
  inst <- C.readPartExpr sym (C.unVB (C.unroll obj Ctx.! Ctx.i1of2)) msg2
  let tab = C.unRV (inst Ctx.! Ctx.i1of2)
- let tab' = Map.insert (Text.pack fname) (W4.justPartExpr sym val) tab
+ let tab' = Map.insert (fieldIdText fid) (W4.justPartExpr sym val) tab
  let inst' = Control.Lens.set (Ctx.ixF Ctx.i1of2) (C.RV tab') inst
  let obj' = C.RolledType (C.injectVariant sym knownRepr Ctx.i1of2 inst')
  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).
+doStaticFieldStore ::
+ IsSymInterface sym =>
+ sym ->
+ JVMContext ->
+ C.SymGlobalState sym ->
+ J.FieldId ->
+ C.RegValue sym JVMValueType ->
+ IO (C.SymGlobalState sym)
+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)
+ where
+ fname = J.unClassName (J.fieldIdClass fid) ++ "." ++ J.fieldIdName fid
+ msg = C.GenericSimError $ "Static field store: field not found: " ++ fname
+
 -- | Write a value at an index of an array reference.
 doArrayStore ::
  IsSymInterface sym =>
@@ -849,24 +869,46 @@ doArrayStore sym globals ref idx val =
  let obj' = C.RolledType (C.injectVariant sym knownRepr Ctx.i2of2 arr')
  EvalStmt.alterRef sym jvmIntrinsicTypes objectRepr ref' (W4.justPartExpr sym obj') globals
 
--- | Read a value from a field of an object reference.
+-- | Read a value from a field of an object reference. The 'FieldId'
+-- must have already been resolved (see §5.4.3.2 of the JVM spec).
 doFieldLoad ::
  IsSymInterface sym =>
  sym ->
  C.SymGlobalState sym ->
- C.RegValue sym JVMRefType -> String {- ^ field name -} ->
+ C.RegValue sym JVMRefType ->
+ J.FieldId ->
  IO (C.RegValue sym JVMValueType)
-doFieldLoad sym globals ref fname =
+doFieldLoad sym globals ref fid =
  do let msg1 = C.GenericSimError "Field load: null reference"
  ref' <- C.readPartExpr sym ref msg1
  obj <- EvalStmt.readRef sym jvmIntrinsicTypes objectRepr ref' globals
  let msg2 = C.GenericSimError "Field load: object is not a class instance"
  inst <- C.readPartExpr sym (C.unVB (C.unroll obj Ctx.! Ctx.i1of2)) msg2
  let tab = C.unRV (inst Ctx.! Ctx.i1of2)
- let msg3 = C.GenericSimError $ "Field load: field not found: " ++ fname
- let key = Text.pack fname
+ let msg3 = C.GenericSimError $ "Field load: field not found: " ++ J.fieldIdName fid
+ let key = fieldIdText fid
  C.readPartExpr sym (fromMaybe W4.Unassigned (Map.lookup key tab)) msg3
 
+-- | Read a value from a static field of a class. The 'FieldId' must
+-- have already been resolved (see §5.4.3.2 of the JVM spec).
+doStaticFieldLoad ::
+ IsSymInterface sym =>
+ sym ->
+ JVMContext ->
+ C.SymGlobalState sym ->
+ J.FieldId ->
+ IO (C.RegValue sym JVMValueType)
+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
+ 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
+
 -- | Read a value at an index of an array reference.
 doArrayLoad ::
  IsSymInterface sym =>

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

@@ -362,10 +362,10 @@ getStaticFieldValue fieldId = do
  let cls = J.fieldIdClass fieldId
  ctx <- gets jsContext
  initializeClass cls
- case Map.lookup (J.fieldIdClass fieldId, fieldId) (staticFields ctx) of
+ case Map.lookup fieldId (staticFields ctx) of
  Just glob -> do
  r <- readGlobal glob
- fromJVMDynamic (J.fieldIdType fieldId) r
+ fromJVMDynamic ("getstatic " <> fieldIdText fieldId) (J.fieldIdType fieldId) r
  Nothing ->
  jvmFail $ "getstatic: field " ++ J.fieldIdName fieldId ++ " not found"
 
@@ -374,7 +374,7 @@ setStaticFieldValue :: J.FieldId -> JVMValue s -> JVMGenerator s ret ()
 setStaticFieldValue fieldId val = do
  ctx <- gets jsContext
  let cName = J.fieldIdClass fieldId
- case Map.lookup (cName, fieldId) (staticFields ctx) of
+ case Map.lookup fieldId (staticFields ctx) of
  Just glob -> do
  writeGlobal glob (valueToExpr val)
  Nothing ->
@@ -834,20 +834,20 @@ resolveField fieldId =
 getInstanceFieldValue :: JVMObject s -> J.FieldId -> JVMGenerator s ret (JVMValue s)
 getInstanceFieldValue obj fieldId =
  do let uobj = App (UnrollRecursive knownRepr knownRepr obj)
- inst <- projectVariant Ctx.i1of2 uobj
+ inst <- projectVariant "getfield: expected class instance" Ctx.i1of2 uobj
  let fields = App (GetStruct inst Ctx.i1of2 knownRepr)
  key <- resolveField fieldId
  let mval = App (LookupStringMapEntry knownRepr fields key)
  dyn <- assertedJustExpr mval "Field not present"
- fromJVMDynamic (J.fieldIdType fieldId) dyn
+ fromJVMDynamic ("getfield " <> fieldIdText fieldId) (J.fieldIdType fieldId) dyn
 
 -- | Update a field of a JVM object (must be a class instance, not an array).
 setInstanceFieldValue :: JVMObject s -> J.FieldId -> JVMValue s -> JVMGenerator s ret (JVMObject s)
 setInstanceFieldValue obj fieldId val =
  do let dyn = valueToExpr val
  let mdyn = App (JustValue knownRepr dyn)
  let uobj = App (UnrollRecursive knownRepr knownRepr obj)
- inst <- projectVariant Ctx.i1of2 uobj
+ inst <- projectVariant "setfield: expected class instance" Ctx.i1of2 uobj
  let fields = App (GetStruct inst Ctx.i1of2 knownRepr)
  key <- resolveField fieldId
  let fields' = App (InsertStringMapEntry knownRepr fields key mdyn)
@@ -859,7 +859,7 @@ setInstanceFieldValue obj fieldId val =
 getJVMInstanceClass :: JVMObject s -> JVMGenerator s ret (JVMClass s)
 getJVMInstanceClass obj = do
  let uobj = App (UnrollRecursive knownRepr knownRepr obj)
- inst <- projectVariant Ctx.i1of2 uobj
+ inst <- projectVariant "invokeinterface: expected class instance" Ctx.i1of2 uobj
  return $ App (GetStruct inst Ctx.i2of2 knownRepr)
 
 

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

@@ -18,6 +18,7 @@ import Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
 import Control.Monad.State.Strict
 import Control.Lens hiding (op, (:>))
+import qualified Data.Text as Text
 
 -- jvm-parser
 import qualified Language.JVM.Parser as J
@@ -39,6 +40,7 @@ import Lang.Crucible.Panic
 import Lang.Crucible.JVM.Types
 import Lang.Crucible.JVM.Context
 -- what4
+import What4.Interface (StringLiteral(..))
 import What4.ProgramLoc (Position(InternalPos))
 
 import Debug.Trace
@@ -187,12 +189,14 @@ valueToExpr (RValue x) = App $ InjectVariant knownRepr tagR x
 
 projectVariant ::
  KnownRepr (Ctx.Assignment TypeRepr) ctx =>
+ Text.Text ->
  Ctx.Index ctx tp ->
  Expr JVM s (VariantType ctx) ->
  JVMGenerator s ret (Expr JVM s tp)
-projectVariant tag var =
+projectVariant msg tag var =
  do let mx = App (ProjectVariant knownRepr tag var)
- assertedJustExpr mx "incorrect variant"
+ let str = App $ StringLit $ UnicodeLiteral ("read failed: " <> msg)
+ assertedJustExpr mx str
 
 injectVariant ::
  KnownRepr (Ctx.Assignment TypeRepr) ctx =>
@@ -202,19 +206,20 @@ injectVariant ::
 injectVariant tag val = App (InjectVariant knownRepr tag val)
 
 
-fromJVMDynamic :: J.Type -> Expr JVM s JVMValueType -> JVMGenerator s ret (JVMValue s)
-fromJVMDynamic ty dyn =
+fromJVMDynamic ::
+ Text.Text -> J.Type -> Expr JVM s JVMValueType -> JVMGenerator s ret (JVMValue s)
+fromJVMDynamic msg ty dyn =
  case ty of
- J.BooleanType -> IValue <$> projectVariant tagI dyn
- J.ArrayType _ -> RValue <$> projectVariant tagR dyn
- J.ByteType -> IValue <$> projectVariant tagI dyn
- J.CharType -> IValue <$> projectVariant tagI dyn
- J.ClassType _ -> RValue <$> projectVariant tagR dyn
- J.DoubleType -> DValue <$> projectVariant tagD dyn
- J.FloatType -> FValue <$> projectVariant tagF dyn
- J.IntType -> IValue <$> projectVariant tagI dyn
- J.LongType -> LValue <$> projectVariant tagL dyn
- J.ShortType -> IValue <$> projectVariant tagI dyn
+ J.BooleanType -> IValue <$> projectVariant msg tagI dyn
+ J.ArrayType _ -> RValue <$> projectVariant msg tagR dyn
+ J.ByteType -> IValue <$> projectVariant msg tagI dyn
+ J.CharType -> IValue <$> projectVariant msg tagI dyn
+ J.ClassType _ -> RValue <$> projectVariant msg tagR dyn
+ J.DoubleType -> DValue <$> projectVariant msg tagD dyn
+ J.FloatType -> FValue <$> projectVariant msg tagF dyn
+ J.IntType -> IValue <$> projectVariant msg tagI dyn
+ J.LongType -> LValue <$> projectVariant msg tagL dyn
+ J.ShortType -> IValue <$> projectVariant msg tagI dyn
 
 toJVMDynamic :: J.Type -> JVMValue s -> JVMGenerator s ret (Expr JVM s JVMValueType)
 toJVMDynamic ty val =