PR feedback - switch to wto

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

src/asm_cfg.cpp

@@ -10,6 +10,7 @@
 
 #include "asm_syntax.hpp"
 #include "crab/cfg.hpp"
+#include "crab/wto.hpp"
 
 using std::optional;
 using std::set;
@@ -359,12 +360,16 @@ std::map<std::string, int> collect_stats(const cfg_t& cfg) {
 }
 
 static void annotate_potential_loops(cfg_t& cfg) {
-    // 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 (const auto& this_label : cfg.potential_loop_headers()) {
-        basic_block_t& bb = cfg.get_node(this_label);
-        bb.insert_front(IncrementLoopCounter{this_label});
+    wto_t wto(cfg);
+
+    std::vector<label_t> cycle_heads;
+    for (auto& component : wto) {
+        if (const auto pc = std::get_if<std::shared_ptr<wto_cycle_t>>(&component)) {
+            cycle_heads.push_back((*pc)->head());
+        }
+    }
+    for (const label_t& label : cycle_heads) {
+        cfg.get_node(label).insert_front(IncrementLoopCounter{label});
     }
 }
 

src/crab/cfg.hpp

@@ -169,22 +169,6 @@ 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
@@ -454,18 +438,6 @@ class cfg_t final {
         return labels;
     }
 
-    [[nodiscard]]
-    std::vector<label_t> potential_loop_headers() const {
-        std::vector<label_t> res;
-        res.reserve(m_blocks.size());
-        for (const auto& label : labels()) {
-            if (get_node(label).has_backwards_branch()) {
-                res.emplace_back(label);
-            }
-        }
-        return res;
-    }
-
   private:
     // Helpers
     [[nodiscard]]

src/crab/fwd_analyzer.cpp

@@ -123,20 +123,16 @@ std::pair<invariant_table_t, invariant_table_t> run_forward_analyzer(const cfg_t
     // Go over the CFG in weak topological order (accounting for loops).
     interleaved_fwd_fixpoint_iterator_t analyzer(cfg);
     if (thread_local_options.check_termination) {
-        // 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;
+        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 (const label_t& label : cycle_heads) {
             entry_inv.initialize_loop_counter(label);
         }
     }
-
     analyzer.set_pre(cfg.entry_label(), entry_inv);
     for (auto& component : analyzer._wto) {
         std::visit(analyzer, component);

test-data/loop.yaml

@@ -416,8 +416,7 @@ messages:
   - "0: Loop counter is too large (pc[0] < 100000)"
 
 ---
-# Check for case where the verifier incorrectly assumes that an instruction is the head of a loop
-# when it is not. Verify that it still computes the correct post-state.
+# Check for case where there are backwards jumps that don't form a loop.
 test-case: non-loop backwards jump
 options: ["termination"]
 
@@ -437,7 +436,6 @@ post:
   - "r0.svalue=3"
   - "r0.uvalue=3"
   - "r0.type=number"
-  - pc[2]=1
 
 messages: []