WIP: Support JDK 9 or later

This allows SAW to deal with JDK 9 or later, which packages its standard
library not in a JAR file, but in a JIMAGE file. Extracting `.class` files
from JIMAGE files proves to be surprisingly tricky, and I've carefully
documented the intricacies of doing so in
`Note [Loading classes from JIMAGE files]` in `SAWScript.JavaCodebase`.
This fixes #861.

This depends on #1030 to work.

Remaining tasks:

* Ideally, the code in `SAWScript.JavaCodebase` would be upstreamed to
  `crucible-jvm`, where the all-important `Codebase` data type lives.
  Unfortunately, some parts of SAW (e.g., `java_verify` still rely on
  the `jvm-verifier` library, which defines a separate `Codebase` type. SAW is
  in the process of phasing out the use of `jvm-verifier` in favor of
  `crucible-jvm` (see #993), but until that happens, I needed to introduce
  some ugly hacks in order to make everything typecheck.

  In particular, the (hopefully temporary) `SAWScript.JavaCodebase` module
  defines a shim version of `Codebase` that puts the experimental new things
  that I added in an `ExperimentalCodebase` constructor, but preserving the
  ability to use the `jvm-verifier` version of `Codebase` in the
  `LegacyCodebase` constructor. If JDK 8 or earlier is used, then
  `LegacyCodebase` is chosen, and if JDK 9 or later is used, then
  `ExperimentalCodebase` is chosen.

* Unfortunately, `java_verify` doesn't work with `ExperimentalCodebase`. Nor
  would we necessarily want to make this happen, as that would require
  upstreaming changes to `jvm-verifier`, which we are in the process of phasing
  out. As a result, this is blocked on #993.

* The CI should be updated to test more versions of the JDK than just 8.

Other things:

* I removed the dependency on the `xdg-basedir`, as it was unused. This
  dependency was likely added quite some time ago, and it appears that
  `saw-script` switched over to using XDG-related functionality from the
  `directory` library since then. I opted to use `directory` to find the
  `.cache` directory as well, so I have made that clear in the `.cabal` file.

Author: RyanGlScott

CHANGES.md

@@ -2,6 +2,8 @@
 
 ## New Features
 
+SAW now supports verifying Java code using JDK 9 or later.
+
 When verifying Java code, the path to Java can be specified with the new
 `--java-bin-dirs`/`-b` command-line option. Alternatively, if
 `--java-bin-dirs` is not set, then SAW searches the `PATH` to find Java.

doc/manual/manual.md

@@ -1544,17 +1544,12 @@ GitHub](https://github.com/GaloisInc/saw-script/issues).
 
 Loading Java code is slightly more complex, because of the more
 structured nature of Java packages. First, when running `saw`, two flags
-control where to look for classes. The `-j` flag takes the name of a JAR
-file as an argument and adds the contents of that file to the class
-database. The `-c` flag takes the name of a directory as an argument and
-adds all class files found in that directory (and its subdirectories) to
-the class database. By default, the current directory is included in the
-class path. However, the Java runtime and standard library (usually
-called `rt.jar`) is generally required for any non-trivial Java code,
-and can be installed in a wide variety of different locations.
-Therefore, for most Java analysis, you must provide the `-j` argument or
-the `SAW_JDK_JAR` environment variable to specify where to find this
-file.
+control where to look for classes. The `-b` flag takes the path where the
+`java` executable lives, which is used to locate the Java standard library
+classes and add them to the class database. The `-c` flag takes the name of a
+directory as an argument and adds all class files found in that directory (and
+its subdirectories) to the class database. By default, the current directory is
+included in the class path.
 
 Once the class path is configured, you can pass the name of a class to
 the `java_load_class` function.

saw-remote-api/src/SAWServer.hs

@@ -47,6 +47,7 @@ import Verifier.SAW.TypedTerm (TypedTerm, CryptolModule)
 
 import qualified SAWScript.Crucible.Common.MethodSpec as CMS (CrucibleMethodSpecIR)
 import qualified SAWScript.Crucible.LLVM.MethodSpecIR as CMS (SomeLLVM, LLVMModule)
+import SAWScript.JavaCodebase (loadCodebase)
 import SAWScript.JavaExpr (JavaType(..))
 import SAWScript.Options (defaultOptions)
 import SAWScript.Position (Pos(..))
@@ -167,7 +168,8 @@ initialState readFileFn =
      ss <- basic_ss sc
      let jarFiles = []
          classPaths = []
-     jcb <- JSS.loadCodebase jarFiles classPaths
+         javaBinDirs = []
+     jcb <- loadCodebase jarFiles classPaths javaBinDirs
      let bic = BuiltinContext { biSharedContext = sc
                               , biJavaCodebase = jcb
                               , biBasicSS = ss

saw-script.cabal

@@ -29,6 +29,7 @@ library
       base >= 4
     , aig
     , array
+    , base16-bytestring >= 0.1 && < 1.1
     , binary
     , bimap
     , bytestring
@@ -41,6 +42,7 @@ library
     , crucible-jvm
     , crucible-llvm >= 0.2
     , crucible-saw
+    , cryptohash-sha1 >= 0.11 && < 0.12
     , deepseq
     , either
     , exceptions
@@ -87,7 +89,6 @@ library
     , utf8-string
     , what4 >= 0.4
     , vector
-    , xdg-basedir
     , GraphSCC
     , macaw-base
     , macaw-x86
@@ -117,6 +118,7 @@ library
     SAWScript.ImportAIG
     SAWScript.Interpreter
     SAWScript.JavaBuiltins
+    SAWScript.JavaCodebase
     SAWScript.JavaExpr
     SAWScript.JavaMethodSpec
     SAWScript.JavaMethodSpec.Evaluator

src/SAWScript/Crucible/JVM/Builtins.hs

@@ -61,10 +61,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
@@ -112,6 +108,7 @@ import qualified SAWScript.Position as SS
 import SAWScript.Options
 import SAWScript.Crucible.JVM.BuiltinsJVM (prepareClassTopLevel)
 
+import SAWScript.JavaCodebase (Codebase)
 import SAWScript.JavaExpr (JavaType(..))
 
 import qualified SAWScript.Crucible.Common as Common
@@ -143,7 +140,7 @@ ppAbortedResult _cc = Common.ppAbortedResult (\_gp -> mempty)
 -- number of classes we load is way too large, and the classes take a
 -- long time to parse and translate.
 
-allClassRefs :: CB.Codebase -> J.ClassName -> IO (Set J.ClassName)
+allClassRefs :: Codebase -> J.ClassName -> IO (Set J.ClassName)
 allClassRefs cb c0 = go seen0 [c0]
   where
     seen0 = Set.fromList CJ.initClasses

src/SAWScript/Crucible/JVM/BuiltinsJVM.hs

@@ -73,6 +73,7 @@ import Verifier.SAW.TypedTerm (TypedTerm(..), abstractTypedExts)
 
 -- saw-script
 import SAWScript.Builtins(fixPos)
+import SAWScript.JavaCodebase (Codebase)
 import SAWScript.Value
 import SAWScript.Options(Options,simVerbose)
 import SAWScript.Crucible.LLVM.Builtins (setupArg, setupArgs, getGlobalPair, runCFG, baseCryptolType)
@@ -93,8 +94,12 @@ 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
+  lookupClass cb = J.lookupClassLegacy cb fixPos
+  findMethod  cb = J.findMethodLegacy  cb fixPos
+
+instance IsCodebase 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

src/SAWScript/Crucible/JVM/MethodSpecIR.hs

@@ -38,10 +38,6 @@ 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
-
 -- jvm-parser
 import qualified Language.JVM.Parser as J
 
@@ -51,6 +47,7 @@ import           Verifier.SAW.TypedTerm (TypedTerm)
 import           SAWScript.Crucible.Common (Sym)
 import qualified SAWScript.Crucible.Common.MethodSpec as MS
 import qualified SAWScript.Crucible.Common.Setup.Type as Setup
+import           SAWScript.JavaCodebase (Codebase)
 
 --------------------------------------------------------------------------------
 -- ** Language features
@@ -158,12 +155,12 @@ instance PPL.Pretty JVMPointsTo where
 --------------------------------------------------------------------------------
 -- *** JVMCrucibleContext
 
-type instance MS.Codebase CJ.JVM = CB.Codebase
+type instance MS.Codebase CJ.JVM = Codebase
 
 data JVMCrucibleContext =
   JVMCrucibleContext
   { _jccJVMClass       :: J.Class
-  , _jccCodebase       :: CB.Codebase
+  , _jccCodebase       :: Codebase
   , _jccJVMContext     :: CJ.JVMContext
   , _jccBackend        :: Sym -- This is stored inside field _ctxSymInterface of Crucible.SimContext; why do we need another one?
   , _jccHandleAllocator :: Crucible.HandleAllocator
@@ -176,7 +173,7 @@ type instance MS.CrucibleContext CJ.JVM = JVMCrucibleContext
 --------------------------------------------------------------------------------
 
 initialDefCrucibleMethodSpecIR ::
-  CB.Codebase ->
+  Codebase ->
   J.ClassName ->
   J.Method ->
   ProgramLoc ->

src/SAWScript/Interpreter.hs

@@ -51,6 +51,7 @@ import SAWScript.Builtins
 import SAWScript.Exceptions (failTypecheck)
 import qualified SAWScript.Import
 import SAWScript.JavaBuiltins
+import SAWScript.JavaCodebase (loadCodebase)
 import SAWScript.JavaExpr
 import SAWScript.LLVMBuiltins
 import SAWScript.Options
@@ -71,7 +72,6 @@ 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 Verifier.SAW.Cryptol.Prelude as CryptolSAW
@@ -421,7 +421,7 @@ buildTopLevelEnv proxy opts =
        simps <- scSimpset sc0 cryptolDefs [] convs
        let sc = rewritingSharedContext sc0 simps
        ss <- basic_ss sc
-       jcb <- JCB.loadCodebase (jarList opts) (classPath opts)
+       jcb <- loadCodebase (jarList opts) (classPath opts) (javaBinDirs opts)
        currDir <- getCurrentDirectory
        Crucible.withHandleAllocator $ \halloc -> do
        let ro0 = TopLevelRO

src/SAWScript/JavaBuiltins.hs

@@ -31,8 +31,8 @@ import Prettyprinter
 
 import Language.JVM.Common
 
-import Verifier.Java.Codebase hiding (lookupClass)
-import Verifier.Java.Simulator as JSS hiding (lookupClass)
+import Verifier.Java.Codebase hiding (lookupClass, Codebase)
+import Verifier.Java.Simulator as JSS hiding (lookupClass, Codebase)
 import Verifier.Java.SAWBackend
 
 import Verifier.SAW.Cryptol (importType, emptyEnv, exportFirstOrderValue)
@@ -46,6 +46,7 @@ import Verifier.SAW.CryptolEnv (schemaNoUser)
 
 import qualified SAWScript.CongruenceClosure as CC
 
+import SAWScript.JavaCodebase (Codebase, legacyCodebaseHack)
 import SAWScript.JavaExpr
 import SAWScript.JavaMethodSpec
 import SAWScript.JavaMethodSpecIR
@@ -64,7 +65,7 @@ import qualified Cryptol.Eval.Concrete as Cryptol (Concrete(..))
 import qualified Cryptol.TypeCheck.AST as Cryptol
 import qualified Cryptol.Utils.PP as Cryptol (pretty)
 
-loadJavaClass :: JSS.Codebase -> String -> IO Class
+loadJavaClass :: Codebase -> String -> IO Class
 loadJavaClass cb =
   lookupClass cb fixPos . mkClassName . dotsToSlashes
 
@@ -112,7 +113,7 @@ symexecJava cls mname inputs outputs satBranches = do
                           " argument in method " ++ methodName meth
       pidx = fromIntegral . localIndexOfParameter meth
   withSAWBackend Nothing $ \sbe -> io $ do
-    runSimulator cb sbe defaultSEH (Just fl) $ do
+    runSimulator (legacyCodebaseHack cb) sbe defaultSEH (Just fl) $ do
       setVerbosity (simVerbose opts)
       assigns <- mapM mkAssign inputs
       let (argAssigns, otherAssigns) = partition (isArg meth . fst) assigns
@@ -164,7 +165,7 @@ extractJava cls mname setup = do
     let fl = defaultSimFlags { alwaysBitBlastBranchTerms =
                                  jsSatBranches setupRes }
         meth = specMethod (jsSpec setupRes)
-    io $ runSimulator cb sbe defaultSEH (Just fl) $ do
+    io $ runSimulator (legacyCodebaseHack cb) sbe defaultSEH (Just fl) $ do
       setVerbosity (simVerbose opts)
       argTypes <- either fail return (getActualArgTypes setupRes)
       args <- mapM (freshJavaVal (Just argsRef) sc) argTypes
@@ -247,8 +248,8 @@ verifyJava cls mname overrides setup = do
       liftIO $ bsCheckAliasTypes pos bs
       liftIO $ printOutLn opts Debug $ "Executing " ++ specName ms ++
                    " at PC " ++ show (bsLoc bs) ++ "."
-      -- runDefSimulator cb sbe $ do
-      runSimulator cb sbe defaultSEH (Just fl) $ do
+      -- runDefSimulator (legacyCodebaseHack cb) sbe $ do
+      runSimulator (legacyCodebaseHack cb) sbe defaultSEH (Just fl) $ do
         setVerbosity (simVerbose opts)
         let prover script vs n g = do
               let exts = getAllExts g
@@ -381,7 +382,7 @@ checkCompatibleType _sc msg aty schema =
                 ]
 
 parseJavaExpr' :: (MonadIO m) =>
-                  JSS.Codebase -> JSS.Class -> JSS.Method -> String
+                  Codebase -> JSS.Class -> JSS.Method -> String
                -> m JavaExpr
 parseJavaExpr' cb cls meth name =
   liftIO (runExceptT (parseJavaExpr cb cls meth name) >>= either fail return)
@@ -401,7 +402,7 @@ getJavaExpr ctx name = do
       , ftext "Maybe you're missing a `java_var` or `java_class_var`?"
       ]
 
-typeJavaExpr :: JSS.Codebase -> String -> JavaType
+typeJavaExpr :: Codebase -> String -> JavaType
              -> JavaSetup (JavaExpr, JavaActualType)
 typeJavaExpr cb name ty = do
   ms <- gets jsSpec