Precondition Invariant: Disjunct over matching state invariants #786
Conversation
In this example, among others, the following precondition_loop_invariants are generated:
loop_invariant:
string: result == 1
[...]
precondition:
string: '*ptr1 == 5 && *ptr2 == 5'
and:
loop_invariant:
string: result == 0
[...]
precondition:
string: '*ptr1 == 5 && *ptr2 == 5'
To fix this issue, grouping of precondition_loop_invariants is required.
jerhard
added
the
pr-dependency
|
An example where the invariants generated were previously inconsistent was added here. |
…ed for one state. In case that an invariant for a state could not be generated, no precondition_loop_invariant is generated. Reason: The invariant (that failed to be generated) must be part of the postcondition.
|
Now, for the example, instead of generating inconsistent/wrong However, due to the way these precondition invariants are created, we still create one precondition invariant per context per program point. For example in this case, we generate this precondition invariant twice. |
| } else { | ||
| result = 1; | ||
| } | ||
| // Look at the generated witness.yml to check whether there are contradictory precondition_loop_invariant[s] |
There was a problem hiding this comment.
This isn't great as a test, but without something like #787 we cannot do any better either.
Given the groupings, couldn't we avoid the duplication? Or would that not work to the possible non-symmetry of the relation? |
…y and Function(-return) nodes to is_invariant_node
…ver all other contexts of the function
As the grouping is implemented now, the problem with deduplicating entries is indeed the possibility of non-symmetry. For this bucket-per-invariant approach, the invariants should best be usable as keys in some hashtable. |
There was a problem hiding this comment.
Looks good! For the order of merging things I would propose the following:
- Get Add experimental generation and validation of YAML witness invariants with preconditions #752 approved itself, because then its diff is easier to look at.
- Then merge this into Add experimental generation and validation of YAML witness invariants with preconditions #752, so it becomes a complete implementation on its own.
- Finally merge Add experimental generation and validation of YAML witness invariants with preconditions #752 into master, with changes from both included.
I mean if this is merged into #752, then when reviewing #752 the diff also contains all the changes of this PR, as if they were made in #752. It just makes it more difficult to distinguish, which changes we already approved here and thus needn't be re-reviewed in #752. But you can merge this into #752 right away as well, if you want. It doesn't really matter for me. |
sim642
removed
the
pr-dependency
This PR builds on #752.
As already discussed, one must take into account that we may discover multiple contexts that fulfill a precondition we generate for a particular context. Thus, the postcondition of a
precondition_loop_invarianthas to be a disjunction over invariants obtained for "matching" unknowns.An alternative implementation may use
Union-Finddata structures to group preconditions together that do no exclude each other. While this alternative approach would reduce the number of precondition invariants generated, it may also lose some information.