diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index b1dac2962..1bf7c4293 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -87,11 +87,10 @@ struct = fun params mem loc -> match params with | (e, _) :: _ -> - (* TODO: only print when debug mode? *) - F.fprintf F.err_formatter "@[=== Infer Print === at %a@," - Location.pp loc; - Dom.Val.pp F.err_formatter (Sem.eval e mem loc); - F.fprintf F.err_formatter "@]"; + if Config.bo_debug >= 1 then + L.err "@[=== Infer Print === at %a@,%a@]%!" + Location.pp loc + Dom.Val.pp (Sem.eval e mem loc); 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 "@.@.================================@."; - F.fprintf F.err_formatter "@[Pre-state : @,"; - Dom.Mem.pp F.err_formatter pre; - F.fprintf F.err_formatter "@]@.@."; - Sil.pp_instr Pp.text F.err_formatter instr; - F.fprintf F.err_formatter "@.@."; - F.fprintf F.err_formatter "@[Post-state : @,"; - Dom.Mem.pp F.err_formatter post; - F.fprintf F.err_formatter "@]@."; - F.fprintf F.err_formatter "================================@.@." + L.err "@\n@\n================================@\n"; + L.err "@[Pre-state : @,%a" Dom.Mem.pp pre; + L.err "@]@\n@\n%a" (Sil.pp_instr Pp.text) instr; + L.err "@\n@\n"; + L.err "@[Post-state : @,%a" Dom.Mem.pp post; + L.err "@]@\n"; + L.err "================================@\n@." 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 "@[Add condition :@,"; - F.fprintf F.err_formatter "array: %a@," ArrayBlk.pp arr; - F.fprintf F.err_formatter " idx: %a@," Itv.pp idx; - F.fprintf F.err_formatter "@]@.")); + (L.err "@[Add condition :@,"; + L.err "array: %a@," ArrayBlk.pp arr; + L.err " idx: %a@," Itv.pp idx; + 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 "@.@.================================@."; - F.fprintf F.err_formatter "@[Pre-state : @,"; - Dom.Mem.pp F.err_formatter pre; - F.fprintf F.err_formatter "@]@.@."; - Sil.pp_instr Pp.text F.err_formatter instr; - F.fprintf F.err_formatter "@[@.@."; - Dom.ConditionSet.pp F.err_formatter cond_set; - F.fprintf F.err_formatter "@]@."; - F.fprintf F.err_formatter "================================@.@.") + (L.err "@\n@\n================================@\n"; + L.err "@[Pre-state : @,%a" Dom.Mem.pp pre; + L.err "@]@\n@\n%a" (Sil.pp_instr Pp.text) instr; + L.err "@[@\n@\n%a" Dom.ConditionSet.pp cond_set; + L.err "@]@\n"; + L.err "================================@\n@.") 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 "@.@[Summary of %a :@," - Typ.Procname.pp proc_name; - Dom.Summary.pp_summary F.err_formatter s; - F.fprintf F.err_formatter "@]@." + L.err "@\n@[Summary of %a :@,%a@]@." + Typ.Procname.pp proc_name + Dom.Summary.pp_summary s let checker : Callbacks.proc_callback_args -> Specs.summary = fun ({ summary } as callback) -> diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index a4dd8ddea..6c9cf7a27 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -125,7 +125,7 @@ let invalid : t -> bool let to_string : t -> string = fun c -> let c = set_size_pos c in - "Offset : " ^ Itv.to_string c.idx ^ " Size : " ^ Itv.to_string c.size + "Offset: " ^ Itv.to_string c.idx ^ " Size: " ^ Itv.to_string c.size ^ " @ " ^ string_of_location c.loc ^ (match c.trace with Inter (_, pname, _) -> @@ -604,14 +604,14 @@ struct let pp : F.formatter -> t -> unit = fun fmt x -> - F.fprintf fmt "Stack :@,"; - F.fprintf fmt "%a@," Stack.pp x.stack; - F.fprintf fmt "Heap :@,"; + F.fprintf fmt "Stack:@;"; + F.fprintf fmt "%a@;" Stack.pp x.stack; + F.fprintf fmt "Heap:@;"; F.fprintf fmt "%a" Heap.pp x.heap let pp_summary : F.formatter -> t -> unit = fun fmt x -> - F.fprintf fmt "@[Parameters :@,"; + F.fprintf fmt "@[Parameters:@,"; F.fprintf fmt "%a" Heap.pp_summary x.heap ; F.fprintf fmt "@]" @@ -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 diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 9813a2918..74aaa4495 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -1,12 +1,12 @@ -codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 16, BUFFER_OVERRUN, [Offset : [0, 10] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/break_continue_return.c:29:5] -codetoanalyze/c/bufferoverrun/do_while.c, do_while, 2, BUFFER_OVERRUN, [Offset : [0, +oo] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/do_while.c:18:5 by call `do_while_sub()` ] -codetoanalyze/c/bufferoverrun/do_while.c, do_while, 3, BUFFER_OVERRUN, [Offset : [0, +oo] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/do_while.c:18:5 by call `do_while_sub()` ] -codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN, [Offset : [0, 9] Size : [5, 10] @ codetoanalyze/c/bufferoverrun/for_loop.c:38:5] -codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN, [Offset : [20, 20] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/function_call.c:18:3 by call `arr_access()` ] -codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN, [Offset : [100, 100] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/function_call.c:17:3 by call `arr_access()` ] -codetoanalyze/c/bufferoverrun/goto_loop.c, goto_loop, 11, BUFFER_OVERRUN, [Offset : [10, +oo] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/goto_loop.c:24:3] -codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN, [Offset : [0, 10] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/nested_loop.c:20:7] -codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN, [Offset : [0, +oo] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/nested_loop_with_label.c:19:5] -codetoanalyze/c/bufferoverrun/prune_alias.c, FP_prune_alias_exp_Ok, 4, BUFFER_OVERRUN, [Offset : [1, 1] Size : [1, 1] @ codetoanalyze/c/bufferoverrun/prune_alias.c:107:5] -codetoanalyze/c/bufferoverrun/trivial.c, trivial, 2, BUFFER_OVERRUN, [Offset : [10, 10] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/trivial.c:15:3] -codetoanalyze/c/bufferoverrun/while_loop.c, while_loop, 3, BUFFER_OVERRUN, [Offset : [0, +oo] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/while_loop.c:16:10] +codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 16, BUFFER_OVERRUN, [Offset: [0, 10] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/break_continue_return.c:29:5] +codetoanalyze/c/bufferoverrun/do_while.c, do_while, 2, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/do_while.c:18:5 by call `do_while_sub()` ] +codetoanalyze/c/bufferoverrun/do_while.c, do_while, 3, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/do_while.c:18:5 by call `do_while_sub()` ] +codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN, [Offset: [0, 9] Size: [5, 10] @ codetoanalyze/c/bufferoverrun/for_loop.c:38:5] +codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN, [Offset: [20, 20] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/function_call.c:18:3 by call `arr_access()` ] +codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN, [Offset: [100, 100] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/function_call.c:17:3 by call `arr_access()` ] +codetoanalyze/c/bufferoverrun/goto_loop.c, goto_loop, 11, BUFFER_OVERRUN, [Offset: [10, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/goto_loop.c:24:3] +codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN, [Offset: [0, 10] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/nested_loop.c:20:7] +codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/nested_loop_with_label.c:19:5] +codetoanalyze/c/bufferoverrun/prune_alias.c, FP_prune_alias_exp_Ok, 4, BUFFER_OVERRUN, [Offset: [1, 1] Size: [1, 1] @ codetoanalyze/c/bufferoverrun/prune_alias.c:107:5] +codetoanalyze/c/bufferoverrun/trivial.c, trivial, 2, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/trivial.c:15:3] +codetoanalyze/c/bufferoverrun/while_loop.c, while_loop, 3, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/while_loop.c:16:10] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 6f24ef3cf..ed798dc99 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -1 +1 @@ -codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN, [Offset : [10, 10] Size : [10, 10] @ codetoanalyze/cpp/bufferoverrun/trivial.cpp:15:3] +codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10] @ codetoanalyze/cpp/bufferoverrun/trivial.cpp:15:3]