[inferbo] Revise modulo semantics for positive values

Reviewed By: mbouaziz

Differential Revision: D5272606

fbshipit-source-id: 2a4f69d

infer/src/bufferoverrun/itv.ml

@@ -592,6 +592,14 @@ struct
   let is_symbolic : t -> bool
     = fun (lb, ub) -> Bound.is_symbolic lb || Bound.is_symbolic ub
 
+  let is_ge_zero : t -> bool
+    = fun (lb, _) ->
+      if lb <> Bound.Bot then Bound.le Bound.zero lb else false
+
+  let is_le_zero : t -> bool
+    = fun (_, ub) ->
+      if ub <> Bound.Bot then Bound.le ub Bound.zero else false
+
   let neg : t -> t
     = fun (l, u) ->
       let l' = Option.value ~default:Bound.MInf (Bound.neg u) in
@@ -653,8 +661,13 @@ struct
   let mod_sem : t -> t -> t
     = fun x y ->
       match is_const x, is_const y with
-      | Some n, Some m -> if Int.equal m 0 then x else of_int (n mod m)
-      | _, Some m -> (Bound.of_int (-m), Bound.of_int m)
+      | _, Some 0 -> x
+      | Some n, Some m -> of_int (n mod m)
+      | _, Some m ->
+          let abs_m = abs m in
+          if is_ge_zero x then (Bound.zero, Bound.of_int (abs_m - 1)) else
+          if is_le_zero x then (Bound.of_int (-abs_m + 1), Bound.zero) else
+            (Bound.of_int (-abs_m + 1), Bound.of_int (abs_m - 1))
       | _, None -> top
 
   (* x << [-1,-1] does nothing. *)

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

@@ -12,14 +12,26 @@ void modulo_signed_Bad(int i) {
   arr[i % 5] = 123;
 }
 
-void modulo_signed_Good_FP(int i) {
+void modulo_signed_Good(int i) {
   char arr[5];
   if (i >= 0) {
     arr[i % 5] = 123;
   }
 }
 
-void modulo_signed_Good2_FP(int i) {
+void modulo_signed_neg_Bad(int i) {
+  char arr[5];
+  arr[i % -5] = 123;
+}
+
+void modulo_signed_neg_Good(int i) {
+  char arr[5];
+  if (i >= 0) {
+    arr[i % -5] = 123;
+  }
+}
+
+void modulo_signed_Good2(int i) {
   char arr[5];
   int j = i % 5;
   if (j >= 0) {

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

@@ -1,7 +1,6 @@
-codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_Bad, 2, BUFFER_OVERRUN, [Offset: [-5, 5] Size: [5, 5]]
-codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_Good2_FP, 4, BUFFER_OVERRUN, [Offset: [0, 5] Size: [5, 5]]
-codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_Good_FP, 3, BUFFER_OVERRUN, [Offset: [-5, 5] Size: [5, 5]]
-codetoanalyze/c/bufferoverrun/arith.c, modulo_unsigned_Good_FP, 2, BUFFER_OVERRUN, [Offset: [-5, 5] Size: [5, 5]]
+codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_Bad, 2, BUFFER_OVERRUN, [Offset: [-4, 4] Size: [5, 5]]
+codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_neg_Bad, 2, BUFFER_OVERRUN, [Offset: [-4, 4] Size: [5, 5]]
+codetoanalyze/c/bufferoverrun/arith.c, modulo_unsigned_Good_FP, 2, BUFFER_OVERRUN, [Offset: [-4, 4] Size: [5, 5]]
 codetoanalyze/c/bufferoverrun/array_dynlength.c, init_variable_array, 3, BUFFER_OVERRUN, [Offset: [3xs$0 + 1, 3xs$1 + 1] Size: [3xs$0 + 1, 3xs$1 + 1]]
 codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 4, CONDITION_ALWAYS_TRUE, []
 codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 13, CONDITION_ALWAYS_TRUE, []