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 
30 
33 class depth_iteratort;
40 
43 {
44  typedef exprt::operandst::const_iterator operands_iteratort;
46  {
47  }
48  std::reference_wrapper<const exprt> expr;
49  std::size_t op_idx;
50 };
51 
52 inline bool operator==(
53  const depth_iterator_expr_statet &left,
54  const depth_iterator_expr_statet &right)
55 {
56  return left.op_idx == right.op_idx && left.expr.get() == right.expr.get();
57 }
58 
65 template<typename depth_iterator_t>
67 {
68 public:
69  typedef void difference_type; // NOLINT Required by STL
70  typedef exprt value_type; // NOLINT
71  typedef const exprt *pointer; // NOLINT
72  typedef const exprt &reference; // NOLINT
73  typedef std::forward_iterator_tag iterator_category; // NOLINT
74 
75  template <typename other_depth_iterator_t>
76  friend class depth_iterator_baset;
77 
78  template <typename other_depth_iterator_t>
79  bool operator==(
81  {
82  return m_stack==other.m_stack;
83  }
84 
85  template <typename other_depth_iterator_t>
86  bool operator!=(
88  {
89  return !(*this == other);
90  }
91 
94  depth_iterator_t &operator++()
95  {
96  PRECONDITION(!m_stack.empty());
97  while(true)
98  {
99  if(m_stack.back().op_idx == m_stack.back().expr.get().operands().size())
100  {
101  m_stack.pop_back();
102  if(m_stack.empty())
103  break;
104  }
105  // Check eg. if we haven't seen this node before
106  else if(this->downcast().push_expr(
107  m_stack.back().expr.get().operands()[m_stack.back().op_idx]))
108  {
109  break;
110  }
111  ++m_stack.back().op_idx;
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().op_idx;
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:
153 
155  explicit depth_iterator_baset(const exprt &root)
156  { this->push_expr(root); }
157 
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  (void)expr->write();
188  state.expr = *expr;
189  // Get the expr for the next level down to use in the next iteration
190  if(!(state == m_stack.back()))
191  expr = &expr->operands()[state.op_idx];
192  }
193  return *expr;
194  }
195 
201  bool push_expr(const exprt &expr)
202  {
203  m_stack.emplace_back(expr);
204  return true;
205  }
206 
207 private:
208  std::deque<depth_iterator_expr_statet> m_stack;
209 
210  depth_iterator_t &downcast()
211  { return static_cast<depth_iterator_t &>(*this); }
212 };
213 
215  public depth_iterator_baset<const_depth_iteratort>
216 {
217 public:
219  explicit const_depth_iteratort(const exprt &expr):
220  depth_iterator_baset(expr) { }
223 };
224 
225 class depth_iteratort final:
226  public depth_iterator_baset<depth_iteratort>
227 {
228 private:
231  std::function<exprt &()> mutate_root;
232 
233 public:
235  depth_iteratort()=default;
236 
241  {
242  }
243 
251  explicit depth_iteratort(
252  const exprt &expr,
253  std::function<exprt &()> mutate_root)
254  : depth_iterator_baset(expr), mutate_root(std::move(mutate_root))
255  {
256  // If you don't provide a mutate_root function then you must pass a
257  // non-const exprt (use the other constructor).
258  PRECONDITION(this->mutate_root);
259  }
260 
268  {
269  if(mutate_root)
270  {
271  exprt &new_root = mutate_root();
272  INVARIANT(
273  &new_root.read() == &get_root().read(),
274  "mutate_root must return the same root node that depth_iteratort was "
275  "constructed with");
276  mutate_root = nullptr;
277  }
279  }
280 };
281 
283  public depth_iterator_baset<const_unique_depth_iteratort>
284 {
286 public:
288  explicit const_unique_depth_iteratort(const exprt &expr):
289  depth_iterator_baset(expr),
290  m_traversed({ expr }) { }
293 private:
295  bool push_expr(const exprt &expr) // "override" - hide base class method
296  {
297  const bool inserted=this->m_traversed.insert(expr).second;
298  if(inserted)
300  return inserted;
301  }
302  std::set<exprt> m_traversed;
303 };
304 
305 #endif
depth_iterator_baset::operator->
const exprt * operator->() const
Dereference operator (member access) Dereferencing end() iterator is undefined behaviour.
Definition: expr_iterator.h:147
depth_iterator_expr_statet
Helper class for depth_iterator_baset.
Definition: expr_iterator.h:43
const_unique_depth_iteratort
Definition: expr_iterator.h:284
depth_iterator_baset::operator++
depth_iterator_t & operator++()
Preincrement operator Do not call on the end() iterator.
Definition: expr_iterator.h:94
const_unique_depth_iteratort::push_expr
bool push_expr(const exprt &expr)
Push expression onto the stack and add to the set of traversed exprts.
Definition: expr_iterator.h:295
depth_iterator_baset::get_root
const exprt & get_root()
Definition: expr_iterator.h:169
depth_iterator_baset::depth_iterator_baset
depth_iterator_baset()=default
Create end iterator.
depth_iterator_expr_statet::expr
std::reference_wrapper< const exprt > expr
Definition: expr_iterator.h:48
depth_iterator_baset::~depth_iterator_baset
~depth_iterator_baset()=default
Destructor Protected to discourage upcasting.
depth_iteratort
Definition: expr_iterator.h:227
depth_iterator_baset::operator++
depth_iterator_t operator++(int)
Post-increment operator Expensive copy.
Definition: expr_iterator.h:130
exprt
Base class for all expressions.
Definition: expr.h:53
depth_iterator_baset::next_sibling_or_parent
depth_iterator_t & next_sibling_or_parent()
Definition: expr_iterator.h:116
const_depth_iteratort::const_depth_iteratort
const_depth_iteratort()=default
Create an end iterator.
sharing_treet::write
dt & write()
Definition: irep.h:275
depth_iterator_baset::depth_iterator_baset
depth_iterator_baset(const depth_iterator_baset &)=default
operator==
bool operator==(const depth_iterator_expr_statet &left, const depth_iterator_expr_statet &right)
Definition: expr_iterator.h:52
depth_iteratort::depth_iteratort
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...
Definition: expr_iterator.h:251
expr.h
depth_iterator_baset::reference
const exprt & reference
Definition: expr_iterator.h:72
const_unique_depth_iteratort::m_traversed
std::set< exprt > m_traversed
Definition: expr_iterator.h:302
depth_iterator_baset::operator*
const exprt & operator*() const
Dereference operator Dereferencing end() iterator is undefined behaviour.
Definition: expr_iterator.h:139
depth_iteratort::mutate_root
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...
Definition: expr_iterator.h:231
depth_iterator_baset::depth_iterator_baset
depth_iterator_baset(depth_iterator_baset &&other)
Definition: expr_iterator.h:163
const_depth_iteratort
Definition: expr_iterator.h:216
const_unique_depth_iteratort::const_unique_depth_iteratort
const_unique_depth_iteratort()=default
Create an end iterator.
depth_iterator_baset::operator=
depth_iterator_baset & operator=(const depth_iterator_baset &)=default
const_unique_depth_iteratort::const_unique_depth_iteratort
const_unique_depth_iteratort(const exprt &expr)
Create iterator starting at the supplied node (root)
Definition: expr_iterator.h:288
const_depth_iteratort::const_depth_iteratort
const_depth_iteratort(const exprt &expr)
Create iterator starting at the supplied node (root)
Definition: expr_iterator.h:219
depth_iterator_baset::pointer
const exprt * pointer
Definition: expr_iterator.h:71
depth_iterator_expr_statet::depth_iterator_expr_statet
depth_iterator_expr_statet(const exprt &expr)
Definition: expr_iterator.h:45
const_unique_depth_iteratort::depth_iterator_baset
friend depth_iterator_baset
Definition: expr_iterator.h:285
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
sharing_treet::read
const dt & read() const
Definition: irep.h:270
depth_iterator_baset::push_expr
bool push_expr(const exprt &expr)
Pushes expression onto the stack If overridden, this function should be called from the inheriting cl...
Definition: expr_iterator.h:201
depth_iterator_expr_statet::op_idx
std::size_t op_idx
Definition: expr_iterator.h:49
depth_iterator_baset
Depth first search iterator base - iterates over supplied expression and all its operands recursively...
Definition: expr_iterator.h:67
depth_iterator_baset::downcast
depth_iterator_t & downcast()
Definition: expr_iterator.h:210
depth_iteratort::mutate
exprt & mutate()
Obtain non-const reference to the exprt instance currently pointed to by the iterator.
Definition: expr_iterator.h:267
depth_iterator_baset::depth_iterator_baset
depth_iterator_baset(const exprt &root)
Create begin iterator, starting at the supplied node.
Definition: expr_iterator.h:155
depth_iterator_baset::value_type
exprt value_type
Definition: expr_iterator.h:70
depth_iterator_baset::operator==
bool operator==(const depth_iterator_baset< other_depth_iterator_t > &other) const
Definition: expr_iterator.h:79
depth_iteratort::depth_iteratort
depth_iteratort()=default
Create an end iterator.
depth_iterator_baset::operator=
depth_iterator_baset & operator=(depth_iterator_baset &&other)
Definition: expr_iterator.h:166
depth_iterator_baset::mutate
exprt & mutate()
Obtain non-const exprt reference.
Definition: expr_iterator.h:179
depth_iterator_baset::m_stack
std::deque< depth_iterator_expr_statet > m_stack
Definition: expr_iterator.h:208
depth_iteratort::depth_iteratort
depth_iteratort(exprt &expr)
Create iterator starting at the supplied node (root) All mutations of the child nodes will be reflect...
Definition: expr_iterator.h:240
invariant.h
depth_iterator_baset::operator!=
bool operator!=(const depth_iterator_baset< other_depth_iterator_t > &other) const
Definition: expr_iterator.h:86
exprt::operands
operandst & operands()
Definition: expr.h:95
depth_iterator_baset::difference_type
void difference_type
Definition: expr_iterator.h:69
depth_iterator_expr_statet::operands_iteratort
exprt::operandst::const_iterator operands_iteratort
Definition: expr_iterator.h:44
validation_modet::INVARIANT
@ INVARIANT
depth_iterator_baset::iterator_category
std::forward_iterator_tag iterator_category
Definition: expr_iterator.h:73