diff --git a/Source/DafnyCore/AST/Statements/Verification/HideRevealStmt.cs b/Source/DafnyCore/AST/Statements/Verification/HideRevealStmt.cs index 778330f259c..f78a07109bd 100644 --- a/Source/DafnyCore/AST/Statements/Verification/HideRevealStmt.cs +++ b/Source/DafnyCore/AST/Statements/Verification/HideRevealStmt.cs @@ -96,7 +96,7 @@ public void Resolve(PreTypeResolver resolver, ResolutionContext resolutionContex if (effectiveExpr is NameSegment) { resolver.ResolveNameSegment((NameSegment)effectiveExpr, true, null, resolutionContext, true); } else { - resolver.ResolveDotSuffix((ExprDotName)effectiveExpr, true, null, resolutionContext, true); + resolver.ResolveDotSuffix((ExprDotName)effectiveExpr, true, true, null, resolutionContext, true); } var callee = (MemberSelectExpr)((ConcreteSyntaxExpression)effectiveExpr).ResolvedExpression; if (callee == null) { @@ -110,7 +110,7 @@ public void Resolve(PreTypeResolver resolver, ResolutionContext resolutionContex if (exprClone is NameSegment) { resolver.ResolveNameSegment((NameSegment)exprClone, true, null, revealResolutionContext, true); } else { - resolver.ResolveDotSuffix((ExprDotName)exprClone, true, null, revealResolutionContext, true); + resolver.ResolveDotSuffix((ExprDotName)exprClone, true, true, null, revealResolutionContext, true); } var revealCallee = ((MemberSelectExpr)((ConcreteSyntaxExpression)exprClone).ResolvedExpression); diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs index e1be4a5584f..ef2929eadb7 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs @@ -187,7 +187,7 @@ public void ResolveExpression(Expression expr, ResolutionContext resolutionConte } case ExprDotName name: { var e = name; - ResolveDotSuffix(e, true, null, resolutionContext, false); + ResolveDotSuffix(e, false, true, null, resolutionContext, false); if (e.PreType is PreTypePlaceholderModule) { ReportError(e.tok, "name of module ({0}) is used as a variable", e.SuffixName); ResetTypeAssignment(e); // the rest of type checking assumes actual types @@ -1446,7 +1446,7 @@ private bool ResolveDatatypeConstructor(NameSegment expr, List/*? /// /// If false, generates an error if the name denotes a method. If true and the name denotes a method, returns /// a Resolver_MethodCall. - public Expression ResolveDotSuffix(ExprDotName expr, bool isLastNameSegment, List args, ResolutionContext resolutionContext, bool allowMethodCall) { + public Expression ResolveDotSuffix(ExprDotName expr, bool allowStaticReferenceToInstance, bool isLastNameSegment, List args, ResolutionContext resolutionContext, bool allowMethodCall) { Contract.Requires(expr != null); Contract.Requires(!expr.WasResolved()); Contract.Requires(resolutionContext != null); @@ -1458,7 +1458,7 @@ public Expression ResolveDotSuffix(ExprDotName expr, bool isLastNameSegment, Lis if (expr.Lhs is NameSegment) { ResolveNameSegment((NameSegment)expr.Lhs, false, null, nonRevealOpts, false); } else if (expr.Lhs is ExprDotName) { - ResolveDotSuffix((ExprDotName)expr.Lhs, false, null, nonRevealOpts, false); + ResolveDotSuffix((ExprDotName)expr.Lhs, false, false, null, nonRevealOpts, false); } else { ResolveExpression(expr.Lhs, nonRevealOpts); } @@ -1561,7 +1561,7 @@ public Expression ResolveDotSuffix(ExprDotName expr, bool isLastNameSegment, Lis if (!resolver.VisibleInScope(member)) { ReportError(expr.tok, $"member '{name}' has not been imported in this scope and cannot be accessed here"); } - if (!member.IsStatic) { + if (!member.IsStatic && !allowStaticReferenceToInstance) { ReportError(expr.tok, $"accessing member '{name}' requires an instance expression"); //TODO Unify with similar error messages // nevertheless, continue creating an expression that approximates a correct one } @@ -1720,7 +1720,7 @@ public MethodCallInformation ResolveApplySuffix(ApplySuffix e, ResolutionContext r = ResolveNameSegment((NameSegment)e.Lhs, true, e.Bindings.ArgumentBindings, resolutionContext, allowMethodCall); // note, if r is non-null, then e.Args have been resolved and r is a resolved expression that incorporates e.Args } else if (e.Lhs is ExprDotName) { - r = ResolveDotSuffix((ExprDotName)e.Lhs, true, e.Bindings.ArgumentBindings, resolutionContext, allowMethodCall); + r = ResolveDotSuffix((ExprDotName)e.Lhs, false, true, e.Bindings.ArgumentBindings, resolutionContext, allowMethodCall); // note, if r is non-null, then e.Args have been resolved and r is a resolved expression that incorporates e.Args } else { ResolveExpression(e.Lhs, resolutionContext); diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs index bd82d9a1159..caf13af4ff3 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs @@ -1202,7 +1202,7 @@ public void ResolveTypeRhs(TypeRhs rr, Statement stmt, ResolutionContext resolut PreType = rr.PreType }; var callLhs = new ExprDotName(((UserDefinedType)rr.EType).tok, lhs, initCallName, ret?.LastComponent.OptTypeArguments); - ResolveDotSuffix(callLhs, true, rr.Bindings.ArgumentBindings, resolutionContext, true); + ResolveDotSuffix(callLhs, false, true, rr.Bindings.ArgumentBindings, resolutionContext, true); if (prevErrorCount == ErrorCount) { Contract.Assert(callLhs.ResolvedExpression is MemberSelectExpr); // since ResolveApplySuffix succeeded and call.Lhs denotes an expression (not a module or a type) var methodSel = (MemberSelectExpr)callLhs.ResolvedExpression; diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealQualified.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealQualified.dfy new file mode 100644 index 00000000000..1a92f15d9e8 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealQualified.dfy @@ -0,0 +1,39 @@ +// RUN: %resolve --type-system-refresh --allow-axioms %s > %t +// RUN: %diff "%s.expect" "%t" + +module Prod { + class Foo { + function P(x: int): bool { + true + } + + static function Q(x: int): bool { + true + } + } + + method StaticRevealWorks() { + hide *; + + reveal Foo.P; + reveal Foo.Q; + } + + method InstanceRevealWorks(foo: Foo) { + hide *; + + reveal foo.P; + reveal foo.Q; + } +} + +module Cons { + import Prod + + method StaticRevealWorks() { + hide *; + + reveal Prod.Foo.P; + reveal Prod.Foo.Q; + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealQualified.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealQualified.dfy.expect new file mode 100644 index 00000000000..f829807e3d5 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealQualified.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier did not attempt verification diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017b.dfy.refresh.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017b.dfy.refresh.expect index fe87273dcb1..0e903fbdd61 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017b.dfy.refresh.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017b.dfy.refresh.expect @@ -13,11 +13,10 @@ git-issue-5017b.dfy(135,13): Error: only functions and constants can be revealed git-issue-5017b.dfy(136,13): Error: only functions and constants can be revealed git-issue-5017b.dfy(140,13): Error: predicate 'Valid' cannot be revealed, because it has no body in trait 'A' git-issue-5017b.dfy(141,13): Error: predicate 'Valid' cannot be revealed, because it has no body in trait 'A' -git-issue-5017b.dfy(145,13): Error: accessing member 'WithBody' requires an instance expression git-issue-5017b.dfy(117,13): Error: unresolved identifier: UnknownFunction git-issue-5017b.dfy(118,13): Error: unresolved identifier: UnknownFunction git-issue-5017b.dfy(119,13): Error: only functions and constants can be revealed git-issue-5017b.dfy(120,13): Error: only functions and constants can be revealed git-issue-5017b.dfy(124,13): Error: cannot reveal 'Valid' because no revealable constant, function, assert label, or requires label in the current scope is named 'Valid' git-issue-5017b.dfy(125,13): Error: cannot reveal 'Valid' because no revealable constant, function, assert label, or requires label in the current scope is named 'Valid' -22 resolution/type errors detected in git-issue-5017b.dfy +21 resolution/type errors detected in git-issue-5017b.dfy diff --git a/docs/dev/news/5760.fix b/docs/dev/news/5760.fix new file mode 100644 index 00000000000..60ee2dd58e6 --- /dev/null +++ b/docs/dev/news/5760.fix @@ -0,0 +1 @@ +The new resolver (accessible using `--type-system-refresh`) can now handle revealing instance functions using a static receiver, as it is the case for the current resolver \ No newline at end of file