Fix: Constant initialization in the Dafny-to-Rust code generator

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<Type>) |
     Index(expr: Expression, collKind: CollKind, indices: seq<Expression>) |
     IndexRange(expr: Expression, isArray: bool, low: Option<Expression>, high: Option<Expression>) |
@@ -323,6 +323,7 @@ module {:extern "DAST"} DAST {
     UnboundedIntRange(start: Expression, up: bool) |
     Quantifier(elemType: Type, collection: Expression, is_forall: bool, lambda: Expression)
 
+  datatype FieldMutability = ConstantField | MutableField | InternalConstantField
   datatype UnaryOp = Not | BitwiseNot | Cardinality
 
   datatype Literal =

Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs

@@ -674,7 +674,7 @@ public void DeclareField(string name, TopLevelDecl enclosingDecl, bool isStatic,
           Sequence<Rune>.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<ConcreteSyntaxTree> obj, Type
           return new ExprLvalue((DAST.Expression)DAST.Expression.create_Select(
             objExpr,
             Sequence<Rune>.UnicodeFromString(compileName),
-            member is ConstantField,
+            member is ConstantField ? new FieldMutability_ConstantField() : new FieldMutability_MutableField(),
             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<Rune>.UnicodeFromString(compiledName),
-          member is ConstantField,
+          member is ConstantField ? new FieldMutability_ConstantField() : new FieldMutability_MutableField(),
           member.EnclosingClass is DatatypeDecl, GenType(expectedType)
         ), (DAST.AssignLhs)DAST.AssignLhs.create_Select(
           objExpr,
@@ -2008,7 +2008,8 @@ member is ConstantField
           return new ExprLvalue((DAST.Expression)DAST.Expression.create_Select(
             objExpr,
             Sequence<Rune>.UnicodeFromString(InternalFieldPrefix + member.GetCompileName(Options)),
-            false,
+            member is ConstantField ? new FieldMutability_InternalConstantField() :
+              new FieldMutability_MutableField(),
             member.EnclosingClass is DatatypeDecl, GenType(expectedType)
           ), (DAST.AssignLhs)DAST.AssignLhs.create_Select(
             objExpr,
@@ -2019,7 +2020,7 @@ member is ConstantField
           return new ExprLvalue((DAST.Expression)DAST.Expression.create_Select(
             objExpr,
             Sequence<Rune>.UnicodeFromString(member.GetCompileName(Options)),
-            member is ConstantField,
+            member is ConstantField ? new FieldMutability_ConstantField() : new FieldMutability_MutableField(),
             member.EnclosingClass is DatatypeDecl, GenType(expectedType)
           ), (DAST.AssignLhs)DAST.AssignLhs.create_Select(
             objExpr,
@@ -2293,7 +2294,7 @@ protected override void EmitDestructor(Action<ConcreteSyntaxTree> source, Formal
             builder.Builder.AddExpr((DAST.Expression)DAST.Expression.create_Select(
               sourceAST,
               Sequence<Rune>.UnicodeFromString(compileName),
-              false,
+              new FieldMutability_ConstantField(),
               true, GenType(dtor.Type)
             ));
           }

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 {
+            if fieldMutability.ConstantField? {
               r := r.Apply0();
               r := r.Clone(); // self could be &mut, so to avoid any borrow checker problem, we clone the value.
+            } else if fieldMutability.InternalConstantField? {
+              r := r.Clone();
             } else {
-              r := read_field_macro.Apply1(r); // Already contains a clone.
+              assert fieldMutability.MutableField?;
+              r := read_mutable_field_macro.Apply1(r); // Already contains a clone.
             }
             r, resultingOwnership := FromOwned(r, expectedOwnership);
             readIdents := recIdents;

Source/DafnyCore/GeneratedFromDafny/DAST.cs

@@ -6013,10 +6013,12 @@ public interface _IExpression {
     BigInteger dtor_dim { get; }
     bool dtor_native { get; }
     Dafny.ISequence<Dafny.Rune> 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<DAST._IType> dtor_arguments { get; }
     DAST._ICollKind dtor_collKind { get; }
     Dafny.ISequence<DAST._IExpression> 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<Dafny.Rune> 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<Dafny.Rune> 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<Dafny.Rune> field, bool onDatatype, bool isStatic, bool isConstant, Dafny.ISequence<DAST._IType> arguments) {
       return new Expression_SelectFn(expr, field, onDatatype, isStatic, isConstant, arguments);
@@ -6531,18 +6533,16 @@ public Dafny.ISequence<Dafny.Rune> 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<DAST._IType> 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<Dafny.Rune> _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<Dafny.Rune> field, bool isConstant, bool onDatatype, DAST._IType fieldType) : base() {
+    public Expression_Select(DAST._IExpression expr, Dafny.ISequence<Dafny.Rune> 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_MutableField { get; }
+    bool is_InternalConstantField { 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<DAST._IFieldMutability> _TYPE = new Dafny.TypeDescriptor<DAST._IFieldMutability>(DAST.FieldMutability.Default());
+    public static Dafny.TypeDescriptor<DAST._IFieldMutability> _TypeDescriptor() {
+      return _TYPE;
+    }
+    public static _IFieldMutability create_ConstantField() {
+      return new FieldMutability_ConstantField();
+    }
+    public static _IFieldMutability create_MutableField() {
+      return new FieldMutability_MutableField();
+    }
+    public static _IFieldMutability create_InternalConstantField() {
+      return new FieldMutability_InternalConstantField();
+    }
+    public bool is_ConstantField { get { return this is FieldMutability_ConstantField; } }
+    public bool is_MutableField { get { return this is FieldMutability_MutableField; } }
+    public bool is_InternalConstantField { get { return this is FieldMutability_InternalConstantField; } }
+    public static System.Collections.Generic.IEnumerable<_IFieldMutability> AllSingletonConstructors {
+      get {
+        yield return FieldMutability.create_ConstantField();
+        yield return FieldMutability.create_MutableField();
+        yield return FieldMutability.create_InternalConstantField();
+      }
+    }
+    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_MutableField : FieldMutability {
+    public FieldMutability_MutableField() : base() {
+    }
+    public override _IFieldMutability DowncastClone() {
+      if (this is _IFieldMutability dt) { return dt; }
+      return new FieldMutability_MutableField();
+    }
+    public override bool Equals(object other) {
+      var oth = other as DAST.FieldMutability_MutableField;
+      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.MutableField";
+      return s;
+    }
+  }
+  public class FieldMutability_InternalConstantField : FieldMutability {
+    public FieldMutability_InternalConstantField() : base() {
+    }
+    public override _IFieldMutability DowncastClone() {
+      if (this is _IFieldMutability dt) { return dt; }
+      return new FieldMutability_InternalConstantField();
+    }
+    public override bool Equals(object other) {
+      var oth = other as DAST.FieldMutability_InternalConstantField;
+      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.InternalConstantField";
+      return s;
+    }
+  }
+
   public interface _IUnaryOp {
     bool is_Not { get; }
     bool is_BitwiseNot { get; }