Merge branch 'vbpf:main' into issue728

vbpf · Oct 30, 2024 · 523b21c · 523b21c
2 parents b5006f8 + 6025c9b
commit 523b21c
Show file tree

Hide file tree

Showing 3 changed files with 570 additions and 17 deletions.
diff --git a/src/asm_parse.cpp b/src/asm_parse.cpp
@@ -154,7 +154,7 @@ Instruction parse_instruction(const std::string& line, const std::map<std::strin
     if (regex_match(text, m, regex("callx " REG))) {
         return Callx{reg(m[1])};
     }
-    if (regex_match(text, m, regex(WREG OPASSIGN REG))) {
+    if (regex_match(text, m, regex(WREG OPASSIGN WREG))) {
         const std::string r = m[1];
         return Bin{.op = str_to_binop.at(m[2]), .dst = reg(r), .v = reg(m[3]), .is64 = is64_reg(r), .lddw = false};
     }

diff --git a/src/crab/ebpf_domain.cpp b/src/crab/ebpf_domain.cpp
@@ -2334,11 +2334,9 @@ void ebpf_domain_t::shl(const Reg& dst_reg, int imm, const int finite_width) {
                 ub_n = ub_n << imm & uint_max;
             }
             m_inv.set(dst.uvalue, interval_t{lb_n, ub_n});
-            if (to_signed(ub_n) >= to_signed(lb_n)) {
-                m_inv.assign(dst.svalue, dst.uvalue);
-            } else {
-                havoc(dst.svalue);
-            }
+            m_inv.assign(dst.svalue, dst.uvalue);
+            overflow_signed(m_inv, dst.svalue, finite_width);
+            overflow_unsigned(m_inv, dst.uvalue, finite_width);
             return;
         }
     }
@@ -2374,12 +2372,9 @@ 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>()) {
-            // ? 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 {
-            havoc(dst.svalue);
-        }
+        m_inv.assign(dst.svalue, dst.uvalue);
+        overflow_signed(m_inv, dst.svalue, finite_width);
+        overflow_unsigned(m_inv, dst.uvalue, finite_width);
         return;
     }
     havoc(dst.svalue);
@@ -2464,11 +2459,9 @@ void ebpf_domain_t::ashr(const Reg& dst_reg, const linear_expression_t& right_sv
                 }
             }
             m_inv.set(dst.svalue, interval_t{lb_n, ub_n});
-            if (to_unsigned(ub_n) >= to_unsigned(lb_n)) {
-                m_inv.assign(dst.uvalue, dst.svalue);
-            } else {
-                havoc(dst.uvalue);
-            }
+            m_inv.assign(dst.uvalue, dst.svalue);
+            overflow_signed(m_inv, dst.svalue, finite_width);
+            overflow_unsigned(m_inv, dst.uvalue, finite_width);
             return;
         }
     }