[inferbo] preciser widening of bound

Summary:
It improves the precision of widening operations of interval:
upper_bound_widen (min(n, s), s) = s
lower_bound_widen (max(n, s), s) = s

Reviewed By: mbouaziz

Differential Revision: D8038941

fbshipit-source-id: 61b10cb

infer/src/bufferoverrun/itv.ml

@@ -366,6 +366,16 @@ module SymLinear = struct
    fun x -> match get_mone_symbol_opt x with Some _ -> true | None -> false
 
 
+  let is_one_symbol_of : Symbol.t -> t -> bool =
+   fun s x ->
+    Option.value_map (get_one_symbol_opt x) ~default:false ~f:(fun s' -> Symbol.equal s s')
+
+
+  let is_mone_symbol_of : Symbol.t -> t -> bool =
+   fun s x ->
+    Option.value_map (get_mone_symbol_opt x) ~default:false ~f:(fun s' -> Symbol.equal s s')
+
+
   let get_symbols : t -> Symbol.t list =
    fun x -> M.fold (fun symbol _coeff acc -> symbol :: acc) x []
 end
@@ -793,6 +803,12 @@ module Bound = struct
     match (x, y) with
     | PInf, _ | _, PInf ->
         L.(die InternalError) "Lower bound cannot be +oo."
+    | MinMax (n1, Plus, Max, _, s1), Linear (n2, s2)
+      when Int.equal n1 n2 && SymLinear.is_one_symbol_of s1 s2 ->
+        y
+    | MinMax (n1, Minus, Min, _, s1), Linear (n2, s2)
+      when Int.equal n1 n2 && SymLinear.is_mone_symbol_of s1 s2 ->
+        y
     | _ ->
         if le x y then x else MInf
 
@@ -802,6 +818,12 @@ module Bound = struct
     match (x, y) with
     | MInf, _ | _, MInf ->
         L.(die InternalError) "Upper bound cannot be -oo."
+    | MinMax (n1, Plus, Min, _, s1), Linear (n2, s2)
+      when Int.equal n1 n2 && SymLinear.is_one_symbol_of s1 s2 ->
+        y
+    | MinMax (n1, Minus, Max, _, s1), Linear (n2, s2)
+      when Int.equal n1 n2 && SymLinear.is_mone_symbol_of s1 s2 ->
+        y
     | _ ->
         if le y x then x else PInf
 

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

@@ -38,3 +38,27 @@ void for_loop() {
     a[i] = 'a'; /* BUG */
   }
 }
+
+void nop() { int k = 0; }
+
+int two_loops(int m) {
+  for (int i = 0; i < m; i++) {
+    nop();
+  }
+  for (int j = 0; j < m; j++) {
+    nop();
+  }
+  return m;
+}
+
+void call_two_loops_Good() {
+  int a[10];
+  int m = 5;
+  a[two_loops(m)] = 1;
+}
+
+void call_two_loops_Bad() {
+  int a[10];
+  int m = 15;
+  a[two_loops(m)] = 1;
+}

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

@@ -17,6 +17,7 @@ codetoanalyze/c/bufferoverrun/duplicates.c, tsa_two_alarms_Bad, 0, BUFFER_OVERRU
 codetoanalyze/c/bufferoverrun/duplicates.c, tsa_two_alarms_Bad, 0, BUFFER_OVERRUN_L1, ERROR, [Call,ArrayDeclaration,Parameter: n,ArrayAccess: Offset: [1, 1] Size: [1, 1] by call to `two_symbolic_accesses()` ]
 codetoanalyze/c/bufferoverrun/external.c, extern_bad, 5, BUFFER_OVERRUN_U5, ERROR, [Unknown value from: lib,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/c/bufferoverrun/external.c, extern_bad, 10, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [30, 30] Size: [10, 10]]
+codetoanalyze/c/bufferoverrun/for_loop.c, call_two_loops_Bad, 3, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: m,Assignment,Return,ArrayAccess: Offset: [15, 15] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN_L3, ERROR, [Call,ArrayDeclaration,Assignment,Assignment,Return,Assignment,Assignment,ArrayAccess: Offset: [0, 9] Size: [5, 10]]
 codetoanalyze/c/bufferoverrun/function_call.c, call_by_arr_bad, 3, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: [-1, -1] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/function_call.c, call_by_ptr_bad, 4, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: [-1, -1] Size: [10, 10]]

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

@@ -49,10 +49,12 @@ codetoanalyze/c/performance/instantiate.c, do_n_times, 1, EXPENSIVE_EXECUTION_TI
 codetoanalyze/c/performance/instantiate.c, do_n_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 3 + 6 * s$1]
 codetoanalyze/c/performance/invariant.c, do_k_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 5 + 5 * s$1^2]
 codetoanalyze/c/performance/invariant.c, do_k_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 5 + 5 * s$1^2]
-codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 0, INFINITE_EXECUTION_TIME_CALL, ERROR, []
 codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 3, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 4 + 6 * s$1]
 codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 4, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 4 + 6 * s$1]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 6, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 8 + 12 * s$1]
 codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 6, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 6 + 6 * s$1]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 7, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 8 + 12 * s$1]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 9, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 10 + 12 * s$1]
 codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 4 + 6 * s$1]
 codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 3, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 4 + 6 * s$1]
 codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 5, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 6 + 6 * s$1]

infer/tests/codetoanalyze/c/performance/two_loops_symbolic.c

@@ -8,8 +8,6 @@
  */
 void nop() { int k = 0; }
 
-/* we report infinity after the first loop, due to the problem in prune node.
- * Instead, we should obtain the appropriate bounds for the two loops */
 int two_loops_symb(int m) {
   int p = 10;
 
@@ -22,8 +20,6 @@ int two_loops_symb(int m) {
   return p;
 }
 
-/* we report the appropriate bounds for the two loops if the loops are over two
- * different arguments */
 int two_loops_symb_diff(int m, int k) {
   int p = 10;
   for (int i = 0; i < m; i++) {