From cae2b258b82b42588695cba6744431da40e86ad1 Mon Sep 17 00:00:00 2001 From: Elazar Gershuni Date: Mon, 17 Jul 2023 19:13:48 +0300 Subject: [PATCH] address linter / compiler warnings Signed-off-by: Elazar Gershuni --- CMakeLists.txt | 4 +-- src/asm_files.cpp | 14 ++++------ src/asm_unmarshal.cpp | 14 ---------- src/assertions.cpp | 1 - src/config.cpp | 1 - src/crab/array_domain.cpp | 1 - src/crab/ebpf_domain.cpp | 48 ++++++++++++-------------------- src/crab/ebpf_domain.hpp | 49 +++++++++++++++++---------------- src/crab_utils/adapt_sgraph.hpp | 17 ++++++------ src/ebpf_vm_isa.hpp | 6 +--- src/spec_type_descriptors.hpp | 43 +++++++++++++++-------------- src/string_constraints.hpp | 2 +- 12 files changed, 83 insertions(+), 117 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index d7cf25631..93ef825ec 100644 --- a/CMakeLists.txt +++ b/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(${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) diff --git a/src/asm_files.cpp b/src/asm_files.cpp index 9bae2c1e7..b05928991 100644 --- a/src/asm_files.cpp +++ b/src/asm_files.cpp @@ -1,23 +1,21 @@ // Copyright (c) Prevail Verifier contributors. // SPDX-License-Identifier: MIT -#include #include #include +#include #include #include -#include -#include #include -#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 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 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]; } } diff --git a/src/asm_unmarshal.cpp b/src/asm_unmarshal.cpp index 3536136f1..4a9609d46 100644 --- a/src/asm_unmarshal.cpp +++ b/src/asm_unmarshal.cpp @@ -1,7 +1,6 @@ // Copyright (c) Prevail Verifier contributors. // SPDX-License-Identifier: MIT #include -#include // memcmp #include #include #include @@ -429,19 +428,6 @@ struct Unmarshaller { break; } } - /* - vector 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"); diff --git a/src/assertions.cpp b/src/assertions.cpp index 7a74218bb..e3c55ae9d 100644 --- a/src/assertions.cpp +++ b/src/assertions.cpp @@ -6,7 +6,6 @@ #include #include "asm_syntax.hpp" -#include "ebpf_vm_isa.hpp" #include "platform.hpp" #include "crab/cfg.hpp" diff --git a/src/config.cpp b/src/config.cpp index 342e4ebd3..3849162c5 100644 --- a/src/config.cpp +++ b/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, diff --git a/src/crab/array_domain.cpp b/src/crab/array_domain.cpp index 31a56668f..ec5be435d 100644 --- a/src/crab/array_domain.cpp +++ b/src/crab/array_domain.cpp @@ -2,7 +2,6 @@ // SPDX-License-Identifier: Apache-2.0 #include -#include #include #include #include diff --git a/src/crab/ebpf_domain.cpp b/src/crab/ebpf_domain.cpp index 157822d37..d49d23977 100644 --- a/src/crab/ebpf_domain.cpp +++ b/src/crab/ebpf_domain.cpp @@ -4,7 +4,6 @@ // This file is eBPF-specific, not derived from CRAB. #include -#include #include #include #include @@ -12,8 +11,6 @@ #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 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 sn = src_interval.singleton()) { uint64_t imm = sn->cast_to_uint64() & (bin.is64 ? 63 : 31); diff --git a/src/crab/ebpf_domain.hpp b/src/crab/ebpf_domain.hpp index 4b5c890c4..4e4aa3710 100644 --- a/src/crab/ebpf_domain.hpp +++ b/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 get_type_offset_variable(const Reg& reg, int type); - std::optional get_type_offset_variable(const Reg& reg, const NumAbsDomain& inv) const; - std::optional get_type_offset_variable(const Reg& reg) const; + [[nodiscard]] std::optional get_type_offset_variable(const Reg& reg, const NumAbsDomain& inv) const; + [[nodiscard]] std::optional get_type_offset_variable(const Reg& reg) const; void scratch_caller_saved_registers(); - std::optional get_map_type(const Reg& map_fd_reg) const; - std::optional 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 get_map_type(const Reg& map_fd_reg) const; + [[nodiscard]] std::optional 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 - 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& 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& opt_val_reg); template 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& transition) const; - NumAbsDomain join_by_if_else(const NumAbsDomain& inv, const linear_constraint_t& condition, - const std::function& if_true, - const std::function& 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& transition) const; + [[nodiscard]] NumAbsDomain join_by_if_else(const NumAbsDomain& inv, const linear_constraint_t& condition, + const std::function& if_true, + const std::function& if_false) const; void selectively_join_based_on_type(NumAbsDomain& dst, NumAbsDomain& src) const; - void add_extra_invariant(NumAbsDomain& dst, - std::map& extra_invariants, + void add_extra_invariant(NumAbsDomain& dst, std::map& 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 diff --git a/src/crab_utils/adapt_sgraph.hpp b/src/crab_utils/adapt_sgraph.hpp index 23741a770..c24ae935c 100644 --- a/src/crab_utils/adapt_sgraph.hpp +++ b/src/crab_utils/adapt_sgraph.hpp @@ -22,7 +22,6 @@ class TreeSMap final { col map; public: - using elt_t = std::pair; 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& 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 _preds; - std::vector _succs; - std::vector _ws; + std::vector _preds{}; + std::vector _succs{}; + std::vector _ws{}; - size_t edge_count; + size_t edge_count{}; - std::vector is_free; - std::vector free_id; - std::vector free_widx; + std::vector is_free{}; + std::vector free_id{}; + std::vector free_widx{}; }; } // namespace crab diff --git a/src/ebpf_vm_isa.hpp b/src/ebpf_vm_isa.hpp index c9716ec1c..0f1f0974c 100644 --- a/src/ebpf_vm_isa.hpp +++ b/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, diff --git a/src/spec_type_descriptors.hpp b/src/spec_type_descriptors.hpp index 437f0a02f..cad589fa7 100644 --- a/src/spec_type_descriptors.hpp +++ b/src/spec_type_descriptors.hpp @@ -32,13 +32,16 @@ struct EbpfMapDescriptor { unsigned int inner_map_fd; }; +constexpr unsigned int DEFAULT_MAP_FD = 0xffffffff; + struct EbpfProgramType { - std::string name; // For ease of display, not used by the verifier. - const ebpf_context_descriptor_t* context_descriptor {}; - uint64_t platform_specific_data {}; // E.g., integer program type. - std::vector section_prefixes; - bool is_privileged {}; + std::string name{}; // For ease of display, not used by the verifier. + const ebpf_context_descriptor_t* context_descriptor{}; + uint64_t platform_specific_data{}; // E.g., integer program type. + std::vector section_prefixes{}; + bool is_privileged{}; }; + void print_map_descriptors(const std::vector& descriptors, std::ostream& o); using EquivalenceKey = std::tuple< @@ -48,25 +51,25 @@ using EquivalenceKey = std::tuple< uint32_t /* max_entries */>; struct program_info { - const struct ebpf_platform_t* platform = nullptr; - std::vector map_descriptors; - EbpfProgramType type; - std::map cache; + const struct ebpf_platform_t* platform{}; + std::vector map_descriptors{}; + EbpfProgramType type{}; + std::map cache{}; }; -typedef struct _btf_line_info { - std::string file_name; - std::string source_line; - uint32_t line_number; - uint32_t column_number; -} btf_line_info_t; +struct btf_line_info_t { + std::string file_name{}; + std::string source_line{}; + uint32_t line_number{}; + uint32_t column_number{}; +}; struct raw_program { - std::string filename; - std::string section; - std::vector prog; - program_info info; - std::vector line_info; + std::string filename{}; + std::string section{}; + std::vector prog{}; + program_info info{}; + std::vector line_info{}; }; extern thread_local crab::lazy_allocator global_program_info; diff --git a/src/string_constraints.hpp b/src/string_constraints.hpp index ead071c34..278c8f414 100644 --- a/src/string_constraints.hpp +++ b/src/string_constraints.hpp @@ -26,7 +26,7 @@ enum type_encoding_t { }; struct string_invariant { - std::optional> maybe_inv; + std::optional> maybe_inv{}; string_invariant() = default;