-
Notifications
You must be signed in to change notification settings - Fork 266
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
fix: Omit type antecedents for unassigned variables (#5877)
In let expressions and named function results, the bound variable was previously introduced with an assumption that the variable satisfied its type. That is not sound, since the type may be empty. This PR removes those premature type assumptions. Fixes #1958 <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
b1dda0f
commit e815f23
Showing
11 changed files
with
223 additions
and
20 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
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
2 changes: 1 addition & 1 deletion
2
Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.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 |
|---|---|---|
| @@ -1,4 +1,4 @@ | ||
|
|
||
| Dafny program verifier finished with 272 verified, 0 errors | ||
| Total resources used is 30526126 | ||
| Total resources used is 30525479 | ||
| Max resources used by VC is 2048364 |
2 changes: 1 addition & 1 deletion
2
Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy.refresh.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 |
|---|---|---|
| @@ -1,4 +1,4 @@ | ||
|
|
||
| Dafny program verifier finished with 276 verified, 0 errors | ||
| Total resources used is 28791320 | ||
| Total resources used is 28790607 | ||
| Max resources used by VC is 974212 |
178 changes: 178 additions & 0 deletions
178
Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1958.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,178 @@ | ||
| // RUN: %exits-with 4 %verify --type-system-refresh --general-traits=datatype "%s" > "%t" | ||
| // RUN: %diff "%s.expect" "%t" | ||
|
|
||
| module Example0 { | ||
| datatype BaseType = Ctor(x: int) | ||
| { | ||
| predicate i() | ||
| } | ||
|
|
||
| type R = r: BaseType | r.i() witness * | ||
|
|
||
| function F0(v: nat): R { // anonymous result value | ||
| var o: R := Ctor(v); // error: this BaseType might not be an R | ||
| o | ||
| } | ||
|
|
||
| function F1(v: nat): (r: R) { // named result value | ||
| var o: R := Ctor(v); // error: this BaseType might not be an R | ||
| o | ||
| } | ||
| } | ||
|
|
||
| module Example1 { | ||
| datatype BaseType = Ctor(x: int) | ||
| { | ||
| predicate i() | ||
| } | ||
|
|
||
| type R = r: BaseType | r.i() witness * | ||
|
|
||
| function G0(v: nat): R { // anonymous result value | ||
| Ctor(v) // error: this BaseType might not be an R | ||
| } | ||
|
|
||
| function G1(v: nat): (r: R) { // named result value | ||
| Ctor(v) // error: this BaseType might not be an R | ||
| } | ||
| } | ||
|
|
||
| module Example2 { | ||
| type BaseType(!new) | ||
| { | ||
| predicate i() | ||
| } | ||
|
|
||
| type R = r: BaseType | r.i() witness * | ||
|
|
||
| ghost function Ctor(x: nat): R | ||
| requires exists b: BaseType :: b.i() | ||
| { | ||
| var b: BaseType :| b.i(); | ||
| b | ||
| } | ||
|
|
||
| ghost function F(v: nat): R { | ||
| var o: R := Ctor(v); // error: precondition failure (***) as reported in issue 1958, this was once not reported | ||
| o | ||
| } | ||
|
|
||
| ghost function G0(v: nat): R { // anonymous result value | ||
| Ctor(v) // error: precondition failure | ||
| } | ||
|
|
||
| ghost function G1(v: nat): (r: R) { // named result value | ||
| Ctor(v) // error: precondition failure (***) as reported in issue 1958, this was once not reported | ||
| } | ||
|
|
||
| method MF(v: nat) returns (ghost r: R) { | ||
| ghost var o: R; | ||
| o := Ctor(v); // error: precondition failure | ||
| return o; | ||
| } | ||
|
|
||
| predicate IsR(r: R) { true } | ||
|
|
||
| method AssignSuchThat() { | ||
| var r: R :| IsR(r); // error: cannot establish existence of r | ||
| } | ||
|
|
||
| ghost function LetSuchThat(): R { | ||
| var r: R :| IsR(r); // error: cannot establish existence of r | ||
| r | ||
| } | ||
| } | ||
|
|
||
| module Example3 { | ||
| datatype BaseType = BaseType | ||
| { | ||
| predicate i() { | ||
| false | ||
| } | ||
| } | ||
|
|
||
| type R = r: BaseType | r.i() witness * | ||
|
|
||
| function Ctor(x: nat): R | ||
| requires exists b: BaseType :: b.i() | ||
| { | ||
| var b: BaseType :| b.i(); | ||
| b | ||
| } | ||
|
|
||
| function F(v: nat): R { | ||
| var o: R := Ctor(v); // error: precondition failure (***) as reported in issue 1958, this was once not reported | ||
| o | ||
| } | ||
|
|
||
| method Main() { | ||
| var r := F(15); | ||
| print r, "\n"; | ||
| } | ||
| } | ||
|
|
||
| // The following tests make sure that the appropriate type information (without allocatedness information) is available | ||
| // when checking the _postcondition_ of functions. | ||
| module FunctionResultType { | ||
| datatype Option<X> = None | Some(value: X) | ||
|
|
||
| function Search0<T(==)>(s: seq<T>, x: T): (o: Option<nat>) | ||
| ensures | ||
| o.Some? && o.value < |s| ==> | ||
| s[o.value] == x // in order to prove ".value" is non-negative, the type of "o" is necessary | ||
| { | ||
| if |s| < 12 then | ||
| None | ||
| else if s[9] == x then | ||
| Some(9) | ||
| else if s[2] == x then | ||
| Some(2) | ||
| else | ||
| None | ||
| } | ||
|
|
||
| function Search1<T(==)>(s: seq<T>, x: T): Option<nat> | ||
| ensures var o := Search1(s, x); | ||
| o.Some? && o.value < |s| ==> | ||
| s[o.value] == x // in order to prove ".value" is non-negative, the type of "Search1(s, x)" and "o" is necessary | ||
| { | ||
| if |s| < 12 then | ||
| None | ||
| else if s[9] == x then | ||
| Some(9) | ||
| else if s[2] == x then | ||
| Some(2) | ||
| else | ||
| None | ||
| } | ||
|
|
||
| function Search2<T(==)>(s: seq<T>, x: T): Option<nat> | ||
| ensures | ||
| Search2(s, x).Some? && Search2(s, x).value < |s| ==> | ||
| s[Search2(s, x).value] == x // in order to prove ".value" is non-negative, the type of "Search2(s, x)" is necessary | ||
| { | ||
| if |s| < 12 then | ||
| None | ||
| else if s[9] == x then | ||
| Some(9) | ||
| else if s[2] == x then | ||
| Some(2) | ||
| else | ||
| None | ||
| } | ||
|
|
||
| function Search4<T(==)>(s: seq<T>, x: T): (o: Option<int>) | ||
| ensures | ||
| o.Some? && o.value < |s| ==> | ||
| s[o.value] == x // error: ".value" may be negative | ||
| { | ||
| if |s| < 12 then | ||
| None | ||
| else if s[9] == x then | ||
| Some(9) | ||
| else if s[2] == x then | ||
| Some(2) | ||
| else | ||
| None | ||
| } | ||
| } |
19 changes: 19 additions & 0 deletions
19
Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1958.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,19 @@ | ||
| git-issue-1958.dfy(13,16): Error: value does not satisfy the subset constraints of 'R' | ||
| git-issue-1958.dfy(18,16): Error: value does not satisfy the subset constraints of 'R' | ||
| git-issue-1958.dfy(32,4): Error: value does not satisfy the subset constraints of 'R' | ||
| git-issue-1958.dfy(36,4): Error: value does not satisfy the subset constraints of 'R' | ||
| git-issue-1958.dfy(56,16): Error: function precondition could not be proved | ||
| git-issue-1958.dfy(49,13): Related location: this proposition could not be proved | ||
| git-issue-1958.dfy(61,4): Error: function precondition could not be proved | ||
| git-issue-1958.dfy(49,13): Related location: this proposition could not be proved | ||
| git-issue-1958.dfy(65,4): Error: function precondition could not be proved | ||
| git-issue-1958.dfy(49,13): Related location: this proposition could not be proved | ||
| git-issue-1958.dfy(70,9): Error: function precondition could not be proved | ||
| git-issue-1958.dfy(49,13): Related location: this proposition could not be proved | ||
| git-issue-1958.dfy(77,13): Error: cannot establish the existence of LHS values that satisfy the such-that predicate | ||
| git-issue-1958.dfy(81,4): Error: cannot establish the existence of LHS values that satisfy the such-that predicate | ||
| git-issue-1958.dfy(104,16): Error: function precondition could not be proved | ||
| git-issue-1958.dfy(97,13): Related location: this proposition could not be proved | ||
| git-issue-1958.dfy(167,7): Error: index out of range | ||
|
|
||
| Dafny program verifier finished with 6 verified, 12 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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1 @@ | ||
| Don't assume type information before binding variables (for let expressions and named function results) |