Porting of fix b2a5d47 from #5668

dafny-lang · Aug 14, 2024 · 58e55dc · 58e55dc
1 parent abff153
commit 58e55dc
Show file tree

Hide file tree

Showing 4 changed files with 19 additions and 2 deletions.
diff --git a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy
@@ -3622,6 +3622,9 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
           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);
             var recVar := TailRecursionPrefix + Strings.OfNat(paramI);
             generated := generated.Then(R.DeclareVar(R.MUT, recVar, None, Some(paramInit)));

diff --git a/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs b/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs
@@ -3329,6 +3329,9 @@ public void GenStmt(DAST._IStatement stmt, DCOMP._ISelfInfo selfIdent, DCOMP._IE
             for (BigInteger _1783_paramI = BigInteger.Zero; _1783_paramI < _hi36; _1783_paramI++) {
               Dafny.ISequence<Dafny.Rune> _1784_param;
               _1784_param = ((env).dtor_names).Select(_1783_paramI);
+              if ((_1784_param).Equals(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("_accumulator"))) {
+                goto continue_4_0;
+              }
               RAST._IExpr _1785_paramInit;
               DCOMP._IOwnership _1786___v90;
               Dafny.ISet<Dafny.ISequence<Dafny.Rune>> _1787___v91;
@@ -3349,7 +3352,9 @@ public void GenStmt(DAST._IStatement stmt, DCOMP._ISelfInfo selfIdent, DCOMP._IE
                 newEnv = (newEnv).AddAssigned(_1788_recVar, _1789_declaredType);
               }
               _1782_loopBegin = (_1782_loopBegin).Then(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_CONST(), _1784_param, Std.Wrappers.Option<RAST._IType>.create_None(), Std.Wrappers.Option<RAST._IExpr>.create_Some(RAST.Expr.create_Identifier(_1788_recVar))));
+            continue_4_0: ;
             }
+          after_4_0: ;
             RAST._IExpr _1790_bodyExpr;
             Dafny.ISet<Dafny.ISequence<Dafny.Rune>> _1791_bodyIdents;
             DCOMP._IEnvironment _1792_bodyEnv;
@@ -5760,7 +5765,7 @@ public void GenExpr(DAST._IExpression e, DCOMP._ISelfInfo selfIdent, DCOMP._IEnv
                       goto after__ASSIGN_SUCH_THAT_3;
                     }
                   }
-                  throw new System.Exception("assign-such-that search produced no value (line 4810)");
+                  throw new System.Exception("assign-such-that search produced no value (line 4813)");
                 after__ASSIGN_SUCH_THAT_3: ;
                   _2096_allReadCloned = Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.Concat(_2096_allReadCloned, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("let ")), _2097_next), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(" = ")), _2097_next), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(".clone();\n"));
                   _2095_recIdents = Dafny.Set<Dafny.ISequence<Dafny.Rune>>.Difference(_2095_recIdents, Dafny.Set<Dafny.ISequence<Dafny.Rune>>.FromElements(_2097_next));
@@ -7078,7 +7083,7 @@ public void GenExpr(DAST._IExpression e, DCOMP._ISelfInfo selfIdent, DCOMP._IEnv
                   goto after__ASSIGN_SUCH_THAT_4;
                 }
               }
-              throw new System.Exception("assign-such-that search produced no value (line 5312)");
+              throw new System.Exception("assign-such-that search produced no value (line 5315)");
             after__ASSIGN_SUCH_THAT_4: ;
               if ((!object.Equals(selfIdent, DCOMP.SelfInfo.create_NoSelf())) && ((_2340_next).Equals(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("_this")))) {
                 RAST._IExpr _2341_selfCloned;

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5647.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5647.dfy
@@ -15,6 +15,14 @@ function {:tailrecursion} GetSum(
     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), "\n";
 }
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5647.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5647.dfy.expect
@@ -1 +1,2 @@
 1010101010
+10