From db75c2beff99c6b9fd75648e3c074589b24f4c15 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Wed, 25 Nov 2020 19:22:35 -0800
Subject: [PATCH] Remove non-functional saw-script function `jvm_global`.

Support for static fields is planned using a different mechanism.
(See #908.)
---
 src/SAWScript/Crucible/JVM/MethodSpecIR.hs      |  2 +-
 src/SAWScript/Crucible/JVM/Override.hs          | 16 +++-------------
 src/SAWScript/Crucible/JVM/ResolveSetupValue.hs |  6 ++----
 src/SAWScript/Interpreter.hs                    |  7 -------
 4 files changed, 6 insertions(+), 25 deletions(-)

diff --git a/src/SAWScript/Crucible/JVM/MethodSpecIR.hs b/src/SAWScript/Crucible/JVM/MethodSpecIR.hs
index f57613b6cc..4d8866712b 100644
--- a/src/SAWScript/Crucible/JVM/MethodSpecIR.hs
+++ b/src/SAWScript/Crucible/JVM/MethodSpecIR.hs
@@ -56,7 +56,7 @@ import qualified SAWScript.Crucible.Common.Setup.Type as Setup
 -- ** Language features
 
 type instance MS.HasSetupNull CJ.JVM = 'True
-type instance MS.HasSetupGlobal CJ.JVM = 'True
+type instance MS.HasSetupGlobal CJ.JVM = 'False
 type instance MS.HasSetupStruct CJ.JVM = 'False
 type instance MS.HasSetupArray CJ.JVM = 'False
 type instance MS.HasSetupElem CJ.JVM = 'False
diff --git a/src/SAWScript/Crucible/JVM/Override.hs b/src/SAWScript/Crucible/JVM/Override.hs
index 5cb373cab0..b734662486 100644
--- a/src/SAWScript/Crucible/JVM/Override.hs
+++ b/src/SAWScript/Crucible/JVM/Override.hs
@@ -466,7 +466,7 @@ matchPointsTos opts sc cc spec prepost = go False []
         MS.SetupVar i                     -> Set.singleton i
         MS.SetupTerm _                    -> Set.empty
         MS.SetupNull ()                   -> Set.empty
-        MS.SetupGlobal () _               -> Set.empty
+        MS.SetupGlobal empty _            -> absurd empty
         MS.SetupStruct empty _ _          -> absurd empty
         MS.SetupArray empty _             -> absurd empty
         MS.SetupElem empty _ _            -> absurd empty
@@ -580,13 +580,7 @@ matchArg opts sc cc cs prepost actual@(RVal ref) expectedTy setupval =
          p   <- liftIO (CJ.refIsNull sym ref)
          addAssert p (Crucible.SimError (cs ^. MS.csLoc) (Crucible.AssertFailureSimError ("null-equality " ++ stateCond prepost) ""))
 
-    MS.SetupGlobal () name ->
-      do let mem = () -- FIXME cc^.ccLLVMEmptyMem
-         sym  <- Ov.getSymInterface
-         ref' <- liftIO $ doResolveGlobal sym mem name
-
-         p  <- liftIO (CJ.refIsEqual sym ref ref')
-         addAssert p (Crucible.SimError (cs ^. MS.csLoc) (Crucible.AssertFailureSimError ("global-equality " ++ stateCond prepost) ""))
+    MS.SetupGlobal empty _ -> absurd empty
 
     _ -> failure (cs ^. MS.csLoc) =<<
            mkStructuralMismatch opts cc sc cs actual setupval expectedTy
@@ -937,7 +931,7 @@ instantiateSetupValue sc s v =
     MS.SetupVar _                     -> return v
     MS.SetupTerm tt                   -> MS.SetupTerm <$> doTerm tt
     MS.SetupNull ()                   -> return v
-    MS.SetupGlobal () _               -> return v
+    MS.SetupGlobal empty _            -> absurd empty
     MS.SetupStruct empty _ _          -> absurd empty
     MS.SetupArray empty _             -> absurd empty
     MS.SetupElem empty _ _            -> absurd empty
@@ -1026,7 +1020,3 @@ decodeJVMVal ty v =
 asRVal :: W4.ProgramLoc -> JVMVal -> OverrideMatcher CJ.JVM w JVMRefVal
 asRVal _ (RVal ptr) = return ptr
 asRVal loc _ = failure loc BadPointerCast
-
-doResolveGlobal :: Sym -> () -> String -> IO JVMRefVal
-doResolveGlobal _sym _mem _name = fail "doResolveGlobal: FIXME"
--- FIXME: replace () with whatever type we need to look up global/static references
diff --git a/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs
index cf70774233..c5ce50532b 100644
--- a/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs
+++ b/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs
@@ -117,8 +117,7 @@ typeOfSetupValue _cc env _nameEnv val =
       -- can be used at, and b) it prevents us from doing any
       -- type-safe field accesses.
       return (J.ClassType (J.mkClassName "java/lang/Object"))
-    MS.SetupGlobal () name ->
-      fail ("typeOfSetupValue: unimplemented jvm_global: " ++ name)
+    MS.SetupGlobal empty _            -> absurd empty
     MS.SetupStruct empty _ _          -> absurd empty
     MS.SetupArray empty _             -> absurd empty
     MS.SetupElem empty _ _            -> absurd empty
@@ -142,8 +141,7 @@ resolveSetupVal cc env _tyenv _nameEnv val =
     MS.SetupTerm tm -> resolveTypedTerm cc tm
     MS.SetupNull () ->
       return (RVal (W4.maybePartExpr sym Nothing))
-    MS.SetupGlobal () name ->
-      fail $ "resolveSetupVal: unimplemented jvm_global: " ++ name
+    MS.SetupGlobal empty _            -> absurd empty
     MS.SetupStruct empty _ _          -> absurd empty
     MS.SetupArray empty _             -> absurd empty
     MS.SetupElem empty _ _            -> absurd empty
diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs
index 0b6d70fa71..09903efcd3 100644
--- a/src/SAWScript/Interpreter.hs
+++ b/src/SAWScript/Interpreter.hs
@@ -2528,13 +2528,6 @@ primitives = Map.fromList
     Experimental
     [ "A JVMValue representing a null pointer value." ]
 
-  , prim "jvm_global"
-    "String -> JVMValue"
-    (pureVal (CMS.SetupGlobal () :: String -> CMS.SetupValue CJ.JVM))
-    Experimental
-    [ "Return a JVMValue representing a pointer to the named global."
-    , "The String may be either the name of a global value or a function name." ]
-
   , prim "jvm_term"
     "Term -> JVMValue"
     (pureVal (CMS.SetupTerm :: TypedTerm -> CMS.SetupValue CJ.JVM))