Convert WTO implementation to iterative instead of recursive

Since recusive generates a stack overflow for large programs.
Also:
* Add WTO test
* Fix spelling of Bourdoncle
* Combine wto_cycle_t::initialize() back into the main visit algorithm
  to better match the Bourdoncle paper.

Fixes vbpf#195

Signed-off-by: Dave Thaler <[email protected]>

CMakeLists.txt

@@ -62,6 +62,7 @@ file(GLOB ALL_TEST
         "./src/test/test_marshal.cpp"
         "./src/test/test_termination.cpp"
         "./src/test/test_verify.cpp"
+        "./src/test/test_wto.cpp"
         "./src/test/test_yaml.cpp"
         )
 

src/crab/cfg.hpp

@@ -45,6 +45,7 @@ class basic_block_t final {
     using label_vec_t = std::set<label_t>;
     using stmt_list_t = std::vector<Instruction>;
     using neighbour_const_iterator = label_vec_t::const_iterator;
+    using neighbour_const_reverse_iterator = label_vec_t::const_reverse_iterator;
     using iterator = typename stmt_list_t::iterator;
     using const_iterator = typename stmt_list_t::const_iterator;
     using reverse_iterator = typename stmt_list_t::reverse_iterator;
@@ -86,6 +87,10 @@ class basic_block_t final {
     [[nodiscard]] size_t size() const { return static_cast<size_t>(std::distance(begin(), end())); }
 
     [[nodiscard]] std::pair<neighbour_const_iterator, neighbour_const_iterator> next_blocks() const { return std::make_pair(m_next.begin(), m_next.end()); }
+    [[nodiscard]] std::pair<neighbour_const_reverse_iterator, neighbour_const_reverse_iterator> next_blocks_reversed() const {
+        return std::make_pair(m_next.rbegin(), m_next.rend());
+    }
+
 
     [[nodiscard]] std::pair<neighbour_const_iterator, neighbour_const_iterator> prev_blocks() const { return std::make_pair(m_prev.begin(), m_prev.end()); }
 
@@ -174,8 +179,10 @@ class cfg_t final {
     using node_t = label_t; // for Bgl graphs
 
     using neighbour_const_iterator = typename basic_block_t::neighbour_const_iterator;
+    using neighbour_const_reverse_iterator = typename basic_block_t::neighbour_const_reverse_iterator;
 
     using neighbour_const_range = boost::iterator_range<neighbour_const_iterator>;
+    using neighbour_const_reverse_range = boost::iterator_range<neighbour_const_reverse_iterator>;
 
   private:
     using basic_block_map_t = std::map<label_t, basic_block_t>;
@@ -217,6 +224,9 @@ class cfg_t final {
     [[nodiscard]] neighbour_const_range next_nodes(const label_t& _label) const {
         return boost::make_iterator_range(get_node(_label).next_blocks());
     }
+    [[nodiscard]] neighbour_const_reverse_range next_nodes_reversed(const label_t& _label) const {
+        return boost::make_iterator_range(get_node(_label).next_blocks_reversed());
+    }
 
     [[nodiscard]] neighbour_const_range prev_nodes(const label_t& _label) const {
         return boost::make_iterator_range(get_node(_label).prev_blocks());

src/crab/wto.cpp

@@ -1,19 +1,138 @@
 // Copyright (c) Prevail Verifier contributors.
 // SPDX-License-Identifier: MIT
-#include "asm_syntax.hpp"
 #include "wto.hpp"
 
-// This is the Component() function described in figure 4 of the paper.
-void wto_cycle_t::initialize(class wto_t& wto, const label_t& vertex, std::shared_ptr<wto_cycle_t>& self)
-{
-    // Walk the control flow graph, adding nodes to this cycle.
-    for (const label_t& succ : wto.cfg().next_nodes(vertex)) {
-        if (wto.dfn(succ) == 0) {
-            wto.visit(succ, _components, self);
+#ifndef RECURSIVE_WTO
+
+// This file contains an iterative implementation of the recursive algorithm in
+// Bourdoncle, "Efficient chaotic iteration strategies with widenings", 1993
+// http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.3574
+// where _visit_stack is roughly equivalent to a stack trace in the recursive
+// algorithm.  However, this scales much higher since it does not run out of
+// stack memory.
+
+void wto_t::push_successors(const label_t& vertex, wto_partition_t& partition,
+                            std::weak_ptr<wto_cycle_t> containing_cycle) {
+    if (_vertex_data[vertex].dfn != 0) {
+        // We found an alternate path to a node already visited, so nothing to do.
+        return;
+    }
+    _vertex_data[vertex].dfn = ++_num;
+    _stack.push(vertex);
+
+    // Schedule the next task for this vertex once we're done with anything else.
+    visit_args_t args(visit_task_type_t::StartVisit, vertex, partition, containing_cycle);
+    _visit_stack.push(args);
+
+    for (const label_t& succ : _cfg.next_nodes_reversed(vertex)) {
+        if (_vertex_data[succ].dfn == 0) {
+            visit_args_t args(visit_task_type_t::PushSuccessors, succ, partition, containing_cycle);
+            _visit_stack.push(args);
+        }
+    }
+}
+
+void wto_t::start_visit(const label_t& vertex, wto_partition_t& partition, std::weak_ptr<wto_cycle_t> containing_cycle) {
+    wto_vertex_data_t& vertex_data = _vertex_data[vertex];
+    int head_dfn = vertex_data.dfn;
+    bool loop = false;
+    int min_dfn = INT_MAX;
+    for (const label_t& succ : _cfg.next_nodes(vertex)) {
+        wto_vertex_data_t& data = _vertex_data[succ];
+        if (_vertex_data[succ].head_dfn != 0 && _vertex_data[succ].dfn != INT_MAX) {
+            min_dfn = _vertex_data[succ].head_dfn;
+        } else {
+            min_dfn = _vertex_data[succ].dfn;
+        }
+        if (min_dfn <= head_dfn) {
+            head_dfn = min_dfn;
+            loop = true;
+        }
+    }
+
+    auto cycle = std::make_shared<wto_cycle_t>(containing_cycle);
+    if (head_dfn == vertex_data.dfn) {  
+        vertex_data.dfn = INT_MAX;
+        label_t& element = _stack.top();
+        _stack.pop();
+        if (loop) {
+            while (element != vertex) {
+                _vertex_data[element].dfn = 0;
+                _vertex_data[element].head_dfn = 0;
+                element = _stack.top();
+                _stack.pop();
+            }
+            vertex_data.head_dfn = head_dfn;
+
+            // Stash a reference to the cycle.
+            _vertex_data[vertex].containing_cycle = cycle;
+
+            // Schedule the next task for this vertex once we're done with anything else.
+            visit_args_t args2(visit_task_type_t::ContinueVisit, vertex, partition, cycle);
+            _visit_stack.push(args2);
+
+            // Walk the control flow graph, adding nodes to this cycle.
+            // This is the Component() function described in figure 4 of the paper.
+            for (const label_t& succ : _cfg.next_nodes_reversed(vertex)) {
+                if (dfn(succ) == 0) {
+                    visit_args_t args(visit_task_type_t::PushSuccessors, succ, cycle->components(), cycle);
+                    _visit_stack.push(args);
+                }
+            }
+            return;
+        } else {
+            // Create a new vertex component.
+            auto component = std::make_shared<wto_component_t>(wto_component_t(vertex));
+
+            // Insert the vertex into the current partition.
+            partition.push_back(component);
+
+            // Remember that we put the vertex into the caller's cycle.
+            _containing_cycle.emplace(vertex, containing_cycle);
         }
     }
+    vertex_data.head_dfn = head_dfn;
+}
 
-    // Finally, add the vertex at the start of the cycle
+void wto_t::continue_visit(const label_t& vertex, wto_partition_t& partition,
+                        std::weak_ptr<wto_cycle_t> containing_cycle) {
+    // Add the vertex at the start of the cycle
     // (end of the vector which stores the cycle in reverse order).
-    _components.push_back(std::make_shared<wto_component_t>(vertex));
+    auto cycle = containing_cycle.lock();
+
+    cycle->components().push_back(std::make_shared<wto_component_t>(vertex));
+
+    // Insert the component into the current partition.
+    auto component = std::make_shared<wto_component_t>(cycle);
+    partition.emplace_back(component);
+
+    // Remember that we put the vertex into the new cycle.
+    _containing_cycle.emplace(vertex, cycle);
+}
+
+wto_t::wto_t(const cfg_t& cfg) : _cfg(cfg) {
+    // Create a map for holding a "depth-first number (DFN)" for each vertex.
+    for (const label_t& label : cfg.labels()) {
+        _vertex_data.emplace(label, 0);
+    }
+
+    // Initialize the DFN counter.
+    _num = 0;
+
+    // Push the entry vertex on the stack to process.
+    visit_args_t args(visit_task_type_t::PushSuccessors, cfg.entry_label(), _components, {});
+    _visit_stack.push(args);
+
+    // Keep processing tasks until we're done.
+    while (!_visit_stack.empty()) {
+        visit_args_t& args2 = _visit_stack.top();
+        _visit_stack.pop();
+        switch (args2.type) {
+        case visit_task_type_t::PushSuccessors: push_successors(args2.vertex, args2.partition, args2.containing_cycle); break;
+        case visit_task_type_t::StartVisit: start_visit(args2.vertex, args2.partition, args2.containing_cycle); break;
+        case visit_task_type_t::ContinueVisit: continue_visit(args2.vertex, args2.partition, args2.containing_cycle); break;
+        default: break;
+        }
+    }
 }
+#endif

src/crab/wto.hpp

@@ -2,8 +2,8 @@
 // SPDX-License-Identifier: MIT
 #pragma once
 
-// This file implements Weak Topological Ordering as defined in
-// Bournacle, "Efficient chaotic iteration strategies with widenings", 1993
+// wto.hpp and wto.cpp implement Weak Topological Ordering as defined in
+// Bourdoncle, "Efficient chaotic iteration strategies with widenings", 1993
 // http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.3574
 //
 // Using the example from section 3.1 in the paper, the graph:
@@ -22,6 +22,12 @@
 // Each arrow points to a wto_component_t, which can be either a
 // single vertex such as 8, or a cycle such as (5 6).
 
+// Define this to use the old recursive algorithm instead of the new
+// iterative algorithm.  The recursive algorithm can result in a stack
+// overflow but we keep it for now to allow doing a performance
+// comparison.
+#undef RECURSIVE_WTO
+
 #include <stack>
 #include <vector>
 #include "crab/cfg.hpp"
@@ -33,17 +39,51 @@ using wto_partition_t = std::vector<std::shared_ptr<wto_component_t>>;
 
 #include "crab/wto_cycle.hpp"
 
+#ifndef RECURSIVE_WTO
+enum class visit_task_type_t {
+    PushSuccessors = 0,
+    StartVisit = 1, // Start of the Visit() function defined in Figure 4 of the paper.
+    ContinueVisit = 2,
+};
+
+struct visit_args_t {
+    visit_task_type_t type;
+    const label_t& vertex;
+    wto_partition_t& partition;
+    std::weak_ptr<wto_cycle_t> containing_cycle;
+
+    visit_args_t(visit_task_type_t t, const label_t& v, wto_partition_t& p, std::weak_ptr<wto_cycle_t> cc)
+        : type(t), vertex(v), partition(p), containing_cycle(cc) {};
+};
+
+struct wto_vertex_data_t {
+    // Bourdoncle's thesis (reference [4]) is all in French but expands
+    // DFN as "depth first number".
+    int dfn;
+    int head_dfn; // Head value returned from Visit() in the paper.
+    std::shared_ptr<wto_cycle_t> containing_cycle;
+};
+#endif
+
 class wto_t final {
     // Original control-flow graph.
     const crab::cfg_t& _cfg;
 
-    // The following members are named to match the names in the paper,
-    // which never explains their meaning.  Bourdoncle's thesis (reference [4])
-    // is all in French but expands DFN as "depth first number".
+    // The following members are named to match the names in the paper.
+#ifdef RECURSIVE_WTO
+    // Bourdoncle's thesis (reference [4]) is all in French but
+    // expands DFN as "depth first number".
     std::map<label_t, int> _dfn;
-    int _num;
+#else
+    std::map<label_t, wto_vertex_data_t> _vertex_data;
+#endif
+    int _num; // Highest DFN used so far.
     std::stack<label_t> _stack;
 
+#ifndef RECURSIVE_WTO
+    std::stack<visit_args_t> _visit_stack;
+#endif
+
     // Top level components, in reverse order.
     wto_partition_t _components;
 
@@ -55,8 +95,12 @@ class wto_t final {
     // looked at so we only create a wto_nesting_t for cases we actually need it.
     std::map<label_t, wto_nesting_t> _nesting;
 
-    public:
-
+#ifndef RECURSIVE_WTO
+    void push_successors(const label_t& vertex, wto_partition_t& partition, std::weak_ptr<wto_cycle_t> containing_cycle);
+    void start_visit(const label_t& vertex, wto_partition_t& partition,
+                            std::weak_ptr<wto_cycle_t> containing_cycle);
+    void continue_visit(const label_t& vertex, wto_partition_t& partition, std::weak_ptr<wto_cycle_t> containing_cycle);
+#else
     // Implementation of the Visit() function defined in Figure 4 of the paper.
     int visit(const label_t& vertex, wto_partition_t& partition, std::weak_ptr<wto_cycle_t> containing_cycle) {
         _stack.push(vertex);
@@ -87,9 +131,19 @@ class wto_t final {
                 }
 
                 // Create a new cycle component.
+                // Walk the control flow graph, adding nodes to this cycle.
+                // This is the Component() function described in figure 4 of the paper.
                 auto cycle = std::make_shared<wto_cycle_t>(containing_cycle);
                 auto component = std::make_shared<wto_component_t>(cycle);
-                cycle->initialize(*this, vertex, cycle);
+                for (const label_t& succ : _cfg.next_nodes(vertex)) {
+                    if (dfn(succ) == 0) {
+                        visit(succ, cycle->components(), cycle);
+                    }
+                }
+
+                // Finally, add the vertex at the start of the cycle
+                // (end of the vector which stores the cycle in reverse order).
+                cycle->components().push_back(std::make_shared<wto_component_t>(vertex));
 
                 // Insert the component into the current partition.
                 partition.emplace_back(component);
@@ -109,20 +163,30 @@ class wto_t final {
         }
         return head;
     }
+#endif
 
+    public:
     [[nodiscard]] const crab::cfg_t& cfg() const { return _cfg; }
+#ifdef RECURSIVE_WTO
     [[nodiscard]] int dfn(const label_t& vertex) const { return _dfn.at(vertex); }
+#else
+    [[nodiscard]] int dfn(const label_t& vertex) const { return _vertex_data.at(vertex).dfn; }
+#endif
 
     // Construct a Weak Topological Ordering from a control-flow graph using
     // the algorithm of figure 4 in the paper, where this constructor matches
     // what is shown there as the Partition function.
+#ifdef RECURSIVE_WTO
     wto_t(const cfg_t& cfg) : _cfg(cfg) {
         for (const label_t& label : cfg.labels()) {
             _dfn.emplace(label, 0);
         }
         _num = 0;
         visit(cfg.entry_label(), _components, {});
     }
+#else
+    wto_t(const cfg_t& cfg);
+#endif
 
     [[nodiscard]] wto_partition_t::reverse_iterator begin() { return _components.rbegin(); }
     [[nodiscard]] wto_partition_t::reverse_iterator end() { return _components.rend(); }

src/crab/wto_cycle.hpp

@@ -5,7 +5,7 @@
 #include <ostream>
 #include "wto.hpp"
 
-// Bournacle, "Efficient chaotic iteration strategies with widenings", 1993
+// Bourdoncle, "Efficient chaotic iteration strategies with widenings", 1993
 // section 3 uses the term "nested component" to refer to what wto_cycle_t implements.
 class wto_cycle_t final {
     // The cycle containing this cycle, or null if there is no parent cycle.
@@ -17,10 +17,6 @@ class wto_cycle_t final {
   public:
     wto_cycle_t(std::weak_ptr<wto_cycle_t>& containing_cycle) : _containing_cycle(containing_cycle) {}
 
-    // Finish initializing this cycle.  This must be done right after construction, where
-    // 'self' is a shared pointer pointing to this instance.
-    void initialize(class wto_t& wto, const label_t& vertex, std::shared_ptr<wto_cycle_t>& self);
-
     // Get a vertex of an entry point of the cycle.
     [[nodiscard]] const label_t& head() const {
         // Any cycle must start with a vertex, not another cycle,
@@ -33,6 +29,7 @@ class wto_cycle_t final {
     [[nodiscard]] wto_partition_t::reverse_iterator end() { return _components.rend(); }
 
     [[nodiscard]] std::weak_ptr<wto_cycle_t> containing_cycle() const { return _containing_cycle; }
+    [[nodiscard]] wto_partition_t& components() { return _components; }
 };
 
 inline std::ostream& operator<<(std::ostream& o, wto_cycle_t& cycle) {

src/crab/wto_nesting.hpp

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: MIT
 #pragma once
 
-// Bournacle, "Efficient chaotic iteration strategies with widenings", 1993
+// Bourdoncle, "Efficient chaotic iteration strategies with widenings", 1993
 // uses the notation w(c) to refer to the set of heads of the nested components
 // containing a vertex c.  This class holds such a set of heads.  The table
 // mapping c to w(c) is stored outside the class, in wto_t._nesting.