From 25a31a8a6d4a916bb2ec2005d2f991a00c64362a Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Wed, 2 Dec 2020 21:18:34 -0800 Subject: [PATCH] Remove some unused `BuiltinContext` and `Options` parameters. Removing those parameters also necessitated the addition of a `roBasicSS` field to the `TopLevelRO` datatype. Fixes #945. --- .../src/SAWServer/JVMCrucibleSetup.hs | 15 +- saw-remote-api/src/SAWServer/JVMVerify.hs | 5 +- .../src/SAWServer/LLVMCrucibleSetup.hs | 17 +- saw-remote-api/src/SAWServer/LLVMVerify.hs | 7 +- .../Crucible/Common/Setup/Builtins.hs | 9 +- src/SAWScript/Crucible/JVM/Builtins.hs | 79 +++---- src/SAWScript/Crucible/JVM/BuiltinsJVM.hs | 28 ++- src/SAWScript/Crucible/LLVM/Builtins.hs | 211 ++++++------------ .../Crucible/LLVM/Skeleton/Builtins.hs | 77 +++---- src/SAWScript/Crucible/LLVM/X86.hs | 19 +- src/SAWScript/Interpreter.hs | 115 +++++----- src/SAWScript/JavaBuiltins.hs | 100 +++++---- src/SAWScript/Value.hs | 4 + 13 files changed, 291 insertions(+), 395 deletions(-) diff --git a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs index c67afed0c1..8a63481d61 100644 --- a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs +++ b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs @@ -33,7 +33,6 @@ import SAWScript.Crucible.JVM.Builtins import SAWScript.Crucible.JVM.BuiltinsJVM import qualified SAWScript.Crucible.JVM.MethodSpecIR as CMS import SAWScript.JavaExpr (JavaType(..)) -import SAWScript.Options (defaultOptions) import SAWScript.Value (BuiltinContext, JVMSetupM(..), biSharedContext) import qualified Verifier.SAW.CryptolEnv as CEnv import Verifier.SAW.CryptolEnv (CryptolEnv) @@ -96,19 +95,19 @@ interpretJVMSetup :: JVMSetupM () interpretJVMSetup fileReader bic cenv0 ss = runStateT (traverse_ go ss) (mempty, cenv0) *> pure () where - go (SetupReturn v) = get >>= \env -> lift $ getSetupVal env v >>= jvm_return bic opts + go (SetupReturn v) = get >>= \env -> lift $ getSetupVal env v >>= jvm_return -- TODO: do we really want two names here? go (SetupFresh name@(ServerName n) debugName ty) = - do t <- lift $ jvm_fresh_var bic opts (T.unpack debugName) ty + do t <- lift $ jvm_fresh_var (T.unpack debugName) ty (env, cenv) <- get put (env, CEnv.bindTypedTerm (mkIdent n, t) cenv) save name (Val (MS.SetupTerm t)) go (SetupAlloc name ty _ (Just _)) = error "attempted to allocate a Java object with alignment information" go (SetupAlloc name (JavaArray n ty) True Nothing) = - lift (jvm_alloc_array bic opts n ty) >>= save name . Val + lift (jvm_alloc_array n ty) >>= save name . Val go (SetupAlloc name (JavaClass c) True Nothing) = - lift (jvm_alloc_object bic opts c) >>= save name . Val + lift (jvm_alloc_object c) >>= save name . Val go (SetupAlloc name ty False Nothing) = error $ "cannot allocate type: " ++ show ty go (SetupPointsTo src tgt) = get >>= \env -> lift $ @@ -117,13 +116,12 @@ interpretJVMSetup fileReader bic cenv0 ss = runStateT (traverse_ go ss) (mempty, error "nyi: points-to" go (SetupExecuteFunction args) = get >>= \env -> - lift $ traverse (getSetupVal env) args >>= jvm_execute_func bic opts + lift $ traverse (getSetupVal env) args >>= jvm_execute_func go (SetupPrecond p) = get >>= \env -> lift $ getTypedTerm env p >>= jvm_precond go (SetupPostcond p) = get >>= \env -> lift $ getTypedTerm env p >>= jvm_postcond - opts = defaultOptions save name val = modify' (\(env, cenv) -> (Map.insert name val env, cenv)) getSetupVal :: @@ -190,7 +188,6 @@ jvmLoadClass (JVMLoadClassParams serverName cname) = case tasks of (_:_) -> raise $ notAtTopLevel $ map fst tasks [] -> - do bic <- view sawBIC <$> getState - c <- tl $ loadJavaClass bic cname + do c <- tl $ loadJavaClass cname setServerVal serverName c ok diff --git a/saw-remote-api/src/SAWServer/JVMVerify.hs b/saw-remote-api/src/SAWServer/JVMVerify.hs index 630408030c..bf2edcc426 100644 --- a/saw-remote-api/src/SAWServer/JVMVerify.hs +++ b/saw-remote-api/src/SAWServer/JVMVerify.hs @@ -12,7 +12,6 @@ import qualified Language.JVM.Common as JVM import SAWScript.Crucible.JVM.Builtins import SAWScript.JavaExpr (JavaType(..)) -import SAWScript.Options (defaultOptions) import SAWScript.Value (rwCryptol) import Argo @@ -44,9 +43,9 @@ jvmVerifyAssume mode (VerifyParams className fun lemmaNames checkSat contract sc VerifyContract -> do lemmas <- mapM getJVMMethodSpecIR lemmaNames proofScript <- interpretProofScript script - tl $ crucible_jvm_verify bic defaultOptions cls fun lemmas checkSat setup proofScript + tl $ crucible_jvm_verify cls fun lemmas checkSat setup proofScript AssumeContract -> - tl $ crucible_jvm_unsafe_assume_spec bic defaultOptions cls fun setup + tl $ crucible_jvm_unsafe_assume_spec cls fun setup dropTask setServerVal lemmaName res ok diff --git a/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs index fc8af24ba1..7a0988bd15 100644 --- a/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs +++ b/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs @@ -45,7 +45,6 @@ import SAWScript.Crucible.LLVM.Builtins , crucible_precond , crucible_postcond ) import qualified SAWScript.Crucible.LLVM.MethodSpecIR as CMS -import SAWScript.Options (defaultOptions) import SAWScript.Value (BuiltinContext, LLVMCrucibleSetupM(..), biSharedContext) import qualified Verifier.SAW.CryptolEnv as CEnv import Verifier.SAW.CryptolEnv (CryptolEnv) @@ -109,28 +108,28 @@ interpretLLVMSetup :: interpretLLVMSetup fileReader bic cenv0 ss = runStateT (traverse_ go ss) (mempty, cenv0) *> pure () where - go (SetupReturn v) = get >>= \env -> lift $ getSetupVal env v >>= crucible_return bic defaultOptions + go (SetupReturn v) = get >>= \env -> lift $ getSetupVal env v >>= crucible_return -- TODO: do we really want two names here? go (SetupFresh name@(ServerName n) debugName ty) = - do t <- lift $ crucible_fresh_var bic defaultOptions (T.unpack debugName) ty + do t <- lift $ crucible_fresh_var (T.unpack debugName) ty (env, cenv) <- get put (env, CEnv.bindTypedTerm (mkIdent n, t) cenv) save name (Val (CMS.anySetupTerm t)) go (SetupAlloc name ty True Nothing) = - lift (crucible_alloc bic defaultOptions ty) >>= save name . Val + lift (crucible_alloc ty) >>= save name . Val go (SetupAlloc name ty False Nothing) = - lift (crucible_alloc_readonly bic defaultOptions ty) >>= save name . Val + lift (crucible_alloc_readonly ty) >>= save name . Val go (SetupAlloc name ty True (Just align)) = - lift (crucible_alloc_aligned bic defaultOptions align ty) >>= save name . Val + lift (crucible_alloc_aligned align ty) >>= save name . Val go (SetupAlloc name ty False (Just align)) = - lift (crucible_alloc_readonly_aligned bic defaultOptions align ty) >>= save name . Val + lift (crucible_alloc_readonly_aligned align ty) >>= save name . Val go (SetupPointsTo src tgt) = get >>= \env -> lift $ do ptr <- getSetupVal env src tgt' <- getSetupVal env tgt - crucible_points_to True bic defaultOptions ptr tgt' + crucible_points_to True ptr tgt' go (SetupExecuteFunction args) = get >>= \env -> - lift $ traverse (getSetupVal env) args >>= crucible_execute_func bic defaultOptions + lift $ traverse (getSetupVal env) args >>= crucible_execute_func go (SetupPrecond p) = get >>= \env -> lift $ getTypedTerm env p >>= crucible_precond go (SetupPostcond p) = get >>= \env -> lift $ diff --git a/saw-remote-api/src/SAWServer/LLVMVerify.hs b/saw-remote-api/src/SAWServer/LLVMVerify.hs index 6de1ad2d58..a70c26f8e5 100644 --- a/saw-remote-api/src/SAWServer/LLVMVerify.hs +++ b/saw-remote-api/src/SAWServer/LLVMVerify.hs @@ -11,7 +11,6 @@ import Control.Lens import SAWScript.Crucible.LLVM.Builtins import SAWScript.Crucible.LLVM.X86 -import SAWScript.Options (defaultOptions) import SAWScript.Value (rwCryptol) import Argo @@ -43,9 +42,9 @@ llvmVerifyAssume mode (VerifyParams modName fun lemmaNames checkSat contract scr VerifyContract -> do lemmas <- mapM getLLVMMethodSpecIR lemmaNames proofScript <- interpretProofScript script - tl $ crucible_llvm_verify bic defaultOptions mod fun lemmas checkSat setup proofScript + tl $ crucible_llvm_verify mod fun lemmas checkSat setup proofScript AssumeContract -> - tl $ crucible_llvm_unsafe_assume_spec bic defaultOptions mod fun setup + tl $ crucible_llvm_unsafe_assume_spec mod fun setup dropTask setServerVal lemmaName res ok @@ -72,7 +71,7 @@ llvmVerifyX86 (X86VerifyParams modName objName fun globals _lemmaNames checkSat proofScript <- interpretProofScript script fileReader <- getFileReader setup <- compileLLVMContract fileReader bic cenv <$> traverse getExpr contract - res <- tl $ crucible_llvm_verify_x86 bic defaultOptions mod objName fun allocs checkSat setup proofScript + res <- tl $ crucible_llvm_verify_x86 mod objName fun allocs checkSat setup proofScript dropTask setServerVal lemmaName res ok diff --git a/src/SAWScript/Crucible/Common/Setup/Builtins.hs b/src/SAWScript/Crucible/Common/Setup/Builtins.hs index 584fd5b3a9..4b408e5ee5 100644 --- a/src/SAWScript/Crucible/Common/Setup/Builtins.hs +++ b/src/SAWScript/Crucible/Common/Setup/Builtins.hs @@ -19,7 +19,6 @@ import qualified What4.ProgramLoc as W4 import Verifier.SAW.TypedTerm (TypedTerm) -import SAWScript.Options (Options) import SAWScript.Value import qualified SAWScript.Crucible.Common.MethodSpec as MS @@ -51,22 +50,18 @@ crucible_postcond loc p = do addCondition (MS.SetupCond_Pred loc p) crucible_return :: - BuiltinContext -> - Options -> MS.SetupValue ext -> CrucibleSetup ext () -crucible_return _bic _opt retval = do +crucible_return retval = do ret <- use (csMethodSpec . MS.csRetValue) case ret of Just _ -> fail "crucible_return: duplicate return value specification" Nothing -> csMethodSpec . MS.csRetValue .= Just retval crucible_execute_func :: - BuiltinContext -> - Options -> [MS.SetupValue ext] -> CrucibleSetup ext () -crucible_execute_func _bic _opt args = do +crucible_execute_func args = do tps <- use (csMethodSpec . MS.csArgs) csPrePost .= MS.PostState csMethodSpec . MS.csArgBindings .= Map.fromList [ (i, (t,a)) diff --git a/src/SAWScript/Crucible/JVM/Builtins.hs b/src/SAWScript/Crucible/JVM/Builtins.hs index b132c8d7b0..dd33c8d7ee 100644 --- a/src/SAWScript/Crucible/JVM/Builtins.hs +++ b/src/SAWScript/Crucible/JVM/Builtins.hs @@ -179,8 +179,6 @@ excludedRefs = Set.fromList ] crucible_jvm_verify :: - BuiltinContext -> - Options -> J.Class -> String {- ^ method name -} -> [CrucibleMethodSpecIR] {- ^ overrides -} -> @@ -188,15 +186,16 @@ crucible_jvm_verify :: JVMSetupM () -> ProofScript SatResult -> TopLevel CrucibleMethodSpecIR -crucible_jvm_verify bic opts cls nm lemmas checkSat setup tactic = +crucible_jvm_verify cls nm lemmas checkSat setup tactic = do cb <- getJavaCodebase + opts <- getOptions -- allocate all of the handles/static vars that are referenced -- (directly or indirectly) by this class allRefs <- io $ Set.toList <$> allClassRefs cb (J.className cls) let refs = CJ.initClasses ++ allRefs -- ++ superRefs - mapM_ (prepareClassTopLevel bic . J.unClassName) refs + mapM_ (prepareClassTopLevel . J.unClassName) refs - cc <- setupCrucibleContext bic opts cls + cc <- setupCrucibleContext cls let sym = cc^.jccBackend let jc = cc^.jccJVMContext @@ -228,7 +227,7 @@ crucible_jvm_verify bic opts cls nm lemmas checkSat setup tactic = io $ verifySimulate opts cc pfs methodSpec args assumes top_loc lemmas globals2 checkSat -- collect the proof obligations - asserts <- verifyPoststate opts (biSharedContext bic) cc + asserts <- verifyPoststate cc methodSpec env globals3 ret -- restore previous assumption state @@ -241,14 +240,12 @@ crucible_jvm_verify bic opts cls nm lemmas checkSat setup tactic = crucible_jvm_unsafe_assume_spec :: - BuiltinContext -> - Options -> J.Class -> String {- ^ Name of the method -} -> JVMSetupM () {- ^ Boundary specification -} -> TopLevel CrucibleMethodSpecIR -crucible_jvm_unsafe_assume_spec bic opts cls nm setup = - do cc <- setupCrucibleContext bic opts cls +crucible_jvm_unsafe_assume_spec cls nm setup = + do cc <- setupCrucibleContext cls cb <- getJavaCodebase -- cls' is either cls or a subclass of cls pos <- getPosition @@ -660,16 +657,16 @@ scAndList sc = conj . filter nontrivial -------------------------------------------------------------------------------- verifyPoststate :: - Options {- ^ saw script debug and print options -} -> - SharedContext {- ^ saw core context -} -> JVMCrucibleContext {- ^ crucible context -} -> CrucibleMethodSpecIR {- ^ specification -} -> Map AllocIndex JVMRefVal {- ^ allocation substitution -} -> Crucible.SymGlobalState Sym {- ^ global variables -} -> Maybe (J.Type, JVMVal) {- ^ optional return value -} -> TopLevel [(String, Term)] {- ^ generated labels and verification conditions -} -verifyPoststate opts sc cc mspec env0 globals ret = - do poststateLoc <- SS.toW4Loc "_SAW_verify_poststate" <$> getPosition +verifyPoststate cc mspec env0 globals ret = + do opts <- getOptions + sc <- getSharedContext + poststateLoc <- SS.toW4Loc "_SAW_verify_poststate" <$> getPosition io $ W4.setCurrentProgramLoc sym poststateLoc let ecs0 = Map.fromList @@ -682,7 +679,7 @@ verifyPoststate opts sc cc mspec env0 globals ret = (view (MS.csPostState . MS.csFreshVars) mspec)) matchPost <- io $ runOverrideMatcher sym globals env0 terms0 initialFree poststateLoc $ - do matchResult + do matchResult opts sc learnCond opts sc cc mspec PostState (mspec ^. MS.csPostState) st <- case matchPost of @@ -692,18 +689,18 @@ verifyPoststate opts sc cc mspec env0 globals ret = obligations <- io $ Crucible.getProofObligations sym io $ Crucible.clearProofObligations sym - io $ mapM verifyObligation (Crucible.proofGoalsToList obligations) + io $ mapM (verifyObligation sc) (Crucible.proofGoalsToList obligations) where sym = cc^.jccBackend - verifyObligation (Crucible.ProofGoal hyps (Crucible.LabeledPred concl (Crucible.SimError _loc err))) = do + verifyObligation sc (Crucible.ProofGoal hyps (Crucible.LabeledPred concl (Crucible.SimError _loc err))) = do hypTerm <- scAndList sc =<< mapM (Crucible.toSC sym) (toListOf (folded . Crucible.labeledPred) hyps) conclTerm <- Crucible.toSC sym concl obligation <- scImplies sc hypTerm conclTerm return ("safety assertion: " ++ Crucible.simErrorReasonMsg err, obligation) - matchResult = + matchResult opts sc = case (ret, mspec ^. MS.csRetValue) of (Just (rty,r), Just expect) -> matchArg opts sc cc mspec PostState r rty expect (Nothing , Just _ ) -> fail "verifyPoststate: unexpected jvm_return specification" @@ -711,14 +708,15 @@ verifyPoststate opts sc cc mspec env0 globals ret = -------------------------------------------------------------------------------- -setupCrucibleContext :: BuiltinContext -> Options -> J.Class -> TopLevel JVMCrucibleContext -setupCrucibleContext bic opts jclass = +setupCrucibleContext :: J.Class -> TopLevel JVMCrucibleContext +setupCrucibleContext jclass = do halloc <- getHandleAlloc jc <- getJVMTrans cb <- getJavaCodebase - let sc = biSharedContext bic + sc <- getSharedContext let gen = globalNonceGenerator sym <- io $ Crucible.newSAWCoreBackend W4.FloatRealRepr sc gen + opts <- getOptions io $ CJ.setSimulatorVerbosity (simVerbose opts) sym -- TODO! there's a lot of options setup we need to replicate @@ -828,24 +826,20 @@ typeOfJavaType jty = -- | Generate a fresh variable term. The name will be used when -- pretty-printing the variable in debug output. jvm_fresh_var :: - BuiltinContext {- ^ context -} -> - Options {- ^ options -} -> String {- ^ variable name -} -> JavaType {- ^ variable type -} -> JVMSetupM TypedTerm {- ^ fresh typed term -} -jvm_fresh_var bic _opts name jty = +jvm_fresh_var name jty = JVMSetupM $ - do let sc = biSharedContext bic + do sc <- lift getSharedContext case cryptolTypeOfActual jty of Nothing -> fail $ "Unsupported type in jvm_fresh_var: " ++ show jty Just cty -> Setup.freshVariable sc name cty jvm_alloc_object :: - BuiltinContext -> - Options -> String {- ^ class name -} -> JVMSetupM SetupValue -jvm_alloc_object _bic _opt cname = +jvm_alloc_object cname = JVMSetupM $ do loc <- SS.toW4Loc "jvm_alloc_object" <$> lift getPosition n <- Setup.csVarCounter <<%= nextAllocIndex @@ -854,12 +848,10 @@ jvm_alloc_object _bic _opt cname = return (MS.SetupVar n) jvm_alloc_array :: - BuiltinContext -> - Options -> Int {- array size -} -> JavaType -> JVMSetupM SetupValue -jvm_alloc_array _bic _opt len ety = +jvm_alloc_array len ety = JVMSetupM $ do loc <- SS.toW4Loc "jvm_alloc_array" <$> lift getPosition n <- Setup.csVarCounter <<%= nextAllocIndex @@ -867,14 +859,11 @@ jvm_alloc_array _bic _opt len ety = return (MS.SetupVar n) jvm_field_is :: - Bool {- ^ whether to check type compatibility -} -> - BuiltinContext -> - Options -> SetupValue {- ^ object -} -> String {- ^ field name -} -> SetupValue {- ^ field value -} -> JVMSetupM () -jvm_field_is _typed _bic _opt ptr fname val = +jvm_field_is ptr fname val = JVMSetupM $ do pos <- lift getPosition loc <- SS.toW4Loc "jvm_field_is" <$> lift getPosition @@ -900,14 +889,11 @@ jvm_field_is _typed _bic _opt ptr fname val = Setup.addPointsTo (JVMPointsToField loc ptr fid val) jvm_elem_is :: - Bool {- ^ whether to check type compatibility -} -> - BuiltinContext -> - Options -> SetupValue {- ^ array -} -> Int {- ^ index -} -> SetupValue {- ^ element value -} -> JVMSetupM () -jvm_elem_is _typed _bic _opt ptr idx val = +jvm_elem_is ptr idx val = JVMSetupM $ do loc <- SS.toW4Loc "jvm_elem_is" <$> lift getPosition st <- get @@ -934,13 +920,10 @@ jvm_elem_is _typed _bic _opt ptr idx val = Setup.addPointsTo (JVMPointsToElem loc ptr idx val) jvm_array_is :: - Bool {- ^ whether to check type compatibility -} -> - BuiltinContext -> - Options -> SetupValue {- ^ array reference -} -> TypedTerm {- ^ array value -} -> JVMSetupM () -jvm_array_is _typed _bic _opt ptr val = +jvm_array_is ptr val = JVMSetupM $ do loc <- SS.toW4Loc "jvm_array_is" <$> lift getPosition st <- get @@ -960,12 +943,12 @@ jvm_postcond term = JVMSetupM $ do loc <- SS.toW4Loc "jvm_postcond" <$> lift getPosition Setup.crucible_postcond loc term -jvm_execute_func :: BuiltinContext -> Options -> [SetupValue] -> JVMSetupM () -jvm_execute_func bic opts args = JVMSetupM $ - Setup.crucible_execute_func bic opts args +jvm_execute_func :: [SetupValue] -> JVMSetupM () +jvm_execute_func args = JVMSetupM $ + Setup.crucible_execute_func args -jvm_return :: BuiltinContext -> Options -> SetupValue -> JVMSetupM () -jvm_return bic opts retVal = JVMSetupM $ Setup.crucible_return bic opts retVal +jvm_return :: SetupValue -> JVMSetupM () +jvm_return retVal = JVMSetupM $ Setup.crucible_return retVal -------------------------------------------------------------------------------- diff --git a/src/SAWScript/Crucible/JVM/BuiltinsJVM.hs b/src/SAWScript/Crucible/JVM/BuiltinsJVM.hs index 066ee59c1f..c0038d261c 100644 --- a/src/SAWScript/Crucible/JVM/BuiltinsJVM.hs +++ b/src/SAWScript/Crucible/JVM/BuiltinsJVM.hs @@ -98,20 +98,23 @@ instance IsCodebase JCB.Codebase where -- | Make sure the class is in the database and allocate handles for its -- methods and static fields -- -loadJavaClass :: BuiltinContext -> String -> TopLevel J.Class -loadJavaClass bic str = do - c <- io $ findClass (biJavaCodebase bic) str - prepareClassTopLevel bic str +loadJavaClass :: String -> TopLevel J.Class +loadJavaClass str = do + cb <- getJavaCodebase + c <- io $ findClass cb str + prepareClassTopLevel str return c ----------------------------------------------------------------------- -- | Allocate the method handles/global static variables for the given -- class and add them to the current translation context -prepareClassTopLevel :: BuiltinContext -> String -> TopLevel () -prepareClassTopLevel bic str = do +prepareClassTopLevel :: String -> TopLevel () +prepareClassTopLevel str = do + + cb <- getJavaCodebase -- get class from codebase - c <- io $ findClass (biJavaCodebase bic) str + c <- io $ findClass cb str -- get current ctx ctx0 <- getJVMTrans @@ -132,10 +135,11 @@ prepareClassTopLevel bic str = do -- | Extract a JVM method to saw-core -- -crucible_java_extract :: BuiltinContext -> Options -> J.Class -> String -> TopLevel TypedTerm -crucible_java_extract bic opts c mname = do - let sc = biSharedContext bic - let cb = biJavaCodebase bic +crucible_java_extract :: J.Class -> String -> TopLevel TypedTerm +crucible_java_extract c mname = do + sc <- getSharedContext + cb <- getJavaCodebase + opts <- getOptions let verbosity = simVerbose opts let gen = Nonce.globalNonceGenerator @@ -150,7 +154,7 @@ crucible_java_extract bic opts c mname = do -- allocate all of the handles/static vars that are directly referenced by -- this class let refs = CJ.initClasses ++ Set.toList (CJ.classRefs c) - mapM_ (prepareClassTopLevel bic . J.unClassName) refs + mapM_ (prepareClassTopLevel . J.unClassName) refs halloc <- getHandleAlloc ctx <- getJVMTrans diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index d919327a95..78c5c8ae47 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -259,8 +259,6 @@ resolveSpecName nm = else return (nm, Nothing) crucible_llvm_verify :: - BuiltinContext -> - Options -> Some LLVMModule -> String -> [SomeLLVM MS.CrucibleMethodSpecIR] -> @@ -268,39 +266,35 @@ crucible_llvm_verify :: LLVMCrucibleSetupM () -> ProofScript SatResult -> TopLevel (SomeLLVM MS.CrucibleMethodSpecIR) -crucible_llvm_verify bic opts (Some lm) nm lemmas checkSat setup tactic = +crucible_llvm_verify (Some lm) nm lemmas checkSat setup tactic = do lemmas' <- checkModuleCompatibility lm lemmas - withMethodSpec bic opts checkSat lm nm setup $ \cc method_spec -> - do (res_method_spec, _) <- verifyMethodSpec bic opts cc method_spec lemmas' checkSat tactic Nothing + withMethodSpec checkSat lm nm setup $ \cc method_spec -> + do (res_method_spec, _) <- verifyMethodSpec cc method_spec lemmas' checkSat tactic Nothing returnProof $ SomeLLVM res_method_spec crucible_llvm_unsafe_assume_spec :: - BuiltinContext -> - Options -> Some LLVMModule -> String {- ^ Name of the function -} -> LLVMCrucibleSetupM () {- ^ Boundary specification -} -> TopLevel (SomeLLVM MS.CrucibleMethodSpecIR) -crucible_llvm_unsafe_assume_spec bic opts (Some lm) nm setup = - withMethodSpec bic opts False lm nm setup $ \_ method_spec -> +crucible_llvm_unsafe_assume_spec (Some lm) nm setup = + withMethodSpec False lm nm setup $ \_ method_spec -> do printOutLnTop Info $ unwords ["Assume override", (method_spec ^. csName)] returnProof $ SomeLLVM method_spec crucible_llvm_array_size_profile :: ProofScript SatResult -> - BuiltinContext -> - Options -> Some LLVMModule -> String -> [SomeLLVM MS.CrucibleMethodSpecIR] -> LLVMCrucibleSetupM () -> TopLevel [(String, [Crucible.FunctionProfile])] -crucible_llvm_array_size_profile assume bic opts (Some lm) nm lemmas setup = do +crucible_llvm_array_size_profile assume (Some lm) nm lemmas setup = do cell <- io $ newIORef (Map.empty :: Map Text.Text [Crucible.FunctionProfile]) lemmas' <- checkModuleCompatibility lm lemmas - withMethodSpec bic opts False lm nm setup $ \cc ms -> do - void . verifyMethodSpec bic opts cc ms lemmas' True assume $ Just cell + withMethodSpec False lm nm setup $ \cc ms -> do + void . verifyMethodSpec cc ms lemmas' True assume $ Just cell profiles <- io $ readIORef cell pure . fmap (\(fnm, prof) -> (Text.unpack fnm, prof)) $ Map.toList profiles @@ -321,8 +315,6 @@ llvmNameInfo :: String -> NameInfo llvmNameInfo symbol_name = ImportedName (llvmURI symbol_name) [ Text.pack symbol_name ] crucible_llvm_compositional_extract :: - BuiltinContext -> - Options -> Some LLVMModule -> String -> String -> @@ -331,9 +323,9 @@ crucible_llvm_compositional_extract :: LLVMCrucibleSetupM () -> ProofScript SatResult -> TopLevel (SomeLLVM MS.CrucibleMethodSpecIR) -crucible_llvm_compositional_extract bic opts (Some lm) nm func_name lemmas checkSat setup tactic = +crucible_llvm_compositional_extract (Some lm) nm func_name lemmas checkSat setup tactic = do lemmas' <- checkModuleCompatibility lm lemmas - withMethodSpec bic opts checkSat lm nm setup $ \cc method_spec -> + withMethodSpec checkSat lm nm setup $ \cc method_spec -> do let value_input_parameters = mapMaybe (\(_, setup_value) -> setupValueAsExtCns setup_value) (Map.elems $ method_spec ^. MS.csArgBindings) @@ -376,9 +368,9 @@ crucible_llvm_compositional_extract bic opts (Some lm) nm func_name lemmas check , "An output parameter must be bound by crucible_return or crucible_points_to." ] - (res_method_spec, post_override_state) <- verifyMethodSpec bic opts cc method_spec lemmas' checkSat tactic Nothing + (res_method_spec, post_override_state) <- verifyMethodSpec cc method_spec lemmas' checkSat tactic Nothing - let shared_context = biSharedContext bic + shared_context <- getSharedContext let output_values = map (((Map.!) $ post_override_state ^. termSub) . ecVarIndex) output_parameters @@ -464,8 +456,6 @@ checkModuleCompatibility llvmModule = foldM step [] -- -- | The real work of 'crucible_llvm_verify' and 'crucible_llvm_unsafe_assume_spec'. withMethodSpec :: - BuiltinContext -> - Options -> Bool {- ^ path sat -} -> LLVMModule arch -> String {- ^ Name of the function -} -> @@ -473,11 +463,12 @@ withMethodSpec :: ((?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => LLVMCrucibleContext arch -> MS.CrucibleMethodSpecIR (LLVM arch) -> TopLevel a) -> TopLevel a -withMethodSpec bic opts pathSat lm nm setup action = +withMethodSpec pathSat lm nm setup action = do (nm', parent) <- resolveSpecName nm let edef = findDefMaybeStatic (modAST lm) nm' let edecl = findDecl (modAST lm) nm' let mtrans = modTrans lm + opts <- getOptions defOrDecls <- case (edef, edecl) of (Right defs, _) -> return (NE.map Left defs) @@ -488,7 +479,7 @@ withMethodSpec bic opts pathSat lm nm setup action = Crucible.llvmPtrWidth (mtrans ^. Crucible.transContext) $ \_ -> fmap NE.head $ forM defOrDecls $ \defOrDecl -> - setupLLVMCrucibleContext bic opts pathSat lm $ \cc -> + setupLLVMCrucibleContext pathSat lm $ \cc -> do let sym = cc^.ccBackend pos <- getPosition @@ -514,8 +505,6 @@ withMethodSpec bic opts pathSat lm nm setup action = verifyMethodSpec :: (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => - BuiltinContext -> - Options -> LLVMCrucibleContext arch -> MS.CrucibleMethodSpecIR (LLVM arch) -> [MS.CrucibleMethodSpecIR (LLVM arch)] -> @@ -523,7 +512,7 @@ verifyMethodSpec :: ProofScript SatResult -> Maybe (IORef (Map Text.Text [Crucible.FunctionProfile])) -> TopLevel (MS.CrucibleMethodSpecIR (LLVM arch), OverrideState (LLVM arch)) -verifyMethodSpec bic opts cc methodSpec lemmas checkSat tactic asp = +verifyMethodSpec cc methodSpec lemmas checkSat tactic asp = do printOutLnTop Info $ unwords ["Verifying", (methodSpec ^. csName) , "..."] @@ -551,6 +540,7 @@ verifyMethodSpec bic opts cc methodSpec lemmas checkSat tactic asp = let globals1 = Crucible.llvmGlobals (ccLLVMContext cc) mem -- construct the initial state for verifications + opts <- getOptions (args, assumes, env, globals2) <- io $ verifyPrestate opts cc methodSpec globals1 @@ -566,7 +556,7 @@ verifyMethodSpec bic opts cc methodSpec lemmas checkSat tactic asp = -- collect the proof obligations (asserts, post_override_state) <- - verifyPoststate opts (biSharedContext bic) cc + verifyPoststate cc methodSpec env globals3 ret -- restore previous assumption state @@ -1161,16 +1151,16 @@ scAndList sc = conj . filter nontrivial verifyPoststate :: (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth wptr, wptr ~ Crucible.ArchWidth arch, Crucible.HasLLVMAnn Sym) => - Options {- ^ saw script debug and print options -} -> - SharedContext {- ^ saw core context -} -> LLVMCrucibleContext arch {- ^ crucible context -} -> MS.CrucibleMethodSpecIR (LLVM arch) {- ^ specification -} -> Map AllocIndex (LLVMPtr wptr) {- ^ allocation substitution -} -> Crucible.SymGlobalState Sym {- ^ global variables -} -> Maybe (Crucible.MemType, LLVMVal) {- ^ optional return value -} -> TopLevel ([(String, Term)], OverrideState (LLVM arch)) {- ^ generated labels and verification conditions -} -verifyPoststate opts sc cc mspec env0 globals ret = +verifyPoststate cc mspec env0 globals ret = do poststateLoc <- toW4Loc "_SAW_verify_poststate" <$> getPosition + sc <- getSharedContext + opts <- getOptions io $ W4.setCurrentProgramLoc sym poststateLoc let ecs0 = Map.fromList @@ -1185,7 +1175,7 @@ verifyPoststate opts sc cc mspec env0 globals ret = matchPost <- io $ runOverrideMatcher sym globals env0 terms0 initialFree poststateLoc $ - do matchResult + do matchResult opts sc learnCond opts sc cc mspec PostState (mspec ^. MS.csGlobalAllocs) (mspec ^. MS.csPreState . MS.csAllocs) @@ -1200,19 +1190,19 @@ verifyPoststate opts sc cc mspec env0 globals ret = obligations <- io $ Crucible.getProofObligations sym io $ Crucible.clearProofObligations sym - sc_obligations <- io $ mapM verifyObligation (Crucible.proofGoalsToList obligations) + sc_obligations <- io $ mapM (verifyObligation sc) (Crucible.proofGoalsToList obligations) return (sc_obligations, st) where sym = cc^.ccBackend - verifyObligation (Crucible.ProofGoal hyps (Crucible.LabeledPred concl err)) = + verifyObligation sc (Crucible.ProofGoal hyps (Crucible.LabeledPred concl err)) = do hypTerm <- CrucibleSAW.toSC sym =<< W4.andAllOf sym (folded . Crucible.labeledPred) hyps conclTerm <- CrucibleSAW.toSC sym concl obligation <- scImplies sc hypTerm conclTerm return (unlines ["safety assertion:", show err], obligation) - matchResult = + matchResult opts sc = case (ret, mspec ^. MS.csRetValue) of (Just (rty,r), Just expect) -> matchArg opts sc cc mspec PostState r rty expect (Nothing , Just _ ) -> @@ -1222,15 +1212,16 @@ verifyPoststate opts sc cc mspec env0 globals ret = -------------------------------------------------------------------------------- setupLLVMCrucibleContext :: - BuiltinContext -> - Options -> Bool {- ^ enable path sat checking -} -> LLVMModule arch -> ((?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => LLVMCrucibleContext arch -> TopLevel a) -> TopLevel a -setupLLVMCrucibleContext bic opts pathSat lm action = +setupLLVMCrucibleContext pathSat lm action = do halloc <- getHandleAlloc + sc <- getSharedContext + opts <- getOptions + basic_ss <- getBasicSS let llvm_mod = modAST lm let mtrans = modTrans lm let ctx = mtrans^.Crucible.transContext @@ -1244,7 +1235,6 @@ setupLLVMCrucibleContext bic opts pathSat lm action = cc <- io $ do let gen = globalNonceGenerator - let sc = biSharedContext bic let verbosity = simVerbose opts sym <- CrucibleSAW.newSAWCoreBackend W4.FloatRealRepr sc gen @@ -1304,7 +1294,7 @@ setupLLVMCrucibleContext bic opts pathSat lm action = , _ccBackend = sym , _ccLLVMSimContext = lsimctx , _ccLLVMGlobals = lglobals - , _ccBasicSS = biBasicSS bic + , _ccBasicSS = basic_ss } action cc @@ -1451,15 +1441,15 @@ extractFromLLVMCFG opts sc cc (Crucible.AnyCFG cfg) = -------------------------------------------------------------------------------- crucible_llvm_extract :: - BuiltinContext -> - Options -> Some LLVMModule -> String -> TopLevel TypedTerm -crucible_llvm_extract bic opts (Some lm) fn_name = +crucible_llvm_extract (Some lm) fn_name = do let ctx = modTrans lm ^. Crucible.transContext let ?lc = ctx^.Crucible.llvmTypeCtx let edef = findDefMaybeStatic (modAST lm) fn_name + sc <- getSharedContext + opts <- getOptions case edef of Right defs -> do let defTypes = @@ -1471,21 +1461,19 @@ crucible_llvm_extract bic opts (Some lm) fn_name = when (any L.isAlias defTypes) $ throwTopLevel "Type aliases are not supported by `crucible_llvm_extract`." Left err -> throwTopLevel (displayVerifExceptionOpts opts err) - setupLLVMCrucibleContext bic opts False lm $ \cc -> + setupLLVMCrucibleContext False lm $ \cc -> case Map.lookup (fromString fn_name) (Crucible.cfgMap (ccLLVMModuleTrans cc)) of Nothing -> throwTopLevel $ unwords ["function", fn_name, "not found"] - Just (_,cfg) -> io $ extractFromLLVMCFG opts (biSharedContext bic) cc cfg + Just (_,cfg) -> io $ extractFromLLVMCFG opts sc cc cfg crucible_llvm_cfg :: - BuiltinContext -> - Options -> Some LLVMModule -> String -> TopLevel SAW_CFG -crucible_llvm_cfg bic opts (Some lm) fn_name = +crucible_llvm_cfg (Some lm) fn_name = do let ctx = modTrans lm ^. Crucible.transContext let ?lc = ctx^.Crucible.llvmTypeCtx - setupLLVMCrucibleContext bic opts False lm $ \cc -> + setupLLVMCrucibleContext False lm $ \cc -> case Map.lookup (fromString fn_name) (Crucible.cfgMap (ccLLVMModuleTrans cc)) of Nothing -> throwTopLevel $ unwords ["function", fn_name, "not found"] Just (_,cfg) -> return (LLVM_CFG cfg) @@ -1534,21 +1522,17 @@ crucible_postcond term = Setup.crucible_postcond loc term crucible_return :: - BuiltinContext -> - Options -> AllLLVM MS.SetupValue -> LLVMCrucibleSetupM () -crucible_return bic opts val = +crucible_return val = LLVMCrucibleSetupM $ - do Setup.crucible_return bic opts (getAllLLVM val) + do Setup.crucible_return (getAllLLVM val) crucible_execute_func :: - BuiltinContext -> - Options -> [AllLLVM MS.SetupValue] -> LLVMCrucibleSetupM () -crucible_execute_func bic opts args = - LLVMCrucibleSetupM $ Setup.crucible_execute_func bic opts (map getAllLLVM args) +crucible_execute_func args = + LLVMCrucibleSetupM $ Setup.crucible_execute_func (map getAllLLVM args) getLLVMCrucibleContext :: CrucibleSetup (LLVM arch) (LLVMCrucibleContext arch) getLLVMCrucibleContext = view Setup.csCrucibleContext <$> get @@ -1581,35 +1565,31 @@ cryptolTypeOfActual dl mt = -- | Generate a fresh variable term. The name will be used when -- pretty-printing the variable in debug output. crucible_fresh_var :: - BuiltinContext {- ^ context -} -> - Options {- ^ options -} -> String {- ^ variable name -} -> L.Type {- ^ variable type -} -> LLVMCrucibleSetupM TypedTerm {- ^ fresh typed term -} -crucible_fresh_var bic _opts name lty = +crucible_fresh_var name lty = LLVMCrucibleSetupM $ do cctx <- getLLVMCrucibleContext let ?lc = ccTypeCtx cctx loc <- getW4Position "crucible_fresh_var" - lty' <- memTypeForLLVMType loc bic lty - let sc = biSharedContext bic + lty' <- memTypeForLLVMType loc lty + sc <- lift getSharedContext let dl = Crucible.llvmDataLayout (ccTypeCtx cctx) case cryptolTypeOfActual dl lty' of Nothing -> throwCrucibleSetup loc $ "Unsupported type in crucible_fresh_var: " ++ show (L.ppType lty) Just cty -> Setup.freshVariable sc name cty crucible_fresh_cryptol_var :: - BuiltinContext -> - Options -> String -> Cryptol.Schema -> LLVMCrucibleSetupM TypedTerm -crucible_fresh_cryptol_var bic _opts name s = +crucible_fresh_cryptol_var name s = LLVMCrucibleSetupM $ do loc <- getW4Position "crucible_fresh_var" case s of Cryptol.Forall [] [] ty -> - do let sc = biSharedContext bic + do sc <- lift getSharedContext Setup.freshVariable sc name ty _ -> throwCrucibleSetup loc $ "Unsupported polymorphic Cryptol type schema: " ++ show s @@ -1620,18 +1600,16 @@ crucible_fresh_cryptol_var bic _opts name s = -- suitable for import as SAW core terms will be matched -- against fresh variables. crucible_fresh_expanded_val :: - BuiltinContext {- ^ context -} -> - Options {- ^ options -} -> L.Type {- ^ variable type -} -> LLVMCrucibleSetupM (AllLLVM SetupValue) {- ^ elaborated setup value -} -crucible_fresh_expanded_val bic _opts lty = +crucible_fresh_expanded_val lty = LLVMCrucibleSetupM $ - do let sc = biSharedContext bic + do sc <- lift getSharedContext cctx <- getLLVMCrucibleContext let ?lc = ccTypeCtx cctx loc <- getW4Position "crucible_fresh_expanded_val" - lty' <- memTypeForLLVMType loc bic lty + lty' <- memTypeForLLVMType loc lty constructExpandedSetupValue cctx sc loc lty' -- | See 'crucible_fresh_expanded_val' @@ -1684,10 +1662,9 @@ constructExpandedSetupValue cc sc loc t = memTypeForLLVMType :: (?lc :: Crucible.TypeContext) => W4.ProgramLoc -> - BuiltinContext -> L.Type -> CrucibleSetup arch Crucible.MemType -memTypeForLLVMType loc _bic lty = +memTypeForLLVMType loc lty = case Crucible.liftMemType lty of Right m -> return m Left err -> throwCrucibleSetup loc $ unlines @@ -1723,12 +1700,10 @@ symTypeAlias _ = Nothing -- | Does the hard work for 'crucible_alloc', 'crucible_alloc_with_size', -- 'crucible_alloc_readonly', etc. crucible_alloc_internal :: - BuiltinContext -> - Options -> L.Type -> LLVMAllocSpec -> CrucibleSetup (Crucible.LLVM arch) (AllLLVM SetupValue) -crucible_alloc_internal _bic _opt lty spec = +crucible_alloc_internal lty spec = do cctx <- getLLVMCrucibleContext let ?lc = ccTypeCtx cctx let ?dl = Crucible.llvmDataLayout ?lc @@ -1744,15 +1719,14 @@ crucible_alloc_with_mutability_and_size :: Crucible.Mutability -> Maybe (Crucible.Bytes) -> Maybe Crucible.Alignment -> - BuiltinContext -> - Options -> L.Type -> LLVMCrucibleSetupM (AllLLVM SetupValue) -crucible_alloc_with_mutability_and_size mut sz alignment bic opts lty = +crucible_alloc_with_mutability_and_size mut sz alignment lty = LLVMCrucibleSetupM $ do cctx <- getLLVMCrucibleContext loc <- getW4Position "crucible_alloc" - memTy <- memTypeForLLVMType loc bic lty + memTy <- memTypeForLLVMType loc lty + opts <- lift getOptions let lc = ccTypeCtx cctx let dl = Crucible.llvmDataLayout lc @@ -1784,7 +1758,7 @@ crucible_alloc_with_mutability_and_size mut sz alignment bic opts lty = pure a Nothing -> pure memTyAlign - crucible_alloc_internal bic opts lty $ + crucible_alloc_internal lty $ LLVMAllocSpec { _allocSpecMut = mut , _allocSpecType = memTy @@ -1795,16 +1769,12 @@ crucible_alloc_with_mutability_and_size mut sz alignment bic opts lty = } crucible_alloc :: - BuiltinContext -> - Options -> L.Type -> LLVMCrucibleSetupM (AllLLVM SetupValue) crucible_alloc = crucible_alloc_with_mutability_and_size Crucible.Mutable Nothing Nothing crucible_alloc_aligned :: - BuiltinContext -> - Options -> Int -> L.Type -> LLVMCrucibleSetupM (AllLLVM SetupValue) @@ -1812,16 +1782,12 @@ crucible_alloc_aligned = crucible_alloc_aligned_with_mutability Crucible.Mutable crucible_alloc_readonly :: - BuiltinContext -> - Options -> L.Type -> LLVMCrucibleSetupM (AllLLVM SetupValue) crucible_alloc_readonly = crucible_alloc_with_mutability_and_size Crucible.Immutable Nothing Nothing crucible_alloc_readonly_aligned :: - BuiltinContext -> - Options -> Int -> L.Type -> LLVMCrucibleSetupM (AllLLVM SetupValue) @@ -1830,19 +1796,15 @@ crucible_alloc_readonly_aligned = crucible_alloc_aligned_with_mutability :: Crucible.Mutability -> - BuiltinContext -> - Options -> Int -> L.Type -> LLVMCrucibleSetupM (AllLLVM SetupValue) -crucible_alloc_aligned_with_mutability mut bic opts n lty = +crucible_alloc_aligned_with_mutability mut n lty = do alignment <- LLVMCrucibleSetupM $ coerceAlignment n crucible_alloc_with_mutability_and_size mut Nothing (Just alignment) - bic - opts lty coerceAlignment :: Int -> CrucibleSetup (LLVM arch) Crucible.Alignment @@ -1858,32 +1820,26 @@ coerceAlignment n = Just alignment -> return alignment crucible_alloc_with_size :: - BuiltinContext -> - Options -> Int {-^ allocation size (in bytes) -} -> L.Type -> LLVMCrucibleSetupM (AllLLVM SetupValue) -crucible_alloc_with_size bic opts sz lty = +crucible_alloc_with_size sz lty = crucible_alloc_with_mutability_and_size Crucible.Mutable (Just (Crucible.toBytes sz)) Nothing - bic - opts lty crucible_symbolic_alloc :: - BuiltinContext -> - Options -> Bool -> Int -> Term -> LLVMCrucibleSetupM (AllLLVM SetupValue) -crucible_symbolic_alloc bic _opts ro align_bytes sz = +crucible_symbolic_alloc ro align_bytes sz = LLVMCrucibleSetupM $ do alignment <- coerceAlignment align_bytes loc <- getW4Position "crucible_symbolic_alloc" - let sc = biSharedContext bic + sc <- lift getSharedContext sz_ty <- liftIO $ Cryptol.scCryptolType sc =<< scTypeOf sc sz when (Just 64 /= asCryptolBVType sz_ty) $ throwCrucibleSetup loc $ unwords @@ -1911,24 +1867,20 @@ asCryptolBVType ty | otherwise = Nothing crucible_alloc_global :: - BuiltinContext -> - Options -> String -> LLVMCrucibleSetupM () -crucible_alloc_global _bic _opts name = +crucible_alloc_global name = LLVMCrucibleSetupM $ do loc <- getW4Position "crucible_alloc_global" Setup.addAllocGlobal . LLVMAllocGlobal loc $ L.Symbol name crucible_fresh_pointer :: - BuiltinContext -> - Options -> L.Type -> LLVMCrucibleSetupM (AllLLVM SetupValue) -crucible_fresh_pointer bic _opt lty = +crucible_fresh_pointer lty = LLVMCrucibleSetupM $ do loc <- getW4Position "crucible_fresh_pointer" - memTy <- memTypeForLLVMType loc bic lty + memTy <- memTypeForLLVMType loc lty constructFreshPointer (llvmTypeAlias lty) loc memTy constructFreshPointer :: @@ -1960,34 +1912,28 @@ constructFreshPointer mid loc memTy = crucible_points_to :: Bool {- ^ whether to check type compatibility -} -> - BuiltinContext -> - Options -> AllLLVM SetupValue -> AllLLVM SetupValue -> LLVMCrucibleSetupM () -crucible_points_to typed bic opt = - crucible_points_to_internal bic opt typed Nothing +crucible_points_to typed = + crucible_points_to_internal typed Nothing crucible_conditional_points_to :: Bool {- ^ whether to check type compatibility -} -> - BuiltinContext -> - Options -> TypedTerm -> AllLLVM SetupValue -> AllLLVM SetupValue -> LLVMCrucibleSetupM () -crucible_conditional_points_to typed bic opt cond = - crucible_points_to_internal bic opt typed (Just cond) +crucible_conditional_points_to typed cond = + crucible_points_to_internal typed (Just cond) crucible_points_to_internal :: - BuiltinContext -> - Options -> Bool {- ^ whether to check type compatibility -} -> Maybe TypedTerm -> AllLLVM SetupValue -> AllLLVM SetupValue -> LLVMCrucibleSetupM () -crucible_points_to_internal _bic _opt typed cond (getAllLLVM -> ptr) (getAllLLVM -> val) = +crucible_points_to_internal typed cond (getAllLLVM -> ptr) (getAllLLVM -> val) = LLVMCrucibleSetupM $ do cc <- getLLVMCrucibleContext loc <- getW4Position "crucible_points_to" @@ -2017,13 +1963,11 @@ crucible_points_to_internal _bic _opt typed cond (getAllLLVM -> ptr) (getAllLLVM Setup.addPointsTo (LLVMPointsTo loc cond ptr $ ConcreteSizeValue val) crucible_points_to_array_prefix :: - BuiltinContext -> - Options -> AllLLVM SetupValue -> TypedTerm -> TypedTerm -> LLVMCrucibleSetupM () -crucible_points_to_array_prefix _bic _opt (getAllLLVM -> ptr) arr sz = +crucible_points_to_array_prefix (getAllLLVM -> ptr) arr sz = LLVMCrucibleSetupM $ do cc <- getLLVMCrucibleContext loc <- getW4Position "crucible_points_to_array_prefix" @@ -2060,12 +2004,10 @@ crucible_points_to_array_prefix _bic _opt (getAllLLVM -> ptr) arr sz = Setup.addPointsTo (LLVMPointsTo loc Nothing ptr $ SymbolicSizeValue arr sz) crucible_equal :: - BuiltinContext -> - Options -> AllLLVM SetupValue -> AllLLVM SetupValue -> LLVMCrucibleSetupM () -crucible_equal _bic _opt (getAllLLVM -> val1) (getAllLLVM -> val2) = +crucible_equal (getAllLLVM -> val1) (getAllLLVM -> val2) = LLVMCrucibleSetupM $ do cc <- getLLVMCrucibleContext loc <- getW4Position "crucible_equal" @@ -2084,22 +2026,18 @@ crucible_equal _bic _opt (getAllLLVM -> val1) (getAllLLVM -> val2) = Setup.addCondition (MS.SetupCond_Equal loc val1 val2) crucible_declare_ghost_state :: - BuiltinContext -> - Options -> String -> TopLevel Value -crucible_declare_ghost_state _bic _opt name = +crucible_declare_ghost_state name = do allocator <- getHandleAlloc global <- liftIO (Crucible.freshGlobalVar allocator (Text.pack name) knownRepr) return (VGhostVar global) crucible_ghost_value :: - BuiltinContext -> - Options -> MS.GhostGlobal -> TypedTerm -> LLVMCrucibleSetupM () -crucible_ghost_value _bic _opt ghost val = LLVMCrucibleSetupM $ +crucible_ghost_value ghost val = LLVMCrucibleSetupM $ do loc <- getW4Position "crucible_ghost_value" Setup.addCondition (MS.SetupCond_Ghost () loc ghost val) @@ -2112,13 +2050,12 @@ crucible_spec_size (SomeLLVM mir) = solverStatsGoalSize $ mir ^. MS.csSolverStats crucible_setup_val_to_typed_term :: - BuiltinContext -> - Options -> AllLLVM SetupValue -> TopLevel TypedTerm -crucible_setup_val_to_typed_term bic _opt (getAllLLVM -> sval) = +crucible_setup_val_to_typed_term (getAllLLVM -> sval) = do opts <- getOptions - mtt <- io $ MaybeT.runMaybeT $ MS.setupToTypedTerm opts (biSharedContext bic) sval + sc <- getSharedContext + mtt <- io $ MaybeT.runMaybeT $ MS.setupToTypedTerm opts sc sval case mtt of Nothing -> throwTopLevel $ "Could not convert a setup value to a term: " ++ show sval Just tt -> return tt diff --git a/src/SAWScript/Crucible/LLVM/Skeleton/Builtins.hs b/src/SAWScript/Crucible/LLVM/Skeleton/Builtins.hs index 39d5e0ba24..748c57e860 100644 --- a/src/SAWScript/Crucible/LLVM/Skeleton/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Skeleton/Builtins.hs @@ -43,7 +43,6 @@ import qualified Lang.Crucible.LLVM.TypeContext as C.LLVM import Verifier.SAW.TypedTerm -import SAWScript.Options import SAWScript.Value import SAWScript.Crucible.Common.MethodSpec import SAWScript.Crucible.LLVM.Builtins @@ -153,38 +152,32 @@ skeleton_guess_arg_sizes mskel (Some m) profiles = do -- ** Writing SAWScript specifications using skeletons skeleton_globals_pre :: - BuiltinContext -> - Options -> ModuleSkeleton -> LLVMCrucibleSetupM () -skeleton_globals_pre bic opts mskel = +skeleton_globals_pre mskel = forM_ (mskel ^. modSkelGlobals) $ \gskel -> when (gskel ^. globSkelMutable) $ do let gname = Text.unpack $ gskel ^. globSkelName - crucible_alloc_global bic opts gname + crucible_alloc_global gname when (gskel ^. globSkelInitialized) - . crucible_points_to True bic opts (anySetupGlobal gname) + . crucible_points_to True (anySetupGlobal gname) $ anySetupGlobalInitializer gname skeleton_globals_post :: - BuiltinContext -> - Options -> ModuleSkeleton -> LLVMCrucibleSetupM () -skeleton_globals_post bic opts mskel = +skeleton_globals_post mskel = forM_ (mskel ^. modSkelGlobals) $ \gskel -> do when (gskel ^. globSkelMutable && gskel ^. globSkelInitialized) $ do let gname = Text.unpack $ gskel ^. globSkelName - crucible_points_to True bic opts (anySetupGlobal gname) + crucible_points_to True (anySetupGlobal gname) $ anySetupGlobalInitializer gname buildArg :: - BuiltinContext -> - Options -> ArgSkeleton -> Int -> LLVMCrucibleSetupM (Maybe TypedTerm, Maybe (AllLLVM SetupValue), Maybe Text) -buildArg bic opts arg idx +buildArg arg idx | arg ^. argSkelType . typeSkelIsPointer = let pt = arg ^. argSkelType . typeSkelLLVMType @@ -195,51 +188,45 @@ buildArg bic opts arg idx | otherwise -> (pt, s ^. sizeGuessInitialized) _ -> (pt, False) in do - ptr <- crucible_alloc bic opts t + ptr <- crucible_alloc t mval <- if initialized then do - val <- crucible_fresh_var bic opts ident t - crucible_points_to True bic opts ptr (anySetupTerm val) + val <- crucible_fresh_var ident t + crucible_points_to True ptr (anySetupTerm val) pure $ Just val else pure Nothing pure (mval, Just ptr, arg ^. argSkelName) | otherwise = do - val <- crucible_fresh_var bic opts ident + val <- crucible_fresh_var ident $ arg ^. argSkelType . typeSkelLLVMType pure (Just val, Nothing, arg ^. argSkelName) where ident = maybe ("arg" <> show idx) Text.unpack $ arg ^. argSkelName skeleton_prestate :: - BuiltinContext -> - Options -> FunctionSkeleton -> LLVMCrucibleSetupM SkeletonState -skeleton_prestate bic opts skel = do - _skelArgs <- mapM (uncurry $ buildArg bic opts) $ zip (skel ^. funSkelArgs) [1,2..] +skeleton_prestate skel = do + _skelArgs <- mapM (uncurry buildArg) $ zip (skel ^. funSkelArgs) [1,2..] pure $ SkeletonState{..} skeleton_exec :: - BuiltinContext -> - Options -> SkeletonState -> LLVMCrucibleSetupM () -skeleton_exec bic opts prestate = do +skeleton_exec prestate = do args <- forM (prestate ^. skelArgs) $ \(mval, mptr, _) -> case (mval, mptr) of (_, Just ptr) -> pure ptr (Just val, Nothing) -> pure $ anySetupTerm val (Nothing, Nothing) -> throwSkeletonLLVM "skeleton_exec" "Invalid pointer-pointee combination on skeleton argument" - crucible_execute_func bic opts args + crucible_execute_func args rebuildArg :: - BuiltinContext -> - Options -> (ArgSkeleton, (Maybe TypedTerm, Maybe (AllLLVM SetupValue), Maybe Text)) -> Int -> LLVMCrucibleSetupM (Maybe TypedTerm, Maybe (AllLLVM SetupValue), Maybe Text) -rebuildArg bic opts (arg, prearg) idx +rebuildArg (arg, prearg) idx | arg ^. argSkelType . typeSkelIsPointer , (_, Just ptr, nm) <- prearg = let @@ -252,35 +239,31 @@ rebuildArg bic opts (arg, prearg) idx _ -> pt ident = maybe ("arg" <> show idx) Text.unpack nm in do - val' <- crucible_fresh_var bic opts ident t - crucible_points_to True bic opts ptr $ anySetupTerm val' + val' <- crucible_fresh_var ident t + crucible_points_to True ptr $ anySetupTerm val' pure (Just val', Just ptr, nm) | otherwise = pure prearg skeleton_poststate :: - BuiltinContext -> - Options -> FunctionSkeleton -> SkeletonState -> LLVMCrucibleSetupM SkeletonState -skeleton_poststate bic opts skel prestate = do - _skelArgs <- zipWithM (rebuildArg bic opts) +skeleton_poststate skel prestate = do + _skelArgs <- zipWithM rebuildArg (zip (skel ^. funSkelArgs) (prestate ^. skelArgs)) [1,2..] case skel ^. funSkelRet . typeSkelLLVMType of LLVM.PrimType LLVM.Void -> pure () t -> do - ret <- crucible_fresh_var bic opts ("return value of " <> (Text.unpack $ skel ^. funSkelName)) t - crucible_return bic opts $ anySetupTerm ret + ret <- crucible_fresh_var ("return value of " <> (Text.unpack $ skel ^. funSkelName)) t + crucible_return $ anySetupTerm ret pure $ SkeletonState{..} skeleton_arg_index :: - BuiltinContext -> - Options -> SkeletonState -> Int -> LLVMCrucibleSetupM TypedTerm -skeleton_arg_index _bic _opts state idx +skeleton_arg_index state idx | idx < length (state ^. skelArgs) , (Just t, _, _) <- (state ^. skelArgs) !! idx = pure t @@ -297,14 +280,12 @@ stateArgIndex state nm = flip findIndex (state ^. skelArgs) $ \(_, _, mnm) -> mnm == Just (Text.pack nm) skeleton_arg :: - BuiltinContext -> - Options -> SkeletonState -> String -> LLVMCrucibleSetupM TypedTerm -skeleton_arg bic opts state nm +skeleton_arg state nm | Just idx <- stateArgIndex state nm - = skeleton_arg_index bic opts state idx + = skeleton_arg_index state idx | otherwise = throwSkeletonLLVM "skeleton_arg" $ mconcat [ "No initialized argument named \"" , nm @@ -312,12 +293,10 @@ skeleton_arg bic opts state nm ] skeleton_arg_index_pointer :: - BuiltinContext -> - Options -> SkeletonState -> Int -> LLVMCrucibleSetupM (AllLLVM SetupValue) -skeleton_arg_index_pointer _bic _opts state idx +skeleton_arg_index_pointer state idx | idx < length (state ^. skelArgs) , (_, mp, _) <- (state ^. skelArgs) !! idx = case mp of @@ -333,14 +312,12 @@ skeleton_arg_index_pointer _bic _opts state idx ] skeleton_arg_pointer :: - BuiltinContext -> - Options -> SkeletonState -> String -> LLVMCrucibleSetupM (AllLLVM SetupValue) -skeleton_arg_pointer bic opts state nm +skeleton_arg_pointer state nm | Just idx <- stateArgIndex state nm - = skeleton_arg_index_pointer bic opts state idx + = skeleton_arg_index_pointer state idx | otherwise = do throwSkeletonLLVM "skeleton_arg_pointer" $ mconcat [ "No argument named \"" diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index e85fa06e7a..127690a90c 100644 --- a/src/SAWScript/Crucible/LLVM/X86.hs +++ b/src/SAWScript/Crucible/LLVM/X86.hs @@ -221,8 +221,6 @@ cryptolUninterpreted _ nm _ xs = throwX86 $ mconcat -- to an LLVM specification. This allows for compositional verification of LLVM -- functions that call x86_64 functions (but not the other way around). crucible_llvm_verify_x86 :: - BuiltinContext -> - Options -> Some LLVMModule {- ^ Module to associate with method spec -} -> FilePath {- ^ Path to ELF file -} -> String {- ^ Function's symbol in ELF file -} -> @@ -231,12 +229,14 @@ crucible_llvm_verify_x86 :: LLVMCrucibleSetupM () {- ^ Specification to verify against -} -> ProofScript SatResult {- ^ Tactic used to use when discharging goals -} -> TopLevel (SomeLLVM MS.CrucibleMethodSpecIR) -crucible_llvm_verify_x86 bic opts (Some (llvmModule :: LLVMModule x)) path nm globsyms checkSat setup tactic +crucible_llvm_verify_x86 (Some (llvmModule :: LLVMModule x)) path nm globsyms checkSat setup tactic | Just Refl <- testEquality (C.LLVM.X86Repr $ knownNat @64) . C.LLVM.llvmArch $ modTrans llvmModule ^. C.LLVM.transContext = do let ?ptrWidth = knownNat @64 let ?recordLLVMAnnotation = \_ _ -> return () - let sc = biSharedContext bic + sc <- getSharedContext + opts <- getOptions + basic_ss <- getBasicSS sym <- liftIO $ C.newSAWCoreBackend W4.FloatRealRepr sc globalNonceGenerator halloc <- getHandleAlloc let mvar = C.LLVM.llvmMemVar . view C.LLVM.transContext $ modTrans llvmModule @@ -262,7 +262,7 @@ crucible_llvm_verify_x86 bic opts (Some (llvmModule :: LLVMModule x)) path nm gl cc = LLVMCrucibleContext { _ccLLVMModule = llvmModule , _ccBackend = sym - , _ccBasicSS = biBasicSS bic + , _ccBasicSS = basic_ss -- It's unpleasant that we need to do this to use resolveSetupVal. , _ccLLVMSimContext = error "Attempted to access ccLLVMSimContext" @@ -278,7 +278,7 @@ crucible_llvm_verify_x86 bic opts (Some (llvmModule :: LLVMModule x)) path nm gl ] liftIO $ printOutLn opts Info "Examining specification to determine preconditions" - methodSpec <- buildMethodSpec bic opts llvmModule nm (show addr) checkSat setup + methodSpec <- buildMethodSpec llvmModule nm (show addr) checkSat setup let ?lc = modTrans llvmModule ^. C.LLVM.transContext . C.LLVM.llvmTypeCtx @@ -430,21 +430,20 @@ buildCFG opts halloc preserved path nm = do -- Unlike in crucible_llvm_verify, we can't reuse the simulator state (due to the -- different memory layout / RegMap). buildMethodSpec :: - BuiltinContext -> - Options -> LLVMModule LLVMArch -> String {- ^ Name of method -} -> String {- ^ Source location for method spec (here, we use the address) -} -> Bool {- ^ check sat -} -> LLVMCrucibleSetupM () -> TopLevel (MS.CrucibleMethodSpecIR LLVM) -buildMethodSpec bic opts lm nm loc checkSat setup = - setupLLVMCrucibleContext bic opts checkSat lm $ \cc -> do +buildMethodSpec lm nm loc checkSat setup = + setupLLVMCrucibleContext checkSat lm $ \cc -> do let methodId = LLVMMethodId nm Nothing let programLoc = W4.mkProgramLoc (W4.functionNameFromText $ Text.pack nm) . W4.OtherPos $ Text.pack loc let lc = modTrans lm ^. C.LLVM.transContext . C.LLVM.llvmTypeCtx + opts <- getOptions (args, ret) <- case llvmSignature opts lm nm of Left err -> fail $ mconcat ["Could not find declaration for \"", nm, "\": ", err] Right x -> pure x diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 5a6b562693..c2c7fc2e0b 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -429,6 +429,7 @@ buildTopLevelEnv proxy opts = , roPosition = SS.Unknown , roProxy = proxy , roInitWorkDir = currDir + , roBasicSS = ss } let bic = BuiltinContext { biSharedContext = sc @@ -1535,7 +1536,7 @@ primitives = Map.fromList --, prim "java_value" "{a} String -> a" , prim "java_var" "String -> JavaType -> JavaSetup Term" - (bicVal javaVar) + (pureVal javaVar) Deprecated [ "Return a term corresponding to the initial value of the named Java" , "variable, which should have the given type. The returned term can be" @@ -1546,7 +1547,7 @@ primitives = Map.fromList ] , prim "java_class_var" "String -> JavaType -> JavaSetup ()" - (bicVal javaClassVar) + (pureVal javaClassVar) Deprecated [ "Declare that the named Java variable should point to an object of the" , "given class type." @@ -1567,14 +1568,14 @@ primitives = Map.fromList ] , prim "java_assert_eq" "String -> Term -> JavaSetup ()" - (bicVal javaAssertEq) + (pureVal javaAssertEq) Deprecated [ "Assert that the given variable should have the given value in the" , "initial state of a Java method." ] , prim "java_ensure_eq" "String -> Term -> JavaSetup ()" - (bicVal javaEnsureEq) + (pureVal javaEnsureEq) Deprecated [ "Specify that the given Java variable should have a value equal to the" , "given term when execution finishes." @@ -1630,7 +1631,7 @@ primitives = Map.fromList [ "The empty specification for 'java_verify'. Equivalent to 'return ()'." ] , prim "java_load_class" "String -> TopLevel JavaClass" - (bicVal (const . CJ.loadJavaClass)) + (pureVal CJ.loadJavaClass) Current [ "Load the named Java class and return a handle to it." ] @@ -1638,7 +1639,7 @@ primitives = Map.fromList , prim "java_extract" "JavaClass -> String -> JavaSetup () -> TopLevel Term" - (bicVal extractJava) + (pureVal extractJava) Deprecated [ "Translate a Java method directly to a Term. The parameters of the" , "Term will be the parameters of the Java method, and the return" @@ -1649,7 +1650,7 @@ primitives = Map.fromList , prim "java_symexec" "JavaClass -> String -> [(String, Term)] -> [String] -> Bool -> TopLevel Term" - (bicVal symexecJava) + (pureVal symexecJava) Deprecated [ "Symbolically execute a Java method and construct a Term corresponding" , "to its result. The first list contains pairs of variable or field" @@ -1663,7 +1664,7 @@ primitives = Map.fromList , prim "java_verify" "JavaClass -> String -> [JavaMethodSpec] -> JavaSetup () -> TopLevel JavaMethodSpec" - (bicVal verifyJava) + (pureVal verifyJava) Deprecated [ "Verify a Java method against a method specification. The first two" , "arguments are the same as for 'java_extract' and 'java_symexec'." @@ -1684,7 +1685,7 @@ primitives = Map.fromList ] -} , prim "crucible_java_extract" "JavaClass -> String -> TopLevel Term" - (bicVal CJ.crucible_java_extract) + (pureVal CJ.crucible_java_extract) Current [ "Translate a Java method directly to a Term. The parameters of the" , "Term will be the parameters of the Java method, and the return" @@ -1774,19 +1775,19 @@ primitives = Map.fromList ] , prim "skeleton_globals_pre" "ModuleSkeleton -> CrucibleSetup ()" - (bicVal skeleton_globals_pre) + (pureVal skeleton_globals_pre) Experimental [ "Allocate and initialize mutable globals from the given module skeleton." ] , prim "skeleton_globals_post" "ModuleSkeleton -> CrucibleSetup ()" - (bicVal skeleton_globals_post) + (pureVal skeleton_globals_post) Experimental [ "Assert that all mutable globals from the given module skeleton are unchanged." ] , prim "skeleton_prestate" "FunctionSkeleton -> CrucibleSetup SkeletonState" - (bicVal skeleton_prestate) + (pureVal skeleton_prestate) Experimental [ "Allocate and initialize the arguments of the given function skeleton." , "Return a 'SkeletonState' from which those arguments can be retrieved," @@ -1794,7 +1795,7 @@ primitives = Map.fromList ] , prim "skeleton_poststate" "FunctionSkeleton -> SkeletonState -> CrucibleSetup SkeletonState" - (bicVal skeleton_poststate) + (pureVal skeleton_poststate) Experimental [ "Assert that pointer arguments of the given function skeleton remain" , "initialized. Return a 'SkeletonState' from which those arguments can" @@ -1802,33 +1803,33 @@ primitives = Map.fromList ] , prim "skeleton_arg_index" "SkeletonState -> Int -> CrucibleSetup Term" - (bicVal skeleton_arg_index) + (pureVal skeleton_arg_index) Experimental [ "Retrieve the argument value at the given index from the given 'SkeletonState'." ] , prim "skeleton_arg" "SkeletonState -> String -> CrucibleSetup Term" - (bicVal skeleton_arg) + (pureVal skeleton_arg) Experimental [ "Retrieve the argument value of the given name from the given 'SkeletonState'." ] , prim "skeleton_arg_index_pointer" "SkeletonState -> Int -> CrucibleSetup SetupValue" - (bicVal skeleton_arg_index_pointer) + (pureVal skeleton_arg_index_pointer) Experimental [ "Retrieve the argument pointer at the given indexfrom the given 'SkeletonState'." , "Fails if the specified argument is not a pointer." ] , prim "skeleton_arg_pointer" "SkeletonState -> String -> CrucibleSetup SetupValue" - (bicVal skeleton_arg_pointer) + (pureVal skeleton_arg_pointer) Experimental [ "Retrieve the argument pointer of the given name from the given 'SkeletonState'." , "Fails if the specified argument is not a pointer." ] , prim "skeleton_exec" "SkeletonState -> CrucibleSetup ()" - (bicVal skeleton_exec) + (pureVal skeleton_exec) Experimental [ "Wrapper around 'crucible_execute_func' that passes the arguments initialized" , "in 'skeleton_prestate'." @@ -1995,13 +1996,13 @@ primitives = Map.fromList -- Crucible/LLVM interface , prim "crucible_llvm_cfg" "LLVMModule -> String -> TopLevel CFG" - (bicVal crucible_llvm_cfg) + (pureVal crucible_llvm_cfg) Current [ "Load a function from the given LLVM module into a Crucible CFG." ] , prim "crucible_llvm_extract" "LLVMModule -> String -> TopLevel Term" - (bicVal crucible_llvm_extract) + (pureVal crucible_llvm_extract) Current [ "Translate an LLVM function directly to a Term. The parameters of the" , "Term will be the parameters of the LLVM function, and the return" @@ -2012,7 +2013,7 @@ primitives = Map.fromList , prim "crucible_llvm_compositional_extract" "LLVMModule -> String -> String -> [CrucibleMethodSpec] -> Bool -> CrucibleSetup () -> ProofScript SatResult -> TopLevel CrucibleMethodSpec" - (bicVal crucible_llvm_compositional_extract) + (pureVal crucible_llvm_compositional_extract) Experimental [ "Translate an LLVM function directly to a Term. The parameters of the" , "Term are the input parameters of the LLVM function: the parameters" @@ -2026,14 +2027,14 @@ primitives = Map.fromList ] , prim "crucible_fresh_var" "String -> LLVMType -> CrucibleSetup Term" - (bicVal crucible_fresh_var) + (pureVal crucible_fresh_var) Current [ "Create a fresh symbolic variable for use within a Crucible" , "specification. The name is used only for pretty-printing." ] , prim "crucible_fresh_cryptol_var" "String -> Type -> CrucibleSetup Term" - (bicVal crucible_fresh_cryptol_var) + (pureVal crucible_fresh_cryptol_var) Experimental [ "Create a fresh symbolic variable of the given Cryptol type for use" , "within a Crucible specification. The given name is used only for" @@ -2042,7 +2043,7 @@ primitives = Map.fromList ] , prim "crucible_alloc" "LLVMType -> CrucibleSetup SetupValue" - (bicVal crucible_alloc) + (pureVal crucible_alloc) Current [ "Declare that an object of the given type should be allocated in a" , "Crucible specification. Before `crucible_execute_func`, this states" @@ -2052,7 +2053,7 @@ primitives = Map.fromList ] , prim "crucible_alloc_aligned" "Int -> LLVMType -> CrucibleSetup SetupValue" - (bicVal crucible_alloc_aligned) + (pureVal crucible_alloc_aligned) Current [ "Declare that a memory region of the given type should be allocated in" , "a Crucible specification, and also specify that the start of the region" @@ -2061,7 +2062,7 @@ primitives = Map.fromList ] , prim "crucible_alloc_readonly" "LLVMType -> CrucibleSetup SetupValue" - (bicVal crucible_alloc_readonly) + (pureVal crucible_alloc_readonly) Current [ "Declare that a read-only memory region of the given type should be" , "allocated in a Crucible specification. The function must not attempt" @@ -2071,7 +2072,7 @@ primitives = Map.fromList ] , prim "crucible_alloc_readonly_aligned" "Int -> LLVMType -> CrucibleSetup SetupValue" - (bicVal crucible_alloc_readonly_aligned) + (pureVal crucible_alloc_readonly_aligned) Current [ "Declare that a read-only memory region of the given type should be" , "a Crucible specification, and also specify that the start of the region" @@ -2083,14 +2084,14 @@ primitives = Map.fromList ] , prim "crucible_alloc_with_size" "Int -> LLVMType -> CrucibleSetup SetupValue" - (bicVal crucible_alloc_with_size) + (pureVal crucible_alloc_with_size) Experimental [ "Like `crucible_alloc`, but with a user-specified size (given in bytes)." , "The specified size must be greater than the size of the LLVM type." ] , prim "crucible_symbolic_alloc" "Bool -> Int -> Term -> CrucibleSetup SetupValue" - (bicVal crucible_symbolic_alloc) + (pureVal crucible_symbolic_alloc) Current [ "Like `crucible_alloc`, but with a (symbolic) size instead of" , "a LLVM type. The first argument specifies whether the allocation is" @@ -2099,7 +2100,7 @@ primitives = Map.fromList ] , prim "crucible_alloc_global" "String -> CrucibleSetup ()" - (bicVal crucible_alloc_global) + (pureVal crucible_alloc_global) Current [ "Declare that memory for the named global should be allocated in a" , "Crucible specification. This is done implicitly for immutable globals." @@ -2107,7 +2108,7 @@ primitives = Map.fromList ] , prim "crucible_fresh_pointer" "LLVMType -> CrucibleSetup SetupValue" - (bicVal crucible_fresh_pointer) + (pureVal crucible_fresh_pointer) Current [ "Create a fresh pointer value for use in a Crucible specification." , "This works like `crucible_alloc` except that the pointer is not" @@ -2115,7 +2116,7 @@ primitives = Map.fromList ] , prim "crucible_fresh_expanded_val" "LLVMType -> CrucibleSetup SetupValue" - (bicVal crucible_fresh_expanded_val) + (pureVal crucible_fresh_expanded_val) Current [ "Create a compound type entirely populated with fresh symbolic variables." , "Equivalent to allocating a new struct or array of the given type and" @@ -2124,7 +2125,7 @@ primitives = Map.fromList ] , prim "crucible_points_to" "SetupValue -> SetupValue -> CrucibleSetup ()" - (bicVal (crucible_points_to True)) + (pureVal (crucible_points_to True)) Current [ "Declare that the memory location indicated by the given pointer (first" , "argument) contains the given value (second argument)." @@ -2136,7 +2137,7 @@ primitives = Map.fromList ] , prim "crucible_conditional_points_to" "Term -> SetupValue -> SetupValue -> CrucibleSetup ()" - (bicVal (crucible_conditional_points_to True)) + (pureVal (crucible_conditional_points_to True)) Current [ "Declare that the memory location indicated by the given pointer (second" , "argument) contains the given value (third argument) if the given" @@ -2149,7 +2150,7 @@ primitives = Map.fromList ] , prim "crucible_points_to_untyped" "SetupValue -> SetupValue -> CrucibleSetup ()" - (bicVal (crucible_points_to False)) + (pureVal (crucible_points_to False)) Current [ "A variant of crucible_points_to that does not check for compatibility" , "between the pointer type and the value type. This may be useful when" @@ -2157,7 +2158,7 @@ primitives = Map.fromList ] , prim "crucible_conditional_points_to_untyped" "Term -> SetupValue -> SetupValue -> CrucibleSetup ()" - (bicVal (crucible_conditional_points_to False)) + (pureVal (crucible_conditional_points_to False)) Current [ "A variant of crucible_conditional_points_to that does not check for" , "compatibility between the pointer type and the value type. This may" @@ -2165,7 +2166,7 @@ primitives = Map.fromList ] , prim "crucible_points_to_array_prefix" "SetupValue -> Term -> Term -> CrucibleSetup ()" - (bicVal crucible_points_to_array_prefix) + (pureVal crucible_points_to_array_prefix) Experimental [ "Declare that the memory location indicated by the given pointer (first" , "argument) contains the prefix of the given array (second argument) of" @@ -2178,7 +2179,7 @@ primitives = Map.fromList ] , prim "crucible_equal" "SetupValue -> SetupValue -> CrucibleSetup ()" - (bicVal crucible_equal) + (pureVal crucible_equal) Current [ "State that two Crucible values should be equal. Can be used as either" , "a pre-condition or a post-condition. It is semantically equivalent to" @@ -2201,7 +2202,7 @@ primitives = Map.fromList ] , prim "crucible_execute_func" "[SetupValue] -> CrucibleSetup ()" - (bicVal crucible_execute_func) + (pureVal crucible_execute_func) Current [ "Specify the given list of values as the arguments of the function." , "" @@ -2213,7 +2214,7 @@ primitives = Map.fromList ] , prim "crucible_return" "SetupValue -> CrucibleSetup ()" - (bicVal crucible_return) + (pureVal crucible_return) Current [ "Specify the given value as the return value of the function. A" , "crucible_return statement is required if and only if the function" @@ -2221,7 +2222,7 @@ primitives = Map.fromList , prim "crucible_llvm_verify" "LLVMModule -> String -> [CrucibleMethodSpec] -> Bool -> CrucibleSetup () -> ProofScript SatResult -> TopLevel CrucibleMethodSpec" - (bicVal crucible_llvm_verify) + (pureVal crucible_llvm_verify) Current [ "Verify the LLVM function named by the second parameter in the module" , "specified by the first. The third parameter lists the CrucibleMethodSpec" @@ -2234,7 +2235,7 @@ primitives = Map.fromList , prim "crucible_llvm_unsafe_assume_spec" "LLVMModule -> String -> CrucibleSetup () -> TopLevel CrucibleMethodSpec" - (bicVal crucible_llvm_unsafe_assume_spec) + (pureVal crucible_llvm_unsafe_assume_spec) Current [ "Return a CrucibleMethodSpec corresponding to a CrucibleSetup block," , "as would be returned by crucible_llvm_verify but without performing" @@ -2243,7 +2244,7 @@ primitives = Map.fromList , prim "crucible_llvm_array_size_profile" "LLVMModule -> String -> [CrucibleMethodSpec] -> CrucibleSetup () -> TopLevel [(String, [FunctionProfile])]" - (bicVal $ crucible_llvm_array_size_profile assumeUnsat) + (pureVal $ crucible_llvm_array_size_profile assumeUnsat) Experimental [ "Symbolically execute the function named by the second parameter in" , "the module specified by the first. The fourth parameter may be used" @@ -2254,7 +2255,7 @@ primitives = Map.fromList , prim "crucible_llvm_verify_x86" "LLVMModule -> String -> String -> [(String, Int)] -> Bool -> CrucibleSetup () -> ProofScript SatResult -> TopLevel CrucibleMethodSpec" - (bicVal crucible_llvm_verify_x86) + (pureVal crucible_llvm_verify_x86) Experimental [ "Verify an x86 function from an ELF file for use as an override in an" , "LLVM verification. The first argument specifies the LLVM module" @@ -2341,7 +2342,7 @@ primitives = Map.fromList , prim "crucible_setup_val_to_term" " SetupValue -> TopLevel Term" - (bicVal crucible_setup_val_to_typed_term) + (pureVal crucible_setup_val_to_typed_term) Current [ "Convert from a setup value to a typed term. This can only be done for a" , "subset of setup values. Fails if a setup value is a global, variable or null." @@ -2350,13 +2351,13 @@ primitives = Map.fromList -- Ghost state support , prim "crucible_declare_ghost_state" "String -> TopLevel Ghost" - (bicVal crucible_declare_ghost_state) + (pureVal crucible_declare_ghost_state) Current [ "Allocates a unique ghost variable." ] , prim "crucible_ghost_value" "Ghost -> Term -> CrucibleSetup ()" - (bicVal crucible_ghost_value) + (pureVal crucible_ghost_value) Current [ "Specifies the value of a ghost variable. This can be used" , "in the pre- and post- conditions of a setup block."] @@ -2378,14 +2379,14 @@ primitives = Map.fromList -- Crucible/JVM commands , prim "jvm_fresh_var" "String -> JavaType -> JVMSetup Term" - (bicVal jvm_fresh_var) + (pureVal jvm_fresh_var) Experimental [ "Create a fresh variable for use within a Crucible specification. The" , "name is used only for pretty-printing." ] , prim "jvm_alloc_object" "String -> JVMSetup JVMValue" - (bicVal jvm_alloc_object) + (pureVal jvm_alloc_object) Experimental [ "Declare that an instance of the given class should be allocated in a" , "Crucible specification. Before `jvm_execute_func`, this states" @@ -2395,7 +2396,7 @@ primitives = Map.fromList ] , prim "jvm_alloc_array" "Int -> JavaType -> JVMSetup JVMValue" - (bicVal jvm_alloc_array) + (pureVal jvm_alloc_array) Experimental [ "Declare that an array of the given size and element type should be" , "allocated in a Crucible specification. Before `jvm_execute_func`, this" @@ -2407,7 +2408,7 @@ primitives = Map.fromList -- TODO: jvm_alloc_multiarray , prim "jvm_field_is" "JVMValue -> String -> JVMValue -> JVMSetup ()" - (bicVal (jvm_field_is True)) + (pureVal jvm_field_is) Experimental [ "Declare that the indicated object (first argument) has a field" , "(second argument) containing the given value (third argument)." @@ -2419,7 +2420,7 @@ primitives = Map.fromList ] , prim "jvm_elem_is" "JVMValue -> Int -> JVMValue -> JVMSetup ()" - (bicVal (jvm_elem_is True)) + (pureVal jvm_elem_is) Experimental [ "Declare that the indicated array (first argument) has an element" , "(second argument) containing the given value (third argument)." @@ -2431,7 +2432,7 @@ primitives = Map.fromList ] , prim "jvm_array_is" "JVMValue -> Term -> JVMSetup ()" - (bicVal (jvm_array_is True)) + (pureVal jvm_array_is) Experimental [ "Declare that the indicated array reference (first argument) contains" , "the given sequence of values (second argument)." @@ -2457,7 +2458,7 @@ primitives = Map.fromList ] , prim "jvm_execute_func" "[JVMValue] -> JVMSetup ()" - (bicVal jvm_execute_func) + (pureVal jvm_execute_func) Experimental [ "Specify the given list of values as the arguments of the function." , "" @@ -2469,7 +2470,7 @@ primitives = Map.fromList ] , prim "jvm_return" "JVMValue -> JVMSetup ()" - (bicVal jvm_return) + (pureVal jvm_return) Experimental [ "Specify the given value as the return value of the function. A" , "jvm_return statement is required if and only if the function" @@ -2477,7 +2478,7 @@ primitives = Map.fromList , prim "crucible_jvm_verify" "JavaClass -> String -> [JVMMethodSpec] -> Bool -> JVMSetup () -> ProofScript SatResult -> TopLevel JVMMethodSpec" - (bicVal crucible_jvm_verify) + (pureVal crucible_jvm_verify) Experimental [ "Verify the JVM function named by the second parameter in the module" , "specified by the first. The third parameter lists the JVMMethodSpec" @@ -2490,7 +2491,7 @@ primitives = Map.fromList , prim "crucible_jvm_unsafe_assume_spec" "JavaClass -> String -> JVMSetup () -> TopLevel JVMMethodSpec" - (bicVal crucible_jvm_unsafe_assume_spec) + (pureVal crucible_jvm_unsafe_assume_spec) Experimental [ "Return a JVMMethodSpec corresponding to a JVMSetup block," , "as would be returned by jvm_verify but without performing any" diff --git a/src/SAWScript/JavaBuiltins.hs b/src/SAWScript/JavaBuiltins.hs index d5aac9e9ff..d763b5b226 100644 --- a/src/SAWScript/JavaBuiltins.hs +++ b/src/SAWScript/JavaBuiltins.hs @@ -64,9 +64,9 @@ import qualified Cryptol.Eval.Concrete as Cryptol (Concrete(..)) import qualified Cryptol.TypeCheck.AST as Cryptol import qualified Cryptol.Utils.PP as Cryptol (pretty) -loadJavaClass :: BuiltinContext -> String -> IO Class -loadJavaClass bic = - lookupClass (biJavaCodebase bic) fixPos . mkClassName . dotsToSlashes +loadJavaClass :: JSS.Codebase -> String -> IO Class +loadJavaClass cb = + lookupClass cb fixPos . mkClassName . dotsToSlashes getActualArgTypes :: JavaSetupState -> Either String [JavaActualType] getActualArgTypes s = mapM getActualType declaredTypes @@ -87,18 +87,17 @@ getActualArgTypes s = mapM getActualType declaredTypes type Assign = (JavaExpr, TypedTerm) -symexecJava :: BuiltinContext - -> Options - -> Class +symexecJava :: Class -> String -> [(String, TypedTerm)] -> [String] -> Bool -> TopLevel TypedTerm -symexecJava bic opts cls mname inputs outputs satBranches = do - let cb = biJavaCodebase bic - pos = fixPos - jsc = biSharedContext bic +symexecJava cls mname inputs outputs satBranches = do + cb <- getJavaCodebase + jsc <- getSharedContext + opts <- getOptions + let pos = fixPos fl = defaultSimFlags { alwaysBitBlastBranchTerms = True , satAtBranches = satBranches } @@ -151,13 +150,14 @@ symexecJava bic opts cls mname inputs outputs satBranches = do _ -> scTuple jsc tms liftIO (mkTypedTerm jsc =<< bundle outtms) -extractJava :: BuiltinContext -> Options -> Class -> String +extractJava :: Class -> String -> JavaSetup () -> TopLevel TypedTerm -extractJava bic opts cls mname setup = do - let cb = biJavaCodebase bic - pos = fixPos - jsc = biSharedContext bic +extractJava cls mname setup = do + cb <- getJavaCodebase + sc <- getSharedContext + opts <- getOptions + let pos = fixPos argsRef <- io $ newIORef [] withSAWBackend (Just argsRef) $ \sbe -> do setupRes <- runJavaSetup pos cb cls mname setup @@ -167,23 +167,22 @@ extractJava bic opts cls mname setup = do io $ runSimulator cb sbe defaultSEH (Just fl) $ do setVerbosity (simVerbose opts) argTypes <- either fail return (getActualArgTypes setupRes) - args <- mapM (freshJavaVal (Just argsRef) jsc) argTypes + args <- mapM (freshJavaVal (Just argsRef) sc) argTypes -- TODO: support initializing other state elements rslt <- case methodIsStatic meth of True -> execStaticMethod (className cls) (methodKey meth) args False -> do - ~(RValue this) <- freshJavaVal (Just argsRef) jsc (ClassInstance cls) + ~(RValue this) <- freshJavaVal (Just argsRef) sc (ClassInstance cls) execInstanceMethod (className cls) (methodKey meth) this args dt <- case (rslt, methodReturnType meth) of (Nothing, _) -> fail $ "No return value from " ++ methodName meth (_, Nothing) -> fail $ "Return value from void method " ++ methodName meth - (Just v, Just tp) -> termOfValueSim jsc tp v + (Just v, Just tp) -> termOfValueSim sc tp v liftIO $ do - let sc = biSharedContext bic argBinds <- reverse <$> readIORef argsRef let exts = mapMaybe asExtCns argBinds -- TODO: group argBinds according to the declared types - scAbstractExts jsc exts dt >>= mkTypedTerm sc + scAbstractExts sc exts dt >>= mkTypedTerm sc withSAWBackend :: Maybe (IORef [Term]) -> (Backend SharedContext -> TopLevel a) @@ -208,21 +207,21 @@ runJavaSetup pos cb cls mname setup = do } execStateT setup setupState -verifyJava :: BuiltinContext -> Options -> Class -> String +verifyJava :: Class -> String -> [JavaMethodSpecIR] -> JavaSetup () -> TopLevel JavaMethodSpecIR -verifyJava bic opts cls mname overrides setup = do +verifyJava cls mname overrides setup = do startTime <- io $ getCurrentTime + cb <- getJavaCodebase + sc <- getSharedContext + opts <- getOptions let pos = fixPos -- TODO - cb = biJavaCodebase bic - bsc = biSharedContext bic - jsc = bsc setupRes <- runJavaSetup pos cb cls mname setup let ms = jsSpec setupRes vp = VerifyParams { vpCode = cb - , vpContext = jsc + , vpContext = sc , vpOpts = opts , vpSpec = ms , vpOver = overrides @@ -253,27 +252,27 @@ verifyJava bic opts cls mname overrides setup = do setVerbosity (simVerbose opts) let prover script vs n g = do let exts = getAllExts g - gprop <- io $ scGeneralizeExts jsc exts =<< scEqTrue jsc g - io $ doExtraChecks opts bsc gprop + gprop <- io $ scGeneralizeExts sc exts =<< scEqTrue sc g + io $ doExtraChecks opts sc gprop let goal = ProofGoal n "vc" (vsVCName vs) (Prop gprop) r <- evalStateT script (startProof goal) case r of SS.Unsat _ -> liftIO $ printOutLn opts Debug "Valid." SS.SatMulti _ vals -> - io $ showCexResults opts jsc (rwPPOpts rw) ms vs exts vals + io $ showCexResults opts sc (rwPPOpts rw) ms vs exts vals let ovds = vpOver vp - initPS <- initializeVerification' jsc ms bs cl + initPS <- initializeVerification' sc ms bs cl liftIO $ printOutLn opts Debug $ "Overriding: " ++ show (map specName ovds) - mapM_ (overrideFromSpec jsc (specPos ms)) ovds + mapM_ (overrideFromSpec sc (specPos ms)) ovds liftIO $ printOutLn opts Debug $ "Running method: " ++ specName ms -- Execute code. run liftIO $ printOutLn opts Debug $ "Checking final state" - pvc <- checkFinalState jsc ms bs cl initPS + pvc <- checkFinalState sc ms bs cl initPS let pvcs = [pvc] -- Only one for now, but that might change liftIO $ printOutLn opts ExtraDebug "Verifying the following:" liftIO $ mapM_ (printOutLn opts ExtraDebug . show . ppPathVC) pvcs - let validator script = runValidation (prover script) vp jsc pvcs + let validator script = runValidation (prover script) vp sc pvcs case jsTactic setupRes of Skip -> liftIO $ printOutLn opts Warn $ "WARNING: skipping verification of " ++ specName ms @@ -402,11 +401,10 @@ getJavaExpr ctx name = do , ftext "Maybe you're missing a `java_var` or `java_class_var`?" ] -typeJavaExpr :: BuiltinContext -> String -> JavaType +typeJavaExpr :: JSS.Codebase -> String -> JavaType -> JavaSetup (JavaExpr, JavaActualType) -typeJavaExpr bic name ty = do +typeJavaExpr cb name ty = do ms <- gets jsSpec - let cb = biJavaCodebase bic expr <- parseJavaExpr' cb (specThisClass ms) (specMethod ms) name jty' <- exportJSSType ty checkEqualTypes (exprType expr) jty' name @@ -441,24 +439,26 @@ javaRequiresClass cls = modifySpec $ \ms -> let clss' = mkClassName (dotsToSlashes cls) : specInitializedClasses ms in ms { specInitializedClasses = clss' } -javaClassVar :: BuiltinContext -> Options -> String -> JavaType +javaClassVar :: String -> JavaType -> JavaSetup () -javaClassVar bic _ name t = do - (expr, aty) <- typeJavaExpr bic name t +javaClassVar name t = do + cb <- lift getJavaCodebase + (expr, aty) <- typeJavaExpr cb name t case aty of ClassInstance _ -> return () _ -> throwJava "Can't use `java_class_var` with variable of non-class type." modifySpec (specAddVarDecl expr aty) -javaVar :: BuiltinContext -> Options -> String -> JavaType +javaVar :: String -> JavaType -> JavaSetup TypedTerm -javaVar bic _ name t = do - (expr, aty) <- typeJavaExpr bic name t +javaVar name t = do + cb <- lift getJavaCodebase + (expr, aty) <- typeJavaExpr cb name t case aty of ClassInstance _ -> throwJava "Can't use `java_var` with variable of class type." _ -> return () modifySpec (specAddVarDecl expr aty) - let sc = biSharedContext bic + sc <- lift getSharedContext case cryptolTypeOfActual aty of Nothing -> throwJava $ "Unsupported type for `java_var`: " ++ show aty Just cty -> @@ -485,21 +485,23 @@ javaAssert (TypedTerm schema v) = do LE le -> modifySpec (specAddAssumption le) JE je -> throwJava $ "Used java_assert with Java expression: " ++ show je -javaAssertEq :: BuiltinContext -> Options -> String -> TypedTerm -> JavaSetup () -javaAssertEq bic _ name (TypedTerm schema t) = do +javaAssertEq :: String -> TypedTerm -> JavaSetup () +javaAssertEq name (TypedTerm schema t) = do (expr, aty) <- (getJavaExpr "java_assert_eq") name - checkCompatibleType (biSharedContext bic) "java_assert_eq" aty schema + sc <- lift getSharedContext + checkCompatibleType sc "java_assert_eq" aty schema me <- mkMixedExpr t modifySpec (specAddLogicAssignment fixPos expr me) -javaEnsureEq :: BuiltinContext -> Options -> String -> TypedTerm -> JavaSetup () -javaEnsureEq bic _ name (TypedTerm schema t) = do +javaEnsureEq :: String -> TypedTerm -> JavaSetup () +javaEnsureEq name (TypedTerm schema t) = do ms <- gets jsSpec + sc <- lift getSharedContext (expr, aty) <- (getJavaExpr "java_ensure_eq") name when (isArg (specMethod ms) expr && isScalarExpr expr) $ throwJava $ "The `java_ensure_eq` function cannot be used " ++ "to set the value of a scalar argument." - checkCompatibleType (biSharedContext bic) "java_ensure_eq" aty schema + checkCompatibleType sc "java_ensure_eq" aty schema me <- mkMixedExpr t cmd <- case (CC.unTerm expr, aty) of (_, ArrayInstance _ _) -> return (EnsureArray fixPos expr me) diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index a14981ab61..9e03f06a15 100644 --- a/src/SAWScript/Value.hs +++ b/src/SAWScript/Value.hs @@ -389,6 +389,7 @@ data TopLevelRO = , roPosition :: SS.Pos , roProxy :: AIGProxy , roInitWorkDir :: FilePath + , roBasicSS :: Simpset } data TopLevelRW = @@ -451,6 +452,9 @@ getOptions = TopLevel (asks roOptions) getProxy :: TopLevel AIGProxy getProxy = TopLevel (asks roProxy) +getBasicSS :: TopLevel Simpset +getBasicSS = TopLevel (asks roBasicSS) + localOptions :: (Options -> Options) -> TopLevel a -> TopLevel a localOptions f (TopLevel m) = TopLevel (local (\x -> x {roOptions = f (roOptions x)}) m)