Fix meet of arrays with different partitioning expressions #486
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
sim642
reviewed
Dec 9, 2021
Member
Author
|
I ran sv-comp again and this fix indeed solves all 120 instances of this problem. |
sim642
approved these changes
Dec 9, 2021
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.
In the course of #419, I modified the
invariantfunction to work on the entire variable instead of only on an offset. The offset is updated and after this the meet between the old and the new value happens.This is beneficial e.g. with our new struct domains.
However, it uncovered an issue with the
meetin the partitioned array domain: If two partitioned values are met and they are partitioned according to different expressions, the resulting component-wisemeetis partitioned according to a bottom expression, which is an invalid value that we never create. (same goes fornarrow).This fixes the immediate problem. In the long run, I will later clean up this mess in #485.
TODO:
Fatal error: exception Failure("ArrayDomain: Unallowed state (one of the partitioning expressions is bot)")for 120 programs #482 on SV-CompCloses #482.