Don't assume shared memory values are trackable

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

src/crab/ebpf_domain.cpp

@@ -2147,9 +2147,8 @@ void ebpf_domain_t::operator()(const Atomic& a) {
 
     if (a.op == Atomic::Op::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.  If we did track shared memory values, we'd need more
-        // complex logic here.
+        // what is in the src register.  We cannot reliably track shared memory values,
+        // since they may be modified from another thread, we just havoc R0.
         Reg r0{R0_RETURN_VALUE};
         havoc_register(m_inv, r0);
         type_inv.havoc_type(m_inv, r0);
@@ -2160,12 +2159,9 @@ void ebpf_domain_t::operator()(const Atomic& a) {
         (*this)(mem);
     }
 
-    // Store the new value back in the original shared memory location.
-    // Note that do_mem_store() currently doesn't track shared memory values,
-    // but it might in the future so we include code here as if it did.
-    mem.value = r11;
-    mem.is_load = false;
-    (*this)(mem);
+    // The actual operation stores the new value back in the original shared memory location.
+    // However we cannot reliably track shared memory values, so do_mem_store() doesn't do
+    // anything if we try to call it, so we don't bother invoking a store operation here.
 
     // Clear the R11 pseudo-register.
     havoc_register(m_inv, r11);