[inferbo] HTML debug for checking pass

Reviewed By: ezgicicek

Differential Revision: D13450061

fbshipit-source-id: ffe9ba062

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -638,28 +638,33 @@ let get_local_decls proc_desc =
 let compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_map * Summary.t =
  fun {proc_desc; tenv; integer_type_widths; summary} ->
   Preanal.do_preanalysis proc_desc tenv ;
-  let oenv = Dom.OndemandEnv.mk proc_desc tenv integer_type_widths in
-  let pdata = ProcData.make proc_desc tenv oenv in
+  let pdata =
+    let oenv = Dom.OndemandEnv.mk proc_desc tenv integer_type_widths in
+    ProcData.make proc_desc tenv oenv
+  in
   let cfg = CFG.from_pdesc proc_desc in
   let initial = Init.initial_state pdata (CFG.start_node cfg) in
   let inv_map = Analyzer.exec_pdesc ~do_narrowing:true ~initial pdata in
-  let locals = get_local_decls proc_desc in
-  let exit_mem =
-    extract_post (CFG.exit_node cfg |> CFG.Node.id) inv_map
-    |> Option.map ~f:(Dom.Mem.forget_locs locals)
-  in
-  let cond_set =
-    Report.check_proc summary proc_desc tenv integer_type_widths cfg inv_map
-    |> Report.report_errors summary |> Report.forget_locs locals |> Report.for_summary
-  in
+  let exit_node = CFG.exit_node cfg in
+  let underlying_exit_node = CFG.Node.underlying_node exit_node in
+  let pp_name f = F.pp_print_string f "bufferoverrun check" in
+  NodePrinter.start_session ~pp_name underlying_exit_node ;
   let summary =
+    let locals = get_local_decls proc_desc in
+    let cond_set =
+      Report.check_proc summary proc_desc tenv integer_type_widths cfg inv_map
+      |> Report.report_errors summary |> Report.forget_locs locals |> Report.for_summary
+    in
+    let exit_mem = extract_post (CFG.Node.id exit_node) inv_map in
     match exit_mem with
     | Some exit_mem ->
-        let post = (Dom.Mem.unset_oenv exit_mem, cond_set) in
-        Payload.update_summary post summary
+        let exit_mem = exit_mem |> Dom.Mem.forget_locs locals |> Dom.Mem.unset_oenv in
+        let payload = (exit_mem, cond_set) in
+        Payload.update_summary payload summary
     | _ ->
         summary
   in
+  NodePrinter.finish_session underlying_exit_node ;
   if Config.hoisting_report_only_expensive then
     let pname = Procdesc.get_proc_name proc_desc in
     WeakInvMapHashTbl.add inv_map_cache (pname, Some inv_map)

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -343,12 +343,11 @@ let rec eval_sympath_partial params p mem =
   match p with
   | Symb.SymbolPath.Pvar x -> (
     try ParamBindings.find x params with Caml.Not_found ->
-      L.(debug BufferOverrun Verbose)
-        "Symbol %a is not found in parameters.@\n" (Pvar.pp Pp.text) x ;
+      L.d_printfln "Symbol %a is not found in parameters." (Pvar.pp Pp.text) x ;
       Val.Itv.top )
   | Symb.SymbolPath.Callsite {cs} ->
-      L.(debug BufferOverrun Verbose)
-        "Symbol for %a is not expected to be in parameters.@\n" Typ.Procname.pp (CallSite.pname cs) ;
+      L.d_printfln "Symbol for %a is not expected to be in parameters." Typ.Procname.pp
+        (CallSite.pname cs) ;
       Mem.find (Loc.of_allocsite (Allocsite.make_symbol p)) mem
   | Symb.SymbolPath.Deref _ | Symb.SymbolPath.Field _ ->
       let locs = eval_locpath params p mem in
@@ -369,8 +368,7 @@ and eval_locpath params p mem =
         PowLoc.append_field ~fn locs
   in
   if PowLoc.is_empty res then (
-    L.(debug BufferOverrun Verbose)
-      "Location value for %a is not found.@\n" Symb.SymbolPath.pp_partial p ;
+    L.d_printfln "Location value for %a is not found." Symb.SymbolPath.pp_partial p ;
     PowLoc.unknown )
   else res