From 9e90e56fb449fd6bb36c3002396b0141e9d10ccb Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Tue, 21 May 2024 18:45:53 +0200 Subject: [PATCH 1/6] fix #4684 --- Source/DafnyCore/AST/Substituter.cs | 6 +-- .../Backends/Python/PythonCodeGenerator.cs | 2 +- .../Backends/SinglePassCodeGenerator.cs | 15 +++++++ .../LitTest/git-issues/git-issue-4684.dfy | 44 +++++++++++++++++++ .../git-issues/git-issue-4684.dfy.expect | 2 + .../git-issues/git-issue-4684.dfy.rs.check | 1 + 6 files changed, 66 insertions(+), 4 deletions(-) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4684.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4684.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4684.dfy.rs.check diff --git a/Source/DafnyCore/AST/Substituter.cs b/Source/DafnyCore/AST/Substituter.cs index ea0a86f23c2..b0ad9564682 100644 --- a/Source/DafnyCore/AST/Substituter.cs +++ b/Source/DafnyCore/AST/Substituter.cs @@ -12,9 +12,9 @@ namespace Microsoft.Dafny { /// particular, the substituter does not copy parts of an expression that are used only for well-formedness checks. /// public class Substituter { - protected readonly Expression receiverReplacement; - protected readonly Dictionary substMap; - protected readonly Dictionary typeMap; + protected Expression receiverReplacement { get; } + protected Dictionary substMap { get; } + protected Dictionary typeMap { get; } protected readonly Label oldHeapLabel; [CanBeNull] protected readonly SystemModuleManager SystemModuleManager; // if non-null, substitutions into FunctionCallExpr's will be wrapped diff --git a/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs b/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs index 57993aaa13c..95e58988ad7 100644 --- a/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs @@ -1169,7 +1169,7 @@ protected override string FullTypeName(UserDefinedType udt, MemberDecl member = }; } - protected override void EmitThis(ConcreteSyntaxTree wr, bool callToInheritedMember) { + protected override void EmitThis(ConcreteSyntaxTree wr, bool _ = false) { var isTailRecursive = enclosingMethod is { IsTailRecursive: true } || enclosingFunction is { IsTailRecursive: true }; wr.Write(isTailRecursive ? "_this" : "self"); } diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator.cs b/Source/DafnyCore/Backends/SinglePassCodeGenerator.cs index 3cd40978592..6c62d82c28e 100644 --- a/Source/DafnyCore/Backends/SinglePassCodeGenerator.cs +++ b/Source/DafnyCore/Backends/SinglePassCodeGenerator.cs @@ -5647,7 +5647,22 @@ void EmitExpr(Expression e2, ConcreteSyntaxTree wr2, bool inLetExpr, ConcreteSyn } else if (expr is LambdaExpr) { var e = (LambdaExpr)expr; + IVariable receiver = null; + if (enclosingMethod is { IsTailRecursive: true } || enclosingFunction is { IsTailRecursive: true }) { + var name = ProtectedFreshId("_this"); + var ty = ModuleResolver.GetThisType(e.tok, thisContext); + receiver = new LocalVariable(RangeToken.NoToken, name, ty, false) { + type = ty + }; + var _this = new ThisExpr(thisContext); + wr = EmitBetaRedex(new List() {IdName(receiver)}, new List() {_this}, new List() {_this.Type}, expr.Type, expr.tok, inLetExprBody, wr, ref wStmts); + } + wr = CaptureFreeVariables(e, false, out var su, inLetExprBody, wr, ref wStmts); + if (receiver != null) { + su = new Substituter(new IdentifierExpr(e.tok, receiver), su.substMap, su.typeMap); + } + wr = CreateLambda(e.BoundVars.ConvertAll(bv => bv.Type), Token.NoToken, e.BoundVars.ConvertAll(IdName), e.Body.Type, wr, wStmts); wStmts = wr.Fork(); wr = EmitReturnExpr(wr); diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4684.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4684.dfy new file mode 100644 index 00000000000..4ae03f4c481 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4684.dfy @@ -0,0 +1,44 @@ +// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" + +class C { + var data: nat + var next: C? + + constructor (n: nat) { + data := n; + if n == 0 { + next := null; + } else { + next := new C(n - 1); + } + } + + function FWithoutTailRecursion(n: nat, g: () ~> int): int + requires g.requires() + reads * + { + if n == 0 || next == null then + g() + else + var h := () reads this => this.data; + var r := next.FWithoutTailRecursion(n - 1, if n < 20 then g else h); + r + } + + function F(n: nat, g: () ~> int): int + requires g.requires() + reads * + { + if n == 0 || next == null then + g() + else + var h := () reads this => this.data; + next.F(n - 1, if n < 20 then g else h) + } +} + +method Main() { + var c := new C(25); + print c.FWithoutTailRecursion(25, () => -1), "\n"; // 20 + print c.F(25, () => -1), "\n"; // 20 +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4684.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4684.dfy.expect new file mode 100644 index 00000000000..b611ed20cf6 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4684.dfy.expect @@ -0,0 +1,2 @@ +20 +20 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4684.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4684.dfy.rs.check new file mode 100644 index 00000000000..ee582662bc2 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4684.dfy.rs.check @@ -0,0 +1 @@ +CHECK: error\[E0599\]: no method named `FWithoutTailRecursion` found for enum `Option` in the current scope \ No newline at end of file From 3d34b575020f94bc64e561743ef9dc37bcf9982a Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Tue, 21 May 2024 18:49:48 +0200 Subject: [PATCH 2/6] news --- docs/dev/news/5473.fix | 1 + 1 file changed, 1 insertion(+) create mode 100644 docs/dev/news/5473.fix diff --git a/docs/dev/news/5473.fix b/docs/dev/news/5473.fix new file mode 100644 index 00000000000..00c2494f303 --- /dev/null +++ b/docs/dev/news/5473.fix @@ -0,0 +1 @@ +Reference the correct `this` after removing the tail call of a function or method \ No newline at end of file From 0f9e102cba677409b94a941548624c4a606c11f8 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Tue, 21 May 2024 23:14:31 +0200 Subject: [PATCH 3/6] Rename 5473.fix to 5474.fix --- docs/dev/news/{5473.fix => 5474.fix} | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) rename docs/dev/news/{5473.fix => 5474.fix} (78%) diff --git a/docs/dev/news/5473.fix b/docs/dev/news/5474.fix similarity index 78% rename from docs/dev/news/5473.fix rename to docs/dev/news/5474.fix index 00c2494f303..05ede052c9b 100644 --- a/docs/dev/news/5473.fix +++ b/docs/dev/news/5474.fix @@ -1 +1 @@ -Reference the correct `this` after removing the tail call of a function or method \ No newline at end of file +Reference the correct `this` after removing the tail call of a function or method From 389ad65f5997cff1aacba1d0d1a12fffedfc1770 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Tue, 21 May 2024 23:22:49 +0200 Subject: [PATCH 4/6] tweak protection level --- Source/DafnyCore/AST/Substituter.cs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/DafnyCore/AST/Substituter.cs b/Source/DafnyCore/AST/Substituter.cs index b0ad9564682..fda6e5655f2 100644 --- a/Source/DafnyCore/AST/Substituter.cs +++ b/Source/DafnyCore/AST/Substituter.cs @@ -13,8 +13,8 @@ namespace Microsoft.Dafny { /// public class Substituter { protected Expression receiverReplacement { get; } - protected Dictionary substMap { get; } - protected Dictionary typeMap { get; } + public Dictionary substMap { get; } + public Dictionary typeMap { get; } protected readonly Label oldHeapLabel; [CanBeNull] protected readonly SystemModuleManager SystemModuleManager; // if non-null, substitutions into FunctionCallExpr's will be wrapped From 32aa35b4b28bdfc60216039caeb42f700f7e0046 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Wed, 22 May 2024 12:00:54 +0200 Subject: [PATCH 5/6] format --- Source/DafnyCore/Backends/SinglePassCodeGenerator.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator.cs b/Source/DafnyCore/Backends/SinglePassCodeGenerator.cs index 6c62d82c28e..ad2b71050b4 100644 --- a/Source/DafnyCore/Backends/SinglePassCodeGenerator.cs +++ b/Source/DafnyCore/Backends/SinglePassCodeGenerator.cs @@ -5655,7 +5655,7 @@ void EmitExpr(Expression e2, ConcreteSyntaxTree wr2, bool inLetExpr, ConcreteSyn type = ty }; var _this = new ThisExpr(thisContext); - wr = EmitBetaRedex(new List() {IdName(receiver)}, new List() {_this}, new List() {_this.Type}, expr.Type, expr.tok, inLetExprBody, wr, ref wStmts); + wr = EmitBetaRedex(new List() { IdName(receiver) }, new List() { _this }, new List() { _this.Type }, expr.Type, expr.tok, inLetExprBody, wr, ref wStmts); } wr = CaptureFreeVariables(e, false, out var su, inLetExprBody, wr, ref wStmts); From c38ceab2cbaba580f79a9bf4963b80ec558a78d2 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Wed, 22 May 2024 12:47:57 +0200 Subject: [PATCH 6/6] Update git-issue-4684.dfy.rs.check --- .../LitTests/LitTest/git-issues/git-issue-4684.dfy.rs.check | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4684.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4684.dfy.rs.check index ee582662bc2..8f800076642 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4684.dfy.rs.check +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4684.dfy.rs.check @@ -1 +1 @@ -CHECK: error\[E0599\]: no method named `FWithoutTailRecursion` found for enum `Option` in the current scope \ No newline at end of file +CHECK: error