diff --git a/src/SAWScript/AutoMatch/LLVM.hs b/src/SAWScript/AutoMatch/LLVM.hs index bbdc286a8a..7758db852a 100644 --- a/src/SAWScript/AutoMatch/LLVM.hs +++ b/src/SAWScript/AutoMatch/LLVM.hs @@ -11,7 +11,7 @@ import qualified Data.AIG as AIG import Text.LLVM import Verifier.SAW.SharedTerm -import SAWScript.Crucible.LLVM.MethodSpecIR (LLVMModule(..)) +import SAWScript.Crucible.LLVM.MethodSpecIR (LLVMModule, modAST, modFilePath) --import Data.Maybe import Data.Either @@ -31,17 +31,17 @@ getDeclsLLVM :: SharedContext -> LLVMModule arch -> IO (Interaction (Maybe [Decl])) -getDeclsLLVM _proxy _sc (LLVMModule file mdl _) = do +getDeclsLLVM _proxy _sc lm = do let symStr (Symbol s) = s return $ do let (untranslateable, translations) = - partitionEithers . for (modDefines mdl) $ \def -> + partitionEithers . for (modDefines (modAST lm)) $ \def -> maybe (Left (symStr (defName def))) Right $ symDefineToDecl def when (not . null $ untranslateable) $ do separator ThinSep - liftF . flip Warning () $ "No translation for the following signatures in " ++ file ++ ":" + liftF . flip Warning () $ "No translation for the following signatures in " ++ modFilePath lm ++ ":" bulleted $ map (("'" ++) . (++ "'")) untranslateable return $ Just translations diff --git a/src/SAWScript/Crucible/LLVM/Boilerplate.hs b/src/SAWScript/Crucible/LLVM/Boilerplate.hs index ff603ade14..169e049c24 100644 --- a/src/SAWScript/Crucible/LLVM/Boilerplate.hs +++ b/src/SAWScript/Crucible/LLVM/Boilerplate.hs @@ -400,13 +400,13 @@ bpFunToSpec (BPFun name setup ret as ls deps) = do llvm_boilerplate_info :: Some LLVMModule -> [Profile] -> TopLevel () llvm_boilerplate_info m profs = liftIO $ - (try . mapM (mapM typeToBPType) $ extractDefines (viewSome _modAST m) profs) >>= + (try . mapM (mapM typeToBPType) $ extractDefines (viewSome modAST m) profs) >>= \case Left (BPException e) -> liftIO . Text.IO.hPutStrLn stderr $ "[error] " <> e Right funs -> liftIO . Text.IO.putStrLn . Text.pack $ show funs llvm_boilerplate :: FilePath -> Some LLVMModule -> [Profile] -> TopLevel () llvm_boilerplate path m profs = liftIO $ - (try . mapM (mapM typeToBPType) $ extractDefines (viewSome _modAST m) profs) >>= + (try . mapM (mapM typeToBPType) $ extractDefines (viewSome modAST m) profs) >>= \case Left (BPException e) -> liftIO . Text.IO.hPutStrLn stderr $ "[error] " <> e Right funs -> liftIO . withFile path WriteMode $ \h -> do binds <- mconcat <$> mapM globalBinds globals @@ -418,7 +418,7 @@ llvm_boilerplate path m profs = liftIO $ mapM bpFunToSpec funs >>= Text.IO.hPutStrLn h . mconcat where globals :: [((LLVM.Type, Text, Bool), Text)] - globals = zip (extractGlobals $ viewSome _modAST m) $ globalName <$> [0, 1..] + globals = zip (extractGlobals $ viewSome modAST m) $ globalName <$> [0, 1..] where globalName :: Int -> Text globalName i = "global" <> Text.pack (show i) globalBinds :: MonadThrow m => ((LLVM.Type, Text, Bool), Text) -> m Text diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index 478b574f0b..e6f5ee0d2d 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -294,10 +294,11 @@ createMethodSpec :: String {- ^ Name of the function -} -> LLVMCrucibleSetupM () {- ^ Boundary specification -} -> TopLevel (MS.CrucibleMethodSpecIR (LLVM arch)) -createMethodSpec verificationArgs asp bic opts lm@(LLVMModule _ _ mtrans) nm setup = do +createMethodSpec verificationArgs asp bic opts lm nm setup = do (nm', parent) <- resolveSpecName nm - let edef = findDefMaybeStatic (lm ^. modAST) nm' - let edecl = findDecl (lm ^. modAST) nm' + let edef = findDefMaybeStatic (modAST lm) nm' + let edecl = findDecl (modAST lm) nm' + let mtrans = modTrans lm defOrDecls <- case (edef, edecl) of (Right defs, _) -> return (NE.map Left defs) (_, Right decl) -> return (Right decl NE.:| []) @@ -343,7 +344,7 @@ createMethodSpec verificationArgs asp bic opts lm@(LLVMModule _ _ mtrans) nm set -- set up the LLVM memory with a pristine heap let globals = cc^.ccLLVMGlobals - let mvar = Crucible.llvmMemVar (cc^.ccLLVMContext) + let mvar = Crucible.llvmMemVar (ccLLVMContext cc) mem0 <- case Crucible.lookupGlobal mvar globals of Nothing -> fail "internal error: LLVM Memory global not found" Just mem0 -> return mem0 @@ -354,7 +355,7 @@ createMethodSpec verificationArgs asp bic opts lm@(LLVMModule _ _ mtrans) nm set (Crucible.memImplHeap mem0) } else mem0 - let globals1 = Crucible.llvmGlobals (cc^.ccLLVMContext) mem + let globals1 = Crucible.llvmGlobals (ccLLVMContext cc) mem -- construct the initial state for verifications (args, assumes, env, globals2) <- @@ -479,12 +480,12 @@ verifyPrestate :: Map AllocIndex (LLVMPtr (Crucible.ArchWidth arch)), Crucible.SymGlobalState Sym) verifyPrestate opts cc mspec globals = do - let ?lc = cc^.ccTypeCtx + let ?lc = ccTypeCtx cc let sym = cc^.ccBackend let prestateLoc = W4.mkProgramLoc "_SAW_verify_prestate" W4.InternalPos liftIO $ W4.setCurrentProgramLoc sym prestateLoc - let lvar = Crucible.llvmMemVar (cc^.ccLLVMContext) + let lvar = Crucible.llvmMemVar (ccLLVMContext cc) let Just mem = Crucible.lookupGlobal lvar globals -- Allocate LLVM memory for each 'crucible_alloc' @@ -570,7 +571,7 @@ setupGlobalAllocs cc allocs mem0 = foldM go mem0 allocs go :: MemImpl -> MS.AllocGlobal (LLVM arch) -> IO MemImpl go mem (LLVMAllocGlobal _ symbol@(L.Symbol name)) = do - let LLVMModule _ _ mtrans = cc ^. ccLLVMModule + let mtrans = ccLLVMModuleTrans cc gimap = Crucible.globalInitMap mtrans case Map.lookup symbol gimap of Just (g, Right (mt, _)) -> do @@ -700,7 +701,7 @@ ppGlobalPair :: LLVMCrucibleContext arch -> Crucible.GlobalPair Sym a -> Doc ppGlobalPair cc gp = - let mvar = Crucible.llvmMemVar (cc^.ccLLVMContext) + let mvar = Crucible.llvmMemVar (ccLLVMContext cc) globals = gp ^. Crucible.gpGlobals in case Crucible.lookupGlobal mvar globals of Nothing -> text "LLVM Memory global variable not initialized" @@ -722,7 +723,7 @@ registerOverride opts cc _ctx top_loc cs = do sc <- CrucibleSAW.saw_ctx <$> liftIO (readIORef (W4.sbStateManager sym)) let fstr = (head cs)^.csName fsym = L.Symbol fstr - llvmctx = cc^.ccLLVMContext + llvmctx = ccLLVMContext cc matches (Crucible.LLVMHandleInfo _ h) = matchingStatics (L.Symbol (Text.unpack (W4.functionName (Crucible.handleName h)))) fsym liftIO $ @@ -787,7 +788,7 @@ withCfg -> IO a withCfg context name k = do let function_id = L.Symbol name - case Map.lookup function_id (Crucible.cfgMap (context^.ccLLVMModuleTrans)) of + case Map.lookup function_id (Crucible.cfgMap (ccLLVMModuleTrans context)) of Just (Crucible.AnyCFG cfg) -> k cfg Nothing -> fail $ "Unexpected function name: " ++ name @@ -864,7 +865,7 @@ verifySimulate opts cc pfs mspec args assumes top_loc lemmas globals checkSat as (registerInvariantOverride opts cc top_loc (HashMap.fromList breakpoints)) (groupOn (view csName) invLemmas) - additionalFeatures <- mapM (Crucible.arraySizeProfile (cc ^. ccLLVMContext)) + additionalFeatures <- mapM (Crucible.arraySizeProfile (ccLLVMContext cc)) $ maybeToList asp let execFeatures = invariantExecFeatures ++ @@ -989,8 +990,10 @@ setupLLVMCrucibleContext :: ((?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => LLVMCrucibleContext arch -> TopLevel a) -> TopLevel a -setupLLVMCrucibleContext bic opts lm@(LLVMModule _ llvm_mod mtrans) action = do +setupLLVMCrucibleContext bic opts lm action = do halloc <- getHandleAlloc + let llvm_mod = modAST lm + let mtrans = modTrans lm let ctx = mtrans^.Crucible.transContext smt_array_memory_model_enabled <- gets rwSMTArrayMemoryModel Crucible.llvmPtrWidth ctx $ \wptr -> Crucible.withPtrWidth wptr $ @@ -1160,9 +1163,9 @@ crucible_llvm_extract :: String -> TopLevel TypedTerm crucible_llvm_extract bic opts (Some lm) fn_name = do - let ctx = lm ^. modTrans . Crucible.transContext + let ctx = modTrans lm ^. Crucible.transContext let ?lc = ctx^.Crucible.llvmTypeCtx - let edef = findDefMaybeStatic (lm ^. modAST) fn_name + let edef = findDefMaybeStatic (modAST lm) fn_name case edef of Right defs -> do let defTypes = fold $ @@ -1174,7 +1177,7 @@ crucible_llvm_extract bic opts (Some lm) fn_name = do fail "Type aliases are not supported by `crucible_llvm_extract`." Left err -> fail (displayVerifExceptionOpts opts err) setupLLVMCrucibleContext bic opts lm $ \cc -> - case Map.lookup (fromString fn_name) (Crucible.cfgMap (cc^.ccLLVMModuleTrans)) of + case Map.lookup (fromString fn_name) (Crucible.cfgMap (ccLLVMModuleTrans cc)) of Nothing -> fail $ unwords ["function", fn_name, "not found"] Just cfg -> io $ extractFromLLVMCFG opts (biSharedContext bic) cc cfg @@ -1185,10 +1188,10 @@ crucible_llvm_cfg :: String -> TopLevel SAW_CFG crucible_llvm_cfg bic opts (Some lm) fn_name = do - let ctx = lm ^. modTrans . Crucible.transContext + let ctx = modTrans lm ^. Crucible.transContext let ?lc = ctx^.Crucible.llvmTypeCtx setupLLVMCrucibleContext bic opts lm $ \cc -> - case Map.lookup (fromString fn_name) (Crucible.cfgMap (cc^.ccLLVMModuleTrans)) of + case Map.lookup (fromString fn_name) (Crucible.cfgMap (ccLLVMModuleTrans cc)) of Nothing -> fail $ unwords ["function", fn_name, "not found"] Just cfg -> return (LLVM_CFG cfg) @@ -1332,10 +1335,10 @@ crucible_fresh_var :: crucible_fresh_var bic _opts name lty = LLVMCrucibleSetupM $ do cctx <- getLLVMCrucibleContext - let ?lc = cctx ^. ccTypeCtx + let ?lc = ccTypeCtx cctx lty' <- memTypeForLLVMType bic lty let sc = biSharedContext bic - let dl = Crucible.llvmDataLayout (cctx^.ccTypeCtx) + let dl = Crucible.llvmDataLayout (ccTypeCtx cctx) case cryptolTypeOfActual dl lty' of Nothing -> fail $ "Unsupported type in crucible_fresh_var: " ++ show (L.ppType lty) Just cty -> Setup.freshVariable sc name cty @@ -1354,7 +1357,7 @@ crucible_fresh_expanded_val :: crucible_fresh_expanded_val bic _opts lty = LLVMCrucibleSetupM $ do let sc = biSharedContext bic cctx <- getLLVMCrucibleContext - let ?lc = cctx ^. ccTypeCtx + let ?lc = ccTypeCtx cctx lty' <- memTypeForLLVMType bic lty loc <- getW4Position "crucible_fresh_expanded_val" constructExpandedSetupValue cctx sc loc lty' @@ -1436,7 +1439,7 @@ crucible_alloc_internal :: CrucibleSetup (Crucible.LLVM arch) (AllLLVM SetupValue) crucible_alloc_internal _bic _opt lty spec = do cctx <- getLLVMCrucibleContext - let ?lc = cctx ^. ccTypeCtx + let ?lc = ccTypeCtx cctx let ?dl = Crucible.llvmDataLayout ?lc n <- Setup.csVarCounter <<%= nextAllocIndex Setup.currentState . MS.csAllocs . at n ?= spec @@ -1459,7 +1462,7 @@ crucible_alloc_with_mutability_and_size mut sz bic opts lty = LLVMCrucibleSetupM memTy <- memTypeForLLVMType bic lty let memTySize = - let ?lc = cctx ^. ccTypeCtx + let ?lc = ccTypeCtx cctx ?dl = Crucible.llvmDataLayout ?lc in Crucible.memTypeSize ?dl memTy @@ -1537,7 +1540,7 @@ constructFreshPointer :: CrucibleSetup (LLVM arch) (AllLLVM SetupValue) constructFreshPointer mid loc memTy = do cctx <- getLLVMCrucibleContext - let ?lc = cctx ^. ccTypeCtx + let ?lc = ccTypeCtx cctx let ?dl = Crucible.llvmDataLayout ?lc n <- Setup.csVarCounter <<%= nextAllocIndex let sz = Crucible.memTypeSize ?dl memTy @@ -1564,8 +1567,8 @@ crucible_points_to typed _bic _opt (getAllLLVM -> ptr) (getAllLLVM -> val) = LLVMCrucibleSetupM $ do cc <- getLLVMCrucibleContext loc <- getW4Position "crucible_points_to" - Crucible.llvmPtrWidth (cc^.ccLLVMContext) $ \wptr -> Crucible.withPtrWidth wptr $ - do let ?lc = cc^.ccTypeCtx + Crucible.llvmPtrWidth (ccLLVMContext cc) $ \wptr -> Crucible.withPtrWidth wptr $ + do let ?lc = ccTypeCtx cc st <- get let rs = st ^. Setup.csResolvedState if st ^. Setup.csPrePost == PreState && MS.testResolved ptr [] rs diff --git a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs index e9eb7c59cc..d5619558c0 100644 --- a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs +++ b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs @@ -29,19 +29,88 @@ Stability : provisional {-# LANGUAGE ViewPatterns #-} {-# OPTIONS_GHC -fno-warn-orphans #-} -module SAWScript.Crucible.LLVM.MethodSpecIR where +module SAWScript.Crucible.LLVM.MethodSpecIR + ( -- * LLVMMethodId + LLVMMethodId(..) + , llvmMethodParent + , llvmMethodName + , csName + , csParentName + -- * LLVMAllocSpec + , LLVMAllocSpec(..) + , allocSpecType + , allocSpecMut + , allocSpecLoc + , allocSpecBytes + , mutIso + , isMut + -- * LLVMModule + , LLVMModule -- abstract + , modFilePath + , modAST + , modTrans + , loadLLVMModule + , showLLVMModule + -- * CrucibleContext + , LLVMCrucibleContext(..) + , ccLLVMSimContext + , ccLLVMModule + , ccLLVMGlobals + , ccBasicSS + , ccBackend + , ccLLVMModuleAST + , ccLLVMModuleTrans + , ccLLVMContext + , ccTypeCtx + -- * PointsTo + , LLVMPointsTo(..) + , ppPointsTo + -- * AllocGlobal + , LLVMAllocGlobal(..) + , ppAllocGlobal + -- * Intrinsics + , intrinsics + -- * Initial CrucibleSetupMethodSpec + , SetupError(..) + , ppSetupError + , resolveArgs + , resolveRetTy + , initialDefCrucibleMethodSpecIR + , initialDeclCrucibleMethodSpecIR + , initialCrucibleSetupState + , initialCrucibleSetupStateDecl + -- * AllLLVM + , AllLLVM + , mkAllLLVM + , getAllLLVM + , anySetupTerm + , anySetupArray + , anySetupStruct + , anySetupElem + , anySetupField + , anySetupNull + , anySetupGlobal + , anySetupGlobalInitializer + -- * SomeLLVM + , SomeLLVM + , pattern SomeLLVM + , mkSomeLLVM + , getSomeLLVM + ) where import Control.Lens import Control.Monad (when) import Data.Functor.Compose (Compose(..)) import Data.IORef import Data.Monoid ((<>)) -import Data.Type.Equality (TestEquality(..), (:~:)(Refl)) +import Data.Type.Equality (TestEquality(..)) import qualified Text.LLVM.AST as L import qualified Text.LLVM.PP as L import qualified Text.PrettyPrint.ANSI.Leijen as PPL hiding ((<$>), (<>)) import qualified Text.PrettyPrint.HughesPJ as PP +import qualified Data.LLVM.BitCode as LLVM + import qualified Cryptol.Utils.PP as Cryptol (pp) import Data.Parameterized.All (All(All)) @@ -53,6 +122,7 @@ import What4.ProgramLoc (ProgramLoc) import qualified Lang.Crucible.Backend.SAWCore as Crucible (SAWCoreBackend, saw_ctx, toSC, SAWCruciblePersonality) +import qualified Lang.Crucible.FunctionHandle as Crucible (HandleAllocator) import qualified Lang.Crucible.Simulator.ExecutionTree as Crucible (SimContext) import qualified Lang.Crucible.Simulator.GlobalState as Crucible (SymGlobalState) import qualified Lang.Crucible.Types as Crucible (SymbolRepr, knownSymbol) @@ -138,23 +208,54 @@ isMut = allocSpecMut . mutIso -------------------------------------------------------------------------------- -- *** LLVMModule +-- | An 'LLVMModule' contains an LLVM module that has been parsed from +-- a bitcode file and translated to Crucible. data LLVMModule arch = LLVMModule - { _modName :: String + { _modFilePath :: FilePath , _modAST :: L.Module , _modTrans :: CL.ModuleTranslation arch } - -makeLenses ''LLVMModule +-- NOTE: Type 'LLVMModule' is exported as an abstract type, and we +-- maintain the invariant that the 'FilePath', 'Module', and +-- 'ModuleTranslation' fields are all consistent with each other; +-- 'loadLLVMModule' is the only function that is allowed to create +-- values of type 'LLVMModule'. + +-- | The file path that the LLVM module was loaded from. +modFilePath :: LLVMModule arch -> FilePath +modFilePath = _modFilePath + +-- | The parsed AST of the LLVM module. +modAST :: LLVMModule arch -> L.Module +modAST = _modAST + +-- | The Crucible translation of an LLVM module. +modTrans :: LLVMModule arch -> CL.ModuleTranslation arch +modTrans = _modTrans + +-- | Load an LLVM module from the given bitcode file, then parse and +-- translate to Crucible. +loadLLVMModule :: + (?laxArith :: Bool) => + FilePath -> + Crucible.HandleAllocator -> + IO (Either LLVM.Error (Some LLVMModule)) +loadLLVMModule file halloc = + do parseResult <- LLVM.parseBitCodeFromFile file + case parseResult of + Left err -> return (Left err) + Right llvm_mod -> + do Some mtrans <- CL.translateModule halloc llvm_mod + return (Right (Some (LLVMModule file llvm_mod mtrans))) instance TestEquality LLVMModule where - testEquality (LLVMModule nm1 lm1 mt1) (LLVMModule nm2 lm2 mt2) = - case testEquality mt1 mt2 of - Nothing -> Nothing - r@(Just Refl) -> - if nm1 == nm2 && lm1 == lm2 - then r - else Nothing + -- As 'LLVMModule' is an abstract type, we know that the values must + -- have been created by a call to 'loadLLVMModule'. Furthermore each + -- call to 'translateModule' generates a 'ModuleTranslation' that + -- contains a fresh nonce; thus comparison of the 'modTrans' fields + -- is sufficient to guarantee equality of two 'LLVMModule' values. + testEquality m1 m2 = testEquality (modTrans m1) (modTrans m2) type instance MS.Codebase (CL.LLVM arch) = LLVMModule arch @@ -217,17 +318,17 @@ data LLVMCrucibleContext arch = makeLenses ''LLVMCrucibleContext -ccLLVMModuleAST :: Simple Lens (LLVMCrucibleContext arch) L.Module -ccLLVMModuleAST = ccLLVMModule . modAST +ccLLVMModuleAST :: LLVMCrucibleContext arch -> L.Module +ccLLVMModuleAST = modAST . _ccLLVMModule -ccLLVMModuleTrans :: Simple Lens (LLVMCrucibleContext arch) (CL.ModuleTranslation arch) -ccLLVMModuleTrans = ccLLVMModule . modTrans +ccLLVMModuleTrans :: LLVMCrucibleContext arch -> CL.ModuleTranslation arch +ccLLVMModuleTrans = modTrans . _ccLLVMModule -ccLLVMContext :: Simple Lens (LLVMCrucibleContext arch) (CL.LLVMContext arch) -ccLLVMContext = ccLLVMModuleTrans . CL.transContext +ccLLVMContext :: LLVMCrucibleContext arch -> CL.LLVMContext arch +ccLLVMContext = view CL.transContext . ccLLVMModuleTrans -ccTypeCtx :: Simple Lens (LLVMCrucibleContext arch) CL.TypeContext -ccTypeCtx = ccLLVMContext . CL.llvmTypeCtx +ccTypeCtx :: LLVMCrucibleContext arch -> CL.TypeContext +ccTypeCtx = view CL.llvmTypeCtx . ccLLVMContext -------------------------------------------------------------------------------- -- ** PointsTo diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs index 7d8e2c0fa5..08f8deba12 100644 --- a/src/SAWScript/Crucible/LLVM/Override.hs +++ b/src/SAWScript/Crucible/LLVM/Override.hs @@ -141,7 +141,7 @@ ppLLVMVal :: OverrideMatcher (LLVM arch) w PP.Doc ppLLVMVal cc val = do sym <- Ov.getSymInterface - mem <- readGlobal (Crucible.llvmMemVar (cc^.ccLLVMContext)) + mem <- readGlobal (Crucible.llvmMemVar (ccLLVMContext cc)) liftIO $ Crucible.ppLLVMValWithGlobals sym (Crucible.memImplGlobalMap mem) val -- | Resolve a 'SetupValue' into a 'LLVMVal' and pretty-print it @@ -322,7 +322,7 @@ ppArgs sym cc cs (Crucible.RegMap args) = do do storTy <- Crucible.toStorableType memTy llvmval <- Crucible.packMemValue sym storTy tyrep val return (llvmval, memTy) - case Crucible.lookupGlobal (Crucible.llvmMemVar (cc^.ccLLVMContext)) (cc^.ccLLVMGlobals) of + case Crucible.lookupGlobal (Crucible.llvmMemVar (ccLLVMContext cc)) (cc^.ccLLVMGlobals) of Nothing -> fail "Internal error: Couldn't find LLVM memory variable" Just mem -> do traverse (Crucible.ppLLVMValWithGlobals sym (Crucible.memImplGlobalMap mem) . fst) =<< @@ -886,7 +886,7 @@ matchArg :: OverrideMatcher (LLVM arch) md () matchArg opts sc cc cs prepost actual expectedTy expected = do - let mvar = Crucible.llvmMemVar $ cc ^. ccLLVMContext + let mvar = Crucible.llvmMemVar (ccLLVMContext cc) mem <- case Crucible.lookupGlobal mvar $ cc ^. ccLLVMGlobals of Nothing -> fail "internal error: LLVM Memory global not found" Just mem -> pure mem @@ -1132,12 +1132,12 @@ learnPointsTo opts sc cc spec prepost (LLVMPointsTo loc ptr val) = sym <- Ov.getSymInterface mem <- readGlobal $ Crucible.llvmMemVar - $ (cc^.ccLLVMContext) + $ ccLLVMContext cc let alignment = Crucible.noAlignment -- default to byte alignment (FIXME) res <- liftIO $ Crucible.loadRaw sym mem ptr1 storTy alignment let summarizeBadLoad = - let dataLayout = Crucible.llvmDataLayout (cc^.ccTypeCtx) + let dataLayout = Crucible.llvmDataLayout (ccTypeCtx cc) sz = Crucible.memTypeSize dataLayout memTy in map (PP.text . unwords) [ [ "When reading through pointer:", show (Crucible.ppPtr ptr1) ] @@ -1236,7 +1236,7 @@ invalidateMutableAllocs :: OverrideMatcher (LLVM arch) RW () invalidateMutableAllocs opts sc cc cs = do sym <- use syminterface - mem <- readGlobal . Crucible.llvmMemVar $ cc ^. ccLLVMContext + mem <- readGlobal . Crucible.llvmMemVar $ ccLLVMContext cc sub <- use setupValueSub let mutableAllocs = Map.filter (view isMut) $ cs ^. MS.csPreState . MS.csAllocs @@ -1251,7 +1251,7 @@ invalidateMutableAllocs opts sc cc cs = do ] ) ) <$> Map.elems (Map.intersectionWith (,) sub mutableAllocs) - LLVMModule _ _ mtrans = cc ^. ccLLVMModule + mtrans = ccLLVMModuleTrans cc gimap = Crucible.globalInitMap mtrans mutableGlobals = cs ^. MS.csGlobalAllocs @@ -1294,7 +1294,7 @@ invalidateMutableAllocs opts sc cc cs = do =<< W4.bvLit sym ?ptrWidth (Crucible.bytesToInteger sz) ) mem danglingPtrs - writeGlobal (Crucible.llvmMemVar $ cc ^. ccLLVMContext) mem' + writeGlobal (Crucible.llvmMemVar $ ccLLVMContext cc) mem' ------------------------------------------------------------------------ @@ -1314,7 +1314,7 @@ executeAllocation opts cc (var, LLVMAllocSpec mut memTy sz loc) = Nothing -> fail "executAllocation: failed to resolve type" -} liftIO $ printOutLn opts Debug $ unwords ["executeAllocation:", show var, show memTy] - let memVar = Crucible.llvmMemVar $ (cc^.ccLLVMContext) + let memVar = Crucible.llvmMemVar (ccLLVMContext cc) mem <- readGlobal memVar sz' <- liftIO $ W4.bvLit sym Crucible.PtrWidth (Crucible.bytesToInteger sz) let alignment = Crucible.noAlignment -- default to byte alignment (FIXME) @@ -1371,7 +1371,7 @@ executePointsTo :: OverrideMatcher (LLVM arch) RW () executePointsTo opts sc cc spec (LLVMPointsTo _loc ptr val) = do (_, ptr') <- resolveSetupValue opts cc sc spec Crucible.PtrRepr ptr - let memVar = Crucible.llvmMemVar $ (cc^.ccLLVMContext) + let memVar = Crucible.llvmMemVar (ccLLVMContext cc) mem <- readGlobal memVar -- In case the types are different (from crucible_points_to_untyped) @@ -1513,7 +1513,7 @@ resolveSetupValueLLVM :: resolveSetupValueLLVM opts cc sc spec sval = do m <- OM (use setupValueSub) s <- OM (use termSub) - mem <- readGlobal (Crucible.llvmMemVar (cc^.ccLLVMContext)) + mem <- readGlobal (Crucible.llvmMemVar (ccLLVMContext cc)) let tyenv = MS.csAllocations spec nameEnv = MS.csTypeNames spec memTy <- liftIO $ typeOfSetupValue cc tyenv nameEnv sval diff --git a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs index df154a8cf6..8eff7d646d 100644 --- a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs @@ -27,7 +27,6 @@ module SAWScript.Crucible.LLVM.ResolveSetupValue import Control.Lens import Control.Monad -import qualified Control.Monad.Fail as Fail import Control.Monad.Fail (MonadFail) import Control.Monad.State import Data.Foldable (toList) @@ -91,7 +90,7 @@ resolveSetupValueInfo cc env nameEnv v = -- SetupGlobal g -> SetupVar i | Just alias <- Map.lookup i nameEnv - , let mdMap = Crucible.llvmMetadataMap (cc^.ccTypeCtx) + , let mdMap = Crucible.llvmMetadataMap (ccTypeCtx cc) -> L.Pointer (guessAliasInfo mdMap alias) SetupField () a n -> fromMaybe L.Unknown $ @@ -123,7 +122,7 @@ resolveSetupFieldIndex cc env nameEnv v n = _ -> Nothing where - lc = cc^.ccTypeCtx + lc = ccTypeCtx cc resolveSetupFieldIndexOrFail :: MonadFail m => @@ -156,7 +155,7 @@ typeOfSetupValue :: SetupValue (Crucible.LLVM arch) -> m Crucible.MemType typeOfSetupValue cc env nameEnv val = - do let ?lc = cc^.ccTypeCtx + do let ?lc = ccTypeCtx cc typeOfSetupValue' cc env nameEnv val typeOfSetupValue' :: forall m arch. @@ -226,7 +225,7 @@ typeOfSetupValue' cc env nameEnv val = return (Crucible.PtrType Crucible.VoidType) -- A global and its initializer have the same type. SetupGlobal () name -> do - let m = cc ^. ccLLVMModuleAST + let m = ccLLVMModuleAST cc tys = [ (L.globalSym g, L.globalType g) | g <- L.modGlobals m ] ++ [ (L.decName d, L.decFunType d) | d <- L.modDeclares m ] ++ [ (L.defName d, L.defFunType d) | d <- L.modDefines m ] @@ -240,7 +239,7 @@ typeOfSetupValue' cc env nameEnv val = ] Right symTy -> return (Crucible.PtrType symTy) SetupGlobalInitializer () name -> do - case Map.lookup (L.Symbol name) (Crucible.globalInitMap $ cc^.ccLLVMModuleTrans) of + case Map.lookup (L.Symbol name) (Crucible.globalInitMap $ ccLLVMModuleTrans cc) of Just (g, _) -> case let ?lc = lc in Crucible.liftMemType (L.globalType g) of Left err -> fail $ unlines [ "typeOfSetupValue: invalid type " ++ show (L.globalType g) @@ -250,7 +249,7 @@ typeOfSetupValue' cc env nameEnv val = Right memTy -> return memTy Nothing -> fail $ "resolveSetupVal: global not found: " ++ name where - lc = cc^.ccTypeCtx + lc = ccTypeCtx cc dl = Crucible.llvmDataLayout lc -- | Translate a SetupValue into a Crucible LLVM value, resolving @@ -316,7 +315,7 @@ resolveSetupVal cc mem env tyenv nameEnv val = do Crucible.ptrToPtrVal <$> Crucible.doResolveGlobal sym mem (L.Symbol name) SetupGlobalInitializer () name -> case Map.lookup (L.Symbol name) - (Crucible.globalInitMap $ cc^.ccLLVMModuleTrans) of + (Crucible.globalInitMap $ ccLLVMModuleTrans cc) of -- There was an error in global -> constant translation Just (_, Left e) -> fail e Just (_, Right (_, Just v)) -> @@ -328,7 +327,7 @@ resolveSetupVal cc mem env tyenv nameEnv val = do fail $ "resolveSetupVal: global not found: " ++ name where sym = cc^.ccBackend - lc = cc^.ccTypeCtx + lc = ccTypeCtx cc dl = Crucible.llvmDataLayout lc resolveTypedTerm :: @@ -415,7 +414,7 @@ resolveSAWTerm cc tp tm = fail "resolveSAWTerm: invalid function type" where sym = cc^.ccBackend - dl = Crucible.llvmDataLayout (cc^.ccTypeCtx) + dl = Crucible.llvmDataLayout (ccTypeCtx cc) data ToLLVMTypeErr = NotYetSupported String | Impossible String @@ -551,7 +550,7 @@ memArrayToSawCoreTerm :: IO Term memArrayToSawCoreTerm crucible_context endianess typed_term = do let sym = crucible_context ^. ccBackend - let data_layout = Crucible.llvmDataLayout $ crucible_context ^. ccTypeCtx + let data_layout = Crucible.llvmDataLayout $ ccTypeCtx crucible_context saw_context <- Crucible.saw_ctx <$> readIORef (W4.sbStateManager sym) let setBytes :: Cryptol.TValue -> Term -> Crucible.Bytes -> StateT (Vector Term) IO () diff --git a/src/SAWScript/LLVMBuiltins.hs b/src/SAWScript/LLVMBuiltins.hs index de662be352..3db73336db 100644 --- a/src/SAWScript/LLVMBuiltins.hs +++ b/src/SAWScript/LLVMBuiltins.hs @@ -32,19 +32,16 @@ import qualified Text.LLVM.Parser as LLVM (parseType) import SAWScript.Value as SV -import qualified SAWScript.Crucible.LLVM.CrucibleLLVM as Crucible (translateModule) -import qualified SAWScript.Crucible.LLVM.MethodSpecIR as CMS (LLVMModule(..)) +import qualified SAWScript.Crucible.LLVM.MethodSpecIR as CMS (LLVMModule, loadLLVMModule) llvm_load_module :: FilePath -> TopLevel (Some CMS.LLVMModule) -llvm_load_module file = do - laxArith <- gets rwLaxArith - let ?laxArith = laxArith - io (LLVM.parseBitCodeFromFile file) >>= \case - Left err -> fail (LLVM.formatError err) - Right llvm_mod -> do - halloc <- getHandleAlloc - Some mtrans <- io $ Crucible.translateModule halloc llvm_mod - return (Some (CMS.LLVMModule file llvm_mod mtrans)) +llvm_load_module file = + do laxArith <- gets rwLaxArith + let ?laxArith = laxArith + halloc <- getHandleAlloc + io (CMS.loadLLVMModule file halloc) >>= \case + Left err -> fail (LLVM.formatError err) + Right llvm_mod -> return llvm_mod llvm_type :: String -> TopLevel LLVM.Type llvm_type str =