From d2ce6debe8e384da33c69382a3500afb5ef6dc79 Mon Sep 17 00:00:00 2001 From: Dave Thaler Date: Mon, 15 Jan 2024 13:23:44 -0800 Subject: [PATCH] FIx atomics to work on all pointers Signed-off-by: Dave Thaler --- src/assertions.cpp | 2 +- src/crab/ebpf_domain.cpp | 16 +++--- test-data/atomic.yaml | 107 ++++++++++++++++++++++++++++++--------- 3 files changed, 90 insertions(+), 35 deletions(-) diff --git a/src/assertions.cpp b/src/assertions.cpp index 7ca7347c8..80cc29bf9 100644 --- a/src/assertions.cpp +++ b/src/assertions.cpp @@ -165,7 +165,7 @@ class AssertExtractor { 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) { diff --git a/src/crab/ebpf_domain.cpp b/src/crab/ebpf_domain.cpp index 039fe5ad1..d4139b4be 100644 --- a/src/crab/ebpf_domain.cpp +++ b/src/crab/ebpf_domain.cpp @@ -1182,11 +1182,6 @@ 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) { @@ -2122,7 +2117,7 @@ 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))) || + if (!m_inv.entail(type_is_pointer(reg_pack(a.access.basereg))) || !m_inv.entail(type_is_number(reg_pack(a.valreg)))) { return; } @@ -2159,9 +2154,12 @@ void ebpf_domain_t::operator()(const Atomic& a) { (*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. + // 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. + mem.value = r11; + mem.is_load = false; + (*this)(mem); // Clear the R11 pseudo-register. havoc_register(m_inv, r11); diff --git a/test-data/atomic.yaml b/test-data/atomic.yaml index 4d17b2641..3346ac5ab 100644 --- a/test-data/atomic.yaml +++ b/test-data/atomic.yaml @@ -1,7 +1,7 @@ # Copyright (c) Prevail Verifier contributors. # SPDX-License-Identifier: MIT --- -test-case: atomic 32-bit ADD +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"] @@ -13,7 +13,7 @@ code: 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 +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"] @@ -25,7 +25,7 @@ code: 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 +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"] @@ -37,7 +37,7 @@ 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 64-bit ADD and fetch +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"] @@ -49,7 +49,7 @@ 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 AND +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"] @@ -61,7 +61,7 @@ code: 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 +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"] @@ -73,7 +73,7 @@ code: 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 +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"] @@ -85,7 +85,7 @@ 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 64-bit AND and fetch +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"] @@ -97,7 +97,7 @@ 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 OR +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"] @@ -109,7 +109,7 @@ code: 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 +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"] @@ -121,7 +121,7 @@ code: 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 +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"] @@ -133,7 +133,7 @@ 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 64-bit OR and fetch +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"] @@ -145,7 +145,7 @@ 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 XOR +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"] @@ -157,7 +157,7 @@ code: 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 +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"] @@ -169,7 +169,7 @@ code: 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 +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"] @@ -181,7 +181,7 @@ 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 64-bit XOR and fetch +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"] @@ -193,7 +193,7 @@ 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 +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"] @@ -205,7 +205,7 @@ code: 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 +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"] @@ -217,7 +217,7 @@ 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 CMPXCHG +test-case: atomic 32-bit CMPXCHG shared pre: ["r0.type=number", "r0.svalue=2", "r0.uvalue=2", "r1.type=number", "r1.svalue=2", "r1.uvalue=2", @@ -230,7 +230,7 @@ code: 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 64-bit CMPXCHG +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", @@ -243,7 +243,7 @@ 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 +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"] @@ -258,20 +258,77 @@ post: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2", 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 +test-case: atomic 32-bit ADD stack 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"] + "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=4", "r2.svalue=[1, 2147418112]", "r2.uvalue=[1, 2147418112]", "r2.svalue=r2.uvalue"] + "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 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: (r2.type == shared)" + - "0: (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