diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index 88343604c..391fe2e4e 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml @@ -416,10 +416,18 @@ module ConditionTrace = struct fun ct -> if has_unknown ct then Some IssueType.buffer_overrun_u5 else None end +module Reported = struct + type t = IssueType.t [@@deriving compare] + + let make issue_type = issue_type + + let equal = [%compare.equal : t] +end + module ConditionWithTrace = struct - type t = {cond: Condition.t; trace: ConditionTrace.t} + type t = {cond: Condition.t; trace: ConditionTrace.t; reported: Reported.t option} - let make cond trace = {cond; trace} + let make cond trace = {cond; trace; reported= None} let pp fmt {cond; trace} = F.fprintf fmt "%a %a" Condition.pp cond ConditionTrace.pp trace @@ -457,7 +465,7 @@ module ConditionWithTrace = struct ConditionTrace.make_call_and_subst ~traces_caller ~caller_pname ~callee_pname location cwt.trace in - Some {cond; trace} + Some {cond; trace; reported= cwt.reported} let set_buffer_overrun_u5 {cond; trace} issue_type = @@ -470,11 +478,34 @@ module ConditionWithTrace = struct else issue_type + let check_aux cwt = + let {report_issue_type; propagate} as checked = Condition.check cwt.cond in + match report_issue_type with + | None -> + checked + | Some issue_type -> + let issue_type = set_buffer_overrun_u5 cwt issue_type in + (* Only report if the precision has improved. + This is approximated by: only report if the issue_type has changed. *) + let report_issue_type = + match cwt.reported with + | Some reported when Reported.equal reported issue_type -> + (* already reported and the precision hasn't improved *) None + | _ -> + (* either never reported or already reported but the precision has improved *) + Some issue_type + in + {report_issue_type; propagate} + + let check ~report cwt = - let {report_issue_type; propagate} = Condition.check cwt.cond in - report_issue_type |> Option.map ~f:(set_buffer_overrun_u5 cwt) - |> Option.iter ~f:(report cwt.cond cwt.trace) ; - propagate + let {report_issue_type; propagate} = check_aux cwt in + match report_issue_type with + | Some issue_type -> + report cwt.cond cwt.trace issue_type ; + if propagate then Some {cwt with reported= Some (Reported.make issue_type)} else None + | None -> + Option.some_if propagate cwt let forget_locs locs cwt = {cwt with cond= Condition.forget_locs locs cwt.cond} @@ -565,7 +596,7 @@ module ConditionSet = struct List.fold condset ~f:subst_add_cwt ~init:[] - let check_all ~report condset = List.filter condset ~f:(ConditionWithTrace.check ~report) + let check_all ~report condset = List.filter_map condset ~f:(ConditionWithTrace.check ~report) let pp_summary : F.formatter -> t -> unit = fun fmt condset -> diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c b/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c index a1b7fbf42..d56344c41 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c @@ -120,21 +120,25 @@ void l5_external_Warn_Bad() { a[unknown_function()] = 0; } -int s2_symbolic_widened_Bad(int n) { +void s2_symbolic_widened_Bad(int n) { int a[n]; for (int i = n; less_than(i, 2 * n); i++) { a[i] = 0; } } -int s2_symbolic_widened_Good_FP(int n) { +void s2_symbolic_widened_Good_FP(int n) { int a[n]; for (int i = n; less_than(i, n); i++) { a[i] = 0; } } -int l1_call_to_s2_symbolic_widened_Bad() { s2_symbolic_widened_Bad(1); } +// Do not report as it was already reported in the callee with the same issue +// type +void call_s2_symbolic_widened_Silenced(int m) { s2_symbolic_widened_Bad(m); } + +void l1_call_to_s2_symbolic_widened_Bad() { s2_symbolic_widened_Bad(1); } void may_underrun_symbolic_Nowarn_Good(int n) { int a[n]; diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index ff44b75ce..497cdfc92 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -33,9 +33,7 @@ codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 6, BUFFER_OVERRUN_L codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_goo, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_lI, 2, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Call,Assignment,Return,Assignment,Return,Assignment,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [0, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_uI_FP, 0, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Parameter: bi,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [-1+max(1, bi.lb), -1+max(1, bi.ub)] Size: [0, +oo]] -codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM_u_FP, 5, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Call,Parameter: bi,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [-1+max(1, t[*].bI.lb), -1+max(1, t[*].bI.ub)] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good, 5, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Call,Call,Call,Parameter: bi,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [0, +oo] Size: [0, +oo]] -codetoanalyze/cpp/bufferoverrun/repro1.cpp, ral_FP, 3, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Call,Call,Parameter: bi,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [-1+max(1, t[*].bI.lb), -1+max(1, t[*].bI.ub)] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Call,Call,ArrayDeclaration,Assignment,Parameter: i,ArrayAccess: Offset: v[*]._size Size: v[*]._size by call to `int_vector_access_at` ] codetoanalyze/cpp/bufferoverrun/std_array.cpp, normal_array_bo, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 42 Size: 42] codetoanalyze/cpp/bufferoverrun/std_array.cpp, std_array_bo_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 42 Size: 42]