Make jvm_field_is support ordinary unqualified field names.

It now performs field resolution on the base field name to determine
the complete fieldId including class name and type.

This implements part of the feature requested in #902.

However, as it stands the feature is not backward-compatible, as
*only* unqualified names currently work. The field resolution
procedure needs to be updated to allow optional qualified names.

Author: Brian Huffman

src/SAWScript/Crucible/JVM/Builtins.hs

@@ -43,6 +43,7 @@ import           Control.Lens
 
 import           Control.Monad.State
 import qualified Control.Monad.State.Strict as Strict
+import           Control.Monad.Trans.Except (runExceptT)
 import qualified Data.BitVector.Sized as BV
 import           Data.Foldable (for_)
 import           Data.Function
@@ -434,10 +435,13 @@ setupPrePointsTos mspec cc env pts mem0 = foldM doPointsTo mem0 pts
     doPointsTo :: Crucible.SymGlobalState Sym -> JVMPointsTo -> IO (Crucible.SymGlobalState Sym)
     doPointsTo mem pt =
       case pt of
-        JVMPointsToField _loc lhs fld rhs ->
+        JVMPointsToField _loc lhs fid rhs ->
           do lhs' <- resolveJVMRefVal lhs
              rhs' <- resolveSetupVal cc env tyenv nameEnv rhs
-             CJ.doFieldStore sym mem lhs' fld (injectJVMVal sym rhs')
+             -- TODO: Change type of CJ.doFieldStore to take a FieldId instead of a String.
+             -- Then we won't have to match the definition of 'fieldIdText' here.
+             let key = J.unClassName (J.fieldIdClass fid) ++ "." ++ J.fieldIdName fid
+             CJ.doFieldStore sym mem lhs' key (injectJVMVal sym rhs')
         JVMPointsToElem _loc lhs idx rhs ->
           do lhs' <- resolveJVMRefVal lhs
              rhs' <- resolveSetupVal cc env tyenv nameEnv rhs
@@ -874,19 +878,23 @@ jvm_field_is ::
   JVMSetupM ()
 jvm_field_is _typed _bic _opt ptr fname val =
   JVMSetupM $
-  do loc <- SS.toW4Loc "jvm_field_is" <$> lift getPosition
+  do pos <- lift getPosition
+     loc <- SS.toW4Loc "jvm_field_is" <$> lift getPosition
      st <- get
      let rs = st ^. Setup.csResolvedState
+     let cc = st ^. Setup.csCrucibleContext
+     let cb = cc ^. jccCodebase
      let path = Left fname
      if st ^. Setup.csPrePost == PreState && MS.testResolved ptr [] rs
        then fail $ "Multiple points-to preconditions on same pointer (field " ++ fname ++ ")"
        else Setup.csResolvedState %= MS.markResolved ptr [path]
-     -- let env = MS.csAllocations (st ^. Setup.csMethodSpec)
-     --     nameEnv = MS.csTypeNames (st ^. Setup.csMethodSpec)
-     -- ptrTy <- typeOfSetupValue cc env nameEnv ptr
+     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
      --when typed (checkMemTypeCompatibility lhsTy valTy)
-     Setup.addPointsTo (JVMPointsToField loc ptr fname val)
+     fid <- either fail pure =<< (liftIO $ runExceptT $ findField cb pos ptrTy fname)
+     Setup.addPointsTo (JVMPointsToField loc ptr fid val)
 
 jvm_elem_is ::
   Bool {- ^ whether to check type compatibility -} ->

src/SAWScript/Crucible/JVM/MethodSpecIR.hs

@@ -122,15 +122,15 @@ type instance MS.AllocSpec CJ.JVM = (ProgramLoc, Allocation)
 type instance MS.PointsTo CJ.JVM = JVMPointsTo
 
 data JVMPointsTo
-  = JVMPointsToField ProgramLoc (MS.SetupValue CJ.JVM) String (MS.SetupValue CJ.JVM)
+  = JVMPointsToField ProgramLoc (MS.SetupValue CJ.JVM) J.FieldId (MS.SetupValue CJ.JVM)
   | JVMPointsToElem ProgramLoc (MS.SetupValue CJ.JVM) Int (MS.SetupValue CJ.JVM)
   | JVMPointsToArray ProgramLoc (MS.SetupValue CJ.JVM) TypedTerm
 
 ppPointsTo :: JVMPointsTo -> PPL.Doc
 ppPointsTo =
   \case
-    JVMPointsToField _loc ptr fld val ->
-      MS.ppSetupValue ptr <> PPL.text "." <> PPL.text fld
+    JVMPointsToField _loc ptr fid val ->
+      MS.ppSetupValue ptr <> PPL.text "." <> PPL.text (J.fieldIdName fid)
       PPL.<+> PPL.text "points to"
       PPL.<+> MS.ppSetupValue val
     JVMPointsToElem _loc ptr idx val ->

src/SAWScript/Crucible/JVM/Override.hs

@@ -677,12 +677,15 @@ learnPointsTo opts sc cc spec prepost pt = do
   globals <- OM (use overrideGlobals)
   case pt of
 
-    JVMPointsToField loc ptr fname val ->
+    JVMPointsToField loc ptr fid val ->
       do ty <- typeOfSetupValue cc tyenv nameEnv val
          (_, ptr') <- resolveSetupValueJVM opts cc sc spec ptr
          rval <- asRVal loc ptr'
-         dyn <- liftIO $ CJ.doFieldLoad sym globals rval fname
-         v <- liftIO $ projectJVMVal sym ty ("field load " ++ fname ++ ", " ++ show loc) dyn
+         -- TODO: Change type of CJ.doFieldStore to take a FieldId instead of a String.
+         -- Then we won't have to match the definition of 'fieldIdText' here.
+         let key = J.unClassName (J.fieldIdClass fid) ++ "." ++ J.fieldIdName fid
+         dyn <- liftIO $ CJ.doFieldLoad sym globals rval key
+         v <- liftIO $ projectJVMVal sym ty ("field load " ++ J.fieldIdName fid ++ ", " ++ show loc) dyn
          matchArg opts sc cc spec prepost v ty val
 
     JVMPointsToElem loc ptr idx val ->
@@ -823,12 +826,15 @@ executePointsTo opts sc cc spec pt = do
   globals <- OM (use overrideGlobals)
   case pt of
 
-    JVMPointsToField loc ptr fname val ->
+    JVMPointsToField loc ptr fid val ->
       do (_, val') <- resolveSetupValueJVM opts cc sc spec val
          (_, ptr') <- resolveSetupValueJVM opts cc sc spec ptr
          rval <- asRVal loc ptr'
          let dyn = injectJVMVal sym val'
-         globals' <- liftIO $ CJ.doFieldStore sym globals rval fname dyn
+         -- TODO: Change type of CJ.doFieldStore to take a FieldId instead of a String.
+         -- Then we won't have to match the definition of 'fieldIdText' here.
+         let key = J.unClassName (J.fieldIdClass fid) ++ "." ++ J.fieldIdName fid
+         globals' <- liftIO $ CJ.doFieldStore sym globals rval key dyn
          OM (overrideGlobals .= globals')
 
     JVMPointsToElem loc ptr idx val ->