Skip to content

Commit

Permalink
Add support for MOVSX* instructions
Browse files Browse the repository at this point in the history 
Per https://www.ietf.org/archive/id/draft-ietf-bpf-isa-00.html#section-3.1

Signed-off-by: Dave Thaler <[email protected]>
  • Loading branch information
@dthaler
dthaler committed Dec 22, 2023
1 parent 86e82a7 commit ef3b6bc
Show file tree
Hide file tree
Showing 11 changed files with 438 additions and 7 deletions.
10 changes: 7 additions & 3 deletions src/asm_cfg.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -181,9 +181,13 @@ static std::string instype(Instruction ins) {
} else if (std::holds_alternative<Packet>(ins)) {
return "packet_access";
} else if (std::holds_alternative<Bin>(ins)) {
if (std::get<Bin>(ins).op == Bin::Op::MOV)
return "assign";
return "arith";
switch (std::get<Bin>(ins).op) {
case Bin::Op::MOV:
case Bin::Op::MOVSX8:
case Bin::Op::MOVSX16:
case Bin::Op::MOVSX32: return "assign";
default: return "arith";
}
} else if (std::holds_alternative<Un>(ins)) {
return "arith";
} else if (std::holds_alternative<LoadMapFd>(ins)) {
Expand Down
21 changes: 19 additions & 2 deletions src/asm_marshal.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,20 +36,37 @@ static uint8_t op(Bin::Op op) {
case Op::ADD: return 0x0;
case Op::SUB: return 0x1;
case Op::MUL: return 0x2;
case Op::SDIV:
case Op::UDIV: return 0x3;
case Op::OR: return 0x4;
case Op::AND: return 0x5;
case Op::LSH: return 0x6;
case Op::RSH: return 0x7;
case Op::SMOD:
case Op::UMOD: return 0x9;
case Op::XOR: return 0xa;
case Op::MOV: return 0xb;
case Op::MOV:
case Op::MOVSX8:
case Op::MOVSX16:
case Op::MOVSX32: return 0xb;
case Op::ARSH: return 0xc;
}
assert(false);
return {};
}

static int16_t offset(Bin::Op op) {
using Op = Bin::Op;
switch (op) {
case Op::SDIV:
case Op::SMOD: return 1;
case Op::MOVSX8: return 8;
case Op::MOVSX16: return 16;
case Op::MOVSX32: return 32;
}
return 0;
}

static uint8_t imm(Un::Op op) {
using Op = Un::Op;
switch (op) {
Expand Down Expand Up @@ -96,7 +113,7 @@ struct MarshalVisitor {
ebpf_inst res{.opcode = static_cast<uint8_t>((b.is64 ? INST_CLS_ALU64 : INST_CLS_ALU) | (op(b.op) << 4)),
.dst = b.dst.v,
.src = 0,
.offset = 0,
.offset = offset(b.op),
.imm = 0};
std::visit(overloaded{[&](Reg right) {
res.opcode |= INST_SRC_REG;
Expand Down
3 changes: 3 additions & 0 deletions src/asm_ostream.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -56,6 +56,9 @@ std::ostream& operator<<(std::ostream& os, Bin::Op op) {
using Op = Bin::Op;
switch (op) {
case Op::MOV: return os;
case Op::MOVSX8: return os << "s8";
case Op::MOVSX16: return os << "s16";
case Op::MOVSX32: return os << "s32";
case Op::ADD: return os << "+";
case Op::SUB: return os << "-";
case Op::MUL: return os << "*";
Expand Down
3 changes: 2 additions & 1 deletion src/asm_parse.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,8 @@ static const std::map<std::string, Bin::Op> str_to_binop = {
{"", Bin::Op::MOV}, {"+", Bin::Op::ADD}, {"-", Bin::Op::SUB}, {"*", Bin::Op::MUL},
{"/", Bin::Op::UDIV}, {"%", Bin::Op::UMOD}, {"|", Bin::Op::OR}, {"&", Bin::Op::AND},
{"<<", Bin::Op::LSH}, {">>", Bin::Op::RSH}, {"s>>", Bin::Op::ARSH}, {"^", Bin::Op::XOR},
{"s/", Bin::Op::SDIV}, {"s%", Bin::Op::SMOD},
{"s/", Bin::Op::SDIV}, {"s%", Bin::Op::SMOD}, {"s8", Bin::Op::MOVSX8}, {"s16", Bin::Op::MOVSX16},
{"s32", Bin::Op::MOVSX32},
};

static const std::map<std::string, Un::Op> str_to_unop = {
Expand Down
3 changes: 3 additions & 0 deletions src/asm_syntax.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -87,6 +87,9 @@ struct Bin {
XOR,
SDIV,
SMOD,
MOVSX8,
MOVSX16,
MOVSX32,
};

Op op;
Expand Down
9 changes: 8 additions & 1 deletion src/asm_unmarshal.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -109,7 +109,14 @@ struct Unmarshaller {
default: throw InvalidInstruction{pc, "invalid ALU op 0x90"};
}
case INST_ALU_OP_XOR: return Bin::Op::XOR;
case INST_ALU_OP_MOV: return Bin::Op::MOV;
case INST_ALU_OP_MOV:
switch (inst.offset) {
case 0: return Bin::Op::MOV;
case 8: return Bin::Op::MOVSX8;
case 16: return Bin::Op::MOVSX16;
case 32: return Bin::Op::MOVSX32;
default: throw InvalidInstruction{pc, "invalid ALU op 0xb0"};
}
case INST_ALU_OP_ARSH:
if ((inst.opcode & INST_CLS_MASK) == INST_CLS_ALU)
note("arsh32 is not allowed");
Expand Down
8 changes: 8 additions & 0 deletions src/assertions.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -180,6 +180,14 @@ class AssertExtractor {
vector<Assert> operator()(Bin ins) const {
switch (ins.op) {
case Bin::Op::MOV: return {};
case Bin::Op::MOVSX8:
case Bin::Op::MOVSX16:
case Bin::Op::MOVSX32:
if (std::holds_alternative<Reg>(ins.v)) {
auto src = reg(ins.v);
return {Assert{TypeConstraint{src, TypeGroup::number}}};
}
return {};
case Bin::Op::ADD:
if (std::holds_alternative<Reg>(ins.v)) {
auto src = reg(ins.v);
Expand Down
56 changes: 56 additions & 0 deletions src/crab/ebpf_domain.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2342,6 +2342,46 @@ void ebpf_domain_t::lshr(const Reg& dst_reg, int imm, int finite_width) {
havoc_offsets(dst_reg);
}

void ebpf_domain_t::sign_extend(const Reg& dst_reg, const linear_expression_t& right_svalue, int finite_width,
Bin::Op op) {
using namespace crab;

int bits;
switch (op) {
case Bin::Op::MOVSX8: bits = 8; break;
case Bin::Op::MOVSX16: bits = 16; break;
case Bin::Op::MOVSX32: bits = 32; break;
default: throw std::exception();
}

reg_pack_t dst = reg_pack(dst_reg);
interval_t right_interval = m_inv.eval_interval(right_svalue);
type_inv.assign_type(m_inv, dst_reg, T_NUM);
havoc_offsets(dst_reg);
int64_t span = 1ULL << bits;
if (right_interval.ub() - right_interval.lb() >= number_t{span}) {
// Interval covers the full space.
havoc(dst.svalue);
return;
}
int64_t mask = 1ULL << (bits - 1);

// Sign extend each bound.
int64_t lb = right_interval.lb().number().value().cast_to_sint64();
lb &= (span - 1);
lb = (lb ^ mask) - mask;
int64_t ub = right_interval.ub().number().value().cast_to_sint64();
ub &= (span - 1);
ub = (ub ^ mask) - mask;
m_inv.set(dst.svalue, crab::interval_t{number_t{lb}, number_t{ub}});

if (finite_width) {
m_inv.assign(dst.uvalue, dst.svalue);
overflow_signed(m_inv, dst.svalue, finite_width);
overflow_unsigned(m_inv, dst.uvalue, finite_width);
}
}

void ebpf_domain_t::ashr(const Reg& dst_reg, const linear_expression_t& right_svalue, int finite_width) {
using namespace crab;

Expand Down Expand Up @@ -2413,6 +2453,11 @@ void ebpf_domain_t::operator()(const Bin& bin) {
type_inv.assign_type(m_inv, bin.dst, T_NUM);
havoc_offsets(bin.dst);
break;
case Bin::Op::MOVSX8:
case Bin::Op::MOVSX16:
case Bin::Op::MOVSX32:
sign_extend(bin.dst, number_t{(int32_t)imm}, finite_width, bin.op);
break;
case Bin::Op::ADD:
if (imm == 0)
return;
Expand Down Expand Up @@ -2655,6 +2700,17 @@ void ebpf_domain_t::operator()(const Bin& bin) {
bitwise_xor(dst.svalue, dst.uvalue, src.uvalue, finite_width);
havoc_offsets(bin.dst);
break;
case Bin::Op::MOVSX8:
case Bin::Op::MOVSX16:
case Bin::Op::MOVSX32:
if (m_inv.entail(type_is_number(src_reg))) {
sign_extend(bin.dst, src.svalue, finite_width, bin.op);
break;
}
havoc(dst.svalue);
havoc(dst.uvalue);
havoc_offsets(bin.dst);
break;
case Bin::Op::MOV:
assign(dst.svalue, src.svalue);
assign(dst.uvalue, src.uvalue);
Expand Down
1 change: 1 addition & 0 deletions src/crab/ebpf_domain.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -139,6 +139,7 @@ class ebpf_domain_t final {
void shl_overflow(variable_t lhss, variable_t lhsu, const number_t& op2);
void lshr(const Reg& reg, int imm, int finite_width);
void ashr(const Reg& reg, const linear_expression_t& right_svalue, int finite_width);
void sign_extend(const Reg& dst_reg, const linear_expression_t& right_svalue, int finite_width, Bin::Op op);

void assume(const linear_constraint_t& cst);

Expand Down
1 change: 1 addition & 0 deletions src/test/test_yaml.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,7 @@ YAML_CASE("test-data/sdivmod.yaml")
YAML_CASE("test-data/full64.yaml")
YAML_CASE("test-data/jump.yaml")
YAML_CASE("test-data/loop.yaml")
YAML_CASE("test-data/movsx.yaml")
YAML_CASE("test-data/packet.yaml")
YAML_CASE("test-data/parse.yaml")
YAML_CASE("test-data/shift.yaml")
Expand Down
Loading

0 comments on commit ef3b6bc

Please sign in to comment.