From a7c4cfc09be30bd6573e285c6573622752f84fd5 Mon Sep 17 00:00:00 2001 From: Dave Thaler Date: Thu, 14 Mar 2024 15:37:39 -0700 Subject: [PATCH] add other atomic instructions (#558) Fixes #483 * Fast path for atomic operations on shared memory --------- Signed-off-by: Dave Thaler --- src/asm_cfg.cpp | 2 +- src/asm_marshal.cpp | 15 +- src/asm_ostream.cpp | 18 +- src/asm_ostream.hpp | 2 +- src/asm_parse.cpp | 18 +- src/asm_syntax.hpp | 21 +- src/asm_unmarshal.cpp | 34 +- src/assertions.cpp | 10 +- src/crab/ebpf_domain.cpp | 65 +++- src/crab/ebpf_domain.hpp | 2 +- src/ebpf_vm_isa.hpp | 20 +- src/test/test_conformance.cpp | 40 +-- src/test/test_marshal.cpp | 25 +- src/test/test_yaml.cpp | 1 + test-data/atomic.yaml | 578 ++++++++++++++++++++++++++++++++++ 15 files changed, 788 insertions(+), 63 deletions(-) create mode 100644 test-data/atomic.yaml diff --git a/src/asm_cfg.cpp b/src/asm_cfg.cpp index 1b37a4328..b67e87921 100644 --- a/src/asm_cfg.cpp +++ b/src/asm_cfg.cpp @@ -178,7 +178,7 @@ static std::string instype(Instruction ins) { return "callx"; } else if (std::holds_alternative(ins)) { return std::get(ins).is_load ? "load" : "store"; - } else if (std::holds_alternative(ins)) { + } else if (std::holds_alternative(ins)) { return "load_store"; } else if (std::holds_alternative(ins)) { return "packet_access"; diff --git a/src/asm_marshal.cpp b/src/asm_marshal.cpp index a80f20345..5e7f015e7 100644 --- a/src/asm_marshal.cpp +++ b/src/asm_marshal.cpp @@ -219,7 +219,7 @@ struct MarshalVisitor { vector operator()(Mem const& b) { Deref access = b.access; ebpf_inst res{ - .opcode = static_cast((INST_MEM << 5) | width_to_opcode(access.width)), + .opcode = static_cast(INST_MODE_MEM | width_to_opcode(access.width)), .dst = 0, .src = 0, .offset = static_cast(access.offset), @@ -253,21 +253,24 @@ struct MarshalVisitor { .imm = static_cast(b.offset), }; if (b.regoffset) { - res.opcode |= (INST_IND << 5); + res.opcode |= INST_MODE_IND; res.src = b.regoffset->v; } else { - res.opcode |= (INST_ABS << 5); + res.opcode |= INST_MODE_ABS; } return {res}; } - vector operator()(LockAdd const& b) { + vector operator()(Atomic const& b) { + int32_t imm = (int32_t)b.op; + if (b.fetch) + imm |= INST_FETCH; return {ebpf_inst{ - .opcode = static_cast(INST_CLS_ST | 0x1 | (INST_XADD << 5) | width_to_opcode(b.access.width)), + .opcode = static_cast(INST_CLS_STX | INST_MODE_ATOMIC | width_to_opcode(b.access.width)), .dst = b.access.basereg.v, .src = b.valreg.v, .offset = static_cast(b.access.offset), - .imm = 0}}; + .imm = imm}}; } vector operator()(IncrementLoopCounter const& ins) { diff --git a/src/asm_ostream.cpp b/src/asm_ostream.cpp index 66e8f1991..283bece2d 100644 --- a/src/asm_ostream.cpp +++ b/src/asm_ostream.cpp @@ -328,10 +328,24 @@ struct InstructionPrinterVisitor { } } - void operator()(LockAdd const& b) { + void operator()(Atomic const& b) { os_ << "lock "; print(b.access); - os_ << " += " << b.valreg; + os_ << " "; + bool showfetch = true; + switch (b.op) { + case Atomic::Op::ADD: os_ << "+"; break; + case Atomic::Op::OR : os_ << "|"; break; + case Atomic::Op::AND: os_ << "&"; break; + case Atomic::Op::XOR: os_ << "^"; break; + case Atomic::Op::XCHG: os_ << "x"; showfetch = false; break; + case Atomic::Op::CMPXCHG: os_ << "cx"; showfetch = false; break; + } + os_ << "= " << b.valreg; + + if (showfetch && b.fetch) { + os_ << " fetch"; + } } void operator()(Assume const& b) { diff --git a/src/asm_ostream.hpp b/src/asm_ostream.hpp index 31af5d63c..e51842cad 100644 --- a/src/asm_ostream.hpp +++ b/src/asm_ostream.hpp @@ -59,7 +59,7 @@ inline std::ostream& operator<<(std::ostream& os, Exit const& a) { return os << inline std::ostream& operator<<(std::ostream& os, Jmp const& a) { return os << (Instruction)a; } inline std::ostream& operator<<(std::ostream& os, Packet const& a) { return os << (Instruction)a; } inline std::ostream& operator<<(std::ostream& os, Mem const& a) { return os << (Instruction)a; } -inline std::ostream& operator<<(std::ostream& os, LockAdd const& a) { return os << (Instruction)a; } +inline std::ostream& operator<<(std::ostream& os, Atomic const& a) { return os << (Instruction)a; } inline std::ostream& operator<<(std::ostream& os, Assume const& a) { return os << (Instruction)a; } inline std::ostream& operator<<(std::ostream& os, Assert const& a) { return os << (Instruction)a; } inline std::ostream& operator<<(std::ostream& os, IncrementLoopCounter const& a) { return os << (Instruction)a; } diff --git a/src/asm_parse.cpp b/src/asm_parse.cpp index a6e00d89b..474446fbd 100644 --- a/src/asm_parse.cpp +++ b/src/asm_parse.cpp @@ -34,6 +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"_((\+|\||&|\^|x|cx)=)_" #define PLUSMINUS R"_((\s*[+-])\s*)_" #define LPAREN R"_(\s*\(\s*)_" @@ -81,6 +82,14 @@ static const std::map str_to_cmpop = { {"s<", Condition::Op::SLT}, {"s<=", Condition::Op::SLE}, {"s>", Condition::Op::SGT}, {"s>=", Condition::Op::SGE}, }; +static const std::map str_to_atomicop = { + {"+", Atomic::Op::ADD}, + {"|", Atomic::Op::OR}, + {"&", Atomic::Op::AND}, + {"^", Atomic::Op::XOR}, + {"x", Atomic::Op::XCHG}, + {"cx", Atomic::Op::CMPXCHG}}; + static const std::map str_to_width = { {"8", 1}, {"16", 2}, @@ -182,8 +191,13 @@ Instruction parse_instruction(const std::string& line, const std::map; +using Instruction = std::variant; using LabeledInstruction = std::tuple>; using InstructionSeq = std::vector; diff --git a/src/asm_unmarshal.cpp b/src/asm_unmarshal.cpp index b6ad9b670..71232c936 100644 --- a/src/asm_unmarshal.cpp +++ b/src/asm_unmarshal.cpp @@ -177,6 +177,21 @@ struct Unmarshaller { return {}; } + auto getAtomicOp(size_t pc, ebpf_inst inst) -> Atomic::Op { + Atomic::Op op = (Atomic::Op)(inst.imm & ~INST_FETCH); + switch (op) { + case Atomic::Op::XCHG: + case Atomic::Op::CMPXCHG: + if ((inst.imm & INST_FETCH) == 0) + throw InvalidInstruction(pc, "unsupported immediate"); + case Atomic::Op::ADD: + case Atomic::Op::OR: + case Atomic::Op::AND: + case Atomic::Op::XOR: return op; + } + throw InvalidInstruction(pc, "unsupported immediate"); + } + uint64_t sign_extend(int32_t imm) { return (uint64_t)(int64_t)imm; } uint64_t zero_extend(int32_t imm) { return (uint64_t)(uint32_t)imm; } @@ -223,9 +238,10 @@ struct Unmarshaller { int width = getMemWidth(inst.opcode); bool isLD = (inst.opcode & INST_CLS_MASK) == INST_CLS_LD; - switch ((inst.opcode & INST_MODE_MASK) >> 5) { - case 0: throw InvalidInstruction(pc, inst.opcode); - case INST_ABS: + switch (inst.opcode & INST_MODE_MASK) { + case INST_MODE_IMM: + throw InvalidInstruction(pc, inst.opcode); + case INST_MODE_ABS: if (!info.platform->legacy || !isLD || (width == 8)) throw InvalidInstruction(pc, inst.opcode); if (inst.dst != 0) @@ -236,7 +252,7 @@ struct Unmarshaller { throw InvalidInstruction(pc, make_opcode_message("nonzero offset for", inst.opcode)); return Packet{.width = width, .offset = inst.imm, .regoffset = {}}; - case INST_IND: + case INST_MODE_IND: if (!info.platform->legacy || !isLD || (width == 8)) throw InvalidInstruction(pc, inst.opcode); if (inst.dst != 0) @@ -247,7 +263,7 @@ struct Unmarshaller { throw InvalidInstruction(pc, make_opcode_message("nonzero offset for", inst.opcode)); return Packet{.width = width, .offset = inst.imm, .regoffset = Reg{inst.src}}; - case INST_MEM: { + case INST_MODE_MEM: { if (isLD) throw InvalidInstruction(pc, inst.opcode); bool isLoad = getMemIsLoad(inst.opcode); @@ -279,14 +295,14 @@ struct Unmarshaller { return res; } - case INST_XADD: + case INST_MODE_ATOMIC: if (((inst.opcode & INST_CLS_MASK) != INST_CLS_STX) || ((inst.opcode & INST_SIZE_MASK) != INST_SIZE_W && (inst.opcode & INST_SIZE_MASK) != INST_SIZE_DW)) throw InvalidInstruction(pc, inst.opcode); - if (inst.imm != 0) - throw InvalidInstruction(pc, "unsupported immediate"); - return LockAdd{ + return Atomic{ + .op = getAtomicOp(pc, inst), + .fetch = (inst.imm & INST_FETCH) == INST_FETCH, .access = Deref{ .width = width, diff --git a/src/assertions.cpp b/src/assertions.cpp index d760a5420..c3e090134 100644 --- a/src/assertions.cpp +++ b/src/assertions.cpp @@ -170,11 +170,17 @@ class AssertExtractor { return res; } - vector operator()(LockAdd ins) const { + vector operator()(Atomic ins) const { vector res; - res.emplace_back(TypeConstraint{ins.access.basereg, TypeGroup::shared}); + res.emplace_back(TypeConstraint{ins.access.basereg, TypeGroup::pointer}); res.emplace_back(ValidAccess{ins.access.basereg, ins.access.offset, Imm{static_cast(ins.access.width)}, false}); + if (ins.op == Atomic::Op::CMPXCHG) { + // The memory contents pointed to by ins.access will be compared + // against the value of the ins.valreg register. Only numbers are + // supported. + res.emplace_back(TypeConstraint{ins.valreg, TypeGroup::number}); + } return res; } diff --git a/src/crab/ebpf_domain.cpp b/src/crab/ebpf_domain.cpp index f0b06bcc1..a8c9e1f01 100644 --- a/src/crab/ebpf_domain.cpp +++ b/src/crab/ebpf_domain.cpp @@ -2154,8 +2154,69 @@ void ebpf_domain_t::do_mem_store(const Mem& b, Type val_type, SValue val_svalue, }); } -void ebpf_domain_t::operator()(const LockAdd& a) { - // nothing to do here +// 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; + if (!m_inv.entail(type_is_pointer(reg_pack(a.access.basereg))) || + !m_inv.entail(type_is_number(reg_pack(a.valreg)))) { + return; + } + if (m_inv.entail(type_is_not_stack(reg_pack(a.access.basereg)))) { + // Shared memory regions are volatile so we can just havoc + // any register that will be updated. + if (a.op == Atomic::Op::CMPXCHG) + havoc_register(m_inv, Reg{R0_RETURN_VALUE}); + else if (a.fetch) + havoc_register(m_inv, a.valreg); + return; + } + + // Fetch the current value into the R11 pseudo-register. + const Reg r11{R11_ATOMIC_SCRATCH}; + (*this)(Mem{.access = a.access, .value = r11, .is_load = true}); + + // Compute the new value in R11. + (*this)(atomic_to_bin(a)); + + if (a.op == Atomic::Op::CMPXCHG) { + // For CMPXCHG, store the original value in r0. + (*this)(Mem{.access = a.access, .value = Reg{R0_RETURN_VALUE}, .is_load = true}); + + // For the destination, there are 3 possibilities: + // 1) dst.value == r0.value : set R11 to valreg + // 2) dst.value != r0.value : don't modify R11 + // 3) dst.value may or may not == r0.value : set R11 to the union of R11 and valreg + // For now we just havoc the value of R11. + havoc_register(m_inv, r11); + } else if (a.fetch) { + // For other FETCH operations, store the original value in the src register. + (*this)(Mem{.access = a.access, .value = a.valreg, .is_load = true}); + } + + // Store the new value back in the original shared memory location. + // Note that do_mem_store() currently doesn't track shared memory values, + // but stack memory values are tracked and are legal here. + (*this)(Mem{.access = a.access, .value = r11, .is_load = false}); + + // Clear the R11 pseudo-register. + havoc_register(m_inv, r11); + type_inv.havoc_type(m_inv, r11); } void ebpf_domain_t::operator()(const Call& call) { diff --git a/src/crab/ebpf_domain.hpp b/src/crab/ebpf_domain.hpp index efc2dabc8..39f11e73b 100644 --- a/src/crab/ebpf_domain.hpp +++ b/src/crab/ebpf_domain.hpp @@ -67,7 +67,7 @@ class ebpf_domain_t final { void operator()(const FuncConstraint&); void operator()(const Jmp&); void operator()(const LoadMapFd&); - void operator()(const LockAdd&); + void operator()(const Atomic&); void operator()(const Mem&); void operator()(const ValidDivisor&); void operator()(const Packet&); diff --git a/src/ebpf_vm_isa.hpp b/src/ebpf_vm_isa.hpp index 1b60c8478..8af2b2503 100644 --- a/src/ebpf_vm_isa.hpp +++ b/src/ebpf_vm_isa.hpp @@ -45,16 +45,19 @@ enum { INST_MODE_MASK = 0xe0, - INST_ABS = 1, // Deprecated - INST_IND = 2, // Deprecated - INST_MEM = 3, - INST_LEN = 4, - INST_MSH = 5, - INST_XADD = 6, - INST_MEM_UNUSED = 7, + INST_MODE_IMM = 0x00, // 64-bit immediate instructions + INST_MODE_ABS = 0x20, // legacy BPF packet access (absolute) + INST_MODE_IND = 0x40, // legacy BPF packet access (indirect) + INST_MODE_MEM = 0x60, // regular load and store operations + INST_MODE_MEMSX = 0x80, // sign-extension load operations + INST_MODE_UNUSED1 = 0xa0, + INST_MODE_ATOMIC = 0xc0, // atomic operations + INST_MODE_UNUSED2 = 0xe0, INST_OP_LDDW_IMM = (INST_CLS_LD | INST_SRC_IMM | INST_SIZE_DW), // Special + INST_FETCH = 0x1, + INST_JA = 0x0, INST_CALL = 0x8, INST_EXIT = 0x9, @@ -91,7 +94,8 @@ enum { R7 = 7, R8 = 8, R9 = 9, - R10_STACK_POINTER = 10 + R10_STACK_POINTER = 10, + R11_ATOMIC_SCRATCH = 11, // Pseudo-register used internally for atomic instructions. }; int opcode_to_width(uint8_t opcode); diff --git a/src/test/test_conformance.cpp b/src/test/test_conformance.cpp index 7474d7257..b1f2dce57 100644 --- a/src/test/test_conformance.cpp +++ b/src/test/test_conformance.cpp @@ -149,26 +149,26 @@ TEST_CONFORMANCE("ldxw.data") TEST_CONFORMANCE("le16.data") TEST_CONFORMANCE("le32.data") TEST_CONFORMANCE("le64.data") -TEST_CONFORMANCE_VERIFICATION_FAILED("lock_add.data") -TEST_CONFORMANCE_VERIFICATION_FAILED("lock_add32.data") -TEST_CONFORMANCE_VERIFICATION_FAILED("lock_and.data") -TEST_CONFORMANCE_VERIFICATION_FAILED("lock_and32.data") -TEST_CONFORMANCE_VERIFICATION_FAILED("lock_cmpxchg.data") -TEST_CONFORMANCE_VERIFICATION_FAILED("lock_cmpxchg32.data") -TEST_CONFORMANCE_VERIFICATION_FAILED("lock_fetch_add.data") -TEST_CONFORMANCE_VERIFICATION_FAILED("lock_fetch_add32.data") -TEST_CONFORMANCE_VERIFICATION_FAILED("lock_fetch_and.data") -TEST_CONFORMANCE_VERIFICATION_FAILED("lock_fetch_and32.data") -TEST_CONFORMANCE_VERIFICATION_FAILED("lock_fetch_or.data") -TEST_CONFORMANCE_VERIFICATION_FAILED("lock_fetch_or32.data") -TEST_CONFORMANCE_VERIFICATION_FAILED("lock_fetch_xor.data") -TEST_CONFORMANCE_VERIFICATION_FAILED("lock_fetch_xor32.data") -TEST_CONFORMANCE_VERIFICATION_FAILED("lock_or.data") -TEST_CONFORMANCE_VERIFICATION_FAILED("lock_or32.data") -TEST_CONFORMANCE_VERIFICATION_FAILED("lock_xchg.data") -TEST_CONFORMANCE_VERIFICATION_FAILED("lock_xchg32.data") -TEST_CONFORMANCE_VERIFICATION_FAILED("lock_xor.data") -TEST_CONFORMANCE_VERIFICATION_FAILED("lock_xor32.data") +TEST_CONFORMANCE("lock_add.data") +TEST_CONFORMANCE_RANGE("lock_add32.data", "[0, 1311768467463790321]") +TEST_CONFORMANCE("lock_and.data") +TEST_CONFORMANCE_TOP("lock_and32.data") +TEST_CONFORMANCE_TOP("lock_cmpxchg.data") +TEST_CONFORMANCE_TOP("lock_cmpxchg32.data") +TEST_CONFORMANCE("lock_fetch_add.data") +TEST_CONFORMANCE_RANGE("lock_fetch_add32.data", "[0, 1311768467463790321]") +TEST_CONFORMANCE("lock_fetch_and.data") +TEST_CONFORMANCE_TOP("lock_fetch_and32.data") +TEST_CONFORMANCE("lock_fetch_or.data") +TEST_CONFORMANCE_TOP("lock_fetch_or32.data") +TEST_CONFORMANCE("lock_fetch_xor.data") +TEST_CONFORMANCE_TOP("lock_fetch_xor32.data") +TEST_CONFORMANCE("lock_or.data") +TEST_CONFORMANCE_TOP("lock_or32.data") +TEST_CONFORMANCE("lock_xchg.data") +TEST_CONFORMANCE("lock_xchg32.data") +TEST_CONFORMANCE("lock_xor.data") +TEST_CONFORMANCE_TOP("lock_xor32.data") TEST_CONFORMANCE("lsh32-imm.data") TEST_CONFORMANCE("lsh32-imm-high.data") TEST_CONFORMANCE("lsh32-imm-neg.data") diff --git a/src/test/test_marshal.cpp b/src/test/test_marshal.cpp index c3ff87c30..02ee4c4ff 100644 --- a/src/test/test_marshal.cpp +++ b/src/test/test_marshal.cpp @@ -434,11 +434,26 @@ TEST_CASE("disasm_marshal", "[disasm][marshal]") { } } - SECTION("LockAdd") { + SECTION("Atomic") { for (int w : ws) { if (w == 4 || w == 8) { Deref access{.width = w, .basereg = Reg{2}, .offset = 17}; - compare_marshal_unmarshal(LockAdd{.access = access, .valreg = Reg{1}}); + compare_marshal_unmarshal(Atomic{.op = Atomic::Op::ADD, .fetch = false, .access = access, .valreg = Reg{1}}); + compare_marshal_unmarshal(Atomic{.op = Atomic::Op::ADD, .fetch = true, .access = access, .valreg = Reg{1}}); + compare_marshal_unmarshal(Atomic{.op = Atomic::Op::OR, .fetch = false, .access = access, .valreg = Reg{1}}); + compare_marshal_unmarshal(Atomic{.op = Atomic::Op::OR, .fetch = true, .access = access, .valreg = Reg{1}}); + compare_marshal_unmarshal(Atomic{.op = Atomic::Op::AND, .fetch = false, .access = access, .valreg = Reg{1}}); + compare_marshal_unmarshal(Atomic{.op = Atomic::Op::AND, .fetch = true, .access = access, .valreg = Reg{1}}); + compare_marshal_unmarshal(Atomic{.op = Atomic::Op::XOR, .fetch = false, .access = access, .valreg = Reg{1}}); + compare_marshal_unmarshal(Atomic{.op = Atomic::Op::XOR, .fetch = true, .access = access, .valreg = Reg{1}}); + check_marshal_unmarshal_fail( + Atomic{.op = Atomic::Op::XCHG, .fetch = false, .access = access, .valreg = Reg{1}}, + "0: unsupported immediate\n"); + compare_marshal_unmarshal(Atomic{.op = Atomic::Op::XCHG, .fetch = true, .access = access, .valreg = Reg{1}}); + check_marshal_unmarshal_fail( + Atomic{.op = Atomic::Op::CMPXCHG, .fetch = false, .access = access, .valreg = Reg{1}}, + "0: unsupported immediate\n"); + compare_marshal_unmarshal(Atomic{.op = Atomic::Op::CMPXCHG, .fetch = true, .access = access, .valreg = Reg{1}}); } } } @@ -450,7 +465,7 @@ TEST_CASE("marshal", "[disasm][marshal]") { Mem m{.access = access, .value = Reg{3}, .is_load = true}; auto ins = marshal(m, 0).at(0); ebpf_inst expect{ - .opcode = (uint8_t)(INST_CLS_LD | (INST_MEM << 5) | width_to_opcode(1) | 0x1), + .opcode = (uint8_t)(INST_CLS_LD | INST_MODE_MEM | width_to_opcode(1) | 0x1), .dst = 3, .src = 4, .offset = 6, @@ -473,7 +488,7 @@ TEST_CASE("marshal", "[disasm][marshal]") { REQUIRE(ins.dst == 4); REQUIRE(ins.offset == 6); REQUIRE(ins.imm == 0); - REQUIRE(ins.opcode == (uint8_t)(INST_CLS_ST | (INST_MEM << 5) | width_to_opcode(1) | 0x1)); + REQUIRE(ins.opcode == (uint8_t)(INST_CLS_ST | INST_MODE_MEM | width_to_opcode(1) | 0x1)); } SECTION("StoreImm") { Deref access{.width = 1, .basereg = Reg{4}, .offset = 6}; @@ -482,7 +497,7 @@ TEST_CASE("marshal", "[disasm][marshal]") { REQUIRE(ins.dst == 4); REQUIRE(ins.offset == 6); REQUIRE(ins.imm == 3); - REQUIRE(ins.opcode == (uint8_t)(INST_CLS_ST | (INST_MEM << 5) | width_to_opcode(1) | 0x0)); + REQUIRE(ins.opcode == (uint8_t)(INST_CLS_ST | INST_MODE_MEM | width_to_opcode(1) | 0x0)); } } diff --git a/src/test/test_yaml.cpp b/src/test/test_yaml.cpp index f94b598d0..da124a8bf 100644 --- a/src/test/test_yaml.cpp +++ b/src/test/test_yaml.cpp @@ -21,6 +21,7 @@ YAML_CASE("test-data/add.yaml") YAML_CASE("test-data/assign.yaml") +YAML_CASE("test-data/atomic.yaml") YAML_CASE("test-data/bitop.yaml") YAML_CASE("test-data/call.yaml") YAML_CASE("test-data/callx.yaml") diff --git a/test-data/atomic.yaml b/test-data/atomic.yaml new file mode 100644 index 000000000..2e4787ef3 --- /dev/null +++ b/test-data/atomic.yaml @@ -0,0 +1,578 @@ +# Copyright (c) Prevail Verifier contributors. +# SPDX-License-Identifier: MIT +--- +test-case: atomic 32-bit ADD shared + +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) += 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 32-bit ADD and fetch shared + +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) += r1 fetch + +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 ADD shared + +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) += 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"] +--- +test-case: atomic 64-bit ADD and fetch shared + +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) += r1 fetch + +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 AND shared + +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) &= 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 32-bit AND and fetch shared + +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) &= r1 fetch + +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 AND shared + +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) &= 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"] +--- +test-case: atomic 64-bit AND and fetch shared + +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) &= r1 fetch + +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 OR shared + +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) |= 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 32-bit OR and fetch shared + +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) |= r1 fetch + +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 OR shared + +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) |= 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"] +--- +test-case: atomic 64-bit OR and fetch shared + +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) |= r1 fetch + +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 XOR shared + +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) ^= 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 32-bit XOR and fetch shared + +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) ^= r1 fetch + +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 XOR shared + +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) ^= 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"] +--- +test-case: atomic 64-bit XOR and fetch shared + +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) ^= r1 fetch + +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 shared + +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 shared + +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"] +--- +test-case: atomic 32-bit CMPXCHG shared + +pre: ["r0.type=number", "r0.svalue=1", "r0.uvalue=1", + "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) cx= r1 + +post: ["r0.type=number", + "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 shared + +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: + : | + lock *(u64 *)(r2 + 4) cx= r1 + +post: ["r0.type=number", + "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 shared 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: + : | + 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 stack + +pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2", + "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "s[4...7].type=number", "s[4...7].svalue=1", "s[4...7].uvalue=1"] + +code: + : | + lock *(u32 *)(r2 + 4) += r1 + +post: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2", + "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "s[4...7].type=number", "s[4...7].svalue=3", "s[4...7].uvalue=3"] +--- +test-case: atomic 32-bit ADD and fetch stack + +pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2", + "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "s[4...7].type=number", "s[4...7].svalue=1", "s[4...7].uvalue=1"] + +code: + : | + lock *(u32 *)(r2 + 4) += r1 fetch + +post: ["r1.type=number", "r1.svalue=1", "r1.uvalue=1", + "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "s[4...7].type=number", "s[4...7].svalue=3", "s[4...7].uvalue=3"] +--- +test-case: atomic 64-bit ADD stack + +pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2", + "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "s[4...11].type=number", "s[4...11].svalue=1", "s[4...11].uvalue=1"] + +code: + : | + lock *(u64 *)(r2 + 4) += r1 + +post: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2", + "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "s[4...11].type=number", "s[4...11].svalue=3", "s[4...11].uvalue=3"] +--- +test-case: atomic 64-bit ADD and fetch stack + +pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2", + "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "s[4...11].type=number", "s[4...11].svalue=1", "s[4...11].uvalue=1"] + +code: + : | + lock *(u64 *)(r2 + 4) += r1 fetch + +post: ["r1.type=number", "r1.svalue=1", "r1.uvalue=1", + "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "s[4...11].type=number", "s[4...11].svalue=3", "s[4...11].uvalue=3"] +--- +test-case: atomic 32-bit AND stack + +pre: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3", + "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "s[4...7].type=number", "s[4...7].svalue=5", "s[4...7].uvalue=5"] + +code: + : | + lock *(u32 *)(r2 + 4) &= r1 + +post: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3", + "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "s[4...7].type=number", "s[4...7].svalue=1", "s[4...7].uvalue=1"] +--- +test-case: atomic 32-bit AND and fetch stack + +pre: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3", + "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "s[4...7].type=number", "s[4...7].svalue=5", "s[4...7].uvalue=5"] + +code: + : | + lock *(u32 *)(r2 + 4) &= r1 fetch + +post: ["r1.type=number", "r1.svalue=5", "r1.uvalue=5", + "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "s[4...7].type=number", "s[4...7].svalue=1", "s[4...7].uvalue=1"] +--- +test-case: atomic 64-bit AND stack + +pre: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3", + "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "s[4...11].type=number", "s[4...11].svalue=5", "s[4...11].uvalue=5"] + +code: + : | + lock *(u64 *)(r2 + 4) &= r1 + +post: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3", + "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "s[4...11].type=number", "s[4...11].svalue=1", "s[4...11].uvalue=1"] +--- +test-case: atomic 64-bit AND and fetch stack + +pre: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3", + "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "s[4...11].type=number", "s[4...11].svalue=5", "s[4...11].uvalue=5"] + +code: + : | + lock *(u64 *)(r2 + 4) &= r1 fetch + +post: ["r1.type=number", "r1.svalue=5", "r1.uvalue=5", + "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "s[4...11].type=number", "s[4...11].svalue=1", "s[4...11].uvalue=1"] +--- +test-case: atomic 32-bit OR stack + +pre: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3", + "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "s[4...7].type=number", "s[4...7].svalue=5", "s[4...7].uvalue=5"] + +code: + : | + lock *(u32 *)(r2 + 4) |= r1 + +post: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3", + "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "s[4...7].type=number", "s[4...7].svalue=7", "s[4...7].uvalue=7"] +--- +test-case: atomic 32-bit OR and fetch stack + +pre: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3", + "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "s[4...7].type=number", "s[4...7].svalue=5", "s[4...7].uvalue=5"] + +code: + : | + lock *(u32 *)(r2 + 4) |= r1 fetch + +post: ["r1.type=number", "r1.svalue=5", "r1.uvalue=5", + "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "s[4...7].type=number", "s[4...7].svalue=7", "s[4...7].uvalue=7"] +--- +test-case: atomic 64-bit OR stack + +pre: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3", + "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "s[4...11].type=number", "s[4...11].svalue=5", "s[4...11].uvalue=5"] + +code: + : | + lock *(u64 *)(r2 + 4) |= r1 + +post: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3", + "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "s[4...11].type=number", "s[4...11].svalue=7", "s[4...11].uvalue=7"] +--- +test-case: atomic 64-bit OR and fetch stack + +pre: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3", + "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "s[4...11].type=number", "s[4...11].svalue=5", "s[4...11].uvalue=5"] + +code: + : | + lock *(u64 *)(r2 + 4) |= r1 fetch + +post: ["r1.type=number", "r1.svalue=5", "r1.uvalue=5", + "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "s[4...11].type=number", "s[4...11].svalue=7", "s[4...11].uvalue=7"] +--- +test-case: atomic 32-bit XOR stack + +pre: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3", + "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "s[4...7].type=number", "s[4...7].svalue=5", "s[4...7].uvalue=5"] + +code: + : | + lock *(u32 *)(r2 + 4) ^= r1 + +post: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3", + "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "s[4...7].type=number", "s[4...7].svalue=6", "s[4...7].uvalue=6"] +--- +test-case: atomic 32-bit XOR and fetch stack + +pre: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3", + "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "s[4...7].type=number", "s[4...7].svalue=5", "s[4...7].uvalue=5"] + +code: + : | + lock *(u32 *)(r2 + 4) ^= r1 fetch + +post: ["r1.type=number", "r1.svalue=5", "r1.uvalue=5", + "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "s[4...7].type=number", "s[4...7].svalue=6", "s[4...7].uvalue=6"] +--- +test-case: atomic 64-bit XOR stack + +pre: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3", + "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "s[4...11].type=number", "s[4...11].svalue=5", "s[4...11].uvalue=5"] + +code: + : | + lock *(u64 *)(r2 + 4) ^= r1 + +post: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3", + "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "s[4...11].type=number", "s[4...11].svalue=6", "s[4...11].uvalue=6"] +--- +test-case: atomic 64-bit XOR and fetch stack + +pre: ["r1.type=number", "r1.svalue=3", "r1.uvalue=3", + "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "s[4...11].type=number", "s[4...11].svalue=5", "s[4...11].uvalue=5"] + +code: + : | + lock *(u64 *)(r2 + 4) ^= r1 fetch + +post: ["r1.type=number", "r1.svalue=5", "r1.uvalue=5", + "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "s[4...11].type=number", "s[4...11].svalue=6", "s[4...11].uvalue=6"] +--- +test-case: atomic 32-bit XCHG stack + +pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2", + "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "s[4...7].type=number", "s[4...7].svalue=5", "s[4...7].uvalue=5"] + +code: + : | + lock *(u32 *)(r2 + 4) x= r1 + +post: ["r1.type=number", "r1.svalue=5", "r1.uvalue=5", + "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "s[4...7].type=number", "s[4...7].svalue=2", "s[4...7].uvalue=2"] +--- +test-case: atomic 64-bit XCHG stack + +pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2", + "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "s[4...11].type=number", "s[4...11].svalue=5", "s[4...11].uvalue=5"] + +code: + : | + lock *(u64 *)(r2 + 4) x= r1 + +post: ["r1.type=number", "r1.svalue=5", "r1.uvalue=5", + "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "s[4...11].type=number", "s[4...11].svalue=2", "s[4...11].uvalue=2"] +--- +test-case: atomic 32-bit CMPXCHG stack + +pre: ["r0.type=number", "r0.svalue=1", "r0.uvalue=1", + "r1.type=number", "r1.svalue=2", "r1.uvalue=2", + "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "s[4...7].type=number", "s[4...7].svalue=1", "s[4...7].uvalue=1"] + +code: + : | + lock *(u32 *)(r2 + 4) cx= r1 + +post: ["r0.type=number", "r0.svalue=1", "r0.uvalue=1", + "r1.type=number", "r1.svalue=2", "r1.uvalue=2", + "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "s[4...7].type=number"] +--- +test-case: atomic 64-bit CMPXCHG stack + +pre: ["r0.type=number", "r0.svalue=1", "r0.uvalue=1", + "r1.type=number", "r1.svalue=2", "r1.uvalue=2", + "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "s[4...11].type=number", "s[4...11].svalue=1", "s[4...11].uvalue=1"] + +code: + : | + lock *(u64 *)(r2 + 4) cx= r1 + +post: ["r0.type=number", "r0.svalue=1", "r0.uvalue=1", + "r1.type=number", "r1.svalue=2", "r1.uvalue=2", + "r2.type=stack", "r2.stack_offset=0", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue", + "s[4...11].type=number"] +--- +test-case: atomic 32-bit ADD to non-pointer space + +pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2", + "r2.type=number", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"] + +code: + : | + lock *(u32 *)(r2 + 4) += r1 + +post: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2", + "r2.type=number", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"] + +messages: + - "0: Invalid type (r2.type in {ctx, stack, packet, shared})" + - "0: Only pointers can be dereferenced (valid_access(r2.offset+4, width=4) for write)" +--- +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: + : | + 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: Invalid type (r1.type == number)"