fix: Reference the correct this after removing the tail call of a f…

…unction or method (dafny-lang#5474)

Fixes dafny-lang#4684

---------

Co-authored-by: Aaron Tomb <[email protected]>

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.
   /// </summary>
   public class Substituter {
-    protected readonly Expression receiverReplacement;
-    protected readonly Dictionary<IVariable, Expression> substMap;
-    protected readonly Dictionary<TypeParameter, Type> typeMap;
+    protected Expression receiverReplacement { get; }
+    public Dictionary<IVariable, Expression> substMap { get; }
+    public Dictionary<TypeParameter, Type> typeMap { get; }
     protected readonly Label oldHeapLabel;
     [CanBeNull] protected readonly SystemModuleManager SystemModuleManager; // if non-null, substitutions into FunctionCallExpr's will be wrapped
 

Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs

@@ -1184,7 +1184,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");
     }

Source/DafnyCore/Backends/SinglePassCodeGenerator.cs

@@ -5661,7 +5661,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<string>() { IdName(receiver) }, new List<Expression>() { _this }, new List<Type>() { _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);

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
+}

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

@@ -0,0 +1,2 @@
+20
+20

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4684.dfy.rs.check

@@ -0,0 +1 @@
+CHECK: error

docs/dev/news/5474.fix

@@ -0,0 +1 @@
+Reference the correct `this` after removing the tail call of a function or method