Fix overflow in conversion from uvalue to svalue

Signed-off-by: Alan Jowett <[email protected]>
vbpf · Oct 30, 2024 · da857be · da857be
1 parent defa790
commit da857be
Show file tree

Hide file tree

Showing 2 changed files with 35 additions and 1 deletion.
diff --git a/src/crab/ebpf_domain.cpp b/src/crab/ebpf_domain.cpp
@@ -2374,7 +2374,8 @@ void ebpf_domain_t::lshr(const Reg& dst_reg, int imm, int finite_width) {
             }
         }
         m_inv.set(dst.uvalue, interval_t{lb_n, ub_n});
-        if (ub_n.narrow<int64_t>() >= lb_n.narrow<int64_t>()) {
+        if ((ub_n.fits<int64_t>() && lb_n.fits<int64_t>()) &&
+            ub_n.narrow<int64_t>() >= lb_n.narrow<int64_t>()) {
             // ? m_inv.set(dst.svalue, crab::interval_t{number_t{(int64_t)lb_n}, number_t{(int64_t)ub_n}});
             m_inv.assign(dst.svalue, dst.uvalue);
         } else {

diff --git a/test-data/shift.yaml b/test-data/shift.yaml
@@ -1104,3 +1104,36 @@ post:
   - r2.type=number
   - r2.svalue=32
   - r2.uvalue=32
+
+---
+test-case: check that unsigned right shift by 0 is idempotent
+
+pre:
+  - r0.type=number
+  - r0.svalue=-8863041185711652825
+  - r0.uvalue=9583702887997898791
+  - r1.type=number
+  - r1.svalue=-8863041185711652825
+  - r1.uvalue=9583702887997898791
+
+code:
+  <start>: |
+    r0 >>= 0
+    if r1 == r0 goto <one>
+    r2 = 0
+    exit
+  <one>: |
+    r2 = 1
+    exit
+
+post:
+  - r0.type=number
+  - r0.uvalue=9583702887997898791
+  - r1.type=number
+  - r1.svalue=-8863041185711652825
+  - r1.uvalue=9583702887997898791
+  - r0.uvalue=r1.uvalue
+  - r2.type=number
+  - r2.svalue=[0, 1]
+  - r2.uvalue=[0, 1]
+  - r2.svalue=r2.uvalue