Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix: Tail-recursion for result copy types in the Dafny-to-Rust backend. #5930

Merged
merged 2 commits into from
Nov 25, 2024
Merged

Fix: Tail-recursion for result copy types in the Dafny-to-Rust backend. #5930

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
960e684
Fixed
MikaelMayer Nov 22, 2024
c03dee9
Merge branch 'master' into fix-5923-better
MikaelMayer Nov 22, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
22 changes: 9 additions & 13 deletions Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1562,15 +1562,18 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
} else {
var tupleArgs := [];
assume {:axiom} |m.outTypes| == |outVars|;
var isTailRecursive := |m.body| == 1 && m.body[0].TailRecursive?;

for outI := 0 to |outVars| {
var outVar := outVars[outI];
var outType := GenType(m.outTypes[outI], GenTypeContext.default());
var outTyp := m.outTypes[outI];
var outType := GenType(outTyp, GenTypeContext.default());
var outName := escapeVar(outVar);
paramNames := paramNames + [outName];
var outMaybeType := if outType.CanReadWithoutClone() then outType else R.MaybePlaceboType(outType);
paramTypes := paramTypes[outName := outMaybeType];

if !isTailRecursive {// Out parameters are assigned in the inner block
paramNames := paramNames + [outName];
var outMaybeType := if outType.CanReadWithoutClone() then outType else R.MaybePlaceboType(outType);
paramTypes := paramTypes[outName := outMaybeType];
}
tupleArgs := tupleArgs + [outName];
}
earlyReturn := Some(tupleArgs);
Expand Down Expand Up @@ -1890,9 +1893,6 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
if param == "_accumulator" {
continue; // This is an already mutable variable handled by SinglePassCodeGenerator
}
if param in oldEnv.types && oldEnv.types[param].ExtractMaybePlacebo().Some? {
continue; // This is an output variable. Output variables don't need to be iterated on.
}
var paramInit, _, _ := GenIdent(param, selfIdent, oldEnv, OwnershipOwned);
var recVar := TailRecursionPrefix + Strings.OfNat(paramI);
generated := generated.Then(R.DeclareVar(R.MUT, recVar, None, Some(paramInit)));
Expand Down Expand Up @@ -2977,11 +2977,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
}
case InitializationValue(typ) => {
var typExpr := GenType(typ, GenTypeContext.default());
if typExpr.IsObjectOrPointer() {
r := typExpr.ToNullExpr();
} else {
r := R.TraitCast(typExpr, R.DefaultTrait).FSel("default").Apply0();
}
r := R.TraitCast(typExpr, R.DefaultTrait).FSel("default").Apply0();
r, resultingOwnership := FromOwned(r, expectedOwnership);
readIdents := {};
return;
Expand Down
61 changes: 30 additions & 31 deletions Source/DafnyCore/GeneratedFromDafny/DCOMP.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1845,25 +1845,31 @@ public RAST._IImplMember GenMethod(DAST._IMethod m, bool forTrait, DAST._IType e
} else {
Dafny.ISequence<Dafny.ISequence<Dafny.Rune>> _42_tupleArgs;
_42_tupleArgs = Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements();
bool _43_isTailRecursive;
_43_isTailRecursive = ((new BigInteger(((m).dtor_body).Count)) == (BigInteger.One)) && ((((m).dtor_body).Select(BigInteger.Zero)).is_TailRecursive);
BigInteger _hi4 = new BigInteger((_37_outVars).Count);
for (BigInteger _43_outI = BigInteger.Zero; _43_outI < _hi4; _43_outI++) {
Dafny.ISequence<Dafny.Rune> _44_outVar;
_44_outVar = (_37_outVars).Select(_43_outI);
RAST._IType _45_outType;
for (BigInteger _44_outI = BigInteger.Zero; _44_outI < _hi4; _44_outI++) {
Dafny.ISequence<Dafny.Rune> _45_outVar;
_45_outVar = (_37_outVars).Select(_44_outI);
DAST._IType _46_outTyp;
_46_outTyp = ((m).dtor_outTypes).Select(_44_outI);
RAST._IType _47_outType;
RAST._IType _out5;
_out5 = (this).GenType(((m).dtor_outTypes).Select(_43_outI), Defs.GenTypeContext.@default());
_45_outType = _out5;
Dafny.ISequence<Dafny.Rune> _46_outName;
_46_outName = Defs.__default.escapeVar(_44_outVar);
_1_paramNames = Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.Concat(_1_paramNames, Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(_46_outName));
RAST._IType _47_outMaybeType;
if ((_45_outType).CanReadWithoutClone()) {
_47_outMaybeType = _45_outType;
} else {
_47_outMaybeType = RAST.__default.MaybePlaceboType(_45_outType);
_out5 = (this).GenType(_46_outTyp, Defs.GenTypeContext.@default());
_47_outType = _out5;
Dafny.ISequence<Dafny.Rune> _48_outName;
_48_outName = Defs.__default.escapeVar(_45_outVar);
if (!(_43_isTailRecursive)) {
_1_paramNames = Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.Concat(_1_paramNames, Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(_48_outName));
RAST._IType _49_outMaybeType;
if ((_47_outType).CanReadWithoutClone()) {
_49_outMaybeType = _47_outType;
} else {
_49_outMaybeType = RAST.__default.MaybePlaceboType(_47_outType);
}
_2_paramTypes = Dafny.Map<Dafny.ISequence<Dafny.Rune>, RAST._IType>.Update(_2_paramTypes, _48_outName, _49_outMaybeType);
}
_2_paramTypes = Dafny.Map<Dafny.ISequence<Dafny.Rune>, RAST._IType>.Update(_2_paramTypes, _46_outName, _47_outMaybeType);
_42_tupleArgs = Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.Concat(_42_tupleArgs, Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(_46_outName));
_42_tupleArgs = Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.Concat(_42_tupleArgs, Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(_48_outName));
}
_36_earlyReturn = Std.Wrappers.Option<Dafny.ISequence<Dafny.ISequence<Dafny.Rune>>>.create_Some(_42_tupleArgs);
}
Expand All @@ -1875,17 +1881,17 @@ public RAST._IImplMember GenMethod(DAST._IMethod m, bool forTrait, DAST._IType e
}
after_match1: ;
_32_env = Defs.Environment.create(Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.Concat(_34_preAssignNames, _1_paramNames), Dafny.Map<Dafny.ISequence<Dafny.Rune>, RAST._IType>.Merge(_35_preAssignTypes, _2_paramTypes));
RAST._IExpr _48_body;
Dafny.ISet<Dafny.ISequence<Dafny.Rune>> _49___v20;
Defs._IEnvironment _50___v21;
RAST._IExpr _50_body;
Dafny.ISet<Dafny.ISequence<Dafny.Rune>> _51___v20;
Defs._IEnvironment _52___v21;
RAST._IExpr _out6;
Dafny.ISet<Dafny.ISequence<Dafny.Rune>> _out7;
Defs._IEnvironment _out8;
(this).GenStmts((m).dtor_body, _8_selfIdent, _32_env, true, _36_earlyReturn, out _out6, out _out7, out _out8);
_48_body = _out6;
_49___v20 = _out7;
_50___v21 = _out8;
_31_fBody = Std.Wrappers.Option<RAST._IExpr>.create_Some((_33_preBody).Then(_48_body));
_50_body = _out6;
_51___v20 = _out7;
_52___v21 = _out8;
_31_fBody = Std.Wrappers.Option<RAST._IExpr>.create_Some((_33_preBody).Then(_50_body));
} else {
_32_env = Defs.Environment.create(_1_paramNames, _2_paramTypes);
_31_fBody = Std.Wrappers.Option<RAST._IExpr>.create_None();
Expand Down Expand Up @@ -2518,9 +2524,6 @@ public void GenStmt(DAST._IStatement stmt, Defs._ISelfInfo selfIdent, Defs._IEnv
if ((_82_param).Equals(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("_accumulator"))) {
goto continue_4_0;
}
if ((((_76_oldEnv).dtor_types).Contains(_82_param)) && (((Dafny.Map<Dafny.ISequence<Dafny.Rune>, RAST._IType>.Select((_76_oldEnv).dtor_types,_82_param)).ExtractMaybePlacebo()).is_Some)) {
goto continue_4_0;
}
RAST._IExpr _83_paramInit;
Defs._IOwnership _84___v39;
Dafny.ISet<Dafny.ISequence<Dafny.Rune>> _85___v40;
Expand Down Expand Up @@ -4369,11 +4372,7 @@ public void GenExpr(DAST._IExpression e, Defs._ISelfInfo selfIdent, Defs._IEnvir
RAST._IType _out13;
_out13 = (this).GenType(_7_typ, Defs.GenTypeContext.@default());
_8_typExpr = _out13;
if ((_8_typExpr).IsObjectOrPointer()) {
r = (_8_typExpr).ToNullExpr();
} else {
r = ((RAST.Expr.create_TraitCast(_8_typExpr, RAST.__default.DefaultTrait)).FSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("default"))).Apply0();
}
r = ((RAST.Expr.create_TraitCast(_8_typExpr, RAST.__default.DefaultTrait)).FSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("default"))).Apply0();
RAST._IExpr _out14;
Defs._IOwnership _out15;
(this).FromOwned(r, expectedOwnership, out _out14, out _out15);
Expand Down
8 changes: 8 additions & 0 deletions Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/newtypes.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -69,6 +69,14 @@ newtype IntWrapper = int {
output := (this / 2).firstTwoBits(maxDepth - 1);
}
}
// non-Copy output values
method firstTwoBitsAreThree(maxDepth: uint32WithMethods) returns (output: bool) {
if this <= 3 || maxDepth == 0 {
output := this == 3;
} else {
output := (this / 2).firstTwoBitsAreThree(maxDepth - 1);
}
}
function add(other: IntWrapper): IntWrapper {
this + other
}
Expand Down