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.

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,22 @@ 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. TODO RGS: What should we do about this? It doesn't really serve a
+  useful purpose anymore now that `--java-bin-dirs`/`PATH` is used, and its
+  functionality is more limited than `--jars`. Perhaps we should deprecate
+  this?
 
 On Windows, semicolon-delimited lists are used instead of colon-delimited
 lists.

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

src/SAWScript/JavaTools.hs

@@ -0,0 +1,85 @@
+{- |
+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 Control.Monad
+import Data.List.Extra (dropPrefix, firstJust, stripInfix)
+import Data.Maybe
+import System.Directory
+import System.Exit
+import System.Process
+
+-- | @'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
+  -- TODO RGS: Is it worth factoring this process-related code out? We do basically the same thing elsewhere in
+  -- https://github.com/GaloisInc/saw-script/blob/a52e408da234f24dbc9847231efe04ab34c185b9/src/SAWScript/Builtins.hs#L968-L975
+  (ec, stdOut, stdErr) <- readProcessWithExitCode javaPath ["-XshowSettings:properties", "-version"] ""
+  when (ec /= ExitSuccess) $
+    fail $ unlines
+      [ javaPath ++ " returned non-zero exit code: " ++ show ec
+      , "Standard output:"
+      , stdOut
+      , "Standard error:"
+      , stdErr
+      ]
+  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."

src/SAWScript/Options.hs

@@ -6,6 +6,7 @@ Maintainer  : atomb
 Stability   : provisional
 -}
 {-# LANGUAGE CPP                 #-}
+{-# LANGUAGE NamedFieldPuns      #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 
 module SAWScript.Options where
@@ -20,11 +21,14 @@ import System.IO
 import Text.Read (readMaybe)
 import Text.Show.Functions ()
 
+import SAWScript.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
   { importPath       :: [FilePath]
   , classPath        :: [FilePath]
   , jarList          :: [FilePath]
+  , javaBinDirs      :: [FilePath]
   , verbLevel        :: Verbosity
   , simVerbose       :: Int
   , detectVacuity    :: Bool
@@ -61,6 +65,7 @@ defaultOptions
       importPath = ["."]
     , classPath = ["."]
     , jarList = []
+    , javaBinDirs = []
     , verbLevel = Info
     , printShowPos = False
     , printOutFn = printOutWith Info
@@ -123,6 +128,12 @@ options =
      "path"
     )
     pathDesc
+  , Option "b" ["java-bin-dirs"]
+    (ReqArg
+     (\p opts -> return opts { javaBinDirs = javaBinDirs opts ++ splitSearchPath p })
+     "path"
+    )
+    pathDesc
   , Option [] ["output-locations"]
     (NoArg
      (\opts -> return opts { printShowPos = True }))
@@ -184,14 +195,47 @@ readVerbosity s =
         "debug"               -> Debug
         _                     -> Debug
 
+-- | Perform some additional post-processing on an 'Options' value based on
+-- whether certain environment variables are defined.
 processEnv :: Options -> IO Options
 processEnv opts = do
   curEnv <- getEnvironment
-  return $ foldr addOpt opts curEnv
-    where addOpt ("SAW_IMPORT_PATH", p) os =
-            os { importPath = importPath os ++ splitSearchPath p }
-          addOpt ("SAW_JDK_JAR", p) os = os { jarList = p : jarList opts }
-          addOpt _ os = os
+  opts' <- addJavaBinDirInducedOpts opts
+  return $ foldr addSawOpt opts' curEnv
+  where
+    -- If a Java executable's path is specified (either by way of
+    -- --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.
+    addJavaBinDirInducedOpts :: Options -> IO Options
+    addJavaBinDirInducedOpts os@Options{javaBinDirs} = do
+      mbJavaPath <- findJavaIn javaBinDirs
+      case mbJavaPath of
+        Nothing       -> pure os
+        Just javaPath -> do
+          javaMajorVersion <- findJavaMajorVersion javaPath
+          if javaMajorVersion >= 9
+             then pure os
+             else addRTJar javaPath os
+
+    -- rt.jar lives in a standard location relative to @java.home@. At least,
+    -- this is the case on every operating system I've tested.
+    addRTJar :: FilePath -> Options -> IO Options
+    addRTJar javaPath os = do
+      mbJavaHome <- findJavaProperty javaPath "java.home"
+      case mbJavaHome of
+        Nothing -> fail $ "Could not find where rt.jar lives for " ++ javaPath
+        Just javaHome ->
+          let rtJarPath = javaHome </> "lib" </> "rt.jar" in
+          pure $ os{ jarList = rtJarPath : jarList os }
+
+    addSawOpt :: (String, String) -> Options -> Options
+    addSawOpt ("SAW_IMPORT_PATH", p) os =
+      os { importPath = importPath os ++ splitSearchPath p }
+    addSawOpt ("SAW_JDK_JAR", p) os = os { jarList = p : jarList os }
+    addSawOpt _ os = os
 
 pathDesc, pathDelim :: String
 

src/SAWScript/Utils.hs

@@ -115,7 +115,11 @@ lookupClass cb site nm = do
   case maybeCl of
     Nothing -> do
      let msg = ftext ("The Java class " ++ JSS.slashesToDots (JSS.unClassName nm) ++ " could not be found.")
-         res = "Please check that the --classpath and --jars options are set correctly."
+         res = unwords [ "Please check that the path to Java is set correctly"
+                       , "(either through the --java-bin-dirs option or your PATH)"
+                       , "and you are using Java 8 or earlier"
+                       , "(SAW does not support 9+ currently)."
+                       ]
       in throwIOExecException site msg res
     Just cl -> return cl