Fix: Recursive constant initialization was not checked if in constructor

[MikaelMayer]

This PR fixes #2727 by adding an appropriate error message if constants are initialized in the wrong order.
It also fixes #2923

Implementation

• In the CheckInit phase, I'm keeping track of assignments and statements, and
  • forbid initialization of constants inside loops or potentially incomplete alternative statements
  • detect partial initialization of constants (e.g. only in the then-branch of an if) and report an error if it's being used afterwards.
  • detect and prevent recursion between constants when they are being built
  • Prevent a constant from being assigned twice (that way, we can implement lazy semantics for constant evaluation without ambiguity)
  • Prevent a constant that depends on a call to a non-static function to be read before "new;"
  • Prevent a constant that depends on an explicit usage of "this" (not its fields) to be read before "new;"

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[MikaelMayer]

This has nothing to do with this PR, but I tried having dafny in a folder with space in its name and I had to fix this to make it work.

[MikaelMayer]

I keep forgetting that these are called "pass", I'm always looking for "phase". Next time, if I forget again, I will be able to find them.

[cpitclaudel]

Nice! The changes look good, but I wonder if we could reuse more of the other code. In particular:

• We already have code to detect loops in constant initialization, as in class C { const a := b; const b := a }, so maybe we could reuse it
• Even if we can't reuse that code, we already have code to find cycles and traverse ASTs, so I don't think we should re-implement the graph traversal; instead, we can use a visitor to collect all field references in the RHS of a variable, and the SCC checker to find cycles

I also think that the check is a bit too strict, since it rejects this:

class C {
  a: int
  b: int

  constructor() { a := 3; b := a; }

Maybe we do want to reject this, but I'm not sure.

[MikaelMayer]

I did check your example, and it passes. I added it to the current test.

class C {
  const a: int
  const b: int

  constructor() { a := 3; b := a; }
}

Let me explain in deeper detail the solution I implemented. This solution has almost nothing to do with the cycle dependency checker that is already implemented. This cycle dependency checker builds a dependency graph between constants based on their definition, and find cycles in this graph.
Here the problem is different, and much simpler to some extent. We don't need to compute yet another dependency graph for constants, because the order of the assignments is already provided (and we are not reordering assignments in the constructor body).
So, the only thing remaining is to verify that, for each assignment of a constant, all the constants it depends on are already assigned.
This is what the recursive function is about, to detect dependencies which are not initialized yet.

Now about the detection of uninitialized recursion: There is a case "Please break this constant initialization cycle", but I don't know how to test it, and it seems from the resolver that this is already being taken care of in previous resolution steps, so I don't think there is a way we could reach this code. I could remove it or throw an error if you prefer. But so that this code is locally consistent and does not require other hypotheses, I would prefer to leave it there.

[cpitclaudel]

I don't understand. When I built your code locally and run it on this:

class C {
  const a: int
  const b: int

  constructor() { a := 3; b := a; }
}

I get this output:

mikael.dfy(5,31): Error: Constant not initialized yet. Missing initialization of field a, which needs to be assigned at this point.
1 resolution/type errors detected in mikael.dfy

Do you not see this?

[cpitclaudel]

Also, when there's a compound expression, I think the error is on the wrong element:

[cpitclaudel]

Here the problem is different, and much simpler to some extent. We don't need to compute yet another dependency graph for constants, because the order of the assignments is already provided (and we are not reordering assignments in the constructor body).

Excellent point, thanks.

How do you deal with conditionals? I'm seeing this with your code:

class C {
  const a: int;

  constructor(c: bool) {
    if true {
      a := 1;
      // Constant not initialized yet. Missing initialization of field a, which needs to be assigned at this point.
    } else {
      a := 2;
    }
  }
}

Is that expected?
I guess I'm just wondering whether we want to even allow read-only properties to be used in the first half of a constructor. For example, we don't allow this:

class C {
  const b: int;
  function method a(): int {
    3
  }

  constructor() {
    b := a() + 1;
  }
}

So, should we allow this?

class C {
  const b: int;
  const a: int := 3;

  constructor() {
    b := a + 1;
  }
}

Now about the detection of uninitialized recursion: There is a case "Please break this constant initialization cycle", but I don't know how to test it, and it seems from the resolver that this is already being taken care of in previous resolution steps

Is it this case?

class C {
  const a: int
  const b: int := a + 1

  constructor() { a := b + 1; }
  // Constant not initialized yet. Missing initialization of field through the dependency b -> a, which needs to be assigned at this point.
}

Sorry if I'm missing something (since it seems that I'm not running the same code as you are based on the example above)

[MikaelMayer]

I don't understand. When I built your code locally and run it on this:

Here is what I have on my side.

So we really have different outputs. That's weird.

Is that expected?

For the conditionals, I hadn't realized you could put conditional statements in the first part of the body. Good catch. I'll fix it.

[MikaelMayer]

Is it this case?

It's actually for this case:

class Error {
  const a: int := b
  const b: int := a
  const c: int
  constructor() {
    c := a;
  }
}

which, incidentally, runs before the check for recursion of constants. Hence, if I see a variable already, I could also consider that it's initialized already and leave the rest of the resolver to actually report the recursion error. Would that make sense?

[MikaelMayer]

It seems to me that disallowing reading constants could prevent the useful pattern:

class ConstantHolder {
  const PREFIX: string := "prefix_"
  const FULL_NAME: string
  constructor(name: string) {
    FULL_NAME := PREFIX + name;
  }
}

Not making it possible to read PREFIX when assigning constants would be cumbersome in this case. We could get around this by assigning PREFIX in the constructor to a common value with FULL_NAME:

class ConstantHolder {
  const PREFIX: string;
  const FULL_NAME: string
  constructor(name: string) {
    var p :=  "prefix_";
    PREFIX := p;
    FULL_NAME := p + name;
  }
}

but now, it seems that 1) we would be adding a breaking change for something that was legit (the first above), and 2) the workaround breaks the idea that the prefix is instance-independent.

[cpitclaudel]

It seems to me that disallowing reading constants could prevent the useful pattern:

Should that pattern use a static constant?

[MikaelMayer]

Should that pattern use a static constant?

That would work as well. So what about the nested pattern?

class ConstantHolder {
  static const PREFIX: string := "prefix_";
  static const SUFFIX: string
  const FULL_NAME: string
  const FULL_NAME_SUFFIXED: string
  constructor(name: string) {
    FULL_NAME := PREFIX + name;
    FULL_NAME_SUFFIXED := FULL_NAME + SUFFIX;
  }
}

This one seems natural: As soon as we defined the constant, we should be able to read it without restriction.
A constant can be said to be defined if it's defined in every branch of a conditional or every case of a match statement.
Are there any other cases I need to consider?
Also, that means I would need to remove the current weird effect that b := a is authorized but not b := 1 + a;

[cpitclaudel]

I don't understand the code above (how can you assign to a static constant?)
We should be able to reuse the code that we use for definite assignment here, right?

[MikaelMayer]

I don't understand the code above (how can you assign to a static constant?)
We should be able to reuse the code that we use for definite assignment here, right?

I just fixed my example, there was something wrong. Please check again.

Also, I did not realize but until now, we were able to assign a value to constants multiple times. This should not be the case.
The following code is currently verifying with the current Dafny, but not with this PR.

class A {
  const a: int
  constructor() {
    a:=1;
    a:=2;
  }
}

With the code on this PR, it will complain that "a" was already assigned. Do you think it is better, or is it expected that you can modify a constant as many times as you want in the first part of a constructor?

[MikaelMayer]

I don't understand the code above (how can you assign to a static constant?)
We should be able to reuse the code that we use for definite assignment here, right?

I just fixed my example, there was something wrong. Please check again.

Also, I did not realize but until now, we were able to assign a value to constants multiple times. This should not be the case. The following code is currently verifying with the current Dafny, but not with this PR.

class A {
  const a: int
  constructor() {
    a:=1;
    a:=2;
  }
}

With the code on this PR, it will complain that "a" was already assigned. Do you think it is better, or is it expected that you can modify a constant as many times as you want in the first part of a constructor?

I ended up removing this extra check, as the verifier is clever enough to not assign final values to a until new;
So we should be good.

[cpitclaudel]

We have decided to debate what the exact semantics of assignment in constructors should be before we merge this. In particular, should constants really behave as functions, like in the following example?

class C {
  const a: int
  const b := a + a

  constructor() {
    a := 1;
    print b; // 2
    a := 2;
    print b; // 4
  }

[MikaelMayer]

Ok, this PR introduces another soundness-crash issue that needs to be fixed

Previously, the following would not verify

class Dummy {
  const i: int
  constructor(i: int) {
    this.i := i;
  }
}
class ThisError {
  const d: Dummy
  const s: set<ThisError>

  constructor() {
    s := {this};
// Here it was complaining about the use of "this.s" in the first part of the constructor.
    var x := set n: ThisError | n in s :: n.d.i;
    d := new Dummy(1);
  }
}

As this PR has assumed "s" can be used safely, the error is not there anymore. Will need a fix.

[MikaelMayer]

This is actually not a new soundness crash issue, it existed before:

#2923