diff --git a/src/crab/ebpf_domain.cpp b/src/crab/ebpf_domain.cpp index d4139b4be..315e91705 100644 --- a/src/crab/ebpf_domain.cpp +++ b/src/crab/ebpf_domain.cpp @@ -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; @@ -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; diff --git a/src/test/test_conformance.cpp b/src/test/test_conformance.cpp index c7a681cfb..079f59984 100644 --- a/src/test/test_conformance.cpp +++ b/src/test/test_conformance.cpp @@ -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") diff --git a/test-data/atomic.yaml b/test-data/atomic.yaml index 3346ac5ab..dca01ad1e 100644 --- a/test-data/atomic.yaml +++ b/test-data/atomic.yaml @@ -219,7 +219,7 @@ 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"] @@ -227,7 +227,8 @@ code: : | 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 @@ -240,7 +241,8 @@ code: : | 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 @@ -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: + : | + 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",