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

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")