[inferbo] Do not re-report issues if the precision hasn't improved

Reviewed By: Julek

Differential Revision: D9400004

fbshipit-source-id: 916de6db1

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
+    let {report_issue_type; propagate} = check_aux cwt in
-    report_issue_type |> Option.map ~f:(set_buffer_overrun_u5 cwt)
+    match report_issue_type with
-    |> Option.iter ~f:(report cwt.cond cwt.trace) ;
+    | Some issue_type ->
-    propagate
+        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 ->

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];

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<TFM>_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<TFM>_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<TFM>_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]