-
Notifications
You must be signed in to change notification settings - Fork 267
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
fix: Fix traits-on-datatype scoping and translation issues (#5058)
This PR fixes and closes three reported bugs related to datatypes extending traits: * Reference-type traits used with `import opened` were not recognized as reference types (issue #4936). * Implicit conversions from a datatype to a parent trait had caused malformed Boogie (issue #4983). This was actually fixed in PR #4997, but the present PR adds tests for it. * Equality (and disequality) comparisons with a datatype (or codatatype) on the _left_ and a parent trait on the _right_ had caused malformed Boogie (issue #4994). Fixes #4936 Closes #4983 Fixes #4994 <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
- Loading branch information
1 parent
598c2c3
commit 81f028b
Showing
18 changed files
with
361 additions
and
37 deletions.
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
16 changes: 16 additions & 0 deletions
16
Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4936a.dfy
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,16 @@ | ||
| // RUN: %testDafnyForEachResolver "%s" -- --general-traits:datatype | ||
|
|
||
| module X { | ||
| trait {:termination false} A extends object {} | ||
| } | ||
|
|
||
| module Y { | ||
| import opened X | ||
|
|
||
| trait B extends A { | ||
| function GetIndex(): nat | ||
| // The following once gave an error, complaining that B is not a reference type. The problem had been that | ||
| // the opened import A was, effectively, hiding the information that A is a reference type. | ||
| reads this | ||
| } | ||
| } |
2 changes: 2 additions & 0 deletions
2
Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4936a.dfy.expect
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,2 @@ | ||
|
|
||
| Dafny program verifier finished with 0 verified, 0 errors |
19 changes: 19 additions & 0 deletions
19
Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4936b.dfy
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,19 @@ | ||
| // RUN: %testDafnyForEachResolver "%s" -- --general-traits:datatype | ||
|
|
||
| module X { | ||
| trait K { } | ||
| trait {:termination false} A extends object, K {} | ||
| } | ||
|
|
||
| module Y { | ||
| import opened X | ||
|
|
||
| trait B extends A { } | ||
|
|
||
| method Test(b: B) returns (a: A) { | ||
| // The following assignment once caused malformed Boogie to be generated. The reason had been that | ||
| // the resolver had not determined B to be a reference type. And that, in turn, had been caused by | ||
| // that the opened import, effectively, had lost the "extends object" information. | ||
| a := b; | ||
| } | ||
| } |
2 changes: 2 additions & 0 deletions
2
Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4936b.dfy.expect
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,2 @@ | ||
|
|
||
| Dafny program verifier finished with 1 verified, 0 errors |
97 changes: 97 additions & 0 deletions
97
Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4936c.dfy
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,97 @@ | ||
| // RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s" -- --general-traits:datatype | ||
|
|
||
| // The early-resolver code that figures out if a trait is a reference type or not is operating so early | ||
| // in the resolver pipeline that opened imports have not yet been resolved into the importing module. | ||
| // Thus, this early-resolver code looks directly into the top-level members of opened imports, but does | ||
| // so without consideration for possible ambiguities. This means that the early-resolver code may not | ||
| // properly figure out if a trait is a reference type or not. But if it gets it wrong, the ambiguity | ||
| // will still be reported as an error later in the resolver pipeline. | ||
| // | ||
| // This test file makes sure that the ambiguous-import errors are indeed being reported and that the | ||
| // resolver doesn't crash until then. | ||
|
|
||
| module X0 { | ||
| // Here, A is a reference type | ||
| trait {:termination false} A extends object {} | ||
| } | ||
|
|
||
| module X1 { | ||
| // Here, A is not a reference type | ||
| trait {:termination false} A {} | ||
| } | ||
|
|
||
| module X2 { | ||
| // Here, A is not a reference type; in fact, it isn't even a type | ||
| const A: object? | ||
| } | ||
|
|
||
| module Y01 { | ||
| import opened X0 | ||
| import opened X1 | ||
|
|
||
| trait B extends A { // error: A is ambiguous | ||
| function GetIndex(): nat | ||
| reads this | ||
| } | ||
| } | ||
|
|
||
| module Y10 { | ||
| import opened X1 | ||
| import opened X0 | ||
|
|
||
| trait B extends A { // error: A is ambiguous | ||
| function GetIndex(): nat | ||
| reads this | ||
| } | ||
| } | ||
|
|
||
| module Y0123 { | ||
| import opened X0 | ||
| import opened X1 | ||
| import opened X2 | ||
|
|
||
| trait B extends A { // error: A is ambiguous | ||
| function GetIndex(): nat | ||
| reads this | ||
| } | ||
| } | ||
|
|
||
| module Y210 { | ||
| import opened X2 | ||
| import opened X1 | ||
| import opened X0 | ||
|
|
||
| trait B extends A { // error: A is ambiguous | ||
| function GetIndex(): nat | ||
| reads this | ||
| } | ||
| } | ||
|
|
||
| module Z { | ||
| import opened X0 | ||
| import opened X1 | ||
| import opened X2 | ||
|
|
||
| } | ||
|
|
||
| module Z1 { | ||
| import opened X0 | ||
| import opened X1 | ||
| import opened X2 | ||
|
|
||
| trait B extends X0.A { // no problem, since X0.A is fully qualified | ||
| function GetIndex(): nat | ||
| reads this // no problem, since B is a reference type | ||
| } | ||
| } | ||
|
|
||
| module Z2 { | ||
| import opened X0 | ||
| import opened X1 | ||
| import opened X2 | ||
|
|
||
| trait B extends X1.A { // no problem, since X1.A is fully qualified | ||
| function GetIndex(): nat | ||
| reads this // error: B is not a reference type | ||
| } | ||
| } |
6 changes: 6 additions & 0 deletions
6
Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4936c.dfy.expect
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,6 @@ | ||
| git-issue-4936c.dfy(32,18): Error: The name A ambiguously refers to a type in one of the modules X0, X1 (try qualifying the type name with the module name) | ||
| git-issue-4936c.dfy(42,18): Error: The name A ambiguously refers to a type in one of the modules X1, X0 (try qualifying the type name with the module name) | ||
| git-issue-4936c.dfy(53,18): Error: The name A ambiguously refers to a type in one of the modules X0, X1 (try qualifying the type name with the module name) | ||
| git-issue-4936c.dfy(64,18): Error: The name A ambiguously refers to a type in one of the modules X1, X0 (try qualifying the type name with the module name) | ||
| git-issue-4936c.dfy(95,12): Error: a reads-clause expression must denote an object, a set/iset/multiset/seq of objects, or a function to a set/iset/multiset/seq of objects (instead got B) | ||
| 5 resolution/type errors detected in git-issue-4936c.dfy |
58 changes: 58 additions & 0 deletions
58
Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4936d.dfy
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,58 @@ | ||
| // RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s" -- --general-traits:datatype | ||
|
|
||
| module X { | ||
| export Public | ||
| provides A | ||
| export Friends | ||
| reveals A | ||
|
|
||
| trait {:termination false} A extends object {} | ||
| } | ||
|
|
||
| module Y0 { | ||
| import opened X`Public | ||
|
|
||
| trait B extends A { // error: A is not even known to be a trait | ||
| function GetIndex(): nat | ||
| reads this | ||
| } | ||
| } | ||
|
|
||
| module Y1 { | ||
| import opened X`Friends | ||
|
|
||
| trait B extends A { | ||
| function GetIndex(): nat | ||
| reads this // fine, since B is known to be a reference type | ||
| } | ||
| } | ||
|
|
||
| module Y2 { | ||
| import opened I = X`Friends | ||
| import opened J = X`Public | ||
|
|
||
| trait B extends A { | ||
| function GetIndex(): nat | ||
| reads this // fine, since B is known to be a reference type | ||
| } | ||
| } | ||
|
|
||
| module Y3 { | ||
| import opened X`Friends | ||
| import opened J = X`Public | ||
|
|
||
| trait B extends J.A { // fine, since the module also imports X`Friends | ||
| function GetIndex(): nat | ||
| reads this // fine, since B is known to be a reference type | ||
| } | ||
| } | ||
|
|
||
| module Y4 { | ||
| import I = X`Friends | ||
| import J = X`Public | ||
|
|
||
| trait B extends J.A { // fine, since the module also imports X`Friends | ||
| function GetIndex(): nat | ||
| reads this // fine, since B is known to be a reference type | ||
| } | ||
| } |
2 changes: 2 additions & 0 deletions
2
Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4936d.dfy.expect
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,2 @@ | ||
| git-issue-4936d.dfy(15,18): Error: a trait can only extend traits (found 'A') | ||
| 1 resolution/type errors detected in git-issue-4936d.dfy |
27 changes: 27 additions & 0 deletions
27
Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4983.dfy
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,27 @@ | ||
| // RUN: %testDafnyForEachResolver --expect-exit-code=2 --refresh-exit-code=0 "%s" -- --general-traits:datatype | ||
|
|
||
| trait Parent {} | ||
|
|
||
| datatype Dt extends Parent = Dt { | ||
| function GetParent(): Parent { | ||
| // The implicit conversion in the following line once caused malformed Boogie to be generated | ||
| this // error (in the legacy resolver): legacy resolver does not understand subtyping relationship with Parent | ||
| } | ||
| } | ||
|
|
||
| function GetDtAsParent(): Parent { | ||
| // The implicit conversion in the following line once caused malformed Boogie to be generated | ||
| Dt // error (in the legacy resolver): legacy resolver does not understand subtyping relationship with Parent | ||
| } | ||
|
|
||
| type Abstract extends Parent { | ||
| function GetParent(): Parent { | ||
| this // error (in the legacy resolver): legacy resolver does not understand subtyping relationship with Parent | ||
| } | ||
| } | ||
|
|
||
| function GetAbstract(): Abstract | ||
|
|
||
| function GetAbstractAsParent(): Parent { | ||
| GetAbstract() // error (in the legacy resolver): legacy resolver does not understand subtyping relationship with Parent | ||
| } |
Oops, something went wrong.