Merge pull request #1046 from GaloisInc/wip/T861-take-two

Experimental support for loading JIMAGE (JDK 9+) files

CHANGES.md

@@ -2,6 +2,12 @@
 
 ## New Features
 
+SAW now includes experimental support for verifying Java code using JDK 9 or
+later. Verifying Java code that only uses primitive data types is known to work
+well, but code that imports certain classes (e.g., `String`) is known to suffer
+from issues documented
+[here](https://github.com/GaloisInc/crucible/issues/641).
+
 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

@@ -1575,9 +1575,11 @@ 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.
+support for JDK 9 and later is experimental. Verifying code that only uses
+primitive data types is known to work well, but there are some as-of-yet
+unresolved issues in verifying code involving classes such as `String`. For
+more information on these issues, refer to
+[this GitHub issue](https://github.com/GaloisInc/crucible/issues/641).
 
 ## Notes on Compiling Code for SAW
 

doc/tutorial/tutorial.md

@@ -237,9 +237,11 @@ 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.
+SAW also includes experimental support for JDK 9 and later. Code that only
+involves primitive data types (such as `FFS.java` above) is known to work well
+under JDK 9+, but there are some as-of-yet unresolved issues in verifying code
+involving classes such as `String`. For more information on these issues, refer
+to [this GitHub issue](https://github.com/GaloisInc/crucible/issues/641).
 
 Now we can do the proof both within and across languages (from
 `ffs_compare.saw`):

saw-remote-api/src/SAWServer.hs

@@ -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-script.cabal

@@ -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

src/SAWScript/Builtins.hs

@@ -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/Interpreter.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/Options.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/Value.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