PR feedback

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

src/asm_cfg.cpp

@@ -360,10 +360,37 @@ 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) {
+        // Add IncrementLoopCounter to blocks that are joins.
+        for (const auto& this_label : det_cfg.labels()) {
+            // Exit blocks can not be loops.
+            if (this_label == label_t::exit) {
+                continue;
+            }
+
+            auto& basic_block = det_cfg.get_node(this_label);
+
+            // Check if this block has jumps to it from later blocks.
+            bool possible_loop = false;
+            for (auto prev : unique(basic_block.prev_blocks())) {
+                // Check if the jump is backwards or to the same block.
+                if (prev.from >= this_label.from) {
+                    possible_loop = true;
+                    break;
+                }
+            }
+
+            if (possible_loop) {
+
+                basic_block.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

@@ -385,8 +385,17 @@ struct ZeroCtxOffset {
     constexpr bool operator==(const ZeroCtxOffset&) const = default;
 };
 
+struct BoundedLoopCount {
+    label_t name;
+    constexpr 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, the verifier will report that it cannot prove termination.
+    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;
@@ -397,10 +406,6 @@ struct Assert {
 struct IncrementLoopCounter {
     label_t name;
     bool operator==(const IncrementLoopCounter&) const = default;
-    // Maximum number of loop iterations allowed during verification.
-    // This prevents infinite loops while allowing reasonable bounded loops.
-    // When exceeded, the verifier will report that it cannot prove termination.
-    static constexpr int limit = 100000;
 };
 
 using Instruction = std::variant<Undefined, Bin, Un, LoadMapFd, Call, CallLocal, Callx, Exit, Jmp, Mem, Packet, Atomic,

src/assertions.cpp

@@ -41,9 +41,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,15 @@ class basic_block_t final {
         m_ts.push_back(arg);
     }
 
+    template <typename T, typename... Args>
+    void insert_front(Args&&... args) {
+        m_ts.insert(m_ts.begin(), T{std::forward<Args>(args)...});
+    }
+
+    void insert_front(const Instruction& arg) {
+        m_ts.insert(m_ts.begin(), arg);
+    }
+
     explicit basic_block_t(label_t _label) : m_label(_label) {}
 
     ~basic_block_t() = default;
@@ -611,7 +620,7 @@ 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

@@ -1410,6 +1410,12 @@ void ebpf_domain_t::operator()(const TypeConstraint& s) {
     }
 }
 
+void ebpf_domain_t::operator()(const BoundedLoopCount& s){
+    using namespace crab::dsl_syntax;
+    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);
@@ -2926,14 +2932,5 @@ extended_number ebpf_domain_t::get_loop_count_upper_bound() const {
 void ebpf_domain_t::operator()(const IncrementLoopCounter& ins) {
     auto counter = variable_t::loop_counter(to_string(ins.name));
     this->add(counter, 1);
-
-    using namespace crab::dsl_syntax;
-
-    std::ostringstream oss;
-    oss << "Label " << ins.name << " loop count " << m_inv[counter].ub() << " <= " << ins.limit;
-    this->current_assertion = oss.str();
-
-    // Require that the loop counter is bounded.
-    require(this->m_inv, counter <= ins.limit, "Cannot prove termination");
 }
 } // 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

@@ -123,17 +123,16 @@ std::pair<invariant_table_t, invariant_table_t> run_forward_analyzer(cfg_t& cfg,
     // 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 basic block that contains a IncrementLoopCounter, initialize the counter to 0.
+        for (const auto& label : cfg.labels()) {
+            basic_block_t& bb = cfg.get_node(label);
+            if (find_if(bb.begin(), bb.end(), [](const auto& ins) { return std::holds_alternative<IncrementLoopCounter>(ins); }) != bb.end()) {
+                entry_inv.initialize_loop_counter(label);
             }
-        }
-        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_verifier.cpp

@@ -222,7 +222,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);
+        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);
@@ -245,7 +245,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);
+    cfg_t cfg = prepare_cfg(prog, info, options->simplify, options->check_termination);
 
     std::optional<InstructionSeq> prog_opt = std::nullopt;
     if (options->print_failures) {

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);
+        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);
+        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

@@ -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);
+    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);
+    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);

test-data/loop.yaml

@@ -186,7 +186,7 @@ post:
   - "pc[1]=[1, +oo]"
 
 messages:
-  - "1: Cannot prove termination (Label 1 loop count +oo <= 100000)"
+  - "1: Loop counter is too large (pc[1] < 100000)"
 
 ---
 test-case: realistic forward loop
@@ -283,7 +283,7 @@ post: []
 
 messages:
   - "1:2: Code is unreachable after 1:2"
-  - "0: Cannot prove termination (Label 0 loop count +oo <= 100000)"
+  - "0: 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: Cannot prove termination (Label 0 loop count +oo <= 100000)"
+  - "0: 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: Cannot prove termination (Label 0 loop count +oo <= 100000)"
+  - "0: 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: Cannot prove termination (Label 0 loop count +oo <= 100000)"
+  - "0: 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: Cannot prove termination (Label 0 loop count +oo <= 100000)"
+  - "0: Loop counter is too large (pc[0] < 100000)"
 ---
 test-case: infinite loop with multiple exits
 options: ["termination"]
@@ -371,30 +371,30 @@ post: []
 messages:
   - "1:2: Code is unreachable after 1:2"
   - "3:4: Code is unreachable after 3:4"
-  - "0: Cannot prove termination (Label 0 loop count +oo <= 100000)"
+  - "0: Loop counter is too large (pc[0] < 100000)"
 
 ---
 # Note: This test case terminates after 100001 iterations, but the verifier assumes that the loop is infinite
 # because it is greater than the default limit of 100000 iterations.
-test-case: very large loop > 100K iterations
+test-case: very large loop > 1M iterations
 options: ["termination"]
 pre: [r0.type=number, r0.svalue=0, r0.uvalue=0]
 code:
   <start>: |
     r0 += 1
-    if r0 < 100001 goto <start>
+    if r0 < 1000001 goto <start>
   <out>: |
     exit
 post:
-  - "pc[0]=100001"
+  - "pc[0]=1000001"
   - "pc[0]=r0.svalue"
   - "pc[0]=r0.uvalue"
-  - "r0.svalue=100001"
+  - "r0.svalue=1000001"
   - "r0.svalue=r0.uvalue"
   - "r0.type=number"
-  - "r0.uvalue=100001"
+  - "r0.uvalue=1000001"
 messages:
-  - "0: Cannot prove termination (Label 0 loop count 100001 <= 100000)"
+  - "0: Loop counter is too large (pc[0] < 100000)"
 
 ---
 test-case: possible infinite loop
@@ -413,4 +413,4 @@ post:
   - "r0.type=number"
 
 messages:
-  - "0: Cannot prove termination (Label 0 loop count +oo <= 100000)"
+  - "0: Loop counter is too large (pc[0] < 100000)"