SMT2 backend: remove byte operators before calling find_symbols #4379
Conversation
smowton
requested review from
allredj,
chrisr-diffblue,
kroening,
martin-cs,
peterschrammel,
romainbrenguier and
tautschnig
as code owners
smowton
force-pushed
the
smowton/fix/smt2-lower-byte-update-before-find-symbols
branch
5 times, most recently
from
25b90c1 to
7a3f22e
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 7a3f22e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/104380042
|
If you want rid of the expr-iterator workarounds, merge #4385 first |
src/solvers/smt2/smt2_conv.cpp
Outdated
| return lowered_expr; | ||
| } | ||
|
|
||
| exprt smt2_convt::prepare_expr(const exprt &expr) |
There was a problem hiding this comment.
Please document this function. Also a better name than prepare_expr would be helpful.
I am a bit surprised this and lower_byte_operators_rec are not const, and if they could be made static this would be better, in particular you could avoid exposing auxiliary functions in the header.
There was a problem hiding this comment.
Documented and renamed. The whole class uses member functions to pass the namespace around -- I won't get into changing that in this PR.
smowton
force-pushed
the
smowton/fix/smt2-lower-byte-update-before-find-symbols
branch
from
7a3f22e to
a1cfbb5
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: a1cfbb5).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/104411418
|
Did you by any chance check whether this also fixes other tests currently marked "broken-smt-backend"? I think there's a fair chance that it does. |
There was a problem hiding this comment.
+1 for getting #4385 merged first, and then please also take a look whether these fixes resolve even more problems with existing tests as just said.
smowton
force-pushed
the
smowton/fix/smt2-lower-byte-update-before-find-symbols
branch
from
e623944 to
01877d1
Compare
|
Checked; found 4 tests now working. |
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: e623944).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/104457441
Status will be re-evaluated on next push.
Common spurious failures:
-
the cbmc commit has disappeared in the mean time (e.g. in a force-push)
-
the author is not in the list of contributors (e.g. first-time contributors).
-
the compatibility was already broken by an earlier merge.
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 01877d1).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/104458674
|
It seems that |
Otherwise the lowering can introduce new array expressions, which the SMT2 backend's convert_expr expects to have been pre-converted into auxiliary symbols.
If the input expression used a union tag, keep that in the result.
smowton
force-pushed
the
smowton/fix/smt2-lower-byte-update-before-find-symbols
branch
from
01877d1 to
0411ef8
Compare
|
Returned the still-broken tests to their prior state; rebased to use the now-working depth-iterator. |
convert_exprassumes thatfind_symbolshas already made an entry for everyarray_exprt, but byte operator lowering can introduce new ones. Therefore run it up front.The particular construction (depth-iterator plus recursion) is a bit ugly -- this is required because (a) we must keep the post-order strategy or we expose other bugs (see #4380) and (b)
expr_iterator.his broken when expressions are mutated and then the iterator is permitted to visit those mutated parts, despite the design intending this feature. I suggest we get this fix in and then tackle those two individually, particularly as this blocks other PRs.