Skip to content

Commit

Permalink
Add FETCH support
Browse files Browse the repository at this point in the history 
Fixes #483

Signed-off-by: Dave Thaler <[email protected]>
  • Loading branch information
@dthaler
dthaler committed Jan 3, 2024
1 parent 88802ae commit cef7a13
Show file tree
Hide file tree
Showing 4 changed files with 247 additions and 29 deletions.
18 changes: 16 additions & 2 deletions src/asm_parse.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ using crab::linear_expression_t;
#define ASSIGN R"_(\s*=\s*)_"
#define LONGLONG R"_(\s*(ll|)\s*)_"
#define UNOP R"_((-|be16|be32|be64|le16|le32|le64|swap16|swap32|swap64))_"
#define ATOMICOP R"_((\+|\||&\^)=)_"
#define ATOMICOP R"_((\+|\||&|\^)=)_"

#define PLUSMINUS R"_((\s*[+-])\s*)_"
#define LPAREN R"_(\s*\(\s*)_"
Expand Down Expand Up @@ -87,6 +87,11 @@ static const std::map<std::string, AtomicOp> str_to_atomicop = {{"+", AtomicOp::
{"&", AtomicOp::INST_ATOMIC_AND},
{"^", AtomicOp::INST_ATOMIC_XOR}};

static const std::map<std::string, AtomicOp> str_to_atomicfetchop = {{"+", AtomicOp::INST_ATOMIC_ADD_FETCH},
{"|", AtomicOp::INST_ATOMIC_OR_FETCH},
{"&", AtomicOp::INST_ATOMIC_AND_FETCH},
{"^", AtomicOp::INST_ATOMIC_XOR_FETCH}};

static const std::map<std::string, int> str_to_width = {
{"8", 1},
{"16", 2},
Expand Down Expand Up @@ -186,7 +191,16 @@ Instruction parse_instruction(const std::string& line, const std::map<std::strin
};
}
if (regex_match(text, m, regex("lock " DEREF PAREN(REG PLUSMINUS IMM) " " ATOMICOP " " REG))) {
return Atomic{.op = str_to_atomicop.at(m[5]), .access = deref(m[1], m[2], m[3], m[4]), .valreg = reg(m[6])};
return Atomic{
.op = str_to_atomicop.at(m[5]),
.access = deref(m[1], m[2], m[3], m[4]),
.valreg = reg(m[6])};
}
if (regex_match(text, m, regex("lock " DEREF PAREN(REG PLUSMINUS IMM) " " ATOMICOP " " REG " fetch"))) {
return Atomic{
.op = str_to_atomicfetchop.at(m[5]),
.access = deref(m[1], m[2], m[3], m[4]),
.valreg = reg(m[6])};
}
if (regex_match(text, m, regex("r0 = " DEREF "skb\\[(.*)\\]"))) {
auto width = str_to_width.at(m[1]);
Expand Down
39 changes: 38 additions & 1 deletion src/crab/ebpf_domain.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2115,7 +2115,44 @@ void ebpf_domain_t::do_mem_store(const Mem& b, Type val_type, SValue val_svalue,
}

void ebpf_domain_t::operator()(const Atomic& a) {
// nothing to do here
if (m_inv.is_bottom())
return;

// Fetch the current value into the R11 pseudo-register.
Reg r11{R11_ATOMIC_SCRATCH};
Mem mem = {.access = a.access, .value = r11, .is_load = true};
(*this)(mem);

// Compute the new value in R11.
Bin bin {.dst = r11, .v = a.valreg, .is64 = (a.access.width == 64), .lddw = false};
switch ((AtomicOp)((uint32_t)a.op & (uint32_t)AtomicOp::INST_ATOMIC_BASE_MASK)) {
case AtomicOp::INST_ATOMIC_ADD: bin.op = Bin::Op::ADD; break;
case AtomicOp::INST_ATOMIC_OR: bin.op = Bin::Op::OR; break;
case AtomicOp::INST_ATOMIC_AND: bin.op = Bin::Op::AND; break;
case AtomicOp::INST_ATOMIC_XOR: bin.op = Bin::Op::XOR; break;
default:
// TODO: handle other instructions.
m_inv.set_to_bottom(); return;
}
(*this)(bin);

// If FETCH is set, store the original value in the src register.
if ((uint32_t)a.op & (uint32_t)AtomicOp::INST_ATOMIC_FETCH) {
mem.value = a.valreg;
mem.is_load = true;
(*this)(mem);
}

// Store the new value back in the original shared memory location.
// Note that do_mem_store() currently doesn't track shared memory values,
// but it might in the future so we include code here as if it did.
mem.value = r11;
mem.is_load = false;
(*this)(mem);

// Clear the R11 pseudo-register.
havoc_register(m_inv, r11);
type_inv.havoc_type(m_inv, r11);
}

void ebpf_domain_t::operator()(const Call& call) {
Expand Down
3 changes: 2 additions & 1 deletion src/ebpf_vm_isa.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -86,7 +86,8 @@ enum {
R7 = 7,
R8 = 8,
R9 = 9,
R10_STACK_POINTER = 10
R10_STACK_POINTER = 10,
R11_ATOMIC_SCRATCH = 11, // Pseudo-register used internally for atomic instructions.
};

enum class AtomicOp {
Expand Down
216 changes: 191 additions & 25 deletions test-data/atomic.yaml
View file
Original file line number Diff line number Diff line change
@@ -1,28 +1,194 @@
# Copyright (c) Prevail Verifier contributors.
# SPDX-License-Identifier: MIT
---
test-case: atomic add number register

pre:
- r10.type=stack
- r10.stack_offset=512
- s[504...511].type=number
- s[504...511].svalue=1
- s[504...511].uvalue=1
- r1.type=number
- r1.svalue=2
- r1.uvalue=2

code:
<start>: |
lock *(u64 *)(r10 - 8) += r1
post:
- r1.type=number
- r1.svalue=2
- r1.uvalue=2
- r10.type=stack
- r10.stack_offset=512
- s[504...511].type=number
- s[504...511].svalue=3
- s[504...511].uvalue=3
test-case: atomic 32-bit ADD

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"]

code:
<start>: |
lock *(u32 *)(r2 + 4) += r1
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

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"]

code:
<start>: |
lock *(u32 *)(r2 + 4) += r1 fetch
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

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"]

code:
<start>: |
lock *(u64 *)(r2 + 4) += r1
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

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"]

code:
<start>: |
lock *(u64 *)(r2 + 4) += r1 fetch
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

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"]

code:
<start>: |
lock *(u32 *)(r2 + 4) &= r1
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

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"]

code:
<start>: |
lock *(u32 *)(r2 + 4) &= r1 fetch
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

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"]

code:
<start>: |
lock *(u64 *)(r2 + 4) &= r1
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

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"]

code:
<start>: |
lock *(u64 *)(r2 + 4) &= r1 fetch
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

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"]

code:
<start>: |
lock *(u32 *)(r2 + 4) |= r1
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

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"]

code:
<start>: |
lock *(u32 *)(r2 + 4) |= r1 fetch
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

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"]

code:
<start>: |
lock *(u64 *)(r2 + 4) |= r1
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

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"]

code:
<start>: |
lock *(u64 *)(r2 + 4) |= r1 fetch
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

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"]

code:
<start>: |
lock *(u32 *)(r2 + 4) ^= r1
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

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"]

code:
<start>: |
lock *(u32 *)(r2 + 4) ^= r1 fetch
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

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"]

code:
<start>: |
lock *(u64 *)(r2 + 4) ^= r1
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

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"]

code:
<start>: |
lock *(u64 *)(r2 + 4) ^= r1 fetch
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"]

0 comments on commit cef7a13

Please sign in to comment.