From aa944819c2f147b4ed92441678dc2c1e360066b3 Mon Sep 17 00:00:00 2001 From: Dave Thaler Date: Fri, 8 Oct 2021 13:31:48 -0700 Subject: [PATCH] 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 #195 Signed-off-by: Dave Thaler --- CMakeLists.txt | 1 + src/crab/cfg.hpp | 10 +++ src/crab/wto.cpp | 139 ++++++++++++++++++++++++++++++++++++--- src/crab/wto.hpp | 82 ++++++++++++++++++++--- src/crab/wto_cycle.hpp | 7 +- src/crab/wto_nesting.hpp | 2 +- src/test/test_wto.cpp | 92 ++++++++++++++++++++++++++ 7 files changed, 308 insertions(+), 25 deletions(-) create mode 100644 src/test/test_wto.cpp diff --git a/CMakeLists.txt b/CMakeLists.txt index 18c09cee9..2c949a169 100644 --- a/CMakeLists.txt +++ b/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" ) diff --git a/src/crab/cfg.hpp b/src/crab/cfg.hpp index ecb5eb462..c4ebe7404 100644 --- a/src/crab/cfg.hpp +++ b/src/crab/cfg.hpp @@ -45,6 +45,7 @@ class basic_block_t final { using label_vec_t = std::set; using stmt_list_t = std::vector; 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(std::distance(begin(), end())); } [[nodiscard]] std::pair next_blocks() const { return std::make_pair(m_next.begin(), m_next.end()); } + [[nodiscard]] std::pair next_blocks_reversed() const { + return std::make_pair(m_next.rbegin(), m_next.rend()); + } + [[nodiscard]] std::pair 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; + using neighbour_const_reverse_range = boost::iterator_range; private: using basic_block_map_t = std::map; @@ -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()); diff --git a/src/crab/wto.cpp b/src/crab/wto.cpp index 7f52b7716..a0fb24ad3 100644 --- a/src/crab/wto.cpp +++ b/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& 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 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 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(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(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 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(vertex)); + auto cycle = containing_cycle.lock(); + + cycle->components().push_back(std::make_shared(vertex)); + + // Insert the component into the current partition. + auto component = std::make_shared(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 diff --git a/src/crab/wto.hpp b/src/crab/wto.hpp index 26d99a6d6..a324f9c2a 100644 --- a/src/crab/wto.hpp +++ b/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 #include #include "crab/cfg.hpp" @@ -33,17 +39,51 @@ using wto_partition_t = std::vector>; #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 containing_cycle; + + visit_args_t(visit_task_type_t t, const label_t& v, wto_partition_t& p, std::weak_ptr 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 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 _dfn; - int _num; +#else + std::map _vertex_data; +#endif + int _num; // Highest DFN used so far. std::stack _stack; +#ifndef RECURSIVE_WTO + std::stack _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 _nesting; - public: - +#ifndef RECURSIVE_WTO + void push_successors(const label_t& vertex, wto_partition_t& partition, std::weak_ptr containing_cycle); + void start_visit(const label_t& vertex, wto_partition_t& partition, + std::weak_ptr containing_cycle); + void continue_visit(const label_t& vertex, wto_partition_t& partition, std::weak_ptr 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 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(containing_cycle); auto component = std::make_shared(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(vertex)); // Insert the component into the current partition. partition.emplace_back(component); @@ -109,13 +163,20 @@ 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); @@ -123,6 +184,9 @@ class wto_t final { _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(); } diff --git a/src/crab/wto_cycle.hpp b/src/crab/wto_cycle.hpp index a6f92e2d9..9071d4e60 100644 --- a/src/crab/wto_cycle.hpp +++ b/src/crab/wto_cycle.hpp @@ -5,7 +5,7 @@ #include #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& 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& 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 containing_cycle() const { return _containing_cycle; } + [[nodiscard]] wto_partition_t& components() { return _components; } }; inline std::ostream& operator<<(std::ostream& o, wto_cycle_t& cycle) { diff --git a/src/crab/wto_nesting.hpp b/src/crab/wto_nesting.hpp index e19dae498..e614be1cb 100644 --- a/src/crab/wto_nesting.hpp +++ b/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. diff --git a/src/test/test_wto.cpp b/src/test/test_wto.cpp new file mode 100644 index 000000000..e0e9548be --- /dev/null +++ b/src/test/test_wto.cpp @@ -0,0 +1,92 @@ +// Copyright (c) Prevail Verifier contributors. +// SPDX-License-Identifier: MIT +#include "catch.hpp" +#include "crab/cfg.hpp" +#include "crab/wto.hpp" + +TEST_CASE("wto figure 1", "[wto]") { + cfg_t cfg; + + // Construct the example graph in figure 1 of Bournacle, + // "Efficient chaotic iteration strategies with widenings", 1993. + + // Add nodes. + for (int i = 1; i <= 8; i++) { + cfg.insert(label_t(i)); + } + + // Add edges. + cfg.get_node(label_t::entry) >> cfg.get_node(label_t(1)); + cfg.get_node(label_t(1)) >> cfg.get_node(label_t(2)); + cfg.get_node(label_t(2)) >> cfg.get_node(label_t(3)); + cfg.get_node(label_t(3)) >> cfg.get_node(label_t(4)); + cfg.get_node(label_t(4)) >> cfg.get_node(label_t(5)); + cfg.get_node(label_t(4)) >> cfg.get_node(label_t(7)); + cfg.get_node(label_t(5)) >> cfg.get_node(label_t(6)); + cfg.get_node(label_t(6)) >> cfg.get_node(label_t(5)); + cfg.get_node(label_t(6)) >> cfg.get_node(label_t(7)); + cfg.get_node(label_t(7)) >> cfg.get_node(label_t(3)); + cfg.get_node(label_t(7)) >> cfg.get_node(label_t(8)); + cfg.get_node(label_t(8)) >> cfg.get_node(label_t::exit); + + wto_t wto(cfg); + + std::ostringstream os; + os << wto; + REQUIRE(os.str() == "entry 1 2 ( 3 4 ( 5 6 ) 7 ) 8 exit \n"); +} + +TEST_CASE("wto figure 2a", "[wto]") { + cfg_t cfg; + + // Construct the example graph in figure 2a of Bournacle, + // "Efficient chaotic iteration strategies with widenings", 1993. + + // Add nodes. + for (int i = 1; i <= 5; i++) { + cfg.insert(label_t(i)); + } + + // Add edges. + cfg.get_node(label_t::entry) >> cfg.get_node(label_t(1)); + cfg.get_node(label_t(1)) >> cfg.get_node(label_t(2)); + cfg.get_node(label_t(1)) >> cfg.get_node(label_t(4)); + cfg.get_node(label_t(2)) >> cfg.get_node(label_t(3)); + cfg.get_node(label_t(3)) >> cfg.get_node(label_t::exit); + cfg.get_node(label_t(4)) >> cfg.get_node(label_t(3)); + cfg.get_node(label_t(4)) >> cfg.get_node(label_t(5)); + cfg.get_node(label_t(5)) >> cfg.get_node(label_t(4)); + + wto_t wto(cfg); + + std::ostringstream os; + os << wto; + REQUIRE(os.str() == "entry 1 ( 4 5 ) 2 3 exit \n"); +} + +TEST_CASE("wto figure 2b", "[wto]") { + cfg_t cfg; + + // Construct the example graph in figure 2b of Bournacle, + // "Efficient chaotic iteration strategies with widenings", 1993. + + // Add nodes. + for (int i = 1; i <= 4; i++) { + cfg.insert(label_t(i)); + } + + // Add edges. + cfg.get_node(label_t::entry) >> cfg.get_node(label_t(1)); + cfg.get_node(label_t(1)) >> cfg.get_node(label_t(2)); + cfg.get_node(label_t(1)) >> cfg.get_node(label_t(4)); + cfg.get_node(label_t(2)) >> cfg.get_node(label_t(3)); + cfg.get_node(label_t(3)) >> cfg.get_node(label_t(1)); + cfg.get_node(label_t(3)) >> cfg.get_node(label_t::exit); + cfg.get_node(label_t(4)) >> cfg.get_node(label_t(3)); + + wto_t wto(cfg); + + std::ostringstream os; + os << wto; + REQUIRE(os.str() == "entry ( 1 4 2 3 ) exit \n"); +} \ No newline at end of file