Allow specifying Java with --java-bin-dirs or PATH

Most of the action happens in:

* The new `SAWScript.JavaTools` module, which exports functionality for
  locating a Java executable and finding its system properties.
* `SAWScript.Options`, which now exposes a new `--java-bin-dirs` flag.
  (Alternatively, one can use the `PATH`.) The `processEnv` function now
  performs additional post-processing based on whether `--java-bin-dirs`/`PATH`
  are set.

Fixes #1022, and paves the way to a better user experience for #861.

Other things:

* I ended up cargo-culting some `process`-related code from
  `SAWScript.Builtins` for use in `SAWScript.JavaTools`. To avoid blatant
  code duplication (and because I end up needing the exact same code later in
  another patch), I factored out this code into the new
  `SAWScript.ProcessUtils` module. I considered putting it in the existing
  `SAWScript.Utils` module, but that would have led to import cycles. Sigh.

CHANGES.md

@@ -1,3 +1,14 @@
+# Unreleased version
+
+## New Features
+
+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.
+When the path to Java is known, SAW can automatically add system-related
+JAR files to the JAR path, which eliminates the need to manually specify
+these files with `-j`.
+
 # Version 0.7
 
 ## New Features

doc/manual/manual.md

@@ -72,6 +72,11 @@ command-line options:
   ~ Specify a colon-delimited list of paths to `.jar` files to search
   for Java classes.
 
+`-b path, --java-bin-dirs`
+
+  ~ Specfy a colon-delimited list of paths to search for a Java
+    executable.
+
 `-d num, --sim-verbose=num`
 
   ~ Set the verbosity level of the Java and LLVM simulators.
@@ -87,14 +92,21 @@ SAW also uses several environment variables for configuration:
   ~ Specify a colon-delimited list of directory paths to search for Cryptol
   imports (including the Cryptol prelude).
 
+`PATH`
+
+  ~ If the `--java-bin-dirs` option is not set, then the `PATH` will be
+    searched to find a Java executable.
+
 `SAW_IMPORT_PATH`
 
   ~ Specify a colon-delimited list of directory paths to search for imports.
 
 `SAW_JDK_JAR`
 
   ~ Specify the path of the `.jar` file containing the core Java
-  libraries.
+  libraries. Note that that is not necessary if the `--java-bin-dirs` option
+  or the `PATH` environment variable is used, as SAW can use this information
+  to determine the location of the core Java libraries' `.jar` file.
 
 On Windows, semicolon-delimited lists are used instead of colon-delimited
 lists.
@@ -1530,18 +1542,23 @@ after 3.5, however, so report any parsing failures as [on
 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.
+structured nature of Java packages. First, when running `saw`, three flags
+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. Alternatively, one can put the directory where `java` lives on the
+  `PATH`, which SAW will search if `-b` is not set.
+
+* 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.
+
+Most Java programs will only require setting the `-b` flag, as that is enough
+to bring in the standard Java libraries.
 
 Once the class path is configured, you can pass the name of a class to
 the `java_load_class` function.

doc/tutorial/code/Makefile

@@ -1,7 +1,6 @@
 SAW?=../../bin/saw
 SAWS=$(wildcard *.saw)
 OUTS=$(SAWS:.saw=.out)
-JAVA_CLASSES=`(java -verbose 2>&1) | grep Opened | head -1 | cut -d ' ' -f 2 | cut -d ']' -f 1`
 
 all: FFS.class ffs.bc double.bc Add.class
 
@@ -14,7 +13,7 @@ run: all ${OUTS}
 	javac -g $<
 
 %.out: %.saw
-	${SAW} -j ${JAVA_CLASSES} $< 2>&1 | tee $@
+	${SAW} $< 2>&1 | tee $@
 
 clean:
 	rm -f *.bc *.class *.smt *.aig *.out

doc/tutorial/tutorial.md

@@ -228,19 +228,13 @@ First, we compile the Java code to a JVM class file.
 Like with `clang`, the `-g` flag instructs `javac` to include debugging
 information, which can be useful to preserve variable names.
 
-Using `saw` with Java code requires a command-line option `-j` that
-locates the Java standard libraries. Run the code in this section with
-the command:
+Using `saw` with Java code requires a command-line option `-b` that
+locates Java. Run the code in this section with the command:
 
-    > saw -j <path to rt.jar or classes.jar from JDK> ffs_compare.saw
+    > saw -b <path to directory where Java lives> ffs_compare.saw
 
-This path can also be specified in the `SAW_JDK_JAR` environment
-variable.
-
-For many versions of Java you can find the standard libraries JAR by
-grepping the output of `java -v`:
-
-    > java -v 2>&1 | grep Opened
+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
@@ -372,7 +366,7 @@ $include all code/java_add.saw
 
 This can be run as follows:
 
-    > saw -j <path to rt.jar or classes.jar from JDK> java_add.saw
+    > saw -b <path to directory where Java lives> java_add.saw
 
 In this example, the definitions of `add_spec` and `dbl_spec` provide
 extra information about how to configure the symbolic simulator when
@@ -481,11 +475,10 @@ implementations, instead.
 $include all code/ffs_java.saw
 ````
 
-As with previous Java examples, this one needs to be run with the `-j`
-flag to tell the interpreter where to find the Java standard
-libraries.
+As with previous Java examples, this one needs to be run with the `-b`
+flag to tell the interpreter where to find Java:
 
-    > saw -j <path to rt.jar or classes.jar from JDK> ffs_java.saw
+    > saw -b <path to directory where Java lives> ffs_java.saw
 
 AIG Export and Import
 ---------------------
@@ -515,7 +508,7 @@ We can use external AIGs to verify the equivalence as follows,
 generating the AIGs with the first script and comparing them with the
 second:
 
-    > saw -j <path to rt.jar or classes.jar from JDK> ffs_gen_aig.saw
+    > saw -b <path to directory where Java lives> ffs_gen_aig.saw
     > saw ffs_compare_aig.saw
 
 Files in AIGER format can be produced and processed by several

examples/ecdsa/Makefile

@@ -1,5 +1,4 @@
 SAW?=../../bin/saw
-JDK?=$(shell (java -verbose 2>&1) | grep Opened | head -1 | cut -d ' ' -f 2 | cut -d ']' -f 1)
 
 all : build
 
@@ -29,6 +28,6 @@ ecdsa.jar: build
 
 # Run the SAWScript verification
 verify : build
-	${SAW} -j "${JDK}" -c build ecdsa.saw
+	${SAW} -c build ecdsa.saw
 
 .PHONY : build clean doc run32 run64 verify

examples/simon-speck/run.sh

@@ -6,7 +6,7 @@ done
 if [ -z "$JAVA_HOME" ]; then
     echo "Need to set JAVA_HOME environment variable"
     exit 1
-fi  
+fi
 if [ ! -e simon.cry ]; then
   wget -q https://github.com/GaloisInc/cryptol/raw/master/examples/contrib/simon.cry
 fi
@@ -26,5 +26,5 @@ javac -g SimonEngine.java
 javac -g SpeckEngine.java
 saw simon.saw
 saw speck.saw
-saw -j $JAVA_HOME/jre/lib/rt.jar speck-java-bug-1.saw
-saw -j $JAVA_HOME/jre/lib/rt.jar speck-java-bug-2.saw
+saw -b $JAVA_HOME/bin speck-java-bug-1.saw
+saw -b $JAVA_HOME/bin speck-java-bug-2.saw

intTests/test_crucible_jvm/Makefile

@@ -1,7 +1,6 @@
 SAW?=../../bin/saw
 SAWS=$(wildcard *.saw)
 OUTS=$(SAWS:.saw=.out)
-JAVA_CLASSES=`(java -verbose 2>&1) | grep Opened | head -1 | cut -d ' ' -f 2 | cut -d ']' -f 1`
 
 all: FFS.class ffs.bc double.bc Add.class
 
@@ -14,7 +13,7 @@ run: all ${OUTS}
 	javac -g $<
 
 %.out: %.saw
-	${SAW} -j ${JAVA_CLASSES} $< 2>&1 | tee $@
+	${SAW} $< 2>&1 | tee $@
 
 clean:
 	rm -f *.bc *.class *.smt *.aig *.out

saw-script.cabal

@@ -46,7 +46,7 @@ library
     , exceptions
     , executable-path
     , extra
-    , directory
+    , directory >= 1.2.4.0
     , fgl
     , filepath
     , free
@@ -121,6 +121,7 @@ library
     SAWScript.JavaMethodSpec
     SAWScript.JavaMethodSpec.Evaluator
     SAWScript.JavaMethodSpecIR
+    SAWScript.JavaTools
     SAWScript.JavaUtils
     SAWScript.JavaPretty
     SAWScript.Lexer
@@ -129,6 +130,7 @@ library
     SAWScript.Panic
     SAWScript.Parser
     SAWScript.PathVC
+    SAWScript.ProcessUtils
     SAWScript.Proof
     SAWScript.Position
     SAWScript.SBVParser

src/SAWScript/Builtins.hs

@@ -125,6 +125,7 @@ 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
@@ -980,14 +981,7 @@ w4AbcVerilog _unints sc _hashcons g =
        -- Run ABC and remove temporaries
        let execName = "abc"
            args = ["-q", "%read " ++ tmp ++"; %blast; &sweep -C 5000; &syn4; &cec -m; write_aiger_cex " ++ tmpCex]
-       (ec, out, err) <- readProcessWithExitCode execName args ""
-       when (ec /= Exit.ExitSuccess) $
-          fail $ unlines [ "ABC returned non-zero exit code: " ++ show ec
-                         , "Standard output:"
-                         , out
-                         , "Standard error:"
-                         , err
-                         ]
+       (_out, _err) <- readProcessExitIfFailure execName args
        cexText <- readFile tmpCex
        removeFile tmp
        removeFile tmpCex

src/SAWScript/JavaTools.hs

@@ -0,0 +1,74 @@
+{- |
+Module      : SAWScript.JavaTools
+Description : Functionality for finding a Java executable and its properties.
+License     : BSD3
+Maintainer  : atomb
+Stability   : provisional
+-}
+
+module SAWScript.JavaTools
+  ( findJavaIn
+  , findJavaProperty
+  , findJavaMajorVersion
+  ) where
+
+import Data.List.Extra (dropPrefix, firstJust, stripInfix)
+import Data.Maybe
+import System.Directory
+
+import SAWScript.ProcessUtils
+
+-- | @'findJavaIn' javaBinDirs@ searches for an executable named @java@ in the
+-- directories in @javaBinDirs@. If @javaBinDirs@ is empty, then the @PATH@ is
+-- searched.
+--
+-- If the search finds at least one executable, then @Just@ the first result is
+-- returned. If no executables are found, then @Nothing@ is returned.
+findJavaIn :: [FilePath] -> IO (Maybe FilePath)
+findJavaIn javaBinDirs
+  | null javaBinDirs = findExecutable "java"
+  | otherwise        = listToMaybe <$> findExecutablesInDirectories javaBinDirs "java"
+
+-- | @'findJavaProperty' javaPath prop@ invokes @javaPath@ to dump its system
+-- properties (see <https://docs.oracle.com/javase/tutorial/essential/environment/sysprop.html>)
+-- and attempts to find the value associated with the property named @prop@.
+-- If such a value is found, then @Just@ that value is returned.
+-- If no property named @prop@ exists, then @Nothing@ is returned.
+--
+-- This will throw an exception if @javaPath@'s system properties cannot be
+-- determined.
+findJavaProperty :: FilePath -> String -> IO (Maybe String)
+findJavaProperty javaPath propertyNeedle = do
+  (_stdOut, stdErr) <- readProcessExitIfFailure javaPath ["-XshowSettings:properties", "-version"]
+  let propertyHaystacks = lines stdErr
+  pure $ firstJust getProperty_maybe propertyHaystacks
+  where
+    -- Each Java system property, as reported by
+    -- @java -XshowSettings:properties@, adheres to this template:
+    --
+    -- "  <prop> = <value>"
+    --
+    -- Note the leading whitespace. As a result, stripInfix is used to detect
+    -- "<prop> = " in the middle of the string and obtain the <value> after it.
+    getProperty_maybe :: String -> Maybe String
+    getProperty_maybe propertyHaystack =
+      snd <$> stripInfix (propertyNeedle ++ " = ") propertyHaystack
+
+-- | @'findJavaMajorVersion' javaPath@ will consult @javaPath@ to find the
+-- major version number corresponding to that Java release.
+findJavaMajorVersion :: FilePath -> IO Int
+findJavaMajorVersion javaPath = do
+  mbVersionStr <- findJavaProperty javaPath "java.version"
+  case mbVersionStr of
+    Nothing         -> fail $ "Could not detect the version of Java at " ++ javaPath
+    Just versionStr -> pure $ read $ takeMajorVersionStr $ dropOldJavaVersionPrefix versionStr
+  where
+    -- e.g., if the version number is "11.0.9.1", then just take the "11" part.
+    takeMajorVersionStr :: String -> String
+    takeMajorVersionStr = takeWhile (/= '.')
+
+    -- Prior to Java 9, the leading version number was always 1. For example,
+    -- Java 8 would use 1.8.<...>. We only care about the 8 part, so drop the
+    -- leading 1. bit.
+    dropOldJavaVersionPrefix :: String -> String
+    dropOldJavaVersionPrefix = dropPrefix "1."