gobra
gobra copied to clipboard
viperproject
Removes Injectivity Assumptions on Inhale
Before merging this, I would also like to run it with verifiedSCION
Makes sense. I've just opened this PR to detect possible issues before the Viper release. Might make sense to run your experiments sooner than later in case we need to defer the Viper release
I believe it makes sense to merge these changes before I start looking at enabling the consistency checks. I am now running tests locally on the verified scion repository.
@ArquintL should we disable the dense_sparse_matrix tests? Or did you find a way to make them pass the injectivity tests?
@ArquintL should we close this PR? Right now, it seems unlikely that it will be merged. Regarding the changes to the encoding, if you think it is worth keeping, maybe we can open a PR for that already
The only changes to me seems to be that I use len(arr) instead of the statically known array length. This is only a problem in the context of null arrays because their length is 1 to we cannot simply use the statically known array length (which can be different from 1). This issue did not show up before because we assumed injectivity but as soon as you no longer assume it Viper will complain about the quantified permissions no longer being injective because injectivity of array locations is defined only within bounds.
I thus think it does not hurt merging the changes to the encoding in even though they are not strictly necessary as long as we assume injectivity. However, there are 2 points we should check:
- what is the impact on performance due to introducing a
lenexpression instead of using anintliteral (while still assuming injectivity) - do we observe incompletenesses (also while still assuming injectivity)
Should only be merged after merging PR #531 and fixing the resulting merge conflicts. Since #531 changes the representation of null values, these changes might actually no longer be needed