Constant fields depending on non-initialized fields should not be usable in first-phase construction

[RustanLeino]

Dafny restricts the use of field in the first phase of an object constructor. It currently allows a field to be used if the field is a const with a given RHS. This is sometimes unsound, as the following program demonstrates.

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
    }
  }
}

method Main() {
  var c := new C(5);
}

The allowance of reading, in the first phase of a constructor, a const with a RHS should apply only if the RHS can be determined not to depend on any const field without a RHS.

[cpitclaudel]

Good catch! You can do a bit worse, too, by creating cycles:

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

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

[keyboardDrummer]

I would like it if constant fields with RHS assignments can be translated to constant fields without a RHS that are assigned in the constructor, to reduce the amount of semantic concepts that exist in the language.

However, I think the current 'lazy' behavior of constant fields cannot be mimicked by assigning them in the constructor. I think if we would add the concept of a lazy variable, as it exists in Scala (ref), then we can implement the desired equivalence, using a transformation that moves all assignment to the constructor, which is trivial since the location where they're assigned does not matter due to the semantics of lazy variables.

[RustanLeino]

Here is a variation of @cpitclaudel 's program, but getting to b indirectly via function B():

class C {
  const a := B()
  const b: int
  function B(): int { b }

  constructor (x: int) {
    b := a + 1;
    new;
    assert false; // ouch! provable
  }
}

and yet another version that throws in a trait:

trait Tr {
  const a := B()
  const b: int
  function B(): int
}

class C extends Tr {
  function B(): int { b }

  constructor (x: int) {
    b := a + 1;
    new;
    assert false; // ouch! provable
  }
}

[MikaelMayer]

Great catch !
I added a test in here #2862 and added a case to catch this.

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

Lines 144 to 154 in 3ac8137

	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
	}
	}

Here is the error it will generate:

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

Line 10 in 3ac8137

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.

Specifically, I took the most permissive route: I forbid the access to constants before the "new;" if their right-hand-side transitively contains a call to a non-static function, because non-static functions could otherwise access uninitialized constants

[MikaelMayer]

Here is how I would now approach this soundness issue. I want a solution that follows the general idea of being able to express anything Dafny needs to prove in Dafny (thanks @robin-aws for the wording)

• Fact A: Fields are like array indices, and "this" is like an array pointer. For the verification point of view and the memory, it's the same.
• Fact B: Before "new;" all the fields of "this" are being assigned, and should not be accessed until assigned at least once. That includes ghost code as well, as if the type was empty, we should not be able to assume a constant of this type had a value before, even ghost.
• Fact C: To access a field, an expression needs a pointer to the object being built (i.e. "this")
• Fact D: "this" is accessible from non-static methods and from functions as it's an implicit argument
• Fact E: We need to be able to put "this" in the Repr for cyclic structures, and Repr has to be assigned before the new; when it's a constant, as it's also a field, even when it's ghost.
• Decision F: Constant fields should be assigned only once

Let's start with Fact B.
Fact B: would be exactly modeled with a heap-aware predicate for each field like assigned(this`field) that is false at the beginning for any field, true for any other object, and on every heap assignment, if this.field is set, then assigned(this`field) becomes true. For decision F, we would just check that aassigned(this`field) is false before a constant assignment.
Then, every access before new; is tested with assigned(this`field), and every field of the object yields an assertion at the new; that assert assigned(this`field);

Fact A and C: tell us that passing "this" to any regular function or method, before the new;, is unsound as these methods would require the implicit forall o, field | allocated(o) && IsField(o, field) :: assigned(o`field), which is not true for the object being build before new;. This includes also passing another object that undercover would be "this" or contain "this".

Fact D then confirm we cannot call instance methods and functions with "this" available unless we have a way for them to NOT assume that all fields are assigned. This could be done in the future with an attribute {:constructor}. Such an attribute will perform the check assigned(this`field) before accessing any field, and pre-/post- conditions could mention assigned(this`field). But as a first approximation, before new; no function or method should be called unless we can prove they won't have any reference to this (i.e. static functions taking only non-reference types).
Fact E is only adding this as part of immutable data structures (set and union, seq, datatypes). If expressions require accessing the fields of any object before new;, then we have to prove anyway that assigned(object`field) for any object and any field, so there is no problem about wrapping "this" in some immutable data structure before the new;.

So now, we have merely two choices:

• Be as precise as possible by defining assigned(object`field), and prevent calling functions and methods that are not {:constructor}
• Be less precise by 1) preventing functions and methods that might take references in argument before the new; 2) by only checking that every expression that might depend on this is not doing any kind of field dereference and 3) Performing unique definite assignment checking on all fields as if they were local variables

[MikaelMayer]

I was just checking the above and figured out that one of the thing that might be tricky for the first one is that, even if we checked definetedness when mentioning fields before the new;, could the verified actually pick up by itself the fact that the field is there to prove false, if the type it has is empty?

Here are my experiments that show how it's currently not possible to do so at least for local variables, although I'm not sure why:

Well-formedness check will prevent the code from verifying if x is mentioned, even once in ghost code:

[MikaelMayer]

It turns out, at least for the verifier of local variables, a subset type is assumed only after the first initialization. So for the verifier, x has type "Int" all the time, it's just that the subset constraint is assumed after the assignment.

However, I was able to coin an example that does verify for the latest Dafny

type Empty = x: int | false witness *

class TestEmpty {
  const x: Empty
  var y: int
  constructor() ensures false {
    x := 2;
    new;
    var y := x;
  }
}

This is alarming.

[MikaelMayer]

Inspecting the Boogie file reveals something curious:

implementation {:verboseName "TestEmpty._ctor (correctness)"} Impl$$_module.TestEmpty.__ctor() returns (this: ref, $_reverifyPost: bool)
{
  var $_Frame: <beta>[ref,Field beta]bool;
  var this.x: int;
  var this.y: int;
  var defass#this.x: bool;
  var defass#y#0: bool;
  var y#0: int where defass#y#0 ==> Lit(false);

    // AddMethodImpl: _ctor, Impl$$_module.TestEmpty.__ctor
    $_Frame := (lambda<alpha> $o: ref, $f: Field alpha :: 
      $o != null && read($Heap, $o, alloc) ==> false);
    $_reverifyPost := false;
    // ----- divided block before new; ----- C:\Users\mimayere\Documents\Dafny tests\classes-empty.dfy(6,32)
    // ----- assignment statement ----- C:\Users\mimayere\Documents\Dafny tests\classes-empty.dfy(7,7)
    assume true;
    assume true;
    assert $Is(LitInt(2), Tclass._module.Empty()); // Should not be provable
    this.x := LitInt(2);
    defass#this.x := true;
    // ----- new; ----- C:\Users\mimayere\Documents\Dafny tests\classes-empty.dfy(6,32)
    assert defass#this.x;
    assume !read($Heap, this, alloc);
    assume _module.TestEmpty.x(this) == this.x;
    assume read($Heap, this, _module.TestEmpty.y) == this.y;
    $Heap := update($Heap, this, alloc, true);
    assume $IsGoodHeap($Heap);
    assume $IsHeapAnchor($Heap);
    // ----- divided block after new; ----- C:\Users\mimayere\Documents\Dafny tests\classes-empty.dfy(6,32)
    // ----- assignment statement ----- C:\Users\mimayere\Documents\Dafny tests\classes-empty.dfy(9,11)
    assume true;
    assume true;
    y#0 := _module.TestEmpty.x(this);
}

It can prove assert $Is(LitInt(2), Tclass._module.Empty()); // Should not be provable if the last assignment y#0 := _module.TestEmpty.x(this); is present.

Iin this context with the last assignment, I try to add assert false after assert $Is(LitInt(2), Tclass._module.Empty());, then it complains it cannot prove the latter:

    assert $Is(LitInt(2), Tclass._module.Empty()); // Error, cannot prove
    assert false;

    assert $Is(LitInt(2), Tclass._module.Empty()); // OK, can prove
    //assert false;

but there is an axiom stating that the two are equivalent. Asserting false at the end always works though.

I shortened the issue tom:

  var y#0: int;
  assert $Is(LitInt(2), Tclass._module.Empty());
  y#0 := _module.TestEmpty.x(this);

which still verifies, despite $Is(LitInt(2), Tclass._module.Empty()) being a synonym of false.

Now, here is one axiom that is required for this to pass:

axiom 1 < $FunctionContextHeight
   ==> (forall $o: ref :: 
    { _module.TestEmpty.x($o) } 
    $o != null && dtype($o) == Tclass._module.TestEmpty?()
       ==> $Is(_module.TestEmpty.x($o), Tclass._module.Empty()));

As you can see, this axiom matches the RHS of the assignment of y, so it fires. Replacing $Is(_module.TestEmpty.x($o), Tclass._module.Empty()) by true removes the error, so it's truly because of that axiom that it can infer false.
It means that the SMT solver is able to instantiate it before the assignment.
And it makes sense. This axiom does not depend on y.

[MikaelMayer]

In short, the fact that there is a constant of a type an empty type is actually picked up before the new; thanks to the encoding, and the solver can assume false and that's it.

[MikaelMayer]

I minimized the example. SMT is more clever than I thought: No need to assign a variable at the end, just need to "ensures false"

type Empty = x: int | false witness *

class TestEmpty {
  const x: Empty
  constructor() ensures false {
    x := 2;
    new;
  }
}