From 18fa1ecd412017d61bc2206b03f245cd5aed1149 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Thu, 9 Jan 2020 15:45:07 -0800 Subject: [PATCH 1/3] Use invariant for datatype `LLVMModule` to permit fast equality test. The invariant is that the `LLVMModule` value should have been created by the `loadLLVMModule` function, so that all of the components (the file path, the parsed AST, and the translated Crucible CFG) all agree. Also replace the lenses for the field components with ordinary projection functions, as we should never want to modify any of the record fields of an `LLVMModule`, only read them. --- src/SAWScript/Crucible/LLVM/Builtins.hs | 46 ++++++------- src/SAWScript/Crucible/LLVM/MethodSpecIR.hs | 65 ++++++++++++++----- src/SAWScript/Crucible/LLVM/Override.hs | 20 +++--- .../Crucible/LLVM/ResolveSetupValue.hs | 21 +++--- src/SAWScript/LLVMBuiltins.hs | 19 +++--- 5 files changed, 98 insertions(+), 73 deletions(-) diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index 478b574f0b..517f7c112e 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -296,8 +296,8 @@ createMethodSpec :: TopLevel (MS.CrucibleMethodSpecIR (LLVM arch)) createMethodSpec verificationArgs asp bic opts lm@(LLVMModule _ _ mtrans) 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' defOrDecls <- case (edef, edecl) of (Right defs, _) -> return (NE.map Left defs) (_, Right decl) -> return (Right decl NE.:| []) @@ -343,7 +343,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 +354,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 +479,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' @@ -700,7 +700,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 +722,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 +787,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 +864,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 ++ @@ -1160,9 +1160,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 +1174,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 +1185,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 +1332,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 +1354,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 +1436,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 +1459,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 +1537,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 +1564,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..ddd44178fc 100644 --- a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs +++ b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs @@ -36,12 +36,14 @@ 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 +55,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 +141,49 @@ 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 +-- | 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 +246,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..e628f6ba9a 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 @@ -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 = From 0143d98be07318aed77ccdc59022cd7c510930fd Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Thu, 9 Jan 2020 16:04:42 -0800 Subject: [PATCH 2/3] Use export list to make `LLVMModule` into a proper abstract datatype. Also rewrite some other functions to use accessor functions instead of pattern matching on `LLVMModule` constructor, which is no longer exported. --- src/SAWScript/AutoMatch/LLVM.hs | 8 +-- src/SAWScript/Crucible/LLVM/Boilerplate.hs | 6 +- src/SAWScript/Crucible/LLVM/Builtins.hs | 9 ++- src/SAWScript/Crucible/LLVM/MethodSpecIR.hs | 69 ++++++++++++++++++++- src/SAWScript/Crucible/LLVM/Override.hs | 2 +- 5 files changed, 82 insertions(+), 12 deletions(-) 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 517f7c112e..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 (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.:| []) @@ -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 @@ -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 $ diff --git a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs index ddd44178fc..344bfc7c3d 100644 --- a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs +++ b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs @@ -29,7 +29,74 @@ 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) diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs index e628f6ba9a..08f8deba12 100644 --- a/src/SAWScript/Crucible/LLVM/Override.hs +++ b/src/SAWScript/Crucible/LLVM/Override.hs @@ -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 From 3abe2efd3dd076001799143890d64fca4bef5d67 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Fri, 10 Jan 2020 15:10:58 -0800 Subject: [PATCH 3/3] Add comment explaining LLVMModule datatype invariant. --- src/SAWScript/Crucible/LLVM/MethodSpecIR.hs | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs index 344bfc7c3d..d5619558c0 100644 --- a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs +++ b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs @@ -216,6 +216,11 @@ data LLVMModule arch = , _modAST :: L.Module , _modTrans :: CL.ModuleTranslation arch } +-- 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