Skip to content

Commit

Permalink
Update to pass atomic conformance tests
Browse files Browse the repository at this point in the history 
Signed-off-by: Dave Thaler <[email protected]>
  • Loading branch information
@dthaler
dthaler committed Jan 15, 2024
1 parent 16d521a commit 86c3148
Show file tree
Hide file tree
Showing 3 changed files with 264 additions and 29 deletions.
17 changes: 11 additions & 6 deletions src/crab/ebpf_domain.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2128,7 +2128,7 @@ void ebpf_domain_t::operator()(const Atomic& a) {
(*this)(mem);

// Compute the new value in R11.
Bin bin {.dst = r11, .v = a.valreg, .is64 = (a.access.width == 64), .lddw = false};
Bin bin {.dst = r11, .v = a.valreg, .is64 = (a.access.width == sizeof(uint64_t)), .lddw = false};
switch ((Atomic::Op)((uint32_t)a.op & (uint32_t)Atomic::Op::BASE_MASK)) {
case Atomic::Op::ADD: bin.op = Bin::Op::ADD; break;
case Atomic::Op::OR: bin.op = Bin::Op::OR; break;
Expand All @@ -2141,12 +2141,17 @@ void ebpf_domain_t::operator()(const Atomic& a) {
(*this)(bin);

if (a.op == Atomic::Op::CMPXCHG) {
// For CMPXCHG, store the original value in r0 if and only if the value matches
// what is in the src register. We cannot reliably track shared memory values,
// since they may be modified from another thread, so we just havoc R0.
// For CMPXCHG, store the original value in r0.
Reg r0{R0_RETURN_VALUE};
havoc_register(m_inv, r0);
type_inv.havoc_type(m_inv, r0);
Mem mem = {.access = a.access, .value = r0, .is_load = true};
(*this)(mem);

// 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 ((uint32_t)a.op & (uint32_t)Atomic::Op::FETCH) {
// For other FETCH operations, store the original value in the src register.
mem.value = a.valreg;
Expand Down
40 changes: 20 additions & 20 deletions src/test/test_conformance.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -144,26 +144,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")
Expand Down
236 changes: 233 additions & 3 deletions test-data/atomic.yaml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -219,15 +219,16 @@ post: ["r1.type=number",
---
test-case: atomic 32-bit CMPXCHG shared

pre: ["r0.type=number", "r0.svalue=2", "r0.uvalue=2",
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:
<start>: |
lock *(u32 *)(r2 + 4) cx= r1
post: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
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
Expand All @@ -240,7 +241,8 @@ code:
<start>: |
lock *(u64 *)(r2 + 4) cx= r1
post: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2",
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
Expand Down Expand Up @@ -314,6 +316,234 @@ 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:
<start>: |
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:
<start>: |
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:
<start>: |
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:
<start>: |
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:
<start>: |
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:
<start>: |
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:
<start>: |
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:
<start>: |
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:
<start>: |
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:
<start>: |
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:
<start>: |
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:
<start>: |
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:
<start>: |
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:
<start>: |
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:
<start>: |
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:
<start>: |
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",
Expand Down

0 comments on commit 86c3148

Please sign in to comment.