[inferbo] Check integer overflow when really need

Summary:
It avoids checking integer overflow when it definitely cannot happen.
For example, it does not check integer overflow of addition when one
of parameters is a negative number, or underflow of subtraction when
its first parameter is a positive number.

Reviewed By: mbouaziz

Differential Revision: D10446161

fbshipit-source-id: b8c86e1b2

infer/src/bufferoverrun/bufferOverrunProofObligations.ml

@@ -364,7 +364,31 @@ module BinaryOperationCondition = struct
     equal_binop binop Mult && (ItvPure.is_one lhs || ItvPure.is_one rhs)
 
 
-  let check {binop; typ; integer_widths; lhs; rhs} =
+  let should_check {binop; typ; lhs; rhs} =
+    let cannot_underflow, cannot_overflow =
+      match (binop, Typ.ikind_is_unsigned typ) with
+      | Plus, true ->
+          (true, false)
+      | Minus, true ->
+          (false, true)
+      | Mult, true ->
+          (true, false)
+      | Plus, false ->
+          ( ItvPure.is_ge_zero lhs || ItvPure.is_ge_zero rhs
+          , ItvPure.is_le_zero lhs || ItvPure.is_le_zero rhs )
+      | Minus, false ->
+          ( ItvPure.is_ge_zero lhs || ItvPure.is_le_zero rhs
+          , ItvPure.is_le_mone lhs || ItvPure.is_ge_zero rhs )
+      | Mult, false ->
+          ( (ItvPure.is_ge_zero lhs && ItvPure.is_ge_zero rhs)
+            || (ItvPure.is_le_zero lhs && ItvPure.is_le_zero rhs)
+          , (ItvPure.is_ge_zero lhs && ItvPure.is_le_zero rhs)
+            || (ItvPure.is_le_zero lhs && ItvPure.is_ge_zero rhs) )
+    in
+    (not cannot_underflow, not cannot_overflow)
+
+
+  let check ({binop; typ; integer_widths; lhs; rhs} as c) =
     if is_mult_one binop lhs rhs then {report_issue_type= None; propagate= false}
     else
       let v =
@@ -381,18 +405,20 @@ module BinaryOperationCondition = struct
         let lb, ub = Typ.range_of_ikind integer_widths typ in
         (Bound.of_big_int lb, Bound.of_big_int ub)
       in
+      let check_underflow, check_overflow = should_check c in
       if
         (* typ_lb <= v_lb and v_ub <= typ_ub, not an error *)
-        Bound.le v_ub typ_ub && Bound.le typ_lb v_lb
+        ((not check_underflow) || Bound.le typ_lb v_lb)
+        && ((not check_overflow) || Bound.le v_ub typ_ub)
       then {report_issue_type= None; propagate= false}
       else if
         (* v_ub < typ_lb or typ_ub < v_lb, definitely an error *)
-        Bound.lt v_ub typ_lb || Bound.lt typ_ub v_lb
+        (check_underflow && Bound.lt v_ub typ_lb) || (check_overflow && Bound.lt typ_ub v_lb)
       then {report_issue_type= Some IssueType.integer_overflow_l1; propagate= false}
       else if
         (* -oo != v_lb < typ_lb or typ_ub < v_ub != +oo, probably an error *)
-        (Bound.lt v_lb typ_lb && Bound.is_not_infty v_lb)
-        || (Bound.lt typ_ub v_ub && Bound.is_not_infty v_ub)
+        (check_underflow && Bound.lt v_lb typ_lb && Bound.is_not_infty v_lb)
+        || (check_overflow && Bound.lt typ_ub v_ub && Bound.is_not_infty v_ub)
       then {report_issue_type= Some IssueType.integer_overflow_l2; propagate= false}
       else
         let is_symbolic = ItvPure.is_symbolic v in

infer/src/bufferoverrun/itv.ml

@@ -580,6 +580,8 @@ module ItvPure = struct
 
   let is_le_zero : t -> bool = fun (_, ub) -> Bound.le ub Bound.zero
 
+  let is_le_mone : t -> bool = fun (_, ub) -> Bound.le ub Bound.mone
+
   let range : t -> ItvRange.t = fun (lb, ub) -> ItvRange.of_bounds ~lb ~ub
 
   let neg : t -> t =

infer/src/bufferoverrun/itv.mli

@@ -100,6 +100,12 @@ module ItvPure : sig
 
   val is_one : t -> bool
 
+  val is_ge_zero : t -> bool
+
+  val is_le_zero : t -> bool
+
+  val is_le_mone : t -> bool
+
   val ( <= ) : lhs:t -> rhs:t -> bool
 
   val have_similar_bounds : t -> t -> bool

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

@@ -190,3 +190,53 @@ void muliply_two_Bad() {
   uint64_t x = unknown_uint();
   uint64_t y = x * 2;
 }
+
+void minus_one_Good() {
+  uint64_t x = unknown_uint();
+  if (x > 0) {
+    uint64_t y = x - 1;
+  }
+}
+
+void minus_one_Bad() {
+  uint64_t x = unknown_uint();
+  if (x >= 0) {
+    uint64_t y = x - 1;
+  }
+}
+
+int64_t unknown_int();
+
+void plus_one_Good() {
+  int64_t x = unknown_int();
+  if (x < INT64_MAX) {
+    int64_t y = x + 1;
+  }
+}
+
+void plus_one_Bad() {
+  int64_t x = unknown_int();
+  if (x <= INT64_MAX) {
+    int64_t y = x + 1;
+  }
+}
+
+void minus_minimum_Good() {
+  int64_t x = -1;
+  int64_t y = x - INT64_MIN;
+}
+
+void minus_minimum_Bad() {
+  int64_t x = 0;
+  int64_t y = x - INT64_MIN;
+}
+
+void mult_minimum_Good() {
+  int64_t x = 1;
+  int64_t y = x * INT64_MIN;
+}
+
+void mult_minimum_Bad() {
+  int64_t x = -1;
+  int64_t y = x * INT64_MIN;
+}

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

@@ -5,16 +5,19 @@ codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_multiplication_Bad, 4
 codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_multiplication_Bad, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
 codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_subtraction_Bad, 4, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (-2000000000 - 2000000000):signed32]
 codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_subtraction_Bad, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
+codetoanalyze/c/bufferoverrun/arith.c, minus_minimum_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (0 - -9223372036854775808):signed64]
+codetoanalyze/c/bufferoverrun/arith.c, minus_one_Bad, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: unknown_uint,Assignment,Binop: ([0, +oo] - 1):unsigned64]
 codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_Bad, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [ArrayDeclaration,Parameter: i,ArrayAccess: Offset: [-4, 4] Size: 5]
 codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_neg_Bad, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [ArrayDeclaration,Parameter: i,ArrayAccess: Offset: [-4, 4] Size: 5]
 codetoanalyze/c/bufferoverrun/arith.c, muliply_two_Bad, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Unknown value from: unknown_uint,Assignment,Binop: ([-oo, +oo] * 2):unsigned64]
+codetoanalyze/c/bufferoverrun/arith.c, mult_minimum_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (-1 * -9223372036854775808):signed64]
 codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min2_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 14] Size: 10]
 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, use_int64_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, []
 codetoanalyze/c/bufferoverrun/array_content.c, call_array_min_index_from_one_good_FP, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: a,Assignment,ArrayAccess: Offset: [1, +oo] Size: 2 by call to `array_min_index_from_one_FP` ]
-codetoanalyze/c/bufferoverrun/array_content.c, call_array_min_index_from_one_good_FP, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Assignment,Return,Binop: ([1, +oo] - 1):signed32]
 codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_arr10_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
 codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_arr_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
 codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_ptr_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []

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

@@ -96,7 +96,6 @@ codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performan
 codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.two_loops():int, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 545, degree = 0]
 codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.two_loops():int, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 546, degree = 0]
 codetoanalyze/java/performance/EvilCfg.java, EvilCfg.foo(int,int,boolean):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
-codetoanalyze/java/performance/EvilCfg.java, EvilCfg.foo(int,int,boolean):void, 7, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Parameter: j,Assignment,Assignment,Assignment,Assignment,Binop: ([-oo, 9] + 1):signed32]
 codetoanalyze/java/performance/FieldAccess.java, codetoanalyze.java.performance.FieldAccess.iterate_upto_field_size(codetoanalyze.java.performance.FieldAccess$Test):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 6 * test.a.ub, degree = 1]
 codetoanalyze/java/performance/FieldAccess.java, codetoanalyze.java.performance.FieldAccess.iterate_upto_field_size(codetoanalyze.java.performance.FieldAccess$Test):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 6 * test.a.ub, degree = 1]
 codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 7 * (k.ub + -1), degree = 1]