From 8357d591d796e3e3bc16dfef0d8eca64eaa5d0fc Mon Sep 17 00:00:00 2001 From: Dave Thaler Date: Wed, 3 Jan 2024 19:23:05 -0800 Subject: [PATCH] Add some failure test cases Signed-off-by: Dave Thaler --- src/asm_ostream.cpp | 17 +-------------- src/asm_unmarshal.cpp | 1 - src/assertions.cpp | 6 +++++ src/crab/ebpf_domain.cpp | 12 +++++++++- test-data/atomic.yaml | 47 ++++++++++++++++++++++++++++++++++++++++ 5 files changed, 65 insertions(+), 18 deletions(-) diff --git a/src/asm_ostream.cpp b/src/asm_ostream.cpp index 003bfa5c8..776f372cb 100644 --- a/src/asm_ostream.cpp +++ b/src/asm_ostream.cpp @@ -324,21 +324,6 @@ struct InstructionPrinterVisitor { void operator()(Atomic const& b) { os_ << "lock "; - - if (b.op == AtomicOp::INST_ATOMIC_XCHG) { - os_ << "xchg("; - print(b.access); - os_ << ", " << b.valreg << ")"; - return; - } - - if (b.op == AtomicOp::INST_ATOMIC_CMPXCHG) { - os_ << "cmpxchg("; - print(b.access); - os_ << ", r0, " << b.valreg << ")"; - return; - } - print(b.access); os_ << " "; bool showfetch = true; @@ -348,7 +333,7 @@ struct InstructionPrinterVisitor { 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; + case AtomicOp::INST_ATOMIC_CMPXCHG_BASE: os_ << "cx"; showfetch = false; break; } os_ << "= " << b.valreg; diff --git a/src/asm_unmarshal.cpp b/src/asm_unmarshal.cpp index 169b9d680..c2f11f458 100644 --- a/src/asm_unmarshal.cpp +++ b/src/asm_unmarshal.cpp @@ -298,7 +298,6 @@ struct Unmarshaller { auto makeLddw(ebpf_inst inst, int32_t next_imm, const vector& insts, pc_t pc) -> Instruction { if (pc >= insts.size() - 1) throw InvalidInstruction(pc, "incomplete LDDW"); - // TODO(#533): if (inst.src > 1 || inst.dst > R10_STACK_POINTER || inst.offset != 0) throw InvalidInstruction(pc, "LDDW uses reserved fields"); diff --git a/src/assertions.cpp b/src/assertions.cpp index a436bfc0c..2ea2b3e72 100644 --- a/src/assertions.cpp +++ b/src/assertions.cpp @@ -168,6 +168,12 @@ class AssertExtractor { res.emplace_back(TypeConstraint{ins.access.basereg, TypeGroup::shared}); res.emplace_back(ValidAccess{ins.access.basereg, ins.access.offset, Imm{static_cast(ins.access.width)}, false}); + if (ins.op == AtomicOp::INST_ATOMIC_CMPXCHG) { + // The shared memory contents pointed to by ins.access will be compared + // against the value of the ins.valreg register. Since shared memory + // must contain a number, so must ins.valreg. + 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 51558b5b3..a61f0ca66 100644 --- a/src/crab/ebpf_domain.cpp +++ b/src/crab/ebpf_domain.cpp @@ -1182,6 +1182,11 @@ static linear_constraint_t type_is_number(const reg_pack_t& r) { return r.type == T_NUM; } +static linear_constraint_t type_is_shared(const reg_pack_t& r) { + using namespace crab::dsl_syntax; + return r.type == T_SHARED; +} + static linear_constraint_t type_is_number(const Reg& r) { return type_is_number(reg_pack(r)); } static linear_constraint_t type_is_not_stack(const reg_pack_t& r) { @@ -2117,6 +2122,10 @@ void ebpf_domain_t::do_mem_store(const Mem& b, Type val_type, SValue val_svalue, void ebpf_domain_t::operator()(const Atomic& a) { if (m_inv.is_bottom()) return; + if (!m_inv.entail(type_is_shared(reg_pack(a.access.basereg))) || + !m_inv.entail(type_is_number(reg_pack(a.valreg)))) { + return; + } // Fetch the current value into the R11 pseudo-register. Reg r11{R11_ATOMIC_SCRATCH}; @@ -2139,7 +2148,8 @@ void ebpf_domain_t::operator()(const Atomic& a) { 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. + // we just havoc R0. If we did track shared memory values, we'd need more + // complex logic here. Reg r0{R0_RETURN_VALUE}; havoc_register(m_inv, r0); type_inv.havoc_type(m_inv, r0); diff --git a/test-data/atomic.yaml b/test-data/atomic.yaml index 2449ecefd..4d17b2641 100644 --- a/test-data/atomic.yaml +++ b/test-data/atomic.yaml @@ -242,3 +242,50 @@ code: 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 32-bit ADD past end of 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 to non-shared space + +pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2", + "r2.type=stack", "r2.stack_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=stack", "r2.stack_offset=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"] + +messages: + - "0: (r2.type == shared)" +--- +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: (r1.type == number)"