From 3268e9b0ab4899835654a9ea6135bd557c882598 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 19 Oct 2021 15:50:05 -0500 Subject: [PATCH 01/27] Added failing tests. --- Test/git-issues/git-issue-697-test.dfy | 19 +++++++++++++++++++ .../git-issue-697-test.dfy.expected | 5 +++++ Test/git-issues/git-issue-698-test.dfy | 16 ++++++++++++++++ .../git-issue-698-test.dfy.expected | 5 +++++ 4 files changed, 45 insertions(+) create mode 100644 Test/git-issues/git-issue-697-test.dfy create mode 100644 Test/git-issues/git-issue-697-test.dfy.expected create mode 100644 Test/git-issues/git-issue-698-test.dfy create mode 100644 Test/git-issues/git-issue-698-test.dfy.expected diff --git a/Test/git-issues/git-issue-697-test.dfy b/Test/git-issues/git-issue-697-test.dfy new file mode 100644 index 00000000000..8b7505c66e8 --- /dev/null +++ b/Test/git-issues/git-issue-697-test.dfy @@ -0,0 +1,19 @@ +// RUN: %dafny /compile:0 /rprint:"%t.rprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +datatype Cell = Cell(x: int) +type EvenCell = c: Cell | c.x % 2 == 0 witness Cell(0) + +function method doubleEvenCell(c: EvenCell): int + { + if c.x % 2 == 1 then 1/0 else c.x * 2 + } + +method Main() { + var x: set := { Cell(1), Cell(2), Cell(3), Cell(4) }; + var y := set c: EvenCell | c in x; + var b: bool := forall c :: c in y ==> doubleEvenCell(c) > 0; + assert b; + print(b); +} + diff --git a/Test/git-issues/git-issue-697-test.dfy.expected b/Test/git-issues/git-issue-697-test.dfy.expected new file mode 100644 index 00000000000..d26ccf9f366 --- /dev/null +++ b/Test/git-issues/git-issue-697-test.dfy.expected @@ -0,0 +1,5 @@ + +Dafny program verifier finished with 3 verified, 0 errors +Running... + +true \ No newline at end of file diff --git a/Test/git-issues/git-issue-698-test.dfy b/Test/git-issues/git-issue-698-test.dfy new file mode 100644 index 00000000000..2deacfa3218 --- /dev/null +++ b/Test/git-issues/git-issue-698-test.dfy @@ -0,0 +1,16 @@ +// RUN: %dafny /compile:0 /rprint:"%t.rprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +type Small = x: int | 0 <= x < 100 && x != 3 + +function method F(x: int): int + requires x != 3 +{ + if x == 3 then 1/0 else 100 +} + +method Main() { + var b := forall n: Small :: F(n) == 100; + assert b; + print b; +} \ No newline at end of file diff --git a/Test/git-issues/git-issue-698-test.dfy.expected b/Test/git-issues/git-issue-698-test.dfy.expected new file mode 100644 index 00000000000..d26ccf9f366 --- /dev/null +++ b/Test/git-issues/git-issue-698-test.dfy.expected @@ -0,0 +1,5 @@ + +Dafny program verifier finished with 3 verified, 0 errors +Running... + +true \ No newline at end of file From 76b2708e6736b551475b225569ce6c96e146feb4 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 19 Oct 2021 16:26:15 -0500 Subject: [PATCH 02/27] Added failing tests for exists and map --- Test/git-issues/git-issue-697b-test.dfy | 20 +++++++++++++++++++ .../git-issue-697b-test.dfy.expected | 5 +++++ Test/git-issues/git-issue-698b-test.dfy | 16 +++++++++++++++ .../git-issue-698b-test.dfy.expected | 5 +++++ 4 files changed, 46 insertions(+) create mode 100644 Test/git-issues/git-issue-697b-test.dfy create mode 100644 Test/git-issues/git-issue-697b-test.dfy.expected create mode 100644 Test/git-issues/git-issue-698b-test.dfy create mode 100644 Test/git-issues/git-issue-698b-test.dfy.expected diff --git a/Test/git-issues/git-issue-697b-test.dfy b/Test/git-issues/git-issue-697b-test.dfy new file mode 100644 index 00000000000..901d52fa9cd --- /dev/null +++ b/Test/git-issues/git-issue-697b-test.dfy @@ -0,0 +1,20 @@ +// RUN: %dafny /compile:0 /rprint:"%t.rprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +datatype Cell = Cell(x: int) +type EvenCell = c: Cell | c.x % 2 == 0 witness Cell(0) + +function method doubleEvenCell(c: EvenCell): int + { + if c.x % 2 == 1 then 1/0 else c.x * 2 + } + +method Main() { + var x: set := {Cell(1), Cell(2), Cell(3), Cell(4)}; + var z: map := map c: EvenCell | c in x :: c.x; + var y := z.Keys; + var b: bool := forall c :: c in y ==> doubleEvenCell(c) > 0; + assert b; + //print(b); +} + diff --git a/Test/git-issues/git-issue-697b-test.dfy.expected b/Test/git-issues/git-issue-697b-test.dfy.expected new file mode 100644 index 00000000000..d26ccf9f366 --- /dev/null +++ b/Test/git-issues/git-issue-697b-test.dfy.expected @@ -0,0 +1,5 @@ + +Dafny program verifier finished with 3 verified, 0 errors +Running... + +true \ No newline at end of file diff --git a/Test/git-issues/git-issue-698b-test.dfy b/Test/git-issues/git-issue-698b-test.dfy new file mode 100644 index 00000000000..df644aa7097 --- /dev/null +++ b/Test/git-issues/git-issue-698b-test.dfy @@ -0,0 +1,16 @@ +// RUN: %dafny /compile:0 /rprint:"%t.rprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +type Small = x: int | 0 <= x < 100 && x != 3 + +function method F(x: int): int + requires x != 3 +{ + if x == 3 then 1/0 else 100 +} + +method Main() { + var b := !exists n: Small :: F(n) != 100; + assert b; + print b; +} \ No newline at end of file diff --git a/Test/git-issues/git-issue-698b-test.dfy.expected b/Test/git-issues/git-issue-698b-test.dfy.expected new file mode 100644 index 00000000000..d26ccf9f366 --- /dev/null +++ b/Test/git-issues/git-issue-698b-test.dfy.expected @@ -0,0 +1,5 @@ + +Dafny program verifier finished with 3 verified, 0 errors +Running... + +true \ No newline at end of file From d3e1d9bec9e8cf1b4de9e1819c9279e332c27d11 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 19 Oct 2021 16:33:28 -0500 Subject: [PATCH 03/27] Renamed tests for consistency --- Test/git-issues/{git-issue-697-test.dfy => git-issue-697.dfy} | 0 ...git-issue-697-test.dfy.expected => git-issue-697.dfy.expected} | 0 Test/git-issues/{git-issue-697b-test.dfy => git-issue-697b.dfy} | 0 ...t-issue-697b-test.dfy.expected => git-issue-697b.dfy.expected} | 0 Test/git-issues/{git-issue-698-test.dfy => git-issue-698.dfy} | 0 ...git-issue-698-test.dfy.expected => git-issue-698.dfy.expected} | 0 Test/git-issues/{git-issue-698b-test.dfy => git-issue-698b.dfy} | 0 ...t-issue-698b-test.dfy.expected => git-issue-698b.dfy.expected} | 0 8 files changed, 0 insertions(+), 0 deletions(-) rename Test/git-issues/{git-issue-697-test.dfy => git-issue-697.dfy} (100%) rename Test/git-issues/{git-issue-697-test.dfy.expected => git-issue-697.dfy.expected} (100%) rename Test/git-issues/{git-issue-697b-test.dfy => git-issue-697b.dfy} (100%) rename Test/git-issues/{git-issue-697b-test.dfy.expected => git-issue-697b.dfy.expected} (100%) rename Test/git-issues/{git-issue-698-test.dfy => git-issue-698.dfy} (100%) rename Test/git-issues/{git-issue-698-test.dfy.expected => git-issue-698.dfy.expected} (100%) rename Test/git-issues/{git-issue-698b-test.dfy => git-issue-698b.dfy} (100%) rename Test/git-issues/{git-issue-698b-test.dfy.expected => git-issue-698b.dfy.expected} (100%) diff --git a/Test/git-issues/git-issue-697-test.dfy b/Test/git-issues/git-issue-697.dfy similarity index 100% rename from Test/git-issues/git-issue-697-test.dfy rename to Test/git-issues/git-issue-697.dfy diff --git a/Test/git-issues/git-issue-697-test.dfy.expected b/Test/git-issues/git-issue-697.dfy.expected similarity index 100% rename from Test/git-issues/git-issue-697-test.dfy.expected rename to Test/git-issues/git-issue-697.dfy.expected diff --git a/Test/git-issues/git-issue-697b-test.dfy b/Test/git-issues/git-issue-697b.dfy similarity index 100% rename from Test/git-issues/git-issue-697b-test.dfy rename to Test/git-issues/git-issue-697b.dfy diff --git a/Test/git-issues/git-issue-697b-test.dfy.expected b/Test/git-issues/git-issue-697b.dfy.expected similarity index 100% rename from Test/git-issues/git-issue-697b-test.dfy.expected rename to Test/git-issues/git-issue-697b.dfy.expected diff --git a/Test/git-issues/git-issue-698-test.dfy b/Test/git-issues/git-issue-698.dfy similarity index 100% rename from Test/git-issues/git-issue-698-test.dfy rename to Test/git-issues/git-issue-698.dfy diff --git a/Test/git-issues/git-issue-698-test.dfy.expected b/Test/git-issues/git-issue-698.dfy.expected similarity index 100% rename from Test/git-issues/git-issue-698-test.dfy.expected rename to Test/git-issues/git-issue-698.dfy.expected diff --git a/Test/git-issues/git-issue-698b-test.dfy b/Test/git-issues/git-issue-698b.dfy similarity index 100% rename from Test/git-issues/git-issue-698b-test.dfy rename to Test/git-issues/git-issue-698b.dfy diff --git a/Test/git-issues/git-issue-698b-test.dfy.expected b/Test/git-issues/git-issue-698b.dfy.expected similarity index 100% rename from Test/git-issues/git-issue-698b-test.dfy.expected rename to Test/git-issues/git-issue-698b.dfy.expected From 83075e60e36fb788e01de65a9c9d9ba17decd78b Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 21 Oct 2021 14:55:59 -0500 Subject: [PATCH 04/27] Changed compilation parameter for tests --- Test/git-issues/git-issue-697.dfy | 8 ++++---- Test/git-issues/git-issue-697b.dfy | 2 +- Test/git-issues/git-issue-698.dfy | 2 +- Test/git-issues/git-issue-698b.dfy | 2 +- 4 files changed, 7 insertions(+), 7 deletions(-) diff --git a/Test/git-issues/git-issue-697.dfy b/Test/git-issues/git-issue-697.dfy index 8b7505c66e8..facdb410cff 100644 --- a/Test/git-issues/git-issue-697.dfy +++ b/Test/git-issues/git-issue-697.dfy @@ -1,13 +1,13 @@ -// RUN: %dafny /compile:0 /rprint:"%t.rprint" "%s" > "%t" +// RUN: %dafny /compile:3 /rprint:"%t.rprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" datatype Cell = Cell(x: int) type EvenCell = c: Cell | c.x % 2 == 0 witness Cell(0) function method doubleEvenCell(c: EvenCell): int - { - if c.x % 2 == 1 then 1/0 else c.x * 2 - } +{ + if c.x % 2 == 1 then 1/0 else c.x * 2 / 0 +} method Main() { var x: set := { Cell(1), Cell(2), Cell(3), Cell(4) }; diff --git a/Test/git-issues/git-issue-697b.dfy b/Test/git-issues/git-issue-697b.dfy index 901d52fa9cd..e4d91a8b455 100644 --- a/Test/git-issues/git-issue-697b.dfy +++ b/Test/git-issues/git-issue-697b.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /rprint:"%t.rprint" "%s" > "%t" +// RUN: %dafny /compile:3 /rprint:"%t.rprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" datatype Cell = Cell(x: int) diff --git a/Test/git-issues/git-issue-698.dfy b/Test/git-issues/git-issue-698.dfy index 2deacfa3218..62f4fb71dbd 100644 --- a/Test/git-issues/git-issue-698.dfy +++ b/Test/git-issues/git-issue-698.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /rprint:"%t.rprint" "%s" > "%t" +// RUN: %dafny /compile:3 /rprint:"%t.rprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" type Small = x: int | 0 <= x < 100 && x != 3 diff --git a/Test/git-issues/git-issue-698b.dfy b/Test/git-issues/git-issue-698b.dfy index df644aa7097..abdd4151149 100644 --- a/Test/git-issues/git-issue-698b.dfy +++ b/Test/git-issues/git-issue-698b.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /rprint:"%t.rprint" "%s" > "%t" +// RUN: %dafny /compile:3 /rprint:"%t.rprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" type Small = x: int | 0 <= x < 100 && x != 3 From 0e8cdf81de9635af8e59868b0dd6de8bdb9d0b6f Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Mon, 25 Oct 2021 11:58:14 -0500 Subject: [PATCH 05/27] Better test files --- Test/git-issues/git-issue-697.dfy | 2 +- ....dfy.expected => git-issue-697.dfy.expect} | 2 -- ...dfy.expected => git-issue-697b.dfy.expect} | 2 -- Test/git-issues/git-issue-697c.dfy | 23 +++++++++++++++++++ Test/git-issues/git-issue-697c.dfy.expect | 3 +++ Test/git-issues/git-issue-697d.dfy | 23 +++++++++++++++++++ ...dfy.expected => git-issue-697d.dfy.expect} | 2 -- ....dfy.expected => git-issue-698.dfy.expect} | 2 -- Test/git-issues/git-issue-698b.dfy.expect | 3 +++ 9 files changed, 53 insertions(+), 9 deletions(-) rename Test/git-issues/{git-issue-697.dfy.expected => git-issue-697.dfy.expect} (84%) rename Test/git-issues/{git-issue-697b.dfy.expected => git-issue-697b.dfy.expect} (84%) create mode 100644 Test/git-issues/git-issue-697c.dfy create mode 100644 Test/git-issues/git-issue-697c.dfy.expect create mode 100644 Test/git-issues/git-issue-697d.dfy rename Test/git-issues/{git-issue-698.dfy.expected => git-issue-697d.dfy.expect} (84%) rename Test/git-issues/{git-issue-698b.dfy.expected => git-issue-698.dfy.expect} (84%) create mode 100644 Test/git-issues/git-issue-698b.dfy.expect diff --git a/Test/git-issues/git-issue-697.dfy b/Test/git-issues/git-issue-697.dfy index facdb410cff..eb6f9fafef7 100644 --- a/Test/git-issues/git-issue-697.dfy +++ b/Test/git-issues/git-issue-697.dfy @@ -6,7 +6,7 @@ type EvenCell = c: Cell | c.x % 2 == 0 witness Cell(0) function method doubleEvenCell(c: EvenCell): int { - if c.x % 2 == 1 then 1/0 else c.x * 2 / 0 + if c.x % 2 == 1 then 1/0 else c.x * 2 } method Main() { diff --git a/Test/git-issues/git-issue-697.dfy.expected b/Test/git-issues/git-issue-697.dfy.expect similarity index 84% rename from Test/git-issues/git-issue-697.dfy.expected rename to Test/git-issues/git-issue-697.dfy.expect index d26ccf9f366..188a72ebc36 100644 --- a/Test/git-issues/git-issue-697.dfy.expected +++ b/Test/git-issues/git-issue-697.dfy.expect @@ -1,5 +1,3 @@ Dafny program verifier finished with 3 verified, 0 errors -Running... - true \ No newline at end of file diff --git a/Test/git-issues/git-issue-697b.dfy.expected b/Test/git-issues/git-issue-697b.dfy.expect similarity index 84% rename from Test/git-issues/git-issue-697b.dfy.expected rename to Test/git-issues/git-issue-697b.dfy.expect index d26ccf9f366..188a72ebc36 100644 --- a/Test/git-issues/git-issue-697b.dfy.expected +++ b/Test/git-issues/git-issue-697b.dfy.expect @@ -1,5 +1,3 @@ Dafny program verifier finished with 3 verified, 0 errors -Running... - true \ No newline at end of file diff --git a/Test/git-issues/git-issue-697c.dfy b/Test/git-issues/git-issue-697c.dfy new file mode 100644 index 00000000000..4d8c4d95aad --- /dev/null +++ b/Test/git-issues/git-issue-697c.dfy @@ -0,0 +1,23 @@ +// RUN: %dafny /compile:3 /rprint:"%t.rprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function ghostPredicate(x: int): bool { + x % 2 == 0 +} + +datatype Cell = Cell(x: int) +type EvenCell = c: Cell | ghostPredicate(c.x) witness Cell(0) + +function method doubleEvenCell(c: EvenCell): int +{ + if c.x % 2 == 1 then 1/0 else c.x * 2 +} + +method Main() { + var x: set := { Cell(1), Cell(2), Cell(3), Cell(4) }; + var y := set c: EvenCell | c in x; + var b: bool := forall c :: c in y ==> doubleEvenCell(c) > 0; + assert b; + print(b); +} + diff --git a/Test/git-issues/git-issue-697c.dfy.expect b/Test/git-issues/git-issue-697c.dfy.expect new file mode 100644 index 00000000000..24a1f33600c --- /dev/null +++ b/Test/git-issues/git-issue-697c.dfy.expect @@ -0,0 +1,3 @@ + +Dafny program verifier finished with 2 verified, 1 errors +true \ No newline at end of file diff --git a/Test/git-issues/git-issue-697d.dfy b/Test/git-issues/git-issue-697d.dfy new file mode 100644 index 00000000000..e9c28c171dc --- /dev/null +++ b/Test/git-issues/git-issue-697d.dfy @@ -0,0 +1,23 @@ +// RUN: %dafny /compile:3 /rprint:"%t.rprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function method nonGhostPredicate(x: int): bool { + x % 2 == 0 +} + +datatype Cell = Cell(x: int) +type EvenCell = c: Cell | nonGhostPredicate(c.x) witness Cell(0) + +function method doubleEvenCell(c: EvenCell): int +{ + if c.x % 2 == 1 then 1/0 else c.x * 2 +} + +method Main() { + var x: set := { Cell(1), Cell(2), Cell(3), Cell(4) }; + var y := set c: EvenCell | c in x; + var b: bool := forall c :: c in y ==> doubleEvenCell(c) > 0; + assert b; + print(b); +} + diff --git a/Test/git-issues/git-issue-698.dfy.expected b/Test/git-issues/git-issue-697d.dfy.expect similarity index 84% rename from Test/git-issues/git-issue-698.dfy.expected rename to Test/git-issues/git-issue-697d.dfy.expect index d26ccf9f366..188a72ebc36 100644 --- a/Test/git-issues/git-issue-698.dfy.expected +++ b/Test/git-issues/git-issue-697d.dfy.expect @@ -1,5 +1,3 @@ Dafny program verifier finished with 3 verified, 0 errors -Running... - true \ No newline at end of file diff --git a/Test/git-issues/git-issue-698b.dfy.expected b/Test/git-issues/git-issue-698.dfy.expect similarity index 84% rename from Test/git-issues/git-issue-698b.dfy.expected rename to Test/git-issues/git-issue-698.dfy.expect index d26ccf9f366..188a72ebc36 100644 --- a/Test/git-issues/git-issue-698b.dfy.expected +++ b/Test/git-issues/git-issue-698.dfy.expect @@ -1,5 +1,3 @@ Dafny program verifier finished with 3 verified, 0 errors -Running... - true \ No newline at end of file diff --git a/Test/git-issues/git-issue-698b.dfy.expect b/Test/git-issues/git-issue-698b.dfy.expect new file mode 100644 index 00000000000..188a72ebc36 --- /dev/null +++ b/Test/git-issues/git-issue-698b.dfy.expect @@ -0,0 +1,3 @@ + +Dafny program verifier finished with 3 verified, 0 errors +true \ No newline at end of file From 2c9aead408308605c5f77388dfe926f4437c8ba3 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Mon, 25 Oct 2021 11:59:20 -0500 Subject: [PATCH 06/27] WIP: Ensuring subset onstraints are compiled --- Source/Dafny/AST/DafnyAst.cs | 1 + Source/Dafny/Compilers/Compiler.cs | 45 ++- Source/Dafny/Resolver.cs | 492 +++-------------------------- Source/Dafny/Util.cs | 438 +++++++++++++++++++++++++ 4 files changed, 514 insertions(+), 462 deletions(-) diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/DafnyAst.cs index c2bde2f0c1c..0eccbd69c3c 100644 --- a/Source/Dafny/AST/DafnyAst.cs +++ b/Source/Dafny/AST/DafnyAst.cs @@ -5695,6 +5695,7 @@ public class SubsetTypeDecl : TypeSynonymDecl, RedirectingTypeDecl { public enum WKind { CompiledZero, Compiled, Ghost, OptOut, Special } public readonly SubsetTypeDecl.WKind WitnessKind; public readonly Expression/*?*/ Witness; // non-null iff WitnessKind is Compiled or Ghost + public bool ConstraintIsCompilable = false; // Will be resolved later. public SubsetTypeDecl(IToken tok, string name, TypeParameter.TypeParameterCharacteristics characteristics, List typeArgs, ModuleDefinition module, BoundVar id, Expression constraint, WKind witnessKind, Expression witness, Attributes attributes) diff --git a/Source/Dafny/Compilers/Compiler.cs b/Source/Dafny/Compilers/Compiler.cs index 284e8da3510..160b8fbc5c9 100644 --- a/Source/Dafny/Compilers/Compiler.cs +++ b/Source/Dafny/Compilers/Compiler.cs @@ -4616,8 +4616,7 @@ void writeObj(ConcreteSyntaxTree w) { } TrExpr(logicalBody, wBody, true); - } else if (expr is SetComprehension) { - var e = (SetComprehension)expr; + } else if (expr is SetComprehension setComprehension) { // For "set i,j,k,l | R(i,j,k,l) :: Term(i,j,k,l)" where the term has type "G", emit something like: // ((System.Func>)(() => { // var _coll = new List(); @@ -4634,29 +4633,47 @@ void writeObj(ConcreteSyntaxTree w) { // } // return Dafny.Set.FromCollection(_coll); // }))() - wr = CaptureFreeVariables(e, true, out var su, inLetExprBody, wr); - e = (SetComprehension)su.Substitute(e); + wr = CaptureFreeVariables(setComprehension, true, out var su, inLetExprBody, wr); + setComprehension = (SetComprehension)su.Substitute(setComprehension); - Contract.Assert(e.Bounds != null); // the resolver would have insisted on finding bounds + Contract.Assert(setComprehension.Bounds != null); // the resolver would have insisted on finding bounds var collectionName = idGenerator.FreshId("_coll"); - var bwr = CreateIIFE0(e.Type.AsSetType, e.tok, wr); + var bwr = CreateIIFE0(setComprehension.Type.AsSetType, setComprehension.tok, wr); wr = bwr; - EmitSetBuilder_New(wr, e, collectionName); - var n = e.BoundVars.Count; - Contract.Assert(e.Bounds.Count == n); + EmitSetBuilder_New(wr, setComprehension, collectionName); + var n = setComprehension.BoundVars.Count; + Contract.Assert(setComprehension.Bounds.Count == n); for (var i = 0; i < n; i++) { - var bound = e.Bounds[i]; - var bv = e.BoundVars[i]; + var bound = setComprehension.Bounds[i]; + var bv = setComprehension.BoundVars[i]; ConcreteSyntaxTree collectionWriter; var tmpVar = idGenerator.FreshId("_compr_"); wr = CreateForeachLoop(tmpVar, GetCollectionEnumerationType(bound, bv), IdName(bv), bv.Type, true, bv.tok, out collectionWriter, wr); + if (bv.Type is UserDefinedType userDefinedType) { + // TODO: What about types built with subset types? And subset types that have type parameters? + // var s = {List(Cell(1)), List(Cell(2), Cell(4)), List(Cell(2), Cell(3))}; + // set x: List | x in s + if (userDefinedType.ResolvedClass is SubsetTypeDecl subsetTypeDecl) { + if (subsetTypeDecl.Constraint != null && subsetTypeDecl.ConstraintIsCompilable) { + var bvIdentifier = new IdentifierExpr(setComprehension.tok, bv); + wr = EmitIf(out var guardWriterInner, false, wr); + var subContract = new Substituter(null, + new Dictionary() { + {subsetTypeDecl.Var, bvIdentifier} + }, + null); + var contraintInContext = subContract.Substitute(subsetTypeDecl.Constraint); + TrExpr(contraintInContext, guardWriterInner, inLetExprBody); + } + } + } CompileCollection(bound, bv, inLetExprBody, true, null, collectionWriter); } ConcreteSyntaxTree guardWriter; var thn = EmitIf(out guardWriter, false, wr); - TrExpr(e.Range, guardWriter, inLetExprBody); - EmitSetBuilder_Add(e.Type.AsSetType, collectionName, e.Term, inLetExprBody, thn); - var s = GetCollectionBuilder_Build(e.Type.AsSetType, e.tok, collectionName, wr); + TrExpr(setComprehension.Range, guardWriter, inLetExprBody); + EmitSetBuilder_Add(setComprehension.Type.AsSetType, collectionName, setComprehension.Term, inLetExprBody, thn); + var s = GetCollectionBuilder_Build(setComprehension.Type.AsSetType, setComprehension.tok, collectionName, wr); EmitReturnExpr(s, bwr); } else if (expr is MapComprehension) { diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 66164d7f3e5..c60d1d17144 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -22,6 +22,10 @@ public class Resolver { ErrorReporter reporter; ModuleSignature moduleInfo = null; + public ErrorReporter getReporter() { + return reporter; + } + private bool RevealedInScope(Declaration d) { Contract.Requires(d != null); Contract.Requires(moduleInfo != null); @@ -2718,7 +2722,7 @@ public void ResolveTopLevelDecls_Core(List/*!*/ declarations, if (member is ConstantField field && field.Rhs != null) { CheckTypeInference(field.Rhs, field); if (!field.IsGhost) { - CheckIsCompilable(field.Rhs, field); + ExpressionTester.CheckIsCompilable(this, field.Rhs, field); } } } @@ -2743,7 +2747,7 @@ public void ResolveTopLevelDecls_Core(List/*!*/ declarations, CheckTypeInference(dd.Witness, dd); } if (reporter.Count(ErrorLevel.Error) == prevErrCnt && dd.WitnessKind == SubsetTypeDecl.WKind.Compiled) { - CheckIsCompilable(dd.Witness, codeContext); + ExpressionTester.CheckIsCompilable(this, dd.Witness, codeContext); } } if (d is TopLevelDeclWithMembers dm) { @@ -3516,7 +3520,7 @@ private void ResolveClassMembers_Pass1(TopLevelDeclWithMembers cl) { ResolveParameterDefaultValues_Pass1(f.Formals, f); if (f.ByMethodBody == null) { if (!f.IsGhost && f.Body != null) { - CheckIsCompilable(f.Body, f); + ExpressionTester.CheckIsCompilable(this, f.Body, f); } if (f.Body != null) { DetermineTailRecursion(f); @@ -3544,7 +3548,7 @@ void ResolveParameterDefaultValues_Pass1(List formals, ICodeContext code foreach (var formal in formals.Where(f => f.DefaultValue != null)) { if ((!codeContext.IsGhost || codeContext is DatatypeDecl) && !formal.IsGhost) { - CheckIsCompilable(formal.DefaultValue, codeContext); + ExpressionTester.CheckIsCompilable(this, formal.DefaultValue, codeContext); } CheckExpression(formal.DefaultValue, this, codeContext); } @@ -6626,13 +6630,21 @@ protected override void VisitOneExpr(Expression expr) { string what = null; Expression whereToLookForBounds = null; var polarity = true; - if (e is QuantifierExpr) { + if (e is QuantifierExpr quantifierExpr) { what = "quantifier"; - whereToLookForBounds = ((QuantifierExpr)e).LogicalBody(); - polarity = e is ExistsExpr; - } else if (e is SetComprehension) { + whereToLookForBounds = quantifierExpr.LogicalBody(); + polarity = quantifierExpr is ExistsExpr; + } else if (e is SetComprehension setComprehension) { what = "set comprehension"; - whereToLookForBounds = e.Range; + whereToLookForBounds = setComprehension.Range; + var setType = setComprehension.Type as SetType; + var argType = setType.Arg; + if (argType is UserDefinedType userDefinedType) { + if (userDefinedType.ResolvedClass is SubsetTypeDecl subsetTypeDecl) { + subsetTypeDecl.ConstraintIsCompilable = + ExpressionTester.CheckIsCompilable(null, subsetTypeDecl.Constraint, codeContext); + } + } } else if (e is MapComprehension) { what = "map comprehension"; whereToLookForBounds = e.Range; @@ -8359,10 +8371,10 @@ public void Visit(Statement stmt, bool mustBeErasable) { if (mustBeErasable) { Error(stmt, "expect statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)"); } else { - resolver.CheckIsCompilable(s.Expr, codeContext); + ExpressionTester.CheckIsCompilable(resolver, s.Expr, codeContext); // If not provided, the message is populated with a default value in resolution Contract.Assert(s.Message != null); - resolver.CheckIsCompilable(s.Message, codeContext); + ExpressionTester.CheckIsCompilable(resolver, s.Message, codeContext); } } else if (stmt is PrintStmt) { @@ -8370,7 +8382,7 @@ public void Visit(Statement stmt, bool mustBeErasable) { if (mustBeErasable) { Error(stmt, "print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)"); } else { - s.Args.Iter(ee => resolver.CheckIsCompilable(ee, codeContext)); + s.Args.Iter(ee => ExpressionTester.CheckIsCompilable(resolver, ee, codeContext)); } } else if (stmt is RevealStmt) { @@ -8405,7 +8417,7 @@ public void Visit(Statement stmt, bool mustBeErasable) { Error(lhs, "cannot assign to {0} in a ghost context", AssignStmt.NonGhostKind_To_String(gk)); } } - } else if (!mustBeErasable && s.AssumeToken == null && resolver.UsesSpecFeatures(s.Expr)) { + } else if (!mustBeErasable && s.AssumeToken == null && ExpressionTester.UsesSpecFeatures(s.Expr)) { foreach (var lhs in s.Lhss) { var gk = AssignStmt.LhsIsToGhost_Which(lhs); if (gk != AssignStmt.NonGhostKind.IsGhost) { @@ -8448,13 +8460,13 @@ public void Visit(Statement stmt, bool mustBeErasable) { if (s.HasGhostModifier || mustBeErasable) { s.IsGhost = s.LocalVars.All(v => v.IsGhost); } else { - var spec = resolver.UsesSpecFeatures(s.RHS); + var spec = ExpressionTester.UsesSpecFeatures(s.RHS); if (spec) { foreach (var local in s.LocalVars) { local.MakeGhost(); } } else { - resolver.CheckIsCompilable(s.RHS, codeContext); + ExpressionTester.CheckIsCompilable(resolver, s.RHS, codeContext); } s.IsGhost = spec; } @@ -8466,7 +8478,7 @@ public void Visit(Statement stmt, bool mustBeErasable) { // Make an auto-ghost variable a ghost if the RHS is a ghost if (lhs.Resolved is AutoGhostIdentifierExpr && s.Rhs is ExprRhs) { var rhs = (ExprRhs)s.Rhs; - if (resolver.UsesSpecFeatures(rhs.Expr)) { + if (ExpressionTester.UsesSpecFeatures(rhs.Expr)) { var autoGhostIdExpr = (AutoGhostIdentifierExpr)lhs.Resolved; autoGhostIdExpr.Var.MakeGhost(); } @@ -8486,33 +8498,33 @@ public void Visit(Statement stmt, bool mustBeErasable) { } else { if (gk == AssignStmt.NonGhostKind.Field) { var mse = (MemberSelectExpr)lhs; - resolver.CheckIsCompilable(mse.Obj, codeContext); + ExpressionTester.CheckIsCompilable(resolver, mse.Obj, codeContext); } else if (gk == AssignStmt.NonGhostKind.ArrayElement) { - resolver.CheckIsCompilable(lhs, codeContext); + ExpressionTester.CheckIsCompilable(resolver, lhs, codeContext); } if (s.Rhs is ExprRhs) { var rhs = (ExprRhs)s.Rhs; if (!AssignStmt.LhsIsToGhost(lhs)) { - resolver.CheckIsCompilable(rhs.Expr, codeContext); + ExpressionTester.CheckIsCompilable(resolver, rhs.Expr, codeContext); } } else if (s.Rhs is HavocRhs) { // cool } else { var rhs = (TypeRhs)s.Rhs; if (rhs.ArrayDimensions != null) { - rhs.ArrayDimensions.ForEach(ee => resolver.CheckIsCompilable(ee, codeContext)); + rhs.ArrayDimensions.ForEach(ee => ExpressionTester.CheckIsCompilable(resolver, ee, codeContext)); if (rhs.ElementInit != null) { resolver.CheckIsCompilable(rhs.ElementInit, codeContext); } if (rhs.InitDisplay != null) { - rhs.InitDisplay.ForEach(ee => resolver.CheckIsCompilable(ee, codeContext)); + rhs.InitDisplay.ForEach(ee => ExpressionTester.CheckIsCompilable(resolver, ee, codeContext)); } } if (rhs.InitCall != null) { for (var i = 0; i < rhs.InitCall.Args.Count; i++) { if (!rhs.InitCall.Method.Ins[i].IsGhost) { - resolver.CheckIsCompilable(rhs.InitCall.Args[i], codeContext); + ExpressionTester.CheckIsCompilable(resolver, rhs.InitCall.Args[i], codeContext); } } } @@ -8532,12 +8544,12 @@ public void Visit(Statement stmt, bool mustBeErasable) { } else { int j; if (!callee.IsGhost) { - resolver.CheckIsCompilable(s.Receiver, codeContext); + ExpressionTester.CheckIsCompilable(resolver, s.Receiver, codeContext); j = 0; foreach (var e in s.Args) { Contract.Assume(j < callee.Ins.Count); // this should have already been checked by the resolver if (!callee.Ins[j].IsGhost) { - resolver.CheckIsCompilable(e, codeContext); + ExpressionTester.CheckIsCompilable(resolver, e, codeContext); } j++; } @@ -8579,7 +8591,7 @@ public void Visit(Statement stmt, bool mustBeErasable) { } else if (stmt is IfStmt) { var s = (IfStmt)stmt; - s.IsGhost = mustBeErasable || (s.Guard != null && resolver.UsesSpecFeatures(s.Guard)); + s.IsGhost = mustBeErasable || (s.Guard != null && ExpressionTester.UsesSpecFeatures(s.Guard)); if (!mustBeErasable && s.IsGhost) { resolver.reporter.Info(MessageSource.Resolver, s.Tok, "ghost if"); } @@ -8592,7 +8604,7 @@ public void Visit(Statement stmt, bool mustBeErasable) { } else if (stmt is AlternativeStmt) { var s = (AlternativeStmt)stmt; - s.IsGhost = mustBeErasable || s.Alternatives.Exists(alt => resolver.UsesSpecFeatures(alt.Guard)); + s.IsGhost = mustBeErasable || s.Alternatives.Exists(alt => ExpressionTester.UsesSpecFeatures(alt.Guard)); if (!mustBeErasable && s.IsGhost) { resolver.reporter.Info(MessageSource.Resolver, s.Tok, "ghost if"); } @@ -8601,7 +8613,7 @@ public void Visit(Statement stmt, bool mustBeErasable) { } else if (stmt is WhileStmt) { var s = (WhileStmt)stmt; - s.IsGhost = mustBeErasable || (s.Guard != null && resolver.UsesSpecFeatures(s.Guard)); + s.IsGhost = mustBeErasable || (s.Guard != null && ExpressionTester.UsesSpecFeatures(s.Guard)); if (!mustBeErasable && s.IsGhost) { resolver.reporter.Info(MessageSource.Resolver, s.Tok, "ghost while"); } @@ -8620,7 +8632,7 @@ public void Visit(Statement stmt, bool mustBeErasable) { } else if (stmt is AlternativeLoopStmt) { var s = (AlternativeLoopStmt)stmt; - s.IsGhost = mustBeErasable || s.Alternatives.Exists(alt => resolver.UsesSpecFeatures(alt.Guard)); + s.IsGhost = mustBeErasable || s.Alternatives.Exists(alt => ExpressionTester.UsesSpecFeatures(alt.Guard)); if (!mustBeErasable && s.IsGhost) { resolver.reporter.Info(MessageSource.Resolver, s.Tok, "ghost while"); } @@ -8635,7 +8647,7 @@ public void Visit(Statement stmt, bool mustBeErasable) { } else if (stmt is ForLoopStmt) { var s = (ForLoopStmt)stmt; - s.IsGhost = mustBeErasable || resolver.UsesSpecFeatures(s.Start) || (s.End != null && resolver.UsesSpecFeatures(s.End)); + s.IsGhost = mustBeErasable || ExpressionTester.UsesSpecFeatures(s.Start) || (s.End != null && ExpressionTester.UsesSpecFeatures(s.End)); if (!mustBeErasable && s.IsGhost) { resolver.reporter.Info(MessageSource.Resolver, s.Tok, "ghost for-loop"); } @@ -8658,7 +8670,7 @@ public void Visit(Statement stmt, bool mustBeErasable) { } else if (stmt is ForallStmt) { var s = (ForallStmt)stmt; - s.IsGhost = mustBeErasable || s.Kind != ForallStmt.BodyKind.Assign || resolver.UsesSpecFeatures(s.Range); + s.IsGhost = mustBeErasable || s.Kind != ForallStmt.BodyKind.Assign || ExpressionTester.UsesSpecFeatures(s.Range); if (s.Body != null) { Visit(s.Body, s.IsGhost); } @@ -8693,7 +8705,7 @@ public void Visit(Statement stmt, bool mustBeErasable) { } else if (stmt is MatchStmt) { var s = (MatchStmt)stmt; - s.IsGhost = mustBeErasable || resolver.UsesSpecFeatures(s.Source); + s.IsGhost = mustBeErasable || ExpressionTester.UsesSpecFeatures(s.Source); if (!mustBeErasable && s.IsGhost) { resolver.reporter.Info(MessageSource.Resolver, s.Tok, "ghost match"); } @@ -17027,196 +17039,6 @@ public static string GhostPrefix(bool isGhost) { return isGhost ? "ghost " : ""; } - /// - /// Try to make "expr" compilable (in particular, mark LHSs of a let-expression as ghosts if - /// the corresponding RHS is ghost), and then report errors for every part that would prevent - /// compilation. - /// Requires "expr" to have been successfully resolved. - /// - void CheckIsCompilable(Expression expr, ICodeContext codeContext) { - Contract.Requires(expr != null); - Contract.Requires(expr.WasResolved()); // this check approximates the requirement that "expr" be resolved - Contract.Requires(codeContext != null); - - if (expr is IdentifierExpr) { - var e = (IdentifierExpr)expr; - if (e.Var != null && e.Var.IsGhost) { - reporter.Error(MessageSource.Resolver, expr, "ghost variables are allowed only in specification contexts"); - return; - } - - } else if (expr is MemberSelectExpr) { - var e = (MemberSelectExpr)expr; - if (e.Member != null && e.Member.IsGhost) { - reporter.Error(MessageSource.Resolver, expr, "ghost fields are allowed only in specification contexts"); - return; - } - - } else if (expr is FunctionCallExpr) { - var e = (FunctionCallExpr)expr; - if (e.Function != null) { - if (e.Function.IsGhost) { - string msg; - if (e.Function is TwoStateFunction || e.Function is ExtremePredicate || e.Function is PrefixPredicate) { - msg = $"a call to a {e.Function.WhatKind} is allowed only in specification contexts"; - } else if (e.Function is Predicate) { - msg = "predicate calls are allowed only in specification contexts (consider declaring the predicate a 'predicate method')"; - } else { - msg = "function calls are allowed only in specification contexts (consider declaring the function a 'function method')"; - } - reporter.Error(MessageSource.Resolver, expr, msg); - return; - } - if (e.Function.ByMethodBody != null) { - Contract.Assert(e.Function.ByMethodDecl != null); // we expect .ByMethodDecl to have been filled in by now - // this call will really go to the method part of the function-by-method, so add that edge to the call graph - AddCallGraphEdge(codeContext, e.Function.ByMethodDecl, e, false); - e.IsByMethodCall = true; - } - // function is okay, so check all NON-ghost arguments - CheckIsCompilable(e.Receiver, codeContext); - for (int i = 0; i < e.Function.Formals.Count; i++) { - if (!e.Function.Formals[i].IsGhost) { - CheckIsCompilable(e.Args[i], codeContext); - } - } - } - return; - - } else if (expr is DatatypeValue) { - var e = (DatatypeValue)expr; - // check all NON-ghost arguments - // note that if resolution is successful, then |e.Arguments| == |e.Ctor.Formals| - for (int i = 0; i < e.Arguments.Count; i++) { - if (!e.Ctor.Formals[i].IsGhost) { - CheckIsCompilable(e.Arguments[i], codeContext); - } - } - return; - - } else if (expr is OldExpr) { - reporter.Error(MessageSource.Resolver, expr, "old expressions are allowed only in specification and ghost contexts"); - return; - - } else if (expr is TypeTestExpr) { - var e = (TypeTestExpr)expr; - if (!IsTypeTestCompilable(e)) { - reporter.Error(MessageSource.Resolver, expr, $"an expression of type '{e.E.Type}' is not run-time checkable to be a '{e.ToType}'"); - return; - } - - } else if (expr is FreshExpr) { - reporter.Error(MessageSource.Resolver, expr, "fresh expressions are allowed only in specification and ghost contexts"); - return; - - } else if (expr is UnchangedExpr) { - reporter.Error(MessageSource.Resolver, expr, "unchanged expressions are allowed only in specification and ghost contexts"); - return; - - } else if (expr is StmtExpr) { - var e = (StmtExpr)expr; - // ignore the statement - CheckIsCompilable(e.E, codeContext); - return; - - } else if (expr is BinaryExpr) { - var e = (BinaryExpr)expr; - switch (e.ResolvedOp_PossiblyStillUndetermined) { - case BinaryExpr.ResolvedOpcode.RankGt: - case BinaryExpr.ResolvedOpcode.RankLt: - reporter.Error(MessageSource.Resolver, expr, "rank comparisons are allowed only in specification and ghost contexts"); - return; - default: - break; - } - - } else if (expr is TernaryExpr) { - var e = (TernaryExpr)expr; - switch (e.Op) { - case TernaryExpr.Opcode.PrefixEqOp: - case TernaryExpr.Opcode.PrefixNeqOp: - reporter.Error(MessageSource.Resolver, expr, "prefix equalities are allowed only in specification and ghost contexts"); - return; - default: - break; - } - } else if (expr is LetExpr) { - var e = (LetExpr)expr; - if (e.Exact) { - Contract.Assert(e.LHSs.Count == e.RHSs.Count); - var i = 0; - foreach (var ee in e.RHSs) { - var lhs = e.LHSs[i]; - // Make LHS vars ghost if the RHS is a ghost - if (UsesSpecFeatures(ee)) { - foreach (var bv in lhs.Vars) { - if (!bv.IsGhost) { - bv.MakeGhost(); - } - } - } - - if (!lhs.Vars.All(bv => bv.IsGhost)) { - CheckIsCompilable(ee, codeContext); - } - i++; - } - CheckIsCompilable(e.Body, codeContext); - } else { - Contract.Assert(e.RHSs.Count == 1); - var lhsVarsAreAllGhost = e.BoundVars.All(bv => bv.IsGhost); - if (!lhsVarsAreAllGhost) { - CheckIsCompilable(e.RHSs[0], codeContext); - } - CheckIsCompilable(e.Body, codeContext); - - // fill in bounds for this to-be-compiled let-such-that expression - Contract.Assert(e.RHSs.Count == 1); // if we got this far, the resolver will have checked this condition successfully - var constraint = e.RHSs[0]; - e.Constraint_Bounds = DiscoverBestBounds_MultipleVars(e.BoundVars.ToList(), constraint, true, ComprehensionExpr.BoundedPool.PoolVirtues.None); - } - return; - } else if (expr is LambdaExpr) { - var e = expr as LambdaExpr; - CheckIsCompilable(e.Body, codeContext); - return; - } else if (expr is ComprehensionExpr) { - var e = (ComprehensionExpr)expr; - var uncompilableBoundVars = e.UncompilableBoundVars(); - if (uncompilableBoundVars.Count != 0) { - string what; - if (e is SetComprehension) { - what = ((SetComprehension)e).Finite ? "set comprehensions" : "iset comprehensions"; - } else if (e is MapComprehension) { - what = ((MapComprehension)e).Finite ? "map comprehensions" : "imap comprehensions"; - } else { - Contract.Assume(e is QuantifierExpr); // otherwise, unexpected ComprehensionExpr (since LambdaExpr is handled separately above) - Contract.Assert(((QuantifierExpr)e).SplitQuantifier == null); // No split quantifiers during resolution - what = "quantifiers"; - } - foreach (var bv in uncompilableBoundVars) { - reporter.Error(MessageSource.Resolver, expr, "{0} in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for '{1}'", what, bv.Name); - } - return; - } - // don't recurse down any attributes - if (e.Range != null) { CheckIsCompilable(e.Range, codeContext); } - CheckIsCompilable(e.Term, codeContext); - return; - - } else if (expr is ChainingExpression) { - // We don't care about the different operators; we only want the operands, so let's get them directly from - // the chaining expression - var e = (ChainingExpression)expr; - e.Operands.ForEach(ee => CheckIsCompilable(ee, codeContext)); - return; - } - - foreach (var ee in expr.SubExpressions) { - CheckIsCompilable(ee, codeContext); - } - } - public void ResolveFunctionCallExpr(FunctionCallExpr e, ResolveOpts opts) { Contract.Requires(e != null); Contract.Requires(e.Type == null); // should not have been type checked before @@ -17304,7 +17126,7 @@ private void AddCallGraphEdgeForField(ICodeContext callingContext, Field field, } } - private static void AddCallGraphEdge(ICodeContext callingContext, ICallable function, Expression e, bool isFunctionReturnValue) { + internal void AddCallGraphEdge(ICodeContext callingContext, ICallable function, Expression e, bool isFunctionReturnValue) { Contract.Requires(callingContext != null); Contract.Requires(function != null); Contract.Requires(e != null); @@ -18176,232 +17998,6 @@ public static BinaryExpr.ResolvedOpcode ResolveOp(BinaryExpr.Opcode op, Type lef } } - /// - /// Returns whether or not 'expr' has any subexpression that uses some feature (like a ghost or quantifier) - /// that is allowed only in specification contexts. - /// Requires 'expr' to be a successfully resolved expression. - /// - bool UsesSpecFeatures(Expression expr) { - Contract.Requires(expr != null); - Contract.Requires(expr.WasResolved()); // this check approximates the requirement that "expr" be resolved - - if (expr is LiteralExpr) { - return false; - } else if (expr is ThisExpr) { - return false; - } else if (expr is IdentifierExpr) { - IdentifierExpr e = (IdentifierExpr)expr; - return cce.NonNull(e.Var).IsGhost; - } else if (expr is DatatypeValue) { - var e = (DatatypeValue)expr; - // check all NON-ghost arguments - // note that if resolution is successful, then |e.Arguments| == |e.Ctor.Formals| - for (int i = 0; i < e.Arguments.Count; i++) { - if (!e.Ctor.Formals[i].IsGhost && UsesSpecFeatures(e.Arguments[i])) { - return true; - } - } - return false; - } else if (expr is DisplayExpression) { - DisplayExpression e = (DisplayExpression)expr; - return e.Elements.Exists(ee => UsesSpecFeatures(ee)); - } else if (expr is MapDisplayExpr) { - MapDisplayExpr e = (MapDisplayExpr)expr; - return e.Elements.Exists(p => UsesSpecFeatures(p.A) || UsesSpecFeatures(p.B)); - } else if (expr is MemberSelectExpr) { - MemberSelectExpr e = (MemberSelectExpr)expr; - if (e.Member != null) { - return cce.NonNull(e.Member).IsGhost || UsesSpecFeatures(e.Obj); - } else { - return false; - } - } else if (expr is SeqSelectExpr) { - SeqSelectExpr e = (SeqSelectExpr)expr; - return UsesSpecFeatures(e.Seq) || - (e.E0 != null && UsesSpecFeatures(e.E0)) || - (e.E1 != null && UsesSpecFeatures(e.E1)); - } else if (expr is MultiSelectExpr) { - MultiSelectExpr e = (MultiSelectExpr)expr; - return UsesSpecFeatures(e.Array) || e.Indices.Exists(ee => UsesSpecFeatures(ee)); - } else if (expr is SeqUpdateExpr) { - SeqUpdateExpr e = (SeqUpdateExpr)expr; - return UsesSpecFeatures(e.Seq) || - UsesSpecFeatures(e.Index) || - UsesSpecFeatures(e.Value); - } else if (expr is FunctionCallExpr) { - var e = (FunctionCallExpr)expr; - if (e.Function.IsGhost) { - return true; - } - // check all NON-ghost arguments - if (UsesSpecFeatures(e.Receiver)) { - return true; - } - for (int i = 0; i < e.Function.Formals.Count; i++) { - if (!e.Function.Formals[i].IsGhost && UsesSpecFeatures(e.Args[i])) { - return true; - } - } - return false; - } else if (expr is ApplyExpr) { - ApplyExpr e = (ApplyExpr)expr; - return UsesSpecFeatures(e.Function) || e.Args.Exists(UsesSpecFeatures); - } else if (expr is OldExpr || expr is UnchangedExpr) { - return true; - } else if (expr is UnaryExpr) { - var e = (UnaryExpr)expr; - if (e is UnaryOpExpr unaryOpExpr && (unaryOpExpr.Op == UnaryOpExpr.Opcode.Fresh || unaryOpExpr.Op == UnaryOpExpr.Opcode.Allocated)) { - return true; - } - if (expr is TypeTestExpr tte && !IsTypeTestCompilable(tte)) { - return true; - } - return UsesSpecFeatures(e.E); - } else if (expr is BinaryExpr) { - BinaryExpr e = (BinaryExpr)expr; - switch (e.ResolvedOp_PossiblyStillUndetermined) { - case BinaryExpr.ResolvedOpcode.RankGt: - case BinaryExpr.ResolvedOpcode.RankLt: - return true; - default: - return UsesSpecFeatures(e.E0) || UsesSpecFeatures(e.E1); - } - } else if (expr is TernaryExpr) { - var e = (TernaryExpr)expr; - switch (e.Op) { - case TernaryExpr.Opcode.PrefixEqOp: - case TernaryExpr.Opcode.PrefixNeqOp: - return true; - default: - break; - } - return UsesSpecFeatures(e.E0) || UsesSpecFeatures(e.E1) || UsesSpecFeatures(e.E2); - } else if (expr is LetExpr) { - var e = (LetExpr)expr; - if (e.Exact) { - MakeGhostAsNeeded(e.LHSs); - return UsesSpecFeatures(e.Body); - } else { - Contract.Assert(e.RHSs.Count == 1); - if (UsesSpecFeatures(e.RHSs[0])) { - foreach (var bv in e.BoundVars) { - bv.MakeGhost(); - } - } - return UsesSpecFeatures(e.Body); - } - } else if (expr is QuantifierExpr) { - var e = (QuantifierExpr)expr; - Contract.Assert(e.SplitQuantifier == null); // No split quantifiers during resolution - return e.UncompilableBoundVars().Count != 0 || UsesSpecFeatures(e.LogicalBody()); - } else if (expr is SetComprehension) { - var e = (SetComprehension)expr; - return !e.Finite || e.UncompilableBoundVars().Count != 0 || (e.Range != null && UsesSpecFeatures(e.Range)) || (e.Term != null && UsesSpecFeatures(e.Term)); - } else if (expr is MapComprehension) { - var e = (MapComprehension)expr; - return !e.Finite || e.UncompilableBoundVars().Count != 0 || UsesSpecFeatures(e.Range) || (e.TermLeft != null && UsesSpecFeatures(e.TermLeft)) || UsesSpecFeatures(e.Term); - } else if (expr is LambdaExpr) { - var e = (LambdaExpr)expr; - return UsesSpecFeatures(e.Term); - } else if (expr is WildcardExpr) { - return false; - } else if (expr is StmtExpr) { - var e = (StmtExpr)expr; - return UsesSpecFeatures(e.E); - } else if (expr is ITEExpr) { - ITEExpr e = (ITEExpr)expr; - return UsesSpecFeatures(e.Test) || UsesSpecFeatures(e.Thn) || UsesSpecFeatures(e.Els); - } else if (expr is NestedMatchExpr) { - return UsesSpecFeatures(((NestedMatchExpr)expr).ResolvedExpression); - } else if (expr is MatchExpr) { - MatchExpr me = (MatchExpr)expr; - if (UsesSpecFeatures(me.Source)) { - return true; - } - return me.Cases.Exists(mc => UsesSpecFeatures(mc.Body)); - } else if (expr is ConcreteSyntaxExpression) { - var e = (ConcreteSyntaxExpression)expr; - return e.ResolvedExpression != null && UsesSpecFeatures(e.ResolvedExpression); - } else if (expr is SeqConstructionExpr) { - var e = (SeqConstructionExpr)expr; - return UsesSpecFeatures(e.N) || UsesSpecFeatures(e.Initializer); - } else if (expr is MultiSetFormingExpr) { - var e = (MultiSetFormingExpr)expr; - return UsesSpecFeatures(e.E); - } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression - } - } - - public static bool IsTypeTestCompilable(TypeTestExpr tte) { - Contract.Requires(tte != null); - var fromType = tte.E.Type; - if (fromType.IsSubtypeOf(tte.ToType, false, true)) { - // this is a no-op, so it can trivially be compiled - return true; - } - - // TODO: It would be nice to allow some subset types in test tests in compiled code. But for now, such cases - // are allowed only in ghost contexts. - var udtTo = (UserDefinedType)tte.ToType.NormalizeExpandKeepConstraints(); - if (udtTo.ResolvedClass is SubsetTypeDecl && !(udtTo.ResolvedClass is NonNullTypeDecl)) { - return false; - } - - // The operation can be performed at run time if the mapping of .ToType's type parameters are injective in fromType's type parameters. - // For illustration, suppose the "is"-operation is testing whether or not the given expression of type A has type B, where - // X and Y are some type expressions. At run time, we can check if the expression has type B<...>, but we can't on all target platforms - // be certain about the "...". So, if both B and B are possible subtypes of A, we can't perform the type test at run time. - // In other words, we CAN perform the type test at run time if the type parameters of A uniquely determine the type parameters of B. - // Let T be a list of type parameters (in particular, we will use the formal TypeParameter's declared in type B). Then, represent - // B in parent type A, and let's say the result is A for some type expression U. If U contains all type parameters from T, - // then the mapping from B to A is unique, which means the mapping frmo B to A is unique, which means we can check if an - // A value is a B value by checking if the value is of type B<...>. - var B = ((UserDefinedType)tte.ToType.NormalizeExpandKeepConstraints()).ResolvedClass; // important to keep constraints here, so no type parameters are lost - var B_T = UserDefinedType.FromTopLevelDecl(tte.tok, B); - var tps = new HashSet(); // There are going to be the type parameters of fromType (that is, T in the discussion above) - if (fromType.TypeArgs.Count != 0) { - // we need this "if" statement, because if "fromType" is "object" or "object?", then it isn't a UserDefinedType - var A = (UserDefinedType)fromType.NormalizeExpand(); // important to NOT keep constraints here, since they won't be evident at run time - var A_U = B_T.AsParentType(A.ResolvedClass); - // the type test can be performed at run time if all the type parameters of "B_T" are free type parameters of "A_U". - A_U.AddFreeTypeParameters(tps); - } - foreach (var tp in B.TypeArgs) { - if (!tps.Contains(tp)) { - // type test cannot be performed at run time, so this is a ghost operation - // TODO: If "tp" is a type parameter for which there is a run-time type descriptor, then we would still be able to perform - // the type test at run time. - return false; - } - } - // type test can be performed at run time - return true; - } - - void MakeGhostAsNeeded(List> lhss) { - foreach (CasePattern lhs in lhss) { - MakeGhostAsNeeded(lhs); - } - } - - void MakeGhostAsNeeded(CasePattern lhs) { - if (lhs.Ctor != null && lhs.Arguments != null) { - for (int i = 0; i < lhs.Arguments.Count && i < lhs.Ctor.Destructors.Count; i++) { - MakeGhostAsNeeded(lhs.Arguments[i], lhs.Ctor.Destructors[i]); - } - } - } - - void MakeGhostAsNeeded(CasePattern arg, DatatypeDestructor d) { - if (arg.Expr is IdentifierExpr ie && ie.Var is BoundVar bv) { - if (d.IsGhost) bv.MakeGhost(); - } - if (arg.Ctor != null) { - MakeGhostAsNeeded(arg); - } - } - /// /// This method adds to "friendlyCalls" all diff --git a/Source/Dafny/Util.cs b/Source/Dafny/Util.cs index 2f9b19f0f2f..8767ec1e85e 100644 --- a/Source/Dafny/Util.cs +++ b/Source/Dafny/Util.cs @@ -465,4 +465,442 @@ public int GetHashCode(IEnumerable obj) { return hash.ToHashCode(); } } + + public class ExpressionTester { + private bool reportErrors = false; + private ErrorReporter reporter = null; + private Resolver resolver = null; + + public ExpressionTester(Resolver resolver = null, bool reportErrors = false) { + Contract.Requires(reportErrors == false || resolver != null); + if (resolver != null) { + this.reporter = resolver.getReporter(); + this.resolver = resolver; + } + + this.reportErrors = reportErrors; + } + + // Static call to CheckIsCompilable + public static bool CheckIsCompilable(Resolver resolver, Expression expr, ICodeContext codeContext) { + return new ExpressionTester(resolver, true).CheckIsCompilable(expr, codeContext); + } + + /// + /// Try to make "expr" compilable (in particular, mark LHSs of a let-expression as ghosts if + /// the corresponding RHS is ghost), and then report errors for every part that would prevent + /// compilation. + /// Requires "expr" to have been successfully resolved. + /// + private bool CheckIsCompilable(Expression expr, ICodeContext codeContext) { + Contract.Requires(expr != null); + Contract.Requires(expr.WasResolved()); // this check approximates the requirement that "expr" be resolved + Contract.Requires(codeContext != null || reporter == null); + + var isCompilable = true; + + if (expr is IdentifierExpr expression) { + if (expression.Var != null && expression.Var.IsGhost) { + reporter?.Error(MessageSource.Resolver, expression, "ghost variables are allowed only in specification contexts"); + return false; + } + + } else if (expr is MemberSelectExpr selectExpr) { + if (selectExpr.Member != null && selectExpr.Member.IsGhost) { + reporter?.Error(MessageSource.Resolver, selectExpr, "ghost fields are allowed only in specification contexts"); + return false; + } + + } else if (expr is FunctionCallExpr callExpr) { + if (callExpr.Function != null) { + if (callExpr.Function.IsGhost) { + if (reportErrors == false) return false; + string msg; + if (callExpr.Function is TwoStateFunction || callExpr.Function is ExtremePredicate || callExpr.Function is PrefixPredicate) { + msg = $"a call to a {callExpr.Function.WhatKind} is allowed only in specification contexts"; + } else if (callExpr.Function is Predicate) { + msg = "predicate calls are allowed only in specification contexts (consider declaring the predicate a 'predicate method')"; + } else { + msg = "function calls are allowed only in specification contexts (consider declaring the function a 'function method')"; + } + reporter?.Error(MessageSource.Resolver, callExpr, msg); + return false; + } + if (callExpr.Function.ByMethodBody != null) { + Contract.Assert(callExpr.Function.ByMethodDecl != null); // we expect .ByMethodDecl to have been filled in by now + // this call will really go to the method part of the function-by-method, so add that edge to the call graph + resolver?.AddCallGraphEdge(codeContext, callExpr.Function.ByMethodDecl, callExpr, false); + callExpr.IsByMethodCall = true; + } + // function is okay, so check all NON-ghost arguments + isCompilable = CheckIsCompilable(callExpr.Receiver, codeContext); + for (var i = 0; i < callExpr.Function.Formals.Count; i++) { + if (!callExpr.Function.Formals[i].IsGhost) { + isCompilable = isCompilable && CheckIsCompilable(callExpr.Args[i], codeContext); + } + } + } + + return isCompilable; + + } else if (expr is DatatypeValue value) { + // check all NON-ghost arguments + // note that if resolution is successful, then |e.Arguments| == |e.Ctor.Formals| + for (int i = 0; i < value.Arguments.Count; i++) { + if (!value.Ctor.Formals[i].IsGhost) { + isCompilable = isCompilable && CheckIsCompilable(value.Arguments[i], codeContext); + } + } + return isCompilable; + + } else if (expr is OldExpr) { + reporter?.Error(MessageSource.Resolver, expr, "old expressions are allowed only in specification and ghost contexts"); + return false; + + } else if (expr is TypeTestExpr tte) { + if (!IsTypeTestCompilable(tte)) { + reporter?.Error(MessageSource.Resolver, tte, $"an expression of type '{tte.E.Type}' is not run-time checkable to be a '{tte.ToType}'"); + return false; + } + + } else if (expr is FreshExpr) { + reporter?.Error(MessageSource.Resolver, expr, "fresh expressions are allowed only in specification and ghost contexts"); + return false; + + } else if (expr is UnchangedExpr) { + reporter?.Error(MessageSource.Resolver, expr, "unchanged expressions are allowed only in specification and ghost contexts"); + return false; + + } else if (expr is StmtExpr stmtExpr) { + // ignore the statement + return CheckIsCompilable(stmtExpr.E, codeContext); + + } else if (expr is BinaryExpr binaryExpr) { + switch (binaryExpr.ResolvedOp_PossiblyStillUndetermined) { + case BinaryExpr.ResolvedOpcode.RankGt: + case BinaryExpr.ResolvedOpcode.RankLt: + reporter?.Error(MessageSource.Resolver, binaryExpr, "rank comparisons are allowed only in specification and ghost contexts"); + return false; + default: + break; + } + + return true; + } else if (expr is TernaryExpr ternaryExpr) { + switch (ternaryExpr.Op) { + case TernaryExpr.Opcode.PrefixEqOp: + case TernaryExpr.Opcode.PrefixNeqOp: + reporter?.Error(MessageSource.Resolver, ternaryExpr, "prefix equalities are allowed only in specification and ghost contexts"); + return false; + default: + break; + } + + return true; + } else if (expr is LetExpr letExpr) { + if (letExpr.Exact) { + Contract.Assert(letExpr.LHSs.Count == letExpr.RHSs.Count); + var i = 0; + foreach (var ee in letExpr.RHSs) { + var lhs = letExpr.LHSs[i]; + // Make LHS vars ghost if the RHS is a ghost + if (UsesSpecFeatures(ee)) { + foreach (var bv in lhs.Vars) { + if (!bv.IsGhost) { + bv.MakeGhost(); + isCompilable = false; + } + } + } + + if (!lhs.Vars.All(bv => bv.IsGhost)) { + isCompilable = isCompilable && CheckIsCompilable(ee, codeContext); + } + i++; + } + isCompilable = isCompilable && CheckIsCompilable(letExpr.Body, codeContext); + } else { + Contract.Assert(letExpr.RHSs.Count == 1); + var lhsVarsAreAllGhost = letExpr.BoundVars.All(bv => bv.IsGhost); + if (!lhsVarsAreAllGhost) { + isCompilable = isCompilable && CheckIsCompilable(letExpr.RHSs[0], codeContext); + } + isCompilable = isCompilable && CheckIsCompilable(letExpr.Body, codeContext); + + // fill in bounds for this to-be-compiled let-such-that expression + Contract.Assert(letExpr.RHSs.Count == 1); // if we got this far, the resolver will have checked this condition successfully + var constraint = letExpr.RHSs[0]; + if (resolver != null) { + letExpr.Constraint_Bounds = Resolver.DiscoverBestBounds_MultipleVars(letExpr.BoundVars.ToList(), + constraint, true, ComprehensionExpr.BoundedPool.PoolVirtues.None); + } + } + return isCompilable; + } else if (expr is LambdaExpr lambdaExpr) { + return CheckIsCompilable(lambdaExpr.Body, codeContext); + } else if (expr is ComprehensionExpr comprehensionExpr) { + var uncompilableBoundVars = comprehensionExpr.UncompilableBoundVars(); + if (uncompilableBoundVars.Count != 0) { + if (reportErrors == false) return false; + string what; + if (comprehensionExpr is SetComprehension comprehension) { + what = comprehension.Finite ? "set comprehensions" : "iset comprehensions"; + } else if (comprehensionExpr is MapComprehension mapComprehension) { + what = mapComprehension.Finite ? "map comprehensions" : "imap comprehensions"; + } else { + Contract.Assume(comprehensionExpr is QuantifierExpr); // otherwise, unexpected ComprehensionExpr (since LambdaExpr is handled separately above) + Contract.Assert(((QuantifierExpr)comprehensionExpr).SplitQuantifier == null); // No split quantifiers during resolution + what = "quantifiers"; + } + foreach (var bv in uncompilableBoundVars) { + reporter.Error(MessageSource.Resolver, comprehensionExpr, "{0} in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for '{1}'", what, bv.Name); + } + return false; + } + // don't recurse down any attributes + if (comprehensionExpr.Range != null) { + isCompilable = isCompilable && CheckIsCompilable(comprehensionExpr.Range, codeContext); + } + isCompilable = isCompilable && CheckIsCompilable(comprehensionExpr.Term, codeContext); + return isCompilable; + + } else if (expr is ChainingExpression chainingExpression) { + // We don't care about the different operators; we only want the operands, so let's get them directly from + // the chaining expression + return chainingExpression.Operands.TrueForAll(ee => CheckIsCompilable(ee, codeContext)); + } + + foreach (var ee in expr.SubExpressions) { + isCompilable = isCompilable && CheckIsCompilable(ee, codeContext); + } + + return isCompilable; + } + + + public static bool IsTypeTestCompilable(TypeTestExpr tte) { + Contract.Requires(tte != null); + var fromType = tte.E.Type; + if (fromType.IsSubtypeOf(tte.ToType, false, true)) { + // this is a no-op, so it can trivially be compiled + return true; + } + + // TODO: It would be nice to allow some subset types in test tests in compiled code. But for now, such cases + // are allowed only in ghost contexts. + var udtTo = (UserDefinedType)tte.ToType.NormalizeExpandKeepConstraints(); + if (udtTo.ResolvedClass is SubsetTypeDecl && !(udtTo.ResolvedClass is NonNullTypeDecl)) { + return false; + } + + // The operation can be performed at run time if the mapping of .ToType's type parameters are injective in fromType's type parameters. + // For illustration, suppose the "is"-operation is testing whether or not the given expression of type A has type B, where + // X and Y are some type expressions. At run time, we can check if the expression has type B<...>, but we can't on all target platforms + // be certain about the "...". So, if both B and B are possible subtypes of A, we can't perform the type test at run time. + // In other words, we CAN perform the type test at run time if the type parameters of A uniquely determine the type parameters of B. + // Let T be a list of type parameters (in particular, we will use the formal TypeParameter's declared in type B). Then, represent + // B in parent type A, and let's say the result is A for some type expression U. If U contains all type parameters from T, + // then the mapping from B to A is unique, which means the mapping frmo B to A is unique, which means we can check if an + // A value is a B value by checking if the value is of type B<...>. + var B = ((UserDefinedType)tte.ToType.NormalizeExpandKeepConstraints()).ResolvedClass; // important to keep constraints here, so no type parameters are lost + var B_T = UserDefinedType.FromTopLevelDecl(tte.tok, B); + var tps = new HashSet(); // There are going to be the type parameters of fromType (that is, T in the discussion above) + if (fromType.TypeArgs.Count != 0) { + // we need this "if" statement, because if "fromType" is "object" or "object?", then it isn't a UserDefinedType + var A = (UserDefinedType)fromType.NormalizeExpand(); // important to NOT keep constraints here, since they won't be evident at run time + var A_U = B_T.AsParentType(A.ResolvedClass); + // the type test can be performed at run time if all the type parameters of "B_T" are free type parameters of "A_U". + A_U.AddFreeTypeParameters(tps); + } + foreach (var tp in B.TypeArgs) { + if (!tps.Contains(tp)) { + // type test cannot be performed at run time, so this is a ghost operation + // TODO: If "tp" is a type parameter for which there is a run-time type descriptor, then we would still be able to perform + // the type test at run time. + return false; + } + } + // type test can be performed at run time + return true; + } + + /// + /// Returns whether or not 'expr' has any subexpression that uses some feature (like a ghost or quantifier) + /// that is allowed only in specification contexts. + /// Requires 'expr' to be a successfully resolved expression. + /// + bool UsesSpecFeatures(Expression expr) { + Contract.Requires(expr != null); + Contract.Requires(expr.WasResolved()); // this check approximates the requirement that "expr" be resolved + + if (expr is LiteralExpr) { + return false; + } else if (expr is ThisExpr) { + return false; + } else if (expr is IdentifierExpr) { + IdentifierExpr e = (IdentifierExpr)expr; + return cce.NonNull(e.Var).IsGhost; + } else if (expr is DatatypeValue) { + var e = (DatatypeValue)expr; + // check all NON-ghost arguments + // note that if resolution is successful, then |e.Arguments| == |e.Ctor.Formals| + for (int i = 0; i < e.Arguments.Count; i++) { + if (!e.Ctor.Formals[i].IsGhost && UsesSpecFeatures(e.Arguments[i])) { + return true; + } + } + return false; + } else if (expr is DisplayExpression) { + DisplayExpression e = (DisplayExpression)expr; + return e.Elements.Exists(ee => UsesSpecFeatures(ee)); + } else if (expr is MapDisplayExpr) { + MapDisplayExpr e = (MapDisplayExpr)expr; + return e.Elements.Exists(p => UsesSpecFeatures(p.A) || UsesSpecFeatures(p.B)); + } else if (expr is MemberSelectExpr) { + MemberSelectExpr e = (MemberSelectExpr)expr; + if (e.Member != null) { + return cce.NonNull(e.Member).IsGhost || UsesSpecFeatures(e.Obj); + } else { + return false; + } + } else if (expr is SeqSelectExpr) { + SeqSelectExpr e = (SeqSelectExpr)expr; + return UsesSpecFeatures(e.Seq) || + (e.E0 != null && UsesSpecFeatures(e.E0)) || + (e.E1 != null && UsesSpecFeatures(e.E1)); + } else if (expr is MultiSelectExpr) { + MultiSelectExpr e = (MultiSelectExpr)expr; + return UsesSpecFeatures(e.Array) || e.Indices.Exists(ee => UsesSpecFeatures(ee)); + } else if (expr is SeqUpdateExpr) { + SeqUpdateExpr e = (SeqUpdateExpr)expr; + return UsesSpecFeatures(e.Seq) || + UsesSpecFeatures(e.Index) || + UsesSpecFeatures(e.Value); + } else if (expr is FunctionCallExpr) { + var e = (FunctionCallExpr)expr; + if (e.Function.IsGhost) { + return true; + } + // check all NON-ghost arguments + if (UsesSpecFeatures(e.Receiver)) { + return true; + } + for (int i = 0; i < e.Function.Formals.Count; i++) { + if (!e.Function.Formals[i].IsGhost && UsesSpecFeatures(e.Args[i])) { + return true; + } + } + return false; + } else if (expr is ApplyExpr) { + ApplyExpr e = (ApplyExpr)expr; + return UsesSpecFeatures(e.Function) || e.Args.Exists(UsesSpecFeatures); + } else if (expr is OldExpr || expr is UnchangedExpr) { + return true; + } else if (expr is UnaryExpr) { + var e = (UnaryExpr)expr; + if (e is UnaryOpExpr unaryOpExpr && (unaryOpExpr.Op == UnaryOpExpr.Opcode.Fresh || unaryOpExpr.Op == UnaryOpExpr.Opcode.Allocated)) { + return true; + } + if (expr is TypeTestExpr tte && !IsTypeTestCompilable(tte)) { + return true; + } + return UsesSpecFeatures(e.E); + } else if (expr is BinaryExpr) { + BinaryExpr e = (BinaryExpr)expr; + switch (e.ResolvedOp_PossiblyStillUndetermined) { + case BinaryExpr.ResolvedOpcode.RankGt: + case BinaryExpr.ResolvedOpcode.RankLt: + return true; + default: + return UsesSpecFeatures(e.E0) || UsesSpecFeatures(e.E1); + } + } else if (expr is TernaryExpr) { + var e = (TernaryExpr)expr; + switch (e.Op) { + case TernaryExpr.Opcode.PrefixEqOp: + case TernaryExpr.Opcode.PrefixNeqOp: + return true; + default: + break; + } + return UsesSpecFeatures(e.E0) || UsesSpecFeatures(e.E1) || UsesSpecFeatures(e.E2); + } else if (expr is LetExpr) { + var e = (LetExpr)expr; + if (e.Exact) { + MakeGhostAsNeeded(e.LHSs); + return UsesSpecFeatures(e.Body); + } else { + Contract.Assert(e.RHSs.Count == 1); + if (UsesSpecFeatures(e.RHSs[0])) { + foreach (var bv in e.BoundVars) { + bv.MakeGhost(); + } + } + return UsesSpecFeatures(e.Body); + } + } else if (expr is QuantifierExpr) { + var e = (QuantifierExpr)expr; + Contract.Assert(e.SplitQuantifier == null); // No split quantifiers during resolution + return e.UncompilableBoundVars().Count != 0 || UsesSpecFeatures(e.LogicalBody()); + } else if (expr is SetComprehension) { + var e = (SetComprehension)expr; + return !e.Finite || e.UncompilableBoundVars().Count != 0 || (e.Range != null && UsesSpecFeatures(e.Range)) || (e.Term != null && UsesSpecFeatures(e.Term)); + } else if (expr is MapComprehension) { + var e = (MapComprehension)expr; + return !e.Finite || e.UncompilableBoundVars().Count != 0 || UsesSpecFeatures(e.Range) || (e.TermLeft != null && UsesSpecFeatures(e.TermLeft)) || UsesSpecFeatures(e.Term); + } else if (expr is LambdaExpr) { + var e = (LambdaExpr)expr; + return UsesSpecFeatures(e.Term); + } else if (expr is WildcardExpr) { + return false; + } else if (expr is StmtExpr) { + var e = (StmtExpr)expr; + return UsesSpecFeatures(e.E); + } else if (expr is ITEExpr) { + ITEExpr e = (ITEExpr)expr; + return UsesSpecFeatures(e.Test) || UsesSpecFeatures(e.Thn) || UsesSpecFeatures(e.Els); + } else if (expr is NestedMatchExpr) { + return UsesSpecFeatures(((NestedMatchExpr)expr).ResolvedExpression); + } else if (expr is MatchExpr) { + MatchExpr me = (MatchExpr)expr; + if (UsesSpecFeatures(me.Source)) { + return true; + } + return me.Cases.Exists(mc => UsesSpecFeatures(mc.Body)); + } else if (expr is ConcreteSyntaxExpression) { + var e = (ConcreteSyntaxExpression)expr; + return e.ResolvedExpression != null && UsesSpecFeatures(e.ResolvedExpression); + } else if (expr is SeqConstructionExpr) { + var e = (SeqConstructionExpr)expr; + return UsesSpecFeatures(e.N) || UsesSpecFeatures(e.Initializer); + } else if (expr is MultiSetFormingExpr) { + var e = (MultiSetFormingExpr)expr; + return UsesSpecFeatures(e.E); + } else { + Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression + } + } + void MakeGhostAsNeeded(List> lhss) { + foreach (CasePattern lhs in lhss) { + MakeGhostAsNeeded(lhs); + } + } + + void MakeGhostAsNeeded(CasePattern lhs) { + if (lhs.Ctor != null && lhs.Arguments != null) { + for (int i = 0; i < lhs.Arguments.Count && i < lhs.Ctor.Destructors.Count; i++) { + MakeGhostAsNeeded(lhs.Arguments[i], lhs.Ctor.Destructors[i]); + } + } + } + + void MakeGhostAsNeeded(CasePattern arg, DatatypeDestructor d) { + if (arg.Expr is IdentifierExpr ie && ie.Var is BoundVar bv) { + if (d.IsGhost) bv.MakeGhost(); + } + if (arg.Ctor != null) { + MakeGhostAsNeeded(arg); + } + } + } } From da3591532b936ba23898762bf7b2842abc0cbb96 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Mon, 25 Oct 2021 16:17:09 -0500 Subject: [PATCH 07/27] WIP fixing interfaces --- Source/Dafny/Resolver.cs | 2 +- Source/Dafny/Rewriter.cs | 7 +++---- Source/Dafny/Util.cs | 8 ++++---- 3 files changed, 8 insertions(+), 9 deletions(-) diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index c60d1d17144..7945193c1c7 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -8515,7 +8515,7 @@ public void Visit(Statement stmt, bool mustBeErasable) { if (rhs.ArrayDimensions != null) { rhs.ArrayDimensions.ForEach(ee => ExpressionTester.CheckIsCompilable(resolver, ee, codeContext)); if (rhs.ElementInit != null) { - resolver.CheckIsCompilable(rhs.ElementInit, codeContext); + ExpressionTester.CheckIsCompilable(resolver, rhs.ElementInit, codeContext); } if (rhs.InitDisplay != null) { rhs.InitDisplay.ForEach(ee => ExpressionTester.CheckIsCompilable(resolver, ee, codeContext)); diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index 1d62f7b3170..a252b08894c 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -1361,15 +1361,14 @@ List generateAutoReqs(Expression expr) { e.UpdateTerm(allReqsSatisfiedAndTerm); reporter.Info(MessageSource.Rewriter, e.tok, "autoreq added (" + Printer.ExtendedExprToString(allReqsSatisfied) + ") &&"); } - } else if (expr is SetComprehension) { - var e = (SetComprehension)expr; + } else if (expr is SetComprehension setComprehension) { // Translate "set xs | R :: T" // See LetExpr for issues with the e.Range //reqs.AddRange(generateAutoReqs(e.Range)); - var auto_reqs = generateAutoReqs(e.Term); + var auto_reqs = generateAutoReqs(setComprehension.Term); if (auto_reqs.Count > 0) { - reqs.Add(Expression.CreateQuantifier(new ForallExpr(e.tok, new List(), e.BoundVars, e.Range, andify(e.Term.tok, auto_reqs), e.Attributes), true)); + reqs.Add(Expression.CreateQuantifier(new ForallExpr(setComprehension.tok, new List(), setComprehension.BoundVars, setComprehension.Range, andify(setComprehension.Term.tok, auto_reqs), setComprehension.Attributes), true)); } } else if (expr is MapComprehension) { var e = (MapComprehension)expr; diff --git a/Source/Dafny/Util.cs b/Source/Dafny/Util.cs index 8767ec1e85e..c014b275655 100644 --- a/Source/Dafny/Util.cs +++ b/Source/Dafny/Util.cs @@ -729,7 +729,7 @@ public static bool IsTypeTestCompilable(TypeTestExpr tte) { /// that is allowed only in specification contexts. /// Requires 'expr' to be a successfully resolved expression. /// - bool UsesSpecFeatures(Expression expr) { + public static bool UsesSpecFeatures(Expression expr) { Contract.Requires(expr != null); Contract.Requires(expr.WasResolved()); // this check approximates the requirement that "expr" be resolved @@ -880,13 +880,13 @@ bool UsesSpecFeatures(Expression expr) { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression } } - void MakeGhostAsNeeded(List> lhss) { + static void MakeGhostAsNeeded(List> lhss) { foreach (CasePattern lhs in lhss) { MakeGhostAsNeeded(lhs); } } - void MakeGhostAsNeeded(CasePattern lhs) { + static void MakeGhostAsNeeded(CasePattern lhs) { if (lhs.Ctor != null && lhs.Arguments != null) { for (int i = 0; i < lhs.Arguments.Count && i < lhs.Ctor.Destructors.Count; i++) { MakeGhostAsNeeded(lhs.Arguments[i], lhs.Ctor.Destructors[i]); @@ -894,7 +894,7 @@ void MakeGhostAsNeeded(CasePattern lhs) { } } - void MakeGhostAsNeeded(CasePattern arg, DatatypeDestructor d) { + static void MakeGhostAsNeeded(CasePattern arg, DatatypeDestructor d) { if (arg.Expr is IdentifierExpr ie && ie.Var is BoundVar bv) { if (d.IsGhost) bv.MakeGhost(); } From 4724c1b23085af34ea0090136e1335e77e9d8980 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 26 Oct 2021 16:32:20 -0500 Subject: [PATCH 08/27] Refactored the code to inject guards for set and map expressions --- Source/Dafny/Compilers/Compiler.cs | 65 +++++++++++++------ Source/Dafny/Resolver.cs | 14 ++-- .../Translator.ExpressionTranslator.cs | 16 ++++- Test/git-issues/git-issue-697b.dfy | 1 - Test/git-issues/git-issue-697b.dfy.expect | 1 - Test/git-issues/git-issue-697c.dfy.expect | 6 +- Test/git-issues/git-issue-697d.dfy | 1 - Test/git-issues/git-issue-697d.dfy.expect | 3 +- Test/git-issues/git-issue-697e.dfy | 17 +++++ 9 files changed, 88 insertions(+), 36 deletions(-) create mode 100644 Test/git-issues/git-issue-697e.dfy diff --git a/Source/Dafny/Compilers/Compiler.cs b/Source/Dafny/Compilers/Compiler.cs index 160b8fbc5c9..dcb698693c2 100644 --- a/Source/Dafny/Compilers/Compiler.cs +++ b/Source/Dafny/Compilers/Compiler.cs @@ -4611,6 +4611,7 @@ void writeObj(ConcreteSyntaxTree w) { var native = AsNativeType(e.BoundVars[i].Type); ConcreteSyntaxTree newWBody = CreateLambda(new List { bv.Type }, e.tok, new List { IdName(bv) }, Type.Bool, wBody, untyped: true); newWBody = EmitReturnExpr(newWBody); + // TODO: Here we should emit the guard for the exists and forall expressions. wBody.Write(')'); wBody = newWBody; } @@ -4643,30 +4644,16 @@ void writeObj(ConcreteSyntaxTree w) { EmitSetBuilder_New(wr, setComprehension, collectionName); var n = setComprehension.BoundVars.Count; Contract.Assert(setComprehension.Bounds.Count == n); - for (var i = 0; i < n; i++) { + int i; + for (i = 0; i < n; i++) { var bound = setComprehension.Bounds[i]; var bv = setComprehension.BoundVars[i]; ConcreteSyntaxTree collectionWriter; var tmpVar = idGenerator.FreshId("_compr_"); wr = CreateForeachLoop(tmpVar, GetCollectionEnumerationType(bound, bv), IdName(bv), bv.Type, true, bv.tok, out collectionWriter, wr); - if (bv.Type is UserDefinedType userDefinedType) { - // TODO: What about types built with subset types? And subset types that have type parameters? - // var s = {List(Cell(1)), List(Cell(2), Cell(4)), List(Cell(2), Cell(3))}; - // set x: List | x in s - if (userDefinedType.ResolvedClass is SubsetTypeDecl subsetTypeDecl) { - if (subsetTypeDecl.Constraint != null && subsetTypeDecl.ConstraintIsCompilable) { - var bvIdentifier = new IdentifierExpr(setComprehension.tok, bv); - wr = EmitIf(out var guardWriterInner, false, wr); - var subContract = new Substituter(null, - new Dictionary() { - {subsetTypeDecl.Var, bvIdentifier} - }, - null); - var contraintInContext = subContract.Substitute(subsetTypeDecl.Constraint); - TrExpr(contraintInContext, guardWriterInner, inLetExprBody); - } - } - } + // var s = {List(Cell(1)), List(Cell(2), Cell(4)), List(Cell(2), Cell(3))}; + // set x: List | x in s + wr = MaybeInjectSubsetConstraint(wr, inLetExprBody, bv, setComprehension); CompileCollection(bound, bv, inLetExprBody, true, null, collectionWriter); } ConcreteSyntaxTree guardWriter; @@ -4712,6 +4699,7 @@ void writeObj(ConcreteSyntaxTree w) { ConcreteSyntaxTree collectionWriter; var tmpVar = idGenerator.FreshId("_compr_"); wr = CreateForeachLoop(tmpVar, GetCollectionEnumerationType(bound, bv), IdName(bv), bv.Type, true, bv.tok, out collectionWriter, wr); + wr = MaybeInjectSubsetConstraint(wr, inLetExprBody, bv, e); CompileCollection(bound, bv, inLetExprBody, true, null, collectionWriter); } ConcreteSyntaxTree guardWriter; @@ -4753,6 +4741,45 @@ void writeObj(ConcreteSyntaxTree w) { } } + private ConcreteSyntaxTree MaybeInjectSubsetConstraint(ConcreteSyntaxTree wr, bool inLetExprBody, BoundVar bv, + Expression e) { + int i; + if (bv.Type is UserDefinedType + { + TypeArgs: var typeArgs, + ResolvedClass: + var subsetTypeDecl and + SubsetTypeDecl + { + TypeArgs: var typeParametersArgs, + Var: var var, + ConstraintIsCompilable: true, + Constraint: var constraint + } + }) { + var bvIdentifier = new IdentifierExpr(e.tok, bv); + wr = EmitIf(out var guardWriterInner, false, wr); + var typeParameters = new Dictionary { }; + for (i = 0; i < typeParametersArgs.Count(); i++) { + typeParameters[typeParametersArgs[i]] = typeArgs[i]; + } + + var subContract = new Substituter(null, + new Dictionary() + { + {var, bvIdentifier} + }, + new Dictionary( + typeParameters + ) + ); + var constraintInContext = subContract.Substitute(constraint); + TrExpr(constraintInContext, guardWriterInner, inLetExprBody); + } + + return wr; + } + protected ConcreteSyntaxTree CaptureFreeVariables(Expression expr, bool captureOnlyAsRequiredByTargetLanguage, out Substituter su, bool inLetExprBody, ConcreteSyntaxTree wr) { if (captureOnlyAsRequiredByTargetLanguage && TargetLambdaCanUseEnclosingLocals) { // nothing to do diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 7945193c1c7..062d627adff 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -2677,6 +2677,12 @@ public void ResolveTopLevelDecls_Core(List/*!*/ declarations, if (!CheckTypeInference_Visitor.IsDetermined(dd.Rhs.NormalizeExpand())) { reporter.Error(MessageSource.Resolver, dd.tok, "subset type's base type is not fully determined; add an explicit type for '{0}'", dd.Var.Name); } + dd.ConstraintIsCompilable = ExpressionTester.CheckIsCompilable(this, dd.Constraint, new CodeContextWrapper(dd, true)); + if (!dd.ConstraintIsCompilable) { + reporter.Error(MessageSource.Resolver, dd.Constraint.tok, + "subset type's constraint must be compilable, until Dafny moves constraints handling to the verifier."); + } + scope.PopMarker(); allTypeParameters.PopMarker(); } @@ -6637,14 +6643,6 @@ protected override void VisitOneExpr(Expression expr) { } else if (e is SetComprehension setComprehension) { what = "set comprehension"; whereToLookForBounds = setComprehension.Range; - var setType = setComprehension.Type as SetType; - var argType = setType.Arg; - if (argType is UserDefinedType userDefinedType) { - if (userDefinedType.ResolvedClass is SubsetTypeDecl subsetTypeDecl) { - subsetTypeDecl.ConstraintIsCompilable = - ExpressionTester.CheckIsCompilable(null, subsetTypeDecl.Constraint, codeContext); - } - } } else if (e is MapComprehension) { what = "map comprehension"; whereToLookForBounds = e.Range; diff --git a/Source/Dafny/Verifier/Translator.ExpressionTranslator.cs b/Source/Dafny/Verifier/Translator.ExpressionTranslator.cs index a734ad94780..b5402572844 100644 --- a/Source/Dafny/Verifier/Translator.ExpressionTranslator.cs +++ b/Source/Dafny/Verifier/Translator.ExpressionTranslator.cs @@ -1292,8 +1292,22 @@ public Boogie.Expr TrExpr(Expression expr) { Boogie.Expr y = new Boogie.IdentifierExpr(expr.tok, yVar); Boogie.Expr lbody; if (e.TermIsSimple) { - // lambda y: BoxType :: CorrectType(y) && R[xs := yUnboxed] var bv = e.BoundVars[0]; + // lambda y: BoxType :: CorrectType(y) && R[xs := yUnboxed] + var assumedType = bv.Type; + if (e.Type is SetType setType) { + if (setType.Arg is UserDefinedType udt) { + if (udt.ResolvedClass is SubsetTypeDecl stdc) { + if (stdc.ConstraintIsCompilable) { + // Ok the filtering will be performed by the compiler, we can assume the subset type. + } else { + // TODO: Substitue type parameters when computing assumedType + create test case + assumedType = stdc.Rhs; + // We need to verify that the bound proves the type. + } + } + } + } Boogie.Expr typeAntecedent = translator.MkIsBox(new Boogie.IdentifierExpr(expr.tok, yVar), bv.Type); if (freeOfAlloc != null && !freeOfAlloc[0]) { var isAlloc = translator.MkIsAlloc(new Boogie.IdentifierExpr(expr.tok, yVar), bv.Type, HeapExpr); diff --git a/Test/git-issues/git-issue-697b.dfy b/Test/git-issues/git-issue-697b.dfy index e4d91a8b455..2bb523bdc5e 100644 --- a/Test/git-issues/git-issue-697b.dfy +++ b/Test/git-issues/git-issue-697b.dfy @@ -15,6 +15,5 @@ method Main() { var y := z.Keys; var b: bool := forall c :: c in y ==> doubleEvenCell(c) > 0; assert b; - //print(b); } diff --git a/Test/git-issues/git-issue-697b.dfy.expect b/Test/git-issues/git-issue-697b.dfy.expect index 188a72ebc36..00a51f822da 100644 --- a/Test/git-issues/git-issue-697b.dfy.expect +++ b/Test/git-issues/git-issue-697b.dfy.expect @@ -1,3 +1,2 @@ Dafny program verifier finished with 3 verified, 0 errors -true \ No newline at end of file diff --git a/Test/git-issues/git-issue-697c.dfy.expect b/Test/git-issues/git-issue-697c.dfy.expect index 24a1f33600c..ddf38868367 100644 --- a/Test/git-issues/git-issue-697c.dfy.expect +++ b/Test/git-issues/git-issue-697c.dfy.expect @@ -1,3 +1,3 @@ - -Dafny program verifier finished with 2 verified, 1 errors -true \ No newline at end of file +git-issue-697c.dfy(9,26): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method') +git-issue-697c.dfy(9,40): Error: subset type's constraint must be compilable, until Dafny moves constraints handling to the verifier. +2 resolution/type errors detected in git-issue-697c.dfy diff --git a/Test/git-issues/git-issue-697d.dfy b/Test/git-issues/git-issue-697d.dfy index e9c28c171dc..8c9c5fa32ab 100644 --- a/Test/git-issues/git-issue-697d.dfy +++ b/Test/git-issues/git-issue-697d.dfy @@ -18,6 +18,5 @@ method Main() { var y := set c: EvenCell | c in x; var b: bool := forall c :: c in y ==> doubleEvenCell(c) > 0; assert b; - print(b); } diff --git a/Test/git-issues/git-issue-697d.dfy.expect b/Test/git-issues/git-issue-697d.dfy.expect index 188a72ebc36..ba00363fc08 100644 --- a/Test/git-issues/git-issue-697d.dfy.expect +++ b/Test/git-issues/git-issue-697d.dfy.expect @@ -1,3 +1,2 @@ -Dafny program verifier finished with 3 verified, 0 errors -true \ No newline at end of file +Dafny program verifier finished with 4 verified, 0 errors diff --git a/Test/git-issues/git-issue-697e.dfy b/Test/git-issues/git-issue-697e.dfy new file mode 100644 index 00000000000..804857efb25 --- /dev/null +++ b/Test/git-issues/git-issue-697e.dfy @@ -0,0 +1,17 @@ +// RUN: %dafny /compile:3 /rprint:"%t.rprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +datatype Cell = Cell(x: int) +type EvenCell = c: Cell | c.x % 2 == 0 witness Cell(0) + +function method doubleEvenCell(f: EvenCell): int +{ + if f.x % 2 == 1 then 1/0 else f.x * 2 +} + +method Main() { + var x: set := { Cell(1), Cell(2), Cell(3), Cell(4) }; + var b: bool := forall g :: g in x ==> doubleEvenCell(g) > 0; + assert b; +} + From 1076022e362c2f5da96d43a98126933c7f774b6e Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 2 Nov 2021 10:09:18 -0500 Subject: [PATCH 09/27] Fixed soundness, but now it does not allow non-compilable guards. --- Source/Dafny/Compilers/Compiler.cs | 16 ++++++++++------ Test/git-issues/git-issue-697e.dfy.expect | 2 ++ 2 files changed, 12 insertions(+), 6 deletions(-) create mode 100644 Test/git-issues/git-issue-697e.dfy.expect diff --git a/Source/Dafny/Compilers/Compiler.cs b/Source/Dafny/Compilers/Compiler.cs index dcb698693c2..1d64a70682c 100644 --- a/Source/Dafny/Compilers/Compiler.cs +++ b/Source/Dafny/Compilers/Compiler.cs @@ -4610,8 +4610,7 @@ void writeObj(ConcreteSyntaxTree w) { wBody.Write(", {0}, ", expr is ForallExpr ? "true" : "false"); var native = AsNativeType(e.BoundVars[i].Type); ConcreteSyntaxTree newWBody = CreateLambda(new List { bv.Type }, e.tok, new List { IdName(bv) }, Type.Bool, wBody, untyped: true); - newWBody = EmitReturnExpr(newWBody); - // TODO: Here we should emit the guard for the exists and forall expressions. + newWBody = MaybeInjectSubsetConstraint(newWBody, inLetExprBody, e.BoundVars[i], e, true, e is ForallExpr); wBody.Write(')'); wBody = newWBody; } @@ -4742,7 +4741,7 @@ void writeObj(ConcreteSyntaxTree w) { } private ConcreteSyntaxTree MaybeInjectSubsetConstraint(ConcreteSyntaxTree wr, bool inLetExprBody, BoundVar bv, - Expression e) { + Expression e, bool isReturning = false, bool elseReturnValue = false) { int i; if (bv.Type is UserDefinedType { @@ -4758,12 +4757,10 @@ var subsetTypeDecl and } }) { var bvIdentifier = new IdentifierExpr(e.tok, bv); - wr = EmitIf(out var guardWriterInner, false, wr); var typeParameters = new Dictionary { }; for (i = 0; i < typeParametersArgs.Count(); i++) { typeParameters[typeParametersArgs[i]] = typeArgs[i]; } - var subContract = new Substituter(null, new Dictionary() { @@ -4774,7 +4771,14 @@ var subsetTypeDecl and ) ); var constraintInContext = subContract.Substitute(constraint); - TrExpr(constraintInContext, guardWriterInner, inLetExprBody); + var thenWriter = EmitIf(out var guardWriter, isReturning, wr); + TrExpr(constraintInContext, guardWriter, inLetExprBody); + if (isReturning) { + wr = EmitReturnExpr(wr); + TrExpr(new LiteralExpr(e.tok, elseReturnValue), wr, inLetExprBody); + thenWriter = EmitReturnExpr(thenWriter); + } + wr = thenWriter; } return wr; diff --git a/Test/git-issues/git-issue-697e.dfy.expect b/Test/git-issues/git-issue-697e.dfy.expect new file mode 100644 index 00000000000..00a51f822da --- /dev/null +++ b/Test/git-issues/git-issue-697e.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 3 verified, 0 errors From e4d1938b2b03a6b82c041e825c00cf5d173b69e2 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 2 Nov 2021 16:27:04 -0500 Subject: [PATCH 10/27] Support for ghost in subset constraints if not used in comprehensions --- Source/Dafny/Resolver.cs | 22 +++++++++++++++++----- Test/git-issues/git-issue-697c.dfy | 1 + Test/git-issues/git-issue-697c.dfy.expect | 8 ++++++-- Test/git-issues/git-issue-697f.dfy | 23 +++++++++++++++++++++++ Test/git-issues/git-issue-697f.dfy.expect | 3 +++ 5 files changed, 50 insertions(+), 7 deletions(-) create mode 100644 Test/git-issues/git-issue-697f.dfy create mode 100644 Test/git-issues/git-issue-697f.dfy.expect diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 062d627adff..f2f4278043e 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -2677,11 +2677,7 @@ public void ResolveTopLevelDecls_Core(List/*!*/ declarations, if (!CheckTypeInference_Visitor.IsDetermined(dd.Rhs.NormalizeExpand())) { reporter.Error(MessageSource.Resolver, dd.tok, "subset type's base type is not fully determined; add an explicit type for '{0}'", dd.Var.Name); } - dd.ConstraintIsCompilable = ExpressionTester.CheckIsCompilable(this, dd.Constraint, new CodeContextWrapper(dd, true)); - if (!dd.ConstraintIsCompilable) { - reporter.Error(MessageSource.Resolver, dd.Constraint.tok, - "subset type's constraint must be compilable, until Dafny moves constraints handling to the verifier."); - } + dd.ConstraintIsCompilable = ExpressionTester.CheckIsCompilable(null, dd.Constraint, new CodeContextWrapper(dd, true)); scope.PopMarker(); allTypeParameters.PopMarker(); @@ -6649,6 +6645,22 @@ protected override void VisitOneExpr(Expression expr) { } else { Contract.Assume(e is LambdaExpr); // otherwise, unexpected ComprehensionExpr } + foreach (var boundVar in e.BoundVars) { + if (boundVar.Type is UserDefinedType + { + ResolvedClass: var subsetTypeDecl and SubsetTypeDecl + { + Constraint: var constraint, + ConstraintIsCompilable: false + } + } + ) { + // Explicitely report the error + this.resolver.getReporter().Error(MessageSource.Resolver, boundVar.tok, + "subset type's constraint is not compilable, hence it cannot yet be used as the type of a bound variable in " + what + ". The next error will explain why the constraint is not compilable."); + ExpressionTester.CheckIsCompilable(this.resolver, constraint, new CodeContextWrapper((subsetTypeDecl as SubsetTypeDecl), true)); + } + } if (whereToLookForBounds != null) { e.Bounds = DiscoverBestBounds_MultipleVars_AllowReordering(e.BoundVars, whereToLookForBounds, polarity, ComprehensionExpr.BoundedPool.PoolVirtues.None); if (2 <= DafnyOptions.O.Allocated && (codeContext is Function || codeContext is ConstantField || CodeContextWrapper.Unwrap(codeContext) is RedirectingTypeDecl)) { diff --git a/Test/git-issues/git-issue-697c.dfy b/Test/git-issues/git-issue-697c.dfy index 4d8c4d95aad..cf16c8cc66f 100644 --- a/Test/git-issues/git-issue-697c.dfy +++ b/Test/git-issues/git-issue-697c.dfy @@ -16,6 +16,7 @@ function method doubleEvenCell(c: EvenCell): int method Main() { var x: set := { Cell(1), Cell(2), Cell(3), Cell(4) }; var y := set c: EvenCell | c in x; + var z: map := map c: EvenCell | c in x :: c.x; var b: bool := forall c :: c in y ==> doubleEvenCell(c) > 0; assert b; print(b); diff --git a/Test/git-issues/git-issue-697c.dfy.expect b/Test/git-issues/git-issue-697c.dfy.expect index ddf38868367..15b93d6806f 100644 --- a/Test/git-issues/git-issue-697c.dfy.expect +++ b/Test/git-issues/git-issue-697c.dfy.expect @@ -1,3 +1,7 @@ +git-issue-697c.dfy(18,15): Error: subset type's constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension. The next error will explain why the constraint is not compilable. git-issue-697c.dfy(9,26): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method') -git-issue-697c.dfy(9,40): Error: subset type's constraint must be compilable, until Dafny moves constraints handling to the verifier. -2 resolution/type errors detected in git-issue-697c.dfy +git-issue-697c.dfy(19,35): Error: subset type's constraint is not compilable, hence it cannot yet be used as the type of a bound variable in map comprehension. The next error will explain why the constraint is not compilable. +git-issue-697c.dfy(9,26): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method') +git-issue-697c.dfy(20,24): Error: subset type's constraint is not compilable, hence it cannot yet be used as the type of a bound variable in quantifier. The next error will explain why the constraint is not compilable. +git-issue-697c.dfy(9,26): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method') +6 resolution/type errors detected in git-issue-697c.dfy diff --git a/Test/git-issues/git-issue-697f.dfy b/Test/git-issues/git-issue-697f.dfy new file mode 100644 index 00000000000..2fd4c835411 --- /dev/null +++ b/Test/git-issues/git-issue-697f.dfy @@ -0,0 +1,23 @@ +// RUN: %dafny /compile:3 /rprint:"%t.rprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function ghostPredicate(x: int): bool { + x % 2 == 0 +} + +datatype Cell = Cell(x: int) +type EvenCell = c: Cell | ghostPredicate(c.x) witness Cell(0) + +function method doubleEvenCell(c: EvenCell): int +{ + if c.x % 2 == 1 then 1/0 else c.x * 2 +} + +// No need for the subset constraint to be compilable. +method Main() { + var a: EvenCell := Cell(2); + if doubleEvenCell(a) > 0 { + print "ok"; + } +} + diff --git a/Test/git-issues/git-issue-697f.dfy.expect b/Test/git-issues/git-issue-697f.dfy.expect new file mode 100644 index 00000000000..3e2cf8d0f69 --- /dev/null +++ b/Test/git-issues/git-issue-697f.dfy.expect @@ -0,0 +1,3 @@ + +Dafny program verifier finished with 4 verified, 0 errors +ok \ No newline at end of file From c9a8e0432223686af37d69bcfae492ebecaef82a Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Wed, 3 Nov 2021 09:39:29 -0500 Subject: [PATCH 11/27] Fixed the merge --- Source/Dafny/Resolver.cs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 33e6987d6cf..1ef5d7a6b47 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -8737,11 +8737,11 @@ private void CheckAssignStmt(AssignStmt s, bool mustBeErasable, [CanBeNull] stri } else if (s.Rhs is TypeRhs tRhs) { if (tRhs.InitCall != null && tRhs.InitCall.Method.IsGhost) { autoGhostIdExpr.Var.MakeGhost(); - } else if (tRhs.ArrayDimensions != null && tRhs.ArrayDimensions.Exists(resolver.UsesSpecFeatures)) { + } else if (tRhs.ArrayDimensions != null && tRhs.ArrayDimensions.Exists(ExpressionTester.UsesSpecFeatures)) { autoGhostIdExpr.Var.MakeGhost(); - } else if (tRhs.ElementInit != null && resolver.UsesSpecFeatures(tRhs.ElementInit)) { + } else if (tRhs.ElementInit != null && ExpressionTester.UsesSpecFeatures(tRhs.ElementInit)) { autoGhostIdExpr.Var.MakeGhost(); - } else if (tRhs.InitDisplay != null && tRhs.InitDisplay.Any(resolver.UsesSpecFeatures)) { + } else if (tRhs.InitDisplay != null && tRhs.InitDisplay.Any(ExpressionTester.UsesSpecFeatures)) { autoGhostIdExpr.Var.MakeGhost(); } } From c6d47e9f964c2a13c184f7ec2491bfb433d60e54 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 5 Nov 2021 11:48:51 -0500 Subject: [PATCH 12/27] Fix should not apply for lambdas, which are special "comprehensions" --- Source/Dafny/Resolver.cs | 24 +++++++++++++----------- 1 file changed, 13 insertions(+), 11 deletions(-) diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 1ef5d7a6b47..c0a90085aa1 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -6645,20 +6645,22 @@ protected override void VisitOneExpr(Expression expr) { } else { Contract.Assume(e is LambdaExpr); // otherwise, unexpected ComprehensionExpr } - foreach (var boundVar in e.BoundVars) { - if (boundVar.Type is UserDefinedType - { - ResolvedClass: var subsetTypeDecl and SubsetTypeDecl + if (what != null) { + foreach (var boundVar in e.BoundVars) { + if (boundVar.Type is UserDefinedType { - Constraint: var constraint, - ConstraintIsCompilable: false + ResolvedClass: var subsetTypeDecl and SubsetTypeDecl + { + Constraint: var constraint, + ConstraintIsCompilable: false + } } + ) { + // Explicitely report the error + this.resolver.getReporter().Error(MessageSource.Resolver, boundVar.tok, + "subset type's constraint is not compilable, hence it cannot yet be used as the type of a bound variable in " + what + ". The next error will explain why the constraint is not compilable."); + ExpressionTester.CheckIsCompilable(this.resolver, constraint, new CodeContextWrapper((subsetTypeDecl as SubsetTypeDecl), true)); } - ) { - // Explicitely report the error - this.resolver.getReporter().Error(MessageSource.Resolver, boundVar.tok, - "subset type's constraint is not compilable, hence it cannot yet be used as the type of a bound variable in " + what + ". The next error will explain why the constraint is not compilable."); - ExpressionTester.CheckIsCompilable(this.resolver, constraint, new CodeContextWrapper((subsetTypeDecl as SubsetTypeDecl), true)); } } if (whereToLookForBounds != null) { From 8bb47462acb4adcd0c4144bfb77de4e6ee055ada Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 5 Nov 2021 14:02:05 -0500 Subject: [PATCH 13/27] Error message only in non-ghost context. More explicit error message about what is the type that is subset. --- Source/Dafny/Resolver.cs | 4 ++-- Test/git-issues/git-issue-697c.dfy.expect | 6 +++--- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index c0a90085aa1..92339d8dddb 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -6645,7 +6645,7 @@ protected override void VisitOneExpr(Expression expr) { } else { Contract.Assume(e is LambdaExpr); // otherwise, unexpected ComprehensionExpr } - if (what != null) { + if (!codeContext.IsGhost && what != null) { foreach (var boundVar in e.BoundVars) { if (boundVar.Type is UserDefinedType { @@ -6658,7 +6658,7 @@ protected override void VisitOneExpr(Expression expr) { ) { // Explicitely report the error this.resolver.getReporter().Error(MessageSource.Resolver, boundVar.tok, - "subset type's constraint is not compilable, hence it cannot yet be used as the type of a bound variable in " + what + ". The next error will explain why the constraint is not compilable."); + boundVar.Type + " is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in " + what + ". The next error will explain why the constraint is not compilable."); ExpressionTester.CheckIsCompilable(this.resolver, constraint, new CodeContextWrapper((subsetTypeDecl as SubsetTypeDecl), true)); } } diff --git a/Test/git-issues/git-issue-697c.dfy.expect b/Test/git-issues/git-issue-697c.dfy.expect index 15b93d6806f..95a30cae8c0 100644 --- a/Test/git-issues/git-issue-697c.dfy.expect +++ b/Test/git-issues/git-issue-697c.dfy.expect @@ -1,7 +1,7 @@ -git-issue-697c.dfy(18,15): Error: subset type's constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension. The next error will explain why the constraint is not compilable. +git-issue-697c.dfy(18,15): Error: EvenCell is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension. The next error will explain why the constraint is not compilable. git-issue-697c.dfy(9,26): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method') -git-issue-697c.dfy(19,35): Error: subset type's constraint is not compilable, hence it cannot yet be used as the type of a bound variable in map comprehension. The next error will explain why the constraint is not compilable. +git-issue-697c.dfy(19,35): Error: EvenCell is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in map comprehension. The next error will explain why the constraint is not compilable. git-issue-697c.dfy(9,26): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method') -git-issue-697c.dfy(20,24): Error: subset type's constraint is not compilable, hence it cannot yet be used as the type of a bound variable in quantifier. The next error will explain why the constraint is not compilable. +git-issue-697c.dfy(20,24): Error: EvenCell is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in quantifier. The next error will explain why the constraint is not compilable. git-issue-697c.dfy(9,26): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method') 6 resolution/type errors detected in git-issue-697c.dfy From 856e38c3cfd11d1d4e6b52fbb539924523aa9a35 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 5 Nov 2021 16:19:47 -0500 Subject: [PATCH 14/27] Check if the constraint is compilable if not already done. --- Source/Dafny/AST/DafnyAst.cs | 1 + Source/Dafny/Resolver.cs | 23 ++++++++++++++++------- 2 files changed, 17 insertions(+), 7 deletions(-) diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/DafnyAst.cs index 2476faaa72d..65acc2ea176 100644 --- a/Source/Dafny/AST/DafnyAst.cs +++ b/Source/Dafny/AST/DafnyAst.cs @@ -5704,6 +5704,7 @@ public enum WKind { CompiledZero, Compiled, Ghost, OptOut, Special } public readonly SubsetTypeDecl.WKind WitnessKind; public readonly Expression/*?*/ Witness; // non-null iff WitnessKind is Compiled or Ghost public bool ConstraintIsCompilable = false; // Will be resolved later. + public bool CheckedIfConstraintIsCompilable = false; // Will be resolved later. public SubsetTypeDecl(IToken tok, string name, TypeParameter.TypeParameterCharacteristics characteristics, List typeArgs, ModuleDefinition module, BoundVar id, Expression constraint, WKind witnessKind, Expression witness, Attributes attributes) diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 92339d8dddb..91326a7f09b 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -2678,6 +2678,7 @@ public void ResolveTopLevelDecls_Core(List/*!*/ declarations, reporter.Error(MessageSource.Resolver, dd.tok, "subset type's base type is not fully determined; add an explicit type for '{0}'", dd.Var.Name); } dd.ConstraintIsCompilable = ExpressionTester.CheckIsCompilable(null, dd.Constraint, new CodeContextWrapper(dd, true)); + dd.CheckedIfConstraintIsCompilable = true; scope.PopMarker(); allTypeParameters.PopMarker(); @@ -6649,17 +6650,25 @@ protected override void VisitOneExpr(Expression expr) { foreach (var boundVar in e.BoundVars) { if (boundVar.Type is UserDefinedType { - ResolvedClass: var subsetTypeDecl and SubsetTypeDecl + ResolvedClass: SubsetTypeDecl { Constraint: var constraint, - ConstraintIsCompilable: false - } + ConstraintIsCompilable: false and var constraintIsCompilable + } and var subsetTypeDecl } ) { - // Explicitely report the error - this.resolver.getReporter().Error(MessageSource.Resolver, boundVar.tok, - boundVar.Type + " is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in " + what + ". The next error will explain why the constraint is not compilable."); - ExpressionTester.CheckIsCompilable(this.resolver, constraint, new CodeContextWrapper((subsetTypeDecl as SubsetTypeDecl), true)); + if (!subsetTypeDecl.CheckedIfConstraintIsCompilable) { + // Builtin types were never resolved. + constraintIsCompilable = ExpressionTester.CheckIsCompilable(null, constraint, new CodeContextWrapper(subsetTypeDecl, true)); + subsetTypeDecl.CheckedIfConstraintIsCompilable = true; + subsetTypeDecl.ConstraintIsCompilable = constraintIsCompilable; + } + if (!constraintIsCompilable) { + // Explicitely report the error + this.resolver.getReporter().Error(MessageSource.Resolver, boundVar.tok, + boundVar.Type + " is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in " + what + ". The next error will explain why the constraint is not compilable."); + ExpressionTester.CheckIsCompilable(this.resolver, constraint, new CodeContextWrapper(subsetTypeDecl, true)); + } } } } From f5392112eee0edd3ffdf6a77dde978a7020e9cae Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 9 Nov 2021 12:36:11 -0600 Subject: [PATCH 15/27] Added the return expression if no subset type in forall. --- Source/Dafny/Compilers/Compiler.cs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Source/Dafny/Compilers/Compiler.cs b/Source/Dafny/Compilers/Compiler.cs index c414aa232b3..f486a3ab9dd 100644 --- a/Source/Dafny/Compilers/Compiler.cs +++ b/Source/Dafny/Compilers/Compiler.cs @@ -4779,6 +4779,8 @@ var subsetTypeDecl and thenWriter = EmitReturnExpr(thenWriter); } wr = thenWriter; + } else if (isReturning) { + wr = EmitReturnExpr(wr); } return wr; From a3f8a6e1e825eb19c8daa535116a2cbd96c734d2 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 9 Nov 2021 13:45:54 -0600 Subject: [PATCH 16/27] fix: tolerate traversing sub-expressions when checking compilability. --- Source/Dafny/Util.cs | 8 -------- 1 file changed, 8 deletions(-) diff --git a/Source/Dafny/Util.cs b/Source/Dafny/Util.cs index c014b275655..c445032a437 100644 --- a/Source/Dafny/Util.cs +++ b/Source/Dafny/Util.cs @@ -581,22 +581,14 @@ private bool CheckIsCompilable(Expression expr, ICodeContext codeContext) { case BinaryExpr.ResolvedOpcode.RankLt: reporter?.Error(MessageSource.Resolver, binaryExpr, "rank comparisons are allowed only in specification and ghost contexts"); return false; - default: - break; } - - return true; } else if (expr is TernaryExpr ternaryExpr) { switch (ternaryExpr.Op) { case TernaryExpr.Opcode.PrefixEqOp: case TernaryExpr.Opcode.PrefixNeqOp: reporter?.Error(MessageSource.Resolver, ternaryExpr, "prefix equalities are allowed only in specification and ghost contexts"); return false; - default: - break; } - - return true; } else if (expr is LetExpr letExpr) { if (letExpr.Exact) { Contract.Assert(letExpr.LHSs.Count == letExpr.RHSs.Count); From 8516e32e6fa2f50ae0fe586abff247707095ea41 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 9 Nov 2021 16:44:47 -0600 Subject: [PATCH 17/27] Default value for IsGhost for top-level declarations. --- Source/Dafny/AST/DafnyAst.cs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/DafnyAst.cs index 65acc2ea176..1b10af5f2df 100644 --- a/Source/Dafny/AST/DafnyAst.cs +++ b/Source/Dafny/AST/DafnyAst.cs @@ -5573,7 +5573,7 @@ public TypeParameter.EqualitySupportValue EqualitySupport { FreshIdGenerator RedirectingTypeDecl.IdGenerator { get { return IdGenerator; } } bool ICodeContext.IsGhost { - get { throw new NotSupportedException(); } // if .IsGhost is needed, the object should always be wrapped in an CodeContextWrapper + get { return false; } } List ICodeContext.TypeArgs { get { return new List(); } } List ICodeContext.Ins { get { return new List(); } } @@ -5656,7 +5656,7 @@ public Type RhsWithArgumentIgnoringScope(List typeArgs) { FreshIdGenerator RedirectingTypeDecl.IdGenerator { get { return IdGenerator; } } bool ICodeContext.IsGhost { - get { throw new NotSupportedException(); } // if .IsGhost is needed, the object should always be wrapped in an CodeContextWrapper + get { return false; } } List ICodeContext.TypeArgs { get { return TypeArgs; } } List ICodeContext.Ins { get { return new List(); } } From 447a93d53ad0e33b68de119392d3f45dbf1e01b4 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Wed, 10 Nov 2021 14:47:47 -0600 Subject: [PATCH 18/27] Enhancement: MissingBounds works even if bounds were never defined. Ensures that CheckIsCompilable does not try to report errors if no resolver is provided. --- Source/Dafny/AST/DafnyAst.cs | 5 ++--- Source/Dafny/Util.cs | 2 +- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/DafnyAst.cs index 1b10af5f2df..2b75b1c39a7 100644 --- a/Source/Dafny/AST/DafnyAst.cs +++ b/Source/Dafny/AST/DafnyAst.cs @@ -11203,12 +11203,11 @@ public static BoundedPool GetBest(List bounds, PoolVirtues required } public static List MissingBounds(List vars, List bounds, PoolVirtues requiredVirtues = PoolVirtues.None) where VT : IVariable { Contract.Requires(vars != null); - Contract.Requires(bounds != null); - Contract.Requires(vars.Count == bounds.Count); + Contract.Requires(bounds == null || vars.Count == bounds.Count); Contract.Ensures(Contract.Result>() != null); var missing = new List(); for (var i = 0; i < vars.Count; i++) { - if (bounds[i] == null || (bounds[i].Virtues & requiredVirtues) != requiredVirtues) { + if (bounds == null || bounds[i] == null || (bounds[i].Virtues & requiredVirtues) != requiredVirtues) { missing.Add(vars[i]); } } diff --git a/Source/Dafny/Util.cs b/Source/Dafny/Util.cs index c445032a437..0f61ae15757 100644 --- a/Source/Dafny/Util.cs +++ b/Source/Dafny/Util.cs @@ -483,7 +483,7 @@ public ExpressionTester(Resolver resolver = null, bool reportErrors = false) { // Static call to CheckIsCompilable public static bool CheckIsCompilable(Resolver resolver, Expression expr, ICodeContext codeContext) { - return new ExpressionTester(resolver, true).CheckIsCompilable(expr, codeContext); + return new ExpressionTester(resolver, resolver != null).CheckIsCompilable(expr, codeContext); } /// From 8793edbcf23dd49b73ee1afb4c42493be3ce0958 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Mon, 15 Nov 2021 13:57:15 -0600 Subject: [PATCH 19/27] Newest way to verify subset constraint --- Source/Dafny/Resolver.cs | 114 +++++++++++++++----- Source/Dafny/Util.cs | 218 +++++++++++++++++++++++++++++++++++++++ 2 files changed, 306 insertions(+), 26 deletions(-) diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index d60362ef25e..8a0a3acd9c9 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -2900,8 +2900,22 @@ public void ResolveTopLevelDecls_Core(List/*!*/ declarations, // ---------------------------------- Pass 2 ---------------------------------- // This pass fills in various additional information. + // * Subset type in comprehensions have a compilable constraint + // * Postconditions and bodies of prefix lemmas + // * Compute postconditions and statement body of prefix lemmas + // * Perform the stratosphere check on inductive datatypes, and compute to what extent the inductive datatypes require equality support + // * Set the SccRepr field of codatatypes + // * Perform the guardedness check on co-datatypes + // * Do datatypes and type synonyms until a fixpoint is reached, same for functions and methods + // * Check that functions claiming to be abstemious really are + // * Check that all == and != operators in non-ghost contexts are applied to equality-supporting types. + // * Extreme predicate recursivity checks + // * Verify that subset constraints are compilable if necessary // ---------------------------------------------------------------------------- + // Verifies that, in all compiled places, subset types in comprehensions have a compilable constraint + new SubsetConstraintGhostChecker(this).Traverse(declarations); + if (reporter.Count(ErrorLevel.Error) == prevErrorCount) { // fill in the postconditions and bodies of prefix lemmas foreach (var com in ModuleDefinition.AllExtremeLemmas(declarations)) { @@ -6646,32 +6660,6 @@ protected override void VisitOneExpr(Expression expr) { } else { Contract.Assume(e is LambdaExpr); // otherwise, unexpected ComprehensionExpr } - if (!codeContext.IsGhost && what != null) { - foreach (var boundVar in e.BoundVars) { - if (boundVar.Type is UserDefinedType - { - ResolvedClass: SubsetTypeDecl - { - Constraint: var constraint, - ConstraintIsCompilable: false and var constraintIsCompilable - } and var subsetTypeDecl - } - ) { - if (!subsetTypeDecl.CheckedIfConstraintIsCompilable) { - // Builtin types were never resolved. - constraintIsCompilable = ExpressionTester.CheckIsCompilable(null, constraint, new CodeContextWrapper(subsetTypeDecl, true)); - subsetTypeDecl.CheckedIfConstraintIsCompilable = true; - subsetTypeDecl.ConstraintIsCompilable = constraintIsCompilable; - } - if (!constraintIsCompilable) { - // Explicitely report the error - this.resolver.getReporter().Error(MessageSource.Resolver, boundVar.tok, - boundVar.Type + " is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in " + what + ". The next error will explain why the constraint is not compilable."); - ExpressionTester.CheckIsCompilable(this.resolver, constraint, new CodeContextWrapper(subsetTypeDecl, true)); - } - } - } - } if (whereToLookForBounds != null) { e.Bounds = DiscoverBestBounds_MultipleVars_AllowReordering(e.BoundVars, whereToLookForBounds, polarity, ComprehensionExpr.BoundedPool.PoolVirtues.None); if (2 <= DafnyOptions.O.Allocated && (codeContext is Function || codeContext is ConstantField || CodeContextWrapper.Unwrap(codeContext) is RedirectingTypeDecl)) { @@ -18299,4 +18287,78 @@ public bool ContainsDecl(Thing t) { return things.Exists(thing => thing == t); } } + + + // Looks for every non-ghost comprehensions, and if they are using a subset type, + // check that the subset constraint is compilable. If it is not compilable, raises an error. + public class SubsetConstraintGhostChecker : ProgramTraverser { + public Resolver resolver; + + public SubsetConstraintGhostChecker(Resolver resolver) { + this.resolver = resolver; + } + + protected override ContinuationStatus OnEnter(Statement stmt, string field, object parent) { + return stmt.IsGhost ? skip : ok; + } + + protected override ContinuationStatus OnEnter(MemberDecl memberDecl, string field, object parent) { + // Includes functions and methods as well. + // Ghost functions can have a compiled implementation. + // We want to recurse only on the by method, not on the sub expressions of the function + if (!memberDecl.IsGhost) return ok; + if (memberDecl is Function f) { + if (Traverse(f.ByMethodDecl, "ByMethodDecl", f)) return stop; + if (f.ByMethodDecl.Body != f.ByMethodBody) { + if (Traverse(f.ByMethodBody, "ByMethodBody", f)) return stop; + } + } + return skip; + } + + public override bool Traverse(Expression expr, [CanBeNull] string field, [CanBeNull] object parent) { + // Since we skipped ghost code, the code has to be compiled here. + if (expr is not QuantifierExpr e) { + return base.Traverse(expr, field, parent); + } + + string what; + if (e is ForallExpr) { + what = "forall expressions"; + } else if (e is ExistsExpr) { + what = "exists expression"; + } else if (e is SetComprehension) { + what = "set comprehension"; + } else if (e is MapComprehension) { + what = "map comprehension"; + } else { + what = "quantifier"; + } + foreach (var boundVar in e.BoundVars) { + if (boundVar.Type is UserDefinedType + { + ResolvedClass: SubsetTypeDecl + { + Constraint: var constraint, + ConstraintIsCompilable: false and var constraintIsCompilable + } and var subsetTypeDecl + } + ) { + if (!subsetTypeDecl.CheckedIfConstraintIsCompilable) { + // Builtin types were never resolved. + constraintIsCompilable = ExpressionTester.CheckIsCompilable(null, constraint, new CodeContextWrapper(subsetTypeDecl, true)); + subsetTypeDecl.CheckedIfConstraintIsCompilable = true; + subsetTypeDecl.ConstraintIsCompilable = constraintIsCompilable; + } + if (!constraintIsCompilable) { + // Explicitely report the error + this.resolver.getReporter().Error(MessageSource.Resolver, boundVar.tok, + boundVar.Type + " is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in " + what + ". The next error will explain why the constraint is not compilable."); + ExpressionTester.CheckIsCompilable(this.resolver, constraint, new CodeContextWrapper(subsetTypeDecl, true)); + } + } + } + return base.Traverse(e, field, parent); + } + } } diff --git a/Source/Dafny/Util.cs b/Source/Dafny/Util.cs index 0f61ae15757..50c7a9889ba 100644 --- a/Source/Dafny/Util.cs +++ b/Source/Dafny/Util.cs @@ -3,11 +3,13 @@ using System; using System.Collections.Generic; +using System.ComponentModel.Design.Serialization; using System.Linq; using System.Text; using System.Diagnostics.Contracts; using JetBrains.Annotations; using Microsoft.Boogie; +using Microsoft.Dafny.Triggers; namespace Microsoft.Dafny { @@ -466,6 +468,222 @@ public int GetHashCode(IEnumerable obj) { } } + // Class to traverse a program top-down, especially aimed at identifying expressions and statements, + // and in their context + // How to use: + // - Define a subclass of ProgramTraverser + // - Implement the methods (TopDown|BottomUp)(Enter|Exit), override Traverse if needed. + // - Call any Traverse() method. + public class ProgramTraverser { + public enum ContinuationStatus { + Ok, // Continue exploration + Skip, // Skip this node and its descendants (valid only on entering a node) + Stop, // Stop the entire traversal here, but traverse ancestors in bottom-up + } + protected const ContinuationStatus ok = ContinuationStatus.Ok; + protected const ContinuationStatus skip = ContinuationStatus.Skip; + protected const ContinuationStatus stop = ContinuationStatus.Stop; + // Returns true if statement needs to be traversed + protected virtual ContinuationStatus OnEnter(Statement stmt, [CanBeNull] string field, [CanBeNull] object parent) { + return ok; + } + // Returns true if expression needs to be traversed + protected virtual ContinuationStatus OnEnter(Expression expr, [CanBeNull] string field, [CanBeNull] object parent) { + return ok; + } + + // Returns true if need to stop the traversal entirely + protected virtual bool OnExit(Statement stmt, [CanBeNull] string field, [CanBeNull] object parent) { + return false; + } + // Returns true if need to stop the traversal entirely + protected virtual bool OnExit(Expression expr, [CanBeNull] string field, [CanBeNull] object parent) { + return false; + } + + protected virtual ContinuationStatus OnEnter(MemberDecl memberDecl, [CanBeNull] string field, [CanBeNull] object parent) { + return ok; + } + + // Traverse methods retun true to interrupt. + public bool Traverse(Program program) { + return program.Modules().Any(Traverse); + } + + public bool Traverse(ModuleDefinition moduleDefinition) { + return Traverse(moduleDefinition.TopLevelDecls); + } + + public bool Traverse(List topLevelDecls) { + return topLevelDecls.Any(Traverse); + } + + public bool Traverse(ModuleDecl moduleDecl) { + if (moduleDecl is LiteralModuleDecl l) { + return Traverse(l.ModuleDef); + } else if (moduleDecl is AbstractModuleDecl a) { + return Traverse(a.CompileRoot); + }/* else if (moduleDecl is AliasModuleDecl a) { + + } else if (moduleDecl is ModuleExportDecl m) { + + }*/ + + return false; + } + + public bool Traverse(Formal formal) { + if (formal.DefaultValue != null && Traverse(formal.DefaultValue, "DefaultValue", formal)) { + return true; + } + + return false; + } + + public bool Traverse(DatatypeCtor ctor) { + if (ctor.Formals.Any(Traverse)) { + return true; + } + + return false; + } + + public bool Traverse(TopLevelDecl topd) { + var d = topd is ClassDecl classDecl ? classDecl.NonNullTypeDecl : topd; + + if (d is TopLevelDeclWithMembers tdm) { + // ClassDecl, DatatypeDecl, OpaqueTypeDecl, NewtypeDecl + if (tdm.Members.Any(memberDecl => Traverse(memberDecl, "Members", tdm))) { + return true; + } + + if (tdm is IteratorDecl iter) { + // TODO: Import this + if (Attributes.SubExpressions(iter.Attributes).Any(e => Traverse(e, "Attributes.SubExpressions", iter))) { + return true; + } + if (Attributes.SubExpressions(iter.Reads.Attributes).Any(e => Traverse(e, "Reads.Attributes.SubExpressions", iter))) { + return true; + } + if (iter.Reads.Expressions.Any(e => Traverse(e.E, "Reads.Expressions.E", iter))) { + return true; + } + if (Attributes.SubExpressions(iter.Modifies.Attributes).Any(e => Traverse(e, "Modifies.Attributes.SubExpressions", iter))) { + return true; + } + if (iter.Modifies.Expressions.Any(e => Traverse(e.E, "Modifies.Expressions.E", iter))) { + return true; + } + if (Attributes.SubExpressions(iter.Decreases.Attributes).Any(e => Traverse(e, "Decreases.Attributes.SubExpressions", iter))) { + return true; + } + if (iter.Decreases.Expressions.Any(e => Traverse(e, "Decreases.Expressions.E", iter))) { + return true; + } + if (iter.Requires.Any(e => Traverse(e.E, "Requires.E", iter))) { + return true; + } + if (iter.Ensures.Any(e => Traverse(e.E, "Ensures.E", iter))) { + return true; + } + if (iter.YieldRequires.Any(e => Traverse(e.E, "YieldRequires.E", iter))) { + return true; + } + if (iter.YieldEnsures.Any(e => Traverse(e.E, "YieldEnsures.E", iter))) { + return true; + } + if (Traverse(iter.Body, "Body", iter)) return true; + } + + if (tdm is DatatypeDecl dtd) { + if (dtd.Ctors.Any(Traverse)) { + return true; + } + } + } else if (d is ModuleDecl md) { + return Traverse(md); + } else if (d is ValuetypeDecl vd) { + if (vd.Members.Any(pair => Traverse(pair.Value, "Members.Value", vd))) { + return true; + } + } else if (d is TypeSynonymDecl tsd) { + // Nothing here. + } + + return false; + } + + public bool Traverse(MemberDecl memberDeclaration, [CanBeNull] string field, [CanBeNull] object parent) { + var enterResult = OnEnter(memberDeclaration, field, parent); + if (enterResult is stop or skip) return enterResult == stop; + if (memberDeclaration is Field fi) { + if (fi.SubExpressions.Any(expr => Traverse(expr, "SubExpressions", fi))) { + return true; + } + } else if (memberDeclaration is Function f) { + if (f.Formals.Any(Traverse)) { + return true; + } + if (f.Result.DefaultValue != null && Traverse(f.Result.DefaultValue, "Result.DefaultValue", f)) { + return true; + } + if (f.Req.Any(e => Traverse(e.E, "Req.E", f))) { + return true; + } + if (f.Reads.Any(e => Traverse(e.E, "Reads.E", f))) { + return true; + } + if (f.Ens.Any(e => Traverse(e.E, "Ens.E", f))) { + return true; + } + if (f.Decreases.Expressions.Any(e => Traverse(e, "Decreases.Expressions", f))) { + return true; + } + if (Traverse(f.Body, "Body", f)) return true; + if (Traverse(f.ByMethodDecl, "ByMethodDecl", f)) return true; + if (f.ByMethodDecl.Body != f.ByMethodBody) { + if (Traverse(f.ByMethodBody, "ByMethodBody", f)) return true; + } + } else if (memberDeclaration is Method m) { + // For example, default value of formals is non-ghost + if (m.Ins.Any(formal => formal.DefaultValue != null + && Traverse(formal.DefaultValue, "Ins.DefaultValue", m))) { + return true; + } + if (m.Req.Any(e => Traverse(e.E, "Req.E", m))) { + return true; + } + if (m.Mod.Expressions.Any(e => Traverse(e.E, "Mod.E", m) == true)) { + return true; + } + if (m.Ens.Any(e => Traverse(e.E, "Ens.E", m))) { + return true; + } + if (m.Decreases.Expressions.Any(e => Traverse(e, "Decreases.Expressions", m))) { + return true; + } + if (Traverse(m.Body, "Body", m)) return true; + } + + return false; + } + + public virtual bool Traverse(Statement stmt, [CanBeNull] string field, [CanBeNull] object parent) { + var enterResult = OnEnter(stmt, field, parent); + if (enterResult is stop or skip) return enterResult == stop; + return stmt.SubStatements.Any(subStmt => Traverse(subStmt, "SubStatements", stmt)) || + stmt.SubExpressions.Any(subExpr => Traverse(subExpr, "SubExpressions", stmt)) || + OnExit(stmt, field, parent); + } + + public virtual bool Traverse(Expression expr, [CanBeNull] string field, [CanBeNull] object parent) { + var enterResult = OnEnter(expr, field, parent); + if (enterResult is stop or skip) return enterResult == stop; + return expr.SubExpressions.Any(subExpr => Traverse(subExpr, "SubExpression", expr)) || + OnExit(expr, field, parent); + } + } + public class ExpressionTester { private bool reportErrors = false; private ErrorReporter reporter = null; From 749b4b1b83e4ad6fe5b275a0b2bb6d963ea5f1c3 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Mon, 15 Nov 2021 14:52:01 -0600 Subject: [PATCH 20/27] Moved subset constraint checker to the right place. Added null tests everywhere needed. More precise error message --- Source/Dafny/Resolver.cs | 17 ++++++++--------- Source/Dafny/Util.cs | 18 ++++++++++++------ Test/git-issues/git-issue-697c.dfy.expect | 2 +- 3 files changed, 21 insertions(+), 16 deletions(-) diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 8a0a3acd9c9..e6703a60b22 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -2913,9 +2913,6 @@ public void ResolveTopLevelDecls_Core(List/*!*/ declarations, // * Verify that subset constraints are compilable if necessary // ---------------------------------------------------------------------------- - // Verifies that, in all compiled places, subset types in comprehensions have a compilable constraint - new SubsetConstraintGhostChecker(this).Traverse(declarations); - if (reporter.Count(ErrorLevel.Error) == prevErrorCount) { // fill in the postconditions and bodies of prefix lemmas foreach (var com in ModuleDefinition.AllExtremeLemmas(declarations)) { @@ -3505,6 +3502,8 @@ public void ResolveTopLevelDecls_Core(List/*!*/ declarations, } } } + // Verifies that, in all compiled places, subset types in comprehensions have a compilable constraint + new SubsetConstraintGhostChecker(this).Traverse(declarations); } private void CheckIsOkayWithoutRHS(ConstantField f) { @@ -18308,9 +18307,9 @@ protected override ContinuationStatus OnEnter(MemberDecl memberDecl, string fiel // We want to recurse only on the by method, not on the sub expressions of the function if (!memberDecl.IsGhost) return ok; if (memberDecl is Function f) { - if (Traverse(f.ByMethodDecl, "ByMethodDecl", f)) return stop; - if (f.ByMethodDecl.Body != f.ByMethodBody) { - if (Traverse(f.ByMethodBody, "ByMethodBody", f)) return stop; + if (f.ByMethodDecl != null && Traverse(f.ByMethodDecl, "ByMethodDecl", f)) return stop; + if (f.ByMethodDecl == null || f.ByMethodDecl.Body != f.ByMethodBody) { + if (f.ByMethodBody != null && Traverse(f.ByMethodBody, "ByMethodBody", f)) return stop; } } return skip; @@ -18318,13 +18317,13 @@ protected override ContinuationStatus OnEnter(MemberDecl memberDecl, string fiel public override bool Traverse(Expression expr, [CanBeNull] string field, [CanBeNull] object parent) { // Since we skipped ghost code, the code has to be compiled here. - if (expr is not QuantifierExpr e) { + if (expr is not ComprehensionExpr e) { return base.Traverse(expr, field, parent); } string what; if (e is ForallExpr) { - what = "forall expressions"; + what = "forall expression"; } else if (e is ExistsExpr) { what = "exists expression"; } else if (e is SetComprehension) { @@ -18332,7 +18331,7 @@ public override bool Traverse(Expression expr, [CanBeNull] string field, [CanBeN } else if (e is MapComprehension) { what = "map comprehension"; } else { - what = "quantifier"; + what = "comprehension"; } foreach (var boundVar in e.BoundVars) { if (boundVar.Type is UserDefinedType diff --git a/Source/Dafny/Util.cs b/Source/Dafny/Util.cs index 50c7a9889ba..bb62cc2686e 100644 --- a/Source/Dafny/Util.cs +++ b/Source/Dafny/Util.cs @@ -515,7 +515,13 @@ public bool Traverse(ModuleDefinition moduleDefinition) { } public bool Traverse(List topLevelDecls) { - return topLevelDecls.Any(Traverse); + foreach (var topLevelDecl in topLevelDecls) { + if (Traverse(topLevelDecl)) { + return true; + } + } + + return false; } public bool Traverse(ModuleDecl moduleDecl) { @@ -549,7 +555,7 @@ public bool Traverse(DatatypeCtor ctor) { } public bool Traverse(TopLevelDecl topd) { - var d = topd is ClassDecl classDecl ? classDecl.NonNullTypeDecl : topd; + var d = topd is ClassDecl classDecl && classDecl.NonNullTypeDecl != null ? classDecl.NonNullTypeDecl : topd; if (d is TopLevelDeclWithMembers tdm) { // ClassDecl, DatatypeDecl, OpaqueTypeDecl, NewtypeDecl @@ -624,7 +630,7 @@ public bool Traverse(MemberDecl memberDeclaration, [CanBeNull] string field, [Ca if (f.Formals.Any(Traverse)) { return true; } - if (f.Result.DefaultValue != null && Traverse(f.Result.DefaultValue, "Result.DefaultValue", f)) { + if (f.Result != null && f.Result.DefaultValue != null && Traverse(f.Result.DefaultValue, "Result.DefaultValue", f)) { return true; } if (f.Req.Any(e => Traverse(e.E, "Req.E", f))) { @@ -640,9 +646,9 @@ public bool Traverse(MemberDecl memberDeclaration, [CanBeNull] string field, [Ca return true; } if (Traverse(f.Body, "Body", f)) return true; - if (Traverse(f.ByMethodDecl, "ByMethodDecl", f)) return true; - if (f.ByMethodDecl.Body != f.ByMethodBody) { - if (Traverse(f.ByMethodBody, "ByMethodBody", f)) return true; + if (f.ByMethodDecl != null && Traverse(f.ByMethodDecl, "ByMethodDecl", f)) return true; + if (f.ByMethodDecl == null || f.ByMethodDecl.Body != f.ByMethodBody) { + if (f.ByMethodBody != null && Traverse(f.ByMethodBody, "ByMethodBody", f)) return true; } } else if (memberDeclaration is Method m) { // For example, default value of formals is non-ghost diff --git a/Test/git-issues/git-issue-697c.dfy.expect b/Test/git-issues/git-issue-697c.dfy.expect index 95a30cae8c0..dadcfb1ce5f 100644 --- a/Test/git-issues/git-issue-697c.dfy.expect +++ b/Test/git-issues/git-issue-697c.dfy.expect @@ -2,6 +2,6 @@ git-issue-697c.dfy(18,15): Error: EvenCell is a subset type and its constraint i git-issue-697c.dfy(9,26): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method') git-issue-697c.dfy(19,35): Error: EvenCell is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in map comprehension. The next error will explain why the constraint is not compilable. git-issue-697c.dfy(9,26): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method') -git-issue-697c.dfy(20,24): Error: EvenCell is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in quantifier. The next error will explain why the constraint is not compilable. +git-issue-697c.dfy(20,24): Error: EvenCell is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in forall expression. The next error will explain why the constraint is not compilable. git-issue-697c.dfy(9,26): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method') 6 resolution/type errors detected in git-issue-697c.dfy From 7e13479baa0714963784179dbaf54ba15caa9bfb Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Mon, 15 Nov 2021 15:54:02 -0600 Subject: [PATCH 21/27] Verification if parameters are null. --- Source/Dafny/Resolver.cs | 5 +++-- Source/Dafny/Util.cs | 10 ++++++++++ 2 files changed, 13 insertions(+), 2 deletions(-) diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index e6703a60b22..7c0d7af9dee 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -18298,14 +18298,14 @@ public SubsetConstraintGhostChecker(Resolver resolver) { } protected override ContinuationStatus OnEnter(Statement stmt, string field, object parent) { - return stmt.IsGhost ? skip : ok; + return stmt != null && stmt.IsGhost ? skip : ok; } protected override ContinuationStatus OnEnter(MemberDecl memberDecl, string field, object parent) { // Includes functions and methods as well. // Ghost functions can have a compiled implementation. // We want to recurse only on the by method, not on the sub expressions of the function - if (!memberDecl.IsGhost) return ok; + if (memberDecl == null || !memberDecl.IsGhost) return ok; if (memberDecl is Function f) { if (f.ByMethodDecl != null && Traverse(f.ByMethodDecl, "ByMethodDecl", f)) return stop; if (f.ByMethodDecl == null || f.ByMethodDecl.Body != f.ByMethodBody) { @@ -18316,6 +18316,7 @@ protected override ContinuationStatus OnEnter(MemberDecl memberDecl, string fiel } public override bool Traverse(Expression expr, [CanBeNull] string field, [CanBeNull] object parent) { + if (expr == null) return false; // Since we skipped ghost code, the code has to be compiled here. if (expr is not ComprehensionExpr e) { return base.Traverse(expr, field, parent); diff --git a/Source/Dafny/Util.cs b/Source/Dafny/Util.cs index bb62cc2686e..f6a69fcba0c 100644 --- a/Source/Dafny/Util.cs +++ b/Source/Dafny/Util.cs @@ -507,14 +507,17 @@ protected virtual ContinuationStatus OnEnter(MemberDecl memberDecl, [CanBeNull] // Traverse methods retun true to interrupt. public bool Traverse(Program program) { + if (program == null) return false; return program.Modules().Any(Traverse); } public bool Traverse(ModuleDefinition moduleDefinition) { + if (moduleDefinition == null) return false; return Traverse(moduleDefinition.TopLevelDecls); } public bool Traverse(List topLevelDecls) { + if (topLevelDecls == null) return false; foreach (var topLevelDecl in topLevelDecls) { if (Traverse(topLevelDecl)) { return true; @@ -525,6 +528,7 @@ public bool Traverse(List topLevelDecls) { } public bool Traverse(ModuleDecl moduleDecl) { + if (moduleDecl == null) return false; if (moduleDecl is LiteralModuleDecl l) { return Traverse(l.ModuleDef); } else if (moduleDecl is AbstractModuleDecl a) { @@ -539,6 +543,7 @@ public bool Traverse(ModuleDecl moduleDecl) { } public bool Traverse(Formal formal) { + if (formal == null) return false; if (formal.DefaultValue != null && Traverse(formal.DefaultValue, "DefaultValue", formal)) { return true; } @@ -547,6 +552,7 @@ public bool Traverse(Formal formal) { } public bool Traverse(DatatypeCtor ctor) { + if (ctor == null) return false; if (ctor.Formals.Any(Traverse)) { return true; } @@ -555,6 +561,7 @@ public bool Traverse(DatatypeCtor ctor) { } public bool Traverse(TopLevelDecl topd) { + if (topd == null) return false; var d = topd is ClassDecl classDecl && classDecl.NonNullTypeDecl != null ? classDecl.NonNullTypeDecl : topd; if (d is TopLevelDeclWithMembers tdm) { @@ -620,6 +627,7 @@ public bool Traverse(TopLevelDecl topd) { } public bool Traverse(MemberDecl memberDeclaration, [CanBeNull] string field, [CanBeNull] object parent) { + if (memberDeclaration == null) return false; var enterResult = OnEnter(memberDeclaration, field, parent); if (enterResult is stop or skip) return enterResult == stop; if (memberDeclaration is Field fi) { @@ -675,6 +683,7 @@ public bool Traverse(MemberDecl memberDeclaration, [CanBeNull] string field, [Ca } public virtual bool Traverse(Statement stmt, [CanBeNull] string field, [CanBeNull] object parent) { + if (stmt == null) return false; var enterResult = OnEnter(stmt, field, parent); if (enterResult is stop or skip) return enterResult == stop; return stmt.SubStatements.Any(subStmt => Traverse(subStmt, "SubStatements", stmt)) || @@ -683,6 +692,7 @@ public virtual bool Traverse(Statement stmt, [CanBeNull] string field, [CanBeNul } public virtual bool Traverse(Expression expr, [CanBeNull] string field, [CanBeNull] object parent) { + if (expr == null) return false; var enterResult = OnEnter(expr, field, parent); if (enterResult is stop or skip) return enterResult == stop; return expr.SubExpressions.Any(subExpr => Traverse(subExpr, "SubExpression", expr)) || From 7d836e82e7c1e8a2bb49ab2826519f01ae95f970 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 16 Nov 2021 09:19:50 -0600 Subject: [PATCH 22/27] Fixed ordering of boolean expressions. Else, recursive calls were skipped. --- Source/Dafny/Util.cs | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/Source/Dafny/Util.cs b/Source/Dafny/Util.cs index f6a69fcba0c..f5339ef0868 100644 --- a/Source/Dafny/Util.cs +++ b/Source/Dafny/Util.cs @@ -770,7 +770,7 @@ private bool CheckIsCompilable(Expression expr, ICodeContext codeContext) { isCompilable = CheckIsCompilable(callExpr.Receiver, codeContext); for (var i = 0; i < callExpr.Function.Formals.Count; i++) { if (!callExpr.Function.Formals[i].IsGhost) { - isCompilable = isCompilable && CheckIsCompilable(callExpr.Args[i], codeContext); + isCompilable = CheckIsCompilable(callExpr.Args[i], codeContext) && isCompilable; } } } @@ -782,7 +782,7 @@ private bool CheckIsCompilable(Expression expr, ICodeContext codeContext) { // note that if resolution is successful, then |e.Arguments| == |e.Ctor.Formals| for (int i = 0; i < value.Arguments.Count; i++) { if (!value.Ctor.Formals[i].IsGhost) { - isCompilable = isCompilable && CheckIsCompilable(value.Arguments[i], codeContext); + isCompilable = CheckIsCompilable(value.Arguments[i], codeContext) && isCompilable; } } return isCompilable; @@ -840,18 +840,18 @@ private bool CheckIsCompilable(Expression expr, ICodeContext codeContext) { } if (!lhs.Vars.All(bv => bv.IsGhost)) { - isCompilable = isCompilable && CheckIsCompilable(ee, codeContext); + isCompilable = CheckIsCompilable(ee, codeContext) && isCompilable; } i++; } - isCompilable = isCompilable && CheckIsCompilable(letExpr.Body, codeContext); + isCompilable = CheckIsCompilable(letExpr.Body, codeContext) && isCompilable; } else { Contract.Assert(letExpr.RHSs.Count == 1); var lhsVarsAreAllGhost = letExpr.BoundVars.All(bv => bv.IsGhost); if (!lhsVarsAreAllGhost) { - isCompilable = isCompilable && CheckIsCompilable(letExpr.RHSs[0], codeContext); + isCompilable = CheckIsCompilable(letExpr.RHSs[0], codeContext) && isCompilable; } - isCompilable = isCompilable && CheckIsCompilable(letExpr.Body, codeContext); + isCompilable = CheckIsCompilable(letExpr.Body, codeContext) && isCompilable; // fill in bounds for this to-be-compiled let-such-that expression Contract.Assert(letExpr.RHSs.Count == 1); // if we got this far, the resolver will have checked this condition successfully @@ -885,9 +885,9 @@ private bool CheckIsCompilable(Expression expr, ICodeContext codeContext) { } // don't recurse down any attributes if (comprehensionExpr.Range != null) { - isCompilable = isCompilable && CheckIsCompilable(comprehensionExpr.Range, codeContext); + isCompilable = CheckIsCompilable(comprehensionExpr.Range, codeContext) && isCompilable; } - isCompilable = isCompilable && CheckIsCompilable(comprehensionExpr.Term, codeContext); + isCompilable = CheckIsCompilable(comprehensionExpr.Term, codeContext) && isCompilable; return isCompilable; } else if (expr is ChainingExpression chainingExpression) { @@ -897,7 +897,7 @@ private bool CheckIsCompilable(Expression expr, ICodeContext codeContext) { } foreach (var ee in expr.SubExpressions) { - isCompilable = isCompilable && CheckIsCompilable(ee, codeContext); + isCompilable = CheckIsCompilable(ee, codeContext) && isCompilable; } return isCompilable; From f9eb6908a1ec58c827705804e5dbac6c0cdd37bd Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 16 Nov 2021 13:04:04 -0600 Subject: [PATCH 23/27] Emitted a block in the else statement for Go. --- Source/Dafny/Compilers/Compiler.cs | 1 + 1 file changed, 1 insertion(+) diff --git a/Source/Dafny/Compilers/Compiler.cs b/Source/Dafny/Compilers/Compiler.cs index f486a3ab9dd..4dc3c9601fa 100644 --- a/Source/Dafny/Compilers/Compiler.cs +++ b/Source/Dafny/Compilers/Compiler.cs @@ -4774,6 +4774,7 @@ var subsetTypeDecl and var thenWriter = EmitIf(out var guardWriter, isReturning, wr); TrExpr(constraintInContext, guardWriter, inLetExprBody); if (isReturning) { + wr = wr.NewBlock("", null, BraceStyle.Nothing); wr = EmitReturnExpr(wr); TrExpr(new LiteralExpr(e.tok, elseReturnValue), wr, inLetExprBody); thenWriter = EmitReturnExpr(thenWriter); From d377748628a5e42b27837f7b886859e28c4450a7 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 16 Nov 2021 14:02:05 -0600 Subject: [PATCH 24/27] Verification step should not apply to lambdas --- Source/Dafny/Resolver.cs | 51 ++++++++++++++++++++++++---------------- 1 file changed, 31 insertions(+), 20 deletions(-) diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 7c0d7af9dee..6e2134b7622 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -18334,27 +18334,38 @@ public override bool Traverse(Expression expr, [CanBeNull] string field, [CanBeN } else { what = "comprehension"; } - foreach (var boundVar in e.BoundVars) { - if (boundVar.Type is UserDefinedType - { - ResolvedClass: SubsetTypeDecl + + if (what != "comprehension") { // should not apply for functions + foreach (var boundVar in e.BoundVars) { + if (boundVar.Type is UserDefinedType { - Constraint: var constraint, - ConstraintIsCompilable: false and var constraintIsCompilable - } and var subsetTypeDecl - } - ) { - if (!subsetTypeDecl.CheckedIfConstraintIsCompilable) { - // Builtin types were never resolved. - constraintIsCompilable = ExpressionTester.CheckIsCompilable(null, constraint, new CodeContextWrapper(subsetTypeDecl, true)); - subsetTypeDecl.CheckedIfConstraintIsCompilable = true; - subsetTypeDecl.ConstraintIsCompilable = constraintIsCompilable; - } - if (!constraintIsCompilable) { - // Explicitely report the error - this.resolver.getReporter().Error(MessageSource.Resolver, boundVar.tok, - boundVar.Type + " is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in " + what + ". The next error will explain why the constraint is not compilable."); - ExpressionTester.CheckIsCompilable(this.resolver, constraint, new CodeContextWrapper(subsetTypeDecl, true)); + ResolvedClass: SubsetTypeDecl + { + Constraint: var constraint, + ConstraintIsCompilable: false and var constraintIsCompilable + } and var subsetTypeDecl + } + ) { + if (!subsetTypeDecl.CheckedIfConstraintIsCompilable) { + // Builtin types were never resolved. + constraintIsCompilable = + ExpressionTester.CheckIsCompilable(null, constraint, new CodeContextWrapper(subsetTypeDecl, true)); + subsetTypeDecl.CheckedIfConstraintIsCompilable = true; + subsetTypeDecl.ConstraintIsCompilable = constraintIsCompilable; + } + + if (!constraintIsCompilable) { + // Explicitely report the error + var showProvenance = constraint.tok.line != 0; + this.resolver.getReporter().Error(MessageSource.Resolver, boundVar.tok, + boundVar.Type + + " is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in " + + what + "." + + (showProvenance ? " The next error will explain why the constraint is not compilable." : "")); + if (showProvenance) + ExpressionTester.CheckIsCompilable(this.resolver, constraint, + new CodeContextWrapper(subsetTypeDecl, true)); + } } } } From 4ccb1fc26b25c45b3d8ffa666478b5c8432a3174 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 16 Nov 2021 14:04:09 -0600 Subject: [PATCH 25/27] Reverted the IsGhost for newtypes and subset types since not used anymore. --- Source/Dafny/AST/DafnyAst.cs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/DafnyAst.cs index 2b75b1c39a7..2c2f7afc74b 100644 --- a/Source/Dafny/AST/DafnyAst.cs +++ b/Source/Dafny/AST/DafnyAst.cs @@ -5573,7 +5573,7 @@ public TypeParameter.EqualitySupportValue EqualitySupport { FreshIdGenerator RedirectingTypeDecl.IdGenerator { get { return IdGenerator; } } bool ICodeContext.IsGhost { - get { return false; } + get { throw new NotSupportedException(); } // if .IsGhost is needed, the object should always be wrapped in an CodeContextWrapper } List ICodeContext.TypeArgs { get { return new List(); } } List ICodeContext.Ins { get { return new List(); } } @@ -5656,7 +5656,7 @@ public Type RhsWithArgumentIgnoringScope(List typeArgs) { FreshIdGenerator RedirectingTypeDecl.IdGenerator { get { return IdGenerator; } } bool ICodeContext.IsGhost { - get { return false; } + get { throw new NotSupportedException(); } // if .IsGhost is needed, the object should always be wrapped in an CodeContextWrapper } List ICodeContext.TypeArgs { get { return TypeArgs; } } List ICodeContext.Ins { get { return new List(); } } From 3ac28b7f208227d52148952e50c158f908ab372a Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Mon, 22 Nov 2021 09:29:54 -0600 Subject: [PATCH 26/27] - Reverted to old var = (subtype) assignment - 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. --- Source/Dafny/AST/DafnyAst.cs | 12 ++++- Source/Dafny/Compilers/Compiler.cs | 52 +++++++++---------- Source/Dafny/Resolver.cs | 34 +++++------- Source/Dafny/Rewriter.cs | 7 +-- Source/Dafny/Util.cs | 6 ++- .../Translator.ExpressionTranslator.cs | 14 ----- .../Synchronization/TextInsertionTest.cs | 2 +- .../Symbols/DafnyLangSymbolResolver.cs | 2 +- Source/DafnyLanguageServer/Program.cs | 2 +- Test/git-issues/git-issue-697.dfy | 6 +-- Test/git-issues/git-issue-697b.dfy | 9 ++-- Test/git-issues/git-issue-697b.dfy.expect | 1 + Test/git-issues/git-issue-697c.dfy | 6 +-- Test/git-issues/git-issue-697c.dfy.expect | 2 +- Test/git-issues/git-issue-697d.dfy | 9 +++- Test/git-issues/git-issue-697d.dfy.expect | 1 + Test/git-issues/git-issue-697e.dfy | 4 +- Test/git-issues/git-issue-697f.dfy | 2 +- 18 files changed, 84 insertions(+), 87 deletions(-) diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/DafnyAst.cs index 2c2f7afc74b..3161ebcbdac 100644 --- a/Source/Dafny/AST/DafnyAst.cs +++ b/Source/Dafny/AST/DafnyAst.cs @@ -1141,6 +1141,14 @@ public TraitDecl/*?*/ AsTraitType { return udt?.ResolvedClass as TraitDecl; } } + + public SubsetTypeDecl /*?*/ AsSubsetType { + get { + var std = NormalizeExpand(true) as UserDefinedType; + return std?.ResolvedClass as SubsetTypeDecl; + } + } + public bool IsArrayType { get { return AsArrayType != null; @@ -5703,8 +5711,8 @@ public class SubsetTypeDecl : TypeSynonymDecl, RedirectingTypeDecl { public enum WKind { CompiledZero, Compiled, Ghost, OptOut, Special } public readonly SubsetTypeDecl.WKind WitnessKind; public readonly Expression/*?*/ Witness; // non-null iff WitnessKind is Compiled or Ghost - public bool ConstraintIsCompilable = false; // Will be resolved later. - public bool CheckedIfConstraintIsCompilable = false; // Will be resolved later. + public bool ConstraintIsCompilable; // Will be filled in by the Resolver + public bool CheckedIfConstraintIsCompilable = false; // Set to true lazily by the Resolver when the Resolver fills in "ConstraintIsCompilable". public SubsetTypeDecl(IToken tok, string name, TypeParameter.TypeParameterCharacteristics characteristics, List typeArgs, ModuleDefinition module, BoundVar id, Expression constraint, WKind witnessKind, Expression witness, Attributes attributes) diff --git a/Source/Dafny/Compilers/Compiler.cs b/Source/Dafny/Compilers/Compiler.cs index 4dc3c9601fa..df5f67fb605 100644 --- a/Source/Dafny/Compilers/Compiler.cs +++ b/Source/Dafny/Compilers/Compiler.cs @@ -4616,7 +4616,8 @@ void writeObj(ConcreteSyntaxTree w) { } TrExpr(logicalBody, wBody, true); - } else if (expr is SetComprehension setComprehension) { + } else if (expr is SetComprehension) { + var e = (SetComprehension)expr; // For "set i,j,k,l | R(i,j,k,l) :: Term(i,j,k,l)" where the term has type "G", emit something like: // ((System.Func>)(() => { // var _coll = new List(); @@ -4633,33 +4634,32 @@ void writeObj(ConcreteSyntaxTree w) { // } // return Dafny.Set.FromCollection(_coll); // }))() - wr = CaptureFreeVariables(setComprehension, true, out var su, inLetExprBody, wr); - setComprehension = (SetComprehension)su.Substitute(setComprehension); + wr = CaptureFreeVariables(e, true, out var su, inLetExprBody, wr); + e = (SetComprehension)su.Substitute(e); - Contract.Assert(setComprehension.Bounds != null); // the resolver would have insisted on finding bounds + Contract.Assert(e.Bounds != null); // the resolver would have insisted on finding bounds var collectionName = idGenerator.FreshId("_coll"); - var bwr = CreateIIFE0(setComprehension.Type.AsSetType, setComprehension.tok, wr); + var bwr = CreateIIFE0(e.Type.AsSetType, e.tok, wr); wr = bwr; - EmitSetBuilder_New(wr, setComprehension, collectionName); - var n = setComprehension.BoundVars.Count; - Contract.Assert(setComprehension.Bounds.Count == n); - int i; - for (i = 0; i < n; i++) { - var bound = setComprehension.Bounds[i]; - var bv = setComprehension.BoundVars[i]; + EmitSetBuilder_New(wr, e, collectionName); + var n = e.BoundVars.Count; + Contract.Assert(e.Bounds.Count == n); + for (var i = 0; i < n; i++) { + var bound = e.Bounds[i]; + var bv = e.BoundVars[i]; ConcreteSyntaxTree collectionWriter; var tmpVar = idGenerator.FreshId("_compr_"); wr = CreateForeachLoop(tmpVar, GetCollectionEnumerationType(bound, bv), IdName(bv), bv.Type, true, bv.tok, out collectionWriter, wr); // var s = {List(Cell(1)), List(Cell(2), Cell(4)), List(Cell(2), Cell(3))}; // set x: List | x in s - wr = MaybeInjectSubsetConstraint(wr, inLetExprBody, bv, setComprehension); + wr = MaybeInjectSubsetConstraint(wr, inLetExprBody, bv, e); CompileCollection(bound, bv, inLetExprBody, true, null, collectionWriter); } ConcreteSyntaxTree guardWriter; var thn = EmitIf(out guardWriter, false, wr); - TrExpr(setComprehension.Range, guardWriter, inLetExprBody); - EmitSetBuilder_Add(setComprehension.Type.AsSetType, collectionName, setComprehension.Term, inLetExprBody, thn); - var s = GetCollectionBuilder_Build(setComprehension.Type.AsSetType, setComprehension.tok, collectionName, wr); + TrExpr(e.Range, guardWriter, inLetExprBody); + EmitSetBuilder_Add(e.Type.AsSetType, collectionName, e.Term, inLetExprBody, thn); + var s = GetCollectionBuilder_Build(e.Type.AsSetType, e.tok, collectionName, wr); EmitReturnExpr(s, bwr); } else if (expr is MapComprehension) { @@ -4742,23 +4742,21 @@ void writeObj(ConcreteSyntaxTree w) { private ConcreteSyntaxTree MaybeInjectSubsetConstraint(ConcreteSyntaxTree wr, bool inLetExprBody, BoundVar bv, Expression e, bool isReturning = false, bool elseReturnValue = false) { - int i; - if (bv.Type is UserDefinedType + if (bv.Type.NormalizeExpand(true) is UserDefinedType { TypeArgs: var typeArgs, ResolvedClass: - var subsetTypeDecl and - SubsetTypeDecl - { - TypeArgs: var typeParametersArgs, - Var: var var, - ConstraintIsCompilable: true, - Constraint: var constraint - } + SubsetTypeDecl + { + TypeArgs: var typeParametersArgs, + Var: var var, + ConstraintIsCompilable: true, + Constraint: var constraint + } }) { var bvIdentifier = new IdentifierExpr(e.tok, bv); var typeParameters = new Dictionary { }; - for (i = 0; i < typeParametersArgs.Count(); i++) { + for (var i = 0; i < typeParametersArgs.Count(); i++) { typeParameters[typeParametersArgs[i]] = typeArgs[i]; } var subContract = new Substituter(null, diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 6e2134b7622..3c26770f518 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -23,9 +23,7 @@ public class Resolver { ErrorReporter reporter; ModuleSignature moduleInfo = null; - public ErrorReporter getReporter() { - return reporter; - } + public ErrorReporter Reporter => reporter; private bool RevealedInScope(Declaration d) { Contract.Requires(d != null); @@ -18305,11 +18303,11 @@ protected override ContinuationStatus OnEnter(MemberDecl memberDecl, string fiel // Includes functions and methods as well. // Ghost functions can have a compiled implementation. // We want to recurse only on the by method, not on the sub expressions of the function - if (memberDecl == null || !memberDecl.IsGhost) return ok; + if (memberDecl == null || !memberDecl.IsGhost) { return ok; } if (memberDecl is Function f) { - if (f.ByMethodDecl != null && Traverse(f.ByMethodDecl, "ByMethodDecl", f)) return stop; + if (f.ByMethodDecl != null && Traverse(f.ByMethodDecl, "ByMethodDecl", f)) { return stop; } if (f.ByMethodDecl == null || f.ByMethodDecl.Body != f.ByMethodBody) { - if (f.ByMethodBody != null && Traverse(f.ByMethodBody, "ByMethodBody", f)) return stop; + if (f.ByMethodBody != null && Traverse(f.ByMethodBody, "ByMethodBody", f)) { return stop; } } } return skip; @@ -18337,14 +18335,11 @@ public override bool Traverse(Expression expr, [CanBeNull] string field, [CanBeN if (what != "comprehension") { // should not apply for functions foreach (var boundVar in e.BoundVars) { - if (boundVar.Type is UserDefinedType - { - ResolvedClass: SubsetTypeDecl - { - Constraint: var constraint, - ConstraintIsCompilable: false and var constraintIsCompilable - } and var subsetTypeDecl - } + if (boundVar.Type.AsSubsetType is + { + Constraint: var constraint, + ConstraintIsCompilable: false and var constraintIsCompilable + } and var subsetTypeDecl ) { if (!subsetTypeDecl.CheckedIfConstraintIsCompilable) { // Builtin types were never resolved. @@ -18355,16 +18350,15 @@ public override bool Traverse(Expression expr, [CanBeNull] string field, [CanBeN } if (!constraintIsCompilable) { - // Explicitely report the error + // Explicitly report the error var showProvenance = constraint.tok.line != 0; - this.resolver.getReporter().Error(MessageSource.Resolver, boundVar.tok, - boundVar.Type + - " is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in " + - what + "." + + this.resolver.Reporter.Error(MessageSource.Resolver, boundVar.tok, + $"{boundVar.Type} is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in {what}." + (showProvenance ? " The next error will explain why the constraint is not compilable." : "")); - if (showProvenance) + if (showProvenance) { ExpressionTester.CheckIsCompilable(this.resolver, constraint, new CodeContextWrapper(subsetTypeDecl, true)); + } } } } diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index a252b08894c..1d62f7b3170 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -1361,14 +1361,15 @@ List generateAutoReqs(Expression expr) { e.UpdateTerm(allReqsSatisfiedAndTerm); reporter.Info(MessageSource.Rewriter, e.tok, "autoreq added (" + Printer.ExtendedExprToString(allReqsSatisfied) + ") &&"); } - } else if (expr is SetComprehension setComprehension) { + } else if (expr is SetComprehension) { + var e = (SetComprehension)expr; // Translate "set xs | R :: T" // See LetExpr for issues with the e.Range //reqs.AddRange(generateAutoReqs(e.Range)); - var auto_reqs = generateAutoReqs(setComprehension.Term); + var auto_reqs = generateAutoReqs(e.Term); if (auto_reqs.Count > 0) { - reqs.Add(Expression.CreateQuantifier(new ForallExpr(setComprehension.tok, new List(), setComprehension.BoundVars, setComprehension.Range, andify(setComprehension.Term.tok, auto_reqs), setComprehension.Attributes), true)); + reqs.Add(Expression.CreateQuantifier(new ForallExpr(e.tok, new List(), e.BoundVars, e.Range, andify(e.Term.tok, auto_reqs), e.Attributes), true)); } } else if (expr is MapComprehension) { var e = (MapComprehension)expr; diff --git a/Source/Dafny/Util.cs b/Source/Dafny/Util.cs index f5339ef0868..dc21d60a890 100644 --- a/Source/Dafny/Util.cs +++ b/Source/Dafny/Util.cs @@ -708,7 +708,7 @@ public class ExpressionTester { public ExpressionTester(Resolver resolver = null, bool reportErrors = false) { Contract.Requires(reportErrors == false || resolver != null); if (resolver != null) { - this.reporter = resolver.getReporter(); + this.reporter = resolver.Reporter; this.resolver = resolver; } @@ -1122,7 +1122,9 @@ static void MakeGhostAsNeeded(CasePattern lhs) { static void MakeGhostAsNeeded(CasePattern arg, DatatypeDestructor d) { if (arg.Expr is IdentifierExpr ie && ie.Var is BoundVar bv) { - if (d.IsGhost) bv.MakeGhost(); + if (d.IsGhost) { + bv.MakeGhost(); + } } if (arg.Ctor != null) { MakeGhostAsNeeded(arg); diff --git a/Source/Dafny/Verifier/Translator.ExpressionTranslator.cs b/Source/Dafny/Verifier/Translator.ExpressionTranslator.cs index b5402572844..06ac1846d6e 100644 --- a/Source/Dafny/Verifier/Translator.ExpressionTranslator.cs +++ b/Source/Dafny/Verifier/Translator.ExpressionTranslator.cs @@ -1294,20 +1294,6 @@ public Boogie.Expr TrExpr(Expression expr) { if (e.TermIsSimple) { var bv = e.BoundVars[0]; // lambda y: BoxType :: CorrectType(y) && R[xs := yUnboxed] - var assumedType = bv.Type; - if (e.Type is SetType setType) { - if (setType.Arg is UserDefinedType udt) { - if (udt.ResolvedClass is SubsetTypeDecl stdc) { - if (stdc.ConstraintIsCompilable) { - // Ok the filtering will be performed by the compiler, we can assume the subset type. - } else { - // TODO: Substitue type parameters when computing assumedType + create test case - assumedType = stdc.Rhs; - // We need to verify that the bound proves the type. - } - } - } - } Boogie.Expr typeAntecedent = translator.MkIsBox(new Boogie.IdentifierExpr(expr.tok, yVar), bv.Type); if (freeOfAlloc != null && !freeOfAlloc[0]) { var isAlloc = translator.MkIsAlloc(new Boogie.IdentifierExpr(expr.tok, yVar), bv.Type, HeapExpr); diff --git a/Source/DafnyLanguageServer.Test/Synchronization/TextInsertionTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/TextInsertionTest.cs index 9608181a971..e4f3f2da8ad 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/TextInsertionTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/TextInsertionTest.cs @@ -166,7 +166,7 @@ function SomeConstant(): int { [TestMethod] public async Task InsertMultipleInSingleChange() { - // Note: line breaks are explicitely defined to avoid compatibility issues of \r and \r\n between + // Note: line breaks are explicitly defined to avoid compatibility issues of \r and \r\n between // the change and the verification. var source = "function GetConstant(): int { 1 }"; var documentItem = CreateTestDocument(source); diff --git a/Source/DafnyLanguageServer/Language/Symbols/DafnyLangSymbolResolver.cs b/Source/DafnyLanguageServer/Language/Symbols/DafnyLangSymbolResolver.cs index f1c11c56320..706a7fda568 100644 --- a/Source/DafnyLanguageServer/Language/Symbols/DafnyLangSymbolResolver.cs +++ b/Source/DafnyLanguageServer/Language/Symbols/DafnyLangSymbolResolver.cs @@ -132,7 +132,7 @@ private void ProcessAndAddAllMembers(TypeWithMembersSymbolBase containingType, T case Function function: return ProcessFunction(scope, function); case Method method: - // TODO handle the constructors explicitely? The constructor is a sub-class of Method. + // TODO handle the constructors explicitly? The constructor is a sub-class of Method. return ProcessMethod(scope, method); case Field field: return ProcessField(scope, field); diff --git a/Source/DafnyLanguageServer/Program.cs b/Source/DafnyLanguageServer/Program.cs index 247a4fc7244..f7652dd48ab 100644 --- a/Source/DafnyLanguageServer/Program.cs +++ b/Source/DafnyLanguageServer/Program.cs @@ -38,7 +38,7 @@ private static IConfiguration CreateConfiguration(string[] args) { } private static void InitializeLogger(IConfiguration configuration) { - // The environment variable is used so a log file can be explicitely created in the application dir. + // The environment variable is used so a log file can be explicitly created in the application dir. Environment.SetEnvironmentVariable("DAFNYLS_APP_DIR", Path.GetDirectoryName(Assembly.GetExecutingAssembly().Location)); Log.Logger = new LoggerConfiguration() .ReadFrom.Configuration(configuration) diff --git a/Test/git-issues/git-issue-697.dfy b/Test/git-issues/git-issue-697.dfy index eb6f9fafef7..af072c44445 100644 --- a/Test/git-issues/git-issue-697.dfy +++ b/Test/git-issues/git-issue-697.dfy @@ -6,14 +6,14 @@ type EvenCell = c: Cell | c.x % 2 == 0 witness Cell(0) function method doubleEvenCell(c: EvenCell): int { - if c.x % 2 == 1 then 1/0 else c.x * 2 + if c.x % 2 == 1 then 1/0 else c.x * 2 } method Main() { var x: set := { Cell(1), Cell(2), Cell(3), Cell(4) }; var y := set c: EvenCell | c in x; - var b: bool := forall c :: c in y ==> doubleEvenCell(c) > 0; + var b := forall c :: c in y ==> doubleEvenCell(c) > 0; assert b; - print(b); + print b; } diff --git a/Test/git-issues/git-issue-697b.dfy b/Test/git-issues/git-issue-697b.dfy index 2bb523bdc5e..562f43bfabf 100644 --- a/Test/git-issues/git-issue-697b.dfy +++ b/Test/git-issues/git-issue-697b.dfy @@ -5,15 +5,16 @@ datatype Cell = Cell(x: int) type EvenCell = c: Cell | c.x % 2 == 0 witness Cell(0) function method doubleEvenCell(c: EvenCell): int - { - if c.x % 2 == 1 then 1/0 else c.x * 2 - } +{ + if c.x % 2 == 1 then 1/0 else c.x * 2 +} method Main() { var x: set := {Cell(1), Cell(2), Cell(3), Cell(4)}; var z: map := map c: EvenCell | c in x :: c.x; var y := z.Keys; - var b: bool := forall c :: c in y ==> doubleEvenCell(c) > 0; + var b := forall c :: c in y ==> doubleEvenCell(c) > 0; assert b; + print Cell(1) in y, " ", z[Cell(2)], "\n"; } diff --git a/Test/git-issues/git-issue-697b.dfy.expect b/Test/git-issues/git-issue-697b.dfy.expect index 00a51f822da..b355409912b 100644 --- a/Test/git-issues/git-issue-697b.dfy.expect +++ b/Test/git-issues/git-issue-697b.dfy.expect @@ -1,2 +1,3 @@ Dafny program verifier finished with 3 verified, 0 errors +false 2 diff --git a/Test/git-issues/git-issue-697c.dfy b/Test/git-issues/git-issue-697c.dfy index cf16c8cc66f..0b7fabcb485 100644 --- a/Test/git-issues/git-issue-697c.dfy +++ b/Test/git-issues/git-issue-697c.dfy @@ -10,15 +10,15 @@ type EvenCell = c: Cell | ghostPredicate(c.x) witness Cell(0) function method doubleEvenCell(c: EvenCell): int { - if c.x % 2 == 1 then 1/0 else c.x * 2 + if c.x % 2 == 1 then 1/0 else c.x * 2 } method Main() { var x: set := { Cell(1), Cell(2), Cell(3), Cell(4) }; var y := set c: EvenCell | c in x; var z: map := map c: EvenCell | c in x :: c.x; - var b: bool := forall c :: c in y ==> doubleEvenCell(c) > 0; + var b := forall c :: c in y ==> doubleEvenCell(c) > 0; assert b; - print(b); + print b; } diff --git a/Test/git-issues/git-issue-697c.dfy.expect b/Test/git-issues/git-issue-697c.dfy.expect index dadcfb1ce5f..44dc023a4b1 100644 --- a/Test/git-issues/git-issue-697c.dfy.expect +++ b/Test/git-issues/git-issue-697c.dfy.expect @@ -2,6 +2,6 @@ git-issue-697c.dfy(18,15): Error: EvenCell is a subset type and its constraint i git-issue-697c.dfy(9,26): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method') git-issue-697c.dfy(19,35): Error: EvenCell is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in map comprehension. The next error will explain why the constraint is not compilable. git-issue-697c.dfy(9,26): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method') -git-issue-697c.dfy(20,24): Error: EvenCell is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in forall expression. The next error will explain why the constraint is not compilable. +git-issue-697c.dfy(20,18): Error: EvenCell is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in forall expression. The next error will explain why the constraint is not compilable. git-issue-697c.dfy(9,26): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method') 6 resolution/type errors detected in git-issue-697c.dfy diff --git a/Test/git-issues/git-issue-697d.dfy b/Test/git-issues/git-issue-697d.dfy index 8c9c5fa32ab..0ac79ec64a4 100644 --- a/Test/git-issues/git-issue-697d.dfy +++ b/Test/git-issues/git-issue-697d.dfy @@ -10,13 +10,18 @@ type EvenCell = c: Cell | nonGhostPredicate(c.x) witness Cell(0) function method doubleEvenCell(c: EvenCell): int { - if c.x % 2 == 1 then 1/0 else c.x * 2 + if c.x % 2 == 1 then 1/0 else c.x * 2 } method Main() { var x: set := { Cell(1), Cell(2), Cell(3), Cell(4) }; var y := set c: EvenCell | c in x; - var b: bool := forall c :: c in y ==> doubleEvenCell(c) > 0; + var b := forall c :: c in y ==> doubleEvenCell(c) > 0; + var b2 := forall c: EvenCell :: c in x ==> c.x % 2 == 0; + var b3 := exists c: EvenCell :: c in x && c.x == 3; assert b; + assert b2; + assert !b3; + print b && b2 && !b3; } diff --git a/Test/git-issues/git-issue-697d.dfy.expect b/Test/git-issues/git-issue-697d.dfy.expect index ba00363fc08..48fb59aeae5 100644 --- a/Test/git-issues/git-issue-697d.dfy.expect +++ b/Test/git-issues/git-issue-697d.dfy.expect @@ -1,2 +1,3 @@ Dafny program verifier finished with 4 verified, 0 errors +true \ No newline at end of file diff --git a/Test/git-issues/git-issue-697e.dfy b/Test/git-issues/git-issue-697e.dfy index 804857efb25..c513caaac80 100644 --- a/Test/git-issues/git-issue-697e.dfy +++ b/Test/git-issues/git-issue-697e.dfy @@ -6,12 +6,12 @@ type EvenCell = c: Cell | c.x % 2 == 0 witness Cell(0) function method doubleEvenCell(f: EvenCell): int { - if f.x % 2 == 1 then 1/0 else f.x * 2 + if f.x % 2 == 1 then 1/0 else f.x * 2 } method Main() { var x: set := { Cell(1), Cell(2), Cell(3), Cell(4) }; - var b: bool := forall g :: g in x ==> doubleEvenCell(g) > 0; + var b := forall g :: g in x ==> doubleEvenCell(g) > 0; assert b; } diff --git a/Test/git-issues/git-issue-697f.dfy b/Test/git-issues/git-issue-697f.dfy index 2fd4c835411..ddd5f3857f0 100644 --- a/Test/git-issues/git-issue-697f.dfy +++ b/Test/git-issues/git-issue-697f.dfy @@ -10,7 +10,7 @@ type EvenCell = c: Cell | ghostPredicate(c.x) witness Cell(0) function method doubleEvenCell(c: EvenCell): int { - if c.x % 2 == 1 then 1/0 else c.x * 2 + if c.x % 2 == 1 then 1/0 else c.x * 2 } // No need for the subset constraint to be compilable. From e7efc3b94d44899e463df6d7eb77707a374125f7 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Wed, 24 Nov 2021 16:06:39 -0600 Subject: [PATCH 27/27] Added the test for integers --- Test/git-issues/git-issue-697g.dfy | 16 ++++++++++++++++ Test/git-issues/git-issue-697g.dfy.expect | 3 +++ 2 files changed, 19 insertions(+) create mode 100644 Test/git-issues/git-issue-697g.dfy create mode 100644 Test/git-issues/git-issue-697g.dfy.expect diff --git a/Test/git-issues/git-issue-697g.dfy b/Test/git-issues/git-issue-697g.dfy new file mode 100644 index 00000000000..234b0e10491 --- /dev/null +++ b/Test/git-issues/git-issue-697g.dfy @@ -0,0 +1,16 @@ +// RUN: %dafny /compile:3 /rprint:"%t.rprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function method returnNat(c: nat): int +{ + if c < 0 then 1/0 else c +} + +method Main() { + var x: set := { -1, 2, -3, 4 }; + var y := set c: nat | c in x; + var b := forall c :: c in y ==> returnNat(c) >= 0; + assert b; + print b; +} + diff --git a/Test/git-issues/git-issue-697g.dfy.expect b/Test/git-issues/git-issue-697g.dfy.expect new file mode 100644 index 00000000000..d9157fa820a --- /dev/null +++ b/Test/git-issues/git-issue-697g.dfy.expect @@ -0,0 +1,3 @@ + +Dafny program verifier finished with 2 verified, 0 errors +true \ No newline at end of file