Expr-depth-iterator: support iterating over mutated expressions #4385
Conversation
smowton
requested review from
kroening,
peterschrammel,
pkesseli and
tautschnig
as code owners
smowton
force-pushed
the
smowton/fix/expr-iterator-mutated
branch
from
9fdaba2 to
ca42367
Compare
src/util/expr_iterator.h
Outdated
| operands_iteratort it, | ||
| operands_iteratort end): | ||
| expr(expr), it(it), end(end) { } | ||
| inline depth_iterator_expr_statet(const exprt &expr) : expr(expr), op_idx(0) |
There was a problem hiding this comment.
Missing explicit (and you can get rid of the inline, which is actually implicit...).
src/util/expr_iterator.h
Outdated
| // Get iterators into the operands of the new expr corresponding to the | ||
| // ones into the operands of the old expr | ||
| const auto it = operands.end() - (state.end - state.it); | ||
| (void)expr->operands(); |
There was a problem hiding this comment.
Maybe that should be (void)expr->write(); instead of a somewhat random function (operands)?
smowton
force-pushed
the
smowton/fix/expr-iterator-mutated
branch
2 times, most recently
from
04d1223 to
fc35a18
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: fc35a18).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/104448724
src/util/expr_iterator.h
Outdated
| expr = &*it; | ||
| } | ||
| if(!(state == m_stack.back())) | ||
| expr = &const_cast<exprt &>(state.expr.get().operands()[state.op_idx]); |
There was a problem hiding this comment.
❓ Why is another const_cast necessary here?
There was a problem hiding this comment.
Fair enough, replaced with the synonym *expr
The iterators are appealing, but are invalidated when an expression is replaced via mutate(), preventing iteration from continuing over the newly altered node.
smowton
force-pushed
the
smowton/fix/expr-iterator-mutated
branch
from
fc35a18 to
17bee52
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 17bee52).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/104465585
Expr-iterator has always had a mutate() function to enable editing part of an expression tree, and a "next_sibling_or_parent" method to skip walking over the changed expression. However as it turns out using the latter with the former was effectively mandatory because when an expression was replaced wholesale (e.g.
it.mutate() = symbol_exprt("something_different", ...)), then a stale iterator referring to the replaced expr's operands vector led to a segfault on the nextoperator++.This takes the simple approach to fixing that: use integer indices instead of iterators. I also add some basic unit tests, including one that exhibits the crash in question.