Fix: Recursive constant initialization was not checked if in constructor

RELEASE_NOTES.md

@@ -1,5 +1,6 @@
 # Upcoming
 
+- fix: Constant initialization checked for recursion (https://github.com/dafny-lang/dafny/pull/2862)
 - fix: Compiled lambdas now close only on non-ghost variables (https://github.com/dafny-lang/dafny/pull/2854)
 - fix: Crash in the LSP in some code that does not parse (https://github.com/dafny-lang/dafny/pull/2833)
 

Source/DafnyCore/DafnyCore.csproj

@@ -3,7 +3,7 @@
   <Target Name="RunCoco" BeforeTargets="PreBuildEvent" Outputs="$(ProjectDir)Parser.cs;$(ProjectDir)Scanner.cs" Inputs="$(ProjectDir)Dafny.atg">
     <Exec Command="dotnet tool restore" />
     <Exec Command="dotnet --info" />
-    <Exec Command="dotnet tool run coco $(ProjectDir)Dafny.atg -namespace Microsoft.Dafny -frames &quot;$(ProjectDir)Coco&quot;" />
+    <Exec Command="dotnet tool run coco &quot;$(ProjectDir)Dafny.atg&quot; -namespace Microsoft.Dafny -frames &quot;$(ProjectDir)Coco&quot;" />
     <!-- Recompute files to build according to https://stackoverflow.com/a/44829863/93197 -->
     <ItemGroup>
       <Compile Include="**/*$(DefaultLanguageSourceExtension)" Exclude="$(DefaultItemExcludes);$(DefaultExcludesInProjectFolder);$(BaseIntermediateOutputPath)**;$(BaseOutputPath)**;@(Compile)" />

Source/DafnyCore/Resolver.cs

@@ -2846,7 +2846,7 @@ public void ResolveTopLevelDecls_Core(List<TopLevelDecl/*!*/>/*!*/ declarations,
       }
 
       // ---------------------------------- Pass 1 ----------------------------------
-      // This pass:
+      // This pass or phase:
       // * checks that type inference was able to determine all types
       // * check that shared destructors in datatypes are in agreement
       // * fills in the .ResolvedOp field of binary expressions
@@ -13768,8 +13768,65 @@ void ResolveBlockStatement(BlockStmt blockStmt, ResolutionContext resolutionCont
         var div = (DividedBlockStmt)blockStmt;
         Contract.Assert(currentMethod is Constructor);  // divided bodies occur only in class constructors
         Contract.Assert(!resolutionContext.InFirstPhaseConstructor);  // divided bodies are never nested
+        // In the first phase of the constructor, we keep track of constants which are fully determined.
+        // We prevent the reading of constants which have dependencies that are yet unassigned constants
+        var constantsAlreadyAssigned = new HashSet<ConstantField>();
+        var constantsWithErrors = new HashSet<ConstantField>();
+
+        // Returns an error if the expression cannot be fully determined
+        (string, ConstantField)? GetErrorIfNotFullyDetermined(Expression expr, List<ConstantField> visited) {
+          if (expr is MemberSelectExpr { Member: ConstantField field } memberSelectExpr && Expression.AsThis(memberSelectExpr.Obj) != null) {
+            if (visited.IndexOf(field) is var index && index >= 0) {
+              var msg = "Please break this constant initialization cycle: " + visited[index].Name;
+              for (var i = index + 1; i < visited.Count; i++) {
+                msg += " -> " + visited[i].Name;
+              }
+              msg += " -> " + field.Name;
+              return (msg, field);
+            }
+            if (field.Rhs == null && !constantsAlreadyAssigned.Contains(field)) {
+              var msg = "Missing initialization of field ";
+              for (var i = 0; i < visited.Count; i++) {
+                msg += (i == 0 ? "through the dependency " : "") + visited[i].Name + " -> ";
+              }
+              msg += field.Name + ", which needs to be assigned at this point.";
+              return (msg, field);
+            }
+            if (field.Rhs != null) {
+              foreach (var subExpr in field.Rhs.SubExpressions) {
+                if (GetErrorIfNotFullyDetermined(subExpr, visited.Append(field).ToList()) is var msgField && msgField != null) {
+                  return msgField;
+                }
+              }
+            }
+          }
+          foreach (var subExpr in expr.SubExpressions) {
+            if (GetErrorIfNotFullyDetermined(subExpr, visited) is var msgField && msgField != null) {
+              return msgField;
+            }
+          }
+
+          return null;
+        }
         foreach (Statement ss in div.BodyInit) {
           ResolveStatementWithLabels(ss, resolutionContext with { InFirstPhaseConstructor = true });
+          var subExpressions = (ss is UpdateStmt updateStmt
+            ? updateStmt.Rhss.SelectMany(rhs => rhs.SubExpressions).ToList()
+            : Microsoft.Dafny.Triggers.ExprExtensions.AllSubExpressions(ss, false, false));
+          foreach (var rhs in subExpressions) {
+            if (GetErrorIfNotFullyDetermined(rhs, new List<ConstantField>()) is var msgField && msgField != null &&
+                !constantsWithErrors.Contains(msgField.Value.Item2)) {
+              reporter.Error(MessageSource.Resolver, rhs, "Constant not initialized yet. " + msgField.Value.Item1);
+              constantsWithErrors.Add(msgField.Value.Item2);
+            }
+          }
+          if (ss is UpdateStmt updateStmt2) {
+            foreach (var lhs in updateStmt2.Lhss) {
+              if (lhs is MemberSelectExpr { Member: ConstantField { IsMutable: false } field } memberSelectExpr && Expression.AsThis(memberSelectExpr.Obj) != null) {
+                constantsAlreadyAssigned.Add(field);
+              }
+            }
+          }
         }
         foreach (Statement ss in div.BodyProper) {
           ResolveStatementWithLabels(ss, resolutionContext);

Test/git-issues/git-issue-2727.dfy

@@ -0,0 +1,34 @@
+// RUN: %dafny_0 -compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+class C {
+  const a := b + b
+  const b: int
+
+  constructor (x: int) {
+    var k := a;
+    print a, "\n";
+    b := x;
+    assert k == a;
+    print a, "\n";
+    if k != a {
+      var y := 5 / 0; // this can crash
+    }
+  }
+}
+
+class D {
+  const a: int := b
+  const b: int
+
+  constructor () {
+    b := a + 1;
+    new;
+    assert false;
+  }
+}
+
+method Main() {
+  var c := new C(5);
+  var d := new D();
+}

Test/git-issues/git-issue-2727.dfy.expect

@@ -0,0 +1,3 @@
+git-issue-2727.dfy(9,13): Error: Constant not initialized yet. Missing initialization of field through the dependency a -> b, which needs to be assigned at this point.
+git-issue-2727.dfy(25,11): Error: Constant not initialized yet. Missing initialization of field through the dependency a -> b, which needs to be assigned at this point.
+2 resolution/type errors detected in git-issue-2727.dfy