CBMC
Loading...
Searching...
No Matches
expr_iterator.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: exprt iterator module
4
5Author: 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
33class 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
52inline bool operator==(
54 const depth_iterator_expr_statet &right)
55{
56 return left.op_idx == right.op_idx && left.expr.get() == right.expr.get();
57}
58
65template<typename depth_iterator_t>
67{
68public:
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>
77
78 template <typename other_depth_iterator_t>
81 {
82 return m_stack==other.m_stack;
83 }
84
85 template <typename other_depth_iterator_t>
88 {
89 return !(*this == other);
90 }
91
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
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
131 {
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
150protected:
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 {
168 m_stack = std::move(other.m_stack);
169 return *this;
170 }
171
173 {
174 return m_stack.front().expr.get();
175 }
176
183 {
184 PRECONDITION(!m_stack.empty());
185 // Cast the root expr to non-const
186 exprt *expr = &const_cast<exprt &>(get_root());
187 for(auto &state : m_stack)
188 {
189 // This deliberately breaks sharing as expr is now non-const
190 (void)expr->write();
191 state.expr = *expr;
192 // Get the expr for the next level down to use in the next iteration
193 if(!(state == m_stack.back()))
194 expr = &expr->operands()[state.op_idx];
195 }
196 return *expr;
197 }
198
204 bool push_expr(const exprt &expr)
205 {
206 m_stack.emplace_back(expr);
207 return true;
208 }
209
210private:
211 std::deque<depth_iterator_expr_statet> m_stack;
212
214 { return static_cast<depth_iterator_t &>(*this); }
215};
216
218 public depth_iterator_baset<const_depth_iteratort>
219{
220public:
222 explicit const_depth_iteratort(const exprt &expr):
223 depth_iterator_baset(expr) { }
226};
227
228class depth_iteratort final:
229 public depth_iterator_baset<depth_iteratort>
230{
231private:
234 std::function<exprt &()> mutate_root;
235
236public:
239
244 {
245 }
246
255 const exprt &expr,
256 std::function<exprt &()> mutate_root)
258 {
259 // If you don't provide a mutate_root function then you must pass a
260 // non-const exprt (use the other constructor).
262 }
263
271 {
272 if(mutate_root)
273 {
275 INVARIANT(
276 &new_root.read() == &get_root().read(),
277 "mutate_root must return the same root node that depth_iteratort was "
278 "constructed with");
279 mutate_root = nullptr;
280 }
282 }
283};
284
286 public depth_iterator_baset<const_unique_depth_iteratort>
287{
289public:
291 explicit const_unique_depth_iteratort(const exprt &expr):
293 m_traversed({ expr }) { }
296private:
298 bool push_expr(const exprt &expr) // "override" - hide base class method
299 {
300 const bool inserted=this->m_traversed.insert(expr).second;
301 if(inserted)
303 return inserted;
304 }
305 std::set<exprt> m_traversed;
306};
307
308#endif
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
const_depth_iteratort(const exprt &expr)
Create iterator starting at the supplied node (root)
const_depth_iteratort()=default
Create an end iterator.
const_unique_depth_iteratort()=default
Create an end iterator.
bool push_expr(const exprt &expr)
Push expression onto the stack and add to the set of traversed exprts.
std::set< exprt > m_traversed
const_unique_depth_iteratort(const exprt &expr)
Create iterator starting at the supplied node (root)
Depth first search iterator base - iterates over supplied expression and all its operands recursively...
depth_iterator_t & next_sibling_or_parent()
depth_iterator_t & operator++()
Preincrement operator Do not call on the end() iterator.
depth_iterator_baset(const depth_iterator_baset &)=default
exprt & mutate()
Obtain non-const exprt reference.
std::deque< depth_iterator_expr_statet > m_stack
depth_iterator_baset & operator=(const depth_iterator_baset &)=default
const exprt * operator->() const
Dereference operator (member access) Dereferencing end() iterator is undefined behaviour.
depth_iterator_baset(const exprt &root)
Create begin iterator, starting at the supplied node.
const exprt & operator*() const
Dereference operator Dereferencing end() iterator is undefined behaviour.
depth_iterator_baset(depth_iterator_baset &&other)
const exprt * pointer
bool operator!=(const depth_iterator_baset< other_depth_iterator_t > &other) const
bool push_expr(const exprt &expr)
Pushes expression onto the stack If overridden, this function should be called from the inheriting cl...
bool operator==(const depth_iterator_baset< other_depth_iterator_t > &other) const
const exprt & get_root()
depth_iterator_t operator++(int)
Post-increment operator Expensive copy.
std::forward_iterator_tag iterator_category
depth_iterator_t & downcast()
const exprt & reference
depth_iterator_baset & operator=(depth_iterator_baset &&other)
~depth_iterator_baset()=default
Destructor Protected to discourage upcasting.
depth_iterator_baset()=default
Create end iterator.
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...
depth_iteratort(exprt &expr)
Create iterator starting at the supplied node (root) All mutations of the child nodes will be reflect...
exprt & mutate()
Obtain non-const reference to the exprt instance currently pointed to by the iterator.
depth_iteratort()=default
Create an end iterator.
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...
Base class for all expressions.
Definition expr.h:56
operandst & operands()
Definition expr.h:94
dt & write()
Definition irep.h:245
bool operator==(const depth_iterator_expr_statet &left, const depth_iterator_expr_statet &right)
int __CPROVER_ID java::java io InputStream read
Definition java.io.c:5
STL namespace.
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
Helper class for depth_iterator_baset.
std::reference_wrapper< const exprt > expr
depth_iterator_expr_statet(const exprt &expr)
exprt::operandst::const_iterator operands_iteratort