[inferbo] Use Logging for logging

Summary:
- Use Logging for logging
- Add a few extra debug (not ON by default)
- No space before colon

Depends on D4961957

Reviewed By: KihongHeo

Differential Revision: D4961989

fbshipit-source-id: 7c8697d

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -87,11 +87,10 @@ struct
     = fun params mem loc ->
       match params with
       | (e, _) :: _ ->
-          (* TODO: only print when debug mode? *)
+          if Config.bo_debug >= 1 then
-          F.fprintf F.err_formatter "@[<v>=== Infer Print === at %a@,"
+            L.err "@[<v>=== Infer Print === at %a@,%a@]%!"
-            Location.pp loc;
+              Location.pp loc
-          Dom.Val.pp F.err_formatter (Sem.eval e mem loc);
+              Dom.Val.pp (Sem.eval e mem loc);
-          F.fprintf F.err_formatter "@]";
           mem
       | _ -> mem
 
@@ -164,7 +163,10 @@ struct
               Sem.eval_array_alloc pname node typ offset size inst_num dimension
             in
             (Dom.Mem.add_heap field v mem, sym_num + 4)
-        | _ -> (mem, sym_num)
+        | _ ->
+            if Config.bo_debug >= 3 then
+              L.err "decl_fld of unhandled type: %a@." (Typ.pp Pp.text) typ;
+            (mem, sym_num)
       in
       match typ.Typ.desc with
       | Typ.Tstruct typename ->
@@ -190,7 +192,10 @@ struct
                 ~inst_num ~sym_num ~dimension:1 mem
             in
             (mem, inst_num + 1, sym_num)
-        | _ -> (mem, inst_num, sym_num) (* TODO: add other cases if necessary *)
+        | _ ->
+            if Config.bo_debug >= 3 then
+              L.err "declare_symbolic_parameter of unhandled type: %a@." (Typ.pp Pp.text) typ;
+            (mem, inst_num, sym_num) (* TODO: add other cases if necessary *)
       in
       List.fold ~f:add_formal ~init:(mem, inst_num, 0) (Sem.get_formals pdesc)
       |> fst3
@@ -216,16 +221,13 @@ struct
     = fun instr pre post ->
       if Config.bo_debug >= 2 then
         begin
-          F.fprintf F.err_formatter "@.@.================================@.";
+          L.err "@\n@\n================================@\n";
-          F.fprintf F.err_formatter "@[<v 2>Pre-state : @,";
+          L.err "@[<v 2>Pre-state : @,%a" Dom.Mem.pp pre;
-          Dom.Mem.pp F.err_formatter pre;
+          L.err "@]@\n@\n%a" (Sil.pp_instr Pp.text) instr;
-          F.fprintf F.err_formatter "@]@.@.";
+          L.err "@\n@\n";
-          Sil.pp_instr Pp.text F.err_formatter instr;
+          L.err "@[<v 2>Post-state : @,%a" Dom.Mem.pp post;
-          F.fprintf F.err_formatter "@.@.";
+          L.err "@]@\n";
-          F.fprintf F.err_formatter "@[<v 2>Post-state : @,";
+          L.err "================================@\n@."
-          Dom.Mem.pp F.err_formatter post;
-          F.fprintf F.err_formatter "@]@.";
-          F.fprintf F.err_formatter "================================@.@."
         end
 
   let exec_instr
@@ -317,10 +319,10 @@ struct
           let offset = ArrayBlk.offsetof arr in
           let idx = (if is_plus then Itv.plus else Itv.minus) offset idx in
           (if Config.bo_debug >= 2 then
-             (F.fprintf F.err_formatter "@[<v 2>Add condition :@,";
+             (L.err "@[<v 2>Add condition :@,";
-              F.fprintf F.err_formatter "array: %a@," ArrayBlk.pp arr;
+              L.err "array: %a@," ArrayBlk.pp arr;
-              F.fprintf F.err_formatter "  idx: %a@," Itv.pp idx;
+              L.err "  idx: %a@," Itv.pp idx;
-              F.fprintf F.err_formatter "@]@."));
+              L.err "@]@."));
           if size <> Itv.bot && idx <> Itv.bot then
             Dom.ConditionSet.add_bo_safety pname loc site ~size ~idx cond_set
           else cond_set
@@ -344,15 +346,12 @@ struct
   let print_debug_info : Sil.instr -> Dom.Mem.astate -> Dom.ConditionSet.t -> unit
     = fun instr pre cond_set ->
       if Config.bo_debug >= 2 then
-        (F.fprintf F.err_formatter "@.@.================================@.";
+        (L.err "@\n@\n================================@\n";
-         F.fprintf F.err_formatter "@[<v 2>Pre-state : @,";
+         L.err "@[<v 2>Pre-state : @,%a" Dom.Mem.pp pre;
-         Dom.Mem.pp F.err_formatter pre;
+         L.err "@]@\n@\n%a" (Sil.pp_instr Pp.text) instr;
-         F.fprintf F.err_formatter "@]@.@.";
+         L.err "@[<v 2>@\n@\n%a" Dom.ConditionSet.pp cond_set;
-         Sil.pp_instr Pp.text F.err_formatter instr;
+         L.err "@]@\n";
-         F.fprintf F.err_formatter "@[<v 2>@.@.";
+         L.err "================================@\n@.")
-         Dom.ConditionSet.pp F.err_formatter cond_set;
-         F.fprintf F.err_formatter "@]@.";
-         F.fprintf F.err_formatter "================================@.@.")
 
   let collect_instr
     : extras ProcData.t -> CFG.node -> Dom.ConditionSet.t * Dom.Mem.astate
@@ -446,10 +445,9 @@ let compute_post
 
 let print_summary : Typ.Procname.t -> Dom.Summary.t -> unit
   = fun proc_name s ->
-    F.fprintf F.err_formatter "@.@[<v 2>Summary of %a :@,"
+    L.err "@\n@[<v 2>Summary of %a :@,%a@]@."
-      Typ.Procname.pp proc_name;
+      Typ.Procname.pp proc_name
-    Dom.Summary.pp_summary F.err_formatter s;
+      Dom.Summary.pp_summary s
-    F.fprintf F.err_formatter "@]@."
 
 let checker : Callbacks.proc_callback_args -> Specs.summary
   = fun ({ summary } as callback) ->

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -604,9 +604,9 @@ struct
 
   let pp : F.formatter -> t -> unit
     = fun fmt x ->
-      F.fprintf fmt "Stack :@,";
+      F.fprintf fmt "Stack:@;";
-      F.fprintf fmt "%a@," Stack.pp x.stack;
+      F.fprintf fmt "%a@;" Stack.pp x.stack;
-      F.fprintf fmt "Heap :@,";
+      F.fprintf fmt "Heap:@;";
       F.fprintf fmt "%a" Heap.pp x.heap
 
   let pp_summary : F.formatter -> t -> unit
@@ -668,7 +668,12 @@ struct
     = fun ploc v s ->
       if can_strong_update ploc
       then strong_update_heap ploc v s
-      else weak_update_heap ploc v s
+      else
+        let () =
+          if Config.bo_debug >= 3 then
+            L.err "Weak update for %a <- %a@." PowLoc.pp ploc Val.pp v
+        in
+        weak_update_heap ploc v s
 end
 
 module Mem = struct