Add some failure test cases

Signed-off-by: Dave Thaler <[email protected]>

src/asm_ostream.cpp

@@ -324,21 +324,6 @@ struct InstructionPrinterVisitor {
 
     void operator()(Atomic const& b) {
         os_ << "lock ";
-
-        if (b.op == AtomicOp::INST_ATOMIC_XCHG) {
-            os_ << "xchg(";
-            print(b.access);
-            os_ << ", " << b.valreg << ")";
-            return;
-        }
-
-        if (b.op == AtomicOp::INST_ATOMIC_CMPXCHG) {
-            os_ << "cmpxchg(";
-            print(b.access);
-            os_ << ", r0, " << b.valreg << ")";
-            return;
-        }
-
         print(b.access);
         os_ << " ";
         bool showfetch = true;
@@ -348,7 +333,7 @@ struct InstructionPrinterVisitor {
         case AtomicOp::INST_ATOMIC_AND: os_ << "&"; break;
         case AtomicOp::INST_ATOMIC_XOR: os_ << "^"; break;
         case AtomicOp::INST_ATOMIC_XCHG_BASE: os_ << "x"; showfetch = false; break;
-        case AtomicOp::INST_ATOMIC_CMPXCHG_BASE: os_ << "cx";showfetch = false; break;
+        case AtomicOp::INST_ATOMIC_CMPXCHG_BASE: os_ << "cx"; showfetch = false; break;
         }
         os_ << "= " << b.valreg;
 

src/asm_unmarshal.cpp

@@ -298,7 +298,6 @@ struct Unmarshaller {
     auto makeLddw(ebpf_inst inst, int32_t next_imm, const vector<ebpf_inst>& insts, pc_t pc) -> Instruction {
         if (pc >= insts.size() - 1)
             throw InvalidInstruction(pc, "incomplete LDDW");
-        // TODO(#533):
         if (inst.src > 1 || inst.dst > R10_STACK_POINTER || inst.offset != 0)
             throw InvalidInstruction(pc, "LDDW uses reserved fields");
 

src/assertions.cpp

@@ -168,6 +168,12 @@ class AssertExtractor {
         res.emplace_back(TypeConstraint{ins.access.basereg, TypeGroup::shared});
         res.emplace_back(ValidAccess{ins.access.basereg, ins.access.offset,
                                      Imm{static_cast<uint32_t>(ins.access.width)}, false});
+        if (ins.op == AtomicOp::INST_ATOMIC_CMPXCHG) {
+            // The shared memory contents pointed to by ins.access will be compared
+            // against the value of the ins.valreg register.  Since shared memory
+            // must contain a number, so must ins.valreg.
+            res.emplace_back(TypeConstraint{ins.valreg, TypeGroup::number});
+        }
         return res;
     }
 

src/crab/ebpf_domain.cpp

@@ -1182,6 +1182,11 @@ static linear_constraint_t type_is_number(const reg_pack_t& r) {
     return r.type == T_NUM;
 }
 
+static linear_constraint_t type_is_shared(const reg_pack_t& r) {
+    using namespace crab::dsl_syntax;
+    return r.type == T_SHARED;
+}
+
 static linear_constraint_t type_is_number(const Reg& r) { return type_is_number(reg_pack(r)); }
 
 static linear_constraint_t type_is_not_stack(const reg_pack_t& r) {
@@ -2117,6 +2122,10 @@ void ebpf_domain_t::do_mem_store(const Mem& b, Type val_type, SValue val_svalue,
 void ebpf_domain_t::operator()(const Atomic& a) {
     if (m_inv.is_bottom())
         return;
+    if (!m_inv.entail(type_is_shared(reg_pack(a.access.basereg))) ||
+        !m_inv.entail(type_is_number(reg_pack(a.valreg)))) {
+        return;
+    }
 
     // Fetch the current value into the R11 pseudo-register.
     Reg r11{R11_ATOMIC_SCRATCH};
@@ -2139,7 +2148,8 @@ void ebpf_domain_t::operator()(const Atomic& a) {
     if (a.op == AtomicOp::INST_ATOMIC_CMPXCHG) {
         // For CMPXCHG, store the original value in r0 if and only if the value matches
         // what is in the src register.  Until we track shared memory values,
-        // we just havoc R0.
+        // we just havoc R0.  If we did track shared memory values, we'd need more
+        // complex logic here.
         Reg r0{R0_RETURN_VALUE};
         havoc_register(m_inv, r0);
         type_inv.havoc_type(m_inv, r0);

test-data/atomic.yaml

@@ -242,3 +242,50 @@ code:
 
 post: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
        "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+---
+test-case: atomic 32-bit ADD past end of region
+
+pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
+      "r2.type=shared", "r2.shared_region_size=10", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+
+code:
+  <start>: |
+    lock *(u32 *)(r2 + 4) += r1
+
+post: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
+       "r2.type=shared", "r2.shared_region_size=10", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+
+messages:
+  - "0: Upper bound must be at most r2.shared_region_size (valid_access(r2.offset+4, width=4) for write)"
+---
+test-case: atomic 32-bit ADD to non-shared space
+
+pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
+      "r2.type=stack", "r2.stack_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+
+code:
+  <start>: |
+    lock *(u32 *)(r2 + 4) += r1
+
+post: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
+      "r2.type=stack", "r2.stack_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+
+messages:
+  - "0:  (r2.type == shared)"
+---
+test-case: atomic 64-bit CMPXCHG comparing against non-number
+
+pre: ["r0.type=number", "r0.svalue=2", "r0.uvalue=2",
+      "r1.type=shared", "r1.shared_region_size=16", "r1.shared_offset=4",
+      "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+
+code:
+  <start>: |
+    lock *(u64 *)(r2 + 4) cx= r1
+
+post: ["r0.type=number", "r0.svalue=2", "r0.uvalue=2",
+       "r1.type=shared", "r1.shared_region_size=16", "r1.shared_offset=4",
+       "r2.type=shared", "r2.shared_region_size=16", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+
+messages:
+  - "0:  (r1.type == number)"