From 3c339335106638960e87503d33d7713f1cfcc012 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Fri, 3 Sep 2021 13:29:37 -0700 Subject: [PATCH] Heapster disable debug output (#1449) * fixed the IRT description generation to match the recent change that made the translation of bitvector permissions to just be bitvectors * added the notion of Heapster debug levels, and threaded them through all of the Heapster code so that no debug output is printed unless the Heapster debug level is set to at least 1 --- .../src/Verifier/SAW/Heapster/Implication.hs | 44 +++++------ .../src/Verifier/SAW/Heapster/Permissions.hs | 24 +++++- .../src/Verifier/SAW/Heapster/RustTypes.hs | 6 +- .../Verifier/SAW/Heapster/SAWTranslation.hs | 32 ++++---- .../Verifier/SAW/Heapster/TypedCrucible.hs | 75 +++++++++++-------- .../src/Verifier/SAW/Heapster/Widening.hs | 23 +++--- src/SAWScript/HeapsterBuiltins.hs | 25 +++++-- src/SAWScript/Interpreter.hs | 6 ++ src/SAWScript/Value.hs | 3 +- 9 files changed, 146 insertions(+), 92 deletions(-) diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs index ceacdc0866..2a430f012a 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs @@ -64,7 +64,6 @@ import Verifier.SAW.Heapster.Permissions import Verifier.SAW.Heapster.GenMonad import GHC.Stack -import Debug.Trace ---------------------------------------------------------------------- @@ -2657,15 +2656,15 @@ data ImplState vars ps = -- ^ Types of all the variables in scope _implStateFailPrefix :: String, -- ^ A prefix string to prepend to any failure messages - _implStateDoTrace :: Bool + _implStateDebugLevel :: DebugLevel -- ^ Whether tracing is turned on or not } makeLenses ''ImplState mkImplState :: CruCtx vars -> PermSet ps -> PermEnv -> - PPInfo -> String -> Bool -> NameMap TypeRepr -> + PPInfo -> String -> DebugLevel -> NameMap TypeRepr -> ImplState vars ps -mkImplState vars perms env info fail_prefix do_trace nameTypes = +mkImplState vars perms env info fail_prefix dlevel nameTypes = ImplState { _implStateVars = vars, _implStatePerms = perms, @@ -2676,7 +2675,7 @@ mkImplState vars perms env info fail_prefix do_trace nameTypes = _implStatePPInfo = info, _implStateNameTypes = nameTypes, _implStateFailPrefix = fail_prefix, - _implStateDoTrace = do_trace + _implStateDebugLevel = dlevel } extImplState :: KnownRepr TypeRepr tp => ImplState vars ps -> @@ -2707,28 +2706,28 @@ runImplM :: PermEnv {- ^ permission environment -} -> PPInfo {- ^ pretty-printer settings -} -> String {- ^ fail prefix -} -> - Bool {- ^ do trace -} -> + DebugLevel {- ^ debug level -} -> NameMap TypeRepr {- ^ name types -} -> ImplM vars s r ps_out ps_in a -> ((a, ImplState vars ps_out) -> State (Closed s) (r ps_out)) -> State (Closed s) (PermImpl r ps_in) -runImplM vars perms env ppInfo fail_prefix do_trace nameTypes m k = +runImplM vars perms env ppInfo fail_prefix dlevel nameTypes m k = runGenStateContT m - (mkImplState vars perms env ppInfo fail_prefix do_trace nameTypes) + (mkImplState vars perms env ppInfo fail_prefix dlevel nameTypes) (\s a -> PermImpl_Done <$> k (a, s)) -- | Run an 'ImplM' computation that returns a 'PermImpl', by inserting that -- 'PermImpl' inside of the larger 'PermImpl' that is built up by the 'ImplM' -- computation. runImplImplM :: CruCtx vars -> PermSet ps_in -> PermEnv -> PPInfo -> - String -> Bool -> NameMap TypeRepr -> + String -> DebugLevel -> NameMap TypeRepr -> ImplM vars s r ps_out ps_in (PermImpl r ps_out) -> State (Closed s) (PermImpl r ps_in) -runImplImplM vars perms env ppInfo fail_prefix do_trace nameTypes m = +runImplImplM vars perms env ppInfo fail_prefix dlevel nameTypes m = runGenStateContT m - (mkImplState vars perms env ppInfo fail_prefix do_trace nameTypes) + (mkImplState vars perms env ppInfo fail_prefix dlevel nameTypes) (\_ -> pure) -- | Embed a sub-computation in a name-binding inside another 'ImplM' @@ -2742,7 +2741,7 @@ embedImplM ps_in m = lift $ runImplM CruCtxNil (distPermSet ps_in) (view implStatePermEnv s) (view implStatePPInfo s) - (view implStateFailPrefix s) (view implStateDoTrace s) + (view implStateFailPrefix s) (view implStateDebugLevel s) (view implStateNameTypes s) m (pure . fst) -- | Embed a sub-computation in a name-binding inside another 'ImplM' @@ -2758,7 +2757,7 @@ embedMbImplM mb_ps_in mb_m = runImplM CruCtxNil ps_in (view implStatePermEnv s) (view implStatePPInfo s) - (view implStateFailPrefix s) (view implStateDoTrace s) + (view implStateFailPrefix s) (view implStateDebugLevel s) (view implStateNameTypes s) m (pure . fst)) mb_ps_in mb_m @@ -3013,26 +3012,23 @@ implApplyImpl1 impl1 mb_ms = implSetNameTypes ns ctx >>> f ns) --- | Emit debugging output using the current 'PPInfo' if the 'implStateDoTrace' --- flag is set +-- | Emit debugging output using the current 'PPInfo' if the 'implStateDebugLevel' +-- is at least 1 implTraceM :: (PPInfo -> PP.Doc ann) -> ImplM vars s r ps ps String implTraceM f = - do do_trace <- use implStateDoTrace + do dlevel <- use implStateDebugLevel doc <- uses implStatePPInfo f let str = renderDoc doc - fn do_trace str (pure str) - where - fn True = trace - fn False = const id + debugTrace dlevel str (return str) --- | Run an 'ImplM' computation with 'implStateDoTrace' temporarily disabled +-- | Run an 'ImplM' computation with the debug level set to 'noDebugLevel' implWithoutTracingM :: ImplM vars s r ps_out ps_in a -> ImplM vars s r ps_out ps_in a implWithoutTracingM m = - use implStateDoTrace >>>= \saved -> - (implStateDoTrace .= False) >>> + use implStateDebugLevel >>>= \saved -> + (implStateDebugLevel .= noDebugLevel) >>> m >>>= \a -> - (implStateDoTrace .= saved) >> + (implStateDebugLevel .= saved) >> pure a -- | Terminate the current proof branch with a failure diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs index 0a0c8da851..a7c41f5a3c 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs @@ -137,6 +137,28 @@ foldMapWithDefault comb def f l = foldr1WithDefault comb def $ map f l -- * Pretty-printing ---------------------------------------------------------------------- +-- | A special-purpose type used to indicate debugging level +data DebugLevel = DebugLevel Int deriving (Eq,Ord) + +-- | The debug level for no debugging +noDebugLevel :: DebugLevel +noDebugLevel = DebugLevel 0 + +-- | The debug level to enable tracing +traceDebugLevel :: DebugLevel +traceDebugLevel = DebugLevel 1 + +-- | Output a debug statement to @stderr@ using 'trace' if the supplied +-- 'DebugLevel' is at least 'traceDebugLevel' +debugTrace :: DebugLevel -> String -> a -> a +debugTrace dlevel | dlevel >= traceDebugLevel = trace +debugTrace _ = const id + +-- | Like 'debugTrace' but take in a 'Doc' instead of a 'String' +debugTracePretty :: DebugLevel -> Doc ann -> a -> a +debugTracePretty dlevel d a = debugTrace dlevel (renderDoc d) a + +-- | The constant string functor newtype StringF a = StringF { unStringF :: String } -- | Convert a type to a base name for printing variables of that type @@ -1007,7 +1029,7 @@ bvLt _ _ = False bvSLt :: (1 <= w, KnownNat w) => PermExpr (BVType w) -> PermExpr (BVType w) -> Bool bvSLt (bvMatchConst -> Just i1) (bvMatchConst -> Just i2) = - trace ("bvSLt " ++ show i1 ++ " " ++ show i2) (BV.slt knownNat i1 i2) + BV.slt knownNat i1 i2 bvSLt _ _ = False -- | Test whether a bitvector expression @e@ is in a 'BVRange' for all diff --git a/heapster-saw/src/Verifier/SAW/Heapster/RustTypes.hs b/heapster-saw/src/Verifier/SAW/Heapster/RustTypes.hs index 0f1771714c..f7c3d319cc 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/RustTypes.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/RustTypes.hs @@ -1099,9 +1099,9 @@ rsConvertFun :: (1 <= w, KnownNat w) => prx w -> Abi -> Generics Span -> FnDecl Span -> RustConvM Some3FunPerm rsConvertFun w abi (Generics ldefs _tparams@[] (WhereClause [] _) _) (FnDecl args maybe_ret_tp False _) = - fmap (\ret -> - tracePretty (pretty "rsConvertFun returning:" <+> - permPretty emptyPPInfo ret) ret) $ + -- fmap (\ret -> + -- tracePretty (pretty "rsConvertFun returning:" <+> + -- permPretty emptyPPInfo ret) ret) $ withLifetimes ldefs $ do arg_shapes <- mapM (rsConvert w) args ret_shape <- maybe (return PExpr_EmptyShape) (rsConvert w) maybe_ret_tp diff --git a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs index 9f6e5a1d9d..080a890d2d 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs @@ -79,7 +79,7 @@ import Verifier.SAW.Heapster.Implication import Verifier.SAW.Heapster.TypedCrucible import GHC.Stack -import Debug.Trace + scInsertDef :: SharedContext -> ModuleName -> Ident -> Term -> Term -> IO () scInsertDef sc mnm ident def_tp def_tm = @@ -3806,16 +3806,18 @@ debugPrettyPermCtx prxs (ptranss :>: ptrans) = translateApply :: String -> OpenTerm -> Mb ctx (DistPerms ps) -> ImpTransM ext blocks tops ret ps ctx OpenTerm translateApply nm f perms = - do expr_ctx <- itiExprCtx <$> ask + do assertPermStackEqM nm perms + expr_ctx <- itiExprCtx <$> ask arg_membs <- itiPermStackVars <$> ask let e_args = RL.map (flip RL.get expr_ctx) arg_membs i_args <- itiPermStack <$> ask return $ + {- trace ("translateApply for " ++ nm ++ " with perm arguments:\n" ++ -- renderDoc (list $ debugPrettyPermCtx (mbToProxy perms) i_args) -- permPrettyString emptyPPInfo (permTransCtxPerms (mbToProxy perms) i_args) permPrettyString emptyPPInfo perms - ) $ + ) $ -} applyOpenTermMulti f (exprCtxToTerms e_args ++ permCtxToTerms i_args) -- | Translate a call to (the translation of) an entrypoint, by either calling @@ -4194,14 +4196,13 @@ piLRTTransM x tps body_f = translateEntryLRT :: TypedEntry TransPhase ext blocks tops ret args ghosts -> TypeTransM ctx OpenTerm translateEntryLRT entry@(TypedEntry {..}) = - trace "translateEntryLRT starting..." $ inEmptyCtxTransM $ + inEmptyCtxTransM $ translateClosed (typedEntryAllArgs entry) >>= \arg_tps -> piLRTTransM "arg" arg_tps $ \ectx -> inCtxTransM ectx $ translate typedEntryPermsIn >>= \perms_in_tps -> piLRTTransM "p" perms_in_tps $ \_ -> translateEntryRetType entry >>= \retType -> - trace "translateEntryLRT finished" $ return $ ctorOpenTerm "Prelude.LRT_Ret" [retType] -- | Build a @LetRecTypes@ list that describes the types of all of the @@ -4209,14 +4210,12 @@ translateEntryLRT entry@(TypedEntry {..}) = translateBlockMapLRTs :: TypedBlockMap TransPhase ext blocks tops ret -> TypeTransM ctx OpenTerm translateBlockMapLRTs = - trace "translateBlockMapLRTs started..." $ foldBlockMapLetRec (\entry rest_m -> do entryType <- translateEntryLRT entry rest <- rest_m return $ ctorOpenTerm "Prelude.LRT_Cons" [entryType, rest]) - (trace "translateBlockMapLRTs finished" $ - return $ ctorOpenTerm "Prelude.LRT_Nil" []) + (return $ ctorOpenTerm "Prelude.LRT_Nil" []) -- | Lambda-abstract over all the entrypoints in a 'TypedBlockMap' that -- correspond to letrec-bound functions, putting the lambda-bound variables into @@ -4273,11 +4272,10 @@ translateBlockMapBodies :: PermCheckExtC ext => TypedBlockMap TransPhase ext blocks tops ret -> TypeTransM ctx OpenTerm translateBlockMapBodies mapTrans = - trace "translateBlockMapBodies starting..." $ foldBlockMapLetRec (\entry restM -> pairOpenTerm <$> translateEntryBody mapTrans entry <*> restM) - (trace "translateBlockMapBodies finished" $ return unitOpenTerm) + (return unitOpenTerm) -- | Translate a typed CFG to a SAW term @@ -4401,9 +4399,9 @@ someCFGAndPermPtrPerm (SomeCFGAndPerm _ _ _ fun_perm) = -- each @tpi@ is the @i@th type in @lrts@ tcTranslateCFGTupleFun :: HasPtrWidth w => - PermEnv -> EndianForm -> [SomeCFGAndPerm LLVM] -> + PermEnv -> EndianForm -> DebugLevel -> [SomeCFGAndPerm LLVM] -> (OpenTerm, OpenTerm) -tcTranslateCFGTupleFun env endianness cfgs_and_perms = +tcTranslateCFGTupleFun env endianness dlevel cfgs_and_perms = let lrts = map (someCFGAndPermLRT env) cfgs_and_perms in let lrts_tm = foldr (\lrt lrts' -> ctorOpenTerm "Prelude.LRT_Cons" [lrt,lrts']) @@ -4427,8 +4425,8 @@ tcTranslateCFGTupleFun env endianness cfgs_and_perms = tupleOpenTerm $ flip map (zip cfgs_and_perms funs) $ \(cfg_and_perm, _) -> case cfg_and_perm of SomeCFGAndPerm sym _ cfg fun_perm -> - trace ("Type-checking " ++ show sym) $ - translateCFG env' $ tcCFG ?ptrWidth env' endianness fun_perm cfg + debugTrace dlevel ("Type-checking " ++ show sym) $ + translateCFG env' $ tcCFG ?ptrWidth env' endianness dlevel fun_perm cfg -- | Make a "coq-safe" identifier from a string that might contain @@ -4458,11 +4456,11 @@ mkSafeIdent mnm nm = tcTranslateAddCFGs :: HasPtrWidth w => SharedContext -> ModuleName -> - PermEnv -> EndianForm -> [SomeCFGAndPerm LLVM] -> + PermEnv -> EndianForm -> DebugLevel -> [SomeCFGAndPerm LLVM] -> IO PermEnv -tcTranslateAddCFGs sc mod_name env endianness cfgs_and_perms = +tcTranslateAddCFGs sc mod_name env endianness dlevel cfgs_and_perms = do let (lrts, tup_fun) = - tcTranslateCFGTupleFun env endianness cfgs_and_perms + tcTranslateCFGTupleFun env endianness dlevel cfgs_and_perms let tup_fun_ident = mkSafeIdent mod_name (someCFGAndPermToName (head cfgs_and_perms) ++ "__tuple_fun") diff --git a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs b/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs index 805c890fec..37f01075a7 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs @@ -81,8 +81,6 @@ import Verifier.SAW.Heapster.NamePropagation import Verifier.SAW.Heapster.Permissions import Verifier.SAW.Heapster.Widening -import Debug.Trace - ---------------------------------------------------------------------- -- * Handling Crucible Extensions @@ -1453,7 +1451,6 @@ entryAddCallSite siteID _ entry (typedEntryCallers entry) = error "entryAddCallSite: call site already exists!" entryAddCallSite siteID perms_in entry = - trace ("entryAddCallSite: " ++ show siteID) $ entry { typedEntryCallers = typedEntryCallers entry ++ [Some $ emptyTypedCallSite siteID perms_in] } @@ -1478,7 +1475,6 @@ blockAddCallSite siteID _ _ perms_in _ blk -- Otherwise, make a new entrypoint blockAddCallSite siteID tops ret perms_in perms_out blk = - trace ("blockAddCallSite: " ++ show siteID) $ addEntryToBlock (singleCallSiteEntry siteID tops (blockArgs blk) ret perms_in perms_out) blk @@ -1709,7 +1705,9 @@ data TopPermCheckState ext cblocks blocks tops ret = stCBlocksEq :: RListToCtxCtx blocks :~: cblocks, -- | The endianness of the current architecture stEndianness :: !EndianForm, - stArchWidth :: SomePtrWidth + stArchWidth :: SomePtrWidth, + -- | The debugging level + stDebugLevel :: DebugLevel } makeLenses ''TopPermCheckState @@ -1721,12 +1719,13 @@ emptyTopPermCheckState :: PermEnv -> FunPerm ghosts (CtxToRList init) ret -> EndianForm -> + DebugLevel -> CFG ext cblocks init ret -> Assignment (Constant Bool) cblocks -> TopPermCheckState ext cblocks (CtxCtxToRList cblocks) (ghosts :++: CtxToRList init) ret -emptyTopPermCheckState env fun_perm endianness cfg sccs = +emptyTopPermCheckState env fun_perm endianness dlevel cfg sccs = let blkMap = cfgBlockMap cfg in TopPermCheckState { stTopCtx = funPermTops fun_perm @@ -1739,6 +1738,7 @@ emptyTopPermCheckState env fun_perm endianness cfg sccs = , stCBlocksEq = reprReprToCruCtxCtxEq (fmapFC blockInputs blkMap) , stEndianness = endianness , stArchWidth = SomePtrWidth + , stDebugLevel = dlevel } @@ -2243,9 +2243,10 @@ getErrorPrefix = gets (fromMaybe emptyDoc . stErrPrefix) stmtTraceM :: (PPInfo -> Doc ()) -> PermCheckM ext cblocks blocks tops ret r ps r ps String stmtTraceM f = - do doc <- f <$> permGetPPInfo + do dlevel <- stDebugLevel <$> top_get + doc <- f <$> permGetPPInfo let str = renderDoc doc - trace str (pure str) + debugTrace dlevel str (return str) -- | Failure in the statement permission-checking monad stmtFailM :: (PPInfo -> Doc ()) -> PermCheckM ext cblocks blocks tops ret r1 ps1 @@ -2286,9 +2287,10 @@ pcmRunImplM vars fail_doc retF impl_m = gets stCurPerms >>>= \perms_in -> gets stPPInfo >>>= \ppInfo -> gets stVarTypes >>>= \varTypes -> + (stDebugLevel <$> top_get) >>>= \dlevel -> liftPermCheckM $ lift $ fmap (AnnotPermImpl (renderDoc (err_prefix <> line <> fail_doc))) $ - runImplM vars perms_in env ppInfo "" True varTypes impl_m + runImplM vars perms_in env ppInfo "" dlevel varTypes impl_m (return . retF . fst) -- | Call 'runImplImplM' in the 'PermCheckM' monad @@ -2304,9 +2306,10 @@ pcmRunImplImplM vars fail_doc impl_m = gets stCurPerms >>>= \perms_in -> gets stPPInfo >>>= \ppInfo -> gets stVarTypes >>>= \varTypes -> + (stDebugLevel <$> top_get) >>>= \dlevel -> liftPermCheckM $ lift $ fmap (AnnotPermImpl (renderDoc (err_prefix <> line <> fail_doc))) $ - runImplImplM vars perms_in env ppInfo "" True varTypes impl_m + runImplImplM vars perms_in env ppInfo "" dlevel varTypes impl_m -- | Embed an implication computation inside a permission-checking computation, -- also supplying an overall error message for failures @@ -2323,8 +2326,9 @@ pcmEmbedImplWithErrM f_impl vars fail_doc m = gets stCurPerms >>>= \perms_in -> gets stPPInfo >>>= \ppInfo -> gets stVarTypes >>>= \varTypes -> + (stDebugLevel <$> top_get) >>>= \dlevel -> - addReader (gcaptureCC (runImplM vars perms_in env ppInfo "" True varTypes m)) + addReader (gcaptureCC (runImplM vars perms_in env ppInfo "" dlevel varTypes m)) >>>= \(a, implSt) -> gmodify ((\st -> st { stPPInfo = implSt ^. implStatePPInfo, @@ -3864,12 +3868,16 @@ tcTermStmt ctx (Br reg tgt1 tgt2) = let treg = tcReg ctx reg in getRegEqualsExpr treg >>>= \treg_expr -> case treg_expr of - PExpr_Bool True -> trace "tcTermStmt: br reg known to be true!" $ - TypedJump <$> tcJumpTarget ctx tgt1 - PExpr_Bool False -> trace "tcTermStmt: br reg known to be false!" $ - TypedJump <$> tcJumpTarget ctx tgt2 - _ -> trace "tcTermStmt: br reg unknown, checking both branches..." $ - TypedBr treg <$> tcJumpTarget ctx tgt1 <*> tcJumpTarget ctx tgt2 + PExpr_Bool True -> + stmtTraceM (const $ pretty "tcTermStmt: br reg known to be true!") >> + (TypedJump <$> tcJumpTarget ctx tgt1) + PExpr_Bool False -> + stmtTraceM (const $ pretty "tcTermStmt: br reg known to be false!") >> + (TypedJump <$> tcJumpTarget ctx tgt2) + _ -> + stmtTraceM (const $ pretty + "tcTermStmt: br reg unknown, checking both branches...") >> + (TypedBr treg <$> tcJumpTarget ctx tgt1 <*> tcJumpTarget ctx tgt2) tcTermStmt ctx (Return reg) = let treg = tcReg ctx reg in get >>>= \st -> @@ -4019,12 +4027,12 @@ visitCallSite (TypedEntry {..}) site@(TypedCallSite {..}) -- | Widen the permissions held by all callers of an entrypoint to compute new, -- weaker input permissions that can hopefully be satisfied by them -widenEntry :: PermCheckExtC ext => +widenEntry :: PermCheckExtC ext => DebugLevel -> TypedEntry TCPhase ext blocks tops ret args ghosts -> Some (TypedEntry TCPhase ext blocks tops ret args) -widenEntry (TypedEntry {..}) = - trace ("Widening entrypoint: " ++ show typedEntryID) $ - case foldl1' (widen typedEntryTops typedEntryArgs) $ +widenEntry dlevel (TypedEntry {..}) = + debugTrace dlevel ("Widening entrypoint: " ++ show typedEntryID) $ + case foldl1' (widen dlevel typedEntryTops typedEntryArgs) $ map (fmapF typedCallSiteArgVarPerms) typedEntryCallers of Some (ArgVarPerms ghosts perms_in) -> let callers = @@ -4051,18 +4059,23 @@ visitEntry :: -- If the entry is already complete, do nothing visitEntry _ _ _ entry | isJust $ completeTypedEntry entry = - trace ("visitEntry " ++ show (typedEntryID entry) ++ ": no change") $ + (stDebugLevel <$> get) >>= \dlevel -> + debugTrace dlevel ("visitEntry " ++ show (typedEntryID entry) + ++ ": no change") $ return $ Some entry -- Otherwise, visit the call sites, widen if needed, and type-check the body -visitEntry _ _ _ (TypedEntry {..}) - | tracePretty (vsep [pretty ("visitEntry " ++ show typedEntryID - ++ " with input perms:"), - permPretty emptyPPInfo typedEntryPermsIn]) False = undefined visitEntry names can_widen blk entry = + (stDebugLevel <$> get) >>= \dlevel -> + debugTracePretty dlevel + (vsep [pretty ("visitEntry " ++ show (typedEntryID entry) + ++ " with input perms:"), + permPretty emptyPPInfo (typedEntryPermsIn entry)]) + (return ()) >>= \() -> + mapM (traverseF $ visitCallSite entry) (typedEntryCallers entry) >>= \callers -> if can_widen && any (anyF typedCallSiteImplFails) callers then - case widenEntry entry of + case widenEntry dlevel entry of Some entry' -> -- If we widen then we are throwing away the old body, so all of its -- callees are no longer needed and can be deleted @@ -4124,15 +4137,17 @@ tcCFG :: forall w ext cblocks ghosts inits ret. (PermCheckExtC ext, KnownRepr ExtRepr ext, 1 <= w, 16 <= w) => NatRepr w -> - PermEnv -> EndianForm -> + PermEnv -> EndianForm -> DebugLevel -> FunPerm ghosts (CtxToRList inits) ret -> CFG ext cblocks inits ret -> TypedCFG ext (CtxCtxToRList cblocks) ghosts (CtxToRList inits) ret -tcCFG w env endianness fun_perm cfg = +tcCFG w env endianness dlevel fun_perm cfg = let h = cfgHandle cfg ghosts = funPermGhosts fun_perm (nodes, sccs) = cfgOrderWithSCCs cfg - init_st = let ?ptrWidth = w in emptyTopPermCheckState env fun_perm endianness cfg sccs + init_st = + let ?ptrWidth = w in + emptyTopPermCheckState env fun_perm endianness dlevel cfg sccs tp_nodes = map (\(Some blkID) -> Some $ stLookupBlockID blkID init_st) nodes in let tp_blk_map = diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Widening.hs b/heapster-saw/src/Verifier/SAW/Heapster/Widening.hs index c31346c8e5..b52408a0e0 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Widening.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/Widening.hs @@ -118,18 +118,19 @@ instance Monad (PolyContT r m) where PolyContT $ \k -> m $ \a -> runPolyContT (f a) k data WidState = WidState { _wsNameMap :: WidNameMap, - _wsPPInfo :: PPInfo } + _wsPPInfo :: PPInfo, + _wsDebugLevel :: DebugLevel } makeLenses ''WidState type WideningM = StateT WidState (PolyContT ExtVarPermsFun Identity) -runWideningM :: WideningM () -> WidNameMap -> RAssign Name args -> +runWideningM :: WideningM () -> DebugLevel -> WidNameMap -> RAssign Name args -> ExtVarPerms args -runWideningM m wnmap = +runWideningM m dlevel wnmap = applyExtVarPermsFun $ runIdentity $ - runPolyContT (runStateT m $ WidState wnmap emptyPPInfo) + runPolyContT (runStateT m $ WidState wnmap emptyPPInfo dlevel) (Identity . wnMapExtWidFun . _wsNameMap . snd) openMb :: CruCtx ctx -> Mb ctx a -> WideningM (RAssign Name ctx, a) @@ -180,8 +181,8 @@ setVarNamesM base xs = modify $ over wsPPInfo $ ppInfoAddExprNames base xs traceM :: (PPInfo -> Doc ()) -> WideningM () traceM f = - (f <$> view wsPPInfo <$> get) >>= \doc -> - tracePretty doc (return ()) + debugTrace <$> (view wsDebugLevel <$> get) + <*> (renderDoc <$> f <$> view wsPPInfo <$> get) <*> (return ()) ---------------------------------------------------------------------- @@ -878,11 +879,13 @@ simplifyGhostPerms _ some_avps = some_avps ---------------------------------------------------------------------- -- | Widen two lists of permissions-in-bindings -widen :: CruCtx tops -> CruCtx args -> Some (ArgVarPerms (tops :++: args)) -> +widen :: DebugLevel -> CruCtx tops -> CruCtx args -> + Some (ArgVarPerms (tops :++: args)) -> Some (ArgVarPerms (tops :++: args)) -> Some (ArgVarPerms (tops :++: args)) -widen tops args (Some (ArgVarPerms vars1 mb_perms1)) (Some (ArgVarPerms - vars2 mb_perms2)) = +widen dlevel tops args (Some (ArgVarPerms + vars1 mb_perms1)) (Some (ArgVarPerms + vars2 mb_perms2)) = let all_args = appendCruCtx tops args prxs1 = cruCtxProxies vars1 prxs2 = cruCtxProxies vars2 @@ -890,7 +893,7 @@ widen tops args (Some (ArgVarPerms vars1 mb_perms1)) (Some (ArgVarPerms simplifyGhostPerms (cruCtxProxies all_args) $ completeArgVarPerms $ flip nuMultiWithElim1 mb_mb_perms1 $ \args_ns1 mb_perms1' -> - (\m -> runWideningM m NameMap.empty args_ns1) $ + (\m -> runWideningM m dlevel NameMap.empty args_ns1) $ do (vars1_ns, ps1) <- openMb vars1 mb_perms1' (ns2, ps2) <- openMb (appendCruCtx all_args vars2) mb_perms2 let (args_ns2, vars2_ns) = RL.split all_args prxs2 ns2 diff --git a/src/SAWScript/HeapsterBuiltins.hs b/src/SAWScript/HeapsterBuiltins.hs index 1900049dd8..89ad20c224 100644 --- a/src/SAWScript/HeapsterBuiltins.hs +++ b/src/SAWScript/HeapsterBuiltins.hs @@ -45,6 +45,7 @@ module SAWScript.HeapsterBuiltins , heapster_print_fun_trans , heapster_export_coq , heapster_parse_test + , heapster_set_debug_level ) where import Data.Maybe @@ -270,10 +271,12 @@ heapster_init_env _bic _opts mod_str llvm_filename = liftIO $ scLoadModule sc (insImport (const True) preludeMod $ emptyModule saw_mod_name) perm_env_ref <- liftIO $ newIORef heapster_default_env + dlevel_ref <- liftIO $ newIORef noDebugLevel return $ HeapsterEnv { heapsterEnvSAWModule = saw_mod_name, heapsterEnvPermEnvRef = perm_env_ref, - heapsterEnvLLVMModules = [llvm_mod] + heapsterEnvLLVMModules = [llvm_mod], + heapsterEnvDebugLevel = dlevel_ref } load_sawcore_from_file :: BuiltinContext -> Options -> String -> TopLevel () @@ -290,10 +293,12 @@ heapster_init_env_from_file _bic _opts mod_filename llvm_filename = (saw_mod, saw_mod_name) <- readModuleFromFile mod_filename liftIO $ tcInsertModule sc saw_mod perm_env_ref <- liftIO $ newIORef heapster_default_env + dlevel_ref <- liftIO $ newIORef noDebugLevel return $ HeapsterEnv { heapsterEnvSAWModule = saw_mod_name, heapsterEnvPermEnvRef = perm_env_ref, - heapsterEnvLLVMModules = [llvm_mod] + heapsterEnvLLVMModules = [llvm_mod], + heapsterEnvDebugLevel = dlevel_ref } heapster_init_env_for_files :: BuiltinContext -> Options -> String -> [String] -> @@ -304,10 +309,12 @@ heapster_init_env_for_files _bic _opts mod_filename llvm_filenames = (saw_mod, saw_mod_name) <- readModuleFromFile mod_filename liftIO $ tcInsertModule sc saw_mod perm_env_ref <- liftIO $ newIORef heapster_default_env + dlevel_ref <- liftIO $ newIORef noDebugLevel return $ HeapsterEnv { heapsterEnvSAWModule = saw_mod_name, heapsterEnvPermEnvRef = perm_env_ref, - heapsterEnvLLVMModules = llvm_mods + heapsterEnvLLVMModules = llvm_mods, + heapsterEnvDebugLevel = dlevel_ref } -- | Look up the CFG associated with a symbol name in a Heapster environment @@ -977,6 +984,7 @@ heapster_typecheck_mut_funs_rename _bic _opts henv fn_names_and_perms = let endianness = llvmDataLayout (modTrans lm ^. transContext ^. llvmTypeCtx) ^. intLayout + dlevel <- liftIO $ readIORef $ heapsterEnvDebugLevel henv LeqProof <- case decideLeq (knownNat @16) w of Left pf -> return pf Right _ -> fail "LLVM arch width is < 16!" @@ -991,8 +999,8 @@ heapster_typecheck_mut_funs_rename _bic _opts henv fn_names_and_perms = let args = mkCruCtx $ handleArgTypes $ cfgHandle cfg let ret = handleReturnType $ cfgHandle cfg SomeFunPerm fun_perm <- - tracePretty (pretty ("Fun args:" :: String) <+> - permPretty emptyPPInfo args) $ + -- tracePretty (pretty ("Fun args:" :: String) <+> + -- permPretty emptyPPInfo args) $ withKnownNat w $ parseFunPermStringMaybeRust "permissions" w env args ret perms_string return (SomeCFGAndPerm (GlobalSymbol $ @@ -1001,7 +1009,7 @@ heapster_typecheck_mut_funs_rename _bic _opts henv fn_names_and_perms = let saw_modname = heapsterEnvSAWModule henv env' <- liftIO $ let ?ptrWidth = w in - tcTranslateAddCFGs sc saw_modname env endianness some_cfgs_and_perms + tcTranslateAddCFGs sc saw_modname env endianness dlevel some_cfgs_and_perms liftIO $ writeIORef (heapsterEnvPermEnvRef henv) env' @@ -1052,6 +1060,11 @@ heapster_export_coq _bic _opts henv filename = translateSAWModule coq_trans_conf saw_mod] liftIO $ writeFile filename (show coq_doc) +heapster_set_debug_level :: BuiltinContext -> Options -> HeapsterEnv -> + Int -> TopLevel () +heapster_set_debug_level _ _ env l = + liftIO $ writeIORef (heapsterEnvDebugLevel env) (DebugLevel l) + heapster_parse_test :: BuiltinContext -> Options -> Some LLVMModule -> String -> String -> TopLevel () heapster_parse_test _bic _opts _some_lm@(Some lm) fn_name perms_string = diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 990913fe52..c063ba0c42 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -3285,6 +3285,12 @@ primitives = Map.fromList Experimental [ "Export a Heapster environment to a Coq file" ] + , prim "heapster_set_debug_level" + "HeapsterEnv -> Int -> TopLevel ()" + (bicVal heapster_set_debug_level) + Experimental + [ "Set the debug level for Heapster; 0 = no debug output, 1 = debug output" ] + , prim "heapster_parse_test" "LLVMModule -> String -> String -> TopLevel ()" (bicVal heapster_parse_test) diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index d7b257059a..34e178a4d6 100644 --- a/src/SAWScript/Value.hs +++ b/src/SAWScript/Value.hs @@ -182,8 +182,9 @@ data HeapsterEnv = HeapsterEnv { -- ^ The SAW module containing all our Heapster definitions heapsterEnvPermEnvRef :: IORef PermEnv, -- ^ The current permissions environment - heapsterEnvLLVMModules :: [Some CMSLLVM.LLVMModule] + heapsterEnvLLVMModules :: [Some CMSLLVM.LLVMModule], -- ^ The list of underlying 'LLVMModule's that we are translating + heapsterEnvDebugLevel :: IORef DebugLevel } showHeapsterEnv :: HeapsterEnv -> String