Heapster disable debug output

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

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

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

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,29 +4196,26 @@ 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
 -- entrypoints in a 'TypedBlockMap'
 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")