Array-cell sensitivity #5057
Merged
Array-cell sensitivity #5057
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
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. The issue is reported here: diffblue#5022
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]`
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.
This explains how field sensitivity transforms instructions that contain array operations.
These tests can now be executed in our test suite.
These are companions to the existing tests that check the show-vcc output, and serve to check that the formulas generated appear to behave properly.
smowton
requested review from
cesaro,
chrisr-diffblue,
cristina-david,
danpoe,
hannes-steffenhagen-diffblue,
kroening,
martin-cs,
peterschrammel,
pkesseli and
tautschnig
as code owners
This will allow the user of symex to set this limit as needed instead of fixing it to an arbitrary value.
together with no-array-field-sensitivity, this makes it possible to control the maximum size for which the transformation is applied and totally deactivate field sensitivity for arrays if needed.
This checks that field sensitivity applies or not to arrays depending on their size and the value of the option.
smowton
force-pushed
the
romain/feature/array-cell-sensitivity
branch
from
4bf4ebc to
123a68e
Compare
peterschrammel
approved these changes
Aug 23, 2019
allredj
reviewed
Aug 23, 2019
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 123a68e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/124400451
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Copy of #4680 while @romainbrenguier is unavailable. Only difference at time of writing: commit "Make field sensitivity max array size configurable" has been fixed to avoid
goto_symextreferences persisting past that class' lifespan.