When doing module and division, first cast to unsigned 32 bit then promote to 64 bit

src/crab/split_dbm.cpp

@@ -1008,9 +1008,30 @@ void SplitDBM::apply(arith_binop_t op, variable_t x, variable_t y, const number_
     case arith_binop_t::MUL: assign(x, linear_expression_t(k, y)); break;
     // For the rest of operations, we fall back on intervals.
     case arith_binop_t::SDIV: set(x, get_interval(y, finite_width).SDiv(interval_t(k))); break;
-    case arith_binop_t::UDIV: set(x, get_interval(y, finite_width).UDiv(interval_t(k))); break;
+    case arith_binop_t::UDIV: {
+        if (finite_width == 32) {
+            // As defined in the BPF ISA specification, for 32 bit unsigned division the immediate value is
+            // treated as a 32-bit unsigned integer, so we need to cast it to uint32_t.
+            set(x, get_interval(y, finite_width).UDiv(interval_t(k.cast_to<uint32_t>())));
+        } else {
+            // As defined in the BPF ISA specification, for 64 bit unsigned division the immediate value is
+            // treated as a 32-bit signed integer, so we need to cast it to int32_t.
+            set(x, get_interval(y, finite_width).UDiv(interval_t(k.cast_to<int32_t>())));
+        }
+        break;
+    }
     case arith_binop_t::SREM: set(x, get_interval(y, finite_width).SRem(interval_t(k))); break;
-    case arith_binop_t::UREM: set(x, get_interval(y, finite_width).URem(interval_t(k))); break;
+    case arith_binop_t::UREM:
+        if (finite_width == 32) {
+            // As defined in the BPF ISA specification, for 32 bit unsigned modulo the immediate value is
+            // treated as a 32-bit unsigned integer, so we need to cast it to uint32_t.
+            set(x, get_interval(y, finite_width).URem(interval_t(k.cast_to<uint32_t>())));
+        } else {
+            // As defined in the BPF ISA specification, for 64 bit unsigned modulo the immediate value is
+            // treated as a 32-bit signed integer, so we need to cast it to int32_t.
+            set(x, get_interval(y, finite_width).URem(interval_t(k.cast_to<int32_t>())));
+        }
+        break;
     default: CRAB_ERROR("DBM: unreachable");
     }
     normalize();

src/test/test_yaml.cpp

@@ -32,6 +32,7 @@ YAML_CASE("test-data/full64.yaml")
 YAML_CASE("test-data/jump.yaml")
 YAML_CASE("test-data/loop.yaml")
 YAML_CASE("test-data/movsx.yaml")
+YAML_CASE("test-data/muldiv.yaml")
 YAML_CASE("test-data/packet.yaml")
 YAML_CASE("test-data/parse.yaml")
 YAML_CASE("test-data/sext.yaml")

test-data/muldiv.yaml

@@ -0,0 +1,60 @@
+# Copyright (c) Prevail Verifier contributors.
+# SPDX-License-Identifier: MIT
+---
+test-case: 32bit division - negative divisor
+
+pre: ["r0.type=number", "r0.svalue=0", "r0.uvalue=0"]
+
+code:
+  <start>: |
+    w0 = 4194435072
+    w0 /= 4096655360
+
+post:
+  - r0.type=number
+  - r0.svalue=1
+  - r0.uvalue=1
+
+---
+test-case: 32bit modulo - negative divisor
+pre: ["r0.type=number", "r0.svalue=0", "r0.uvalue=0"]
+
+code:
+  <start>: |
+    w0 = 4194435072
+    w0 %= 4096655360
+
+post:
+  - r0.type=number
+  - r0.svalue=97779712
+  - r0.uvalue=97779712
+
+---
+test-case: 64bit division - negative divisor
+
+pre: ["r0.type=number", "r0.svalue=0", "r0.uvalue=0"]
+
+code:
+  <start>: |
+    r0 = 4194435072
+    r0 /= 4096655360
+
+post:
+  - r0.type=number
+  - r0.svalue=1
+  - r0.uvalue=1
+
+---
+test-case: 64bit modulo - negative divisor
+
+pre: ["r0.type=number", "r0.svalue=0", "r0.uvalue=0"]
+
+code:
+  <start>: |
+    r0 = 4194435072
+    r0 %= 4096655360
+
+post:
+  - r0.type=number
+  - r0.svalue=-100532224
+  - r0.uvalue=18446744073609019392