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. This leverages `crucible-jvm`
changes from GaloisInc/crucible#634.

This fixes #861.

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.

Author: RyanGlScott

.github/ci.sh

@@ -199,7 +199,7 @@ bundle_files() {
 find_java() {
   pushd .github
   javac PropertiesTest.java
-  RT_JAR="$(java PropertiesTest | tr : '\n' | grep rt.jar | head -n 1)"
+  RT_JAR="$(java PropertiesTest | tr : '\n' | grep rt.jar | head -n 1 || true)"
   export RT_JAR
   echo "RT_JAR=$RT_JAR" >> "$GITHUB_ENV"
   rm PropertiesTest.class

.github/workflows/build.yml

@@ -38,6 +38,7 @@ jobs:
       matrix:
         os: [ubuntu-18.04]
         ghc: ["8.6.5", "8.8.4", "8.10.2"]
+        jdk: ["8", "15"]
         continue-on-error: [false]
         include:
           - os: macos-latest
@@ -52,7 +53,7 @@ jobs:
         exclude:
           - os: windows-latest
             ghc: "8.8.4"
-    name: SAWScript - GHC v${{ matrix.ghc }} - ${{ matrix.os }}
+    name: SAWScript - GHC v${{ matrix.ghc }} - JDK ${{ matrix.jdk }} - ${{ matrix.os }}
     env:
       RELEASE: ${{ needs.outputs.outputs.release }}
     continue-on-error: ${{ matrix.continue-on-error }}
@@ -111,7 +112,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.

deps/crucible

@@ -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/manual/manual.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`):

doc/tutorial/tutorial.md

@@ -46,7 +46,11 @@ for i in "$TESTBASE"/jars/*.jar; do
   if [ "$OS" == "Windows_NT" ]; then
     i=$(cygpath -w "$i")
   fi
-  CP=$CP$CPSEP$i
+  if [ -z "$CP" ]; then
+    CP=$i
+  else
+    CP=$CP$CPSEP$i
+  fi
 done
 export CP
 

intTests/runtests.sh

@@ -165,9 +165,9 @@ initialState readFileFn =
      ss <- basic_ss sc
      let jarFiles = []
          classPaths = []
-     jcb <- JSS.loadCodebase jarFiles classPaths
+         javaBinDirs = []
+     jcb <- JSS.loadCodebase jarFiles classPaths javaBinDirs
      let bic = BuiltinContext { biSharedContext = sc
-                              , biJavaCodebase = jcb
                               , biBasicSS = ss
                               }
      cenv <- initCryptolEnv sc

saw-remote-api/src/SAWServer.hs

@@ -85,7 +85,6 @@ library
     , utf8-string
     , what4 >= 0.4
     , vector
-    , xdg-basedir
     , GraphSCC
     , macaw-base
     , macaw-x86
@@ -115,15 +114,13 @@ library
     SAWScript.ImportAIG
     SAWScript.Interpreter
     SAWScript.JavaExpr
-    SAWScript.JavaTools
     SAWScript.JavaPretty
     SAWScript.Lexer
     SAWScript.LLVMBuiltins
     SAWScript.Options
     SAWScript.Panic
     SAWScript.Parser
     SAWScript.PathVC
-    SAWScript.ProcessUtils
     SAWScript.Proof
     SAWScript.Position
     SAWScript.SBVParser

saw-script.cabal

@@ -77,6 +77,9 @@ import Verifier.SAW.TypedAST
 
 import SAWScript.Position
 
+-- crucible-jvm
+import Lang.JVM.ProcessUtils
+
 -- cryptol-saw-core
 import qualified Verifier.SAW.CryptolEnv as CEnv
 
@@ -118,7 +121,6 @@ import SAWScript.ImportAIG
 
 import SAWScript.AST (getVal, pShow, Located(..))
 import SAWScript.Options as Opts
-import SAWScript.ProcessUtils
 import SAWScript.Proof
 import SAWScript.TopLevel
 import qualified SAWScript.Value as SV

src/SAWScript/Builtins.hs

@@ -418,7 +418,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 <- JCB.loadCodebase (jarList opts) (classPath opts) (javaBinDirs opts)
        currDir <- getCurrentDirectory
        Crucible.withHandleAllocator $ \halloc -> do
        let ro0 = TopLevelRO
@@ -433,7 +433,6 @@ buildTopLevelEnv proxy opts =
                    }
        let bic = BuiltinContext {
                    biSharedContext = sc
-                 , biJavaCodebase = jcb
                  , biBasicSS = ss
                  }
            primsAvail = Set.fromList [Current]

src/SAWScript/Interpreter.hs

@@ -21,7 +21,7 @@ import System.IO
 import Text.Read (readMaybe)
 import Text.Show.Functions ()
 
-import SAWScript.JavaTools
+import Lang.JVM.JavaTools
 
 -- TODO: wouldn't it be better to extract the options-processing code from this file and put it in saw/Main.hs (which already does part of the options processing)? It seems that other parts of SAW only need the datatype definition below, and not the rest.
 data Options = Options
@@ -207,8 +207,9 @@ processEnv opts = do
     -- --java-bin-dirs or PATH, see the Haddocks for findJavaIn), then use that
     -- to detect the path to Java's standard rt.jar file and add it to the
     -- jarList on Java 8 or earlier. (Later versions of Java do not use
-    -- rt.jar—see #861.) If Java's path is not specified, return the Options
-    -- unchanged.
+    -- rt.jar—see Note [Loading classes from JIMAGE files] in
+    -- Lang.JVM.Codebase in crucible-jvm.)
+    -- If Java's path is not specified, return the Options unchanged.
     addJavaBinDirInducedOpts :: Options -> IO Options
     addJavaBinDirInducedOpts os@Options{javaBinDirs} = do
       mbJavaPath <- findJavaIn javaBinDirs

src/SAWScript/JavaTools.hs

@@ -164,7 +164,6 @@ data SAW_CFG where
   JVM_CFG :: Crucible.AnyCFG JVM -> SAW_CFG
 
 data BuiltinContext = BuiltinContext { biSharedContext :: SharedContext
-                                     , biJavaCodebase  :: JSS.Codebase
                                      , biBasicSS       :: Simpset
                                      }
   deriving Generic