Remove deprecated java commands

saw-remote-api/saw-remote-api.cabal

@@ -53,7 +53,6 @@ common deps
                  cryptonite-conduit,
                  directory,
                  jvm-parser,
-                 jvm-verifier,
                  lens,
                  llvm-pretty,
                  llvm-pretty-bc-parser,

saw-remote-api/src/SAWServer.hs

@@ -37,7 +37,7 @@ import qualified Data.AIG as AIG
 import qualified Lang.Crucible.FunctionHandle as Crucible (HandleAllocator, newHandleAllocator)
 import qualified Lang.Crucible.JVM as CJ
 import qualified Text.LLVM.AST as LLVM
-import qualified Verifier.Java.Codebase as JSS
+import qualified Lang.JVM.Codebase as JSS
 import qualified Verifier.SAW.CryptolEnv as CryptolEnv
 import Verifier.SAW.Module (emptyModule)
 import Verifier.SAW.SharedTerm (mkSharedContext, scLoadModule)
@@ -55,7 +55,6 @@ import SAWScript.Value (AIGProxy(..), BuiltinContext(..), JVMSetupM, LLVMCrucibl
 import qualified Verifier.SAW.Cryptol.Prelude as CryptolSAW
 import Verifier.SAW.CryptolEnv (initCryptolEnv, bindTypedTerm)
 import Verifier.SAW.Rewriter (Simpset)
-import qualified Verifier.Java.SAWBackend as JavaSAW
 import qualified Cryptol.Utils.Ident as Cryptol
 
 import Argo
@@ -160,7 +159,6 @@ initialState readFileFn =
   silence $
   do sc <- mkSharedContext
      CryptolSAW.scLoadPreludeModule sc
-     JavaSAW.scLoadJavaModule sc
      CryptolSAW.scLoadCryptolModule sc
      let mn = mkModuleName ["SAWScript"]
      scLoadModule sc (emptyModule mn)

saw-script.cabal

@@ -52,7 +52,6 @@ library
     , haskeline
     , IfElse
     , jvm-parser
-    , jvm-verifier
     , lens
     , llvm-pretty >= 0.8
     , llvm-pretty-bc-parser >= 0.1.3.1
@@ -115,13 +114,8 @@ library
     SAWScript.Import
     SAWScript.ImportAIG
     SAWScript.Interpreter
-    SAWScript.JavaBuiltins
     SAWScript.JavaExpr
-    SAWScript.JavaMethodSpec
-    SAWScript.JavaMethodSpec.Evaluator
-    SAWScript.JavaMethodSpecIR
     SAWScript.JavaTools
-    SAWScript.JavaUtils
     SAWScript.JavaPretty
     SAWScript.Lexer
     SAWScript.LLVMBuiltins

src/SAWScript/AutoMatch.hs

@@ -56,7 +56,6 @@ import SAWScript.AutoMatch.LLVM
 import SAWScript.AutoMatch.Cryptol
 
 import SAWScript.LLVMBuiltins
---import SAWScript.JavaBuiltins
 import Language.JVM.Common (dotsToSlashes, mkClassName)
 
 import Prettyprinter.Render.Text (putDoc, hPutDoc)

src/SAWScript/AutoMatch/JVM.hs

@@ -5,8 +5,6 @@ module SAWScript.AutoMatch.JVM where
 
 import qualified Language.JVM.Parser as JVM
 
-import qualified Verifier.Java.Simulator as JSS hiding (lookupClass)
-
 --import SAWScript.Builtins
 --import SAWScript.Options
 import SAWScript.AutoMatch.Declaration
@@ -19,22 +17,22 @@ import Data.Either
 
 -- | Parse a Java class into a list of declarations
 --   Yields an Interaction so that we can talk to the user about what went wrong
-getDeclsJVM :: JSS.Class -> IO (Interaction (Maybe [Decl]))
+getDeclsJVM :: JVM.Class -> IO (Interaction (Maybe [Decl]))
 getDeclsJVM cls = return $ do
 
    let (untranslateable, translations) =
-         partitionEithers . for (JSS.classMethods cls) $ \method ->
-            maybe (Left $ JSS.methodName method) Right $ do
-               returnType <- jssTypeToStdType =<< JSS.methodReturnType method
-               argTypes <- mapM jssTypeToStdType $ JSS.methodParameterTypes method
-               let argIndices = map (JSS.localIndexOfParameter method) [0 .. length argTypes - 1]
-               tableEntries <- forM argIndices $ JSS.lookupLocalVariableByIdx method 0
-               let args = zipWith Arg (map JSS.localName tableEntries) argTypes
-               return $ Decl (JSS.methodName method) returnType args
+         partitionEithers . for (JVM.classMethods cls) $ \method ->
+            maybe (Left $ JVM.methodName method) Right $ do
+               returnType <- jssTypeToStdType =<< JVM.methodReturnType method
+               argTypes <- mapM jssTypeToStdType $ JVM.methodParameterTypes method
+               let argIndices = map (JVM.localIndexOfParameter method) [0 .. length argTypes - 1]
+               tableEntries <- forM argIndices $ JVM.lookupLocalVariableByIdx method 0
+               let args = zipWith Arg (map JVM.localName tableEntries) argTypes
+               return $ Decl (JVM.methodName method) returnType args
 
    when (not . null $ untranslateable) $ do
       separator ThinSep
-      liftF . flip Warning () $ "No translation for the following signatures in " ++ JVM.unClassName (JSS.className cls) ++ ".class:"
+      liftF . flip Warning () $ "No translation for the following signatures in " ++ JVM.unClassName (JVM.className cls) ++ ".class:"
       bulleted $ map (("'" ++) . (++ "'")) untranslateable
 
    return $ Just translations

src/SAWScript/Crucible/JVM/Builtins.hs

@@ -60,10 +60,6 @@ import           Data.Void (absurd)
 import           Prettyprinter
 import           System.IO
 
--- jvm-verifier
--- TODO: transition to Lang.JVM.Codebase from crucible-jvm
-import qualified Verifier.Java.Codebase as CB
-
 -- cryptol
 import qualified Cryptol.Eval.Type as Cryptol (evalValType)
 import qualified Cryptol.TypeCheck.Type as Cryptol
@@ -88,6 +84,7 @@ import qualified Lang.Crucible.Simulator.GlobalState as Crucible
 import qualified Lang.Crucible.Simulator.SimError as Crucible
 
 -- crucible-jvm
+import qualified Lang.JVM.Codebase as CB
 import qualified Lang.Crucible.JVM as CJ
 
 -- parameterized-utils

src/SAWScript/Crucible/JVM/BuiltinsJVM.hs

@@ -83,21 +83,14 @@ import SAWScript.Crucible.LLVM.Builtins (setupArg, setupArgs, getGlobalPair, run
 import qualified Language.JVM.Common as J
 import qualified Language.JVM.Parser as J
 import qualified SAWScript.Utils as J
-import qualified "jvm-verifier" Verifier.Java.Codebase as JCB
+import qualified Lang.JVM.Codebase as JCB
 
 -- crucible-jvm
 import           Lang.Crucible.JVM (IsCodebase(..))
 import qualified Lang.Crucible.JVM as CJ
 
 import Debug.Trace
 
---
--- | Use the Codebase implementation from the old Java static simulator
---
-instance IsCodebase JCB.Codebase where
-  lookupClass cb = J.lookupClass cb fixPos
-  findMethod  cb = J.findMethod  cb fixPos
-
 -----------------------------------------------------------------------
 -- | Make sure the class is in the database and allocate handles for its
 -- methods and static fields

src/SAWScript/Crucible/JVM/MethodSpecIR.hs

@@ -37,10 +37,7 @@ import qualified Lang.Crucible.FunctionHandle as Crucible (HandleAllocator)
 
 -- crucible-jvm
 import qualified Lang.Crucible.JVM as CJ
-
--- jvm-verifier
--- TODO: transition to Lang.JVM.Codebase from crucible-jvm
-import qualified Verifier.Java.Codebase as CB
+import qualified Lang.JVM.Codebase as CB
 
 -- jvm-parser
 import qualified Language.JVM.Parser as J

src/SAWScript/Interpreter.hs

@@ -50,7 +50,6 @@ import SAWScript.AST (Located(..),Import(..))
 import SAWScript.Builtins
 import SAWScript.Exceptions (failTypecheck)
 import qualified SAWScript.Import
-import SAWScript.JavaBuiltins
 import SAWScript.JavaExpr
 import SAWScript.LLVMBuiltins
 import SAWScript.Options
@@ -71,8 +70,7 @@ import Verifier.SAW.TypedAST
 import Verifier.SAW.TypedTerm
 import qualified Verifier.SAW.CryptolEnv as CEnv
 
-import qualified Verifier.Java.Codebase as JCB
-import qualified Verifier.Java.SAWBackend as JavaSAW
+import qualified Lang.JVM.Codebase as JCB
 
 import qualified Verifier.SAW.Cryptol.Prelude as CryptolSAW
 
@@ -400,7 +398,6 @@ buildTopLevelEnv proxy opts =
        sc0 <- mkSharedContext
        let ?fileReader = BS.readFile
        CryptolSAW.scLoadPreludeModule sc0
-       JavaSAW.scLoadJavaModule sc0
        CryptolSAW.scLoadCryptolModule sc0
        scLoadModule sc0 (emptyModule mn)
        cryptol_mod <- scFindModule sc0 $ mkModuleName ["Cryptol"]
@@ -1647,157 +1644,11 @@ primitives = Map.fromList
     Current
     [ "The Java type corresponding to the named class." ]
 
-  --, prim "java_value"          "{a} String -> a"
-
-  , prim "java_var"            "String -> JavaType -> JavaSetup Term"
-    (pureVal javaVar)
-    Deprecated
-    [ "Return a term corresponding to the initial value of the named Java"
-    , "variable, which should have the given type. The returned term can be"
-    , "used to construct more complex expressions. For example it can be used"
-    , "with 'java_return' to describe the expected return value in terms"
-    , "of the initial value of a variable. The Java variable can also be of"
-    , "the form \"args[n]\" to refer to the (0-based) nth argument of a method."
-    ]
-
-  , prim "java_class_var"      "String -> JavaType -> JavaSetup ()"
-    (pureVal javaClassVar)
-    Deprecated
-    [ "Declare that the named Java variable should point to an object of the"
-    , "given class type."
-    ]
-
-  , prim "java_may_alias"      "[String] -> JavaSetup ()"
-    (pureVal javaMayAlias)
-    Deprecated
-    [ "Indicate that the given set of Java variables are allowed to alias"
-    , "each other."
-    ]
-
-  , prim "java_assert"         "Term -> JavaSetup ()"
-    (pureVal javaAssert)
-    Deprecated
-    [ "Assert that the given term should evaluate to true in the initial"
-    , "state of a Java method."
-    ]
-
-  , prim "java_assert_eq"      "String -> Term -> JavaSetup ()"
-    (pureVal javaAssertEq)
-    Deprecated
-    [ "Assert that the given variable should have the given value in the"
-    , "initial state of a Java method."
-    ]
-
-  , prim "java_ensure_eq"      "String -> Term -> JavaSetup ()"
-    (pureVal javaEnsureEq)
-    Deprecated
-    [ "Specify that the given Java variable should have a value equal to the"
-    , "given term when execution finishes."
-    ]
-
-  , prim "java_modify"         "String -> JavaSetup ()"
-    (pureVal javaModify)
-    Deprecated
-    [ "Indicate that a Java method may modify the named portion of the state." ]
-
-  , prim "java_return"         "Term -> JavaSetup ()"
-    (pureVal javaReturn)
-    Deprecated
-    [ "Indicate the expected return value of a Java method." ]
-
-  , prim "java_verify_tactic"  "ProofScript SatResult -> JavaSetup ()"
-    (pureVal javaVerifyTactic)
-    Deprecated
-    [ "Use the given proof script to prove the specified properties about"
-    , "a Java method."
-    ]
-
-  , prim "java_sat_branches"   "Bool -> JavaSetup ()"
-    (pureVal javaSatBranches)
-    Deprecated
-    [ "Turn on or off satisfiability checking of branch conditions during"
-    , "symbolic execution."
-    ]
-
-  , prim "java_no_simulate"    "JavaSetup ()"
-    (pureVal javaNoSimulate)
-    Deprecated
-    [ "Skip symbolic simulation for this Java method." ]
-
-  , prim "java_allow_alloc"    "JavaSetup ()"
-    (pureVal javaAllowAlloc)
-    Deprecated
-    [ "Allow allocation of new objects or arrays during simulation,"
-    , "as long as the behavior of the method can still be described"
-    , "as a pure function."
-    ]
-
-   , prim "java_requires_class"  "String -> JavaSetup ()"
-     (pureVal javaRequiresClass)
-     Deprecated
-     [ "Declare that the given method can only be executed if the given"
-     , "class has already been initialized."
-     ]
-
-  , prim "java_pure"           "JavaSetup ()"
-    (pureVal javaPure)
-    Deprecated
-    [ "The empty specification for 'java_verify'. Equivalent to 'return ()'." ]
-
   , prim "java_load_class"     "String -> TopLevel JavaClass"
     (pureVal CJ.loadJavaClass)
     Current
     [ "Load the named Java class and return a handle to it." ]
 
-  --, prim "java_class_info"     "JavaClass -> TopLevel ()"
-
-  , prim "java_extract"
-    "JavaClass -> String -> JavaSetup () -> TopLevel Term"
-    (pureVal extractJava)
-    Deprecated
-    [ "Translate a Java method directly to a Term. The parameters of the"
-    , "Term will be the parameters of the Java method, and the return"
-    , "value will be the return value of the method. Only static methods"
-    , "with scalar argument and return types are currently supported. For"
-    , "more flexibility, see 'java_symexec' or 'java_verify'."
-    ]
-
-  , prim "java_symexec"
-    "JavaClass -> String -> [(String, Term)] -> [String] -> Bool -> TopLevel Term"
-    (pureVal symexecJava)
-    Deprecated
-    [ "Symbolically execute a Java method and construct a Term corresponding"
-    , "to its result. The first list contains pairs of variable or field"
-    , "names along with Terms specifying their initial (possibly symbolic)"
-    , "values. The second list contains the names of the variables or fields"
-    , "to treat as outputs. The resulting Term will be of tuple type, with"
-    , "as many elements as there are names in the output list."
-    , "The final boolean value indicates if path conditions should be checked for"
-    , "satisfiability at branch points."
-    ]
-
-  , prim "java_verify"
-    "JavaClass -> String -> [JavaMethodSpec] -> JavaSetup () -> TopLevel JavaMethodSpec"
-    (pureVal verifyJava)
-    Deprecated
-    [ "Verify a Java method against a method specification. The first two"
-    , "arguments are the same as for 'java_extract' and 'java_symexec'."
-    , "The list of JavaMethodSpec values in the third argument makes it"
-    , "possible to use the results of previous verifications to take the"
-    , "place of actual execution when encountering a method call. The last"
-    , "parameter is a setup block, containing a sequence of commands of type"
-    , "'JavaSetup a' that configure the symbolic simulator and specify the"
-    , "types of variables in scope, the expected results of execution, and"
-    , "the tactics to use to verify that the method produces the expected"
-    , "results."
-    ]
-
-{-  , prim "crucible_java_cfg"
-    "JavaClass -> String -> TopLevel CFG"
-    (bicVal crucible_java_cfg)
-    [ "Convert a Java method to a Crucible CFG."
-    ] -}
-
   , prim "jvm_extract"  "JavaClass -> String -> TopLevel Term"
     (pureVal CJ.jvm_extract)
     Current