diff --git a/src/asm_cfg.cpp b/src/asm_cfg.cpp index cd1ade2a1..fabd9c2ba 100644 --- a/src/asm_cfg.cpp +++ b/src/asm_cfg.cpp @@ -1,8 +1,7 @@ // Copyright (c) Prevail Verifier contributors. // SPDX-License-Identifier: MIT -#include - #include +#include #include #include #include @@ -87,7 +86,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 +142,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 +162,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 +182,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)) { @@ -230,6 +229,8 @@ static cfg_t instruction_seq_to_cfg(const InstructionSeq& insts, const bool must } cfg_t prepare_cfg(const InstructionSeq& prog, const program_info& info, const prepare_cfg_options& options) { + thread_local_program_info.set(info); + // Convert the instruction sequence to a deterministic control-flow graph. cfg_t cfg = instruction_seq_to_cfg(prog, options.must_have_exit); diff --git a/src/asm_files.cpp b/src/asm_files.cpp index 53039f741..27e987e7f 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)}; } @@ -38,15 +38,15 @@ static vector vector_of(const ELFIO::section& sec) { int create_map_crab(const EbpfMapType& map_type, const uint32_t key_size, const uint32_t value_size, const uint32_t max_entries, ebpf_verifier_options_t) { const EquivalenceKey equiv{map_type.value_type, key_size, value_size, map_type.is_array ? max_entries : 0}; - if (!global_program_info->cache.contains(equiv)) { + if (!thread_local_program_info->cache.contains(equiv)) { // +1 so 0 is the null FD - global_program_info->cache[equiv] = gsl::narrow(global_program_info->cache.size()) + 1; + thread_local_program_info->cache[equiv] = gsl::narrow(thread_local_program_info->cache.size()) + 1; } - return global_program_info->cache.at(equiv); + return thread_local_program_info->cache.at(equiv); } EbpfMapDescriptor* find_map_descriptor(const int map_fd) { - for (EbpfMapDescriptor& map : global_program_info->map_descriptors) { + for (EbpfMapDescriptor& map : thread_local_program_info->map_descriptors) { if (map.original_fd == map_fd) { return ↦ } @@ -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}; @@ -307,7 +307,7 @@ vector read_elf(std::istream& input_stream, const std::string& path if (btf) { // Parse the BTF type data. btf_data = vector_of(*btf); - if (options.dump_btf_types_json) { + if (options.verbosity_opts.dump_btf_types_json) { std::stringstream output; std::cout << "Dumping BTF data for" << path << std::endl; // Dump the BTF data to cout for debugging purposes. @@ -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_ostream.cpp b/src/asm_ostream.cpp index ddd7022c6..cd707de83 100644 --- a/src/asm_ostream.cpp +++ b/src/asm_ostream.cpp @@ -257,7 +257,7 @@ struct AssertionPrinterVisitor { } void operator()(ValidCall const& a) { - const EbpfHelperPrototype proto = global_program_info->platform->get_helper_prototype(a.func); + const EbpfHelperPrototype proto = thread_local_program_info->platform->get_helper_prototype(a.func); _os << "valid call(" << proto.name << ")"; } diff --git a/src/asm_unmarshal.cpp b/src/asm_unmarshal.cpp index 094917238..7bb7ab7e2 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); @@ -794,9 +794,9 @@ struct Unmarshaller { }; std::variant unmarshal(const raw_program& raw_prog, vector>& notes) { - global_program_info = raw_prog.info; + thread_local_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/assertions.cpp b/src/assertions.cpp index faebc9579..e7f769d35 100644 --- a/src/assertions.cpp +++ b/src/assertions.cpp @@ -193,7 +193,7 @@ class AssertExtractor { vector operator()(const Mem& ins) const { vector res; const Reg basereg = ins.access.basereg; - Imm width{static_cast(ins.access.width)}; + Imm width{gsl::narrow(ins.access.width)}; const int offset = ins.access.offset; if (basereg.v == R10_STACK_POINTER) { // We know we are accessing the stack. @@ -201,6 +201,10 @@ class AssertExtractor { // This assertion will fail res.emplace_back(make_valid_access(basereg, offset, width, false, ins.is_load ? AccessType::read : AccessType::write)); + } else if (ins.is_load) { + // This assertion is not for bound checks but for reading initialized memory. + // TODO: avoid load assertions: use post-assertion to check that the loaded value is initialized + // res.emplace_back(make_valid_access(basereg, offset, width, false, AccessType::read)); } } else { res.emplace_back(TypeConstraint{basereg, TypeGroup::pointer}); diff --git a/src/config.hpp b/src/config.hpp index 09d5d919e..c46629e03 100644 --- a/src/config.hpp +++ b/src/config.hpp @@ -4,13 +4,27 @@ #include "crab/cfg.hpp" +struct verbosity_options_t { + /// When true, prints simplified control flow graph by merging chains into basic blocks. + bool simplify = true; + + /// Print the invariants for each basic block. + bool print_invariants = false; + + /// Print failures that occur during verification. + bool print_failures = false; + + /// When printing the control flow graph, print the line number of each instruction. + bool print_line_info = false; + + /// Print the BTF types in JSON format. + bool dump_btf_types_json = false; +}; + struct ebpf_verifier_options_t { // Options that control how the control flow graph is built. prepare_cfg_options cfg_opts; - /// When true, simplifies the control flow graph by merging basic blocks. - bool simplify = true; - // True to assume prior failed assertions are true and continue verification. bool assume_assertions = false; @@ -29,23 +43,12 @@ struct ebpf_verifier_options_t { // True if the ELF file is built on a big endian system. bool big_endian = false; - // Print the invariants for each basic block. - bool print_invariants = false; - - // Print failures that occur during verification. - bool print_failures = false; - - // When printing the control flow graph, print the line number of each instruction. - bool print_line_info = false; - - // Print the BTF types in JSON format. - bool dump_btf_types_json = false; + verbosity_options_t verbosity_opts; }; 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/array_domain.cpp b/src/crab/array_domain.cpp index 0461514c3..e6ad08303 100644 --- a/src/crab/array_domain.cpp +++ b/src/crab/array_domain.cpp @@ -421,17 +421,11 @@ std::vector offset_map_t::get_overlap_cells(const offset_t o, const unsi // We use a global array map using array_map_t = std::unordered_map; -static thread_local lazy_allocator global_array_map; +static thread_local lazy_allocator thread_local_array_map; -void clear_thread_local_state() { global_array_map.clear(); } +void clear_thread_local_state() { thread_local_array_map.clear(); } -static offset_map_t& lookup_array_map(const data_kind_t kind) { return (*global_array_map)[kind]; } - -/** - Ugly this needs to be fixed: needed if multiple analyses are - run so we can clear the array map from one run to another. -**/ -void clear_global_state() { global_array_map->clear(); } +static offset_map_t& lookup_array_map(const data_kind_t kind) { return (*thread_local_array_map)[kind]; } void array_domain_t::initialize_numbers(const int lb, const int width) { num_bytes.reset(lb, width); diff --git a/src/crab/array_domain.hpp b/src/crab/array_domain.hpp index 0768927a1..2eb561677 100644 --- a/src/crab/array_domain.hpp +++ b/src/crab/array_domain.hpp @@ -34,8 +34,6 @@ namespace crab::domains { // Numerical abstract domain. using NumAbsDomain = AddBottom; -void clear_global_state(); - void clear_thread_local_state(); class array_domain_t final { 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..4a09e5490 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,16 +149,16 @@ 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, + require(inv, ub <= thread_local_program_info->type.context_descriptor->size, std::string("Upper bound must be at most ") + - std::to_string(global_program_info->type.context_descriptor->size)); + std::to_string(thread_local_program_info->type.context_descriptor->size)); } 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); @@ -243,18 +243,14 @@ void ebpf_checker::operator()(const FuncConstraint& s) { if (sn->fits()) { // We can now process it as if the id was immediate. const int32_t imm = sn->cast_to(); - if (!global_program_info->platform->is_helper_usable(imm)) { + if (!thread_local_program_info->platform->is_helper_usable(imm)) { require("invalid helper function id " + std::to_string(imm)); return; } - const Call call = make_call(imm, *global_program_info->platform); - for (const Assertion& sub_assertion : get_assertions(call, *global_program_info, {})) { + const Call call = make_call(imm, *thread_local_program_info->platform); + for (const Assertion& sub_assertion : get_assertions(call, *thread_local_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,15 +258,15 @@ 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); + const EbpfHelperPrototype proto = thread_local_program_info->platform->get_helper_prototype(s.func); if (proto.return_type == EBPF_RETURN_TYPE_INTEGER_OR_NO_RETURN_IF_SUCCEED) { require("tail call not supported in subprogram"); return; @@ -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); @@ -313,7 +309,7 @@ void ebpf_checker::operator()(const ValidMapKeyValue& s) { require(inv, linear_constraint_t::false_const(), "Illegal map update with a non-numerical value [" + lb_s + "-" + ub_s + ")"); } else if (thread_local_options.strict && fd_type.has_value()) { - EbpfMapType map_type = global_program_info->platform->get_map_type(*fd_type); + EbpfMapType map_type = thread_local_program_info->platform->get_map_type(*fd_type); if (map_type.is_array) { // Get offset value. variable_t key_ptr = access_reg.stack_offset; @@ -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.cpp b/src/crab/ebpf_domain.cpp index cb4ca0b6c..6539ab311 100644 --- a/src/crab/ebpf_domain.cpp +++ b/src/crab/ebpf_domain.cpp @@ -184,7 +184,7 @@ std::optional ebpf_domain_t::get_map_type(const Reg& map_fd_reg) const std::optional type; for (int32_t map_fd = start_fd; map_fd <= end_fd; map_fd++) { - EbpfMapDescriptor* map = &global_program_info->platform->get_map_descriptor(map_fd); + EbpfMapDescriptor* map = &thread_local_program_info->platform->get_map_descriptor(map_fd); if (map == nullptr) { return std::optional(); } @@ -206,7 +206,7 @@ std::optional ebpf_domain_t::get_map_inner_map_fd(const Reg& map_fd_re std::optional inner_map_fd; for (int map_fd = start_fd; map_fd <= end_fd; map_fd++) { - EbpfMapDescriptor* map = &global_program_info->platform->get_map_descriptor(map_fd); + EbpfMapDescriptor* map = &thread_local_program_info->platform->get_map_descriptor(map_fd); if (map == nullptr) { return {}; } @@ -228,7 +228,7 @@ interval_t ebpf_domain_t::get_map_key_size(const Reg& map_fd_reg) const { interval_t result = interval_t::bottom(); for (int map_fd = start_fd; map_fd <= end_fd; map_fd++) { - if (const EbpfMapDescriptor* map = &global_program_info->platform->get_map_descriptor(map_fd)) { + if (const EbpfMapDescriptor* map = &thread_local_program_info->platform->get_map_descriptor(map_fd)) { result = result | interval_t{map->key_size}; } else { return interval_t::top(); @@ -246,7 +246,7 @@ interval_t ebpf_domain_t::get_map_value_size(const Reg& map_fd_reg) const { interval_t result = interval_t::bottom(); for (int map_fd = start_fd; map_fd <= end_fd; map_fd++) { - if (const EbpfMapDescriptor* map = &global_program_info->platform->get_map_descriptor(map_fd)) { + if (const EbpfMapDescriptor* map = &thread_local_program_info->platform->get_map_descriptor(map_fd)) { result = result | interval_t(map->value_size); } else { return interval_t::top(); @@ -264,7 +264,7 @@ interval_t ebpf_domain_t::get_map_max_entries(const Reg& map_fd_reg) const { interval_t result = interval_t::bottom(); for (int map_fd = start_fd; map_fd <= end_fd; map_fd++) { - if (const EbpfMapDescriptor* map = &global_program_info->platform->get_map_descriptor(map_fd)) { + if (const EbpfMapDescriptor* map = &thread_local_program_info->platform->get_map_descriptor(map_fd)) { result = result | interval_t(map->max_entries); } else { return interval_t::top(); @@ -281,6 +281,8 @@ extended_number ebpf_domain_t::get_loop_count_upper_bound() const { return ub; } +interval_t ebpf_domain_t::get_r0() const { return m_inv[reg_pack(R0_RETURN_VALUE).svalue]; } + std::ostream& operator<<(std::ostream& o, const ebpf_domain_t& dom) { if (dom.is_bottom()) { o << "_|_"; @@ -298,7 +300,7 @@ void ebpf_domain_t::initialize_packet() { inv += 0 <= variable_t::packet_size(); inv += variable_t::packet_size() < MAX_PACKET_SIZE; - const auto info = *global_program_info; + const auto info = *thread_local_program_info; if (info.type.context_descriptor->meta >= 0) { inv += variable_t::meta_offset() <= 0; inv += variable_t::meta_offset() >= -4098; diff --git a/src/crab/ebpf_domain.hpp b/src/crab/ebpf_domain.hpp index 001dcfaf3..1981536a4 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); @@ -66,6 +66,7 @@ class ebpf_domain_t final { static ebpf_domain_t calculate_constant_limits(); extended_number get_loop_count_upper_bound() const; + interval_t get_r0() const; static ebpf_domain_t setup_entry(bool init_r1); static ebpf_domain_t from_constraints(const std::set& constraints, bool setup_constraints); diff --git a/src/crab/ebpf_transformer.cpp b/src/crab/ebpf_transformer.cpp index c809990d9..c3eec5d45 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()); } @@ -1364,7 +1364,7 @@ void ebpf_transformer::do_load_ctx(NumAbsDomain& inv, const Reg& target_reg, con return; } - const ebpf_context_descriptor_t* desc = global_program_info->type.context_descriptor; + const ebpf_context_descriptor_t* desc = thread_local_program_info->type.context_descriptor; const reg_pack_t& target = reg_pack(target_reg); @@ -1760,7 +1760,7 @@ void ebpf_transformer::operator()(const Call& call) { // This is the only way to get a null pointer if (maybe_fd_reg) { if (const auto map_type = dom.get_map_type(*maybe_fd_reg)) { - if (global_program_info->platform->get_map_type(*map_type).value_type == EbpfMapValueType::MAP) { + if (thread_local_program_info->platform->get_map_type(*map_type).value_type == EbpfMapValueType::MAP) { if (const auto inner_map_fd = dom.get_map_inner_map_fd(*maybe_fd_reg)) { do_load_mapfd(r0_reg, to_signed(*inner_map_fd), true); goto out; @@ -1815,18 +1815,18 @@ void ebpf_transformer::operator()(const Callx& callx) { if (sn->fits()) { // We can now process it as if the id was immediate. const int32_t imm = sn->cast_to(); - if (!global_program_info->platform->is_helper_usable(imm)) { + if (!thread_local_program_info->platform->is_helper_usable(imm)) { return; } - const Call call = make_call(imm, *global_program_info->platform); + const Call call = make_call(imm, *thread_local_program_info->platform); (*this)(call); } } } void ebpf_transformer::do_load_mapfd(const Reg& dst_reg, const int mapfd, const bool maybe_null) { - const EbpfMapDescriptor& desc = global_program_info->platform->get_map_descriptor(mapfd); - const EbpfMapType& type = global_program_info->platform->get_map_type(desc.type); + const EbpfMapDescriptor& desc = thread_local_program_info->platform->get_map_descriptor(mapfd); + const EbpfMapType& type = thread_local_program_info->platform->get_map_type(desc.type); if (type.value_type == EbpfMapValueType::PROGRAM) { type_inv.assign_type(m_inv, dst_reg, T_MAP_PROGRAMS); } else { diff --git a/src/crab/fwd_analyzer.cpp b/src/crab/fwd_analyzer.cpp index f77e8e90a..268f7e158 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_table_t _inv; /// number of narrowing iterations. If the narrowing operator is /// indeed a narrowing operator this parameter is not @@ -65,7 +63,11 @@ 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.at(label).pre = v; } + + ebpf_domain_t get_pre(const label_t& node) { return _inv.at(node).pre; } + + ebpf_domain_t get_post(const label_t& node) { return _inv.at(node).post; } void transform_to_post(const label_t& label, ebpf_domain_t pre) { const GuardedInstruction& ins = _cfg.at(label); @@ -78,7 +80,7 @@ class interleaved_fwd_fixpoint_iterator_t final { } ebpf_domain_transform(pre, ins.cmd); - _post[label] = std::move(pre); + _inv.at(label).post = std::move(pre); } [[nodiscard]] @@ -102,6 +104,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 +117,18 @@ 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.emplace(label, invariant_map_pair{ebpf_domain_t::bottom(), ebpf_domain_t::bottom()}); } } - ebpf_domain_t get_pre(const label_t& node) { return _pre.at(node); } - - ebpf_domain_t get_post(const label_t& node) { return _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_table_t 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_table_t 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 +143,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 +155,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..c87839689 100644 --- a/src/crab/fwd_analyzer.hpp +++ b/src/crab/fwd_analyzer.hpp @@ -9,8 +9,12 @@ namespace crab { -using invariant_table_t = std::map; +struct invariant_map_pair { + ebpf_domain_t pre; + ebpf_domain_t post; +}; +using invariant_table_t = std::map; -std::pair run_forward_analyzer(const cfg_t& cfg, ebpf_domain_t entry_inv); +invariant_table_t run_forward_analyzer(const cfg_t& cfg, ebpf_domain_t entry_inv); } // namespace crab diff --git a/src/crab/split_dbm.cpp b/src/crab/split_dbm.cpp index b8cf2ce50..1005a1272 100644 --- a/src/crab/split_dbm.cpp +++ b/src/crab/split_dbm.cpp @@ -1205,7 +1205,8 @@ string_invariant SplitDBM::to_set() const { std::ostream& operator<<(std::ostream& o, const SplitDBM& dom) { return o << dom.to_set(); } bool SplitDBM::eval_expression_overflow(const linear_expression_t& e, Weight& out) const { - [[maybe_unused]] const bool overflow = convert_NtoW_overflow(e.constant_term(), out); + [[maybe_unused]] + const bool overflow = convert_NtoW_overflow(e.constant_term(), out); assert(!overflow); for (const auto& [variable, coefficient] : e.variable_terms()) { Weight coef; diff --git a/src/crab/split_dbm.hpp b/src/crab/split_dbm.hpp index f45cd84be..8ec93be2c 100644 --- a/src/crab/split_dbm.hpp +++ b/src/crab/split_dbm.hpp @@ -304,7 +304,7 @@ class SplitDBM final { string_invariant to_set() const; public: - static void clear_thread_local_state() { GraphOps::clear_thread_local_state(); } + static void clear_thread_local_state() { GraphOps::clear_thread_local_state(); } }; // class SplitDBM } // namespace domains diff --git a/src/crab/type_domain.cpp b/src/crab/type_domain.cpp index f2185b676..2fbd7c522 100644 --- a/src/crab/type_domain.cpp +++ b/src/crab/type_domain.cpp @@ -308,7 +308,7 @@ bool TypeDomain::is_in_group(const NumAbsDomain& inv, const Reg& r, const TypeGr } } -std::string typeset_to_string(const std::vector& items) { +std::string typeset_to_string(const std::vector& items) { std::stringstream ss; ss << "{"; for (auto it = items.begin(); it != items.end(); ++it) { diff --git a/src/crab/var_factory.cpp b/src/crab/var_factory.cpp index 00ace7328..7eeaadf54 100644 --- a/src/crab/var_factory.cpp +++ b/src/crab/var_factory.cpp @@ -134,7 +134,7 @@ std::vector default_variable_names() { "data_size", "meta_size", }; -}; +} thread_local lazy_allocator, default_variable_names> variable_t::names; diff --git a/src/crab_utils/stats.cpp b/src/crab_utils/stats.cpp index 8e9b24002..59ba6dd3b 100644 --- a/src/crab_utils/stats.cpp +++ b/src/crab_utils/stats.cpp @@ -101,7 +101,6 @@ void CrabStats::count_max(const std::string& name, const unsigned v) { unsigned CrabStats::uset(const std::string& n, const unsigned v) { return (*counters)[n] = v; } unsigned CrabStats::get(const std::string& n) { return (*counters)[n]; } - /** Outputs all statistics to std output */ void CrabStats::Print(std::ostream& OS) { OS << "\n\n************** STATS ***************** \n"; diff --git a/src/crab_verifier.cpp b/src/crab_verifier.cpp index 3a42f55f6..a1d18932d 100644 --- a/src/crab_verifier.cpp +++ b/src/crab_verifier.cpp @@ -7,246 +7,192 @@ #include #include +#include #include #include -#include - +#include "asm_files.hpp" +#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" using crab::ebpf_domain_t; using std::string; -thread_local crab::lazy_allocator global_program_info; +thread_local crab::lazy_allocator thread_local_program_info; thread_local ebpf_verifier_options_t thread_local_options; - -// 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(); +void ebpf_verifier_clear_before_analysis(); + +struct LineInfoPrinter { + std::ostream& os; + std::string previous_source_line; + + void print_line_info(const label_t& label) { + if (thread_local_options.verbosity_opts.print_line_info) { + const auto& line_info_map = thread_local_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 std::numeric_limits::max(); } - checks_db() = default; }; -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; +bool Invariants::is_valid_after(const label_t& label, const string_invariant& state) const { + const ebpf_domain_t abstract_state = + ebpf_domain_t::from_constraints(state.value(), thread_local_options.setup_constraints); + return abstract_state <= invariants.at(label).post; +} + +void Invariants::print_invariants(std::ostream& os, const cfg_t& cfg) const { + LineInfoPrinter printer{os}; 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(); + printer.print_line_info(label); + const auto& inv_pair = invariants.at(label); + os << "\nPre-invariant : " << inv_pair.pre << "\n"; + os << cfg.get_node(label); + os << "\nPost-invariant: " << inv_pair.post << "\n"; + } + os << "\n"; +} - 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); +string_invariant Invariants::invariant_at(const label_t& label) const { return invariants.at(label).post.to_set(); } - if (!pre_bot && from_inv.is_bottom()) { - m_db.add_unreachable(label, std::string("Code is unreachable after ") + to_string(label)); - } - } +crab::interval_t Invariants::exit_value() const { return invariants.at(label_t::exit).post.get_r0(); } - 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()); - } +int Invariants::max_loop_count() const { + crab::extended_number max_loop_count{0}; + // Gather the upper bound of loop counts from post-invariants. + for (const auto& inv_pair : std::views::values(invariants)) { + max_loop_count = std::max(max_loop_count, inv_pair.post.get_loop_count_upper_bound()); } - return m_db; + const auto m = max_loop_count.number(); + if (m && m->fits()) { + return m->cast_to(); + } + return std::numeric_limits::max(); } -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()); - } - } - return label_to_line_info; +Invariants analyze(const cfg_t& cfg, ebpf_domain_t&& entry_invariant) { + return Invariants{run_forward_analyzer(cfg, std::move(entry_invariant))}; } -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; - } - } +Invariants analyze(const cfg_t& cfg) { + ebpf_verifier_clear_before_analysis(); + return analyze(cfg, ebpf_domain_t::setup_entry(thread_local_options.setup_constraints)); +} + +Invariants analyze(const cfg_t& cfg, const string_invariant& entry_invariant) { + ebpf_verifier_clear_before_analysis(); + return analyze(cfg, + ebpf_domain_t::from_constraints(entry_invariant.value(), thread_local_options.setup_constraints)); +} + +void Report::print_reachability(std::ostream& os) const { + for (const auto& [label, notes] : reachability) { + for (const auto& msg : notes) { os << label << ": " << msg << "\n"; } } 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); - } - 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; - } - } - s << "\nPre-invariant : " << pre_invariants.at(label) << "\n"; - s << cfg.get_node(label); - s << "\nPost-invariant: " << post_invariants.at(label) << "\n"; +void Report::print_warnings(std::ostream& os) const { + LineInfoPrinter printer{os}; + for (const auto& [label, warnings] : warnings) { + for (const auto& msg : warnings) { + printer.print_line_info(label); + os << label << ": " << msg << "\n"; } } - return db; + os << "\n"; } -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; - } +void Report::print_all_messages(std::ostream& os) const { + print_reachability(os); + print_warnings(os); } -/// 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(); +std::set Report::all_messages() const { + std::set result = warning_set(); + for (const auto& note : reachability_set()) { + result.insert(note); } - return report.total_warnings == 0; + return result; } -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()); +std::set Report::reachability_set() const { + std::set result; + for (const auto& [label, warnings] : reachability) { + for (const auto& msg : warnings) { + result.insert(to_string(label) + ": " + msg); + } } - return res; + return result; } -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(); - - 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"); - } - 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}; +std::set Report::warning_set() const { + std::set result; + for (const auto& [label, warnings] : warnings) { + for (const auto& msg : warnings) { + result.insert(to_string(label) + ": " + msg); + } } + return result; } -/// 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); +bool Report::verified() const { return warnings.empty(); } - std::optional prog_opt = std::nullopt; - if (options.print_failures) { - prog_opt = prog; +bool Invariants::verified(const cfg_t& cfg) const { + for (const auto& [label, inv_pair] : invariants) { + if (inv_pair.pre.is_bottom()) { + continue; + } + for (const Assertion& assertion : cfg.at(label).preconditions) { + if (!ebpf_domain_check(inv_pair.pre, assertion).empty()) { + return false; + } + } } + return true; +} - 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); +Report Invariants::check_assertions(const cfg_t& cfg) const { + Report report; + for (const auto& [label, inv_pair] : invariants) { + if (inv_pair.pre.is_bottom()) { + continue; } - if (stats) { - stats->total_unreachable = report.total_unreachable; - stats->total_warnings = report.total_warnings; - stats->max_loop_count = report.get_max_loop_count(); + const auto ins = cfg.at(label); + for (const Assertion& assertion : ins.preconditions) { + const auto warnings = ebpf_domain_check(inv_pair.pre, assertion); + for (const auto& msg : warnings) { + report.warnings[label].emplace_back(msg); + } + } + if (std::holds_alternative(ins.cmd)) { + if (inv_pair.post.is_bottom()) { + const auto s = to_string(std::get(ins.cmd)); + report.reachability[label].emplace_back("Code becomes unreachable (" + s + ")"); + } } - return report.total_warnings == 0; - } catch (std::logic_error& e) { - std::cerr << e.what(); - return false; } + return report; } -void ebpf_verifier_clear_thread_local_state() { +void ebpf_verifier_clear_before_analysis() { + crab::domains::clear_thread_local_state(); crab::variable_t::clear_thread_local_state(); +} + +void ebpf_verifier_clear_thread_local_state() { crab::CrabStats::clear_thread_local_state(); - global_program_info.clear(); + thread_local_program_info.clear(); crab::domains::clear_thread_local_state(); crab::domains::SplitDBM::clear_thread_local_state(); } diff --git a/src/crab_verifier.hpp b/src/crab_verifier.hpp index 1da1d5e22..b5dc99b89 100644 --- a/src/crab_verifier.hpp +++ b/src/crab_verifier.hpp @@ -4,21 +4,48 @@ #include "config.hpp" #include "crab/cfg.hpp" +#include "crab/fwd_analyzer.hpp" #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); +class Report final { + std::map> warnings; + std::map> reachability; + friend class Invariants; -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); + public: + void print_reachability(std::ostream& os) const; + void print_warnings(std::ostream& os) const; + void print_all_messages(std::ostream& os) const; + std::set all_messages() const; + std::set reachability_set() const; + std::set warning_set() const; + bool verified() const; +}; -using string_invariant_map = std::map; +class Invariants final { + crab::invariant_table_t invariants; -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); + public: + explicit Invariants(crab::invariant_table_t&& invariants) : invariants(std::move(invariants)) {} + Invariants(Invariants&& invariants) = default; + Invariants(const Invariants& invariants) = default; + + bool is_valid_after(const label_t& label, const string_invariant& state) const; + void print_invariants(std::ostream& os, const cfg_t& cfg) const; + + string_invariant invariant_at(const label_t& label) const; + + crab::interval_t exit_value() const; + + int max_loop_count() const; + bool verified(const cfg_t& cfg) const; + Report check_assertions(const cfg_t& cfg) const; +}; + +Invariants analyze(const cfg_t& cfg); +Invariants analyze(const cfg_t& cfg, const string_invariant& entry_invariant); +inline bool verify(const cfg_t& cfg) { return analyze(cfg).verified(cfg); } 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/gpl/spec_prototypes.cpp b/src/linux/gpl/spec_prototypes.cpp index f00c885d1..09e64913a 100644 --- a/src/linux/gpl/spec_prototypes.cpp +++ b/src/linux/gpl/spec_prototypes.cpp @@ -2281,7 +2281,7 @@ bool is_helper_usable_linux(const int32_t n) { // If the helper has a context_descriptor, it must match the hook's context_descriptor. if ((prototypes[n].context_descriptor != nullptr) && - (prototypes[n].context_descriptor != global_program_info->type.context_descriptor)) { + (prototypes[n].context_descriptor != thread_local_program_info->type.context_descriptor)) { return false; } diff --git a/src/linux/linux_platform.cpp b/src/linux/linux_platform.cpp index a7a08947c..68ea28ca8 100644 --- a/src/linux/linux_platform.cpp +++ b/src/linux/linux_platform.cpp @@ -3,18 +3,23 @@ #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" #include "linux/gpl/spec_type_descriptors.hpp" #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; @@ -175,8 +180,7 @@ void resolve_inner_map_references_linux(std::vector& map_desc for (size_t i = 0; i < map_descriptors.size(); i++) { const unsigned int inner = map_descriptors[i].inner_map_fd; // Get the inner_map_idx back. if (inner >= map_descriptors.size()) { - throw std::runtime_error(std::string("bad inner map index ") + std::to_string(inner) + " for map " + - std::to_string(i)); + throw UnmarshalError("bad inner map index " + std::to_string(inner) + " for map " + std::to_string(i)); } map_descriptors[i].inner_map_fd = map_descriptors.at(inner).original_fd; } @@ -198,7 +202,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; @@ -207,15 +211,13 @@ static int create_map_linux(const uint32_t map_type, const uint32_t key_size, co attr.map_flags = map_type == BPF_MAP_TYPE_HASH ? BPF_F_NO_PREALLOC : 0; const int map_fd = do_bpf(BPF_MAP_CREATE, attr); if (map_fd < 0) { - if (options.print_failures) { - std::cerr << "Failed to create map, " << strerror(errno) << "\n"; - std::cerr << "Map: \n" - << " map_type = " << attr.map_type << "\n" - << " key_size = " << attr.key_size << "\n" - << " value_size = " << attr.value_size << "\n" - << " max_entries = " << attr.max_entries << "\n" - << " map_flags = " << attr.map_flags << "\n"; - } + std::cerr << "Failed to create map, " << strerror(errno) << "\n"; + std::cerr << "Map: \n" + << " map_type = " << attr.map_type << "\n" + << " key_size = " << attr.key_size << "\n" + << " value_size = " << attr.value_size << "\n" + << " max_entries = " << attr.max_entries << "\n" + << " map_flags = " << attr.map_flags << "\n"; exit(2); } return map_fd; @@ -237,7 +239,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 " + std::to_string(map_fd) + " not found"); } const ebpf_platform_t g_ebpf_platform_linux = {get_program_type_linux, diff --git a/src/linux/linux_platform.hpp b/src/linux/linux_platform.hpp index 1ce6121b3..3d6f95fe2 100644 --- a/src/linux/linux_platform.hpp +++ b/src/linux/linux_platform.hpp @@ -2,5 +2,7 @@ // SPDX-License-Identifier: MIT #pragma once +#include "helpers.hpp" + EbpfHelperPrototype get_helper_prototype_linux(int32_t n); bool is_helper_usable_linux(int32_t n); diff --git a/src/main/check.cpp b/src/main/check.cpp index f6874a99a..cabfc4155 100644 --- a/src/main/check.cpp +++ b/src/main/check.cpp @@ -12,7 +12,6 @@ #include "memsize_linux.hpp" #endif #include "linux_verifier.hpp" -#include "utils.hpp" // Avoid affecting other headers by macros. #include "CLI11/CLI11.hpp" @@ -124,19 +123,22 @@ int main(int argc, char** argv) { ->expected(0, _conformance_groups.size()) ->check(CLI::IsMember(_get_conformance_group_names())); - app.add_flag("--simplify,!--no-simplify", ebpf_verifier_options.simplify, + app.add_flag("--simplify,!--no-simplify", ebpf_verifier_options.verbosity_opts.simplify, "Simplify the CFG before analysis by merging chains of instructions into a single basic block. " "Default: enabled") ->group("Verbosity"); - app.add_flag("--line-info", ebpf_verifier_options.print_line_info, "Print line information")->group("Verbosity"); - app.add_flag("--print-btf-types", ebpf_verifier_options.dump_btf_types_json, "Print BTF types")->group("Verbosity"); + app.add_flag("--line-info", ebpf_verifier_options.verbosity_opts.print_line_info, "Print line information") + ->group("Verbosity"); + app.add_flag("--print-btf-types", ebpf_verifier_options.verbosity_opts.dump_btf_types_json, "Print BTF types") + ->group("Verbosity"); app.add_flag("--assume-assert,!--no-assume-assert", ebpf_verifier_options.assume_assertions, "Assume assertions (useful for debugging verification failures). Default: disabled") ->group("Verbosity"); - app.add_flag("-i", ebpf_verifier_options.print_invariants, "Print invariants")->group("Verbosity"); - app.add_flag("-f", ebpf_verifier_options.print_failures, "Print verifier's failure logs")->group("Verbosity"); + app.add_flag("-i", ebpf_verifier_options.verbosity_opts.print_invariants, "Print invariants")->group("Verbosity"); + app.add_flag("-f", ebpf_verifier_options.verbosity_opts.print_failures, "Print verifier's failure logs") + ->group("Verbosity"); bool verbose = false; app.add_flag("-v", verbose, "Print both invariants and failures")->group("Verbosity"); @@ -148,7 +150,8 @@ int main(int argc, char** argv) { CLI11_PARSE(app, argc, argv); if (verbose) { - ebpf_verifier_options.print_invariants = ebpf_verifier_options.print_failures = true; + ebpf_verifier_options.verbosity_opts.print_invariants = ebpf_verifier_options.verbosity_opts.print_failures = + true; } // Enable default conformance groups, which don't include callx or packet. @@ -229,20 +232,46 @@ int main(int argc, char** argv) { if (!asmfile.empty()) { std::ofstream out{asmfile}; print(prog, out, {}); - print_map_descriptors(global_program_info->map_descriptors, out); + print_map_descriptors(thread_local_program_info->map_descriptors, out); } - 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 && - (ebpf_verifier_options.print_failures || ebpf_verifier_options.print_invariants)) { - std::cout << "Program terminates within " << verifier_stats.max_loop_count << " loop iterations\n"; + if (domain == "zoneCrab" || domain == "cfg") { + // Convert the instruction sequence to a control-flow graph. + try { + const cfg_t cfg = prepare_cfg(prog, raw_prog.info, ebpf_verifier_options.cfg_opts); + if (domain == "cfg") { + std::cout << cfg; + std::cout << "\n"; + return 0; + } + const auto begin = std::chrono::steady_clock::now(); + auto invariants = analyze(cfg); + const auto end = std::chrono::steady_clock::now(); + const auto seconds = std::chrono::duration(end - begin).count(); + + if (ebpf_verifier_options.verbosity_opts.print_invariants) { + invariants.print_invariants(std::cout, cfg); + } + + bool pass; + if (ebpf_verifier_options.verbosity_opts.print_failures) { + auto report = invariants.check_assertions(cfg); + report.print_warnings(std::cout); + pass = report.verified(); + } else { + pass = invariants.verified(cfg); + } + if (pass && ebpf_verifier_options.cfg_opts.check_for_termination && + (ebpf_verifier_options.verbosity_opts.print_failures || + ebpf_verifier_options.verbosity_opts.print_invariants)) { + std::cout << "Program terminates within " << invariants.max_loop_count() << " loop iterations\n"; + } + std::cout << pass << "," << seconds << "," << resident_set_size_kb() << "\n"; + return pass ? 0 : 1; + } catch (UnmarshalError& e) { + std::cerr << "error: " << e.what() << std::endl; + return 1; } - std::cout << res << "," << seconds << "," << resident_set_size_kb() << "\n"; - return !res; } 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); @@ -262,11 +291,6 @@ int main(int argc, char** argv) { std::cout << "," << stats.at(h); } std::cout << "\n"; - } else if (domain == "cfg") { - // Convert the instruction sequence to a control-flow graph. - const cfg_t cfg = prepare_cfg(prog, raw_prog.info, ebpf_verifier_options.cfg_opts); - std::cout << cfg; - std::cout << "\n"; } else { assert(false); } diff --git a/src/main/linux_verifier.cpp b/src/main/linux_verifier.cpp index 103d4e3e3..8d43cbc34 100644 --- a/src/main/linux_verifier.cpp +++ b/src/main/linux_verifier.cpp @@ -2,7 +2,6 @@ // SPDX-License-Identifier: MIT #if __linux__ -#include #include #include #include @@ -10,43 +9,46 @@ #include "config.hpp" #include "linux_verifier.hpp" #include "spec_type_descriptors.hpp" -#include "utils.hpp" static int do_bpf(const bpf_cmd cmd, union bpf_attr& attr) { return syscall(321, cmd, &attr, sizeof(attr)); } /** Run the built-in Linux verifier on a raw eBPF program. * - * \return A pair (passed, elapsec_secs) + * \return A pair (passed, elapsed_secs) */ std::tuple bpf_verify_program(const EbpfProgramType& type, const std::vector& raw_prog, ebpf_verifier_options_t* options) { - std::vector buf(options->print_failures ? 1000000 : 10); + std::vector buf(options->verbosity_opts.print_failures ? 1000000 : 10); buf[0] = 0; memset(buf.data(), '\0', buf.size()); - union bpf_attr attr{}; + union bpf_attr attr {}; memset(&attr, '\0', sizeof(attr)); - attr.prog_type = (__u32)type.platform_specific_data; - attr.insn_cnt = (__u32)raw_prog.size(); - attr.insns = (__u64)raw_prog.data(); - attr.license = (__u64) "GPL"; - if (options->print_failures) { - attr.log_buf = (__u64)buf.data(); + attr.prog_type = gsl::narrow<__u32>(type.platform_specific_data); + attr.insn_cnt = gsl::narrow<__u32>(raw_prog.size()); + attr.insns = reinterpret_cast<__u64>(raw_prog.data()); + attr.license = reinterpret_cast<__u64>("GPL"); + if (options->verbosity_opts.print_failures) { + attr.log_buf = reinterpret_cast<__u64>(buf.data()); attr.log_size = buf.size(); attr.log_level = 3; } attr.kern_version = 0x041800; attr.prog_flags = 0; - const auto [res, elapsed_secs] = timed_execution([&] { return do_bpf(BPF_PROG_LOAD, attr); }); + const auto begin = std::chrono::steady_clock::now(); + const int res = do_bpf(BPF_PROG_LOAD, attr); + const auto end = std::chrono::steady_clock::now(); + const auto seconds = std::chrono::duration(end - begin).count(); + if (res < 0) { - if (options->print_failures) { + if (options->verbosity_opts.print_failures) { std::cerr << "Failed to verify program: " << strerror(errno) << " (" << errno << ")\n"; - std::cerr << "LOG: " << (char*)attr.log_buf; + std::cerr << "LOG: " << reinterpret_cast(attr.log_buf); } - return {false, elapsed_secs}; + return {false, seconds}; } - return {true, elapsed_secs}; + return {true, seconds}; } #endif 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/main/utils.hpp b/src/main/utils.hpp deleted file mode 100644 index 042dec059..000000000 --- a/src/main/utils.hpp +++ /dev/null @@ -1,16 +0,0 @@ -// Copyright (c) Prevail Verifier contributors. -// SPDX-License-Identifier: MIT - -#pragma once - -template -auto timed_execution(F f) { - const clock_t begin = clock(); - - const auto& res = f(); - - const clock_t end = clock(); - - double elapsed_secs = static_cast(end - begin) / CLOCKS_PER_SEC; - return std::make_tuple(res, elapsed_secs); -} diff --git a/src/spec_type_descriptors.hpp b/src/spec_type_descriptors.hpp index 89a7d537f..cc8523c76 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,11 +70,10 @@ 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); std::ostream& operator<<(std::ostream& os, const btf_line_info_t& line_info); -extern thread_local crab::lazy_allocator global_program_info; +extern thread_local crab::lazy_allocator thread_local_program_info; diff --git a/src/test/ebpf_yaml.cpp b/src/test/ebpf_yaml.cpp index ec02500c4..a822a6fef 100644 --- a/src/test/ebpf_yaml.cpp +++ b/src/test/ebpf_yaml.cpp @@ -171,13 +171,13 @@ static ebpf_verifier_options_t raw_options_to_options(const std::set& ra ebpf_verifier_options_t options{}; // Use ~simplify for YAML tests unless otherwise specified. - options.simplify = false; + options.verbosity_opts.simplify = false; // All YAML tests use !setup_constraints. options.setup_constraints = false; // Default to the machine's native endianness. - options.big_endian = (std::endian::native == std::endian::big); + options.big_endian = std::endian::native == std::endian::big; // Default to not assuming assertions. options.assume_assertions = false; @@ -193,7 +193,7 @@ static ebpf_verifier_options_t raw_options_to_options(const std::set& ra } else if (name == "strict") { options.strict = true; } else if (name == "simplify") { - options.simplify = true; + options.verbosity_opts.simplify = true; } else if (name == "big_endian") { options.big_endian = true; } else if (name == "!big_endian") { @@ -225,20 +225,6 @@ static vector read_suite(const string& path) { return res; } -static std::set extract_messages(const string& str) { - vector output; - boost::split(output, str, boost::is_any_of("\n")); - - std::set actual_messages; - for (auto& item : output) { - boost::trim(item); - if (!item.empty()) { - actual_messages.insert(item); - } - } - return actual_messages; -} - template static Diff make_diff(const T& actual, const T& expected) { return Diff{ @@ -248,27 +234,41 @@ static Diff make_diff(const T& actual, const T& expected) { } std::optional run_yaml_test_case(TestCase test_case, bool debug) { + test_case.options.verbosity_opts.print_failures = true; if (debug) { - test_case.options.print_failures = true; - test_case.options.print_invariants = true; - test_case.options.simplify = false; + test_case.options.verbosity_opts.print_invariants = true; } ebpf_context_descriptor_t context_descriptor{64, 0, 4, -1}; EbpfProgramType program_type = make_program_type(test_case.name, &context_descriptor); program_info info{&g_platform_test, {}, program_type}; + thread_local_options = test_case.options; + try { + const cfg_t cfg = prepare_cfg(test_case.instruction_seq, info, test_case.options.cfg_opts); + const Invariants invariants = analyze(cfg, test_case.assumed_pre_invariant); + const string_invariant actual_last_invariant = invariants.invariant_at(label_t::exit); + const std::set actual_messages = invariants.check_assertions(cfg).all_messages(); - 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); - std::set actual_messages = extract_messages(ss.str()); - - if (actual_last_invariant == test_case.expected_post_invariant && actual_messages == test_case.expected_messages) { - return {}; + if (actual_last_invariant == test_case.expected_post_invariant && + actual_messages == test_case.expected_messages) { + return {}; + } + return Failure{ + .invariant = make_diff(actual_last_invariant, test_case.expected_post_invariant), + .messages = make_diff(actual_messages, test_case.expected_messages), + }; + } catch (crab::InvalidControlFlow& ex) { + const std::set actual_messages{ex.what()}; + if (test_case.expected_post_invariant == string_invariant::top() && + actual_messages == test_case.expected_messages) { + return {}; + } + return Failure{ + .invariant = make_diff(string_invariant::top(), test_case.expected_post_invariant), + .messages = make_diff(actual_messages, test_case.expected_messages), + }; } - return Failure{.invariant = make_diff(actual_last_invariant, test_case.expected_post_invariant), - .messages = make_diff(actual_messages, test_case.expected_messages)}; } template @@ -358,64 +358,51 @@ ConformanceTestResult run_conformance_test_case(const std::vector& me ebpf_verifier_options_t options{}; if (debug) { print(prog, std::cout, {}); - options.print_failures = true; - options.print_invariants = true; - options.simplify = false; + options.verbosity_opts.print_failures = true; + options.verbosity_opts.print_invariants = true; + options.verbosity_opts.simplify = false; } + thread_local_options = options; 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()) { - if (invariant.rfind("r0.svalue=", 0) == 0) { - crab::number_t lb, ub; - if (invariant[10] == '[') { - lb = std::stoll(invariant.substr(11)); - ub = std::stoll(invariant.substr(invariant.find(',', 11) + 1)); - } else { - lb = ub = std::stoll(invariant.substr(10)); - } - return {result, crab::interval_t(lb, ub)}; - } - } - return {result, crab::interval_t::top()}; + const cfg_t cfg = prepare_cfg(prog, info, options.cfg_opts); + const Invariants invariants = analyze(cfg, pre_invariant); + return ConformanceTestResult{.success = invariants.verified(cfg), .r0_value = invariants.exit_value()}; } catch (const std::exception&) { // Catch exceptions thrown in ebpf_domain.cpp. return {}; } } -void print_failure(const Failure& failure, std::ostream& out) { +void print_failure(const Failure& failure, std::ostream& os) { constexpr auto INDENT = " "; if (!failure.invariant.unexpected.empty()) { - std::cout << "Unexpected properties:\n" << INDENT << failure.invariant.unexpected << "\n"; + os << "Unexpected properties:\n" << INDENT << failure.invariant.unexpected << "\n"; } else { - std::cout << "Unexpected properties: None\n"; + os << "Unexpected properties: None\n"; } if (!failure.invariant.unseen.empty()) { - std::cout << "Unseen properties:\n" << INDENT << failure.invariant.unseen << "\n"; + os << "Unseen properties:\n" << INDENT << failure.invariant.unseen << "\n"; } else { - std::cout << "Unseen properties: None\n"; + os << "Unseen properties: None\n"; } if (!failure.messages.unexpected.empty()) { - std::cout << "Unexpected messages:\n"; + os << "Unexpected messages:\n"; for (const auto& item : failure.messages.unexpected) { - std::cout << INDENT << item << "\n"; + os << INDENT << item << "\n"; } } else { - std::cout << "Unexpected messages: None\n"; + os << "Unexpected messages: None\n"; } if (!failure.messages.unseen.empty()) { - std::cout << "Unseen messages:\n"; + os << "Unseen messages:\n"; for (const auto& item : failure.messages.unseen) { - std::cout << INDENT << item << "\n"; + os << INDENT << item << "\n"; } } else { - std::cout << "Unseen messages: None\n"; + os << "Unseen messages: None\n"; } } diff --git a/src/test/ebpf_yaml.hpp b/src/test/ebpf_yaml.hpp index b427c5114..2803cdbf8 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::ostream& os = std::cout); 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..1dfaef318 100644 --- a/src/test/test_verify.cpp +++ b/src/test/test_verify.cpp @@ -32,53 +32,59 @@ FAIL_LOAD_ELF("invalid", "badsymsize.o", "xdp_redirect_map") 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) \ - do { \ - auto raw_progs = read_elf("ebpf-samples/" dirname "/" filename, sectionname, {}, platform); \ - REQUIRE(raw_progs.size() == 1); \ - raw_program raw_prog = raw_progs.back(); \ - 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); \ - } while (0) +#define FAIL_ANALYZE(dirname, filename, sectionname) \ + TEST_CASE("Try analyze bad program: " dirname "/" filename " " sectionname, "[cfg]") { \ + auto raw_progs = read_elf("ebpf-samples/" dirname "/" filename, sectionname, {}, &g_ebpf_platform_linux); \ + REQUIRE(raw_progs.size() == 1); \ + raw_program raw_prog = raw_progs.back(); \ + std::variant prog_or_error = unmarshal(raw_prog); \ + const auto prog = std::get_if(&prog_or_error); \ + REQUIRE(prog != nullptr); \ + cfg_t cfg = prepare_cfg(*prog, raw_prog.info, thread_local_options.cfg_opts); \ + REQUIRE_THROWS_AS(analyze(cfg), UnmarshalError); \ + } + +FAIL_ANALYZE("build", "badmapptr.o", "test") // 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, should_pass, count) \ + do { \ + thread_local_options = _options; \ + const auto raw_progs = read_elf("ebpf-samples/" dirname "/" filename, section_name, {}, platform); \ + REQUIRE(raw_progs.size() == count); \ + for (const auto& raw_prog : raw_progs) { \ + if (count == 1 || raw_prog.function_name == program_name) { \ + const auto prog_or_error = unmarshal(raw_prog); \ + const auto prog = std::get_if(&prog_or_error); \ + REQUIRE(prog != nullptr); \ + const cfg_t cfg = prepare_cfg(*prog, raw_prog.info, thread_local_options.cfg_opts); \ + REQUIRE(verify(cfg) == should_pass); \ + } \ + } \ } while (0) +// Verify a section with only one program in it. +#define VERIFY_SECTION(dirname, filename, section_name, _options, platform, should_pass) \ + VERIFY_PROGRAM(dirname, filename, section_name, "", _options, platform, should_pass, 1) + #define TEST_SECTION(project, filename, section) \ TEST_CASE(project "/" filename " " section, "[verify][samples][" project "]") { \ VERIFY_SECTION(project, filename, section, {}, &g_ebpf_platform_linux, true); \ } -#define TEST_PROGRAM(project, filename, section_name, program_name) \ - TEST_CASE(project "/" filename " " program_name, "[verify][samples][" project "]") { \ - VERIFY_PROGRAM(project, filename, section_name, program_name, {}, &g_ebpf_platform_linux, true); \ +#define TEST_PROGRAM(project, filename, section_name, program_name, count) \ + TEST_CASE(project "/" filename " " program_name, "[verify][samples][" project "]") { \ + VERIFY_PROGRAM(project, filename, section_name, program_name, {}, &g_ebpf_platform_linux, true, count); \ + } + +#define TEST_PROGRAM_REJECT(project, filename, section_name, program_name, count) \ + TEST_CASE(project "/" filename " " program_name, "[verify][samples][" project "]") { \ + VERIFY_PROGRAM(project, filename, section_name, program_name, {}, &g_ebpf_platform_linux, false, count); \ } -#define TEST_PROGRAM_REJECT(project, filename, section_name, program_name) \ - TEST_CASE(project "/" filename " " program_name, "[verify][samples][" project "]") { \ - VERIFY_PROGRAM(project, filename, section_name, program_name, {}, &g_ebpf_platform_linux, false); \ +#define TEST_PROGRAM_REJECT_FAIL(project, filename, section_name, program_name, count) \ + TEST_CASE(project "/" filename " " program_name, "[!shouldfail][verify][samples][" project "]") { \ + VERIFY_PROGRAM(project, filename, section_name, program_name, {}, &g_ebpf_platform_linux, false, count); \ } #define TEST_SECTION_REJECT(project, filename, section) \ @@ -114,6 +120,7 @@ FAIL_UNMARSHAL("invalid", "invalid-lddw.o", ".text") std::variant prog_or_error = unmarshal(raw_prog); \ REQUIRE(std::holds_alternative(prog_or_error)); \ } + #define TEST_SECTION_LEGACY(dirname, filename, sectionname) \ TEST_SECTION(dirname, filename, sectionname) \ TEST_LEGACY(dirname, filename, sectionname) @@ -500,8 +507,10 @@ TEST_SECTION("raw_tracepoint/filler/sys_sendmsg_x") TEST_SECTION("raw_tracepoint/filler/proc_startupdate_2") TEST_SECTION("raw_tracepoint/filler/sys_recvfrom_x") */ -TEST_PROGRAM_REJECT("build", "bpf2bpf.o", ".text", "plus1"); // Subprogram will fail verification. -TEST_PROGRAM("build", "bpf2bpf.o", "test", "func"); // Subprogram can be called from main program. + +TEST_PROGRAM_REJECT_FAIL("build", "bpf2bpf.o", ".text", "plus1", 1); // Subprogram should fail verification. +TEST_PROGRAM("build", "bpf2bpf.o", "test", "func", 1); // Subprogram can be called from main program. + TEST_SECTION("build", "byteswap.o", ".text") TEST_SECTION("build", "stackok.o", ".text") TEST_SECTION("build", "packet_start_ok.o", "xdp") @@ -514,16 +523,15 @@ TEST_SECTION("build", "store_map_value_in_map.o", ".text") TEST_SECTION("build", "twomaps.o", ".text"); TEST_SECTION("build", "twostackvars.o", ".text"); TEST_SECTION("build", "twotypes.o", ".text"); -TEST_PROGRAM("build", "prog_array.o", ".text", "func"); -TEST_PROGRAM("build", "prog_array.o", ".text", "func0"); -TEST_PROGRAM("build", "prog_array.o", ".text", "func1"); -TEST_PROGRAM("build", "prog_array.o", ".text", "func2"); -TEST_PROGRAM("build", "prog_array.o", ".text", "func3"); +TEST_PROGRAM("build", "prog_array.o", ".text", "func", 5); +TEST_PROGRAM("build", "prog_array.o", ".text", "func0", 5); +TEST_PROGRAM("build", "prog_array.o", ".text", "func1", 5); +TEST_PROGRAM("build", "prog_array.o", ".text", "func2", 5); +TEST_PROGRAM("build", "prog_array.o", ".text", "func3", 5); // Test some programs that ought to fail verification. TEST_SECTION_REJECT("build", "badhelpercall.o", ".text") TEST_SECTION_REJECT("build", "ctxoffset.o", "sockops") -TEST_SECTION_REJECT("build", "badmapptr.o", "test") TEST_SECTION_FAIL("build", "dependent_read.o", "xdp") TEST_SECTION_REJECT("build", "exposeptr.o", ".text") TEST_SECTION_REJECT("build", "exposeptr2.o", ".text") @@ -595,7 +603,8 @@ 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); + thread_local_program_info.set(*info); + *res = verify(*cfg); } // Test multithreading 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..2aa159e81 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:3: Code becomes unreachable (assume r0 <= 0)" - "2 (counter): Loop counter is too large (pc[2] < 100000)" - - "2:3: Code is unreachable after 2:3" 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]"]