From 728433a99a96394b14dff8862c14b1dc4b00d1f8 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 8 Feb 2024 07:05:25 -0800 Subject: [PATCH] fix: Fill in type arguments in implicit function-by-method postcondition (#5068) This PR fills in any type arguments `X` to the `result = F(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. 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). --- Source/DafnyCore/Resolver/ModuleResolver.cs | 2 +- Source/DafnyCore/Rewriters/ExpectContracts.cs | 18 ++++++++--------- .../DafnyCore/Rewriters/RewriterCollection.cs | 2 +- Source/DafnyCore/Rewriters/RewriterErrors.cs | 1 + .../Rewriters/RunAllTestsMainMethod.cs | 6 ++++++ .../contract-wrappers/AllExterns.dfy.expect | 1 + .../contract-wrappers/Inputs/CheckExtern.dfy | 13 ++++++++++++ .../TestedExterns.dfy.expect | 1 + .../git-issue-3839/git-issue-3839a.dfy | 20 ++++++++++++++++--- .../git-issue-3839/git-issue-3839a.dfy.expect | 5 ++++- .../LitTest/git-issues/git-issue-4998.dfy | 8 ++++++++ .../git-issues/git-issue-4998.dfy.expect | 2 ++ docs/dev/news/5068.fix | 1 + 13 files changed, 64 insertions(+), 16 deletions(-) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4998.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4998.dfy.expect create mode 100644 docs/dev/news/5068.fix diff --git a/Source/DafnyCore/Resolver/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs index 9c8f34e5191..09de13eb308 100644 --- a/Source/DafnyCore/Resolver/ModuleResolver.cs +++ b/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)); diff --git a/Source/DafnyCore/Rewriters/ExpectContracts.cs b/Source/DafnyCore/Rewriters/ExpectContracts.cs index e493d9d7b7d..22790e612ac 100644 --- a/Source/DafnyCore/Rewriters/ExpectContracts.cs +++ b/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 wrappedDeclarations = new(); + private readonly SystemModuleManager systemModuleManager; - public ExpectContracts(ErrorReporter reporter) : base(reporter) { + public ExpectContracts(ErrorReporter reporter, SystemModuleManager systemModuleManager) : base(reporter) { + this.systemModuleManager = systemModuleManager; } /// @@ -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 }); diff --git a/Source/DafnyCore/Rewriters/RewriterCollection.cs b/Source/DafnyCore/Rewriters/RewriterCollection.cs index d06393da5ef..c2e1c05b3ba 100644 --- a/Source/DafnyCore/Rewriters/RewriterCollection.cs +++ b/Source/DafnyCore/Rewriters/RewriterCollection.cs @@ -26,7 +26,7 @@ public static IList 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)) { diff --git a/Source/DafnyCore/Rewriters/RewriterErrors.cs b/Source/DafnyCore/Rewriters/RewriterErrors.cs index 276d4a0aee5..f8430120c20 100644 --- a/Source/DafnyCore/Rewriters/RewriterErrors.cs +++ b/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, diff --git a/Source/DafnyCore/Rewriters/RunAllTestsMainMethod.cs b/Source/DafnyCore/Rewriters/RunAllTestsMainMethod.cs index e22b9684858..7ce2cf36a0e 100644 --- a/Source/DafnyCore/Rewriters/RunAllTestsMainMethod.cs +++ b/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(); diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AllExterns.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AllExterns.dfy.expect index 0cf0890ae3d..6cd7d8f73f1 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AllExterns.dfy.expect +++ b/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. diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/Inputs/CheckExtern.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/Inputs/CheckExtern.dfy index a947d4544f6..5beeb2bd0e9 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/Inputs/CheckExtern.dfy +++ b/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() { + true +} by method { + var a: A := *; + var b: A := a; + return true; +} + +method {:test} CallFunctionByMethod() { + var t := UnusedTypeParameterForFunctionByMethod(); + expect t; +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.dfy.expect index 3d25b4f5879..f247ee2efd9 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.dfy.expect +++ b/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. diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3839/git-issue-3839a.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3839/git-issue-3839a.dfy index 467b950aafe..4a596b71ba0 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3839/git-issue-3839a.dfy +++ b/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() returns (y: X) { // error: type parameters not supported + y := *; +} + +method {:test} MethodWithTypeParameter() returns (u: seq) { // error: type parameters not supported + u := []; +} + +predicate {:test} UnusedTypeParameterForFunctionByMethod() { // error: type parameters not supported + true +} by method { + return true; } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3839/git-issue-3839a.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3839/git-issue-3839a.dfy.expect index 06d273e175f..d134c938e17 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3839/git-issue-3839a.dfy.expect +++ b/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 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4998.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4998.dfy new file mode 100644 index 00000000000..e053bc78edb --- /dev/null +++ b/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() { + true +} by method { + return true; +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4998.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4998.dfy.expect new file mode 100644 index 00000000000..823a60a105c --- /dev/null +++ b/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 diff --git a/docs/dev/news/5068.fix b/docs/dev/news/5068.fix new file mode 100644 index 00000000000..64c95d5ffc7 --- /dev/null +++ b/docs/dev/news/5068.fix @@ -0,0 +1 @@ +Don't emit an error message for a `function-by-method` with unused type parameters.