[inferbo] Revise deduplication

Reviewed By: mbouaziz

Differential Revision: D12819709

fbshipit-source-id: db2cb99af

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -621,7 +621,7 @@ module Report = struct
             | Some callee_payload ->
                 let callee_pdesc = Summary.get_proc_desc callee_summary in
                 instantiate_cond tenv callee_pdesc params mem callee_payload location
-                |> PO.ConditionSet.join cond_set
+                |> PO.ConditionSet.merge cond_set
             | None ->
                 (* no inferbo payload *) cond_set )
           | None ->

infer/src/bufferoverrun/bufferOverrunProofObligations.ml

@@ -708,7 +708,7 @@ module ConditionWithTrace = struct
     else issue_type
 
 
-  let check_aux cwt =
+  let check cwt =
     let ({report_issue_type; propagate} as checked) = Condition.check cwt.cond in
     match report_issue_type with
     | None ->
@@ -728,14 +728,11 @@ module ConditionWithTrace = struct
         {report_issue_type; propagate}
 
 
-  let check ~report cwt =
-    let {report_issue_type; propagate} = check_aux cwt in
-    match report_issue_type with
-    | Some issue_type ->
+  let report ~report ((cwt, checked) as default) =
+    Option.value_map checked.report_issue_type ~default ~f:(fun 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
+        if checked.propagate then ({cwt with reported= Some (Reported.make issue_type)}, checked)
+        else default )
 
 
   let forget_locs locs cwt = {cwt with cond= Condition.forget_locs locs cwt.cond}
@@ -755,48 +752,54 @@ module ConditionSet = struct
 
   let empty = []
 
-  let try_merge ~existing ~new_ =
+  let try_merge ~existing:(existing_cwt, existing_checked) ~new_:(new_cwt, new_checked) =
     (* we don't want to remove issues that would end up in a higher bucket,
      e.g. [a, b] < [c, d] is subsumed by [a, +oo] < [c, d] but the latter is less precise *)
-    if ConditionWithTrace.have_similar_bounds existing new_ then
-      match ConditionWithTrace.xcompare ~lhs:existing ~rhs:new_ with
+    match (existing_checked.report_issue_type, new_checked.report_issue_type) with
+    | _, None ->
+        `AddAndStop
+    | Some existing_issue_type, Some new_issue_type
+      when IssueType.equal existing_issue_type new_issue_type
+           && ConditionWithTrace.have_similar_bounds existing_cwt new_cwt -> (
+      match ConditionWithTrace.xcompare ~lhs:existing_cwt ~rhs:new_cwt with
       | `LeftSubsumesRight ->
           `DoNotAddAndStop
       | `RightSubsumesLeft ->
           `RemoveExistingAndContinue
       | `NotComparable ->
-          `KeepExistingAndContinue
-    else `KeepExistingAndContinue
+          `KeepExistingAndContinue )
+    | _, _ ->
+        `KeepExistingAndContinue
 
 
   let join_one condset new_ =
-    let rec aux ~new_ acc ~same = function
+    let pp_cond fmt (cond, _) = ConditionWithTrace.pp fmt cond in
+    let rec aux acc ~same = function
       | [] ->
           if Config.bo_debug >= 3 then
-            L.(debug BufferOverrun Verbose)
-              "[InferboPO] Adding new condition %a@." ConditionWithTrace.pp new_ ;
+            L.d_printfln "[InferboPO] Adding new condition %a@." pp_cond new_ ;
           if same then new_ :: condset else new_ :: acc
       | existing :: rest as existings -> (
         match try_merge ~existing ~new_ with
+        | `AddAndStop ->
+            new_ :: (if same then condset else List.rev_append acc existings)
         | `DoNotAddAndStop ->
             if Config.bo_debug >= 3 then
-              L.(debug BufferOverrun Verbose)
-                "[InferboPO] Not adding condition %a (because of existing %a)@."
-                ConditionWithTrace.pp new_ ConditionWithTrace.pp existing ;
+              L.d_printfln "[InferboPO] Not adding condition %a (because of existing %a)@." pp_cond
+                new_ pp_cond existing ;
             if same then condset else List.rev_append acc existings
         | `RemoveExistingAndContinue ->
             if Config.bo_debug >= 3 then
-              L.(debug BufferOverrun Verbose)
-                "[InferboPO] Removing condition %a (because of new %a)@." ConditionWithTrace.pp
-                existing ConditionWithTrace.pp new_ ;
-            aux ~new_ acc ~same:false rest
+              L.d_printfln "[InferboPO] Removing condition %a (because of new %a)@." pp_cond
+                existing pp_cond new_ ;
+            aux acc ~same:false rest
         | `KeepExistingAndContinue ->
-            aux ~new_ (existing :: acc) ~same rest )
+            aux (existing :: acc) ~same rest )
     in
-    aux ~new_ [] ~same:true condset
+    aux [] ~same:true condset
 
 
-  let join condset1 condset2 = List.fold_left ~f:join_one condset1 ~init:condset2
+  let merge condset1 condset2 = List.rev_append condset1 condset2
 
   let add_opt location val_traces condset = function
     | None ->
@@ -804,7 +807,7 @@ module ConditionSet = struct
     | Some cond ->
         let trace = ConditionTrace.make location val_traces in
         let cwt = ConditionWithTrace.make cond trace in
-        join [cwt] condset
+        cwt :: condset
 
 
   let add_array_access location ~offset ~idx ~size ~is_collection_add ~idx_sym_exp ~size_sym_exp
@@ -834,12 +837,24 @@ module ConditionSet = struct
       | None ->
           condset
       | Some cwt ->
-          join_one condset cwt
+          cwt :: condset
     in
     List.fold condset ~f:subst_add_cwt ~init:[]
 
 
-  let check_all ~report condset = List.filter_map condset ~f:(ConditionWithTrace.check ~report)
+  let check_all ~report condset =
+    let condset = List.map condset ~f:(fun cwt -> (cwt, ConditionWithTrace.check cwt)) in
+    let conds_to_report, rest =
+      List.partition_tf condset ~f:(fun (_, {report_issue_type}) ->
+          Option.is_some report_issue_type )
+    in
+    let conds_reported =
+      List.fold conds_to_report ~init:[] ~f:join_one
+      |> List.map ~f:(ConditionWithTrace.report ~report)
+    in
+    List.rev_append conds_reported rest
+    |> List.filter_map ~f:(fun (cwt, {propagate}) -> Option.some_if propagate cwt)
+
 
   let pp_summary : F.formatter -> _ t0 -> unit =
    fun fmt condset ->

infer/src/bufferoverrun/bufferOverrunProofObligations.mli

@@ -59,7 +59,7 @@ module ConditionSet : sig
     -> t
     -> t
 
-  val join : t -> t -> t
+  val merge : t -> t -> t
 
   val subst :
        summary_t

infer/tests/codetoanalyze/c/bufferoverrun/arith.c

@@ -306,3 +306,32 @@ void minmax_div_const_Bad(int n) {
     int x = a[n / 8];
   }
 }
+
+uint32_t unknown_nat() {
+  uint32_t x = unknown_function();
+  if (x >= 0) {
+    return x;
+  } else {
+    return 0;
+  }
+}
+
+void two_safety_conditions2_Bad(uint32_t s) {
+  uint32_t x = unknown_nat();
+  uint32_t y, z;
+
+  if (unknown_function()) {
+    y = 0;
+  } else {
+    y = 80;
+  }
+  z = x + y; // integer overflow L5: [0, +oo] + [0, 80]
+
+  if (s >= 10 && s <= 20) {
+    z = x + s; // [0, +oo] + [max(10, s.lb), min(20, s.ub)]
+  }
+}
+
+void call_two_safety_conditions2_Bad() {
+  two_safety_conditions2_Bad(15); // integer overflow L5: [0, +oo] + 15
+}

infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c

@@ -241,3 +241,24 @@ void False_Issue_Type_l3_unknown_function_Bad() {
     }
   }
 }
+
+int mone_to_one() {
+  int x = unknown_function();
+  if (x >= -1 && x <= 1) {
+    return x;
+  } else {
+    return 0;
+  }
+}
+
+void two_safety_conditions(int n) {
+  char a[10];
+  int y = mone_to_one();
+  if (unknown_function()) {
+    a[n] = 0; // should be L1 when n=10
+  } else {
+    a[n + y] = 0; // should be L2 when n=10
+  }
+}
+
+void call_two_safety_conditions_l1_and_l2_Bad() { two_safety_conditions(10); }

infer/tests/codetoanalyze/c/bufferoverrun/issues.exp

@@ -1,3 +1,4 @@
+codetoanalyze/c/bufferoverrun/arith.c, call_two_safety_conditions2_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter: s,Binop: ([0, +oo] + 15):unsigned32 by call to `two_safety_conditions2_Bad` ]
 codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_ge1_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: x,Binop: (0 - 1):unsigned32 by call to `unsigned_prune_ge1_Good` ]
 codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_zero1_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: x,Binop: (0 - 1):unsigned32 by call to `unsigned_prune_zero1_Good` ]
 codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_zero2_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter: y,Assignment,Binop: ([-oo, 0] - 1):unsigned32 by call to `unsigned_prune_zero2_Good` ]
@@ -19,6 +20,7 @@ codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min2_Good_FP, 2, BUFFER_OVERR
 codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min3_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 25] Size: 20]
 codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 19] Size: 19]
 codetoanalyze/c/bufferoverrun/arith.c, plus_one_Bad, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: unknown_int,Assignment,Binop: ([-oo, 9223372036854775807] + 1):signed64]
+codetoanalyze/c/bufferoverrun/arith.c, two_safety_conditions2_Bad, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + [0, 80]):unsigned32]
 codetoanalyze/c/bufferoverrun/arith.c, use_int64_max_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 15 Size: 10]
 codetoanalyze/c/bufferoverrun/arith.c, use_uint64_max_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 15 Size: 10]
 codetoanalyze/c/bufferoverrun/array_content.c, array_min_index_from_one_FP, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
@@ -84,6 +86,8 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_negative_Bad, 0, INFER
 codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_negative_Good_FP, 0, INFERBO_ALLOC_MAY_BE_NEGATIVE, no_bucket, ERROR, [Call,Assignment,Return,Alloc: Length: [-5, 5]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, call_to_alloc_may_be_big2_is_big_Bad, 1, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Call,Parameter: n,Alloc: Length: [100000000, +oo] by call to `alloc_may_be_big2_Silenced` ]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, call_to_alloc_may_be_big2_is_big_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter: n,Binop: (100000000 + [0, +oo]):signed32 by call to `alloc_may_be_big2_Silenced` ]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, call_two_safety_conditions_l1_and_l2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: n,ArrayAccess: Offset: 10 Size: 10 by call to `two_safety_conditions` ]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, call_two_safety_conditions_l1_and_l2_Bad, 0, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: n,ArrayAccess: Offset: [9, 11] Size: 10 by call to `two_safety_conditions` ]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_call_to_s2_symbolic_widened_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Offset: [1, +oo] Size: 1 by call to `s2_symbolic_widened_Bad` ]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_call_to_s2_symbolic_widened_Bad, 0, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter: n,Assignment,Binop: ([1, +oo] + 1):signed32 by call to `s2_symbolic_widened_Bad` ]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_concrete_overrun_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10]
@@ -176,7 +180,8 @@ codetoanalyze/c/bufferoverrun/relation.c, FP_call_array_access_Ok, 0, BUFFER_OVE
 codetoanalyze/c/bufferoverrun/sizeof.c, FN_static_stride_bad, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
 codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
 codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 1 Size: 0]
-codetoanalyze/c/bufferoverrun/trivial.c, trivial, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10]
+codetoanalyze/c/bufferoverrun/trivial.c, malloc_zero_Bad, 2, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Alloc: Length: 0]
+codetoanalyze/c/bufferoverrun/trivial.c, trivial_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10]
 codetoanalyze/c/bufferoverrun/unreachable.c, FP_loop_once_intentional_good, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
 codetoanalyze/c/bufferoverrun/unreachable.c, FP_loop_with_break_good, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
 codetoanalyze/c/bufferoverrun/unreachable.c, FP_loop_with_exit_good, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []

infer/tests/codetoanalyze/c/bufferoverrun/trivial.c

@@ -7,7 +7,13 @@
  * LICENSE file in the root directory of this source tree.
  */
 
-void trivial() {
+void trivial_Bad() {
   int a[10];
   a[10] = 0; /* BUG */
 }
+
+void malloc_zero_Bad() {
+  char* x;
+  x = malloc(0);
+  x = malloc(1);
+}

infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp

@@ -35,6 +35,7 @@ codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call3_plus_params2_Ok, 0, BUFFE
 codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call3_plus_params_Ok, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: x,ArrayAccess: Offset: -1 Size: 5 by call to `plus_params` ]
 codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call_id_Ok, 4, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Assignment,Call,Assignment,Return,Assignment,ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: 5 Size: [0, 6]]
 codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call_loop_with_type_casting_Ok, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: data,Assignment,ArrayAccess: Offset: [2, +oo] (= [0, +oo] + 2) Size: 1 by call to `loop_with_type_casting` ]
+codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call_loop_with_type_casting_Ok, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: data,Assignment,ArrayAccess: Offset: [0, +oo] Size: 1 by call to `loop_with_type_casting` ]
 codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_loop2_Ok, 9, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Assignment,ArrayDeclaration,Assignment,ArrayAccess: Offset: [2, +oo] (= [0, +oo] + 2) Size: 12]
 codetoanalyze/cpp/bufferoverrun/relation.cpp, call2_loop_Bad, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: arr,ArrayAccess: Offset: [0, +oo] Size: 5 by call to `loop` ]
 codetoanalyze/cpp/bufferoverrun/relation.cpp, call2_plus_params2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: x,ArrayAccess: Offset: 11 Size: 5 by call to `plus_params2` ]