Emit warning if maximum number of iterations is reached.

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

src/asm_syntax.hpp

@@ -397,6 +397,10 @@ 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/crab/ebpf_domain.cpp

@@ -2924,6 +2924,16 @@ 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);
+    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_verifier.cpp

@@ -95,9 +95,16 @@ 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();
+        // Calculate the maximum loop count across all post-invariants to detect potential
+        // infinite loops or excessive iterations in any part of the program.
+        for (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,10 +134,6 @@ 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,

test-data/loop.yaml

@@ -186,7 +186,7 @@ post:
   - "pc[1]=[1, +oo]"
 
 messages:
-  - "Could not prove termination."
+  - "1: Cannot prove termination (Label 1 loop count +oo <= 100000)"
 
 ---
 test-case: realistic forward loop
@@ -266,3 +266,151 @@ post:
   - r4.uvalue-r2.svalue<=0
   - r4.uvalue-r2.uvalue<=0
   - r4.uvalue=[1, 255]
+
+---
+test-case: simple infinite loop, less than
+options: ["termination"]
+
+pre: []
+
+code:
+  <start>: |
+    r0 = 0
+    if r0 < 1 goto <start>
+    exit
+
+post: []
+
+messages:
+  - "1:2: Code is unreachable after 1:2"
+  - "0: Cannot prove termination (Label 0 loop count +oo <= 100000)"
+---
+test-case: simple infinite loop, less than or equal
+options: ["termination"]
+
+pre: []
+
+code:
+  <start>: |
+    r0 = 0
+    if r0 <= 1 goto <start>
+    exit
+
+post: []
+
+messages:
+  - "1:2: Code is unreachable after 1:2"
+  - "0: Cannot prove termination (Label 0 loop count +oo <= 100000)"
+
+---
+test-case: simple infinite loop, equal
+options: ["termination"]
+
+pre: []
+
+code:
+  <start>: |
+    r0 = 0
+    if r0 == 0 goto <start>
+    exit
+
+post: []
+
+messages:
+  - "1:2: Code is unreachable after 1:2"
+  - "0: Cannot prove termination (Label 0 loop count +oo <= 100000)"
+
+---
+test-case: simple infinite loop, greater than
+options: ["termination"]
+
+pre: []
+
+code:
+  <start>: |
+    r0 = 1
+    if r0 > 0 goto <start>
+    exit
+
+post: []
+
+messages:
+  - "1:2: Code is unreachable after 1:2"
+  - "0: Cannot prove termination (Label 0 loop count +oo <= 100000)"
+
+---
+test-case: simple infinite loop, greater than or equal
+options: ["termination"]
+
+pre: []
+
+code:
+  <start>: |
+    r0 = 1
+    if r0 >= 0 goto <start>
+    exit
+
+post: []
+
+messages:
+  - "1:2: Code is unreachable after 1:2"
+  - "0: Cannot prove termination (Label 0 loop count +oo <= 100000)"
+---
+test-case: infinite loop with multiple exits
+options: ["termination"]
+pre: []
+code:
+  <start>: |
+    r0 = 1
+    if r0 > 0 goto <loop1>
+    exit
+  <loop1>: |
+    if r0 < 2 goto <start>
+    exit
+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)"
+
+---
+# 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
+options: ["termination"]
+pre: [r0.type=number, r0.svalue=0, r0.uvalue=0]
+code:
+  <start>: |
+    r0 += 1
+    if r0 < 100001 goto <start>
+  <out>: |
+    exit
+post:
+  - "pc[0]=100001"
+  - "pc[0]=r0.svalue"
+  - "pc[0]=r0.uvalue"
+  - "r0.svalue=100001"
+  - "r0.svalue=r0.uvalue"
+  - "r0.type=number"
+  - "r0.uvalue=100001"
+messages:
+  - "0: Cannot prove termination (Label 0 loop count 100001 <= 100000)"
+
+---
+test-case: possible infinite loop
+options: ["termination"]
+
+pre: [r0.type=number]
+code:
+  <start>: |
+    if r0 > 0 goto <start>
+    exit
+
+post:
+  - "pc[0]=[1, +oo]"
+  - "r0.svalue=0"
+  - "r0.uvalue=0"
+  - "r0.type=number"
+
+messages:
+  - "0: Cannot prove termination (Label 0 loop count +oo <= 100000)"