Minor updates to move the code to more const-correct

src/asm_files.cpp

@@ -423,8 +423,8 @@ vector<raw_program> read_elf(std::istream& input_stream, const std::string& path
                         function_relocation fr{.prog_index = res.size(),
                                                .source_offset = offset / sizeof(ebpf_inst),
                                                .relocation_entry_index = index,
-                                               .target_function_name = symbol_name};
-                        function_relocations.push_back(fr);
+                                               .target_function_name = std::move(symbol_name)};
+                        function_relocations.emplace_back(std::move(fr));
                         continue;
                     }
 
@@ -436,11 +436,11 @@ vector<raw_program> read_elf(std::istream& input_stream, const std::string& path
 
                     string unresolved_symbol = "Unresolved external symbol " + symbol_name + " in section " + name +
                                                " at location " + std::to_string(offset / sizeof(ebpf_inst));
-                    unresolved_symbols_errors.push_back(unresolved_symbol);
+                    unresolved_symbols_errors.emplace_back(std::move(unresolved_symbol));
                 }
             }
             prog.line_info.resize(prog.prog.size());
-            res.push_back(prog);
+            res.emplace_back(std::move(prog));
             program_offset += program_size;
         }
     }

src/asm_ostream.cpp

@@ -299,7 +299,7 @@ struct InstructionPrinterVisitor {
 
     void print(Deref const& access) {
         const string sign = access.offset < 0 ? " - " : " + ";
-        int offset = std::abs(access.offset); // what about INT_MIN?
+        const int offset = std::abs(access.offset); // what about INT_MIN?
         os_ << "*(" << size(access.width) << " *)";
         os_ << "(" << access.basereg << sign << offset << ")";
     }
@@ -440,6 +440,7 @@ void print(const InstructionSeq& insts, std::ostream& out, const std::optional<c
     }
 }
 
+// clang-format off
 std::ostream& operator<<(std::ostream& o, const EbpfMapDescriptor& desc) {
     return o << "("
              << "original_fd = " << desc.original_fd << ", "
@@ -449,6 +450,7 @@ std::ostream& operator<<(std::ostream& o, const EbpfMapDescriptor& desc) {
              << "value_size = " << desc.value_size << ", "
              << "key_size = " << desc.key_size << ")";
 }
+// clang-format on
 
 void print_map_descriptors(const std::vector<EbpfMapDescriptor>& descriptors, std::ostream& o) {
     int i = 0;
@@ -493,8 +495,7 @@ std::ostream& operator<<(std::ostream& o, const basic_block_t& bb) {
     }
     auto [it, et] = bb.next_blocks();
     if (it != et) {
-        o << "  "
-          << "goto ";
+        o << "  " << "goto ";
         while (it != et) {
             o << *it;
             ++it;

src/asm_unmarshal.cpp

@@ -539,7 +539,7 @@ struct Unmarshaller {
                 }
                 const bool can_be_zero = (args[i + 1] == EBPF_ARGUMENT_TYPE_CONST_SIZE_OR_ZERO);
                 res.pairs.push_back({toArgPairKind(args[i]), Reg{gsl::narrow<uint8_t>(i)},
-                                     Reg{gsl::narrow<uint8_t>(i + 1)}, can_be_zero});
+                                               Reg{gsl::narrow<uint8_t>(i + 1)}, can_be_zero});
                 i++;
                 break;
             }

src/assertions.cpp

@@ -1,5 +1,6 @@
 // Copyright (c) Prevail Verifier contributors.
 // SPDX-License-Identifier: MIT
+#include <cassert>
 #include <cinttypes>
 
 #include <utility>
@@ -41,7 +42,7 @@ class AssertExtractor {
         return {};
     }
 
-    vector<Assert> operator()(IncrementLoopCounter) const {
+    vector<Assert> operator()(IncrementLoopCounter const&) const {
         assert(false);
         return {};
     }
@@ -193,6 +194,7 @@ class AssertExtractor {
         Imm width{static_cast<uint32_t>(ins.access.width)};
         const int offset = ins.access.offset;
         if (basereg.v == R10_STACK_POINTER) {
+            // We know we are accessing the stack.
             if (offset < -EBPF_STACK_SIZE || offset + static_cast<int>(width.v) > 0) {
                 // This assertion will fail
                 res.emplace_back(

src/crab/add_bottom.hpp

@@ -110,7 +110,7 @@ class AddBottom final {
         if (!dom || !o.dom) {
             return bottom();
         }
-        if (auto res = (*dom).meet(*o.dom)) {
+        if (const auto res = (*dom).meet(*o.dom)) {
             return AddBottom(*res);
         }
         return bottom();

src/crab/array_domain.cpp

@@ -2,6 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0
 
 #include <algorithm>
+#include <cassert>
 #include <optional>
 #include <set>
 #include <unordered_map>
@@ -345,9 +346,9 @@ std::vector<cell_t> offset_map_t::get_overlap_cells(const offset_t o, const unsi
         std::vector<cell_set_t> upto_lb;
         upto_lb.reserve(std::distance(_map.begin(), lb_it));
         for (auto it = _map.begin(), et = lb_it; it != et; ++it) {
-            upto_lb.push_back(it->second);
+            upto_lb.emplace_back(it->second);
         }
-        upto_lb.push_back(lb_it->second);
+        upto_lb.emplace_back(lb_it->second);
 
         for (int i = gsl::narrow<int>(upto_lb.size() - 1); i >= 0; --i) {
             ///////
@@ -494,7 +495,7 @@ void array_domain_t::split_number_var(NumAbsDomain& inv, data_kind_t kind, const
     auto size = n_bytes->narrow<unsigned int>();
     offset_t o(n->narrow<index_t>());
 
-    std::vector<cell_t> cells = offset_map.get_overlap_cells(o, size);
+    const std::vector<cell_t> cells = offset_map.get_overlap_cells(o, size);
     for (cell_t const& c : cells) {
         interval_t intv = c.to_interval();
         int cell_start_index = intv.lb().narrow<int>();
@@ -714,7 +715,7 @@ std::optional<linear_expression_t> array_domain_t::load(const NumAbsDomain& inv,
 
         std::vector<cell_t> cells = offset_map.get_overlap_cells(o, size);
         if (cells.empty()) {
-            cell_t c = offset_map.mk_cell(o, size);
+            const cell_t c = offset_map.mk_cell(o, size);
             // Here it's ok to do assignment (instead of expand) because c is not a summarized variable.
             // Otherwise, it would be unsound.
             return c.get_scalar(kind);

src/crab/bitset_domain.cpp

@@ -2,6 +2,8 @@
 // SPDX-License-Identifier: MIT
 #include "bitset_domain.hpp"
 #include <ostream>
+#include <set>
+#include <string>
 
 std::ostream& operator<<(std::ostream& o, const bitset_domain_t& b) {
     o << "Numbers -> {";
@@ -58,5 +60,6 @@ string_invariant bitset_domain_t::to_set() const {
         result.insert(value);
         i = j;
     }
-    return string_invariant{result};
+
+    return string_invariant{std::move(result)};
 }

src/crab/cfg.hpp

@@ -15,6 +15,7 @@
 #include <map>
 #include <memory>
 #include <set>
+#include <utility>
 #include <variant>
 #include <vector>
 
@@ -62,10 +63,10 @@ class basic_block_t final {
     void insert(const Instruction& arg) {
         assert(label() != label_t::entry);
         assert(label() != label_t::exit);
-        m_ts.push_back(arg);
+        m_ts.emplace_back(arg);
     }
 
-    explicit basic_block_t(label_t _label) : m_label(_label) {}
+    explicit basic_block_t(label_t _label) : m_label(std::move(_label)) {}
 
     ~basic_block_t() = default;
 
@@ -338,7 +339,7 @@ class cfg_t final {
             }
         }
 
-        for (auto p : dead_edges) {
+        for (const auto p : dead_edges) {
             (*p.first) -= (*p.second);
         }
 
@@ -373,7 +374,7 @@ class cfg_t final {
         std::vector<label_t> res;
         res.reserve(m_blocks.size());
         for (const auto& p : m_blocks) {
-            res.push_back(p.first);
+            res.emplace_back(p.first);
         }
         return res;
     }
@@ -524,7 +525,7 @@ class cfg_rev_t final {
     neighbour_const_range prev_nodes(const label_t& bb) { return _cfg.next_nodes(bb); }
 
     basic_block_rev_t& get_node(const label_t& _label) {
-        auto it = _rev_bbs.find(_label);
+        const auto it = _rev_bbs.find(_label);
         if (it == _rev_bbs.end()) {
             CRAB_ERROR("Basic block ", _label, " not found in the CFG: ", __LINE__);
         }
@@ -533,7 +534,7 @@ class cfg_rev_t final {
 
     [[nodiscard]]
     const basic_block_rev_t& get_node(const label_t& _label) const {
-        auto it = _rev_bbs.find(_label);
+        const auto it = _rev_bbs.find(_label);
         if (it == _rev_bbs.end()) {
             CRAB_ERROR("Basic block ", _label, " not found in the CFG: ", __LINE__);
         }

src/crab/fwd_analyzer.cpp

@@ -1,7 +1,9 @@
 // Copyright (c) Prevail Verifier contributors.
 // SPDX-License-Identifier: Apache-2.0
+#include <memory>
 #include <utility>
 #include <variant>
+#include <vector>
 
 #include "crab/cfg.hpp"
 #include "crab/wto.hpp"
@@ -126,7 +128,7 @@ std::pair<invariant_table_t, invariant_table_t> run_forward_analyzer(cfg_t& cfg,
         std::vector<label_t> cycle_heads;
         for (auto& component : analyzer._wto) {
             if (const auto pc = std::get_if<std::shared_ptr<wto_cycle_t>>(&component)) {
-                cycle_heads.push_back((*pc)->head());
+                cycle_heads.emplace_back((*pc)->head());
             }
         }
         for (const label_t& label : cycle_heads) {

src/crab/interval.hpp

@@ -175,8 +175,8 @@ class interval_t final {
         } else if (x.is_bottom()) {
             return *this;
         } else {
-            bound_t lb = x._lb < _lb ? ts.get_prev(x._lb) : _lb;
-            bound_t ub = _ub < x._ub ? ts.get_next(x._ub) : _ub;
+            const bound_t lb = x._lb < _lb ? ts.get_prev(x._lb) : _lb;
+            const bound_t ub = _ub < x._ub ? ts.get_next(x._ub) : _ub;
             return interval_t{lb, ub};
         }
     }

src/crab/linear_expression.hpp

@@ -25,7 +25,7 @@ class linear_expression_t final {
     // Get the coefficient for a given variable, which is 0 if it has no term in the expression.
     [[nodiscard]]
     number_t coefficient_of(const variable_t& variable) const {
-        auto it = _variable_terms.find(variable);
+        const auto it = _variable_terms.find(variable);
         if (it == _variable_terms.end()) {
             return 0;
         }
@@ -155,7 +155,7 @@ inline std::ostream& operator<<(std::ostream& o, const linear_expression_t& expr
     expression.output_variable_terms(o);
 
     // Output the constant term.
-    number_t constant = expression.constant_term();
+    const number_t constant = expression.constant_term();
     if (constant < 0) {
         o << constant;
     } else if (constant > 0) {

src/crab/split_dbm.cpp

@@ -1,6 +1,9 @@
 // Copyright (c) Prevail Verifier contributors.
 // SPDX-License-Identifier: Apache-2.0
+#include <cassert>
+#include <optional>
 #include <utility>
+#include <vector>
 
 #include <gsl/narrow>
 
@@ -785,8 +788,7 @@ bool SplitDBM::add_constraint(const linear_constraint_t& cst) {
     case constraint_kind_t::EQUALS_ZERO: {
         const linear_expression_t& exp = cst.expression();
         if (!add_linear_leq(exp) || !add_linear_leq(exp.negate())) {
-            CRAB_LOG("zones-split", std::cout << " ~~> _|_"
-                                              << "\n");
+            CRAB_LOG("zones-split", std::cout << " ~~> _|_" << "\n");
             return false;
         }
         // g.check_adjs();
@@ -1200,7 +1202,7 @@ string_invariant SplitDBM::to_set() const {
             result.insert(to_string(vd, vs, w, false));
         }
     }
-    return string_invariant{result};
+    return string_invariant{std::move(result)};
 }
 
 std::ostream& operator<<(std::ostream& o, const SplitDBM& dom) { return o << dom.to_set(); }

src/crab/split_dbm.hpp

@@ -226,7 +226,7 @@ class SplitDBM final {
 
     void assign(variable_t lhs, const linear_expression_t& e);
 
-    void assign(std::optional<variable_t> x, const linear_expression_t& e) {
+    void assign(const std::optional<variable_t>& x, const linear_expression_t& e) {
         if (x) {
             assign(*x, e);
         }

src/crab/var_factory.cpp

@@ -148,8 +148,7 @@ std::ostream& operator<<(std::ostream& o, const data_kind_t& s) { return o << na
 
 static std::string mk_scalar_name(const data_kind_t kind, const number_t& o, const number_t& size) {
     std::stringstream os;
-    os << "s"
-       << "[" << o;
+    os << "s" << "[" << o;
     if (size != 1) {
         os << "..." << o + size - 1;
     }
@@ -167,7 +166,7 @@ variable_t variable_t::cell_var(const data_kind_t array, const number_t& offset,
 
 // Given a type variable, get the associated variable of a given kind.
 variable_t variable_t::kind_var(const data_kind_t kind, const variable_t type_variable) {
-    const std::string name = type_variable.name();
+    const std::string& name = type_variable.name();
     return make(name.substr(0, name.rfind('.') + 1) + name_of(kind));
 }
 

src/crab/variable.hpp

@@ -35,8 +35,9 @@ class variable_t final {
     // for flat_map
     bool operator<(const variable_t o) const { return _id < o._id; }
 
+    // callers can take a copy if they need it
     [[nodiscard]]
-    std::string name() const {
+    const std::string& name() const {
         return names->at(_id);
     }
 

src/crab/wto.cpp

@@ -163,7 +163,7 @@ void wto_builder_t::continue_visit(const label_t& vertex, wto_partition_t& parti
     // (end of the vector which stores the cycle in reverse order).
     auto cycle = containing_cycle.lock();
 
-    cycle->_components.push_back(vertex);
+    cycle->_components.emplace_back(vertex);
 
     // Insert the component into the current partition.
     partition.emplace_back(cycle);