[inferbo] Improve division on constant

Reviewed By: mbouaziz, jvillard

Differential Revision: D12921835

fbshipit-source-id: 9d0e85696

infer/src/bufferoverrun/bounds.ml

@@ -750,6 +750,8 @@ module Bound = struct
         Some (if NonZeroInt.is_positive n then MInf else PInf)
     | PInf ->
         Some (if NonZeroInt.is_positive n then PInf else MInf)
+    | Linear (c, x') when SymLinear.is_zero x' ->
+        Some (Linear (Z.(c / (n :> Z.t)), SymLinear.zero))
     | Linear (c, x') when NonZeroInt.is_multiple c n -> (
       match SymLinear.exact_div_const_exn x' n with
       | x'' ->

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

@@ -307,6 +307,34 @@ void minmax_div_const_Bad(int n) {
   }
 }
 
+void div_const_Good() {
+  int a[3];
+  int x = 5 / 2;
+  a[x] = 0;
+}
+
+void div_const_Bad() {
+  int a[2];
+  int x = 5 / 2;
+  a[x] = 0;
+}
+
+void div_const2_FP(int n) {
+  int a[1];
+  int x = (n * 2 + 1) / 2;
+  a[x] = 0;
+}
+
+void minmax_div_const2_Good() {
+  div_const2(-1);
+  div_const2(0);
+}
+
+void minmax_div_const2_Bad_FN() {
+  div_const2(1);
+  div_const2(-2);
+}
+
 uint32_t unknown_nat() {
   uint32_t x = unknown_function();
   if (x >= 0) {

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

@@ -5,6 +5,8 @@ codetoanalyze/c/bufferoverrun/arith.c, band_positive_Bad, 6, BUFFER_OVERRUN_L2,
 codetoanalyze/c/bufferoverrun/arith.c, band_positive_constant_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 2 Size: 2]
 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, div_const2_FP, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [ArrayDeclaration,Parameter: n,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: 1]
+codetoanalyze/c/bufferoverrun/arith.c, div_const_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 2 Size: 2]
 codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_Bad, 4, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (2000000000 + 2000000000):signed32]
 codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_Bad, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
 codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_l2_Bad, 7, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Assignment,Binop: ([0, 2000000000] + [0, 2000000000]):signed32]

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

@@ -167,10 +167,8 @@ codetoanalyze/c/performance/switch_continue.c, test_switch, 11, EXPENSIVE_EXECUT
 codetoanalyze/c/performance/switch_continue.c, test_switch, 17, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 602, degree = 0]
 codetoanalyze/c/performance/switch_continue.c, test_switch, 19, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 602, degree = 0]
 codetoanalyze/c/performance/switch_continue.c, unroll_loop_FP, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
-codetoanalyze/c/performance/switch_continue.c, unroll_loop_FP, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Parameter: n,Binop: (n + [-oo, +oo]):signed32]
 codetoanalyze/c/performance/switch_continue.c, unroll_loop_FP, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32]
 codetoanalyze/c/performance/switch_continue.c, unroll_loop_FP, 9, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []
-codetoanalyze/c/performance/switch_continue.c, unroll_loop_FP, 15, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Parameter: n,Assignment,Binop: ([-oo, +oo] - 1):signed32]
 codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 6 * m.ub + 2 * (1+max(0, m.ub)), degree = 1]
 codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 6 * m.ub + 2 * (1+max(0, m.ub)), degree = 1]
 codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 12 * m.ub + 4 * (1+max(0, m.ub)), degree = 1]