crucible-jvm: Add --java-bin-dirs

This mirrors a similar recent change introduced to SAW in
GaloisInc/saw-script#1030.

While I was in town, I updated the two `crucible-jvm`–related test suites
to use the `PATH` instead of the `-j` flag. I can't exactly confirm via CI
if these changes work (see #634), but they appear to do the right thing
locally.

Fixes #633.

crucible-jvm/crucible-jvm.cabal

@@ -57,13 +57,15 @@ library
     containers,
     crucible,
     directory,
+    extra >= 1.6.4,
     filepath,
     haskeline >= 0.7,
     jvm-parser >= 0.3,
     lens,
     mtl >= 2.1,
     parameterized-utils >= 1.0 && < 2.2,
     pretty >= 1.1,
+    process,
     split >= 0.2,
     text,
     transformers >= 0.3,
@@ -85,6 +87,7 @@ library
     Lang.Crucible.JVM.ClassRefs
     Lang.Crucible.JVM.Overrides
     Lang.JVM.Codebase
+    Lang.JVM.JavaTools
   other-modules:
 
   ghc-options: -Wall -Wcompat -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns

crucible-jvm/src/Lang/JVM/JavaTools.hs

@@ -0,0 +1,110 @@
+{- |
+Module      : Lang.JVM.JavaTools
+Description : Functionality for finding a Java executable and its properties.
+Copyright   : (c) Galois, Inc 2021
+License     : BSD3
+Maintainer  : [email protected]
+Stability   : provisional
+-}
+
+module Lang.JVM.JavaTools
+  ( findJavaIn, findJimageIn, findJavaToolIn
+  , findJavaProperty
+  , findJavaMajorVersion
+  ) where
+
+import Control.Monad (when)
+import Data.List.Extra (dropPrefix, firstJust, stripInfix)
+import Data.Maybe
+import System.Directory
+import System.Exit (ExitCode(..))
+import System.Process (readProcessWithExitCode)
+
+-- | @'findJavaIn' searchPaths@ searches for an executable named @java@ among
+-- the directories in @searchPaths@. If @searchPaths@ 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 = findJavaToolIn "java"
+
+-- | @'findJavaIn' searchPaths@ searches for an executable named @java@ among
+-- the directories in @searchPaths@. If @searchPaths@ 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.
+findJimageIn :: [FilePath] -> IO (Maybe FilePath)
+findJimageIn = findJavaToolIn "jimage"
+
+-- | @'findJavaToolIn' toolName searchPaths@ searches for an executable named
+-- @toolName@ among the directories in @searchPaths@. If @searchPaths@ 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.
+findJavaToolIn :: FilePath -> [FilePath] -> IO (Maybe FilePath)
+findJavaToolIn toolName searchPaths
+  | null searchPaths = findExecutable toolName
+  | otherwise        = listToMaybe <$> findExecutablesInDirectories searchPaths toolName
+
+-- | @'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."
+
+-- | Invokes @readProcessWithExitCode@ with no standard input, and returns the
+-- resulting standard output and standard error. If the exit code of the
+-- process is not 'ExitSuccess', throw an exception with some information that
+-- may be helpful to debug what went wrong.
+readProcessExitIfFailure :: FilePath -> [String] -> IO (String, String)
+readProcessExitIfFailure cmd args = do
+  (ec, out, err) <- readProcessWithExitCode cmd args ""
+  when (ec /= ExitSuccess) $
+     fail $ unlines [ cmd ++ " returned non-zero exit code: " ++ show ec
+                    , "Standard output:"
+                    , out
+                    , "Standard error:"
+                    , err
+                    ]
+  pure (out, err)

crucible-jvm/tests/ashes/README.md

@@ -4,13 +4,15 @@ How to run the ashes test suite.
 
 2. compile crucible-jvm   (`cabal new-build` in `saw-script/deps/crucible/crucible-jvm/`)
 
-3. make sure that `runcrucible.sh` includes correct reference to `rt.jar` for your
-   system (and the correct reference to the crucible-jvm executable)
+3. make sure that either:
+
+   (a) Java is on the `PATH`, or
+   (b) `runcrucible.sh` points to Java's location with the `-b` flag
 
 4. `./runAshes.hs`
 
 5. To run a single test, ghci runAshes.hs and then edit `wip` to that test name.
 
 These instructions assume that you are using cabal new-build to
 compile crucible-jvm. If using stack, need to edit `runcrucible.sh` to
-the correct way to invoke the crucible-jvm executable.
+the correct way to invoke the crucible-jvm executable.

crucible-jvm/tests/ashes/runcrucible.sh

@@ -1,5 +1,3 @@
 #!/bin/bash
 
-RTJAR=/Library/Java/JavaVirtualMachines/jdk1.8.0_171.jdk/Contents/Home/jre/lib/rt.jar
-
-cabal new-exec crucible-jvm -- -j $RTJAR $@
+cabal new-exec crucible-jvm -- $@

crucible-jvm/tests/test.sh

@@ -1,8 +1,5 @@
 TESTCASE=Str
 
-RTJAR=/Library/Java/JavaVirtualMachines/jdk1.8.0_171.jdk/Contents/Home/jre/lib/rt.jar
-
-
 make $TESTCASE.class
 javap -c $TESTCASE
-cabal new-exec crucible-jvm -- -d 3 -j $RTJAR $TESTCASE.java
+cabal new-exec crucible-jvm -- -d 3 $TESTCASE.java

crucible-jvm/tool/Main.hs

@@ -17,6 +17,7 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# Language ImplicitParams #-}
+{-# Language NamedFieldPuns #-}
 
 {-# OPTIONS_GHC -fno-warn-missing-signatures #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
@@ -40,7 +41,7 @@ import System.Console.GetOpt
 import System.IO
 import System.Environment(getProgName,getArgs)
 import System.Exit (ExitCode(..), exitWith, exitFailure)
-import System.FilePath(takeExtension,takeBaseName)
+import System.FilePath((</>),takeExtension,takeBaseName)
 import System.FilePath(splitSearchPath)
 
 import Data.Parameterized.Nonce(withIONonceGenerator)
@@ -80,6 +81,7 @@ import qualified Crux.Config.Common as Crux
 
 
 import qualified Lang.JVM.Codebase as JCB
+import           Lang.JVM.JavaTools
 
 import           Lang.Crucible.JVM.Simulate (setupCrucibleJVMCrux)
 import           Lang.Crucible.JVM.Types
@@ -99,17 +101,44 @@ data JVMOptions = JVMOptions
     -- this must include rt.jar from the JDK
     -- (The JDK_JAR environment variable can also be used to
     -- to specify this JAR).
+  , javaBinDirs      :: [FilePath]
+    -- ^ where to look to find the @java@ executable
   , mainMethod       :: String
   }
 
 defaultOptions :: JVMOptions
 defaultOptions =
   JVMOptions
-  { classPath  = ["."]
-  , jarList    = []
-  , mainMethod = "main"
+  { classPath   = ["."]
+  , jarList     = []
+  , javaBinDirs = []
+  , mainMethod  = "main"
   }
 
+-- | Perform some additional post-processing on a 'JVMOptions' value based on
+-- whether @--java-bin-dirs@ (or the @PATH@) is set.
+processJVMOptions :: JVMOptions -> IO JVMOptions
+processJVMOptions opts@JVMOptions{javaBinDirs} = do
+  mbJavaPath <- findJavaIn javaBinDirs
+  case mbJavaPath of
+    Nothing       -> pure opts
+    Just javaPath -> do
+      javaMajorVersion <- findJavaMajorVersion javaPath
+      if javaMajorVersion >= 9
+         then pure opts
+         else addRTJar javaPath opts
+  where
+    -- 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 -> JVMOptions -> IO JVMOptions
+    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 }
+
 cruxJVMConfig :: Crux.Config JVMOptions
 cruxJVMConfig = Crux.Config
   { Crux.cfgFile = pure defaultOptions
@@ -129,6 +158,11 @@ cruxJVMConfig = Crux.Config
         $ Crux.ReqArg "TODO"
         $ \p opts ->
             Right $ opts { jarList = jarList opts ++ splitSearchPath p }
+      , Crux.Option ['b'] ["java-bin-dirs"]
+        "TODO"
+        $ Crux.ReqArg "TODO"
+        $ \p opts ->
+            Right $ opts { javaBinDirs = javaBinDirs opts ++ splitSearchPath p }
       , Crux.Option ['m'] ["method"]
         "Method to simulate"
         $ Crux.ReqArg "method name"
@@ -164,6 +198,7 @@ simulateJVM copts opts = Crux.SimulatorCallback $ \sym _maybeOnline -> do
 main :: IO ()
 main =
   Crux.loadOptions Crux.defaultOutputConfig "crux-jvm" "0.1" cruxJVMConfig $
-    \(cruxOpts, jvmOpts) ->
+    \(cruxOpts, jvmOpts) -> do
+      jvmOpts' <- processJVMOptions jvmOpts
       exitWith =<< Crux.postprocessSimResult cruxOpts =<<
-        Crux.runSimulator cruxOpts (simulateJVM cruxOpts jvmOpts)
+        Crux.runSimulator cruxOpts (simulateJVM cruxOpts jvmOpts')