Add experimental generation and validation of YAML witness invariants with preconditions #752
Conversation
sim642
added
cleanup
|
Although the entry type for invariants with preconditions is currently unofficial, it would be good to get this merged for its refactoring of the YAML witnesses. The refactoring makes it easy to work with different entry types, possibly including |
jerhard
left a comment
jerhard
left a comment
There was a problem hiding this comment.
We discussed this here a bit in Munich, with @michael-schwarz, @stilscher.
It probably makes sense to implement this grouping of preconditions before merging this, as otherwise the produced precondition-witnesses could be misleading.
For a function, one would first generate all the invariant expressions for the contexts, and then check which of the start states may satisfy the condition and group them. Subsequently one would generate the precondition-invariants for these groups of contexts.
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.
…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.
…y and Function(-return) nodes to is_invariant_node
…ver all other contexts of the function
Precondition Invariant: Disjunct over matching state invariants
2 participants
Adds the experimental YAML witness entry type
precondition_loop_invariant, which is likeloop_invariant, but has a secondpreconditionexpression to match contexts.Current validation semantics is that the invariant is only checked for contexts where the precondition must hold.
Additionally refactors all the YAML witness type definitions etc to be more type-safe and extensible.