Emit warning if maximum number of iterations is reached.

Signed-off-by: Alan Jowett <[email protected]>

src/asm_cfg.cpp

@@ -359,10 +359,20 @@ std::map<std::string, int> collect_stats(const cfg_t& cfg) {
 }
 
 cfg_t prepare_cfg(const InstructionSeq& prog, const program_info& info, const bool simplify,
-                  const bool must_have_exit) {
+                  const bool check_for_termination, const bool must_have_exit) {
     // Convert the instruction sequence to a deterministic control-flow graph.
     cfg_t det_cfg = instruction_seq_to_cfg(prog, must_have_exit);
 
+    if (check_for_termination) {
+        // Insert loop counter instructions at potential loop entry points to enforce
+        // an upper bound on iterations. The IncrementLoopCounter instruction will
+        // trigger a verification failure if the loop count exceeds the defined limit.
+        for (auto const& this_label : det_cfg.potential_loop_headers()) {
+            basic_block_t& bb = det_cfg.get_node(this_label);
+            bb.insert_front(IncrementLoopCounter{this_label});
+        }
+    }
+
     // Annotate the CFG by adding in assertions before every memory instruction.
     explicate_assertions(det_cfg, info);
 

src/asm_ostream.cpp

@@ -135,6 +135,10 @@ std::ostream& operator<<(std::ostream& os, ValidAccess const& a) {
     return os;
 }
 
+std::ostream& operator<<(std::ostream& os, const BoundedLoopCount& a) {
+    return os << crab::variable_t::loop_counter(to_string(a.name)) << " < " << a.limit;
+}
+
 static crab::variable_t typereg(const Reg& r) { return crab::variable_t::reg(crab::data_kind_t::types, r.v); }
 
 std::ostream& operator<<(std::ostream& os, ValidSize const& a) {

src/asm_syntax.hpp

@@ -397,8 +397,17 @@ struct ZeroCtxOffset {
     constexpr bool operator==(const ZeroCtxOffset&) const = default;
 };
 
+struct BoundedLoopCount {
+    label_t name;
+    bool operator==(const BoundedLoopCount&) const = default;
+    // Maximum number of loop iterations allowed during verification.
+    // This prevents infinite loops while allowing reasonable bounded loops.
+    // When exceeded, verification fails as the loop might not terminate.
+    static constexpr int limit = 100000;
+};
+
 using AssertionConstraint = std::variant<Comparable, Addable, ValidDivisor, ValidAccess, ValidStore, ValidSize,
-                                         ValidMapKeyValue, ValidCall, TypeConstraint, FuncConstraint, ZeroCtxOffset>;
+                                         ValidMapKeyValue, ValidCall, TypeConstraint, FuncConstraint, ZeroCtxOffset, BoundedLoopCount>;
 
 struct Assert {
     AssertionConstraint cst;

src/assertions.cpp

@@ -47,9 +47,8 @@ class AssertExtractor {
         return {};
     }
 
-    vector<Assert> operator()(IncrementLoopCounter) const {
-        assert(false);
-        return {};
+    vector<Assert> operator()(IncrementLoopCounter& ipc) const {
+        return {{BoundedLoopCount{ipc.name}}};
     }
 
     vector<Assert> operator()(LoadMapFd const&) const { return {}; }

src/crab/cfg.hpp

@@ -65,6 +65,19 @@ class basic_block_t final {
         m_ts.push_back(arg);
     }
 
+    template <typename T, typename... Args>
+    void insert_front(Args&&... args) {
+        assert(label() != label_t::entry);
+        assert(label() != label_t::exit);
+        m_ts.insert(m_ts.begin(), T{std::forward<Args>(args)...});
+    }
+
+    void insert_front(const Instruction& 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(_label) {}
 
     ~basic_block_t() = default;
@@ -156,6 +169,22 @@ class basic_block_t final {
     }
 
     void swap_instructions(stmt_list_t& ts) { std::swap(m_ts, ts); }
+
+    bool has_backwards_branch() const {
+        // If this is an exit block, then it's not a loop header.
+        if (m_label == label_t::exit) {
+            return false;
+        }
+
+        // If there is a previous block that has a higher instruction number
+        // than this block, then this block has a backwards branch.
+        for (const auto& prev : m_prev) {
+            if (prev.from >= m_label.from) {
+                return true;
+            }
+        }
+        return false;
+    }
 };
 
 // Viewing basic_block_t with all statements reversed. Useful for
@@ -425,6 +454,17 @@ class cfg_t final {
         return labels;
     }
 
+    [[nodiscard]]
+    std::vector<label_t> potential_loop_headers() const {
+        std::vector<label_t> res;
+        for (const auto& label : labels()) {
+            if (get_node(label).has_backwards_branch()) {
+                res.emplace_back(label);
+            }
+        }
+        return res;
+    }
+
   private:
     // Helpers
     [[nodiscard]]
@@ -611,7 +651,8 @@ std::vector<std::string> stats_headers();
 
 std::map<std::string, int> collect_stats(const cfg_t&);
 
-cfg_t prepare_cfg(const InstructionSeq& prog, const program_info& info, bool simplify, bool must_have_exit = true);
+cfg_t prepare_cfg(const InstructionSeq& prog, const program_info& info, bool simplify, bool check_for_termination,
+                  bool must_have_exit = true);
 
 void explicate_assertions(cfg_t& cfg, const program_info& info);
 std::vector<Assert> get_assertions(Instruction ins, const program_info& info, const std::optional<label_t>& label);

src/crab/ebpf_domain.cpp

@@ -1435,6 +1435,12 @@ void ebpf_domain_t::operator()(const TypeConstraint& s) {
     }
 }
 
+void ebpf_domain_t::operator()(const BoundedLoopCount& s){
+    using namespace crab::dsl_syntax;
+    const auto counter = variable_t::loop_counter(to_string(s.name));
+    require(m_inv, counter <= s.limit, "Loop counter is too large");
+}
+
 void ebpf_domain_t::operator()(const FuncConstraint& s) {
     // Look up the helper function id.
     const reg_pack_t& reg = reg_pack(s.reg);
@@ -2954,6 +2960,7 @@ extended_number ebpf_domain_t::get_loop_count_upper_bound() const {
 }
 
 void ebpf_domain_t::operator()(const IncrementLoopCounter& ins) {
-    this->add(variable_t::loop_counter(to_string(ins.name)), 1);
+    const auto counter = variable_t::loop_counter(to_string(ins.name));
+    this->add(counter, 1);
 }
 } // namespace crab

src/crab/ebpf_domain.hpp

@@ -78,6 +78,7 @@ class ebpf_domain_t final {
     void operator()(const ValidStore&);
     void operator()(const ZeroCtxOffset&);
     void operator()(const IncrementLoopCounter&);
+    void operator()(const BoundedLoopCount&);
 
     void initialize_loop_counter(const label_t& label);
     static ebpf_domain_t calculate_constant_limits();

src/crab/fwd_analyzer.cpp

@@ -50,7 +50,7 @@ class member_component_visitor final {
 class interleaved_fwd_fixpoint_iterator_t final {
     using iterator = invariant_table_t::iterator;
 
-    cfg_t& _cfg;
+    const cfg_t& _cfg;
     wto_t _wto;
     invariant_table_t _pre, _post;
 
@@ -68,7 +68,7 @@ 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) {
-        basic_block_t& bb = _cfg.get_node(label);
+        const basic_block_t& bb = _cfg.get_node(label);
         pre(bb);
         _post[label] = std::move(pre);
     }
@@ -101,7 +101,7 @@ class interleaved_fwd_fixpoint_iterator_t final {
     }
 
   public:
-    explicit interleaved_fwd_fixpoint_iterator_t(cfg_t& cfg) : _cfg(cfg), _wto(cfg) {
+    explicit interleaved_fwd_fixpoint_iterator_t(const cfg_t& cfg) : _cfg(cfg), _wto(cfg) {
         for (const auto& label : _cfg.labels()) {
             _pre.emplace(label, ebpf_domain_t::bottom());
             _post.emplace(label, ebpf_domain_t::bottom());
@@ -116,24 +116,27 @@ class interleaved_fwd_fixpoint_iterator_t final {
 
     void operator()(const std::shared_ptr<wto_cycle_t>& cycle);
 
-    friend std::pair<invariant_table_t, invariant_table_t> run_forward_analyzer(cfg_t& cfg, ebpf_domain_t entry_inv);
+    friend std::pair<invariant_table_t, invariant_table_t> run_forward_analyzer(const cfg_t& cfg, ebpf_domain_t entry_inv);
 };
 
-std::pair<invariant_table_t, invariant_table_t> run_forward_analyzer(cfg_t& cfg, ebpf_domain_t entry_inv) {
+std::pair<invariant_table_t, invariant_table_t> run_forward_analyzer(const cfg_t& cfg, ebpf_domain_t entry_inv) {
     // Go over the CFG in weak topological order (accounting for loops).
     interleaved_fwd_fixpoint_iterator_t analyzer(cfg);
     if (thread_local_options.check_termination) {
-        std::vector<label_t> cycle_heads;
-        for (auto& component : analyzer._wto) {
-            if (const auto pc = std::get_if<std::shared_ptr<wto_cycle_t>>(&component)) {
-                cycle_heads.push_back((*pc)->head());
+        // For every potential loop header, initialize the loop counter to 0.
+        for (const auto& label : cfg.potential_loop_headers()) {
+            // See prepare_cfg() in src/asm_cfg.cpp.
+            // It adds IncrementLoopCounter to blocks that are possible loops, but only
+            // on the first pass, where all labels are in the form from::-1. After the cfg is converted to its
+            // non-deterministic form there will be additional labels in the form of from::to where to will be != -1.
+            // Only initialize the loop counter for the original labels.
+            if (label.to != -1) {
+                continue;
             }
-        }
-        for (const label_t& label : cycle_heads) {
             entry_inv.initialize_loop_counter(label);
-            cfg.get_node(label).insert(IncrementLoopCounter{label});
         }
     }
+
     analyzer.set_pre(cfg.entry_label(), entry_inv);
     for (auto& component : analyzer._wto) {
         std::visit(analyzer, component);

src/crab/fwd_analyzer.hpp

@@ -11,6 +11,6 @@ namespace crab {
 
 using invariant_table_t = std::map<label_t, ebpf_domain_t>;
 
-std::pair<invariant_table_t, invariant_table_t> run_forward_analyzer(cfg_t& cfg, ebpf_domain_t entry_inv);
+std::pair<invariant_table_t, invariant_table_t> run_forward_analyzer(const cfg_t& cfg, ebpf_domain_t entry_inv);
 
 } // namespace crab

src/crab_verifier.cpp

@@ -56,11 +56,11 @@ struct checks_db final {
     checks_db() = default;
 };
 
-static checks_db generate_report(cfg_t& cfg, const crab::invariant_table_t& pre_invariants,
+static checks_db generate_report(const cfg_t& cfg, const crab::invariant_table_t& pre_invariants,
                                  const crab::invariant_table_t& post_invariants) {
     checks_db m_db;
     for (const label_t& label : cfg.sorted_labels()) {
-        basic_block_t& bb = cfg.get_node(label);
+        const basic_block_t& bb = cfg.get_node(label);
         ebpf_domain_t from_inv(pre_invariants.at(label));
         from_inv.set_require_check(
             [&m_db, label](auto& inv, const crab::linear_constraint_t& cst, const std::string& s) {
@@ -95,8 +95,13 @@ static checks_db generate_report(cfg_t& cfg, const crab::invariant_table_t& pre_
     }
 
     if (thread_local_options.check_termination) {
-        const auto last_inv = post_invariants.at(cfg.exit_label());
-        m_db.max_loop_count = last_inv.get_loop_count_upper_bound();
+        // Gather the upper bound of loop counts from post-invariants.
+        for (const auto [label, inv] : post_invariants) {
+            if (inv.is_bottom()) {
+                continue;
+            }
+            m_db.max_loop_count = std::max(m_db.max_loop_count, inv.get_loop_count_upper_bound());
+        }
     }
     return m_db;
 }
@@ -127,13 +132,9 @@ static void print_report(std::ostream& os, const checks_db& db, const Instructio
         }
     }
     os << "\n";
-    const crab::number_t max_loop_count{100000};
-    if (db.max_loop_count > max_loop_count) {
-        os << "Could not prove termination.\n";
-    }
 }
 
-static checks_db get_analysis_report(std::ostream& s, cfg_t& cfg, const crab::invariant_table_t& pre_invariants,
+static checks_db get_analysis_report(std::ostream& s, const cfg_t& cfg, const crab::invariant_table_t& pre_invariants,
                                      const crab::invariant_table_t& post_invariants,
                                      const std::optional<InstructionSeq>& prog = std::nullopt) {
     // Analyze the control-flow graph.
@@ -161,7 +162,7 @@ static checks_db get_analysis_report(std::ostream& s, cfg_t& cfg, const crab::in
     return db;
 }
 
-static checks_db get_ebpf_report(std::ostream& s, cfg_t& cfg, program_info info, const ebpf_verifier_options_t* options,
+static checks_db get_ebpf_report(std::ostream& s, const cfg_t& cfg, program_info info, const ebpf_verifier_options_t* options,
                                  const std::optional<InstructionSeq>& prog = std::nullopt) {
     global_program_info = std::move(info);
     crab::domains::clear_global_state();
@@ -182,7 +183,7 @@ static checks_db get_ebpf_report(std::ostream& s, cfg_t& cfg, program_info info,
 }
 
 /// Returned value is true if the program passes verification.
-bool run_ebpf_analysis(std::ostream& s, cfg_t& cfg, const program_info& info, const ebpf_verifier_options_t* options,
+bool run_ebpf_analysis(std::ostream& s, const cfg_t& cfg, const program_info& info, const ebpf_verifier_options_t* options,
                        ebpf_verifier_stats_t* stats) {
     if (options == nullptr) {
         options = &ebpf_verifier_default_options;
@@ -219,7 +220,7 @@ std::tuple<string_invariant, bool> ebpf_analyze_program_for_test(std::ostream& o
         throw std::runtime_error("Entry invariant is inconsistent");
     }
     try {
-        cfg_t cfg = prepare_cfg(prog, info, options.simplify, false);
+        const cfg_t cfg = prepare_cfg(prog, info, options.simplify, options.check_termination, false);
         auto [pre_invariants, post_invariants] = run_forward_analyzer(cfg, std::move(entry_inv));
         const checks_db report = get_analysis_report(std::cerr, cfg, pre_invariants, post_invariants);
         print_report(os, report, prog, false);
@@ -242,7 +243,7 @@ bool ebpf_verify_program(std::ostream& os, const InstructionSeq& prog, const pro
 
     // Convert the instruction sequence to a control-flow graph
     // in a "passive", non-deterministic form.
-    cfg_t cfg = prepare_cfg(prog, info, options->simplify);
+    const cfg_t cfg = prepare_cfg(prog, info, options->simplify, options->check_termination);
 
     std::optional<InstructionSeq> prog_opt = std::nullopt;
     if (options->print_failures) {

src/crab_verifier.hpp

@@ -7,7 +7,7 @@
 #include "spec_type_descriptors.hpp"
 #include "string_constraints.hpp"
 
-bool run_ebpf_analysis(std::ostream& s, cfg_t& cfg, const program_info& info, const ebpf_verifier_options_t* options,
+bool run_ebpf_analysis(std::ostream& s, const cfg_t& cfg, const program_info& info, const ebpf_verifier_options_t* options,
                        ebpf_verifier_stats_t* stats);
 
 bool ebpf_verify_program(std::ostream& os, const InstructionSeq& prog, const program_info& info,

src/main/check.cpp

@@ -250,7 +250,7 @@ int main(int argc, char** argv) {
         return !res;
     } else if (domain == "stats") {
         // Convert the instruction sequence to a control-flow graph.
-        cfg_t cfg = prepare_cfg(prog, raw_prog.info, ebpf_verifier_options.simplify);
+        const cfg_t cfg = prepare_cfg(prog, raw_prog.info, ebpf_verifier_options.simplify, ebpf_verifier_options.check_termination);
 
         // Just print eBPF program stats.
         auto stats = collect_stats(cfg);
@@ -264,7 +264,7 @@ int main(int argc, char** argv) {
         std::cout << "\n";
     } else if (domain == "cfg") {
         // Convert the instruction sequence to a control-flow graph.
-        cfg_t cfg = prepare_cfg(prog, raw_prog.info, ebpf_verifier_options.simplify);
+        const cfg_t cfg = prepare_cfg(prog, raw_prog.info, ebpf_verifier_options.simplify, ebpf_verifier_options.check_termination);
         std::cout << cfg;
         std::cout << "\n";
     } else {

src/test/test_verify.cpp

@@ -586,7 +586,7 @@ TEST_SECTION_FAIL("cilium", "bpf_xdp_snat_linux.o", "2/16")
 // False positive, unknown cause
 TEST_SECTION_FAIL("linux", "test_map_in_map_kern.o", "kprobe/sys_connect")
 
-void test_analyze_thread(cfg_t* cfg, program_info* info, bool* res) {
+void test_analyze_thread(const cfg_t* cfg, program_info* info, bool* res) {
     *res = run_ebpf_analysis(std::cout, *cfg, *info, nullptr, nullptr);
 }
 
@@ -598,15 +598,15 @@ TEST_CASE("multithreading", "[verify][multithreading]") {
     auto prog_or_error1 = unmarshal(raw_prog1);
     auto prog1 = std::get_if<InstructionSeq>(&prog_or_error1);
     REQUIRE(prog1 != nullptr);
-    cfg_t cfg1 = prepare_cfg(*prog1, raw_prog1.info, true);
+    const cfg_t cfg1 = prepare_cfg(*prog1, raw_prog1.info, true, true);
 
     auto raw_progs2 = read_elf("ebpf-samples/bpf_cilium_test/bpf_netdev.o", "2/2", nullptr, &g_ebpf_platform_linux);
     REQUIRE(raw_progs2.size() == 1);
     raw_program raw_prog2 = raw_progs2.back();
     auto prog_or_error2 = unmarshal(raw_prog2);
     auto prog2 = std::get_if<InstructionSeq>(&prog_or_error2);
     REQUIRE(prog2 != nullptr);
-    cfg_t cfg2 = prepare_cfg(*prog2, raw_prog2.info, true);
+    const cfg_t cfg2 = prepare_cfg(*prog2, raw_prog2.info, true, true);
 
     bool res1, res2;
     std::thread a(test_analyze_thread, &cfg1, &raw_prog1.info, &res1);