search

Whiley / Whiley2Boogie

A compiler backend for translating Whiley programs into Boogie programs for verification.
Apache License 2.0
1 stars 0 forks source link

Problem with Cyclic Reference Type Invariants #61

Open DavePearce opened 3 years ago

DavePearce commented 3 years ago

The following (Reference_Valid_11) fails for reasons unknown:

type Cyclic is { null|&Cyclic ptr, int data }

public export method test():
    &Cyclic p = new {ptr:null, data: 0}
    &Cyclic q = new {ptr:p, data: 0}
    // Make it cyclic!
    p->ptr = q

The relevant Boogie is (removing all box / unbox operations):

function Cyclic#is($ : Any, HEAP : [Ref]Any) returns (bool) {
  ((Record#is($) 
  && ((($[$ptr] == Null) || (Ref#is($[$ptr]) && Cyclic#is(HEAP[$[$ptr]],HEAP))) && Int#is($[$data]))) 
  && (forall f:Field :: (($ptr != f) && ($data != f)) ==> ($[f] == Void)))
}
  ...
   HEAP := HEAP[p:=HEAP[p][$ptr:=Ref#box(q)]];
   assert (HEAP[p][$ptr] == Null) 
            || (Ref#is(HEAP[p][$ptr]) && Cyclic#is(HEAP[HEAP[p][$ptr]],HEAP));
DavePearce commented 3 years ago

New version of Boogie / Z3 resolved this.

DavePearce commented 2 years ago

Still a problem for me now on Boogie 2.9.4.0 and z3 4.8.10