diff --git a/Source/DafnyCore/Resolver.cs b/Source/DafnyCore/Resolver.cs
index 3f6abf31e8b..d82dc78313a 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
@@ -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,15 @@ 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} cannot be assigned twice.");
+ } else {
+ constantsAlreadyAssigned.Peek().Add(constantField2);
+ }
+ }
} else {
VisitExpr(s.Lhs); // (++)
s.Rhs.SubExpressions.Iter(VisitExpr); // (+++)
@@ -9089,9 +9127,58 @@ 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 = constantsAlreadyAssigned.Pop();
+ locallyNewlyAssigned.RemoveWhere(constantField => previouslyAssigned.Contains(constantField));
+ newlyAssignedAtLeastOnce.UnionWith(locallyNewlyAssigned);
+ locallyNewlyAssigneds.Add(locallyNewlyAssigned);
+ constantsAlreadyAssigned.Push(new HashSet(previouslyAssigned));
+ }
+ }
+
+ 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)) {
+ constantsPartiallyAssigned.Add(constantField);
+ }
+ }
+ }
+
+ newlyAssignedAtLeastOnce.RemoveWhere(constantField => constantsPartiallyAssigned.Contains(constantField));
+ constantsAlreadyAssigned.Peek().UnionWith(newlyAssignedAtLeastOnce);
+ }
+
int dummy = 0;
VisitOneStmt(stmt, ref dummy); // (***)
+
+ if (cannotAssignConstant) {
+ ContextIfCannotAssignConstant.Pop();
+ }
}
void VisitExpr(Expression expr) {
Contract.Requires(expr != null);
@@ -9100,8 +9187,15 @@ 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;
+ }
}
} 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 +9215,98 @@ 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;
+ }
+ }
+ }
+
+ 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) {
+ return msgField;
+ }
+ }
+
+ return null;
+ }
+
static bool IsThisDotField(MemberSelectExpr expr) {
Contract.Requires(expr != null);
return Expression.AsThis(expr.Obj) != null && expr.Member is Field;
@@ -13784,6 +13950,7 @@ 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
+
foreach (Statement ss in div.BodyInit) {
ResolveStatementWithLabels(ss, resolutionContext with { InFirstPhaseConstructor = true });
}
diff --git a/Test/git-issues/git-issue-2727.dfy b/Test/git-issues/git-issue-2727.dfy
new file mode 100644
index 00000000000..d1301c0614e
--- /dev/null
+++ b/Test/git-issues/git-issue-2727.dfy
@@ -0,0 +1,199 @@
+// 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 := a3 + 1
+ 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;
+ }
+ 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
+ const b: int
+ const b2: int
+
+ 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 SecondInitializationError {
+ const a := b + b
+ const b: int
+
+ constructor (x: int) {
+ var k := a; // Error here
+ print a, "\n";
+ b := x;
+ assert k == a;
+ print a, "\n";
+ if k != a {
+ var y := 5 / 0;
+ }
+ }
+}
+
+class RecursiveError {
+ const a: int := b
+ const b: int
+
+ constructor () {
+ b := a + 1; // Error here
+ new;
+ }
+}
+
+class MultipleAssignmentError {
+ const b: int
+
+ constructor () {
+ b := 1;
+ b := 2; // Error here
+ new;
+ }
+}
+
+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
+ }
+}
+
+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();
+}
\ 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..0f2307fa287
--- /dev/null
+++ b/Test/git-issues/git-issue-2727.dfy.expect
@@ -0,0 +1,14 @@
+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.
+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
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;
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