Byte-operator lowering: use lambda_exprt for non-constant width #4651
Conversation
tautschnig
requested review from
chrisr-diffblue,
kroening,
martin-cs,
peterschrammel,
pkesseli and
smowton
as code owners
tautschnig
force-pushed
the
use-lambda
branch
2 times, most recently
from
2256b1e to
f445df5
Compare
src/util/simplify_expr_array.cpp
Outdated
| expr.swap(tmp); | ||
| simplify_rec(expr); |
There was a problem hiding this comment.
Is this in the wrong commit? It doesn't match the commit message.
There was a problem hiding this comment.
Fair point, I have put it into a commit of its own.
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: f445df5).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/111703192
Status will be re-evaluated on next push.
Common spurious failures include: 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); compatibility was already broken by an earlier merge.
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 72fa110).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/111728575
Status will be re-evaluated on next push.
Common spurious failures include: 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); compatibility was already broken by an earlier merge.
src/util/std_expr.h
Outdated
| @@ -4460,4 +4460,78 @@ inline cond_exprt &to_cond_expr(exprt &expr) | |||
| return ret; | |||
| } | |||
|
|
|||
| /// \brief Construct an array from an anonymous function | |||
There was a problem hiding this comment.
It's good that there is a comment here, but it isn't enough that I can figure out what it does. Why is it always an array? Is it because it's used in flattening?
There was a problem hiding this comment.
Fixed in #4672, which now takes care of the initial commits in this PR.
There was a problem hiding this comment.
Thanks, I find that much clearer
tautschnig
changed the title
Add an API for lambda expressions [blocks: #4651]
tautschnig
changed the title
tautschnig
assigned smowton, kroening, peterschrammel and chrisr-diffblue and unassigned tautschnig
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 89afd23).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/112376060
Status will be re-evaluated on next push.
Common spurious failures include: 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); compatibility was already broken by an earlier merge.
tautschnig
assigned tautschnig and unassigned smowton, kroening, peterschrammel and chrisr-diffblue
Array comprehension expressions are very useful to construct arrays of unbounded size. To support this use case, the array theory in the bit blasting back-end needs to handle them.
This case shouldn't actually occur, and is thus now an invariant rather than half-supporting it and otherwise failing with an exception. This is a first step towards getting rid of the remaining exceptions in byte-operator lowering.
Arrays with non-constant size are now encoded using array comprehensions. This lifts the prior limit of only being able to perform byte updates when at least the size of the update or the size of the target was known.
The two remaining cases really _are_ invariants.
This PR does/has to do a couple of things (please review commit-by-commit):