Skip to content

Commit

Permalink
Const all the things (#778)
Browse files Browse the repository at this point in the history
also some modernization

Signed-off-by: Elazar Gershuni <[email protected]>
  • Loading branch information
elazarg authored Nov 7, 2024
1 parent 0669c85 commit 1e5de90
Show file tree
Hide file tree
Showing 31 changed files with 213 additions and 217 deletions.
16 changes: 8 additions & 8 deletions src/asm_cfg.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,7 @@ static void add_cfg_nodes(cfg_t& cfg, const label_t& caller_label, const label_t
// and store a copy in the CallLocal instruction since the instruction-specific
// labels may only exist until the CFG is simplified.
basic_block_t& caller_node = cfg.get_node(caller_label);
std::string stack_frame_prefix = to_string(caller_label);
const std::string stack_frame_prefix = to_string(caller_label);
for (auto& inst : caller_node) {
if (const auto pcall = std::get_if<CallLocal>(&inst)) {
pcall->stack_frame_prefix = stack_frame_prefix;
Expand All @@ -70,7 +70,7 @@ static void add_cfg_nodes(cfg_t& cfg, const label_t& caller_label, const label_t
}

// Clone the macro block into a new block with the new stack frame prefix.
const label_t label(macro_label.from, macro_label.to, stack_frame_prefix);
const label_t label{macro_label.from, macro_label.to, stack_frame_prefix};
auto& bb = cfg.insert(label);
for (auto inst : cfg.get_node(macro_label)) {
if (const auto pexit = std::get_if<Exit>(&inst)) {
Expand Down Expand Up @@ -119,8 +119,8 @@ static void add_cfg_nodes(cfg_t& cfg, const label_t& caller_label, const label_t

// Finally, recurse to replace any nested function macros.
string caller_label_str = to_string(caller_label);
long stack_frame_depth = std::ranges::count(caller_label_str, STACK_FRAME_DELIMITER) + 2;
for (auto& macro_label : seen_labels) {
const long stack_frame_depth = std::ranges::count(caller_label_str, STACK_FRAME_DELIMITER) + 2;
for (const auto& macro_label : seen_labels) {
for (const label_t label(macro_label.from, macro_label.to, caller_label_str);
const auto& inst : cfg.get_node(label)) {
if (const auto pins = std::get_if<CallLocal>(&inst)) {
Expand Down Expand Up @@ -180,7 +180,7 @@ static cfg_t instruction_seq_to_cfg(const InstructionSeq& insts, const bool must
// Now replace macros. We have to do this as a second pass so that
// we only add new nodes that are actually reachable, based on the
// results of the first pass.
for (auto& [label, inst, _] : insts) {
for (const auto& [label, inst, _] : insts) {
if (const auto pins = std::get_if<CallLocal>(&inst)) {
add_cfg_nodes(cfg, label, pins->target);
}
Expand Down Expand Up @@ -232,7 +232,7 @@ static vector<label_t> unique(const std::pair<T, T>& be) {
/// immediately after the branch.
static cfg_t to_nondet(const cfg_t& cfg) {
cfg_t res;
for (auto const& [this_label, bb] : cfg) {
for (const auto& [this_label, bb] : cfg) {
basic_block_t& newbb = res.insert(this_label);

for (const auto& ins : bb) {
Expand All @@ -259,7 +259,7 @@ static cfg_t to_nondet(const cfg_t& cfg) {
{jmp.target, *jmp.cond},
{fallthrough, reverse(*jmp.cond)},
};
for (auto const& [next_label, cond1] : jumps) {
for (const auto& [next_label, cond1] : jumps) {
label_t jump_label = label_t::make_jump(mid_label, next_label);
basic_block_t& jump_bb = res.insert(jump_label);
jump_bb.insert(Assume{cond1});
Expand Down Expand Up @@ -369,7 +369,7 @@ cfg_t prepare_cfg(const InstructionSeq& prog, const program_info& info, const bo
// hierarchical decomposition of the CFG that identifies all strongly connected components (cycles) and their entry
// points. These entry points serve as natural locations for loop counters that help verify program termination.
if (check_for_termination) {
wto_t wto(det_cfg);
const wto_t wto(det_cfg);
wto.for_each_loop_head(
[&](const label_t& label) { det_cfg.get_node(label).insert_front(IncrementLoopCounter{label}); });
}
Expand Down
6 changes: 3 additions & 3 deletions src/asm_files.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -232,7 +232,7 @@ static void append_subprograms(raw_program& prog, const vector<raw_program>& pro
const ELFIO::const_symbol_section_accessor& symbols) {
// Perform function relocations and fill in the inst.imm values of CallLocal instructions.
std::map<string, ELFIO::Elf_Xword> subprogram_offsets;
for (auto& reloc : function_relocations) {
for (const auto& reloc : function_relocations) {
if (reloc.prog_index >= programs.size()) {
continue;
}
Expand Down Expand Up @@ -265,7 +265,7 @@ static void append_subprograms(raw_program& prog, const vector<raw_program>& pro
std::map<std::string, size_t> parse_map_section(const libbtf::btf_type_data& btf_data,
std::vector<EbpfMapDescriptor>& map_descriptors) {
std::map<std::string, size_t> map_offsets;
for (auto& map : parse_btf_map_section(btf_data)) {
for (const auto& map : parse_btf_map_section(btf_data)) {
map_offsets.emplace(map.name, map_descriptors.size());
map_descriptors.push_back({
.original_fd = gsl::narrow_cast<int>(map.type_id),
Expand Down Expand Up @@ -339,7 +339,7 @@ vector<raw_program> read_elf(std::istream& input_stream, const std::string& path
std::map<int, int> type_id_to_fd_map;
int pseudo_fd = 1;
// Gather the typeids for each map and assign a pseudo-fd to each map.
for (auto& map_descriptor : info.map_descriptors) {
for (const auto& map_descriptor : info.map_descriptors) {
if (!type_id_to_fd_map.contains(map_descriptor.original_fd)) {
type_id_to_fd_map[map_descriptor.original_fd] = pseudo_fd++;
}
Expand Down
4 changes: 2 additions & 2 deletions src/asm_marshal.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -327,9 +327,9 @@ vector<ebpf_inst> marshal(const InstructionSeq& insts) {
for (auto [label, ins, _] : insts) {
(void)label; // unused
if (const auto pins = std::get_if<Jmp>(&ins)) {
pins->target = label_t(pc_of_label.at(pins->target));
pins->target = label_t{gsl::narrow<int>(pc_of_label.at(pins->target))};
}
for (auto e : marshal(ins, pc)) {
for (const auto e : marshal(ins, pc)) {
pc++;
res.push_back(e);
}
Expand Down
28 changes: 14 additions & 14 deletions src/asm_ostream.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ using std::optional;
using std::string;
using std::vector;

std::ostream& operator<<(std::ostream& os, ArgSingle::Kind kind) {
std::ostream& operator<<(std::ostream& os, const ArgSingle::Kind kind) {
switch (kind) {
case ArgSingle::Kind::ANYTHING: return os << "uint64_t";
case ArgSingle::Kind::PTR_TO_CTX: return os << "ctx";
Expand All @@ -34,7 +34,7 @@ std::ostream& operator<<(std::ostream& os, ArgSingle::Kind kind) {
return os;
}

std::ostream& operator<<(std::ostream& os, ArgPair::Kind kind) {
std::ostream& operator<<(std::ostream& os, const ArgPair::Kind kind) {
switch (kind) {
case ArgPair::Kind::PTR_TO_READABLE_MEM: return os << "mem";
case ArgPair::Kind::PTR_TO_READABLE_MEM_OR_NULL: return os << "mem?";
Expand All @@ -44,12 +44,12 @@ std::ostream& operator<<(std::ostream& os, ArgPair::Kind kind) {
return os;
}

std::ostream& operator<<(std::ostream& os, ArgSingle arg) {
std::ostream& operator<<(std::ostream& os, const ArgSingle arg) {
os << arg.kind << " " << arg.reg;
return os;
}

std::ostream& operator<<(std::ostream& os, ArgPair arg) {
std::ostream& operator<<(std::ostream& os, const ArgPair arg) {
os << arg.kind << " " << arg.mem << "[" << arg.size;
if (arg.can_be_zero) {
os << "?";
Expand All @@ -58,7 +58,7 @@ std::ostream& operator<<(std::ostream& os, ArgPair arg) {
return os;
}

std::ostream& operator<<(std::ostream& os, Bin::Op op) {
std::ostream& operator<<(std::ostream& os, const Bin::Op op) {
using Op = Bin::Op;
switch (op) {
case Op::MOV: return os;
Expand All @@ -83,7 +83,7 @@ std::ostream& operator<<(std::ostream& os, Bin::Op op) {
return os;
}

std::ostream& operator<<(std::ostream& os, Condition::Op op) {
std::ostream& operator<<(std::ostream& os, const Condition::Op op) {
using Op = Condition::Op;
switch (op) {
case Op::EQ: return os << "==";
Expand All @@ -103,7 +103,7 @@ std::ostream& operator<<(std::ostream& os, Condition::Op op) {
return os;
}

static string size(int w) { return string("u") + std::to_string(w * 8); }
static string size(const int w) { return string("u") + std::to_string(w * 8); }

std::ostream& operator<<(std::ostream& os, ValidStore const& a) {
return os << a.mem << ".type != stack -> " << TypeConstraint{a.val, TypeGroup::number};
Expand Down Expand Up @@ -196,7 +196,7 @@ struct InstructionPrinterVisitor {

// llvm-objdump uses "w<number>" for 32-bit operations and "r<number>" for 64-bit operations.
// We use the same convention here for consistency.
static std::string reg_name(Reg const& a, bool is64) { return ((is64) ? "r" : "w") + std::to_string(a.v); }
static std::string reg_name(Reg const& a, const bool is64) { return ((is64) ? "r" : "w") + std::to_string(a.v); }

void operator()(Bin const& b) {
os_ << reg_name(b.dst, b.is64) << " " << b.op << "= " << b.v;
Expand Down Expand Up @@ -226,7 +226,7 @@ struct InstructionPrinterVisitor {
os_ << "r0 = " << call.name << ":" << call.func << "(";
for (uint8_t r = 1; r <= 5; r++) {
// Look for a singleton.
auto single = std::ranges::find_if(call.singles, [r](ArgSingle arg) { return arg.reg.v == r; });
auto single = std::ranges::find_if(call.singles, [r](const ArgSingle arg) { return arg.reg.v == r; });
if (single != call.singles.end()) {
if (r > 1) {
os_ << ", ";
Expand All @@ -236,7 +236,7 @@ struct InstructionPrinterVisitor {
}

// Look for the start of a pair.
auto pair = std::ranges::find_if(call.pairs, [r](ArgPair arg) { return arg.mem.v == r; });
auto pair = std::ranges::find_if(call.pairs, [r](const ArgPair arg) { return arg.mem.v == r; });
if (pair != call.pairs.end()) {
if (r > 1) {
os_ << ", ";
Expand Down Expand Up @@ -269,7 +269,7 @@ struct InstructionPrinterVisitor {
os_ << "goto label <" << to_string(b.target) << ">";
}

void operator()(Jmp const& b, int offset) {
void operator()(Jmp const& b, const int offset) {
const string sign = offset > 0 ? "+" : "";
const string target = sign + std::to_string(offset) + " <" + to_string(b.target) + ">";

Expand Down Expand Up @@ -403,7 +403,7 @@ auto get_labels(const InstructionSeq& insts) {
}

void print(const InstructionSeq& insts, std::ostream& out, const std::optional<const label_t>& label_to_print,
bool print_line_info) {
const bool print_line_info) {
const auto pc_of_label = get_labels(insts);
pc_t pc = 0;
std::string previous_source;
Expand Down Expand Up @@ -491,7 +491,7 @@ void print_dot(const cfg_t& cfg, const std::string& outfile) {

std::ostream& operator<<(std::ostream& o, const basic_block_t& bb) {
o << bb.label() << ":\n";
for (auto const& s : bb) {
for (const auto& s : bb) {
o << " " << s << ";\n";
}
auto [it, et] = bb.next_blocks();
Expand All @@ -514,7 +514,7 @@ std::ostream& operator<<(std::ostream& o, const basic_block_t& bb) {

std::ostream& operator<<(std::ostream& o, const crab::basic_block_rev_t& bb) {
o << bb.label() << ":\n";
for (auto const& s : bb) {
for (const auto& s : bb) {
o << " " << s << ";\n";
}
o << "--> [";
Expand Down
2 changes: 1 addition & 1 deletion src/asm_parse.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -93,7 +93,7 @@ static Reg reg(const std::string& s) {
return Reg{res};
}

static Imm imm(const std::string& s, bool lddw) {
static Imm imm(const std::string& s, const bool lddw) {
const int base = s.find("0x") != std::string::npos ? 16 : 10;

if (lddw) {
Expand Down
26 changes: 12 additions & 14 deletions src/assertions.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -37,26 +37,24 @@ class AssertExtractor {
explicit AssertExtractor(program_info info, std::optional<label_t> label)
: info{std::move(info)}, current_label(label) {}

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

vector<Assert> operator()(Assert const&) const {
vector<Assert> operator()(const Assert&) const {
assert(false);
return {};
}

vector<Assert> operator()(IncrementLoopCounter& ipc) const {
return {{BoundedLoopCount{ipc.name}}};
}
vector<Assert> operator()(const IncrementLoopCounter& ipc) const { return {{BoundedLoopCount{ipc.name}}}; }

vector<Assert> operator()(LoadMapFd const&) const { return {}; }
vector<Assert> operator()(const LoadMapFd&) const { return {}; }

/// Packet access implicitly uses R6, so verify that R6 still has a pointer to the context.
vector<Assert> operator()(Packet const&) const { return zero_offset_ctx({6}); }
vector<Assert> operator()(const Packet&) const { return zero_offset_ctx({6}); }

vector<Assert> operator()(Exit const&) const {
vector<Assert> operator()(const Exit&) const {
vector<Assert> res;
if (current_label->stack_frame_prefix.empty()) {
// Verify that Exit returns a number.
Expand All @@ -65,7 +63,7 @@ class AssertExtractor {
return res;
}

vector<Assert> operator()(Call const& call) const {
vector<Assert> operator()(const Call& call) const {
vector<Assert> res;
std::optional<Reg> map_fd_reg;
res.emplace_back(ValidCall{call.func, call.stack_frame_prefix});
Expand Down Expand Up @@ -122,9 +120,9 @@ class AssertExtractor {
return res;
}

vector<Assert> operator()(CallLocal const& call) const { return {}; }
vector<Assert> operator()(const CallLocal&) const { return {}; }

vector<Assert> operator()(Callx const& callx) const {
vector<Assert> operator()(const Callx& callx) const {
vector<Assert> res;
res.emplace_back(TypeConstraint{callx.func, TypeGroup::number});
res.emplace_back(FuncConstraint{callx.func});
Expand Down Expand Up @@ -231,7 +229,7 @@ class AssertExtractor {
};
}

vector<Assert> operator()(const Un ins) const { return {Assert{TypeConstraint{ins.dst, TypeGroup::number}}}; }
vector<Assert> operator()(const Un& ins) const { return {Assert{TypeConstraint{ins.dst, TypeGroup::number}}}; }

vector<Assert> operator()(const Bin& ins) const {
switch (ins.op) {
Expand Down Expand Up @@ -305,8 +303,8 @@ void explicate_assertions(cfg_t& cfg, const program_info& info) {
for (auto& [label, bb] : cfg) {
(void)label; // unused
vector<Instruction> insts;
for (const auto& ins : vector<Instruction>(bb.begin(), bb.end())) {
for (auto a : get_assertions(ins, info, bb.label())) {
for (const auto& ins : bb) {
for (const auto& a : get_assertions(ins, info, bb.label())) {
insts.emplace_back(a);
}
insts.push_back(ins);
Expand Down
6 changes: 3 additions & 3 deletions src/crab/array_domain.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -226,7 +226,7 @@ class offset_map_t final {
void operator-=(const cell_t& c) { remove_cell(c); }

void operator-=(const std::vector<cell_t>& cells) {
for (auto const& c : cells) {
for (const auto& c : cells) {
this->operator-=(c);
}
}
Expand Down Expand Up @@ -290,7 +290,7 @@ std::vector<cell_t> offset_map_t::get_overlap_cells_symbolic_offset(const NumAbs
}
if (!largest_cell.is_null()) {
if (largest_cell.symbolic_overlap(symb_lb, symb_ub, dom)) {
for (auto& c : o_cells) {
for (const auto& c : o_cells) {
out.push_back(c);
}
}
Expand Down Expand Up @@ -547,7 +547,7 @@ static std::optional<std::pair<offset_t, unsigned>> kill_and_find_var(NumAbsDoma
}
if (!cells.empty()) {
// Forget the scalars from the numerical domain
for (auto const& c : cells) {
for (const auto& c : cells) {
inv -= c.get_scalar(kind);

// Forget signed and unsigned values together.
Expand Down
Loading

0 comments on commit 1e5de90

Please sign in to comment.