PR feedback

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

src/asm_cfg.cpp

@@ -359,14 +359,18 @@ std::map<std::string, int> collect_stats(const cfg_t& cfg) {
     return res;
 }
 
+// ISSUE: 774 - Rationalize the list of bools being passed to prepare_cfg.
 cfg_t prepare_cfg(const InstructionSeq& prog, const program_info& info, const bool simplify,
                   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);
 
+    // Detect loops using Weak Topological Ordering (WTO) and insert counters at loop entry points. WTO provides a
+    // hierarchical decomposition of the CFG that identifies all strongly connected components (cycles) and their entry
+    // points. These entry points serve as natural locations for loop counters that help verify program termination.
     if (check_for_termination) {
         wto_t wto(det_cfg);
-        wto.visit_loop_heads([&](const label_t& label) {
+        wto.for_each_loop_head([&](const label_t& label) {
             det_cfg.get_node(label).insert_front(IncrementLoopCounter{label});
         });
     }

src/crab/cfg.hpp

@@ -65,13 +65,8 @@ class basic_block_t final {
         m_ts.push_back(arg);
     }
 
-    template <typename T, typename... Args>
-    void insert_front(Args&&... args) {
-        assert(label() != label_t::entry);
-        assert(label() != label_t::exit);
-        m_ts.insert(m_ts.begin(), T{std::forward<Args>(args)...});
-    }
-
+    /// Insert an instruction at the front of the basic block.
+    /// @note Cannot modify entry or exit blocks.
     void insert_front(const Instruction& arg) {
         assert(label() != label_t::entry);
         assert(label() != label_t::exit);

src/crab/fwd_analyzer.cpp

@@ -126,7 +126,8 @@ std::pair<invariant_table_t, invariant_table_t> run_forward_analyzer(const cfg_t
         // Initialize loop counters for potential loop headers.
         // This enables enforcement of upper bounds on loop iterations
         // during program verification.
-        analyzer._wto.visit_loop_heads([&](const label_t& label) { entry_inv.initialize_loop_counter(label); });
+        // TODO: Consider making this an instruction instead of an explicit call.
+        analyzer._wto.for_each_loop_head([&](const label_t& label) { entry_inv.initialize_loop_counter(label); });
     }
     analyzer.set_pre(cfg.entry_label(), entry_inv);
     for (auto& component : analyzer._wto) {

src/crab/wto.hpp

@@ -129,13 +129,12 @@ class wto_t final {
     /**
      * Visit the heads of all loops in the WTO.
      *
-     * @tparam F A callable type with signature void(const label_t&).
      * @param f The callable to be invoked for each loop head.
      *
      * The order in which the heads are visited is not specified.
      */
     template<typename F>
-    void visit_loop_heads(F&& f) const {
+    void for_each_loop_head(F&& f) const {
         for (const auto& component : *this) {
             if (const auto pc = std::get_if<std::shared_ptr<wto_cycle_t>>(&component)) {
                 f((*pc)->head());