Simplify loop detection

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

src/asm_cfg.cpp

@@ -366,27 +366,9 @@ cfg_t prepare_cfg(const InstructionSeq& prog, const program_info& info, const bo
 
     if (check_for_termination) {
         // Add IncrementLoopCounter to blocks that are possible loops.
-        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});
-            }
+        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});
         }
     }
 

src/crab/cfg.hpp

@@ -165,6 +165,24 @@ 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 is a loop header.
+        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
@@ -253,6 +271,7 @@ class cfg_t final {
 
   private:
     basic_block_map_t m_blocks;
+    std::optional<std::vector<label_t>> m_potential_loop_headers;
 
     using visited_t = std::set<label_t>;
 
@@ -434,6 +453,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]]

src/crab/fwd_analyzer.cpp

@@ -123,13 +123,13 @@ 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) {
-        // 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 every potential loop header, initialize the loop counter to 0.
+        for (const auto& label : cfg.potential_loop_headers()) {
+            // Skip non-deterministic blocks. Only deterministic blocks have loop counters.
+            if (label.to != -1) {
+                continue;
             }
-
+            entry_inv.initialize_loop_counter(label);
         }
     }