diff --git a/Source/DafnyCore/Backends/Dafny/AST.dfy b/Source/DafnyCore/Backends/Dafny/AST.dfy index ff7fa674b28..85e163c2fad 100644 --- a/Source/DafnyCore/Backends/Dafny/AST.dfy +++ b/Source/DafnyCore/Backends/Dafny/AST.dfy @@ -200,7 +200,7 @@ module {:extern "DAST"} DAST { datatype ClassItem = Method(Method) - datatype Field = Field(formal: Formal, defaultValue: Option) + datatype Field = Field(formal: Formal, isConstant: bool, defaultValue: Option) datatype Formal = Formal(name: VarName, typ: Type, attributes: seq) @@ -239,13 +239,13 @@ module {:extern "DAST"} DAST { JumpTailCallStart() | Halt() | Print(Expression) | - ConstructorNewSeparator(fields: seq) + ConstructorNewSeparator(fields: seq) { } datatype AssignLhs = Ident(ident: VarName) | - Select(expr: Expression, field: VarName) | + Select(expr: Expression, field: VarName, isConstant: bool) | Index(expr: Expression, indices: seq) datatype CollKind = Seq | Array | Map diff --git a/Source/DafnyCore/Backends/Dafny/ASTBuilder.cs b/Source/DafnyCore/Backends/Dafny/ASTBuilder.cs index e00b0adaa52..aa6e8068dba 100644 --- a/Source/DafnyCore/Backends/Dafny/ASTBuilder.cs +++ b/Source/DafnyCore/Backends/Dafny/ASTBuilder.cs @@ -133,8 +133,8 @@ public void AddMethod(DAST.Method item) { body.Add(item); } - public void AddField(DAST.Formal item, _IOption defaultValue) { - fields.Add((DAST.Field)DAST.Field.create_Field(item, defaultValue)); + public void AddField(DAST.Formal item, bool isConstant, _IOption defaultValue) { + fields.Add((DAST.Field)DAST.Field.create_Field(item, isConstant, defaultValue)); } public object Finish() { @@ -187,7 +187,7 @@ public void AddMethod(DAST.Method item) { body.Add(item); } - public void AddField(DAST.Formal item, _IOption defaultValue) { + public void AddField(DAST.Formal item, bool isConstant, _IOption defaultValue) { throw new UnsupportedFeatureException(Token.NoToken, Feature.RunAllTests); } @@ -243,7 +243,7 @@ public void AddMethod(DAST.Method item) { throw new UnsupportedFeatureException(Token.NoToken, Feature.RunAllTests); } - public void AddField(DAST.Formal item, _IOption defaultValue) { + public void AddField(DAST.Formal item, bool isConstant, _IOption defaultValue) { throw new UnsupportedFeatureException(Token.NoToken, Feature.RunAllTests); } @@ -343,7 +343,7 @@ public void AddMethod(DAST.Method item) { body.Add(item); } - public void AddField(DAST.Formal item, _IOption defaultValue) { + public void AddField(DAST.Formal item, bool isConstant, _IOption defaultValue) { throw new UnsupportedFeatureException(Token.NoToken, Feature.RunAllTests); } @@ -363,7 +363,7 @@ public object Finish() { interface ClassLike { void AddMethod(DAST.Method item); - void AddField(DAST.Formal item, _IOption defaultValue); + void AddField(DAST.Formal item, bool isConstant, _IOption defaultValue); public MethodBuilder Method(bool isStatic, bool hasBody, bool outVarsAreUninitFieldsToAssign, bool wasFunction, ISequence> overridingPath, diff --git a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs index dee5a1c26f3..7aaddb93e69 100644 --- a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs @@ -482,17 +482,21 @@ protected override void TrDividedBlockStmt(Constructor m, DividedBlockStmt divid if (writer is BuilderSyntaxTree builder) { var membersToInitialize = ((TopLevelDeclWithMembers)m.EnclosingClass).Members.Where((md => md is Field and not ConstantField { Rhs: { } })); - var outFormals = membersToInitialize.Select((MemberDecl md) => - DAST.Formal.create_Formal( - Sequence.UnicodeFromString( - (md is ConstantField ? InternalFieldPrefix : "") + - md.GetCompileName(Options)), - GenType(((Field)md).Type.Subst(((TopLevelDeclWithMembers)((Field)md).EnclosingClass).ParentFormalTypeParametersToActuals)) - , ParseAttributes(md.Attributes) - ) + var outFields = membersToInitialize.Select((MemberDecl md) => { + var formal = DAST.Formal.create_Formal( + Sequence.UnicodeFromString( + (md is ConstantField ? InternalFieldPrefix : "") + + md.GetCompileName(Options)), + GenType(((Field)md).Type.Subst(((TopLevelDeclWithMembers)((Field)md).EnclosingClass) + .ParentFormalTypeParametersToActuals)) + , ParseAttributes(md.Attributes) + ); + return DAST.Field.create_Field(formal, md is ConstantField, + Std.Wrappers.Option.create_None()); + } ).ToList(); builder.Builder.AddStatement((DAST.Statement)DAST.Statement.create_ConstructorNewSeparator( - Sequence<_IFormal>.FromArray(outFormals.ToArray()))); + Sequence<_IField>.FromArray(outFields.ToArray()))); } else { throw new InvalidCastException("Divided block statement outside of a statement container"); } @@ -669,7 +673,7 @@ public void DeclareField(string name, TopLevelDecl enclosingDecl, bool isStatic, Sequence.UnicodeFromString(name), compiler.GenType(type), compiler.ParseAttributes(field.Attributes) - ), rhsExpr); + ), isConst, rhsExpr); } public void InitializeField(Field field, Type instantiatedFieldType, TopLevelDeclWithMembers enclosingClass) { @@ -1929,7 +1933,8 @@ protected override ILvalue EmitMemberSelect(Action obj, Type member.EnclosingClass is DatatypeDecl, GenType(expectedType) ), (DAST.AssignLhs)DAST.AssignLhs.create_Select( objExpr, - Sequence.UnicodeFromString(member.GetCompileName(Options)) + Sequence.UnicodeFromString(member.GetCompileName(Options)), + member is ConstantField ), this); } } else if (member is SpecialField { SpecialId: SpecialField.ID.ArrayLength } arraySpecial) { @@ -1973,7 +1978,8 @@ protected override ILvalue EmitMemberSelect(Action obj, Type member.EnclosingClass is DatatypeDecl, GenType(expectedType) ), (DAST.AssignLhs)DAST.AssignLhs.create_Select( objExpr, - Sequence.UnicodeFromString(compiledName) + Sequence.UnicodeFromString(compiledName), + member is ConstantField ), this); } else if (member is SpecialField sf2 && sf2.SpecialId == SpecialField.ID.UseIdParam && sf2.IdParam is string fieldName && fieldName.StartsWith("is_")) { obj(new BuilderSyntaxTree(objReceiver, this)); @@ -2005,7 +2011,8 @@ protected override ILvalue EmitMemberSelect(Action obj, Type member.EnclosingClass is DatatypeDecl, GenType(expectedType) ), (DAST.AssignLhs)DAST.AssignLhs.create_Select( objExpr, - Sequence.UnicodeFromString(InternalFieldPrefix + member.GetCompileName(Options)) + Sequence.UnicodeFromString(InternalFieldPrefix + member.GetCompileName(Options)), + member is ConstantField ), this); } else { return new ExprLvalue((DAST.Expression)DAST.Expression.create_Select( @@ -2015,7 +2022,8 @@ protected override ILvalue EmitMemberSelect(Action obj, Type member.EnclosingClass is DatatypeDecl, GenType(expectedType) ), (DAST.AssignLhs)DAST.AssignLhs.create_Select( objExpr, - Sequence.UnicodeFromString(member.GetCompileName(Options)) + Sequence.UnicodeFromString(member.GetCompileName(Options)), + member is ConstantField ), this); } } diff --git a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy index 4a78198fb53..9cd6c8a7c9e 100644 --- a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy +++ b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy @@ -30,18 +30,25 @@ module {:extern "DCOMP"} DafnyToRustCompiler { const allocate_fn := "_" + allocate const update_field_uninit_macro := if pointerType.Raw? then "update_field_uninit!" else "update_field_uninit_object!" + const update_field_mut_uninit_macro := + if pointerType.Raw? then "update_field_mut_uninit!" else "update_field_mut_uninit_object!" const thisInConstructor := if pointerType.Raw? then R.Identifier("this") else R.Identifier("this").Clone() const array_construct := if pointerType.Raw? then "construct" else "construct_object" const modify_macro := R.dafny_runtime.MSel(if pointerType.Raw? then "modify!" else "md!").AsExpr() const read_macro := R.dafny_runtime.MSel(if pointerType.Raw? then "read!" else "rd!").AsExpr() + const modify_field_macro := R.dafny_runtime.MSel("modify_field!").AsExpr() + const read_field_macro := R.dafny_runtime.MSel("read_field!").AsExpr() + function Object(underlying: R.Type): R.Type { if pointerType.Raw? then R.PtrType(underlying) else R.ObjectType(underlying) } const placebos_usize := if pointerType.Raw? then "placebos_usize" else "placebos_usize_object" const update_field_if_uninit_macro := if pointerType.Raw? then "update_field_if_uninit!" else "update_field_if_uninit_object!" + const update_field_mut_if_uninit_macro := + if pointerType.Raw? then "update_field_mut_if_uninit!" else "update_field_mut_if_uninit_object!" const Upcast := if pointerType.Raw? then "Upcast" else "UpcastObject" const UpcastFnMacro := @@ -207,6 +214,9 @@ module {:extern "DCOMP"} DafnyToRustCompiler { for fieldI := 0 to |c.fields| { var field := c.fields[fieldI]; var fieldType := GenType(field.formal.typ, GenTypeContext.default()); + if !field.isConstant { + fieldType := R.dafny_runtime.MSel("Field").AsType().Apply([fieldType]); + } usedTypeParams := GatherTypeParamNames(usedTypeParams, fieldType); var fieldRustName := escapeVar(field.formal.name); fields := fields + [R.Field(R.PUB, R.Formal(fieldRustName, fieldType))]; @@ -1392,7 +1402,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler { case _ => enclosingType }; if (forTrait) { - var selfFormal := if m.wasFunction then R.Formal.selfBorrowed else R.Formal.selfBorrowedMut; + var selfFormal := R.Formal.selfBorrowed; params := [selfFormal] + params; } else { var tpe := GenType(instanceType, GenTypeContext.default()); @@ -1403,11 +1413,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler { // For raw pointers, no borrowing is necessary, because it implements the Copy type } else if selfId == "self" { if tpe.IsObjectOrPointer() { // For classes and traits - if m.wasFunction { - tpe := R.SelfBorrowed; - } else { - tpe := R.SelfBorrowedMut; - } + tpe := R.SelfBorrowed; } else { // For Rc-defined datatypes if enclosingType.UserDefined? && enclosingType.resolved.kind.Datatype? && IsRcWrapped(enclosingType.resolved.attributes) { @@ -1584,7 +1590,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler { needsIIFE := false; } - case Select(on, field) => { + case Select(on, field, isConstant) => { var fieldName := escapeVar(field); var onExpr, onOwned, recIdents := GenExpr(on, selfIdent, env, OwnershipAutoBorrowed); @@ -1594,7 +1600,12 @@ module {:extern "DCOMP"} DafnyToRustCompiler { | UnaryOp("&", Identifier("this"), _) => var isAssignedVar := AddAssignedPrefix(fieldName); if isAssignedVar in newEnv.names { - generated := R.dafny_runtime.MSel(update_field_uninit_macro).AsExpr().Apply( + var update_field_uninit := + if isConstant then + update_field_uninit_macro + else + update_field_mut_uninit_macro; + generated := R.dafny_runtime.MSel(update_field_uninit).AsExpr().Apply( [ thisInConstructor, R.Identifier(fieldName), R.Identifier(isAssignedVar), @@ -1602,14 +1613,13 @@ module {:extern "DCOMP"} DafnyToRustCompiler { newEnv := newEnv.RemoveAssigned(isAssignedVar); } else { // Already assigned, safe to override - generated := R.Assign(Some(R.SelectMember(modify_macro.Apply1(thisInConstructor), fieldName)), rhs); + generated := modify_field_macro.Apply([read_macro.Apply1(thisInConstructor).Sel(fieldName), rhs]); } case _ => if onExpr != R.Identifier("self") { - onExpr := modify_macro.Apply1(onExpr); + onExpr := read_macro.Apply1(onExpr); } - generated := - R.AssignMember(onExpr, fieldName, rhs); + generated := modify_field_macro.Apply([onExpr.Sel(fieldName), rhs]); } readIdents := recIdents; needsIIFE := false; @@ -1658,15 +1668,17 @@ module {:extern "DCOMP"} DafnyToRustCompiler { newEnv := env; for i := 0 to |fields| { var field := fields[i]; - var fieldName := escapeVar(field.name); - var fieldTyp := GenType(field.typ, GenTypeContext.default()); + var fieldName := escapeVar(field.formal.name); + var fieldTyp := GenType(field.formal.typ, GenTypeContext.default()); var isAssignedVar := AddAssignedPrefix(fieldName); if isAssignedVar in newEnv.names { - assume {:axiom} InitializationValue(field.typ) < stmt; // Needed for termination - var rhs, _, _ := GenExpr(InitializationValue(field.typ), selfIdent, env, OwnershipOwned); + assume {:axiom} InitializationValue(field.formal.typ) < stmt; // Needed for termination + var rhs, _, _ := GenExpr(InitializationValue(field.formal.typ), selfIdent, env, OwnershipOwned); readIdents := readIdents + {isAssignedVar}; - generated := generated.Then(R.dafny_runtime.MSel(update_field_if_uninit_macro).AsExpr().Apply([ - R.Identifier("this"), R.Identifier(fieldName), R.Identifier(isAssignedVar), rhs])); + var update_if_uninit := + if field.isConstant then update_field_if_uninit_macro else update_field_mut_if_uninit_macro; + generated := generated.Then(R.dafny_runtime.MSel(update_if_uninit).AsExpr().Apply( + [ R.Identifier("this"), R.Identifier(fieldName), R.Identifier(isAssignedVar), rhs])); newEnv := newEnv.RemoveAssigned(isAssignedVar); } } @@ -1855,7 +1867,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler { case CallName(_, Some(tpe), _, _, _) => var typ := GenType(tpe, GenTypeContext.default()); if typ.IsObjectOrPointer() && onExpr != R.Identifier("self") { - onExpr := modify_macro.Apply1(onExpr); + onExpr := read_macro.Apply1(onExpr); } case _ => } @@ -3288,8 +3300,10 @@ module {:extern "DCOMP"} DafnyToRustCompiler { r := r.Sel(escapeVar(field)); if isConstant { r := r.Apply0(); + r := r.Clone(); // self could be &mut, so to avoid any borrow checker problem, we clone the value. + } else { + r := read_field_macro.Apply1(r); // Already contains a clone. } - r := r.Clone(); // self could be &mut, so to avoid any borrow checker problem, we clone the value. r, resultingOwnership := FromOwned(r, expectedOwnership); readIdents := recIdents; } diff --git a/Source/DafnyCore/GeneratedFromDafny/DAST.cs b/Source/DafnyCore/GeneratedFromDafny/DAST.cs index 1179a0a0174..50b364d3c50 100644 --- a/Source/DafnyCore/GeneratedFromDafny/DAST.cs +++ b/Source/DafnyCore/GeneratedFromDafny/DAST.cs @@ -3390,28 +3390,32 @@ public DAST._IMethod dtor_Method_a0 { public interface _IField { bool is_Field { get; } DAST._IFormal dtor_formal { get; } + bool dtor_isConstant { get; } Std.Wrappers._IOption dtor_defaultValue { get; } _IField DowncastClone(); } public class Field : _IField { public readonly DAST._IFormal _formal; + public readonly bool _isConstant; public readonly Std.Wrappers._IOption _defaultValue; - public Field(DAST._IFormal formal, Std.Wrappers._IOption defaultValue) { + public Field(DAST._IFormal formal, bool isConstant, Std.Wrappers._IOption defaultValue) { this._formal = formal; + this._isConstant = isConstant; this._defaultValue = defaultValue; } public _IField DowncastClone() { if (this is _IField dt) { return dt; } - return new Field(_formal, _defaultValue); + return new Field(_formal, _isConstant, _defaultValue); } public override bool Equals(object other) { var oth = other as DAST.Field; - return oth != null && object.Equals(this._formal, oth._formal) && object.Equals(this._defaultValue, oth._defaultValue); + return oth != null && object.Equals(this._formal, oth._formal) && this._isConstant == oth._isConstant && object.Equals(this._defaultValue, oth._defaultValue); } public override int GetHashCode() { ulong hash = 5381; hash = ((hash << 5) + hash) + 0; hash = ((hash << 5) + hash) + ((ulong)Dafny.Helpers.GetHashCode(this._formal)); + hash = ((hash << 5) + hash) + ((ulong)Dafny.Helpers.GetHashCode(this._isConstant)); hash = ((hash << 5) + hash) + ((ulong)Dafny.Helpers.GetHashCode(this._defaultValue)); return (int) hash; } @@ -3420,11 +3424,13 @@ public override string ToString() { s += "("; s += Dafny.Helpers.ToString(this._formal); s += ", "; + s += Dafny.Helpers.ToString(this._isConstant); + s += ", "; s += Dafny.Helpers.ToString(this._defaultValue); s += ")"; return s; } - private static readonly DAST._IField theDefault = create(DAST.Formal.Default(), Std.Wrappers.Option.Default()); + private static readonly DAST._IField theDefault = create(DAST.Formal.Default(), false, Std.Wrappers.Option.Default()); public static DAST._IField Default() { return theDefault; } @@ -3432,11 +3438,11 @@ public static DAST._IField Default() { public static Dafny.TypeDescriptor _TypeDescriptor() { return _TYPE; } - public static _IField create(DAST._IFormal formal, Std.Wrappers._IOption defaultValue) { - return new Field(formal, defaultValue); + public static _IField create(DAST._IFormal formal, bool isConstant, Std.Wrappers._IOption defaultValue) { + return new Field(formal, isConstant, defaultValue); } - public static _IField create_Field(DAST._IFormal formal, Std.Wrappers._IOption defaultValue) { - return create(formal, defaultValue); + public static _IField create_Field(DAST._IFormal formal, bool isConstant, Std.Wrappers._IOption defaultValue) { + return create(formal, isConstant, defaultValue); } public bool is_Field { get { return true; } } public DAST._IFormal dtor_formal { @@ -3444,6 +3450,11 @@ public DAST._IFormal dtor_formal { return this._formal; } } + public bool dtor_isConstant { + get { + return this._isConstant; + } + } public Std.Wrappers._IOption dtor_defaultValue { get { return this._defaultValue; @@ -3996,7 +4007,7 @@ public interface _IStatement { DAST._IExpression dtor_expr { get; } Std.Wrappers._IOption> dtor_toLabel { get; } DAST._IExpression dtor_Print_a0 { get; } - Dafny.ISequence dtor_fields { get; } + Dafny.ISequence dtor_fields { get; } _IStatement DowncastClone(); } public abstract class Statement : _IStatement { @@ -4052,7 +4063,7 @@ public static _IStatement create_Halt() { public static _IStatement create_Print(DAST._IExpression _a0) { return new Statement_Print(_a0); } - public static _IStatement create_ConstructorNewSeparator(Dafny.ISequence fields) { + public static _IStatement create_ConstructorNewSeparator(Dafny.ISequence fields) { return new Statement_ConstructorNewSeparator(fields); } public bool is_DeclareVar { get { return this is Statement_DeclareVar; } } @@ -4200,7 +4211,7 @@ public DAST._IExpression dtor_Print_a0 { return ((Statement_Print)d)._a0; } } - public Dafny.ISequence dtor_fields { + public Dafny.ISequence dtor_fields { get { var d = this; return ((Statement_ConstructorNewSeparator)d)._fields; @@ -4639,8 +4650,8 @@ public override string ToString() { } } public class Statement_ConstructorNewSeparator : Statement { - public readonly Dafny.ISequence _fields; - public Statement_ConstructorNewSeparator(Dafny.ISequence fields) : base() { + public readonly Dafny.ISequence _fields; + public Statement_ConstructorNewSeparator(Dafny.ISequence fields) : base() { this._fields = fields; } public override _IStatement DowncastClone() { @@ -4673,6 +4684,7 @@ public interface _IAssignLhs { Dafny.ISequence dtor_ident { get; } DAST._IExpression dtor_expr { get; } Dafny.ISequence dtor_field { get; } + bool dtor_isConstant { get; } Dafny.ISequence dtor_indices { get; } _IAssignLhs DowncastClone(); } @@ -4690,8 +4702,8 @@ public static DAST._IAssignLhs Default() { public static _IAssignLhs create_Ident(Dafny.ISequence ident) { return new AssignLhs_Ident(ident); } - public static _IAssignLhs create_Select(DAST._IExpression expr, Dafny.ISequence field) { - return new AssignLhs_Select(expr, field); + public static _IAssignLhs create_Select(DAST._IExpression expr, Dafny.ISequence field, bool isConstant) { + return new AssignLhs_Select(expr, field, isConstant); } public static _IAssignLhs create_Index(DAST._IExpression expr, Dafny.ISequence indices) { return new AssignLhs_Index(expr, indices); @@ -4718,6 +4730,12 @@ public Dafny.ISequence dtor_field { return ((AssignLhs_Select)d)._field; } } + public bool dtor_isConstant { + get { + var d = this; + return ((AssignLhs_Select)d)._isConstant; + } + } public Dafny.ISequence dtor_indices { get { var d = this; @@ -4756,23 +4774,26 @@ public override string ToString() { public class AssignLhs_Select : AssignLhs { public readonly DAST._IExpression _expr; public readonly Dafny.ISequence _field; - public AssignLhs_Select(DAST._IExpression expr, Dafny.ISequence field) : base() { + public readonly bool _isConstant; + public AssignLhs_Select(DAST._IExpression expr, Dafny.ISequence field, bool isConstant) : base() { this._expr = expr; this._field = field; + this._isConstant = isConstant; } public override _IAssignLhs DowncastClone() { if (this is _IAssignLhs dt) { return dt; } - return new AssignLhs_Select(_expr, _field); + return new AssignLhs_Select(_expr, _field, _isConstant); } public override bool Equals(object other) { var oth = other as DAST.AssignLhs_Select; - return oth != null && object.Equals(this._expr, oth._expr) && object.Equals(this._field, oth._field); + return oth != null && object.Equals(this._expr, oth._expr) && object.Equals(this._field, oth._field) && this._isConstant == oth._isConstant; } public override int GetHashCode() { ulong hash = 5381; hash = ((hash << 5) + hash) + 1; hash = ((hash << 5) + hash) + ((ulong)Dafny.Helpers.GetHashCode(this._expr)); hash = ((hash << 5) + hash) + ((ulong)Dafny.Helpers.GetHashCode(this._field)); + hash = ((hash << 5) + hash) + ((ulong)Dafny.Helpers.GetHashCode(this._isConstant)); return (int) hash; } public override string ToString() { @@ -4781,6 +4802,8 @@ public override string ToString() { s += Dafny.Helpers.ToString(this._expr); s += ", "; s += Dafny.Helpers.ToString(this._field); + s += ", "; + s += Dafny.Helpers.ToString(this._isConstant); s += ")"; return s; } diff --git a/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs b/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs index d4a7ebe0d61..b3cf7a3e6f0 100644 --- a/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs +++ b/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs @@ -249,6 +249,9 @@ public bool IsSameResolvedType(DAST._IResolvedType r1, DAST._IResolvedType r2) RAST._IType _out4; _out4 = (this).GenType(((_9_field).dtor_formal).dtor_typ, Defs.GenTypeContext.@default()); _10_fieldType = _out4; + if (!((_9_field).dtor_isConstant)) { + _10_fieldType = (((RAST.__default.dafny__runtime).MSel(Dafny.Sequence.UnicodeFromString("Field"))).AsType()).Apply(Dafny.Sequence.FromElements(_10_fieldType)); + } _7_usedTypeParams = (this).GatherTypeParamNames(_7_usedTypeParams, _10_fieldType); Dafny.ISequence _11_fieldRustName; _11_fieldRustName = Defs.__default.escapeVar(((_9_field).dtor_formal).dtor_name); @@ -1674,11 +1677,7 @@ public RAST._IImplMember GenMethod(DAST._IMethod m, bool forTrait, DAST._IType e after_match0: ; if (forTrait) { RAST._IFormal _14_selfFormal; - if ((m).dtor_wasFunction) { - _14_selfFormal = RAST.Formal.selfBorrowed; - } else { - _14_selfFormal = RAST.Formal.selfBorrowedMut; - } + _14_selfFormal = RAST.Formal.selfBorrowed; _0_params = Dafny.Sequence.Concat(Dafny.Sequence.FromElements(_14_selfFormal), _0_params); } else { RAST._IType _15_tpe; @@ -1691,11 +1690,7 @@ public RAST._IImplMember GenMethod(DAST._IMethod m, bool forTrait, DAST._IType e } } else if ((_9_selfId).Equals(Dafny.Sequence.UnicodeFromString("self"))) { if ((_15_tpe).IsObjectOrPointer()) { - if ((m).dtor_wasFunction) { - _15_tpe = RAST.__default.SelfBorrowed; - } else { - _15_tpe = RAST.__default.SelfBorrowedMut; - } + _15_tpe = RAST.__default.SelfBorrowed; } else { if ((((enclosingType).is_UserDefined) && ((((enclosingType).dtor_resolved).dtor_kind).is_Datatype)) && ((this).IsRcWrapped(((enclosingType).dtor_resolved).dtor_attributes))) { _15_tpe = RAST.Type.create_Borrowed(RAST.__default.Rc(RAST.__default.SelfOwned)); @@ -1949,20 +1944,21 @@ public void GenAssignLhs(DAST._IAssignLhs lhs, RAST._IExpr rhs, Defs._ISelfInfo if (_source0.is_Select) { DAST._IExpression _2_on = _source0.dtor_expr; Dafny.ISequence _3_field = _source0.dtor_field; + bool _4_isConstant = _source0.dtor_isConstant; { - Dafny.ISequence _4_fieldName; - _4_fieldName = Defs.__default.escapeVar(_3_field); - RAST._IExpr _5_onExpr; - Defs._IOwnership _6_onOwned; - Dafny.ISet> _7_recIdents; + Dafny.ISequence _5_fieldName; + _5_fieldName = Defs.__default.escapeVar(_3_field); + RAST._IExpr _6_onExpr; + Defs._IOwnership _7_onOwned; + Dafny.ISet> _8_recIdents; RAST._IExpr _out0; Defs._IOwnership _out1; Dafny.ISet> _out2; (this).GenExpr(_2_on, selfIdent, env, Defs.Ownership.create_OwnershipAutoBorrowed(), out _out0, out _out1, out _out2); - _5_onExpr = _out0; - _6_onOwned = _out1; - _7_recIdents = _out2; - RAST._IExpr _source1 = _5_onExpr; + _6_onExpr = _out0; + _7_onOwned = _out1; + _8_recIdents = _out2; + RAST._IExpr _source1 = _6_onExpr; { bool disjunctiveMatch0 = false; if (_source1.is_Call) { @@ -1999,72 +1995,78 @@ public void GenAssignLhs(DAST._IAssignLhs lhs, RAST._IExpr rhs, Defs._ISelfInfo } } if (disjunctiveMatch0) { - Dafny.ISequence _8_isAssignedVar; - _8_isAssignedVar = Defs.__default.AddAssignedPrefix(_4_fieldName); - if (((newEnv).dtor_names).Contains(_8_isAssignedVar)) { - generated = (((RAST.__default.dafny__runtime).MSel((this).update__field__uninit__macro)).AsExpr()).Apply(Dafny.Sequence.FromElements((this).thisInConstructor, RAST.Expr.create_Identifier(_4_fieldName), RAST.Expr.create_Identifier(_8_isAssignedVar), rhs)); - newEnv = (newEnv).RemoveAssigned(_8_isAssignedVar); + Dafny.ISequence _9_isAssignedVar; + _9_isAssignedVar = Defs.__default.AddAssignedPrefix(_5_fieldName); + if (((newEnv).dtor_names).Contains(_9_isAssignedVar)) { + Dafny.ISequence _10_update__field__uninit; + if (_4_isConstant) { + _10_update__field__uninit = (this).update__field__uninit__macro; + } else { + _10_update__field__uninit = (this).update__field__mut__uninit__macro; + } + generated = (((RAST.__default.dafny__runtime).MSel(_10_update__field__uninit)).AsExpr()).Apply(Dafny.Sequence.FromElements((this).thisInConstructor, RAST.Expr.create_Identifier(_5_fieldName), RAST.Expr.create_Identifier(_9_isAssignedVar), rhs)); + newEnv = (newEnv).RemoveAssigned(_9_isAssignedVar); } else { - generated = RAST.Expr.create_Assign(Std.Wrappers.Option.create_Some(RAST.AssignLhs.create_SelectMember(((this).modify__macro).Apply1((this).thisInConstructor), _4_fieldName)), rhs); + generated = ((this).modify__field__macro).Apply(Dafny.Sequence.FromElements((((this).read__macro).Apply1((this).thisInConstructor)).Sel(_5_fieldName), rhs)); } goto after_match1; } } { - if (!object.Equals(_5_onExpr, RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("self")))) { - _5_onExpr = ((this).modify__macro).Apply1(_5_onExpr); + if (!object.Equals(_6_onExpr, RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("self")))) { + _6_onExpr = ((this).read__macro).Apply1(_6_onExpr); } - generated = RAST.__default.AssignMember(_5_onExpr, _4_fieldName, rhs); + generated = ((this).modify__field__macro).Apply(Dafny.Sequence.FromElements((_6_onExpr).Sel(_5_fieldName), rhs)); } after_match1: ; - readIdents = _7_recIdents; + readIdents = _8_recIdents; needsIIFE = false; } goto after_match0; } } { - DAST._IExpression _9_on = _source0.dtor_expr; - Dafny.ISequence _10_indices = _source0.dtor_indices; + DAST._IExpression _11_on = _source0.dtor_expr; + Dafny.ISequence _12_indices = _source0.dtor_indices; { - RAST._IExpr _11_onExpr; - Defs._IOwnership _12_onOwned; - Dafny.ISet> _13_recIdents; + RAST._IExpr _13_onExpr; + Defs._IOwnership _14_onOwned; + Dafny.ISet> _15_recIdents; RAST._IExpr _out3; Defs._IOwnership _out4; Dafny.ISet> _out5; - (this).GenExpr(_9_on, selfIdent, env, Defs.Ownership.create_OwnershipAutoBorrowed(), out _out3, out _out4, out _out5); - _11_onExpr = _out3; - _12_onOwned = _out4; - _13_recIdents = _out5; - readIdents = _13_recIdents; - _11_onExpr = ((this).modify__macro).Apply1(_11_onExpr); - RAST._IExpr _14_r; - _14_r = (this).InitEmptyExpr(); - Dafny.ISequence _15_indicesExpr; - _15_indicesExpr = Dafny.Sequence.FromElements(); - BigInteger _hi0 = new BigInteger((_10_indices).Count); - for (BigInteger _16_i = BigInteger.Zero; _16_i < _hi0; _16_i++) { - RAST._IExpr _17_idx; - Defs._IOwnership _18___v30; - Dafny.ISet> _19_recIdentsIdx; + (this).GenExpr(_11_on, selfIdent, env, Defs.Ownership.create_OwnershipAutoBorrowed(), out _out3, out _out4, out _out5); + _13_onExpr = _out3; + _14_onOwned = _out4; + _15_recIdents = _out5; + readIdents = _15_recIdents; + _13_onExpr = ((this).modify__macro).Apply1(_13_onExpr); + RAST._IExpr _16_r; + _16_r = (this).InitEmptyExpr(); + Dafny.ISequence _17_indicesExpr; + _17_indicesExpr = Dafny.Sequence.FromElements(); + BigInteger _hi0 = new BigInteger((_12_indices).Count); + for (BigInteger _18_i = BigInteger.Zero; _18_i < _hi0; _18_i++) { + RAST._IExpr _19_idx; + Defs._IOwnership _20___v30; + Dafny.ISet> _21_recIdentsIdx; RAST._IExpr _out6; Defs._IOwnership _out7; Dafny.ISet> _out8; - (this).GenExpr((_10_indices).Select(_16_i), selfIdent, env, Defs.Ownership.create_OwnershipOwned(), out _out6, out _out7, out _out8); - _17_idx = _out6; - _18___v30 = _out7; - _19_recIdentsIdx = _out8; - Dafny.ISequence _20_varName; - _20_varName = Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("__idx"), Std.Strings.__default.OfNat(_16_i)); - _15_indicesExpr = Dafny.Sequence.Concat(_15_indicesExpr, Dafny.Sequence.FromElements(RAST.Expr.create_Identifier(_20_varName))); - _14_r = (_14_r).Then(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_CONST(), _20_varName, Std.Wrappers.Option.create_None(), Std.Wrappers.Option.create_Some(RAST.__default.IntoUsize(_17_idx)))); - readIdents = Dafny.Set>.Union(readIdents, _19_recIdentsIdx); - } - if ((new BigInteger((_10_indices).Count)) > (BigInteger.One)) { - _11_onExpr = (_11_onExpr).Sel(Dafny.Sequence.UnicodeFromString("data")); - } - generated = (_14_r).Then(RAST.Expr.create_Assign(Std.Wrappers.Option.create_Some(RAST.AssignLhs.create_Index(_11_onExpr, _15_indicesExpr)), rhs)); + (this).GenExpr((_12_indices).Select(_18_i), selfIdent, env, Defs.Ownership.create_OwnershipOwned(), out _out6, out _out7, out _out8); + _19_idx = _out6; + _20___v30 = _out7; + _21_recIdentsIdx = _out8; + Dafny.ISequence _22_varName; + _22_varName = Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("__idx"), Std.Strings.__default.OfNat(_18_i)); + _17_indicesExpr = Dafny.Sequence.Concat(_17_indicesExpr, Dafny.Sequence.FromElements(RAST.Expr.create_Identifier(_22_varName))); + _16_r = (_16_r).Then(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_CONST(), _22_varName, Std.Wrappers.Option.create_None(), Std.Wrappers.Option.create_Some(RAST.__default.IntoUsize(_19_idx)))); + readIdents = Dafny.Set>.Union(readIdents, _21_recIdentsIdx); + } + if ((new BigInteger((_12_indices).Count)) > (BigInteger.One)) { + _13_onExpr = (_13_onExpr).Sel(Dafny.Sequence.UnicodeFromString("data")); + } + generated = (_16_r).Then(RAST.Expr.create_Assign(Std.Wrappers.Option.create_Some(RAST.AssignLhs.create_Index(_13_onExpr, _17_indicesExpr)), rhs)); needsIIFE = true; } } @@ -2078,20 +2080,20 @@ public void GenStmt(DAST._IStatement stmt, Defs._ISelfInfo selfIdent, Defs._IEnv DAST._IStatement _source0 = stmt; { if (_source0.is_ConstructorNewSeparator) { - Dafny.ISequence _0_fields = _source0.dtor_fields; + Dafny.ISequence _0_fields = _source0.dtor_fields; { generated = (this).InitEmptyExpr(); readIdents = Dafny.Set>.FromElements(); newEnv = env; BigInteger _hi0 = new BigInteger((_0_fields).Count); for (BigInteger _1_i = BigInteger.Zero; _1_i < _hi0; _1_i++) { - DAST._IFormal _2_field; + DAST._IField _2_field; _2_field = (_0_fields).Select(_1_i); Dafny.ISequence _3_fieldName; - _3_fieldName = Defs.__default.escapeVar((_2_field).dtor_name); + _3_fieldName = Defs.__default.escapeVar(((_2_field).dtor_formal).dtor_name); RAST._IType _4_fieldTyp; RAST._IType _out0; - _out0 = (this).GenType((_2_field).dtor_typ, Defs.GenTypeContext.@default()); + _out0 = (this).GenType(((_2_field).dtor_formal).dtor_typ, Defs.GenTypeContext.@default()); _4_fieldTyp = _out0; Dafny.ISequence _5_isAssignedVar; _5_isAssignedVar = Defs.__default.AddAssignedPrefix(_3_fieldName); @@ -2102,12 +2104,18 @@ public void GenStmt(DAST._IStatement stmt, Defs._ISelfInfo selfIdent, Defs._IEnv RAST._IExpr _out1; Defs._IOwnership _out2; Dafny.ISet> _out3; - (this).GenExpr(DAST.Expression.create_InitializationValue((_2_field).dtor_typ), selfIdent, env, Defs.Ownership.create_OwnershipOwned(), out _out1, out _out2, out _out3); + (this).GenExpr(DAST.Expression.create_InitializationValue(((_2_field).dtor_formal).dtor_typ), selfIdent, env, Defs.Ownership.create_OwnershipOwned(), out _out1, out _out2, out _out3); _6_rhs = _out1; _7___v31 = _out2; _8___v32 = _out3; readIdents = Dafny.Set>.Union(readIdents, Dafny.Set>.FromElements(_5_isAssignedVar)); - generated = (generated).Then((((RAST.__default.dafny__runtime).MSel((this).update__field__if__uninit__macro)).AsExpr()).Apply(Dafny.Sequence.FromElements(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("this")), RAST.Expr.create_Identifier(_3_fieldName), RAST.Expr.create_Identifier(_5_isAssignedVar), _6_rhs))); + Dafny.ISequence _9_update__if__uninit; + if ((_2_field).dtor_isConstant) { + _9_update__if__uninit = (this).update__field__if__uninit__macro; + } else { + _9_update__if__uninit = (this).update__field__mut__if__uninit__macro; + } + generated = (generated).Then((((RAST.__default.dafny__runtime).MSel(_9_update__if__uninit)).AsExpr()).Apply(Dafny.Sequence.FromElements(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("this")), RAST.Expr.create_Identifier(_3_fieldName), RAST.Expr.create_Identifier(_5_isAssignedVar), _6_rhs))); newEnv = (newEnv).RemoveAssigned(_5_isAssignedVar); } } @@ -2117,48 +2125,48 @@ public void GenStmt(DAST._IStatement stmt, Defs._ISelfInfo selfIdent, Defs._IEnv } { if (_source0.is_DeclareVar) { - Dafny.ISequence _9_name = _source0.dtor_name; - DAST._IType _10_typ = _source0.dtor_typ; + Dafny.ISequence _10_name = _source0.dtor_name; + DAST._IType _11_typ = _source0.dtor_typ; Std.Wrappers._IOption maybeValue0 = _source0.dtor_maybeValue; if (maybeValue0.is_Some) { - DAST._IExpression _11_expression = maybeValue0.dtor_value; + DAST._IExpression _12_expression = maybeValue0.dtor_value; { - RAST._IType _12_tpe; + RAST._IType _13_tpe; RAST._IType _out4; - _out4 = (this).GenType(_10_typ, Defs.GenTypeContext.@default()); - _12_tpe = _out4; - Dafny.ISequence _13_varName; - _13_varName = Defs.__default.escapeVar(_9_name); - bool _14_hasCopySemantics; - _14_hasCopySemantics = (_12_tpe).CanReadWithoutClone(); - if (((_11_expression).is_InitializationValue) && (!(_14_hasCopySemantics))) { - generated = RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), _13_varName, Std.Wrappers.Option.create_None(), Std.Wrappers.Option.create_Some(((((RAST.__default.MaybePlaceboPath).AsExpr()).ApplyType1(_12_tpe)).FSel(Dafny.Sequence.UnicodeFromString("new"))).Apply0())); + _out4 = (this).GenType(_11_typ, Defs.GenTypeContext.@default()); + _13_tpe = _out4; + Dafny.ISequence _14_varName; + _14_varName = Defs.__default.escapeVar(_10_name); + bool _15_hasCopySemantics; + _15_hasCopySemantics = (_13_tpe).CanReadWithoutClone(); + if (((_12_expression).is_InitializationValue) && (!(_15_hasCopySemantics))) { + 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(_13_varName, RAST.__default.MaybePlaceboType(_12_tpe)); + newEnv = (env).AddAssigned(_14_varName, RAST.__default.MaybePlaceboType(_13_tpe)); } else { - RAST._IExpr _15_expr = RAST.Expr.Default(); - Dafny.ISet> _16_recIdents = Dafny.Set>.Empty; - if (((_11_expression).is_InitializationValue) && ((_12_tpe).IsObjectOrPointer())) { - _15_expr = (_12_tpe).ToNullExpr(); - _16_recIdents = Dafny.Set>.FromElements(); + RAST._IExpr _16_expr = RAST.Expr.Default(); + Dafny.ISet> _17_recIdents = Dafny.Set>.Empty; + if (((_12_expression).is_InitializationValue) && ((_13_tpe).IsObjectOrPointer())) { + _16_expr = (_13_tpe).ToNullExpr(); + _17_recIdents = Dafny.Set>.FromElements(); } else { - Defs._IOwnership _17_exprOwnership = Defs.Ownership.Default(); + Defs._IOwnership _18_exprOwnership = Defs.Ownership.Default(); RAST._IExpr _out5; Defs._IOwnership _out6; Dafny.ISet> _out7; - (this).GenExpr(_11_expression, selfIdent, env, Defs.Ownership.create_OwnershipOwned(), out _out5, out _out6, out _out7); - _15_expr = _out5; - _17_exprOwnership = _out6; - _16_recIdents = _out7; + (this).GenExpr(_12_expression, selfIdent, env, Defs.Ownership.create_OwnershipOwned(), out _out5, out _out6, out _out7); + _16_expr = _out5; + _18_exprOwnership = _out6; + _17_recIdents = _out7; } - readIdents = _16_recIdents; - if ((_11_expression).is_NewUninitArray) { - _12_tpe = (_12_tpe).TypeAtInitialization(); + readIdents = _17_recIdents; + if ((_12_expression).is_NewUninitArray) { + _13_tpe = (_13_tpe).TypeAtInitialization(); } else { - _12_tpe = _12_tpe; + _13_tpe = _13_tpe; } - generated = RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), _13_varName, Std.Wrappers.Option.create_Some(_12_tpe), Std.Wrappers.Option.create_Some(_15_expr)); - newEnv = (env).AddAssigned(_13_varName, _12_tpe); + generated = RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), _14_varName, Std.Wrappers.Option.create_Some(_13_tpe), Std.Wrappers.Option.create_Some(_16_expr)); + newEnv = (env).AddAssigned(_14_varName, _13_tpe); } } goto after_match0; @@ -2167,17 +2175,17 @@ public void GenStmt(DAST._IStatement stmt, Defs._ISelfInfo selfIdent, Defs._IEnv } { if (_source0.is_DeclareVar) { - Dafny.ISequence _18_name = _source0.dtor_name; - DAST._IType _19_typ = _source0.dtor_typ; + Dafny.ISequence _19_name = _source0.dtor_name; + DAST._IType _20_typ = _source0.dtor_typ; Std.Wrappers._IOption maybeValue1 = _source0.dtor_maybeValue; if (maybeValue1.is_None) { { - DAST._IStatement _20_newStmt; - _20_newStmt = DAST.Statement.create_DeclareVar(_18_name, _19_typ, Std.Wrappers.Option.create_Some(DAST.Expression.create_InitializationValue(_19_typ))); + DAST._IStatement _21_newStmt; + _21_newStmt = DAST.Statement.create_DeclareVar(_19_name, _20_typ, Std.Wrappers.Option.create_Some(DAST.Expression.create_InitializationValue(_20_typ))); RAST._IExpr _out8; Dafny.ISet> _out9; Defs._IEnvironment _out10; - (this).GenStmt(_20_newStmt, selfIdent, env, isLast, earlyReturn, out _out8, out _out9, out _out10); + (this).GenStmt(_21_newStmt, selfIdent, env, isLast, earlyReturn, out _out8, out _out9, out _out10); generated = _out8; readIdents = _out9; newEnv = _out10; @@ -2188,124 +2196,124 @@ public void GenStmt(DAST._IStatement stmt, Defs._ISelfInfo selfIdent, Defs._IEnv } { if (_source0.is_Assign) { - DAST._IAssignLhs _21_lhs = _source0.dtor_lhs; - DAST._IExpression _22_expression = _source0.dtor_value; + DAST._IAssignLhs _22_lhs = _source0.dtor_lhs; + DAST._IExpression _23_expression = _source0.dtor_value; { - RAST._IExpr _23_exprGen; - Defs._IOwnership _24___v33; - Dafny.ISet> _25_exprIdents; + RAST._IExpr _24_exprGen; + Defs._IOwnership _25___v33; + Dafny.ISet> _26_exprIdents; RAST._IExpr _out11; Defs._IOwnership _out12; Dafny.ISet> _out13; - (this).GenExpr(_22_expression, selfIdent, env, Defs.Ownership.create_OwnershipOwned(), out _out11, out _out12, out _out13); - _23_exprGen = _out11; - _24___v33 = _out12; - _25_exprIdents = _out13; - 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); + (this).GenExpr(_23_expression, selfIdent, env, Defs.Ownership.create_OwnershipOwned(), out _out11, out _out12, out _out13); + _24_exprGen = _out11; + _25___v33 = _out12; + _26_exprIdents = _out13; + if ((_22_lhs).is_Ident) { + Dafny.ISequence _27_rustId; + _27_rustId = Defs.__default.escapeVar((_22_lhs).dtor_ident); + Std.Wrappers._IOption _28_tpe; + _28_tpe = (env).GetType(_27_rustId); + if (((_28_tpe).is_Some) && ((((_28_tpe).dtor_value).ExtractMaybePlacebo()).is_Some)) { + _24_exprGen = RAST.__default.MaybePlacebo(_24_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); + if (((_22_lhs).is_Index) && (((_22_lhs).dtor_expr).is_Ident)) { + Dafny.ISequence _29_rustId; + _29_rustId = Defs.__default.escapeVar(((_22_lhs).dtor_expr).dtor_name); + Std.Wrappers._IOption _30_tpe; + _30_tpe = (env).GetType(_29_rustId); + if (((_30_tpe).is_Some) && ((((_30_tpe).dtor_value).ExtractMaybeUninitArrayElement()).is_Some)) { + _24_exprGen = RAST.__default.MaybeUninitNew(_24_exprGen); } } - RAST._IExpr _30_lhsGen; - bool _31_needsIIFE; - Dafny.ISet> _32_recIdents; - Defs._IEnvironment _33_resEnv; + RAST._IExpr _31_lhsGen; + bool _32_needsIIFE; + Dafny.ISet> _33_recIdents; + Defs._IEnvironment _34_resEnv; RAST._IExpr _out14; bool _out15; Dafny.ISet> _out16; Defs._IEnvironment _out17; - (this).GenAssignLhs(_21_lhs, _23_exprGen, selfIdent, env, out _out14, out _out15, out _out16, out _out17); - _30_lhsGen = _out14; - _31_needsIIFE = _out15; - _32_recIdents = _out16; - _33_resEnv = _out17; - generated = _30_lhsGen; - newEnv = _33_resEnv; - if (_31_needsIIFE) { + (this).GenAssignLhs(_22_lhs, _24_exprGen, selfIdent, env, out _out14, out _out15, out _out16, out _out17); + _31_lhsGen = _out14; + _32_needsIIFE = _out15; + _33_recIdents = _out16; + _34_resEnv = _out17; + generated = _31_lhsGen; + newEnv = _34_resEnv; + if (_32_needsIIFE) { generated = RAST.Expr.create_Block(generated); } - readIdents = Dafny.Set>.Union(_32_recIdents, _25_exprIdents); + readIdents = Dafny.Set>.Union(_33_recIdents, _26_exprIdents); } goto after_match0; } } { if (_source0.is_If) { - DAST._IExpression _34_cond = _source0.dtor_cond; - Dafny.ISequence _35_thnDafny = _source0.dtor_thn; - Dafny.ISequence _36_elsDafny = _source0.dtor_els; + DAST._IExpression _35_cond = _source0.dtor_cond; + Dafny.ISequence _36_thnDafny = _source0.dtor_thn; + Dafny.ISequence _37_elsDafny = _source0.dtor_els; { - RAST._IExpr _37_cond; - Defs._IOwnership _38___v34; - Dafny.ISet> _39_recIdents; + RAST._IExpr _38_cond; + Defs._IOwnership _39___v34; + Dafny.ISet> _40_recIdents; RAST._IExpr _out18; Defs._IOwnership _out19; Dafny.ISet> _out20; - (this).GenExpr(_34_cond, selfIdent, env, Defs.Ownership.create_OwnershipOwned(), out _out18, out _out19, out _out20); - _37_cond = _out18; - _38___v34 = _out19; - _39_recIdents = _out20; - 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; + (this).GenExpr(_35_cond, selfIdent, env, Defs.Ownership.create_OwnershipOwned(), out _out18, out _out19, out _out20); + _38_cond = _out18; + _39___v34 = _out19; + _40_recIdents = _out20; + Dafny.ISequence _41_condString; + _41_condString = (_38_cond)._ToString(Defs.__default.IND); + readIdents = _40_recIdents; + RAST._IExpr _42_thn; + Dafny.ISet> _43_thnIdents; + Defs._IEnvironment _44_thnEnv; RAST._IExpr _out21; Dafny.ISet> _out22; Defs._IEnvironment _out23; - (this).GenStmts(_35_thnDafny, selfIdent, env, isLast, earlyReturn, out _out21, out _out22, out _out23); - _41_thn = _out21; - _42_thnIdents = _out22; - _43_thnEnv = _out23; - readIdents = Dafny.Set>.Union(readIdents, _42_thnIdents); - RAST._IExpr _44_els; - Dafny.ISet> _45_elsIdents; - Defs._IEnvironment _46_elsEnv; + (this).GenStmts(_36_thnDafny, selfIdent, env, isLast, earlyReturn, out _out21, out _out22, out _out23); + _42_thn = _out21; + _43_thnIdents = _out22; + _44_thnEnv = _out23; + readIdents = Dafny.Set>.Union(readIdents, _43_thnIdents); + RAST._IExpr _45_els; + Dafny.ISet> _46_elsIdents; + Defs._IEnvironment _47_elsEnv; RAST._IExpr _out24; Dafny.ISet> _out25; Defs._IEnvironment _out26; - (this).GenStmts(_36_elsDafny, selfIdent, env, isLast, earlyReturn, out _out24, out _out25, out _out26); - _44_els = _out24; - _45_elsIdents = _out25; - _46_elsEnv = _out26; - readIdents = Dafny.Set>.Union(readIdents, _45_elsIdents); + (this).GenStmts(_37_elsDafny, selfIdent, env, isLast, earlyReturn, out _out24, out _out25, out _out26); + _45_els = _out24; + _46_elsIdents = _out25; + _47_elsEnv = _out26; + readIdents = Dafny.Set>.Union(readIdents, _46_elsIdents); newEnv = env; - generated = RAST.Expr.create_IfExpr(_37_cond, _41_thn, _44_els); + generated = RAST.Expr.create_IfExpr(_38_cond, _42_thn, _45_els); } goto after_match0; } } { if (_source0.is_Labeled) { - Dafny.ISequence _47_lbl = _source0.dtor_lbl; - Dafny.ISequence _48_body = _source0.dtor_body; + Dafny.ISequence _48_lbl = _source0.dtor_lbl; + Dafny.ISequence _49_body = _source0.dtor_body; { - RAST._IExpr _49_body; - Dafny.ISet> _50_bodyIdents; - Defs._IEnvironment _51_env2; + RAST._IExpr _50_body; + Dafny.ISet> _51_bodyIdents; + Defs._IEnvironment _52_env2; RAST._IExpr _out27; Dafny.ISet> _out28; Defs._IEnvironment _out29; - (this).GenStmts(_48_body, selfIdent, env, isLast, earlyReturn, out _out27, out _out28, out _out29); - _49_body = _out27; - _50_bodyIdents = _out28; - _51_env2 = _out29; - 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())))); + (this).GenStmts(_49_body, selfIdent, env, isLast, earlyReturn, out _out27, out _out28, out _out29); + _50_body = _out27; + _51_bodyIdents = _out28; + _52_env2 = _out29; + readIdents = _51_bodyIdents; + generated = RAST.Expr.create_Labelled(Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("label_"), _48_lbl), RAST.Expr.create_Loop(Std.Wrappers.Option.create_None(), RAST.Expr.create_StmtExpr(_50_body, RAST.Expr.create_Break(Std.Wrappers.Option>.create_None())))); newEnv = env; } goto after_match0; @@ -2313,91 +2321,91 @@ public void GenStmt(DAST._IStatement stmt, Defs._ISelfInfo selfIdent, Defs._IEnv } { if (_source0.is_While) { - DAST._IExpression _52_cond = _source0.dtor_cond; - Dafny.ISequence _53_body = _source0.dtor_body; + DAST._IExpression _53_cond = _source0.dtor_cond; + Dafny.ISequence _54_body = _source0.dtor_body; { - RAST._IExpr _54_cond; - Defs._IOwnership _55___v35; - Dafny.ISet> _56_recIdents; + RAST._IExpr _55_cond; + Defs._IOwnership _56___v35; + Dafny.ISet> _57_recIdents; RAST._IExpr _out30; Defs._IOwnership _out31; Dafny.ISet> _out32; - (this).GenExpr(_52_cond, selfIdent, env, Defs.Ownership.create_OwnershipOwned(), out _out30, out _out31, out _out32); - _54_cond = _out30; - _55___v35 = _out31; - _56_recIdents = _out32; - readIdents = _56_recIdents; - RAST._IExpr _57_bodyExpr; - Dafny.ISet> _58_bodyIdents; - Defs._IEnvironment _59_bodyEnv; + (this).GenExpr(_53_cond, selfIdent, env, Defs.Ownership.create_OwnershipOwned(), out _out30, out _out31, out _out32); + _55_cond = _out30; + _56___v35 = _out31; + _57_recIdents = _out32; + readIdents = _57_recIdents; + RAST._IExpr _58_bodyExpr; + Dafny.ISet> _59_bodyIdents; + Defs._IEnvironment _60_bodyEnv; RAST._IExpr _out33; Dafny.ISet> _out34; Defs._IEnvironment _out35; - (this).GenStmts(_53_body, selfIdent, env, false, earlyReturn, out _out33, out _out34, out _out35); - _57_bodyExpr = _out33; - _58_bodyIdents = _out34; - _59_bodyEnv = _out35; + (this).GenStmts(_54_body, selfIdent, env, false, earlyReturn, out _out33, out _out34, out _out35); + _58_bodyExpr = _out33; + _59_bodyIdents = _out34; + _60_bodyEnv = _out35; newEnv = env; - readIdents = Dafny.Set>.Union(readIdents, _58_bodyIdents); - generated = RAST.Expr.create_Loop(Std.Wrappers.Option.create_Some(_54_cond), _57_bodyExpr); + readIdents = Dafny.Set>.Union(readIdents, _59_bodyIdents); + generated = RAST.Expr.create_Loop(Std.Wrappers.Option.create_Some(_55_cond), _58_bodyExpr); } goto after_match0; } } { if (_source0.is_Foreach) { - 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; + Dafny.ISequence _61_boundName = _source0.dtor_boundName; + DAST._IType _62_boundType = _source0.dtor_boundType; + DAST._IExpression _63_overExpr = _source0.dtor_over; + Dafny.ISequence _64_body = _source0.dtor_body; { - RAST._IExpr _64_over; - Defs._IOwnership _65___v36; - Dafny.ISet> _66_recIdents; + RAST._IExpr _65_over; + Defs._IOwnership _66___v36; + Dafny.ISet> _67_recIdents; RAST._IExpr _out36; Defs._IOwnership _out37; Dafny.ISet> _out38; - (this).GenExpr(_62_overExpr, selfIdent, env, Defs.Ownership.create_OwnershipOwned(), out _out36, out _out37, out _out38); - _64_over = _out36; - _65___v36 = _out37; - _66_recIdents = _out38; - if (((_62_overExpr).is_MapBoundedPool) || ((_62_overExpr).is_SetBoundedPool)) { - _64_over = ((_64_over).Sel(Dafny.Sequence.UnicodeFromString("cloned"))).Apply0(); - } - RAST._IType _67_boundTpe; + (this).GenExpr(_63_overExpr, selfIdent, env, Defs.Ownership.create_OwnershipOwned(), out _out36, out _out37, out _out38); + _65_over = _out36; + _66___v36 = _out37; + _67_recIdents = _out38; + if (((_63_overExpr).is_MapBoundedPool) || ((_63_overExpr).is_SetBoundedPool)) { + _65_over = ((_65_over).Sel(Dafny.Sequence.UnicodeFromString("cloned"))).Apply0(); + } + RAST._IType _68_boundTpe; RAST._IType _out39; - _out39 = (this).GenType(_61_boundType, Defs.GenTypeContext.@default()); - _67_boundTpe = _out39; - 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; + _out39 = (this).GenType(_62_boundType, Defs.GenTypeContext.@default()); + _68_boundTpe = _out39; + readIdents = _67_recIdents; + Dafny.ISequence _69_boundRName; + _69_boundRName = Defs.__default.escapeVar(_61_boundName); + RAST._IExpr _70_bodyExpr; + Dafny.ISet> _71_bodyIdents; + Defs._IEnvironment _72_bodyEnv; RAST._IExpr _out40; Dafny.ISet> _out41; Defs._IEnvironment _out42; - (this).GenStmts(_63_body, selfIdent, (env).AddAssigned(_68_boundRName, _67_boundTpe), false, earlyReturn, out _out40, out _out41, out _out42); - _69_bodyExpr = _out40; - _70_bodyIdents = _out41; - _71_bodyEnv = _out42; - readIdents = Dafny.Set>.Difference(Dafny.Set>.Union(readIdents, _70_bodyIdents), Dafny.Set>.FromElements(_68_boundRName)); + (this).GenStmts(_64_body, selfIdent, (env).AddAssigned(_69_boundRName, _68_boundTpe), false, earlyReturn, out _out40, out _out41, out _out42); + _70_bodyExpr = _out40; + _71_bodyIdents = _out41; + _72_bodyEnv = _out42; + readIdents = Dafny.Set>.Difference(Dafny.Set>.Union(readIdents, _71_bodyIdents), Dafny.Set>.FromElements(_69_boundRName)); newEnv = env; - generated = RAST.Expr.create_For(_68_boundRName, _64_over, _69_bodyExpr); + generated = RAST.Expr.create_For(_69_boundRName, _65_over, _70_bodyExpr); } goto after_match0; } } { if (_source0.is_Break) { - Std.Wrappers._IOption> _72_toLabel = _source0.dtor_toLabel; + Std.Wrappers._IOption> _73_toLabel = _source0.dtor_toLabel; { - Std.Wrappers._IOption> _source1 = _72_toLabel; + Std.Wrappers._IOption> _source1 = _73_toLabel; { if (_source1.is_Some) { - Dafny.ISequence _73_lbl = _source1.dtor_value; + Dafny.ISequence _74_lbl = _source1.dtor_value; { - generated = RAST.Expr.create_Break(Std.Wrappers.Option>.create_Some(Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("label_"), _73_lbl))); + generated = RAST.Expr.create_Break(Std.Wrappers.Option>.create_Some(Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("label_"), _74_lbl))); } goto after_match1; } @@ -2416,67 +2424,67 @@ public void GenStmt(DAST._IStatement stmt, Defs._ISelfInfo selfIdent, Defs._IEnv } { if (_source0.is_TailRecursive) { - Dafny.ISequence _74_body = _source0.dtor_body; + Dafny.ISequence _75_body = _source0.dtor_body; { generated = (this).InitEmptyExpr(); if (!object.Equals(selfIdent, Defs.SelfInfo.create_NoSelf())) { - RAST._IExpr _75_selfClone; - Defs._IOwnership _76___v37; - Dafny.ISet> _77___v38; + RAST._IExpr _76_selfClone; + Defs._IOwnership _77___v37; + Dafny.ISet> _78___v38; RAST._IExpr _out43; Defs._IOwnership _out44; Dafny.ISet> _out45; (this).GenIdent((selfIdent).dtor_rSelfName, selfIdent, Defs.Environment.Empty(), Defs.Ownership.create_OwnershipOwned(), out _out43, out _out44, out _out45); - _75_selfClone = _out43; - _76___v37 = _out44; - _77___v38 = _out45; - 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))); + _76_selfClone = _out43; + _77___v37 = _out44; + _78___v38 = _out45; + 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))); } newEnv = env; - RAST._IExpr _78_loopBegin; - _78_loopBegin = RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("")); + RAST._IExpr _79_loopBegin; + _79_loopBegin = RAST.Expr.create_RawExpr(Dafny.Sequence.UnicodeFromString("")); BigInteger _hi1 = new BigInteger(((env).dtor_names).Count); - 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"))) { + for (BigInteger _80_paramI = BigInteger.Zero; _80_paramI < _hi1; _80_paramI++) { + Dafny.ISequence _81_param; + _81_param = ((env).dtor_names).Select(_80_paramI); + if ((_81_param).Equals(Dafny.Sequence.UnicodeFromString("_accumulator"))) { goto continue_4_0; } - RAST._IExpr _81_paramInit; - Defs._IOwnership _82___v39; - Dafny.ISet> _83___v40; + RAST._IExpr _82_paramInit; + Defs._IOwnership _83___v39; + Dafny.ISet> _84___v40; RAST._IExpr _out46; Defs._IOwnership _out47; Dafny.ISet> _out48; - (this).GenIdent(_80_param, selfIdent, env, Defs.Ownership.create_OwnershipOwned(), out _out46, out _out47, out _out48); - _81_paramInit = _out46; - _82___v39 = _out47; - _83___v40 = _out48; - Dafny.ISequence _84_recVar; - _84_recVar = Dafny.Sequence.Concat(Defs.__default.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); + (this).GenIdent(_81_param, selfIdent, env, Defs.Ownership.create_OwnershipOwned(), out _out46, out _out47, out _out48); + _82_paramInit = _out46; + _83___v39 = _out47; + _84___v40 = _out48; + 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 (((env).dtor_types).Contains(_81_param)) { + RAST._IType _86_declaredType; + _86_declaredType = (Dafny.Map, RAST._IType>.Select((env).dtor_types,_81_param)).ToOwned(); + newEnv = (newEnv).AddAssigned(_81_param, _86_declaredType); + newEnv = (newEnv).AddAssigned(_85_recVar, _86_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)))); + _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 _86_bodyExpr; - Dafny.ISet> _87_bodyIdents; - Defs._IEnvironment _88_bodyEnv; + RAST._IExpr _87_bodyExpr; + Dafny.ISet> _88_bodyIdents; + Defs._IEnvironment _89_bodyEnv; RAST._IExpr _out49; Dafny.ISet> _out50; Defs._IEnvironment _out51; - (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 _out49, out _out50, out _out51); - _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)))); + (this).GenStmts(_75_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 _out49, out _out50, out _out51); + _87_bodyExpr = _out49; + _88_bodyIdents = _out50; + _89_bodyEnv = _out51; + 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; } @@ -2493,83 +2501,83 @@ public void GenStmt(DAST._IStatement stmt, Defs._ISelfInfo selfIdent, Defs._IEnv } { if (_source0.is_Call) { - 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; + 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; { - Dafny.ISequence _94_argExprs; - Dafny.ISet> _95_recIdents; - Dafny.ISequence _96_typeExprs; - Std.Wrappers._IOption _97_fullNameQualifier; + Dafny.ISequence _95_argExprs; + Dafny.ISet> _96_recIdents; + Dafny.ISequence _97_typeExprs; + Std.Wrappers._IOption _98_fullNameQualifier; Dafny.ISequence _out52; Dafny.ISet> _out53; Dafny.ISequence _out54; Std.Wrappers._IOption _out55; - (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; + (this).GenArgs(selfIdent, _91_name, _92_typeArgs, _93_args, env, out _out52, out _out53, out _out54, out _out55); + _95_argExprs = _out52; + _96_recIdents = _out53; + _97_typeExprs = _out54; + _98_fullNameQualifier = _out55; + readIdents = _96_recIdents; + Std.Wrappers._IOption _source2 = _98_fullNameQualifier; { if (_source2.is_Some) { DAST._IResolvedType value0 = _source2.dtor_value; - 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; + Dafny.ISequence> _99_path = value0.dtor_path; + Dafny.ISequence _100_onTypeArgs = value0.dtor_typeArgs; + DAST._IResolvedTypeBase _101_base = value0.dtor_kind; + RAST._IExpr _102_fullPath; RAST._IExpr _out56; - _out56 = (this).GenPathExpr(_98_path, true); - _101_fullPath = _out56; - Dafny.ISequence _102_onTypeExprs; + _out56 = (this).GenPathExpr(_99_path, true); + _102_fullPath = _out56; + Dafny.ISequence _103_onTypeExprs; Dafny.ISequence _out57; - _out57 = (this).GenTypeArgs(_99_onTypeArgs, Defs.GenTypeContext.@default()); - _102_onTypeExprs = _out57; - RAST._IExpr _103_onExpr = RAST.Expr.Default(); - Defs._IOwnership _104_recOwnership = Defs.Ownership.Default(); - Dafny.ISet> _105_recIdents = Dafny.Set>.Empty; - if (((_100_base).is_Trait) || ((_100_base).is_Class)) { + _out57 = (this).GenTypeArgs(_100_onTypeArgs, Defs.GenTypeContext.@default()); + _103_onTypeExprs = _out57; + RAST._IExpr _104_onExpr = RAST.Expr.Default(); + Defs._IOwnership _105_recOwnership = Defs.Ownership.Default(); + Dafny.ISet> _106_recIdents = Dafny.Set>.Empty; + if (((_101_base).is_Trait) || ((_101_base).is_Class)) { RAST._IExpr _out58; Defs._IOwnership _out59; Dafny.ISet> _out60; - (this).GenExpr(_89_on, selfIdent, env, Defs.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); + (this).GenExpr(_90_on, selfIdent, env, Defs.Ownership.create_OwnershipOwned(), out _out58, out _out59, out _out60); + _104_onExpr = _out58; + _105_recOwnership = _out59; + _106_recIdents = _out60; + _104_onExpr = ((this).modify__macro).Apply1(_104_onExpr); + readIdents = Dafny.Set>.Union(readIdents, _106_recIdents); } else { RAST._IExpr _out61; Defs._IOwnership _out62; Dafny.ISet> _out63; - (this).GenExpr(_89_on, selfIdent, env, Defs.Ownership.create_OwnershipBorrowed(), out _out61, out _out62, out _out63); - _103_onExpr = _out61; - _104_recOwnership = _out62; - _105_recIdents = _out63; - readIdents = Dafny.Set>.Union(readIdents, _105_recIdents); + (this).GenExpr(_90_on, selfIdent, env, Defs.Ownership.create_OwnershipBorrowed(), out _out61, out _out62, out _out63); + _104_onExpr = _out61; + _105_recOwnership = _out62; + _106_recIdents = _out63; + readIdents = Dafny.Set>.Union(readIdents, _106_recIdents); } - generated = ((((_101_fullPath).ApplyType(_102_onTypeExprs)).FSel(Defs.__default.escapeName((_90_name).dtor_name))).ApplyType(_96_typeExprs)).Apply(Dafny.Sequence.Concat(Dafny.Sequence.FromElements(_103_onExpr), _94_argExprs)); + generated = ((((_102_fullPath).ApplyType(_103_onTypeExprs)).FSel(Defs.__default.escapeName((_91_name).dtor_name))).ApplyType(_97_typeExprs)).Apply(Dafny.Sequence.Concat(Dafny.Sequence.FromElements(_104_onExpr), _95_argExprs)); goto after_match2; } } { - RAST._IExpr _106_onExpr; - Defs._IOwnership _107___v45; - Dafny.ISet> _108_enclosingIdents; + RAST._IExpr _107_onExpr; + Defs._IOwnership _108___v45; + Dafny.ISet> _109_enclosingIdents; RAST._IExpr _out64; Defs._IOwnership _out65; Dafny.ISet> _out66; - (this).GenExpr(_89_on, selfIdent, env, Defs.Ownership.create_OwnershipAutoBorrowed(), out _out64, out _out65, out _out66); - _106_onExpr = _out64; - _107___v45 = _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; + (this).GenExpr(_90_on, selfIdent, env, Defs.Ownership.create_OwnershipAutoBorrowed(), out _out64, out _out65, out _out66); + _107_onExpr = _out64; + _108___v45 = _out65; + _109_enclosingIdents = _out66; + readIdents = Dafny.Set>.Union(readIdents, _109_enclosingIdents); + Dafny.ISequence _110_renderedName; + _110_renderedName = (this).GetMethodName(_90_on, _91_name); + DAST._IExpression _source3 = _90_on; { bool disjunctiveMatch0 = false; if (_source3.is_Companion) { @@ -2580,26 +2588,26 @@ public void GenStmt(DAST._IStatement stmt, Defs._ISelfInfo selfIdent, Defs._IEnv } if (disjunctiveMatch0) { { - _106_onExpr = (_106_onExpr).FSel(_109_renderedName); + _107_onExpr = (_107_onExpr).FSel(_110_renderedName); } goto after_match3; } } { { - if (!object.Equals(_106_onExpr, RAST.__default.self)) { - DAST._ICallName _source4 = _90_name; + if (!object.Equals(_107_onExpr, RAST.__default.self)) { + DAST._ICallName _source4 = _91_name; { if (_source4.is_CallName) { Std.Wrappers._IOption onType0 = _source4.dtor_onType; if (onType0.is_Some) { - DAST._IType _110_tpe = onType0.dtor_value; - RAST._IType _111_typ; + DAST._IType _111_tpe = onType0.dtor_value; + RAST._IType _112_typ; RAST._IType _out67; - _out67 = (this).GenType(_110_tpe, Defs.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); + _out67 = (this).GenType(_111_tpe, Defs.GenTypeContext.@default()); + _112_typ = _out67; + if (((_112_typ).IsObjectOrPointer()) && (!object.Equals(_107_onExpr, RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("self"))))) { + _107_onExpr = ((this).read__macro).Apply1(_107_onExpr); } goto after_match4; } @@ -2609,39 +2617,39 @@ public void GenStmt(DAST._IStatement stmt, Defs._ISelfInfo selfIdent, Defs._IEnv } after_match4: ; } - _106_onExpr = (_106_onExpr).Sel(_109_renderedName); + _107_onExpr = (_107_onExpr).Sel(_110_renderedName); } } after_match3: ; - generated = ((_106_onExpr).ApplyType(_96_typeExprs)).Apply(_94_argExprs); + generated = ((_107_onExpr).ApplyType(_97_typeExprs)).Apply(_95_argExprs); } after_match2: ; - if (((_93_maybeOutVars).is_Some) && ((new BigInteger(((_93_maybeOutVars).dtor_value).Count)) == (BigInteger.One))) { - Dafny.ISequence _112_outVar; - _112_outVar = Defs.__default.escapeVar(((_93_maybeOutVars).dtor_value).Select(BigInteger.Zero)); - if (!((env).CanReadWithoutClone(_112_outVar))) { + if (((_94_maybeOutVars).is_Some) && ((new BigInteger(((_94_maybeOutVars).dtor_value).Count)) == (BigInteger.One))) { + Dafny.ISequence _113_outVar; + _113_outVar = Defs.__default.escapeVar(((_94_maybeOutVars).dtor_value).Select(BigInteger.Zero)); + if (!((env).CanReadWithoutClone(_113_outVar))) { generated = RAST.__default.MaybePlacebo(generated); } - generated = RAST.__default.AssignVar(_112_outVar, generated); - } else if (((_93_maybeOutVars).is_None) || ((new BigInteger(((_93_maybeOutVars).dtor_value).Count)).Sign == 0)) { + generated = RAST.__default.AssignVar(_113_outVar, generated); + } else if (((_94_maybeOutVars).is_None) || ((new BigInteger(((_94_maybeOutVars).dtor_value).Count)).Sign == 0)) { } else { - 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 = Defs.__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); + Dafny.ISequence _114_tmpVar; + _114_tmpVar = Dafny.Sequence.UnicodeFromString("_x"); + RAST._IExpr _115_tmpId; + _115_tmpId = RAST.Expr.create_Identifier(_114_tmpVar); + generated = RAST.Expr.create_DeclareVar(RAST.DeclareType.create_CONST(), _114_tmpVar, Std.Wrappers.Option.create_None(), Std.Wrappers.Option.create_Some(generated)); + Dafny.ISequence> _116_outVars; + _116_outVars = (_94_maybeOutVars).dtor_value; + BigInteger _hi2 = new BigInteger((_116_outVars).Count); + for (BigInteger _117_outI = BigInteger.Zero; _117_outI < _hi2; _117_outI++) { + Dafny.ISequence _118_outVar; + _118_outVar = Defs.__default.escapeVar((_116_outVars).Select(_117_outI)); + RAST._IExpr _119_rhs; + _119_rhs = (_115_tmpId).Sel(Std.Strings.__default.OfNat(_117_outI)); + if (!((env).CanReadWithoutClone(_118_outVar))) { + _119_rhs = RAST.__default.MaybePlacebo(_119_rhs); } - generated = (generated).Then(RAST.__default.AssignVar(_117_outVar, _118_rhs)); + generated = (generated).Then(RAST.__default.AssignVar(_118_outVar, _119_rhs)); } } newEnv = env; @@ -2651,23 +2659,23 @@ public void GenStmt(DAST._IStatement stmt, Defs._ISelfInfo selfIdent, Defs._IEnv } { if (_source0.is_Return) { - DAST._IExpression _119_exprDafny = _source0.dtor_expr; + DAST._IExpression _120_exprDafny = _source0.dtor_expr; { - RAST._IExpr _120_expr; - Defs._IOwnership _121___v55; - Dafny.ISet> _122_recIdents; + RAST._IExpr _121_expr; + Defs._IOwnership _122___v55; + Dafny.ISet> _123_recIdents; RAST._IExpr _out68; Defs._IOwnership _out69; Dafny.ISet> _out70; - (this).GenExpr(_119_exprDafny, selfIdent, env, Defs.Ownership.create_OwnershipOwned(), out _out68, out _out69, out _out70); - _120_expr = _out68; - _121___v55 = _out69; - _122_recIdents = _out70; - readIdents = _122_recIdents; + (this).GenExpr(_120_exprDafny, selfIdent, env, Defs.Ownership.create_OwnershipOwned(), out _out68, out _out69, out _out70); + _121_expr = _out68; + _122___v55 = _out69; + _123_recIdents = _out70; + readIdents = _123_recIdents; if (isLast) { - generated = _120_expr; + generated = _121_expr; } else { - generated = RAST.Expr.create_Return(Std.Wrappers.Option.create_Some(_120_expr)); + generated = RAST.Expr.create_Return(Std.Wrappers.Option.create_Some(_121_expr)); } newEnv = env; } @@ -2685,27 +2693,27 @@ public void GenStmt(DAST._IStatement stmt, Defs._ISelfInfo selfIdent, Defs._IEnv } } { - 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; - Defs._IOwnership _127___v56; - Dafny.ISet> _128___v57; + Dafny.ISequence> _124_rustIdents = _source5.dtor_value; + Dafny.ISequence _125_tupleArgs; + _125_tupleArgs = Dafny.Sequence.FromElements(); + BigInteger _hi3 = new BigInteger((_124_rustIdents).Count); + for (BigInteger _126_i = BigInteger.Zero; _126_i < _hi3; _126_i++) { + RAST._IExpr _127_rIdent; + Defs._IOwnership _128___v56; + Dafny.ISet> _129___v57; RAST._IExpr _out71; Defs._IOwnership _out72; Dafny.ISet> _out73; - (this).GenIdent((_123_rustIdents).Select(_125_i), selfIdent, env, Defs.Ownership.create_OwnershipOwned(), out _out71, out _out72, out _out73); - _126_rIdent = _out71; - _127___v56 = _out72; - _128___v57 = _out73; - _124_tupleArgs = Dafny.Sequence.Concat(_124_tupleArgs, Dafny.Sequence.FromElements(_126_rIdent)); + (this).GenIdent((_124_rustIdents).Select(_126_i), selfIdent, env, Defs.Ownership.create_OwnershipOwned(), out _out71, out _out72, out _out73); + _127_rIdent = _out71; + _128___v56 = _out72; + _129___v57 = _out73; + _125_tupleArgs = Dafny.Sequence.Concat(_125_tupleArgs, Dafny.Sequence.FromElements(_127_rIdent)); } - if ((new BigInteger((_124_tupleArgs).Count)) == (BigInteger.One)) { - generated = RAST.Expr.create_Return(Std.Wrappers.Option.create_Some((_124_tupleArgs).Select(BigInteger.Zero))); + if ((new BigInteger((_125_tupleArgs).Count)) == (BigInteger.One)) { + generated = RAST.Expr.create_Return(Std.Wrappers.Option.create_Some((_125_tupleArgs).Select(BigInteger.Zero))); } else { - generated = RAST.Expr.create_Return(Std.Wrappers.Option.create_Some(RAST.Expr.create_Tuple(_124_tupleArgs))); + generated = RAST.Expr.create_Return(Std.Wrappers.Option.create_Some(RAST.Expr.create_Tuple(_125_tupleArgs))); } } after_match5: ; @@ -2726,20 +2734,20 @@ public void GenStmt(DAST._IStatement stmt, Defs._ISelfInfo selfIdent, Defs._IEnv } } { - DAST._IExpression _129_e = _source0.dtor_Print_a0; + DAST._IExpression _130_e = _source0.dtor_Print_a0; { - RAST._IExpr _130_printedExpr; - Defs._IOwnership _131_recOwnership; - Dafny.ISet> _132_recIdents; + RAST._IExpr _131_printedExpr; + Defs._IOwnership _132_recOwnership; + Dafny.ISet> _133_recIdents; RAST._IExpr _out74; Defs._IOwnership _out75; Dafny.ISet> _out76; - (this).GenExpr(_129_e, selfIdent, env, Defs.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; + (this).GenExpr(_130_e, selfIdent, env, Defs.Ownership.create_OwnershipBorrowed(), out _out74, out _out75, out _out76); + _131_printedExpr = _out74; + _132_recOwnership = _out75; + _133_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(_131_printedExpr))); + readIdents = _133_recIdents; newEnv = env; } } @@ -5562,8 +5570,10 @@ public void GenExpr(DAST._IExpression e, Defs._ISelfInfo selfIdent, Defs._IEnvir r = (r).Sel(Defs.__default.escapeVar(_219_field)); if (_220_isConstant) { r = (r).Apply0(); + r = (r).Clone(); + } else { + r = ((this).read__field__macro).Apply1(r); } - r = (r).Clone(); RAST._IExpr _out200; Defs._IOwnership _out201; (this).FromOwned(r, expectedOwnership, out _out200, out _out201); @@ -6736,6 +6746,13 @@ public Dafny.ISequence update__field__uninit__macro { get { return Dafny.Sequence.UnicodeFromString("update_field_uninit_object!"); } } } + public Dafny.ISequence update__field__mut__uninit__macro { get { + if (((this).pointerType).is_Raw) { + return Dafny.Sequence.UnicodeFromString("update_field_mut_uninit!"); + } else { + return Dafny.Sequence.UnicodeFromString("update_field_mut_uninit_object!"); + } + } } public RAST._IExpr thisInConstructor { get { if (((this).pointerType).is_Raw) { return RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("this")); @@ -6770,6 +6787,13 @@ public Dafny.ISequence update__field__if__uninit__macro { get { return Dafny.Sequence.UnicodeFromString("update_field_if_uninit_object!"); } } } + public Dafny.ISequence update__field__mut__if__uninit__macro { get { + if (((this).pointerType).is_Raw) { + return Dafny.Sequence.UnicodeFromString("update_field_mut_if_uninit!"); + } else { + return Dafny.Sequence.UnicodeFromString("update_field_mut_if_uninit_object!"); + } + } } public Dafny.ISequence Upcast { get { if (((this).pointerType).is_Raw) { return Dafny.Sequence.UnicodeFromString("Upcast"); @@ -6794,5 +6818,11 @@ public Dafny.ISequence downcast { get { return Dafny.Sequence.UnicodeFromString("cast_object!"); } } } + public RAST._IExpr read__field__macro { get { + return ((RAST.__default.dafny__runtime).MSel(Dafny.Sequence.UnicodeFromString("read_field!"))).AsExpr(); + } } + public RAST._IExpr modify__field__macro { get { + return ((RAST.__default.dafny__runtime).MSel(Dafny.Sequence.UnicodeFromString("modify_field!"))).AsExpr(); + } } } } // end of namespace DCOMP \ No newline at end of file diff --git a/Source/DafnyCore/bash.exe.stackdump b/Source/DafnyCore/bash.exe.stackdump new file mode 100644 index 00000000000..ab93e0789e0 --- /dev/null +++ b/Source/DafnyCore/bash.exe.stackdump @@ -0,0 +1,52 @@ +Exception: STATUS_ACCESS_VIOLATION at rip=0002101729BC +rax=0000000800000000 rbx=006D0069006D005C rcx=0000000000000007 +rdx=0000000000000009 rsi=0000000000000007 rdi=00000002102ADAE0 +r8 =000000080000CE78 r9 =FFFFFF978CD18691 r10=000000080000CE78 +r11=FEFEFEFEFEFEFEFF r12=0000000000000007 r13=000000080000C7D0 +r14=0000000000000003 r15=0000000800009228 +rbp=00000002102686E0 rsp=00000007FFFFC6B0 +program=C:\Users\mimayere\AppData\Local\Programs\Git\usr\bin\bash.exe, pid 2869, thread main +cs=0033 ds=002B es=002B fs=0053 gs=002B ss=002B +Stack trace: +Frame Function Args +0002102686E0 0002101729BC (000000000000, 000000000000, 000000000000, B34B498AE1C5) msys-2.0.dll+0x1329BC +000800008D00 00021017378B (0002102684E0, 000000000003, 000210173660, 00080000CC58) msys-2.0.dll+0x13378B +000800008D00 00021021CE4F (000003E706FF, 0003000000FF, 6C4C8C2A00000006, 000000000000) msys-2.0.dll+0x1DCE4F +000000000003 00021021CBCB (000000000000, 000210268500, 000210173590, 000000000E68) msys-2.0.dll+0x1DCBCB +000000000003 000210058F8C (000800008D00, 000000000000, 0002100FBB76, 000800008D00) msys-2.0.dll+0x18F8C +000000000003 000210059271 (000000000000, 0002100649F0, 0007FFFFC950, 0000000000FF) msys-2.0.dll+0x19271 +0007FFFFCAB0 0002100D0229 (000000000001, 0007FFFFCA3C, 000210214700, 000000000003) msys-2.0.dll+0x90229 +0007FFFFCAB0 0002101948DB (000000000001, 0007FFFFCA3C, 000210214700, 000000000003) msys-2.0.dll+0x1548DB +0007FFFFCAB0 00010040EC29 (0007FFFFCAB0, 000000000050, FFFFFFFFFFFF978C, 000000000005) bash.exe+0xEC29 +0007FFFFCAB0 0001004E9A70 (000A00000460, 000A00000160, 000000000164, 000000000000) bash.exe+0xE9A70 +0007FFFFCD30 000210047F11 (000000000000, 000000000000, 000000000000, 000000000000) msys-2.0.dll+0x7F11 +000000000000 000210045AC3 (000000000000, 000000000000, 000000000000, 000000000000) msys-2.0.dll+0x5AC3 +0007FFFFFFF0 000210045B74 (000000000000, 000000000000, 000000000000, 000000000000) msys-2.0.dll+0x5B74 +End of stack trace +Loaded modules: +000100400000 bash.exe +7FFF0BD10000 ntdll.dll +7FFF0AA50000 KERNEL32.DLL +7FFF09780000 KERNELBASE.dll +7FFF0B320000 USER32.dll +000210040000 msys-2.0.dll +7FFF09A80000 win32u.dll +7FFF0B150000 GDI32.dll +7FFF09520000 gdi32full.dll +7FFF096E0000 msvcp_win.dll +7FFF09C40000 ucrtbase.dll +7FFF0B0A0000 advapi32.dll +7FFF0AB20000 msvcrt.dll +7FFF0B530000 sechost.dll +7FFF0B180000 RPCRT4.dll +7FFF09640000 bcrypt.dll +7FFF08BB0000 CRYPTBASE.DLL +7FFF09AB0000 bcryptPrimitives.dll +7FFF0ABC0000 IMM32.DLL +000000B40000 umppc18511.dll +7FFF08720000 iphlpapi.dll +7FFF08760000 DNSAPI.dll +7FFF0ABF0000 NSI.dll +7FFF01E30000 dhcpcsvc6.DLL +7FFF01B60000 dhcpcsvc.DLL +7FFF02230000 WINNSI.DLL diff --git a/Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs b/Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs index c0b9c3d73f7..ed9accbcc4d 100644 --- a/Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs +++ b/Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs @@ -3135,6 +3135,16 @@ macro_rules! update_field_nodrop { }; } +// Same as update_field_nodrop but for mutable fields +#[macro_export] +macro_rules! update_field_mut_nodrop { + ($ptr:expr, $field:ident, $value:expr) => { + let lhs = $ptr; + let value = $value; + unsafe { $crate::read!(lhs).$field.get().write(value) } + }; +} + // When initializing an uninitialized field for the first time, // we ensure we don't drop the previous content #[macro_export] @@ -3185,6 +3195,21 @@ macro_rules! update_field_uninit { }}; } +// Same as update_field_uninit but for mutable fields +#[macro_export] +macro_rules! update_field_mut_uninit { + ($t:expr, $field:ident, $field_assigned:expr, $value:expr) => {{ + let computed_value = $value; + #[allow(unused_assignments)] + if $field_assigned { + $crate::modify_field!($crate::read!($t).$field, computed_value); + } else { + $crate::update_field_mut_nodrop!($t, $field, computed_value); + $field_assigned = true; + } + }}; +} + // Macro to call at the end of the first new; constructor when not every field is guaranteed to be assigned. #[macro_export] macro_rules! update_field_if_uninit { @@ -3197,6 +3222,18 @@ macro_rules! update_field_if_uninit { }}; } +// Same as update_field_if_uninit but for mutable fields +#[macro_export] +macro_rules! update_field_mut_if_uninit { + ($t:expr, $field:ident, $field_assigned:expr, $value:expr) => {{ + let computed_value = $value; + if !$field_assigned { + $crate::update_field_mut_nodrop!($t, $field, computed_value); + $field_assigned = true; + } + }}; +} + ///////////////// // Raw pointers (require wrapping because of equality) ///////////////// @@ -3510,6 +3547,14 @@ macro_rules! update_field_nodrop_object { }; } +// Same but for mutable fields +#[macro_export] +macro_rules! update_field_mut_nodrop_object { + ($ptr:expr, $field: ident, $value:expr) => { + unsafe { ($crate::rcmut::borrow_mut(&mut $ptr.0.clone().unwrap())).$field.get().write($value) } + }; +} + // Equivalent of update_nodrop but for rcmut #[macro_export] macro_rules! update_nodrop_object { @@ -3522,15 +3567,28 @@ macro_rules! update_nodrop_object { #[macro_export] macro_rules! update_field_if_uninit_object { ($t:expr, $field:ident, $field_assigned:expr, $value:expr) => {{ - let computed_value = $value; #[allow(unused_assignments)] if !$field_assigned { + let computed_value = $value; $crate::update_field_nodrop_object!($t, $field, computed_value); $field_assigned = true; } }}; } +// Same for mutable fields +#[macro_export] +macro_rules! update_field_mut_if_uninit_object { + ($t:expr, $field:ident, $field_assigned:expr, $value:expr) => {{ + #[allow(unused_assignments)] + if !$field_assigned { + let computed_value = $value; + $crate::update_field_mut_nodrop_object!($t, $field, computed_value); + $field_assigned = true; + } + }}; +} + // Equivalent of update_field_uninit but for rcmut #[macro_export] macro_rules! update_field_uninit_object { @@ -3546,6 +3604,22 @@ macro_rules! update_field_uninit_object { }}; } +// Same but for mutable fields +#[macro_export] +macro_rules! update_field_mut_uninit_object { + ($t:expr, $field:ident, $field_assigned:expr, $value:expr) => {{ + let computed_value = $value; + #[allow(unused_assignments)] + if $field_assigned { + $crate::modify_field!($crate::rd!($t).$field, computed_value); + } else { + $crate::update_field_mut_nodrop_object!($t, $field, computed_value); + $field_assigned = true; + } + }}; +} + + // Equivalent of modify but for rcmut #[macro_export] macro_rules! md { @@ -3562,6 +3636,32 @@ macro_rules! rd { }; } +// To use when modifying a mutable field that is wrapped with UnsafeCell +#[macro_export] +macro_rules! modify_field { + ($pointer:expr, $rhs:expr) => { + let lhs = $pointer.get(); + let rhs = $rhs; + unsafe {*lhs = rhs} + }; +} + +// To use when reading a mutable field that is wrapped with UnsafeCell +#[macro_export] +macro_rules! read_field { + ($pointer:expr) => { + { + let lhs = $pointer.get(); + unsafe {(*lhs).clone()} + } + }; +} + +pub type Field = UnsafeCell; +pub fn new_field(t: T) -> Field { + UnsafeCell::new(t) +} + // Count the number of references to the given object #[macro_export] macro_rules! refcount { diff --git a/Source/DafnyRuntime/DafnyRuntimeRust/src/tests/mod.rs b/Source/DafnyRuntime/DafnyRuntimeRust/src/tests/mod.rs index 4efbc02b45b..02643fcc55c 100644 --- a/Source/DafnyRuntime/DafnyRuntimeRust/src/tests/mod.rs +++ b/Source/DafnyRuntime/DafnyRuntimeRust/src/tests/mod.rs @@ -382,33 +382,58 @@ mod tests { } struct ClassWrapper { - /*var*/ t: T, - /*var*/ x: crate::DafnyInt, + /*var*/ t: Field, + /*var*/ x: Field, /*const*/ next: Ptr>, /*const*/ constant: crate::DafnyInt, } impl ClassWrapper { fn constant_plus_x(&self) -> crate::DafnyInt { - self.constant.clone() + self.x.clone() + self.constant.clone() + read_field!(self.x) } fn increment_x(&mut self) { - self.x = self.x.clone() + int!(1); + modify_field!(self.x, read_field!(self.x) + int!(1)); } } impl ClassWrapper { fn constructor(t: T) -> Ptr> { let this = crate::allocate::>(); - update_field_nodrop!(this, t, t); + update_field_mut_nodrop!(this, t, t); update_field_nodrop!(this, next, this); // If x is assigned twice, we need to keep track of whether it's assigned // like in methods. let mut x_assigned = false; - update_field_uninit!(this, x, x_assigned, int!(2)); - update_field_uninit!(this, x, x_assigned, int!(1)); + update_field_mut_uninit!(this, x, x_assigned, int!(2)); + update_field_mut_uninit!(this, x, x_assigned, int!(1)); // If we can prove that x is assigned, we can even write this - modify!(this).x = int!(0); + modify_field!(read!(this).x,int!(0)); update_field_nodrop!(this, constant, int!(42)); + update_field_mut_if_uninit!(this, x, x_assigned, int!(0)); + assert_eq!(x_assigned, true); + let mut next_assigned = true; + update_field_if_uninit!(this, next, next_assigned, this); + assert_eq!(next_assigned, true); + this + } + + fn constructor_object(t: T) -> Object> { + let mut this = crate::allocate_object::>(); + update_field_mut_nodrop_object!(this, t, t); + update_field_nodrop_object!(this, next, Ptr::from_raw_nonnull(this.as_mut())); + // If x is assigned twice, we need to keep track of whether it's assigned + // like in methods. + let mut x_assigned = false; + update_field_mut_uninit_object!(this, x, x_assigned, int!(2)); + update_field_mut_uninit_object!(this, x, x_assigned, int!(1)); + // If we can prove that x is assigned, we can even write this + modify_field!(rd!(this).x,int!(0)); + update_field_nodrop_object!(this, constant, int!(42)); + update_field_mut_if_uninit_object!(this, x, x_assigned, int!(0)); + assert_eq!(x_assigned, true); + let mut next_assigned = true; + update_field_if_uninit_object!(this, next, next_assigned, Ptr::from_raw_nonnull(this.as_mut())); + assert_eq!(next_assigned, true); this } } @@ -425,22 +450,40 @@ mod tests { fn test_class_wrapper() { let c: Ptr> = ClassWrapper::constructor(53); assert_eq!(read!(c).constant, int!(42)); - assert_eq!(read!(c).t, 53); - assert_eq!(read!(c).x, int!(0)); - assert_eq!(read!(read!(c).next).t, 53); + assert_eq!(read_field!(read!(c).t), 53); + assert_eq!(read_field!(read!(c).x), int!(0)); + assert_eq!(read_field!(read!(read!(c).next).t), 53); assert_eq!(read!(c).constant_plus_x(), int!(42)); modify!(c).increment_x(); assert_eq!(read!(c).constant_plus_x(), int!(43)); - modify!(c).x = int!(40); + modify_field!(read!(c).x,int!(40)); assert_eq!(read!(c).constant_plus_x(), int!(82)); - modify!(c).t = 54; - assert_eq!(read!(c).t, 54); - let x_copy = read!(c).x.clone(); + modify_field!(read!(c).t,54); + assert_eq!(read_field!(read!(c).t), 54); + let x_copy = read_field!(read!(c).x); assert_eq!(Rc::strong_count(&x_copy.data), 2); deallocate(c); assert_eq!(Rc::strong_count(&x_copy.data), 1); } + + #[test] + #[allow(unused_unsafe)] + fn test_class_wrapper_object() { + let c: Object> = ClassWrapper::constructor_object(53); + assert_eq!(rd!(c).constant, int!(42)); + assert_eq!(read_field!(rd!(c).t), 53); + assert_eq!(read_field!(rd!(c).x), int!(0)); + assert_eq!(read_field!(rd!(rd!(c).next).t), 53); + assert_eq!(rd!(c).constant_plus_x(), int!(42)); + md!(c).increment_x(); + assert_eq!(rd!(c).constant_plus_x(), int!(43)); + modify_field!(rd!(c).x,int!(40)); + assert_eq!(rd!(c).constant_plus_x(), int!(82)); + modify_field!(rd!(c).t,54); + assert_eq!(read_field!(rd!(c).t), 54); + } + // Requires test1 || test2 // We will not do that as it enables the compiler to assume that t contains a valid Rc when it does not. // Prefer MaybePlacebo diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/avoid_soundness_mut.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/avoid_soundness_mut.dfy new file mode 100644 index 00000000000..2335ca7bd41 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/avoid_soundness_mut.dfy @@ -0,0 +1,44 @@ +// RUN: %baredafny build -t:rs "%s" +// RUN: "%S/avoid_soundness_mut-rust/cargo" run --release > "%t" +// RUN: %diff "%s.expect" "%t" +// RUN: %baredafny build -t:rs --raw-pointers "%s" +// RUN: "%S/avoid_soundness_mut-rust/cargo" run --release > "%t" +// RUN: %diff "%s.expect" "%t" + +newtype u8 = x: int | 0 <= x < 256 + +class X { + var x: u8 + constructor() { + x := 0; + } + + method DoBoth(other: X) + modifies this, other + requires this == other + { + this.x := 0; + other.x := 1; + if this.x == 1 { + print "Correct\n"; + } else { + assert false; + print "Soundness issue\n"; + } + } +} + +method Main() { + var c := new X(); + c.DoBoth(c); + + var other := c; + c.x := 0; + other.x := 1; + if c.x == 1 { + print "Correct\n"; + } else { + assert false; + print "Soundness issue\n"; + } +} \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/avoid_soundness_mut.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/avoid_soundness_mut.dfy.expect new file mode 100644 index 00000000000..09acc484713 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/avoid_soundness_mut.dfy.expect @@ -0,0 +1,2 @@ +Correct +Correct diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/externalclasses.rs b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/externalclasses.rs index 9b207e2af1b..e061478f099 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/externalclasses.rs +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/externalclasses.rs @@ -83,14 +83,14 @@ pub mod DafnyLibraries { pub mod ExternModuleWithOneClassToImport { pub struct NonShareableBox { - s: ::dafny_runtime::DafnyString + s: ::dafny_runtime::Field<::dafny_runtime::DafnyString> } impl NonShareableBox { pub fn _allocate_object() -> ::dafny_runtime::Object { // SAFETY: The Rc has not been shared before unsafe { ::dafny_runtime::Object::from_rc(::std::rc::Rc::new(NonShareableBox { - s: ::dafny_runtime::string_of("") + s: ::dafny_runtime::Field::new(::dafny_runtime::string_of("")) })) } } @@ -98,10 +98,10 @@ pub mod ExternModuleWithOneClassToImport { impl crate::ExternModuleWithOneClassToImport::TraitDefinedInModule for NonShareableBox { fn Get(&self) -> ::dafny_runtime::DafnyString { - self.s.clone() + ::dafny_runtime::read_field!(self.s) } - fn Put(&mut self, c: &::dafny_runtime::DafnyString) { - self.s = c.clone(); + fn Put(&self, c: &::dafny_runtime::DafnyString) { + ::dafny_runtime::modify_field!(self.s, c.clone()); } } } \ No newline at end of file