diff --git a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs index 466bc8ec17..adc8ce2228 100644 --- a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs +++ b/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 stmtContainer) { stmtContainer.Builder.AddStatement((DAST.Statement)DAST.Statement.create_JumpTailCallStart()); diff --git a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy index 83a75a75e9..55fb008c70 100644 --- a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy +++ b/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 var optimizations: seq 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")); diff --git a/Source/DafnyCore/Backends/Rust/RustCodeGenerator.cs b/Source/DafnyCore/Backends/Rust/RustCodeGenerator.cs index fb83b0a185..243eb5ba08 100644 --- a/Source/DafnyCore/Backends/Rust/RustCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Rust/RustCodeGenerator.cs @@ -1,4 +1,5 @@ using System; +using System.Configuration; using System.IO; using System.Linq; using Dafny; diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs index c4069d85ac..7647eb0c11 100644 --- a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs +++ b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs @@ -4554,6 +4554,10 @@ void TrTailCallStmt(IToken tok, Method method, Expression receiver, List inParameters, Expression receiver, List args, ConcreteSyntaxTree wr) { // assign the actual in-parameters to temporary variables var inTmps = new List(); @@ -4593,13 +4597,18 @@ void TrTailCall(IToken tok, bool isStatic, List 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); diff --git a/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs b/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs index 8ff0b87159..afc7e6a72e 100644 --- a/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs +++ b/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs @@ -3284,39 +3284,50 @@ public void GenStmt(DAST._IStatement stmt, DCOMP._ISelfInfo selfIdent, DCOMP._IE generated = (generated).Then(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), Dafny.Sequence.UnicodeFromString("_this"), Std.Wrappers.Option.create_None(), Std.Wrappers.Option.create_Some(_75_selfClone))); } newEnv = env; + RAST._IExpr _78_loopBegin; + _78_loopBegin = RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("")); BigInteger _hi1 = new BigInteger(((env).dtor_names).Count); - for (BigInteger _78_paramI = BigInteger.Zero; _78_paramI < _hi1; _78_paramI++) { - Dafny.ISequence _79_param; - _79_param = ((env).dtor_names).Select(_78_paramI); - RAST._IExpr _80_paramInit; - DCOMP._IOwnership _81___v90; - Dafny.ISet> _82___v91; + for (BigInteger _79_paramI = BigInteger.Zero; _79_paramI < _hi1; _79_paramI++) { + Dafny.ISequence _80_param; + _80_param = ((env).dtor_names).Select(_79_paramI); + if ((_80_param).Equals(Dafny.Sequence.UnicodeFromString("_accumulator"))) { + goto continue_4_0; + } + RAST._IExpr _81_paramInit; + DCOMP._IOwnership _82___v90; + Dafny.ISet> _83___v91; RAST._IExpr _out46; DCOMP._IOwnership _out47; Dafny.ISet> _out48; - (this).GenIdent(_79_param, selfIdent, env, DCOMP.Ownership.create_OwnershipOwned(), out _out46, out _out47, out _out48); - _80_paramInit = _out46; - _81___v90 = _out47; - _82___v91 = _out48; - generated = (generated).Then(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), _79_param, Std.Wrappers.Option.create_None(), Std.Wrappers.Option.create_Some(_80_paramInit))); - if (((env).dtor_types).Contains(_79_param)) { - RAST._IType _83_declaredType; - _83_declaredType = (Dafny.Map, RAST._IType>.Select((env).dtor_types,_79_param)).ToOwned(); - newEnv = (newEnv).AddAssigned(_79_param, _83_declaredType); + (this).GenIdent(_80_param, selfIdent, env, DCOMP.Ownership.create_OwnershipOwned(), out _out46, out _out47, out _out48); + _81_paramInit = _out46; + _82___v90 = _out47; + _83___v91 = _out48; + Dafny.ISequence _84_recVar; + _84_recVar = Dafny.Sequence.Concat(DCOMP.COMP.TailRecursionPrefix, Std.Strings.__default.OfNat(_79_paramI)); + generated = (generated).Then(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), _84_recVar, Std.Wrappers.Option.create_None(), Std.Wrappers.Option.create_Some(_81_paramInit))); + if (((env).dtor_types).Contains(_80_param)) { + RAST._IType _85_declaredType; + _85_declaredType = (Dafny.Map, RAST._IType>.Select((env).dtor_types,_80_param)).ToOwned(); + newEnv = (newEnv).AddAssigned(_80_param, _85_declaredType); + newEnv = (newEnv).AddAssigned(_84_recVar, _85_declaredType); } + _78_loopBegin = (_78_loopBegin).Then(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_CONST(), _80_param, Std.Wrappers.Option.create_None(), Std.Wrappers.Option.create_Some(RAST.Expr.create_Identifier(_84_recVar)))); + continue_4_0: ; } - RAST._IExpr _84_bodyExpr; - Dafny.ISet> _85_bodyIdents; - DCOMP._IEnvironment _86_bodyEnv; + after_4_0: ; + RAST._IExpr _86_bodyExpr; + Dafny.ISet> _87_bodyIdents; + DCOMP._IEnvironment _88_bodyEnv; RAST._IExpr _out49; Dafny.ISet> _out50; DCOMP._IEnvironment _out51; (this).GenStmts(_74_body, ((!object.Equals(selfIdent, DCOMP.SelfInfo.create_NoSelf())) ? (DCOMP.SelfInfo.create_ThisTyped(Dafny.Sequence.UnicodeFromString("_this"), (selfIdent).dtor_dafnyType)) : (DCOMP.SelfInfo.create_NoSelf())), newEnv, false, earlyReturn, out _out49, out _out50, out _out51); - _84_bodyExpr = _out49; - _85_bodyIdents = _out50; - _86_bodyEnv = _out51; - readIdents = _85_bodyIdents; - generated = (generated).Then(RAST.Expr.create_Labelled(Dafny.Sequence.UnicodeFromString("TAIL_CALL_START"), RAST.Expr.create_Loop(Std.Wrappers.Option.create_None(), _84_bodyExpr))); + _86_bodyExpr = _out49; + _87_bodyIdents = _out50; + _88_bodyEnv = _out51; + readIdents = _87_bodyIdents; + generated = (generated).Then(RAST.Expr.create_Labelled(Dafny.Sequence.UnicodeFromString("TAIL_CALL_START"), RAST.Expr.create_Loop(Std.Wrappers.Option.create_None(), (_78_loopBegin).Then(_86_bodyExpr)))); } goto after_match0; } @@ -3333,83 +3344,83 @@ public void GenStmt(DAST._IStatement stmt, DCOMP._ISelfInfo selfIdent, DCOMP._IE } { if (_source0.is_Call) { - DAST._IExpression _87_on = _source0.dtor_on; - DAST._ICallName _88_name = _source0.dtor_callName; - Dafny.ISequence _89_typeArgs = _source0.dtor_typeArgs; - Dafny.ISequence _90_args = _source0.dtor_args; - Std.Wrappers._IOption>> _91_maybeOutVars = _source0.dtor_outs; + DAST._IExpression _89_on = _source0.dtor_on; + DAST._ICallName _90_name = _source0.dtor_callName; + Dafny.ISequence _91_typeArgs = _source0.dtor_typeArgs; + Dafny.ISequence _92_args = _source0.dtor_args; + Std.Wrappers._IOption>> _93_maybeOutVars = _source0.dtor_outs; { - Dafny.ISequence _92_argExprs; - Dafny.ISet> _93_recIdents; - Dafny.ISequence _94_typeExprs; - Std.Wrappers._IOption _95_fullNameQualifier; + Dafny.ISequence _94_argExprs; + Dafny.ISet> _95_recIdents; + Dafny.ISequence _96_typeExprs; + Std.Wrappers._IOption _97_fullNameQualifier; Dafny.ISequence _out52; Dafny.ISet> _out53; Dafny.ISequence _out54; Std.Wrappers._IOption _out55; - (this).GenArgs(selfIdent, _88_name, _89_typeArgs, _90_args, env, out _out52, out _out53, out _out54, out _out55); - _92_argExprs = _out52; - _93_recIdents = _out53; - _94_typeExprs = _out54; - _95_fullNameQualifier = _out55; - readIdents = _93_recIdents; - Std.Wrappers._IOption _source2 = _95_fullNameQualifier; + (this).GenArgs(selfIdent, _90_name, _91_typeArgs, _92_args, env, out _out52, out _out53, out _out54, out _out55); + _94_argExprs = _out52; + _95_recIdents = _out53; + _96_typeExprs = _out54; + _97_fullNameQualifier = _out55; + readIdents = _95_recIdents; + Std.Wrappers._IOption _source2 = _97_fullNameQualifier; { if (_source2.is_Some) { DAST._IResolvedType value0 = _source2.dtor_value; - Dafny.ISequence> _96_path = value0.dtor_path; - Dafny.ISequence _97_onTypeArgs = value0.dtor_typeArgs; - DAST._IResolvedTypeBase _98_base = value0.dtor_kind; - RAST._IExpr _99_fullPath; + Dafny.ISequence> _98_path = value0.dtor_path; + Dafny.ISequence _99_onTypeArgs = value0.dtor_typeArgs; + DAST._IResolvedTypeBase _100_base = value0.dtor_kind; + RAST._IExpr _101_fullPath; RAST._IExpr _out56; - _out56 = DCOMP.COMP.GenPathExpr(_96_path, true); - _99_fullPath = _out56; - Dafny.ISequence _100_onTypeExprs; + _out56 = DCOMP.COMP.GenPathExpr(_98_path, true); + _101_fullPath = _out56; + Dafny.ISequence _102_onTypeExprs; Dafny.ISequence _out57; - _out57 = (this).GenTypeArgs(_97_onTypeArgs, DCOMP.GenTypeContext.@default()); - _100_onTypeExprs = _out57; - RAST._IExpr _101_onExpr = RAST.Expr.Default(); - DCOMP._IOwnership _102_recOwnership = DCOMP.Ownership.Default(); - Dafny.ISet> _103_recIdents = Dafny.Set>.Empty; - if (((_98_base).is_Trait) || ((_98_base).is_Class)) { + _out57 = (this).GenTypeArgs(_99_onTypeArgs, DCOMP.GenTypeContext.@default()); + _102_onTypeExprs = _out57; + RAST._IExpr _103_onExpr = RAST.Expr.Default(); + DCOMP._IOwnership _104_recOwnership = DCOMP.Ownership.Default(); + Dafny.ISet> _105_recIdents = Dafny.Set>.Empty; + if (((_100_base).is_Trait) || ((_100_base).is_Class)) { RAST._IExpr _out58; DCOMP._IOwnership _out59; Dafny.ISet> _out60; - (this).GenExpr(_87_on, selfIdent, env, DCOMP.Ownership.create_OwnershipOwned(), out _out58, out _out59, out _out60); - _101_onExpr = _out58; - _102_recOwnership = _out59; - _103_recIdents = _out60; - _101_onExpr = ((this).modify__macro).Apply1(_101_onExpr); - readIdents = Dafny.Set>.Union(readIdents, _103_recIdents); + (this).GenExpr(_89_on, selfIdent, env, DCOMP.Ownership.create_OwnershipOwned(), out _out58, out _out59, out _out60); + _103_onExpr = _out58; + _104_recOwnership = _out59; + _105_recIdents = _out60; + _103_onExpr = ((this).modify__macro).Apply1(_103_onExpr); + readIdents = Dafny.Set>.Union(readIdents, _105_recIdents); } else { RAST._IExpr _out61; DCOMP._IOwnership _out62; Dafny.ISet> _out63; - (this).GenExpr(_87_on, selfIdent, env, DCOMP.Ownership.create_OwnershipBorrowedMut(), out _out61, out _out62, out _out63); - _101_onExpr = _out61; - _102_recOwnership = _out62; - _103_recIdents = _out63; - readIdents = Dafny.Set>.Union(readIdents, _103_recIdents); + (this).GenExpr(_89_on, selfIdent, env, DCOMP.Ownership.create_OwnershipBorrowedMut(), out _out61, out _out62, out _out63); + _103_onExpr = _out61; + _104_recOwnership = _out62; + _105_recIdents = _out63; + readIdents = Dafny.Set>.Union(readIdents, _105_recIdents); } - generated = ((((_99_fullPath).ApplyType(_100_onTypeExprs)).FSel(DCOMP.__default.escapeName((_88_name).dtor_name))).ApplyType(_94_typeExprs)).Apply(Dafny.Sequence.Concat(Dafny.Sequence.FromElements(_101_onExpr), _92_argExprs)); + generated = ((((_101_fullPath).ApplyType(_102_onTypeExprs)).FSel(DCOMP.__default.escapeName((_90_name).dtor_name))).ApplyType(_96_typeExprs)).Apply(Dafny.Sequence.Concat(Dafny.Sequence.FromElements(_103_onExpr), _94_argExprs)); goto after_match2; } } { - RAST._IExpr _104_onExpr; - DCOMP._IOwnership _105___v96; - Dafny.ISet> _106_enclosingIdents; + RAST._IExpr _106_onExpr; + DCOMP._IOwnership _107___v96; + Dafny.ISet> _108_enclosingIdents; RAST._IExpr _out64; DCOMP._IOwnership _out65; Dafny.ISet> _out66; - (this).GenExpr(_87_on, selfIdent, env, DCOMP.Ownership.create_OwnershipAutoBorrowed(), out _out64, out _out65, out _out66); - _104_onExpr = _out64; - _105___v96 = _out65; - _106_enclosingIdents = _out66; - readIdents = Dafny.Set>.Union(readIdents, _106_enclosingIdents); - Dafny.ISequence _107_renderedName; - _107_renderedName = (this).GetMethodName(_87_on, _88_name); - DAST._IExpression _source3 = _87_on; + (this).GenExpr(_89_on, selfIdent, env, DCOMP.Ownership.create_OwnershipAutoBorrowed(), out _out64, out _out65, out _out66); + _106_onExpr = _out64; + _107___v96 = _out65; + _108_enclosingIdents = _out66; + readIdents = Dafny.Set>.Union(readIdents, _108_enclosingIdents); + Dafny.ISequence _109_renderedName; + _109_renderedName = (this).GetMethodName(_89_on, _90_name); + DAST._IExpression _source3 = _89_on; { bool disjunctiveMatch0 = false; if (_source3.is_Companion) { @@ -3420,26 +3431,26 @@ public void GenStmt(DAST._IStatement stmt, DCOMP._ISelfInfo selfIdent, DCOMP._IE } if (disjunctiveMatch0) { { - _104_onExpr = (_104_onExpr).FSel(_107_renderedName); + _106_onExpr = (_106_onExpr).FSel(_109_renderedName); } goto after_match3; } } { { - if (!object.Equals(_104_onExpr, RAST.__default.self)) { - DAST._ICallName _source4 = _88_name; + if (!object.Equals(_106_onExpr, RAST.__default.self)) { + DAST._ICallName _source4 = _90_name; { if (_source4.is_CallName) { Std.Wrappers._IOption onType0 = _source4.dtor_onType; if (onType0.is_Some) { - DAST._IType _108_tpe = onType0.dtor_value; - RAST._IType _109_typ; + DAST._IType _110_tpe = onType0.dtor_value; + RAST._IType _111_typ; RAST._IType _out67; - _out67 = (this).GenType(_108_tpe, DCOMP.GenTypeContext.@default()); - _109_typ = _out67; - if (((_109_typ).IsObjectOrPointer()) && (!object.Equals(_104_onExpr, RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("self"))))) { - _104_onExpr = ((this).modify__macro).Apply1(_104_onExpr); + _out67 = (this).GenType(_110_tpe, DCOMP.GenTypeContext.@default()); + _111_typ = _out67; + if (((_111_typ).IsObjectOrPointer()) && (!object.Equals(_106_onExpr, RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("self"))))) { + _106_onExpr = ((this).modify__macro).Apply1(_106_onExpr); } goto after_match4; } @@ -3449,39 +3460,39 @@ public void GenStmt(DAST._IStatement stmt, DCOMP._ISelfInfo selfIdent, DCOMP._IE } after_match4: ; } - _104_onExpr = (_104_onExpr).Sel(_107_renderedName); + _106_onExpr = (_106_onExpr).Sel(_109_renderedName); } } after_match3: ; - generated = ((_104_onExpr).ApplyType(_94_typeExprs)).Apply(_92_argExprs); + generated = ((_106_onExpr).ApplyType(_96_typeExprs)).Apply(_94_argExprs); } after_match2: ; - if (((_91_maybeOutVars).is_Some) && ((new BigInteger(((_91_maybeOutVars).dtor_value).Count)) == (BigInteger.One))) { - Dafny.ISequence _110_outVar; - _110_outVar = DCOMP.__default.escapeVar(((_91_maybeOutVars).dtor_value).Select(BigInteger.Zero)); - if (!((env).CanReadWithoutClone(_110_outVar))) { + if (((_93_maybeOutVars).is_Some) && ((new BigInteger(((_93_maybeOutVars).dtor_value).Count)) == (BigInteger.One))) { + Dafny.ISequence _112_outVar; + _112_outVar = DCOMP.__default.escapeVar(((_93_maybeOutVars).dtor_value).Select(BigInteger.Zero)); + if (!((env).CanReadWithoutClone(_112_outVar))) { generated = RAST.__default.MaybePlacebo(generated); } - generated = RAST.__default.AssignVar(_110_outVar, generated); - } else if (((_91_maybeOutVars).is_None) || ((new BigInteger(((_91_maybeOutVars).dtor_value).Count)).Sign == 0)) { + generated = RAST.__default.AssignVar(_112_outVar, generated); + } else if (((_93_maybeOutVars).is_None) || ((new BigInteger(((_93_maybeOutVars).dtor_value).Count)).Sign == 0)) { } else { - Dafny.ISequence _111_tmpVar; - _111_tmpVar = Dafny.Sequence.UnicodeFromString("_x"); - RAST._IExpr _112_tmpId; - _112_tmpId = RAST.Expr.create_Identifier(_111_tmpVar); - generated = RAST.Expr.create_DeclareVar(RAST.DeclareType.create_CONST(), _111_tmpVar, Std.Wrappers.Option.create_None(), Std.Wrappers.Option.create_Some(generated)); - Dafny.ISequence> _113_outVars; - _113_outVars = (_91_maybeOutVars).dtor_value; - BigInteger _hi2 = new BigInteger((_113_outVars).Count); - for (BigInteger _114_outI = BigInteger.Zero; _114_outI < _hi2; _114_outI++) { - Dafny.ISequence _115_outVar; - _115_outVar = DCOMP.__default.escapeVar((_113_outVars).Select(_114_outI)); - RAST._IExpr _116_rhs; - _116_rhs = (_112_tmpId).Sel(Std.Strings.__default.OfNat(_114_outI)); - if (!((env).CanReadWithoutClone(_115_outVar))) { - _116_rhs = RAST.__default.MaybePlacebo(_116_rhs); + Dafny.ISequence _113_tmpVar; + _113_tmpVar = Dafny.Sequence.UnicodeFromString("_x"); + RAST._IExpr _114_tmpId; + _114_tmpId = RAST.Expr.create_Identifier(_113_tmpVar); + generated = RAST.Expr.create_DeclareVar(RAST.DeclareType.create_CONST(), _113_tmpVar, Std.Wrappers.Option.create_None(), Std.Wrappers.Option.create_Some(generated)); + Dafny.ISequence> _115_outVars; + _115_outVars = (_93_maybeOutVars).dtor_value; + BigInteger _hi2 = new BigInteger((_115_outVars).Count); + for (BigInteger _116_outI = BigInteger.Zero; _116_outI < _hi2; _116_outI++) { + Dafny.ISequence _117_outVar; + _117_outVar = DCOMP.__default.escapeVar((_115_outVars).Select(_116_outI)); + RAST._IExpr _118_rhs; + _118_rhs = (_114_tmpId).Sel(Std.Strings.__default.OfNat(_116_outI)); + if (!((env).CanReadWithoutClone(_117_outVar))) { + _118_rhs = RAST.__default.MaybePlacebo(_118_rhs); } - generated = (generated).Then(RAST.__default.AssignVar(_115_outVar, _116_rhs)); + generated = (generated).Then(RAST.__default.AssignVar(_117_outVar, _118_rhs)); } } newEnv = env; @@ -3491,23 +3502,23 @@ public void GenStmt(DAST._IStatement stmt, DCOMP._ISelfInfo selfIdent, DCOMP._IE } { if (_source0.is_Return) { - DAST._IExpression _117_exprDafny = _source0.dtor_expr; + DAST._IExpression _119_exprDafny = _source0.dtor_expr; { - RAST._IExpr _118_expr; - DCOMP._IOwnership _119___v106; - Dafny.ISet> _120_recIdents; + RAST._IExpr _120_expr; + DCOMP._IOwnership _121___v106; + Dafny.ISet> _122_recIdents; RAST._IExpr _out68; DCOMP._IOwnership _out69; Dafny.ISet> _out70; - (this).GenExpr(_117_exprDafny, selfIdent, env, DCOMP.Ownership.create_OwnershipOwned(), out _out68, out _out69, out _out70); - _118_expr = _out68; - _119___v106 = _out69; - _120_recIdents = _out70; - readIdents = _120_recIdents; + (this).GenExpr(_119_exprDafny, selfIdent, env, DCOMP.Ownership.create_OwnershipOwned(), out _out68, out _out69, out _out70); + _120_expr = _out68; + _121___v106 = _out69; + _122_recIdents = _out70; + readIdents = _122_recIdents; if (isLast) { - generated = _118_expr; + generated = _120_expr; } else { - generated = RAST.Expr.create_Return(Std.Wrappers.Option.create_Some(_118_expr)); + generated = RAST.Expr.create_Return(Std.Wrappers.Option.create_Some(_120_expr)); } newEnv = env; } @@ -3525,27 +3536,27 @@ public void GenStmt(DAST._IStatement stmt, DCOMP._ISelfInfo selfIdent, DCOMP._IE } } { - Dafny.ISequence> _121_rustIdents = _source5.dtor_value; - Dafny.ISequence _122_tupleArgs; - _122_tupleArgs = Dafny.Sequence.FromElements(); - BigInteger _hi3 = new BigInteger((_121_rustIdents).Count); - for (BigInteger _123_i = BigInteger.Zero; _123_i < _hi3; _123_i++) { - RAST._IExpr _124_rIdent; - DCOMP._IOwnership _125___v107; - Dafny.ISet> _126___v108; + Dafny.ISequence> _123_rustIdents = _source5.dtor_value; + Dafny.ISequence _124_tupleArgs; + _124_tupleArgs = Dafny.Sequence.FromElements(); + BigInteger _hi3 = new BigInteger((_123_rustIdents).Count); + for (BigInteger _125_i = BigInteger.Zero; _125_i < _hi3; _125_i++) { + RAST._IExpr _126_rIdent; + DCOMP._IOwnership _127___v107; + Dafny.ISet> _128___v108; RAST._IExpr _out71; DCOMP._IOwnership _out72; Dafny.ISet> _out73; - (this).GenIdent((_121_rustIdents).Select(_123_i), selfIdent, env, DCOMP.Ownership.create_OwnershipOwned(), out _out71, out _out72, out _out73); - _124_rIdent = _out71; - _125___v107 = _out72; - _126___v108 = _out73; - _122_tupleArgs = Dafny.Sequence.Concat(_122_tupleArgs, Dafny.Sequence.FromElements(_124_rIdent)); + (this).GenIdent((_123_rustIdents).Select(_125_i), selfIdent, env, DCOMP.Ownership.create_OwnershipOwned(), out _out71, out _out72, out _out73); + _126_rIdent = _out71; + _127___v107 = _out72; + _128___v108 = _out73; + _124_tupleArgs = Dafny.Sequence.Concat(_124_tupleArgs, Dafny.Sequence.FromElements(_126_rIdent)); } - if ((new BigInteger((_122_tupleArgs).Count)) == (BigInteger.One)) { - generated = RAST.Expr.create_Return(Std.Wrappers.Option.create_Some((_122_tupleArgs).Select(BigInteger.Zero))); + if ((new BigInteger((_124_tupleArgs).Count)) == (BigInteger.One)) { + generated = RAST.Expr.create_Return(Std.Wrappers.Option.create_Some((_124_tupleArgs).Select(BigInteger.Zero))); } else { - generated = RAST.Expr.create_Return(Std.Wrappers.Option.create_Some(RAST.Expr.create_Tuple(_122_tupleArgs))); + generated = RAST.Expr.create_Return(Std.Wrappers.Option.create_Some(RAST.Expr.create_Tuple(_124_tupleArgs))); } } after_match5: ; @@ -3566,20 +3577,20 @@ public void GenStmt(DAST._IStatement stmt, DCOMP._ISelfInfo selfIdent, DCOMP._IE } } { - DAST._IExpression _127_e = _source0.dtor_Print_a0; + DAST._IExpression _129_e = _source0.dtor_Print_a0; { - RAST._IExpr _128_printedExpr; - DCOMP._IOwnership _129_recOwnership; - Dafny.ISet> _130_recIdents; + RAST._IExpr _130_printedExpr; + DCOMP._IOwnership _131_recOwnership; + Dafny.ISet> _132_recIdents; RAST._IExpr _out74; DCOMP._IOwnership _out75; Dafny.ISet> _out76; - (this).GenExpr(_127_e, selfIdent, env, DCOMP.Ownership.create_OwnershipBorrowed(), out _out74, out _out75, out _out76); - _128_printedExpr = _out74; - _129_recOwnership = _out75; - _130_recIdents = _out76; - generated = (RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("print!"))).Apply(Dafny.Sequence.FromElements(RAST.Expr.create_LiteralString(Dafny.Sequence.UnicodeFromString("{}"), false, false), (((RAST.__default.dafny__runtime).MSel(Dafny.Sequence.UnicodeFromString("DafnyPrintWrapper"))).AsExpr()).Apply1(_128_printedExpr))); - readIdents = _130_recIdents; + (this).GenExpr(_129_e, selfIdent, env, DCOMP.Ownership.create_OwnershipBorrowed(), out _out74, out _out75, out _out76); + _130_printedExpr = _out74; + _131_recOwnership = _out75; + _132_recIdents = _out76; + generated = (RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("print!"))).Apply(Dafny.Sequence.FromElements(RAST.Expr.create_LiteralString(Dafny.Sequence.UnicodeFromString("{}"), false, false), (((RAST.__default.dafny__runtime).MSel(Dafny.Sequence.UnicodeFromString("DafnyPrintWrapper"))).AsExpr()).Apply1(_130_printedExpr))); + readIdents = _132_recIdents; newEnv = env; } } @@ -7792,6 +7803,9 @@ public Dafny.ISequence downcast { get { public static Dafny.IMap> OpTable { get { return Dafny.Map>.FromElements(new Dafny.Pair>(DAST.BinOp.create_Mod(), Dafny.Sequence.UnicodeFromString("%")), new Dafny.Pair>(DAST.BinOp.create_And(), Dafny.Sequence.UnicodeFromString("&&")), new Dafny.Pair>(DAST.BinOp.create_Or(), Dafny.Sequence.UnicodeFromString("||")), new Dafny.Pair>(DAST.BinOp.create_Div(), Dafny.Sequence.UnicodeFromString("/")), new Dafny.Pair>(DAST.BinOp.create_Lt(), Dafny.Sequence.UnicodeFromString("<")), new Dafny.Pair>(DAST.BinOp.create_LtChar(), Dafny.Sequence.UnicodeFromString("<")), new Dafny.Pair>(DAST.BinOp.create_Plus(), Dafny.Sequence.UnicodeFromString("+")), new Dafny.Pair>(DAST.BinOp.create_Minus(), Dafny.Sequence.UnicodeFromString("-")), new Dafny.Pair>(DAST.BinOp.create_Times(), Dafny.Sequence.UnicodeFromString("*")), new Dafny.Pair>(DAST.BinOp.create_BitwiseAnd(), Dafny.Sequence.UnicodeFromString("&")), new Dafny.Pair>(DAST.BinOp.create_BitwiseOr(), Dafny.Sequence.UnicodeFromString("|")), new Dafny.Pair>(DAST.BinOp.create_BitwiseXor(), Dafny.Sequence.UnicodeFromString("^")), new Dafny.Pair>(DAST.BinOp.create_BitwiseShiftRight(), Dafny.Sequence.UnicodeFromString(">>")), new Dafny.Pair>(DAST.BinOp.create_BitwiseShiftLeft(), Dafny.Sequence.UnicodeFromString("<<"))); } } + public static Dafny.ISequence TailRecursionPrefix { get { + return Dafny.Sequence.UnicodeFromString("_r"); + } } public static Dafny.ISequence DAFNY__EXTERN__MODULE { get { return Dafny.Sequence.UnicodeFromString("_dafny_externs"); } } 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 new file mode 100644 index 0000000000..cb86f223c2 --- /dev/null +++ b/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); +} 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 new file mode 100644 index 0000000000..739a8f781f --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5647.dfy.expect @@ -0,0 +1,2 @@ +1010101010 +10 \ No newline at end of file diff --git a/docs/dev/news/5647.fix b/docs/dev/news/5647.fix new file mode 100644 index 0000000000..72275f0e32 --- /dev/null +++ b/docs/dev/news/5647.fix @@ -0,0 +1 @@ +Tail-Recursion for the Dafny-to-Rust compiler \ No newline at end of file