fix: Set/forall comprehensions with subtyping for issue #697 #1522
Conversation
This file contains 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
Fixed conflicts in Resolver.cs
More explicit error message about what is the type that is subset.
MikaelMayer
commented
Nov 9, 2021
Ensures that CheckIsCompilable does not try to report errors if no resolver is provided.
Added null tests everywhere needed. More precise error message
Else, recursive calls were skipped.
RustanLeino
requested changes
Nov 19, 2021
- Fixed Explicitely => Explicitly everywhere. - Use of NormalizeExpand(true) in the two pattern matching places - Defined `AsSubsetType` in DafnyAST - "var" and "int" closer to the for loop - Simpler getter for ErrorReporter repporter - Curly braces around newly inserted single if-statements. - String interpolation for error message - Removed dead code - Corrected indentation in dfy files - Removed useless type annotations in dfy files - test 697b prints something - Test 697d tests forall and exists with compilable constraints and prints something.
RustanLeino
approved these changes
Dec 1, 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.
This PR is a quick fix for issues #697 and #698.
The problem: Unsound comprehensions with subset types.
The solution implemented in this PR:
ConstraintIsCompilableforSubsetTypeDeclexpressions.ConstraintIsCompilableis false, will raise two errors, the second one indicating why it is not compilable. This has been implemented as a new traversal as the end of Pass 2 in the Resolver, as I did not find a tree traversal feature which is fully ghost-awareMaybeInjectSubsetConstraintwhich injects the guard code for for-comprehensions, exists-comprehensions, map-comprehensions and set-comprehensions.How I tested it.
I added 8 tests:
git-issues/git-issue-697.dfy: A set comprehension with compilable subset constraint that did not compile correctly and used to crash at execution. Now it compiles and does not crash.git-issues/git-issue-697b.dfy: A map comprehension with compilable subset constraint that did not compile correctly and used to crash at execution. Now it compiles and does not crash.git-issues/git-issue-697c.dfy: A set comprehension, a map comprehension and a forall comprehension with ghost subset constraint that used to compile and crash at execution. Now it does not compiles and raises six errors.git-issues/git-issue-697d.dfy: A set comprehension with ghost & compilable subset constraint that used to compile and crash at execution. Now it compiles and does not crash.git-issues/git-issue-697e.dfy: A forall comprehension with only inferred ghost subset constraint. It used to compile and crash at execution time. Now it compiles and does not crash.git-issues/git-issue-697f.dfy: A ghost subset constraint that is never used in comprehensions. It used to compile and continues to compile, ensuring this PR does not break this existing desirable behavior.git-issues/git-issue-698.dfy: A forall comprehension with compilable subset constraint that did not compile correctly and used to crash at execution. Now it compiles and does not crash.git-issues/git-issue-698b.dfy: An exist comprehension with compilable subset constraint that did not compile correctly and used to crash at execution. Now it compiles and does not crash.