From 0b346978ffe19b26561a49f8d5ec1576cccc76df Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 7 Oct 2022 10:47:46 -0500 Subject: [PATCH 01/10] Fix: Recursive constant initialization was not checked if in constructor This PR fixes #2727 by adding an appropriate error message if constants are initialized in the wrong order. --- Source/DafnyCore/DafnyCore.csproj | 2 +- Source/DafnyCore/Resolver.cs | 59 ++++++++++++++++++++++- Test/git-issues/git-issue-2727.dfy | 34 +++++++++++++ Test/git-issues/git-issue-2727.dfy.expect | 3 ++ 4 files changed, 96 insertions(+), 2 deletions(-) create mode 100644 Test/git-issues/git-issue-2727.dfy create mode 100644 Test/git-issues/git-issue-2727.dfy.expect diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj index 5ce43807457..b97954843c9 100644 --- a/Source/DafnyCore/DafnyCore.csproj +++ b/Source/DafnyCore/DafnyCore.csproj @@ -3,7 +3,7 @@ - + diff --git a/Source/DafnyCore/Resolver.cs b/Source/DafnyCore/Resolver.cs index 7b2d4647d7f..6f8fd792d30 100644 --- a/Source/DafnyCore/Resolver.cs +++ b/Source/DafnyCore/Resolver.cs @@ -2846,7 +2846,7 @@ public void ResolveTopLevelDecls_Core(List/*!*/ 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(); + var constantsWithErrors = new HashSet(); + + // Returns an error if the expression cannot be fully determined + (string, ConstantField)? GetErrorIfNotFullyDetermined(Expression expr, List 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()) 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); diff --git a/Test/git-issues/git-issue-2727.dfy b/Test/git-issues/git-issue-2727.dfy new file mode 100644 index 00000000000..8689ce591cd --- /dev/null +++ b/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(); +} \ No newline at end of file diff --git a/Test/git-issues/git-issue-2727.dfy.expect b/Test/git-issues/git-issue-2727.dfy.expect new file mode 100644 index 00000000000..4db2cc8ad34 --- /dev/null +++ b/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 From dd2ec2e518db506ae46507e3d1d3c60fa6a4357f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= Date: Fri, 7 Oct 2022 10:51:50 -0500 Subject: [PATCH 02/10] Update RELEASE_NOTES.md --- RELEASE_NOTES.md | 1 + 1 file changed, 1 insertion(+) diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index cb6737b4a81..ccfd035578f 100644 --- a/RELEASE_NOTES.md +++ b/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) From 75344fb15bc475c1ae85c9418c2daa473f670f25 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 7 Oct 2022 14:37:14 -0500 Subject: [PATCH 03/10] Added review comment use case and fixed the code --- Source/DafnyCore/Resolver.cs | 5 ++++- Test/git-issues/git-issue-2727.dfy | 7 +++++++ 2 files changed, 11 insertions(+), 1 deletion(-) diff --git a/Source/DafnyCore/Resolver.cs b/Source/DafnyCore/Resolver.cs index 6f8fd792d30..92ec6d6f4ed 100644 --- a/Source/DafnyCore/Resolver.cs +++ b/Source/DafnyCore/Resolver.cs @@ -13822,7 +13822,10 @@ void ResolveBlockStatement(BlockStmt blockStmt, ResolutionContext resolutionCont } 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) { + var finalLhs = lhs is ConcreteSyntaxExpression concreteSyntaxExpression + ? concreteSyntaxExpression.Resolved ?? lhs + : lhs; + if (finalLhs is MemberSelectExpr { Member: ConstantField { IsMutable: false } field } memberSelectExpr && Expression.AsThis(memberSelectExpr.Obj) != null) { constantsAlreadyAssigned.Add(field); } } diff --git a/Test/git-issues/git-issue-2727.dfy b/Test/git-issues/git-issue-2727.dfy index 8689ce591cd..2e5f72532b5 100644 --- a/Test/git-issues/git-issue-2727.dfy +++ b/Test/git-issues/git-issue-2727.dfy @@ -1,6 +1,13 @@ // RUN: %dafny_0 -compile:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" +class NoError { + const a: int + const b: int + + constructor() { a := 3; b := a; } +} + class C { const a := b + b const b: int From f7e90a2e820859c9a3d1812571cdc12a5289b6de Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 11 Oct 2022 14:39:19 -0500 Subject: [PATCH 04/10] Better handling of alternatives --- Source/DafnyCore/Resolver.cs | 256 +++++++++++++++------- Test/git-issues/git-issue-2727.dfy | 89 +++++++- Test/git-issues/git-issue-2727.dfy.expect | 12 +- 3 files changed, 267 insertions(+), 90 deletions(-) diff --git a/Source/DafnyCore/Resolver.cs b/Source/DafnyCore/Resolver.cs index 92ec6d6f4ed..8f1af3bd8b0 100644 --- a/Source/DafnyCore/Resolver.cs +++ b/Source/DafnyCore/Resolver.cs @@ -9049,8 +9049,27 @@ public CheckDividedConstructorInit_Visitor(Resolver resolver) : base(resolver) { Contract.Requires(resolver != null); } + + // Constants that were surely assigned at the point of being read + // Forms a non-empty stack so that we can figure out if constants are fully assigned + // Every pushed element of the stack constains all the elements on the stack. + // So there is no need to look further in the stack for already assigned constants + public Stack> constantsAlreadyAssigned = new Stack>(); + // Constants for which there was a code path in which there were assigned + // but it cannot be guaranteed (gives a better error message) + public HashSet constantsPartiallyAssigned = new HashSet(); + // Constants for which an error was already reported, to avoid duplicates + public HashSet constantsWithErrors = new HashSet(); + + [CanBeNull] public Stack ContextIfCannotAssignConstant = new(); + public void CheckInit(List initStmts) { Contract.Requires(initStmts != null); + constantsAlreadyAssigned.Clear(); + constantsAlreadyAssigned.Push(new HashSet()); + constantsPartiallyAssigned = new(); + constantsWithErrors = new(); + ContextIfCannotAssignConstant.Clear(); initStmts.Iter(CheckInit); } /// @@ -9074,7 +9093,17 @@ void CheckInit(Statement stmt) { Attributes.SubExpressions(s.Attributes).Iter(VisitExpr); // (+) var mse = s.Lhs as MemberSelectExpr; if (mse != null && Expression.AsThis(mse.Obj) != null) { - if (s.Rhs is ExprRhs) { + if (mse.Member is ConstantField constantField && ContextIfCannotAssignConstant.Count > 0) { + var why = ContextIfCannotAssignConstant.Peek() switch { + LoopStmt => " in a loop statement", + AlternativeStmt => " in an alternative if-case statement", + ForallStmt => " in a forall statement", + _ => " here " + }; + resolver.reporter.Error(MessageSource.Resolver, + mse.tok, "Cannot assign constant field " + why); + } + if (s.Rhs is ExprRhs or TypeRhs) { // This is a special case we allow. Omit s.Lhs in the recursive visits. That is, we omit (++). // Furthermore, because the assignment goes to a field of "this" and won't be available until after // the "new;", we can allow certain specific (and useful) uses of "this" in the RHS. @@ -9082,6 +9111,14 @@ void CheckInit(Statement stmt) { } else { s.Rhs.SubExpressions.Iter(VisitExpr); // (+++) } + + if (mse.Member is ConstantField constantField2) { + if (constantsAlreadyAssigned.Peek().Contains(constantField2)) { + resolver.reporter.Error(MessageSource.Resolver, mse.tok, "The constant " + constantField2.Name + " was already assigned"); + } else { + constantsAlreadyAssigned.Peek().Add(constantField2); + } + } } else { VisitExpr(s.Lhs); // (++) s.Rhs.SubExpressions.Iter(VisitExpr); // (+++) @@ -9089,9 +9126,64 @@ void CheckInit(Statement stmt) { } else { stmt.SubExpressions.Iter(VisitExpr); // (*) } - stmt.SubStatements.Iter(CheckInit); // (**) + + // If true, only constants assigned in every branch can be considered 'assigned'. + // This is because match and if then-else are guaranteed to be exhaustive. + var alternative = stmt is IfStmt or MatchStmt; + var cannotAssignConstant = stmt is LoopStmt or AlternativeStmt or ForallStmt; + + if (cannotAssignConstant) { + ContextIfCannotAssignConstant.Push(stmt); + } + + var previouslyAssigned = constantsAlreadyAssigned.Peek(); + var locallyNewlyAssigneds = new List>(); // used if alternative + var newlyAssignedAtLeastOnce = new HashSet(); + if (alternative) { + constantsAlreadyAssigned.Push(new HashSet(previouslyAssigned)); + } + + foreach (var subStmt in stmt.SubStatements) { + CheckInit(subStmt); // (**) + if (alternative) { + var locallyNewlyAssigned = new HashSet(); + foreach (var constantField in constantsAlreadyAssigned.Pop()) { + if (!previouslyAssigned.Contains(constantField)) { + locallyNewlyAssigned.Add(constantField); + newlyAssignedAtLeastOnce.Add(constantField); + } + } + locallyNewlyAssigneds.Add(locallyNewlyAssigned); + constantsAlreadyAssigned.Push(new HashSet(previouslyAssigned)); + } + } + + if (alternative && stmt is IfStmt ifStmt && ifStmt.Els == null) { + locallyNewlyAssigneds.Add(new HashSet()); + } + + if (alternative) { + foreach (var locallyNewlyAssigned in locallyNewlyAssigneds) { + foreach (var constantField in newlyAssignedAtLeastOnce) { + if (!locallyNewlyAssigned.Contains(constantField)) { + constantsPartiallyAssigned.Add(constantField); + } + } + } + + foreach (var constantField in newlyAssignedAtLeastOnce) { + if (!constantsPartiallyAssigned.Contains(constantField)) { + constantsAlreadyAssigned.Peek().Add(constantField); + } + } + } + int dummy = 0; VisitOneStmt(stmt, ref dummy); // (***) + + if (cannotAssignConstant) { + ContextIfCannotAssignConstant.Pop(); + } } void VisitExpr(Expression expr) { Contract.Requires(expr != null); @@ -9100,8 +9192,17 @@ void VisitExpr(Expression expr) { protected override bool VisitOneExpr(Expression expr, ref int unused) { if (expr is MemberSelectExpr) { var e = (MemberSelectExpr)expr; - if (e.Member.IsInstanceIndependentConstant && Expression.AsThis(e.Obj) != null) { - return false; // don't continue the recursion + if (Expression.AsThis(e.Obj) != null) { + if (e.Member is ConstantField) { + var errorField = GetErrorIfConstantFieldNotInitialized(expr, new List()); + if (errorField == null) { + return false; + } + resolver.reporter.Error(MessageSource.Resolver, expr.tok, errorField.Value.message); + return false; + } + + return false; // don't continue the recursion } } else if (expr is ThisExpr && !(expr is ImplicitThisExpr_ConstructorCall)) { resolver.reporter.Error(MessageSource.Resolver, expr.tok, "in the first division of the constructor body (before 'new;'), 'this' can only be used to assign to its fields"); @@ -9121,26 +9222,82 @@ void LiberalRHSVisit(Expression expr) { // a field of "this", we must apply the same rules to uses of the values of fields of "this". if (expr is ConcreteSyntaxExpression) { } else if (expr is ThisExpr) { - } else if (expr is MemberSelectExpr && IsThisDotField((MemberSelectExpr)expr)) { - } else if (expr is SetDisplayExpr) { - } else if (expr is MultiSetDisplayExpr) { - } else if (expr is SeqDisplayExpr) { - } else if (expr is MapDisplayExpr) { - } else if (expr is BinaryExpr && IsCollectionOperator(((BinaryExpr)expr).ResolvedOp)) { - } else if (expr is DatatypeValue) { - } else if (expr is ITEExpr) { - var e = (ITEExpr)expr; - VisitExpr(e.Test); - LiberalRHSVisit(e.Thn); - LiberalRHSVisit(e.Els); - return; } else { - // defer to the usual Visit - VisitExpr(expr); - return; + // We ensure that we access only constants that were surely previously assigned + if (expr is MemberSelectExpr memberSelectExpr + && memberSelectExpr.Member is Field f + && (Expression.AsThis(memberSelectExpr.Obj) != null)) { + if (f is ConstantField constantField) { + var errorField = GetErrorIfConstantFieldNotInitialized(expr, new List()); + if (errorField != null) { + if (!constantsWithErrors.Contains(errorField.Value.constantField)) { + resolver.reporter.Error(MessageSource.Resolver, expr.tok, errorField.Value.message); + constantsWithErrors.Add(errorField.Value.constantField); + } + } + + return; + } + } else if (expr is SetDisplayExpr) { + } else if (expr is MultiSetDisplayExpr) { + } else if (expr is SeqDisplayExpr) { + } else if (expr is MapDisplayExpr) { + } else if (expr is BinaryExpr && IsCollectionOperator(((BinaryExpr)expr).ResolvedOp)) { + } else if (expr is DatatypeValue) { + } else if (expr is ITEExpr) { + var e = (ITEExpr)expr; + VisitExpr(e.Test); + LiberalRHSVisit(e.Thn); + LiberalRHSVisit(e.Els); + return; + } else { + // defer to the usual Visit + VisitExpr(expr); + return; + } } + expr.SubExpressions.Iter(LiberalRHSVisit); } + + // Returns an error if the expression cannot be fully determined + (string message, ConstantField constantField)? GetErrorIfConstantFieldNotInitialized(Expression expr, List 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.Peek().Contains(field)) { + var msg = constantsPartiallyAssigned.Contains(field) ? + "Not all paths might have initialized the constant field " : + "Missing initialization of constant 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 initialized at this point."; + return (msg, field); + } + if (field.Rhs != null) { + foreach (var subExpr in field.Rhs.SubExpressions) { + if (GetErrorIfConstantFieldNotInitialized(subExpr, visited.Append(field).ToList()) is var msgField && msgField != null) { + return msgField; + } + } + } + } + foreach (var subExpr in expr.SubExpressions) { + if (GetErrorIfConstantFieldNotInitialized(subExpr, visited) is var msgField && msgField != null) { + return msgField; + } + } + + return null; + } + static bool IsThisDotField(MemberSelectExpr expr) { Contract.Requires(expr != null); return Expression.AsThis(expr.Obj) != null && expr.Member is Field; @@ -13768,68 +13925,9 @@ 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(); - var constantsWithErrors = new HashSet(); - - // Returns an error if the expression cannot be fully determined - (string, ConstantField)? GetErrorIfNotFullyDetermined(Expression expr, List 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()) 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) { - var finalLhs = lhs is ConcreteSyntaxExpression concreteSyntaxExpression - ? concreteSyntaxExpression.Resolved ?? lhs - : lhs; - if (finalLhs 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); diff --git a/Test/git-issues/git-issue-2727.dfy b/Test/git-issues/git-issue-2727.dfy index 2e5f72532b5..a673eb83cfc 100644 --- a/Test/git-issues/git-issue-2727.dfy +++ b/Test/git-issues/git-issue-2727.dfy @@ -1,41 +1,114 @@ // RUN: %dafny_0 -compile:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" +class Dummy { + const i: int + constructor(i: int) { + this.i := i; + } +} + class NoError { const a: int + const a2: int + const a3: int + const b: int + const c: int + const d: Dummy + const e: array + + constructor() { + a := 3; + if a == 3 { + a2 := 1; + } else { + a2 := 2; + } + match a2 { + case 2 => + a3 := a; + case _ => + a3 := a + 1; + } + b := a3 + 1; + c := a2; + d := new Dummy(c); + e := new int[b]; + } +} + +class AlternativeError { + const a: int + const a2: int const b: int + const b2: int - constructor() { a := 3; b := a; } + constructor() { + if true { + a := 1; + } + b := a; // Error here + match true { + case true => + a2 := 1; + case false => + } + b2 := a2; // Error here + } +} + +class LoopError { + const a: int + const a2: int + const a3: int + const a4: int + + constructor() { + while true { + a := 1; // Error here + } + while { + case true => + a2 := 1; // Error here + } + if { + case true => + a3 := 1; // Error here + } + /*forall x: nat { + a4 := 1; // Error here + }*/ + } } -class C { +class SecondInitializationError { const a := b + b const b: int constructor (x: int) { - var k := a; + var k := a; // Error here print a, "\n"; b := x; assert k == a; print a, "\n"; if k != a { - var y := 5 / 0; // this can crash + var y := 5 / 0; } } } -class D { +class RecursiveError { const a: int := b const b: int constructor () { - b := a + 1; + b := a + 1; // Error here new; assert false; } } method Main() { - var c := new C(5); - var d := new D(); + var c := new SecondInitializationError(5); + var d := new RecursiveError(); } \ No newline at end of file diff --git a/Test/git-issues/git-issue-2727.dfy.expect b/Test/git-issues/git-issue-2727.dfy.expect index 4db2cc8ad34..8c9d45a99b7 100644 --- a/Test/git-issues/git-issue-2727.dfy.expect +++ b/Test/git-issues/git-issue-2727.dfy.expect @@ -1,3 +1,9 @@ -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 +git-issue-2727.dfy(50,9): Error: Not all paths might have initialized the constant field a, which needs to be initialized at this point. +git-issue-2727.dfy(56,10): Error: Not all paths might have initialized the constant field a2, which needs to be initialized at this point. +git-issue-2727.dfy(68,6): Error: Cannot assign constant field in a loop statement +git-issue-2727.dfy(72,8): Error: Cannot assign constant field in a loop statement +git-issue-2727.dfy(76,8): Error: Cannot assign constant field in an alternative if-case statement +git-issue-2727.dfy(89,13): Error: Missing initialization of constant field through the dependency a -> b, which needs to be initialized at this point. +git-issue-2727.dfy(90,10): Error: Missing initialization of constant field through the dependency a -> b, which needs to be initialized at this point. +git-issue-2727.dfy(105,9): Error: Missing initialization of constant field through the dependency a -> b, which needs to be initialized at this point. +8 resolution/type errors detected in git-issue-2727.dfy From 04eeb43fe6a4400bf484213d32c22eb29ebdb56a Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 11 Oct 2022 15:04:01 -0500 Subject: [PATCH 05/10] Refactoring --- Source/DafnyCore/Resolver.cs | 34 ++++++++++------------- Test/git-issues/git-issue-2727.dfy.expect | 6 ++-- 2 files changed, 17 insertions(+), 23 deletions(-) diff --git a/Source/DafnyCore/Resolver.cs b/Source/DafnyCore/Resolver.cs index 8f1af3bd8b0..47c62974240 100644 --- a/Source/DafnyCore/Resolver.cs +++ b/Source/DafnyCore/Resolver.cs @@ -9095,10 +9095,10 @@ void CheckInit(Statement stmt) { if (mse != null && Expression.AsThis(mse.Obj) != null) { if (mse.Member is ConstantField constantField && ContextIfCannotAssignConstant.Count > 0) { var why = ContextIfCannotAssignConstant.Peek() switch { - LoopStmt => " in a loop statement", - AlternativeStmt => " in an alternative if-case statement", - ForallStmt => " in a forall statement", - _ => " here " + LoopStmt => " in a loop statement.", + AlternativeStmt => " in an alternative if-case statement.", + ForallStmt => " in a forall statement.", + _ => " here." }; resolver.reporter.Error(MessageSource.Resolver, mse.tok, "Cannot assign constant field " + why); @@ -9146,23 +9146,20 @@ void CheckInit(Statement stmt) { foreach (var subStmt in stmt.SubStatements) { CheckInit(subStmt); // (**) if (alternative) { - var locallyNewlyAssigned = new HashSet(); - foreach (var constantField in constantsAlreadyAssigned.Pop()) { - if (!previouslyAssigned.Contains(constantField)) { - locallyNewlyAssigned.Add(constantField); - newlyAssignedAtLeastOnce.Add(constantField); - } - } + var locallyNewlyAssigned = constantsAlreadyAssigned.Pop(); + locallyNewlyAssigned.RemoveWhere(constantField => previouslyAssigned.Contains(constantField)); + newlyAssignedAtLeastOnce.UnionWith(locallyNewlyAssigned); locallyNewlyAssigneds.Add(locallyNewlyAssigned); constantsAlreadyAssigned.Push(new HashSet(previouslyAssigned)); } } - if (alternative && stmt is IfStmt ifStmt && ifStmt.Els == null) { - locallyNewlyAssigneds.Add(new HashSet()); - } - if (alternative) { + constantsAlreadyAssigned.Pop(); + if (stmt is IfStmt ifStmt && ifStmt.Els == null) { + locallyNewlyAssigneds.Add(new HashSet()); + } + foreach (var locallyNewlyAssigned in locallyNewlyAssigneds) { foreach (var constantField in newlyAssignedAtLeastOnce) { if (!locallyNewlyAssigned.Contains(constantField)) { @@ -9171,11 +9168,8 @@ void CheckInit(Statement stmt) { } } - foreach (var constantField in newlyAssignedAtLeastOnce) { - if (!constantsPartiallyAssigned.Contains(constantField)) { - constantsAlreadyAssigned.Peek().Add(constantField); - } - } + newlyAssignedAtLeastOnce.RemoveWhere(constantField => constantsPartiallyAssigned.Contains(constantField)); + constantsAlreadyAssigned.Peek().UnionWith(newlyAssignedAtLeastOnce); } int dummy = 0; diff --git a/Test/git-issues/git-issue-2727.dfy.expect b/Test/git-issues/git-issue-2727.dfy.expect index 8c9d45a99b7..000729d88f4 100644 --- a/Test/git-issues/git-issue-2727.dfy.expect +++ b/Test/git-issues/git-issue-2727.dfy.expect @@ -1,8 +1,8 @@ git-issue-2727.dfy(50,9): Error: Not all paths might have initialized the constant field a, which needs to be initialized at this point. git-issue-2727.dfy(56,10): Error: Not all paths might have initialized the constant field a2, which needs to be initialized at this point. -git-issue-2727.dfy(68,6): Error: Cannot assign constant field in a loop statement -git-issue-2727.dfy(72,8): Error: Cannot assign constant field in a loop statement -git-issue-2727.dfy(76,8): Error: Cannot assign constant field in an alternative if-case statement +git-issue-2727.dfy(68,6): Error: Cannot assign constant field in a loop statement. +git-issue-2727.dfy(72,8): Error: Cannot assign constant field in a loop statement. +git-issue-2727.dfy(76,8): Error: Cannot assign constant field in an alternative if-case statement. git-issue-2727.dfy(89,13): Error: Missing initialization of constant field through the dependency a -> b, which needs to be initialized at this point. git-issue-2727.dfy(90,10): Error: Missing initialization of constant field through the dependency a -> b, which needs to be initialized at this point. git-issue-2727.dfy(105,9): Error: Missing initialization of constant field through the dependency a -> b, which needs to be initialized at this point. From 55686641ba326909bb4324dda20724f609df114d Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 11 Oct 2022 16:28:20 -0500 Subject: [PATCH 06/10] Fix CI --- Source/DafnyCore/Resolver.cs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Source/DafnyCore/Resolver.cs b/Source/DafnyCore/Resolver.cs index 47c62974240..44b92d1faa2 100644 --- a/Source/DafnyCore/Resolver.cs +++ b/Source/DafnyCore/Resolver.cs @@ -9114,7 +9114,9 @@ void CheckInit(Statement stmt) { if (mse.Member is ConstantField constantField2) { if (constantsAlreadyAssigned.Peek().Contains(constantField2)) { - resolver.reporter.Error(MessageSource.Resolver, mse.tok, "The constant " + constantField2.Name + " was already assigned"); + // Breaking change: Do we want to report on constants assigned multiple times? + /*resolver.reporter.Error(MessageSource.Resolver, mse.tok, + $"The constant {constantField2.Name} was already assigned");*/ } else { constantsAlreadyAssigned.Peek().Add(constantField2); } @@ -9195,8 +9197,6 @@ protected override bool VisitOneExpr(Expression expr, ref int unused) { resolver.reporter.Error(MessageSource.Resolver, expr.tok, errorField.Value.message); return false; } - - return false; // don't continue the recursion } } else if (expr is ThisExpr && !(expr is ImplicitThisExpr_ConstructorCall)) { resolver.reporter.Error(MessageSource.Resolver, expr.tok, "in the first division of the constructor body (before 'new;'), 'this' can only be used to assign to its fields"); From bd717d1655655eb735d2ae4a2f3bc7a78de49e61 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= Date: Wed, 12 Oct 2022 14:28:13 -0500 Subject: [PATCH 07/10] Create 2862.fix --- docs/dev/news/2862.fix | 1 + 1 file changed, 1 insertion(+) create mode 100644 docs/dev/news/2862.fix diff --git a/docs/dev/news/2862.fix b/docs/dev/news/2862.fix new file mode 100644 index 00000000000..9564950ea04 --- /dev/null +++ b/docs/dev/news/2862.fix @@ -0,0 +1 @@ +Constant initialization checked for recursion From 2e98a55bdd36c41e909494fd475e1159d88bbe75 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 14 Oct 2022 13:32:11 -0500 Subject: [PATCH 08/10] Prevent constants to be assigned twice --- Source/DafnyCore/Resolver.cs | 7 +++---- Test/git-issues/git-issue-2727.dfy | 12 +++++++++++- Test/git-issues/git-issue-2727.dfy.expect | 9 +++++---- Test/traits/TraitCompile.dfy | 2 -- 4 files changed, 19 insertions(+), 11 deletions(-) diff --git a/Source/DafnyCore/Resolver.cs b/Source/DafnyCore/Resolver.cs index 44b92d1faa2..ae00a87acd6 100644 --- a/Source/DafnyCore/Resolver.cs +++ b/Source/DafnyCore/Resolver.cs @@ -9101,7 +9101,7 @@ void CheckInit(Statement stmt) { _ => " here." }; resolver.reporter.Error(MessageSource.Resolver, - mse.tok, "Cannot assign constant field " + why); + mse.tok, "Cannot assign constant field" + why); } if (s.Rhs is ExprRhs or TypeRhs) { // This is a special case we allow. Omit s.Lhs in the recursive visits. That is, we omit (++). @@ -9114,9 +9114,8 @@ void CheckInit(Statement stmt) { if (mse.Member is ConstantField constantField2) { if (constantsAlreadyAssigned.Peek().Contains(constantField2)) { - // Breaking change: Do we want to report on constants assigned multiple times? - /*resolver.reporter.Error(MessageSource.Resolver, mse.tok, - $"The constant {constantField2.Name} was already assigned");*/ + resolver.reporter.Error(MessageSource.Resolver, mse.tok, + $"The constant {constantField2.Name} cannot be assigned twice."); } else { constantsAlreadyAssigned.Peek().Add(constantField2); } diff --git a/Test/git-issues/git-issue-2727.dfy b/Test/git-issues/git-issue-2727.dfy index a673eb83cfc..1818e24bb7a 100644 --- a/Test/git-issues/git-issue-2727.dfy +++ b/Test/git-issues/git-issue-2727.dfy @@ -104,10 +104,20 @@ class RecursiveError { constructor () { b := a + 1; // Error here new; - assert false; } } +class MultipleAssignmentError { + const b: int + + constructor () { + b := 1; + b := 2; // Error here + new; + } +} + + method Main() { var c := new SecondInitializationError(5); var d := new RecursiveError(); diff --git a/Test/git-issues/git-issue-2727.dfy.expect b/Test/git-issues/git-issue-2727.dfy.expect index 000729d88f4..2d1fa6b5008 100644 --- a/Test/git-issues/git-issue-2727.dfy.expect +++ b/Test/git-issues/git-issue-2727.dfy.expect @@ -1,9 +1,10 @@ git-issue-2727.dfy(50,9): Error: Not all paths might have initialized the constant field a, which needs to be initialized at this point. git-issue-2727.dfy(56,10): Error: Not all paths might have initialized the constant field a2, which needs to be initialized at this point. -git-issue-2727.dfy(68,6): Error: Cannot assign constant field in a loop statement. -git-issue-2727.dfy(72,8): Error: Cannot assign constant field in a loop statement. -git-issue-2727.dfy(76,8): Error: Cannot assign constant field in an alternative if-case statement. +git-issue-2727.dfy(68,6): Error: Cannot assign constant field in a loop statement. +git-issue-2727.dfy(72,8): Error: Cannot assign constant field in a loop statement. +git-issue-2727.dfy(76,8): Error: Cannot assign constant field in an alternative if-case statement. git-issue-2727.dfy(89,13): Error: Missing initialization of constant field through the dependency a -> b, which needs to be initialized at this point. git-issue-2727.dfy(90,10): Error: Missing initialization of constant field through the dependency a -> b, which needs to be initialized at this point. git-issue-2727.dfy(105,9): Error: Missing initialization of constant field through the dependency a -> b, which needs to be initialized at this point. -8 resolution/type errors detected in git-issue-2727.dfy +git-issue-2727.dfy(115,4): Error: The constant b cannot be assigned twice. +9 resolution/type errors detected in git-issue-2727.dfy diff --git a/Test/traits/TraitCompile.dfy b/Test/traits/TraitCompile.dfy index 0d341c08711..583d1d48b3e 100644 --- a/Test/traits/TraitCompile.dfy +++ b/Test/traits/TraitCompile.dfy @@ -189,7 +189,6 @@ module GenericBasics { // Cl has fewer type parameters than Tr class Cl extends Tr { constructor () { - abc := 100; this.abc := 101; xyz := 20; this.xyz := 21; @@ -247,7 +246,6 @@ module GenericBasics { // Mega has more type parameters than Tr class Mega extends Tr { constructor () { - abc := 100; this.abc := 101; xyz := 20; this.xyz := 21; From 3ac8137a2aeef7c88fce29c917c80b1db672cfed Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Wed, 26 Oct 2022 09:55:43 -0500 Subject: [PATCH 09/10] One more soundness fix --- Source/DafnyCore/Resolver.cs | 7 +++ Test/git-issues/git-issue-2727.dfy | 69 ++++++++++++++++++++++- Test/git-issues/git-issue-2727.dfy.expect | 23 ++++---- 3 files changed, 86 insertions(+), 13 deletions(-) diff --git a/Source/DafnyCore/Resolver.cs b/Source/DafnyCore/Resolver.cs index d9f40078931..5c534592696 100644 --- a/Source/DafnyCore/Resolver.cs +++ b/Source/DafnyCore/Resolver.cs @@ -9281,6 +9281,13 @@ void LiberalRHSVisit(Expression expr) { } } } + } else if (expr is FunctionCallExpr { tok: var tok, Function: { IsStatic: false } function }) { + var msg = "Constant field '" + visited[0].Name + "' cannot be accessed before 'new;'"; + for (var i = 1; i < visited.Count; i++) { + msg += (i == 1 ? " because of the dependency " + visited[0].Name : "") + " -> " + visited[i].Name; + } + msg += ", " + (visited.Count > 1 ? "and" : "because") + " '" + visited[visited.Count - 1].Name + "' depends on the non-static function '" + function.Name + "' that can potentially read other uninitialized constants."; + return (msg, visited[0]); } foreach (var subExpr in expr.SubExpressions) { if (GetErrorIfConstantFieldNotInitialized(subExpr, visited) is var msgField && msgField != null) { diff --git a/Test/git-issues/git-issue-2727.dfy b/Test/git-issues/git-issue-2727.dfy index 1818e24bb7a..1cc55217cf7 100644 --- a/Test/git-issues/git-issue-2727.dfy +++ b/Test/git-issues/git-issue-2727.dfy @@ -12,7 +12,7 @@ class NoError { const a: int const a2: int const a3: int - const b: int + const b: int := a3 + 1 const c: int const d: Dummy const e: array @@ -30,13 +30,37 @@ class NoError { case _ => a3 := a + 1; } - b := a3 + 1; - c := a2; + c := a2 + b; // a3 is defined so b can be used here d := new Dummy(c); e := new int[b]; } } + +class FunctionInitializationOK { + const a := B() + const b: int + static function method B(): int { 1 } + + constructor (x: int) { + b := a + 1; // No problem here! + new; + } +} + +class FunctionInitializationOK2 { + const a := B() + const b: int + var c: int + function method B(): int { b } + + constructor (x: int) { + b := 1; + new; + c := a; // OK here + } +} + class AlternativeError { const a: int const a2: int @@ -117,6 +141,45 @@ class MultipleAssignmentError { } } +class FunctionInitializationError { + const a := B() + const b: int + function method B(): int { b } + + constructor (x: int) { + b := a + 1; // Error: a is not guaranteed to be initialized here + new; + assert false; // We should never be able to prove this + } +} +class FunctionInitializationError2 { + const a := B() + const c := a; + const b: int + function method B(): int { b } + + constructor (x: int) { + b := c + 1; // Error: a is not guaranteed to be initialized here + new; + assert false; // We should never be able to prove this + } +} + +trait Tr { + const a := B() + const b: int + function method B(): int +} + +class C extends Tr { + function method B(): int { b } + + constructor (x: int) { + b := a + 1; // Error: a is not guaranteed to be initialized here + new; + assert false; // We should never be able to prove this + } +} method Main() { var c := new SecondInitializationError(5); diff --git a/Test/git-issues/git-issue-2727.dfy.expect b/Test/git-issues/git-issue-2727.dfy.expect index 2d1fa6b5008..4c4329294c6 100644 --- a/Test/git-issues/git-issue-2727.dfy.expect +++ b/Test/git-issues/git-issue-2727.dfy.expect @@ -1,10 +1,13 @@ -git-issue-2727.dfy(50,9): Error: Not all paths might have initialized the constant field a, which needs to be initialized at this point. -git-issue-2727.dfy(56,10): Error: Not all paths might have initialized the constant field a2, which needs to be initialized at this point. -git-issue-2727.dfy(68,6): Error: Cannot assign constant field in a loop statement. -git-issue-2727.dfy(72,8): Error: Cannot assign constant field in a loop statement. -git-issue-2727.dfy(76,8): Error: Cannot assign constant field in an alternative if-case statement. -git-issue-2727.dfy(89,13): Error: Missing initialization of constant field through the dependency a -> b, which needs to be initialized at this point. -git-issue-2727.dfy(90,10): Error: Missing initialization of constant field through the dependency a -> b, which needs to be initialized at this point. -git-issue-2727.dfy(105,9): Error: Missing initialization of constant field through the dependency a -> b, which needs to be initialized at this point. -git-issue-2727.dfy(115,4): Error: The constant b cannot be assigned twice. -9 resolution/type errors detected in git-issue-2727.dfy +git-issue-2727.dfy(74,9): Error: Not all paths might have initialized the constant field a, which needs to be initialized at this point. +git-issue-2727.dfy(80,10): Error: Not all paths might have initialized the constant field a2, which needs to be initialized at this point. +git-issue-2727.dfy(92,6): Error: Cannot assign constant field in a loop statement. +git-issue-2727.dfy(96,8): Error: Cannot assign constant field in a loop statement. +git-issue-2727.dfy(100,8): Error: Cannot assign constant field in an alternative if-case statement. +git-issue-2727.dfy(113,13): Error: Missing initialization of constant field through the dependency a -> b, which needs to be initialized at this point. +git-issue-2727.dfy(114,10): Error: Missing initialization of constant field through the dependency a -> b, which needs to be initialized at this point. +git-issue-2727.dfy(129,9): Error: Missing initialization of constant field through the dependency a -> b, which needs to be initialized at this point. +git-issue-2727.dfy(139,4): Error: The constant b cannot be assigned twice. +git-issue-2727.dfy(150,9): Error: Constant field 'a' cannot be accessed before 'new;', because 'a' depends on the non-static function 'B' that can potentially read other uninitialized constants. +git-issue-2727.dfy(162,9): Error: Constant field 'c' cannot be accessed before 'new;' because of the dependency c -> a, and 'a' depends on the non-static function 'B' that can potentially read other uninitialized constants. +git-issue-2727.dfy(178,9): Error: Constant field 'a' cannot be accessed before 'new;', because 'a' depends on the non-static function 'B' that can potentially read other uninitialized constants. +12 resolution/type errors detected in git-issue-2727.dfy From 5555cde4be8a15bb63e149d5fc5cc9620257ae44 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Wed, 26 Oct 2022 10:37:12 -0500 Subject: [PATCH 10/10] One more soundness fix --- Source/DafnyCore/Resolver.cs | 11 ++++++++++- Test/git-issues/git-issue-2727.dfy | 12 ++++++++++++ Test/git-issues/git-issue-2727.dfy.expect | 3 ++- 3 files changed, 24 insertions(+), 2 deletions(-) diff --git a/Source/DafnyCore/Resolver.cs b/Source/DafnyCore/Resolver.cs index 5c534592696..d82dc78313a 100644 --- a/Source/DafnyCore/Resolver.cs +++ b/Source/DafnyCore/Resolver.cs @@ -9281,13 +9281,22 @@ void LiberalRHSVisit(Expression expr) { } } } - } else if (expr is FunctionCallExpr { tok: var tok, Function: { IsStatic: false } function }) { + + return null; // No problem to declare for this field + } else if (expr is FunctionCallExpr { tok: var tok, Function: { IsStatic: false } function } && visited.Count > 0) { var msg = "Constant field '" + visited[0].Name + "' cannot be accessed before 'new;'"; for (var i = 1; i < visited.Count; i++) { msg += (i == 1 ? " because of the dependency " + visited[0].Name : "") + " -> " + visited[i].Name; } msg += ", " + (visited.Count > 1 ? "and" : "because") + " '" + visited[visited.Count - 1].Name + "' depends on the non-static function '" + function.Name + "' that can potentially read other uninitialized constants."; return (msg, visited[0]); + } else if (expr is ThisExpr && visited.Count > 0) { + var msg = "Constant field '" + visited[0].Name + "' cannot be accessed before 'new;'"; + for (var i = 1; i < visited.Count; i++) { + msg += (i == 1 ? " because of the dependency " + visited[0].Name : "") + " -> " + visited[i].Name; + } + msg += ", " + (visited.Count > 1 ? "and" : "because") + " '" + visited[visited.Count - 1].Name + "' depends on the object 'this' itself, that can potentially read other uninitialized constants."; + return (msg, visited[0]); } foreach (var subExpr in expr.SubExpressions) { if (GetErrorIfConstantFieldNotInitialized(subExpr, visited) is var msgField && msgField != null) { diff --git a/Test/git-issues/git-issue-2727.dfy b/Test/git-issues/git-issue-2727.dfy index 1cc55217cf7..d1301c0614e 100644 --- a/Test/git-issues/git-issue-2727.dfy +++ b/Test/git-issues/git-issue-2727.dfy @@ -181,6 +181,18 @@ class C extends Tr { } } +class DeepThisError { + const d: Dummy + const t: set := {this} + + constructor() { + var x := set n: DeepThisError | n in t :: n.d.i; + // Error above: cannot use 't' because it depends on "this" which might have uninitialized constants + d := new Dummy(1); + new; + } +} + method Main() { var c := new SecondInitializationError(5); var d := new RecursiveError(); diff --git a/Test/git-issues/git-issue-2727.dfy.expect b/Test/git-issues/git-issue-2727.dfy.expect index 4c4329294c6..0f2307fa287 100644 --- a/Test/git-issues/git-issue-2727.dfy.expect +++ b/Test/git-issues/git-issue-2727.dfy.expect @@ -10,4 +10,5 @@ git-issue-2727.dfy(139,4): Error: The constant b cannot be assigned twice. git-issue-2727.dfy(150,9): Error: Constant field 'a' cannot be accessed before 'new;', because 'a' depends on the non-static function 'B' that can potentially read other uninitialized constants. git-issue-2727.dfy(162,9): Error: Constant field 'c' cannot be accessed before 'new;' because of the dependency c -> a, and 'a' depends on the non-static function 'B' that can potentially read other uninitialized constants. git-issue-2727.dfy(178,9): Error: Constant field 'a' cannot be accessed before 'new;', because 'a' depends on the non-static function 'B' that can potentially read other uninitialized constants. -12 resolution/type errors detected in git-issue-2727.dfy +git-issue-2727.dfy(189,41): Error: Constant field 't' cannot be accessed before 'new;', because 't' depends on the object 'this' itself, that can potentially read other uninitialized constants. +13 resolution/type errors detected in git-issue-2727.dfy