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