Skip to content

Commit

Permalink
const all the things
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
elazarg committed Nov 7, 2024
1 parent 0669c85 commit 9d02903
Show file tree
Hide file tree
Showing 33 changed files with 198 additions and 202 deletions.
16 changes: 8 additions & 8 deletions src/asm_cfg.cpp
View file
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
View file
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
View file
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
View file
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
View file
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
8 changes: 3 additions & 5 deletions src/assertions.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -47,9 +47,7 @@ class AssertExtractor {
return {};
}

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

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

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 : vector(bb.begin(), bb.end())) {
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
View file
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
29 changes: 14 additions & 15 deletions src/crab/cfg.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -145,7 +145,7 @@ class basic_block_t final {
// insert all statements of other at the back
void move_back(basic_block_t& other) {
m_ts.reserve(m_ts.size() + other.m_ts.size());
std::move(other.m_ts.begin(), other.m_ts.end(), std::back_inserter(m_ts));
std::ranges::move(other.m_ts, std::back_inserter(m_ts));
}

[[nodiscard]]
Expand Down Expand Up @@ -242,8 +242,8 @@ class cfg_t final {
public:
using iterator = basic_block_map_t::iterator;
using const_iterator = basic_block_map_t::const_iterator;
using label_iterator = boost::transform_iterator<get_label, typename basic_block_map_t::iterator>;
using const_label_iterator = boost::transform_iterator<get_label, typename basic_block_map_t::const_iterator>;
using label_iterator = boost::transform_iterator<get_label, basic_block_map_t::iterator>;
using const_label_iterator = boost::transform_iterator<get_label, basic_block_map_t::const_iterator>;

private:
basic_block_map_t m_blocks;
Expand Down Expand Up @@ -341,8 +341,8 @@ class cfg_t final {
}
}

for (auto p : dead_edges) {
(*p.first) -= (*p.second);
for (const auto& p : dead_edges) {
*p.first -= *p.second;
}

m_blocks.erase(_label);
Expand Down Expand Up @@ -457,7 +457,7 @@ class cfg_t final {
// mark reachable blocks from curId
template <class AnyCfg>
void mark_alive_blocks(label_t curId, AnyCfg& cfg_t, visited_t& visited) {
if (visited.count(curId) > 0) {
if (visited.contains(curId)) {
return;
}
visited.insert(curId);
Expand All @@ -482,7 +482,6 @@ class cfg_rev_t final {
// For BGL
using neighbour_const_iterator = basic_block_t::neighbour_const_iterator;

public:
using basic_block_rev_map_t = std::map<label_t, basic_block_rev_t>;
using iterator = basic_block_rev_map_t::iterator;
using const_iterator = basic_block_rev_map_t::const_iterator;
Expand Down Expand Up @@ -557,9 +556,9 @@ class cfg_rev_t final {
return _rev_bbs.end();
}

label_iterator label_begin() { return _cfg.label_begin(); }
label_iterator label_begin() const { return _cfg.label_begin(); }

label_iterator label_end() { return _cfg.label_end(); }
label_iterator label_end() const { return _cfg.label_end(); }

[[nodiscard]]
label_t exit_label() const {
Expand All @@ -573,11 +572,11 @@ inline void cfg_t::remove_useless_blocks() {
visited_t useful, useless;
mark_alive_blocks(rev_cfg.entry_label(), rev_cfg, useful);

if (!useful.count(exit_label())) {
if (!useful.contains(exit_label())) {
CRAB_ERROR("Exit block must be reachable");
}
for (auto const& label : labels()) {
if (!useful.count(label)) {
for (const auto& label : labels()) {
if (!useful.contains(label)) {
useless.insert(label);
}
}
Expand All @@ -591,13 +590,13 @@ inline void cfg_t::remove_unreachable_blocks() {
visited_t alive, dead;
mark_alive_blocks(entry_label(), *this, alive);

for (auto const& label : labels()) {
if (alive.count(label) <= 0) {
for (const auto& label : labels()) {
if (!alive.contains(label)) {
dead.insert(label);
}
}

if (dead.count(exit_label())) {
if (dead.contains(exit_label())) {
CRAB_ERROR("Exit block must be reachable");
}
for (const auto& _label : dead) {
Expand Down
Loading

0 comments on commit 9d02903

Please sign in to comment.