From 04a599bb6b55735abd8d78fa440ccdbebe29a225 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Wed, 1 Dec 2021 09:42:35 -0800 Subject: [PATCH] Heapster/exponential code explosion (#1528) NOTE: the heapster-tests tests succeeded last time through the CI, so I'm going to push this even though they haven't finished this time... * short-circut true `BVProp_Neq`s in the translation * fixed a bug in splitLLVMBlockPerm * small tweaks to the widening code to make the precise conditions of various cases more clear * added support for constant propagation through and, or, xor, and not of bitvectors * optimized implGetLLVMPermForOffset so that it only returns permissions that could actually be used to prove a permission at the given offset * changed the translation of LLVM globals so that each is translated to its own SAW core definition, rather than having the entire global be copied into each spec when it is used * removed no longer needed imports from SAWTranslation.hs * added the OpenTerm combinator completeNormOpenTerm to beta-normalize an OpenTerm after it is completed * changed the translation of TypedSetReg to let-bind its output expression translation, to avoid exponential code explosion * changed the translation of lambdas so that their bodies have let-bindings for repeated terms; added a type ascription term to the Coq AST; changed the translation of the unit type to give it an explicit ascription to sort Type rather than Set * added a dummy translation of BVUndef to the 0 bitvector value Co-authored-by: Matthew Yacavone --- .../src/Verifier/SAW/Heapster/Implication.hs | 21 ++++- .../Verifier/SAW/Heapster/LLVMGlobalConst.hs | 36 +++++--- .../src/Verifier/SAW/Heapster/Permissions.hs | 53 +++++++---- .../Verifier/SAW/Heapster/SAWTranslation.hs | 87 ++++++++++--------- .../Verifier/SAW/Heapster/TypedCrucible.hs | 20 ++++- .../src/Verifier/SAW/Heapster/Widening.hs | 14 ++- saw-core/src/Verifier/SAW/OpenTerm.hs | 6 +- src/SAWScript/HeapsterBuiltins.hs | 11 +-- 8 files changed, 160 insertions(+), 88 deletions(-) diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs index 60923bf632..0cfd435c9c 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs @@ -4757,6 +4757,25 @@ implElimAppendIthLLVMBlock _ _ _ = error "implElimAppendIthLLVMBlock: malformed inputs" +-- | Return the indices in a list of permissions for all of those that could be +-- used to prove a permission containing the specified offset. Field and block +-- permissions can only be used if they definitely (in the sense of +-- 'bvPropHolds') contain the offset, while the 'Bool' flag indicates whether +-- array permissions are allowed to only possibly contain (in the sense of +-- 'bvPropCouldHold') the offset. +permIndicesForProvingOffset :: (1 <= w, KnownNat w) => + [AtomicPerm (LLVMPointerType w)] -> Bool -> + PermExpr (BVType w) -> [Int] +permIndicesForProvingOffset ps imprecise_p off = + let ixs_holdss = flip findMaybeIndices ps $ \p -> + case llvmPermContainsOffset off p of + Just (_, True) -> Just True + Just _ | isLLVMArrayPerm p && imprecise_p -> Just False + _ -> Nothing in + case find (\(_,holds) -> holds) ixs_holdss of + Just (i,_) -> [i] + Nothing -> map fst ixs_holdss + -- | Assume @x:p@ is on top of the stack, where @p@ is a @memblock@ permission -- that contains the supplied offset @off@, and repeatedly eliminate this -- @memblock@ permission until @p@ has been converted to a non-@memblock@ @@ -4818,7 +4837,7 @@ implGetLLVMPermForOffset :: (AtomicPerm (LLVMPointerType w)) implGetLLVMPermForOffset x ps imprecise_p elim_blocks_p off mb_p = - case llvmPermIndicesForOffset ps imprecise_p off of + case permIndicesForProvingOffset ps imprecise_p off of -- If we didn't find any matches, try to unfold on the left [] -> implUnfoldOrFail x ps mb_p >>>= \_ -> diff --git a/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs b/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs index fcf6d75807..b5e431d2fd 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs @@ -29,6 +29,8 @@ import Lang.Crucible.LLVM.DataLayout import Lang.Crucible.LLVM.MemModel import Verifier.SAW.OpenTerm +import Verifier.SAW.Term.Functor (ModuleName) +import Verifier.SAW.SharedTerm import Verifier.SAW.Heapster.Permissions @@ -201,11 +203,11 @@ llvmZeroInitValue tp = traceAndZeroM ("llvmZeroInitValue cannot handle type:\n" ++ show (L.ppType tp)) --- | Add an LLVM global constant to a 'PermEnv', if the global has a type and --- value we can translate to Heapster, otherwise silently ignore it -permEnvAddGlobalConst :: (1 <= w, KnownNat w) => DebugLevel -> EndianForm -> - NatRepr w -> PermEnv -> L.Global -> PermEnv -permEnvAddGlobalConst dlevel endianness w env global = +-- | Top-level call to 'translateLLVMValue', running the 'LLVMTransM' monad +translateLLVMValueTop :: (1 <= w, KnownNat w) => DebugLevel -> EndianForm -> + NatRepr w -> PermEnv -> L.Global -> + Maybe (PermExpr (LLVMShapeType w), OpenTerm) +translateLLVMValueTop dlevel endianness w env global = let sym = show (L.globalSym global) in let trans_info = LLVMTransInfo { llvmTransInfoEnv = env, llvmTransInfoEndianness = endianness, @@ -213,13 +215,27 @@ permEnvAddGlobalConst dlevel endianness w env global = debugTrace dlevel ("Global: " ++ sym ++ "; value =\n" ++ maybe "None" ppLLVMValue (L.globalValue global)) $ - maybe env id $ (\x -> case x of Just _ -> debugTrace dlevel (sym ++ " translated") x Nothing -> debugTrace dlevel (sym ++ " not translated") x) $ flip runLLVMTransM trans_info $ do val <- lift $ L.globalValue global - (sh, t) <- translateLLVMValue w (L.globalType global) val - let p = ValPerm_LLVMBlock $ llvmReadBlockOfShape sh - return $ permEnvAddGlobalSyms env - [PermEnvGlobalEntry (GlobalSymbol $ L.globalSym global) p [t]] + translateLLVMValue w (L.globalType global) val + +-- | Add an LLVM global constant to a 'PermEnv', if the global has a type and +-- value we can translate to Heapster, otherwise silently ignore it +permEnvAddGlobalConst :: (1 <= w, KnownNat w) => SharedContext -> ModuleName -> + DebugLevel -> EndianForm -> NatRepr w -> PermEnv -> + L.Global -> IO PermEnv +permEnvAddGlobalConst sc mod_name dlevel endianness w env global = + case translateLLVMValueTop dlevel endianness w env global of + Nothing -> return env + Just (sh, t) -> + do let ident = mkSafeIdent mod_name $ show $ L.globalSym global + complete_t <- completeOpenTerm sc t + tp <- completeOpenTermType sc t + scInsertDef sc mod_name ident tp complete_t + let p = ValPerm_LLVMBlock $ llvmReadBlockOfShape sh + let t_ident = globalOpenTerm ident + return $ permEnvAddGlobalSyms env + [PermEnvGlobalEntry (GlobalSymbol $ L.globalSym global) p [t_ident]] diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs index 1653d4089f..c5af937ed5 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs @@ -29,7 +29,9 @@ module Verifier.SAW.Heapster.Permissions where import Prelude hiding (pred) -import Data.Char (isDigit) +import Numeric (showHex) +import Data.Char +import qualified Data.Text as Text import Data.Word import Data.Maybe import Data.Either @@ -80,7 +82,9 @@ import Lang.Crucible.LLVM.DataLayout import Lang.Crucible.LLVM.MemModel import Lang.Crucible.LLVM.Bytes import Lang.Crucible.CFG.Core -import Verifier.SAW.Term.Functor (Ident) +import Verifier.SAW.Term.Functor (ModuleName) +import Verifier.SAW.Module +import Verifier.SAW.SharedTerm hiding (Constant) import Verifier.SAW.OpenTerm import Verifier.SAW.Heapster.CruUtil @@ -193,6 +197,34 @@ nameSetFromFlags ns flags = data RecurseFlag = RecLeft | RecRight | RecNone deriving (Eq, Show, Read) +-- | Make a "coq-safe" identifier from a string that might contain +-- non-identifier characters, where we use the SAW core notion of identifier +-- characters as letters, digits, underscore and primes. Any disallowed +-- character is mapped to the string @__xNN@, where @NN@ is the hexadecimal code +-- for that character. Additionally, a SAW core identifier is not allowed to +-- start with a prime, so a leading underscore is added in such a case. +mkSafeIdent :: ModuleName -> String -> Ident +mkSafeIdent _ [] = fromString "_" +mkSafeIdent mnm nm = + let is_safe_char c = isAlphaNum c || c == '_' || c == '\'' in + mkIdent mnm $ Text.pack $ + (if nm!!0 == '\'' then ('_' :) else id) $ + concatMap + (\c -> if is_safe_char c then [c] else + "__x" ++ showHex (ord c) "") + nm + +-- | Insert a definition into a SAW core module +scInsertDef :: SharedContext -> ModuleName -> Ident -> Term -> Term -> IO () +scInsertDef sc mnm ident def_tp def_tm = + do t <- scConstant' sc (ModuleIdentifier ident) def_tm def_tp + scRegisterGlobal sc ident t + scModifyModule sc mnm $ \m -> + insDef m $ Def { defIdent = ident, + defQualifier = NoQualifier, + defType = def_tp, + defBody = Just def_tm } + ---------------------------------------------------------------------- -- * Pretty-printing @@ -3958,7 +3990,7 @@ splitLLVMBlockPerm off bp splitLLVMBlockPerm off bp@(llvmBlockShape -> PExpr_EmptyShape) = Just (bp { llvmBlockLen = bvSub off (llvmBlockOffset bp) }, bp { llvmBlockOffset = off, - llvmBlockLen = bvSub (llvmBlockLen bp) off }) + llvmBlockLen = bvSub (llvmBlockEndOffset bp) off }) splitLLVMBlockPerm off bp@(LLVMBlockPerm { llvmBlockShape = sh }) | Just sh_len <- llvmShapeLength sh , bvLt sh_len (bvSub off (llvmBlockOffset bp)) = @@ -4563,21 +4595,6 @@ llvmAtomicPermOverlapsRange rng (Perm_LLVMBlock bp) = bvRangesOverlap rng (llvmBlockRange bp) llvmAtomicPermOverlapsRange _ _ = False --- | Search through a list of permissions for either some permission that --- definitely contains (as in 'bvPropHolds') the given offset or, failing that, --- and if the supplied 'Bool' flag is 'True', for all permissions that could (as --- in 'bvPropCouldHold') contain the given offset. Return the indices in the --- list for the permissions that were found. -llvmPermIndicesForOffset :: (1 <= w, KnownNat w) => - [AtomicPerm (LLVMPointerType w)] -> Bool -> - PermExpr (BVType w) -> [Int] -llvmPermIndicesForOffset ps imprecise_p off = - let ixs_props = findMaybeIndices (llvmPermContainsOffset off) ps in - case find (\(_,(_,holds)) -> holds) ixs_props of - Just (i,_) -> [i] - Nothing | imprecise_p -> map fst ixs_props - Nothing -> [] - -- | Return the total length of an LLVM array permission in bytes llvmArrayLengthBytes :: (1 <= w, KnownNat w) => LLVMArrayPerm w -> PermExpr (BVType w) diff --git a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs index 72eb1af7d3..fa436b6397 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs @@ -30,8 +30,6 @@ module Verifier.SAW.Heapster.SAWTranslation where import Prelude hiding (pi) -import Numeric (showHex) -import Data.Char import Data.Maybe import Numeric.Natural import Data.List hiding (inits) @@ -69,7 +67,6 @@ import Lang.Crucible.CFG.Core import Verifier.SAW.OpenTerm import Verifier.SAW.Term.Functor -import Verifier.SAW.Module import Verifier.SAW.SharedTerm import Verifier.SAW.Heapster.CruUtil @@ -80,17 +77,6 @@ import Verifier.SAW.Heapster.TypedCrucible import GHC.Stack -scInsertDef :: SharedContext -> ModuleName -> Ident -> Term -> Term -> IO () -scInsertDef sc mnm ident def_tp def_tm = - do t <- scConstant' sc (ModuleIdentifier ident) def_tm def_tp - scRegisterGlobal sc ident t - scModifyModule sc mnm $ \m -> - insDef m $ Def { defIdent = ident, - defQualifier = NoQualifier, - defType = def_tp, - defBody = Just def_tm } - - ---------------------------------------------------------------------- -- * Translation Monads ---------------------------------------------------------------------- @@ -332,6 +318,15 @@ inExtMultiTransM MNil m = m inExtMultiTransM (ctx :>: etrans) m = inExtMultiTransM ctx $ inExtTransM etrans m +-- | Run a translation computation in an extended context, where we let-bind any +-- term in the supplied expression translation +inExtTransLetBindM :: TransInfo info => TypeTrans (ExprTrans tp) -> + ExprTrans tp -> TransM info (ctx :> tp) OpenTerm -> + TransM info ctx OpenTerm +inExtTransLetBindM tp_trans etrans m = + letTransMultiM "z" (typeTransTypes tp_trans) (transTerms etrans) $ \var_tms -> + inExtTransM (typeTransF tp_trans var_tms) m + -- | Run a translation computation in context @(ctx1 :++: ctx2) :++: ctx2@ by -- copying the @ctx2@ portion of the current context inExtMultiTransCopyLastM :: TransInfo info => prx ctx1 -> RAssign any ctx2 -> @@ -429,6 +424,18 @@ letTransM x tp rhs_m body_m = return $ letOpenTerm (pack x) tp (runTransM rhs_m r) (\x' -> runTransM (body_m x') r) +-- | Build 0 or more let-bindings in a translation monad, using the same +-- variable name +letTransMultiM :: String -> [OpenTerm] -> [OpenTerm] -> + ([OpenTerm] -> TransM info ctx OpenTerm) -> + TransM info ctx OpenTerm +letTransMultiM _ [] [] f = f [] +letTransMultiM x (tp:tps) (rhs:rhss) f = + letTransM x tp (return rhs) $ \var_tm -> + letTransMultiM x tps rhss (\var_tms -> f (var_tm:var_tms)) +letTransMultiM _ _ _ _ = + error "letTransMultiM: numbers of types and right-hand sides disagree" + -- | Build a bitvector type in a translation monad bitvectorTransM :: TransM info ctx OpenTerm -> TransM info ctx OpenTerm bitvectorTransM m = @@ -3606,6 +3613,13 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl , applyMultiTransM (return $ globalOpenTerm "Prelude.bvEqWithProof") [ return (natOpenTerm $ natVal2 prop) , translate1 e1, translate1 e2]] + -- If e1 and e2 are already unequal, short-circuit and do nothing + ([nuMP| Impl1_TryProveBVProp x prop@(BVProp_Neq e1 e2) _ |], _) + | not $ mbLift (mbMap2 bvCouldEqual e1 e2) -> + translatePermImplUnary mb_impls $ + withPermStackM (:>: translateVar x) + (:>: PTrans_Conj [APTrans_BVProp (BVPropTrans prop unitOpenTerm)]) + -- For an inequality test, we don't need a proof, so just insert an if ([nuMP| Impl1_TryProveBVProp x prop@(BVProp_Neq e1 e2) prop_str |], [nuMP| MbPermImpls_Cons _ _ mb_impl' |]) -> @@ -3864,6 +3878,10 @@ instance (PermCheckExtC ext, TransInfo info) => [nuMP| HandleLit _ |] -> return ETrans_Fun -- Bitvectors + [nuMP| BVUndef w |] -> + -- FIXME: we should really handle poison values; this translation just + -- treats them as if there were the bitvector 0 value + return $ ETrans_Term $ bvBVOpenTerm (mbLift w) $ BV.zero (mbLift w) [nuMP| BVLit w mb_bv |] -> return $ ETrans_Term $ bvBVOpenTerm (mbLift w) $ mbLift mb_bv [nuMP| BVConcat w1 w2 e1 e2 |] -> @@ -4140,10 +4158,11 @@ translateStmt :: PermCheckExtC ext => ImpTransM ext blocks tops ret ps_out (ctx :++: rets) OpenTerm -> ImpTransM ext blocks tops ret ps_in ctx OpenTerm translateStmt loc mb_stmt m = case mbMatch mb_stmt of - [nuMP| TypedSetReg _ e |] -> - do etrans <- tpTransM $ translate e + [nuMP| TypedSetReg tp e |] -> + do tp_trans <- translate tp + etrans <- tpTransM $ translate e let ptrans = exprOutPerm e - inExtTransM etrans $ + inExtTransLetBindM tp_trans etrans $ withPermStackM (:>: Member_Base) (:>: extPermTrans ptrans) m [nuMP| TypedSetRegPermExpr _ e |] -> @@ -4683,24 +4702,6 @@ tcTranslateCFGTupleFun env checks endianness dlevel cfgs_and_perms = tcCFG ?ptrWidth env' endianness dlevel fun_perm cfg --- | Make a "coq-safe" identifier from a string that might contain --- non-identifier characters, where we use the SAW core notion of identifier --- characters as letters, digits, underscore and primes. Any disallowed --- character is mapped to the string @__xNN@, where @NN@ is the hexadecimal code --- for that character. Additionally, a SAW core identifier is not allowed to --- start with a prime, so a leading underscore is added in such a case. -mkSafeIdent :: ModuleName -> String -> Ident -mkSafeIdent _ [] = "_" -mkSafeIdent mnm nm = - let is_safe_char c = isAlphaNum c || c == '_' || c == '\'' in - mkIdent mnm $ Data.Text.pack $ - (if nm!!0 == '\'' then ('_' :) else id) $ - concatMap - (\c -> if is_safe_char c then [c] else - "__x" ++ showHex (ord c) "") - nm - - -- | Type-check a set of CFGs against their function permissions, translate the -- results to SAW core functions, and add them as definitions to the SAW core -- module with the given module name. The name of each definition will be the @@ -4717,18 +4718,18 @@ tcTranslateAddCFGs sc mod_name env checks endianness dlevel cfgs_and_perms = let tup_fun_ident = mkSafeIdent mod_name (someCFGAndPermToName (head cfgs_and_perms) ++ "__tuple_fun") - tup_fun_tp <- completeOpenTerm sc $ + tup_fun_tp <- completeNormOpenTerm sc $ applyOpenTerm (globalOpenTerm "Prelude.lrtTupleType") lrts - tup_fun_tm <- completeOpenTerm sc $ + tup_fun_tm <- completeNormOpenTerm sc $ applyOpenTermMulti (globalOpenTerm "Prelude.multiFixM") [lrts, tup_fun] scInsertDef sc mod_name tup_fun_ident tup_fun_tp tup_fun_tm new_entries <- zipWithM (\cfg_and_perm i -> - do tp <- completeOpenTerm sc $ + do tp <- completeNormOpenTerm sc $ applyOpenTerm (globalOpenTerm "Prelude.lrtToType") $ someCFGAndPermLRT env cfg_and_perm - tm <- completeOpenTerm sc $ + tm <- completeNormOpenTerm sc $ projTupleOpenTerm i (globalOpenTerm tup_fun_ident) let ident = mkSafeIdent mod_name (someCFGAndPermToName cfg_and_perm) scInsertDef sc mod_name ident tp tm @@ -4748,13 +4749,13 @@ tcTranslateAddCFGs sc mod_name env checks endianness dlevel cfgs_and_perms = translateCompleteFunPerm :: SharedContext -> PermEnv -> FunPerm ghosts args ret -> IO Term translateCompleteFunPerm sc env fun_perm = - completeOpenTerm sc $ + completeNormOpenTerm sc $ runNilTypeTransM env noChecks (translate $ emptyMb fun_perm) -- | Translate a 'TypeRepr' to the SAW core type it represents translateCompleteType :: SharedContext -> PermEnv -> TypeRepr tp -> IO Term translateCompleteType sc env typ_perm = - completeOpenTerm sc $ typeTransType1 $ + completeNormOpenTerm sc $ typeTransType1 $ runNilTypeTransM env noChecks $ translate $ emptyMb typ_perm -- | Translate a 'TypeRepr' within the given context of type arguments to the @@ -4762,7 +4763,7 @@ translateCompleteType sc env typ_perm = translateCompleteTypeInCtx :: SharedContext -> PermEnv -> CruCtx args -> Mb args (TypeRepr a) -> IO Term translateCompleteTypeInCtx sc env args ret = - completeOpenTerm sc $ + completeNormOpenTerm sc $ runNilTypeTransM env noChecks (piExprCtx args (typeTransType1 <$> translate ret')) where ret' = mbCombine (cruCtxProxies args) . emptyMb $ ret @@ -4776,7 +4777,7 @@ translateCompletePureFun :: SharedContext -> PermEnv -> Mb ctx (ValuePerm ret) -- ^ Return type perm -> IO Term translateCompletePureFun sc env ctx args ret = - completeOpenTerm sc $ runNilTypeTransM env noChecks $ + completeNormOpenTerm sc $ runNilTypeTransM env noChecks $ piExprCtx ctx $ piPermCtx args' $ const $ typeTransTupleType <$> translate ret' where args' = mbCombine pxys . emptyMb $ args diff --git a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs b/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs index 3657d60986..df49b4e60f 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs @@ -2805,6 +2805,21 @@ tcExpr (BVZext w2 _ (RegWithVal _ (bvMatchConst -> Just bv))) = tcExpr (BVSext w2 w (RegWithVal _ (bvMatchConst -> Just bv))) = withKnownNat w2 $ pure $ Just $ bvBV $ BV.sext w w2 bv +tcExpr (BVNot w (RegWithVal _ (bvMatchConst -> Just bv))) = + withKnownNat w $ pure $ Just $ bvBV $ BV.complement w bv +tcExpr (BVAnd w (RegWithVal _ (bvMatchConst -> + Just bv1)) (RegWithVal _ + (bvMatchConst -> Just bv2))) = + withKnownNat w $ pure $ Just $ bvBV $ BV.and bv1 bv2 +tcExpr (BVOr w (RegWithVal _ (bvMatchConst -> + Just bv1)) (RegWithVal _ + (bvMatchConst -> Just bv2))) = + withKnownNat w $ pure $ Just $ bvBV $ BV.or bv1 bv2 +tcExpr (BVXor w (RegWithVal _ (bvMatchConst -> + Just bv1)) (RegWithVal _ + (bvMatchConst -> Just bv2))) = + withKnownNat w $ pure $ Just $ bvBV $ BV.xor bv1 bv2 + tcExpr (BVAdd w (RegWithVal _ e1) (RegWithVal _ e2)) = withKnownNat w $ pure $ Just $ bvAdd e1 e2 @@ -3876,7 +3891,7 @@ tcJumpTarget ctx (JumpTarget blkID args_tps args) = -- reflexivity. implWithoutTracingM (implPushOrReflMultiM perms_in) >>> pure (PermImpl_Done $ - TypedJumpTarget siteID Proxy (mkCruCtx args_tps) perms_in) + TypedJumpTarget siteID Proxy (mkCruCtx args_tps) perms_in) -- | Type-check a termination statement @@ -4012,7 +4027,8 @@ proveCallSiteImpl srcID destID args ghosts vars mb_perms_in mb_perms_out = mbSeparate (cruCtxProxies ghosts) $ mbValuePermsToDistPerms mb_perms_out in stmtTraceM (\i -> - pretty "proveCallSiteImpl:" <> line <> + pretty ("proveCallSiteImpl, src = " ++ show srcID ++ + ", dest = " ++ show destID) <> line <> indent 2 (permPretty i perms_in) <> line <> pretty "-o" <> line <> indent 2 (permPretty i perms_out)) >>> diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Widening.hs b/heapster-saw/src/Verifier/SAW/Heapster/Widening.hs index 98c8606774..c0133094be 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Widening.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/Widening.hs @@ -501,14 +501,12 @@ equalizeLLVMBlockRanges' bp1 bp2 | bvEq (llvmBlockLen bp1) (llvmBlockLen bp2) = return (bp1, bp2, [], []) equalizeLLVMBlockRanges' bp1 bp2 - | bvLeq (llvmBlockLen bp1) (llvmBlockLen bp2) = - do (bp2', bp2'') <- splitLLVMBlockPerm (bvAdd (llvmBlockOffset bp1) - (llvmBlockLen bp1)) bp2 + | bvLt (llvmBlockLen bp1) (llvmBlockLen bp2) = + do (bp2', bp2'') <- splitLLVMBlockPerm (llvmBlockEndOffset bp1) bp2 return (bp1, bp2', [], [bp2'']) equalizeLLVMBlockRanges' bp1 bp2 - | bvLeq (llvmBlockLen bp2) (llvmBlockLen bp1) = - do (bp1', bp1'') <- splitLLVMBlockPerm (bvAdd (llvmBlockOffset bp2) - (llvmBlockLen bp2)) bp1 + | bvLt (llvmBlockLen bp2) (llvmBlockLen bp1) = + do (bp1', bp1'') <- splitLLVMBlockPerm (llvmBlockEndOffset bp2) bp1 return (bp1', bp2, [bp1''], []) equalizeLLVMBlockRanges' _ _ = Nothing @@ -524,12 +522,12 @@ equalizeLLVMBlockRanges bp1 bp2 | bvEq (llvmBlockOffset bp1) (llvmBlockOffset bp2) = equalizeLLVMBlockRanges' bp1 bp2 equalizeLLVMBlockRanges bp1 bp2 - | bvLeq (llvmBlockOffset bp1) (llvmBlockOffset bp2) = + | bvLt (llvmBlockOffset bp1) (llvmBlockOffset bp2) = do (bp1', bp1'') <- splitLLVMBlockPerm (llvmBlockOffset bp2) bp1 (bp1_ret, bp2_ret, bps1, bps2) <- equalizeLLVMBlockRanges' bp1'' bp2 return (bp1_ret, bp2_ret, bp1':bps1, bps2) equalizeLLVMBlockRanges bp1 bp2 - | bvLeq (llvmBlockOffset bp2) (llvmBlockOffset bp1) = + | bvLt (llvmBlockOffset bp2) (llvmBlockOffset bp1) = do (bp2', bp2'') <- splitLLVMBlockPerm (llvmBlockOffset bp1) bp2 (bp1_ret, bp2_ret, bps1, bps2) <- equalizeLLVMBlockRanges' bp1 bp2'' return (bp1_ret, bp2_ret, bps1, bp2':bps2) diff --git a/saw-core/src/Verifier/SAW/OpenTerm.hs b/saw-core/src/Verifier/SAW/OpenTerm.hs index a28c6b7e7f..afef3cb420 100644 --- a/saw-core/src/Verifier/SAW/OpenTerm.hs +++ b/saw-core/src/Verifier/SAW/OpenTerm.hs @@ -18,7 +18,7 @@ built. module Verifier.SAW.OpenTerm ( -- * Open terms and converting to closed terms - OpenTerm(..), completeOpenTerm, completeOpenTermType, + OpenTerm(..), completeOpenTerm, completeNormOpenTerm, completeOpenTermType, -- * Basic operations for building open terms closedOpenTerm, flatOpenTerm, sortOpenTerm, natOpenTerm, unitOpenTerm, unitTypeOpenTerm, @@ -59,6 +59,10 @@ completeOpenTerm sc (OpenTerm termM) = either (fail . show) return =<< runTCM (typedVal <$> termM) sc Nothing [] +-- | "Complete" an 'OpenTerm' to a closed term and 'betaNormalize' the result +completeNormOpenTerm :: SharedContext -> OpenTerm -> IO Term +completeNormOpenTerm sc m = completeOpenTerm sc m >>= betaNormalize sc + -- | "Complete" an 'OpenTerm' to a closed term for its type completeOpenTermType :: SharedContext -> OpenTerm -> IO Term completeOpenTermType sc (OpenTerm termM) = diff --git a/src/SAWScript/HeapsterBuiltins.hs b/src/SAWScript/HeapsterBuiltins.hs index f879ed16df..58f94c936c 100644 --- a/src/SAWScript/HeapsterBuiltins.hs +++ b/src/SAWScript/HeapsterBuiltins.hs @@ -273,7 +273,8 @@ parseAndInsDef henv nm term_tp term_string = mkHeapsterEnv :: DebugLevel -> ModuleName -> [Some LLVMModule] -> TopLevel HeapsterEnv mkHeapsterEnv dlevel saw_mod_name llvm_mods@(Some first_mod:_) = - do let w = llvmModuleArchReprWidth first_mod + do sc <- getSharedContext + let w = llvmModuleArchReprWidth first_mod let endianness = llvmDataLayout (modTrans first_mod ^. transContext ^. llvmTypeCtx) ^. intLayout @@ -281,10 +282,10 @@ mkHeapsterEnv dlevel saw_mod_name llvm_mods@(Some first_mod:_) = Left pf -> return pf Right _ -> fail "LLVM arch width is 0!" let globals = concatMap (\(Some lm) -> L.modGlobals $ modAST lm) llvm_mods - env = - withKnownNat w $ withLeqProof leq_proof $ - foldl (permEnvAddGlobalConst dlevel endianness w) - heapster_default_env globals + env <- + liftIO $ withKnownNat w $ withLeqProof leq_proof $ + foldM (permEnvAddGlobalConst sc saw_mod_name dlevel endianness w) + heapster_default_env globals env_ref <- liftIO $ newIORef env dlevel_ref <- liftIO $ newIORef dlevel checks_ref <- liftIO $ newIORef doChecks