Check for division overflow in modulo operations

Author: sim642

src/cdomain/value/cdomains/int/intDomTuple.ml

@@ -448,7 +448,12 @@ module IntDomTupleImpl = struct
       {f2_ovc = (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.div ?no_ov ik)}
 
   let rem ik =
-    map2 ik {f2= (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.rem ik)}
+    map2ovc ~op:(Binop Mod) ik
+      {f2_ovc = (fun (type a) (module I : SOverflow with type t = a) ?no_ov x y ->
+           (* C11 6.5.5.6: if [x/y] is not representable (i.e. overflows), then [x%y] is undefined (let's also call it overflow) *)
+           let (_, div_ov) = I.div ?no_ov ik x y in
+           (I.rem ik x y, div_ov) (* TODO: should [div] overflow check be moved into each [rem] in each int domain? *)
+         )}
 
   let lt ik =
     map2 ik {f2= (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.lt ik)}

tests/regression/39-signed-overflows/17-mod-minus-1.c

@@ -6,7 +6,7 @@ int main() {
     int x, y;
     bad = x % y; // WARN (div by zero and overflow, distinguished in cram test)
     if (y != 0) {
-        bad = x % y; // TODO WARN (overflow)
+        bad = x % y; // WARN (overflow)
     }
     return 0;
 }

tests/regression/39-signed-overflows/17-mod-minus-1.t

@@ -1,5 +1,7 @@
 TODO: should warn about overflow in all three %-s
   $ goblint --enable warn.deterministic --enable ana.int.interval 17-mod-minus-1.c
+  [Warning][Integer > Overflow][CWE-190] Signed integer overflow in % (17-mod-minus-1.c:7:5-7:16)
+  [Warning][Integer > Overflow][CWE-190] Signed integer overflow in % (17-mod-minus-1.c:9:9-9:20)
   [Warning][Integer > DivByZero][CWE-369] Second argument of modulo might be zero (17-mod-minus-1.c:7:5-7:16)
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 6
@@ -8,6 +10,8 @@ TODO: should warn about overflow in all three %-s
 
 TODO: should warn about overflow in all three %-s
   $ goblint --enable warn.deterministic --enable ana.int.interval_set 17-mod-minus-1.c
+  [Warning][Integer > Overflow][CWE-190] Signed integer overflow in % (17-mod-minus-1.c:7:5-7:16)
+  [Warning][Integer > Overflow][CWE-190] Signed integer overflow in % (17-mod-minus-1.c:9:9-9:20)
   [Warning][Integer > DivByZero][CWE-369] Second argument of modulo might be zero (17-mod-minus-1.c:7:5-7:16)
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 6