Refuse to apply sort predicates to unevaluated terms #4133
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
Sort predicates in K (`isMySort : KItem -> Bool`) only match on the
sort injection of the argument into `KItem`.
Paraphrased:
```
rule isMySort(inj{MySort,KItem}(VAR)) => true
rule isMySort( VAR ) => false [owise]
```
Therefore, the result is wrong in the presence of a function that may
return a super-sort of the target sort.
```
syntax SuperSort ::= MySort | SomethingElse
syntax SuperSort ::= f ( Int ) [function, total]
```
leads to a wrong matching result for a term `isMySort(f(0))`, which in kore would be
`LblisMySort(kseq{}(inj{SortSuperSort{},SortKItem{}}(Lblf{}(\dv{SortInt}("0"))),dotk{}()))`.
The matching routine would report a failed match due to the sorts
being different in the sort injections. However, the sort injection
would change as soon as f(0) gets evaluated (to an `A:MySort`).
See added test for an example K program going wrong without the fix.
The PR changes the evaluation routine to return an indeterminate match
in case it detects a sort predicate applied to a function call. The
iterative evaluation will (bottom-up) evaluate the function call in
the next round and is ultimately able to evaluate the predicate.
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.
Sort predicates in K (
isMySort : KItem -> Bool) only match on the sort injection of the argument intoKItem.Paraphrased:
Therefore, the result is wrong in the presence of a function that may return a super-sort of the target sort.
leads to a wrong matching result for a term
isMySort(f(0)), which in kore would beLblisMySort(kseq{}(inj{SortSuperSort{},SortKItem{}}(Lblf{}(\dv{SortInt}("0"))),dotk{}())).The matching routine would report a failed match due to the sorts being different in the sort injections. However, the sort injection would change as soon as f(0) gets evaluated (to an
A:MySort).See added test for an example K program going wrong without the fix.
The PR changes the evaluation routine to return an indeterminate match in case it detects a sort predicate applied to a function call. The iterative evaluation will (bottom-up) evaluate the function call in the next round and is ultimately able to evaluate the predicate.
Fixes #4132