Fix 32-bit arithmetic operations

Signed-off-by: Dave Thaler <dthaler@microsoft.com>
vbpf · Nov 16, 2022 · 3d2c373 · 3d2c373
1 parent 67cb4d1
commit 3d2c373
Show file tree

Hide file tree

Showing 5 changed files with 15 additions and 7 deletions.
diff --git a/src/asm_ostream.hpp b/src/asm_ostream.hpp
@@ -28,7 +28,7 @@ std::string to_string(Instruction const& ins);
 std::ostream& operator<<(std::ostream& os, Bin::Op op);
 std::ostream& operator<<(std::ostream& os, Condition::Op op);
 
-inline std::ostream& operator<<(std::ostream& os, Imm imm) { return os << (int32_t)imm.v; }
+inline std::ostream& operator<<(std::ostream& os, Imm imm) { return os << (int64_t)imm.v; }
 inline std::ostream& operator<<(std::ostream& os, Reg const& a) { return os << "r" << (int)a.v; }
 inline std::ostream& operator<<(std::ostream& os, Value const& a) {
     if (std::holds_alternative<Imm>(a))

diff --git a/src/asm_unmarshal.cpp b/src/asm_unmarshal.cpp
@@ -215,6 +215,8 @@ struct Unmarshaller {
                 ((inst.opcode & INST_SIZE_MASK) != INST_SIZE_W &&
                  (inst.opcode & INST_SIZE_MASK) != INST_SIZE_DW))
                 throw InvalidInstruction(pc, "Bad instruction");
+            if (inst.imm != 0)
+                throw InvalidInstruction(pc, "Unsupported atomic instruction");
             return LockAdd{
                 .access =
                     Deref{

diff --git a/src/crab/ebpf_domain.cpp b/src/crab/ebpf_domain.cpp
@@ -382,7 +382,7 @@ void ebpf_domain_t::operator+=(const linear_constraint_t& cst) { m_inv += cst; }
 void ebpf_domain_t::operator-=(variable_t var) { m_inv -= var; }
 
 void ebpf_domain_t::assign(variable_t x, const linear_expression_t& e) { m_inv.assign(x, e); }
-void ebpf_domain_t::assign(variable_t x, long e) { m_inv.set(x, crab::interval_t(number_t(e))); }
+void ebpf_domain_t::assign(variable_t x, int64_t e) { m_inv.set(x, crab::interval_t(number_t(e))); }
 
 void ebpf_domain_t::apply(crab::arith_binop_t op, variable_t x, variable_t y, const number_t& z) { m_inv.apply(op, x, y, z); }
 
@@ -1525,7 +1525,13 @@ void ebpf_domain_t::operator()(const Bin& bin) {
 
     if (std::holds_alternative<Imm>(bin.v)) {
         // dst += K
-        int imm = static_cast<int>(std::get<Imm>(bin.v).v);
+        int64_t imm;
+        if (bin.is64) {
+            imm = static_cast<int64_t>(std::get<Imm>(bin.v).v);
+        } else {
+            imm = static_cast<int>(std::get<Imm>(bin.v).v);
+            bitwise_and(dst.value, UINT32_MAX);
+        }
         switch (bin.op) {
         case Bin::Op::MOV:
             assign(dst.value, imm);
@@ -1785,7 +1791,7 @@ void ebpf_domain_t::operator()(const Bin& bin) {
                             m_inv.set(dst.value, crab::interval_t(number_t((unsigned long long)output),
                                                                   number_t((unsigned long long)output)));
                         } else {
-                            int32_t output = (int32_t)((int32_t)input >> (int32_t)src_n.value());
+                            int32_t output = (int32_t)((int32_t)input >> (int32_t)(int64_t)src_n.value());
                             m_inv.set(dst.value, crab::interval_t(number_t((uint32_t)output), number_t((uint32_t)output)));
                         }
                         break;

diff --git a/src/crab/ebpf_domain.hpp b/src/crab/ebpf_domain.hpp
@@ -83,7 +83,7 @@ class ebpf_domain_t final {
 
     void assign(variable_t lhs, variable_t rhs);
     void assign(variable_t x, const linear_expression_t& e);
-    void assign(variable_t x, long e);
+    void assign(variable_t x, int64_t e);
 
     void apply(crab::arith_binop_t op, variable_t x, variable_t y, const number_t& z);
     void apply(crab::arith_binop_t op, variable_t x, variable_t y, variable_t z);

diff --git a/src/test/test_conformance.cpp b/src/test/test_conformance.cpp
@@ -130,8 +130,8 @@ TEST_CONFORMANCE_VERIFICATION_FAILED("lock_add.data")
 TEST_CONFORMANCE_VERIFICATION_FAILED("lock_add32.data")
 TEST_CONFORMANCE_VERIFICATION_FAILED("lock_and.data")
 TEST_CONFORMANCE_VERIFICATION_FAILED("lock_and32.data")
-TEST_CONFORMANCE("lock_cmpxchg.data") // FAILS!!
-TEST_CONFORMANCE("lock_cmpxchg32.data") // FAILS!!
+TEST_CONFORMANCE_VERIFICATION_FAILED("lock_cmpxchg.data")
+TEST_CONFORMANCE_VERIFICATION_FAILED("lock_cmpxchg32.data")
 TEST_CONFORMANCE_VERIFICATION_FAILED("lock_or.data")
 TEST_CONFORMANCE_VERIFICATION_FAILED("lock_or32.data")
 TEST_CONFORMANCE("lock_xchg.data")