Add support for atomic CMPXCHG

Signed-off-by: Dave Thaler <[email protected]>
vbpf · Jan 3, 2024 · aa01605 · aa01605
1 parent 7f11e03
commit aa01605
Show file tree

Hide file tree

Showing 2 changed files with 38 additions and 6 deletions.
diff --git a/src/crab/ebpf_domain.cpp b/src/crab/ebpf_domain.cpp
@@ -2130,15 +2130,21 @@ void ebpf_domain_t::operator()(const Atomic& a) {
     case AtomicOp::INST_ATOMIC_OR: bin.op = Bin::Op::OR; break;
     case AtomicOp::INST_ATOMIC_AND: bin.op = Bin::Op::AND; break;
     case AtomicOp::INST_ATOMIC_XOR: bin.op = Bin::Op::XOR; break;
-    case AtomicOp::INST_ATOMIC_XCHG_BASE: bin.op = Bin::Op::MOV; break;
-    case AtomicOp::INST_ATOMIC_CMPXCHG_BASE:
-        // TODO: handle other instructions.
-        m_inv.set_to_bottom(); return;
+    case AtomicOp::INST_ATOMIC_XCHG_BASE:
+    case AtomicOp::INST_ATOMIC_CMPXCHG_BASE: bin.op = Bin::Op::MOV; break;
+    default: throw std::exception();
     }
     (*this)(bin);
 
-    // If FETCH is set, store the original value in the src register.
-    if ((uint32_t)a.op & (uint32_t)AtomicOp::INST_ATOMIC_FETCH) {
+    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.
+        Reg r0{R0_RETURN_VALUE};
+        havoc_register(m_inv, r0);
+        type_inv.havoc_type(m_inv, r0);
+    } else if ((uint32_t)a.op & (uint32_t)AtomicOp::INST_ATOMIC_FETCH) {
+        // For other FETCH operations, store the original value in the src register.
         mem.value = a.valreg;
         mem.is_load = true;
         (*this)(mem);

diff --git a/test-data/atomic.yaml b/test-data/atomic.yaml
@@ -216,3 +216,29 @@ code:
 
 post: ["r1.type=number",
        "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 CMPXCHG
+
+pre: ["r0.type=number", "r0.svalue=2", "r0.uvalue=2",
+      "r1.type=number", "r1.svalue=2", "r1.uvalue=2",
+      "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+
+code:
+  <start>: |
+    lock *(u32 *)(r2 + 4) cx= r1
+
+post: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
+       "r2.type=shared", "r2.shared_region_size=12", "r2.shared_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"]
+---
+test-case: atomic 64-bit CMPXCHG
+
+pre: ["r0.type=number", "r0.svalue=2", "r0.uvalue=2",
+      "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"]
+
+code:
+  <start>: |
+    lock *(u64 *)(r2 + 4) cx= r1
+
+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"]