From 7f11e03198d01300c6af565352a7dd23aaae07da Mon Sep 17 00:00:00 2001 From: Dave Thaler Date: Wed, 3 Jan 2024 15:07:36 -0800 Subject: [PATCH] Add support for atomic XCHG Signed-off-by: Dave Thaler --- src/asm_ostream.cpp | 8 +++++--- src/asm_parse.cpp | 6 ++++-- src/crab/ebpf_domain.cpp | 3 ++- src/ebpf_vm_isa.hpp | 4 ++-- test-data/atomic.yaml | 24 ++++++++++++++++++++++++ 5 files changed, 37 insertions(+), 8 deletions(-) diff --git a/src/asm_ostream.cpp b/src/asm_ostream.cpp index fbb3e6c68..003bfa5c8 100644 --- a/src/asm_ostream.cpp +++ b/src/asm_ostream.cpp @@ -341,17 +341,19 @@ struct InstructionPrinterVisitor { print(b.access); os_ << " "; + bool showfetch = true; switch ((AtomicOp)((uint32_t)b.op & (uint32_t)AtomicOp::INST_ATOMIC_BASE_MASK)) { case AtomicOp::INST_ATOMIC_ADD: os_ << "+"; break; case AtomicOp::INST_ATOMIC_OR: os_ << "|"; break; 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; } os_ << "= " << b.valreg; - if ((uint32_t)b.op & (uint32_t)AtomicOp::INST_ATOMIC_FETCH) { - os_ << "; " << b.valreg << " = "; - print(b.access); + if (showfetch && ((uint32_t)b.op & (uint32_t)AtomicOp::INST_ATOMIC_FETCH)) { + os_ << " fetch"; } } diff --git a/src/asm_parse.cpp b/src/asm_parse.cpp index 3bf1bdb05..e1ecda839 100644 --- a/src/asm_parse.cpp +++ b/src/asm_parse.cpp @@ -34,7 +34,7 @@ using crab::linear_expression_t; #define ASSIGN R"_(\s*=\s*)_" #define LONGLONG R"_(\s*(ll|)\s*)_" #define UNOP R"_((-|be16|be32|be64|le16|le32|le64|swap16|swap32|swap64))_" -#define ATOMICOP R"_((\+|\||&|\^)=)_" +#define ATOMICOP R"_((\+|\||&|\^|x|cx)=)_" #define PLUSMINUS R"_((\s*[+-])\s*)_" #define LPAREN R"_(\s*\(\s*)_" @@ -85,7 +85,9 @@ static const std::map str_to_cmpop = { static const std::map str_to_atomicop = {{"+", AtomicOp::INST_ATOMIC_ADD}, {"|", AtomicOp::INST_ATOMIC_OR}, {"&", AtomicOp::INST_ATOMIC_AND}, - {"^", AtomicOp::INST_ATOMIC_XOR}}; + {"^", AtomicOp::INST_ATOMIC_XOR}, + {"x", AtomicOp::INST_ATOMIC_XCHG}, + {"cx", AtomicOp::INST_ATOMIC_CMPXCHG}}; static const std::map str_to_atomicfetchop = {{"+", AtomicOp::INST_ATOMIC_ADD_FETCH}, {"|", AtomicOp::INST_ATOMIC_OR_FETCH}, diff --git a/src/crab/ebpf_domain.cpp b/src/crab/ebpf_domain.cpp index b4a21a2d0..b8a25ffb3 100644 --- a/src/crab/ebpf_domain.cpp +++ b/src/crab/ebpf_domain.cpp @@ -2130,7 +2130,8 @@ 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; - default: + 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; } diff --git a/src/ebpf_vm_isa.hpp b/src/ebpf_vm_isa.hpp index 0ef3035a9..a83aad7d0 100644 --- a/src/ebpf_vm_isa.hpp +++ b/src/ebpf_vm_isa.hpp @@ -105,10 +105,10 @@ enum class AtomicOp { INST_ATOMIC_XOR = 0xa0, INST_ATOMIC_XOR_FETCH = (INST_ATOMIC_XOR | INST_ATOMIC_FETCH), INST_ATOMIC_XCHG_BASE = 0xe0, // Not valid by itself - INST_ATOMIX_CMPXCHG_BASE = 0xf0, // Not valid by itself + INST_ATOMIC_CMPXCHG_BASE = 0xf0, // Not valid by itself INST_ATOMIC_XCHG = (INST_ATOMIC_XCHG_BASE | INST_ATOMIC_FETCH), - INST_ATOMIC_CMPXCHG = (INST_ATOMIX_CMPXCHG_BASE | INST_ATOMIC_FETCH), + INST_ATOMIC_CMPXCHG = (INST_ATOMIC_CMPXCHG_BASE | INST_ATOMIC_FETCH), }; int opcode_to_width(uint8_t opcode); diff --git a/test-data/atomic.yaml b/test-data/atomic.yaml index 5ea280e7a..1311eb3f1 100644 --- a/test-data/atomic.yaml +++ b/test-data/atomic.yaml @@ -192,3 +192,27 @@ 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 XCHG + +pre: ["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: + : | + lock *(u32 *)(r2 + 4) x= r1 + +post: ["r1.type=number", + "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 XCHG + +pre: ["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: + : | + lock *(u64 *)(r2 + 4) x= r1 + +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"]