[inferbo] Precise mod semantics on unsigned integer

Summary:
This diff improves the precision of the mod operator.

For example, result of x % c (when x>=0 and c>0) is
(before) [0, c-1]
(after) [0, min(c-1,x)]

Reviewed By: ezgicicek

Differential Revision: D16518578

fbshipit-source-id: a68660ee7

infer/src/bufferoverrun/itv.ml

@@ -257,8 +257,10 @@ module ItvPure = struct
           of_big_int Z.(n mod m)
       | None ->
           let abs_m = Z.abs m in
-          if is_ge_zero x then (Bound.zero, Bound.of_big_int Z.(abs_m - one))
-          else if is_le_zero x then (Bound.of_big_int Z.(one - abs_m), Bound.zero)
+          if is_ge_zero x then
+            (Bound.zero, Bound.overapprox_min (Bound.of_big_int Z.(abs_m - one)) (ub x))
+          else if is_le_zero x then
+            (Bound.overapprox_max (Bound.of_big_int Z.(one - abs_m)) (lb x), Bound.zero)
           else (Bound.of_big_int Z.(one - abs_m), Bound.of_big_int Z.(abs_m - one)) )
 
 

infer/tests/codetoanalyze/cpp/bufferoverrun/arith.cpp

@@ -5,6 +5,7 @@
  * LICENSE file in the root directory of this source tree.
  */
 #include <cstdint>
+#include <cstdlib>
 
 void sizeof_bool_Good() {
   int a[2];
@@ -115,3 +116,19 @@ void call_integer_overflow_param_1_Good() { integer_overflow_param_1(0); }
 uint32_t integer_overflow_param_2(uint32_t x) { return x - 1; }
 
 void call_integer_overflow_param_2_Bad() { integer_overflow_param_2(0); }
+
+void mod_ub(const char* msg, size_t leng) {
+  size_t rem = leng % 32;
+  if (rem == 15) {
+    char d = msg[14]; // Good
+  }
+  if (rem == 10) {
+    char d = msg[14]; // Bad
+  }
+}
+
+void call_mod_ub_1_Good() { mod_ub("ab", 2); }
+
+void call_mod_ub_2_Good() { mod_ub("abcdefghijklmno", 15); }
+
+void call_mod_ub_Bad() { mod_ub("abcdefghij", 10); }

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

@@ -9,6 +9,7 @@ codetoanalyze/cpp/bufferoverrun/arith.cpp, bool_overflow_Good_FP, 2, CONDITION_A
 codetoanalyze/cpp/bufferoverrun/arith.cpp, bool_overflow_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
 codetoanalyze/cpp/bufferoverrun/arith.cpp, call_integer_overflow_param_2_Bad, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,<LHS trace>,Parameter `x`,Binary operation: (0 - 1):unsigned32 by call to `integer_overflow_param_2` ]
 codetoanalyze/cpp/bufferoverrun/arith.cpp, call_integer_overflow_x_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,Parameter `init`,Assignment,Call,<LHS trace>,Parameter `this->x`,<RHS trace>,Assignment,Binary operation: (4294967295 × 4294967295):unsigned32 by call to `RG::integer_overflow_x` ]
+codetoanalyze/cpp/bufferoverrun/arith.cpp, call_mod_ub_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Length trace>,Parameter `*msg`,Array access: Offset: 14 Size: 11 by call to `mod_ub` ]
 codetoanalyze/cpp/bufferoverrun/arith.cpp, integer_overflow_field_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [<RHS trace>,Assignment,Binary operation: (0 - 1):unsigned32]
 codetoanalyze/cpp/bufferoverrun/arith.cpp, range_bool_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
 codetoanalyze/cpp/bufferoverrun/arith.cpp, range_bool_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 2 Size: 2]