Enable automatic limit for array-as-uninterpreted-function [depends-on: #1874] #2108
Conversation
tautschnig
requested review from
kroening,
martin-cs and
peterschrammel
as code owners
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 8089c08).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/108222857
|
Reviews would be appreciated, but still marking do-not-merge as benchmarking is required. (Initial benchmarking on ReachSafety-Arrays suggests that, as expected, the memory footprint grows.) |
tautschnig
changed the title
Record constraints of indexed access to array constants [blocks: #2108]
tautschnig
changed the title
tautschnig
added
the
Needs data
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 4615ed1).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/113976199
|
I have now run this on SV-COMP, and did notice a speedup in some cases, but also a single-digit number of benchmarks newly running out of memory. That's not unexpected, but it does suggest we should put #1874 in place before merging this one. |
tautschnig
changed the title
tautschnig
added
dependent - do not merge
and removed
do not merge
Needs data
|
As discussed in #6130 it would probably be good to merge this PR soon. With that in mind, I've locally rebuilt, rebase, and run unit/regression tests and not seen any problems (or major performance changes). If there is no blocker remaining perhaps this can be rebased, pushed and reviewed for a merge to resole #6130. |
@tautschnig Any issues with merging this as is? @kroening @peterschrammel @martin-cs Codeowner approval/disapproval? |
This is a duplicate of PR diffblue#2108. This is here for alternative author management. Fixes diffblue#6130
There was a problem hiding this comment.
I am OK with this but there is some kind of bug in equality of unbounded arrays which I have yet to reliably trigger via C or locate. I figure that this might expose it so it would be good to have a few tests of what happens when an array is over MAX_FLATTENED_ARRAY_SIZE
| if(total>(1<<30)) // realistic limit | ||
| throw analysis_exceptiont("array too large for flattening"); | ||
|
|
||
| if(total < 0) |
There was a problem hiding this comment.
I feel l;ke maybe this would like to become an invariant?
This is a duplicate of PR diffblue#2108. This is here for alternative author management. Fixes diffblue#6130
Previously, the command line permitted setting uninterpreted functions to "never" or "always", where "never" actually was the default. The "automatic" mode could not be enabled in any way. This reverts diffblue#6232, but now includes additional changes to the array theory to handle nested struct members no different from members of a top-level struct. Fixes: diffblue#2018
tautschnig
changed the title
tautschnig
force-pushed
the
array-auto
branch
from
1677386 to
c9ca311
Compare
|
Note to self: |
|
Closing due to age (no further comment on PR content), please reopen with rebase on develop if you intent to continue this work. |
Previously, the command line permitted setting uninterpreted functions to "never" or "always", where "never" actually was the default. The "automatic" mode could not be enabled in any way. We previously attempted to do this in in diffblue#6194 (inspired by diffblue#2108, but not picking up all its changes), but then reverted the gist of the change in diffblue#6232 as `array-bug-6230/main.c` demonstrated lingering issues. This PR now addresses the flaw in the array theory back-end. We may still run into performance regressions as the threshold of 1000 bits of total size of the array object is possibly lower than where the cost of bit-blasting exceeds the cost of constraints produced by our current array theory implementation. Two of our existing regression tests already demonstrate this problem, hence those now use `--arrays-uf-never`.
Previously, the command line permitted setting uninterpreted functions
to "never" or "always", where "never" actually was the default. The
"automatic" mode could not be enabled in any way.
This reverts #6232, but now includes additional changes to the array
theory to handle nested struct members no different from members of a
top-level struct.
Fixes: #2018