Skip to content

Commit

Permalink
Merge pull request #623 from GaloisInc/issue622
Browse files Browse the repository at this point in the history 
Fast equality test for `LLVMModule`
  • Loading branch information
brianhuffman authored Jan 11, 2020
2 parents 74ddfaf + 3abe2ef commit faf2dee
Show file tree
Hide file tree
Showing 7 changed files with 186 additions and 86 deletions.
8 changes: 4 additions & 4 deletions src/SAWScript/AutoMatch/LLVM.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down
6 changes: 3 additions & 3 deletions src/SAWScript/Crucible/LLVM/Boilerplate.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down
55 changes: 29 additions & 26 deletions src/SAWScript/Crucible/LLVM/Builtins.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.:| [])
Expand Down Expand Up @@ -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
Expand All @@ -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) <-
Expand Down Expand Up @@ -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'
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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"
Expand All @@ -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 $
Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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 ++
Expand Down Expand Up @@ -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 $
Expand Down Expand Up @@ -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 $
Expand All @@ -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

Expand All @@ -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)

Expand Down Expand Up @@ -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
Expand All @@ -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'
Expand Down Expand Up @@ -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
Expand All @@ -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

Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down
Loading

0 comments on commit faf2dee

Please sign in to comment.