fix: Fill in type arguments in implicit function-by-method postcondit…

…ion (#5068)

This PR fills in any type arguments `X` to the `result = F<X>(args)`
postcondition that's generated for the method part of a
`function-by-method` declaration.

Fixes #4998 

Reviewer notes: The desugaring of `function-by-method` is done in two
places in the code. I filled in the type arguments in both places.
However, in the second place (which is for `{:test}` functions/methods),
`dafny` would crash if any type parameters were declared (even for type
parameters that were not auto-init `(0)`). Since the `{:test}` was
already not allowed for functions/methods with parameters, I also added
error messages if `{:test}` is used with a function/method with type
parameters.

<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/ModuleResolver.cs

@@ -777,7 +777,7 @@ public void RegisterByMethod(Function f, TopLevelDeclWithMembers cl) {
       var isStatic = f.HasStaticKeyword || cl is DefaultClassDecl;
       var receiver = isStatic ? (Expression)new StaticReceiverExpr(tok, cl, true) : new ImplicitThisExpr(tok);
       var fn = new ApplySuffix(tok, null,
-        new ExprDotName(tok, receiver, f.Name, null),
+        new ExprDotName(tok, receiver, f.Name, f.TypeArgs.ConvertAll(typeParameter => (Type)new UserDefinedType(f.tok, typeParameter))),
         new ActualBindings(f.Formals.ConvertAll(Expression.CreateIdentExpr)).ArgumentBindings,
         tok);
       var post = new AttributedExpression(new BinaryExpr(tok, BinaryExpr.Opcode.Eq, r, fn));

Source/DafnyCore/Rewriters/ExpectContracts.cs

@@ -18,8 +18,10 @@ namespace Microsoft.Dafny;
 public class ExpectContracts : IRewriter {
   private readonly ClonerButDropMethodBodies cloner = new(true);
   private readonly Dictionary<MemberDecl, MemberDecl> wrappedDeclarations = new();
+  private readonly SystemModuleManager systemModuleManager;
 
-  public ExpectContracts(ErrorReporter reporter) : base(reporter) {
+  public ExpectContracts(ErrorReporter reporter, SystemModuleManager systemModuleManager) : base(reporter) {
+    this.systemModuleManager = systemModuleManager;
   }
 
   /// <summary>
@@ -112,12 +114,8 @@ private MemberDecl GenerateFunctionWrapper(TopLevelDeclWithMembers parent, Membe
 
     var args = newFunc.Formals.Select(Expression.CreateIdentExpr).ToList();
     var receiver = ModuleResolver.GetReceiver(parent, origFunc, decl.tok);
-    var callExpr = new FunctionCallExpr(tok, origFunc.Name, receiver, null, null, args) {
-      Function = origFunc,
-      TypeApplication_JustFunction = newFunc.TypeArgs.Select(tp => (Type)new UserDefinedType(tp)).ToList(),
-      TypeApplication_AtEnclosingClass = parent.TypeArgs.Select(tp => (Type)new UserDefinedType(tp)).ToList(),
-      Type = newFunc.ResultType,
-    };
+    var callExpr = Expression.CreateResolvedCall(tok, receiver, origFunc, args,
+      newFunc.TypeArgs.Select(tp => (Type)new UserDefinedType(tp)).ToList(), systemModuleManager);
 
     newFunc.Body = callExpr;
 
@@ -185,7 +183,7 @@ private MemberDecl GenerateMethodWrapper(TopLevelDeclWithMembers parent, MemberD
   }
 
 
-  private static void RegisterResolvedByMethod(Function f, TopLevelDeclWithMembers cl) {
+  private void RegisterResolvedByMethod(Function f, TopLevelDeclWithMembers cl) {
 
     var tok = f.ByMethodTok;
     var resultVar = f.Result ?? new Formal(tok, "#result", f.ResultType, false, false, null);
@@ -195,8 +193,8 @@ private static void RegisterResolvedByMethod(Function f, TopLevelDeclWithMembers
     // been set. Instead, we compute here directly from f.HasStaticKeyword and "cl".
     var isStatic = f.HasStaticKeyword || cl is DefaultClassDecl;
     var receiver = isStatic ? (Expression)new StaticReceiverExpr(tok, cl, true) : new ImplicitThisExpr(tok);
-    var fn = new FunctionCallExpr(tok, f.Name, receiver, null, null,
-      f.Formals.ConvertAll(Expression.CreateIdentExpr));
+    var fn = Expression.CreateResolvedCall(tok, receiver, f, f.Formals.ConvertAll(Expression.CreateIdentExpr),
+      f.TypeArgs.ConvertAll(typeParameter => (Type)new UserDefinedType(f.tok, typeParameter)), systemModuleManager);
     var post = new AttributedExpression(new BinaryExpr(tok, BinaryExpr.Opcode.Eq, r, fn) {
       Type = Type.Bool
     });

Source/DafnyCore/Rewriters/RewriterCollection.cs

@@ -26,7 +26,7 @@ public static IList<IRewriter> GetRewriters(ErrorReporter reporter, Program prog
     }
 
     if (reporter.Options.TestContracts != DafnyOptions.ContractTestingMode.None) {
-      result.Add(new ExpectContracts(reporter));
+      result.Add(new ExpectContracts(reporter, program.SystemModuleManager));
     }
 
     if (reporter.Options.Get(RunAllTestsMainMethod.IncludeTestRunner)) {

Source/DafnyCore/Rewriters/RewriterErrors.cs

@@ -17,6 +17,7 @@ public enum ErrorId {
     rw_unusual_indentation_start,
     rw_unusual_indentation_end,
     rw_test_methods_may_not_have_inputs,
+    rw_test_methods_may_not_have_type_parameters,
     rw_test_method_has_too_many_returns,
     rw_clause_cannot_be_compiled,
     rw_no_wrapper,

Source/DafnyCore/Rewriters/RunAllTestsMainMethod.cs

@@ -150,6 +150,12 @@ internal override void PostResolve(Program program) {
             continue;
           }
 
+          if (method.TypeArgs.Count != 0) {
+            ReportError(ErrorId.rw_test_methods_may_not_have_type_parameters, method.tok,
+              "Methods with the :test attribute may not have type parameters");
+            continue;
+          }
+
           Expression resultVarExpr = null;
           var lhss = new List<Expression>();
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AllExterns.dfy.expect

@@ -13,5 +13,6 @@ GenFunctionTest: FAILED
 GenMethodTest: FAILED
 	CheckExtern.dfy(59,13): Runtime failure of requires clause from CheckExtern.dfy(59,13)
 BazTest: PASSED
+CallFunctionByMethod: PASSED
 [Program halted] AllExterns.dfy(8,0): Test failures occurred: see above.
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/Inputs/CheckExtern.dfy

@@ -75,3 +75,16 @@ method {:test} BazTest()
   // already ensure that y == 3.
   expect y != 7;
 }
+
+predicate UnusedTypeParameterForFunctionByMethod<A(0)>() {
+  true
+} by method {
+  var a: A := *;
+  var b: A := a;
+  return true;
+}
+
+method {:test} CallFunctionByMethod() {
+  var t := UnusedTypeParameterForFunctionByMethod<real>();
+  expect t;
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.dfy.expect

@@ -14,5 +14,6 @@ GenFunctionTest: FAILED
 GenMethodTest: FAILED
 	CheckExtern.dfy(59,13): Runtime failure of requires clause from CheckExtern.dfy(59,13)
 BazTest: PASSED
+CallFunctionByMethod: PASSED
 [Program halted] TestedExterns.dfy(8,0): Test failures occurred: see above.
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3839/git-issue-3839a.dfy

@@ -1,8 +1,22 @@
 // RUN: ! %baredafny test --use-basename-for-filename --show-snippets:false "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-method {:test} M(x: int) returns (r: int)
+method {:test} M(x: int) returns (r: int) // error: in-parameters not supported
 {
-    expect x != x;
-    return x;
+  expect x != x;
+  return x;
+}
+
+method {:test} MethodWithTypeParameters<X(0)>() returns (y: X) { // error: type parameters not supported
+  y := *;
+}
+
+method {:test} MethodWithTypeParameter<X>() returns (u: seq<X>) { // error: type parameters not supported
+  u := [];
+}
+
+predicate {:test} UnusedTypeParameterForFunctionByMethod<A>() { // error: type parameters not supported
+  true
+} by method {
+  return true;
 }

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3839/git-issue-3839a.dfy.expect

@@ -1,2 +1,5 @@
 git-issue-3839a.dfy(4,15): Error: Methods with the :test attribute may not have input arguments
-1 resolution/type errors detected in git-issue-3839a.dfy
+git-issue-3839a.dfy(10,15): Error: Methods with the :test attribute may not have type parameters
+git-issue-3839a.dfy(14,15): Error: Methods with the :test attribute may not have type parameters
+git-issue-3839a.dfy(18,18): Error: Methods with the :test attribute may not have type parameters
+4 resolution/type errors detected in git-issue-3839a.dfy

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4998.dfy

@@ -0,0 +1,8 @@
+// RUN: %testDafnyForEachResolver "%s"
+
+// this once crashed, because the implicit postcondition didn't include the type parameter
+predicate Foo<A>() {
+  true
+} by method {
+  return true;
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4998.dfy.expect

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

docs/dev/news/5068.fix

@@ -0,0 +1 @@
+Don't emit an error message for a `function-by-method` with unused type parameters.