Line data    Source code

       1             : // Author(s): Jan Friso Groote
       2             : // Copyright: see the accompanying file COPYING or copy at
       3             : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
       4             : //
       5             : // Distributed under the Boost Software License, Version 1.0.
       6             : // (See accompanying file LICENSE_1_0.txt or copy at
       7             : // http://www.boost.org/LICENSE_1_0.txt)
       8             : //
       9             : /// \file rewrite_stack.h
      10             : /// \brief This file contains a rewrite stack that can operate
      11             : ///        alongside the normal stack. As it is an atermpp container
      12             : ///        protection of aterm derived data types is guaranteed, 
      13             : ///        without explicitly putting each entry in a protection set.
      14             : ///        This makes the use of this stack much cheaper than using
      15             : ///        the processor stack. An additional advantage is that
      16             : ///        rewriting does not run out of stack space that quickly 
      17             : ///        anymore. 
      18             : 
      19             : #ifndef MCRL2_DATA_DETAIL_REWRITE_STACK_H
      20             : #define MCRL2_DATA_DETAIL_REWRITE_STACK_H
      21             : 
      22             : #include <algorithm>
      23             : #include "mcrl2/atermpp/standard_containers/vector.h"
      24             : #include "mcrl2/data/data_expression.h"
      25             : 
      26             : namespace mcrl2
      27             : {
      28             : namespace data
      29             : {
      30             : namespace detail
      31             : {
      32             : 
      33             : /// This is an exception that is thrown when the rewrite 
      34             : /// stack must be resized. As the rewrite stack is a vector
      35             : /// this invalidates all references and iterators in it,
      36             : /// and that means that when resizing is necessary, the 
      37             : /// current term must be resized. When this exception is
      38             : /// thrown, the current substitution must also be restored. 
      39             : ///
      40             : /// Note that the vector leaves terms on the stack as protected
      41             : /// members when the stack is decreased. This is done intentionally
      42             : /// because the stack is intensively used by the rewriters, and
      43             : /// destroying and creating elements in the vector is a relatively
      44             : /// expensive operation. 
      45             : 
      46             : struct recalculate_term_as_stack_is_too_small {};
      47             : 
      48             : 
      49             : class rewrite_stack : protected atermpp::vector<data_expression>
      50             : {
      51             :   protected:
      52             :     std::size_t m_stack_size;
      53             :     std::size_t m_reserved_stack_size; // This is equal to the size() of the underlying stack.
      54             :                                        // Access of "size()" expensive as it is surrounded by a mutex. 
      55             : 
      56             : 
      57             :   public:
      58             : 
      59             :     /// \brief Constructor
      60        1806 :     rewrite_stack() 
      61        1806 :       : m_stack_size(0)
      62             :     {
      63        1806 :       reserve_more_space();
      64        1806 :     }
      65             : 
      66        1807 :     void reserve_more_space() 
      67             :     {
      68        1807 :       resize(std::max(2*size(),static_cast<std::size_t>(128)));
      69        1807 :       m_reserved_stack_size=size();
      70        1807 :       m_stack_size=0;
      71        1807 :     }
      72             : 
      73     1128094 :     void increase(std::size_t distance)
      74             :     { 
      75     1128094 :       if (m_stack_size+distance>=m_reserved_stack_size)
      76             :       { 
      77           1 :         throw recalculate_term_as_stack_is_too_small();
      78             :       }
      79     1128093 :       m_stack_size=m_stack_size+distance;
      80     1128093 :     }
      81             : 
      82     1128056 :     void decrease(std::size_t distance)
      83             :     { 
      84     1128056 :       assert(distance<=m_stack_size);
      85     1128056 :       m_stack_size=m_stack_size-distance;
      86     1128056 :     }
      87             : 
      88       14897 :     data_expression& new_stack_position()
      89             :     { 
      90       14897 :       if (m_stack_size+1>=m_reserved_stack_size)
      91             :       { 
      92           0 :         throw recalculate_term_as_stack_is_too_small();
      93             :       }
      94       14897 :       data_expression& result=operator[](m_stack_size);
      95       14897 :       m_stack_size++;
      96       14897 :       return result;
      97             :     }
      98             : 
      99      744824 :     data_expression& top()
     100             :     { 
     101      744824 :       assert(m_stack_size>0);
     102      744824 :       return operator[](m_stack_size-1);
     103             :     }
     104             : 
     105          41 :     void set_element(std::size_t pos, std::size_t frame_size, const data_expression& d)
     106             :     {
     107          41 :       assert(m_stack_size+pos>=frame_size && pos<frame_size);
     108          41 :       operator[](m_stack_size-frame_size+pos)=d;
     109          41 :     }
     110             : 
     111     6733077 :     data_expression& element(std::size_t pos, std::size_t frame_size)
     112             :     {
     113     6733077 :       assert(m_stack_size+pos>=frame_size && pos<frame_size);
     114     6733077 :       return operator[](m_stack_size-frame_size+pos);
     115             :     }
     116             : 
     117     1549004 :     atermpp::vector<data_expression>::const_iterator stack_iterator(std::size_t pos, std::size_t frame_size) const
     118             :     {
     119     1549004 :       assert(m_stack_size+pos>=frame_size && pos<frame_size);
     120     1549004 :       return begin()+m_stack_size-frame_size+pos;
     121             :     }
     122             : 
     123      563714 :     std::size_t stack_size() const
     124             :     {
     125      563714 :       return m_stack_size;
     126             :     }
     127             : 
     128       26172 :     void reset_stack_size(std::size_t n)
     129             :     {
     130       26172 :       m_stack_size=n;
     131       26172 :     }
     132             : };
     133             : 
     134             : } // namespace detail
     135             : } // namespace data
     136             : } // namespace mcrl2
     137             : 
     138             : #endif // MCRL2_DATA_DETAIL_REWRITE_STACK_H
     139             :