cprover
expr_iterator.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: exprt iterator module
4 
5  Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_UTIL_EXPR_ITERATOR_H
10 #define CPROVER_UTIL_EXPR_ITERATOR_H
11 
12 #include <deque>
13 #include <iterator>
14 #include <functional>
15 #include <set>
16 #include <algorithm>
17 #include "expr.h"
18 #include "invariant.h"
19 
20 // Forward declarations - table of contents
21 
29 
32 class depth_iteratort;
39 
42 {
43  typedef exprt::operandst::const_iterator operands_iteratort;
45  const exprt &expr,
48  expr(expr), it(it), end(end) { }
49  std::reference_wrapper<const exprt> expr;
52 };
53 
54 inline bool operator==(
55  const depth_iterator_expr_statet &left,
56  const depth_iterator_expr_statet &right)
57 {
58  return distance(left.it, left.end) == distance(right.it, right.end) &&
59  left.expr.get() == right.expr.get();
60 }
61 
68 template<typename depth_iterator_t>
70 {
71 public:
72  typedef void difference_type; // NOLINT Required by STL
73  typedef exprt value_type; // NOLINT
74  typedef const exprt *pointer; // NOLINT
75  typedef const exprt &reference; // NOLINT
76  typedef std::forward_iterator_tag iterator_category; // NOLINT
77 
78  template <typename other_depth_iterator_t>
79  friend class depth_iterator_baset;
80 
81  template <typename other_depth_iterator_t>
82  bool operator==(
84  {
85  return m_stack==other.m_stack;
86  }
87 
88  template <typename other_depth_iterator_t>
89  bool operator!=(
91  {
92  return !(*this == other);
93  }
94 
97  depth_iterator_t &operator++()
98  {
99  PRECONDITION(!m_stack.empty());
100  while(true)
101  {
102  if(m_stack.back().it==m_stack.back().end)
103  {
104  m_stack.pop_back();
105  if(m_stack.empty())
106  break;
107  }
108  // Check eg. if we haven't seen this node before
109  else if(this->downcast().push_expr(*m_stack.back().it))
110  break;
111  m_stack.back().it++;
112  }
113  return this->downcast();
114  }
115 
116  depth_iterator_t &next_sibling_or_parent()
117  {
118  PRECONDITION(!m_stack.empty());
119  m_stack.pop_back();
120  if(!m_stack.empty())
121  {
122  ++m_stack.back().it;
123  return ++(*this);
124  }
125  return this->downcast();
126  }
127 
130  depth_iterator_t operator++(int)
131  {
132  depth_iterator_t tmp(this->downcast());
133  this->operator++();
134  return tmp;
135  }
136 
139  const exprt &operator*() const
140  {
141  PRECONDITION(!m_stack.empty());
142  return m_stack.back().expr.get();
143  }
144 
147  const exprt *operator->() const
148  { return &**this; }
149 
150 protected:
152  depth_iterator_baset()=default;
153 
155  explicit depth_iterator_baset(const exprt &root)
156  { this->push_expr(root); }
157 
160  ~depth_iterator_baset()=default;
161 
164  { m_stack=std::move(other.m_stack); }
167  { m_stack=std::move(other.m_stack); }
168 
169  const exprt &get_root()
170  {
171  return m_stack.front().expr.get();
172  }
173 
180  {
181  PRECONDITION(!m_stack.empty());
182  // Cast the root expr to non-const
183  exprt *expr = &const_cast<exprt &>(get_root());
184  for(auto &state : m_stack)
185  {
186  // This deliberately breaks sharing as expr is now non-const
187  auto &operands = expr->operands();
188  // Get iterators into the operands of the new expr corresponding to the
189  // ones into the operands of the old expr
190  const auto i=operands.size()-(state.end-state.it);
191  const auto it=operands.begin()+i;
192  state.expr = *expr;
193  state.it=it;
194  state.end=operands.end();
195  // Get the expr for the next level down to use in the next iteration
196  if(!(state==m_stack.back()))
197  {
198  expr = &*it;
199  }
200  }
201  return *expr;
202  }
203 
210  bool push_expr(const exprt &expr)
211  {
212  m_stack.emplace_back(expr, expr.operands().begin(), expr.operands().end());
213  return true;
214  }
215 
216 private:
217  std::deque<depth_iterator_expr_statet> m_stack;
218 
219  depth_iterator_t &downcast()
220  { return static_cast<depth_iterator_t &>(*this); }
221 };
222 
224  public depth_iterator_baset<const_depth_iteratort>
225 {
226 public:
228  explicit const_depth_iteratort(const exprt &expr):
229  depth_iterator_baset(expr) { }
231  const_depth_iteratort()=default;
232 };
233 
234 class depth_iteratort final:
235  public depth_iterator_baset<depth_iteratort>
236 {
237 private:
240  std::function<exprt &()> mutate_root;
241 
242 public:
244  depth_iteratort()=default;
245 
250  {
251  }
252 
260  explicit depth_iteratort(
261  const exprt &expr,
262  std::function<exprt &()> mutate_root)
264  {
265  // If you don't provide a mutate_root function then you must pass a
266  // non-const exprt (use the other constructor).
267  PRECONDITION(this->mutate_root);
268  }
269 
277  {
278  if(mutate_root)
279  {
280  exprt &new_root = mutate_root();
281  INVARIANT(
282  &new_root.read() == &get_root().read(),
283  "mutate_root must return the same root node that depth_iteratort was "
284  "constructed with");
285  mutate_root = nullptr;
286  }
288  }
289 };
290 
292  public depth_iterator_baset<const_unique_depth_iteratort>
293 {
295 public:
297  explicit const_unique_depth_iteratort(const exprt &expr):
298  depth_iterator_baset(expr),
299  m_traversed({ expr }) { }
302 private:
304  bool push_expr(const exprt &expr) // "override" - hide base class method
305  {
306  const bool inserted=this->m_traversed.insert(expr).second;
307  if(inserted)
309  return inserted;
310  }
311  std::set<exprt> m_traversed;
312 };
313 
314 #endif
const exprt & reference
Definition: expr_iterator.h:75
const_unique_depth_iteratort(const exprt &expr)
Create iterator starting at the supplied node (root)
exprt & mutate()
Obtain non-const exprt reference.
depth_iterator_t & downcast()
const exprt * pointer
Definition: expr_iterator.h:74
bool operator==(const depth_iterator_baset< other_depth_iterator_t > &other) const
Definition: expr_iterator.h:82
std::deque< depth_iterator_expr_statet > m_stack
depth_iteratort(exprt &expr)
Create iterator starting at the supplied node (root) All mutations of the child nodes will be reflect...
std::set< exprt > m_traversed
bool push_expr(const exprt &expr)
Pushes expression onto the stack If overridden, this function should be called from the inheriting cl...
std::reference_wrapper< const exprt > expr
Definition: expr_iterator.h:49
depth_iteratort()=default
Create an end iterator.
exprt & mutate()
Obtain non-const reference to the exprt instance currently pointed to by the iterator.
depth_iterator_baset(const exprt &root)
Create begin iterator, starting at the supplied node.
STL namespace.
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
depth_iterator_baset & operator=(depth_iterator_baset &&other)
const dt & read() const
Definition: irep.h:334
exprt::operandst::const_iterator operands_iteratort
Definition: expr_iterator.h:43
const exprt * operator->() const
Dereference operator (member access) Dereferencing end() iterator is undefined behaviour.
bool operator!=(const depth_iterator_baset< other_depth_iterator_t > &other) const
Definition: expr_iterator.h:89
depth_iterator_expr_statet(const exprt &expr, operands_iteratort it, operands_iteratort end)
Definition: expr_iterator.h:44
#define PRECONDITION(CONDITION)
Definition: invariant.h:230
std::forward_iterator_tag iterator_category
Definition: expr_iterator.h:76
const_depth_iteratort()=default
Create an end iterator.
depth_iterator_baset()=default
Create end iterator.
depth_iterator_t operator++(int)
Post-increment operator Expensive copy.
const_unique_depth_iteratort()=default
Create an end iterator.
depth_iterator_t & next_sibling_or_parent()
bool operator==(const depth_iterator_expr_statet &left, const depth_iterator_expr_statet &right)
Definition: expr_iterator.h:54
Depth first search iterator base - iterates over supplied expression and all its operands recursively...
Definition: expr_iterator.h:69
depth_iterator_t & operator++()
Preincrement operator Do not call on the end() iterator.
Definition: expr_iterator.h:97
const exprt & get_root()
bool push_expr(const exprt &expr)
Push expression onto the stack and add to the set of traversed exprts.
~depth_iterator_baset()=default
Destructor Protected to discourage upcasting.
Base class for all expressions.
Definition: expr.h:42
depth_iterator_baset & operator=(const depth_iterator_baset &)=default
depth_iteratort(const exprt &expr, std::function< exprt &()> mutate_root)
Create iterator starting at the supplied node (root) If mutations of the child nodes are required the...
const exprt & operator*() const
Dereference operator Dereferencing end() iterator is undefined behaviour.
std::function< exprt &()> mutate_root
If this is non-empty then the root is currently const and this function must be called before any mut...
Helper class for depth_iterator_baset.
Definition: expr_iterator.h:41
depth_iterator_baset(depth_iterator_baset &&other)
operands_iteratort end
Definition: expr_iterator.h:51
operandst & operands()
Definition: expr.h:66
operands_iteratort it
Definition: expr_iterator.h:50
const_depth_iteratort(const exprt &expr)
Create iterator starting at the supplied node (root)