Merge remote-tracking branch 'origin/overflow-mod' into dash-dev

Author: karoliineh

goblint.opam

@@ -102,7 +102,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 x-maintenance-intent: ["(latest)" "(latest).(latest-1)"] # also keep previous minor version (with two releases per year, always keep a SV-COMP release)
 available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
 pin-depends: [
-  [ "goblint-cil.2.0.9" "git+https://github.com/goblint/cil.git#2edc807cfc8ce80e74e932a8d84a809a44ec0c3d" ]
+  [ "goblint-cil.2.0.9" "git+https://github.com/goblint/cil.git#d4ff56f4994f8acbe1544f15a103748942645961" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release
   [ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ]
 ]

goblint.opam.locked

@@ -148,7 +148,7 @@ post-messages: [
 pin-depends: [
   [
     "goblint-cil.2.0.9"
-    "git+https://github.com/goblint/cil.git#2edc807cfc8ce80e74e932a8d84a809a44ec0c3d"
+    "git+https://github.com/goblint/cil.git#d4ff56f4994f8acbe1544f15a103748942645961"
   ]
   [
     "apron.v0.9.15"

goblint.opam.template

@@ -3,7 +3,7 @@
 x-maintenance-intent: ["(latest)" "(latest).(latest-1)"] # also keep previous minor version (with two releases per year, always keep a SV-COMP release)
 available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
 pin-depends: [
-  [ "goblint-cil.2.0.9" "git+https://github.com/goblint/cil.git#2edc807cfc8ce80e74e932a8d84a809a44ec0c3d" ]
+  [ "goblint-cil.2.0.9" "git+https://github.com/goblint/cil.git#d4ff56f4994f8acbe1544f15a103748942645961" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release
   [ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ]
 ]

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

@@ -0,0 +1,12 @@
+// PARAM: --enable ana.int.interval
+#include <limits.h>
+
+int main() {
+    int bad = INT_MIN % -1; // WARN (overflow)
+    int x, y;
+    bad = x % y; // WARN (div by zero and overflow, distinguished in cram test)
+    if (y != 0) {
+        bad = x % y; // WARN (overflow)
+    }
+    return 0;
+}

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

@@ -0,0 +1,20 @@
+  $ 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:5:9-5:26)
+  [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
+    dead: 0
+    total lines: 6
+
+  $ 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:5:9-5:26)
+  [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
+    dead: 0
+    total lines: 6
+