From 56ba4ea3a0418680b6216570701ff7393cc02e4f Mon Sep 17 00:00:00 2001 From: Elazar Gershuni Date: Sun, 10 Nov 2024 22:28:55 +0200 Subject: [PATCH] CR and moving namespaces around Signed-off-by: Elazar Gershuni --- src/asm_marshal.cpp | 2 +- src/asm_ostream.cpp | 214 ++++++++++++++++++---------------- src/asm_syntax.hpp | 47 ++------ src/crab/cfg.hpp | 66 +---------- src/crab/ebpf_checker.cpp | 1 + src/crab/label.hpp | 33 +++++- src/crab_verifier.cpp | 2 - src/spec_type_descriptors.hpp | 6 +- 8 files changed, 160 insertions(+), 211 deletions(-) diff --git a/src/asm_marshal.cpp b/src/asm_marshal.cpp index 4ac4284de..953435b70 100644 --- a/src/asm_marshal.cpp +++ b/src/asm_marshal.cpp @@ -292,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 093d21351..ddd7022c6 100644 --- a/src/asm_ostream.cpp +++ b/src/asm_ostream.cpp @@ -11,6 +11,7 @@ #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" @@ -20,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"; @@ -354,32 +462,6 @@ struct CommandPrinterVisitor { }; // ReSharper restore CppMemberFunctionMayBeConst -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(); -} - std::ostream& operator<<(std::ostream& os, Instruction const& ins) { std::visit(CommandPrinterVisitor{os}, ins); return os; @@ -452,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); @@ -465,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& 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 crab::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; -} - 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_syntax.hpp b/src/asm_syntax.hpp index 5fe599bbb..ae04c59a7 100644 --- a/src/asm_syntax.hpp +++ b/src/asm_syntax.hpp @@ -2,11 +2,8 @@ // SPDX-License-Identifier: MIT #pragma once -#include -#include #include #include -#include #include #include #include @@ -362,42 +359,6 @@ 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; - -} // namespace asm_syntax - -using namespace asm_syntax; - -// 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::ostream& operator<<(std::ostream& os, const label_t& label); -std::string to_string(label_t const& label); - std::ostream& operator<<(std::ostream& os, Instruction const& ins); std::string to_string(Instruction const& ins); @@ -416,6 +377,14 @@ inline std::ostream& operator<<(std::ostream& os, Value const& 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... { using Ts::operator()...; diff --git a/src/crab/cfg.hpp b/src/crab/cfg.hpp index bc1935646..678d1312e 100644 --- a/src/crab/cfg.hpp +++ b/src/crab/cfg.hpp @@ -37,7 +37,7 @@ class value_t final { private: label_t m_label; - GuardedInstruction m_instruction; + GuardedInstruction m_instruction{.cmd = Undefined{}}; label_vec_t m_prev, m_next; public: @@ -484,60 +484,11 @@ class basic_block_t final { 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 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())); - } -}; - -inline void cfg_t::remove_unreachable_blocks() { - visited_t alive, dead; - mark_alive_blocks(entry_label(), *this, alive); - - 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 @@ -559,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::value_t& value); -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 c98894e4f..4d734780d 100644 --- a/src/crab/ebpf_checker.cpp +++ b/src/crab/ebpf_checker.cpp @@ -7,6 +7,7 @@ #include #include +#include "asm_syntax.hpp" #include "asm_unmarshal.hpp" #include "config.hpp" #include "crab/array_domain.hpp" diff --git a/src/crab/label.hpp b/src/crab/label.hpp index 81736e16f..db8c55ea5 100644 --- a/src/crab/label.hpp +++ b/src/crab/label.hpp @@ -3,7 +3,10 @@ #pragma once #include +#include #include +#include +#include #include #include #include @@ -61,7 +64,31 @@ struct label_t { inline const label_t label_t::entry{-1}; inline const label_t label_t::exit{INT_MAX}; -} // namespace crab +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); + }; +} -std::ostream& operator<<(std::ostream& os, const crab::label_t& label); -std::string to_string(crab::label_t const& label); +// 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_verifier.cpp b/src/crab_verifier.cpp index d08d92e0d..00695c18e 100644 --- a/src/crab_verifier.cpp +++ b/src/crab_verifier.cpp @@ -20,8 +20,6 @@ #include "crab_verifier.hpp" #include "string_constraints.hpp" -#include - using crab::ebpf_domain_t; using std::string; 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;