Make hide/reveal work for the old resolver

Source/DafnyCore/AST/Statements/Verification/HideRevealStmt.cs

@@ -5,7 +5,7 @@
 
 namespace Microsoft.Dafny;
 
-public class HideRevealStmt : Statement, ICloneable<HideRevealStmt>, ICanFormat {
+public class HideRevealStmt : Statement, ICloneable<HideRevealStmt>, ICanFormat, ICanResolveNewAndOld {
   public const string RevealLemmaPrefix = "reveal_";
 
   public string Kind => Mode == HideRevealCmd.Modes.Hide ? "hide" : "reveal";
@@ -72,7 +72,7 @@ public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {
     return formatter.SetIndentPrintRevealStmt(indentBefore, OwnedTokens);
   }
 
-  public void Resolve(PreTypeResolver resolver, ResolutionContext resolutionContext) {
+  public override void GenResolve(INewOrOldResolver resolver, ResolutionContext resolutionContext) {
     ((ICodeContainer)resolutionContext.CodeContext).ContainsHide |= Mode == HideRevealCmd.Modes.Hide;
 
     if (Wildcard) {
@@ -93,33 +93,38 @@ public void Resolve(PreTypeResolver resolver, ResolutionContext resolutionContex
           effectiveExpr = applySuffix.Lhs;
         }
         if (effectiveExpr is NameSegment or ExprDotName) {
-          if (effectiveExpr is NameSegment) {
-            resolver.ResolveNameSegment((NameSegment)effectiveExpr, true, null, resolutionContext, true);
+          if (effectiveExpr is NameSegment segment) {
+            resolver.ResolveNameSegment(segment, true, null, resolutionContext, true);
           } else {
             resolver.ResolveDotSuffix((ExprDotName)effectiveExpr, true, true, null, resolutionContext, true);
           }
-          var callee = (MemberSelectExpr)((ConcreteSyntaxExpression)effectiveExpr).ResolvedExpression;
-          if (callee == null) {
+
+          if (effectiveExpr.Resolved == null) {
             // error from resolving child
+          } else if (effectiveExpr.Resolved is not MemberSelectExpr callee) {
+            resolver.Reporter.Error(MessageSource.Resolver, effectiveExpr.Tok,
+              $"cannot reveal '{name}' because no revealable constant, function, assert label, or requires label in the current scope is named '{name}'");
           } else {
             if (callee.Member is Function or ConstantField) {
               OffsetMembers.Add(callee.Member);
-              if (callee.Member.IsOpaque && Mode == HideRevealCmd.Modes.Reveal) {
-                var revealResolutionContext = resolutionContext with { InReveal = true };
-                var exprClone = new Cloner().CloneExpr(effectiveExpr);
-                if (exprClone is NameSegment) {
-                  resolver.ResolveNameSegment((NameSegment)exprClone, true, null, revealResolutionContext, true);
-                } else {
-                  resolver.ResolveDotSuffix((ExprDotName)exprClone, true, true, null, revealResolutionContext, true);
-                }
-
-                var revealCallee = ((MemberSelectExpr)((ConcreteSyntaxExpression)exprClone).ResolvedExpression);
-                if (revealCallee != null) {
-                  var call = new CallStmt(RangeToken, new List<Expression>(),
-                    revealCallee,
-                    new List<ActualBinding>(), effectiveExpr.tok);
-                  ResolvedStatements.Add(call);
-                }
+              if (!BoogieGenerator.IsOpaque(callee.Member, resolver.Options) || Mode != HideRevealCmd.Modes.Reveal) {
+                continue;
+              }
+
+              var revealResolutionContext = resolutionContext with { InReveal = true };
+              var exprClone = new Cloner().CloneExpr(effectiveExpr);
+              if (exprClone is NameSegment nameSegment) {
+                resolver.ResolveNameSegment(nameSegment, true, null, revealResolutionContext, true);
+              } else {
+                resolver.ResolveDotSuffix((ExprDotName)exprClone, true, true, null, revealResolutionContext, true);
+              }
+
+              var revealCallee = ((MemberSelectExpr)((ConcreteSyntaxExpression)exprClone).ResolvedExpression);
+              if (revealCallee != null) {
+                var call = new CallStmt(RangeToken, new List<Expression>(),
+                  revealCallee,
+                  new List<ActualBinding>(), effectiveExpr.tok);
+                ResolvedStatements.Add(call);
               }
             } else {
               resolver.Reporter.Error(MessageSource.Resolver, effectiveExpr.Tok,

Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs

@@ -544,7 +544,7 @@ public void ResolveExpressionX(Expression expr, ResolutionContext resolutionCont
 
       } else if (expr is ExprDotName) {
         var e = (ExprDotName)expr;
-        ResolveDotSuffix(e, true, null, resolutionContext, false);
+        ResolveDotSuffix(e, false, true, null, resolutionContext, false);
         if (e.Type is Resolver_IdentifierExpr.ResolverType_Module) {
           reporter.Error(MessageSource.Resolver, e.tok, "name of module ({0}) is used as a variable", e.SuffixName);
           e.ResetTypeAssignment();  // the rest of type checking assumes actual types
@@ -3500,50 +3500,7 @@ public void ResolveStatement(Statement stmt, ResolutionContext resolutionContext
         s.Args.ForEach(e => ResolveExpression(e, resolutionContext));
 
       } else if (stmt is HideRevealStmt hideRevealStmt) {
-        foreach (var expr in hideRevealStmt.Exprs) {
-          var name = HideRevealStmt.SingleName(expr);
-          var labeledAssert = name == null ? null : DominatingStatementLabels.Find(name) as AssertLabel;
-          if (labeledAssert != null) {
-            hideRevealStmt.LabeledAsserts.Add(labeledAssert);
-          } else {
-            var revealResolutionContext = resolutionContext with { InReveal = true };
-            if (expr is ApplySuffix) {
-              var e = (ApplySuffix)expr;
-              var methodCallInfo = ResolveApplySuffix(e, revealResolutionContext, true);
-              if (methodCallInfo == null) {
-                // 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) {
-                Contract.Assert(methodCallInfo.Callee.Member is TwoStateLemma);
-                reporter.Error(MessageSource.Resolver, methodCallInfo.Tok, "to reveal a two-state function, do not list any parameters or @-labels");
-              } else {
-                var call = new CallStmt(hideRevealStmt.RangeToken, new List<Expression>(), methodCallInfo.Callee, methodCallInfo.ActualParameters, methodCallInfo.Tok);
-                hideRevealStmt.ResolvedStatements.Add(call);
-              }
-            } else if (expr is NameSegment or ExprDotName) {
-              if (expr is NameSegment) {
-                ResolveNameSegment((NameSegment)expr, true, null, revealResolutionContext, true);
-              } else {
-                ResolveDotSuffix((ExprDotName)expr, true, null, revealResolutionContext, true);
-              }
-              MemberSelectExpr callee = (MemberSelectExpr)((ConcreteSyntaxExpression)expr).ResolvedExpression;
-              if (callee == null) {
-              } else if (callee.Member is Lemma or TwoStateLemma && Attributes.Contains(callee.Member.Attributes, "axiom")) {
-                //The revealed member is a function
-                reporter.Error(MessageSource.Resolver, callee.tok, "to reveal a function ({0}), append parentheses", callee.Member.ToString().Substring(7));
-              } else {
-                var call = new CallStmt(hideRevealStmt.RangeToken, new List<Expression>(), callee, new List<ActualBinding>(), expr.tok);
-                hideRevealStmt.ResolvedStatements.Add(call);
-              }
-            } else {
-              ResolveExpression(expr, revealResolutionContext);
-            }
-          }
-        }
-        foreach (var a in hideRevealStmt.ResolvedStatements) {
-          ResolveStatement(a, resolutionContext);
-        }
+        stmt.GenResolve(this, resolutionContext);
       } else if (stmt is BreakStmt) {
         var s = (BreakStmt)stmt;
         if (s.TargetLabel != null) {
@@ -4448,7 +4405,7 @@ public void ResolveTypeRhs(TypeRhs rr, Statement stmt, ResolutionContext resolut
               // type, create a dot-suffix expression around this receiver, and then resolve it in the usual way for dot-suffix expressions.
               var lhs = new ImplicitThisExpr_ConstructorCall(initCallTok) { Type = rr.EType };
               var callLhs = new ExprDotName(((UserDefinedType)rr.EType).tok, lhs, initCallName, ret == null ? null : ret.LastComponent.OptTypeArguments);
-              ResolveDotSuffix(callLhs, true, rr.Bindings.ArgumentBindings, resolutionContext, true);
+              ResolveDotSuffix(callLhs, false, true, rr.Bindings.ArgumentBindings, resolutionContext, true);
               if (prevErrorCount == reporter.Count(ErrorLevel.Error)) {
                 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;
@@ -5604,7 +5561,7 @@ void ResolveNameSegment_Type(NameSegment expr, ResolutionContext resolutionConte
     /// <param name="resolutionContext"></param>
     /// <param name="allowMethodCall">If false, generates an error if the name denotes a method. If true and the name denotes a method, returns
     /// a Resolver_MethodCall.</param>
-    Expression ResolveDotSuffix(ExprDotName expr, bool isLastNameSegment, List<ActualBinding> args, ResolutionContext resolutionContext, bool allowMethodCall) {
+    public Expression ResolveDotSuffix(ExprDotName expr, bool allowStaticReferenceToInstance, bool isLastNameSegment, List<ActualBinding> args, ResolutionContext resolutionContext, bool allowMethodCall) {
       Contract.Requires(expr != null);
       Contract.Requires(!expr.WasResolved());
       Contract.Requires(resolutionContext != null);
@@ -5617,7 +5574,7 @@ Expression ResolveDotSuffix(ExprDotName expr, bool isLastNameSegment, List<Actua
       if (expr.Lhs is NameSegment) {
         ResolveNameSegment((NameSegment)expr.Lhs, false, null, nonRevealOpts, false, true, out shadowedImport);
       } 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);
       }
@@ -5726,7 +5683,7 @@ Expression ResolveDotSuffix(ExprDotName expr, bool isLastNameSegment, List<Actua
             if (!VisibleInScope(member)) {
               reporter.Error(MessageSource.Resolver, expr.tok, "member '{0}' has not been imported in this scope and cannot be accessed here", name);
             }
-            if (!member.IsStatic) {
+            if (!member.IsStatic && !allowStaticReferenceToInstance) {
               reporter.Error(MessageSource.Resolver, expr.tok, "accessing member '{0}' requires an instance expression", name); //TODO Unify with similar error messages
               // nevertheless, continue creating an expression that approximates a correct one
             }
@@ -5890,7 +5847,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);

Source/DafnyCore/Resolver/PreType/INewOrOldResolver.cs

@@ -31,4 +31,10 @@ void ResolveFrameExpression(
     FrameExpression frameExpression,
     FrameExpressionUse frameExpressionUse,
     ResolutionContext context);
+
+  public Expression ResolveNameSegment(NameSegment expr, bool isLastNameSegment, List<ActualBinding> args,
+    ResolutionContext resolutionContext, bool allowMethodCall, bool complain = true);
+
+  public Expression ResolveDotSuffix(ExprDotName expr, bool allowStaticReferenceToInstance, bool isLastNameSegment, List<ActualBinding> args,
+    ResolutionContext resolutionContext, bool allowMethodCall);
 }

Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs

@@ -1164,6 +1164,11 @@ private void ReportMemberNotFoundError(IToken tok, string memberName, [CanBeNull
       }
     }
 
+    public Expression ResolveNameSegment(NameSegment expr, bool isLastNameSegment, List<ActualBinding> args,
+      ResolutionContext resolutionContext, bool allowMethodCall, bool complain = true) {
+      return ResolveNameSegment(expr, isLastNameSegment, args, resolutionContext, allowMethodCall, complain, false);
+    }
+
     /// <summary>
     /// Look up expr.Name in the following order:
     ///  0. Local variable, parameter, or bound variable.
@@ -1192,7 +1197,7 @@ private void ReportMemberNotFoundError(IToken tok, string memberName, [CanBeNull
     /// there is no "this" in scope. This seems like a terrible hack, because it breaks scope invariants about the AST. But, for now, it's here
     /// to mimic what the legacy resolver does.</param>
     public Expression ResolveNameSegment(NameSegment expr, bool isLastNameSegment, List<ActualBinding> args,
-      ResolutionContext resolutionContext, bool allowMethodCall, bool complain = true, bool specialOpaqueHackAllowance = false) {
+      ResolutionContext resolutionContext, bool allowMethodCall, bool complain, bool specialOpaqueHackAllowance) {
       Contract.Requires(expr != null);
       Contract.Requires(!expr.WasResolved());
       Contract.Requires(resolutionContext != null);

Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs

@@ -112,8 +112,6 @@ public void ResolveStatement(Statement stmt, ResolutionContext resolutionContext
           ResolveExpression(e, resolutionContext);
         }
 
-      } else if (stmt is HideRevealStmt hideRevealStmt) {
-        hideRevealStmt.Resolve(this, resolutionContext);
       } else if (stmt is BreakStmt) {
         var s = (BreakStmt)stmt;
         if (s.TargetLabel != null) {

Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs

@@ -1023,7 +1023,7 @@ public void ResolveAttributes(IAttributeBearingDeclaration attributeHost, Resolu
         if (attr.Args != null) {
           foreach (var arg in attr.Args) {
             if (Attributes.Contains(attributeHost.Attributes, "opaque_reveal") && attr.Name is "revealedFunction" && arg is NameSegment nameSegment) {
-              ResolveNameSegment(nameSegment, true, null, opts, false, specialOpaqueHackAllowance: true);
+              ResolveNameSegment(nameSegment, true, null, opts, false, complain: true, specialOpaqueHackAllowance: true);
             } else {
               ResolveExpression(arg, opts);
             }

Source/DafnyCore/Verifier/BoogieGenerator.Fields.cs

@@ -118,7 +118,7 @@ Bpl.Function GetReadonlyField(Field f) {
           var cf = (ConstantField)f;
           if (cf.Rhs != null && RevealedInScope(cf)) {
             var etran = new ExpressionTranslator(this, predef, NewOneHeapExpr(f.tok), null);
-            if (!IsOpaque(cf)) {
+            if (!IsOpaque(cf, options)) {
               var definitionAxiom = ff.CreateDefinitionAxiom(etran.TrExpr(cf.Rhs));
               definitionAxiom.CanHide = true;
               sink.AddTopLevelDeclaration(definitionAxiom);

Source/DafnyCore/Verifier/BoogieGenerator.cs

@@ -1378,9 +1378,9 @@ public Bpl.Expr GetArrayIndexFieldName(IToken tok, List<Bpl.Expr> indices) {
     bool FunctionBodyIsAvailable(Function f, ModuleDefinition context, VisibilityScope scope, bool revealProtectedBody) {
       Contract.Requires(f != null);
       Contract.Requires(context != null);
-      return f.Body != null && !IsOpaque(f) && f.IsRevealedInScope(scope);
+      return f.Body != null && !IsOpaque(f, options) && f.IsRevealedInScope(scope);
     }
-    bool IsOpaque(MemberDecl f) {
+    public static bool IsOpaque(MemberDecl f, DafnyOptions options) {
       Contract.Requires(f != null);
       if (f is Function f1) {
         return Attributes.Contains(f.Attributes, "opaque") || f.IsOpaque || f1.IsMadeImplicitlyOpaque(options);

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/LabeledAssertsResolution.dfy.expect

@@ -7,7 +7,7 @@ LabeledAssertsResolution.dfy(34,24): Error: assert label shadows a dominating la
 LabeledAssertsResolution.dfy(73,12): Error: break label is undefined or not in scope: ABC
 LabeledAssertsResolution.dfy(81,17): Error: cannot reveal 'C' because no revealable constant, function, assert label, or requires label in the current scope is named 'C'
 LabeledAssertsResolution.dfy(94,17): Error: no label 'XYZ' in scope at this time
-LabeledAssertsResolution.dfy(115,14): Error: cannot reveal 'X' because no revealable constant, function, assert label, or requires label in the current scope is named 'X'
+LabeledAssertsResolution.dfy(115,14): Error: unresolved identifier: X
 LabeledAssertsResolution.dfy(52,11): Error: assert label shadows a dominating label
 LabeledAssertsResolution.dfy(54,11): Error: assert label shadows a dominating label
 LabeledAssertsResolution.dfy(125,6): Error: an assert-by body is not allowed to update a variable it doesn't declare

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/OpaqueConstants.dfy

@@ -12,7 +12,7 @@ module Module {
     } else {
       reveal M.Five;
       assert M.Five == 5;
-    }
+    }    
   }
 }
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Twostate-Resolution.dfy

@@ -478,21 +478,21 @@ module TwoStateAt {
   method UseOrdinaryOpaque() {
     label L:
     reveal OrdinaryOpaque();
-    reveal OrdinaryOpaque;  // error: missing parentheses
+    reveal OrdinaryOpaque;
     reveal OrdinaryOpaque@K();  // error: label K not in scope
     reveal OrdinaryOpaque@L();  // error: @ can only be applied to something two-state (error message can be improved)
   }
   ghost function FuncUseOrdinaryOpaque(): int {
     reveal OrdinaryOpaque();
-    reveal OrdinaryOpaque;  // error: missing parentheses
+    reveal OrdinaryOpaque;
     reveal OrdinaryOpaque@K();  // error: label K not in scope
     10
   }
   twostate function {:opaque} Opaque(): int { 12 }
   method UseOpaque() {
     label L:
     reveal Opaque();
-    reveal Opaque;  // error: missing parentheses
+    reveal Opaque;
     reveal Opaque@K();  // error: label K not in scope
     reveal Opaque@L();  // error: all parameters in a reveal must be implicit, including labels
   }
@@ -504,7 +504,7 @@ module TwoStateAt {
   }
   twostate function TwoFuncUseOpaque(): int {
     reveal Opaque();
-    reveal Opaque;  // error: missing parentheses
+    reveal Opaque;
     reveal Opaque@K();  // error: label K not in scope
     10
   }