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