Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add support for MOVSX* instructions #548

Merged
merged 1 commit into from
Dec 24, 2023
Merged

Add support for MOVSX* instructions #548

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 7 additions & 3 deletions src/asm_cfg.cpp
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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