From 9d7101e7ef7240bf897f1a3eaf434479319a1922 Mon Sep 17 00:00:00 2001
From: Dave Thaler <dthaler1968@gmail.com>
Date: Thu, 14 Mar 2024 13:40:19 -0700
Subject: [PATCH] Added atomic_to_bin function

Signed-off-by: Dave Thaler <dthaler1968@gmail.com>
---
 src/crab/ebpf_domain.cpp | 28 +++++++++++++++++-----------
 1 file changed, 17 insertions(+), 11 deletions(-)

diff --git a/src/crab/ebpf_domain.cpp b/src/crab/ebpf_domain.cpp
index 9ecfc49e2..a8c9e1f01 100644
--- a/src/crab/ebpf_domain.cpp
+++ b/src/crab/ebpf_domain.cpp
@@ -2154,6 +2154,22 @@ void ebpf_domain_t::do_mem_store(const Mem& b, Type val_type, SValue val_svalue,
     });
 }
 
+// Construct a Bin operation that does the main operation that a given Atomic operation does atomically.
+static Bin atomic_to_bin(const Atomic& a) {
+    Bin bin{
+        .dst = Reg{R11_ATOMIC_SCRATCH}, .v = a.valreg, .is64 = (a.access.width == sizeof(uint64_t)), .lddw = false};
+    switch (a.op) {
+    case Atomic::Op::ADD: bin.op = Bin::Op::ADD; break;
+    case Atomic::Op::OR: bin.op = Bin::Op::OR; break;
+    case Atomic::Op::AND: bin.op = Bin::Op::AND; break;
+    case Atomic::Op::XOR: bin.op = Bin::Op::XOR; break;
+    case Atomic::Op::XCHG:
+    case Atomic::Op::CMPXCHG: bin.op = Bin::Op::MOV; break;
+    default: throw std::exception();
+    }
+    return bin;
+}
+
 void ebpf_domain_t::operator()(const Atomic& a) {
     if (m_inv.is_bottom())
         return;
@@ -2176,17 +2192,7 @@ void ebpf_domain_t::operator()(const Atomic& a) {
     (*this)(Mem{.access = a.access, .value = r11, .is_load = true});
 
     // Compute the new value in R11.
-    Bin bin {.dst = r11, .v = a.valreg, .is64 = (a.access.width == sizeof(uint64_t)), .lddw = false};
-    switch (a.op) {
-    case Atomic::Op::ADD: bin.op = Bin::Op::ADD; break;
-    case Atomic::Op::OR: bin.op = Bin::Op::OR; break;
-    case Atomic::Op::AND: bin.op = Bin::Op::AND; break;
-    case Atomic::Op::XOR: bin.op = Bin::Op::XOR; break;
-    case Atomic::Op::XCHG:
-    case Atomic::Op::CMPXCHG: bin.op = Bin::Op::MOV; break;
-    default: throw std::exception();
-    }
-    (*this)(bin);
+    (*this)(atomic_to_bin(a));
 
     if (a.op == Atomic::Op::CMPXCHG) {
         // For CMPXCHG, store the original value in r0.