Reduce coupling between control flow graph and instructions

src/asm_files.cpp

@@ -205,8 +205,7 @@ struct function_relocation {
     string target_function_name;
 };
 
-static raw_program* find_subprogram(vector<raw_program>& programs,
-                                    const ELFIO::section& subprogram_section,
+static raw_program* find_subprogram(vector<raw_program>& programs, const ELFIO::section& subprogram_section,
                                     const std::string& symbol_name) {
     // Find subprogram by name.
     for (auto& subprog : programs) {
@@ -219,8 +218,8 @@ static raw_program* find_subprogram(vector<raw_program>& programs,
 
 // Returns an error message, or empty string on success.
 static std::string append_subprograms(raw_program& prog, vector<raw_program>& programs,
-                                      const vector<function_relocation>& function_relocations, const ELFIO::elfio& reader,
-                                      const ELFIO::const_symbol_section_accessor& symbols) {
+                                      const vector<function_relocation>& function_relocations,
+                                      const ELFIO::elfio& reader, const ELFIO::const_symbol_section_accessor& symbols) {
     if (prog.resolved_subprograms) {
         // We've already appended any relevant subprograms.
         return {};

src/asm_ostream.cpp

@@ -23,23 +23,6 @@ using std::optional;
 using std::string;
 using std::vector;
 
-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;
-            }
-        }
-    }
-};
-
 namespace crab {
 
 std::string number_t::to_string() const { return _n.str(); }
@@ -76,52 +59,29 @@ string to_string(label_t const& 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=\"";
+} // namespace crab
 
-        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";
+struct LineInfoPrinter {
+    std::ostream& os;
+    std::string previous_source_line;
 
-        out << "\"];\n";
-        for (const label_t& next : value.next_labels_set()) {
-            out << "    \"" << label << "\" -> \"" << next << "\";\n";
+    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;
+            }
         }
-        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);
-}
-
-void print_label(std::ostream& o, const value_t& value) { o << value.label() << ":\n"; }
-
-void print_assertions(std::ostream& o, const value_t& value) {
-    for (const auto& pre : value.instruction().preconditions) {
-        o << "  "
-          << "assert " << pre << ";\n";
     }
-}
-
-void print_instruction(std::ostream& o, const value_t& value) { o << "  " << value.instruction().cmd << ";\n"; }
+};
 
-void print_goto(std::ostream& o, const value_t& value) {
-    auto [it, et] = value.next_labels();
+void print_jump(std::ostream& o, const std::string& direction, const std::set<label_t>& labels) {
+    auto [it, et] = std::pair{labels.begin(), labels.end()};
     if (it != et) {
-        o << "  "
-          << "goto ";
+        o << "  " << direction << " ";
         while (it != et) {
             o << *it;
             ++it;
@@ -135,49 +95,59 @@ void print_goto(std::ostream& o, const value_t& value) {
     o << "\n";
 }
 
-void print_from(std::ostream& o, const value_t& value) {
-    auto [it, et] = value.prev_labels();
-    if (it != et) {
-        o << "  "
-          << "from ";
-        while (it != et) {
-            o << *it;
-            ++it;
-            if (it == et) {
-                o << ";";
-            } else {
-                o << ",";
+void print_cfg(const crab::cfg_t& cfg, std::ostream& os, const bool simplify, const printfunc& prefunc,
+               const printfunc& postfunc) {
+    LineInfoPrinter printer{os};
+    for (const crab::basic_block_t& bb : crab::basic_block_t::collect_basic_blocks(cfg, simplify)) {
+        prefunc(os, bb.first_label());
+        print_jump(os, "from", cfg.parents_of(bb.first_label()));
+        os << bb.first_label() << ":\n";
+        for (const label_t& label : bb) {
+            printer.print_line_info(label);
+            for (const auto& pre : cfg.assertions_at(label)) {
+                os << "  " << "assert " << pre << ";\n";
             }
+            os << "  " << cfg.instruction_at(label) << ";\n";
         }
+        print_jump(os, "goto", cfg.children_of(bb.last_label()));
+        postfunc(os, bb.last_label());
     }
-    o << "\n";
+    os << "\n";
 }
 
-static void print_cfg(std::ostream& os, const cfg_t& cfg, const bool simplify, const invariant_table_t* invariants) {
-    LineInfoPrinter printer{os};
-    for (const auto& bb : basic_block_t::collect_basic_blocks(cfg, simplify)) {
-        if (invariants) {
-            os << "\nPre-invariant : " << invariants->at(bb.first_label()).pre << "\n";
-        }
-        const value_t& first_node = cfg.get_node(bb.first_label());
-        print_from(os, first_node);
-        print_label(os, first_node);
-        for (const label_t& label : bb) {
-            printer.print_line_info(label);
-            const value_t& node = cfg.get_node(label);
-            print_assertions(os, node);
-            print_instruction(os, node);
+static void nop(std::ostream&, const label_t&) {}
+
+void print_cfg(const crab::cfg_t& cfg, std::ostream& os, const bool simplify) {
+    print_cfg(cfg, os, simplify, nop, nop);
+}
+
+void print_dot(const crab::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=\"";
+
+        for (const auto& pre : cfg.assertions_at(label)) {
+            out << "assert " << pre << "\\l";
         }
-        print_goto(os, cfg.get_node(bb.last_label()));
-        if (invariants) {
-            os << "\nPost-invariant: " << invariants->at(bb.last_label()).post << "\n";
+        out << cfg.instruction_at(label) << "\\l";
+
+        out << "\"];\n";
+        for (const label_t& next : cfg.children_of(label)) {
+            out << "    \"" << label << "\" -> \"" << next << "\";\n";
         }
+        out << "\n";
     }
-    os << "\n";
+    out << "}\n";
 }
-void print_cfg(std::ostream& os, const cfg_t& cfg, const bool simplify) { print_cfg(os, cfg, simplify, nullptr); }
 
-} // namespace crab
+void print_dot(const crab::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);
+}
 
 void print_reachability(std::ostream& os, const Report& report) {
     for (const auto& [label, notes] : report.reachability) {
@@ -204,8 +174,15 @@ void print_all_messages(std::ostream& os, const Report& report) {
     print_warnings(os, report);
 }
 
-void print_invariants(std::ostream& os, const cfg_t& cfg, const bool simplify, const Invariants& invariants) {
-    print_cfg(os, cfg, simplify, &invariants.invariants);
+void print_invariants(std::ostream& os, const crab::cfg_t& cfg, const bool simplify, const Invariants& invariants) {
+    print_cfg(
+        cfg, os, simplify,
+        [&](std::ostream& os, const label_t& label) -> void {
+            os << "\nPre-invariant : " << invariants.invariants.at(label).pre << "\n";
+        },
+        [&](std::ostream& os, const label_t& label) -> void {
+            os << "\nPost-invariant : " << invariants.invariants.at(label).post << "\n";
+        });
 }
 
 namespace asm_syntax {
@@ -631,13 +608,9 @@ void print(const InstructionSeq& insts, std::ostream& out, const std::optional<c
 } // namespace asm_syntax
 
 std::ostream& operator<<(std::ostream& o, const EbpfMapDescriptor& desc) {
-    return o << "("
-             << "original_fd = " << desc.original_fd << ", "
-             << "inner_map_fd = " << desc.inner_map_fd << ", "
-             << "type = " << desc.type << ", "
-             << "max_entries = " << desc.max_entries << ", "
-             << "value_size = " << desc.value_size << ", "
-             << "key_size = " << desc.key_size << ")";
+    return o << "(" << "original_fd = " << desc.original_fd << ", " << "inner_map_fd = " << desc.inner_map_fd << ", "
+             << "type = " << desc.type << ", " << "max_entries = " << desc.max_entries << ", "
+             << "value_size = " << desc.value_size << ", " << "key_size = " << desc.key_size << ")";
 }
 
 void print_map_descriptors(const std::vector<EbpfMapDescriptor>& descriptors, std::ostream& o) {
@@ -652,4 +625,4 @@ 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;
-}
+}

src/asm_parse.cpp

@@ -212,7 +212,7 @@ Instruction parse_instruction(const std::string& line, const std::map<std::strin
             .cond =
                 Condition{
                     .op = str_to_cmpop.at(m[2]), .left = reg(m[1]), .right = reg_or_imm(m[3]), .is64 = is64_reg(m[1])},
-            .is_explicit = true,
+            .is_implicit = false,
         };
         return res;
     }

src/asm_syntax.hpp

@@ -237,8 +237,8 @@ struct Undefined {
 struct Assume {
     Condition cond;
 
-    // True if the condition is explicitly written in the program (for tests).
-    bool is_explicit{};
+    // True if the condition is implicitly written in the program (False for tests).
+    bool is_implicit{true};
 
     constexpr bool operator==(const Assume&) const = default;
 };

src/asm_unmarshal.cpp

@@ -6,6 +6,7 @@
 #include <vector>
 
 #include "asm_unmarshal.hpp"
+#include "crab_utils/debug.hpp"
 #include "crab_utils/num_safety.hpp"
 #include "ebpf_vm_isa.hpp"
 
@@ -416,8 +417,8 @@ struct Unmarshaller {
     }
 
     [[nodiscard]]
-    auto makeLddw(const ebpf_inst inst, const int32_t next_imm, const vector<ebpf_inst>& insts, const pc_t pc) const
-        -> Instruction {
+    auto makeLddw(const ebpf_inst inst, const int32_t next_imm, const vector<ebpf_inst>& insts,
+                  const pc_t pc) const -> Instruction {
         if (!info.platform->supports_group(bpf_conformance_groups_t::base64)) {
             throw InvalidInstruction{pc, inst.opcode};
         }

src/assertions.cpp

@@ -1,7 +1,7 @@
 // Copyright (c) Prevail Verifier contributors.
 // SPDX-License-Identifier: MIT
+#include <cassert>
 #include <cinttypes>
-
 #include <utility>
 #include <vector>
 
@@ -177,7 +177,7 @@ class AssertExtractor {
     }
 
     vector<Assertion> operator()(const Assume& ins) const {
-        if (ins.is_explicit) {
+        if (!ins.is_implicit) {
             return explicate(ins.cond);
         }
         return {};
@@ -297,19 +297,11 @@ class AssertExtractor {
     }
 };
 
-vector<Assertion> get_assertions(Instruction ins, const program_info& info, const std::optional<label_t>& label) {
-    return std::visit(AssertExtractor{info, label}, ins);
-}
-
 /// Annotate the CFG by adding explicit assertions for all the preconditions
 /// of any instruction. For example, jump instructions are asserted not to
 /// compare numbers and pointers, or pointers to potentially distinct memory
 /// 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, value] : cfg) {
-        (void)label; // unused
-        auto& ins = value.instruction();
-        ins.preconditions = get_assertions(ins.cmd, info, value.label());
-    }
+vector<Assertion> get_assertions(Instruction ins, const program_info& info, const std::optional<label_t>& label) {
+    return std::visit(AssertExtractor{info, label}, ins);
 }

src/config.hpp

@@ -2,7 +2,12 @@
 // SPDX-License-Identifier: MIT
 #pragma once
 
-#include "crab/cfg.hpp"
+struct prepare_cfg_options {
+    /// When true, verifies that the program terminates.
+    bool check_for_termination = false;
+    /// When true, ensures the program has a valid exit block.
+    bool must_have_exit = true;
+};
 
 struct verbosity_options_t {
     /// When true, prints simplified control flow graph by merging chains into basic blocks.