Prototype: array-cell-sensitivity #4918
Closed
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
smowton
requested review from
kroening,
peterschrammel and
tautschnig
as code owners
smowton
force-pushed
the
smowton/cleanup/rename-lhs-rvalues-up-front
branch
from
722cfec to
a3bec27
Compare
smowton
force-pushed
the
smowton/cleanup/rename-lhs-rvalues-up-front
branch
2 times, most recently
from
ff94188 to
64cfecf
Compare
allredj
reviewed
Jul 25, 2019
Contributor
allredj
left a comment
allredj
left a comment
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 64cfecf).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/120673312
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.
smowton
force-pushed
the
smowton/cleanup/rename-lhs-rvalues-up-front
branch
from
64cfecf to
e8f16c4
Compare
This allows applying constant propagation without upgrading non-constant symbols to L2, which is useful for the dereferencing logic, as the value-set used to resolve pointer aliasing is indexed by L1 names.
This may lead to application of array-cell-sensitivity (i.e. querying the symbol some_array[[1]] instead of some_array[some_index]), leading to higher precision. Some tests must be amended because better constant propagation causes some test behaviour to change as symex has better knowledge regarding the targets of pointers.
The use of field_sensitivity for arrays can be expensive for big arrays so we have to set a limit on the size of constant arrays which get processed. The value 64 was determined by changing the size of the array in the test regression/cbmc/variable-access-to-constant-array and reducing it until there was no significant difference in execution time between the versions of CBMC with and without array cell propagation. For the chosen value the execution time was around 0.05 second in both cases (for comparison with size 1024 the time with propagation was 0.5 sec, against 0.1 without).
In some cases, like the test in regression/cbmc/Global_Initialization2, the array type is incomplete and changed in the symbol table after the main function has been converted, leading to inconsistencies. This means we can get nil instead of the size in field_sensitivityt::apply, though the actual size is present in the symbol table.
This is to allow constant propagation to take place and know whether the size is actually constant, which can allow field sensitivity to apply.
When the index is not constant when accessing a constant size array, we
should expand the expression into `{array[0]; array[1];...}[index]` so
that the relation with field sensitivity expressions `array[[0]]`,
`array[[1]]`, etc, is not lost.
This is important to consider dereferenced object as read value.
This may be necessary for constant propagation of the format string. An example of that is in regression/cbmc/printf1
With field sensitivity on arrays, the element can be initialized in two steps, first the field f then the field array.
Propagatiof of values of array cells lead to different expressions in VCC.
This is failing because of this bug: diffblue#4749
Avoid lhs of the form `{array[0], array[1]}[0]`
These used to have side-effects on their parameters, and will still compile if used that way, so let's use NODISCARD to enforce that their new return value is consulted when necessary.
Most are for C, then a couple are duplicated for Java to check whether its use of a structure to represent all arrays makes any difference.
smowton
force-pushed
the
smowton/cleanup/rename-lhs-rvalues-up-front
branch
from
e8f16c4 to
e817618
Compare
smowton
changed the title
Contributor
Author
|
Work on this has moved back to #4680 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Do not review; this is a test branch for array-cell sensitivity