Skip to content

Commit

Permalink
FIx atomics to work on all pointers
Browse files Browse the repository at this point in the history
Signed-off-by: Dave Thaler <[email protected]>
  • Loading branch information
dthaler committed Jan 15, 2024
1 parent f6b21c8 commit 16d521a
Show file tree
Hide file tree
Showing 3 changed files with 90 additions and 35 deletions.
2 changes: 1 addition & 1 deletion src/assertions.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -165,7 +165,7 @@ class AssertExtractor {

vector<Assert> operator()(Atomic ins) const {
vector<Assert> 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<uint32_t>(ins.access.width)}, false});
if (ins.op == Atomic::Op::CMPXCHG) {
Expand Down
16 changes: 7 additions & 9 deletions src/crab/ebpf_domain.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Expand Down Expand Up @@ -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;
}
Expand Down Expand Up @@ -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);
Expand Down
107 changes: 82 additions & 25 deletions test-data/atomic.yaml
Original file line number Diff line number Diff line change
@@ -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"]
Expand All @@ -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"]
Expand All @@ -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"]
Expand All @@ -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"]
Expand All @@ -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"]
Expand All @@ -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"]
Expand All @@ -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"]
Expand All @@ -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"]
Expand All @@ -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"]
Expand All @@ -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"]
Expand All @@ -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"]
Expand All @@ -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"]
Expand All @@ -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"]
Expand All @@ -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"]
Expand All @@ -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"]
Expand All @@ -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"]
Expand All @@ -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"]
Expand All @@ -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"]
Expand All @@ -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",
Expand All @@ -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",
Expand All @@ -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"]
Expand All @@ -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:
<start>: |
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:
<start>: |
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:
<start>: |
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:
<start>: |
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:
<start>: |
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

Expand Down

0 comments on commit 16d521a

Please sign in to comment.