Address linter / compiler warnings

CMakeLists.txt

@@ -37,7 +37,7 @@ elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
   if (NOT NUGET)
     message("ERROR: You must first install nuget.exe from https://www.nuget.org/downloads")
   else ()
-    exec_program(${NUGET} ARGS install "Boost" -Version 1.81.0 -ExcludeVersion -OutputDirectory ${CMAKE_BINARY_DIR}/packages)
+    execute_process(COMMAND ${NUGET} ARGS install "Boost" -Version 1.81.0 -ExcludeVersion -OutputDirectory ${CMAKE_BINARY_DIR}/packages)
     set(BOOST_VERSION 1.81.0)
   endif()
   set(Boost_INCLUDE_DIRS ${CMAKE_BINARY_DIR}/packages/boost/lib/native/include)
@@ -93,7 +93,7 @@ if ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU" OR
     "${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang")
   set(COMMON_FLAGS -Wall -Wfatal-errors -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8)
 
-  set(RELEASE_FLAGS -O2 -flto -ffat-lto-objects)
+  set(RELEASE_FLAGS -O2 -flto=auto -ffat-lto-objects)
 
   set(DEBUG_FLAGS -O0 -g3 -fno-omit-frame-pointer)
 

src/asm_files.cpp

@@ -1,23 +1,21 @@
 // Copyright (c) Prevail Verifier contributors.
 // SPDX-License-Identifier: MIT
-#include <cassert>
 #include <iostream>
 #include <map>
+#include <set>
 #include <string>
 #include <vector>
-#include <set>
-#include <map>
 #include <sys/stat.h>
 
-#include "asm_files.hpp"
 #include "libbtf/btf.h"
 #include "libbtf/btf_json.h"
 #include "libbtf/btf_map.h"
 #include "libbtf/btf_parse.h"
-#include "platform.hpp"
-
 #include "elfio/elfio.hpp"
 
+#include "asm_files.hpp"
+#include "platform.hpp"
+
 using std::cout;
 using std::string;
 using std::vector;
@@ -183,7 +181,7 @@ vector<raw_program> read_elf(std::istream& input_stream, const std::string& path
                 .key_size = map.key_size,
                 .value_size = map.value_size,
                 .max_entries = map.max_entries,
-                .inner_map_fd = map.inner_map_type_id != 0 ? map.inner_map_type_id : -1,
+                .inner_map_fd = map.inner_map_type_id != 0 ? map.inner_map_type_id : DEFAULT_MAP_FD,
             });
         }
         map_record_size_or_map_offsets = map_offsets;
@@ -203,7 +201,7 @@ vector<raw_program> read_elf(std::istream& input_stream, const std::string& path
         // Replace the typeids with the pseudo-fds.
         for (auto &map_descriptor : info.map_descriptors) {
             map_descriptor.original_fd = type_id_to_fd_map[map_descriptor.original_fd];
-            if (map_descriptor.inner_map_fd != -1) {
+            if (map_descriptor.inner_map_fd != DEFAULT_MAP_FD) {
                 map_descriptor.inner_map_fd = type_id_to_fd_map[map_descriptor.inner_map_fd];
             }
         }

src/asm_unmarshal.cpp

@@ -1,7 +1,6 @@
 // Copyright (c) Prevail Verifier contributors.
 // SPDX-License-Identifier: MIT
 #include <cassert>
-#include <cstring> // memcmp
 #include <iostream>
 #include <string>
 #include <vector>
@@ -429,19 +428,6 @@ struct Unmarshaller {
                 break;
             }
             }
-            /*
-            vector<ebpf_inst> marshalled = marshal(new_ins[0], pc);
-            ebpf_inst actual = marshalled[0];
-            if (std::memcmp(&actual, &inst, sizeof(inst))) {
-                std::cerr << "new: " << new_ins[0] << "\n";
-                compare("opcode", actual.opcode, inst.opcode);
-                compare("dst", actual.dst, inst.dst);
-                compare("src", actual.src, inst.src);
-                compare("offset", actual.offset, inst.offset);
-                compare("imm", actual.imm, inst.imm);
-                std::cerr << "\n";
-            }
-            */
             if (pc == insts.size() - 1 && fallthrough)
                 note("fallthrough in last instruction");
 

src/assertions.cpp

@@ -6,7 +6,6 @@
 #include <vector>
 
 #include "asm_syntax.hpp"
-#include "ebpf_vm_isa.hpp"
 #include "platform.hpp"
 #include "crab/cfg.hpp"
 

src/config.cpp

@@ -1,7 +1,6 @@
 // Copyright (c) Prevail Verifier contributors.
 // SPDX-License-Identifier: MIT
 #include "config.hpp"
-#include "platform.hpp"
 
 const ebpf_verifier_options_t ebpf_verifier_default_options = {
     .check_termination = false,

src/crab/array_domain.cpp

@@ -2,7 +2,6 @@
 // SPDX-License-Identifier: Apache-2.0
 
 #include <algorithm>
-#include <bitset>
 #include <optional>
 #include <set>
 #include <unordered_map>

src/crab/ebpf_domain.cpp

@@ -4,16 +4,13 @@
 // This file is eBPF-specific, not derived from CRAB.
 
 #include <bitset>
-#include <functional>
 #include <optional>
 #include <utility>
 #include <vector>
 
 #include "boost/endian/conversion.hpp"
 #include "boost/range/algorithm/set_algorithm.hpp"
 
-#include "crab_utils/stats.hpp"
-
 #include "crab/array_domain.hpp"
 #include "crab/ebpf_domain.hpp"
 
@@ -289,10 +286,6 @@ assume_signed_64bit_lt(const NumAbsDomain& inv, bool strict, variable_t left_sva
     using crab::interval_t;
     using namespace crab::dsl_syntax;
 
-    auto rlb = right_interval.lb();
-    auto lnub = left_interval_negative.truncate_to_sint(true).ub();
-    auto lnlb = left_interval_negative.truncate_to_sint(true).lb();
-
     if (right_interval <= interval_t::negative_int(true)) {
         // Interval can be represented as both an svalue and a uvalue since it fits in [INT_MIN, -1].
         return {strict ? (left_svalue < right_svalue) : (left_svalue <= right_svalue), number_t{0} <= left_uvalue,
@@ -316,9 +309,6 @@ assume_signed_32bit_lt(const NumAbsDomain& inv, bool strict, variable_t left_sva
     using crab::interval_t;
     using namespace crab::dsl_syntax;
 
-    auto rlb = right_interval.lb();
-    auto lpub = left_interval_positive.truncate_to_sint(false).ub();
-
     if (right_interval <= interval_t::negative_int(false)) {
         // Interval can be represented as both an svalue and a uvalue since it fits in [INT_MIN, -1],
         // aka [INT_MAX+1, UINT_MAX].
@@ -327,7 +317,8 @@ assume_signed_32bit_lt(const NumAbsDomain& inv, bool strict, variable_t left_sva
                 strict ? (left_svalue < right_svalue) : (left_svalue <= right_svalue)};
     } else if ((left_interval_negative | left_interval_positive) <= interval_t::nonnegative_int(false) &&
                right_interval <= interval_t::nonnegative_int(false)) {
-        // Interval can be represented as both an svalue and a uvalue since it fits in [0, INT_MAX].
+        // Interval can be represented as both an svalue and a uvalue since it fits in [0, INT_MAX]
+        auto lpub = left_interval_positive.truncate_to_sint(false).ub();
         return {left_svalue >= 0,
                 strict ? left_svalue < right_svalue : left_svalue <= right_svalue,
                 left_svalue <= left_uvalue,
@@ -384,9 +375,6 @@ assume_signed_32bit_gt(const NumAbsDomain& inv, bool strict, variable_t left_sva
     using crab::interval_t;
     using namespace crab::dsl_syntax;
 
-    auto rlb = right_interval.lb();
-    auto lpub = left_interval_positive.truncate_to_sint(false).ub();
-
     if (right_interval <= interval_t::nonnegative_int(false)) {
         // Interval can be represented as both an svalue and a uvalue since it fits in [0, INT_MAX].
         auto lpub = left_interval_positive.truncate_to_sint(false).ub();
@@ -1271,24 +1259,24 @@ bool ebpf_domain_t::TypeDomain::implies_type(const NumAbsDomain& inv, const line
     return inv.when(a).entail(b);
 }
 
-bool ebpf_domain_t::TypeDomain::is_in_group(const NumAbsDomain& m_inv, const Reg& r, TypeGroup group) const {
+bool ebpf_domain_t::TypeDomain::is_in_group(const NumAbsDomain& inv, const Reg& r, TypeGroup group) const {
     using namespace crab::dsl_syntax;
     variable_t t = reg_pack(r).type;
     switch (group) {
-    case TypeGroup::number: return m_inv.entail(t == T_NUM);
-    case TypeGroup::map_fd: return m_inv.entail(t == T_MAP);
-    case TypeGroup::map_fd_programs: return m_inv.entail(t == T_MAP_PROGRAMS);
-    case TypeGroup::ctx: return m_inv.entail(t == T_CTX);
-    case TypeGroup::packet: return m_inv.entail(t == T_PACKET);
-    case TypeGroup::stack: return m_inv.entail(t == T_STACK);
-    case TypeGroup::shared: return m_inv.entail(t == T_SHARED);
-    case TypeGroup::non_map_fd: return m_inv.entail(t >= T_NUM);
-    case TypeGroup::mem: return m_inv.entail(t >= T_PACKET);
-    case TypeGroup::mem_or_num: return m_inv.entail(t >= T_NUM) && m_inv.entail(t != T_CTX);
-    case TypeGroup::pointer: return m_inv.entail(t >= T_CTX);
-    case TypeGroup::ptr_or_num: return m_inv.entail(t >= T_NUM);
-    case TypeGroup::stack_or_packet: return m_inv.entail(t >= T_PACKET) && m_inv.entail(t <= T_STACK);
-    case TypeGroup::singleton_ptr: return m_inv.entail(t >= T_CTX) && m_inv.entail(t <= T_STACK);
+    case TypeGroup::number: return inv.entail(t == T_NUM);
+    case TypeGroup::map_fd: return inv.entail(t == T_MAP);
+    case TypeGroup::map_fd_programs: return inv.entail(t == T_MAP_PROGRAMS);
+    case TypeGroup::ctx: return inv.entail(t == T_CTX);
+    case TypeGroup::packet: return inv.entail(t == T_PACKET);
+    case TypeGroup::stack: return inv.entail(t == T_STACK);
+    case TypeGroup::shared: return inv.entail(t == T_SHARED);
+    case TypeGroup::non_map_fd: return inv.entail(t >= T_NUM);
+    case TypeGroup::mem: return inv.entail(t >= T_PACKET);
+    case TypeGroup::mem_or_num: return inv.entail(t >= T_NUM) && inv.entail(t != T_CTX);
+    case TypeGroup::pointer: return inv.entail(t >= T_CTX);
+    case TypeGroup::ptr_or_num: return inv.entail(t >= T_NUM);
+    case TypeGroup::stack_or_packet: return inv.entail(t >= T_PACKET) && inv.entail(t <= T_STACK);
+    case TypeGroup::singleton_ptr: return inv.entail(t >= T_CTX) && inv.entail(t <= T_STACK);
     }
     assert(false);
     return false;
@@ -2581,7 +2569,6 @@ void ebpf_domain_t::operator()(const Bin& bin) {
             break;
         case Bin::Op::LSH:
             if (m_inv.entail(type_is_number(src_reg))) {
-                auto src = reg_pack(src_reg);
                 auto src_interval = m_inv.eval_interval(src.uvalue);
                 if (std::optional<number_t> sn = src_interval.singleton()) {
                     uint64_t imm = sn->cast_to_uint64() & (bin.is64 ? 63 : 31);
@@ -2600,7 +2587,6 @@ void ebpf_domain_t::operator()(const Bin& bin) {
             break;
         case Bin::Op::RSH:
             if (m_inv.entail(type_is_number(src_reg))) {
-                auto src = reg_pack(src_reg);
                 auto src_interval = m_inv.eval_interval(src.uvalue);
                 if (std::optional<number_t> sn = src_interval.singleton()) {
                     uint64_t imm = sn->cast_to_uint64() & (bin.is64 ? 63 : 31);

src/crab/ebpf_domain.hpp

@@ -31,8 +31,8 @@ class ebpf_domain_t final {
     static ebpf_domain_t bottom();
     void set_to_top();
     void set_to_bottom();
-    bool is_bottom() const;
-    bool is_top() const;
+    [[nodiscard]] bool is_bottom() const;
+    [[nodiscard]] bool is_top() const;
     bool operator<=(const ebpf_domain_t& other);
     bool operator==(const ebpf_domain_t& other) const;
     void operator|=(ebpf_domain_t&& other);
@@ -102,7 +102,7 @@ class ebpf_domain_t final {
     void apply_signed(crab::domains::NumAbsDomain& inv, crab::binop_t op, variable_t xs, variable_t xu, variable_t y,
                       variable_t z, int finite_width);
     void apply_unsigned(crab::domains::NumAbsDomain& inv, crab::binop_t op, variable_t xs, variable_t xu, variable_t y,
-                      variable_t z, int finite_width);
+                        variable_t z, int finite_width);
 
     void add(const Reg& reg, int imm, int finite_width);
     void add(variable_t lhs, variable_t op2);
@@ -147,15 +147,15 @@ class ebpf_domain_t final {
     void havoc_offsets(NumAbsDomain& inv, const Reg& reg);
 
     static std::optional<variable_t> get_type_offset_variable(const Reg& reg, int type);
-    std::optional<variable_t> get_type_offset_variable(const Reg& reg, const NumAbsDomain& inv) const;
-    std::optional<variable_t> get_type_offset_variable(const Reg& reg) const;
+    [[nodiscard]] std::optional<variable_t> get_type_offset_variable(const Reg& reg, const NumAbsDomain& inv) const;
+    [[nodiscard]] std::optional<variable_t> get_type_offset_variable(const Reg& reg) const;
 
     void scratch_caller_saved_registers();
-    std::optional<uint32_t> get_map_type(const Reg& map_fd_reg) const;
-    std::optional<uint32_t> get_map_inner_map_fd(const Reg& map_fd_reg) const;
-    crab::interval_t get_map_key_size(const Reg& map_fd_reg) const;
-    crab::interval_t get_map_value_size(const Reg& map_fd_reg) const;
-    crab::interval_t get_map_max_entries(const Reg& map_fd_reg) const;
+    [[nodiscard]] std::optional<uint32_t> get_map_type(const Reg& map_fd_reg) const;
+    [[nodiscard]] std::optional<uint32_t> get_map_inner_map_fd(const Reg& map_fd_reg) const;
+    [[nodiscard]] crab::interval_t get_map_key_size(const Reg& map_fd_reg) const;
+    [[nodiscard]] crab::interval_t get_map_value_size(const Reg& map_fd_reg) const;
+    [[nodiscard]] crab::interval_t get_map_max_entries(const Reg& map_fd_reg) const;
     void forget_packet_pointers();
     void havoc_register(NumAbsDomain& inv, const Reg& reg);
     void do_load_mapfd(const Reg& dst_reg, int mapfd, bool maybe_null);
@@ -178,14 +178,15 @@ class ebpf_domain_t final {
 
     void recompute_stack_numeric_size(NumAbsDomain& inv, const Reg& reg);
     void recompute_stack_numeric_size(NumAbsDomain& inv, variable_t type_variable);
-    void do_load_stack(NumAbsDomain& inv, const Reg& target_reg, const linear_expression_t& addr, int width, const Reg& src_reg);
+    void do_load_stack(NumAbsDomain& inv, const Reg& target_reg, const linear_expression_t& addr, int width,
+                       const Reg& src_reg);
     void do_load_ctx(NumAbsDomain& inv, const Reg& target_reg, const linear_expression_t& addr_vague, int width);
     void do_load_packet_or_shared(NumAbsDomain& inv, const Reg& target_reg, const linear_expression_t& addr, int width);
     void do_load(const Mem& b, const Reg& target_reg);
 
     template <typename X, typename Y, typename Z>
-    void do_store_stack(crab::domains::NumAbsDomain& inv, const number_t& width, const linear_expression_t& addr, X val_type, Y val_svalue, Z val_uvalue,
-                        const std::optional<reg_pack_t>& opt_val_reg);
+    void do_store_stack(crab::domains::NumAbsDomain& inv, const number_t& width, const linear_expression_t& addr,
+                        X val_type, Y val_svalue, Z val_uvalue, const std::optional<reg_pack_t>& opt_val_reg);
 
     template <typename Type, typename SValue, typename UValue>
     void do_mem_store(const Mem& b, Type val_type, SValue val_svalue, UValue val_uvalue,
@@ -195,7 +196,6 @@ class ebpf_domain_t final {
 
     static void initialize_packet(ebpf_domain_t& inv);
 
-
   private:
     /// Mapping from variables (including registers, types, offsets,
     /// memory locations, etc.) to numeric intervals or relationships
@@ -228,16 +228,17 @@ class ebpf_domain_t final {
         [[nodiscard]] bool has_type(const NumAbsDomain& inv, const number_t& t, type_encoding_t type) const;
 
         [[nodiscard]] bool same_type(const NumAbsDomain& inv, const Reg& a, const Reg& b) const;
-        [[nodiscard]] bool implies_type(const NumAbsDomain& inv, const linear_constraint_t& a, const linear_constraint_t& b) const;
-
-        NumAbsDomain join_over_types(const NumAbsDomain& inv, const Reg& reg,
-                                     const std::function<void(NumAbsDomain&, type_encoding_t)>& transition) const;
-        NumAbsDomain join_by_if_else(const NumAbsDomain& inv, const linear_constraint_t& condition,
-                                     const std::function<void(NumAbsDomain&)>& if_true,
-                                     const std::function<void(NumAbsDomain&)>& if_false) const;
+        [[nodiscard]] bool implies_type(const NumAbsDomain& inv, const linear_constraint_t& a,
+                                        const linear_constraint_t& b) const;
+
+        [[nodiscard]] NumAbsDomain
+        join_over_types(const NumAbsDomain& inv, const Reg& reg,
+                        const std::function<void(NumAbsDomain&, type_encoding_t)>& transition) const;
+        [[nodiscard]] NumAbsDomain join_by_if_else(const NumAbsDomain& inv, const linear_constraint_t& condition,
+                                                   const std::function<void(NumAbsDomain&)>& if_true,
+                                                   const std::function<void(NumAbsDomain&)>& if_false) const;
         void selectively_join_based_on_type(NumAbsDomain& dst, NumAbsDomain& src) const;
-        void add_extra_invariant(NumAbsDomain& dst,
-                                 std::map<crab::variable_t, crab::interval_t>& extra_invariants,
+        void add_extra_invariant(NumAbsDomain& dst, std::map<crab::variable_t, crab::interval_t>& extra_invariants,
                                  variable_t type_variable, type_encoding_t type, crab::data_kind_t kind,
                                  const NumAbsDomain& other) const;
 
@@ -248,4 +249,4 @@ class ebpf_domain_t final {
     std::string current_assertion;
 }; // end ebpf_domain_t
 
-}
+} // namespace crab

src/crab_utils/adapt_sgraph.hpp

@@ -22,7 +22,6 @@ class TreeSMap final {
     col map;
 
   public:
-    using elt_t = std::pair<key_t, val_t>;
     using elt_iter_t = col::const_iterator;
     [[nodiscard]] size_t size() const { return map.size(); }
 
@@ -142,7 +141,7 @@ class AdaptGraph final {
     }
 
     struct vert_const_iterator {
-        vert_id v;
+        vert_id v{};
         const std::vector<int>& is_free;
 
         vert_id operator*() const { return v; }
@@ -401,14 +400,14 @@ class AdaptGraph final {
 
     // Ick. This'll have another indirection on every operation.
     // We'll see what the performance costs are like.
-    std::vector<smap_t> _preds;
-    std::vector<smap_t> _succs;
-    std::vector<Weight> _ws;
+    std::vector<smap_t> _preds{};
+    std::vector<smap_t> _succs{};
+    std::vector<Weight> _ws{};
 
-    size_t edge_count;
+    size_t edge_count{};
 
-    std::vector<int> is_free;
-    std::vector<vert_id> free_id;
-    std::vector<size_t> free_widx;
+    std::vector<int> is_free{};
+    std::vector<vert_id> free_id{};
+    std::vector<size_t> free_widx{};
 };
 } // namespace crab

src/ebpf_vm_isa.hpp

@@ -57,9 +57,7 @@ enum {
     INST_OP_JA = (INST_CLS_JMP | 0x00),
     INST_OP_CALL = (INST_CLS_JMP | 0x80),
     INST_OP_EXIT = (INST_CLS_JMP | 0x90),
-};
 
-enum {
     INST_ALU_OP_ADD  = 0x00,
     INST_ALU_OP_SUB  = 0x10,
     INST_ALU_OP_MUL  = 0x20,
@@ -74,10 +72,8 @@ enum {
     INST_ALU_OP_MOV  = 0xb0,
     INST_ALU_OP_ARSH = 0xc0,
     INST_ALU_OP_END  = 0xd0,
-    INST_ALU_OP_MASK = 0xf0
-};
+    INST_ALU_OP_MASK = 0xf0,
 
-enum {
     R0_RETURN_VALUE = 0,
     R1_ARG = 1,
     R2_ARG = 2,