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.

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

Cleanup, modernize and silence compiler warnings #704

Merged
merged 1 commit into from
Sep 29, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
74 changes: 31 additions & 43 deletions src/asm_marshal.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@

using std::vector;

static uint8_t op(Condition::Op op) {
static uint8_t op(const Condition::Op op) {
using Op = Condition::Op;
switch (op) {
case Op::EQ: return 0x1;
Expand All @@ -30,7 +30,7 @@ static uint8_t op(Condition::Op op) {
return {};
}

static uint8_t op(Bin::Op op) {
static uint8_t op(const Bin::Op op) {
using Op = Bin::Op;
switch (op) {
case Op::ADD: return 0x0;
Expand All @@ -55,19 +55,19 @@ static uint8_t op(Bin::Op op) {
return {};
}

static int16_t offset(Bin::Op op) {
static int16_t offset(const 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;
default: return 0;
elazarg marked this conversation as resolved.
Show resolved Hide resolved
}
return 0;
}

static uint8_t imm_endian(Un::Op op) {
static uint8_t imm_endian(const Un::Op op) {
using Op = Un::Op;
switch (op) {
case Op::NEG: assert(false); return 0;
Expand All @@ -87,7 +87,7 @@ static uint8_t imm_endian(Un::Op op) {

struct MarshalVisitor {
private:
static vector<ebpf_inst> makeLddw(Reg dst, bool isFd, int32_t imm, int32_t next_imm) {
static vector<ebpf_inst> makeLddw(const Reg dst, const bool isFd, const int32_t imm, const int32_t next_imm) {
return {ebpf_inst{.opcode = static_cast<uint8_t>(INST_CLS_LD | width_to_opcode(8)),
.dst = dst.v,
.src = static_cast<uint8_t>(isFd ? 1 : 0),
Expand All @@ -100,14 +100,14 @@ struct MarshalVisitor {
std::function<auto(label_t)->int16_t> label_to_offset16;
std::function<auto(label_t)->int32_t> label_to_offset32;

vector<ebpf_inst> operator()(Undefined const& a) {
vector<ebpf_inst> operator()(Undefined const& a) const {
assert(false);
return {};
}

vector<ebpf_inst> operator()(LoadMapFd const& b) { return makeLddw(b.dst, true, b.mapfd, 0); }
vector<ebpf_inst> operator()(LoadMapFd const& b) const { return makeLddw(b.dst, true, b.mapfd, 0); }

vector<ebpf_inst> operator()(Bin const& b) {
vector<ebpf_inst> operator()(Bin const& b) const {
if (b.lddw) {
const auto pimm = std::get_if<Imm>(&b.v);
assert(pimm != nullptr);
Expand All @@ -120,16 +120,16 @@ struct MarshalVisitor {
.src = 0,
.offset = offset(b.op),
.imm = 0};
std::visit(overloaded{[&](Reg right) {
std::visit(overloaded{[&](const Reg right) {
res.opcode |= INST_SRC_REG;
res.src = right.v;
},
[&](Imm right) { res.imm = static_cast<int32_t>(right.v); }},
[&](const Imm right) { res.imm = static_cast<int32_t>(right.v); }},
b.v);
return {res};
}

vector<ebpf_inst> operator()(Un const& b) {
vector<ebpf_inst> operator()(Un const& b) const {
switch (b.op) {
case Un::Op::NEG:
return {ebpf_inst{
Expand Down Expand Up @@ -174,55 +174,55 @@ struct MarshalVisitor {
return {};
}

vector<ebpf_inst> operator()(Call const& b) {
vector<ebpf_inst> operator()(Call const& b) const {
return {ebpf_inst{.opcode = static_cast<uint8_t>(INST_OP_CALL),
.dst = 0,
.src = INST_CALL_STATIC_HELPER,
.offset = 0,
.imm = b.func}};
}

vector<ebpf_inst> operator()(CallLocal const& b) {
vector<ebpf_inst> operator()(CallLocal const& b) const {
return {ebpf_inst{.opcode = static_cast<uint8_t>(INST_OP_CALL),
.dst = 0,
.src = INST_CALL_LOCAL,
.offset = 0,
.imm = label_to_offset32(b.target)}};
}

vector<ebpf_inst> operator()(Callx const& b) {
vector<ebpf_inst> operator()(Callx const& b) const {
// callx is defined to have the register in 'dst' not in 'src'.
return {ebpf_inst{.opcode = static_cast<uint8_t>(INST_OP_CALLX),
.dst = b.func.v,
.src = INST_CALL_STATIC_HELPER,
.offset = 0}};
}

vector<ebpf_inst> operator()(Exit const& b) {
vector<ebpf_inst> operator()(Exit const& b) const {
return {ebpf_inst{.opcode = INST_OP_EXIT, .dst = 0, .src = 0, .offset = 0, .imm = 0}};
}

vector<ebpf_inst> operator()(Assume const& b) { throw std::invalid_argument("Cannot marshal assumptions"); }
vector<ebpf_inst> operator()(Assume const&) const { throw std::invalid_argument("Cannot marshal assumptions"); }

vector<ebpf_inst> operator()(Assert const& b) { throw std::invalid_argument("Cannot marshal assertions"); }
vector<ebpf_inst> operator()(Assert const&) const { throw std::invalid_argument("Cannot marshal assertions"); }

vector<ebpf_inst> operator()(Jmp const& b) {
vector<ebpf_inst> operator()(Jmp const& b) const {
if (b.cond) {
ebpf_inst res{
.opcode = static_cast<uint8_t>(INST_CLS_JMP | (op(b.cond->op) << 4)),
.dst = b.cond->left.v,
.src = 0,
.offset = label_to_offset16(b.target),
};
visit(overloaded{[&](Reg right) {
visit(overloaded{[&](const Reg right) {
res.opcode |= INST_SRC_REG;
res.src = right.v;
},
[&](Imm right) { res.imm = static_cast<int32_t>(right.v); }},
[&](const Imm right) { res.imm = static_cast<int32_t>(right.v); }},
b.cond->right);
return {res};
} else {
int32_t imm = label_to_offset32(b.target);
const int32_t imm = label_to_offset32(b.target);
if (imm != 0) {
return {ebpf_inst{.opcode = INST_OP_JA32, .imm = imm}};
} else {
Expand All @@ -231,8 +231,8 @@ struct MarshalVisitor {
}
}

vector<ebpf_inst> operator()(Mem const& b) {
Deref access = b.access;
vector<ebpf_inst> operator()(Mem const& b) const {
const Deref access = b.access;
ebpf_inst res{
.opcode = static_cast<uint8_t>(INST_MODE_MEM | width_to_opcode(access.width)),
.dst = 0,
Expand All @@ -245,7 +245,7 @@ struct MarshalVisitor {
}
res.opcode |= INST_CLS_LD | 0x1;
res.dst = static_cast<uint8_t>(std::get<Reg>(b.value).v);
res.src = static_cast<uint8_t>(access.basereg.v);
res.src = access.basereg.v;
} else {
res.opcode |= INST_CLS_ST;
res.dst = access.basereg.v;
Expand All @@ -260,7 +260,7 @@ struct MarshalVisitor {
return {res};
}

vector<ebpf_inst> operator()(Packet const& b) {
vector<ebpf_inst> operator()(Packet const& b) const {
ebpf_inst res{
.opcode = static_cast<uint8_t>(INST_CLS_LD | width_to_opcode(b.width)),
.dst = 0,
Expand All @@ -277,8 +277,8 @@ struct MarshalVisitor {
return {res};
}

vector<ebpf_inst> operator()(Atomic const& b) {
int32_t imm = (int32_t)b.op;
vector<ebpf_inst> operator()(Atomic const& b) const {
int32_t imm = static_cast<int32_t>(b.op);
if (b.fetch) {
imm |= INST_FETCH;
}
Expand All @@ -290,25 +290,13 @@ struct MarshalVisitor {
.imm = imm}};
}

vector<ebpf_inst> operator()(IncrementLoopCounter const& ins) { return {}; }
vector<ebpf_inst> operator()(IncrementLoopCounter const&) const { return {}; }
};

vector<ebpf_inst> marshal(const Instruction& ins, pc_t pc) {
vector<ebpf_inst> marshal(const Instruction& ins, const pc_t pc) {
return std::visit(MarshalVisitor{label_to_offset16(pc), label_to_offset32(pc)}, ins);
}

vector<ebpf_inst> marshal(const vector<Instruction>& insts) {
vector<ebpf_inst> res;
pc_t pc = 0;
for (const auto& ins : insts) {
for (auto e : marshal(ins, pc)) {
pc++;
res.push_back(e);
}
}
return res;
}

static int size(const Instruction& inst) {
if (const auto pins = std::get_if<Bin>(&inst)) {
if (pins->lddw) {
Expand All @@ -333,7 +321,7 @@ static auto get_labels(const InstructionSeq& insts) {

vector<ebpf_inst> marshal(const InstructionSeq& insts) {
vector<ebpf_inst> res;
auto pc_of_label = get_labels(insts);
const auto pc_of_label = get_labels(insts);
pc_t pc = 0;
for (auto [label, ins, _] : insts) {
(void)label; // unused
Expand Down
33 changes: 16 additions & 17 deletions src/crab/array_domain.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,8 @@

namespace crab::domains {

using index_t = uint64_t;

static bool maybe_between(const NumAbsDomain& dom, const extended_number& x, const linear_expression_t& symb_lb,
const linear_expression_t& symb_ub) {
using namespace dsl_syntax;
Expand Down Expand Up @@ -60,7 +62,7 @@ int radix_length(const offset_t& offset) {
// Get a range of bits out of the middle of a key, starting at [begin] for a given length.
[[maybe_unused]]
offset_t radix_substr(const offset_t& key, const int begin, const int length) {
uint64_t mask;
index_t mask;

if (length == offset_t::bitsize) {
mask = 0;
Expand All @@ -79,11 +81,8 @@ offset_t radix_substr(const offset_t& key, const int begin, const int length) {
// Concatenate two bit patterns.
[[maybe_unused]]
offset_t radix_join(const offset_t& entry1, const offset_t& entry2) {
const index_t value1 = (index_t)entry1;
const index_t value2 = (index_t)entry2;
const index_t value = value1 | (value2 >> entry1.prefix_length());
const index_t value = entry1 | (entry2 >> entry1.prefix_length());
const int prefix_length = entry1.prefix_length() + entry2.prefix_length();

return offset_t{value, prefix_length};
}

Expand Down Expand Up @@ -491,7 +490,7 @@ void array_domain_t::split_number_var(NumAbsDomain& inv, data_kind_t kind, const
return;
}
auto size = static_cast<unsigned int>(*n_bytes);
offset_t o(static_cast<uint64_t>(*n));
offset_t o(static_cast<index_t>(*n));

std::vector<cell_t> cells = offset_map.get_overlap_cells(o, size);
for (cell_t const& c : cells) {
Expand All @@ -500,7 +499,7 @@ void array_domain_t::split_number_var(NumAbsDomain& inv, data_kind_t kind, const
int cell_end_index = static_cast<int>(*intv.ub().number());

if (!this->num_bytes.all_num(cell_start_index, cell_end_index + 1) ||
cell_end_index + 1 < cell_start_index + sizeof(int64_t)) {
cell_end_index + 1UL < cell_start_index + sizeof(int64_t)) {
// We can only split numeric cells of size 8 or less.
continue;
}
Expand All @@ -509,11 +508,11 @@ void array_domain_t::split_number_var(NumAbsDomain& inv, data_kind_t kind, const
// We can only split cells with a singleton value.
continue;
}
if (cell_start_index < o) {
if (static_cast<index_t>(cell_start_index) < o) {
// Use the bytes to the left of the specified range.
split_cell(inv, kind, cell_start_index, static_cast<unsigned int>(o - cell_start_index));
}
if (o + size - 1 < cell_end_index) {
if (o + size < cell_end_index + 1UL) {
// Use the bytes to the right of the specified range.
split_cell(inv, kind, static_cast<int>(o + size),
static_cast<unsigned int>(cell_end_index - (o + size - 1)));
Expand All @@ -535,7 +534,7 @@ static std::optional<std::pair<offset_t, unsigned>> kill_and_find_var(NumAbsDoma
if (auto n_bytes = i_elem_size.singleton()) {
auto size = static_cast<unsigned int>(*n_bytes);
// -- Constant index: kill overlapping cells
offset_t o(static_cast<uint64_t>(*n));
offset_t o(static_cast<index_t>(*n));
cells = offset_map.get_overlap_cells(o, size);
res = std::make_pair(o, size);
}
Expand Down Expand Up @@ -599,7 +598,7 @@ std::optional<uint8_t> get_value_byte(const NumAbsDomain& inv, const offset_t o,
if (!t) {
return {};
}
uint64_t n = t->cast_to<uint64_t>();
index_t n = t->cast_to<index_t>();

// Convert value to bytes of the appropriate endian-ness.
switch (width) {
Expand All @@ -618,11 +617,11 @@ std::optional<uint8_t> get_value_byte(const NumAbsDomain& inv, const offset_t o,
n = boost::endian::native_to_little<uint32_t>(n);
}
break;
case sizeof(uint64_t):
case sizeof(index_t):
if (thread_local_options.big_endian) {
n = boost::endian::native_to_big<uint64_t>(n);
n = boost::endian::native_to_big<index_t>(n);
} else {
n = boost::endian::native_to_little<uint64_t>(n);
n = boost::endian::native_to_little<index_t>(n);
}
break;
default: CRAB_ERROR("Unexpected width ", width);
Expand Down Expand Up @@ -700,11 +699,11 @@ std::optional<linear_expression_t> array_domain_t::load(const NumAbsDomain& inv,
return b;
}
if (size == 8) {
uint64_t b = *reinterpret_cast<uint64_t*>(result_buffer);
index_t b = *reinterpret_cast<index_t*>(result_buffer);
if (thread_local_options.big_endian) {
b = boost::endian::native_to_big<uint64_t>(b);
b = boost::endian::native_to_big<index_t>(b);
} else {
b = boost::endian::native_to_little<uint64_t>(b);
b = boost::endian::native_to_little<index_t>(b);
}
return kind == data_kind_t::uvalues ? number_t(b) : number_t(static_cast<int64_t>(b));
}
Expand Down
3 changes: 3 additions & 0 deletions src/crab/ebpf_domain.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -2510,6 +2510,9 @@ 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: CRAB_ERROR("Unsupported operation");
elazarg marked this conversation as resolved.
Show resolved Hide resolved
case Bin::Op::ADD:
if (imm == 0) {
return;
Expand Down
2 changes: 1 addition & 1 deletion src/crab/split_dbm.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1168,7 +1168,7 @@ string_invariant SplitDBM::to_set() const {
std::ostream& operator<<(std::ostream& o, const SplitDBM& dom) { return o << dom.to_set(); }

bool SplitDBM::eval_expression_overflow(const linear_expression_t& e, Weight& out) const {
bool overflow = convert_NtoW_overflow(e.constant_term(), out);
[[maybe_unused]] bool overflow = convert_NtoW_overflow(e.constant_term(), out);
assert(!overflow);
for (const auto& [variable, coefficient] : e.variable_terms()) {
Weight coef;
Expand Down
Loading
Loading