Emit warning if exit is unreachable.

Emit warning if maximum number of iterations is reached.

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

src/crab_verifier.cpp

@@ -23,6 +23,10 @@
 using crab::ebpf_domain_t;
 using std::string;
 
+// Maximum number of loop iterations allowed before considering the loop potentially non-terminating.
+// This bound helps detect infinite loops while allowing reasonable finite loops to pass verification.
+const crab::number_t TERMINATION_BOUND = 100000;
+
 thread_local crab::lazy_allocator<program_info> global_program_info;
 thread_local ebpf_verifier_options_t thread_local_options;
 
@@ -97,7 +101,27 @@ 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();
+
+        // If the exit is unreachable, we can't be sure if the program is terminating.
+        // Add a warning to fail the verification.
+        if (last_inv.is_bottom()) {
+            m_db.add_warning(label_t::exit, "Exit is unreachable.");
+        }
+
+        // Check if the loop count breached the termination bound.
+        // If so, add a warning to fail the verification.
+        if (m_db.max_loop_count > TERMINATION_BOUND) {
+
+            if (m_db.max_loop_count.number().has_value()) {
+                m_db.add_warning(label_t::exit, "Could not prove termination (loop count is " +
+                                                    m_db.max_loop_count.number()->to_string() + " but limit is " +
+                                                    TERMINATION_BOUND.to_string() + ").");
+            } else {
+                m_db.add_warning(label_t::exit, "Could not prove termination (maximum loop count is unknown).");
+            }
+        }
     }
+
     return m_db;
 }
 
@@ -127,10 +151,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."
+  - "exit: Could not prove termination (maximum loop count is unknown)."
 
 ---
 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"
+  - "exit: Exit is unreachable."
+---
+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"
+  - "exit: Exit is unreachable."
+
+---
+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"
+  - "exit: Exit is unreachable."
+
+---
+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"
+  - "exit: Exit is unreachable."
+
+---
+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"
+  - "exit: Exit is unreachable."
+---
+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"
+  - "exit: Exit is unreachable."
+
+---
+# 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:
+  - "exit: Could not prove termination (loop count is 100001 but limit is 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:
+  - "exit: Could not prove termination (maximum loop count is unknown)."