From 7f0e62a696e966968616ec20ea63b8a6a8800c09 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Tue, 20 Feb 2024 12:15:09 -0800 Subject: [PATCH 01/12] fix: Use reveal_ constant as function argument in override axiom --- .../Verifier/BoogieGenerator.Methods.cs | 4 +--- .../LitTest/git-issues/git-issue-5017.dfy | 23 +++++++++++++++++++ .../git-issues/git-issue-5017.dfy.expect | 2 ++ 3 files changed, 26 insertions(+), 3 deletions(-) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017.dfy.expect diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs index 36d88d7a24a..1f11eaa93cb 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs @@ -1263,9 +1263,7 @@ private Boogie.Axiom FunctionOverrideAxiom(Function f, Function overridingFuncti reveal = new Boogie.IdentifierExpr(f.tok, revealVar); argsJF.Add(reveal); } else if (overridingFunction.IsOpaque || overridingFunction.IsMadeImplicitlyOpaque(options)) { - // We can't use a bound variable $fuel, because then one of the triggers won't be mentioning this $fuel. - // Instead, we do the next best thing: use the literal false. - reveal = new Boogie.LiteralExpr(f.tok, false); + reveal = GetRevealConstant(overridingFunction); } // Add heap arguments diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017.dfy new file mode 100644 index 00000000000..b2ef13813d9 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017.dfy @@ -0,0 +1,23 @@ +// RUN: %testDafnyForEachResolver "%s" + +trait A { + ghost predicate Valid() +} + +trait B extends A { + ghost opaque predicate Valid() { true } +} + +method TestByRequires(b: B) + requires b.Valid() +{ + var a: A := b; + assert a.Valid(); +} + +method TestByReveal(b: B) { + var a: A := b; + assert a.Valid() by { + reveal b.Valid(); + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017.dfy.expect new file mode 100644 index 00000000000..ba00363fc08 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 4 verified, 0 errors From f5b6ab9cc517b6086252992ac295568868df0710 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Tue, 20 Feb 2024 14:01:12 -0800 Subject: [PATCH 02/12] Add resolution checks --- Source/DafnyCore/Resolver/ModuleResolver.cs | 3 + .../LitTest/git-issues/git-issue-5017.dfy | 23 ---- .../git-issues/git-issue-5017.dfy.expect | 2 - .../LitTest/git-issues/git-issue-5017a.dfy | 120 ++++++++++++++++++ .../git-issues/git-issue-5017a.dfy.expect | 5 + .../LitTest/git-issues/git-issue-5017b.dfy | 104 +++++++++++++++ .../git-issues/git-issue-5017b.dfy.expect | 10 ++ 7 files changed, 242 insertions(+), 25 deletions(-) delete mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017.dfy delete mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017a.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017a.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017b.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017b.dfy.expect diff --git a/Source/DafnyCore/Resolver/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs index 4cae2e3f69a..be17eeec518 100644 --- a/Source/DafnyCore/Resolver/ModuleResolver.cs +++ b/Source/DafnyCore/Resolver/ModuleResolver.cs @@ -2437,6 +2437,9 @@ void InheritedTraitMembers(TopLevelDeclWithMembers cl) { } else if (member.IsGhost != traitMember.IsGhost) { reporter.Error(MessageSource.Resolver, member.tok, "overridden {0} '{1}' in '{2}' has different ghost/compiled status than in trait '{3}'", traitMember.WhatKind, traitMember.Name, cl.Name, trait.Name); + } else if (!member.IsOpaque && traitMember.IsOpaque) { + reporter.Error(MessageSource.Resolver, member.tok, "overridden {0} '{1}' in '{2}' must be 'opaque' since the member is 'opaque' in trait '{3}'", + traitMember.WhatKind, traitMember.Name, cl.Name, trait.Name); } else { // Copy trait member's extern attribute onto class member if class does not provide one if (!Attributes.Contains(member.Attributes, "extern") && Attributes.Contains(traitMember.Attributes, "extern")) { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017.dfy deleted file mode 100644 index b2ef13813d9..00000000000 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017.dfy +++ /dev/null @@ -1,23 +0,0 @@ -// RUN: %testDafnyForEachResolver "%s" - -trait A { - ghost predicate Valid() -} - -trait B extends A { - ghost opaque predicate Valid() { true } -} - -method TestByRequires(b: B) - requires b.Valid() -{ - var a: A := b; - assert a.Valid(); -} - -method TestByReveal(b: B) { - var a: A := b; - assert a.Valid() by { - reveal b.Valid(); - } -} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017.dfy.expect deleted file mode 100644 index ba00363fc08..00000000000 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017.dfy.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Dafny program verifier finished with 4 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017a.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017a.dfy new file mode 100644 index 00000000000..ba7f96a4e5b --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017a.dfy @@ -0,0 +1,120 @@ +// RUN: %testDafnyForEachResolver "%s" -- --general-traits=datatype + +module True { + trait A { + ghost predicate Valid() + } + + trait B extends A { + ghost opaque predicate Valid() { true } + } + + method TestByRequires(b: B) + requires b.Valid() + { + var a: A := b; + assert a.Valid(); + } + + method TestByReveal(b: B) { + var a: A := b; + assert a.Valid() by { + reveal b.Valid(); + } + } +} + +module X { + trait A { + ghost predicate Valid(w: bool) + } + + trait B extends A { + ghost opaque predicate Valid(x: bool) { x } + } + + method TestByRequires(b: B, y: bool) + requires b.Valid(y) + { + var a: A := b; + assert a.Valid(y); + } + + method TestByReveal(b: B, y: bool) { + var a: A := b; + assert a.Valid(y) by { // error: assertion violation + reveal b.Valid(); + } + } +} + +module Parameters { + trait A { + ghost predicate P(t: T) + } + + trait B extends A { + ghost opaque predicate P(t: T) { t == t } + } + + + method TestByRequires(b: B) + requires b.P(5) + { + var a: A := b; + assert a.P(5); + } + + method TestByRequires'(b: B) + requires b.P(6) + { + var a: A := b; + assert a.P(5); // error: assertion violation + } + + method TestByRequires''(b: B) + requires b.P(true) + { + var a: A := b; + assert a.P(5); // error: assertion violation + } + + + method TestByReveal(b: B) { + var a: A := b; + assert a.P(5) by { + reveal b.P(); + } + } + + method TestByReveal'(b: B) { + var a: A := b; + assert a.P(true) by { + reveal b.P(); + } + } +} + +module StayOpaque { + trait A { + opaque predicate Valid() + } + + trait B extends A { + opaque predicate Valid() { true } + } + + method TestByRequires(b: B) + requires b.Valid() + { + var a: A := b; + assert a.Valid(); + } + + method TestByReveal(b: B) { + var a: A := b; + assert a.Valid() by { + reveal b.Valid(); + } + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017a.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017a.dfy.expect new file mode 100644 index 00000000000..1a1b0c1d16a --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017a.dfy.expect @@ -0,0 +1,5 @@ +git-issue-5017a.dfy(45,18): Error: assertion might not hold +git-issue-5017a.dfy(72,14): Error: assertion might not hold +git-issue-5017a.dfy(79,14): Error: assertion might not hold + +Dafny program verifier finished with 12 verified, 3 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017b.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017b.dfy new file mode 100644 index 00000000000..ff82103ea8a --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017b.dfy @@ -0,0 +1,104 @@ +// RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s" -- --general-traits=datatype + +module Opaque { + trait A { + predicate Valid() + } + + trait B { + opaque predicate Valid() { true } + } + + trait C { + opaque predicate Valid() + } + + + trait K0 extends A { + predicate Valid() + } + trait K1 extends A { + opaque predicate Valid() + } + trait K2 extends A { + predicate Valid() { true } + } + trait K3 extends A { + opaque predicate Valid() { true } + } + + trait L0 extends B { + predicate Valid() { true } // error: B.Valid already has a body + } + trait L1 extends B { + opaque predicate Valid() { true } // error: B.Valid already has a body + } + + trait M0 extends C { + predicate Valid() // error: must be opaque (since it is in C) + } + trait M1 extends C { + opaque predicate Valid() + } + trait M2 extends C { + predicate Valid() { true } // error: must be opaque (since it is in C) + } + trait M3 extends C { + opaque predicate Valid() { true } + } + + + datatype W0 extends A = W0 { + predicate Valid() { true } + } + class W1 extends A { + predicate Valid() { true } + } + + datatype X0 extends A = X0 { + opaque predicate Valid() { true } + } + class X1 extends A { + opaque predicate Valid() { true } + } + + datatype Y0 extends C = Y0 { + predicate Valid() { true } // error: must be opaque (since it is in C) + } + class Y1 extends C { + predicate Valid() { true } // error: must be opaque (since it is in C) + } + + datatype Z0 extends C = Z0 { + opaque predicate Valid() { true } + } + class Z1 extends C { + opaque predicate Valid() { true } + } +} + +module StayOpaque { + trait A { + opaque predicate Valid() + } + + datatype B extends A = B { + opaque predicate Valid() { true } + } + + class C extends A { + opaque predicate Valid() { true } + } + + method TestA(a: A) { + reveal a.Valid(); // error: nothing to reveal + } + + method TestB(b: B) { + reveal b.Valid(); + } + + method TestC(c: C) { + reveal c.Valid(); + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017b.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017b.dfy.expect new file mode 100644 index 00000000000..3cc1ce136f7 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017b.dfy.expect @@ -0,0 +1,10 @@ +git-issue-5017b.dfy(31,14): Error: fully defined predicate 'Valid' is inherited from trait 'B' and is not allowed to be re-declared +git-issue-5017b.dfy(34,21): Error: fully defined predicate 'Valid' is inherited from trait 'B' and is not allowed to be re-declared +git-issue-5017b.dfy(34,21): Error: static lemma 'reveal_Valid' is inherited from trait 'B' and is not allowed to be re-declared +git-issue-5017b.dfy(38,14): Error: overridden predicate 'Valid' in 'M0' must be 'opaque' since the member is 'opaque' in trait 'C' +git-issue-5017b.dfy(44,14): Error: overridden predicate 'Valid' in 'M2' must be 'opaque' since the member is 'opaque' in trait 'C' +git-issue-5017b.dfy(66,14): Error: overridden predicate 'Valid' in 'Y0' must be 'opaque' since the member is 'opaque' in trait 'C' +git-issue-5017b.dfy(69,14): Error: overridden predicate 'Valid' in 'Y1' must be 'opaque' since the member is 'opaque' in trait 'C' +git-issue-5017b.dfy(94,13): Error: member 'reveal_Valid' does not exist in trait 'A' +git-issue-5017b.dfy(94,18): Error: expression has no reveal lemma +9 resolution/type errors detected in git-issue-5017b.dfy From 59a03d08b09e1dacbdbbf85b26a11c50669d12c3 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Tue, 20 Feb 2024 15:40:46 -0800 Subject: [PATCH 03/12] Add axiom to correlate reveal_ constants for overrides --- Source/DafnyCore/Verifier/BoogieGenerator.cs | 8 ++ .../LitTest/git-issues/git-issue-5017a.dfy | 18 ++++ .../git-issues/git-issue-5017a.dfy.expect | 3 +- .../LitTest/git-issues/git-issue-5017c.dfy | 86 +++++++++++++++++++ .../git-issues/git-issue-5017c.dfy.expect | 4 + 5 files changed, 118 insertions(+), 1 deletion(-) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017c.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017c.dfy.expect diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.cs index e1d1f68fb63..0641fd46f9d 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.cs @@ -1042,6 +1042,14 @@ private void CreateRevealableConstant(Function f) { sink.AddTopLevelDeclaration(revealTrigger); Bpl.Expr revealTrigger_expr = new Bpl.IdentifierExpr(f.tok, revealTrigger); this.functionReveals[f] = revealTrigger_expr; + + // If this is an override, generate: + // axiom reveal_FunctionA ==> reveal_FunctionParent; + if (f.OverriddenFunction is { IsOpaque: true }) { + var revealParent = GetRevealConstant(f.OverriddenFunction); + var implication = BplImp(revealTrigger_expr, revealParent); + AddOtherDefinition(revealTrigger, new Axiom(f.tok, implication)); + } } } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017a.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017a.dfy index ba7f96a4e5b..83ffb34d85b 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017a.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017a.dfy @@ -104,6 +104,10 @@ module StayOpaque { opaque predicate Valid() { true } } + trait C extends A { + opaque predicate Valid() { true } + } + method TestByRequires(b: B) requires b.Valid() { @@ -117,4 +121,18 @@ module StayOpaque { reveal b.Valid(); } } + + method TestIndependence0(b: B, c: C) { + var a: A := b; + assert b.Valid() by { // error: revealing for C should not affect B + reveal c.Valid(); + } + } + + method TestIndependence1(b: B, c: C) { + var a: A := b; + assert a.Valid() by { // fine: revealing for C also reveals for all A's + reveal c.Valid(); + } + } } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017a.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017a.dfy.expect index 1a1b0c1d16a..8731f53b7d9 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017a.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017a.dfy.expect @@ -1,5 +1,6 @@ git-issue-5017a.dfy(45,18): Error: assertion might not hold git-issue-5017a.dfy(72,14): Error: assertion might not hold git-issue-5017a.dfy(79,14): Error: assertion might not hold +git-issue-5017a.dfy(127,18): Error: assertion might not hold -Dafny program verifier finished with 12 verified, 3 errors +Dafny program verifier finished with 14 verified, 4 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017c.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017c.dfy new file mode 100644 index 00000000000..32f945566c0 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017c.dfy @@ -0,0 +1,86 @@ +// RUN: %exits-with 4 %verify --type-system-refresh --general-traits=datatype "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +module Datatype { + trait A { + opaque predicate Valid() + } + + datatype B extends A = B { + opaque predicate Valid() { true } + } + + datatype C extends A = C { + opaque predicate Valid() { true } + } + + method TestByRequires(b: B) + requires b.Valid() + { + var a: A := b; + assert a.Valid(); + } + + method TestByReveal(b: B) { + var a: A := b; + assert a.Valid() by { + reveal b.Valid(); + } + } + + method TestIndependence0(b: B, c: C) { + var a: A := b; + assert b.Valid() by { // error: revealing for C should not affect B + reveal c.Valid(); + } + } + + method TestIndependence1(b: B, c: C) { + var a: A := b; + assert a.Valid() by { // fine: revealing for C also reveals for all A's + reveal c.Valid(); + } + } +} + +module Class { + trait A { + opaque predicate Valid() + } + + class B extends A { + opaque predicate Valid() { true } + } + + class C extends A { + opaque predicate Valid() { true } + } + + method TestByRequires(b: B) + requires b.Valid() + { + var a: A := b; + assert a.Valid(); + } + + method TestByReveal(b: B) { + var a: A := b; + assert a.Valid() by { + reveal b.Valid(); + } + } + + method TestIndependence0(b: B, c: C) { + var a: A := b; + assert b.Valid() by { // error: revealing for C should not affect B + reveal c.Valid(); + } + } + + method TestIndependence1(b: B, c: C) { + var a: A := b; + assert a.Valid() by { // fine: revealing for C also reveals for all A's + reveal c.Valid(); + } + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017c.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017c.dfy.expect new file mode 100644 index 00000000000..a8af3f86f5a --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017c.dfy.expect @@ -0,0 +1,4 @@ +git-issue-5017c.dfy(33,18): Error: assertion might not hold +git-issue-5017c.dfy(75,18): Error: assertion might not hold + +Dafny program verifier finished with 11 verified, 2 errors From 589fd808d7e6afee7302c172af365c78c228b194 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Tue, 20 Feb 2024 15:46:41 -0800 Subject: [PATCH 04/12] Add release notes --- docs/dev/news/5111.fix | 3 +++ 1 file changed, 3 insertions(+) create mode 100644 docs/dev/news/5111.fix diff --git a/docs/dev/news/5111.fix b/docs/dev/news/5111.fix new file mode 100644 index 00000000000..7f2a4cb3650 --- /dev/null +++ b/docs/dev/news/5111.fix @@ -0,0 +1,3 @@ +Let verifier understand opaque function overrides, supporting both when the overridden function is opaque and non-opaque. Revealing such a function for one overriding type has the effect of revealing it for all overriding types. + +Also, forbid the case where a function is opaque in a parent trait and the function override is not opaque. (Previously, this had caused a crash.) From 0c38b1284336a7f4768575b39a939cd610d1a531 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Wed, 21 Feb 2024 09:48:33 -0800 Subject: [PATCH 05/12] Fix exit-code expectation --- .../TestFiles/LitTests/LitTest/git-issues/git-issue-5017a.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017a.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017a.dfy index 83ffb34d85b..bae69ef1d7d 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017a.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017a.dfy @@ -1,4 +1,4 @@ -// RUN: %testDafnyForEachResolver "%s" -- --general-traits=datatype +// RUN: %testDafnyForEachResolver --expect-exit-code=4 "%s" -- --general-traits=datatype module True { trait A { From b9916ea35112a5a55cf72bc99185c965bd824ab1 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Wed, 28 Feb 2024 20:00:32 -0800 Subject: [PATCH 06/12] =?UTF-8?q?Introduce=20const=20for=20=E2=80=9Creveal?= =?UTF-8?q?=5F=E2=80=9D?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Source/DafnyCore/AST/Grammar/Printer/Printer.cs | 2 +- .../DafnyCore/AST/Statements/Verification/RevealStmt.cs | 2 ++ .../CheckTypeInferenceVisitor.cs | 2 +- .../NameResolutionAndTypeInference.cs | 4 ++-- .../Resolver/PreType/PreTypeResolve.Expressions.cs | 4 ++-- .../Resolver/PreType/UnderspecificationDetector.cs | 2 +- .../DafnyCore/Rewriters/AutoRevealFunctionDependencies.cs | 2 +- Source/DafnyCore/Rewriters/OpaqueMemberRewriter.cs | 8 +++++--- Source/DafnyCore/Verifier/BoogieGenerator.cs | 2 +- Source/DafnyDriver/DafnyDoc.cs | 2 +- 10 files changed, 17 insertions(+), 13 deletions(-) diff --git a/Source/DafnyCore/AST/Grammar/Printer/Printer.cs b/Source/DafnyCore/AST/Grammar/Printer/Printer.cs index d341139be68..a52b6de0264 100644 --- a/Source/DafnyCore/AST/Grammar/Printer/Printer.cs +++ b/Source/DafnyCore/AST/Grammar/Printer/Printer.cs @@ -980,7 +980,7 @@ private bool PrintModeSkipFunctionOrMethod(bool IsGhost, Attributes attributes, if (printMode == PrintModes.NoIncludes || printMode == PrintModes.NoGhost) { bool verify = true; if (Attributes.ContainsBool(attributes, "verify", ref verify) && !verify) { return true; } - if (name.Contains("INTERNAL") || name.StartsWith("reveal_")) { return true; } + if (name.Contains("INTERNAL") || name.StartsWith(RevealStmt.RevealLemmaPrefix)) { return true; } } return false; } diff --git a/Source/DafnyCore/AST/Statements/Verification/RevealStmt.cs b/Source/DafnyCore/AST/Statements/Verification/RevealStmt.cs index 7e0c98223fc..cf429919606 100644 --- a/Source/DafnyCore/AST/Statements/Verification/RevealStmt.cs +++ b/Source/DafnyCore/AST/Statements/Verification/RevealStmt.cs @@ -5,6 +5,8 @@ namespace Microsoft.Dafny; public class RevealStmt : Statement, ICloneable, ICanFormat { + public const string RevealLemmaPrefix = "reveal_"; + public readonly List Exprs; [FilledInDuringResolution] public readonly List LabeledAsserts = new List(); // to indicate that "Expr" denotes a labeled assertion [FilledInDuringResolution] public readonly List ResolvedStatements = new List(); diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/CheckTypeInferenceVisitor.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/CheckTypeInferenceVisitor.cs index 492569c0f9e..d5f8eb0d73c 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/CheckTypeInferenceVisitor.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/CheckTypeInferenceVisitor.cs @@ -189,7 +189,7 @@ protected override void PostVisitOneExpression(Expression expr, TypeInferenceChe ? e.Function.EnclosingClass.TypeArgs[i] : e.Function.TypeArgs[i - e.TypeApplication_AtEnclosingClass.Count]; if (!IsDetermined(p.Normalize())) { - var hint = e.Name.StartsWith("reveal_") + var hint = e.Name.StartsWith(RevealStmt.RevealLemmaPrefix) ? ". If you are making an opaque function, make sure that the function can be called." : ""; resolver.ReportError(ResolutionErrors.ErrorId.r_function_type_parameter_undetermined, e.tok, diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs index 6375c6efdc6..cbcd37e7790 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs @@ -5301,7 +5301,7 @@ Expression ResolveNameSegment(NameSegment expr, bool isLastNameSegment, List pair; - var name = resolutionContext.InReveal ? "reveal_" + expr.Name : expr.Name; + var name = resolutionContext.InReveal ? RevealStmt.RevealLemmaPrefix + expr.Name : expr.Name; var v = scope.Find(name); if (v != null) { // ----- 0. local variable, parameter, or bound variable @@ -1357,7 +1357,7 @@ Expression ResolveDotSuffix(ExprDotName expr, bool isLastNameSegment, List decl.Name == callableName); Type.PushScope(callableClass.EnclosingModuleDefinition.VisibilityScope); diff --git a/Source/DafnyCore/Rewriters/OpaqueMemberRewriter.cs b/Source/DafnyCore/Rewriters/OpaqueMemberRewriter.cs index a7d78d5a87c..55afa68a9d6 100644 --- a/Source/DafnyCore/Rewriters/OpaqueMemberRewriter.cs +++ b/Source/DafnyCore/Rewriters/OpaqueMemberRewriter.cs @@ -147,12 +147,14 @@ private void GenerateRevealLemma(MemberDecl m, List newDecls) { } Method reveal; if (m is TwoStateFunction) { - reveal = new TwoStateLemma(m.RangeToken.MakeAutoGenerated(), m.NameNode.Prepend("reveal_"), isStatic, new List(), new List(), new List(), new List(), + reveal = new TwoStateLemma(m.RangeToken.MakeAutoGenerated(), m.NameNode.Prepend(RevealStmt.RevealLemmaPrefix), isStatic, + new List(), new List(), new List(), new List(), new Specification(), new Specification(), ens, new Specification(new List(), null), null, lemma_attrs, null); } else { - reveal = new Lemma(m.RangeToken.MakeAutoGenerated(), m.NameNode.Prepend("reveal_"), isStatic, new List(), new List(), new List(), new List(), - new Specification(), new Specification(), ens, + reveal = new Lemma(m.RangeToken.MakeAutoGenerated(), m.NameNode.Prepend(RevealStmt.RevealLemmaPrefix), isStatic, new List(), + new List(), new List(), new List(), + new Specification(), new Specification(), ens, new Specification(new List(), null), null, lemma_attrs, null); } newDecls.Add(reveal); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.cs index 35a64e2441d..f2f9ee68601 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.cs @@ -1039,7 +1039,7 @@ private void CreateRevealableConstant(Function f) { if (!this.functionReveals.ContainsKey(f)) { // const reveal_FunctionA : bool Bpl.Constant revealTrigger = - new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, "reveal_" + f.FullName, Bpl.Type.Bool), false); + new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, RevealStmt.RevealLemmaPrefix + f.FullName, Bpl.Type.Bool), false); sink.AddTopLevelDeclaration(revealTrigger); Bpl.Expr revealTrigger_expr = new Bpl.IdentifierExpr(f.tok, revealTrigger); this.functionReveals[f] = revealTrigger_expr; diff --git a/Source/DafnyDriver/DafnyDoc.cs b/Source/DafnyDriver/DafnyDoc.cs index 6bc09cd9eb3..5688801be13 100644 --- a/Source/DafnyDriver/DafnyDoc.cs +++ b/Source/DafnyDriver/DafnyDoc.cs @@ -805,7 +805,7 @@ public static string AttrString(Attributes attr) { } public static bool IsGeneratedName(string name) { - return (name.Length > 1 && name[0] == '_') || name.StartsWith("reveal_"); + return (name.Length > 1 && name[0] == '_') || name.StartsWith(RevealStmt.RevealLemmaPrefix); } public string IndentedHtml(string docstring, bool nothingIfNull = false) { From 248dec2ef01bca32add32ee61c9fd9eb3d74d6c1 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 29 Feb 2024 14:47:01 -0800 Subject: [PATCH 07/12] Use keyword itself rather than keyword-is-present --- .../Assignment/AssignOrReturnStmt.cs | 2 +- Source/DafnyCore/Resolver/ModuleResolver.cs | 25 +++++++------- .../PreType/PreTypeResolve.Statements.cs | 34 +++++++++---------- .../LitTest/exceptions/TypecheckErrors.dfy | 16 +++++++-- 4 files changed, 43 insertions(+), 34 deletions(-) diff --git a/Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs b/Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs index 21e53ea79f1..0b6199ae2bb 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs @@ -235,7 +235,7 @@ public override void Resolve(ModuleResolver resolver, ResolutionContext resoluti DesugarElephantStatement(expectExtract, lhsExtract, firstType, resolver, (Method)resolutionContext.CodeContext); ResolvedStatements.ForEach(a => resolver.ResolveStatement(a, resolutionContext)); - resolver.EnsureSupportsErrorHandling(Tok, firstType, expectExtract, KeywordToken != null); + resolver.EnsureSupportsErrorHandling(Tok, firstType, expectExtract, KeywordToken?.Token.val); } public void ResolveKeywordToken(INewOrOldResolver resolver, ResolutionContext resolutionContext) { diff --git a/Source/DafnyCore/Resolver/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs index bf6f79c261b..8f45994d178 100644 --- a/Source/DafnyCore/Resolver/ModuleResolver.cs +++ b/Source/DafnyCore/Resolver/ModuleResolver.cs @@ -2952,7 +2952,7 @@ public Expression makeTemp(String prefix, AssignOrReturnStmt s, ResolutionContex return id; } - public void EnsureSupportsErrorHandling(IToken tok, Type tp, bool expectExtract, bool hasKeywordToken) { + public void EnsureSupportsErrorHandling(IToken tok, Type tp, bool expectExtract, [CanBeNull] string keyword) { // The "method not found" errors which will be generated here were already reported while // resolving the statement, so we don't want them to reappear and redirect them into a sink. var origReporter = reporter; @@ -2962,23 +2962,22 @@ public void EnsureSupportsErrorHandling(IToken tok, Type tp, bool expectExtract, var propagateFailure = ResolveMember(tok, tp, "PropagateFailure", out _); var extract = ResolveMember(tok, tp, "Extract", out _); - if (hasKeywordToken) { + if (keyword != null) { if (isFailure == null || (extract != null) != expectExtract) { // more details regarding which methods are missing have already been reported by regular resolution + var requiredMembers = expectExtract + ? "functions 'IsFailure()' and 'Extract()'" + : "function 'IsFailure()', but not 'Extract()'"; origReporter.Error(MessageSource.Resolver, tok, - "The right-hand side of ':-', which is of type '{0}', with a keyword token must have function{1}", tp, - expectExtract - ? "s 'IsFailure()' and 'Extract()'" - : " 'IsFailure()', but not 'Extract()'"); + $"The right-hand side of ':- {keyword}', which is of type '{tp}', with a keyword token must have {requiredMembers}"); } } else { if (isFailure == null || propagateFailure == null || (extract != null) != expectExtract) { // more details regarding which methods are missing have already been reported by regular resolution - origReporter.Error(MessageSource.Resolver, tok, - "The right-hand side of ':-', which is of type '{0}', must have function{1}", tp, - expectExtract - ? "s 'IsFailure()', 'PropagateFailure()', and 'Extract()'" - : "s 'IsFailure()' and 'PropagateFailure()', but not 'Extract()'"); + var requiredMembers = expectExtract + ? "functions 'IsFailure()', 'PropagateFailure()', and 'Extract()'" + : "functions 'IsFailure()' and 'PropagateFailure()', but not 'Extract()'"; + origReporter.Error(MessageSource.Resolver, tok, $"The right-hand side of ':-', which is of type '{tp}', must have {requiredMembers}"); } } @@ -2998,7 +2997,7 @@ void CheckIsFunction([CanBeNull] MemberDecl memberDecl, bool allowMethod) { } CheckIsFunction(isFailure, false); - if (!hasKeywordToken) { + if (keyword == null) { CheckIsFunction(propagateFailure, true); } if (expectExtract) { @@ -3148,7 +3147,7 @@ public void ResolveLetOrFailExpr(LetOrFailExpr expr, ResolutionContext resolutio ResolveExpression(expr.ResolvedExpression, resolutionContext); expr.Type = expr.ResolvedExpression.Type; bool expectExtract = (expr.Lhs != null); - EnsureSupportsErrorHandling(expr.tok, PartiallyResolveTypeForMemberSelection(expr.tok, tempType), expectExtract, false); + EnsureSupportsErrorHandling(expr.tok, PartiallyResolveTypeForMemberSelection(expr.tok, tempType), expectExtract, null); } public static Type SelectAppropriateArrowTypeForFunction(Function function, Dictionary subst, SystemModuleManager systemModuleManager) { diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs index 5e7ae6c0871..57c7d758db8 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs @@ -1111,35 +1111,35 @@ private void ResolveAssignOrReturnStmt(AssignOrReturnStmt s, ResolutionContext r } s.ResolvedStatements.ForEach(a => ResolveStatement(a, resolutionContext)); - EnsureSupportsErrorHandling(s.Tok, failureSupportingType, expectExtract, s.KeywordToken != null); + EnsureSupportsErrorHandling(s.Tok, failureSupportingType, expectExtract, s.KeywordToken?.Token.val); } - private void EnsureSupportsErrorHandling(IToken tok, TopLevelDeclWithMembers failureSupportingType, bool expectExtract, bool hasKeywordToken) { + private void EnsureSupportsErrorHandling(IToken tok, TopLevelDeclWithMembers failureSupportingType, bool expectExtract, [CanBeNull] string keyword) { var isFailure = failureSupportingType.Members.Find(x => x.Name == "IsFailure"); var propagateFailure = failureSupportingType.Members.Find(x => x.Name == "PropagateFailure"); var extract = failureSupportingType.Members.Find(x => x.Name == "Extract"); - if (hasKeywordToken) { + if (keyword != null) { if (isFailure == null || (extract != null) != expectExtract) { // more details regarding which methods are missing have already been reported by regular resolution - ReportError(tok, - "The right-hand side of ':-', which is of type '{0}', with a keyword token must have function{1}", failureSupportingType, - expectExtract ? "s 'IsFailure()' and 'Extract()'" : " 'IsFailure()', but not 'Extract()'"); + var requiredMembers = expectExtract + ? "functions 'IsFailure()' and 'Extract()'" + : "function 'IsFailure()', but not 'Extract()'"; + ReportError(tok, $"The right-hand side of ':- {keyword}', which is of type '{failureSupportingType}', must have {requiredMembers}"); } } else { if (isFailure == null || propagateFailure == null || (extract != null) != expectExtract) { // more details regarding which methods are missing have already been reported by regular resolution - ReportError(tok, - "The right-hand side of ':-', which is of type '{0}', must have function{1}", failureSupportingType, - expectExtract - ? "s 'IsFailure()', 'PropagateFailure()', and 'Extract()'" - : "s 'IsFailure()' and 'PropagateFailure()', but not 'Extract()'"); + var requiredMembers = expectExtract + ? "functions 'IsFailure()', 'PropagateFailure()', and 'Extract()'" + : "functions 'IsFailure()' and 'PropagateFailure()', but not 'Extract()'"; + ReportError(tok, $"The right-hand side of ':-', which is of type '{failureSupportingType}', must have {requiredMembers}"); } } - void checkIsFunction([CanBeNull] MemberDecl memberDecl, bool allowMethod) { - if (memberDecl == null || memberDecl is Function) { + void CheckIsFunction([CanBeNull] MemberDecl memberDecl, bool allowMethod) { + if (memberDecl is null or Function) { // fine } else if (allowMethod && memberDecl is Method) { // give a deprecation warning, so we will remove this language feature around the Dafny 4 time frame @@ -1153,12 +1153,12 @@ void checkIsFunction([CanBeNull] MemberDecl memberDecl, bool allowMethod) { } } - checkIsFunction(isFailure, false); - if (!hasKeywordToken) { - checkIsFunction(propagateFailure, true); + CheckIsFunction(isFailure, false); + if (keyword == null) { + CheckIsFunction(propagateFailure, true); } if (expectExtract) { - checkIsFunction(extract, true); + CheckIsFunction(extract, true); } } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/TypecheckErrors.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/TypecheckErrors.dfy index a646da421d7..36a4fd53cbf 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/TypecheckErrors.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/TypecheckErrors.dfy @@ -36,15 +36,15 @@ trait BadOutcome3 { } method TestMissingMethods1(o: BadOutcome1) returns (res: BadOutcome1) { - var a :- o; return o; // TODO infers 'BadOutcome1?' for RHS of ':-' instead of 'BadOutcome1' (should not infer nullable) + var a :- o; return o; } method TestMissingMethods2(o: BadOutcome2) returns (res: BadOutcome2) { - var a :- o; return o; // TODO infers 'BadOutcome2?' for RHS of ':-' instead of 'BadOutcome2' (should not infer nullable) + var a :- o; return o; } method TestMissingMethods3(o: BadOutcome3) returns (res: BadOutcome3) { - var a :- o; return o; // TODO infers 'BadOutcome3?' for RHS of ':-' instead of 'BadOutcome3' (should not infer nullable) + var a :- o; return o; } method TestTypecheckingInDesugaredTerm_Void() returns (res: VoidOutcome) { @@ -78,3 +78,13 @@ method TestMissingVoidMethods2(o: BadVoidOutcome2) returns (res: BadVoidOutcome2 method TestMissingVoidMethods3(o: BadVoidOutcome3) returns (res: BadVoidOutcome3) { :- o; return o; } + +method TestMissingMethods2WithKeyword(o: BadOutcome2) returns (res: BadOutcome2) { + var a :- assert o; // with "assert" keyword, it's fine that PropagateFailure is missing + return o; +} + +method TestMissingVoidMethods2WithKeyword(o: BadVoidOutcome2) returns (res: BadVoidOutcome2) { + :- assert o; // with "assert" keyword, it's fine that PropagateFailure is missing + return o; +} From 8a4b908f818b454fb52e2371bdb84ad25128ec30 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 29 Feb 2024 14:50:19 -0800 Subject: [PATCH 08/12] Extract method ReportMemberNotFoundError --- .../NameResolutionAndTypeInference.cs | 8 ++++++-- .../Resolver/PreType/PreTypeResolve.Expressions.cs | 11 ++++++++--- 2 files changed, 14 insertions(+), 5 deletions(-) diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs index cbcd37e7790..01334eea214 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs @@ -4550,7 +4550,7 @@ public MemberDecl ResolveMember(IToken tok, Type receiverType, string memberName if (memberName == "_ctor") { reporter.Error(MessageSource.Resolver, tok, "{0} {1} does not have an anonymous constructor", cd.WhatKind, cd.Name); } else { - reporter.Error(MessageSource.Resolver, tok, "member '{0}' does not exist in {2} '{1}'", memberName, cd.Name, cd.WhatKind); + ReportMemberNotFoundError(tok, memberName, cd); } } else if (!VisibleInScope(member)) { reporter.Error(MessageSource.Resolver, tok, "member '{0}' has not been imported in this scope and cannot be accessed here", memberName); @@ -4567,6 +4567,10 @@ public MemberDecl ResolveMember(IToken tok, Type receiverType, string memberName return null; } + private void ReportMemberNotFoundError(IToken tok, string memberName, TopLevelDecl receiverDecl) { + reporter.Error(MessageSource.Resolver, tok, $"member '{memberName}' does not exist in {receiverDecl.WhatKind} '{receiverDecl.Name}'"); + } + /// /// Roughly speaking, tries to figure out the head of the type of "t", making as few inference decisions as possible. /// More precisely, returns a type that contains all the members of "t"; or if "memberName" is non-null, a type @@ -5735,7 +5739,7 @@ Expression ResolveDotSuffix(ExprDotName expr, bool isLastNameSegment, List members, + TopLevelDecl receiverDecl, ResolutionContext resolutionContext) { + ReportError(tok, $"member '{memberName}' does not exist in {receiverDecl.WhatKind} '{receiverDecl.Name}'"); + } + /// /// Look up expr.Name in the following order: /// 0. Local variable, parameter, or bound variable. @@ -1456,7 +1461,7 @@ Expression ResolveDotSuffix(ExprDotName expr, bool isLastNameSegment, List Date: Thu, 29 Feb 2024 14:51:50 -0800 Subject: [PATCH 09/12] Add resolutionContext parameter --- .../PreType/PreTypeResolve.Expressions.cs | 16 +++++++++------- .../DafnyCore/Resolver/PreType/PreTypeResolve.cs | 5 +++-- 2 files changed, 12 insertions(+), 9 deletions(-) diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs index f453fa527db..f3867f7b966 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs @@ -11,6 +11,7 @@ using System.Numerics; using System.Diagnostics.Contracts; using DafnyCore; +using JetBrains.Annotations; using ResolutionContext = Microsoft.Dafny.ResolutionContext; namespace Microsoft.Dafny { @@ -604,7 +605,7 @@ resolutionContext.CodeContext is ConstantField || Constraints.AddGuardedConstraint(() => { if (e.Rhs.PreType.NormalizeWrtScope() is DPreType receiverPreType) { bool expectExtract = e.Lhs != null; - EnsureSupportsErrorHandling(e.tok, receiverPreType, expectExtract); + EnsureSupportsErrorHandling(e.tok, receiverPreType, expectExtract, resolutionContext, null); return true; } return false; @@ -1018,7 +1019,8 @@ private void ConstrainOperandTypes(IToken tok, string opString, Expression e0, E /// "receiverPreType" is an unresolved proxy type and that, after solving more type constraints, "receiverPreType" /// eventually gets set to a type more specific than "tentativeReceiverType". /// - (MemberDecl/*?*/, DPreType/*?*/) FindMember(IToken tok, PreType receiverPreType, string memberName, bool reportErrorOnMissingMember = true) { + (MemberDecl /*?*/, DPreType /*?*/) FindMember(IToken tok, PreType receiverPreType, string memberName, ResolutionContext resolutionContext, + bool reportErrorOnMissingMember = true) { Contract.Requires(tok != null); Contract.Requires(receiverPreType != null); Contract.Requires(memberName != null); @@ -1466,7 +1468,7 @@ Expression ResolveDotSuffix(ExprDotName expr, bool isLastNameSegment, List { DPreType dp = fe.E.PreType.NormalizeWrtScope() as DPreType; if (dp == null) { @@ -1486,7 +1487,7 @@ void ResolveFrameExpression(FrameExpression fe, FrameExpressionUse use, ICodeCon } if (fe.FieldName != null) { - var (member, tentativeReceiverType) = FindMember(fe.E.tok, dp, fe.FieldName); + var (member, tentativeReceiverType) = FindMember(fe.E.tok, dp, fe.FieldName, resolutionContext); Contract.Assert((member == null) == (tentativeReceiverType == null)); // follows from contract of FindMember if (member == null) { // error has already been reported by FindMember From 16a2e955c5dcc97c9357d1af470b91dcb49a3604 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 29 Feb 2024 14:52:23 -0800 Subject: [PATCH 10/12] chore: Improve code formatting --- .../DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs index f3867f7b966..46040d43474 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs @@ -2148,7 +2148,9 @@ private void EnsureSupportsErrorHandling(IToken tok, DPreType burritoPreType, bo if (keyword != null) { if (memberIsFailure == null || (memberExtract != null) != expectExtract) { // more details regarding which methods are missing have already been reported by regular resolution - var requiredMembers = expectExtract ? "members IsFailure() and Extract()" : "member IsFailure(), but not Extract()"; + var requiredMembers = expectExtract + ? "members IsFailure() and Extract()" + : "member IsFailure(), but not Extract()"; ReportError(tok, $"right-hand side of ':- {keyword}', which is of type '{burritoPreType}', must have {requiredMembers}"); } } else { From 563d9a88cb1d0da0454159b9aa0ab17f8744ac19 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 29 Feb 2024 15:09:40 -0800 Subject: [PATCH 11/12] Improve error messages for reveal --- .../NameResolutionAndTypeInference.cs | 27 ++++++++++- .../PreType/PreTypeResolve.Expressions.cs | 35 ++++++++++++++- .../PreType/PreTypeResolve.Statements.cs | 2 +- .../LitTest/git-issues/git-issue-5017b.dfy | 45 ++++++++++++++++++- .../git-issues/git-issue-5017b.dfy.expect | 22 +++++++-- 5 files changed, 123 insertions(+), 8 deletions(-) diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs index 01334eea214..58ce855888a 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs @@ -3535,7 +3535,7 @@ public void ResolveStatement(Statement stmt, ResolutionContext resolutionContext var e = (ApplySuffix)expr; var methodCallInfo = ResolveApplySuffix(e, revealResolutionContext, true); if (methodCallInfo == null) { - reporter.Error(MessageSource.Resolver, expr.tok, "expression has no reveal lemma"); + // error has already been reported } else if (methodCallInfo.Callee.Member is TwoStateLemma && !revealResolutionContext.IsTwoState) { reporter.Error(MessageSource.Resolver, methodCallInfo.Tok, "a two-state function can only be revealed in a two-state context"); } else if (methodCallInfo.Callee.AtLabel != null) { @@ -4568,7 +4568,28 @@ public MemberDecl ResolveMember(IToken tok, Type receiverType, string memberName } private void ReportMemberNotFoundError(IToken tok, string memberName, TopLevelDecl receiverDecl) { + if (memberName.StartsWith(RevealStmt.RevealLemmaPrefix)) { + var nameToBeRevealed = memberName[RevealStmt.RevealLemmaPrefix.Length..]; + var members = receiverDecl is TopLevelDeclWithMembers topLevelDeclWithMembers ? GetClassMembers(topLevelDeclWithMembers) : null; + if (members == null) { + reporter.Error(MessageSource.Resolver, tok, $"member '{nameToBeRevealed}' does not exist in {receiverDecl.WhatKind} '{receiverDecl.Name}'"); + } else if (!members.TryGetValue(nameToBeRevealed, out var member)) { + reporter.Error(MessageSource.Resolver, tok, $"member '{nameToBeRevealed}' does not exist in {receiverDecl.WhatKind} '{receiverDecl.Name}'"); + } else if (member is not (ConstantField or Function)) { + Contract.Assert(!member.IsOpaque); + reporter.Error(MessageSource.Resolver, tok, + $"a {member.WhatKind} ('{nameToBeRevealed}') cannot be revealed; only opaque constants and functions can be revealed"); + } else if (!member.IsOpaque) { + reporter.Error(MessageSource.Resolver, tok, $"{member.WhatKind} '{nameToBeRevealed}' cannot be revealed, because it is not opaque"); + } else if (member is Function { Body: null }) { + reporter.Error(MessageSource.Resolver, tok, + $"{member.WhatKind} '{nameToBeRevealed}' cannot be revealed, because it has no body in {receiverDecl.WhatKind} '{receiverDecl.Name}'"); + } else { + reporter.Error(MessageSource.Resolver, tok, $"cannot reveal '{nameToBeRevealed}'"); + } + } else { reporter.Error(MessageSource.Resolver, tok, $"member '{memberName}' does not exist in {receiverDecl.WhatKind} '{receiverDecl.Name}'"); + } } /// @@ -5402,7 +5423,9 @@ Expression ResolveNameSegment(NameSegment expr, bool isLastNameSegment, List members, TopLevelDecl receiverDecl, ResolutionContext resolutionContext) { + if (memberName.StartsWith(RevealStmt.RevealLemmaPrefix)) { + var nameToBeRevealed = memberName[RevealStmt.RevealLemmaPrefix.Length..]; + if (members == null) { + if (receiverDecl is TopLevelDeclWithMembers receiverDeclWithMembers) { + // try this instead: + members = resolver.GetClassMembers(receiverDeclWithMembers); + } + } + if (members == null) { + ReportError(tok, $"member '{nameToBeRevealed}' does not exist in {receiverDecl.WhatKind} '{receiverDecl.Name}'"); + } else if (!members.TryGetValue(nameToBeRevealed, out var member)) { + ReportError(tok, $"member '{nameToBeRevealed}' does not exist in {receiverDecl.WhatKind} '{receiverDecl.Name}'"); + } else if (member is not (ConstantField or Function)) { + Contract.Assert(!member.IsOpaque); + ReportError(tok, + $"a {member.WhatKind} ('{nameToBeRevealed}') cannot be revealed; only opaque constants and functions can be revealed"); + } else if (!member.IsOpaque) { + ReportError(tok, $"{member.WhatKind} '{nameToBeRevealed}' cannot be revealed, because it is not opaque"); + } else if (member is Function { Body: null }) { + ReportError(tok, + $"{member.WhatKind} '{nameToBeRevealed}' cannot be revealed, because it has no body in {receiverDecl.WhatKind} '{receiverDecl.Name}'"); + } else { + ReportError(tok, $"cannot reveal '{nameToBeRevealed}'"); + } + } else { ReportError(tok, $"member '{memberName}' does not exist in {receiverDecl.WhatKind} '{receiverDecl.Name}'"); + } } /// @@ -1216,7 +1242,14 @@ Expression ResolveNameSegment(NameSegment expr, bool isLastNameSegment, List Date: Thu, 29 Feb 2024 15:25:30 -0800 Subject: [PATCH 12/12] Further improve error messages --- .../NameResolutionAndTypeInference.cs | 21 +++++++++++------- .../PreType/PreTypeResolve.Expressions.cs | 22 +++++++++++-------- .../LabeledAssertsResolution.dfy.expect | 4 ++-- .../LitTest/exports/ExportResolve.dfy.expect | 5 ++--- .../git-issues/git-issue-3804d.dfy.expect | 8 +++---- 5 files changed, 34 insertions(+), 26 deletions(-) diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs index 58ce855888a..f541f12dda3 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs @@ -5422,13 +5422,7 @@ Expression ResolveNameSegment(NameSegment expr, bool isLastNameSegment, List optTypeArguments, TopLevelDecl decl) { Contract.Requires(tok != null); Contract.Requires(name != null); @@ -1454,7 +1458,7 @@ Expression ResolveDotSuffix(ExprDotName expr, bool isLastNameSegment, List