this is not fresh and fresh in well-formedness

[MikaelMayer]

Dafny version

latest-nightly and 4.3.0

Code to produce this issue

class Test {
  constructor()
    ensures && fresh(this)
            && (var x := foo(); true)
  {
  }
}

predicate foo()
  requires false
  ensures foo() == true
{ false }

method Main() {
  var t := new Test();
  assert false;
}

Command to run and resulting output

Dafny verifies the code

What happened?

The well-formedness is proved using a contradiction, which we can leak with a predicate after the construction of the object and prove false.

What type of operating system are you experiencing the problem on?

Windows

[jtristan]

class A {
  constructor()
}

class Test {

  var x: A

  constructor()
    ensures fresh(this.x)
    ensures foo()
  {
    x := new A();
  }
}

predicate foo()
  requires false
  ensures false 
{ true }

method Main() {
  var t := new Test();
  assert false;
}

[jtristan]

Here is the relevant Boogie code:

procedure {:verboseName "Test._ctor (well-formedness)"} CheckWellFormed$$_module.Test.__ctor(this: ref
       where this != null
         && 
        $Is(this, Tclass._module.Test())
         && $IsAlloc(this, Tclass._module.Test(), $Heap));
  free requires 1 == $FunctionContextHeight;
  modifies $Heap;



implementation {:verboseName "Test._ctor (well-formedness)"} CheckWellFormed$$_module.Test.__ctor(this: ref)
{
  var $_Frame: <beta>[ref,Field beta]bool;

    // AddMethodImpl: _ctor, CheckWellFormed$$_module.Test.__ctor
    $_Frame := (lambda<alpha> $o: ref, $f: Field alpha :: 
      $o != null && read($Heap, $o, alloc) ==> false);
    havoc $Heap;
    assume (forall $o: ref :: 
      { $Heap[$o] } 
      $o != null && read(old($Heap), $o, alloc) ==> $Heap[$o] == old($Heap)[$o]);
    assume $HeapSucc(old($Heap), $Heap);
    assume this != null && !read(old($Heap), this, alloc);
    assert {:subsumption 0} Lit(false);
    assume Lit(false);
    assume _module.__default.foo#canCall();
    assume Lit(_module.__default.foo());
}

We can see that we both assume that this is allocated, in the precondition of the procedure, while we also assume that it is not with the fresh. It seems like perhaps we consider the object to be allocated sooner than we should?

Consequently, it really seems like a verifier problem rather than a logical one.

[RustanLeino]

The where clause of parameter this in the CheckWellFormed$$ procedure for Dafny constructors should not include $IsAlloc(this, Tclass._module.Test(), $Heap). In fact, we should make this be an out-parameter of such procedures, just like it is for the corresponding Impl$$ procedures.

The Call$$ procedure declares this to be an out-parameter and includes $IsAlloc(this, ...). That's fine for Call$$ (but not for CheckWellFormed$$ and Impl$$.

[atomb]

That seems like it should be relatively straightforward to fix. Would you agree, @jtristan and @RustanLeino? And do you think that, with the understanding that you have in mind, either of you would be up for trying to implement a fix?

[atomb]

Given @RustanLeino's comment on #5248, I'm re-opening this.