From ea2278b614622d3bbc6ec109bd9c4bfbac7f0ba3 Mon Sep 17 00:00:00 2001
From: Alan Jowett <alan.jowett@microsoft.com>
Date: Wed, 16 Oct 2024 12:45:21 -0700
Subject: [PATCH] Restrict udiv optimization to case where both are singletons

Signed-off-by: Alan Jowett <alan.jowett@microsoft.com>
---
 src/crab/interval.cpp  | 17 ++++++++---------
 test-data/sdivmod.yaml | 21 +++++++++++++++++++++
 test-data/udivmod.yaml | 21 +++++++++++++++++++++
 3 files changed, 50 insertions(+), 9 deletions(-)

diff --git a/src/crab/interval.cpp b/src/crab/interval.cpp
index 8db510e2a..4c8856f29 100644
--- a/src/crab/interval.cpp
+++ b/src/crab/interval.cpp
@@ -187,16 +187,15 @@ interval_t interval_t::URem(const interval_t& x) const {
     if (is_bottom() || x.is_bottom()) {
         return bottom();
     }
-    if (const auto n = x.singleton()) {
-        // Divisor is a singleton:
-        //   the linear interval solver can perform many divisions where
-        //   the divisor is a singleton interval. We optimize for this case.
-        number_t c = *n;
-        if (c > number_t{0}) {
-            return interval_t(_lb.URem(bound_t{c}), _ub.URem(bound_t{c}));
+    if (const auto dividend = singleton()) {
+        if (const auto divisor = x.singleton()) {
+            if (*divisor == 0) {
+                return interval_t(*dividend);
+            }
+            auto dividend_val = dividend->cast_to<uint64_t>();
+            auto divisor_val = divisor->cast_to<uint64_t>();
+            return interval_t(dividend_val % divisor_val);
         }
-        // The eBPF ISA defines modulo 0 as being unchanged.
-        return *this;
     }
     if (x.contains(0)) {
         // The divisor contains 0.
diff --git a/test-data/sdivmod.yaml b/test-data/sdivmod.yaml
index 8da36fb5b..6221bd65f 100644
--- a/test-data/sdivmod.yaml
+++ b/test-data/sdivmod.yaml
@@ -569,3 +569,24 @@ post:
   - r2.type=number
   - r2.svalue=[7, 10]
   - r2.uvalue=[7, 10]
+
+---
+test-case: Inverted range after modulo
+
+pre: [r0.type=number]
+
+code:
+  <start>: |
+    if r0 s< 0x8000 goto <reset>
+    r0 %= 0x808
+    goto <exit>
+  <reset>: |
+    r0 = 0
+  <exit>: |
+    exit
+
+post:
+  - r0.type=number
+  - r0.svalue=[0, 2055]
+  - r0.uvalue=[0, 2055]
+  - r0.svalue=r0.uvalue
diff --git a/test-data/udivmod.yaml b/test-data/udivmod.yaml
index 5255c026b..56d7a5caa 100644
--- a/test-data/udivmod.yaml
+++ b/test-data/udivmod.yaml
@@ -573,3 +573,24 @@ post:
   - r2.type=number
   - r2.svalue=[7, 10]
   - r2.uvalue=[7, 10]
+
+---
+test-case: Inverted range after modulo
+
+pre: [r0.type=number]
+
+code:
+  <start>: |
+    if r0 s< 0x8000 goto <reset>
+    r0 %= 0x808
+    goto <exit>
+  <reset>: |
+    r0 = 0
+  <exit>: |
+    exit
+
+post:
+  - r0.type=number
+  - r0.svalue=[0, 2055]
+  - r0.uvalue=[0, 2055]
+  - r0.svalue=r0.uvalue