Fix: dafny-lang#4315, allowing static reveal lemmas to reference non-…

…static original procedures (dafny-lang#4319)

This PR fixes dafny-lang#4315
I added the corresponding test.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs

@@ -316,7 +316,11 @@ public void ResolveAttributes(IAttributeBearingDeclaration attributeHost, Resolu
         if (attr.Args != null) {
           foreach (var arg in attr.Args) {
             Contract.Assert(arg != null);
-            ResolveExpression(arg, resolutionContext);
+            if (!(Attributes.Contains(attributeHost.Attributes, "opaque_reveal") && attr.Name == "fuel" && arg is NameSegment)) {
+              ResolveExpression(arg, resolutionContext);
+            } else {
+              ResolveRevealLemmaAttribute(arg);
+            }
           }
         }
       }
@@ -326,6 +330,49 @@ public void ResolveAttributes(IAttributeBearingDeclaration attributeHost, Resolu
       }
     }
 
+    // <summary>
+    // Manually resolving NameSegments that are present in fuel attributes of reveal lemmas.
+    // This is because reveal lemmas are static and we want to allow a reference to non-static original procedures
+    // in static context in this setting.
+    //
+    // Most of the following code is copied from AnnotateRevealFunction() in OpaqueMemberRewriter.cs.
+    // </summary>
+    public void ResolveRevealLemmaAttribute(Expression arg) {
+      MemberDecl member = null;
+      var ret = GetClassMembers(currentClass).TryGetValue(((NameSegment)arg).Name, out member);
+      Contract.Assert(ret);
+
+      var f = (Function)member;
+      Expression receiver;
+      if (f.IsStatic) {
+        receiver = new StaticReceiverExpr(f.tok, (TopLevelDeclWithMembers)f.EnclosingClass, true);
+      } else {
+        receiver = new ImplicitThisExpr(f.tok);
+        receiver.Type = GetThisType(f.tok, (TopLevelDeclWithMembers)member.EnclosingClass);
+      }
+
+      var typeApplication = new List<Type>();
+      var typeApplication_JustForMember = new List<Type>();
+      for (int i = 0; i < f.TypeArgs.Count; i++) {
+        // doesn't matter what type, just so we have it to make the resolver happy when resolving function member of
+        // the fuel attribute. This might not be needed after fixing codeplex issue #172.
+        typeApplication.Add(new IntType());
+        typeApplication_JustForMember.Add(new IntType());
+      }
+
+      var rr = new MemberSelectExpr(f.tok, receiver, f.Name);
+      rr.Member = f;
+      rr.TypeApplication_AtEnclosingClass = typeApplication;
+      rr.TypeApplication_JustMember = typeApplication_JustForMember;
+      List<Type> args = new List<Type>();
+      for (int i = 0; i < f.Formals.Count; i++) {
+        args.Add(new IntType());
+      }
+      rr.Type = new ArrowType(f.tok, args, new IntType());
+      ((NameSegment)arg).ResolvedExpression = rr;
+      arg.Type = rr.Type;
+    }
+
     /// <summary>
     /// "IsTwoState" implies that "old" and "fresh" expressions are allowed.
     /// </summary>

Test/git-issues/git-issue-4315.dfy

@@ -0,0 +1,11 @@
+// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+module M1 {
+  class C {
+    opaque function f() : bool { true }
+  }
+}
+
+module M2 refines M1 {
+}

Test/git-issues/git-issue-4315.dfy.expect

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 0 verified, 0 errors

docs/dev/news/4315.fix

@@ -0,0 +1 @@
+Refining an abstract module with a class with an opaque function no longer crashes