MikaelMayer
commented
10 months ago I think this issue could be solved with two things:
- (minimal) Arguments of calls to twostate predicates should always be checked for allocatedness on the heap before. But that would prevent a lot of useful scenarios like being about to reason about multiple references being allocated or not.
- Add an attribute like
{:assume _allocated false}on ghost predicates and functions so that allocation is no longer assumed and object access needs to be guarded. Such functions can never call another function or lemma not marked with{:assume _allocated false}- In this case, because allocatedness is state, we need a special reads clause saying our function depends on that state. Otherwise, the following would ensure false:
method Ooops() ensures false { var o := new O(); assert WasNotAllocatedBefore(o); label afterAlloc: o.x := 1; assert WasNotAllocatedBefore@afterAlloc(o); // No reads clause makes this function have the same value for both heaps! // Contradiction }
- In this case, because allocatedness is state, we need a special reads clause saying our function depends on that state. Otherwise, the following would ensure false:
class O { var x: int constructor() {} }
{:assume_allocated false} twostate predicate WasNotAllocatedBefore(o: O) { !old(allocated(o)) }
Put together, we would have the following code that would be sound:
```dafny
method Finallyyyyy()
{
var o := new O();
assert WasNotAllocatedBefore(o);
label afterAlloc:
o.x := 1;
assert WasNotAllocatedBefore@afterAlloc(o); // Error, because it reads the allocated bit which was modified for the first heap.
}
class O {
var x: int
constructor() {}
}
{:assume_allocated false}
twostate predicate WasNotAllocatedBefore(o: O)
reads o`allocated // Need a reads clause like this
{ !old(allocated(o)) }
RustanLeino
Dafny version
latest-nightly
Code to produce this issue
Command to run and resulting output
What happened?
Twostate predicates can refer to non-allocated state. However, they assume everything is allocated, so we can extract this assumption and prove that objects in their old state were not allocated. Even if we did not have this assumption in twostate predicate, they could call predicates that would in turn assume allocatedness. Or lemmas that could assume allocatedness.
Really it all boils down to alloc being a field and assuming it in ghost contexts when the ghost context could actually refer to an object before it was allocated (through
old@()), which is not possible for compiled contexts.My advice is that that every time we call a twostate function or twostate lemma in a method, we need to check
allocated()for all their arguments in the pre-state. In the example above, the proof obligationwould have caught the issue upfront.
In the long-term, we might want to have twostate functions, ghost functions and lemmas that would not assume allocatedness in any way; however, they become a new color of functions/lemmas as they should not be able to call other ghost functions or lemmas that assume allocatedness without proving the allocatedness of all their arguments. Still, they would make it possible to implement the following currently impossible program in Dafny
To solve the above issue, we could introduce quantification over any heap:
Note that in the above case, if we removed the argument for the test, we would still be able to write this as this is always allocated at the beginning of methods
and that would make our test to work
What type of operating system are you experiencing the problem on?
Windows