From 1dcf4de42e5ab5faf82a62f80210b1c75a718ca5 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Wed, 16 Dec 2020 02:28:59 -0800
Subject: [PATCH 1/3] Refactor function `resolveField` into two parts.

---
 .../src/Lang/Crucible/JVM/Translation/Class.hs    | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

diff --git a/crucible-jvm/src/Lang/Crucible/JVM/Translation/Class.hs b/crucible-jvm/src/Lang/Crucible/JVM/Translation/Class.hs
index e5a988df4..327f036d4 100644
--- a/crucible-jvm/src/Lang/Crucible/JVM/Translation/Class.hs
+++ b/crucible-jvm/src/Lang/Crucible/JVM/Translation/Class.hs
@@ -813,13 +813,12 @@ newInstanceInstr cls fieldIds = do
 -- the JVM context to determine the class where the field was actually
 -- declared (which may be a superclass of the one specified in the
 -- input 'J.FieldId'), as specified in section 5.4.3.2 "Field
--- Resolution" of the Java Virtual Machine Specification. Then return
--- a key that can be used with an object's field map.
-resolveField :: J.FieldId -> JVMGenerator s ret (Expr JVM s (StringType Unicode))
+-- Resolution" of the Java Virtual Machine Specification.
+resolveField :: J.FieldId -> JVMGenerator s ret J.FieldId
 resolveField fieldId =
   do cls <- lookupClassGen (J.fieldIdClass fieldId)
      case any fieldMatch (J.classFields cls) of
-       True -> pure (App (StringLit (UnicodeLiteral (fieldIdText fieldId))))
+       True -> pure fieldId
        False ->
          -- otherwise recursively check the superclass
          case J.superClass cls of
@@ -830,13 +829,17 @@ resolveField fieldId =
     fieldMatch f =
       (J.fieldName f, J.fieldType f) == (J.fieldIdName fieldId, J.fieldIdType fieldId)
 
+-- | Convert a 'J.FieldId' into a string key that can be used with an object's field map.
+fieldIdKey :: J.FieldId -> Expr JVM s (StringType Unicode)
+fieldIdKey fieldId = App (StringLit (UnicodeLiteral (fieldIdText fieldId)))
+
 -- | Access the field component of a JVM object (must be a class instance, not an array).
 getInstanceFieldValue :: JVMObject s -> J.FieldId -> JVMGenerator s ret (JVMValue s)
 getInstanceFieldValue obj fieldId =
   do let uobj = App (UnrollRecursive knownRepr knownRepr obj)
      inst <- projectVariant "getfield: expected class instance" Ctx.i1of2 uobj
      let fields = App (GetStruct inst Ctx.i1of2 knownRepr)
-     key <- resolveField fieldId
+     key <- fieldIdKey <$> resolveField fieldId
      let mval = App (LookupStringMapEntry knownRepr fields key)
      dyn <- assertedJustExpr mval "Field not present"
      fromJVMDynamic ("getfield " <> fieldIdText fieldId) (J.fieldIdType fieldId) dyn
@@ -849,7 +852,7 @@ setInstanceFieldValue obj fieldId val =
      let uobj = App (UnrollRecursive knownRepr knownRepr obj)
      inst <- projectVariant "setfield: expected class instance" Ctx.i1of2 uobj
      let fields = App (GetStruct inst Ctx.i1of2 knownRepr)
-     key <- resolveField fieldId
+     key <- fieldIdKey <$> resolveField fieldId
      let fields' = App (InsertStringMapEntry knownRepr fields key mdyn)
      let inst'  = App (SetStruct knownRepr inst Ctx.i1of2 fields')
      let uobj' = App (InjectVariant knownRepr Ctx.i1of2 inst')

From 1e64b65ce60dc579845203dcf6867ad962945cd0 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Wed, 16 Dec 2020 02:33:40 -0800
Subject: [PATCH 2/3] Reimplement translation of `getstatic` and `putstatic`
 following JVM spec.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

According to the JVM spec, each of these instructions starts with the
same two steps: "The referenced field is resolved (§5.4.3.2). On
successful resolution of the field, the class or interface that
declared the resolved field is initialized (§5.5) if that class or
interface has not already been initialized."
---
 .../src/Lang/Crucible/JVM/Translation.hs      |  2 +-
 .../Lang/Crucible/JVM/Translation/Class.hs    | 49 +++++++++++--------
 2 files changed, 29 insertions(+), 22 deletions(-)

diff --git a/crucible-jvm/src/Lang/Crucible/JVM/Translation.hs b/crucible-jvm/src/Lang/Crucible/JVM/Translation.hs
index 77f7e8c94..0046185b4 100644
--- a/crucible-jvm/src/Lang/Crucible/JVM/Translation.hs
+++ b/crucible-jvm/src/Lang/Crucible/JVM/Translation.hs
@@ -733,7 +733,7 @@ generateInstruction (pc, instr) =
 
     J.Putstatic fieldId -> do
       val <- popValue
-      lift $ setStaticFieldValue fieldId val
+      lift $ putStaticFieldValue fieldId val
 
 
     -- array creation
diff --git a/crucible-jvm/src/Lang/Crucible/JVM/Translation/Class.hs b/crucible-jvm/src/Lang/Crucible/JVM/Translation/Class.hs
index 327f036d4..f6da3eca4 100644
--- a/crucible-jvm/src/Lang/Crucible/JVM/Translation/Class.hs
+++ b/crucible-jvm/src/Lang/Crucible/JVM/Translation/Class.hs
@@ -85,6 +85,7 @@ module Lang.Crucible.JVM.Translation.Class
    , findDynamicMethod
    -- ** Static fields and methods
    , getStaticFieldValue
+   , putStaticFieldValue
    , setStaticFieldValue
    , getStaticMethod
    -- * Strings
@@ -358,28 +359,34 @@ setInitStatus c status = do
 
 -- | Read the global variable corresponding to the given static field.
 getStaticFieldValue :: J.FieldId -> JVMGenerator s ret (JVMValue s)
-getStaticFieldValue fieldId = do
-      let cls = J.fieldIdClass fieldId
-      ctx <- gets jsContext
-      initializeClass cls
-      case Map.lookup fieldId (staticFields ctx) of
-        Just glob -> do
-          r <- readGlobal glob
-          fromJVMDynamic ("getstatic " <> fieldIdText fieldId) (J.fieldIdType fieldId) r
-        Nothing ->
-          jvmFail $ "getstatic: field " ++ J.fieldIdName fieldId ++ " not found"
-
--- | Update the value of a static field.
+getStaticFieldValue rawFieldId =
+  do fieldId <- resolveField rawFieldId
+     initializeClass (J.fieldIdClass fieldId)
+     ctx <- gets jsContext
+     case Map.lookup fieldId (staticFields ctx) of
+       Just glob ->
+         do r <- readGlobal glob
+            fromJVMDynamic ("getstatic " <> fieldIdText fieldId) (J.fieldIdType fieldId) r
+       Nothing ->
+         jvmFail $ "getstatic: field " ++ show (fieldIdText fieldId) ++ " not found"
+
+-- | Resolve a static field, initialize the resulting class, and
+-- update the value.
+putStaticFieldValue :: J.FieldId -> JVMValue s -> JVMGenerator s ret ()
+putStaticFieldValue rawFieldId val =
+  do fieldId <- resolveField rawFieldId
+     initializeClass (J.fieldIdClass fieldId)
+     setStaticFieldValue fieldId val
+
+-- | Update the value of a static field, without doing any field resolution or class initialization.
 setStaticFieldValue :: J.FieldId -> JVMValue s -> JVMGenerator s ret ()
-setStaticFieldValue  fieldId val = do
-    ctx <- gets jsContext
-    let cName = J.fieldIdClass fieldId
-    case Map.lookup fieldId (staticFields ctx) of
-         Just glob -> do
-           writeGlobal glob (valueToExpr val)
-         Nothing ->
-           jvmFail $ "putstatic: field " ++ J.unClassName cName
-                     ++ "." ++ (J.fieldIdName fieldId) ++ " not found"
+setStaticFieldValue fieldId val =
+  do ctx <- gets jsContext
+     case Map.lookup fieldId (staticFields ctx) of
+       Just glob ->
+         writeGlobal glob (valueToExpr val)
+       Nothing ->
+         jvmFail $ "putstatic: field " ++ show (fieldIdText fieldId) ++ " not found"
 
 -- | Look up a method in the static method table (i.e. 'methodHandles').
 -- (See section 5.4.3.3 "Method Resolution" of the JVM spec.)

From 16440bb9608b5b69a056251f3b363cf01dd44854 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Mon, 11 Jan 2021 19:12:08 -0800
Subject: [PATCH 3/3] Add comment explaining when to use `setStaticFieldValue`.

---
 crucible-jvm/src/Lang/Crucible/JVM/Translation/Class.hs | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/crucible-jvm/src/Lang/Crucible/JVM/Translation/Class.hs b/crucible-jvm/src/Lang/Crucible/JVM/Translation/Class.hs
index f6da3eca4..3c09eb724 100644
--- a/crucible-jvm/src/Lang/Crucible/JVM/Translation/Class.hs
+++ b/crucible-jvm/src/Lang/Crucible/JVM/Translation/Class.hs
@@ -378,7 +378,11 @@ putStaticFieldValue rawFieldId val =
      initializeClass (J.fieldIdClass fieldId)
      setStaticFieldValue fieldId val
 
--- | Update the value of a static field, without doing any field resolution or class initialization.
+-- | Update the value of a static field, without doing any field
+-- resolution or class initialization. This function must be used
+-- instead of 'putStaticFieldValue' for implementing static class
+-- initializers, to avoid calling the class initializer in an infinite
+-- loop.
 setStaticFieldValue :: J.FieldId -> JVMValue s -> JVMGenerator s ret ()
 setStaticFieldValue fieldId val =
   do ctx <- gets jsContext