Fix: Tail-Recursion for the Dafny-to-Rust compiler

Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs

@@ -730,6 +730,10 @@ protected override ConcreteSyntaxTree EmitTailCallStructure(MemberDecl member, C
       }
     }
 
+    public override string TailRecursiveVar(int inParamIndex, IVariable variable) {
+      return preventShadowing ? base.TailRecursiveVar(inParamIndex, variable) : DCOMP.COMP.TailRecursionPrefix.ToVerbatimString(false) + inParamIndex;
+    }
+
     protected override void EmitJumpToTailCallStart(ConcreteSyntaxTree wr) {
       if (wr is BuilderSyntaxTree<StatementContainer> stmtContainer) {
         stmtContainer.Builder.AddStatement((DAST.Statement)DAST.Statement.create_JumpTailCallStart());

Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy

@@ -1828,6 +1828,8 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
 
     const ObjectType: ObjectType
 
+    static const TailRecursionPrefix := "_r"
+
     var error: Option<string>
 
     var optimizations: seq<R.Mod -> R.Mod>
@@ -3586,22 +3588,31 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
             generated := generated.Then(R.DeclareVar(R.MUT, "_this", None, Some(selfClone)));
           }
           newEnv := env;
+          var loopBegin := R.RawExpr("");
           for paramI := 0 to |env.names| {
             var param := env.names[paramI];
+            if param == "_accumulator" {
+              continue; // This is an already mutable variable handled by SinglePassCodeGenerator
+            }
             var paramInit, _, _ := GenIdent(param, selfIdent, env, OwnershipOwned);
-            generated := generated.Then(R.DeclareVar(R.MUT, param, None, Some(paramInit)));
+            var recVar := TailRecursionPrefix + Strings.OfNat(paramI);
+            generated := generated.Then(R.DeclareVar(R.MUT, recVar, None, Some(paramInit)));
             if param in env.types {
               // We made the input type owned by the variable.
               // so we can remove borrow annotations.
               var declaredType := env.types[param].ToOwned();
               newEnv := newEnv.AddAssigned(param, declaredType);
+              newEnv := newEnv.AddAssigned(recVar, declaredType);
             }
+            // Redeclare the input parameter, take ownership of the recursive value
+            loopBegin := loopBegin.Then(R.DeclareVar(R.CONST, param, None, Some(R.Identifier(recVar))));
           }
           var bodyExpr, bodyIdents, bodyEnv := GenStmts(body, if selfIdent != NoSelf then ThisTyped("_this", selfIdent.dafnyType) else NoSelf, newEnv, false, earlyReturn);
           readIdents := bodyIdents;
           generated := generated.Then(
             R.Labelled("TAIL_CALL_START",
-                       R.Loop(None, bodyExpr)));
+                       R.Loop(None,
+                              loopBegin.Then(bodyExpr))));
         }
         case JumpTailCallStart() => {
           generated := R.Continue(Some("TAIL_CALL_START"));

Source/DafnyCore/Backends/Rust/RustCodeGenerator.cs

@@ -1,4 +1,5 @@
 using System;
+using System.Configuration;
 using System.IO;
 using System.Linq;
 using Dafny;

Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs

@@ -4554,6 +4554,10 @@ void TrTailCallStmt(IToken tok, Method method, Expression receiver, List<Express
       TrTailCall(tok, method.IsStatic, method.Ins, receiver, args, wr);
     }
 
+    public virtual string TailRecursiveVar(int inParamIndex, IVariable variable) {
+      return IdName(variable);
+    }
+
     void TrTailCall(IToken tok, bool isStatic, List<Formal> inParameters, Expression receiver, List<Expression> args, ConcreteSyntaxTree wr) {
       // assign the actual in-parameters to temporary variables
       var inTmps = new List<string>();
@@ -4593,13 +4597,18 @@ void TrTailCall(IToken tok, bool isStatic, List<Formal> inParameters, Expression
         EndStmt(wr);
         n++;
       }
+
+      var inParamIndex = 0;
       foreach (var p in inParameters) {
         if (!p.IsGhost) {
-          EmitIdentifier(
-            inTmps[n],
-            EmitAssignment(IdentLvalue(IdName(p)), p.Type, inTypes[n], wr, tok)
-          );
+          // We want to assign the value to input parameters. However, if input parameters were shadowed
+          // for the compilers that support the same shadowing rules as Dafny (e.g. the Dafny-to-Rust compiler)
+          // we need to assign the result to the temporary and mutable variables instead
+          var wrAssignRhs =
+            EmitAssignment(IdentLvalue(TailRecursiveVar(inParamIndex, p)), p.Type, inTypes[n], wr, tok);
+          EmitIdentifier(inTmps[n], wrAssignRhs);
           n++;
+          inParamIndex++;
         }
       }
       Contract.Assert(n == inTmps.Count);

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

@@ -0,0 +1,28 @@
+// RUN: %testDafnyForEachCompiler "%s"
+
+// Verify shadowing
+
+function {:tailrecursion} GetSum(
+  a_b': nat,
+  ac_c: string)
+  : string
+{
+  if a_b' == 0 then
+    ac_c
+  else
+    var j := a_b';
+    var a_b' := if a_b' % 2 == 0 then "1" else "0";
+    GetSum(j - 1, ac_c + a_b')
+}
+
+function GetSumAuto(x: nat, y: nat): nat
+  decreases y - x
+{
+  if x >= y then y else
+  1 + GetSumAuto(x + 1, y)
+}
+
+method Main() {
+  print GetSum(10, ""), "\n";
+  print GetSumAuto(0, 5);
+}

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

@@ -0,0 +1,2 @@
+1010101010
+10

docs/dev/news/5647.fix

@@ -0,0 +1 @@
+Tail-Recursion for the Dafny-to-Rust compiler