Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

this is not fresh and fresh in well-formedness #4700

Open
MikaelMayer opened this issue Oct 20, 2023 · 5 comments · Fixed by #5248
Open

this is not fresh and fresh in well-formedness #4700

MikaelMayer opened this issue Oct 20, 2023 · 5 comments · Fixed by #5248
Labels
during 3: execution of incorrect program An bug in the verifier that allows Dafny to run a program that does not correctly implement its spec introduced: v4.1.0 kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label makes-mikael-grateful This issue, is fixed, would make Mikael Mayer grateful part: verifier Translation from Dafny to Boogie (translator) priority: next Will consider working on this after in progress work is done

Comments

@MikaelMayer
Copy link
Member

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

@MikaelMayer MikaelMayer added kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label logic An inconsistency in Dafny's logic (e.g. in the Boogie prelude) makes-mikael-grateful This issue, is fixed, would make Mikael Mayer grateful during 3: execution of incorrect program An bug in the verifier that allows Dafny to run a program that does not correctly implement its spec and removed logic An inconsistency in Dafny's logic (e.g. in the Boogie prelude) labels Oct 20, 2023
@jtristan
Copy link
Contributor

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
Copy link
Contributor

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
Copy link
Collaborator

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
Copy link
Member

atomb commented Oct 23, 2023

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?

@keyboardDrummer keyboardDrummer added the priority: next Will consider working on this after in progress work is done label Feb 21, 2024
@atomb atomb assigned atomb and keyboardDrummer and unassigned atomb Mar 1, 2024
keyboardDrummer added a commit that referenced this issue Mar 27, 2024
#5248)

Fixes #4700

### Description
Fix a soundness issue that could be triggered by calling ensures fresh
in the post-condition of a constructor.

### How has this been tested?
Added a littish test

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
@atomb
Copy link
Member

atomb commented Mar 29, 2024

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

@atomb atomb reopened this Mar 29, 2024
@keyboardDrummer keyboardDrummer added the part: verifier Translation from Dafny to Boogie (translator) label Apr 29, 2024
@keyboardDrummer keyboardDrummer removed their assignment May 14, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
during 3: execution of incorrect program An bug in the verifier that allows Dafny to run a program that does not correctly implement its spec introduced: v4.1.0 kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label makes-mikael-grateful This issue, is fixed, would make Mikael Mayer grateful part: verifier Translation from Dafny to Boogie (translator) priority: next Will consider working on this after in progress work is done
Projects
None yet
Development

Successfully merging a pull request may close this issue.

5 participants