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  const exprt &expr,
49  expr(expr), it(it), end(end) { }
50  std::reference_wrapper<const exprt> expr;
53 };
54 
55 inline bool operator==(
56  const depth_iterator_expr_statet &left,
57  const depth_iterator_expr_statet &right)
58 {
59  return distance(left.it, left.end) == distance(right.it, right.end) &&
60  left.expr.get() == right.expr.get();
61 }
62 
69 template<typename depth_iterator_t>
71 {
72 public:
73  typedef void difference_type; // NOLINT Required by STL
74  typedef exprt value_type; // NOLINT
75  typedef const exprt *pointer; // NOLINT
76  typedef const exprt &reference; // NOLINT
77  typedef std::forward_iterator_tag iterator_category; // NOLINT
78 
79  template <typename other_depth_iterator_t>
80  friend class depth_iterator_baset;
81 
82  template <typename other_depth_iterator_t>
83  bool operator==(
85  {
86  return m_stack==other.m_stack;
87  }
88 
89  template <typename other_depth_iterator_t>
90  bool operator!=(
92  {
93  return !(*this == other);
94  }
95 
98  depth_iterator_t &operator++()
99  {
100  PRECONDITION(!m_stack.empty());
101  while(true)
102  {
103  if(m_stack.back().it==m_stack.back().end)
104  {
105  m_stack.pop_back();
106  if(m_stack.empty())
107  break;
108  }
109  // Check eg. if we haven't seen this node before
110  else if(this->downcast().push_expr(*m_stack.back().it))
111  break;
112  m_stack.back().it++;
113  }
114  return this->downcast();
115  }
116 
117  depth_iterator_t &next_sibling_or_parent()
118  {
119  PRECONDITION(!m_stack.empty());
120  m_stack.pop_back();
121  if(!m_stack.empty())
122  {
123  ++m_stack.back().it;
124  return ++(*this);
125  }
126  return this->downcast();
127  }
128 
131  depth_iterator_t operator++(int)
132  {
133  depth_iterator_t tmp(this->downcast());
134  this->operator++();
135  return tmp;
136  }
137 
140  const exprt &operator*() const
141  {
142  PRECONDITION(!m_stack.empty());
143  return m_stack.back().expr.get();
144  }
145 
148  const exprt *operator->() const
149  { return &**this; }
150 
151 protected:
153  depth_iterator_baset()=default;
154 
156  explicit depth_iterator_baset(const exprt &root)
157  { this->push_expr(root); }
158 
161  ~depth_iterator_baset()=default;
162 
165  { m_stack=std::move(other.m_stack); }
168  { m_stack=std::move(other.m_stack); }
169 
170  const exprt &get_root()
171  {
172  return m_stack.front().expr.get();
173  }
174 
181  {
182  PRECONDITION(!m_stack.empty());
183  // Cast the root expr to non-const
184  exprt *expr = &const_cast<exprt &>(get_root());
185  for(auto &state : m_stack)
186  {
187  // This deliberately breaks sharing as expr is now non-const
188  auto &operands = expr->operands();
189  // Get iterators into the operands of the new expr corresponding to the
190  // ones into the operands of the old expr
191  const auto i=operands.size()-(state.end-state.it);
192  const auto it=operands.begin()+i;
193  state.expr = *expr;
194  state.it=it;
195  state.end=operands.end();
196  // Get the expr for the next level down to use in the next iteration
197  if(!(state==m_stack.back()))
198  {
199  expr = &*it;
200  }
201  }
202  return *expr;
203  }
204 
211  bool push_expr(const exprt &expr)
212  {
213  m_stack.emplace_back(expr, expr.operands().begin(), expr.operands().end());
214  return true;
215  }
216 
217 private:
218  std::deque<depth_iterator_expr_statet> m_stack;
219 
220  depth_iterator_t &downcast()
221  { return static_cast<depth_iterator_t &>(*this); }
222 };
223 
225  public depth_iterator_baset<const_depth_iteratort>
226 {
227 public:
229  explicit const_depth_iteratort(const exprt &expr):
230  depth_iterator_baset(expr) { }
232  const_depth_iteratort()=default;
233 };
234 
235 class depth_iteratort final:
236  public depth_iterator_baset<depth_iteratort>
237 {
238 private:
241  std::function<exprt &()> mutate_root;
242 
243 public:
245  depth_iteratort()=default;
246 
251  {
252  }
253 
261  explicit depth_iteratort(
262  const exprt &expr,
263  std::function<exprt &()> mutate_root)
264  : depth_iterator_baset(expr), mutate_root(std::move(mutate_root))
265  {
266  // If you don't provide a mutate_root function then you must pass a
267  // non-const exprt (use the other constructor).
268  PRECONDITION(this->mutate_root);
269  }
270 
278  {
279  if(mutate_root)
280  {
281  exprt &new_root = mutate_root();
282  INVARIANT(
283  &new_root.read() == &get_root().read(),
284  "mutate_root must return the same root node that depth_iteratort was "
285  "constructed with");
286  mutate_root = nullptr;
287  }
289  }
290 };
291 
293  public depth_iterator_baset<const_unique_depth_iteratort>
294 {
296 public:
298  explicit const_unique_depth_iteratort(const exprt &expr):
299  depth_iterator_baset(expr),
300  m_traversed({ expr }) { }
303 private:
305  bool push_expr(const exprt &expr) // "override" - hide base class method
306  {
307  const bool inserted=this->m_traversed.insert(expr).second;
308  if(inserted)
310  return inserted;
311  }
312  std::set<exprt> m_traversed;
313 };
314 
315 #endif
depth_iterator_baset::operator->
const exprt * operator->() const
Dereference operator (member access) Dereferencing end() iterator is undefined behaviour.
Definition: expr_iterator.h:148
depth_iterator_expr_statet
Helper class for depth_iterator_baset.
Definition: expr_iterator.h:42
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
const_unique_depth_iteratort
Definition: expr_iterator.h:292
depth_iterator_baset::operator++
depth_iterator_t & operator++()
Preincrement operator Do not call on the end() iterator.
Definition: expr_iterator.h:98
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:305
depth_iterator_baset::get_root
const exprt & get_root()
Definition: expr_iterator.h:170
depth_iterator_expr_statet::expr
std::reference_wrapper< const exprt > expr
Definition: expr_iterator.h:50
depth_iterator_baset::~depth_iterator_baset
~depth_iterator_baset()=default
Destructor Protected to discourage upcasting.
depth_iteratort
Definition: expr_iterator.h:235
depth_iterator_baset::operator++
depth_iterator_t operator++(int)
Post-increment operator Expensive copy.
Definition: expr_iterator.h:131
depth_iterator_expr_statet::end
operands_iteratort end
Definition: expr_iterator.h:52
exprt
Base class for all expressions.
Definition: expr.h:54
invariant.h
depth_iterator_baset::depth_iterator_baset
friend class depth_iterator_baset
Definition: expr_iterator.h:80
depth_iterator_baset::next_sibling_or_parent
depth_iterator_t & next_sibling_or_parent()
Definition: expr_iterator.h:117
depth_iterator_expr_statet::depth_iterator_expr_statet
depth_iterator_expr_statet(const exprt &expr, operands_iteratort it, operands_iteratort end)
Definition: expr_iterator.h:45
depth_iterator_baset::reference
const typedef exprt & reference
Definition: expr_iterator.h:76
const_depth_iteratort::const_depth_iteratort
const_depth_iteratort()=default
Create an end iterator.
operator==
bool operator==(const depth_iterator_expr_statet &left, const depth_iterator_expr_statet &right)
Definition: expr_iterator.h:55
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:261
expr.h
const_unique_depth_iteratort::m_traversed
std::set< exprt > m_traversed
Definition: expr_iterator.h:312
depth_iterator_baset::operator*
const exprt & operator*() const
Dereference operator Dereferencing end() iterator is undefined behaviour.
Definition: expr_iterator.h:140
irept::read
const dt & read() const
Definition: irep.h:406
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:241
depth_iterator_baset::depth_iterator_baset
depth_iterator_baset(depth_iterator_baset &&other)
Definition: expr_iterator.h:164
const_depth_iteratort
Definition: expr_iterator.h:224
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:298
const_depth_iteratort::const_depth_iteratort
const_depth_iteratort(const exprt &expr)
Create iterator starting at the supplied node (root)
Definition: expr_iterator.h:229
const_unique_depth_iteratort::depth_iterator_baset
friend depth_iterator_baset
Definition: expr_iterator.h:295
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:211
depth_iterator_baset
Depth first search iterator base - iterates over supplied expression and all its operands recursively...
Definition: expr_iterator.h:70
depth_iterator_baset::downcast
depth_iterator_t & downcast()
Definition: expr_iterator.h:220
depth_iteratort::mutate
exprt & mutate()
Obtain non-const reference to the exprt instance currently pointed to by the iterator.
Definition: expr_iterator.h:277
depth_iterator_baset::depth_iterator_baset
depth_iterator_baset(const exprt &root)
Create begin iterator, starting at the supplied node.
Definition: expr_iterator.h:156
depth_iterator_baset::value_type
exprt value_type
Definition: expr_iterator.h:74
depth_iterator_baset::operator==
bool operator==(const depth_iterator_baset< other_depth_iterator_t > &other) const
Definition: expr_iterator.h:83
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:167
depth_iterator_baset::pointer
const typedef exprt * pointer
Definition: expr_iterator.h:75
depth_iterator_baset::mutate
exprt & mutate()
Obtain non-const exprt reference.
Definition: expr_iterator.h:180
depth_iterator_baset::m_stack
std::deque< depth_iterator_expr_statet > m_stack
Definition: expr_iterator.h:218
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:250
depth_iterator_baset::operator!=
bool operator!=(const depth_iterator_baset< other_depth_iterator_t > &other) const
Definition: expr_iterator.h:90
exprt::operands
operandst & operands()
Definition: expr.h:78
depth_iterator_baset::difference_type
void difference_type
Definition: expr_iterator.h:73
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:77
depth_iterator_expr_statet::it
operands_iteratort it
Definition: expr_iterator.h:51