diff --git a/Source/DafnyCore.Test/GeneratedFromDafny/DefsCoverage.cs b/Source/DafnyCore.Test/GeneratedFromDafny/DefsCoverage.cs index b46418fee58..9ea4308a4f6 100644 --- a/Source/DafnyCore.Test/GeneratedFromDafny/DefsCoverage.cs +++ b/Source/DafnyCore.Test/GeneratedFromDafny/DefsCoverage.cs @@ -73,6 +73,8 @@ public static void Tests() DefsCoverage.__default.Expect(object.Equals(Defs.__default.DetectAssignmentStatus(Dafny.Sequence.Concat(Dafny.Sequence.FromElements(DAST.Statement.create_Print(_2_z)), _3_assigns__x), _0_x), Defs.AssignmentStatus.create_SurelyAssigned())); DefsCoverage.__default.Expect(object.Equals(Defs.__default.DetectAssignmentStatus(Dafny.Sequence.Concat(Dafny.Sequence.FromElements(DAST.Statement.create_Print(_2_z)), _3_assigns__x), _0_x), Defs.AssignmentStatus.create_SurelyAssigned())); DefsCoverage.__default.Expect(object.Equals(Defs.__default.DetectAssignmentStatus(Dafny.Sequence.Concat(Dafny.Sequence.FromElements(DAST.Statement.create_While(_2_z, Dafny.Sequence.FromElements())), _3_assigns__x), _0_x), Defs.AssignmentStatus.create_Unknown())); + DefsCoverage.__default.Expect(object.Equals(Defs.__default.DetectAssignmentStatus(Dafny.Sequence.FromElements(DAST.Statement.create_If(_5_cond, _3_assigns__x, Dafny.Sequence.FromElements(DAST.Statement.create_If(_5_cond, _3_assigns__x, _4_assigns__y)))), _0_x), Defs.AssignmentStatus.create_Unknown())); + DefsCoverage.__default.Expect(object.Equals(Defs.__default.DetectAssignmentStatus(Dafny.Sequence.FromElements(DAST.Statement.create_If(_5_cond, Dafny.Sequence.Concat(Dafny.Sequence.FromElements(DAST.Statement.create_If(_5_cond, Dafny.Sequence.FromElements(DAST.Statement.create_Return(_2_z)), Dafny.Sequence.FromElements())), _3_assigns__x), Dafny.Sequence.FromElements(DAST.Statement.create_If(_5_cond, Dafny.Sequence.Concat(Dafny.Sequence.FromElements(DAST.Statement.create_If(_5_cond, Dafny.Sequence.FromElements(DAST.Statement.create_Return(_2_z)), Dafny.Sequence.FromElements())), _3_assigns__x), _4_assigns__y)))), _0_x), Defs.AssignmentStatus.create_Unknown())); } public static Dafny.ISequence IND { get { return RAST.__default.IND; diff --git a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-definitions-coverage.dfy b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-definitions-coverage.dfy index 9f7fd18d1d9..ad1627b2325 100644 --- a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-definitions-coverage.dfy +++ b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-definitions-coverage.dfy @@ -70,5 +70,15 @@ module {:extern "DefsCoverage"} DafnyToRustCompilerDefinitionsCoverage { Expect(DetectAssignmentStatus([Print(z)] + assigns_x, x) == SurelyAssigned); Expect(DetectAssignmentStatus([Print(z)] + assigns_x, x) == SurelyAssigned); Expect(DetectAssignmentStatus([While(z, [])] + assigns_x, x) == Unknown); + Expect(DetectAssignmentStatus([If(cond, assigns_x, [If(cond, assigns_x, assigns_y)])], x) == Unknown); + Expect( + DetectAssignmentStatus( + [ If(cond, + [If(cond, [Return(z)], [])] + + assigns_x, + [If(cond, + [If(cond, [Return(z)], [])] + + assigns_x, + assigns_y)])], x) == Unknown); } } \ No newline at end of file diff --git a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-definitions.dfy b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-definitions.dfy index 8ffdc9a03dc..b663516e10c 100644 --- a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-definitions.dfy +++ b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-definitions.dfy @@ -778,37 +778,66 @@ module {:extern "Defs"} DafnyToRustCompilerDefinitions { if SurelyAssigned? then SurelyAssigned else if NotAssigned? then other else Unknown // It's not as simple. If there are are two paths leading to one being assigned, the other not, - // Rust won't be albe to figure out the rules + // Rust won't be able to figure out the rules } } - // What could be problematic is the presence of branches in the assignment - // and one branch where a value is not assigned at all. - // If return false, we don't know if it's assigned or not + /** Detects if a given variable can be detected to be surely assigned or surely unassigned by the Rust compiler */ function DetectAssignmentStatus(stmts_remainder: seq, dafny_name: VarName): AssignmentStatus { if |stmts_remainder| == 0 then NotAssigned else var stmt := stmts_remainder[0]; - match stmt { + var tailAssigned := DetectAssignmentStatus(stmts_remainder[1..], dafny_name); + var stop := stmt.Return? || stmt.EarlyReturn? || stmt.JumpTailCallStart? || (stmt.DeclareVar? && stmt.name == dafny_name); + var thisAssign := match stmt { case Assign(Ident(assign_name), _) => - if assign_name == dafny_name then SurelyAssigned else - DetectAssignmentStatus(stmts_remainder[1..], dafny_name) + if assign_name == dafny_name then SurelyAssigned else NotAssigned case If(cond, thn, els) => - DetectAssignmentStatus(thn, dafny_name).Join(DetectAssignmentStatus(els, dafny_name)) + DetectAssignmentStatus(thn, dafny_name) + .Join(DetectAssignmentStatus(els, dafny_name)) case Call(on, callName, typeArgs, args, outs) => - if outs.Some? && dafny_name in outs.value then - SurelyAssigned - else - DetectAssignmentStatus(stmts_remainder[1..], dafny_name) + if outs.Some? && dafny_name in outs.value then SurelyAssigned else NotAssigned case Labeled(_, stmts) => - DetectAssignmentStatus(stmts, dafny_name).Then(DetectAssignmentStatus(stmts_remainder[1..], dafny_name)) + DetectAssignmentStatus(stmts, dafny_name) case DeclareVar(name, _, _) => - if name == dafny_name then - NotAssigned // Shadowed - else - DetectAssignmentStatus(stmts_remainder[1..], dafny_name) + NotAssigned // If it's the same name, it's shadowed case Return(_) | EarlyReturn() | JumpTailCallStart() => NotAssigned - case Print(_) => DetectAssignmentStatus(stmts_remainder[1..], dafny_name) + case Print(_) => NotAssigned case _ => Unknown + }; + if stop then thisAssign else thisAssign.Then(tailAssigned) + } by method { + for i := 0 to |stmts_remainder| + invariant DetectAssignmentStatus(stmts_remainder, dafny_name) == DetectAssignmentStatus(stmts_remainder[i..], dafny_name) + { + assert stmts_remainder[i..][0] == stmts_remainder[i]; + var stmt := stmts_remainder[i]; + match stmt { + case Assign(Ident(assign_name), _) => + if assign_name == dafny_name { + return SurelyAssigned; + } + case If(cond, thn, els) => + var rec := DetectAssignmentStatus(thn, dafny_name); + if rec == Unknown { return Unknown; } + var rec2 := DetectAssignmentStatus(els, dafny_name); + if rec2 == Unknown { return Unknown; } + if rec != rec2 { return Unknown; } + if rec.SurelyAssigned? { return SurelyAssigned; } + case Call(on, callName, typeArgs, args, outs) => + if outs.Some? && dafny_name in outs.value { return SurelyAssigned; } + case Labeled(_, stmts) => + var rec := DetectAssignmentStatus(stmts, dafny_name); + if !rec.NotAssigned? { return rec; } + case DeclareVar(name, _, _) => + if name == dafny_name { return NotAssigned; /* Shadowed */ } + case Return(_) | EarlyReturn() | JumpTailCallStart() => + return NotAssigned; + case Print(_) => + case _ => + return Unknown; + } + assert DetectAssignmentStatus(stmts_remainder[i..][1..], dafny_name) == DetectAssignmentStatus(stmts_remainder[i+1..], dafny_name); } + return NotAssigned; } } diff --git a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy index 3960a82bfcc..c11ae4de1e7 100644 --- a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy +++ b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy @@ -1736,43 +1736,80 @@ module {:extern "DCOMP"} DafnyToRustCompiler { readIdents := {}; var i := 0; newEnv := env; - ghost var oldStmts := stmts; - var stmts := stmts; // Make it mutable while i < |stmts| { var stmt := stmts[i]; - // Avoid maybe placebo wrapping if not necessary - match stmt { - case DeclareVar(name, optType, None) => - var laterAssignmentStatus := DetectAssignmentStatus(stmts[i + 1..], name); - newEnv := newEnv.AddAssignmentStatus(escapeVar(name), laterAssignmentStatus); - case DeclareVar(name, optType, Some(InitializationValue(typ))) => - var tpe := GenType(typ, GenTypeContext.default()); - var varName := escapeVar(name); - var laterAssignmentStatus := DetectAssignmentStatus(stmts[i + 1..], name); - newEnv := newEnv.AddAssignmentStatus(varName, laterAssignmentStatus); - case _ => - - } - assume {:axiom} stmt in oldStmts; - var stmtExpr, recIdents, newEnv2 := GenStmt(stmt, selfIdent, newEnv, isLast && (i == |stmts| - 1), earlyReturn); - newEnv := newEnv2; + // Special case "var x: T; x = ...". We need to merge them + // because normally x can read a variable named x, and with two statements + // this is not possible. + if stmt.DeclareVar? && stmt.maybeValue.None? && + i + 1 < |stmts| && + stmts[i + 1].Assign? && + stmts[i + 1].lhs.Ident? && + stmts[i + 1].lhs.ident == stmt.name { + var name := stmt.name; + var typ := stmt.typ; + var stmtExpr, recIdents, newEnv2 := GenDeclareVarAssign(name, typ, stmts[i + 1].value, selfIdent, newEnv); + newEnv := newEnv2; + readIdents := readIdents + (recIdents - declarations); + declarations := declarations + {escapeVar(name)}; + generated := generated.Then(stmtExpr); + i := i + 2; + } else { + // Avoid maybe placebo wrapping if not necessary + match stmt { + case DeclareVar(name, optType, None) => + var laterAssignmentStatus := DetectAssignmentStatus(stmts[i + 1..], name); + newEnv := newEnv.AddAssignmentStatus(escapeVar(name), laterAssignmentStatus); + case DeclareVar(name, optType, Some(InitializationValue(typ))) => + var tpe := GenType(typ, GenTypeContext.default()); + var varName := escapeVar(name); + var laterAssignmentStatus := DetectAssignmentStatus(stmts[i + 1..], name); + newEnv := newEnv.AddAssignmentStatus(varName, laterAssignmentStatus); + case _ => + } + var stmtExpr, recIdents, newEnv2 := GenStmt(stmt, selfIdent, newEnv, isLast && (i == |stmts| - 1), earlyReturn); + newEnv := newEnv2; - match stmt { - case DeclareVar(name, _, _) => { - declarations := declarations + {escapeVar(name)}; + match stmt { + case DeclareVar(name, _, _) => { + declarations := declarations + {escapeVar(name)}; + } + case _ => {} + } + readIdents := readIdents + (recIdents - declarations); + generated := generated.Then(stmtExpr); + if stmtExpr.Return? { // The rest of statements is unreachable + break; } - case _ => {} - } - readIdents := readIdents + (recIdents - declarations); - generated := generated.Then(stmtExpr); - i := i + 1; - if stmtExpr.Return? { // The rest of statements is unreachable - break; + i := i + 1; } } } + method GenDeclareVarAssign(name: VarName, typ: Type, rhs: Expression, selfIdent: SelfInfo, env: Environment) + returns (generated: R.Expr, readIdents: set, newEnv: Environment) + decreases rhs + modifies this + { + var tpe := GenType(typ, GenTypeContext.default()); + var varName := escapeVar(name); + var exprRhs; + if rhs.InitializationValue? && + tpe.IsObjectOrPointer() { + readIdents := {}; + tpe := if rhs.NewUninitArray? then tpe.TypeAtInitialization() else tpe; + exprRhs := tpe.ToNullExpr(); + } else { + var expr, exprOwnership; + expr, exprOwnership, readIdents := GenExpr(rhs, selfIdent, env, OwnershipOwned); + tpe := if rhs.NewUninitArray? then tpe.TypeAtInitialization() else tpe; + exprRhs := expr; + } + generated := R.DeclareVar(R.MUT, varName, Some(tpe), Some(exprRhs)); + newEnv := env.AddAssigned(varName, tpe); + } + method GenAssignLhs(lhs: AssignLhs, rhs: R.Expr, selfIdent: SelfInfo, env: Environment) returns (generated: R.Expr, needsIIFE: bool, readIdents: set, newEnv: Environment) decreases lhs, 1 modifies this @@ -1962,30 +1999,18 @@ module {:extern "DCOMP"} DafnyToRustCompiler { var varName := escapeVar(name); var hasCopySemantics := tpe.CanReadWithoutClone(); if expression.InitializationValue? && !hasCopySemantics { + // We might be able to just let the variable uninitialized. if env.IsAssignmentStatusKnown(varName) { - var tpe := GenType(typ, GenTypeContext.default()); generated := R.DeclareVar(R.MUT, varName, Some(tpe), None); - readIdents := {}; - newEnv := env.AddAssigned(varName, tpe); } else { generated := R.DeclareVar(R.MUT, varName, None, Some(R.MaybePlaceboPath.AsExpr().ApplyType1(tpe).FSel("new").Apply0())); - readIdents := {}; - newEnv := env.AddAssigned(varName, R.MaybePlaceboType(tpe)); + tpe := R.MaybePlaceboType(tpe); } - } else { - var expr, recIdents; - if expression.InitializationValue? && - tpe.IsObjectOrPointer() { - expr := tpe.ToNullExpr(); - recIdents := {}; - } else { - var exprOwnership; - expr, exprOwnership, recIdents := GenExpr(expression, selfIdent, env, OwnershipOwned); - } - readIdents := recIdents; - tpe := if expression.NewUninitArray? then tpe.TypeAtInitialization() else tpe; - generated := R.DeclareVar(R.MUT, varName, Some(tpe), Some(expr)); + readIdents := {}; newEnv := env.AddAssigned(varName, tpe); + } else { + generated, readIdents, newEnv := GenDeclareVarAssign(name, typ, expression, selfIdent, env); + return; } } case DeclareVar(name, typ, None) => { diff --git a/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs b/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs index 1cf2e5f77fd..31e88065057 100644 --- a/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs +++ b/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs @@ -1998,85 +1998,145 @@ public void GenStmts(Dafny.ISequence stmts, Defs._ISelfInfo se BigInteger _1_i; _1_i = BigInteger.Zero; newEnv = env; - Dafny.ISequence _2_stmts; - _2_stmts = stmts; - while ((_1_i) < (new BigInteger((_2_stmts).Count))) { - DAST._IStatement _3_stmt; - _3_stmt = (_2_stmts).Select(_1_i); - DAST._IStatement _source0 = _3_stmt; - { - if (_source0.is_DeclareVar) { - Dafny.ISequence _4_name = _source0.dtor_name; - DAST._IType _5_optType = _source0.dtor_typ; - Std.Wrappers._IOption maybeValue0 = _source0.dtor_maybeValue; - if (maybeValue0.is_None) { - Defs._IAssignmentStatus _6_laterAssignmentStatus; - _6_laterAssignmentStatus = Defs.__default.DetectAssignmentStatus((_2_stmts).Drop((_1_i) + (BigInteger.One)), _4_name); - newEnv = (newEnv).AddAssignmentStatus(Defs.__default.escapeVar(_4_name), _6_laterAssignmentStatus); - goto after_match0; + while ((_1_i) < (new BigInteger((stmts).Count))) { + DAST._IStatement _2_stmt; + _2_stmt = (stmts).Select(_1_i); + if (((((((_2_stmt).is_DeclareVar) && (((_2_stmt).dtor_maybeValue).is_None)) && (((_1_i) + (BigInteger.One)) < (new BigInteger((stmts).Count)))) && (((stmts).Select((_1_i) + (BigInteger.One))).is_Assign)) && ((((stmts).Select((_1_i) + (BigInteger.One))).dtor_lhs).is_Ident)) && (object.Equals((((stmts).Select((_1_i) + (BigInteger.One))).dtor_lhs).dtor_ident, (_2_stmt).dtor_name))) { + Dafny.ISequence _3_name; + _3_name = (_2_stmt).dtor_name; + DAST._IType _4_typ; + _4_typ = (_2_stmt).dtor_typ; + RAST._IExpr _5_stmtExpr; + Dafny.ISet> _6_recIdents; + Defs._IEnvironment _7_newEnv2; + RAST._IExpr _out0; + Dafny.ISet> _out1; + Defs._IEnvironment _out2; + (this).GenDeclareVarAssign(_3_name, _4_typ, ((stmts).Select((_1_i) + (BigInteger.One))).dtor_value, selfIdent, newEnv, out _out0, out _out1, out _out2); + _5_stmtExpr = _out0; + _6_recIdents = _out1; + _7_newEnv2 = _out2; + newEnv = _7_newEnv2; + readIdents = Dafny.Set>.Union(readIdents, Dafny.Set>.Difference(_6_recIdents, _0_declarations)); + _0_declarations = Dafny.Set>.Union(_0_declarations, Dafny.Set>.FromElements(Defs.__default.escapeVar(_3_name))); + generated = (generated).Then(_5_stmtExpr); + _1_i = (_1_i) + (new BigInteger(2)); + } else { + DAST._IStatement _source0 = _2_stmt; + { + if (_source0.is_DeclareVar) { + Dafny.ISequence _8_name = _source0.dtor_name; + DAST._IType _9_optType = _source0.dtor_typ; + Std.Wrappers._IOption maybeValue0 = _source0.dtor_maybeValue; + if (maybeValue0.is_None) { + Defs._IAssignmentStatus _10_laterAssignmentStatus; + _10_laterAssignmentStatus = Defs.__default.DetectAssignmentStatus((stmts).Drop((_1_i) + (BigInteger.One)), _8_name); + newEnv = (newEnv).AddAssignmentStatus(Defs.__default.escapeVar(_8_name), _10_laterAssignmentStatus); + goto after_match0; + } } } - } - { - if (_source0.is_DeclareVar) { - Dafny.ISequence _7_name = _source0.dtor_name; - DAST._IType _8_optType = _source0.dtor_typ; - Std.Wrappers._IOption maybeValue1 = _source0.dtor_maybeValue; - if (maybeValue1.is_Some) { - DAST._IExpression value0 = maybeValue1.dtor_value; - if (value0.is_InitializationValue) { - DAST._IType _9_typ = value0.dtor_typ; - RAST._IType _10_tpe; - RAST._IType _out0; - _out0 = (this).GenType(_9_typ, Defs.GenTypeContext.@default()); - _10_tpe = _out0; - Dafny.ISequence _11_varName; - _11_varName = Defs.__default.escapeVar(_7_name); - Defs._IAssignmentStatus _12_laterAssignmentStatus; - _12_laterAssignmentStatus = Defs.__default.DetectAssignmentStatus((_2_stmts).Drop((_1_i) + (BigInteger.One)), _7_name); - newEnv = (newEnv).AddAssignmentStatus(_11_varName, _12_laterAssignmentStatus); - goto after_match0; + { + if (_source0.is_DeclareVar) { + Dafny.ISequence _11_name = _source0.dtor_name; + DAST._IType _12_optType = _source0.dtor_typ; + Std.Wrappers._IOption maybeValue1 = _source0.dtor_maybeValue; + if (maybeValue1.is_Some) { + DAST._IExpression value0 = maybeValue1.dtor_value; + if (value0.is_InitializationValue) { + DAST._IType _13_typ = value0.dtor_typ; + RAST._IType _14_tpe; + RAST._IType _out3; + _out3 = (this).GenType(_13_typ, Defs.GenTypeContext.@default()); + _14_tpe = _out3; + Dafny.ISequence _15_varName; + _15_varName = Defs.__default.escapeVar(_11_name); + Defs._IAssignmentStatus _16_laterAssignmentStatus; + _16_laterAssignmentStatus = Defs.__default.DetectAssignmentStatus((stmts).Drop((_1_i) + (BigInteger.One)), _11_name); + newEnv = (newEnv).AddAssignmentStatus(_15_varName, _16_laterAssignmentStatus); + goto after_match0; + } } } } - } - { - } - after_match0: ; - RAST._IExpr _13_stmtExpr; - Dafny.ISet> _14_recIdents; - Defs._IEnvironment _15_newEnv2; - RAST._IExpr _out1; - Dafny.ISet> _out2; - Defs._IEnvironment _out3; - (this).GenStmt(_3_stmt, selfIdent, newEnv, (isLast) && ((_1_i) == ((new BigInteger((_2_stmts).Count)) - (BigInteger.One))), earlyReturn, out _out1, out _out2, out _out3); - _13_stmtExpr = _out1; - _14_recIdents = _out2; - _15_newEnv2 = _out3; - newEnv = _15_newEnv2; - DAST._IStatement _source1 = _3_stmt; - { - if (_source1.is_DeclareVar) { - Dafny.ISequence _16_name = _source1.dtor_name; - { - _0_declarations = Dafny.Set>.Union(_0_declarations, Dafny.Set>.FromElements(Defs.__default.escapeVar(_16_name))); + { + } + after_match0: ; + RAST._IExpr _17_stmtExpr; + Dafny.ISet> _18_recIdents; + Defs._IEnvironment _19_newEnv2; + RAST._IExpr _out4; + Dafny.ISet> _out5; + Defs._IEnvironment _out6; + (this).GenStmt(_2_stmt, selfIdent, newEnv, (isLast) && ((_1_i) == ((new BigInteger((stmts).Count)) - (BigInteger.One))), earlyReturn, out _out4, out _out5, out _out6); + _17_stmtExpr = _out4; + _18_recIdents = _out5; + _19_newEnv2 = _out6; + newEnv = _19_newEnv2; + DAST._IStatement _source1 = _2_stmt; + { + if (_source1.is_DeclareVar) { + Dafny.ISequence _20_name = _source1.dtor_name; + { + _0_declarations = Dafny.Set>.Union(_0_declarations, Dafny.Set>.FromElements(Defs.__default.escapeVar(_20_name))); + } + goto after_match1; } - goto after_match1; } - } - { - } - after_match1: ; - readIdents = Dafny.Set>.Union(readIdents, Dafny.Set>.Difference(_14_recIdents, _0_declarations)); - generated = (generated).Then(_13_stmtExpr); - _1_i = (_1_i) + (BigInteger.One); - if ((_13_stmtExpr).is_Return) { - goto after_0; + { + } + after_match1: ; + readIdents = Dafny.Set>.Union(readIdents, Dafny.Set>.Difference(_18_recIdents, _0_declarations)); + generated = (generated).Then(_17_stmtExpr); + if ((_17_stmtExpr).is_Return) { + goto after_0; + } + _1_i = (_1_i) + (BigInteger.One); } continue_0: ; } after_0: ; } + public void GenDeclareVarAssign(Dafny.ISequence name, DAST._IType typ, DAST._IExpression rhs, Defs._ISelfInfo selfIdent, Defs._IEnvironment env, out RAST._IExpr generated, out Dafny.ISet> readIdents, out Defs._IEnvironment newEnv) + { + generated = RAST.Expr.Default(); + readIdents = Dafny.Set>.Empty; + newEnv = Defs.Environment.Default(); + RAST._IType _0_tpe; + RAST._IType _out0; + _out0 = (this).GenType(typ, Defs.GenTypeContext.@default()); + _0_tpe = _out0; + Dafny.ISequence _1_varName; + _1_varName = Defs.__default.escapeVar(name); + RAST._IExpr _2_exprRhs = RAST.Expr.Default(); + if (((rhs).is_InitializationValue) && ((_0_tpe).IsObjectOrPointer())) { + readIdents = Dafny.Set>.FromElements(); + if ((rhs).is_NewUninitArray) { + _0_tpe = (_0_tpe).TypeAtInitialization(); + } else { + _0_tpe = _0_tpe; + } + _2_exprRhs = (_0_tpe).ToNullExpr(); + } else { + RAST._IExpr _3_expr = RAST.Expr.Default(); + Defs._IOwnership _4_exprOwnership = Defs.Ownership.Default(); + RAST._IExpr _out1; + Defs._IOwnership _out2; + Dafny.ISet> _out3; + (this).GenExpr(rhs, selfIdent, env, Defs.Ownership.create_OwnershipOwned(), out _out1, out _out2, out _out3); + _3_expr = _out1; + _4_exprOwnership = _out2; + readIdents = _out3; + if ((rhs).is_NewUninitArray) { + _0_tpe = (_0_tpe).TypeAtInitialization(); + } else { + _0_tpe = _0_tpe; + } + _2_exprRhs = _3_expr; + } + generated = RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), _1_varName, Std.Wrappers.Option.create_Some(_0_tpe), Std.Wrappers.Option.create_Some(_2_exprRhs)); + newEnv = (env).AddAssigned(_1_varName, _0_tpe); + } public void GenAssignLhs(DAST._IAssignLhs lhs, RAST._IExpr rhs, Defs._ISelfInfo selfIdent, Defs._IEnvironment env, out RAST._IExpr generated, out bool needsIIFE, out Dafny.ISet> readIdents, out Defs._IEnvironment newEnv) { generated = RAST.Expr.Default(); @@ -2448,42 +2508,22 @@ public void GenStmt(DAST._IStatement stmt, Defs._ISelfInfo selfIdent, Defs._IEnv _15_hasCopySemantics = (_13_tpe).CanReadWithoutClone(); if (((_12_expression).is_InitializationValue) && (!(_15_hasCopySemantics))) { if ((env).IsAssignmentStatusKnown(_14_varName)) { - RAST._IType _16_tpe; - RAST._IType _out5; - _out5 = (this).GenType(_11_typ, Defs.GenTypeContext.@default()); - _16_tpe = _out5; - generated = RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), _14_varName, Std.Wrappers.Option.create_Some(_16_tpe), Std.Wrappers.Option.create_None()); - readIdents = Dafny.Set>.FromElements(); - newEnv = (env).AddAssigned(_14_varName, _16_tpe); + generated = RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), _14_varName, Std.Wrappers.Option.create_Some(_13_tpe), Std.Wrappers.Option.create_None()); } else { generated = RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), _14_varName, Std.Wrappers.Option.create_None(), Std.Wrappers.Option.create_Some(((((RAST.__default.MaybePlaceboPath).AsExpr()).ApplyType1(_13_tpe)).FSel(Dafny.Sequence.UnicodeFromString("new"))).Apply0())); - readIdents = Dafny.Set>.FromElements(); - newEnv = (env).AddAssigned(_14_varName, RAST.__default.MaybePlaceboType(_13_tpe)); - } - } else { - RAST._IExpr _17_expr = RAST.Expr.Default(); - Dafny.ISet> _18_recIdents = Dafny.Set>.Empty; - if (((_12_expression).is_InitializationValue) && ((_13_tpe).IsObjectOrPointer())) { - _17_expr = (_13_tpe).ToNullExpr(); - _18_recIdents = Dafny.Set>.FromElements(); - } else { - Defs._IOwnership _19_exprOwnership = Defs.Ownership.Default(); - RAST._IExpr _out6; - Defs._IOwnership _out7; - Dafny.ISet> _out8; - (this).GenExpr(_12_expression, selfIdent, env, Defs.Ownership.create_OwnershipOwned(), out _out6, out _out7, out _out8); - _17_expr = _out6; - _19_exprOwnership = _out7; - _18_recIdents = _out8; - } - readIdents = _18_recIdents; - if ((_12_expression).is_NewUninitArray) { - _13_tpe = (_13_tpe).TypeAtInitialization(); - } else { - _13_tpe = _13_tpe; + _13_tpe = RAST.__default.MaybePlaceboType(_13_tpe); } - generated = RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), _14_varName, Std.Wrappers.Option.create_Some(_13_tpe), Std.Wrappers.Option.create_Some(_17_expr)); + readIdents = Dafny.Set>.FromElements(); newEnv = (env).AddAssigned(_14_varName, _13_tpe); + } else { + RAST._IExpr _out5; + Dafny.ISet> _out6; + Defs._IEnvironment _out7; + (this).GenDeclareVarAssign(_10_name, _11_typ, _12_expression, selfIdent, env, out _out5, out _out6, out _out7); + generated = _out5; + readIdents = _out6; + newEnv = _out7; + return ; } } goto after_match0; @@ -2492,31 +2532,31 @@ public void GenStmt(DAST._IStatement stmt, Defs._ISelfInfo selfIdent, Defs._IEnv } { if (_source0.is_DeclareVar) { - Dafny.ISequence _20_name = _source0.dtor_name; - DAST._IType _21_typ = _source0.dtor_typ; + Dafny.ISequence _16_name = _source0.dtor_name; + DAST._IType _17_typ = _source0.dtor_typ; Std.Wrappers._IOption maybeValue1 = _source0.dtor_maybeValue; if (maybeValue1.is_None) { { - Dafny.ISequence _22_varName; - _22_varName = Defs.__default.escapeVar(_20_name); - if ((env).IsAssignmentStatusKnown(_22_varName)) { - RAST._IType _23_tpe; - RAST._IType _out9; - _out9 = (this).GenType(_21_typ, Defs.GenTypeContext.@default()); - _23_tpe = _out9; - generated = RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), _22_varName, Std.Wrappers.Option.create_Some(_23_tpe), Std.Wrappers.Option.create_None()); + Dafny.ISequence _18_varName; + _18_varName = Defs.__default.escapeVar(_16_name); + if ((env).IsAssignmentStatusKnown(_18_varName)) { + RAST._IType _19_tpe; + RAST._IType _out8; + _out8 = (this).GenType(_17_typ, Defs.GenTypeContext.@default()); + _19_tpe = _out8; + generated = RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), _18_varName, Std.Wrappers.Option.create_Some(_19_tpe), Std.Wrappers.Option.create_None()); readIdents = Dafny.Set>.FromElements(); - newEnv = (env).AddAssigned(_22_varName, _23_tpe); + newEnv = (env).AddAssigned(_18_varName, _19_tpe); } else { - DAST._IStatement _24_newStmt; - _24_newStmt = DAST.Statement.create_DeclareVar(_20_name, _21_typ, Std.Wrappers.Option.create_Some(DAST.Expression.create_InitializationValue(_21_typ))); - RAST._IExpr _out10; - Dafny.ISet> _out11; - Defs._IEnvironment _out12; - (this).GenStmt(_24_newStmt, selfIdent, env, isLast, earlyReturn, out _out10, out _out11, out _out12); - generated = _out10; - readIdents = _out11; - newEnv = _out12; + DAST._IStatement _20_newStmt; + _20_newStmt = DAST.Statement.create_DeclareVar(_16_name, _17_typ, Std.Wrappers.Option.create_Some(DAST.Expression.create_InitializationValue(_17_typ))); + RAST._IExpr _out9; + Dafny.ISet> _out10; + Defs._IEnvironment _out11; + (this).GenStmt(_20_newStmt, selfIdent, env, isLast, earlyReturn, out _out9, out _out10, out _out11); + generated = _out9; + readIdents = _out10; + newEnv = _out11; } } goto after_match0; @@ -2525,124 +2565,124 @@ public void GenStmt(DAST._IStatement stmt, Defs._ISelfInfo selfIdent, Defs._IEnv } { if (_source0.is_Assign) { - DAST._IAssignLhs _25_lhs = _source0.dtor_lhs; - DAST._IExpression _26_expression = _source0.dtor_value; + DAST._IAssignLhs _21_lhs = _source0.dtor_lhs; + DAST._IExpression _22_expression = _source0.dtor_value; { - RAST._IExpr _27_exprGen; - Defs._IOwnership _28___v46; - Dafny.ISet> _29_exprIdents; - RAST._IExpr _out13; - Defs._IOwnership _out14; - Dafny.ISet> _out15; - (this).GenExpr(_26_expression, selfIdent, env, Defs.Ownership.create_OwnershipOwned(), out _out13, out _out14, out _out15); - _27_exprGen = _out13; - _28___v46 = _out14; - _29_exprIdents = _out15; - if ((_25_lhs).is_Ident) { - Dafny.ISequence _30_rustId; - _30_rustId = Defs.__default.escapeVar((_25_lhs).dtor_ident); - Std.Wrappers._IOption _31_tpe; - _31_tpe = (env).GetType(_30_rustId); - if (((_31_tpe).is_Some) && ((((_31_tpe).dtor_value).ExtractMaybePlacebo()).is_Some)) { - _27_exprGen = RAST.__default.MaybePlacebo(_27_exprGen); + RAST._IExpr _23_exprGen; + Defs._IOwnership _24___v46; + Dafny.ISet> _25_exprIdents; + RAST._IExpr _out12; + Defs._IOwnership _out13; + Dafny.ISet> _out14; + (this).GenExpr(_22_expression, selfIdent, env, Defs.Ownership.create_OwnershipOwned(), out _out12, out _out13, out _out14); + _23_exprGen = _out12; + _24___v46 = _out13; + _25_exprIdents = _out14; + if ((_21_lhs).is_Ident) { + Dafny.ISequence _26_rustId; + _26_rustId = Defs.__default.escapeVar((_21_lhs).dtor_ident); + Std.Wrappers._IOption _27_tpe; + _27_tpe = (env).GetType(_26_rustId); + if (((_27_tpe).is_Some) && ((((_27_tpe).dtor_value).ExtractMaybePlacebo()).is_Some)) { + _23_exprGen = RAST.__default.MaybePlacebo(_23_exprGen); } } - if (((_25_lhs).is_Index) && (((_25_lhs).dtor_expr).is_Ident)) { - Dafny.ISequence _32_rustId; - _32_rustId = Defs.__default.escapeVar(((_25_lhs).dtor_expr).dtor_name); - Std.Wrappers._IOption _33_tpe; - _33_tpe = (env).GetType(_32_rustId); - if (((_33_tpe).is_Some) && ((((_33_tpe).dtor_value).ExtractMaybeUninitArrayElement()).is_Some)) { - _27_exprGen = RAST.__default.MaybeUninitNew(_27_exprGen); + if (((_21_lhs).is_Index) && (((_21_lhs).dtor_expr).is_Ident)) { + Dafny.ISequence _28_rustId; + _28_rustId = Defs.__default.escapeVar(((_21_lhs).dtor_expr).dtor_name); + Std.Wrappers._IOption _29_tpe; + _29_tpe = (env).GetType(_28_rustId); + if (((_29_tpe).is_Some) && ((((_29_tpe).dtor_value).ExtractMaybeUninitArrayElement()).is_Some)) { + _23_exprGen = RAST.__default.MaybeUninitNew(_23_exprGen); } } - RAST._IExpr _34_lhsGen; - bool _35_needsIIFE; - Dafny.ISet> _36_recIdents; - Defs._IEnvironment _37_resEnv; - RAST._IExpr _out16; - bool _out17; - Dafny.ISet> _out18; - Defs._IEnvironment _out19; - (this).GenAssignLhs(_25_lhs, _27_exprGen, selfIdent, env, out _out16, out _out17, out _out18, out _out19); - _34_lhsGen = _out16; - _35_needsIIFE = _out17; - _36_recIdents = _out18; - _37_resEnv = _out19; - generated = _34_lhsGen; - newEnv = _37_resEnv; - if (_35_needsIIFE) { + RAST._IExpr _30_lhsGen; + bool _31_needsIIFE; + Dafny.ISet> _32_recIdents; + Defs._IEnvironment _33_resEnv; + RAST._IExpr _out15; + bool _out16; + Dafny.ISet> _out17; + Defs._IEnvironment _out18; + (this).GenAssignLhs(_21_lhs, _23_exprGen, selfIdent, env, out _out15, out _out16, out _out17, out _out18); + _30_lhsGen = _out15; + _31_needsIIFE = _out16; + _32_recIdents = _out17; + _33_resEnv = _out18; + generated = _30_lhsGen; + newEnv = _33_resEnv; + if (_31_needsIIFE) { generated = RAST.Expr.create_Block(generated); } - readIdents = Dafny.Set>.Union(_36_recIdents, _29_exprIdents); + readIdents = Dafny.Set>.Union(_32_recIdents, _25_exprIdents); } goto after_match0; } } { if (_source0.is_If) { - DAST._IExpression _38_cond = _source0.dtor_cond; - Dafny.ISequence _39_thnDafny = _source0.dtor_thn; - Dafny.ISequence _40_elsDafny = _source0.dtor_els; + DAST._IExpression _34_cond = _source0.dtor_cond; + Dafny.ISequence _35_thnDafny = _source0.dtor_thn; + Dafny.ISequence _36_elsDafny = _source0.dtor_els; { - RAST._IExpr _41_cond; - Defs._IOwnership _42___v47; - Dafny.ISet> _43_recIdents; - RAST._IExpr _out20; - Defs._IOwnership _out21; - Dafny.ISet> _out22; - (this).GenExpr(_38_cond, selfIdent, env, Defs.Ownership.create_OwnershipOwned(), out _out20, out _out21, out _out22); - _41_cond = _out20; - _42___v47 = _out21; - _43_recIdents = _out22; - Dafny.ISequence _44_condString; - _44_condString = (_41_cond)._ToString(Defs.__default.IND); - readIdents = _43_recIdents; - RAST._IExpr _45_thn; - Dafny.ISet> _46_thnIdents; - Defs._IEnvironment _47_thnEnv; - RAST._IExpr _out23; - Dafny.ISet> _out24; - Defs._IEnvironment _out25; - (this).GenStmts(_39_thnDafny, selfIdent, env, isLast, earlyReturn, out _out23, out _out24, out _out25); - _45_thn = _out23; - _46_thnIdents = _out24; - _47_thnEnv = _out25; - readIdents = Dafny.Set>.Union(readIdents, _46_thnIdents); - RAST._IExpr _48_els; - Dafny.ISet> _49_elsIdents; - Defs._IEnvironment _50_elsEnv; - RAST._IExpr _out26; - Dafny.ISet> _out27; - Defs._IEnvironment _out28; - (this).GenStmts(_40_elsDafny, selfIdent, env, isLast, earlyReturn, out _out26, out _out27, out _out28); - _48_els = _out26; - _49_elsIdents = _out27; - _50_elsEnv = _out28; - readIdents = Dafny.Set>.Union(readIdents, _49_elsIdents); + RAST._IExpr _37_cond; + Defs._IOwnership _38___v47; + Dafny.ISet> _39_recIdents; + RAST._IExpr _out19; + Defs._IOwnership _out20; + Dafny.ISet> _out21; + (this).GenExpr(_34_cond, selfIdent, env, Defs.Ownership.create_OwnershipOwned(), out _out19, out _out20, out _out21); + _37_cond = _out19; + _38___v47 = _out20; + _39_recIdents = _out21; + Dafny.ISequence _40_condString; + _40_condString = (_37_cond)._ToString(Defs.__default.IND); + readIdents = _39_recIdents; + RAST._IExpr _41_thn; + Dafny.ISet> _42_thnIdents; + Defs._IEnvironment _43_thnEnv; + RAST._IExpr _out22; + Dafny.ISet> _out23; + Defs._IEnvironment _out24; + (this).GenStmts(_35_thnDafny, selfIdent, env, isLast, earlyReturn, out _out22, out _out23, out _out24); + _41_thn = _out22; + _42_thnIdents = _out23; + _43_thnEnv = _out24; + readIdents = Dafny.Set>.Union(readIdents, _42_thnIdents); + RAST._IExpr _44_els; + Dafny.ISet> _45_elsIdents; + Defs._IEnvironment _46_elsEnv; + RAST._IExpr _out25; + Dafny.ISet> _out26; + Defs._IEnvironment _out27; + (this).GenStmts(_36_elsDafny, selfIdent, env, isLast, earlyReturn, out _out25, out _out26, out _out27); + _44_els = _out25; + _45_elsIdents = _out26; + _46_elsEnv = _out27; + readIdents = Dafny.Set>.Union(readIdents, _45_elsIdents); newEnv = env; - generated = RAST.Expr.create_IfExpr(_41_cond, _45_thn, _48_els); + generated = RAST.Expr.create_IfExpr(_37_cond, _41_thn, _44_els); } goto after_match0; } } { if (_source0.is_Labeled) { - Dafny.ISequence _51_lbl = _source0.dtor_lbl; - Dafny.ISequence _52_body = _source0.dtor_body; + Dafny.ISequence _47_lbl = _source0.dtor_lbl; + Dafny.ISequence _48_body = _source0.dtor_body; { - RAST._IExpr _53_body; - Dafny.ISet> _54_bodyIdents; - Defs._IEnvironment _55_env2; - RAST._IExpr _out29; - Dafny.ISet> _out30; - Defs._IEnvironment _out31; - (this).GenStmts(_52_body, selfIdent, env, isLast, earlyReturn, out _out29, out _out30, out _out31); - _53_body = _out29; - _54_bodyIdents = _out30; - _55_env2 = _out31; - readIdents = _54_bodyIdents; - generated = RAST.Expr.create_Labelled(Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("label_"), _51_lbl), RAST.Expr.create_Loop(Std.Wrappers.Option.create_None(), RAST.Expr.create_StmtExpr(_53_body, RAST.Expr.create_Break(Std.Wrappers.Option>.create_None())))); + RAST._IExpr _49_body; + Dafny.ISet> _50_bodyIdents; + Defs._IEnvironment _51_env2; + RAST._IExpr _out28; + Dafny.ISet> _out29; + Defs._IEnvironment _out30; + (this).GenStmts(_48_body, selfIdent, env, isLast, earlyReturn, out _out28, out _out29, out _out30); + _49_body = _out28; + _50_bodyIdents = _out29; + _51_env2 = _out30; + readIdents = _50_bodyIdents; + generated = RAST.Expr.create_Labelled(Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("label_"), _47_lbl), RAST.Expr.create_Loop(Std.Wrappers.Option.create_None(), RAST.Expr.create_StmtExpr(_49_body, RAST.Expr.create_Break(Std.Wrappers.Option>.create_None())))); newEnv = env; } goto after_match0; @@ -2650,91 +2690,91 @@ public void GenStmt(DAST._IStatement stmt, Defs._ISelfInfo selfIdent, Defs._IEnv } { if (_source0.is_While) { - DAST._IExpression _56_cond = _source0.dtor_cond; - Dafny.ISequence _57_body = _source0.dtor_body; + DAST._IExpression _52_cond = _source0.dtor_cond; + Dafny.ISequence _53_body = _source0.dtor_body; { - RAST._IExpr _58_cond; - Defs._IOwnership _59___v48; - Dafny.ISet> _60_recIdents; - RAST._IExpr _out32; - Defs._IOwnership _out33; - Dafny.ISet> _out34; - (this).GenExpr(_56_cond, selfIdent, env, Defs.Ownership.create_OwnershipOwned(), out _out32, out _out33, out _out34); - _58_cond = _out32; - _59___v48 = _out33; - _60_recIdents = _out34; - readIdents = _60_recIdents; - RAST._IExpr _61_bodyExpr; - Dafny.ISet> _62_bodyIdents; - Defs._IEnvironment _63_bodyEnv; - RAST._IExpr _out35; - Dafny.ISet> _out36; - Defs._IEnvironment _out37; - (this).GenStmts(_57_body, selfIdent, env, false, earlyReturn, out _out35, out _out36, out _out37); - _61_bodyExpr = _out35; - _62_bodyIdents = _out36; - _63_bodyEnv = _out37; + RAST._IExpr _54_cond; + Defs._IOwnership _55___v48; + Dafny.ISet> _56_recIdents; + RAST._IExpr _out31; + Defs._IOwnership _out32; + Dafny.ISet> _out33; + (this).GenExpr(_52_cond, selfIdent, env, Defs.Ownership.create_OwnershipOwned(), out _out31, out _out32, out _out33); + _54_cond = _out31; + _55___v48 = _out32; + _56_recIdents = _out33; + readIdents = _56_recIdents; + RAST._IExpr _57_bodyExpr; + Dafny.ISet> _58_bodyIdents; + Defs._IEnvironment _59_bodyEnv; + RAST._IExpr _out34; + Dafny.ISet> _out35; + Defs._IEnvironment _out36; + (this).GenStmts(_53_body, selfIdent, env, false, earlyReturn, out _out34, out _out35, out _out36); + _57_bodyExpr = _out34; + _58_bodyIdents = _out35; + _59_bodyEnv = _out36; newEnv = env; - readIdents = Dafny.Set>.Union(readIdents, _62_bodyIdents); - generated = RAST.Expr.create_Loop(Std.Wrappers.Option.create_Some(_58_cond), _61_bodyExpr); + readIdents = Dafny.Set>.Union(readIdents, _58_bodyIdents); + generated = RAST.Expr.create_Loop(Std.Wrappers.Option.create_Some(_54_cond), _57_bodyExpr); } goto after_match0; } } { if (_source0.is_Foreach) { - Dafny.ISequence _64_boundName = _source0.dtor_boundName; - DAST._IType _65_boundType = _source0.dtor_boundType; - DAST._IExpression _66_overExpr = _source0.dtor_over; - Dafny.ISequence _67_body = _source0.dtor_body; + Dafny.ISequence _60_boundName = _source0.dtor_boundName; + DAST._IType _61_boundType = _source0.dtor_boundType; + DAST._IExpression _62_overExpr = _source0.dtor_over; + Dafny.ISequence _63_body = _source0.dtor_body; { - RAST._IExpr _68_over; - Defs._IOwnership _69___v49; - Dafny.ISet> _70_recIdents; - RAST._IExpr _out38; - Defs._IOwnership _out39; - Dafny.ISet> _out40; - (this).GenExpr(_66_overExpr, selfIdent, env, Defs.Ownership.create_OwnershipOwned(), out _out38, out _out39, out _out40); - _68_over = _out38; - _69___v49 = _out39; - _70_recIdents = _out40; - if (((_66_overExpr).is_MapBoundedPool) || ((_66_overExpr).is_SetBoundedPool)) { - _68_over = ((_68_over).Sel(Dafny.Sequence.UnicodeFromString("cloned"))).Apply0(); - } - RAST._IType _71_boundTpe; - RAST._IType _out41; - _out41 = (this).GenType(_65_boundType, Defs.GenTypeContext.@default()); - _71_boundTpe = _out41; - readIdents = _70_recIdents; - Dafny.ISequence _72_boundRName; - _72_boundRName = Defs.__default.escapeVar(_64_boundName); - RAST._IExpr _73_bodyExpr; - Dafny.ISet> _74_bodyIdents; - Defs._IEnvironment _75_bodyEnv; - RAST._IExpr _out42; - Dafny.ISet> _out43; - Defs._IEnvironment _out44; - (this).GenStmts(_67_body, selfIdent, (env).AddAssigned(_72_boundRName, _71_boundTpe), false, earlyReturn, out _out42, out _out43, out _out44); - _73_bodyExpr = _out42; - _74_bodyIdents = _out43; - _75_bodyEnv = _out44; - readIdents = Dafny.Set>.Difference(Dafny.Set>.Union(readIdents, _74_bodyIdents), Dafny.Set>.FromElements(_72_boundRName)); + RAST._IExpr _64_over; + Defs._IOwnership _65___v49; + Dafny.ISet> _66_recIdents; + RAST._IExpr _out37; + Defs._IOwnership _out38; + Dafny.ISet> _out39; + (this).GenExpr(_62_overExpr, selfIdent, env, Defs.Ownership.create_OwnershipOwned(), out _out37, out _out38, out _out39); + _64_over = _out37; + _65___v49 = _out38; + _66_recIdents = _out39; + if (((_62_overExpr).is_MapBoundedPool) || ((_62_overExpr).is_SetBoundedPool)) { + _64_over = ((_64_over).Sel(Dafny.Sequence.UnicodeFromString("cloned"))).Apply0(); + } + RAST._IType _67_boundTpe; + RAST._IType _out40; + _out40 = (this).GenType(_61_boundType, Defs.GenTypeContext.@default()); + _67_boundTpe = _out40; + readIdents = _66_recIdents; + Dafny.ISequence _68_boundRName; + _68_boundRName = Defs.__default.escapeVar(_60_boundName); + RAST._IExpr _69_bodyExpr; + Dafny.ISet> _70_bodyIdents; + Defs._IEnvironment _71_bodyEnv; + RAST._IExpr _out41; + Dafny.ISet> _out42; + Defs._IEnvironment _out43; + (this).GenStmts(_63_body, selfIdent, (env).AddAssigned(_68_boundRName, _67_boundTpe), false, earlyReturn, out _out41, out _out42, out _out43); + _69_bodyExpr = _out41; + _70_bodyIdents = _out42; + _71_bodyEnv = _out43; + readIdents = Dafny.Set>.Difference(Dafny.Set>.Union(readIdents, _70_bodyIdents), Dafny.Set>.FromElements(_68_boundRName)); newEnv = env; - generated = RAST.Expr.create_For(_72_boundRName, _68_over, _73_bodyExpr); + generated = RAST.Expr.create_For(_68_boundRName, _64_over, _69_bodyExpr); } goto after_match0; } } { if (_source0.is_Break) { - Std.Wrappers._IOption> _76_toLabel = _source0.dtor_toLabel; + Std.Wrappers._IOption> _72_toLabel = _source0.dtor_toLabel; { - Std.Wrappers._IOption> _source1 = _76_toLabel; + Std.Wrappers._IOption> _source1 = _72_toLabel; { if (_source1.is_Some) { - Dafny.ISequence _77_lbl = _source1.dtor_value; + Dafny.ISequence _73_lbl = _source1.dtor_value; { - generated = RAST.Expr.create_Break(Std.Wrappers.Option>.create_Some(Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("label_"), _77_lbl))); + generated = RAST.Expr.create_Break(Std.Wrappers.Option>.create_Some(Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("label_"), _73_lbl))); } goto after_match1; } @@ -2753,72 +2793,72 @@ public void GenStmt(DAST._IStatement stmt, Defs._ISelfInfo selfIdent, Defs._IEnv } { if (_source0.is_TailRecursive) { - Dafny.ISequence _78_body = _source0.dtor_body; + Dafny.ISequence _74_body = _source0.dtor_body; { generated = (this).InitEmptyExpr(); - Defs._IEnvironment _79_oldEnv; - _79_oldEnv = env; + Defs._IEnvironment _75_oldEnv; + _75_oldEnv = env; if (!object.Equals(selfIdent, Defs.SelfInfo.create_NoSelf())) { - RAST._IExpr _80_selfClone; - Defs._IOwnership _81___v50; - Dafny.ISet> _82___v51; - RAST._IExpr _out45; - Defs._IOwnership _out46; - Dafny.ISet> _out47; - (this).GenIdent((selfIdent).dtor_rSelfName, selfIdent, Defs.Environment.Empty(), Defs.Ownership.create_OwnershipOwned(), out _out45, out _out46, out _out47); - _80_selfClone = _out45; - _81___v50 = _out46; - _82___v51 = _out47; - 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(_80_selfClone))); - if (((_79_oldEnv).dtor_names).Contains((selfIdent).dtor_rSelfName)) { - _79_oldEnv = (_79_oldEnv).RemoveAssigned((selfIdent).dtor_rSelfName); + RAST._IExpr _76_selfClone; + Defs._IOwnership _77___v50; + Dafny.ISet> _78___v51; + RAST._IExpr _out44; + Defs._IOwnership _out45; + Dafny.ISet> _out46; + (this).GenIdent((selfIdent).dtor_rSelfName, selfIdent, Defs.Environment.Empty(), Defs.Ownership.create_OwnershipOwned(), out _out44, out _out45, out _out46); + _76_selfClone = _out44; + _77___v50 = _out45; + _78___v51 = _out46; + 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(_76_selfClone))); + if (((_75_oldEnv).dtor_names).Contains((selfIdent).dtor_rSelfName)) { + _75_oldEnv = (_75_oldEnv).RemoveAssigned((selfIdent).dtor_rSelfName); } } - RAST._IExpr _83_loopBegin; - _83_loopBegin = RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("")); + RAST._IExpr _79_loopBegin; + _79_loopBegin = RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("")); newEnv = env; - BigInteger _hi1 = new BigInteger(((_79_oldEnv).dtor_names).Count); - for (BigInteger _84_paramI = BigInteger.Zero; _84_paramI < _hi1; _84_paramI++) { - Dafny.ISequence _85_param; - _85_param = ((_79_oldEnv).dtor_names).Select(_84_paramI); - if ((_85_param).Equals(Dafny.Sequence.UnicodeFromString("_accumulator"))) { + BigInteger _hi1 = new BigInteger(((_75_oldEnv).dtor_names).Count); + for (BigInteger _80_paramI = BigInteger.Zero; _80_paramI < _hi1; _80_paramI++) { + Dafny.ISequence _81_param; + _81_param = ((_75_oldEnv).dtor_names).Select(_80_paramI); + if ((_81_param).Equals(Dafny.Sequence.UnicodeFromString("_accumulator"))) { goto continue_4_0; } - RAST._IExpr _86_paramInit; - Defs._IOwnership _87___v52; - Dafny.ISet> _88___v53; - RAST._IExpr _out48; - Defs._IOwnership _out49; - Dafny.ISet> _out50; - (this).GenIdent(_85_param, selfIdent, _79_oldEnv, Defs.Ownership.create_OwnershipOwned(), out _out48, out _out49, out _out50); - _86_paramInit = _out48; - _87___v52 = _out49; - _88___v53 = _out50; - Dafny.ISequence _89_recVar; - _89_recVar = Dafny.Sequence.Concat(Defs.__default.TailRecursionPrefix, Std.Strings.__default.OfNat(_84_paramI)); - generated = (generated).Then(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), _89_recVar, Std.Wrappers.Option.create_None(), Std.Wrappers.Option.create_Some(_86_paramInit))); - if (((_79_oldEnv).dtor_types).Contains(_85_param)) { - RAST._IType _90_declaredType; - _90_declaredType = (Dafny.Map, RAST._IType>.Select((_79_oldEnv).dtor_types,_85_param)).ToOwned(); - newEnv = (newEnv).AddAssigned(_85_param, _90_declaredType); - newEnv = (newEnv).AddAssigned(_89_recVar, _90_declaredType); + RAST._IExpr _82_paramInit; + Defs._IOwnership _83___v52; + Dafny.ISet> _84___v53; + RAST._IExpr _out47; + Defs._IOwnership _out48; + Dafny.ISet> _out49; + (this).GenIdent(_81_param, selfIdent, _75_oldEnv, Defs.Ownership.create_OwnershipOwned(), out _out47, out _out48, out _out49); + _82_paramInit = _out47; + _83___v52 = _out48; + _84___v53 = _out49; + Dafny.ISequence _85_recVar; + _85_recVar = Dafny.Sequence.Concat(Defs.__default.TailRecursionPrefix, Std.Strings.__default.OfNat(_80_paramI)); + generated = (generated).Then(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), _85_recVar, Std.Wrappers.Option.create_None(), Std.Wrappers.Option.create_Some(_82_paramInit))); + if (((_75_oldEnv).dtor_types).Contains(_81_param)) { + RAST._IType _86_declaredType; + _86_declaredType = (Dafny.Map, RAST._IType>.Select((_75_oldEnv).dtor_types,_81_param)).ToOwned(); + newEnv = (newEnv).AddAssigned(_81_param, _86_declaredType); + newEnv = (newEnv).AddAssigned(_85_recVar, _86_declaredType); } - _83_loopBegin = (_83_loopBegin).Then(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_CONST(), _85_param, Std.Wrappers.Option.create_None(), Std.Wrappers.Option.create_Some(RAST.Expr.create_Identifier(_89_recVar)))); + _79_loopBegin = (_79_loopBegin).Then(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_CONST(), _81_param, Std.Wrappers.Option.create_None(), Std.Wrappers.Option.create_Some(RAST.Expr.create_Identifier(_85_recVar)))); continue_4_0: ; } after_4_0: ; - RAST._IExpr _91_bodyExpr; - Dafny.ISet> _92_bodyIdents; - Defs._IEnvironment _93_bodyEnv; - RAST._IExpr _out51; - Dafny.ISet> _out52; - Defs._IEnvironment _out53; - (this).GenStmts(_78_body, ((!object.Equals(selfIdent, Defs.SelfInfo.create_NoSelf())) ? (Defs.SelfInfo.create_ThisTyped(Dafny.Sequence.UnicodeFromString("_this"), (selfIdent).dtor_dafnyType)) : (Defs.SelfInfo.create_NoSelf())), newEnv, false, earlyReturn, out _out51, out _out52, out _out53); - _91_bodyExpr = _out51; - _92_bodyIdents = _out52; - _93_bodyEnv = _out53; - readIdents = _92_bodyIdents; - generated = (generated).Then(RAST.Expr.create_Labelled(Dafny.Sequence.UnicodeFromString("TAIL_CALL_START"), RAST.Expr.create_Loop(Std.Wrappers.Option.create_None(), (_83_loopBegin).Then(_91_bodyExpr)))); + RAST._IExpr _87_bodyExpr; + Dafny.ISet> _88_bodyIdents; + Defs._IEnvironment _89_bodyEnv; + RAST._IExpr _out50; + Dafny.ISet> _out51; + Defs._IEnvironment _out52; + (this).GenStmts(_74_body, ((!object.Equals(selfIdent, Defs.SelfInfo.create_NoSelf())) ? (Defs.SelfInfo.create_ThisTyped(Dafny.Sequence.UnicodeFromString("_this"), (selfIdent).dtor_dafnyType)) : (Defs.SelfInfo.create_NoSelf())), newEnv, false, earlyReturn, out _out50, out _out51, out _out52); + _87_bodyExpr = _out50; + _88_bodyIdents = _out51; + _89_bodyEnv = _out52; + readIdents = _88_bodyIdents; + generated = (generated).Then(RAST.Expr.create_Labelled(Dafny.Sequence.UnicodeFromString("TAIL_CALL_START"), RAST.Expr.create_Loop(Std.Wrappers.Option.create_None(), (_79_loopBegin).Then(_87_bodyExpr)))); } goto after_match0; } @@ -2835,44 +2875,44 @@ public void GenStmt(DAST._IStatement stmt, Defs._ISelfInfo selfIdent, Defs._IEnv } { if (_source0.is_Call) { - DAST._IExpression _94_on = _source0.dtor_on; - DAST._ICallName _95_name = _source0.dtor_callName; - Dafny.ISequence _96_typeArgs = _source0.dtor_typeArgs; - Dafny.ISequence _97_args = _source0.dtor_args; - Std.Wrappers._IOption>> _98_maybeOutVars = _source0.dtor_outs; + DAST._IExpression _90_on = _source0.dtor_on; + DAST._ICallName _91_name = _source0.dtor_callName; + Dafny.ISequence _92_typeArgs = _source0.dtor_typeArgs; + Dafny.ISequence _93_args = _source0.dtor_args; + Std.Wrappers._IOption>> _94_maybeOutVars = _source0.dtor_outs; { - RAST._IExpr _out54; - Dafny.ISet> _out55; - (this).GenOwnedCallPart(_94_on, selfIdent, _95_name, _96_typeArgs, _97_args, env, out _out54, out _out55); - generated = _out54; - readIdents = _out55; + RAST._IExpr _out53; + Dafny.ISet> _out54; + (this).GenOwnedCallPart(_90_on, selfIdent, _91_name, _92_typeArgs, _93_args, env, out _out53, out _out54); + generated = _out53; + readIdents = _out54; newEnv = env; - if (((_98_maybeOutVars).is_Some) && ((new BigInteger(((_98_maybeOutVars).dtor_value).Count)) == (BigInteger.One))) { - Dafny.ISequence _99_outVar; - _99_outVar = Defs.__default.escapeVar(((_98_maybeOutVars).dtor_value).Select(BigInteger.Zero)); - if ((env).IsMaybePlacebo(_99_outVar)) { + if (((_94_maybeOutVars).is_Some) && ((new BigInteger(((_94_maybeOutVars).dtor_value).Count)) == (BigInteger.One))) { + Dafny.ISequence _95_outVar; + _95_outVar = Defs.__default.escapeVar(((_94_maybeOutVars).dtor_value).Select(BigInteger.Zero)); + if ((env).IsMaybePlacebo(_95_outVar)) { generated = RAST.__default.MaybePlacebo(generated); } - generated = RAST.__default.AssignVar(_99_outVar, generated); - } else if (((_98_maybeOutVars).is_None) || ((new BigInteger(((_98_maybeOutVars).dtor_value).Count)).Sign == 0)) { + generated = RAST.__default.AssignVar(_95_outVar, generated); + } else if (((_94_maybeOutVars).is_None) || ((new BigInteger(((_94_maybeOutVars).dtor_value).Count)).Sign == 0)) { } else { - Dafny.ISequence _100_tmpVar; - _100_tmpVar = Dafny.Sequence.UnicodeFromString("_x"); - RAST._IExpr _101_tmpId; - _101_tmpId = RAST.Expr.create_Identifier(_100_tmpVar); - generated = RAST.Expr.create_DeclareVar(RAST.DeclareType.create_CONST(), _100_tmpVar, Std.Wrappers.Option.create_None(), Std.Wrappers.Option.create_Some(generated)); - Dafny.ISequence> _102_outVars; - _102_outVars = (_98_maybeOutVars).dtor_value; - BigInteger _hi2 = new BigInteger((_102_outVars).Count); - for (BigInteger _103_outI = BigInteger.Zero; _103_outI < _hi2; _103_outI++) { - Dafny.ISequence _104_outVar; - _104_outVar = Defs.__default.escapeVar((_102_outVars).Select(_103_outI)); - RAST._IExpr _105_rhs; - _105_rhs = (_101_tmpId).Sel(Std.Strings.__default.OfNat(_103_outI)); - if ((env).IsMaybePlacebo(_104_outVar)) { - _105_rhs = RAST.__default.MaybePlacebo(_105_rhs); + Dafny.ISequence _96_tmpVar; + _96_tmpVar = Dafny.Sequence.UnicodeFromString("_x"); + RAST._IExpr _97_tmpId; + _97_tmpId = RAST.Expr.create_Identifier(_96_tmpVar); + generated = RAST.Expr.create_DeclareVar(RAST.DeclareType.create_CONST(), _96_tmpVar, Std.Wrappers.Option.create_None(), Std.Wrappers.Option.create_Some(generated)); + Dafny.ISequence> _98_outVars; + _98_outVars = (_94_maybeOutVars).dtor_value; + BigInteger _hi2 = new BigInteger((_98_outVars).Count); + for (BigInteger _99_outI = BigInteger.Zero; _99_outI < _hi2; _99_outI++) { + Dafny.ISequence _100_outVar; + _100_outVar = Defs.__default.escapeVar((_98_outVars).Select(_99_outI)); + RAST._IExpr _101_rhs; + _101_rhs = (_97_tmpId).Sel(Std.Strings.__default.OfNat(_99_outI)); + if ((env).IsMaybePlacebo(_100_outVar)) { + _101_rhs = RAST.__default.MaybePlacebo(_101_rhs); } - generated = (generated).Then(RAST.__default.AssignVar(_104_outVar, _105_rhs)); + generated = (generated).Then(RAST.__default.AssignVar(_100_outVar, _101_rhs)); } } newEnv = env; @@ -2882,23 +2922,23 @@ public void GenStmt(DAST._IStatement stmt, Defs._ISelfInfo selfIdent, Defs._IEnv } { if (_source0.is_Return) { - DAST._IExpression _106_exprDafny = _source0.dtor_expr; + DAST._IExpression _102_exprDafny = _source0.dtor_expr; { - RAST._IExpr _107_expr; - Defs._IOwnership _108___v54; - Dafny.ISet> _109_recIdents; - RAST._IExpr _out56; - Defs._IOwnership _out57; - Dafny.ISet> _out58; - (this).GenExpr(_106_exprDafny, selfIdent, env, Defs.Ownership.create_OwnershipOwned(), out _out56, out _out57, out _out58); - _107_expr = _out56; - _108___v54 = _out57; - _109_recIdents = _out58; - readIdents = _109_recIdents; + RAST._IExpr _103_expr; + Defs._IOwnership _104___v54; + Dafny.ISet> _105_recIdents; + RAST._IExpr _out55; + Defs._IOwnership _out56; + Dafny.ISet> _out57; + (this).GenExpr(_102_exprDafny, selfIdent, env, Defs.Ownership.create_OwnershipOwned(), out _out55, out _out56, out _out57); + _103_expr = _out55; + _104___v54 = _out56; + _105_recIdents = _out57; + readIdents = _105_recIdents; if (isLast) { - generated = _107_expr; + generated = _103_expr; } else { - generated = RAST.Expr.create_Return(Std.Wrappers.Option.create_Some(_107_expr)); + generated = RAST.Expr.create_Return(Std.Wrappers.Option.create_Some(_103_expr)); } newEnv = env; } @@ -2916,27 +2956,27 @@ public void GenStmt(DAST._IStatement stmt, Defs._ISelfInfo selfIdent, Defs._IEnv } } { - Dafny.ISequence> _110_rustIdents = _source2.dtor_value; - Dafny.ISequence _111_tupleArgs; - _111_tupleArgs = Dafny.Sequence.FromElements(); - BigInteger _hi3 = new BigInteger((_110_rustIdents).Count); - for (BigInteger _112_i = BigInteger.Zero; _112_i < _hi3; _112_i++) { - RAST._IExpr _113_rIdent; - Defs._IOwnership _114___v55; - Dafny.ISet> _115___v56; - RAST._IExpr _out59; - Defs._IOwnership _out60; - Dafny.ISet> _out61; - (this).GenIdent((_110_rustIdents).Select(_112_i), selfIdent, env, Defs.Ownership.create_OwnershipOwned(), out _out59, out _out60, out _out61); - _113_rIdent = _out59; - _114___v55 = _out60; - _115___v56 = _out61; - _111_tupleArgs = Dafny.Sequence.Concat(_111_tupleArgs, Dafny.Sequence.FromElements(_113_rIdent)); + Dafny.ISequence> _106_rustIdents = _source2.dtor_value; + Dafny.ISequence _107_tupleArgs; + _107_tupleArgs = Dafny.Sequence.FromElements(); + BigInteger _hi3 = new BigInteger((_106_rustIdents).Count); + for (BigInteger _108_i = BigInteger.Zero; _108_i < _hi3; _108_i++) { + RAST._IExpr _109_rIdent; + Defs._IOwnership _110___v55; + Dafny.ISet> _111___v56; + RAST._IExpr _out58; + Defs._IOwnership _out59; + Dafny.ISet> _out60; + (this).GenIdent((_106_rustIdents).Select(_108_i), selfIdent, env, Defs.Ownership.create_OwnershipOwned(), out _out58, out _out59, out _out60); + _109_rIdent = _out58; + _110___v55 = _out59; + _111___v56 = _out60; + _107_tupleArgs = Dafny.Sequence.Concat(_107_tupleArgs, Dafny.Sequence.FromElements(_109_rIdent)); } - if ((new BigInteger((_111_tupleArgs).Count)) == (BigInteger.One)) { - generated = RAST.Expr.create_Return(Std.Wrappers.Option.create_Some((_111_tupleArgs).Select(BigInteger.Zero))); + if ((new BigInteger((_107_tupleArgs).Count)) == (BigInteger.One)) { + generated = RAST.Expr.create_Return(Std.Wrappers.Option.create_Some((_107_tupleArgs).Select(BigInteger.Zero))); } else { - generated = RAST.Expr.create_Return(Std.Wrappers.Option.create_Some(RAST.Expr.create_Tuple(_111_tupleArgs))); + generated = RAST.Expr.create_Return(Std.Wrappers.Option.create_Some(RAST.Expr.create_Tuple(_107_tupleArgs))); } } after_match2: ; @@ -2957,20 +2997,20 @@ public void GenStmt(DAST._IStatement stmt, Defs._ISelfInfo selfIdent, Defs._IEnv } } { - DAST._IExpression _116_e = _source0.dtor_Print_a0; + DAST._IExpression _112_e = _source0.dtor_Print_a0; { - RAST._IExpr _117_printedExpr; - Defs._IOwnership _118_recOwnership; - Dafny.ISet> _119_recIdents; - RAST._IExpr _out62; - Defs._IOwnership _out63; - Dafny.ISet> _out64; - (this).GenExpr(_116_e, selfIdent, env, Defs.Ownership.create_OwnershipBorrowed(), out _out62, out _out63, out _out64); - _117_printedExpr = _out62; - _118_recOwnership = _out63; - _119_recIdents = _out64; - 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(_117_printedExpr))); - readIdents = _119_recIdents; + RAST._IExpr _113_printedExpr; + Defs._IOwnership _114_recOwnership; + Dafny.ISet> _115_recIdents; + RAST._IExpr _out61; + Defs._IOwnership _out62; + Dafny.ISet> _out63; + (this).GenExpr(_112_e, selfIdent, env, Defs.Ownership.create_OwnershipBorrowed(), out _out61, out _out62, out _out63); + _113_printedExpr = _out61; + _114_recOwnership = _out62; + _115_recIdents = _out63; + 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(_113_printedExpr))); + readIdents = _115_recIdents; newEnv = env; } } diff --git a/Source/DafnyCore/GeneratedFromDafny/Defs.cs b/Source/DafnyCore/GeneratedFromDafny/Defs.cs index 2e190842a7a..12da1978bd9 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Defs.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Defs.cs @@ -542,60 +542,87 @@ public static RAST._IModDecl PartialOrdImpl(Dafny.ISequence stmts__remainder, Dafny.ISequence dafny__name) { - if ((new BigInteger((stmts__remainder).Count)).Sign == 0) { - return Defs.AssignmentStatus.create_NotAssigned(); - } else { - DAST._IStatement _0_stmt = (stmts__remainder).Select(BigInteger.Zero); - DAST._IStatement _source0 = _0_stmt; + Defs._IAssignmentStatus _hresult = Defs.AssignmentStatus.Default(); + BigInteger _hi0 = new BigInteger((stmts__remainder).Count); + for (BigInteger _0_i = BigInteger.Zero; _0_i < _hi0; _0_i++) { + DAST._IStatement _1_stmt; + _1_stmt = (stmts__remainder).Select(_0_i); + DAST._IStatement _source0 = _1_stmt; { if (_source0.is_Assign) { DAST._IAssignLhs lhs0 = _source0.dtor_lhs; if (lhs0.is_Ident) { - Dafny.ISequence _1_assign__name = lhs0.dtor_ident; - if (object.Equals(_1_assign__name, dafny__name)) { - return Defs.AssignmentStatus.create_SurelyAssigned(); - } else { - return Defs.__default.DetectAssignmentStatus((stmts__remainder).Drop(BigInteger.One), dafny__name); + Dafny.ISequence _2_assign__name = lhs0.dtor_ident; + if (object.Equals(_2_assign__name, dafny__name)) { + _hresult = Defs.AssignmentStatus.create_SurelyAssigned(); + return _hresult; } + goto after_match0; } } } { if (_source0.is_If) { - DAST._IExpression _2_cond = _source0.dtor_cond; - Dafny.ISequence _3_thn = _source0.dtor_thn; - Dafny.ISequence _4_els = _source0.dtor_els; - return (Defs.__default.DetectAssignmentStatus(_3_thn, dafny__name)).Join(Defs.__default.DetectAssignmentStatus(_4_els, dafny__name)); + DAST._IExpression _3_cond = _source0.dtor_cond; + Dafny.ISequence _4_thn = _source0.dtor_thn; + Dafny.ISequence _5_els = _source0.dtor_els; + Defs._IAssignmentStatus _6_rec; + _6_rec = Defs.__default.DetectAssignmentStatus(_4_thn, dafny__name); + if (object.Equals(_6_rec, Defs.AssignmentStatus.create_Unknown())) { + _hresult = Defs.AssignmentStatus.create_Unknown(); + return _hresult; + } + Defs._IAssignmentStatus _7_rec2; + _7_rec2 = Defs.__default.DetectAssignmentStatus(_5_els, dafny__name); + if (object.Equals(_7_rec2, Defs.AssignmentStatus.create_Unknown())) { + _hresult = Defs.AssignmentStatus.create_Unknown(); + return _hresult; + } + if (!object.Equals(_6_rec, _7_rec2)) { + _hresult = Defs.AssignmentStatus.create_Unknown(); + return _hresult; + } + if ((_6_rec).is_SurelyAssigned) { + _hresult = Defs.AssignmentStatus.create_SurelyAssigned(); + return _hresult; + } + goto after_match0; } } { if (_source0.is_Call) { - DAST._IExpression _5_on = _source0.dtor_on; - DAST._ICallName _6_callName = _source0.dtor_callName; - Dafny.ISequence _7_typeArgs = _source0.dtor_typeArgs; - Dafny.ISequence _8_args = _source0.dtor_args; - Std.Wrappers._IOption>> _9_outs = _source0.dtor_outs; - if (((_9_outs).is_Some) && (((_9_outs).dtor_value).Contains(dafny__name))) { - return Defs.AssignmentStatus.create_SurelyAssigned(); - } else { - return Defs.__default.DetectAssignmentStatus((stmts__remainder).Drop(BigInteger.One), dafny__name); + DAST._IExpression _8_on = _source0.dtor_on; + DAST._ICallName _9_callName = _source0.dtor_callName; + Dafny.ISequence _10_typeArgs = _source0.dtor_typeArgs; + Dafny.ISequence _11_args = _source0.dtor_args; + Std.Wrappers._IOption>> _12_outs = _source0.dtor_outs; + if (((_12_outs).is_Some) && (((_12_outs).dtor_value).Contains(dafny__name))) { + _hresult = Defs.AssignmentStatus.create_SurelyAssigned(); + return _hresult; } + goto after_match0; } } { if (_source0.is_Labeled) { - Dafny.ISequence _10_stmts = _source0.dtor_body; - return (Defs.__default.DetectAssignmentStatus(_10_stmts, dafny__name)).Then(Defs.__default.DetectAssignmentStatus((stmts__remainder).Drop(BigInteger.One), dafny__name)); + Dafny.ISequence _13_stmts = _source0.dtor_body; + Defs._IAssignmentStatus _14_rec; + _14_rec = Defs.__default.DetectAssignmentStatus(_13_stmts, dafny__name); + if (!((_14_rec).is_NotAssigned)) { + _hresult = _14_rec; + return _hresult; + } + goto after_match0; } } { if (_source0.is_DeclareVar) { - Dafny.ISequence _11_name = _source0.dtor_name; - if (object.Equals(_11_name, dafny__name)) { - return Defs.AssignmentStatus.create_NotAssigned(); - } else { - return Defs.__default.DetectAssignmentStatus((stmts__remainder).Drop(BigInteger.One), dafny__name); + Dafny.ISequence _15_name = _source0.dtor_name; + if (object.Equals(_15_name, dafny__name)) { + _hresult = Defs.AssignmentStatus.create_NotAssigned(); + return _hresult; } + goto after_match0; } } { @@ -610,18 +637,25 @@ public static Defs._IAssignmentStatus DetectAssignmentStatus(Dafny.ISequence> reserved__rust { get { return Dafny.Set>.FromElements(Dafny.Sequence.UnicodeFromString("as"), Dafny.Sequence.UnicodeFromString("async"), Dafny.Sequence.UnicodeFromString("await"), Dafny.Sequence.UnicodeFromString("break"), Dafny.Sequence.UnicodeFromString("const"), Dafny.Sequence.UnicodeFromString("continue"), Dafny.Sequence.UnicodeFromString("crate"), Dafny.Sequence.UnicodeFromString("dyn"), Dafny.Sequence.UnicodeFromString("else"), Dafny.Sequence.UnicodeFromString("enum"), Dafny.Sequence.UnicodeFromString("extern"), Dafny.Sequence.UnicodeFromString("false"), Dafny.Sequence.UnicodeFromString("fn"), Dafny.Sequence.UnicodeFromString("for"), Dafny.Sequence.UnicodeFromString("if"), Dafny.Sequence.UnicodeFromString("impl"), Dafny.Sequence.UnicodeFromString("in"), Dafny.Sequence.UnicodeFromString("let"), Dafny.Sequence.UnicodeFromString("loop"), Dafny.Sequence.UnicodeFromString("match"), Dafny.Sequence.UnicodeFromString("mod"), Dafny.Sequence.UnicodeFromString("move"), Dafny.Sequence.UnicodeFromString("mut"), Dafny.Sequence.UnicodeFromString("pub"), Dafny.Sequence.UnicodeFromString("ref"), Dafny.Sequence.UnicodeFromString("return"), Dafny.Sequence.UnicodeFromString("static"), Dafny.Sequence.UnicodeFromString("struct"), Dafny.Sequence.UnicodeFromString("super"), Dafny.Sequence.UnicodeFromString("trait"), Dafny.Sequence.UnicodeFromString("true"), Dafny.Sequence.UnicodeFromString("type"), Dafny.Sequence.UnicodeFromString("union"), Dafny.Sequence.UnicodeFromString("unsafe"), Dafny.Sequence.UnicodeFromString("use"), Dafny.Sequence.UnicodeFromString("where"), Dafny.Sequence.UnicodeFromString("while"), Dafny.Sequence.UnicodeFromString("Keywords"), Dafny.Sequence.UnicodeFromString("The"), Dafny.Sequence.UnicodeFromString("abstract"), Dafny.Sequence.UnicodeFromString("become"), Dafny.Sequence.UnicodeFromString("box"), Dafny.Sequence.UnicodeFromString("do"), Dafny.Sequence.UnicodeFromString("final"), Dafny.Sequence.UnicodeFromString("macro"), Dafny.Sequence.UnicodeFromString("override"), Dafny.Sequence.UnicodeFromString("priv"), Dafny.Sequence.UnicodeFromString("try"), Dafny.Sequence.UnicodeFromString("typeof"), Dafny.Sequence.UnicodeFromString("unsized"), Dafny.Sequence.UnicodeFromString("virtual"), Dafny.Sequence.UnicodeFromString("yield")); diff --git a/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs b/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs index c2a8b8162a1..bd28edcf2ae 100644 --- a/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs +++ b/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs @@ -76,6 +76,23 @@ assert x !is B.>< Assert.Empty(completionList); } + [Fact] + public async Task TestInsertion() { + await TestCodeAction(@" +datatype L = N | C(t: L) + +method Dec(c: L) + decreases c, 1, 1 +{(>Insert explicit failing assertion-> + assert (old(c), old(1) decreases to c, 1);<) + Da> Handle(CodeActionParams var ideState = await projectManager.GetStateAfterResolutionAsync(); var quickFixers = GetDafnyCodeActionProviders(); var fixesWithId = GetFixesWithIds(quickFixers, ideState, request).ToArray(); - - documentUriToDafnyCodeActions.AddOrUpdate(uri.ToString(), _ => fixesWithId, (_, _) => fixesWithId); + var key = uri.ToString(); + documentUriToDafnyCodeActions.AddOrUpdate(key, _ => fixesWithId, (_, _) => fixesWithId); var codeActions = fixesWithId.Select(fixWithId => { CommandOrCodeAction t = new CodeAction { Title = fixWithId.DafnyCodeAction.Title, - Data = new JArray(uri, fixWithId.Id), + Data = new JArray(key, fixWithId.Id), Diagnostics = fixWithId.DafnyCodeAction.Diagnostics, Kind = CodeActionKind.QuickFix }; diff --git a/Source/DafnyLanguageServer/Language/ImplicitFailingAssertionCodeActionProvider.cs b/Source/DafnyLanguageServer/Language/ImplicitFailingAssertionCodeActionProvider.cs index 1f43f7c8b68..998da220765 100644 --- a/Source/DafnyLanguageServer/Language/ImplicitFailingAssertionCodeActionProvider.cs +++ b/Source/DafnyLanguageServer/Language/ImplicitFailingAssertionCodeActionProvider.cs @@ -72,7 +72,8 @@ public override IEnumerable GetEdits() { var node = nodesTillFailure[i]; var nextNode = i < nodesTillFailure.Count - 1 ? nodesTillFailure[i + 1] : null; if (node is Statement or LetExpr && - node is not AssignStatement && nextNode is not VarDeclStmt && nextNode is not AssignSuchThatStmt) { + ((node is AssignStatement or AssignSuchThatStmt && nextNode is not VarDeclStmt) || + (node is not AssignStatement && nextNode is not VarDeclStmt && nextNode is not AssignSuchThatStmt))) { insertionNode = node; break; }