Const all the things

src/asm_cfg.cpp

@@ -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;
@@ -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)) {
@@ -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)) {
@@ -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);
         }
@@ -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) {
@@ -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});
@@ -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}); });
     }

src/asm_files.cpp

@@ -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;
         }
@@ -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),
@@ -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++;
             }

src/asm_marshal.cpp

@@ -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);
         }

src/asm_ostream.cpp

@@ -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";
@@ -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?";
@@ -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 << "?";
@@ -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;
@@ -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 << "==";
@@ -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};
@@ -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;
@@ -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_ << ", ";
@@ -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_ << ", ";
@@ -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) + ">";
 
@@ -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;
@@ -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();
@@ -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 << "--> [";

src/asm_parse.cpp

@@ -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) {

src/assertions.cpp

@@ -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.
@@ -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});
@@ -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});
@@ -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) {
@@ -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);

src/crab/array_domain.cpp

@@ -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);
         }
     }
@@ -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);
                 }
             }
@@ -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.