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.

Remaining tasks:

* Ideally, the code in `SAWScript.JavaCodebase` would be upstreamed to
  `crucible-jvm`, where the all-important `Codebase` data type lives.
  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 version of `Codebase` that keeps
  track of JIMAGE-related paths.

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.

* The `biJavaCodebase :: Codebase` field of `BuiltinContext` is completely
  unused, which I noticed when making changes to the `Codebase` type. Let's
  just remove it. This fixes #1003.

Author: RyanGlScott

.github/workflows/build.yml

@@ -35,6 +35,7 @@ jobs:
       matrix:
         os: [ubuntu-latest]
         ghc: ["8.6.5", "8.8.4", "8.10.2"]
+        jdk: ["8", "15"]
         continue-on-error: [false]
         include:
           - os: macos-latest
@@ -108,7 +109,7 @@ jobs:
 
       - uses: actions/setup-java@v1
         with:
-          java-version: "8"
+          java-version: ${{ matrix.jdk }}
           java-package: jdk
           architecture: x64
 

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

@@ -1568,10 +1568,7 @@ the `java_load_class` function.
 The resulting `JavaClass` can be passed into the various functions
 described below to perform analysis of specific Java methods.
 
-Java class files from any JDK newer than version 6 should work. However,
-JDK version 9 and newer do not contain a JAR file containing the
-standard libraries, and therefore do not currently work with SAW. We are
-investigating the best way to resolve this issue.
+Java class files from any JDK newer than version 6 should work.
 
 ## Notes on Compiling Code for SAW
 

doc/tutorial/tutorial.md

@@ -236,10 +236,7 @@ locates Java. Run the code in this section with the command:
 Alternatively, if Java is located on your `PATH`, you can omit the `-b`
 option entirely.
 
-Both Oracle JDK and OpenJDK versions 6 through 8 work well with SAW.
-From version 9 onward, the core libraries are no longer stored in a
-standard JAR file, making them inacessible to SAW. We're currently
-considering strategies for working with newer Java versions.
+Both Oracle JDK and OpenJDK versions 6 and later work well with SAW.
 
 Now we can do the proof both within and across languages (from
 `ffs_compare.saw`):

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(..))
@@ -165,9 +166,9 @@ 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
                               }
      cenv <- initCryptolEnv sc

saw-script.cabal

@@ -29,6 +29,7 @@ library
       base >= 4
     , aig
     , array
+    , base16-bytestring >= 0.1 && < 1.1
     , binary
     , bimap
     , bytestring
@@ -40,6 +41,7 @@ library
     , crucible >= 0.4
     , crucible-jvm
     , crucible-llvm >= 0.2
+    , cryptohash-sha1 >= 0.11 && < 0.12
     , deepseq
     , either
     , exceptions
@@ -85,7 +87,6 @@ library
     , utf8-string
     , what4 >= 0.4
     , vector
-    , xdg-basedir
     , GraphSCC
     , macaw-base
     , macaw-x86
@@ -114,6 +115,7 @@ library
     SAWScript.Import
     SAWScript.ImportAIG
     SAWScript.Interpreter
+    SAWScript.JavaCodebase
     SAWScript.JavaExpr
     SAWScript.JavaTools
     SAWScript.JavaPretty

src/SAWScript/Crucible/JVM/Builtins.hs

@@ -84,7 +84,6 @@ 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
@@ -107,6 +106,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
@@ -138,7 +138,7 @@ ppJVMAbortedResult _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

@@ -74,6 +74,7 @@ import Verifier.SAW.Simulator.What4.ReturnTrip
 
 -- saw-script
 import SAWScript.Builtins(fixPos)
+import SAWScript.JavaCodebase (Codebase)
 import SAWScript.Value
 import SAWScript.Options(Options,simVerbose)
 import SAWScript.Crucible.Common
@@ -83,14 +84,17 @@ 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 Lang.JVM.Codebase as JCB
 
 -- crucible-jvm
 import           Lang.Crucible.JVM (IsCodebase(..))
 import qualified Lang.Crucible.JVM as CJ
 
 import Debug.Trace
 
+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
 -- methods and static fields

src/SAWScript/Crucible/JVM/MethodSpecIR.hs

@@ -37,7 +37,6 @@ import qualified Lang.Crucible.FunctionHandle as Crucible (HandleAllocator)
 
 -- crucible-jvm
 import qualified Lang.Crucible.JVM as CJ
-import qualified Lang.JVM.Codebase as CB
 
 -- jvm-parser
 import qualified Language.JVM.Parser as J
@@ -48,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
@@ -177,12 +177,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
@@ -195,7 +195,7 @@ type instance MS.CrucibleContext CJ.JVM = JVMCrucibleContext
 --------------------------------------------------------------------------------
 
 initialDefCrucibleMethodSpecIR ::
-  CB.Codebase ->
+  Codebase ->
   J.ClassName ->
   J.Method ->
   ProgramLoc ->

src/SAWScript/Interpreter.hs

@@ -50,6 +50,7 @@ import SAWScript.AST (Located(..),Import(..))
 import SAWScript.Builtins
 import SAWScript.Exceptions (failTypecheck)
 import qualified SAWScript.Import
+import SAWScript.JavaCodebase (loadCodebase)
 import SAWScript.JavaExpr
 import SAWScript.LLVMBuiltins
 import SAWScript.Options
@@ -70,8 +71,6 @@ import Verifier.SAW.TypedAST
 import Verifier.SAW.TypedTerm
 import qualified Verifier.SAW.CryptolEnv as CEnv
 
-import qualified Lang.JVM.Codebase as JCB
-
 import qualified Verifier.SAW.Cryptol.Prelude as CryptolSAW
 
 -- Crucible
@@ -418,7 +417,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
@@ -433,7 +432,6 @@ buildTopLevelEnv proxy opts =
                    }
        let bic = BuiltinContext {
                    biSharedContext = sc
-                 , biJavaCodebase = jcb
                  , biBasicSS = ss
                  }
            primsAvail = Set.fromList [Current]