[inferbo] Widening threshold by comparison

Summary:
This diff adds a constant to the set of widening thresholds if the
constant is compared to an abstract value in condition expressions.
Each abstract value has its own set of thresholds.

Reviewed By: mbouaziz

Differential Revision: D14147150

fbshipit-source-id: ca0db34d4

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -24,9 +24,16 @@ type eval_sym_trace =
   ; trace_of_sym: Symb.Symbol.t -> Trace.Set.t
   ; eval_locpath: PowLoc.eval_locpath }
 
+module ItvThresholds = AbstractDomain.FiniteSet (struct
+  include Z
+
+  let pp = pp_print
+end)
+
 module Val = struct
   type t =
     { itv: Itv.t
+    ; itv_thresholds: ItvThresholds.t
     ; sym: Relation.Sym.t
     ; powloc: PowLoc.t
     ; arrayblk: ArrayBlk.t
@@ -37,6 +44,7 @@ module Val = struct
 
   let bot : t =
     { itv= Itv.bot
+    ; itv_thresholds= ItvThresholds.empty
     ; sym= Relation.Sym.bot
     ; powloc= PowLoc.bot
     ; arrayblk= ArrayBlk.bot
@@ -47,6 +55,10 @@ module Val = struct
 
 
   let pp fmt x =
+    let itv_thresholds_pp fmt itv_thresholds =
+      if Config.bo_debug >= 3 && not (ItvThresholds.is_empty itv_thresholds) then
+        F.fprintf fmt " (thresholds:%a)" ItvThresholds.pp itv_thresholds
+    in
     let relation_sym_pp fmt sym =
       if Option.is_some Config.bo_relational_domain then F.fprintf fmt ", %a" Relation.Sym.pp sym
     in
@@ -54,9 +66,9 @@ module Val = struct
       if Config.bo_debug >= 1 then F.fprintf fmt ", %a" TraceSet.pp traces
     in
     let represents_multiple_values_str = if x.represents_multiple_values then "M" else "" in
-    F.fprintf fmt "%s(%a%a, %a, %a%a%a%a)" represents_multiple_values_str Itv.pp x.itv
-      relation_sym_pp x.sym PowLoc.pp x.powloc ArrayBlk.pp x.arrayblk relation_sym_pp x.offset_sym
-      relation_sym_pp x.size_sym trace_pp x.traces
+    F.fprintf fmt "%s(%a%a%a, %a, %a%a%a%a)" represents_multiple_values_str Itv.pp x.itv
+      itv_thresholds_pp x.itv_thresholds relation_sym_pp x.sym PowLoc.pp x.powloc ArrayBlk.pp
+      x.arrayblk relation_sym_pp x.offset_sym relation_sym_pp x.size_sym trace_pp x.traces
 
 
   let sets_represents_multiple_values : represents_multiple_values:bool -> t -> t =
@@ -67,6 +79,7 @@ module Val = struct
    fun ~callee_pname ~location ->
     let traces = Trace.(Set.singleton_final location (UnknownFrom callee_pname)) in
     { itv= Itv.top
+    ; itv_thresholds= ItvThresholds.empty
     ; sym= Relation.Sym.top
     ; powloc= PowLoc.unknown
     ; arrayblk= ArrayBlk.unknown
@@ -80,6 +93,7 @@ module Val = struct
     if phys_equal lhs rhs then true
     else
       Itv.( <= ) ~lhs:lhs.itv ~rhs:rhs.itv
+      && ItvThresholds.( <= ) ~lhs:lhs.itv_thresholds ~rhs:rhs.itv_thresholds
       && Relation.Sym.( <= ) ~lhs:lhs.sym ~rhs:rhs.sym
       && PowLoc.( <= ) ~lhs:lhs.powloc ~rhs:rhs.powloc
       && ArrayBlk.( <= ) ~lhs:lhs.arrayblk ~rhs:rhs.arrayblk
@@ -91,7 +105,12 @@ module Val = struct
   let widen ~prev ~next ~num_iters =
     if phys_equal prev next then prev
     else
-      { itv= Itv.widen ~prev:prev.itv ~next:next.itv ~num_iters
+      let itv_thresholds = ItvThresholds.join prev.itv_thresholds next.itv_thresholds in
+      { itv=
+          Itv.widen_thresholds
+            ~thresholds:(ItvThresholds.elements itv_thresholds)
+            ~prev:prev.itv ~next:next.itv ~num_iters
+      ; itv_thresholds
       ; sym= Relation.Sym.widen ~prev:prev.sym ~next:next.sym ~num_iters
       ; powloc= PowLoc.widen ~prev:prev.powloc ~next:next.powloc ~num_iters
       ; arrayblk= ArrayBlk.widen ~prev:prev.arrayblk ~next:next.arrayblk ~num_iters
@@ -107,6 +126,7 @@ module Val = struct
     if phys_equal x y then x
     else
       { itv= Itv.join x.itv y.itv
+      ; itv_thresholds= ItvThresholds.join x.itv_thresholds y.itv_thresholds
       ; sym= Relation.Sym.join x.sym y.sym
       ; powloc= PowLoc.join x.powloc y.powloc
       ; arrayblk= ArrayBlk.join x.arrayblk y.arrayblk
@@ -192,6 +212,7 @@ module Val = struct
   let lift_itv : (Itv.t -> Itv.t -> Itv.t) -> ?f_trace:_ -> t -> t -> t =
    fun f ?f_trace x y ->
     let itv = f x.itv y.itv in
+    let itv_thresholds = ItvThresholds.join x.itv_thresholds y.itv_thresholds in
     let traces =
       match f_trace with
       | Some f_trace ->
@@ -205,7 +226,7 @@ module Val = struct
         | true, true | false, false ->
             TraceSet.join x.traces y.traces )
     in
-    {bot with itv; traces}
+    {bot with itv; itv_thresholds; traces}
 
 
   let lift_cmp_itv : (Itv.t -> Itv.t -> Boolean.t) -> Boolean.EqualOrder.t -> t -> t -> t =
@@ -291,13 +312,23 @@ module Val = struct
       (Itv.t -> Itv.t -> Itv.t) -> (ArrayBlk.t -> ArrayBlk.t -> ArrayBlk.t) -> t -> t -> t =
    fun f g x y ->
     let itv = f x.itv y.itv in
+    let itv_thresholds =
+      Option.value_map (Itv.is_const y.itv) ~default:x.itv_thresholds ~f:(fun z ->
+          x.itv_thresholds
+          |> ItvThresholds.add Z.(z - one)
+          |> ItvThresholds.add z
+          |> ItvThresholds.add Z.(z + one) )
+    in
     let arrayblk = g x.arrayblk y.arrayblk in
-    if phys_equal itv x.itv && phys_equal arrayblk x.arrayblk then
-      (* x hasn't changed, don't join traces *)
+    if
+      phys_equal itv x.itv
+      && phys_equal itv_thresholds x.itv_thresholds
+      && phys_equal arrayblk x.arrayblk
+    then (* x hasn't changed, don't join traces *)
       x
     else
       warn_against_pruning_multiple_values
-        {x with itv; arrayblk; traces= TraceSet.join x.traces y.traces}
+        {x with itv; itv_thresholds; arrayblk; traces= TraceSet.join x.traces y.traces}
 
 
   let prune_eq_zero : t -> t = lift_prune1 Itv.prune_eq_zero

infer/tests/codetoanalyze/c/bufferoverrun/for_loop.c

@@ -96,3 +96,41 @@ void call_initialize_arr_Bad() {
   int arr[10];
   initialize_arr(arr, 20);
 }
+
+void threshold_by_comparison_1_Good() {
+  int arr[100];
+  for (int i = 0; i != 100; i++) {
+    arr[i] = 0;
+  }
+}
+
+void threshold_by_comparison_1_Bad() {
+  int arr[50];
+  for (int i = 0; i != 100; i++) {
+    arr[i] = 0;
+  }
+}
+
+void threshold_by_comparison_2_Good() {
+  int arr[100];
+  int j = 0;
+  while (1) { // widening threshold for j should be 99, not 100
+    j++;
+    if (j == 100) {
+      j = 0;
+    }
+    arr[j] = 0;
+  }
+}
+
+void threshold_by_comparison_2_Bad() {
+  int arr[50];
+  int j = 0;
+  while (1) { // widening threshold for j should be 99, not 100
+    j++;
+    if (j == 100) {
+      j = 0;
+    }
+    arr[j] = 0;
+  }
+}

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

@@ -102,6 +102,10 @@ codetoanalyze/c/bufferoverrun/external.c, extern_bad, 10, BUFFER_OVERRUN_L1, no_
 codetoanalyze/c/bufferoverrun/for_loop.c, call_initialize_arr_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Array declaration,Call,<Offset trace>,Assignment,<Length trace>,Parameter `*arr`,Array access: Offset: [0, 19] Size: 10 by call to `initialize_arr` ]
 codetoanalyze/c/bufferoverrun/for_loop.c, call_two_loops_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,Call,Parameter `m`,Assignment,<Length trace>,Array declaration,Array access: Offset: 15 Size: 10]
 codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN_L3, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Call,Array declaration,Assignment,Assignment,Assignment,Array access: Offset: [0, 9] Size: [5, 10]]
+codetoanalyze/c/bufferoverrun/for_loop.c, threshold_by_comparison_1_Bad, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 99] Size: 50]
+codetoanalyze/c/bufferoverrun/for_loop.c, threshold_by_comparison_2_Bad, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
+codetoanalyze/c/bufferoverrun/for_loop.c, threshold_by_comparison_2_Bad, 8, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 99] Size: 50]
+codetoanalyze/c/bufferoverrun/for_loop.c, threshold_by_comparison_2_Good, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/function_call.c, call_access_index_4_on_local_array_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Length trace>,Parameter `*arr`,Array access: Offset: 4 Size: 4 by call to `access_index_4` ]
 codetoanalyze/c/bufferoverrun/function_call.c, call_access_index_4_on_malloced_array_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,<Length trace>,Parameter `*arr`,Array access: Offset: 4 Size: 4 by call to `access_index_4` ]
 codetoanalyze/c/bufferoverrun/function_call.c, call_by_arr_bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Array declaration,Array access: Offset: -1 Size: 10]

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

@@ -26,7 +26,7 @@ codetoanalyze/c/performance/cost_test.c, loop2_bad, 2, EXPENSIVE_EXECUTION_TIME_
 codetoanalyze/c/performance/cost_test.c, main_bad, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 214, degree = 0]
 codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 6 ⋅ (-m + 20), degree = 1,{-m + 20},Loop at line 117, column 3]
 codetoanalyze/c/performance/cost_test_deps.c, if_bad_loop, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 235, degree = 0]
-codetoanalyze/c/performance/cost_test_deps.c, if_bad_loop, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([3, +oo] + 1):signed32]
+codetoanalyze/c/performance/cost_test_deps.c, if_bad_loop, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
 codetoanalyze/c/performance/cost_test_deps.c, loop_despite_inferbo, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1307, degree = 0]
 codetoanalyze/c/performance/cost_test_deps.c, loop_no_dep1, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 609, degree = 0]
 codetoanalyze/c/performance/cost_test_deps.c, loop_no_dep1, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]

infer/tests/codetoanalyze/java/performance/issues.exp

@@ -68,7 +68,7 @@ codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Co
 codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.main_bad():int, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 205, degree = 0]
 codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.if_bad(int):void, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 613, degree = 0]
 codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.if_bad_loop():int, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 201, degree = 0]
-codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.if_bad_loop():int, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([3, +oo] + 1):signed32]
+codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.if_bad_loop():int, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
 codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.loop_despite_inferbo(int):int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1303, degree = 0]
 codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.loop_no_dep1(int):int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 605, degree = 0]
 codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.loop_no_dep1(int):int, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]