From 71c3f8d154b1faa6ac8862e654871e6d24f39df6 Mon Sep 17 00:00:00 2001 From: Elazar Gershuni Date: Fri, 15 Nov 2024 16:21:46 +0200 Subject: [PATCH 1/2] no transform on check.cpp. reorganize check.cpp No reachability notes on assume-assert Signed-off-by: Elazar Gershuni --- src/asm_cfg.cpp | 8 +- src/asm_files.cpp | 64 +++---- src/asm_files.hpp | 5 + src/asm_unmarshal.cpp | 8 +- src/config.hpp | 5 +- src/crab/cfg.hpp | 21 +-- src/crab/ebpf_checker.cpp | 124 +++++++------- src/crab/ebpf_domain.hpp | 2 +- src/crab/ebpf_transformer.cpp | 2 +- src/crab/fwd_analyzer.cpp | 30 ++-- src/crab/fwd_analyzer.hpp | 7 +- src/crab_verifier.cpp | 305 +++++++++++++--------------------- src/crab_verifier.hpp | 23 +-- src/linux/linux_platform.cpp | 18 +- src/main/check.cpp | 12 +- src/main/run_yaml.cpp | 2 +- src/spec_type_descriptors.hpp | 16 +- src/test/ebpf_yaml.cpp | 32 +++- src/test/ebpf_yaml.hpp | 2 +- src/test/test_verify.cpp | 52 +++--- src/test/test_yaml.cpp | 2 +- test-data/jump.yaml | 59 +++---- test-data/loop.yaml | 18 +- test-data/shift.yaml | 196 ---------------------- test-data/unsigned.yaml | 136 +++++++-------- 25 files changed, 443 insertions(+), 706 deletions(-) diff --git a/src/asm_cfg.cpp b/src/asm_cfg.cpp index cd1ade2a1..9bc05face 100644 --- a/src/asm_cfg.cpp +++ b/src/asm_cfg.cpp @@ -87,7 +87,7 @@ static void add_cfg_nodes(cfg_t& cfg, const label_t& caller_label, const label_t macro_labels.erase(macro_label); if (stack_frame_prefix == macro_label.stack_frame_prefix) { - throw std::runtime_error{stack_frame_prefix + ": illegal recursion"}; + throw crab::InvalidControlFlow{stack_frame_prefix + ": illegal recursion"}; } // Clone the macro block into a new block with the new stack frame prefix. @@ -143,7 +143,7 @@ static void add_cfg_nodes(cfg_t& cfg, const label_t& caller_label, const label_t const label_t label(macro_label.from, macro_label.to, caller_label_str); if (const auto pins = std::get_if(&cfg.at(label).cmd)) { if (stack_frame_depth >= MAX_CALL_STACK_FRAMES) { - throw std::runtime_error{"too many call stack frames"}; + throw crab::InvalidControlFlow{"too many call stack frames"}; } add_cfg_nodes(cfg, label, pins->target); } @@ -163,7 +163,7 @@ static cfg_t instruction_seq_to_cfg(const InstructionSeq& insts, const bool must } if (insts.size() == 0) { - throw std::invalid_argument{"empty instruction sequence"}; + throw crab::InvalidControlFlow{"empty instruction sequence"}; } else { const auto& [label, inst, _0] = insts[0]; cfg.get_node(cfg.entry_label()) >> cfg.get_node(label); @@ -183,7 +183,7 @@ static cfg_t instruction_seq_to_cfg(const InstructionSeq& insts, const bool must fallthrough = std::get<0>(insts[i + 1]); } else { if (has_fall(inst) && must_have_exit) { - throw std::invalid_argument{"fallthrough in last instruction"}; + throw crab::InvalidControlFlow{"fallthrough in last instruction"}; } } if (const auto jmp = std::get_if(&inst)) { diff --git a/src/asm_files.cpp b/src/asm_files.cpp index 53039f741..594c2a613 100644 --- a/src/asm_files.cpp +++ b/src/asm_files.cpp @@ -24,7 +24,7 @@ template requires std::is_trivially_copyable_v static vector vector_of(const char* data, const ELFIO::Elf_Xword size) { if (size % sizeof(T) != 0 || size > std::numeric_limits::max() || !data) { - throw std::runtime_error("Invalid argument to vector_of"); + throw UnmarshalError("Invalid argument to vector_of"); } return {reinterpret_cast(data), reinterpret_cast(data + size)}; } @@ -111,10 +111,10 @@ static size_t parse_map_sections(const ebpf_verifier_options_t& options, const e if (map_count > 0) { map_record_size = s->get_size() / map_count; if (s->get_data() == nullptr || map_record_size == 0) { - throw std::runtime_error("bad maps section"); + throw UnmarshalError("bad maps section"); } if (s->get_size() % map_record_size != 0) { - throw std::runtime_error("bad maps section size"); + throw UnmarshalError("bad maps section size"); } platform->parse_maps_section(map_descriptors, s->get_data(), map_record_size, map_count, platform, options); } @@ -131,9 +131,9 @@ vector read_elf(const string& path, const string& desired_section, } struct stat st; if (stat(path.c_str(), &st)) { - throw std::runtime_error(string(strerror(errno)) + " opening " + path); + throw UnmarshalError(string(strerror(errno)) + " opening " + path); } - throw std::runtime_error("Can't process ELF file " + path); + throw UnmarshalError("Can't process ELF file " + path); } static std::tuple @@ -168,8 +168,8 @@ void relocate_map(ebpf_inst& inst, const std::string& symbol_name, const ELFIO::const_symbol_section_accessor& symbols) { // Only permit loading the address of the map. if ((inst.opcode & INST_CLS_MASK) != INST_CLS_LD) { - throw std::runtime_error("Illegal operation on symbol " + symbol_name + " at location " + - std::to_string(offset / sizeof(ebpf_inst))); + throw UnmarshalError("Illegal operation on symbol " + symbol_name + " at location " + + std::to_string(offset / sizeof(ebpf_inst))); } inst.src = 1; // magic number for LoadFd @@ -190,8 +190,8 @@ void relocate_map(ebpf_inst& inst, const std::string& symbol_name, } } if (reloc_value >= info.map_descriptors.size()) { - throw std::runtime_error("Bad reloc value (" + std::to_string(reloc_value) + "). " + - "Make sure to compile with -O2."); + throw UnmarshalError("Bad reloc value (" + std::to_string(reloc_value) + "). " + + "Make sure to compile with -O2."); } inst.imm = info.map_descriptors.at(reloc_value).original_fd; } @@ -213,8 +213,8 @@ static vector read_subprogram(const ELFIO::section& subprogram_sectio auto [subprogram_name, subprogram_size] = get_program_name_and_size(subprogram_section, subprogram_offset, symbols); if (subprogram_size == 0) { - throw std::runtime_error("Zero-size subprogram '" + subprogram_name + "' in section '" + - subprogram_section.get_name() + "'"); + throw UnmarshalError("Zero-size subprogram '" + subprogram_name + "' in section '" + + subprogram_section.get_name() + "'"); } if (subprogram_name == symbol_name) { // Append subprogram instructions to the main program. @@ -222,8 +222,8 @@ static vector read_subprogram(const ELFIO::section& subprogram_sectio } subprogram_offset += subprogram_size; } - throw std::runtime_error("Subprogram '" + symbol_name + "' not found in section '" + subprogram_section.get_name() + - "'"); + throw UnmarshalError("Subprogram '" + symbol_name + "' not found in section '" + subprogram_section.get_name() + + "'"); } static void append_subprograms(raw_program& prog, const vector& programs, @@ -254,8 +254,8 @@ static void append_subprograms(raw_program& prog, const vector& pro const int64_t target_offset = gsl::narrow_cast(subprogram_offsets[reloc.target_function_name]); const auto offset_diff = target_offset - gsl::narrow(reloc.source_offset) - 1; if (offset_diff < std::numeric_limits::min() || offset_diff > std::numeric_limits::max()) { - throw std::runtime_error("Offset difference out of int32_t range for instruction at source offset " + - std::to_string(reloc.source_offset)); + throw UnmarshalError("Offset difference out of int32_t range for instruction at source offset " + + std::to_string(reloc.source_offset)); } prog.prog[reloc.source_offset].imm = gsl::narrow_cast(offset_diff); } @@ -282,12 +282,12 @@ vector read_elf(std::istream& input_stream, const std::string& path const ebpf_verifier_options_t& options, const ebpf_platform_t* platform) { ELFIO::elfio reader; if (!reader.load(input_stream)) { - throw std::runtime_error("Can't process ELF file " + path); + throw UnmarshalError("Can't process ELF file " + path); } auto symbol_section = reader.sections[".symtab"]; if (!symbol_section) { - throw std::runtime_error("No symbol section found in ELF file " + path); + throw UnmarshalError("No symbol section found in ELF file " + path); } // Make sure the ELFIO library will be able to parse the symbol section correctly. @@ -295,7 +295,7 @@ vector read_elf(std::istream& input_stream, const std::string& path reader.get_class() == ELFIO::ELFCLASS32 ? sizeof(ELFIO::Elf32_Sym) : sizeof(ELFIO::Elf64_Sym); if (symbol_section->get_entry_size() != expected_entry_size) { - throw std::runtime_error("Invalid symbol section found in ELF file " + path); + throw UnmarshalError("Invalid symbol section found in ELF file " + path); } program_info info{platform}; @@ -324,7 +324,7 @@ vector read_elf(std::istream& input_stream, const std::string& path parse_map_sections(options, platform, reader, info.map_descriptors, map_section_indices, symbols); } else { if (!btf_data.has_value()) { - throw std::runtime_error("No BTF section found in ELF file " + path); + throw UnmarshalError("No BTF section found in ELF file " + path); } map_record_size_or_map_offsets = parse_map_section(*btf_data, info.map_descriptors); // Prevail requires: @@ -390,7 +390,7 @@ vector read_elf(std::istream& input_stream, const std::string& path if (prelocs) { if (!prelocs->get_data()) { - throw std::runtime_error("Malformed relocation data"); + throw UnmarshalError("Malformed relocation data"); } ELFIO::const_relocation_section_accessor reloc{reader, prelocs}; @@ -410,7 +410,7 @@ vector read_elf(std::istream& input_stream, const std::string& path } offset -= program_offset; if (offset / sizeof(ebpf_inst) >= prog.prog.size()) { - throw std::runtime_error("Invalid relocation data"); + throw UnmarshalError("Invalid relocation data"); } ebpf_inst& inst = prog.prog[offset / sizeof(ebpf_inst)]; @@ -437,7 +437,6 @@ vector read_elf(std::istream& input_stream, const std::string& path unresolved_symbols_errors.push_back(unresolved_symbol); } } - prog.line_info.resize(prog.prog.size()); res.push_back(prog); program_offset += program_size; } @@ -457,8 +456,8 @@ vector read_elf(std::istream& input_stream, const std::string& path for (const auto& unresolved_symbol : unresolved_symbols_errors) { std::cerr << unresolved_symbol << std::endl; } - throw std::runtime_error("There are relocations in section but no maps sections in file " + path + - "\nMake sure to inline all function calls."); + throw UnmarshalError("There are relocations in section but no maps sections in file " + path + + "\nMake sure to inline all function calls."); } auto btf_ext = reader.sections[".BTF.ext"]; @@ -469,10 +468,11 @@ vector read_elf(std::istream& input_stream, const std::string& path if (program.section_name == section && instruction_offset >= program.insn_off && instruction_offset < program.insn_off + program.prog.size() * sizeof(ebpf_inst)) { const size_t inst_index = (instruction_offset - program.insn_off) / sizeof(ebpf_inst); - if (inst_index >= program.line_info.size()) { - throw std::runtime_error("Invalid BTF data"); + if (inst_index >= program.prog.size()) { + throw UnmarshalError("Invalid BTF data"); } - program.line_info[inst_index] = {file_name, source, line_number, column_number}; + program.info.line_info.insert_or_assign( + inst_index, btf_line_info_t{file_name, source, line_number, column_number}); return; } } @@ -482,10 +482,10 @@ vector read_elf(std::istream& input_stream, const std::string& path // BTF doesn't include line info for every instruction, only on the first instruction per source line. for (auto& program : res) { - for (size_t i = 1; i < program.line_info.size(); i++) { + for (size_t i = 1; i < program.info.line_info.size(); i++) { // If the previous PC has line info, copy it. - if (program.line_info[i].line_number == 0 && program.line_info[i - 1].line_number != 0) { - program.line_info[i] = program.line_info[i - 1]; + if (program.info.line_info[i].line_number == 0 && program.info.line_info[i - 1].line_number != 0) { + program.info.line_info[i] = program.info.line_info[i - 1]; } } } @@ -493,9 +493,9 @@ vector read_elf(std::istream& input_stream, const std::string& path if (res.empty()) { if (desired_section.empty()) { - throw std::runtime_error("Can't find any non-empty TEXT sections in file " + path); + throw UnmarshalError("Can't find any non-empty TEXT sections in file " + path); } - throw std::runtime_error("Can't find section " + desired_section + " in file " + path); + throw UnmarshalError("Can't find section " + desired_section + " in file " + path); } return res; } diff --git a/src/asm_files.hpp b/src/asm_files.hpp index f8534d7ef..ceab045bd 100644 --- a/src/asm_files.hpp +++ b/src/asm_files.hpp @@ -9,6 +9,11 @@ #include "asm_syntax.hpp" #include "platform.hpp" +class UnmarshalError final : public std::runtime_error { + public: + explicit UnmarshalError(const std::string& what) : std::runtime_error(what) {} +}; + std::vector read_raw(std::string path, program_info info); std::vector read_elf(const std::string& path, const std::string& desired_section, const ebpf_verifier_options_t& options, const ebpf_platform_t* platform); diff --git a/src/asm_unmarshal.cpp b/src/asm_unmarshal.cpp index 094917238..aff20fbb9 100644 --- a/src/asm_unmarshal.cpp +++ b/src/asm_unmarshal.cpp @@ -696,7 +696,7 @@ struct Unmarshaller { } } - vector unmarshal(vector const& insts, vector const& line_info) { + vector unmarshal(vector const& insts) { vector prog; int exit_count = 0; if (insts.empty()) { @@ -773,8 +773,8 @@ struct Unmarshaller { std::optional current_line_info = {}; - if (pc < line_info.size()) { - current_line_info = line_info[pc]; + if (pc < info.line_info.size()) { + current_line_info = info.line_info.at(pc); } prog.emplace_back(label_t(gsl::narrow(pc)), new_ins, current_line_info); @@ -796,7 +796,7 @@ struct Unmarshaller { std::variant unmarshal(const raw_program& raw_prog, vector>& notes) { global_program_info = raw_prog.info; try { - return Unmarshaller{notes, raw_prog.info}.unmarshal(raw_prog.prog, raw_prog.line_info); + return Unmarshaller{notes, raw_prog.info}.unmarshal(raw_prog.prog); } catch (InvalidInstruction& arg) { std::ostringstream ss; ss << arg.pc << ": " << arg.what() << "\n"; diff --git a/src/config.hpp b/src/config.hpp index 09d5d919e..609e1f96b 100644 --- a/src/config.hpp +++ b/src/config.hpp @@ -43,9 +43,8 @@ struct ebpf_verifier_options_t { }; struct ebpf_verifier_stats_t { - int total_unreachable; - int total_warnings; - int max_loop_count; + int total_warnings{}; + int max_loop_count{}; }; extern thread_local ebpf_verifier_options_t thread_local_options; diff --git a/src/crab/cfg.hpp b/src/crab/cfg.hpp index 678d1312e..3b30adc74 100644 --- a/src/crab/cfg.hpp +++ b/src/crab/cfg.hpp @@ -22,6 +22,11 @@ namespace crab { +class InvalidControlFlow final : public std::runtime_error { + public: + explicit InvalidControlFlow(const std::string& what) : std::runtime_error(what) {} +}; + class cfg_t; // Node type for the CFG @@ -322,7 +327,7 @@ class cfg_t final { [[nodiscard]] std::vector sorted_labels() const { std::vector labels = this->labels(); - std::sort(labels.begin(), labels.end()); + std::ranges::sort(labels); return labels; } @@ -351,20 +356,6 @@ class cfg_t final { const auto rng = prev_nodes(b); return std::distance(rng.begin(), rng.end()) == 1; } - - // mark reachable blocks from curId - template - void mark_alive_blocks(label_t curId, AnyCfg& cfg_t, visited_t& visited) { - if (visited.contains(curId)) { - return; - } - visited.insert(curId); - for (const auto& child : cfg_t.next_nodes(curId)) { - mark_alive_blocks(child, cfg_t, visited); - } - } - - void remove_unreachable_blocks(); }; class basic_block_t final { diff --git a/src/crab/ebpf_checker.cpp b/src/crab/ebpf_checker.cpp index 4d734780d..95333be67 100644 --- a/src/crab/ebpf_checker.cpp +++ b/src/crab/ebpf_checker.cpp @@ -38,63 +38,50 @@ static bool check_require(const NumAbsDomain& inv, const linear_constraint_t& cs return false; } +using OnRequire = std::function; + class ebpf_checker final { public: - explicit ebpf_checker(ebpf_domain_t& dom, const Assertion& assertion, const std::optional& label = {}) - : assertion{assertion}, label{label}, dom(dom), m_inv(dom.m_inv), stack(dom.stack), type_inv(dom.type_inv) {} + explicit ebpf_checker(ebpf_domain_t& dom, const Assertion& assertion, const OnRequire& on_require) + : assertion{assertion}, on_require{on_require}, dom(dom), m_inv(dom.m_inv), stack(dom.stack), + type_inv(dom.type_inv) {} void visit(const Assertion& assertion) { std::visit(*this, assertion); } - void operator()(const Addable&); - void operator()(const BoundedLoopCount&); - void operator()(const Comparable&); - void operator()(const FuncConstraint&); - void operator()(const ValidDivisor&); - void operator()(const TypeConstraint&); - void operator()(const ValidAccess&); - void operator()(const ValidCall&); - void operator()(const ValidMapKeyValue&); - void operator()(const ValidSize&); - void operator()(const ValidStore&); - void operator()(const ZeroCtxOffset&); + void operator()(const Addable&) const; + void operator()(const BoundedLoopCount&) const; + void operator()(const Comparable&) const; + void operator()(const FuncConstraint&) const; + void operator()(const ValidDivisor&) const; + void operator()(const TypeConstraint&) const; + void operator()(const ValidAccess&) const; + void operator()(const ValidCall&) const; + void operator()(const ValidMapKeyValue&) const; + void operator()(const ValidSize&) const; + void operator()(const ValidStore&) const; + void operator()(const ZeroCtxOffset&) const; private: std::string create_warning(const std::string& s) const { return s + " (" + to_string(assertion) + ")"; } - void require(NumAbsDomain& inv, const linear_constraint_t& cst, const std::string& msg) { - if (label && !check_require(inv, cst)) { - warnings.push_back(create_warning(msg)); - } - - if (thread_local_options.assume_assertions) { - // avoid redundant errors - inv += cst; - } + void require(NumAbsDomain& inv, const linear_constraint_t& cst, const std::string& msg) const { + on_require(inv, cst, create_warning(msg)); } - void require(const std::string& msg) { - if (label) { - warnings.push_back(create_warning(msg)); - } - if (thread_local_options.assume_assertions) { - m_inv.set_to_bottom(); - } - } + void require(const std::string& msg) const { require(m_inv, linear_constraint_t::false_const(), msg); } // memory check / load / store - void check_access_stack(NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub); - void check_access_context(NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub); + void check_access_stack(NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub) const; + void check_access_context(NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub) const; void check_access_packet(NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub, - std::optional packet_size); + std::optional packet_size) const; void check_access_shared(NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub, - variable_t shared_region_size); + variable_t shared_region_size) const; public: - std::vector warnings; - private: - const Assertion& assertion; - const std::optional label; + const Assertion assertion; + const OnRequire on_require; ebpf_domain_t& dom; // shorthands: @@ -107,16 +94,28 @@ void ebpf_domain_assume(ebpf_domain_t& dom, const Assertion& assertion) { if (dom.is_bottom()) { return; } - ebpf_checker{dom, assertion}.visit(assertion); + ebpf_checker{dom, assertion, + [](NumAbsDomain& inv, const linear_constraint_t& cst, const std::string&) { + // avoid redundant errors + inv += cst; + }} + .visit(assertion); } -std::vector ebpf_domain_check(ebpf_domain_t& dom, const label_t& label, const Assertion& assertion) { +std::vector ebpf_domain_check(const ebpf_domain_t& dom, const Assertion& assertion) { if (dom.is_bottom()) { return {}; } - ebpf_checker checker{dom, assertion, label}; + ebpf_domain_t copy = dom; + std::vector warnings; + ebpf_checker checker{copy, assertion, + [&warnings](const NumAbsDomain& inv, const linear_constraint_t& cst, const std::string& msg) { + if (!check_require(inv, cst)) { + warnings.push_back(msg); + } + }}; checker.visit(assertion); - return std::move(checker.warnings); + return warnings; } static linear_constraint_t type_is_pointer(const reg_pack_t& r) { @@ -136,7 +135,8 @@ static linear_constraint_t type_is_not_stack(const reg_pack_t& r) { return r.type != T_STACK; } -void ebpf_checker::check_access_stack(NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub) { +void ebpf_checker::check_access_stack(NumAbsDomain& inv, const linear_expression_t& lb, + const linear_expression_t& ub) const { using namespace crab::dsl_syntax; const variable_t r10_stack_offset = reg_pack(R10_STACK_POINTER).stack_offset; const auto interval = inv.eval_interval(r10_stack_offset); @@ -149,7 +149,7 @@ void ebpf_checker::check_access_stack(NumAbsDomain& inv, const linear_expression } void ebpf_checker::check_access_context(NumAbsDomain& inv, const linear_expression_t& lb, - const linear_expression_t& ub) { + const linear_expression_t& ub) const { using namespace crab::dsl_syntax; require(inv, lb >= 0, "Lower bound must be at least 0"); require(inv, ub <= global_program_info->type.context_descriptor->size, @@ -158,7 +158,7 @@ void ebpf_checker::check_access_context(NumAbsDomain& inv, const linear_expressi } void ebpf_checker::check_access_packet(NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub, - const std::optional packet_size) { + const std::optional packet_size) const { using namespace crab::dsl_syntax; require(inv, lb >= variable_t::meta_offset(), "Lower bound must be at least meta_offset"); if (packet_size) { @@ -170,13 +170,13 @@ void ebpf_checker::check_access_packet(NumAbsDomain& inv, const linear_expressio } void ebpf_checker::check_access_shared(NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub, - const variable_t shared_region_size) { + const variable_t shared_region_size) const { using namespace crab::dsl_syntax; require(inv, lb >= 0, "Lower bound must be at least 0"); require(inv, ub <= shared_region_size, std::string("Upper bound must be at most ") + shared_region_size.name()); } -void ebpf_checker::operator()(const Comparable& s) { +void ebpf_checker::operator()(const Comparable& s) const { using namespace crab::dsl_syntax; if (type_inv.same_type(m_inv, s.r1, s.r2)) { // Same type. If both are numbers, that's okay. Otherwise: @@ -197,13 +197,13 @@ void ebpf_checker::operator()(const Comparable& s) { }; } -void ebpf_checker::operator()(const Addable& s) { +void ebpf_checker::operator()(const Addable& s) const { if (!type_inv.implies_type(m_inv, type_is_pointer(reg_pack(s.ptr)), type_is_number(s.num))) { require("Only numbers can be added to pointers"); } } -void ebpf_checker::operator()(const ValidDivisor& s) { +void ebpf_checker::operator()(const ValidDivisor& s) const { using namespace crab::dsl_syntax; const auto reg = reg_pack(s.reg); if (!type_inv.implies_type(m_inv, type_is_pointer(reg), type_is_number(s.reg))) { @@ -215,19 +215,19 @@ void ebpf_checker::operator()(const ValidDivisor& s) { } } -void ebpf_checker::operator()(const ValidStore& s) { +void ebpf_checker::operator()(const ValidStore& s) const { if (!type_inv.implies_type(m_inv, type_is_not_stack(reg_pack(s.mem)), type_is_number(s.val))) { require("Only numbers can be stored to externally-visible regions"); } } -void ebpf_checker::operator()(const TypeConstraint& s) { +void ebpf_checker::operator()(const TypeConstraint& s) const { if (!type_inv.is_in_group(m_inv, s.reg, s.types)) { require("Invalid type"); } } -void ebpf_checker::operator()(const BoundedLoopCount& s) { +void ebpf_checker::operator()(const BoundedLoopCount& s) const { // Enforces an upper bound on loop iterations by checking that the loop counter // does not exceed the specified limit using namespace crab::dsl_syntax; @@ -235,7 +235,7 @@ void ebpf_checker::operator()(const BoundedLoopCount& s) { require(m_inv, counter <= s.limit, "Loop counter is too large"); } -void ebpf_checker::operator()(const FuncConstraint& s) { +void ebpf_checker::operator()(const FuncConstraint& s) const { // Look up the helper function id. const reg_pack_t& reg = reg_pack(s.reg); const auto src_interval = m_inv.eval_interval(reg.svalue); @@ -250,11 +250,7 @@ void ebpf_checker::operator()(const FuncConstraint& s) { const Call call = make_call(imm, *global_program_info->platform); for (const Assertion& sub_assertion : get_assertions(call, *global_program_info, {})) { // TODO: create explicit sub assertions elsewhere - ebpf_checker sub_checker{dom, sub_assertion, label}; - sub_checker.visit(sub_assertion); - for (const auto& warning : sub_checker.warnings) { - warnings.push_back(warning); - } + ebpf_checker{dom, sub_assertion, on_require}.visit(sub_assertion); } return; } @@ -262,13 +258,13 @@ void ebpf_checker::operator()(const FuncConstraint& s) { require("callx helper function id is not a valid singleton"); } -void ebpf_checker::operator()(const ValidSize& s) { +void ebpf_checker::operator()(const ValidSize& s) const { using namespace crab::dsl_syntax; const auto r = reg_pack(s.reg); require(m_inv, s.can_be_zero ? r.svalue >= 0 : r.svalue > 0, "Invalid size"); } -void ebpf_checker::operator()(const ValidCall& s) { +void ebpf_checker::operator()(const ValidCall& s) const { if (!s.stack_frame_prefix.empty()) { const EbpfHelperPrototype proto = global_program_info->platform->get_helper_prototype(s.func); if (proto.return_type == EBPF_RETURN_TYPE_INTEGER_OR_NO_RETURN_IF_SUCCEED) { @@ -278,7 +274,7 @@ void ebpf_checker::operator()(const ValidCall& s) { } } -void ebpf_checker::operator()(const ValidMapKeyValue& s) { +void ebpf_checker::operator()(const ValidMapKeyValue& s) const { using namespace crab::dsl_syntax; const auto fd_type = dom.get_map_type(s.map_fd_reg); @@ -360,7 +356,7 @@ static std::tuple lb_ub_access_pair(co return {lb, ub}; } -void ebpf_checker::operator()(const ValidAccess& s) { +void ebpf_checker::operator()(const ValidAccess& s) const { using namespace crab::dsl_syntax; const bool is_comparison_check = s.width == Value{Imm{0}}; @@ -435,7 +431,7 @@ void ebpf_checker::operator()(const ValidAccess& s) { }); } -void ebpf_checker::operator()(const ZeroCtxOffset& s) { +void ebpf_checker::operator()(const ZeroCtxOffset& s) const { using namespace crab::dsl_syntax; const auto reg = reg_pack(s.reg); require(m_inv, reg.ctx_offset == 0, "Nonzero context offset"); diff --git a/src/crab/ebpf_domain.hpp b/src/crab/ebpf_domain.hpp index 001dcfaf3..1fe34ba15 100644 --- a/src/crab/ebpf_domain.hpp +++ b/src/crab/ebpf_domain.hpp @@ -28,7 +28,7 @@ class ebpf_domain_t; void ebpf_domain_transform(ebpf_domain_t& inv, const Instruction& ins); void ebpf_domain_assume(ebpf_domain_t& dom, const Assertion& assertion); -std::vector ebpf_domain_check(ebpf_domain_t& dom, const label_t& label, const Assertion& assertion); +std::vector ebpf_domain_check(const ebpf_domain_t& dom, const Assertion& assertion); // TODO: make this an explicit instruction void ebpf_domain_initialize_loop_counter(ebpf_domain_t& dom, const label_t& label); diff --git a/src/crab/ebpf_transformer.cpp b/src/crab/ebpf_transformer.cpp index c809990d9..935ae207d 100644 --- a/src/crab/ebpf_transformer.cpp +++ b/src/crab/ebpf_transformer.cpp @@ -141,7 +141,7 @@ void ebpf_domain_transform(ebpf_domain_t& inv, const Instruction& ins) { // Fail. raise an exception to stop the analysis. std::stringstream msg; msg << "Bug! pre-invariant:\n" - << inv.to_set() << "\n followed by instruction: " << ins << "\n" + << inv << "\n followed by instruction: " << ins << "\n" << "leads to bottom"; throw std::logic_error(msg.str()); } diff --git a/src/crab/fwd_analyzer.cpp b/src/crab/fwd_analyzer.cpp index f77e8e90a..27cb31b2f 100644 --- a/src/crab/fwd_analyzer.cpp +++ b/src/crab/fwd_analyzer.cpp @@ -48,11 +48,9 @@ class member_component_visitor final { }; class interleaved_fwd_fixpoint_iterator_t final { - using iterator = invariant_table_t::iterator; - const cfg_t& _cfg; wto_t _wto; - invariant_table_t _pre, _post; + invariant_map_pair _inv; /// number of narrowing iterations. If the narrowing operator is /// indeed a narrowing operator this parameter is not @@ -65,7 +63,7 @@ class interleaved_fwd_fixpoint_iterator_t final { bool _skip{true}; private: - void set_pre(const label_t& label, const ebpf_domain_t& v) { _pre[label] = v; } + void set_pre(const label_t& label, const ebpf_domain_t& v) { _inv.pre[label] = v; } void transform_to_post(const label_t& label, ebpf_domain_t pre) { const GuardedInstruction& ins = _cfg.at(label); @@ -78,7 +76,7 @@ class interleaved_fwd_fixpoint_iterator_t final { } ebpf_domain_transform(pre, ins.cmd); - _post[label] = std::move(pre); + _inv.post[label] = std::move(pre); } [[nodiscard]] @@ -102,6 +100,9 @@ class interleaved_fwd_fixpoint_iterator_t final { } ebpf_domain_t join_all_prevs(const label_t& node) { + if (node == _cfg.entry_label()) { + return get_pre(node); + } ebpf_domain_t res = ebpf_domain_t::bottom(); for (const label_t& prev : _cfg.prev_nodes(node)) { res |= get_post(prev); @@ -112,24 +113,23 @@ class interleaved_fwd_fixpoint_iterator_t final { public: explicit interleaved_fwd_fixpoint_iterator_t(const cfg_t& cfg) : _cfg(cfg), _wto(cfg) { for (const auto& label : _cfg.labels()) { - _pre.emplace(label, ebpf_domain_t::bottom()); - _post.emplace(label, ebpf_domain_t::bottom()); + _inv.pre.emplace(label, ebpf_domain_t::bottom()); + _inv.post.emplace(label, ebpf_domain_t::bottom()); } } - ebpf_domain_t get_pre(const label_t& node) { return _pre.at(node); } + ebpf_domain_t get_pre(const label_t& node) { return _inv.pre.at(node); } - ebpf_domain_t get_post(const label_t& node) { return _post.at(node); } + ebpf_domain_t get_post(const label_t& node) { return _inv.post.at(node); } void operator()(const label_t& node); void operator()(const std::shared_ptr& cycle); - friend std::pair run_forward_analyzer(const cfg_t& cfg, - ebpf_domain_t entry_inv); + friend invariant_map_pair run_forward_analyzer(const cfg_t& cfg, ebpf_domain_t entry_inv); }; -std::pair run_forward_analyzer(const cfg_t& cfg, ebpf_domain_t entry_inv) { +invariant_map_pair run_forward_analyzer(const cfg_t& cfg, ebpf_domain_t entry_inv) { // Go over the CFG in weak topological order (accounting for loops). interleaved_fwd_fixpoint_iterator_t analyzer(cfg); if (thread_local_options.cfg_opts.check_for_termination) { @@ -144,7 +144,7 @@ std::pair run_forward_analyzer(const cfg_t for (const auto& component : analyzer._wto) { std::visit(analyzer, component); } - return std::make_pair(analyzer._pre, analyzer._post); + return std::move(analyzer._inv); } void interleaved_fwd_fixpoint_iterator_t::operator()(const label_t& node) { @@ -156,10 +156,10 @@ void interleaved_fwd_fixpoint_iterator_t::operator()(const label_t& node) { return; } - const ebpf_domain_t pre = node == _cfg.entry_label() ? get_pre(node) : join_all_prevs(node); + ebpf_domain_t pre = join_all_prevs(node); set_pre(node, pre); - transform_to_post(node, pre); + transform_to_post(node, std::move(pre)); } void interleaved_fwd_fixpoint_iterator_t::operator()(const std::shared_ptr& cycle) { diff --git a/src/crab/fwd_analyzer.hpp b/src/crab/fwd_analyzer.hpp index 3445e92fe..db916a52f 100644 --- a/src/crab/fwd_analyzer.hpp +++ b/src/crab/fwd_analyzer.hpp @@ -10,7 +10,10 @@ namespace crab { using invariant_table_t = std::map; - -std::pair run_forward_analyzer(const cfg_t& cfg, ebpf_domain_t entry_inv); +struct invariant_map_pair { + invariant_table_t pre; + invariant_table_t post; +}; +invariant_map_pair run_forward_analyzer(const cfg_t& cfg, ebpf_domain_t entry_inv); } // namespace crab diff --git a/src/crab_verifier.cpp b/src/crab_verifier.cpp index 3a42f55f6..b07039774 100644 --- a/src/crab_verifier.cpp +++ b/src/crab_verifier.cpp @@ -10,237 +10,168 @@ #include #include -#include - +#include "asm_syntax.hpp" #include "crab/ebpf_domain.hpp" #include "crab/fwd_analyzer.hpp" #include "crab_utils/lazy_allocator.hpp" - -#include "asm_syntax.hpp" #include "crab_verifier.hpp" #include "string_constraints.hpp" +#include +#include + using crab::ebpf_domain_t; using std::string; thread_local crab::lazy_allocator global_program_info; thread_local ebpf_verifier_options_t thread_local_options; +void ebpf_verifier_clear_before_analysis(); -// Toy database to store invariants. -struct checks_db final { - std::map> m_db{}; - int total_warnings{}; - int total_unreachable{}; - crab::extended_number max_loop_count{crab::number_t{0}}; - - void add(const label_t& label, const std::string& msg) { m_db[label].emplace_back(msg); } - - void add_warning(const label_t& label, const std::string& msg) { - add(label, msg); - total_warnings++; - } - - void add_unreachable(const label_t& label, const std::string& msg) { - add(label, msg); - total_unreachable++; - } - - [[nodiscard]] - int get_max_loop_count() const { - const auto m = this->max_loop_count.number(); - if (m && m->fits()) { - return m->cast_to(); - } - return std::numeric_limits::max(); - } - checks_db() = default; +struct Messages { + std::map> warnings; + std::map> info; }; -static checks_db generate_report(const cfg_t& cfg, const crab::invariant_table_t& pre_invariants, - const crab::invariant_table_t& post_invariants) { - checks_db m_db; - for (const label_t& label : cfg.sorted_labels()) { - ebpf_domain_t from_inv{pre_invariants.at(label)}; - const bool pre_bot = from_inv.is_bottom(); - - const GuardedInstruction& instruction = cfg.at(label); - for (const Assertion& assertion : instruction.preconditions) { - for (const auto& warning : ebpf_domain_check(from_inv, label, assertion)) { - m_db.add_warning(label, warning); - } - } - ebpf_domain_transform(from_inv, instruction.cmd); - - if (!pre_bot && from_inv.is_bottom()) { - m_db.add_unreachable(label, std::string("Code is unreachable after ") + to_string(label)); - } - } - +static int maximum_loop_count(const crab::invariant_table_t& post_invariants) { + crab::extended_number max_loop_count{0}; if (thread_local_options.cfg_opts.check_for_termination) { // Gather the upper bound of loop counts from post-invariants. - for (const auto& [label, inv] : post_invariants) { - if (inv.is_bottom()) { - continue; - } - m_db.max_loop_count = std::max(m_db.max_loop_count, inv.get_loop_count_upper_bound()); + for (const auto& inv : std::views::values(post_invariants)) { + max_loop_count = std::max(max_loop_count, inv.get_loop_count_upper_bound()); } } - return m_db; -} - -static auto get_line_info(const InstructionSeq& insts) { - std::map label_to_line_info; - for (const auto& [label, inst, line_info] : insts) { - if (line_info.has_value()) { - label_to_line_info.emplace(label.from, line_info.value()); - } + const auto m = max_loop_count.number(); + if (m && m->fits()) { + return m->cast_to(); } - return label_to_line_info; + return std::numeric_limits::max(); } -static void print_report(std::ostream& os, const checks_db& db, const InstructionSeq& prog, - const bool print_line_info) { - auto label_to_line_info = get_line_info(prog); - os << "\n"; - for (const auto& [label, messages] : db.m_db) { - for (const auto& msg : messages) { - if (print_line_info) { - auto line_info = label_to_line_info.find(label.from); - if (line_info != label_to_line_info.end()) { - os << line_info->second; - } - } - os << label << ": " << msg << "\n"; +static Messages check_assertions_and_reachability(const cfg_t& cfg, const crab::invariant_map_pair& invariants) { + Messages messages; + for (const auto& [label, pre_inv] : invariants.pre) { + if (pre_inv.is_bottom()) { + continue; } - } - os << "\n"; -} - -static checks_db get_analysis_report(std::ostream& s, const cfg_t& cfg, const crab::invariant_table_t& pre_invariants, - const crab::invariant_table_t& post_invariants, - const std::optional& prog = std::nullopt) { - // Analyze the control-flow graph. - checks_db db = generate_report(cfg, pre_invariants, post_invariants); - if (thread_local_options.print_invariants) { - std::optional> line_info_map = std::nullopt; - if (prog.has_value()) { - line_info_map = get_line_info(*prog); + const auto ins = cfg.at(label); + for (const Assertion& assertion : ins.preconditions) { + const auto warnings = ebpf_domain_check(pre_inv, assertion); + for (const auto& msg : warnings) { + messages.warnings[label].emplace_back(msg); + } } - std::string previous_source_line = ""; - for (const label_t& label : cfg.sorted_labels()) { - if (line_info_map.has_value()) { - auto line_info = line_info_map->find(label.from); - // Print line info only once. - if (line_info != line_info_map->end() && line_info->second.source_line != previous_source_line) { - s << "\n" << line_info->second << "\n"; - previous_source_line = line_info->second.source_line; - } + if (std::holds_alternative(ins.cmd)) { + if (invariants.post.at(label).is_bottom()) { + const auto s = to_string(std::get(ins.cmd)); + messages.info[label].emplace_back("Code becomes unreachable (" + s + ")"); } - s << "\nPre-invariant : " << pre_invariants.at(label) << "\n"; - s << cfg.get_node(label); - s << "\nPost-invariant: " << post_invariants.at(label) << "\n"; } } - return db; + return messages; } -static checks_db get_ebpf_report(std::ostream& s, const cfg_t& cfg, program_info info, - const ebpf_verifier_options_t& options, - const std::optional& prog = std::nullopt) { - global_program_info = std::move(info); - crab::domains::clear_global_state(); - crab::variable_t::clear_thread_local_state(); - thread_local_options = options; - - try { - // Get dictionaries of pre-invariants and post-invariants for each basic block. - ebpf_domain_t entry_dom = ebpf_domain_t::setup_entry(true); - auto [pre_invariants, post_invariants] = run_forward_analyzer(cfg, std::move(entry_dom)); - return get_analysis_report(s, cfg, pre_invariants, post_invariants, prog); - } catch (std::runtime_error& e) { - // Convert verifier runtime_error exceptions to failure. - checks_db db; - db.add_warning(label_t::exit, e.what()); - return db; +static int count_warnings(const Messages& messages) { + int count = 0; + for (const auto& msgs : std::views::values(messages.warnings)) { + count += msgs.size(); } + return count; } -/// Returned value is true if the program passes verification. -bool run_ebpf_analysis(std::ostream& s, const cfg_t& cfg, const program_info& info, - const ebpf_verifier_options_t& options, ebpf_verifier_stats_t* stats) { - const checks_db report = get_ebpf_report(s, cfg, info, options); - if (stats) { - stats->total_unreachable = report.total_unreachable; - stats->total_warnings = report.total_warnings; - stats->max_loop_count = report.get_max_loop_count(); +struct LineInfoPrinter { + std::ostream& os; + std::string previous_source_line; + + void print_line_info(const label_t& label) { + if (thread_local_options.print_line_info) { + const auto& line_info_map = global_program_info.get().line_info; + const auto& line_info = line_info_map.find(label.from); + // Print line info only once. + if (line_info != line_info_map.end() && line_info->second.source_line != previous_source_line) { + os << "\n" << line_info->second << "\n"; + previous_source_line = line_info->second.source_line; + } + } } - return report.total_warnings == 0; -} +}; -static string_invariant_map to_string_invariant_map(crab::invariant_table_t& inv_table) { - string_invariant_map res; - for (const auto& [label, inv] : inv_table) { - res.insert_or_assign(label, inv.to_set()); +ebpf_verifier_stats_t analyze_and_report(const analyze_params_t& params) { + if (!params.prog && !params.cfg) { + throw std::invalid_argument("Either prog or cfg must be provided"); } - return res; -} - -std::tuple ebpf_analyze_program_for_test(std::ostream& os, const InstructionSeq& prog, - const string_invariant& entry_invariant, - const program_info& info, - const ebpf_verifier_options_t& options) { - crab::domains::clear_global_state(); - crab::variable_t::clear_thread_local_state(); + ebpf_verifier_clear_before_analysis(); - thread_local_options = options; - global_program_info = info; - assert(!entry_invariant.is_bottom()); - ebpf_domain_t entry_inv = ebpf_domain_t::from_constraints(entry_invariant.value(), options.setup_constraints); - if (entry_inv.is_bottom()) { - throw std::runtime_error("Entry invariant is inconsistent"); + if (params.info) { + global_program_info = *params.info; } - try { - const cfg_t cfg = prepare_cfg(prog, info, options.cfg_opts); - auto [pre_invariants, post_invariants] = run_forward_analyzer(cfg, std::move(entry_inv)); - const checks_db report = get_analysis_report(std::cerr, cfg, pre_invariants, post_invariants); - print_report(os, report, prog, false); - - auto pre_invariant_map = to_string_invariant_map(pre_invariants); - - return {pre_invariant_map.at(label_t::exit), (report.total_warnings == 0)}; - } catch (std::runtime_error& e) { - os << e.what(); - return {string_invariant::top(), false}; + if (params.options) { + thread_local_options = *params.options; } -} + std::ostream& os = params.os ? *params.os : std::cout; + try { + cfg_t cfg = params.cfg ? std::move(*params.cfg) + : prepare_cfg(*params.prog, global_program_info.get(), thread_local_options.cfg_opts); + ebpf_domain_t entry_invariant = params.entry_invariant + ? ebpf_domain_t::from_constraints(params.entry_invariant->value(), + thread_local_options.setup_constraints) + : ebpf_domain_t::setup_entry(thread_local_options.setup_constraints); + + const auto invariants = run_forward_analyzer(cfg, std::move(entry_invariant)); + + if (thread_local_options.print_invariants) { + LineInfoPrinter printer{os}; + for (const label_t& label : cfg.sorted_labels()) { + printer.print_line_info(label); + os << "\nPre-invariant : " << invariants.pre.at(label) << "\n"; + os << cfg.get_node(label); + os << "\nPost-invariant: " << invariants.post.at(label) << "\n"; + } + } -/// Returned value is true if the program passes verification. -bool ebpf_verify_program(std::ostream& os, const InstructionSeq& prog, const program_info& info, - const ebpf_verifier_options_t& options, ebpf_verifier_stats_t* stats) { - // Convert the instruction sequence to a control-flow graph - // in a "passive", non-deterministic form. - const cfg_t cfg = prepare_cfg(prog, info, options.cfg_opts); + if (params.out_invariants) { + string_invariant_map invariant_map; + for (const auto& label : std::ranges::views::keys(*params.out_invariants)) { + invariant_map.insert_or_assign(label, invariants.post.at(label).to_set()); + } + *params.out_invariants = std::move(invariant_map); + } - std::optional prog_opt = std::nullopt; - if (options.print_failures) { - prog_opt = prog; - } + const Messages messages = check_assertions_and_reachability(cfg, invariants); - try { - const checks_db report = get_ebpf_report(os, cfg, info, options, prog_opt); - if (options.print_failures) { - print_report(os, report, prog, options.print_line_info); - } - if (stats) { - stats->total_unreachable = report.total_unreachable; - stats->total_warnings = report.total_warnings; - stats->max_loop_count = report.get_max_loop_count(); + if (thread_local_options.print_failures) { + os << "\n"; + LineInfoPrinter printer{os}; + for (const auto& [label, warnings] : messages.warnings) { + for (const auto& msg : warnings) { + printer.print_line_info(label); + os << label << ": " << msg << "\n"; + } + } + for (const auto& [label, notes] : messages.info) { + for (const auto& msg : notes) { + os << label << ": " << msg << "\n"; + } + } + os << "\n"; } - return report.total_warnings == 0; + + return ebpf_verifier_stats_t{ + .total_warnings = count_warnings(std::move(messages)), + .max_loop_count = maximum_loop_count(invariants.post), + }; + } catch (crab::InvalidControlFlow& e) { + os << e.what(); + } catch (UnmarshalError& e) { + os << e.what(); } catch (std::logic_error& e) { std::cerr << e.what(); - return false; } + return ebpf_verifier_stats_t{.total_warnings = 1}; +} + +void ebpf_verifier_clear_before_analysis() { + crab::domains::clear_global_state(); + crab::variable_t::clear_thread_local_state(); } void ebpf_verifier_clear_thread_local_state() { diff --git a/src/crab_verifier.hpp b/src/crab_verifier.hpp index 1da1d5e22..b851be822 100644 --- a/src/crab_verifier.hpp +++ b/src/crab_verifier.hpp @@ -7,18 +7,21 @@ #include "spec_type_descriptors.hpp" #include "string_constraints.hpp" -bool run_ebpf_analysis(std::ostream& s, const cfg_t& cfg, const program_info& info, - const ebpf_verifier_options_t& options, ebpf_verifier_stats_t* stats); - -bool ebpf_verify_program(std::ostream& os, const InstructionSeq& prog, const program_info& info, - const ebpf_verifier_options_t& options, ebpf_verifier_stats_t* stats); - using string_invariant_map = std::map; -std::tuple ebpf_analyze_program_for_test(std::ostream& os, const InstructionSeq& prog, - const string_invariant& entry_invariant, - const program_info& info, - const ebpf_verifier_options_t& options); +struct analyze_params_t { + std::ostream* os{&std::cout}; + const InstructionSeq* prog{}; + // if exists, it will be moved from + std::unique_ptr cfg{}; + // invariants will be added to labels that appear as keys in out_invariants + const string_invariant* entry_invariant{}; + string_invariant_map* out_invariants{}; + const program_info* info{}; + ebpf_verifier_options_t* options{}; +}; + +ebpf_verifier_stats_t analyze_and_report(const analyze_params_t& params = {}); int create_map_crab(const EbpfMapType& map_type, uint32_t key_size, uint32_t value_size, uint32_t max_entries, ebpf_verifier_options_t options); diff --git a/src/linux/linux_platform.cpp b/src/linux/linux_platform.cpp index a7a08947c..80b158d50 100644 --- a/src/linux/linux_platform.cpp +++ b/src/linux/linux_platform.cpp @@ -3,11 +3,15 @@ #include #if __linux__ #include -#define PTYPE(name, descr, native_type, prefixes) {name, descr, native_type, prefixes} -#define PTYPE_PRIVILEGED(name, descr, native_type, prefixes) {name, descr, native_type, prefixes, true} +#define PTYPE(name, descr, native_type, prefixes) \ + { name, descr, native_type, prefixes } +#define PTYPE_PRIVILEGED(name, descr, native_type, prefixes) \ + { name, descr, native_type, prefixes, true } #else -#define PTYPE(name, descr, native_type, prefixes) {name, descr, 0, prefixes} -#define PTYPE_PRIVILEGED(name, descr, native_type, prefixes) {name, descr, 0, prefixes, true} +#define PTYPE(name, descr, native_type, prefixes) \ + { name, descr, 0, prefixes } +#define PTYPE_PRIVILEGED(name, descr, native_type, prefixes) \ + { name, descr, 0, prefixes, true } #endif #include "crab_verifier.hpp" #include "helpers.hpp" @@ -15,6 +19,8 @@ #include "linux_platform.hpp" #include "platform.hpp" +#include + // Map definitions as they appear in an ELF file, so field width matters. struct bpf_load_map_def { uint32_t type; @@ -198,7 +204,7 @@ static int create_map_linux(const uint32_t map_type, const uint32_t key_size, co } #if __linux__ - union bpf_attr attr{}; + union bpf_attr attr {}; memset(&attr, '\0', sizeof(attr)); attr.map_type = map_type; attr.key_size = key_size; @@ -237,7 +243,7 @@ EbpfMapDescriptor& get_map_descriptor_linux(const int map_fd) { // (key size, value size) from the execution context, but this is // not yet supported on Linux. - throw std::runtime_error(std::string("map_fd not found")); + throw UnmarshalError("map_fd not found"); } const ebpf_platform_t g_ebpf_platform_linux = {get_program_type_linux, diff --git a/src/main/check.cpp b/src/main/check.cpp index f6874a99a..c9f46d7b9 100644 --- a/src/main/check.cpp +++ b/src/main/check.cpp @@ -233,16 +233,14 @@ int main(int argc, char** argv) { } if (domain == "zoneCrab") { - ebpf_verifier_stats_t verifier_stats; - const auto [res, seconds] = timed_execution([&] { - return ebpf_verify_program(std::cout, prog, raw_prog.info, ebpf_verifier_options, &verifier_stats); - }); - if (res && ebpf_verifier_options.cfg_opts.check_for_termination && + const auto [verifier_stats, seconds] = timed_execution([&prog] { return analyze_and_report({.prog = &prog}); }); + const bool pass = verifier_stats.total_warnings == 0; + if (pass && ebpf_verifier_options.cfg_opts.check_for_termination && (ebpf_verifier_options.print_failures || ebpf_verifier_options.print_invariants)) { std::cout << "Program terminates within " << verifier_stats.max_loop_count << " loop iterations\n"; } - std::cout << res << "," << seconds << "," << resident_set_size_kb() << "\n"; - return !res; + std::cout << pass << "," << seconds << "," << resident_set_size_kb() << "\n"; + return pass; } else if (domain == "linux") { // Pass the instruction sequence to the Linux kernel verifier. const auto [res, seconds] = bpf_verify_program(raw_prog.info.type, raw_prog.prog, &ebpf_verifier_options); diff --git a/src/main/run_yaml.cpp b/src/main/run_yaml.cpp index f447b9881..c80086f5b 100644 --- a/src/main/run_yaml.cpp +++ b/src/main/run_yaml.cpp @@ -41,7 +41,7 @@ int main(int argc, char** argv) { std::cout << "failed:\n"; res = false; std::cout << "------\n"; - print_failure(*maybe_failure, std::cout); + print_failure(*maybe_failure); std::cout << "------\n"; } else { std::cout << "pass\n"; diff --git a/src/spec_type_descriptors.hpp b/src/spec_type_descriptors.hpp index 89a7d537f..7e1821f29 100644 --- a/src/spec_type_descriptors.hpp +++ b/src/spec_type_descriptors.hpp @@ -48,13 +48,6 @@ struct EquivalenceKey { std::strong_ordering operator<=>(const EquivalenceKey&) const = default; }; -struct program_info { - const struct ebpf_platform_t* platform{}; - std::vector map_descriptors{}; - EbpfProgramType type{}; - std::map cache{}; -}; - struct btf_line_info_t { std::string file_name{}; std::string source_line{}; @@ -62,6 +55,14 @@ struct btf_line_info_t { uint32_t column_number{}; }; +struct program_info { + const struct ebpf_platform_t* platform{}; + std::vector map_descriptors{}; + EbpfProgramType type{}; + std::map cache{}; + std::map line_info{}; +}; + struct raw_program { std::string filename{}; std::string section_name{}; @@ -69,7 +70,6 @@ struct raw_program { std::string function_name{}; std::vector prog{}; program_info info{}; - std::vector line_info{}; }; void print_map_descriptors(const std::vector& descriptors, std::ostream& o); diff --git a/src/test/ebpf_yaml.cpp b/src/test/ebpf_yaml.cpp index ec02500c4..5fd83f9f9 100644 --- a/src/test/ebpf_yaml.cpp +++ b/src/test/ebpf_yaml.cpp @@ -248,10 +248,9 @@ static Diff make_diff(const T& actual, const T& expected) { } std::optional run_yaml_test_case(TestCase test_case, bool debug) { + test_case.options.print_failures = true; if (debug) { - test_case.options.print_failures = true; test_case.options.print_invariants = true; - test_case.options.simplify = false; } ebpf_context_descriptor_t context_descriptor{64, 0, 4, -1}; @@ -259,10 +258,18 @@ std::optional run_yaml_test_case(TestCase test_case, bool debug) { program_info info{&g_platform_test, {}, program_type}; + string_invariant_map out_invariants{{label_t::exit, string_invariant::top()}}; std::ostringstream ss; - const auto& [actual_last_invariant, result] = ebpf_analyze_program_for_test( - ss, test_case.instruction_seq, test_case.assumed_pre_invariant, info, test_case.options); + (void)analyze_and_report(analyze_params_t{ + .os = &ss, + .prog = &test_case.instruction_seq, + .entry_invariant = &test_case.assumed_pre_invariant, + .out_invariants = &out_invariants, + .info = &info, + .options = &test_case.options, + }); std::set actual_messages = extract_messages(ss.str()); + const string_invariant actual_last_invariant = out_invariants.at(label_t::exit); if (actual_last_invariant == test_case.expected_post_invariant && actual_messages == test_case.expected_messages) { return {}; @@ -365,10 +372,19 @@ ConformanceTestResult run_conformance_test_case(const std::vector& me try { std::ostringstream null_stream; - const auto& [actual_last_invariant, result] = - ebpf_analyze_program_for_test(null_stream, prog, pre_invariant, info, options); - for (const std::string& invariant : actual_last_invariant.value()) { + string_invariant_map out_invariants{{label_t::exit, string_invariant::top()}}; + const auto& stats = analyze_and_report(analyze_params_t{ + .os = &null_stream, + .prog = &prog, + .entry_invariant = &pre_invariant, + .out_invariants = &out_invariants, + .info = &info, + .options = &options, + }); + const bool result = stats.total_warnings == 0; + + for (const std::string& invariant : out_invariants.at(label_t::exit).value()) { if (invariant.rfind("r0.svalue=", 0) == 0) { crab::number_t lb, ub; if (invariant[10] == '[') { @@ -387,7 +403,7 @@ ConformanceTestResult run_conformance_test_case(const std::vector& me } } -void print_failure(const Failure& failure, std::ostream& out) { +void print_failure(const Failure& failure) { constexpr auto INDENT = " "; if (!failure.invariant.unexpected.empty()) { std::cout << "Unexpected properties:\n" << INDENT << failure.invariant.unexpected << "\n"; diff --git a/src/test/ebpf_yaml.hpp b/src/test/ebpf_yaml.hpp index b427c5114..72d6a0faa 100644 --- a/src/test/ebpf_yaml.hpp +++ b/src/test/ebpf_yaml.hpp @@ -30,7 +30,7 @@ struct Failure { Diff> messages; }; -void print_failure(const Failure& failure, std::ostream& out); +void print_failure(const Failure& failure); std::optional run_yaml_test_case(TestCase test_case, bool debug = false); diff --git a/src/test/test_verify.cpp b/src/test/test_verify.cpp index a8e97cbf3..d7a5f0327 100644 --- a/src/test/test_verify.cpp +++ b/src/test/test_verify.cpp @@ -33,7 +33,7 @@ FAIL_UNMARSHAL("build", "wronghelper.o", "xdp") FAIL_UNMARSHAL("invalid", "invalid-lddw.o", ".text") // Verify a section with only one program in it. -#define VERIFY_SECTION(dirname, filename, sectionname, options, platform, pass) \ +#define VERIFY_SECTION(dirname, filename, sectionname, _options, platform, pass) \ do { \ auto raw_progs = read_elf("ebpf-samples/" dirname "/" filename, sectionname, {}, platform); \ REQUIRE(raw_progs.size() == 1); \ @@ -41,7 +41,10 @@ FAIL_UNMARSHAL("invalid", "invalid-lddw.o", ".text") auto prog_or_error = unmarshal(raw_prog); \ auto prog = std::get_if(&prog_or_error); \ REQUIRE(prog != nullptr); \ - bool res = ebpf_verify_program(std::cout, *prog, raw_prog.info, options, nullptr); \ + ebpf_verifier_options_t new_options = _options; \ + const ebpf_verifier_stats_t stats = \ + analyze_and_report({.prog = prog, .info = &raw_prog.info, .options = &new_options}); \ + const bool res = stats.total_warnings == 0; \ if (pass) \ REQUIRE(res); \ else \ @@ -49,21 +52,24 @@ FAIL_UNMARSHAL("invalid", "invalid-lddw.o", ".text") } while (0) // Verify a program in a section that may have multiple programs in it. -#define VERIFY_PROGRAM(dirname, filename, section_name, program_name, options, platform, pass) \ - do { \ - auto raw_progs = read_elf("ebpf-samples/" dirname "/" filename, section_name, {}, platform); \ - for (const auto& raw_prog : raw_progs) { \ - if (raw_prog.function_name == program_name) { \ - auto prog_or_error = unmarshal(raw_prog); \ - auto prog = std::get_if(&prog_or_error); \ - REQUIRE(prog != nullptr); \ - bool res = ebpf_verify_program(std::cout, *prog, raw_prog.info, options, nullptr); \ - if (pass) \ - REQUIRE(res); \ - else \ - REQUIRE(!res); \ - } \ - } \ +#define VERIFY_PROGRAM(dirname, filename, section_name, program_name, _options, platform, pass) \ + do { \ + auto raw_progs = read_elf("ebpf-samples/" dirname "/" filename, section_name, {}, platform); \ + for (const auto& raw_prog : raw_progs) { \ + if (raw_prog.function_name == program_name) { \ + auto prog_or_error = unmarshal(raw_prog); \ + auto prog = std::get_if(&prog_or_error); \ + REQUIRE(prog != nullptr); \ + ebpf_verifier_options_t new_options = _options; \ + const ebpf_verifier_stats_t stats = analyze_and_report( \ + analyze_params_t{.prog = prog, .info = &raw_prog.info, .options = &new_options}); \ + const bool res = stats.total_warnings == 0; \ + if (pass) \ + REQUIRE(res); \ + else \ + REQUIRE(!res); \ + } \ + } \ } while (0) #define TEST_SECTION(project, filename, section) \ @@ -594,8 +600,8 @@ TEST_SECTION_LEGACY_FAIL("cilium", "bpf_lxc.o", "2/10") TEST_SECTION_FAIL("cilium", "bpf_lxc.o", "2/11") TEST_SECTION_FAIL("cilium", "bpf_lxc.o", "2/12") -void test_analyze_thread(const cfg_t* cfg, program_info* info, bool* res) { - *res = run_ebpf_analysis(std::cout, *cfg, *info, {}, nullptr); +void test_analyze_thread(std::unique_ptr cfg, program_info* info, bool* res) { + *res = analyze_and_report({.cfg = std::move(cfg), .info = info}).total_warnings == 0; } // Test multithreading @@ -606,7 +612,7 @@ TEST_CASE("multithreading", "[verify][multithreading]") { auto prog_or_error1 = unmarshal(raw_prog1); auto prog1 = std::get_if(&prog_or_error1); REQUIRE(prog1 != nullptr); - const cfg_t cfg1 = prepare_cfg(*prog1, raw_prog1.info, {}); + cfg_t cfg1 = prepare_cfg(*prog1, raw_prog1.info, {}); auto raw_progs2 = read_elf("ebpf-samples/bpf_cilium_test/bpf_netdev.o", "2/2", {}, &g_ebpf_platform_linux); REQUIRE(raw_progs2.size() == 1); @@ -614,11 +620,11 @@ TEST_CASE("multithreading", "[verify][multithreading]") { auto prog_or_error2 = unmarshal(raw_prog2); auto prog2 = std::get_if(&prog_or_error2); REQUIRE(prog2 != nullptr); - const cfg_t cfg2 = prepare_cfg(*prog2, raw_prog2.info, {}); + auto cfg2 = prepare_cfg(*prog2, raw_prog2.info, {}); bool res1, res2; - std::thread a(test_analyze_thread, &cfg1, &raw_prog1.info, &res1); - std::thread b(test_analyze_thread, &cfg2, &raw_prog2.info, &res2); + std::thread a(test_analyze_thread, std::make_unique(std::move(cfg1)), &raw_prog1.info, &res1); + std::thread b(test_analyze_thread, std::make_unique(std::move(cfg2)), &raw_prog2.info, &res2); a.join(); b.join(); diff --git a/src/test/test_yaml.cpp b/src/test/test_yaml.cpp index b7fb6b4d6..a29ab173c 100644 --- a/src/test/test_yaml.cpp +++ b/src/test/test_yaml.cpp @@ -13,7 +13,7 @@ std::optional failure = run_yaml_test_case(test_case); \ if (failure) { \ std::cout << "test case: " << test_case.name << "\n"; \ - print_failure(*failure, std::cout); \ + print_failure(*failure); \ } \ REQUIRE(!failure); \ }); \ diff --git a/test-data/jump.yaml b/test-data/jump.yaml index decbd2910..a5ffb1746 100644 --- a/test-data/jump.yaml +++ b/test-data/jump.yaml @@ -121,7 +121,7 @@ code: post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 w== 13)" --- test-case: assume number w!= reg @@ -204,9 +204,9 @@ post: - r0.svalue=1 - r0.uvalue=1 messages: - - "2:5: Code is unreachable after 2:5" - - "3:5: Code is unreachable after 3:5" - - "4:5: Code is unreachable after 4:5" + - "2:5: Code becomes unreachable (assume r1 s< -3)" + - "3:5: Code becomes unreachable (assume r1 s< -2)" + - "4:5: Code becomes unreachable (assume r1 s>= -1)" --- test-case: jump-32 @@ -238,9 +238,9 @@ post: - r0.svalue=1 - r0.uvalue=1 messages: - - "3:9: Code is unreachable after 3:9" - - "4:9: Code is unreachable after 4:9" - - "5:6: Code is unreachable after 5:6" + - "3:9: Code becomes unreachable (assume r1 w< 4)" + - "4:9: Code becomes unreachable (assume r1 w< 5)" + - "5:6: Code becomes unreachable (assume r1 w>= 6)" --- test-case: join stack @@ -555,7 +555,7 @@ post: - r10.stack_offset=512 messages: - - "7:9: Code is unreachable after 7:9" + - "7:9: Code becomes unreachable (assume r1 == r2)" --- test-case: lost implications in correlated branches @@ -622,7 +622,7 @@ post: - r4.uvalue=18446744073709551594 messages: - - "0:1: Code is unreachable after 0:1" + - "0:1: Code becomes unreachable (assume r4 w== 0)" --- test-case: unsigned comparison of negative number @@ -645,7 +645,7 @@ post: - r1.uvalue=18446744073709551615 messages: - - "0:1: Code is unreachable after 0:1" + - "0:1: Code becomes unreachable (assume r1 <= 0)" --- test-case: JMP32 @@ -668,7 +668,7 @@ post: - r1.uvalue=4294967294 messages: - - "0:2: Code is unreachable after 0:2" + - "0:2: Code becomes unreachable (assume r1 ws> 0)" --- test-case: assume map_fd == map_fd @@ -691,7 +691,7 @@ code: post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 != r1)" --- test-case: assume map_fd1 != map_fd2 @@ -717,7 +717,7 @@ code: post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 != r2)" --- test-case: assume map_fd1 < map_fd2 @@ -762,7 +762,7 @@ post: - r1.type=ctx messages: - - "0:2: Code is unreachable after 0:2" + - "0:2: Code becomes unreachable (assume r1 == 0)" --- test-case: JNE with imm 0 and pointer options: ["assume_assertions"] @@ -781,8 +781,7 @@ code: post: [] messages: - - "0:1: Code is unreachable after 0:1" - - "2: Code is unreachable after 2" + - "0:1: Code becomes unreachable (assume r1 == 0)" - "2: Invalid type (r0.type == number)" --- @@ -803,7 +802,6 @@ code: post: [] messages: - - "2: Code is unreachable after 2" - "2: Invalid type (r0.type == number)" --- @@ -824,7 +822,6 @@ code: post: [] messages: - - "2: Code is unreachable after 2" - "2: Invalid type (r0.type == number)" --- @@ -852,7 +849,7 @@ post: - r1.uvalue=[0, +oo] messages: - - "0:2: Code is unreachable after 0:2" + - "0:2: Code becomes unreachable (assume r1 < 0)" --- test-case: JLE with imm 0 and pointer @@ -879,7 +876,7 @@ post: - r1.uvalue=[1, +oo] messages: - - "0:2: Code is unreachable after 0:2" + - "0:2: Code becomes unreachable (assume r1 <= 0)" --- test-case: JGT with imm 0 and pointer @@ -899,8 +896,7 @@ code: post: [] messages: - - "0:1: Code is unreachable after 0:1" - - "2: Code is unreachable after 2" + - "0:1: Code becomes unreachable (assume r1 <= 0)" - "2: Invalid type (r0.type == number)" --- @@ -921,8 +917,7 @@ code: post: [] messages: - - "0:1: Code is unreachable after 0:1" - - "2: Code is unreachable after 2" + - "0:1: Code becomes unreachable (assume r1 < 0)" - "2: Invalid type (r0.type == number)" --- @@ -943,7 +938,6 @@ code: post: [] messages: - - "0: Code is unreachable after 0" - "0: Invalid type (r1.type == number)" --- @@ -964,7 +958,6 @@ code: post: [] messages: - - "0: Code is unreachable after 0" - "0: Invalid type (r1.type == number)" --- @@ -985,7 +978,6 @@ code: post: [] messages: - - "0: Code is unreachable after 0" - "0: Invalid type (r1.type == number)" --- @@ -1006,7 +998,6 @@ code: post: [] messages: - - "0: Code is unreachable after 0" - "0: Invalid type (r1.type == number)" --- @@ -1027,7 +1018,6 @@ code: post: [] messages: - - "0: Code is unreachable after 0" - "0: Invalid type (r1.type == number)" --- @@ -1048,7 +1038,6 @@ code: post: [] messages: - - "0: Code is unreachable after 0" - "0: Invalid type (r1.type == number)" --- @@ -1069,7 +1058,6 @@ code: post: [] messages: - - "0: Code is unreachable after 0" - "0: Invalid type (r1.type == number)" --- @@ -1090,7 +1078,6 @@ code: post: [] messages: - - "0: Code is unreachable after 0" - "0: Invalid type (r1.type == number)" --- @@ -1111,7 +1098,6 @@ code: post: [] messages: - - "0: Code is unreachable after 0" - "0: Invalid type (r1.type == number)" --- @@ -1132,7 +1118,6 @@ code: post: [] messages: - - "0: Code is unreachable after 0" - "0: Invalid type (r1.type == number)" --- @@ -1153,7 +1138,6 @@ code: post: [] messages: - - "0: Code is unreachable after 0" - "0: Invalid type (r1.type == number)" --- @@ -1174,7 +1158,6 @@ code: post: [] messages: - - "0: Code is unreachable after 0" - "0: Invalid type (r1.type == number)" --- @@ -1195,7 +1178,6 @@ code: post: [] messages: - - "0: Code is unreachable after 0" - "0: Invalid type (r1.type == number)" --- @@ -1216,7 +1198,6 @@ code: post: [] messages: - - "0: Code is unreachable after 0" - "0: Invalid type (r1.type == number)" --- @@ -1237,7 +1218,6 @@ code: post: [] messages: - - "0: Code is unreachable after 0" - "0: Invalid type (r1.type == number)" --- @@ -1258,5 +1238,4 @@ code: post: [] messages: - - "0: Code is unreachable after 0" - "0: Invalid type (r1.type == number)" diff --git a/test-data/loop.yaml b/test-data/loop.yaml index e47f1a6e0..2a33c7d64 100644 --- a/test-data/loop.yaml +++ b/test-data/loop.yaml @@ -282,7 +282,7 @@ code: post: [] messages: - - "1:2: Code is unreachable after 1:2" + - "1:2: Code becomes unreachable (assume r0 >= 1)" - "0 (counter): Loop counter is too large (pc[0] < 100000)" --- test-case: simple infinite loop, less than or equal @@ -299,7 +299,7 @@ code: post: [] messages: - - "1:2: Code is unreachable after 1:2" + - "1:2: Code becomes unreachable (assume r0 > 1)" - "0 (counter): Loop counter is too large (pc[0] < 100000)" --- @@ -317,7 +317,7 @@ code: post: [] messages: - - "1:2: Code is unreachable after 1:2" + - "1:2: Code becomes unreachable (assume r0 != 0)" - "0 (counter): Loop counter is too large (pc[0] < 100000)" --- @@ -335,7 +335,7 @@ code: post: [] messages: - - "1:2: Code is unreachable after 1:2" + - "1:2: Code becomes unreachable (assume r0 <= 0)" - "0 (counter): Loop counter is too large (pc[0] < 100000)" --- @@ -353,7 +353,7 @@ code: post: [] messages: - - "1:2: Code is unreachable after 1:2" + - "1:2: Code becomes unreachable (assume r0 < 0)" - "0 (counter): Loop counter is too large (pc[0] < 100000)" --- test-case: infinite loop with multiple exits @@ -369,8 +369,8 @@ code: exit post: [] messages: - - "1:2: Code is unreachable after 1:2" - - "3:4: Code is unreachable after 3:4" + - "1:2: Code becomes unreachable (assume r0 <= 0)" + - "3:4: Code becomes unreachable (assume r0 >= 2)" - "0 (counter): Loop counter is too large (pc[0] < 100000)" --- @@ -460,6 +460,6 @@ code: post: [] messages: - - "1:3: Code is unreachable after 1:3" + - "1:3: Code becomes unreachable (assume r0 > 10)" - "2 (counter): Loop counter is too large (pc[2] < 100000)" - - "2:3: Code is unreachable after 2:3" + - "2:3: Code becomes unreachable (assume r0 <= 0)" diff --git a/test-data/shift.yaml b/test-data/shift.yaml index b9d0e1ac3..8d3b1c5f5 100644 --- a/test-data/shift.yaml +++ b/test-data/shift.yaml @@ -1119,12 +1119,6 @@ pre: code: : | r0 >>= 0 - if r1 == r0 goto - r2 = 0 - exit - : | - r2 = 1 - exit post: - r0.type=number @@ -1133,14 +1127,6 @@ post: - r1.type=number - r1.svalue=-9223372036854775808 - r1.uvalue=9223372036854775808 - - r0.svalue=r1.svalue - - r0.uvalue=r1.uvalue - - r2.svalue=1 - - r2.type=number - - r2.uvalue=1 - -messages: - - "1:2: Code is unreachable after 1:2" --- test-case: check that unsigned right shift by 0 is idempotent - MAX_INT64 @@ -1156,28 +1142,14 @@ pre: code: : | r0 >>= 0 - if r1 == r0 goto - r2 = 0 - exit - : | - r2 = 1 - exit post: - r0.svalue=9223372036854775807 - - r0.svalue=r1.svalue - r0.type=number - r0.uvalue=9223372036854775807 - - r0.uvalue=r1.uvalue - r1.svalue=9223372036854775807 - r1.type=number - r1.uvalue=9223372036854775807 - - r2.svalue=1 - - r2.type=number - - r2.uvalue=1 - -messages: - - "1:2: Code is unreachable after 1:2" --- test-case: check that unsigned right shift by 0 is idempotent - MIN_INT64 - via register @@ -1196,12 +1168,6 @@ pre: code: : | r0 >>= r3 - if r1 == r0 goto - r2 = 0 - exit - : | - r2 = 1 - exit post: - r0.type=number @@ -1210,18 +1176,10 @@ post: - r1.type=number - r1.svalue=-9223372036854775808 - r1.uvalue=9223372036854775808 - - r0.svalue=r1.svalue - - r0.uvalue=r1.uvalue - - r2.svalue=1 - - r2.type=number - - r2.uvalue=1 - r3.type=number - r3.uvalue=0 - r3.svalue=0 -messages: - - "1:2: Code is unreachable after 1:2" - --- test-case: check that unsigned right shift by 0 is idempotent - MAX_INT64 - via register @@ -1239,32 +1197,18 @@ pre: code: : | r0 >>= r3 - if r1 == r0 goto - r2 = 0 - exit - : | - r2 = 1 - exit post: - r0.svalue=9223372036854775807 - - r0.svalue=r1.svalue - r0.type=number - r0.uvalue=9223372036854775807 - - r0.uvalue=r1.uvalue - r1.svalue=9223372036854775807 - r1.type=number - r1.uvalue=9223372036854775807 - - r2.svalue=1 - - r2.type=number - - r2.uvalue=1 - r3.type=number - r3.uvalue=0 - r3.svalue=0 -messages: - - "1:2: Code is unreachable after 1:2" - --- test-case: check that signed right shift by 0 is idempotent - MIN_INT64 @@ -1279,12 +1223,6 @@ pre: code: : | r0 s>>= 0 - if r1 == r0 goto - r2 = 0 - exit - : | - r2 = 1 - exit post: - r0.type=number @@ -1293,14 +1231,6 @@ post: - r1.type=number - r1.svalue=-9223372036854775808 - r1.uvalue=9223372036854775808 - - r0.svalue=r1.svalue - - r0.uvalue=r1.uvalue - - r2.svalue=1 - - r2.type=number - - r2.uvalue=1 - -messages: - - "1:2: Code is unreachable after 1:2" --- test-case: check that signed right shift by 0 is idempotent - MAX_INT64 @@ -1316,28 +1246,14 @@ pre: code: : | r0 s>>= 0 - if r1 == r0 goto - r2 = 0 - exit - : | - r2 = 1 - exit post: - r0.svalue=9223372036854775807 - - r0.svalue=r1.svalue - r0.type=number - r0.uvalue=9223372036854775807 - - r0.uvalue=r1.uvalue - r1.svalue=9223372036854775807 - r1.type=number - r1.uvalue=9223372036854775807 - - r2.svalue=1 - - r2.type=number - - r2.uvalue=1 - -messages: - - "1:2: Code is unreachable after 1:2" --- test-case: check that signed right shift by 0 is idempotent - MAX_UINT64 @@ -1353,28 +1269,14 @@ pre: code: : | r0 s>>= 0 - if r1 == r0 goto - r2 = 0 - exit - : | - r2 = 1 - exit post: - r0.svalue=-1 - - r0.svalue=r1.svalue - r0.type=number - r0.uvalue=18446744073709551615 - - r0.uvalue=r1.uvalue - r1.svalue=-1 - r1.type=number - r1.uvalue=18446744073709551615 - - r2.svalue=1 - - r2.type=number - - r2.uvalue=1 - -messages: - - "1:2: Code is unreachable after 1:2" --- test-case: check that signed right shift by 0 is idempotent - MIN_INT64 - via register @@ -1393,12 +1295,6 @@ pre: code: : | r0 s>>= r3 - if r1 == r0 goto - r2 = 0 - exit - : | - r2 = 1 - exit post: - r0.type=number @@ -1407,18 +1303,10 @@ post: - r1.type=number - r1.svalue=-9223372036854775808 - r1.uvalue=9223372036854775808 - - r0.svalue=r1.svalue - - r0.uvalue=r1.uvalue - - r2.svalue=1 - - r2.type=number - - r2.uvalue=1 - r3.type=number - r3.uvalue=0 - r3.svalue=0 -messages: - - "1:2: Code is unreachable after 1:2" - --- test-case: check that signed right shift by 0 is idempotent - MAX_INT64 @@ -1436,32 +1324,18 @@ pre: code: : | r0 s>>= r3 - if r1 == r0 goto - r2 = 0 - exit - : | - r2 = 1 - exit post: - r0.svalue=9223372036854775807 - - r0.svalue=r1.svalue - r0.type=number - r0.uvalue=9223372036854775807 - - r0.uvalue=r1.uvalue - r1.svalue=9223372036854775807 - r1.type=number - r1.uvalue=9223372036854775807 - - r2.svalue=1 - - r2.type=number - - r2.uvalue=1 - r3.type=number - r3.uvalue=0 - r3.svalue=0 -messages: - - "1:2: Code is unreachable after 1:2" - --- test-case: check that signed right shift by 0 is idempotent - MAX_UINT64 - via register @@ -1479,32 +1353,18 @@ pre: code: : | r0 s>>= r3 - if r1 == r0 goto - r2 = 0 - exit - : | - r2 = 1 - exit post: - r0.svalue=-1 - - r0.svalue=r1.svalue - r0.type=number - r0.uvalue=18446744073709551615 - - r0.uvalue=r1.uvalue - r1.svalue=-1 - r1.type=number - r1.uvalue=18446744073709551615 - - r2.svalue=1 - - r2.type=number - - r2.uvalue=1 - r3.type=number - r3.uvalue=0 - r3.svalue=0 -messages: - - "1:2: Code is unreachable after 1:2" - --- test-case: check that left shift by 0 is idempotent - MIN_INT64 @@ -1519,12 +1379,6 @@ pre: code: : | r0 <<= 0 - if r1 == r0 goto - r2 = 0 - exit - : | - r2 = 1 - exit post: - r0.type=number @@ -1533,14 +1387,6 @@ post: - r1.type=number - r1.svalue=-9223372036854775808 - r1.uvalue=9223372036854775808 - - r0.svalue=r1.svalue - - r0.uvalue=r1.uvalue - - r2.svalue=1 - - r2.type=number - - r2.uvalue=1 - -messages: - - "1:2: Code is unreachable after 1:2" --- test-case: check that left shift by 0 is idempotent - MAX_INT64 @@ -1556,28 +1402,14 @@ pre: code: : | r0 <<= 0 - if r1 == r0 goto - r2 = 0 - exit - : | - r2 = 1 - exit post: - r0.svalue=9223372036854775807 - - r0.svalue=r1.svalue - r0.type=number - r0.uvalue=9223372036854775807 - - r0.uvalue=r1.uvalue - r1.svalue=9223372036854775807 - r1.type=number - r1.uvalue=9223372036854775807 - - r2.svalue=1 - - r2.type=number - - r2.uvalue=1 - -messages: - - "1:2: Code is unreachable after 1:2" --- test-case: check that left shift by 0 is idempotent - MIN_INT64 - via register @@ -1596,12 +1428,6 @@ pre: code: : | r0 <<= r3 - if r1 == r0 goto - r2 = 0 - exit - : | - r2 = 1 - exit post: - r0.type=number @@ -1610,18 +1436,10 @@ post: - r1.type=number - r1.svalue=-9223372036854775808 - r1.uvalue=9223372036854775808 - - r0.svalue=r1.svalue - - r0.uvalue=r1.uvalue - - r2.svalue=1 - - r2.type=number - - r2.uvalue=1 - r3.type=number - r3.uvalue=0 - r3.svalue=0 -messages: - - "1:2: Code is unreachable after 1:2" - --- test-case: check that left shift by 0 is idempotent - MAX_INT64 - via register @@ -1639,28 +1457,14 @@ pre: code: : | r0 <<= r3 - if r1 == r0 goto - r2 = 0 - exit - : | - r2 = 1 - exit post: - r0.svalue=9223372036854775807 - - r0.svalue=r1.svalue - r0.type=number - r0.uvalue=9223372036854775807 - - r0.uvalue=r1.uvalue - r1.svalue=9223372036854775807 - r1.type=number - r1.uvalue=9223372036854775807 - - r2.svalue=1 - - r2.type=number - - r2.uvalue=1 - r3.type=number - r3.uvalue=0 - r3.svalue=0 - -messages: - - "1:2: Code is unreachable after 1:2" diff --git a/test-data/unsigned.yaml b/test-data/unsigned.yaml index d05033357..6fcc0369d 100644 --- a/test-data/unsigned.yaml +++ b/test-data/unsigned.yaml @@ -7,7 +7,7 @@ code: : assume r1 < 0 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 < 0)" --- test-case: "assume 0 w< 0 implies bottom" pre: ["r1.type=number", "r1.svalue=0", "r1.uvalue=0"] @@ -15,7 +15,7 @@ code: : assume w1 < 0 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 w< 0)" --- test-case: "assume -1 < 0 implies bottom" pre: ["r1.type=number", "r1.svalue=-1", "r1.uvalue=18446744073709551615"] @@ -23,7 +23,7 @@ code: : assume r1 < 0 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 < 0)" --- test-case: "assume -1 w< 0 implies bottom" pre: ["r1.type=number", "r1.svalue=-1", "r1.uvalue=18446744073709551615"] @@ -31,7 +31,7 @@ code: : assume w1 < 0 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 w< 0)" --- test-case: "assume -1 < 1 implies bottom" pre: ["r1.type=number", "r1.svalue=-1", "r1.uvalue=18446744073709551615"] @@ -39,7 +39,7 @@ code: : assume r1 < 1 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 < 1)" --- test-case: "assume -1 w< 1 implies bottom" pre: ["r1.type=number", "r1.svalue=-1", "r1.uvalue=18446744073709551615"] @@ -47,7 +47,7 @@ code: : assume w1 < 1 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 w< 1)" --- test-case: "assume 1 < 0 implies bottom" pre: ["r1.type=number", "r1.svalue=1", "r1.uvalue=1"] @@ -55,7 +55,7 @@ code: : assume r1 < 0 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 < 0)" --- test-case: "assume 1 w< 0 implies bottom" pre: ["r1.type=number", "r1.svalue=1", "r1.uvalue=1"] @@ -63,7 +63,7 @@ code: : assume w1 < 0 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 w< 0)" --- test-case: "assume 1 < 1 implies bottom" pre: ["r1.type=number", "r1.svalue=1", "r1.uvalue=1"] @@ -71,7 +71,7 @@ code: : assume r1 < 1 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 < 1)" --- test-case: "assume 1 w< 1 implies bottom" pre: ["r1.type=number", "r1.svalue=1", "r1.uvalue=1"] @@ -79,7 +79,7 @@ code: : assume w1 < 1 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 w< 1)" --- test-case: "assume 2 < 1 implies bottom" pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2"] @@ -87,7 +87,7 @@ code: : assume r1 < 1 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 < 1)" --- test-case: "assume 2 w< 1 implies bottom" pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2"] @@ -95,7 +95,7 @@ code: : assume w1 < 1 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 w< 1)" --- test-case: "assume [0, 1] < 0 implies bottom" pre: ["r1.type=number", "r1.svalue=[0, 1]", "r1.uvalue=[0, 1]", "r1.svalue=r1.uvalue"] @@ -103,7 +103,7 @@ code: : assume r1 < 0 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 < 0)" --- test-case: "assume [0, 1] w< 0 implies bottom" pre: ["r1.type=number", "r1.svalue=[0, 1]", "r1.uvalue=[0, 1]", "r1.svalue=r1.uvalue"] @@ -111,7 +111,7 @@ code: : assume w1 < 0 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 w< 0)" --- test-case: "assume [2, 3] < 1 implies bottom" pre: ["r1.type=number", "r1.svalue=[2, 3]", "r1.uvalue=[2, 3]", "r1.svalue=r1.uvalue"] @@ -119,7 +119,7 @@ code: : assume r1 < 1 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 < 1)" --- test-case: "assume [2, 3] w< 1 implies bottom" pre: ["r1.type=number", "r1.svalue=[2, 3]", "r1.uvalue=[2, 3]", "r1.svalue=r1.uvalue"] @@ -127,7 +127,7 @@ code: : assume w1 < 1 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 w< 1)" --- test-case: "assume [-2, -1] < 0 implies bottom" pre: ["r1.type=number", "r1.svalue=[-2, -1]", "r1.uvalue=[18446744073709551614, 18446744073709551615]"] @@ -135,7 +135,7 @@ code: : assume r1 < 1 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 < 1)" --- test-case: "assume [-2, -1] w< 0 implies bottom" pre: ["r1.type=number", "r1.svalue=[-2, -1]", "r1.uvalue=[18446744073709551614, 18446744073709551615]"] @@ -143,7 +143,7 @@ code: : assume w1 < 1 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 w< 1)" --- test-case: "assume [-3, -2] < -3 implies bottom" pre: ["r1.type=number", "r1.svalue=[-3, -2]", "r1.uvalue=[18446744073709551613, 18446744073709551614]"] @@ -151,7 +151,7 @@ code: : assume r1 < -3 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 < -3)" --- test-case: "assume [-3, -2] w< -3 implies bottom" pre: ["r1.type=number", "r1.svalue=[-3, -2]", "r1.uvalue=[18446744073709551613, 18446744073709551614]"] @@ -159,7 +159,7 @@ code: : assume w1 < -3 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 w< -3)" --- test-case: "assume [-3, -2] < -4 implies bottom" pre: ["r1.type=number", "r1.svalue=[-3, -2]", "r1.uvalue=[18446744073709551613, 18446744073709551614]"] @@ -167,7 +167,7 @@ code: : assume r1 < -4 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 < -4)" --- test-case: "assume [-3, -2] w< -4 implies bottom" pre: ["r1.type=number", "r1.svalue=[-3, -2]", "r1.uvalue=[18446744073709551613, 18446744073709551614]"] @@ -175,7 +175,7 @@ code: : assume w1 < -4 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 w< -4)" --- test-case: "assume 1 < [0, 1] implies bottom" pre: ["r1.type=number", "r1.svalue=1", "r1.uvalue=1", @@ -184,7 +184,7 @@ code: : assume r1 < r2 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 < r2)" --- test-case: "assume 1 w< [0, 1] implies bottom" pre: ["r1.type=number", "r1.svalue=1", "r1.uvalue=1", @@ -193,7 +193,7 @@ code: : assume w1 < r2 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 w< r2)" --- test-case: "assume -1 < [0, 1] implies bottom" pre: ["r1.type=number", "r1.svalue=-1", "r1.uvalue=18446744073709551615", @@ -202,7 +202,7 @@ code: : assume r1 < r2 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 < r2)" --- test-case: "assume -1 w< [0, 1] implies bottom" pre: ["r1.type=number", "r1.svalue=-1", "r1.uvalue=18446744073709551615", @@ -211,7 +211,7 @@ code: : assume w1 < r2 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 w< r2)" --- test-case: "assume -1 < [1, 2] implies bottom" pre: ["r1.type=number", "r1.svalue=-1", "r1.uvalue=18446744073709551615", @@ -220,7 +220,7 @@ code: : assume r1 < r2 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 < r2)" --- test-case: "assume -1 w< [1, 2] implies bottom" pre: ["r1.type=number", "r1.svalue=-1", "r1.uvalue=18446744073709551615", @@ -229,7 +229,7 @@ code: : assume w1 < r2 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 w< r2)" --- test-case: "assume 2 < [0, 1] implies bottom" pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2", @@ -238,7 +238,7 @@ code: : assume r1 < r2 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 < r2)" --- test-case: "assume 2 w< [0, 1] implies bottom" pre: ["r1.type=number", "r1.svalue=2", "r1.uvalue=2", @@ -247,7 +247,7 @@ code: : assume w1 < r2 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 w< r2)" --- test-case: "assume 1 < [0, 1] implies bottom" pre: ["r1.type=number", "r1.svalue=1", "r1.uvalue=1", @@ -256,7 +256,7 @@ code: : assume r1 < r2 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 < r2)" --- test-case: "assume 1 w< [0, 1] implies bottom" pre: ["r1.type=number", "r1.svalue=1", "r1.uvalue=1", @@ -265,7 +265,7 @@ code: : assume w1 < r2 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 w< r2)" --- test-case: "assume 2 < [0, 1] implies bottom" pre: ["r1.type=number", "r1.svalue=1", "r1.uvalue=1", @@ -274,7 +274,7 @@ code: : assume r1 < r2 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 < r2)" --- test-case: "assume 2 w< [0, 1] implies bottom" pre: ["r1.type=number", "r1.svalue=1", "r1.uvalue=1", @@ -283,7 +283,7 @@ code: : assume w1 < r2 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 w< r2)" --- test-case: "assume [2, 3] < [1, 2] implies bottom" pre: ["r1.type=number", "r1.svalue=[2, 3]", "r1.uvalue=[2, 3]", "r1.svalue=r1.uvalue", @@ -292,7 +292,7 @@ code: : assume r1 < r2 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 < r2)" --- test-case: "assume [2, 3] w< [1, 2] implies bottom" pre: ["r1.type=number", "r1.svalue=[2, 3]", "r1.uvalue=[2, 3]", "r1.svalue=r1.uvalue", @@ -301,7 +301,7 @@ code: : assume w1 < r2 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 w< r2)" --- test-case: "assume [-2, -1] < [0, 1] implies bottom" pre: ["r1.type=number", "r1.svalue=[-2, -1]", "r1.uvalue=[18446744073709551614, 18446744073709551615]", @@ -310,7 +310,7 @@ code: : assume r1 < r2 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 < r2)" --- test-case: "assume [-2, -1] w< [0, 1] implies bottom" pre: ["r1.type=number", "r1.svalue=[-2, -1]", "r1.uvalue=[18446744073709551614, 18446744073709551615]", @@ -319,7 +319,7 @@ code: : assume w1 < r2 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 w< r2)" --- test-case: "assume [-3, -2] < [-4, -3] implies bottom" pre: ["r1.type=number", "r1.svalue=[-3, -2]", "r1.uvalue=[18446744073709551613, 18446744073709551614]", @@ -328,7 +328,7 @@ code: : assume r1 < r2 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 < r2)" --- test-case: "assume [-3, -2] w< [-4, -3] implies bottom" pre: ["r1.type=number", "r1.svalue=[-3, -2]", "r1.uvalue=[18446744073709551613, 18446744073709551614]", @@ -337,7 +337,7 @@ code: : assume w1 < r2 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 w< r2)" --- test-case: "assume [-3, -2] < [-5, -4] implies bottom" pre: ["r1.type=number", "r1.svalue=[-3, -2]", "r1.uvalue=[18446744073709551613, 18446744073709551614]", @@ -346,7 +346,7 @@ code: : assume r1 < r2 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 < r2)" --- test-case: "assume [-3, -2] w< [-5, -4] implies bottom" pre: ["r1.type=number", "r1.svalue=[-3, -2]", "r1.uvalue=[18446744073709551613, 18446744073709551614]", @@ -355,7 +355,7 @@ code: : assume w1 < r2 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 w< r2)" --- test-case: "assume INT_MIN+1 < 0 implies bottom" pre: [] @@ -365,7 +365,7 @@ code: assume r1 < 0 post: [] messages: - - "1: Code is unreachable after 1" + - "1: Code becomes unreachable (assume r1 < 0)" --- test-case: "assume INT_MIN+1 w< 0 implies bottom" pre: [] @@ -375,7 +375,7 @@ code: assume w1 < 0 post: [] messages: - - "1: Code is unreachable after 1" + - "1: Code becomes unreachable (assume r1 w< 0)" --- test-case: "assume INT_MIN+1 w< 2 nop" pre: [] @@ -391,7 +391,7 @@ code: : assume r1 < 0 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 < 0)" --- test-case: "assume [INT32_MIN, -1] w< 0 implies bottom" pre: ["r1.type=number", "r1.svalue=[-2147483648, -1]", "r1.uvalue=[18446744071562067968, 18446744073709551615]"] @@ -400,7 +400,7 @@ code: assume w1 < 0 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 w< 0)" --- test-case: "assume something w< 0 implies bottom" pre: ["r1.type=number", "r1.svalue=-4294967298", "r1.uvalue=18446744069414584318"] @@ -409,7 +409,7 @@ code: assume w1 < 0 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 w< 0)" --- test-case: "assume INT_MIN+1 < 1 implies bottom" pre: [] @@ -419,7 +419,7 @@ code: assume r1 < 1 post: [] messages: - - "1: Code is unreachable after 1" + - "1: Code becomes unreachable (assume r1 < 1)" --- test-case: "assume INT32_MIN w< 1 implies bottom" pre: [] @@ -429,7 +429,7 @@ code: assume w1 < 1 post: [] messages: - - "1: Code is unreachable after 1" + - "1: Code becomes unreachable (assume r1 w< 1)" --- test-case: "assume INT_MIN+1 < INT_MIN+1 implies bottom" pre: [] @@ -440,7 +440,7 @@ code: assume r1 < r2 post: [] messages: - - "2: Code is unreachable after 2" + - "2: Code becomes unreachable (assume r1 < r2)" --- test-case: "assume INT32_MIN w< INT32_MIN implies bottom" pre: [] @@ -451,7 +451,7 @@ code: assume w1 < r2 post: [] messages: - - "2: Code is unreachable after 2" + - "2: Code becomes unreachable (assume r1 w< r2)" --- test-case: "assume INT_MIN+2 < INT_MIN+1 implies bottom" pre: [] @@ -462,7 +462,7 @@ code: assume r1 < r2 post: [] messages: - - "2: Code is unreachable after 2" + - "2: Code becomes unreachable (assume r1 < r2)" --- test-case: "assume -1 < INT_MIN+1 implies bottom" pre: [] @@ -473,7 +473,7 @@ code: assume r1 < r2 post: [] messages: - - "2: Code is unreachable after 2" + - "2: Code becomes unreachable (assume r1 < r2)" --- test-case: "assume -1 w< INT32_MIN implies bottom" pre: [] @@ -484,7 +484,7 @@ code: assume w1 < r2 post: [] messages: - - "2: Code is unreachable after 2" + - "2: Code becomes unreachable (assume r1 w< r2)" --- test-case: "assume INT32_MIN w< INT32_MAX implies bottom" pre: [] @@ -495,7 +495,7 @@ code: assume w1 < r2 post: [] messages: - - "2: Code is unreachable after 2" + - "2: Code becomes unreachable (assume r1 w< r2)" --- test-case: "assume [1, INT_MAX] < 1 implies bottom" pre: ["r1.type=number", "r1.svalue=[0, 9223372036854775806]", "r1.uvalue=[0, 9223372036854775806]", "r1.svalue=r1.uvalue"] @@ -505,7 +505,7 @@ code: assume r1 < 1 post: [] messages: - - "1: Code is unreachable after 1" + - "1: Code becomes unreachable (assume r1 < 1)" --- test-case: "assume [1, INT32_MAX] w< 1 implies bottom" pre: ["r1.type=number", "r1.svalue=[1, 2147483647]", "r1.uvalue=[1, 2147483647]", "r1.svalue=r1.uvalue"] @@ -514,7 +514,7 @@ code: assume w1 < 1 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 w< 1)" --- test-case: "assume [INT_MAX-1, INT_MAX] < 1 implies bottom" pre: ["r1.type=number", "r1.svalue=[9223372036854775803, 9223372036854775804]", "r1.uvalue=[9223372036854775803, 9223372036854775804]", "r1.svalue=r1.uvalue"] @@ -524,7 +524,7 @@ code: assume r1 < 1 post: [] messages: - - "1: Code is unreachable after 1" + - "1: Code becomes unreachable (assume r1 < 1)" --- test-case: "assume [INT32_MAX-1, INT32_MAX] < 1 implies bottom" pre: ["r1.type=number", "r1.svalue=[2147483646, 2147483647]", "r1.uvalue=[2147483646, 2147483647]", "r1.svalue=r1.uvalue"] @@ -533,7 +533,7 @@ code: assume w1 < 1 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 w< 1)" --- test-case: "assume [INT_MAX, INT_MAX+1] < 1 implies bottom" pre: ["r1.type=number", "r1.svalue=[9223372036854775803, 9223372036854775804]", "r1.uvalue=[9223372036854775803, 9223372036854775804]", "r1.svalue=r1.uvalue"] @@ -543,7 +543,7 @@ code: assume r1 < 1 post: [] messages: - - "1: Code is unreachable after 1" + - "1: Code becomes unreachable (assume r1 < 1)" --- test-case: "assume 0 < 1 nop" pre: [] @@ -596,7 +596,7 @@ code: assume r1 > 1 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 > 1)" --- test-case: "assume [0, 1] w> 1 implies bottom" pre: ["r1.type=number", "r1.svalue=[0, 1]", "r1.uvalue=[0, 1]", "r1.svalue=r1.uvalue"] @@ -605,7 +605,7 @@ code: assume w1 > 1 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 w> 1)" --- test-case: "assume [1, 2] > 1 narrows to 2" pre: ["r1.type=number", "r1.svalue=[1, 2]", "r1.uvalue=[1, 2]", "r1.svalue=r1.uvalue"] @@ -685,7 +685,7 @@ code: assume r1 > r2 post: [] messages: - - "1: Code is unreachable after 1" + - "1: Code becomes unreachable (assume r1 > r2)" --- test-case: "assume [0, INT32_MAX] w> INT32_MAX implies bottom" pre: ["r1.type=number", "r1.svalue=[0, 2147483647]", "r1.uvalue=[0, 2147483647]", "r1.svalue=r1.uvalue"] @@ -694,7 +694,7 @@ code: assume w1 > 2147483647 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 w> 2147483647)" --- test-case: "assume [0, INT_MAX-4] >= INT_MAX-4 narrows to INT_MAX-4" pre: ["r1.type=number", "r1.svalue=[0, 9223372036854775803]", "r1.uvalue=[0, 9223372036854775803]", "r1.svalue=r1.uvalue"] @@ -1085,7 +1085,7 @@ code: : assume r1 != 11 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 != 11)" --- test-case: "assume [0, 1] != 1 narrows to 0" pre: ["r1.type=number", "r1.svalue=[0, 1]", "r1.uvalue=[0, 1]"] @@ -1111,7 +1111,7 @@ code: : assume w1 != 11 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 w!= 11)" --- test-case: "assume [3, 4] w< 2 implies bottom" pre: ["r1.type=number", "r1.svalue=[3, 4]", "r1.uvalue=[3, 4]"] @@ -1119,7 +1119,7 @@ code: : assume w1 < 2 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 w< 2)" --- test-case: "assume [UINT32_MAX+1, UINT32_MAX+5] w< 2" pre: ["r1.type=number", "r1.uvalue=[4294967296, 4294967300]"] @@ -1248,7 +1248,7 @@ code: : assume w1 s> 0 post: [] messages: - - "0: Code is unreachable after 0" + - "0: Code becomes unreachable (assume r1 ws> 0)" --- test-case: signed 32-bit GT reg pre: ["r1.type=number", "r1.svalue=[-2, 2]", "r2.type=number", "r2.svalue=[-2, 2]"] From 5044c77e9a0debbf80e5c1dd6fb807710fd37889 Mon Sep 17 00:00:00 2001 From: Elazar Gershuni Date: Fri, 15 Nov 2024 16:43:49 +0200 Subject: [PATCH 2/2] code review Signed-off-by: Elazar Gershuni --- src/main/check.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/check.cpp b/src/main/check.cpp index c9f46d7b9..a3db7169a 100644 --- a/src/main/check.cpp +++ b/src/main/check.cpp @@ -240,7 +240,7 @@ int main(int argc, char** argv) { std::cout << "Program terminates within " << verifier_stats.max_loop_count << " loop iterations\n"; } std::cout << pass << "," << seconds << "," << resident_set_size_kb() << "\n"; - return pass; + return !pass; } else if (domain == "linux") { // Pass the instruction sequence to the Linux kernel verifier. const auto [res, seconds] = bpf_verify_program(raw_prog.info.type, raw_prog.prog, &ebpf_verifier_options);