Skip to content

Commit

Permalink
WIP: Support JDK 9 or later
Browse files Browse the repository at this point in the history
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. Extracting `.class` files
from JIMAGE files proves to be surprisingly tricky, and I've carefully
documented the intricacies of doing so in
`Note [Loading classes from JIMAGE files]` in `SAWScript.JavaCodebase`.
This fixes #861.

Remaining tasks:

* Ideally, the code in `SAWScript.JavaCodebase` would be upstreamed to
  `crucible-jvm`, where the all-important `Codebase` data type lives.
  Unfortunately, some parts of SAW (e.g., `java_verify` still rely on
  the `jvm-verifier` library, which defines a separate `Codebase` type. SAW is
  in the process of phasing out the use of `jvm-verifier` in favor of
  `crucible-jvm` (see #993), but until that happens, I needed to introduce
  some ugly hacks in order to make everything typecheck.

  In particular, the (hopefully temporary) `SAWScript.JavaCodebase` module
  defines a shim version of `Codebase` that puts the experimental new things
  that I added in an `ExperimentalCodebase` constructor, but preserving the
  ability to use the `jvm-verifier` version of `Codebase` in the
  `LegacyCodebase` constructor. If JDK 8 or earlier is used, then
  `LegacyCodebase` is chosen, and if JDK 9 or later is used, then
  `ExperimentalCodebase` is chosen.

* Unfortunately, `java_verify` doesn't work with `ExperimentalCodebase`. Nor
  would we necessarily want to make this happen, as that would require
  upstreaming changes to `jvm-verifier`, which we are in the process of phasing
  out. As a result, this is blocked on #993.

* The CI should be updated to test more versions of the JDK than just 8.

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.
  • Loading branch information
RyanGlScott committed Jan 29, 2021
1 parent 50e325f commit d4189fd
Show file tree
Hide file tree
Showing 16 changed files with 545 additions and 50 deletions.
2 changes: 2 additions & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
4 changes: 3 additions & 1 deletion saw-remote-api/src/SAWServer.hs
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,7 @@ import Verifier.SAW.TypedTerm (TypedTerm, CryptolModule)

import qualified SAWScript.Crucible.Common.MethodSpec as CMS (CrucibleMethodSpecIR)
import qualified SAWScript.Crucible.LLVM.MethodSpecIR as CMS (SomeLLVM, LLVMModule)
import SAWScript.JavaCodebase (loadCodebase)
import SAWScript.JavaExpr (JavaType(..))
import SAWScript.Options (defaultOptions)
import SAWScript.Position (Pos(..))
Expand Down Expand Up @@ -167,7 +168,8 @@ initialState readFileFn =
ss <- basic_ss sc
let jarFiles = []
classPaths = []
jcb <- JSS.loadCodebase jarFiles classPaths
javaBinDirs = []
jcb <- loadCodebase jarFiles classPaths javaBinDirs
let bic = BuiltinContext { biSharedContext = sc
, biJavaCodebase = jcb
, biBasicSS = ss
Expand Down
4 changes: 3 additions & 1 deletion saw-script.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,7 @@ library
base >= 4
, aig
, array
, base16-bytestring >= 0.1 && < 1.1
, binary
, bimap
, bytestring
Expand All @@ -41,6 +42,7 @@ library
, crucible-jvm
, crucible-llvm >= 0.2
, crucible-saw
, cryptohash-sha1 >= 0.11 && < 0.12
, deepseq
, either
, exceptions
Expand Down Expand Up @@ -87,7 +89,6 @@ library
, utf8-string
, what4 >= 0.4
, vector
, xdg-basedir
, GraphSCC
, macaw-base
, macaw-x86
Expand Down Expand Up @@ -117,6 +118,7 @@ library
SAWScript.ImportAIG
SAWScript.Interpreter
SAWScript.JavaBuiltins
SAWScript.JavaCodebase
SAWScript.JavaExpr
SAWScript.JavaMethodSpec
SAWScript.JavaMethodSpec.Evaluator
Expand Down
7 changes: 2 additions & 5 deletions src/SAWScript/Crucible/JVM/Builtins.hs
Original file line number Diff line number Diff line change
Expand Up @@ -61,10 +61,6 @@ import Data.Void (absurd)
import Prettyprinter
import System.IO

-- jvm-verifier
-- TODO: transition to Lang.JVM.Codebase from crucible-jvm
import qualified Verifier.Java.Codebase as CB

-- cryptol
import qualified Cryptol.Eval.Type as Cryptol (evalValType)
import qualified Cryptol.TypeCheck.Type as Cryptol
Expand Down Expand Up @@ -112,6 +108,7 @@ import qualified SAWScript.Position as SS
import SAWScript.Options
import SAWScript.Crucible.JVM.BuiltinsJVM (prepareClassTopLevel)

import SAWScript.JavaCodebase (Codebase)
import SAWScript.JavaExpr (JavaType(..))

import qualified SAWScript.Crucible.Common as Common
Expand Down Expand Up @@ -143,7 +140,7 @@ ppAbortedResult _cc = Common.ppAbortedResult (\_gp -> mempty)
-- number of classes we load is way too large, and the classes take a
-- long time to parse and translate.

allClassRefs :: CB.Codebase -> J.ClassName -> IO (Set J.ClassName)
allClassRefs :: Codebase -> J.ClassName -> IO (Set J.ClassName)
allClassRefs cb c0 = go seen0 [c0]
where
seen0 = Set.fromList CJ.initClasses
Expand Down
9 changes: 7 additions & 2 deletions src/SAWScript/Crucible/JVM/BuiltinsJVM.hs
Original file line number Diff line number Diff line change
Expand Up @@ -73,6 +73,7 @@ import Verifier.SAW.TypedTerm (TypedTerm(..), abstractTypedExts)

-- saw-script
import SAWScript.Builtins(fixPos)
import SAWScript.JavaCodebase (Codebase)
import SAWScript.Value
import SAWScript.Options(Options,simVerbose)
import SAWScript.Crucible.LLVM.Builtins (setupArg, setupArgs, getGlobalPair, runCFG, baseCryptolType)
Expand All @@ -93,8 +94,12 @@ import Debug.Trace
-- | Use the Codebase implementation from the old Java static simulator
--
instance IsCodebase JCB.Codebase where
lookupClass cb = J.lookupClass cb fixPos
findMethod cb = J.findMethod cb fixPos
lookupClass cb = J.lookupClassLegacy cb fixPos
findMethod cb = J.findMethodLegacy cb fixPos

instance IsCodebase Codebase where
lookupClass cb = J.lookupClass cb fixPos
findMethod cb = J.findMethod cb fixPos

-----------------------------------------------------------------------
-- | Make sure the class is in the database and allocate handles for its
Expand Down
11 changes: 4 additions & 7 deletions src/SAWScript/Crucible/JVM/MethodSpecIR.hs
Original file line number Diff line number Diff line change
Expand Up @@ -38,10 +38,6 @@ import qualified Lang.Crucible.FunctionHandle as Crucible (HandleAllocator)
-- crucible-jvm
import qualified Lang.Crucible.JVM as CJ

-- jvm-verifier
-- TODO: transition to Lang.JVM.Codebase from crucible-jvm
import qualified Verifier.Java.Codebase as CB

-- jvm-parser
import qualified Language.JVM.Parser as J

Expand All @@ -51,6 +47,7 @@ import Verifier.SAW.TypedTerm (TypedTerm)
import SAWScript.Crucible.Common (Sym)
import qualified SAWScript.Crucible.Common.MethodSpec as MS
import qualified SAWScript.Crucible.Common.Setup.Type as Setup
import SAWScript.JavaCodebase (Codebase)

--------------------------------------------------------------------------------
-- ** Language features
Expand Down Expand Up @@ -180,12 +177,12 @@ instance PPL.Pretty JVMPointsTo where
--------------------------------------------------------------------------------
-- *** JVMCrucibleContext

type instance MS.Codebase CJ.JVM = CB.Codebase
type instance MS.Codebase CJ.JVM = Codebase

data JVMCrucibleContext =
JVMCrucibleContext
{ _jccJVMClass :: J.Class
, _jccCodebase :: CB.Codebase
, _jccCodebase :: Codebase
, _jccJVMContext :: CJ.JVMContext
, _jccBackend :: Sym -- This is stored inside field _ctxSymInterface of Crucible.SimContext; why do we need another one?
, _jccHandleAllocator :: Crucible.HandleAllocator
Expand All @@ -198,7 +195,7 @@ type instance MS.CrucibleContext CJ.JVM = JVMCrucibleContext
--------------------------------------------------------------------------------

initialDefCrucibleMethodSpecIR ::
CB.Codebase ->
Codebase ->
J.ClassName ->
J.Method ->
ProgramLoc ->
Expand Down
4 changes: 2 additions & 2 deletions src/SAWScript/Interpreter.hs
Original file line number Diff line number Diff line change
Expand Up @@ -51,6 +51,7 @@ import SAWScript.Builtins
import SAWScript.Exceptions (failTypecheck)
import qualified SAWScript.Import
import SAWScript.JavaBuiltins
import SAWScript.JavaCodebase (loadCodebase)
import SAWScript.JavaExpr
import SAWScript.LLVMBuiltins
import SAWScript.Options
Expand All @@ -71,7 +72,6 @@ import Verifier.SAW.TypedAST
import Verifier.SAW.TypedTerm
import qualified Verifier.SAW.CryptolEnv as CEnv

import qualified Verifier.Java.Codebase as JCB
import qualified Verifier.Java.SAWBackend as JavaSAW

import qualified Verifier.SAW.Cryptol.Prelude as CryptolSAW
Expand Down Expand Up @@ -421,7 +421,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 <- loadCodebase (jarList opts) (classPath opts) (javaBinDirs opts)
currDir <- getCurrentDirectory
Crucible.withHandleAllocator $ \halloc -> do
let ro0 = TopLevelRO
Expand Down
19 changes: 10 additions & 9 deletions src/SAWScript/JavaBuiltins.hs
Original file line number Diff line number Diff line change
Expand Up @@ -31,8 +31,8 @@ import Prettyprinter

import Language.JVM.Common

import Verifier.Java.Codebase hiding (lookupClass)
import Verifier.Java.Simulator as JSS hiding (lookupClass)
import Verifier.Java.Codebase hiding (lookupClass, Codebase)
import Verifier.Java.Simulator as JSS hiding (lookupClass, Codebase)
import Verifier.Java.SAWBackend

import Verifier.SAW.Cryptol (importType, emptyEnv, exportFirstOrderValue)
Expand All @@ -46,6 +46,7 @@ import Verifier.SAW.CryptolEnv (schemaNoUser)

import qualified SAWScript.CongruenceClosure as CC

import SAWScript.JavaCodebase (Codebase, legacyCodebaseHack)
import SAWScript.JavaExpr
import SAWScript.JavaMethodSpec
import SAWScript.JavaMethodSpecIR
Expand All @@ -64,7 +65,7 @@ import qualified Cryptol.Eval.Concrete as Cryptol (Concrete(..))
import qualified Cryptol.TypeCheck.AST as Cryptol
import qualified Cryptol.Utils.PP as Cryptol (pretty)

loadJavaClass :: JSS.Codebase -> String -> IO Class
loadJavaClass :: Codebase -> String -> IO Class
loadJavaClass cb =
lookupClass cb fixPos . mkClassName . dotsToSlashes

Expand Down Expand Up @@ -112,7 +113,7 @@ symexecJava cls mname inputs outputs satBranches = do
" argument in method " ++ methodName meth
pidx = fromIntegral . localIndexOfParameter meth
withSAWBackend Nothing $ \sbe -> io $ do
runSimulator cb sbe defaultSEH (Just fl) $ do
runSimulator (legacyCodebaseHack cb) sbe defaultSEH (Just fl) $ do
setVerbosity (simVerbose opts)
assigns <- mapM mkAssign inputs
let (argAssigns, otherAssigns) = partition (isArg meth . fst) assigns
Expand Down Expand Up @@ -164,7 +165,7 @@ extractJava cls mname setup = do
let fl = defaultSimFlags { alwaysBitBlastBranchTerms =
jsSatBranches setupRes }
meth = specMethod (jsSpec setupRes)
io $ runSimulator cb sbe defaultSEH (Just fl) $ do
io $ runSimulator (legacyCodebaseHack cb) sbe defaultSEH (Just fl) $ do
setVerbosity (simVerbose opts)
argTypes <- either fail return (getActualArgTypes setupRes)
args <- mapM (freshJavaVal (Just argsRef) sc) argTypes
Expand Down Expand Up @@ -247,8 +248,8 @@ verifyJava cls mname overrides setup = do
liftIO $ bsCheckAliasTypes pos bs
liftIO $ printOutLn opts Debug $ "Executing " ++ specName ms ++
" at PC " ++ show (bsLoc bs) ++ "."
-- runDefSimulator cb sbe $ do
runSimulator cb sbe defaultSEH (Just fl) $ do
-- runDefSimulator (legacyCodebaseHack cb) sbe $ do
runSimulator (legacyCodebaseHack cb) sbe defaultSEH (Just fl) $ do
setVerbosity (simVerbose opts)
let prover script vs n g = do
let exts = getAllExts g
Expand Down Expand Up @@ -381,7 +382,7 @@ checkCompatibleType _sc msg aty schema =
]

parseJavaExpr' :: (MonadIO m) =>
JSS.Codebase -> JSS.Class -> JSS.Method -> String
Codebase -> JSS.Class -> JSS.Method -> String
-> m JavaExpr
parseJavaExpr' cb cls meth name =
liftIO (runExceptT (parseJavaExpr cb cls meth name) >>= either fail return)
Expand All @@ -401,7 +402,7 @@ getJavaExpr ctx name = do
, ftext "Maybe you're missing a `java_var` or `java_class_var`?"
]

typeJavaExpr :: JSS.Codebase -> String -> JavaType
typeJavaExpr :: Codebase -> String -> JavaType
-> JavaSetup (JavaExpr, JavaActualType)
typeJavaExpr cb name ty = do
ms <- gets jsSpec
Expand Down
Loading

0 comments on commit d4189fd

Please sign in to comment.