From 7c8d40f3f7f13953b7b52a1d5a6fc0e43e9e55d3 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Thu, 17 Oct 2024 19:10:51 +0200 Subject: [PATCH 1/2] chore: `apt-get update` before `apt-get install` (#5839) --- .github/workflows/doc-tests.yml | 2 +- .github/workflows/integration-tests-reusable.yml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/doc-tests.yml b/.github/workflows/doc-tests.yml index c6a68115327..212fe5d6520 100644 --- a/.github/workflows/doc-tests.yml +++ b/.github/workflows/doc-tests.yml @@ -37,7 +37,7 @@ jobs: path: dafny - name: Load Z3 run: | - sudo apt-get install -qq libarchive-tools + sudo apt-get update && sudo apt-get install -qq libarchive-tools mkdir -p dafny/Binaries/z3/bin wget -qO- https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-x64-ubuntu-20.04-bin.zip | bsdtar -xf - mv z3-* dafny/Binaries/z3/bin/ diff --git a/.github/workflows/integration-tests-reusable.yml b/.github/workflows/integration-tests-reusable.yml index 7dc0d80617f..3df76e1caea 100644 --- a/.github/workflows/integration-tests-reusable.yml +++ b/.github/workflows/integration-tests-reusable.yml @@ -142,7 +142,7 @@ jobs: - name: Load Z3 if: "!inputs.all_platforms" run: | - sudo apt-get install -qq libarchive-tools + sudo apt-get update && sudo apt-get install -qq libarchive-tools mkdir -p dafny/Binaries/z3/bin wget -qO- https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-x64-ubuntu-20.04-bin.zip | bsdtar -xf - mv z3-4.12.1 dafny/Binaries/z3/bin/ From eb924089777cdb5652b09763c9a096782ea74bca Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= Date: Thu, 17 Oct 2024 12:55:02 -0500 Subject: [PATCH 2/2] Fix: Constant initialization in the Dafny-to-Rust code generator (#5837) Fixes #5833 ### Description There are now three kinds of generated fields: * Internal constant fields (internal const): They have the same type and assigned and read using regular field read and field update. * Mutable fields (var): They are wrapped with `::dafny_runtime::Field<...>` to avoid any soundness issue, and use the wrappers `read_field` and `modify_field` to read and modify them. * Constant fields (const): They are called with a function call with zero argument. Before this PR, only the last two were implemented, which lead to issues when trying to assign the default value of a class constant. This issue was not captured because the test started to fail but since it's was marked `%testForEachCompiler` and these tests are ignored in the CI, we did not detect it. ### How has this been tested? Updated the file classes.dfy. All other tests in comp/rust should pass. By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt). --- Source/DafnyCore/Backends/Dafny/AST.dfy | 11 +- .../Backends/Dafny/DafnyCodeGenerator.cs | 20 ++- .../Backends/Rust/Dafny-compiler-rust.dfy | 23 +-- Source/DafnyCore/GeneratedFromDafny/DAST.cs | 156 +++++++++++++++--- Source/DafnyCore/GeneratedFromDafny/DCOMP.cs | 94 ++++++----- .../LitTests/LitTest/comp/rust/classes.dfy | 7 +- 6 files changed, 230 insertions(+), 81 deletions(-) diff --git a/Source/DafnyCore/Backends/Dafny/AST.dfy b/Source/DafnyCore/Backends/Dafny/AST.dfy index 6e0b149dff4..4c0e1272daf 100644 --- a/Source/DafnyCore/Backends/Dafny/AST.dfy +++ b/Source/DafnyCore/Backends/Dafny/AST.dfy @@ -300,7 +300,7 @@ module {:extern "DAST"} DAST { MapKeys(expr: Expression) | MapValues(expr: Expression) | MapItems(expr: Expression) | - Select(expr: Expression, field: VarName, isConstant: bool, onDatatype: bool, fieldType: Type) | + Select(expr: Expression, field: VarName, fieldMutability: FieldMutability, isDatatype: bool, fieldType: Type) | SelectFn(expr: Expression, field: VarName, onDatatype: bool, isStatic: bool, isConstant: bool, arguments: seq) | Index(expr: Expression, collKind: CollKind, indices: seq) | IndexRange(expr: Expression, isArray: bool, low: Option, high: Option) | @@ -323,6 +323,15 @@ module {:extern "DAST"} DAST { UnboundedIntRange(start: Expression, up: bool) | Quantifier(elemType: Type, collection: Expression, is_forall: bool, lambda: Expression) + // Since constant fields need to be set up in the constructor, + // accessing constant fields is done in two ways: + // - The internal field access (through the internal field that contains the value of the constant) + // it's not initialized at the beginning of the constructor + // - The external field access (through a function), which when accessed + // must always be initialized + // For Select expressions, it's important to know how the field is being accessed + // For mutable fields, there is no wrapping function so only one way to access the mutable field + datatype FieldMutability = ConstantField | InternalClassConstantField | ClassMutableField datatype UnaryOp = Not | BitwiseNot | Cardinality datatype Literal = diff --git a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs index 18e17532882..45a3bda471a 100644 --- a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs @@ -674,7 +674,7 @@ public void DeclareField(string name, TopLevelDecl enclosingDecl, bool isStatic, Sequence.UnicodeFromString(name), compiler.GenType(type), compiler.ParseAttributes(field.Attributes) - ), isConst, rhsExpr); + ), isConst || field is ConstantField, rhsExpr); } public void InitializeField(Field field, Type instantiatedFieldType, TopLevelDeclWithMembers enclosingClass) { @@ -1930,7 +1930,7 @@ protected override ILvalue EmitMemberSelect(Action obj, Type return new ExprLvalue((DAST.Expression)DAST.Expression.create_Select( objExpr, Sequence.UnicodeFromString(compileName), - member is ConstantField, + FieldMutabilityOf(member), member.EnclosingClass is DatatypeDecl, GenType(expectedType) ), (DAST.AssignLhs)DAST.AssignLhs.create_Select( objExpr, @@ -1975,7 +1975,7 @@ member is ConstantField return new ExprLvalue((DAST.Expression)DAST.Expression.create_Select( objExpr, Sequence.UnicodeFromString(compiledName), - member is ConstantField, + FieldMutabilityOf(member), member.EnclosingClass is DatatypeDecl, GenType(expectedType) ), (DAST.AssignLhs)DAST.AssignLhs.create_Select( objExpr, @@ -2008,7 +2008,7 @@ member is ConstantField return new ExprLvalue((DAST.Expression)DAST.Expression.create_Select( objExpr, Sequence.UnicodeFromString(InternalFieldPrefix + member.GetCompileName(Options)), - false, + FieldMutabilityOf(member, isInternal: true), member.EnclosingClass is DatatypeDecl, GenType(expectedType) ), (DAST.AssignLhs)DAST.AssignLhs.create_Select( objExpr, @@ -2019,7 +2019,7 @@ member is ConstantField return new ExprLvalue((DAST.Expression)DAST.Expression.create_Select( objExpr, Sequence.UnicodeFromString(member.GetCompileName(Options)), - member is ConstantField, + FieldMutabilityOf(member), member.EnclosingClass is DatatypeDecl, GenType(expectedType) ), (DAST.AssignLhs)DAST.AssignLhs.create_Select( objExpr, @@ -2030,6 +2030,14 @@ member is ConstantField } } + private static _IFieldMutability FieldMutabilityOf(MemberDecl member, bool isInternal = false) { + return member is ConstantField + ? isInternal + ? new FieldMutability_InternalClassConstantField() + : new FieldMutability_ConstantField() + : new FieldMutability_ClassMutableField(); + } + protected override ConcreteSyntaxTree EmitArraySelect(List> indices, Type elmtType, ConcreteSyntaxTree wr) { if (GetExprBuilder(wr, out var builder)) { var indicesAST = indices.Select(i => { @@ -2293,7 +2301,7 @@ protected override void EmitDestructor(Action source, Formal builder.Builder.AddExpr((DAST.Expression)DAST.Expression.create_Select( sourceAST, Sequence.UnicodeFromString(compileName), - false, + new FieldMutability_ConstantField(), true, GenType(dtor.Type) )); } diff --git a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy index 6583dfeae97..b77139a0f79 100644 --- a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy +++ b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy @@ -38,8 +38,8 @@ module {:extern "DCOMP"} DafnyToRustCompiler { 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() + const modify_mutable_field_macro := R.dafny_runtime.MSel("modify_field!").AsExpr() + const read_mutable_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) @@ -1613,13 +1613,13 @@ module {:extern "DCOMP"} DafnyToRustCompiler { newEnv := newEnv.RemoveAssigned(isAssignedVar); } else { // Already assigned, safe to override - generated := modify_field_macro.Apply([read_macro.Apply1(thisInConstructor).Sel(fieldName), rhs]); + generated := modify_mutable_field_macro.Apply([read_macro.Apply1(thisInConstructor).Sel(fieldName), rhs]); } case _ => if onExpr != R.Identifier("self") { onExpr := read_macro.Apply1(onExpr); } - generated := modify_field_macro.Apply([onExpr.Sel(fieldName), rhs]); + generated := modify_mutable_field_macro.Apply([onExpr.Sel(fieldName), rhs]); } readIdents := recIdents; needsIIFE := false; @@ -3265,7 +3265,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler { readIdents := recIdents; return; } - case Select(on, field, isConstant, isDatatype, fieldType) => { + case Select(on, field, fieldMutability, isDatatype, fieldType) => { if on.Companion? || on.ExternCompanion? { var onExpr, onOwned, recIdents := GenExpr(on, selfIdent, env, OwnershipAutoBorrowed); @@ -3298,11 +3298,14 @@ module {:extern "DCOMP"} DafnyToRustCompiler { r := read_macro.Apply1(r); } 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. + match fieldMutability { + case ConstantField() => + r := r.Apply0(); + r := r.Clone(); + case InternalClassConstantField() => + r := r.Clone(); + case ClassMutableField() => + r := read_mutable_field_macro.Apply1(r); // Already contains a clone. } r, resultingOwnership := FromOwned(r, expectedOwnership); readIdents := recIdents; diff --git a/Source/DafnyCore/GeneratedFromDafny/DAST.cs b/Source/DafnyCore/GeneratedFromDafny/DAST.cs index 6a53b8f6762..2ba103165a0 100644 --- a/Source/DafnyCore/GeneratedFromDafny/DAST.cs +++ b/Source/DafnyCore/GeneratedFromDafny/DAST.cs @@ -6013,10 +6013,12 @@ public interface _IExpression { BigInteger dtor_dim { get; } bool dtor_native { get; } Dafny.ISequence dtor_field { get; } - bool dtor_isConstant { get; } - bool dtor_onDatatype { get; } + DAST._IFieldMutability dtor_fieldMutability { get; } + bool dtor_isDatatype { get; } DAST._IType dtor_fieldType { get; } + bool dtor_onDatatype { get; } bool dtor_isStatic { get; } + bool dtor_isConstant { get; } Dafny.ISequence dtor_arguments { get; } DAST._ICollKind dtor_collKind { get; } Dafny.ISequence dtor_indices { get; } @@ -6144,8 +6146,8 @@ public static _IExpression create_MapValues(DAST._IExpression expr) { public static _IExpression create_MapItems(DAST._IExpression expr) { return new Expression_MapItems(expr); } - public static _IExpression create_Select(DAST._IExpression expr, Dafny.ISequence field, bool isConstant, bool onDatatype, DAST._IType fieldType) { - return new Expression_Select(expr, field, isConstant, onDatatype, fieldType); + public static _IExpression create_Select(DAST._IExpression expr, Dafny.ISequence field, DAST._IFieldMutability fieldMutability, bool isDatatype, DAST._IType fieldType) { + return new Expression_Select(expr, field, fieldMutability, isDatatype, fieldType); } public static _IExpression create_SelectFn(DAST._IExpression expr, Dafny.ISequence field, bool onDatatype, bool isStatic, bool isConstant, Dafny.ISequence arguments) { return new Expression_SelectFn(expr, field, onDatatype, isStatic, isConstant, arguments); @@ -6531,18 +6533,16 @@ public Dafny.ISequence dtor_field { return ((Expression_SelectFn)d)._field; } } - public bool dtor_isConstant { + public DAST._IFieldMutability dtor_fieldMutability { get { var d = this; - if (d is Expression_Select) { return ((Expression_Select)d)._isConstant; } - return ((Expression_SelectFn)d)._isConstant; + return ((Expression_Select)d)._fieldMutability; } } - public bool dtor_onDatatype { + public bool dtor_isDatatype { get { var d = this; - if (d is Expression_Select) { return ((Expression_Select)d)._onDatatype; } - return ((Expression_SelectFn)d)._onDatatype; + return ((Expression_Select)d)._isDatatype; } } public DAST._IType dtor_fieldType { @@ -6552,12 +6552,24 @@ public DAST._IType dtor_fieldType { return ((Expression_TupleSelect)d)._fieldType; } } + public bool dtor_onDatatype { + get { + var d = this; + return ((Expression_SelectFn)d)._onDatatype; + } + } public bool dtor_isStatic { get { var d = this; return ((Expression_SelectFn)d)._isStatic; } } + public bool dtor_isConstant { + get { + var d = this; + return ((Expression_SelectFn)d)._isConstant; + } + } public Dafny.ISequence dtor_arguments { get { var d = this; @@ -7650,31 +7662,31 @@ public override string ToString() { public class Expression_Select : Expression { public readonly DAST._IExpression _expr; public readonly Dafny.ISequence _field; - public readonly bool _isConstant; - public readonly bool _onDatatype; + public readonly DAST._IFieldMutability _fieldMutability; + public readonly bool _isDatatype; public readonly DAST._IType _fieldType; - public Expression_Select(DAST._IExpression expr, Dafny.ISequence field, bool isConstant, bool onDatatype, DAST._IType fieldType) : base() { + public Expression_Select(DAST._IExpression expr, Dafny.ISequence field, DAST._IFieldMutability fieldMutability, bool isDatatype, DAST._IType fieldType) : base() { this._expr = expr; this._field = field; - this._isConstant = isConstant; - this._onDatatype = onDatatype; + this._fieldMutability = fieldMutability; + this._isDatatype = isDatatype; this._fieldType = fieldType; } public override _IExpression DowncastClone() { if (this is _IExpression dt) { return dt; } - return new Expression_Select(_expr, _field, _isConstant, _onDatatype, _fieldType); + return new Expression_Select(_expr, _field, _fieldMutability, _isDatatype, _fieldType); } public override bool Equals(object other) { var oth = other as DAST.Expression_Select; - return oth != null && object.Equals(this._expr, oth._expr) && object.Equals(this._field, oth._field) && this._isConstant == oth._isConstant && this._onDatatype == oth._onDatatype && object.Equals(this._fieldType, oth._fieldType); + return oth != null && object.Equals(this._expr, oth._expr) && object.Equals(this._field, oth._field) && object.Equals(this._fieldMutability, oth._fieldMutability) && this._isDatatype == oth._isDatatype && object.Equals(this._fieldType, oth._fieldType); } public override int GetHashCode() { ulong hash = 5381; hash = ((hash << 5) + hash) + 29; 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)); - hash = ((hash << 5) + hash) + ((ulong)Dafny.Helpers.GetHashCode(this._onDatatype)); + hash = ((hash << 5) + hash) + ((ulong)Dafny.Helpers.GetHashCode(this._fieldMutability)); + hash = ((hash << 5) + hash) + ((ulong)Dafny.Helpers.GetHashCode(this._isDatatype)); hash = ((hash << 5) + hash) + ((ulong)Dafny.Helpers.GetHashCode(this._fieldType)); return (int) hash; } @@ -7685,9 +7697,9 @@ public override string ToString() { s += ", "; s += Dafny.Helpers.ToString(this._field); s += ", "; - s += Dafny.Helpers.ToString(this._isConstant); + s += Dafny.Helpers.ToString(this._fieldMutability); s += ", "; - s += Dafny.Helpers.ToString(this._onDatatype); + s += Dafny.Helpers.ToString(this._isDatatype); s += ", "; s += Dafny.Helpers.ToString(this._fieldType); s += ")"; @@ -8436,6 +8448,108 @@ public override string ToString() { } } + public interface _IFieldMutability { + bool is_ConstantField { get; } + bool is_InternalClassConstantField { get; } + bool is_ClassMutableField { get; } + _IFieldMutability DowncastClone(); + } + public abstract class FieldMutability : _IFieldMutability { + public FieldMutability() { + } + private static readonly DAST._IFieldMutability theDefault = create_ConstantField(); + public static DAST._IFieldMutability Default() { + return theDefault; + } + private static readonly Dafny.TypeDescriptor _TYPE = new Dafny.TypeDescriptor(DAST.FieldMutability.Default()); + public static Dafny.TypeDescriptor _TypeDescriptor() { + return _TYPE; + } + public static _IFieldMutability create_ConstantField() { + return new FieldMutability_ConstantField(); + } + public static _IFieldMutability create_InternalClassConstantField() { + return new FieldMutability_InternalClassConstantField(); + } + public static _IFieldMutability create_ClassMutableField() { + return new FieldMutability_ClassMutableField(); + } + public bool is_ConstantField { get { return this is FieldMutability_ConstantField; } } + public bool is_InternalClassConstantField { get { return this is FieldMutability_InternalClassConstantField; } } + public bool is_ClassMutableField { get { return this is FieldMutability_ClassMutableField; } } + public static System.Collections.Generic.IEnumerable<_IFieldMutability> AllSingletonConstructors { + get { + yield return FieldMutability.create_ConstantField(); + yield return FieldMutability.create_InternalClassConstantField(); + yield return FieldMutability.create_ClassMutableField(); + } + } + public abstract _IFieldMutability DowncastClone(); + } + public class FieldMutability_ConstantField : FieldMutability { + public FieldMutability_ConstantField() : base() { + } + public override _IFieldMutability DowncastClone() { + if (this is _IFieldMutability dt) { return dt; } + return new FieldMutability_ConstantField(); + } + public override bool Equals(object other) { + var oth = other as DAST.FieldMutability_ConstantField; + return oth != null; + } + public override int GetHashCode() { + ulong hash = 5381; + hash = ((hash << 5) + hash) + 0; + return (int) hash; + } + public override string ToString() { + string s = "DAST.FieldMutability.ConstantField"; + return s; + } + } + public class FieldMutability_InternalClassConstantField : FieldMutability { + public FieldMutability_InternalClassConstantField() : base() { + } + public override _IFieldMutability DowncastClone() { + if (this is _IFieldMutability dt) { return dt; } + return new FieldMutability_InternalClassConstantField(); + } + public override bool Equals(object other) { + var oth = other as DAST.FieldMutability_InternalClassConstantField; + return oth != null; + } + public override int GetHashCode() { + ulong hash = 5381; + hash = ((hash << 5) + hash) + 1; + return (int) hash; + } + public override string ToString() { + string s = "DAST.FieldMutability.InternalClassConstantField"; + return s; + } + } + public class FieldMutability_ClassMutableField : FieldMutability { + public FieldMutability_ClassMutableField() : base() { + } + public override _IFieldMutability DowncastClone() { + if (this is _IFieldMutability dt) { return dt; } + return new FieldMutability_ClassMutableField(); + } + public override bool Equals(object other) { + var oth = other as DAST.FieldMutability_ClassMutableField; + return oth != null; + } + public override int GetHashCode() { + ulong hash = 5381; + hash = ((hash << 5) + hash) + 2; + return (int) hash; + } + public override string ToString() { + string s = "DAST.FieldMutability.ClassMutableField"; + return s; + } + } + public interface _IUnaryOp { bool is_Not { get; } bool is_BitwiseNot { get; } diff --git a/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs b/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs index 0998dea6b4e..9158c6ca83b 100644 --- a/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs +++ b/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs @@ -2007,7 +2007,7 @@ public void GenAssignLhs(DAST._IAssignLhs lhs, RAST._IExpr rhs, Defs._ISelfInfo 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 = ((this).modify__field__macro).Apply(Dafny.Sequence.FromElements((((this).read__macro).Apply1((this).thisInConstructor)).Sel(_5_fieldName), rhs)); + generated = ((this).modify__mutable__field__macro).Apply(Dafny.Sequence.FromElements((((this).read__macro).Apply1((this).thisInConstructor)).Sel(_5_fieldName), rhs)); } goto after_match1; } @@ -2016,7 +2016,7 @@ public void GenAssignLhs(DAST._IAssignLhs lhs, RAST._IExpr rhs, Defs._ISelfInfo if (!object.Equals(_6_onExpr, RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("self")))) { _6_onExpr = ((this).read__macro).Apply1(_6_onExpr); } - generated = ((this).modify__field__macro).Apply(Dafny.Sequence.FromElements((_6_onExpr).Sel(_5_fieldName), rhs)); + generated = ((this).modify__mutable__field__macro).Apply(Dafny.Sequence.FromElements((_6_onExpr).Sel(_5_fieldName), rhs)); } after_match1: ; readIdents = _8_recIdents; @@ -5485,8 +5485,8 @@ public void GenExpr(DAST._IExpression e, Defs._ISelfInfo selfIdent, Defs._IEnvir if (_source0.is_Select) { DAST._IExpression _218_on = _source0.dtor_expr; Dafny.ISequence _219_field = _source0.dtor_field; - bool _220_isConstant = _source0.dtor_isConstant; - bool _221_isDatatype = _source0.dtor_onDatatype; + DAST._IFieldMutability _220_fieldMutability = _source0.dtor_fieldMutability; + bool _221_isDatatype = _source0.dtor_isDatatype; DAST._IType _222_fieldType = _source0.dtor_fieldType; { if (((_218_on).is_Companion) || ((_218_on).is_ExternCompanion)) { @@ -5568,12 +5568,24 @@ public void GenExpr(DAST._IExpression e, Defs._ISelfInfo selfIdent, Defs._IEnvir r = ((this).read__macro).Apply1(r); } 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); + DAST._IFieldMutability _source3 = _220_fieldMutability; + { + if (_source3.is_ConstantField) { + r = (r).Apply0(); + r = (r).Clone(); + goto after_match3; + } } + { + if (_source3.is_InternalClassConstantField) { + r = (r).Clone(); + goto after_match3; + } + } + { + r = ((this).read__mutable__field__macro).Apply1(r); + } + after_match3: ; RAST._IExpr _out200; Defs._IOwnership _out201; (this).FromOwned(r, expectedOwnership, out _out200, out _out201); @@ -5699,10 +5711,10 @@ public void GenExpr(DAST._IExpression e, Defs._ISelfInfo selfIdent, Defs._IEnvir } Dafny.ISequence _256_arguments; _256_arguments = Dafny.Sequence.FromElements(); - Std.Wrappers._IOption _source3 = _249_low; + Std.Wrappers._IOption _source4 = _249_low; { - if (_source3.is_Some) { - DAST._IExpression _257_l = _source3.dtor_value; + if (_source4.is_Some) { + DAST._IExpression _257_l = _source4.dtor_value; { RAST._IExpr _258_lExpr; Defs._IOwnership _259___v146; @@ -5717,16 +5729,16 @@ public void GenExpr(DAST._IExpression e, Defs._ISelfInfo selfIdent, Defs._IEnvir _256_arguments = Dafny.Sequence.Concat(_256_arguments, Dafny.Sequence.FromElements(_258_lExpr)); readIdents = Dafny.Set>.Union(readIdents, _260_recIdentsL); } - goto after_match3; + goto after_match4; } } { } - after_match3: ; - Std.Wrappers._IOption _source4 = _250_high; + after_match4: ; + Std.Wrappers._IOption _source5 = _250_high; { - if (_source4.is_Some) { - DAST._IExpression _261_h = _source4.dtor_value; + if (_source5.is_Some) { + DAST._IExpression _261_h = _source5.dtor_value; { RAST._IExpr _262_hExpr; Defs._IOwnership _263___v147; @@ -5741,12 +5753,12 @@ public void GenExpr(DAST._IExpression e, Defs._ISelfInfo selfIdent, Defs._IEnvir _256_arguments = Dafny.Sequence.Concat(_256_arguments, Dafny.Sequence.FromElements(_262_hExpr)); readIdents = Dafny.Set>.Union(readIdents, _264_recIdentsH); } - goto after_match4; + goto after_match5; } } { } - after_match4: ; + after_match5: ; r = _252_onExpr; if (_248_isArray) { if (!(_255_methodName).Equals(Dafny.Sequence.UnicodeFromString(""))) { @@ -5794,19 +5806,19 @@ public void GenExpr(DAST._IExpression e, Defs._ISelfInfo selfIdent, Defs._IEnvir _271_recIdents = _out226; Dafny.ISequence _272_selName; _272_selName = Std.Strings.__default.OfNat(_267_idx); - DAST._IType _source5 = _268_fieldType; + DAST._IType _source6 = _268_fieldType; { - if (_source5.is_Tuple) { - Dafny.ISequence _273_tps = _source5.dtor_Tuple_a0; + if (_source6.is_Tuple) { + Dafny.ISequence _273_tps = _source6.dtor_Tuple_a0; if (((_268_fieldType).is_Tuple) && ((new BigInteger((_273_tps).Count)) > (RAST.__default.MAX__TUPLE__SIZE))) { _272_selName = Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("_"), _272_selName); } - goto after_match5; + goto after_match6; } } { } - after_match5: ; + after_match6: ; r = ((_269_onExpr).Sel(_272_selName)).Clone(); RAST._IExpr _out227; Defs._IOwnership _out228; @@ -5840,10 +5852,10 @@ public void GenExpr(DAST._IExpression e, Defs._ISelfInfo selfIdent, Defs._IEnvir _280_typeExprs = _out231; _281_fullNameQualifier = _out232; readIdents = _279_recIdents; - Std.Wrappers._IOption _source6 = _281_fullNameQualifier; + Std.Wrappers._IOption _source7 = _281_fullNameQualifier; { - if (_source6.is_Some) { - DAST._IResolvedType value0 = _source6.dtor_value; + if (_source7.is_Some) { + DAST._IResolvedType value0 = _source7.dtor_value; Dafny.ISequence> _282_path = value0.dtor_path; Dafny.ISequence _283_onTypeArgs = value0.dtor_typeArgs; DAST._IResolvedTypeBase _284_base = value0.dtor_kind; @@ -5884,7 +5896,7 @@ public void GenExpr(DAST._IExpression e, Defs._ISelfInfo selfIdent, Defs._IEnvir (this).FromOwned(r, expectedOwnership, out _out241, out _out242); r = _out241; resultingOwnership = _out242; - goto after_match6; + goto after_match7; } } { @@ -5901,29 +5913,29 @@ public void GenExpr(DAST._IExpression e, Defs._ISelfInfo selfIdent, Defs._IEnvir readIdents = Dafny.Set>.Union(readIdents, _292_recIdents); Dafny.ISequence _293_renderedName; _293_renderedName = (this).GetMethodName(_274_on, _275_name); - DAST._IExpression _source7 = _274_on; + DAST._IExpression _source8 = _274_on; { bool disjunctiveMatch0 = false; - if (_source7.is_Companion) { + if (_source8.is_Companion) { disjunctiveMatch0 = true; } - if (_source7.is_ExternCompanion) { + if (_source8.is_ExternCompanion) { disjunctiveMatch0 = true; } if (disjunctiveMatch0) { { _290_onExpr = (_290_onExpr).FSel(_293_renderedName); } - goto after_match7; + goto after_match8; } } { { if (!object.Equals(_290_onExpr, RAST.__default.self)) { - DAST._ICallName _source8 = _275_name; + DAST._ICallName _source9 = _275_name; { - if (_source8.is_CallName) { - Std.Wrappers._IOption onType0 = _source8.dtor_onType; + if (_source9.is_CallName) { + Std.Wrappers._IOption onType0 = _source9.dtor_onType; if (onType0.is_Some) { DAST._IType _294_tpe = onType0.dtor_value; RAST._IType _295_typ; @@ -5933,18 +5945,18 @@ public void GenExpr(DAST._IExpression e, Defs._ISelfInfo selfIdent, Defs._IEnvir if ((_295_typ).IsObjectOrPointer()) { _290_onExpr = ((this).read__macro).Apply1(_290_onExpr); } - goto after_match8; + goto after_match9; } } } { } - after_match8: ; + after_match9: ; } _290_onExpr = (_290_onExpr).Sel(_293_renderedName); } } - after_match7: ; + after_match8: ; r = ((_290_onExpr).ApplyType(_280_typeExprs)).Apply(_278_argExprs); RAST._IExpr _out247; Defs._IOwnership _out248; @@ -5953,7 +5965,7 @@ public void GenExpr(DAST._IExpression e, Defs._ISelfInfo selfIdent, Defs._IEnvir resultingOwnership = _out248; return ; } - after_match6: ; + after_match7: ; } goto after_match0; } @@ -6848,10 +6860,10 @@ public Dafny.ISequence downcast { get { return Dafny.Sequence.UnicodeFromString("cast_object!"); } } } - public RAST._IExpr read__field__macro { get { + public RAST._IExpr read__mutable__field__macro { get { return ((RAST.__default.dafny__runtime).MSel(Dafny.Sequence.UnicodeFromString("read_field!"))).AsExpr(); } } - public RAST._IExpr modify__field__macro { get { + public RAST._IExpr modify__mutable__field__macro { get { return ((RAST.__default.dafny__runtime).MSel(Dafny.Sequence.UnicodeFromString("modify_field!"))).AsExpr(); } } } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/classes.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/classes.dfy index 6086f7a6b19..3bc5b6caeb3 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/classes.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/classes.dfy @@ -7,13 +7,16 @@ class Y { var c: int ghost var Repr: set - constructor(c: int) ensures this.c == c { + const d: int + constructor(c: int) ensures this.c == c && d == c { this.c := c; + this.d := c; this.Repr := {this}; } - constructor Two() ensures c == 2 { + constructor Two() ensures c == 2 == d { this.c := 2; + this.d := c; this.Repr := {this}; } }