diff options
Diffstat (limited to 'Test/civl')
53 files changed, 624 insertions, 154 deletions
diff --git a/Test/civl/DeviceCache.bpl.expect b/Test/civl/DeviceCache.bpl.expect index c4cf5ccf..129e60e2 100644 --- a/Test/civl/DeviceCache.bpl.expect +++ b/Test/civl/DeviceCache.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 30 verified, 0 errors +Boogie program verifier finished with 39 verified, 0 errors diff --git a/Test/civl/FlanaganQadeer.bpl.expect b/Test/civl/FlanaganQadeer.bpl.expect index 00ddb38b..76a9a2bf 100644 --- a/Test/civl/FlanaganQadeer.bpl.expect +++ b/Test/civl/FlanaganQadeer.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 4 verified, 0 errors +Boogie program verifier finished with 8 verified, 0 errors diff --git a/Test/civl/Program1.bpl.expect b/Test/civl/Program1.bpl.expect index 41374b00..00ddb38b 100644 --- a/Test/civl/Program1.bpl.expect +++ b/Test/civl/Program1.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 2 verified, 0 errors +Boogie program verifier finished with 4 verified, 0 errors diff --git a/Test/civl/Program2.bpl.expect b/Test/civl/Program2.bpl.expect index a9949f2e..9823d44a 100644 --- a/Test/civl/Program2.bpl.expect +++ b/Test/civl/Program2.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 3 verified, 0 errors +Boogie program verifier finished with 6 verified, 0 errors diff --git a/Test/civl/Program3.bpl.expect b/Test/civl/Program3.bpl.expect index a9949f2e..9823d44a 100644 --- a/Test/civl/Program3.bpl.expect +++ b/Test/civl/Program3.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 3 verified, 0 errors +Boogie program verifier finished with 6 verified, 0 errors diff --git a/Test/civl/Program4.bpl b/Test/civl/Program4.bpl index 68c2a5f3..11ba8afa 100644 --- a/Test/civl/Program4.bpl +++ b/Test/civl/Program4.bpl @@ -1,67 +1,138 @@ // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" // RUN: %diff "%s.expect" "%t" -type Tid; -var {:layer 0,1} a:[Tid]int; +var {:layer 0,2} a:[int]int; +var {:layer 0,1} count: int; +var {:layer 1,1} {:linear "tid"} allocated:[int]bool; -procedure {:yields} {:layer 1} main() { - var {:linear "tid"} tid:Tid; +procedure {:yields} {:layer 2} main() +requires {:layer 1} allocated == MapConstBool(false); +{ + var {:layer 1} {:linear "tid"} tid:int; + var i: int; yield; - while (true) { - call tid := Allocate(); - async call P(tid); + assert {:layer 1} AllocInv(count, allocated); + while (true) + invariant {:layer 1} AllocInv(count, allocated); + { + call tid, i := Allocate(); + async call P(tid, i); yield; + assert {:layer 1} AllocInv(count, allocated); } yield; } -procedure {:yields} {:layer 1} P({:linear "tid"} tid: Tid) -ensures {:layer 1} a[tid] == old(a)[tid] + 1; +procedure {:yields} {:layer 2} P({:layer 1} {:linear "tid"} tid: int, i: int) +requires {:layer 1} tid == i; +requires {:layer 1} AllocInv(count, allocated); +ensures {:layer 1} AllocInv(count, allocated); +ensures {:layer 2} a[tid] == old(a)[tid] + 1; { var t:int; yield; - assert {:layer 1} a[tid] == old(a)[tid]; - call t := Read(tid); + assert {:layer 1} AllocInv(count, allocated); + assert {:layer 2} a[tid] == old(a)[tid]; + call t := Read(tid, i); yield; - assert {:layer 1} a[tid] == t; - call Write(tid, t + 1); + assert {:layer 1} AllocInv(count, allocated); + assert {:layer 2} a[tid] == t; + call Write(tid, i, t + 1); yield; - assert {:layer 1} a[tid] == t + 1; + assert {:layer 1} AllocInv(count, allocated); + assert {:layer 2} a[tid] == t + 1; } -procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: Tid) +procedure {:yields} {:layer 1,2} Allocate() returns ({:layer 1} {:linear "tid"} tid: int, i: int) +requires {:layer 1} AllocInv(count, allocated); +ensures {:layer 1} AllocInv(count, allocated); +ensures {:layer 1} tid == i; +ensures {:atomic} +|{A: + return true; +}|; { yield; - call tid := AllocateLow(); + assert {:layer 1} AllocInv(count, allocated); + call i := AllocateLow(); + call tid := MakeLinear(i); yield; + assert {:layer 1} AllocInv(count, allocated); } -procedure {:yields} {:layer 0,1} Read({:linear "tid"} tid: Tid) returns (val: int); +procedure {:yields} {:layer 1,2} Read({:layer 1} {:linear "tid"} tid: int, i: int) returns (val: int) +requires {:layer 1} tid == i; +requires {:layer 1} AllocInv(count, allocated); +ensures {:layer 1} AllocInv(count, allocated); ensures {:atomic} |{A: val := a[tid]; return true; }|; +{ + yield; + assert {:layer 1} AllocInv(count, allocated); + call val := ReadLow(i); + yield; + assert {:layer 1} AllocInv(count, allocated); +} -procedure {:yields} {:layer 0,1} Write({:linear "tid"} tid: Tid, val: int); +procedure {:yields} {:layer 1,2} Write({:layer 1} {:linear "tid"} tid: int, i: int, val: int) +requires {:layer 1} tid == i; +requires {:layer 1} AllocInv(count, allocated); +ensures {:layer 1} AllocInv(count, allocated); ensures {:atomic} |{A: a[tid] := val; return true; }|; +{ + yield; + assert {:layer 1} AllocInv(count, allocated); + call WriteLow(i, val); + yield; + assert {:layer 1} AllocInv(count, allocated); +} -procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: Tid); -ensures {:atomic} |{ A: return true; }|; +function {:inline} AllocInv(count: int, allocated:[int]bool): (bool) +{ + (forall x: int :: allocated[x] ==> x < count) +} + +procedure {:yields} {:layer 0,1} ReadLow(i: int) returns (val: int); +ensures {:atomic} +|{A: + val := a[i]; return true; +}|; + +procedure {:yields} {:layer 0,1} WriteLow(i: int, val: int); +ensures {:atomic} +|{A: + a[i] := val; return true; +}|; +procedure {:yields} {:layer 0,1} AllocateLow() returns (i: int); +ensures {:atomic} +|{A: + i := count; + count := i + 1; + return true; +}|; +// We can prove that this primitive procedure preserves the permission invariant locally. +// We only need to using its specification and the definitions of TidCollector and TidSetCollector. +procedure {:layer 1} MakeLinear(i: int) returns ({:linear "tid"} tid: int); +requires !allocated[i]; +modifies allocated; +ensures tid == i && allocated == old(allocated)[i := true]; -function {:builtin "MapConst"} MapConstBool(bool): [Tid]bool; -function {:builtin "MapOr"} MapOr([Tid]bool, [Tid]bool) : [Tid]bool; +function {:builtin "MapConst"} MapConstBool(bool): [int]bool; +function {:builtin "MapOr"} MapOr([int]bool, [int]bool) : [int]bool; -function {:inline} {:linear "tid"} TidCollector(x: Tid) : [Tid]bool +function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool { MapConstBool(false)[x := true] } -function {:inline} {:linear "tid"} TidSetCollector(x: [Tid]bool) : [Tid]bool +function {:inline} {:linear "tid"} TidSetCollector(x: [int]bool) : [int]bool { x } diff --git a/Test/civl/Program4.bpl.expect b/Test/civl/Program4.bpl.expect index a9949f2e..f08c6e00 100644 --- a/Test/civl/Program4.bpl.expect +++ b/Test/civl/Program4.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 3 verified, 0 errors +Boogie program verifier finished with 12 verified, 0 errors diff --git a/Test/civl/Program5.bpl.expect b/Test/civl/Program5.bpl.expect index fde7e712..4bcb1071 100644 --- a/Test/civl/Program5.bpl.expect +++ b/Test/civl/Program5.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 18 verified, 0 errors +Boogie program verifier finished with 21 verified, 0 errors diff --git a/Test/civl/StoreBuffer.bpl.expect b/Test/civl/StoreBuffer.bpl.expect index 8c74fe2e..1931ffd2 100644 --- a/Test/civl/StoreBuffer.bpl.expect +++ b/Test/civl/StoreBuffer.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 17 verified, 0 errors +Boogie program verifier finished with 27 verified, 0 errors diff --git a/Test/civl/akash.bpl.expect b/Test/civl/akash.bpl.expect index 00ddb38b..76a9a2bf 100644 --- a/Test/civl/akash.bpl.expect +++ b/Test/civl/akash.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 4 verified, 0 errors +Boogie program verifier finished with 8 verified, 0 errors diff --git a/Test/civl/alloc.bpl b/Test/civl/alloc.bpl new file mode 100644 index 00000000..68b7e6c6 --- /dev/null +++ b/Test/civl/alloc.bpl @@ -0,0 +1,175 @@ +// RUN: %boogie -noinfer -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +function {:builtin "MapConst"} MapConstBool(bool) : [int]bool; + +type lmap; +function {:linear "mem"} dom(lmap): [int]bool; +function map(lmap): [int]int; +function cons([int]bool, [int]int) : lmap; +axiom (forall x: [int]bool, y: [int]int :: {cons(x,y)} dom(cons(x, y)) == x && map(cons(x,y)) == y); + +function EmptyLmap(): (lmap); +axiom (dom(EmptyLmap()) == MapConstBool(false)); + +function Add(x: lmap, i: int): (lmap); +axiom (forall x: lmap, i: int :: dom(Add(x, i)) == dom(x)[i:=true] && map(Add(x, i)) == map(x)); + +function Remove(x: lmap, i: int): (lmap); +axiom (forall x: lmap, i: int :: dom(Remove(x, i)) == dom(x)[i:=false] && map(Remove(x, i)) == map(x)); + +function {:inline} PoolInv(unallocated:[int]bool, pool: lmap) : (bool) +{ + (forall x: int :: unallocated[x] ==> dom(pool)[x]) +} + +procedure {:yields} {:layer 2} Main() +requires {:layer 1} PoolInv(unallocated, pool); +ensures {:layer 1} PoolInv(unallocated, pool); +{ + var {:layer 1} {:linear "mem"} l: lmap; + var i: int; + par Yield() | Dummy(); + while (*) + invariant {:layer 1} PoolInv(unallocated, pool); + { + call l, i := Alloc(); + async call Thread(l, i); + par Yield() | Dummy(); + } + par Yield() | Dummy(); +} + +procedure {:yields} {:layer 2} Thread({:layer 1} {:linear_in "mem"} local_in: lmap, i: int) +requires {:layer 1} PoolInv(unallocated, pool); +ensures {:layer 1} PoolInv(unallocated, pool); +requires {:layer 1} dom(local_in)[i] && map(local_in)[i] == mem[i]; +requires {:layer 2} dom(local_in)[i]; +{ + var y, o: int; + var {:layer 1} {:linear "mem"} local: lmap; + var {:layer 1} {:linear "mem"} l: lmap; + + par YieldMem(local_in, i) | Dummy(); + call local := Copy(local_in); + call local := Write(local, i, 42); + call o := Read(local, i); + assert {:layer 2} o == 42; + while (*) + invariant {:layer 1} PoolInv(unallocated, pool); + { + call l, y := Alloc(); + call l := Write(l, y, 42); + call o := Read(l, y); + assert {:layer 2} o == 42; + call Free(l, y); + par Yield() | Dummy(); + } + par Yield() | Dummy(); +} + +procedure {:pure} {:inline 1} Copy({:linear_in "mem"} l: lmap) returns ({:linear "mem"} l': lmap) +{ + l' := l; +} + +procedure {:yields} {:layer 1,2} Alloc() returns ({:layer 1} {:linear "mem"} l: lmap, i: int) +requires {:layer 1} PoolInv(unallocated, pool); +ensures {:layer 1} PoolInv(unallocated, pool); +ensures {:layer 1} dom(l)[i] && map(l)[i] == mem[i]; +ensures {:right} |{ A: assume dom(l)[i]; return true; }|; +{ + call Yield(); + call i := PickAddr(); + call l := AllocLinear(i); + call YieldMem(l, i); +} + +procedure {:yields} {:layer 1,2} Free({:layer 1} {:linear_in "mem"} l: lmap, i: int) +requires {:layer 1} PoolInv(unallocated, pool); +ensures {:layer 1} PoolInv(unallocated, pool); +requires {:layer 1} dom(l)[i]; +ensures {:both} |{ A: return true; }|; +{ + call Yield(); + call FreeLinear(l, i); + call ReturnAddr(i); + call Yield(); +} + +procedure {:yields} {:layer 1,2} Read({:layer 1} {:linear "mem"} l: lmap, i: int) returns (o: int) +requires {:layer 1} PoolInv(unallocated, pool); +ensures {:layer 1} PoolInv(unallocated, pool); +requires {:layer 1} dom(l)[i] && map(l)[i] == mem[i]; +ensures {:both} |{ A: assert dom(l)[i]; o := map(l)[i]; return true; }|; +{ + call YieldMem(l, i); + call o := ReadLow(i); + call YieldMem(l, i); +} + +procedure {:yields} {:layer 1,2} Write({:layer 1} {:linear_in "mem"} l: lmap, i: int, o: int) returns ({:layer 1} {:linear "mem"} l': lmap) +requires {:layer 1} PoolInv(unallocated, pool); +ensures {:layer 1} PoolInv(unallocated, pool); +requires {:layer 1} dom(l)[i] && map(l)[i] == mem[i]; +ensures {:layer 1} dom(l')[i] && map(l')[i] == mem[i]; +ensures {:both} |{ A: assert dom(l)[i]; l' := cons(dom(l), map(l)[i := o]); return true; }|; +{ + call YieldMem(l, i); + call WriteLow(i, o); + call l' := WriteLinear(l, i, o); + call YieldMem(l', i); +} + +procedure {:layer 1} AllocLinear(i: int) returns ({:linear "mem"} l: lmap); +modifies pool; +requires dom(pool)[i]; +ensures pool == Remove(old(pool), i) && dom(l)[i] && map(l)[i] == mem[i]; + +procedure {:layer 1} FreeLinear({:linear_in "mem"} l: lmap, i: int); +modifies pool; +requires dom(l)[i]; +ensures pool == Add(old(pool), i); + +procedure {:layer 1} WriteLinear({:layer 1} {:linear_in "mem"} l: lmap, i: int, o: int) returns ({:layer 1} {:linear "mem"} l': lmap); +requires dom(l)[i]; +ensures l' == cons(dom(l), map(l)[i := o]); + +procedure {:yields} {:layer 1} Yield() +requires {:layer 1} PoolInv(unallocated, pool); +ensures {:layer 1} PoolInv(unallocated, pool); +{ + yield; + assert {:layer 1} PoolInv(unallocated, pool); +} + +procedure {:yields} {:layer 1} YieldMem({:layer 1} {:linear "mem"} l: lmap, i: int) +requires {:layer 1} PoolInv(unallocated, pool); +ensures {:layer 1} PoolInv(unallocated, pool); +requires {:layer 1} dom(l)[i] && map(l)[i] == mem[i]; +ensures {:layer 1} dom(l)[i] && map(l)[i] == mem[i]; +{ + yield; + assert {:layer 1} PoolInv(unallocated, pool); + assert {:layer 1} dom(l)[i] && map(l)[i] == mem[i]; +} + +procedure {:yields} {:layer 2} Dummy() +{ + yield; +} + +var {:layer 1, 1} {:linear "mem"} pool: lmap; +var {:layer 0, 1} mem:[int]int; +var {:layer 0, 1} unallocated:[int]bool; + +procedure {:yields} {:layer 0, 1} ReadLow(i: int) returns (o: int); +ensures {:atomic} |{ A: o := mem[i]; return true; }|; + +procedure {:yields} {:layer 0, 1} WriteLow(i: int, o: int); +ensures {:atomic} |{ A: mem[i] := o; return true; }|; + +procedure {:yields} {:layer 0, 1} PickAddr() returns (i: int); +ensures {:atomic} |{ A: assume unallocated[i]; unallocated[i] := false; return true; }|; + +procedure {:yields} {:layer 0, 1} ReturnAddr(i: int); +ensures {:atomic} |{ A: unallocated[i] := true; return true; }|;
\ No newline at end of file diff --git a/Test/civl/alloc.bpl.expect b/Test/civl/alloc.bpl.expect new file mode 100644 index 00000000..4bcb1071 --- /dev/null +++ b/Test/civl/alloc.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 21 verified, 0 errors diff --git a/Test/civl/bar.bpl.expect b/Test/civl/bar.bpl.expect index 810c93bf..be6722fe 100644 --- a/Test/civl/bar.bpl.expect +++ b/Test/civl/bar.bpl.expect @@ -10,4 +10,4 @@ Execution trace: (0,0): anon00 (0,0): inline$Impl_YieldChecker_PC_1$0$L0 -Boogie program verifier finished with 3 verified, 2 errors +Boogie program verifier finished with 8 verified, 2 errors diff --git a/Test/civl/chris2.bpl.expect b/Test/civl/chris2.bpl.expect index ddb8537e..f3b66f4a 100644 --- a/Test/civl/chris2.bpl.expect +++ b/Test/civl/chris2.bpl.expect @@ -15,4 +15,4 @@ Execution trace: Execution trace: (0,0): this_A -Boogie program verifier finished with 1 verified, 4 errors +Boogie program verifier finished with 2 verified, 4 errors diff --git a/Test/civl/chris5.bpl b/Test/civl/chris5.bpl new file mode 100644 index 00000000..23ebe424 --- /dev/null +++ b/Test/civl/chris5.bpl @@ -0,0 +1,19 @@ +// RUN: %boogie -noinfer -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var{:layer 1,1} g:int; + +procedure{:layer 1} P(x:int) + requires {:layer 1} x == 0; +{ +} + +procedure{:yields}{:layer 1,2} Y(x:int) + ensures{:atomic} |{ A: return true; }|; +{ + yield; + + call P(x); + assert{:layer 1} x == 0; + + yield; +} diff --git a/Test/civl/chris5.bpl.expect b/Test/civl/chris5.bpl.expect new file mode 100644 index 00000000..32b474f5 --- /dev/null +++ b/Test/civl/chris5.bpl.expect @@ -0,0 +1,7 @@ +chris5.bpl(15,3): Error BP5002: A precondition for this call might not hold. +chris5.bpl(6,3): Related location: This is the precondition that might not hold. +Execution trace: + chris5.bpl(13,3): anon0 + (0,0): anon00 + +Boogie program verifier finished with 1 verified, 1 error diff --git a/Test/civl/chris6.bpl b/Test/civl/chris6.bpl new file mode 100644 index 00000000..a0aecf1e --- /dev/null +++ b/Test/civl/chris6.bpl @@ -0,0 +1,14 @@ +// RUN: %boogie -noinfer -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure{:extern}{:yields}{:layer 1,2} P1(); + requires{:layer 1} false; + ensures{:atomic} |{ A: return true; }|; + +procedure{:yields}{:layer 2,3} P2() + ensures{:atomic} |{ A: return true; }|; +{ + assert{:layer 1} false; + yield; + call P1(); + yield; +} diff --git a/Test/civl/chris6.bpl.expect b/Test/civl/chris6.bpl.expect new file mode 100644 index 00000000..229e4e10 --- /dev/null +++ b/Test/civl/chris6.bpl.expect @@ -0,0 +1,5 @@ +chris6.bpl(10,3): Error BP5001: This assertion might not hold. +Execution trace: + chris6.bpl(10,3): anon0 + +Boogie program verifier finished with 1 verified, 1 error diff --git a/Test/civl/chris7.bpl b/Test/civl/chris7.bpl new file mode 100644 index 00000000..a8fd25d3 --- /dev/null +++ b/Test/civl/chris7.bpl @@ -0,0 +1,14 @@ +// RUN: %boogie -noinfer -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure{:layer 1}{:extern} P() returns(i:int); + +procedure{:yields}{:layer 1,1}{:extern} Y({:layer 1}x:int); + +procedure{:yields}{:layer 1,2} A({:layer 1}y:int) + ensures {:atomic} |{ A: return true; }|; +{ + var{:layer 1} tmp:int; + call Y(y); + call tmp := P(); + call Y(tmp); +} diff --git a/Test/civl/chris7.bpl.expect b/Test/civl/chris7.bpl.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/civl/chris7.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/civl/chris8.bpl b/Test/civl/chris8.bpl new file mode 100644 index 00000000..070cfec4 --- /dev/null +++ b/Test/civl/chris8.bpl @@ -0,0 +1,15 @@ +// RUN: %boogie -noinfer -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var{:layer 1,1} x:int; + +procedure{:layer 1}{:extern} P1(i:int); +procedure{:pure}{:extern} P2(j:int); + +procedure{:yields}{:layer 1,2} A1({:layer 1}i:int) + ensures {:atomic} |{ A: return true; }|; +{ + yield; + call P1(i); + call P2(i); + yield; +} diff --git a/Test/civl/chris8.bpl.expect b/Test/civl/chris8.bpl.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/civl/chris8.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/civl/civl-paper.bpl.expect b/Test/civl/civl-paper.bpl.expect index 11d204a8..bd1df2f9 100644 --- a/Test/civl/civl-paper.bpl.expect +++ b/Test/civl/civl-paper.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 35 verified, 0 errors +Boogie program verifier finished with 45 verified, 0 errors diff --git a/Test/civl/foo.bpl.expect b/Test/civl/foo.bpl.expect index 41e30691..44a93860 100644 --- a/Test/civl/foo.bpl.expect +++ b/Test/civl/foo.bpl.expect @@ -5,4 +5,4 @@ Execution trace: foo.bpl(14,3): inline$Incr_1$0$A (0,0): inline$Impl_YieldChecker_PC_1$0$L0 -Boogie program verifier finished with 4 verified, 1 error +Boogie program verifier finished with 9 verified, 1 error diff --git a/Test/civl/funky.bpl b/Test/civl/funky.bpl new file mode 100644 index 00000000..ad5bf271 --- /dev/null +++ b/Test/civl/funky.bpl @@ -0,0 +1,133 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +type X; +const nil: X; +function {:builtin "MapConst"} MapConstBool(bool) : [X]bool; +function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool +{ + MapConstBool(false)[x := true] +} + +var {:layer 0, 3} A: X; +var {:layer 0, 3} B: X; +var {:layer 0, 3} counter: int; + +procedure {:yields} {:layer 0, 3} LockA({:linear "tid"} tid: X); +ensures {:right} |{ A: assert tid != nil; assume A == nil; A := tid; return true; }|; + +procedure {:yields} {:layer 0, 1} IncrA({:linear "tid"} tid: X); +ensures {:right} |{ A: assert tid != nil && A == tid; counter := counter + 1; return true; }|; + +procedure {:yields} {:layer 0, 1} DecrA({:linear "tid"} tid: X); +ensures {:right} |{ A: assert tid != nil && A == tid; counter := counter - 1; return true; }|; + +procedure {:yields} {:layer 0, 3} UnlockA({:linear "tid"} tid: X); +ensures {:left} |{ A: assert tid != nil && A == tid; A := nil; return true; }|; + +procedure {:yields} {:layer 0, 3} LockB({:linear "tid"} tid: X); +ensures {:right} |{ A: assert tid != nil; assume B == nil; B := tid; return true; }|; + +procedure {:yields} {:layer 0, 2} IncrB({:linear "tid"} tid: X); +ensures {:atomic} |{ A: assert tid != nil && B == tid; counter := counter + 1; return true; }|; + +procedure {:yields} {:layer 0, 1} DecrB({:linear "tid"} tid: X); +ensures {:atomic} |{ A: assert tid != nil && B == tid; counter := counter - 1; return true; }|; + +procedure {:yields} {:layer 0, 3} UnlockB({:linear "tid"} tid: X); +ensures {:left} |{ A: assert tid != nil && B == tid; B := nil; return true; }|; + +procedure {:yields} {:layer 0, 3} AssertA({:linear "tid"} tid: X); +ensures {:atomic} |{ A: assert tid != nil && A == tid; assert counter >= -1; return true; }|; + +procedure {:yields} {:layer 0, 3} AssertB({:linear "tid"} tid: X); +ensures {:atomic} |{ A: assert tid != nil && A == tid && B == tid; assert counter == 0; return true; }|; + +procedure {:pure} AllocTid() returns ({:linear "tid"} tid: X); +ensures tid != nil; + +procedure {:yields} {:layer 1, 2} AbsDecrB({:linear "tid"} tid: X) +ensures {:right} |{ A: assert tid != nil && B == tid && counter == 0; counter := counter - 1; return true; }|; +{ + yield; + call DecrB(tid); + yield; +} + +procedure {:yields} {:layer 2, 3} AbsAssertA({:linear "tid"} tid: X) +ensures {:both} |{ A: assert tid != nil && A == tid; assert counter >= -1; return true; }|; +{ + yield; + call AssertA(tid); + yield; +} + +procedure {:yields} {:layer 2, 3} AbsAssertB({:linear "tid"} tid: X) +ensures {:both} |{ A: assert tid != nil && A == tid && B == tid; assert counter == 0; return true; }|; +{ + yield; + call AssertB(tid); + yield; +} + +procedure {:yields} {:layer 1} TA({:linear "tid"} tid: X) +requires {:layer 1} tid != nil; +{ + yield; + call LockA(tid); + call IncrA(tid); + call DecrA(tid); + call UnlockA(tid); + yield; +} + +procedure {:yields} {:layer 2, 3} TB({:linear "tid"} tid: X) +ensures {:both} |{ A: assert tid != nil && counter == 0; return true; }|; +{ + yield; + call LockB(tid); + call AbsDecrB(tid); + call IncrB(tid); + call UnlockB(tid); + yield; +} + +procedure {:yields} {:layer 3} AbsTB({:linear "tid"} tid: X) +requires {:layer 3} tid != nil && counter == 0; +{ + yield; + assert {:layer 3} counter == 0; + call TB(tid); + yield; +} + +procedure {:yields} {:layer 3} main({:linear "tid"} tid: X) +requires {:layer 3} tid != nil && counter == 0; +{ + var {:linear "tid"} cid: X; + + yield; + assert {:layer 3} counter == 0; + while (*) + invariant {:layer 3} counter == 0; + { + if (*) { + call cid := AllocTid(); + async call TA(cid); + } + if (*) { + call cid := AllocTid(); + async call AbsTB(cid); + } + yield; + assert {:layer 3} counter == 0; + call LockA(tid); + call AbsAssertA(tid); + call LockB(tid); + call AbsAssertB(tid); + call UnlockB(tid); + call UnlockA(tid); + yield; + assert {:layer 3} counter == 0; + } + yield; +}
\ No newline at end of file diff --git a/Test/civl/funky.bpl.expect b/Test/civl/funky.bpl.expect new file mode 100644 index 00000000..0a114594 --- /dev/null +++ b/Test/civl/funky.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 75 verified, 0 errors diff --git a/Test/civl/ghost.bpl b/Test/civl/ghost.bpl index 74d16acf..1468fa56 100644 --- a/Test/civl/ghost.bpl +++ b/Test/civl/ghost.bpl @@ -5,7 +5,7 @@ var {:layer 0} x: int; procedure {:yields} {:layer 0,1} Incr(); ensures {:right} |{ A: x := x + 1; return true; }|; -procedure ghost(y: int) returns (z: int) +procedure {:pure} ghost(y: int) returns (z: int) requires y == 1; ensures z == 2; { @@ -15,8 +15,7 @@ ensures z == 2; procedure {:yields} {:layer 1,2} Incr2() ensures {:right} |{ A: x := x + 2; return true; }|; { - var {:ghost} a: int; - var {:ghost} b: int; + var {:layer 1} a: int; yield; call a := ghost(1); @@ -25,7 +24,7 @@ ensures {:right} |{ A: x := x + 2; return true; }|; yield; } -procedure ghost_0() returns (z: int) +procedure {:layer 1} ghost_0() returns (z: int) ensures z == x; { z := x; @@ -34,8 +33,8 @@ ensures z == x; procedure {:yields} {:layer 1,2} Incr2_0() ensures {:right} |{ A: x := x + 2; return true; }|; { - var {:ghost} a: int; - var {:ghost} b: int; + var {:layer 1} a: int; + var {:layer 1} b: int; yield; call a := ghost_0(); diff --git a/Test/civl/ghost.bpl.expect b/Test/civl/ghost.bpl.expect index 9823d44a..76a9a2bf 100644 --- a/Test/civl/ghost.bpl.expect +++ b/Test/civl/ghost.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 6 verified, 0 errors +Boogie program verifier finished with 8 verified, 0 errors diff --git a/Test/civl/linear-set.bpl.expect b/Test/civl/linear-set.bpl.expect index 00ddb38b..76a9a2bf 100644 --- a/Test/civl/linear-set.bpl.expect +++ b/Test/civl/linear-set.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 4 verified, 0 errors +Boogie program verifier finished with 8 verified, 0 errors diff --git a/Test/civl/linear-set2.bpl.expect b/Test/civl/linear-set2.bpl.expect index 00ddb38b..76a9a2bf 100644 --- a/Test/civl/linear-set2.bpl.expect +++ b/Test/civl/linear-set2.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 4 verified, 0 errors +Boogie program verifier finished with 8 verified, 0 errors diff --git a/Test/civl/lock-introduced.bpl b/Test/civl/lock-introduced.bpl index fa0a3977..5403e5d4 100644 --- a/Test/civl/lock-introduced.bpl +++ b/Test/civl/lock-introduced.bpl @@ -67,6 +67,9 @@ ensures {:atomic} |{ A: assume !b; b := true; lock := tid; return true; }|; yield; L: call status := CAS(false, true); + if (status) { + call SetLock(tid); + } yield; goto A, B; @@ -85,9 +88,16 @@ ensures {:atomic} |{ A: b := false; lock := nil; return true; }|; { yield; call SET(false); + call SetLock(nil); yield; } +procedure {:layer 1} {:inline 1} SetLock(v: X) +modifies lock; +{ + lock := v; +} + procedure {:yields} {:layer 0,1} CAS(prev: bool, next: bool) returns (status: bool); ensures {:atomic} |{ A: goto B, C; diff --git a/Test/civl/lock-introduced.bpl.expect b/Test/civl/lock-introduced.bpl.expect index f08c6e00..8c74fe2e 100644 --- a/Test/civl/lock-introduced.bpl.expect +++ b/Test/civl/lock-introduced.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 12 verified, 0 errors +Boogie program verifier finished with 17 verified, 0 errors diff --git a/Test/civl/lock.bpl.expect b/Test/civl/lock.bpl.expect index 3e6d423a..76a9a2bf 100644 --- a/Test/civl/lock.bpl.expect +++ b/Test/civl/lock.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 5 verified, 0 errors +Boogie program verifier finished with 8 verified, 0 errors diff --git a/Test/civl/lock2.bpl.expect b/Test/civl/lock2.bpl.expect index 3e6d423a..76a9a2bf 100644 --- a/Test/civl/lock2.bpl.expect +++ b/Test/civl/lock2.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 5 verified, 0 errors +Boogie program verifier finished with 8 verified, 0 errors diff --git a/Test/civl/multiset.bpl.expect b/Test/civl/multiset.bpl.expect index 0a77c517..63682bb4 100644 --- a/Test/civl/multiset.bpl.expect +++ b/Test/civl/multiset.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 78 verified, 0 errors +Boogie program verifier finished with 85 verified, 0 errors diff --git a/Test/civl/new1.bpl.expect b/Test/civl/new1.bpl.expect index 41374b00..00ddb38b 100644 --- a/Test/civl/new1.bpl.expect +++ b/Test/civl/new1.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 2 verified, 0 errors +Boogie program verifier finished with 4 verified, 0 errors diff --git a/Test/civl/nocollector.bpl b/Test/civl/nocollector.bpl new file mode 100644 index 00000000..5a6f1e5d --- /dev/null +++ b/Test/civl/nocollector.bpl @@ -0,0 +1,8 @@ +// RUN: %boogie -noinfer -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var {:linear "L"} x:int; + +procedure{:yields}{:layer 1} P() +{ + yield; +} diff --git a/Test/civl/nocollector.bpl.expect b/Test/civl/nocollector.bpl.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/civl/nocollector.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/civl/one.bpl.expect b/Test/civl/one.bpl.expect index 37fad75c..41374b00 100644 --- a/Test/civl/one.bpl.expect +++ b/Test/civl/one.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 1 verified, 0 errors +Boogie program verifier finished with 2 verified, 0 errors diff --git a/Test/civl/par-incr.bpl.expect b/Test/civl/par-incr.bpl.expect index 00ddb38b..3e3dc54b 100644 --- a/Test/civl/par-incr.bpl.expect +++ b/Test/civl/par-incr.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 4 verified, 0 errors +Boogie program verifier finished with 7 verified, 0 errors diff --git a/Test/civl/parallel1.bpl.expect b/Test/civl/parallel1.bpl.expect index 889ee4f2..fa974099 100644 --- a/Test/civl/parallel1.bpl.expect +++ b/Test/civl/parallel1.bpl.expect @@ -5,4 +5,4 @@ Execution trace: parallel1.bpl(14,3): inline$Incr_1$0$A (0,0): inline$Impl_YieldChecker_PC_1$0$L0 -Boogie program verifier finished with 3 verified, 1 error +Boogie program verifier finished with 7 verified, 1 error diff --git a/Test/civl/parallel2.bpl.expect b/Test/civl/parallel2.bpl.expect index 3e6d423a..12041afe 100644 --- a/Test/civl/parallel2.bpl.expect +++ b/Test/civl/parallel2.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 5 verified, 0 errors +Boogie program verifier finished with 10 verified, 0 errors diff --git a/Test/civl/parallel4.bpl.expect b/Test/civl/parallel4.bpl.expect index 2d4c8148..baf228c8 100644 --- a/Test/civl/parallel4.bpl.expect +++ b/Test/civl/parallel4.bpl.expect @@ -3,4 +3,4 @@ Execution trace: parallel4.bpl(29,5): anon0 (0,0): anon01 -Boogie program verifier finished with 3 verified, 1 error +Boogie program verifier finished with 7 verified, 1 error diff --git a/Test/civl/parallel5.bpl.expect b/Test/civl/parallel5.bpl.expect index 3e6d423a..12041afe 100644 --- a/Test/civl/parallel5.bpl.expect +++ b/Test/civl/parallel5.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 5 verified, 0 errors +Boogie program verifier finished with 10 verified, 0 errors diff --git a/Test/civl/perm.bpl.expect b/Test/civl/perm.bpl.expect index 41374b00..00ddb38b 100644 --- a/Test/civl/perm.bpl.expect +++ b/Test/civl/perm.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 2 verified, 0 errors +Boogie program verifier finished with 4 verified, 0 errors diff --git a/Test/civl/t1.bpl.expect b/Test/civl/t1.bpl.expect index fcef7e58..27a208d4 100644 --- a/Test/civl/t1.bpl.expect +++ b/Test/civl/t1.bpl.expect @@ -6,4 +6,4 @@ Execution trace: t1.bpl(25,21): inline$SetG_1$0$A (0,0): inline$Impl_YieldChecker_A_1$0$L1 -Boogie program verifier finished with 4 verified, 1 error +Boogie program verifier finished with 9 verified, 1 error diff --git a/Test/civl/termination2.bpl.expect b/Test/civl/termination2.bpl.expect index 37fad75c..41374b00 100644 --- a/Test/civl/termination2.bpl.expect +++ b/Test/civl/termination2.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 1 verified, 0 errors +Boogie program verifier finished with 2 verified, 0 errors diff --git a/Test/civl/ticket.bpl b/Test/civl/ticket.bpl index 9fc55646..df19aae4 100644 --- a/Test/civl/ticket.bpl +++ b/Test/civl/ticket.bpl @@ -6,7 +6,6 @@ axiom (forall x: int, y: int :: RightOpen(x)[y] <==> y < x); axiom (forall x: int, y: int :: RightClosed(x)[y] <==> y <= x); type X; -function {:builtin "MapConst"} mapconstbool(bool): [X]bool; const nil: X; var {:layer 0,2} t: int; var {:layer 0,2} s: int; @@ -42,7 +41,7 @@ ensures {:layer 1} {:layer 2} xl != nil; } procedure {:yields} {:layer 2} main({:linear_in "tid"} xls':[X]bool) -requires {:layer 2} xls' == mapconstbool(true); +requires {:layer 2} xls' == MapConstBool(true); { var {:linear "tid"} tid: X; var {:linear "tid"} xls: [X]bool; @@ -132,7 +131,7 @@ ensures {:layer 1} Inv1(T,t); } procedure {:yields} {:layer 0,2} Init({:linear "tid"} xls:[X]bool); -ensures {:atomic} |{ A: assert xls == mapconstbool(true); cs := nil; t := 0; s := 0; T := RightOpen(0); return true; }|; +ensures {:atomic} |{ A: assert xls == MapConstBool(true); cs := nil; t := 0; s := 0; T := RightOpen(0); return true; }|; procedure {:yields} {:layer 0,1} GetTicket({:linear "tid"} tid: X) returns (m: int); ensures {:atomic} |{ A: m := t; t := t + 1; T[m] := true; return true; }|; diff --git a/Test/civl/ticket.bpl.expect b/Test/civl/ticket.bpl.expect index b072912b..dc45a0ee 100644 --- a/Test/civl/ticket.bpl.expect +++ b/Test/civl/ticket.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 16 verified, 0 errors +Boogie program verifier finished with 24 verified, 0 errors diff --git a/Test/civl/treiber-stack.bpl b/Test/civl/treiber-stack.bpl index 751ce861..a184886d 100644 --- a/Test/civl/treiber-stack.bpl +++ b/Test/civl/treiber-stack.bpl @@ -1,62 +1,71 @@ // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" // RUN: %diff "%s.expect" "%t" -type Node = int; -const unique null: Node; + +const null: int; type lmap; -function {:linear "Node"} dom(lmap): [Node]bool; -function map(lmap): [Node]Node; -function {:builtin "MapConst"} MapConstBool(bool) : [Node]bool; +function {:linear "Node"} dom(lmap): [int]bool; +function map(lmap): [int]int; +function {:builtin "MapConst"} MapConstBool(bool) : [int]bool; function EmptyLmap(): (lmap); axiom (dom(EmptyLmap()) == MapConstBool(false)); -function Add(x: lmap, i: Node, v: Node): (lmap); -axiom (forall x: lmap, i: Node, v: Node :: dom(Add(x, i, v)) == dom(x)[i:=true] && map(Add(x, i, v)) == map(x)[i := v]); +function Add(x: lmap, i: int, v: int): (lmap); +axiom (forall x: lmap, i: int, v: int :: dom(Add(x, i, v)) == dom(x)[i:=true] && map(Add(x, i, v)) == map(x)[i := v]); -function Remove(x: lmap, i: Node): (lmap); -axiom (forall x: lmap, i: Node :: dom(Remove(x, i)) == dom(x)[i:=false] && map(Remove(x, i)) == map(x)); +function Remove(x: lmap, i: int): (lmap); +axiom (forall x: lmap, i: int :: dom(Remove(x, i)) == dom(x)[i:=false] && map(Remove(x, i)) == map(x)); -procedure {:yields} {:layer 0,1} ReadTopOfStack() returns (v:Node); -ensures {:right} |{ A: assume dom(Stack)[v] || dom(Used)[v]; return true; }|; +procedure {:yields} {:layer 0,1} ReadTopOfStack() returns (v:int); +ensures {:right} |{ A: assume v == null || dom(Stack)[v] || Used[v]; return true; }|; -procedure {:yields} {:layer 0,1} Load(i:Node) returns (v:Node); -ensures {:right} |{ A: assert dom(Stack)[i] || dom(Used)[i]; goto B,C; +procedure {:yields} {:layer 0,1} Load(i:int) returns (v:int); +ensures {:right} |{ A: assert dom(Stack)[i] || Used[i]; goto B,C; B: assume dom(Stack)[i]; v := map(Stack)[i]; return true; C: assume !dom(Stack)[i]; return true; }|; -procedure {:yields} {:layer 0,1} Store({:linear_in "Node"} l_in:lmap, i:Node, v:Node) returns ({:linear "Node"} l_out:lmap); +procedure {:yields} {:layer 0,1} Store({:linear_in "Node"} l_in:lmap, i:int, v:int) returns ({:linear "Node"} l_out:lmap); ensures {:both} |{ A: assert dom(l_in)[i]; l_out := Add(l_in, i, v); return true; }|; -procedure {:yields} {:layer 0,1} TransferToStack(oldVal: Node, newVal: Node, {:linear_in "Node"} l_in:lmap) returns (r: bool, {:linear "Node"} l_out:lmap); +procedure {:yields} {:layer 0,1} TransferToStack(oldVal: int, newVal: int, {:linear_in "Node"} l_in:lmap) returns (r: bool, {:linear "Node"} l_out:lmap); ensures {:atomic} |{ A: assert dom(l_in)[newVal]; goto B,C; B: assume oldVal == TopOfStack; TopOfStack := newVal; l_out := EmptyLmap(); Stack := Add(Stack, newVal, map(l_in)[newVal]); r := true; return true; C: assume oldVal != TopOfStack; l_out := l_in; r := false; return true; }|; -procedure {:yields} {:layer 0,1} TransferFromStack(oldVal: Node, newVal: Node) returns (r: bool); +procedure {:yields} {:layer 0,1} TransferFromStack(oldVal: int, newVal: int) returns (r: bool); ensures {:atomic} |{ A: goto B,C; - B: assume oldVal == TopOfStack; TopOfStack := newVal; Used := Add(Used, oldVal, map(Stack)[oldVal]); Stack := Remove(Stack, oldVal); r := true; return true; + B: assume oldVal == TopOfStack; TopOfStack := newVal; Used[oldVal] := true; Stack := Remove(Stack, oldVal); r := true; return true; C: assume oldVal != TopOfStack; r := false; return true; }|; -var {:layer 0} TopOfStack: Node; +var {:layer 0} TopOfStack: int; var {:linear "Node"} {:layer 0} Stack: lmap; -function {:inline} Inv(TopOfStack: Node, Stack: lmap) : (bool) +function {:inline} Inv(TopOfStack: int, Stack: lmap) : (bool) { BetweenSet(map(Stack), TopOfStack, null)[TopOfStack] && Subset(BetweenSet(map(Stack), TopOfStack, null), Union(Singleton(null), dom(Stack))) } -var {:linear "Node"} {:layer 0} Used: lmap; +var {:linear "Node"} {:layer 0} Used: [int]bool; + +function {:inline} {:linear "Node"} NodeCollector(x: int) : [int]bool +{ + MapConstBool(false)[x := true] +} +function {:inline} {:linear "Node"} NodeSetCollector(x: [int]bool) : [int]bool +{ + x +} -procedure {:yields} {:layer 1} push(x: Node, {:linear_in "Node"} x_lmap: lmap) +procedure {:yields} {:layer 1} push(x: int, {:linear_in "Node"} x_lmap: lmap) requires {:layer 1} dom(x_lmap)[x]; requires {:layer 1} Inv(TopOfStack, Stack); ensures {:layer 1} Inv(TopOfStack, Stack); ensures {:atomic} |{ A: Stack := Add(Stack, x, TopOfStack); TopOfStack := x; return true; }|; { - var t: Node; + var t: int; var g: bool; var {:linear "Node"} t_lmap: lmap; @@ -71,7 +80,6 @@ ensures {:atomic} |{ A: Stack := Add(Stack, x, TopOfStack); TopOfStack := x; ret call t_lmap := Store(t_lmap, x, t); call g, t_lmap := TransferToStack(t, x, t_lmap); if (g) { - assert {:layer 1} map(Stack)[x] == t; break; } yield; @@ -82,13 +90,13 @@ ensures {:atomic} |{ A: Stack := Add(Stack, x, TopOfStack); TopOfStack := x; ret assert {:expand} {:layer 1} Inv(TopOfStack, Stack); } -procedure {:yields} {:layer 1} pop() returns (t: Node) +procedure {:yields} {:layer 1} pop() returns (t: int) requires {:layer 1} Inv(TopOfStack, Stack); ensures {:layer 1} Inv(TopOfStack, Stack); -ensures {:atomic} |{ A: assume TopOfStack != null; t := TopOfStack; Used := Add(Used, t, map(Stack)[t]); TopOfStack := map(Stack)[t]; Stack := Remove(Stack, t); return true; }|; +ensures {:atomic} |{ A: assume TopOfStack != null; t := TopOfStack; Used[t] := true; TopOfStack := map(Stack)[t]; Stack := Remove(Stack, t); return true; }|; { var g: bool; - var x: Node; + var x: int; yield; assert {:layer 1} Inv(TopOfStack, Stack); @@ -115,7 +123,6 @@ function Subset([int]bool, [int]bool) returns (bool); function Empty() returns ([int]bool); function Singleton(int) returns ([int]bool); -function Reachable([int,int]bool, int) returns ([int]bool); function Union([int]bool, [int]bool) returns ([int]bool); axiom(forall x:int :: !Empty()[x]); diff --git a/Test/civl/treiber-stack.bpl.expect b/Test/civl/treiber-stack.bpl.expect index 9823d44a..76a9a2bf 100644 --- a/Test/civl/treiber-stack.bpl.expect +++ b/Test/civl/treiber-stack.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 6 verified, 0 errors +Boogie program verifier finished with 8 verified, 0 errors diff --git a/Test/civl/wsq.bpl b/Test/civl/wsq.bpl index 17f53401..0a2227b6 100644 --- a/Test/civl/wsq.bpl +++ b/Test/civl/wsq.bpl @@ -89,13 +89,11 @@ ensures {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T); ensures {:atomic} |{ var i: int; A: assume status[i] == NOT_IN_Q; status[i] := IN_Q; return true; }|; { var t: int; - var {:ghost} oldH:int; - var {:ghost} oldT:int; - var {:ghost} oldStatusT:bool; + var {:layer 3} oldH:int; + var {:layer 3} oldT:int; + var {:layer 3} oldStatusT:bool; - - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; assert {:layer 3} {:expand} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); @@ -104,8 +102,7 @@ ensures {:atomic} |{ var i: int; A: assume status[i] == NOT_IN_Q; status[i] := I call t := readT_put(tid); - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && put_in_cs; assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); @@ -115,9 +112,8 @@ ensures {:atomic} |{ var i: int; A: assume status[i] == NOT_IN_Q; status[i] := I call writeItems_put(tid,t, task); - oldH := H; - oldT := T; - oldStatusT := status[T]; + call oldH, oldT := GhostRead(); + call oldStatusT := GhostReadStatus(); yield; assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && t == T && tid == ptTid && !take_in_cs && put_in_cs; assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); @@ -128,8 +124,7 @@ ensures {:atomic} |{ var i: int; A: assume status[i] == NOT_IN_Q; status[i] := I call writeT_put(tid, t+1); - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); @@ -147,11 +142,10 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu { var h, t: int; var chk: bool; - var {:ghost} oldH:int; - var {:ghost} oldT:int; + var {:layer 3} oldH:int; + var {:layer 3} oldT:int; - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); @@ -164,8 +158,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu invariant {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); { - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); @@ -173,8 +166,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu call t := readT_take_init(tid); - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); @@ -185,8 +177,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu t := t-1; call writeT_take(tid, t); - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && !take_in_cs && !put_in_cs && t_ss[tid] == t; assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); @@ -196,8 +187,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu call h := readH_take(tid); - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && take_in_cs && !put_in_cs && h_ss[tid] == h && t_ss[tid] == t; assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); @@ -214,8 +204,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu call writeT_take_abort(tid, h); task := EMPTY; - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} h <= H; assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; @@ -227,8 +216,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu call task, taskstatus := readItems(tid, t); - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} H >= h; assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && take_in_cs && h_ss[tid] == h && t_ss[tid] == t; @@ -240,8 +228,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu if(t>h) { call takeExitCS(tid); - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && h_ss[tid] == h && t_ss[tid] == t; assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); @@ -250,8 +237,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu return; } call writeT_take_eq(tid, h+1); - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t; @@ -265,8 +251,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu call chk := CAS_H_take(tid, h,h+1); - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} chk ==> (h+1 == oldH && h_ss[tid] == oldH -1 && task != EMPTY); assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t; @@ -279,8 +264,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu if(!chk) { - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t; assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); @@ -290,8 +274,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu goto LOOP_ENTRY_1; } - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t; assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); @@ -301,8 +284,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu return; } - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && !put_in_cs; assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); @@ -322,11 +304,10 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu { var h, t: int; var chk: bool; - var {:ghost} oldH:int; - var {:ghost} oldT:int; + var {:layer 3} oldH:int; + var {:layer 3} oldT:int; - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} stealerTid(tid); assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); @@ -341,8 +322,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu invariant {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); invariant {:layer 3} !steal_in_cs[tid]; { - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} stealerTid(tid); assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); @@ -352,8 +332,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu call h := readH_steal(tid); - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} H >= h; assert {:layer 3} !steal_in_cs[tid]; @@ -365,8 +344,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu call t := readT_steal(tid); - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} steal_in_cs[tid]; assert {:layer 3} stealerTid(tid) && H >= h && steal_in_cs[tid] && h_ss[tid] == h; @@ -381,8 +359,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu task := EMPTY; call stealExitCS(tid); - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} !steal_in_cs[tid]; assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid] && h_ss[tid] == h; @@ -395,8 +372,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu call task, taskstatus := readItems(tid, h); - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} stealerTid(tid) && steal_in_cs[tid] && h_ss[tid] == h; assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); @@ -408,8 +384,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu call chk := CAS_H_steal(tid, h,h+1); - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} h_ss[tid] == h; assert {:layer 3} chk ==> (h+1 == oldH && h_ss[tid] == h && task != EMPTY && taskstatus == IN_Q); @@ -423,8 +398,7 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu goto LOOP_ENTRY_2; } - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid]; assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); @@ -433,14 +407,24 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu return; } - oldH := H; - oldT := T; + call oldH, oldT := GhostRead(); yield; assert {:layer 3} chk && task != EMPTY; assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid]; assert {:layer 3} oldH <= H; } +procedure {:layer 3} {:inline 1} GhostRead() returns (oldH: int, oldT: int) +{ + oldH := H; + oldT := T; +} + +procedure {:layer 3} {:inline 1} GhostReadStatus() returns (oldStatus: bool) +{ + oldStatus := status[T]; +} + procedure {:yields}{:layer 0,3} readH_take({:linear "tid"} tid:Tid) returns (y: int); ensures {:atomic} |{A: assert tid == ptTid; y := H; diff --git a/Test/civl/wsq.bpl.expect b/Test/civl/wsq.bpl.expect index a9949f2e..9823d44a 100644 --- a/Test/civl/wsq.bpl.expect +++ b/Test/civl/wsq.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 3 verified, 0 errors +Boogie program verifier finished with 6 verified, 0 errors |