Byte-operator lowering: use lambda_exprt for non-constant width#4651
Byte-operator lowering: use lambda_exprt for non-constant width#4651tautschnig merged 4 commits intodiffblue:developfrom
Conversation
2256b1e to
f445df5
Compare
| exprt tmp = lambda_expr.body(); | ||
| replace_expr(lambda_expr.arg(), expr.op1(), tmp); | ||
| 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.
allredj
left a comment
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.
allredj
left a comment
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.
martin-cs
left a comment
There was a problem hiding this comment.
Yes; this could give a significant improvement in performance.
src/util/std_expr.h
Outdated
| 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
Add an API for lambda expressions [blocks: #4651]
allredj
left a comment
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.
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):