feat: Support for the {:opaque} attibute on const
#2545
There are no files selected for viewing
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
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
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
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
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
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,96 @@ | ||
| // RUN: %dafny_0 /compile:0 "%s" > "%t" | ||
| // RUN: %diff "%s.expect" "%t" | ||
|
|
||
| module Module { | ||
| module M { | ||
| const {:opaque} Five := 5; | ||
|
There was a problem hiding this comment. The semi-colon at the end of the line is not needed. |
||
| } | ||
|
|
||
| method Test() { | ||
| assert M.Five == 5; // error: this is not known here | ||
| reveal M.Five; | ||
| assert M.Five == 5; | ||
|
There was a problem hiding this comment. This test might not have the effect you think. If you assert something twice, I expect Dafny to complain only about the first assert. This is because Dafny's semantics of Instead, I suggest that you create two paths through your method: if * {
assert M.Five == 5;
} else {
reveal M.Five;
assert M.Five == 5;
}or if
case true =>
assert M.Five == 5;
case true =>
reveal M.Five;
assert M.Five == 5; |
||
| } | ||
| } | ||
|
|
||
| module Class { | ||
| class Class { | ||
| const {:opaque} Five := 5; | ||
| } | ||
|
|
||
| method Test(c: Class) { | ||
| assert c.Five == 5; // error: this is not known here | ||
| reveal c.Five; | ||
| assert c.Five == 5; | ||
| } | ||
| } | ||
|
|
||
| module TypeMembers { | ||
| trait Tr { | ||
| const fav: bool; | ||
| const {:opaque} IsFavorite := fav; | ||
| static const {:opaque} Five := 5; | ||
| } | ||
|
|
||
| datatype Color = Carrot | Pumpkin | ||
| { | ||
| const {:opaque} IsFavorite := this == Pumpkin | ||
| static const {:opaque} Five := 5; | ||
| } | ||
|
|
||
| newtype Small = x | 30 <= x < 40 witness 30 | ||
| { | ||
| const {:opaque} IsFavorite := this == 34 | ||
| static const {:opaque} Five := 5; | ||
| } | ||
|
|
||
| method Test(tr: Tr, c: Color, s: Small) { | ||
| if | ||
| case tr.IsFavorite => | ||
| assert tr.fav; // error: this is not known here | ||
| case c.IsFavorite => | ||
| assert c == Pumpkin; // error: this is not known here | ||
| case s.IsFavorite => | ||
| assert s == 34; // error: this is not known here | ||
| case tr.IsFavorite => | ||
| reveal tr.IsFavorite; | ||
| assert tr.fav; | ||
| case c.IsFavorite => | ||
| reveal c.IsFavorite; | ||
| assert c == Pumpkin; | ||
| case s.IsFavorite => | ||
| reveal s.IsFavorite; | ||
| assert s == 34; | ||
| case true => | ||
| if tr.IsFavorite && c.IsFavorite && s.IsFavorite { | ||
| reveal tr.IsFavorite, c.IsFavorite, s.IsFavorite; | ||
| assert !tr.fav || c == Carrot || s == 39; // error: not true | ||
| } | ||
| } | ||
|
|
||
| function IsUneven(i: int): bool { i % 2 == 1 } | ||
|
|
||
| method StaticTest() { | ||
| if | ||
| case IsUneven(Tr.Five) => | ||
| assert Tr.Five == 5; // error: this is not known here | ||
| case IsUneven(Color.Five) => | ||
| assert Color.Five == 5; // error: this is not known here | ||
| case IsUneven(Small.Five) => | ||
| assert Color.Five == 5; // error: this is not known here | ||
| case IsUneven(Tr.Five) => | ||
| reveal Tr.Five; | ||
| assert Tr.Five == 5; | ||
| case IsUneven(Color.Five) => | ||
| reveal Color.Five; | ||
| assert Color.Five == 5; | ||
| case IsUneven(Small.Five) => | ||
| reveal Small.Five; | ||
| assert Small.Five == 5; | ||
| case true => | ||
| if IsUneven(Tr.Five) && IsUneven(Color.Five) && IsUneven(Small.Five) { | ||
| reveal Tr.Five, Color.Five, Small.Five; | ||
| assert Tr.Five != 5 || Color.Five != 5 || Small.Five != 5; // error: not true | ||
| } | ||
| } | ||
| } | ||
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,12 @@ | ||
| OpaqueConstants.dfy(10,18): Error: assertion might not hold | ||
| OpaqueConstants.dfy(22,18): Error: assertion might not hold | ||
| OpaqueConstants.dfy(50,16): Error: assertion might not hold | ||
| OpaqueConstants.dfy(52,15): Error: assertion might not hold | ||
| OpaqueConstants.dfy(54,15): Error: assertion might not hold | ||
| OpaqueConstants.dfy(67,38): Error: assertion might not hold | ||
| OpaqueConstants.dfy(76,21): Error: assertion might not hold | ||
| OpaqueConstants.dfy(78,24): Error: assertion might not hold | ||
| OpaqueConstants.dfy(80,24): Error: assertion might not hold | ||
| OpaqueConstants.dfy(93,47): Error: assertion might not hold | ||
|
|
||
| Dafny program verifier finished with 3 verified, 10 errors |
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
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
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
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I suggest combining these two rewriters into one
OpaqueRewriter.