Merge branch 'master' into onlyClaimVerificationMemoryPerModule

.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/

.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/

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,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 =

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,
+            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<Rune>.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<Rune>.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<Rune>.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<Action<ConcreteSyntaxTree>> 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<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 {
-              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;