replace recursion in letify_rec by loop [blocks: #4395] #4406
Conversation
kroening
requested review from
allredj,
martin-cs,
peterschrammel,
romainbrenguier and
tautschnig
as code owners
This avoids stack overflow in the case of expressions with many unique subexpressions. PR #4395 is an exemplar.
kroening
force-pushed
the
non-rec-letify
branch
from
edfe7a0 to
a4a4073
Compare
src/solvers/smt2/letify.cpp
Outdated
| if(map.find(current)->second.count < LET_COUNT) | ||
| return letify_rec(expr, let_order, map, i + 1); | ||
| auto m_it = map.find(current); | ||
| INVARIANT(m_it != map.end(), "expression should have been seen already"); |
There was a problem hiding this comment.
This invariant should be documented. It looks like a precondition of letify.
| @@ -46,11 +46,10 @@ class letifyt | |||
| seen_expressionst &map, | |||
| std::vector<exprt> &let_order); | |||
|
|
|||
| static exprt letify_rec( | |||
| static exprt letify( | |||
There was a problem hiding this comment.
It's maybe a good occasion to document the function
There was a problem hiding this comment.
A request for documentation/aiding understanding below, but my bigger concern is the absence of newly viable tests. I believe we have a number of tests that are marked broken-smt-backend because of this stack overflow. If this fix does what it promises, then presumably it should be possible to enable those tests? I could be wrong, because there may be further problems down the line, but I'd at least like to see this discussed.
src/solvers/smt2/letify.cpp
Outdated
| auto m_it = map.find(current); | ||
| INVARIANT(m_it != map.end(), "expression should have been seen already"); | ||
|
|
||
| if(m_it->second.count >= LET_COUNT) |
There was a problem hiding this comment.
It would be nice to document this magic number. At least I have absolutely no idea why "2" is the right value, or indeed what it even is good for.
There was a problem hiding this comment.
Two is really the only viable choice, and the symbolic name could well be replaced by 2.
"2" means that the expression is used more than once.
"3" (or higher) implies that the procedure becomes worst-case exponential.
There was a problem hiding this comment.
Maybe using "1" instead of "2" would make things a lot clearer? That would make clear we are talking about something we have seen more than once. The named constant here really obfuscates this code, because 1) the name does not convey useful information and 2) one has to look elsewhere to find the value.
There was a problem hiding this comment.
Adding to my comment moments ago: I think this one should be if(m_it->second.count != 1).
There was a problem hiding this comment.
... and the other one in substitute_let is likely also best written as != 1, mirroring this one.
|
@tautschnig The tests are in #4406! |
(I suppose #4395, which solves that part of my request-for-changes. Will comment on the other one above.) |
tautschnig
changed the title
|
Now with improved documentation |
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 7ed433f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/105593807
This avoids stack overflow in the case of expressions with many unique subexpressions. PR #4395 is an exemplar.