Skip to content

Commit 884d002

Browse files
author
Daniel Kroening
committed
pre/post traversal expression transformers
Transformers for expressions that offer an interface similar to that offered by void goto_programt::transform(std::function<optionalt<exprt>(exprt)>); on goto programs. Both pre- and post-traversal options are available. The key benefit over the non-const visit method is that sharing is only broken up when required.
1 parent 16f63e8 commit 884d002

File tree

2 files changed

+59
-0
lines changed

2 files changed

+59
-0
lines changed

src/util/expr.cpp

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -287,6 +287,63 @@ void exprt::visit_post(std::function<void(const exprt &)> visitor) const
287287
visit_post_template(visitor, this);
288288
}
289289

290+
optionalt<exprt>
291+
exprt::transform_pre(std::function<optionalt<exprt>(exprt)> visitor) const
292+
{
293+
auto visitor_result = visitor(*this);
294+
295+
// make a copy
296+
exprt tmp = visitor_result.value_or(*this);
297+
298+
bool op_changed = false;
299+
300+
for(auto &op : tmp.operands()) // this breaks sharing of the copy
301+
{
302+
auto op_result = op.transform_pre(visitor);
303+
if(op_result.has_value())
304+
{
305+
op = std::move(op_result.value());
306+
op_changed = true;
307+
}
308+
}
309+
310+
if(op_changed)
311+
return std::move(tmp);
312+
else
313+
return visitor_result;
314+
}
315+
316+
optionalt<exprt>
317+
exprt::transform_post(std::function<optionalt<exprt>(exprt)> visitor) const
318+
{
319+
// make a copy
320+
exprt tmp = *this;
321+
322+
bool op_changed = false;
323+
324+
for(auto &op : tmp.operands()) // this breaks sharing of the copy
325+
{
326+
auto op_result = op.transform_post(visitor);
327+
if(op_result.has_value())
328+
{
329+
op = std::move(op_result.value());
330+
op_changed = true;
331+
}
332+
}
333+
334+
if(op_changed)
335+
{
336+
auto visitor_result = visitor(tmp);
337+
338+
if(visitor_result.has_value())
339+
return std::move(visitor_result.value());
340+
else
341+
return std::move(tmp);
342+
}
343+
else
344+
return visitor(*this);
345+
}
346+
290347
template <typename T>
291348
static void visit_pre_template(std::function<void(T &)> visitor, T *_expr)
292349
{

src/util/expr.h

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -332,12 +332,14 @@ class exprt:public irept
332332
void visit(class const_expr_visitort &visitor) const;
333333
void visit_pre(std::function<void(exprt &)>);
334334
void visit_pre(std::function<void(const exprt &)>) const;
335+
optionalt<exprt> transform_pre(std::function<optionalt<exprt>(exprt)>) const;
335336

336337
/// These are post-order traversal visitors, i.e.,
337338
/// the visitor is executed on a node _after_ its children
338339
/// have been visited.
339340
void visit_post(std::function<void(exprt &)>);
340341
void visit_post(std::function<void(const exprt &)>) const;
342+
optionalt<exprt> transform_post(std::function<optionalt<exprt>(exprt)>) const;
341343

342344
depth_iteratort depth_begin();
343345
depth_iteratort depth_end();

0 commit comments

Comments
 (0)