diff --git a/src/asm_cfg.cpp b/src/asm_cfg.cpp index d1fb4a7b8..cd1ade2a1 100644 --- a/src/asm_cfg.cpp +++ b/src/asm_cfg.cpp @@ -18,13 +18,36 @@ using std::string; using std::to_string; using std::vector; -static optional get_jump(Instruction ins) { - if (const auto pins = std::get_if(&ins)) { - return pins->target; +/// Get the inverse of a given comparison operation. +static Condition::Op reverse(const Condition::Op op) { + switch (op) { + case Condition::Op::EQ: return Condition::Op::NE; + case Condition::Op::NE: return Condition::Op::EQ; + + case Condition::Op::GE: return Condition::Op::LT; + case Condition::Op::LT: return Condition::Op::GE; + + case Condition::Op::SGE: return Condition::Op::SLT; + case Condition::Op::SLT: return Condition::Op::SGE; + + case Condition::Op::LE: return Condition::Op::GT; + case Condition::Op::GT: return Condition::Op::LE; + + case Condition::Op::SLE: return Condition::Op::SGT; + case Condition::Op::SGT: return Condition::Op::SLE; + + case Condition::Op::SET: return Condition::Op::NSET; + case Condition::Op::NSET: return Condition::Op::SET; } + assert(false); return {}; } +/// Get the inverse of a given comparison condition. +static Condition reverse(const Condition& cond) { + return {.op = reverse(cond.op), .left = cond.left, .right = cond.right, .is64 = cond.is64}; +} + static bool has_fall(const Instruction& ins) { if (std::holds_alternative(ins)) { return false; @@ -44,17 +67,15 @@ static void add_cfg_nodes(cfg_t& cfg, const label_t& caller_label, const label_t bool first = true; // Get the label of the node to go to on returning from the macro. - basic_block_t& exit_to_node = cfg.get_node(cfg.next_nodes(caller_label).front()); + crab::value_t& exit_to_node = cfg.get_node(cfg.next_nodes(caller_label).front()); // Construct the variable prefix to use for the new stack frame, // and store a copy in the CallLocal instruction since the instruction-specific // labels may only exist until the CFG is simplified. - basic_block_t& caller_node = cfg.get_node(caller_label); + crab::value_t& caller_node = cfg.get_node(caller_label); const std::string stack_frame_prefix = to_string(caller_label); - for (auto& inst : caller_node) { - if (const auto pcall = std::get_if(&inst.cmd)) { - pcall->stack_frame_prefix = stack_frame_prefix; - } + if (const auto pcall = std::get_if(&caller_node.instruction().cmd)) { + pcall->stack_frame_prefix = stack_frame_prefix; } // Walk the transitive closure of CFG nodes starting at entry_label and ending at @@ -71,15 +92,13 @@ static void add_cfg_nodes(cfg_t& cfg, const label_t& caller_label, const label_t // Clone the macro block into a new block with the new stack frame prefix. const label_t label{macro_label.from, macro_label.to, stack_frame_prefix}; - auto& bb = cfg.insert(label); - for (auto inst : cfg.get_node(macro_label)) { - if (const auto pexit = std::get_if(&inst.cmd)) { - pexit->stack_frame_prefix = label.stack_frame_prefix; - } else if (const auto pcall = std::get_if(&inst.cmd)) { - pcall->stack_frame_prefix = label.stack_frame_prefix; - } - bb.insert(inst); + auto inst = cfg.at(macro_label); + if (const auto pexit = std::get_if(&inst.cmd)) { + pexit->stack_frame_prefix = label.stack_frame_prefix; + } else if (const auto pcall = std::get_if(&inst.cmd)) { + pcall->stack_frame_prefix = label.stack_frame_prefix; } + crab::value_t& bb = cfg.insert(label, inst.cmd); if (first) { // Add an edge from the caller to the new block. @@ -121,14 +140,12 @@ static void add_cfg_nodes(cfg_t& cfg, const label_t& caller_label, const label_t string caller_label_str = to_string(caller_label); const long stack_frame_depth = std::ranges::count(caller_label_str, STACK_FRAME_DELIMITER) + 2; for (const auto& macro_label : seen_labels) { - for (const label_t label(macro_label.from, macro_label.to, caller_label_str); - const auto& inst : cfg.get_node(label)) { - if (const auto pins = std::get_if(&inst.cmd)) { - if (stack_frame_depth >= MAX_CALL_STACK_FRAMES) { - throw std::runtime_error{"too many call stack frames"}; - } - add_cfg_nodes(cfg, label, pins->target); + 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"}; } + add_cfg_nodes(cfg, label, pins->target); } } } @@ -136,44 +153,67 @@ static void add_cfg_nodes(cfg_t& cfg, const label_t& caller_label, const label_t /// Convert an instruction sequence to a control-flow graph (CFG). static cfg_t instruction_seq_to_cfg(const InstructionSeq& insts, const bool must_have_exit) { cfg_t cfg; - std::optional falling_from = {}; - bool first = true; - // Do a first pass ignoring all function macro calls. + // First add all instructions to the CFG without connecting for (const auto& [label, inst, _] : insts) { - if (std::holds_alternative(inst)) { continue; } + cfg.insert(label, inst); + } - auto& bb = cfg.insert(label); + if (insts.size() == 0) { + throw std::invalid_argument{"empty instruction sequence"}; + } else { + const auto& [label, inst, _0] = insts[0]; + cfg.get_node(cfg.entry_label()) >> cfg.get_node(label); + } - if (first) { - first = false; - cfg.get_node(cfg.entry_label()) >> bb; - } + // Do a first pass ignoring all function macro calls. + for (size_t i = 0; i < insts.size(); i++) { + const auto& [label, inst, _0] = insts[i]; - bb.insert({.cmd = inst}); - if (falling_from) { - cfg.get_node(*falling_from) >> bb; - falling_from = {}; - } - if (has_fall(inst)) { - falling_from = label; - } - if (auto jump_target = get_jump(inst)) { - bb >> cfg.insert(*jump_target); + if (std::holds_alternative(inst)) { + continue; } + auto& value = cfg.get_node(label); - if (std::holds_alternative(inst)) { - bb >> cfg.get_node(cfg.exit_label()); + label_t fallthrough{cfg.exit_label()}; + if (i + 1 < insts.size()) { + fallthrough = std::get<0>(insts[i + 1]); + } else { + if (has_fall(inst) && must_have_exit) { + throw std::invalid_argument{"fallthrough in last instruction"}; + } } - } - if (falling_from) { - if (must_have_exit) { - throw std::invalid_argument{"fallthrough in last instruction"}; + if (const auto jmp = std::get_if(&inst)) { + if (const auto cond = jmp->cond) { + label_t target_label = jmp->target; + if (target_label == fallthrough) { + value >> cfg.get_node(fallthrough); + continue; + } + + vector> jumps{ + {target_label, *cond}, + {fallthrough, reverse(*cond)}, + }; + for (const auto& [next_label, cond1] : jumps) { + label_t jump_label = label_t::make_jump(label, next_label); + crab::value_t& jump_node = cfg.insert(jump_label, Assume{.cond = cond1, .is_explicit = false}); + value >> jump_node; + jump_node >> cfg.get_node(next_label); + } + } else { + value >> cfg.get_node(jmp->target); + } } else { - cfg.get_node(*falling_from) >> cfg.get_node(cfg.exit_label()); + if (has_fall(inst)) { + value >> cfg.get_node(fallthrough); + } + } + if (std::holds_alternative(inst)) { + value >> cfg.get_node(cfg.exit_label()); } } @@ -189,34 +229,24 @@ static cfg_t instruction_seq_to_cfg(const InstructionSeq& insts, const bool must return cfg; } -/// Get the inverse of a given comparison operation. -static Condition::Op reverse(const Condition::Op op) { - switch (op) { - case Condition::Op::EQ: return Condition::Op::NE; - case Condition::Op::NE: return Condition::Op::EQ; - - case Condition::Op::GE: return Condition::Op::LT; - case Condition::Op::LT: return Condition::Op::GE; - - case Condition::Op::SGE: return Condition::Op::SLT; - case Condition::Op::SLT: return Condition::Op::SGE; - - case Condition::Op::LE: return Condition::Op::GT; - case Condition::Op::GT: return Condition::Op::LE; - - case Condition::Op::SLE: return Condition::Op::SGT; - case Condition::Op::SGT: return Condition::Op::SLE; +cfg_t prepare_cfg(const InstructionSeq& prog, const program_info& info, const prepare_cfg_options& options) { + // Convert the instruction sequence to a deterministic control-flow graph. + cfg_t cfg = instruction_seq_to_cfg(prog, options.must_have_exit); - case Condition::Op::SET: return Condition::Op::NSET; - case Condition::Op::NSET: return Condition::Op::SET; + // Detect loops using Weak Topological Ordering (WTO) and insert counters at loop entry points. WTO provides a + // hierarchical decomposition of the CFG that identifies all strongly connected components (cycles) and their entry + // points. These entry points serve as natural locations for loop counters that help verify program termination. + if (options.check_for_termination) { + const wto_t wto{cfg}; + wto.for_each_loop_head([&](const label_t& label) -> void { + cfg.insert_after(label, label_t::make_increment_counter(label), IncrementLoopCounter{label}); + }); } - assert(false); - return {}; -} -/// Get the inverse of a given comparison condition. -static Condition reverse(const Condition& cond) { - return {.op = reverse(cond.op), .left = cond.left, .right = cond.right, .is64 = cond.is64}; + // Annotate the CFG by adding in assertions before every memory instruction. + explicate_assertions(cfg, info); + + return cfg; } template @@ -226,53 +256,6 @@ static vector unique(const std::pair& be) { return res; } -/// Get a non-deterministic version of a control-flow graph, -/// i.e., where instead of using if/else, both branches are taken -/// simultaneously, and are replaced by Assume instructions -/// immediately after the branch. -static cfg_t to_nondet(const cfg_t& cfg) { - cfg_t res; - for (const auto& [this_label, bb] : cfg) { - basic_block_t& newbb = res.insert(this_label); - - for (const auto& ins : bb) { - newbb.insert(ins); - } - - for (const label_t& prev_label : bb.prev_blocks_set()) { - bool is_one = cfg.get_node(prev_label).next_blocks_set().size() > 1; - basic_block_t& pbb = res.insert(is_one ? label_t::make_jump(prev_label, this_label) : prev_label); - pbb >> newbb; - } - // note the special case where we jump to fallthrough - auto nextlist = bb.next_blocks_set(); - if (nextlist.size() == 2) { - label_t mid_label = this_label; - auto jmp = std::get(bb.rbegin()->cmd); - - nextlist.erase(jmp.target); - label_t fallthrough = *nextlist.begin(); - - vector> jumps{ - {jmp.target, *jmp.cond}, - {fallthrough, reverse(*jmp.cond)}, - }; - for (const auto& [next_label, cond1] : jumps) { - label_t jump_label = label_t::make_jump(mid_label, next_label); - basic_block_t& jump_bb = res.insert(jump_label); - jump_bb.insert({.cmd = Assume{cond1}}); - newbb >> jump_bb; - jump_bb >> res.insert(next_label); - } - } else { - for (const auto& label : nextlist) { - newbb >> res.insert(label); - } - } - } - return res; -} - /// Get the type of given Instruction. /// Most of these type names are also statistics header labels. static std::string instype(Instruction ins) { @@ -329,62 +312,28 @@ std::map collect_stats(const cfg_t& cfg) { } for (const auto& this_label : cfg.labels()) { res["basic_blocks"]++; - basic_block_t const& bb = cfg.get_node(this_label); - - for (const auto& ins : bb) { - if (const auto pins = std::get_if(&ins.cmd)) { - if (pins->mapfd == -1) { - res["map_in_map"] = 1; - } + const crab::value_t& value = cfg.get_node(this_label); + const auto cmd = value.instruction().cmd; + if (const auto pins = std::get_if(&cmd)) { + if (pins->mapfd == -1) { + res["map_in_map"] = 1; } - if (const auto pins = std::get_if(&ins.cmd)) { - if (pins->reallocate_packet) { - res["reallocate"] = 1; - } - } - if (const auto pins = std::get_if(&ins.cmd)) { - res[pins->is64 ? "arith64" : "arith32"]++; + } + if (const auto pins = std::get_if(&cmd)) { + if (pins->reallocate_packet) { + res["reallocate"] = 1; } - res[instype(ins.cmd)]++; } - if (unique(bb.prev_blocks()).size() > 1) { + if (const auto pins = std::get_if(&cmd)) { + res[pins->is64 ? "arith64" : "arith32"]++; + } + res[instype(cmd)]++; + if (unique(value.prev_labels()).size() > 1) { res["joins"]++; } - if (unique(bb.prev_blocks()).size() > 1) { + if (unique(value.prev_labels()).size() > 1) { res["jumps"]++; } } return res; } - -cfg_t prepare_cfg(const InstructionSeq& prog, const program_info& info, const prepare_cfg_options& options) { - // Convert the instruction sequence to a deterministic control-flow graph. - cfg_t det_cfg = instruction_seq_to_cfg(prog, options.must_have_exit); - - // Detect loops using Weak Topological Ordering (WTO) and insert counters at loop entry points. WTO provides a - // hierarchical decomposition of the CFG that identifies all strongly connected components (cycles) and their entry - // points. These entry points serve as natural locations for loop counters that help verify program termination. - if (options.check_for_termination) { - const wto_t wto(det_cfg); - wto.for_each_loop_head( - [&](const label_t& label) { det_cfg.get_node(label).insert_front({.cmd = IncrementLoopCounter{label}}); }); - } - - // Annotate the CFG by adding in assertions before every memory instruction. - explicate_assertions(det_cfg, info); - - // Translate conditional jumps to non-deterministic jumps. - cfg_t cfg = to_nondet(det_cfg); - - // Except when debugging, combine chains of instructions into - // basic blocks where possible, i.e., into a range of instructions - // where there is a single entry point and a single exit point. - // An abstract interpreter will keep values at every basic block, - // so the fewer basic blocks we have, the less information it has to - // keep track of. - if (options.simplify) { - cfg.simplify(); - } - - return cfg; -} diff --git a/src/asm_marshal.cpp b/src/asm_marshal.cpp index 9ce4d2f09..953435b70 100644 --- a/src/asm_marshal.cpp +++ b/src/asm_marshal.cpp @@ -6,7 +6,6 @@ #include #include "asm_marshal.hpp" -#include "asm_ostream.hpp" #include "crab_utils/num_safety.hpp" using std::vector; @@ -293,7 +292,7 @@ struct MarshalVisitor { }; vector marshal(const Instruction& ins, const pc_t pc) { - return std::visit(MarshalVisitor{label_to_offset16(pc), label_to_offset32(pc)}, ins); + return std::visit(MarshalVisitor{crab::label_to_offset16(pc), crab::label_to_offset32(pc)}, ins); } static int size(const Instruction& inst) { diff --git a/src/asm_ostream.cpp b/src/asm_ostream.cpp index f76e023e1..ddd7022c6 100644 --- a/src/asm_ostream.cpp +++ b/src/asm_ostream.cpp @@ -6,12 +6,12 @@ #include #include -#include "asm_ostream.hpp" #include "asm_syntax.hpp" #include "crab/cfg.hpp" #include "crab/interval.hpp" #include "crab/type_encoding.hpp" #include "crab/variable.hpp" +#include "crab_utils/num_big.hpp" #include "helpers.hpp" #include "platform.hpp" #include "spec_type_descriptors.hpp" @@ -21,6 +21,113 @@ using std::optional; using std::string; using std::vector; +namespace crab { + +std::string number_t::to_string() const { return _n.str(); } + +std::string interval_t::to_string() const { + std::ostringstream s; + s << *this; + return s.str(); +} + +std::ostream& operator<<(std::ostream& os, const label_t& label) { + if (label == label_t::entry) { + return os << "entry"; + } + if (label == label_t::exit) { + return os << "exit"; + } + if (!label.stack_frame_prefix.empty()) { + os << label.stack_frame_prefix << STACK_FRAME_DELIMITER; + } + os << label.from; + if (label.to != -1) { + os << ":" << label.to; + } + if (!label.special_label.empty()) { + os << " (" << label.special_label << ")"; + } + return os; +} + +string to_string(label_t const& label) { + std::stringstream str; + str << label; + return str.str(); +} + +void print_dot(const cfg_t& cfg, std::ostream& out) { + out << "digraph program {\n"; + out << " node [shape = rectangle];\n"; + for (const auto& label : cfg.labels()) { + out << " \"" << label << "\"[xlabel=\"" << label << "\",label=\""; + + const auto& value = cfg.get_node(label); + const auto& ins = value.instruction(); + for (const auto& pre : ins.preconditions) { + out << "assert " << pre << "\\l"; + } + out << ins.cmd << "\\l"; + + out << "\"];\n"; + for (const label_t& next : value.next_labels_set()) { + out << " \"" << label << "\" -> \"" << next << "\";\n"; + } + out << "\n"; + } + out << "}\n"; +} + +void print_dot(const cfg_t& cfg, const std::string& outfile) { + std::ofstream out{outfile}; + if (out.fail()) { + throw std::runtime_error(std::string("Could not open file ") + outfile); + } + print_dot(cfg, out); +} + +std::ostream& operator<<(std::ostream& o, const value_t& value) { + o << value.label() << ":\n"; + const auto ins = value.instruction(); + for (const auto& pre : ins.preconditions) { + o << " " + << "assert " << pre << ";\n"; + } + o << " " << ins.cmd << ";\n"; + auto [it, et] = value.next_labels(); + if (it != et) { + o << " " + << "goto "; + while (it != et) { + o << *it; + ++it; + if (it == et) { + o << ";"; + } else { + o << ","; + } + } + } + o << "\n"; + return o; +} + +std::ostream& operator<<(std::ostream& o, const cfg_t& cfg) { + for (const label_t& label : cfg.sorted_labels()) { + o << cfg.get_node(label); + o << "edges to:"; + for (const label_t& next_label : cfg.next_nodes(label)) { + o << " " << next_label; + } + o << "\n"; + } + return o; +} + +} // namespace crab + +namespace asm_syntax { std::ostream& operator<<(std::ostream& os, const ArgSingle::Kind kind) { switch (kind) { case ArgSingle::Kind::ANYTHING: return os << "uint64_t"; @@ -355,12 +462,6 @@ struct CommandPrinterVisitor { }; // ReSharper restore CppMemberFunctionMayBeConst -string to_string(label_t const& label) { - std::stringstream str; - str << label; - return str.str(); -} - std::ostream& operator<<(std::ostream& os, Instruction const& ins) { std::visit(CommandPrinterVisitor{os}, ins); return os; @@ -433,7 +534,7 @@ void print(const InstructionSeq& insts, std::ostream& out, const std::optional(&ins)) { if (!pc_of_label.contains(jmp->target)) { - throw std::runtime_error(string("Cannot find label ") + to_string(jmp->target)); + throw std::runtime_error(string("Cannot find label ") + crab::to_string(jmp->target)); } const pc_t target_pc = pc_of_label.at(jmp->target); visitor(*jmp, target_pc - static_cast(pc) - 1); @@ -446,6 +547,8 @@ void print(const InstructionSeq& insts, std::ostream& out, const std::optional& descriptors, st } } -void print_dot(const cfg_t& cfg, std::ostream& out) { - out << "digraph program {\n"; - out << " node [shape = rectangle];\n"; - for (const auto& label : cfg.labels()) { - out << " \"" << label << "\"[xlabel=\"" << label << "\",label=\""; - - const auto& bb = cfg.get_node(label); - for (const auto& ins : bb) { - for (const auto& pre : ins.preconditions) { - out << "assert " << pre << "\\l"; - } - out << ins.cmd << "\\l"; - } - - out << "\"];\n"; - for (const label_t& next : bb.next_blocks_set()) { - out << " \"" << label << "\" -> \"" << next << "\";\n"; - } - out << "\n"; - } - out << "}\n"; -} - -void print_dot(const cfg_t& cfg, const std::string& outfile) { - std::ofstream out{outfile}; - if (out.fail()) { - throw std::runtime_error(std::string("Could not open file ") + outfile); - } - print_dot(cfg, out); -} - -std::ostream& operator<<(std::ostream& o, const basic_block_t& bb) { - o << bb.label() << ":\n"; - for (const auto& s : bb) { - for (const auto& pre : s.preconditions) { - o << " " - << "assert " << pre << ";\n"; - } - o << " " << s.cmd << ";\n"; - } - auto [it, et] = bb.next_blocks(); - if (it != et) { - o << " " - << "goto "; - while (it != et) { - o << *it; - ++it; - if (it == et) { - o << ";"; - } else { - o << ","; - } - } - } - o << "\n"; - return o; -} - -std::ostream& operator<<(std::ostream& o, const crab::basic_block_rev_t& bb) { - o << bb.label() << ":\n"; - for (const auto& s : bb) { - for (const auto& pre : s.preconditions) { - o << " " - << "assert " << pre << ";\n"; - } - o << " " << s.cmd << ";\n"; - } - o << "--> ["; - for (const label_t& label : bb.next_blocks_set()) { - o << label << ";"; - } - o << "]\n"; - return o; -} - -std::ostream& operator<<(std::ostream& o, const cfg_t& cfg) { - for (const label_t& label : cfg.sorted_labels()) { - o << cfg.get_node(label); - o << "edges to:"; - for (const label_t& next_label : cfg.next_nodes(label)) { - o << " " << next_label; - } - o << "\n"; - } - return o; -} - std::ostream& operator<<(std::ostream& os, const btf_line_info_t& line_info) { os << "; " << line_info.file_name << ":" << line_info.line_number << "\n"; os << "; " << line_info.source_line << "\n"; return os; } - -std::string crab::number_t::to_string() const { return _n.str(); } - -std::string crab::interval_t::to_string() const { - std::ostringstream s; - s << *this; - return s.str(); -} diff --git a/src/asm_ostream.hpp b/src/asm_ostream.hpp deleted file mode 100644 index 5f9d0e190..000000000 --- a/src/asm_ostream.hpp +++ /dev/null @@ -1,58 +0,0 @@ -// Copyright (c) Prevail Verifier contributors. -// SPDX-License-Identifier: MIT -#pragma once - -#include -#include -#include - -#include - -#include "asm_syntax.hpp" -#include "crab_utils/num_safety.hpp" - -// We use a 16-bit offset whenever it fits in 16 bits. -inline std::function label_to_offset16(const pc_t pc) { - return [=](const label_t& label) { - const int64_t offset = label.from - gsl::narrow(pc) - 1; - const bool is16 = - std::numeric_limits::min() <= offset && offset <= std::numeric_limits::max(); - return gsl::narrow(is16 ? offset : 0); - }; -} - -// We use the JA32 opcode with the offset in 'imm' when the offset -// of an unconditional jump doesn't fit in an int16_t. -inline std::function label_to_offset32(const pc_t pc) { - return [=](const label_t& label) { - const int64_t offset = label.from - gsl::narrow(pc) - 1; - const bool is16 = - std::numeric_limits::min() <= offset && offset <= std::numeric_limits::max(); - return is16 ? 0 : gsl::narrow(offset); - }; -} - -std::ostream& operator<<(std::ostream& os, const btf_line_info_t& line_info); - -void print(const InstructionSeq& insts, std::ostream& out, const std::optional& label_to_print, - bool print_line_info = false); - -std::string to_string(label_t const& label); - -std::ostream& operator<<(std::ostream& os, Instruction const& ins); -std::string to_string(Instruction const& ins); - -std::ostream& operator<<(std::ostream& os, Bin::Op op); -std::ostream& operator<<(std::ostream& os, Condition::Op op); - -inline std::ostream& operator<<(std::ostream& os, const Imm imm) { return os << crab::to_signed(imm.v); } -inline std::ostream& operator<<(std::ostream& os, Reg const& a) { return os << "r" << gsl::narrow(a.v); } -inline std::ostream& operator<<(std::ostream& os, Value const& a) { - if (const auto pa = std::get_if(&a)) { - return os << *pa; - } - return os << std::get(a); -} - -std::ostream& operator<<(std::ostream& os, const Assertion& a); -std::string to_string(const Assertion& constraint); diff --git a/src/asm_parse.cpp b/src/asm_parse.cpp index 792d6ef43..50c99efdc 100644 --- a/src/asm_parse.cpp +++ b/src/asm_parse.cpp @@ -208,8 +208,12 @@ Instruction parse_instruction(const std::string& line, const std::map +#include #include #include #include #include #include -#include "crab/variable.hpp" +#include "crab/label.hpp" +#include "crab/type_encoding.hpp" +#include "crab_utils/num_safety.hpp" #include "spec_type_descriptors.hpp" -constexpr char STACK_FRAME_DELIMITER = '/'; - -namespace crab { -struct label_t { - int from; ///< Jump source, or simply index of instruction - int to; ///< Jump target or -1 - std::string stack_frame_prefix; ///< Variable prefix when calling this label. - - explicit label_t(const int index, const int to = -1, std::string stack_frame_prefix = {}) noexcept - : from(index), to(to), stack_frame_prefix(std::move(stack_frame_prefix)) {} - - static label_t make_jump(const label_t& src_label, const label_t& target_label) { - return label_t{src_label.from, target_label.from, target_label.stack_frame_prefix}; - } - - bool operator==(const label_t& other) const noexcept = default; - - constexpr bool operator<(const label_t& other) const { - if (this == &other) { - return false; - } - if (*this == label_t::exit) { - return false; - } - if (other == label_t::exit) { - return true; - } - return (stack_frame_prefix < other.stack_frame_prefix || - (stack_frame_prefix == other.stack_frame_prefix && - (from < other.from || (from == other.from && to < other.to)))); - } - - // no hash; intended for use in ordered containers. - - [[nodiscard]] - constexpr bool isjump() const { - return to != -1; - } - - [[nodiscard]] - int call_stack_depth() const { - // The call stack depth is the number of '/' separated components in the label, - // which is one more than the number of '/' separated components in the prefix, - // hence two more than the number of '/' in the prefix, if any. - if (stack_frame_prefix.empty()) { - return 1; - } - return gsl::narrow(2 + std::ranges::count(stack_frame_prefix, STACK_FRAME_DELIMITER)); - } - - friend std::ostream& operator<<(std::ostream& os, const label_t& label) { - if (label == entry) { - return os << "entry"; - } - if (label == exit) { - return os << "exit"; - } - if (!label.stack_frame_prefix.empty()) { - os << label.stack_frame_prefix << STACK_FRAME_DELIMITER; - } - if (label.to == -1) { - return os << label.from; - } - return os << label.from << ":" << label.to; - } - - static const label_t entry; - static const label_t exit; -}; - -inline const label_t label_t::entry{-1}; -inline const label_t label_t::exit{-2}; - -} // namespace crab using crab::label_t; // Assembly syntax. @@ -307,6 +236,10 @@ struct Undefined { /// the branch and before each jump target. struct Assume { Condition cond; + + // True if the condition is explicitly written in the program (for tests). + bool is_explicit{}; + constexpr bool operator==(const Assume&) const = default; }; @@ -426,12 +359,31 @@ struct GuardedInstruction { bool operator==(const GuardedInstruction&) const = default; }; -// cpu=v4 supports 32-bit PC offsets so we need a large enough type. -using pc_t = uint32_t; +std::ostream& operator<<(std::ostream& os, Instruction const& ins); +std::string to_string(Instruction const& ins); + +std::ostream& operator<<(std::ostream& os, Bin::Op op); +std::ostream& operator<<(std::ostream& os, Condition::Op op); + +inline std::ostream& operator<<(std::ostream& os, const Imm imm) { return os << crab::to_signed(imm.v); } +inline std::ostream& operator<<(std::ostream& os, Reg const& a) { return os << "r" << gsl::narrow(a.v); } +inline std::ostream& operator<<(std::ostream& os, Value const& a) { + if (const auto pa = std::get_if(&a)) { + return os << *pa; + } + return os << std::get(a); +} + +std::ostream& operator<<(std::ostream& os, const Assertion& a); +std::string to_string(const Assertion& constraint); + +void print(const InstructionSeq& insts, std::ostream& out, const std::optional& label_to_print, + bool print_line_info = false); } // namespace asm_syntax using namespace asm_syntax; +using crab::pc_t; template struct overloaded : Ts... { diff --git a/src/assertions.cpp b/src/assertions.cpp index 96ce593e5..faebc9579 100644 --- a/src/assertions.cpp +++ b/src/assertions.cpp @@ -38,7 +38,7 @@ class AssertExtractor { : info{std::move(info)}, current_label(label) {} vector operator()(const Undefined&) const { - assert(false); + // assert(false); return {}; } @@ -176,7 +176,12 @@ class AssertExtractor { return res; } - vector operator()(const Assume& ins) const { return explicate(ins.cond); } + vector operator()(const Assume& ins) const { + if (ins.is_explicit) { + return explicate(ins.cond); + } + return {}; + } vector operator()(const Jmp& ins) const { if (!ins.cond) { @@ -298,10 +303,9 @@ vector get_assertions(Instruction ins, const program_info& info, cons /// regions. The verifier will use these assertions to treat the program as /// unsafe unless it can prove that the assertions can never fail. void explicate_assertions(cfg_t& cfg, const program_info& info) { - for (auto& [label, bb] : cfg) { + for (auto& [label, value] : cfg) { (void)label; // unused - for (auto& ins : bb) { - ins.preconditions = get_assertions(ins.cmd, info, bb.label()); - } + auto& ins = value.instruction(); + ins.preconditions = get_assertions(ins.cmd, info, value.label()); } } diff --git a/src/config.hpp b/src/config.hpp index b109a35c8..09d5d919e 100644 --- a/src/config.hpp +++ b/src/config.hpp @@ -8,6 +8,9 @@ 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; @@ -20,7 +23,7 @@ struct ebpf_verifier_options_t { // True to allow division by zero and assume BPF ISA defined semantics. bool allow_division_by_zero = true; - // Setup the entry constraints for a BPF program. + // Set up the entry constraints for a BPF program. bool setup_constraints = true; // True if the ELF file is built on a big endian system. diff --git a/src/crab/cfg.hpp b/src/crab/cfg.hpp index 8dd6e9ba0..678d1312e 100644 --- a/src/crab/cfg.hpp +++ b/src/crab/cfg.hpp @@ -3,14 +3,7 @@ #pragma once /* - * Build a CFG to interface with the abstract domains and fixpoint - * iterators. - * - * All the CFG statements are strongly typed. However, only variables - * need to be typed. The types of constants can be inferred from the - * context since they always appear together with at least one - * variable. - * + * Build a CFG to interface with the abstract domains and fixpoint iterators. */ #include #include @@ -22,7 +15,6 @@ #include #include -#include "asm_ostream.hpp" #include "asm_syntax.hpp" #include "crab_utils/debug.hpp" #include "crab_utils/num_big.hpp" @@ -32,103 +24,68 @@ namespace crab { class cfg_t; -class basic_block_t final { +// Node type for the CFG +class value_t final { friend class cfg_t; public: - basic_block_t(const basic_block_t&) = delete; + value_t(const value_t&) = delete; using label_vec_t = std::set; - using stmt_list_t = std::vector; using neighbour_const_iterator = label_vec_t::const_iterator; using neighbour_const_reverse_iterator = label_vec_t::const_reverse_iterator; - using iterator = stmt_list_t::iterator; - using const_iterator = stmt_list_t::const_iterator; - using reverse_iterator = stmt_list_t::reverse_iterator; - using const_reverse_iterator = stmt_list_t::const_reverse_iterator; private: label_t m_label; - stmt_list_t m_ts; + GuardedInstruction m_instruction{.cmd = Undefined{}}; label_vec_t m_prev, m_next; public: - void insert(const GuardedInstruction& arg) { - assert(label() != label_t::entry); - assert(label() != label_t::exit); - m_ts.push_back(arg); - } + explicit value_t(label_t _label) : m_label{std::move(_label)} {} - /// Insert a GuardedInstruction at the front of the basic block. - /// @note Cannot modify entry or exit blocks. - void insert_front(const GuardedInstruction& arg) { - assert(label() != label_t::entry); - assert(label() != label_t::exit); - m_ts.insert(m_ts.begin(), arg); - } - - explicit basic_block_t(label_t _label) : m_label(std::move(_label)) {} - - ~basic_block_t() = default; + ~value_t() = default; [[nodiscard]] label_t label() const { return m_label; } - iterator begin() { return (m_ts.begin()); } - iterator end() { return (m_ts.end()); } [[nodiscard]] - const_iterator begin() const { - return (m_ts.begin()); - } - [[nodiscard]] - const_iterator end() const { - return (m_ts.end()); + GuardedInstruction& instruction() { + return m_instruction; } - reverse_iterator rbegin() { return (m_ts.rbegin()); } - reverse_iterator rend() { return (m_ts.rend()); } [[nodiscard]] - const_reverse_iterator rbegin() const { - return (m_ts.rbegin()); - } - [[nodiscard]] - const_reverse_iterator rend() const { - return (m_ts.rend()); - } - - [[nodiscard]] - size_t size() const { - return gsl::narrow(std::distance(begin(), end())); + const GuardedInstruction& instruction() const { + return m_instruction; } [[nodiscard]] - std::pair next_blocks() const { + std::pair next_labels() const { return std::make_pair(m_next.begin(), m_next.end()); } [[nodiscard]] - std::pair next_blocks_reversed() const { + std::pair next_labels_reversed() const { return std::make_pair(m_next.rbegin(), m_next.rend()); } [[nodiscard]] - std::pair prev_blocks() const { + std::pair prev_labels() const { return std::make_pair(m_prev.begin(), m_prev.end()); } [[nodiscard]] - const label_vec_t& next_blocks_set() const { + const label_vec_t& next_labels_set() const { return m_next; } [[nodiscard]] - const label_vec_t& prev_blocks_set() const { + const label_vec_t& prev_labels_set() const { return m_prev; } // Add a cfg_t edge from *this to b - void operator>>(basic_block_t& b) { + void operator>>(value_t& b) { assert(b.label() != label_t::entry); assert(this->label() != label_t::exit); m_next.insert(b.m_label); @@ -136,17 +93,11 @@ class basic_block_t final { } // Remove a cfg_t edge from *this to b - void operator-=(basic_block_t& b) { + void operator-=(value_t& b) { m_next.erase(b.m_label); b.m_prev.erase(m_label); } - // insert all statements of other at the back - void move_back(basic_block_t& other) { - m_ts.reserve(m_ts.size() + other.m_ts.size()); - std::ranges::move(other.m_ts, std::back_inserter(m_ts)); - } - [[nodiscard]] size_t in_degree() const { return m_prev.size(); @@ -156,108 +107,47 @@ class basic_block_t final { size_t out_degree() const { return m_next.size(); } - - void swap_instructions(stmt_list_t& ts) { std::swap(m_ts, ts); } -}; - -// Viewing basic_block_t with all statements reversed. Useful for -// backward analysis. -class basic_block_rev_t final { - public: - using neighbour_const_iterator = basic_block_t::neighbour_const_iterator; - - using iterator = basic_block_t::reverse_iterator; - using const_iterator = basic_block_t::const_reverse_iterator; - - public: - basic_block_t& _bb; - - explicit basic_block_rev_t(basic_block_t& bb) : _bb(bb) {} - - [[nodiscard]] - label_t label() const { - return _bb.label(); - } - - iterator begin() { return _bb.rbegin(); } - - iterator end() { return _bb.rend(); } - - [[nodiscard]] - const_iterator begin() const { - return _bb.rbegin(); - } - - [[nodiscard]] - const_iterator end() const { - return _bb.rend(); - } - - [[nodiscard]] - std::size_t size() const { - return gsl::narrow(std::distance(begin(), end())); - } - - [[nodiscard]] - std::pair next_blocks() const { - return _bb.prev_blocks(); - } - - [[nodiscard]] - std::pair prev_blocks() const { - return _bb.next_blocks(); - } - - [[nodiscard]] - const basic_block_t::label_vec_t& next_blocks_set() const { - return _bb.prev_blocks_set(); - } - - [[nodiscard]] - const basic_block_t::label_vec_t& prev_blocks_set() const { - return _bb.next_blocks_set(); - } }; -/// Control-Flow Graph. +/// Control-Flow Graph class cfg_t final { public: using node_t = label_t; // for Bgl graphs - using neighbour_const_iterator = basic_block_t::neighbour_const_iterator; - using neighbour_const_reverse_iterator = basic_block_t::neighbour_const_reverse_iterator; + using neighbour_const_iterator = value_t::neighbour_const_iterator; + using neighbour_const_reverse_iterator = value_t::neighbour_const_reverse_iterator; using neighbour_const_range = boost::iterator_range; using neighbour_const_reverse_range = boost::iterator_range; private: - using basic_block_map_t = std::map; - using binding_t = basic_block_map_t::value_type; + using map_t = std::map; + using binding_t = map_t::value_type; struct get_label { label_t operator()(const binding_t& p) const { return p.second.label(); } }; public: - using iterator = basic_block_map_t::iterator; - using const_iterator = basic_block_map_t::const_iterator; - using label_iterator = boost::transform_iterator; - using const_label_iterator = boost::transform_iterator; + using iterator = map_t::iterator; + using const_iterator = map_t::const_iterator; + using label_iterator = boost::transform_iterator; + using const_label_iterator = boost::transform_iterator; private: - basic_block_map_t m_blocks; + map_t m_map; using visited_t = std::set; public: cfg_t() { - m_blocks.emplace(entry_label(), entry_label()); - m_blocks.emplace(exit_label(), exit_label()); + m_map.emplace(entry_label(), entry_label()); + m_map.emplace(exit_label(), exit_label()); } cfg_t(const cfg_t&) = delete; - cfg_t(cfg_t&& o) noexcept : m_blocks(std::move(o.m_blocks)) {} + cfg_t(cfg_t&& o) noexcept : m_map(std::move(o.m_map)) {} ~cfg_t() = default; @@ -275,45 +165,89 @@ class cfg_t final { [[nodiscard]] neighbour_const_range next_nodes(const label_t& _label) const { - return boost::make_iterator_range(get_node(_label).next_blocks()); + return boost::make_iterator_range(get_node(_label).next_labels()); } + [[nodiscard]] neighbour_const_reverse_range next_nodes_reversed(const label_t& _label) const { - return boost::make_iterator_range(get_node(_label).next_blocks_reversed()); + return boost::make_iterator_range(get_node(_label).next_labels_reversed()); } [[nodiscard]] neighbour_const_range prev_nodes(const label_t& _label) const { - return boost::make_iterator_range(get_node(_label).prev_blocks()); + return boost::make_iterator_range(get_node(_label).prev_labels()); } - basic_block_t& get_node(const label_t& _label) { - auto it = m_blocks.find(_label); - if (it == m_blocks.end()) { - CRAB_ERROR("Basic block ", _label, " not found in the CFG: ", __LINE__); + value_t& get_node(const label_t& _label) { + const auto it = m_map.find(_label); + if (it == m_map.end()) { + CRAB_ERROR("Label ", to_string(_label), " not found in the CFG: "); } return it->second; } - [[nodiscard]] - const basic_block_t& get_node(const label_t& _label) const { - auto it = m_blocks.find(_label); - if (it == m_blocks.end()) { - CRAB_ERROR("Basic block ", _label, " not found in the CFG: ", __LINE__); + const value_t& get_node(const label_t& _label) const { + const auto it = m_map.find(_label); + if (it == m_map.end()) { + CRAB_ERROR("Label ", to_string(_label), " not found in the CFG: "); } return it->second; } + GuardedInstruction& at(const label_t& _label) { + const auto it = m_map.find(_label); + if (it == m_map.end()) { + CRAB_ERROR("Label ", to_string(_label), " not found in the CFG: "); + } + return it->second.instruction(); + } + + [[nodiscard]] + const GuardedInstruction& at(const label_t& _label) const { + const auto it = m_map.find(_label); + if (it == m_map.end()) { + CRAB_ERROR("Label ", to_string(_label), " not found in the CFG: "); + } + return it->second.instruction(); + } + // --- End ikos fixpoint API - basic_block_t& insert(const label_t& _label) { - auto it = m_blocks.find(_label); - if (it != m_blocks.end()) { + value_t& insert_after(const label_t& prev_label, const label_t& new_label, const Instruction& _ins) { + value_t& res = insert(new_label, GuardedInstruction{.cmd = _ins}); + value_t& prev = get_node(prev_label); + std::vector nexts; + for (const label_t& next : prev.next_labels_set()) { + nexts.push_back(next); + } + prev.m_next.clear(); + + std::vector prevs; + for (const label_t& next_label : nexts) { + get_node(next_label).m_prev.erase(prev_label); + } + + for (const label_t& next : nexts) { + get_node(prev_label) >> res; + res >> get_node(next); + } + return res; + } + + value_t& insert(const label_t& _label, const Instruction& _ins) { + return insert(_label, GuardedInstruction{.cmd = _ins}); + } + + value_t& insert(const label_t& _label, GuardedInstruction&& _ins) { + const auto it = m_map.find(_label); + if (it != m_map.end()) { return it->second; } - m_blocks.emplace(_label, _label); - return get_node(_label); + m_map.emplace(_label, _label); + value_t& v = get_node(_label); + v.m_instruction = std::move(_ins); + return v; } void remove(const label_t& _label) { @@ -325,16 +259,16 @@ class cfg_t final { CRAB_ERROR("Cannot remove exit block"); } - std::vector> dead_edges; + std::vector> dead_edges; auto& bb = get_node(_label); - for (const auto& id : boost::make_iterator_range(bb.prev_blocks())) { + for (const auto& id : boost::make_iterator_range(bb.prev_labels())) { if (_label != id) { dead_edges.emplace_back(&get_node(id), &bb); } } - for (const auto& id : boost::make_iterator_range(bb.next_blocks())) { + for (const auto& id : boost::make_iterator_range(bb.next_labels())) { if (_label != id) { dead_edges.emplace_back(&bb, &get_node(id)); } @@ -344,37 +278,37 @@ class cfg_t final { *p.first -= *p.second; } - m_blocks.erase(_label); + m_map.erase(_label); } //! return a begin iterator of basic_block_t's - iterator begin() { return m_blocks.begin(); } + iterator begin() { return m_map.begin(); } //! return an end iterator of basic_block_t's - iterator end() { return m_blocks.end(); } + iterator end() { return m_map.end(); } [[nodiscard]] const_iterator begin() const { - return m_blocks.begin(); + return m_map.begin(); } [[nodiscard]] const_iterator end() const { - return m_blocks.end(); + return m_map.end(); } //! return a begin iterator of label_t's - const_label_iterator label_begin() const { return boost::make_transform_iterator(m_blocks.begin(), get_label()); } + const_label_iterator label_begin() const { return boost::make_transform_iterator(m_map.begin(), get_label()); } //! return an end iterator of label_t's - const_label_iterator label_end() const { return boost::make_transform_iterator(m_blocks.end(), get_label()); } + const_label_iterator label_end() const { return boost::make_transform_iterator(m_map.end(), get_label()); } //! return a begin iterator of label_t's [[nodiscard]] std::vector labels() const { std::vector res; - res.reserve(m_blocks.size()); - for (const auto& p : m_blocks) { + res.reserve(m_map.size()); + for (const auto& p : m_map) { res.push_back(p.first); } return res; @@ -385,41 +319,6 @@ class cfg_t final { return gsl::narrow(std::distance(begin(), end())); } - void simplify() { - std::set worklist(this->label_begin(), this->label_end()); - while (!worklist.empty()) { - label_t label = *worklist.begin(); - worklist.erase(label); - - basic_block_t& bb = get_node(label); - if (bb.in_degree() == 1 && get_parent(label).out_degree() == 1) { - continue; - } - while (bb.out_degree() == 1) { - basic_block_t& next_bb = get_child(label); - - if (&next_bb == &bb || next_bb.in_degree() != 1) { - break; - } - if (next_bb.label() == exit_label()) { - break; - } - worklist.erase(next_bb.label()); - - bb.move_back(next_bb); - bb -= next_bb; - auto children = next_bb.m_next; - for (const label_t& next_next_label : children) { - basic_block_t& next_next_bb = get_node(next_next_label); - bb >> next_next_bb; - } - - // delete next_bb entirely - remove(next_bb.label()); - } - } - } - [[nodiscard]] std::vector sorted_labels() const { std::vector labels = this->labels(); @@ -427,30 +326,30 @@ class cfg_t final { return labels; } + value_t& get_child(const label_t& b) { + assert(has_one_child(b)); + const auto rng = next_nodes(b); + return get_node(*rng.begin()); + } + + value_t& get_parent(const label_t& b) { + assert(has_one_parent(b)); + const auto rng = prev_nodes(b); + return get_node(*rng.begin()); + } + private: // Helpers [[nodiscard]] bool has_one_child(const label_t& b) const { - auto rng = next_nodes(b); - return (std::distance(rng.begin(), rng.end()) == 1); + const auto rng = next_nodes(b); + return std::distance(rng.begin(), rng.end()) == 1; } [[nodiscard]] bool has_one_parent(const label_t& b) const { - auto rng = prev_nodes(b); - return (std::distance(rng.begin(), rng.end()) == 1); - } - - basic_block_t& get_child(const label_t& b) { - assert(has_one_child(b)); - auto rng = next_nodes(b); - return get_node(*(rng.begin())); - } - - basic_block_t& get_parent(const label_t& b) { - assert(has_one_parent(b)); - auto rng = prev_nodes(b); - return get_node(*(rng.begin())); + const auto rng = prev_nodes(b); + return std::distance(rng.begin(), rng.end()) == 1; } // mark reachable blocks from curId @@ -466,142 +365,130 @@ class cfg_t final { } void remove_unreachable_blocks(); - - // remove blocks that cannot reach the exit block - void remove_useless_blocks(); }; -// Viewing a cfg_t with all edges and block statements reversed. Useful for backward analysis. -class cfg_rev_t final { - public: - using node_t = label_t; // for Bgl graphs - - using neighbour_const_range = cfg_t::neighbour_const_range; +class basic_block_t final { + friend class cfg_t; - // For BGL - using neighbour_const_iterator = basic_block_t::neighbour_const_iterator; + public: + basic_block_t(const basic_block_t&) = delete; - using basic_block_rev_map_t = std::map; - using iterator = basic_block_rev_map_t::iterator; - using const_iterator = basic_block_rev_map_t::const_iterator; - using label_iterator = cfg_t::label_iterator; - using const_label_iterator = cfg_t::const_label_iterator; + using label_vec_t = std::set; + using stmt_list_t = std::vector; + using iterator = stmt_list_t::iterator; + using const_iterator = stmt_list_t::const_iterator; + using reverse_iterator = stmt_list_t::reverse_iterator; + using const_reverse_iterator = stmt_list_t::const_reverse_iterator; private: - cfg_t& _cfg; - basic_block_rev_map_t _rev_bbs; + label_t m_label; + stmt_list_t m_ts; public: - explicit cfg_rev_t(cfg_t& cfg) : _cfg(cfg) { - // Create basic_block_rev_t from basic_block_t objects - // Note that basic_block_rev_t is also a view of basic_block_t so it - // doesn't modify basic_block_t objects. - for (auto& [label, bb] : cfg) { - _rev_bbs.emplace(label, bb); - } - } + static std::map collect_basic_blocks(cfg_t& cfg) { + std::map res; - cfg_rev_t(const cfg_rev_t& o) = default; + std::set worklist(cfg.label_begin(), cfg.label_end()); + std::set seen; + while (!worklist.empty()) { + label_t label = *worklist.begin(); + worklist.erase(label); + if (seen.contains(label)) { + continue; + } + seen.insert(label); - cfg_rev_t(cfg_rev_t&& o) noexcept : _cfg(o._cfg), _rev_bbs(std::move(o._rev_bbs)) {} + const value_t& value = cfg.get_node(label); + if (value.in_degree() == 1 && cfg.get_parent(label).out_degree() == 1) { + continue; + } + res.emplace(label, label); + basic_block_t& bb = res.at(label); + while (value.out_degree() == 1) { + value_t& next_value = cfg.get_child(label); - [[nodiscard]] - label_t entry_label() const { - return _cfg.exit_label(); - } + if (&next_value == &value || next_value.in_degree() != 1) { + break; + } + if (next_value.label() == cfg.exit_label()) { + break; + } + worklist.erase(next_value.label()); - [[nodiscard]] - neighbour_const_range next_nodes(const label_t& bb) const { - return _cfg.prev_nodes(bb); + bb.m_ts.push_back(&next_value.instruction()); + + // delete next_bb entirely + // remove(next_value.label()); + seen.insert(next_value.label()); + } + } + return res; } - [[nodiscard]] - neighbour_const_range prev_nodes(const label_t& bb) const { - return _cfg.next_nodes(bb); + void insert(GuardedInstruction* arg) { + assert(label() != label_t::entry); + assert(label() != label_t::exit); + m_ts.push_back(arg); } - neighbour_const_range next_nodes(const label_t& bb) { return _cfg.prev_nodes(bb); } + /// Insert a GuardedInstruction at the front of the basic block. + /// @note Cannot modify entry or exit blocks. + void insert_front(GuardedInstruction* arg) { + assert(label() != label_t::entry); + assert(label() != label_t::exit); + m_ts.insert(m_ts.begin(), arg); + } - neighbour_const_range prev_nodes(const label_t& bb) { return _cfg.next_nodes(bb); } + explicit basic_block_t(label_t _label) : m_label(std::move(_label)) {} - basic_block_rev_t& get_node(const label_t& _label) { - auto it = _rev_bbs.find(_label); - if (it == _rev_bbs.end()) { - CRAB_ERROR("Basic block ", _label, " not found in the CFG: ", __LINE__); - } - return it->second; - } + ~basic_block_t() = default; [[nodiscard]] - const basic_block_rev_t& get_node(const label_t& _label) const { - auto it = _rev_bbs.find(_label); - if (it == _rev_bbs.end()) { - CRAB_ERROR("Basic block ", _label, " not found in the CFG: ", __LINE__); - } - return it->second; + label_t label() const { + return m_label; } - iterator begin() { return _rev_bbs.begin(); } - - iterator end() { return _rev_bbs.end(); } - + iterator begin() { return (m_ts.begin()); } + iterator end() { return (m_ts.end()); } [[nodiscard]] const_iterator begin() const { - return _rev_bbs.begin(); + return m_ts.begin(); } - [[nodiscard]] const_iterator end() const { - return _rev_bbs.end(); + return m_ts.end(); } - const_label_iterator label_begin() const { return _cfg.label_begin(); } - - const_label_iterator label_end() const { return _cfg.label_end(); } - + reverse_iterator rbegin() { return (m_ts.rbegin()); } + reverse_iterator rend() { return (m_ts.rend()); } [[nodiscard]] - label_t exit_label() const { - return _cfg.entry_label(); + const_reverse_iterator rbegin() const { + return m_ts.rbegin(); } -}; - -inline void cfg_t::remove_useless_blocks() { - cfg_rev_t rev_cfg(*this); - - visited_t useful, useless; - mark_alive_blocks(rev_cfg.entry_label(), rev_cfg, useful); - - if (!useful.contains(exit_label())) { - CRAB_ERROR("Exit block must be reachable"); + [[nodiscard]] + const_reverse_iterator rend() const { + return m_ts.rend(); } - for (const auto& label : labels()) { - if (!useful.contains(label)) { - useless.insert(label); - } + + [[nodiscard]] + size_t size() const { + return gsl::narrow(std::distance(begin(), end())); } - for (const auto& _label : useless) { - remove(_label); + // insert all statements of other at the back + void move_back(basic_block_t& other) { + m_ts.reserve(m_ts.size() + other.m_ts.size()); + std::ranges::move(other.m_ts, std::back_inserter(m_ts)); } -} -inline void cfg_t::remove_unreachable_blocks() { - visited_t alive, dead; - mark_alive_blocks(entry_label(), *this, alive); + void swap_instructions(stmt_list_t& ts) { std::swap(m_ts, ts); } +}; - for (const auto& label : labels()) { - if (!alive.contains(label)) { - dead.insert(label); - } - } +void print_dot(const cfg_t& cfg, std::ostream& out); +void print_dot(const cfg_t& cfg, const std::string& outfile); - if (dead.contains(exit_label())) { - CRAB_ERROR("Exit block must be reachable"); - } - for (const auto& _label : dead) { - remove(_label); - } -} +std::ostream& operator<<(std::ostream& o, const value_t& value); +std::ostream& operator<<(std::ostream& o, const cfg_t& cfg); } // end namespace crab @@ -613,8 +500,6 @@ std::vector stats_headers(); std::map collect_stats(const cfg_t&); struct prepare_cfg_options { - /// When true, simplifies the control flow graph by merging basic blocks. - bool simplify = true; /// When true, verifies that the program terminates. bool check_for_termination = false; /// When true, ensures the program has a valid exit block. @@ -625,10 +510,3 @@ cfg_t prepare_cfg(const InstructionSeq& prog, const program_info& info, const pr void explicate_assertions(cfg_t& cfg, const program_info& info); std::vector get_assertions(Instruction ins, const program_info& info, const std::optional& label); - -void print_dot(const cfg_t& cfg, std::ostream& out); -void print_dot(const cfg_t& cfg, const std::string& outfile); - -std::ostream& operator<<(std::ostream& o, const basic_block_t& bb); -std::ostream& operator<<(std::ostream& o, const crab::basic_block_rev_t& bb); -std::ostream& operator<<(std::ostream& o, const cfg_t& cfg); diff --git a/src/crab/ebpf_checker.cpp b/src/crab/ebpf_checker.cpp index 3ec0ed85f..4d734780d 100644 --- a/src/crab/ebpf_checker.cpp +++ b/src/crab/ebpf_checker.cpp @@ -7,7 +7,7 @@ #include #include -#include "asm_ostream.hpp" +#include "asm_syntax.hpp" #include "asm_unmarshal.hpp" #include "config.hpp" #include "crab/array_domain.hpp" diff --git a/src/crab/ebpf_domain.cpp b/src/crab/ebpf_domain.cpp index 8d3ef4f48..cb4ca0b6c 100644 --- a/src/crab/ebpf_domain.cpp +++ b/src/crab/ebpf_domain.cpp @@ -9,7 +9,6 @@ #include "boost/endian/conversion.hpp" -#include "asm_ostream.hpp" #include "asm_unmarshal.hpp" #include "config.hpp" #include "crab/array_domain.hpp" diff --git a/src/crab/ebpf_transformer.cpp b/src/crab/ebpf_transformer.cpp index 7936600c8..743427ad0 100644 --- a/src/crab/ebpf_transformer.cpp +++ b/src/crab/ebpf_transformer.cpp @@ -10,7 +10,6 @@ #include "boost/endian/conversion.hpp" -#include "asm_ostream.hpp" #include "asm_unmarshal.hpp" #include "config.hpp" #include "crab/array_domain.hpp" diff --git a/src/crab/fwd_analyzer.cpp b/src/crab/fwd_analyzer.cpp index 5afa2e0a2..f77e8e90a 100644 --- a/src/crab/fwd_analyzer.cpp +++ b/src/crab/fwd_analyzer.cpp @@ -68,17 +68,16 @@ class interleaved_fwd_fixpoint_iterator_t final { void set_pre(const label_t& label, const ebpf_domain_t& v) { _pre[label] = v; } void transform_to_post(const label_t& label, ebpf_domain_t pre) { - const basic_block_t& bb = _cfg.get_node(label); + const GuardedInstruction& ins = _cfg.at(label); - for (const GuardedInstruction& ins : bb) { - if (thread_local_options.assume_assertions) { - for (const auto& assertion : ins.preconditions) { - // avoid redundant errors - ebpf_domain_assume(pre, assertion); - } + if (thread_local_options.assume_assertions) { + for (const auto& assertion : ins.preconditions) { + // avoid redundant errors + ebpf_domain_assume(pre, assertion); } - ebpf_domain_transform(pre, ins.cmd); - }; + } + ebpf_domain_transform(pre, ins.cmd); + _post[label] = std::move(pre); } diff --git a/src/crab/interval.hpp b/src/crab/interval.hpp index c7de6dda6..c4a2c0a7d 100644 --- a/src/crab/interval.hpp +++ b/src/crab/interval.hpp @@ -104,7 +104,8 @@ class interval_t final { template [[nodiscard]] std::tuple bound(T elb, T eub) const { - auto [lb, ub] = bound(static_cast>(elb), static_cast>(eub)); + using C = std::underlying_type_t; + auto [lb, ub] = bound(static_cast(elb), static_cast(eub)); return {static_cast(lb), static_cast(ub)}; } diff --git a/src/crab/label.hpp b/src/crab/label.hpp new file mode 100644 index 000000000..db8c55ea5 --- /dev/null +++ b/src/crab/label.hpp @@ -0,0 +1,94 @@ +// Copyright (c) Prevail Verifier contributors. +// SPDX-License-Identifier: MIT +#pragma once + +#include +#include +#include +#include +#include +#include +#include +#include +#include + +#include "crab_utils/num_safety.hpp" + +constexpr char STACK_FRAME_DELIMITER = '/'; + +namespace crab { +struct label_t { + std::string stack_frame_prefix; ///< Variable prefix when calling this label. + int from{}; ///< Jump source, or simply index of instruction + int to{}; ///< Jump target or -1 + std::string special_label; ///< Special label for special instructions. + + explicit label_t(const int index, const int to = -1, std::string stack_frame_prefix = {}) noexcept + : stack_frame_prefix(std::move(stack_frame_prefix)), from(index), to(to) {} + + static label_t make_jump(const label_t& src_label, const label_t& target_label) { + return label_t{src_label.from, target_label.from, target_label.stack_frame_prefix}; + } + + static label_t make_increment_counter(const label_t& label) { + // XXX: This is a hack to increment the loop counter. + label_t res{label.from, label.to, label.stack_frame_prefix}; + res.special_label = "counter"; + return res; + } + + std::strong_ordering operator<=>(const label_t& other) const = default; + + // no hash; intended for use in ordered containers. + + [[nodiscard]] + constexpr bool isjump() const { + return to != -1; + } + + [[nodiscard]] + int call_stack_depth() const { + // The call stack depth is the number of '/' separated components in the label, + // which is one more than the number of '/' separated components in the prefix, + // hence two more than the number of '/' in the prefix, if any. + if (stack_frame_prefix.empty()) { + return 1; + } + return gsl::narrow(2 + std::ranges::count(stack_frame_prefix, STACK_FRAME_DELIMITER)); + } + + static const label_t entry; + static const label_t exit; +}; + +inline const label_t label_t::entry{-1}; +inline const label_t label_t::exit{INT_MAX}; + +std::ostream& operator<<(std::ostream& os, const label_t& label); +std::string to_string(label_t const& label); + +// cpu=v4 supports 32-bit PC offsets so we need a large enough type. +using pc_t = uint32_t; + +// We use a 16-bit offset whenever it fits in 16 bits. +inline std::function label_to_offset16(const pc_t pc) { + return [=](const label_t& label) { + const int64_t offset = label.from - gsl::narrow(pc) - 1; + const bool is16 = + std::numeric_limits::min() <= offset && offset <= std::numeric_limits::max(); + return gsl::narrow(is16 ? offset : 0); + }; +} + +// We use the JA32 opcode with the offset in 'imm' when the offset +// of an unconditional jump doesn't fit in an int16_t. +inline std::function label_to_offset32(const pc_t pc) { + return [=](const label_t& label) { + const int64_t offset = label.from - gsl::narrow(pc) - 1; + const bool is16 = + std::numeric_limits::min() <= offset && offset <= std::numeric_limits::max(); + return is16 ? 0 : gsl::narrow(offset); + }; +} + +} // namespace crab diff --git a/src/crab/split_dbm.cpp b/src/crab/split_dbm.cpp index 1c8620718..b8cf2ce50 100644 --- a/src/crab/split_dbm.cpp +++ b/src/crab/split_dbm.cpp @@ -1143,9 +1143,8 @@ string_invariant SplitDBM::to_set() const { if (!this->g.elem(0, v) && !this->g.elem(v, 0)) { continue; } - interval_t v_out = - interval_t(this->g.elem(v, 0) ? -number_t(this->g.edge_val(v, 0)) : extended_number::minus_infinity(), - this->g.elem(0, v) ? number_t(this->g.edge_val(0, v)) : extended_number::plus_infinity()); + interval_t v_out{this->g.elem(v, 0) ? -number_t(this->g.edge_val(v, 0)) : extended_number::minus_infinity(), + this->g.elem(0, v) ? number_t(this->g.edge_val(0, v)) : extended_number::plus_infinity()}; assert(!v_out.is_bottom()); variable_t variable = *this->rev_map[v]; @@ -1153,7 +1152,7 @@ string_invariant SplitDBM::to_set() const { std::stringstream elem; elem << variable; if (variable.is_type()) { - auto [lb, ub] = v_out.bound(T_MIN, T_MAX); + auto [lb, ub] = v_out.bound(T_UNINIT, T_MAX); if (lb == ub) { if (variable.is_in_stack() && lb == T_NUM) { // no need to show this @@ -1206,8 +1205,7 @@ 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/thresholds.cpp b/src/crab/thresholds.cpp index 88e3e689e..5cf436d30 100644 --- a/src/crab/thresholds.cpp +++ b/src/crab/thresholds.cpp @@ -2,6 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 #include "crab/thresholds.hpp" #include "crab/cfg.hpp" +#include "crab/label.hpp" namespace crab { @@ -48,7 +49,7 @@ std::ostream& operator<<(std::ostream& o, const thresholds_t& t) { return o; } -void wto_thresholds_t::get_thresholds(const basic_block_t& bb, thresholds_t& thresholds) const {} +void wto_thresholds_t::get_thresholds(const value_t& bb, thresholds_t& thresholds) const {} void wto_thresholds_t::operator()(const label_t& vertex) { if (m_stack.empty()) { @@ -59,7 +60,7 @@ void wto_thresholds_t::operator()(const label_t& vertex) { const auto it = m_head_to_thresholds.find(head); if (it != m_head_to_thresholds.end()) { thresholds_t& thresholds = it->second; - const basic_block_t& bb = m_cfg.get_node(vertex); + const value_t& bb = m_cfg.get_node(vertex); get_thresholds(bb, thresholds); } else { CRAB_ERROR("No head found while gathering thresholds"); @@ -73,7 +74,7 @@ void wto_thresholds_t::operator()(const std::shared_ptr& cycle) { // XXX: if we want to consider constants from loop // initializations - for (const auto& pre : boost::make_iterator_range(bb.prev_blocks())) { + for (const auto& pre : boost::make_iterator_range(bb.prev_labels())) { if (pre != cycle->head()) { auto& pred_bb = m_cfg.get_node(pre); get_thresholds(pred_bb, thresholds); @@ -90,7 +91,7 @@ void wto_thresholds_t::operator()(const std::shared_ptr& cycle) { std::ostream& operator<<(std::ostream& o, const wto_thresholds_t& t) { for (const auto& [label, th] : t.m_head_to_thresholds) { - o << label << "=" << th << "\n"; + o << to_string(label) << "=" << th << "\n"; } return o; } diff --git a/src/crab/thresholds.hpp b/src/crab/thresholds.hpp index fe5a2e079..1e3d67635 100644 --- a/src/crab/thresholds.hpp +++ b/src/crab/thresholds.hpp @@ -58,7 +58,7 @@ class wto_thresholds_t final { // the top of the stack is the current wto head std::vector m_stack; - void get_thresholds(const basic_block_t& bb, thresholds_t& thresholds) const; + void get_thresholds(const value_t& bb, thresholds_t& thresholds) const; public: wto_thresholds_t(cfg_t& cfg, const size_t max_size) : m_cfg(cfg), m_max_size(max_size) {} diff --git a/src/crab/var_factory.cpp b/src/crab/var_factory.cpp index f4c243229..00ace7328 100644 --- a/src/crab/var_factory.cpp +++ b/src/crab/var_factory.cpp @@ -4,7 +4,7 @@ * Factories for variable names. */ -#include "asm_syntax.hpp" +#include "crab/label.hpp" #include "crab/variable.hpp" #include "crab_utils/lazy_allocator.hpp" diff --git a/src/crab_utils/debug.hpp b/src/crab_utils/debug.hpp index e70d15c54..e71baa424 100644 --- a/src/crab_utils/debug.hpp +++ b/src/crab_utils/debug.hpp @@ -43,13 +43,14 @@ void ___print___(std::ostream& os, ArgTypes... args) { (void)expand_variadic_pack{0, ((os << args), void(), 0)...}; } -#define CRAB_ERROR(...) \ - do { \ - std::ostringstream os; \ - os << "CRAB ERROR: "; \ - crab::___print___(os, __VA_ARGS__); \ - os << "\n"; \ - throw std::runtime_error(os.str()); \ +#define CRAB_ERROR(...) \ + do { \ + std::ostringstream os; \ + os << "CRAB ERROR: "; \ + crab::___print___(os, __VA_ARGS__); \ + crab::___print___(os, "; function ", __func__, ", line ", __LINE__); \ + os << "\n"; \ + throw std::runtime_error(os.str()); \ } while (0) extern bool CrabWarningFlag; diff --git a/src/crab_verifier.cpp b/src/crab_verifier.cpp index 6680c884b..00695c18e 100644 --- a/src/crab_verifier.cpp +++ b/src/crab_verifier.cpp @@ -60,21 +60,19 @@ static checks_db generate_report(const cfg_t& cfg, const crab::invariant_table_t const crab::invariant_table_t& post_invariants) { checks_db m_db; for (const label_t& label : cfg.sorted_labels()) { - const basic_block_t& bb = cfg.get_node(label); ebpf_domain_t from_inv{pre_invariants.at(label)}; const bool pre_bot = from_inv.is_bottom(); - for (const GuardedInstruction& ins : bb) { - for (const Assertion& assertion : ins.preconditions) { - for (const auto& warning : ebpf_domain_check(from_inv, label, assertion)) { - m_db.add_warning(label, warning); - } + 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, ins.cmd); } + ebpf_domain_transform(from_inv, instruction.cmd); if (!pre_bot && from_inv.is_bottom()) { - m_db.add_unreachable(label, std::string("Code is unreachable after ") + to_string(bb.label())); + m_db.add_unreachable(label, std::string("Code is unreachable after ") + to_string(label)); } } diff --git a/src/main/check.cpp b/src/main/check.cpp index 81d224de1..f6874a99a 100644 --- a/src/main/check.cpp +++ b/src/main/check.cpp @@ -124,7 +124,7 @@ 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.cfg_opts.simplify, + app.add_flag("--simplify,!--no-simplify", ebpf_verifier_options.simplify, "Simplify the CFG before analysis by merging chains of instructions into a single basic block. " "Default: enabled") ->group("Verbosity"); diff --git a/src/spec_type_descriptors.hpp b/src/spec_type_descriptors.hpp index 3da18504e..89a7d537f 100644 --- a/src/spec_type_descriptors.hpp +++ b/src/spec_type_descriptors.hpp @@ -38,8 +38,6 @@ struct EbpfProgramType { bool is_privileged{}; }; -void print_map_descriptors(const std::vector& descriptors, std::ostream& o); - // Represents the key characteristics that determine equivalence between eBPF maps. // Used to cache and compare map configurations across the program. struct EquivalenceKey { @@ -74,4 +72,8 @@ struct raw_program { 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; diff --git a/src/test/ebpf_yaml.cpp b/src/test/ebpf_yaml.cpp index 017d17806..ec02500c4 100644 --- a/src/test/ebpf_yaml.cpp +++ b/src/test/ebpf_yaml.cpp @@ -11,8 +11,8 @@ #include -#include "asm_ostream.hpp" #include "asm_parse.hpp" +#include "asm_syntax.hpp" #include "ebpf_verifier.hpp" #include "ebpf_yaml.hpp" #include "string_constraints.hpp" @@ -171,7 +171,7 @@ 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.cfg_opts.simplify = false; + options.simplify = false; // All YAML tests use !setup_constraints. options.setup_constraints = 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.cfg_opts.simplify = true; + options.simplify = true; } else if (name == "big_endian") { options.big_endian = true; } else if (name == "!big_endian") { @@ -251,7 +251,7 @@ std::optional run_yaml_test_case(TestCase test_case, bool debug) { if (debug) { test_case.options.print_failures = true; test_case.options.print_invariants = true; - test_case.options.cfg_opts.simplify = false; + test_case.options.simplify = false; } ebpf_context_descriptor_t context_descriptor{64, 0, 4, -1}; @@ -360,7 +360,7 @@ ConformanceTestResult run_conformance_test_case(const std::vector& me print(prog, std::cout, {}); options.print_failures = true; options.print_invariants = true; - options.cfg_opts.simplify = false; + options.simplify = false; } try { diff --git a/src/test/test_conformance.cpp b/src/test/test_conformance.cpp index 074bae979..9d5eebb3a 100644 --- a/src/test/test_conformance.cpp +++ b/src/test/test_conformance.cpp @@ -6,7 +6,7 @@ #define CONFORMANCE_TEST_PATH "external/bpf_conformance/tests/" -static void test_conformance(const std::string& filename, bpf_conformance_test_result_t expected_result, +static void test_conformance(const std::string& filename, const bpf_conformance_test_result_t& expected_result, const std::string& expected_reason) { std::vector test_files = {CONFORMANCE_TEST_PATH + filename}; boost::filesystem::path test_path = boost::dll::program_location(); diff --git a/src/test/test_marshal.cpp b/src/test/test_marshal.cpp index 230d045c9..82756292c 100644 --- a/src/test/test_marshal.cpp +++ b/src/test/test_marshal.cpp @@ -3,7 +3,6 @@ #include #include "asm_marshal.hpp" -#include "asm_ostream.hpp" #include "asm_unmarshal.hpp" // Below we define a tample of instruction templates that specify diff --git a/src/test/test_print.cpp b/src/test/test_print.cpp index bcf1675f1..515c92ef6 100644 --- a/src/test/test_print.cpp +++ b/src/test/test_print.cpp @@ -12,7 +12,6 @@ #endif #include "asm_files.hpp" -#include "asm_ostream.hpp" #include "asm_unmarshal.hpp" #define TEST_OBJECT_FILE_DIRECTORY "ebpf-samples/build/" diff --git a/src/test/test_wto.cpp b/src/test/test_wto.cpp index 4e5ac738a..091efebc3 100644 --- a/src/test/test_wto.cpp +++ b/src/test/test_wto.cpp @@ -12,22 +12,22 @@ TEST_CASE("wto figure 1", "[wto]") { // Add nodes. for (int i = 1; i <= 8; i++) { - cfg.insert(label_t(i)); + cfg.insert(label_t{i}, Undefined{}); } // Add edges. - cfg.get_node(label_t::entry) >> cfg.get_node(label_t(1)); - cfg.get_node(label_t(1)) >> cfg.get_node(label_t(2)); - cfg.get_node(label_t(2)) >> cfg.get_node(label_t(3)); - cfg.get_node(label_t(3)) >> cfg.get_node(label_t(4)); - cfg.get_node(label_t(4)) >> cfg.get_node(label_t(5)); - cfg.get_node(label_t(4)) >> cfg.get_node(label_t(7)); - cfg.get_node(label_t(5)) >> cfg.get_node(label_t(6)); - cfg.get_node(label_t(6)) >> cfg.get_node(label_t(5)); - cfg.get_node(label_t(6)) >> cfg.get_node(label_t(7)); - cfg.get_node(label_t(7)) >> cfg.get_node(label_t(3)); - cfg.get_node(label_t(7)) >> cfg.get_node(label_t(8)); - cfg.get_node(label_t(8)) >> cfg.get_node(label_t::exit); + cfg.get_node(label_t::entry) >> cfg.get_node(label_t{1}); + cfg.get_node(label_t{1}) >> cfg.get_node(label_t{2}); + cfg.get_node(label_t{2}) >> cfg.get_node(label_t{3}); + cfg.get_node(label_t{3}) >> cfg.get_node(label_t{4}); + cfg.get_node(label_t{4}) >> cfg.get_node(label_t{5}); + cfg.get_node(label_t{4}) >> cfg.get_node(label_t{7}); + cfg.get_node(label_t{5}) >> cfg.get_node(label_t{6}); + cfg.get_node(label_t{6}) >> cfg.get_node(label_t{5}); + cfg.get_node(label_t{6}) >> cfg.get_node(label_t{7}); + cfg.get_node(label_t{7}) >> cfg.get_node(label_t{3}); + cfg.get_node(label_t{7}) >> cfg.get_node(label_t{8}); + cfg.get_node(label_t{8}) >> cfg.get_node(label_t::exit); const wto_t wto(cfg); @@ -44,18 +44,18 @@ TEST_CASE("wto figure 2a", "[wto]") { // Add nodes. for (int i = 1; i <= 5; i++) { - cfg.insert(label_t(i)); + cfg.insert(label_t{i}, Undefined{}); } // Add edges. - cfg.get_node(label_t::entry) >> cfg.get_node(label_t(1)); - cfg.get_node(label_t(1)) >> cfg.get_node(label_t(2)); - cfg.get_node(label_t(1)) >> cfg.get_node(label_t(4)); - cfg.get_node(label_t(2)) >> cfg.get_node(label_t(3)); - cfg.get_node(label_t(3)) >> cfg.get_node(label_t::exit); - cfg.get_node(label_t(4)) >> cfg.get_node(label_t(3)); - cfg.get_node(label_t(4)) >> cfg.get_node(label_t(5)); - cfg.get_node(label_t(5)) >> cfg.get_node(label_t(4)); + cfg.get_node(label_t::entry) >> cfg.get_node(label_t{1}); + cfg.get_node(label_t{1}) >> cfg.get_node(label_t{2}); + cfg.get_node(label_t{1}) >> cfg.get_node(label_t{4}); + cfg.get_node(label_t{2}) >> cfg.get_node(label_t{3}); + cfg.get_node(label_t{3}) >> cfg.get_node(label_t::exit); + cfg.get_node(label_t{4}) >> cfg.get_node(label_t{3}); + cfg.get_node(label_t{4}) >> cfg.get_node(label_t{5}); + cfg.get_node(label_t{5}) >> cfg.get_node(label_t{4}); const wto_t wto(cfg); @@ -72,17 +72,17 @@ TEST_CASE("wto figure 2b", "[wto]") { // Add nodes. for (int i = 1; i <= 4; i++) { - cfg.insert(label_t(i)); + cfg.insert(label_t{i}, Undefined{}); } // Add edges. - cfg.get_node(label_t::entry) >> cfg.get_node(label_t(1)); - cfg.get_node(label_t(1)) >> cfg.get_node(label_t(2)); - cfg.get_node(label_t(1)) >> cfg.get_node(label_t(4)); - cfg.get_node(label_t(2)) >> cfg.get_node(label_t(3)); - cfg.get_node(label_t(3)) >> cfg.get_node(label_t(1)); - cfg.get_node(label_t(3)) >> cfg.get_node(label_t::exit); - cfg.get_node(label_t(4)) >> cfg.get_node(label_t(3)); + cfg.get_node(label_t::entry) >> cfg.get_node(label_t{1}); + cfg.get_node(label_t{1}) >> cfg.get_node(label_t{2}); + cfg.get_node(label_t{1}) >> cfg.get_node(label_t{4}); + cfg.get_node(label_t{2}) >> cfg.get_node(label_t{3}); + cfg.get_node(label_t{3}) >> cfg.get_node(label_t{1}); + cfg.get_node(label_t{3}) >> cfg.get_node(label_t::exit); + cfg.get_node(label_t{4}) >> cfg.get_node(label_t{3}); const wto_t wto(cfg); diff --git a/test-data/jump.yaml b/test-data/jump.yaml index 2ff819504..decbd2910 100644 --- a/test-data/jump.yaml +++ b/test-data/jump.yaml @@ -1,5 +1,23 @@ # Copyright (c) Prevail Verifier contributors. # SPDX-License-Identifier: MIT +--- +test-case: jump to fallthrough + +pre: [] + +code: + : | + r0 = 0 + if r0 != 0 goto + : | + exit + +post: + - r0.type=number + - r0.svalue=0 + - r0.uvalue=0 +messages: [] + --- test-case: simple conditional jump forward diff --git a/test-data/loop.yaml b/test-data/loop.yaml index a0f3d939a..e47f1a6e0 100644 --- a/test-data/loop.yaml +++ b/test-data/loop.yaml @@ -186,7 +186,7 @@ post: - "pc[1]=[1, +oo]" messages: - - "1: Loop counter is too large (pc[1] < 100000)" + - "1 (counter): Loop counter is too large (pc[1] < 100000)" --- test-case: realistic forward loop @@ -207,8 +207,8 @@ code: r2 -= r1 r3 = 0 r0 = 0 -# r2 <<= 32; this fails with "11: Upper bound must be at most packet_size (valid_access(r4.offset, width=1) for read)" -# r2 >>= 32 + # r2 <<= 32; this fails with "11: Upper bound must be at most packet_size (valid_access(r4.offset, width=1) for read)" + # r2 >>= 32 : | r4 = r1 r4 += r3 @@ -283,7 +283,7 @@ post: [] messages: - "1:2: Code is unreachable after 1:2" - - "0: Loop counter is too large (pc[0] < 100000)" + - "0 (counter): Loop counter is too large (pc[0] < 100000)" --- test-case: simple infinite loop, less than or equal options: ["termination"] @@ -300,7 +300,7 @@ post: [] messages: - "1:2: Code is unreachable after 1:2" - - "0: Loop counter is too large (pc[0] < 100000)" + - "0 (counter): Loop counter is too large (pc[0] < 100000)" --- test-case: simple infinite loop, equal @@ -318,7 +318,7 @@ post: [] messages: - "1:2: Code is unreachable after 1:2" - - "0: Loop counter is too large (pc[0] < 100000)" + - "0 (counter): Loop counter is too large (pc[0] < 100000)" --- test-case: simple infinite loop, greater than @@ -336,7 +336,7 @@ post: [] messages: - "1:2: Code is unreachable after 1:2" - - "0: Loop counter is too large (pc[0] < 100000)" + - "0 (counter): Loop counter is too large (pc[0] < 100000)" --- test-case: simple infinite loop, greater than or equal @@ -354,7 +354,7 @@ post: [] messages: - "1:2: Code is unreachable after 1:2" - - "0: Loop counter is too large (pc[0] < 100000)" + - "0 (counter): Loop counter is too large (pc[0] < 100000)" --- test-case: infinite loop with multiple exits options: ["termination"] @@ -371,7 +371,7 @@ post: [] messages: - "1:2: Code is unreachable after 1:2" - "3:4: Code is unreachable after 3:4" - - "0: Loop counter is too large (pc[0] < 100000)" + - "0 (counter): Loop counter is too large (pc[0] < 100000)" --- # Note: This test case terminates after 1000001 iterations, but the verifier assumes that the loop is infinite @@ -394,7 +394,7 @@ post: - "r0.type=number" - "r0.uvalue=1000001" messages: - - "0: Loop counter is too large (pc[0] < 100000)" + - "0 (counter): Loop counter is too large (pc[0] < 100000)" --- test-case: possible infinite loop @@ -413,7 +413,7 @@ post: - "r0.type=number" messages: - - "0: Loop counter is too large (pc[0] < 100000)" + - "0 (counter): Loop counter is too large (pc[0] < 100000)" --- # Check for case where there are backwards jumps that don't form a loop. @@ -461,5 +461,5 @@ post: [] messages: - "1:3: Code is unreachable after 1:3" - - "2: Loop counter is too large (pc[2] < 100000)" + - "2 (counter): Loop counter is too large (pc[2] < 100000)" - "2:3: Code is unreachable after 2:3" diff --git a/test-data/uninit.yaml b/test-data/uninit.yaml index 9dcb18a44..aada2a9d1 100644 --- a/test-data/uninit.yaml +++ b/test-data/uninit.yaml @@ -12,11 +12,11 @@ code: : | r0 += r3 -post: [] +post: + - "r0.type=uninit" messages: - "0: Invalid type (r3.type in {number, ctx, stack, packet, shared})" - - "CRAB ERROR: Cannot convert bottom to tuple" --- test-case: subtraction of a number and an uninitialized register