diff options
Diffstat (limited to 'Test/civl')
88 files changed, 4019 insertions, 0 deletions
diff --git a/Test/civl/DeviceCache.bpl b/Test/civl/DeviceCache.bpl new file mode 100644 index 00000000..01b1be01 --- /dev/null +++ b/Test/civl/DeviceCache.bpl @@ -0,0 +1,210 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +type X; +function {:builtin "MapConst"} mapconstbool(bool): [X]bool; +const nil: X; +var {:layer 0,1} ghostLock: X; +var {:layer 0,1} lock: X; +var {:layer 0,1} currsize: int; +var {:layer 0,1} newsize: int; + +function {:builtin "MapConst"} MapConstBool(bool) : [X]bool; +function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool +{ + MapConstBool(false)[x := true] +} +function {:inline} {:linear "tid"} TidSetCollector(x: [X]bool) : [X]bool +{ + x +} + +function {:inline} Inv(ghostLock: X, currsize: int, newsize: int) : (bool) +{ + 0 <= currsize && currsize <= newsize && + (ghostLock == nil <==> currsize == newsize) +} + +procedure {:yields} {:layer 1} Yield() +requires {:layer 1} Inv(ghostLock, currsize, newsize); +ensures {:layer 1} Inv(ghostLock, currsize, newsize); +{ + yield; + assert {:layer 1} Inv(ghostLock, currsize, newsize); +} + +procedure {:yields} {:layer 1} YieldToReadCache({:linear "tid"} tid: X) +requires {:layer 1} Inv(ghostLock, currsize, newsize) && tid != nil; +ensures {:layer 1} Inv(ghostLock, currsize, newsize) && old(currsize) <= currsize; +{ + yield; + assert {:layer 1} Inv(ghostLock, currsize, newsize) && old(currsize) <= currsize; +} + +procedure {:yields} {:layer 1} YieldToWriteCache({:linear "tid"} tid: X) +requires {:layer 1} Inv(ghostLock, currsize, newsize) && ghostLock == tid && tid != nil; +ensures {:layer 1} Inv(ghostLock, currsize, newsize) && ghostLock == tid && old(currsize) == currsize && old(newsize) == newsize; +{ + yield; + assert {:layer 1} Inv(ghostLock, currsize, newsize) && tid != nil && ghostLock == tid && old(currsize) == currsize && old(newsize) == newsize; +} + +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xl: X) +ensures {:layer 1} xl != nil; +{ + yield; + call xl := AllocateLow(); + yield; +} + +procedure {:yields} {:layer 1} main({:linear_in "tid"} xls: [X]bool) +requires {:layer 1} xls == mapconstbool(true); +{ + var {:linear "tid"} tid: X; + + yield; + + call Init(xls); + + yield; + assert {:layer 1} Inv(ghostLock, currsize, newsize); + + while (*) + invariant {:layer 1} Inv(ghostLock, currsize, newsize); + { + par tid := Allocate() | Yield(); + yield; + assert {:layer 1} Inv(ghostLock, currsize, newsize); + async call Thread(tid); + yield; + assert {:layer 1} Inv(ghostLock, currsize, newsize); + } + yield; +} + +procedure {:yields} {:layer 1} Thread({:linear "tid"} tid: X) +requires {:layer 1} tid != nil; +requires {:layer 1} Inv(ghostLock, currsize, newsize); +{ + var start, size, bytesRead: int; + + havoc start, size; + assume (0 <= start && 0 <= size); + call bytesRead := Read(tid, start, size); +} + +procedure {:yields} {:layer 1} Read({:linear "tid"} tid: X, start : int, size : int) returns (bytesRead : int) +requires {:layer 1} tid != nil; +requires {:layer 1} 0 <= start && 0 <= size; +requires {:layer 1} Inv(ghostLock, currsize, newsize); +ensures {:layer 1} 0 <= bytesRead && bytesRead <= size; +{ + var i, tmp: int; + + par YieldToReadCache(tid); + bytesRead := size; + call acquire(tid); + call i := ReadCurrsize(tid); + call tmp := ReadNewsize(tid); + if (start + size <= i) { + call release(tid); + goto COPY_TO_BUFFER; + } else if (tmp > i) { + bytesRead := if (start <= i) then (i - start) else 0; + call release(tid); + goto COPY_TO_BUFFER; + } else { + call WriteNewsize(tid, start + size); + call release(tid); + goto READ_DEVICE; + } + +READ_DEVICE: + par YieldToWriteCache(tid); + call WriteCache(tid, start + size); + par YieldToWriteCache(tid); + call acquire(tid); + call tmp := ReadNewsize(tid); + call WriteCurrsize(tid, tmp); + call release(tid); + +COPY_TO_BUFFER: + par YieldToReadCache(tid); + call ReadCache(tid, start, bytesRead); +} + +procedure {:yields} {:layer 1} WriteCache({:linear "tid"} tid: X, index: int) +requires {:layer 1} Inv(ghostLock, currsize, newsize); +requires {:layer 1} ghostLock == tid && tid != nil; +ensures {:layer 1} ghostLock == tid; +ensures {:layer 1} Inv(ghostLock, currsize, newsize) && old(currsize) == currsize && old(newsize) == newsize; +{ + var j: int; + + par YieldToWriteCache(tid); + call j := ReadCurrsize(tid); + while (j < index) + invariant {:layer 1} ghostLock == tid && currsize <= j && tid == tid; + invariant {:layer 1} Inv(ghostLock, currsize, newsize) && old(currsize) == currsize && old(newsize) == newsize; + { + par YieldToWriteCache(tid); + call WriteCacheEntry(tid, j); + j := j + 1; + } + par YieldToWriteCache(tid); +} + +procedure {:yields} {:layer 1} ReadCache({:linear "tid"} tid: X, start: int, bytesRead: int) +requires {:layer 1} Inv(ghostLock, currsize, newsize); +requires {:layer 1} tid != nil; +requires {:layer 1} 0 <= start && 0 <= bytesRead; +requires {:layer 1} (bytesRead == 0 || start + bytesRead <= currsize); +ensures {:layer 1} Inv(ghostLock, currsize, newsize); +{ + var j: int; + + par YieldToReadCache(tid); + + j := 0; + while(j < bytesRead) + invariant {:layer 1} 0 <= j; + invariant {:layer 1} bytesRead == 0 || start + bytesRead <= currsize; + invariant {:layer 1} Inv(ghostLock, currsize, newsize); + { + assert {:layer 1} start + j < currsize; + call ReadCacheEntry(tid, start + j); + j := j + 1; + par YieldToReadCache(tid); + } + + par YieldToReadCache(tid); +} + +procedure {:yields} {:layer 0,1} Init({:linear_in "tid"} xls:[X]bool); +ensures {:atomic} |{ A: assert xls == mapconstbool(true); currsize := 0; newsize := 0; lock := nil; ghostLock := nil; return true; }|; + +procedure {:yields} {:layer 0,1} ReadCurrsize({:linear "tid"} tid: X) returns (val: int); +ensures {:right} |{A: assert tid != nil; assert lock == tid || ghostLock == tid; val := currsize; return true; }|; + +procedure {:yields} {:layer 0,1} ReadNewsize({:linear "tid"} tid: X) returns (val: int); +ensures {:right} |{A: assert tid != nil; assert lock == tid || ghostLock == tid; val := newsize; return true; }|; + +procedure {:yields} {:layer 0,1} WriteNewsize({:linear "tid"} tid: X, val: int); +ensures {:atomic} |{A: assert tid != nil; assert lock == tid && ghostLock == nil; newsize := val; ghostLock := tid; return true; }|; + +procedure {:yields} {:layer 0,1} WriteCurrsize({:linear "tid"} tid: X, val: int); +ensures {:atomic} |{A: assert tid != nil; assert lock == tid && ghostLock == tid; currsize := val; ghostLock := nil; return true; }|; + +procedure {:yields} {:layer 0,1} ReadCacheEntry({:linear "tid"} tid: X, index: int); +ensures {:atomic} |{ A: assert 0 <= index && index < currsize; return true; }|; + +procedure {:yields} {:layer 0,1} WriteCacheEntry({:linear "tid"} tid: X, index: int); +ensures {:right} |{ A: assert tid != nil; assert currsize <= index && ghostLock == tid; return true; }|; + +procedure {:yields} {:layer 0,1} acquire({:linear "tid"} tid: X); +ensures {:right} |{ A: assert tid != nil; assume lock == nil; lock := tid; return true; }|; + +procedure {:yields} {:layer 0,1} release({:linear "tid"} tid: X); +ensures {:left} |{ A: assert tid != nil; assert lock == tid; lock := nil; return true; }|; + +procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: X); +ensures {:atomic} |{ A: assume tid != nil; return true; }|; diff --git a/Test/civl/DeviceCache.bpl.expect b/Test/civl/DeviceCache.bpl.expect new file mode 100644 index 00000000..129e60e2 --- /dev/null +++ b/Test/civl/DeviceCache.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 39 verified, 0 errors diff --git a/Test/civl/FlanaganQadeer.bpl b/Test/civl/FlanaganQadeer.bpl new file mode 100644 index 00000000..97df7ce2 --- /dev/null +++ b/Test/civl/FlanaganQadeer.bpl @@ -0,0 +1,75 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +type X; +const nil: X; +var {:layer 0,1} l: X; +var {:layer 0,1} x: int; + +function {:builtin "MapConst"} MapConstBool(bool) : [X]bool; +function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool +{ + MapConstBool(false)[x := true] +} + +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xl: X) +ensures {:layer 1} xl != nil; +{ + yield; + call xl := AllocateLow(); + yield; +} + +procedure {:yields} {:layer 1} main() +{ + var {:linear "tid"} tid: X; + var val: int; + + yield; + while (*) + { + call tid := Allocate(); + havoc val; + async call foo(tid, val); + yield; + } + yield; +} +procedure {:yields} {:layer 0,1} Lock(tid: X); +ensures {:atomic} |{A: assume l == nil; l := tid; return true; }|; + +procedure {:yields} {:layer 0,1} Unlock(); +ensures {:atomic} |{A: l := nil; return true; }|; + +procedure {:yields} {:layer 0,1} Set(val: int); +ensures {:atomic} |{A: x := val; return true; }|; + +procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xl: X); +ensures {:atomic} |{ A: assume xl != nil; return true; }|; + +procedure {:yields} {:layer 1} foo({:linear_in "tid"} tid': X, val: int) +requires {:layer 1} tid' != nil; +{ + var {:linear "tid"} tid: X; + tid := tid'; + + yield; + call Lock(tid); + call tid := Yield(tid); + call Set(val); + call tid := Yield(tid); + assert {:layer 1} x == val; + call tid := Yield(tid); + call Unlock(); + yield; +} + +procedure {:yields} {:layer 1} Yield({:linear_in "tid"} tid': X) returns ({:linear "tid"} tid: X) +requires {:layer 1} tid' != nil; +ensures {:layer 1} tid == tid'; +ensures {:layer 1} old(l) == tid ==> old(l) == l && old(x) == x; +{ + tid := tid'; + yield; + assert {:layer 1} tid != nil; + assert {:layer 1} (old(l) == tid ==> old(l) == l && old(x) == x); +}
\ No newline at end of file diff --git a/Test/civl/FlanaganQadeer.bpl.expect b/Test/civl/FlanaganQadeer.bpl.expect new file mode 100644 index 00000000..76a9a2bf --- /dev/null +++ b/Test/civl/FlanaganQadeer.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 8 verified, 0 errors diff --git a/Test/civl/Program1.bpl b/Test/civl/Program1.bpl new file mode 100644 index 00000000..5fe49480 --- /dev/null +++ b/Test/civl/Program1.bpl @@ -0,0 +1,33 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var {:layer 0,1} x:int; + +procedure {:yields} {:layer 1} p() +requires {:layer 1} x >= 5; +ensures {:layer 1} x >= 8; +{ + yield; + assert {:layer 1} x >= 5; + call Incr(1); + yield; + assert {:layer 1} x >= 6; + call Incr(1); + yield; + assert {:layer 1} x >= 7; + call Incr(1); + yield; + assert {:layer 1} x >= 8; +} + +procedure {:yields} {:layer 1} q() +{ + yield; + call Incr(3); + yield; +} + +procedure {:yields} {:layer 0,1} Incr(val: int); +ensures {:atomic} +|{A: + x := x + val; return true; +}|; diff --git a/Test/civl/Program1.bpl.expect b/Test/civl/Program1.bpl.expect new file mode 100644 index 00000000..00ddb38b --- /dev/null +++ b/Test/civl/Program1.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 4 verified, 0 errors diff --git a/Test/civl/Program2.bpl b/Test/civl/Program2.bpl new file mode 100644 index 00000000..16b20cf2 --- /dev/null +++ b/Test/civl/Program2.bpl @@ -0,0 +1,37 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var {:layer 0,1} x:int; + +procedure {:yields} {:layer 1} yield_x(n: int) +requires {:layer 1} x >= n; +ensures {:layer 1} x >= n; +{ + yield; + assert {:layer 1} x >= n; +} + +procedure {:yields} {:layer 1} p() +requires {:layer 1} x >= 5; +ensures {:layer 1} x >= 8; +{ + call yield_x(5); + call Incr(1); + call yield_x(6); + call Incr(1); + call yield_x(7); + call Incr(1); + call yield_x(8); +} + +procedure {:yields} {:layer 1} q() +{ + yield; + call Incr(3); + yield; +} + +procedure {:yields} {:layer 0,1} Incr(val: int); +ensures {:atomic} +|{A: + x := x + val; return true; +}|; diff --git a/Test/civl/Program2.bpl.expect b/Test/civl/Program2.bpl.expect new file mode 100644 index 00000000..9823d44a --- /dev/null +++ b/Test/civl/Program2.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 6 verified, 0 errors diff --git a/Test/civl/Program3.bpl b/Test/civl/Program3.bpl new file mode 100644 index 00000000..565279e7 --- /dev/null +++ b/Test/civl/Program3.bpl @@ -0,0 +1,36 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var {:layer 0,1} x:int; + +procedure {:yields} {:layer 1} yield_x() +ensures {:layer 1} x >= old(x); +{ + yield; + assert {:layer 1} x >= old(x); +} + +procedure {:yields} {:layer 1} p() +requires {:layer 1} x >= 5; +ensures {:layer 1} x >= 8; +{ + call yield_x(); + call Incr(1); + call yield_x(); + call Incr(1); + call yield_x(); + call Incr(1); + call yield_x(); +} + +procedure {:yields} {:layer 1} q() +{ + yield; + call Incr(3); + yield; +} + +procedure {:yields} {:layer 0,1} Incr(val: int); +ensures {:atomic} +|{A: + x := x + val; return true; +}|; diff --git a/Test/civl/Program3.bpl.expect b/Test/civl/Program3.bpl.expect new file mode 100644 index 00000000..9823d44a --- /dev/null +++ b/Test/civl/Program3.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 6 verified, 0 errors diff --git a/Test/civl/Program4.bpl b/Test/civl/Program4.bpl new file mode 100644 index 00000000..11ba8afa --- /dev/null +++ b/Test/civl/Program4.bpl @@ -0,0 +1,139 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +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 2} main() +requires {:layer 1} allocated == MapConstBool(false); +{ + var {:layer 1} {:linear "tid"} tid:int; + var i: int; + + yield; + 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 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} AllocInv(count, allocated); + assert {:layer 2} a[tid] == old(a)[tid]; + call t := Read(tid, i); + yield; + assert {:layer 1} AllocInv(count, allocated); + assert {:layer 2} a[tid] == t; + call Write(tid, i, t + 1); + yield; + assert {:layer 1} AllocInv(count, allocated); + assert {:layer 2} a[tid] == t + 1; +} + +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; + assert {:layer 1} AllocInv(count, allocated); + call i := AllocateLow(); + call tid := MakeLinear(i); + yield; + assert {:layer 1} AllocInv(count, allocated); +} + +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 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); +} + +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): [int]bool; +function {:builtin "MapOr"} MapOr([int]bool, [int]bool) : [int]bool; + +function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool +{ + MapConstBool(false)[x := true] +} +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 new file mode 100644 index 00000000..f08c6e00 --- /dev/null +++ b/Test/civl/Program4.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 12 verified, 0 errors diff --git a/Test/civl/Program5.bpl b/Test/civl/Program5.bpl new file mode 100644 index 00000000..362a6d9d --- /dev/null +++ b/Test/civl/Program5.bpl @@ -0,0 +1,84 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +type Tid; +const unique nil: Tid; + +function {:inline} UNALLOC():int { 0 } +function {:inline} WHITE():int { 1 } +function {:inline} GRAY():int { 2 } +function {:inline} BLACK():int { 3 } +function {:inline} Unalloc(i:int) returns(bool) { i <= 0 } +function {:inline} White(i:int) returns(bool) { i == 1 } +function {:inline} WhiteOrLighter(i:int) returns(bool) { i <= 1 } +function {:inline} Gray(i:int) returns(bool) { i == 2 } +function {:inline} Black(i:int) returns(bool) { i >= 3 } + +procedure {:yields} {:layer 2} YieldColorOnlyGetsDarker() +ensures {:layer 2} Color >= old(Color); +{ + yield; + assert {:layer 2} Color >= old(Color); +} + +procedure {:yields} {:layer 2,3} WriteBarrier({:linear "tid"} tid:Tid) +ensures {:atomic} |{ A: assert tid != nil; goto B, C; + B: assume White(Color); Color := GRAY(); return true; + C: assume !White(Color); return true;}|; +requires {:layer 2} Color >= WHITE(); +ensures {:layer 2} Color >= GRAY(); +{ + var colorLocal:int; + yield; + assert {:layer 2} Color >= WHITE(); + call colorLocal := GetColorNoLock(); + call YieldColorOnlyGetsDarker(); + if (WhiteOrLighter(colorLocal)) { call WriteBarrierSlow(tid); } + yield; + assert {:layer 2} Color >= GRAY(); +} + +procedure {:yields} {:layer 1,2} WriteBarrierSlow({:linear "tid"} tid:Tid) +ensures {:atomic} |{ A: assert tid != nil; goto B, C; + B: assume WhiteOrLighter(Color); Color := GRAY(); return true; + C: assume !WhiteOrLighter(Color); return true; }|; +{ + var colorLocal:int; + yield; + call AcquireLock(tid); + call colorLocal := GetColorLocked(tid); + if (WhiteOrLighter(colorLocal)) { call SetColorLocked(tid, GRAY()); } + call ReleaseLock(tid); + yield; +} + +procedure {:yields} {:layer 0,1} AcquireLock({:linear "tid"} tid: Tid); + ensures {:right} |{ A: assert tid != nil; assume lock == nil; lock := tid; return true; }|; + +procedure {:yields} {:layer 0,1} ReleaseLock({:linear "tid"} tid: Tid); + ensures {:left} |{ A: assert tid != nil; assert lock == tid; lock := nil; return true; }|; + +procedure {:yields} {:layer 0,1} SetColorLocked({:linear "tid"} tid:Tid, newCol:int); + ensures {:atomic} |{A: assert tid != nil; assert lock == tid; Color := newCol; return true;}|; + +procedure {:yields} {:layer 0,1} GetColorLocked({:linear "tid"} tid:Tid) returns (col:int); + ensures {:both} |{A: assert tid != nil; assert lock == tid; col := Color; return true;}|; + +procedure {:yields} {:layer 0,2} GetColorNoLock() returns (col:int); + ensures {:atomic} |{A: col := Color; return true;}|; + + + +function {:builtin "MapConst"} MapConstBool(bool): [Tid]bool; +function {:builtin "MapOr"} MapOr([Tid]bool, [Tid]bool) : [Tid]bool; + +var {:layer 0} Color:int; +var {:layer 0} lock:Tid; + +function {:inline} {:linear "tid"} TidCollector(x: Tid) : [Tid]bool +{ + MapConstBool(false)[x := true] +} +function {:inline} {:linear "tid"} TidSetCollector(x: [Tid]bool) : [Tid]bool +{ + x +} diff --git a/Test/civl/Program5.bpl.expect b/Test/civl/Program5.bpl.expect new file mode 100644 index 00000000..4bcb1071 --- /dev/null +++ b/Test/civl/Program5.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 21 verified, 0 errors diff --git a/Test/civl/StoreBuffer.bpl b/Test/civl/StoreBuffer.bpl new file mode 100644 index 00000000..d2d27ef9 --- /dev/null +++ b/Test/civl/StoreBuffer.bpl @@ -0,0 +1,187 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +function {:builtin "MapConst"} MapConstBool(bool) : [int]bool; + +function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool +{ + MapConstBool(false)[x := true] +} + +function {:inline} {:linear "addr"} AddrCollector(x: int) : [int]bool +{ + MapConstBool(false)[x := true] +} + +const numMutators: int; +axiom 0 < numMutators; +function {:inline} mutatorTid(i: int) : bool { 1 <= i && i <= numMutators } + +const GcTid: int; +axiom numMutators < GcTid; +function {:inline} mutatorOrGcTid(i: int) : bool { (1 <= i && i <= numMutators) || i == GcTid } + +const lockAddr: int; +axiom 0 < lockAddr; +const collectorPhaseAddr: int; +axiom lockAddr < collectorPhaseAddr; + +var {:layer 0,1} Mem: [int]int; +var {:layer 0,1} StoreBufferVal: [int][int]int; +var {:layer 0,1} StoreBufferPresent: [int][int]bool; + +var {:layer 0} lock: int; +var {:layer 0} collectorPhase: int; +var {:layer 0} collectorPhaseDelayed: int; + +function {:inline} LockInv(StoreBufferPresent:[int][int]bool, StoreBufferVal:[int][int]int, Mem:[int]int, lock:int, collectorPhase:int, collectorPhaseDelayed:int): bool +{ + (Mem[lockAddr] == 0 <==> lock == 0) && + (forall i:int :: mutatorOrGcTid(i) && StoreBufferPresent[i][lockAddr] ==> StoreBufferVal[i][lockAddr] == 0) && + (forall i:int :: mutatorOrGcTid(i) ==> lock == i || StoreBufferPresent[i] == MapConstBool(false)) && + (Mem[collectorPhaseAddr] == collectorPhase || (exists i:int :: mutatorOrGcTid(i) && StoreBufferPresent[i][collectorPhaseAddr])) && + (forall i:int :: mutatorOrGcTid(i) && StoreBufferPresent[i][collectorPhaseAddr] ==> StoreBufferVal[i][collectorPhaseAddr] == collectorPhase) && + collectorPhaseDelayed == Mem[collectorPhaseAddr] +} + +// Layer 1 +procedure {:yields} {:layer 1} YieldLock() +requires {:expand} {:layer 1} LockInv(StoreBufferPresent, StoreBufferVal, Mem, lock, collectorPhase, collectorPhaseDelayed); +ensures {:layer 1} LockInv(StoreBufferPresent, StoreBufferVal, Mem, lock, collectorPhase, collectorPhaseDelayed); +{ + yield; + assert {:layer 1} LockInv(StoreBufferPresent, StoreBufferVal, Mem, lock, collectorPhase, collectorPhaseDelayed); +} + +procedure {:yields} {:layer 1} YieldStoreBufferLockAddrPresent({:linear "tid"} tid:int) +requires {:layer 1} StoreBufferPresent[tid][lockAddr]; +ensures {:layer 1} StoreBufferPresent[tid][lockAddr]; +{ + yield; + assert {:layer 1} StoreBufferPresent[tid][lockAddr]; +} + +procedure {:yields} {:layer 1} YieldStoreBufferLockAddrAbsent({:linear "tid"} tid:int) +requires {:layer 1} !StoreBufferPresent[tid][lockAddr]; +ensures {:layer 1} !StoreBufferPresent[tid][lockAddr]; +{ + yield; + assert {:layer 1} !StoreBufferPresent[tid][lockAddr]; +} + +procedure {:yields} {:layer 1} LockAcquire({:linear "tid"} tid: int) +requires {:layer 1} mutatorOrGcTid(tid); +requires {:layer 1} LockInv(StoreBufferPresent, StoreBufferVal, Mem, lock, collectorPhase, collectorPhaseDelayed); +ensures {:layer 1} LockInv(StoreBufferPresent, StoreBufferVal, Mem, lock, collectorPhase, collectorPhaseDelayed); +ensures {:right} |{ A: assert mutatorOrGcTid(tid); assume lock == 0; lock := tid; return true; }|; +{ + var status:bool; + call YieldLock(); + while (true) + invariant {:layer 1} LockInv(StoreBufferPresent, StoreBufferVal, Mem, lock, collectorPhase, collectorPhaseDelayed); + { + call status := LockCAS(tid); + if (status) + { + call YieldLock(); + return; + } + call YieldLock(); + } + call YieldLock(); +} + +procedure {:yields} {:layer 1} LockRelease({:linear "tid"} tid:int) +requires {:layer 1} mutatorOrGcTid(tid); +requires {:layer 1} !StoreBufferPresent[tid][lockAddr]; +requires {:layer 1} LockInv(StoreBufferPresent, StoreBufferVal, Mem, lock, collectorPhase, collectorPhaseDelayed); +ensures {:layer 1} !StoreBufferPresent[tid][lockAddr]; +ensures {:layer 1} LockInv(StoreBufferPresent, StoreBufferVal, Mem, lock, collectorPhase, collectorPhaseDelayed); +ensures {:atomic} |{ A: assert mutatorOrGcTid(tid); assert lock == tid; lock := 0; return true; }|; +{ + par YieldLock() | YieldStoreBufferLockAddrAbsent(tid); + call LockZero(tid); + par YieldLock() | YieldStoreBufferLockAddrPresent(tid); + call FlushStoreBufferEntryForLock(tid); + par YieldLock() | YieldStoreBufferLockAddrAbsent(tid); +} + +procedure {:yields} {:layer 1} ReadCollectorPhaseLocked({:linear "tid"} tid: int) returns (phase: int) +requires {:layer 1} mutatorOrGcTid(tid); +requires {:layer 1} LockInv(StoreBufferPresent, StoreBufferVal, Mem, lock, collectorPhase, collectorPhaseDelayed); +ensures {:layer 1} LockInv(StoreBufferPresent, StoreBufferVal, Mem, lock, collectorPhase, collectorPhaseDelayed); +ensures {:atomic} |{ A: assert mutatorOrGcTid(tid); assert lock == tid; phase := collectorPhase; return true; }|; +{ + call YieldLock(); + call phase := PrimitiveRead(tid, collectorPhaseAddr); + call YieldLock(); +} + +procedure {:yields} {:layer 1} ReadCollectorPhaseUnlocked({:linear "tid"} tid: int) returns (phase: int) +requires {:layer 1} mutatorOrGcTid(tid); +requires {:layer 1} LockInv(StoreBufferPresent, StoreBufferVal, Mem, lock, collectorPhase, collectorPhaseDelayed); +ensures {:layer 1} LockInv(StoreBufferPresent, StoreBufferVal, Mem, lock, collectorPhase, collectorPhaseDelayed); +ensures {:atomic} |{ A: assert mutatorOrGcTid(tid); assert lock != tid; phase := collectorPhaseDelayed; return true; }|; +{ + call YieldLock(); + call phase := PrimitiveRead(tid, collectorPhaseAddr); + call YieldLock(); +} + +procedure {:yields} {:layer 1} SetCollectorPhase({:linear "tid"} tid: int, phase: int) +requires {:layer 1} mutatorOrGcTid(tid); +requires {:layer 1} LockInv(StoreBufferPresent, StoreBufferVal, Mem, lock, collectorPhase, collectorPhaseDelayed); +ensures {:layer 1} LockInv(StoreBufferPresent, StoreBufferVal, Mem, lock, collectorPhase, collectorPhaseDelayed); +ensures {:atomic} |{ A: assert mutatorOrGcTid(tid); assert lock == tid; assert collectorPhase == collectorPhaseDelayed; collectorPhase := phase; return true; }|; +{ + call YieldLock(); + call PrimitiveSetCollectorPhase(tid, phase); + call YieldLock(); +} + +procedure {:yields} {:layer 1} SyncCollectorPhase({:linear "tid"} tid: int) +requires {:layer 1} LockInv(StoreBufferPresent, StoreBufferVal, Mem, lock, collectorPhase, collectorPhaseDelayed); +ensures {:layer 1} LockInv(StoreBufferPresent, StoreBufferVal, Mem, lock, collectorPhase, collectorPhaseDelayed); +ensures {:atomic} |{ A: collectorPhaseDelayed := collectorPhase; return true; }|; +{ + call YieldLock(); + call FlushStoreBufferEntryForCollectorPhase(); + call YieldLock(); +} + +procedure {:yields} {:layer 1} Barrier({:linear "tid"} tid: int) +requires {:layer 1} mutatorOrGcTid(tid); +requires {:layer 1} LockInv(StoreBufferPresent, StoreBufferVal, Mem, lock, collectorPhase, collectorPhaseDelayed); +ensures {:layer 1} LockInv(StoreBufferPresent, StoreBufferVal, Mem, lock, collectorPhase, collectorPhaseDelayed); +ensures {:atomic} |{ A: assert mutatorOrGcTid(tid); assert lock == tid; assume collectorPhase == collectorPhaseDelayed; return true; }|; +{ + call YieldLock(); + call WaitForFlush(tid); + call YieldLock(); +} + +// Layer 0 +procedure {:yields} {:layer 0,1} LockCAS(tid: int) returns (status: bool); +ensures {:atomic} |{ A: goto B, C; + B: assume Mem[lockAddr] == 0; Mem[lockAddr] := 1; lock := tid; status := true; return true; + C: status := false; return true; + }|; + +procedure {:yields} {:layer 0,1} LockZero(tid: int); +ensures {:atomic} |{ A: assert !StoreBufferPresent[tid][lockAddr]; StoreBufferPresent[tid][lockAddr] := true; StoreBufferVal[tid][lockAddr] := 0; return true; }|; + +procedure {:yields} {:layer 0,1} FlushStoreBufferEntryForLock(tid: int); +ensures {:atomic} |{ A: assert StoreBufferPresent[tid][lockAddr]; assume StoreBufferPresent[tid] == MapConstBool(false)[lockAddr := true]; Mem[lockAddr] := StoreBufferVal[tid][lockAddr]; StoreBufferPresent[tid][lockAddr] := false; lock := 0; return true; }|; + +procedure {:yields} {:layer 0,1} PrimitiveRead(tid: int, addr: int) returns (val: int); +ensures {:atomic} |{ A: goto B, C; + B: assume StoreBufferPresent[tid][addr]; val := StoreBufferVal[tid][addr]; return true; + C: assume !StoreBufferPresent[tid][addr]; val := Mem[addr]; return true; }|; + +procedure {:yields} {:layer 0,1} PrimitiveSetCollectorPhase(tid: int, phase:int); +ensures {:atomic} |{ A: StoreBufferPresent[tid][collectorPhaseAddr] := true; StoreBufferVal[tid][collectorPhaseAddr] := phase; collectorPhase := phase; return true; }|; + +procedure {:yields} {:layer 0,1} FlushStoreBufferEntryForCollectorPhase(); +ensures {:atomic} |{ var tid:int; A: assume mutatorOrGcTid(tid) && StoreBufferPresent[tid][collectorPhaseAddr]; Mem[collectorPhaseAddr] := StoreBufferVal[tid][collectorPhaseAddr]; StoreBufferPresent[tid][collectorPhaseAddr] := false; collectorPhaseDelayed := Mem[collectorPhaseAddr]; return true; }|; + +procedure {:yields} {:layer 0,1} WaitForFlush(tid: int); +ensures {:atomic} |{ A: assume StoreBufferPresent[tid] == MapConstBool(false); return true; }|; diff --git a/Test/civl/StoreBuffer.bpl.expect b/Test/civl/StoreBuffer.bpl.expect new file mode 100644 index 00000000..1931ffd2 --- /dev/null +++ b/Test/civl/StoreBuffer.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 27 verified, 0 errors diff --git a/Test/civl/akash.bpl b/Test/civl/akash.bpl new file mode 100644 index 00000000..fabfcea5 --- /dev/null +++ b/Test/civl/akash.bpl @@ -0,0 +1,106 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +function {:builtin "MapConst"} mapconstbool(bool) : [int]bool; + +function {:builtin "MapConst"} MapConstBool(bool) : [int]bool; +function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool +{ + MapConstBool(false)[x := true] +} + +function {:inline} {:linear "1"} SetCollector1(x: [int]bool) : [int]bool +{ + x +} + +function {:inline} {:linear "2"} SetCollector2(x: [int]bool) : [int]bool +{ + x +} + +var {:layer 0,1} g: int; +var {:layer 0,1} h: int; + +procedure {:yields} {:layer 0,1} SetG(val:int); +ensures {:atomic} |{A: g := val; return true; }|; + +procedure {:yields} {:layer 0,1} SetH(val:int); +ensures {:atomic} |{A: h := val; return true; }|; + +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xl: int) +ensures {:layer 1} xl != 0; +{ + yield; + call xl := AllocateLow(); + yield; +} + +procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xls: int); +ensures {:atomic} |{ A: assume xls != 0; return true; }|; + +procedure {:yields} {:layer 1} A({:linear_in "tid"} tid_in: int, {:linear_in "1"} x: [int]bool, {:linear_in "2"} y: [int]bool) returns ({:linear "tid"} tid_out: int) +requires {:layer 1} x == mapconstbool(true); +requires {:layer 1} y == mapconstbool(true); +{ + var {:linear "tid"} tid_child: int; + tid_out := tid_in; + + yield; + call SetG(0); + yield; + assert {:layer 1} g == 0 && x == mapconstbool(true); + + yield; + call tid_child := Allocate(); + async call B(tid_child, x); + + yield; + call SetH(0); + + yield; + assert {:layer 1} h == 0 && y == mapconstbool(true); + + yield; + call tid_child := Allocate(); + async call C(tid_child, y); + + yield; +} + +procedure {:yields} {:layer 1} B({:linear_in "tid"} tid_in: int, {:linear_in "1"} x_in: [int]bool) +requires {:layer 1} x_in != mapconstbool(false); +{ + var {:linear "tid"} tid_out: int; + var {:linear "1"} x: [int]bool; + tid_out := tid_in; + x := x_in; + + yield; + + call SetG(1); + + yield; + + call SetG(2); + + yield; +} + +procedure {:yields} {:layer 1} C({:linear_in "tid"} tid_in: int, {:linear_in "2"} y_in: [int]bool) +requires {:layer 1} y_in != mapconstbool(false); +{ + var {:linear "tid"} tid_out: int; + var {:linear "2"} y: [int]bool; + tid_out := tid_in; + y := y_in; + + yield; + + call SetH(1); + + yield; + + call SetH(2); + + yield; +}
\ No newline at end of file diff --git a/Test/civl/akash.bpl.expect b/Test/civl/akash.bpl.expect new file mode 100644 index 00000000..76a9a2bf --- /dev/null +++ b/Test/civl/akash.bpl.expect @@ -0,0 +1,2 @@ + +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 b/Test/civl/bar.bpl new file mode 100644 index 00000000..b5068edd --- /dev/null +++ b/Test/civl/bar.bpl @@ -0,0 +1,57 @@ +// RUN: %boogie -noinfer "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var {:layer 0,1} g:int; + +procedure {:yields} {:layer 1} PB() +{ + yield; + call Incr(); + yield; +} + +procedure {:yields} {:layer 0,1} Incr(); +ensures {:atomic} +|{A: + g := g + 1; return true; +}|; + +procedure {:yields} {:layer 0,1} Set(v: int); +ensures {:atomic} +|{A: + g := v; return true; +}|; + +procedure {:yields} {:layer 1} PC() +ensures {:layer 1} g == old(g); +{ + yield; + assert {:layer 1} g == old(g); +} + +procedure {:yields} {:layer 1} PE() +{ + call PC(); +} + +procedure {:yields} {:layer 1} PD() +{ + yield; + call Set(3); + call PC(); + assert {:layer 1} g == 3; +} + +procedure {:yields} {:layer 1} Main2() +{ + yield; + while (*) + { + async call PB(); + yield; + async call PE(); + yield; + async call PD(); + yield; + } + yield; +} diff --git a/Test/civl/bar.bpl.expect b/Test/civl/bar.bpl.expect new file mode 100644 index 00000000..be6722fe --- /dev/null +++ b/Test/civl/bar.bpl.expect @@ -0,0 +1,13 @@ +bar.bpl(28,3): Error: Non-interference check failed +Execution trace: + bar.bpl(7,3): anon0 + (0,0): anon00 + bar.bpl(14,3): inline$Incr_1$0$A + (0,0): inline$Impl_YieldChecker_PC_1$0$L0 +bar.bpl(28,3): Error: Non-interference check failed +Execution trace: + bar.bpl(38,3): anon0 + (0,0): anon00 + (0,0): inline$Impl_YieldChecker_PC_1$0$L0 + +Boogie program verifier finished with 8 verified, 2 errors diff --git a/Test/civl/chris.bpl b/Test/civl/chris.bpl new file mode 100644 index 00000000..d755c76d --- /dev/null +++ b/Test/civl/chris.bpl @@ -0,0 +1,28 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var{:layer 1} x:int; + +procedure{:yields}{:layer 2} Havoc() + ensures{:atomic} |{ A: return true; }|; +{ + yield; +} + +procedure{:yields}{:layer 1} Recover() + ensures{:atomic} |{ A: assert x == 5; return true; }|; +{ + yield; +} + +procedure{:yields}{:layer 3} P() + ensures{:atomic} |{ A: return true; }|; + requires{:layer 2,3} x == 5; + ensures {:layer 2,3} x == 5; +{ + + yield; assert{:layer 2,3} x == 5; + call Havoc(); + yield; assert{:layer 3} x == 5; + call Recover(); + yield; assert{:layer 2,3} x == 5; +} diff --git a/Test/civl/chris.bpl.expect b/Test/civl/chris.bpl.expect new file mode 100644 index 00000000..9823d44a --- /dev/null +++ b/Test/civl/chris.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 6 verified, 0 errors diff --git a/Test/civl/chris2.bpl b/Test/civl/chris2.bpl new file mode 100644 index 00000000..268c6aa3 --- /dev/null +++ b/Test/civl/chris2.bpl @@ -0,0 +1,34 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var{:layer 20} x:int; + +procedure{:yields}{:layer 20,25} p_gt1_lower(); + ensures{:both} + |{ + A: + x := x + 1; + return true; + }|; + +procedure{:yields}{:layer 25,40} p_gt1() + ensures{:both} + |{ + A: + x := x + 1; + return true; + }|; +{ + yield; + call p_gt1_lower(); + yield; +} + +procedure{:yields}{:layer 20,40} p_gt2(); + ensures{:both} + |{ + A: + assert x == 0; + return true; + }|; + + diff --git a/Test/civl/chris2.bpl.expect b/Test/civl/chris2.bpl.expect new file mode 100644 index 00000000..f3b66f4a --- /dev/null +++ b/Test/civl/chris2.bpl.expect @@ -0,0 +1,18 @@ +(0,0): Error BP5003: A postcondition might not hold on this return path. +chris2.bpl(30,5): Related location: Gate not preserved by p_gt1_lower +Execution trace: + (0,0): this_A +(0,0): Error BP5003: A postcondition might not hold on this return path. +(0,0): Related location: Gate failure of p_gt2 not preserved by p_gt1_lower +Execution trace: + (0,0): this_A +(0,0): Error BP5003: A postcondition might not hold on this return path. +chris2.bpl(30,5): Related location: Gate not preserved by p_gt1 +Execution trace: + (0,0): this_A +(0,0): Error BP5003: A postcondition might not hold on this return path. +(0,0): Related location: Gate failure of p_gt2 not preserved by p_gt1 +Execution trace: + (0,0): this_A + +Boogie program verifier finished with 2 verified, 4 errors diff --git a/Test/civl/chris3.bpl b/Test/civl/chris3.bpl new file mode 100644 index 00000000..5cbc000a --- /dev/null +++ b/Test/civl/chris3.bpl @@ -0,0 +1,19 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure{:yields}{:layer 94,94} H() +{ + yield; +} + +procedure{:yields}{:layer 94,95} A() + ensures{:atomic} |{ A: return true; }|; +{ + yield; +} + +procedure{:yields}{:layer 95,95} P() +{ + yield; + par A() | H(); + yield; +} diff --git a/Test/civl/chris3.bpl.expect b/Test/civl/chris3.bpl.expect new file mode 100644 index 00000000..b415d3b9 --- /dev/null +++ b/Test/civl/chris3.bpl.expect @@ -0,0 +1,2 @@ +chris3.bpl(17,2): Error: The callee is not available in the caller procedure +1 type checking errors detected in chris3.bpl diff --git a/Test/civl/chris4.bpl b/Test/civl/chris4.bpl new file mode 100644 index 00000000..7a19f975 --- /dev/null +++ b/Test/civl/chris4.bpl @@ -0,0 +1,16 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure{:yields}{:layer 94,95} Test() +{ + yield; + L: + yield; +} + +procedure{:yields}{:layer 94,95} Test2() +{ + yield; + assert{:layer 94} 2 + 2 == 3; + L: + yield; +} diff --git a/Test/civl/chris4.bpl.expect b/Test/civl/chris4.bpl.expect new file mode 100644 index 00000000..d3d00979 --- /dev/null +++ b/Test/civl/chris4.bpl.expect @@ -0,0 +1,5 @@ +chris4.bpl(13,3): Error BP5001: This assertion might not hold. +Execution trace: + chris4.bpl(12,3): anon0 + +Boogie program verifier finished with 1 verified, 1 error 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 b/Test/civl/civl-paper.bpl new file mode 100644 index 00000000..6cac5cea --- /dev/null +++ b/Test/civl/civl-paper.bpl @@ -0,0 +1,175 @@ +// 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] +} + +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); + +var {:layer 0,3} {:linear "mem"} g: lmap; +var {:layer 0,3} lock: X; +var {:layer 0,1} b: bool; + +const p: int; + +procedure {:yields} {:layer 1} Yield1() +requires {:layer 1} InvLock(lock, b); +ensures {:layer 1} InvLock(lock, b); +{ + yield; + assert {:layer 1} InvLock(lock, b); +} + +function {:inline} InvLock(lock: X, b: bool) : bool +{ + lock != nil <==> b +} + +procedure {:yields} {:layer 2} Yield2() +{ + yield; +} + +procedure {:yields} {:layer 3} Yield3() +requires {:layer 3} Inv(g); +ensures {:layer 3} Inv(g); +{ + yield; + assert {:layer 3} Inv(g); +} + +function {:inline} Inv(g: lmap) : bool +{ + dom(g)[p] && dom(g)[p+4] && map(g)[p] == map(g)[p+4] +} + +procedure {:yields} {:layer 3} P({:linear "tid"} tid: X) +requires {:layer 1} tid != nil && InvLock(lock, b); +ensures {:layer 1} InvLock(lock, b); +requires {:layer 3} tid != nil && Inv(g); +ensures {:layer 3} Inv(g); +{ + var t: int; + var {:linear "mem"} l: lmap; + + par Yield3() | Yield1(); + call AcquireProtected(tid); + call l := TransferFromGlobalProtected(tid); + call t := Load(l, p); + call l := Store(l, p, t+1); + call t := Load(l, p+4); + call l := Store(l, p+4, t+1); + call TransferToGlobalProtected(tid, l); + call ReleaseProtected(tid); + par Yield3() | Yield1(); +} + + +procedure {:yields} {:layer 2,3} TransferToGlobalProtected({:linear "tid"} tid: X, {:linear_in "mem"} l: lmap) +ensures {:both} |{ A: assert tid != nil && lock == tid; g := l; return true; }|; +requires {:layer 1} InvLock(lock, b); +ensures {:layer 1} InvLock(lock, b); +{ + par Yield1() | Yield2(); + call TransferToGlobal(tid, l); + par Yield1() | Yield2(); +} + +procedure {:yields} {:layer 2,3} TransferFromGlobalProtected({:linear "tid"} tid: X) returns ({:linear "mem"} l: lmap) +ensures {:both} |{ A: assert tid != nil && lock == tid; l := g; return true; }|; +requires {:layer 1} InvLock(lock, b); +ensures {:layer 1} InvLock(lock, b); +{ + par Yield1() | Yield2(); + call l := TransferFromGlobal(tid); + par Yield1() | Yield2(); +} + +procedure {:yields} {:layer 2,3} AcquireProtected({:linear "tid"} tid: X) +ensures {:right} |{ A: assert tid != nil; assume lock == nil; lock := tid; return true; }|; +requires {:layer 1} tid != nil && InvLock(lock, b); +ensures {:layer 1} InvLock(lock, b); +{ + par Yield1() | Yield2(); + call Acquire(tid); + par Yield1() | Yield2(); +} + +procedure {:yields} {:layer 2,3} ReleaseProtected({:linear "tid"} tid: X) +ensures {:left} |{ A: assert tid != nil && lock == tid; lock := nil; return true; }|; +requires {:layer 1} InvLock(lock, b); +ensures {:layer 1} InvLock(lock, b); +{ + par Yield1() | Yield2(); + call Release(tid); + par Yield1() | Yield2(); +} + +procedure {:yields} {:layer 1,2} Acquire({:linear "tid"} tid: X) +requires {:layer 1} tid != nil && InvLock(lock, b); +ensures {:layer 1} InvLock(lock, b); +ensures {:atomic} |{ A: assume lock == nil; lock := tid; return true; }|; +{ + var status: bool; + var tmp: X; + + par Yield1(); + L: + assert {:layer 1} InvLock(lock, b); + call status := CAS(tid, false, true); + par Yield1(); + goto A, B; + + A: + assume status; + par Yield1(); + return; + + B: + assume !status; + goto L; +} + +procedure {:yields} {:layer 1,2} Release({:linear "tid"} tid: X) +ensures {:atomic} |{ A: lock := nil; return true; }|; +requires {:layer 1} InvLock(lock, b); +ensures {:layer 1} InvLock(lock, b); +{ + par Yield1(); + call CLEAR(tid, false); + par Yield1(); +} + +procedure {:yields} {:layer 0,2} TransferToGlobal({:linear "tid"} tid: X, {:linear_in "mem"} l: lmap); +ensures {:atomic} |{ A: g := l; return true; }|; + +procedure {:yields} {:layer 0,2} TransferFromGlobal({:linear "tid"} tid: X) returns ({:linear "mem"} l: lmap); +ensures {:atomic} |{ A: l := g; return true; }|; + +procedure {:yields} {:layer 0,3} Load({:linear "mem"} l: lmap, a: int) returns (v: int); +ensures {:both} |{ A: v := map(l)[a]; return true; }|; + +procedure {:yields} {:layer 0,3} Store({:linear_in "mem"} l_in: lmap, a: int, v: int) returns ({:linear "mem"} l_out: lmap); +ensures {:both} |{ A: assume l_out == cons(dom(l_in), map(l_in)[a := v]); return true; }|; + +procedure {:yields} {:layer 0,1} CAS(tid: X, prev: bool, next: bool) returns (status: bool); +ensures {:atomic} |{ +A: goto B, C; +B: assume b == prev; b := next; status := true; lock := tid; return true; +C: status := false; return true; +}|; + +procedure {:yields} {:layer 0,1} CLEAR(tid: X, next: bool); +ensures {:atomic} |{ +A: b := next; lock := nil; return true; +}|; + diff --git a/Test/civl/civl-paper.bpl.expect b/Test/civl/civl-paper.bpl.expect new file mode 100644 index 00000000..bd1df2f9 --- /dev/null +++ b/Test/civl/civl-paper.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 45 verified, 0 errors diff --git a/Test/civl/foo.bpl b/Test/civl/foo.bpl new file mode 100644 index 00000000..8b7b4aa6 --- /dev/null +++ b/Test/civl/foo.bpl @@ -0,0 +1,57 @@ +// RUN: %boogie -noinfer "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var {:layer 0,1} g:int; + +procedure {:yields} {:layer 1} PB() +{ + yield; + call Incr(); + yield; +} + +procedure {:yields} {:layer 0,1} Incr(); +ensures {:atomic} +|{A: + g := g + 1; return true; +}|; + +procedure {:yields} {:layer 0,1} Set(v: int); +ensures {:atomic} +|{A: + g := v; return true; +}|; + +procedure {:yields} {:layer 1} PC() +ensures {:layer 1} g == 3; +{ + yield; + call Set(3); + yield; + assert {:layer 1} g == 3; +} + +procedure {:yields} {:layer 1} PE() +{ + call PC(); +} + +procedure {:yields} {:layer 1} PD() +{ + call PC(); + assert {:layer 1} g == 3; +} + +procedure {:yields} {:layer 1} Main() +{ + yield; + while (*) + { + async call PB(); + yield; + async call PE(); + yield; + async call PD(); + yield; + } + yield; +} diff --git a/Test/civl/foo.bpl.expect b/Test/civl/foo.bpl.expect new file mode 100644 index 00000000..44a93860 --- /dev/null +++ b/Test/civl/foo.bpl.expect @@ -0,0 +1,8 @@ +foo.bpl(30,3): Error: Non-interference check failed +Execution trace: + foo.bpl(7,3): anon0 + (0,0): anon00 + foo.bpl(14,3): inline$Incr_1$0$A + (0,0): inline$Impl_YieldChecker_PC_1$0$L0 + +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 new file mode 100644 index 00000000..1468fa56 --- /dev/null +++ b/Test/civl/ghost.bpl @@ -0,0 +1,45 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var {:layer 0} x: int; + +procedure {:yields} {:layer 0,1} Incr(); +ensures {:right} |{ A: x := x + 1; return true; }|; + +procedure {:pure} ghost(y: int) returns (z: int) +requires y == 1; +ensures z == 2; +{ + z := y + 1; +} + +procedure {:yields} {:layer 1,2} Incr2() +ensures {:right} |{ A: x := x + 2; return true; }|; +{ + var {:layer 1} a: int; + + yield; + call a := ghost(1); + assert {:layer 1} a == 2; + par Incr() | Incr(); + yield; +} + +procedure {:layer 1} ghost_0() returns (z: int) +ensures z == x; +{ + z := x; +} + +procedure {:yields} {:layer 1,2} Incr2_0() +ensures {:right} |{ A: x := x + 2; return true; }|; +{ + var {:layer 1} a: int; + var {:layer 1} b: int; + + yield; + call a := ghost_0(); + par Incr() | Incr(); + call b := ghost_0(); + assert {:layer 1} b == a + 2; + yield; +} diff --git a/Test/civl/ghost.bpl.expect b/Test/civl/ghost.bpl.expect new file mode 100644 index 00000000..76a9a2bf --- /dev/null +++ b/Test/civl/ghost.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 8 verified, 0 errors diff --git a/Test/civl/linear-set.bpl b/Test/civl/linear-set.bpl new file mode 100644 index 00000000..de7f72f4 --- /dev/null +++ b/Test/civl/linear-set.bpl @@ -0,0 +1,105 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +type X; +function {:builtin "MapConst"} MapConstInt(int) : [X]int; +function {:builtin "MapConst"} MapConstBool(bool) : [X]bool; +function {:builtin "MapOr"} MapOr([X]bool, [X]bool) : [X]bool; + +function {:inline} None() : [X]bool +{ + MapConstBool(false) +} + +function {:inline} All() : [X]bool +{ + MapConstBool(true) +} + +function {:inline} {:linear "x"} XCollector(xs: [X]bool) : [X]bool +{ + xs +} + +var {:layer 0,1} x: int; +var {:layer 0,1} l: [X]bool; + + +procedure {:yields} {:layer 1} Split({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool) +ensures {:layer 1} xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None(); +{ + yield; + call xls1, xls2 := SplitLow(xls); + yield; +} + +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: [X]bool) +{ + yield; + call xls := AllocateLow(); + yield; +} + +procedure {:yields} {:layer 0,1} Set(v: int); +ensures {:atomic} |{A: x := v; return true; }|; + +procedure {:yields} {:layer 0,1} Lock(tidls: [X]bool); +ensures {:atomic} |{A: assume l == None(); l := tidls; return true; }|; + +procedure {:yields} {:layer 0,1} Unlock(); +ensures {:atomic} |{A: l := None(); return true; }|; + +procedure {:yields} {:layer 0,1} SplitLow({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool); +ensures {:atomic} |{ A: assume xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None(); return true; }|; + +procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xls: [X]bool); +ensures {:atomic} |{ A: return true; }|; + +procedure {:yields} {:layer 1} main({:linear_in "tid"} tidls': [X]bool, {:linear_in "x"} xls': [X]bool) +requires {:layer 1} tidls' != None() && xls' == All(); +{ + var {:linear "tid"} tidls: [X]bool; + var {:linear "x"} xls: [X]bool; + var {:linear "tid"} lsChild: [X]bool; + var {:linear "x"} xls1: [X]bool; + var {:linear "x"} xls2: [X]bool; + + tidls := tidls'; + xls := xls'; + yield; + call Set(42); + yield; + assert {:layer 1} xls == All(); + assert {:layer 1} x == 42; + call xls1, xls2 := Split(xls); + call lsChild := Allocate(); + assume (lsChild != None()); + yield; + async call thread(lsChild, xls1); + call lsChild := Allocate(); + assume (lsChild != None()); + yield; + async call thread(lsChild, xls2); + yield; +} + +procedure {:yields} {:layer 1} thread({:linear_in "tid"} tidls': [X]bool, {:linear_in "x"} xls': [X]bool) +requires {:layer 1} tidls' != None() && xls' != None(); +{ + var {:linear "x"} xls: [X]bool; + var {:linear "tid"} tidls: [X]bool; + + tidls := tidls'; + xls := xls'; + + yield; + call Lock(tidls); + yield; + assert {:layer 1} tidls != None() && xls != None(); + call Set(0); + yield; + assert {:layer 1} tidls != None() && xls != None(); + assert {:layer 1} x == 0; + assert {:layer 1} tidls != None() && xls != None(); + call Unlock(); + yield; +} diff --git a/Test/civl/linear-set.bpl.expect b/Test/civl/linear-set.bpl.expect new file mode 100644 index 00000000..76a9a2bf --- /dev/null +++ b/Test/civl/linear-set.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 8 verified, 0 errors diff --git a/Test/civl/linear-set2.bpl b/Test/civl/linear-set2.bpl new file mode 100644 index 00000000..4a0c6a1f --- /dev/null +++ b/Test/civl/linear-set2.bpl @@ -0,0 +1,106 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +type X; +function {:builtin "MapConst"} MapConstInt(int) : [X]int; +function {:builtin "MapConst"} MapConstBool(bool) : [X]bool; +function {:builtin "MapOr"} MapOr([X]bool, [X]bool) : [X]bool; + +function {:inline} None() : [X]bool +{ + MapConstBool(false) +} + +function {:inline} All() : [X]bool +{ + MapConstBool(true) +} + +function {:inline} {:linear "x"} XCollector(xs: [X]bool) : [X]bool +{ + xs +} + +var {:layer 0,1} x: int; +var {:layer 0,1} l: X; +const nil: X; + +procedure {:yields} {:layer 1} Split({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool) +ensures {:layer 1} xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None(); +{ + yield; + call xls1, xls2 := SplitLow(xls); + yield; +} + +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: X) +ensures {:layer 1} xls != nil; +{ + yield; + call xls := AllocateLow(); + yield; +} + +procedure {:yields} {:layer 0,1} Set(v: int); +ensures {:atomic} |{A: x := v; return true; }|; + +procedure {:yields} {:layer 0,1} Lock(tidls: X); +ensures {:atomic} |{A: assume l == nil; l := tidls; return true; }|; + +procedure {:yields} {:layer 0,1} Unlock(); +ensures {:atomic} |{A: l := nil; return true; }|; + +procedure {:yields} {:layer 0,1} SplitLow({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool); +ensures {:atomic} |{ A: assume xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None(); return true; }|; + +procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xls: X); +ensures {:atomic} |{ A: assume xls != nil; return true; }|; + +procedure {:yields} {:layer 1} main({:linear_in "tid"} tidls': X, {:linear_in "x"} xls': [X]bool) +requires {:layer 1} tidls' != nil && xls' == All(); +{ + var {:linear "tid"} tidls: X; + var {:linear "x"} xls: [X]bool; + var {:linear "tid"} lsChild: X; + var {:linear "x"} xls1: [X]bool; + var {:linear "x"} xls2: [X]bool; + + tidls := tidls'; + xls := xls'; + + yield; + call Set(42); + yield; + assert {:layer 1} xls == All(); + assert {:layer 1} x == 42; + call xls1, xls2 := Split(xls); + call lsChild := Allocate(); + yield; + async call thread(lsChild, xls1); + call lsChild := Allocate(); + yield; + async call thread(lsChild, xls2); + yield; +} + +procedure {:yields} {:layer 1} thread({:linear_in "tid"} tidls': X, {:linear_in "x"} xls': [X]bool) +requires {:layer 1} tidls' != nil && xls' != None(); +{ + var {:linear "x"} xls: [X]bool; + var {:linear "tid"} tidls: X; + + tidls := tidls'; + xls := xls'; + + yield; + call Lock(tidls); + yield; + assert {:layer 1} tidls != nil && xls != None(); + call Set(0); + yield; + assert {:layer 1} tidls != nil && xls != None(); + assert {:layer 1} x == 0; + yield; + assert {:layer 1} tidls != nil && xls != None(); + call Unlock(); + yield; +} diff --git a/Test/civl/linear-set2.bpl.expect b/Test/civl/linear-set2.bpl.expect new file mode 100644 index 00000000..76a9a2bf --- /dev/null +++ b/Test/civl/linear-set2.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 8 verified, 0 errors diff --git a/Test/civl/lock-introduced.bpl b/Test/civl/lock-introduced.bpl new file mode 100644 index 00000000..5403e5d4 --- /dev/null +++ b/Test/civl/lock-introduced.bpl @@ -0,0 +1,110 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +function {:builtin "MapConst"} MapConstBool(bool) : [X]bool; +function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool +{ + MapConstBool(false)[x := true] +} + +type X; +const nil: X; +var {:layer 0,2} b: bool; +var {:layer 1,3} lock: X; + +procedure {:yields} {:layer 3} Customer({:linear "tid"} tid: X) +requires {:layer 2} tid != nil; +requires {:layer 2} InvLock(lock, b); +ensures {:layer 2} InvLock(lock, b); +{ + yield; + assert {:layer 2} InvLock(lock, b); + while (*) + invariant {:layer 2} InvLock(lock, b); + { + call Enter(tid); + call Leave(tid); + yield; + assert {:layer 2} InvLock(lock, b); + } + yield; + assert {:layer 2} InvLock(lock, b); +} + +function {:inline} InvLock(lock: X, b: bool) : bool +{ + lock != nil <==> b +} + +procedure {:yields} {:layer 2,3} Enter({:linear "tid"} tid: X) +requires {:layer 2} tid != nil; +requires {:layer 2} InvLock(lock, b); +ensures {:layer 2} InvLock(lock, b); +ensures {:right} |{ A: assume lock == nil && tid != nil; lock := tid; return true; }|; +{ + yield; + assert {:layer 2} InvLock(lock, b); + call LowerEnter(tid); + yield; + assert {:layer 2} InvLock(lock, b); +} + +procedure {:yields} {:layer 2,3} Leave({:linear "tid"} tid:X) +requires {:layer 2} InvLock(lock, b); +ensures {:layer 2} InvLock(lock, b); +ensures {:atomic} |{ A: assert lock == tid && tid != nil; lock := nil; return true; }|; +{ + yield; + assert {:layer 2} InvLock(lock, b); + call LowerLeave(); + yield; + assert {:layer 2} InvLock(lock, b); +} + +procedure {:yields} {:layer 1,2} LowerEnter({:linear "tid"} tid: X) +ensures {:atomic} |{ A: assume !b; b := true; lock := tid; return true; }|; +{ + var status: bool; + yield; + L: + call status := CAS(false, true); + if (status) { + call SetLock(tid); + } + yield; + goto A, B; + + A: + assume status; + yield; + return; + + B: + assume !status; + goto L; +} + +procedure {:yields} {:layer 1,2} LowerLeave() +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; +B: assume b == prev; b := next; status := true; return true; +C: status := false; return true; +}|; + +procedure {:yields} {:layer 0,1} SET(next: bool); +ensures {:atomic} |{ A: b := next; return true; }|; + diff --git a/Test/civl/lock-introduced.bpl.expect b/Test/civl/lock-introduced.bpl.expect new file mode 100644 index 00000000..8c74fe2e --- /dev/null +++ b/Test/civl/lock-introduced.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 17 verified, 0 errors diff --git a/Test/civl/lock.bpl b/Test/civl/lock.bpl new file mode 100644 index 00000000..ee736029 --- /dev/null +++ b/Test/civl/lock.bpl @@ -0,0 +1,57 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var {:layer 0,2} b: bool; + +procedure {:yields} {:layer 2} main() +{ + yield; + while (*) + { + async call Customer(); + yield; + } + yield; +} + +procedure {:yields} {:layer 2} Customer() +{ + yield; + while (*) + { + call Enter(); + yield; + call Leave(); + yield; + } + yield; +} + +procedure {:yields} {:layer 1,2} Enter() +ensures {:atomic} |{ A: assume !b; b := true; return true; }|; +{ + var status: bool; + yield; + L: + call status := CAS(false, true); + yield; + goto A, B; + + A: + assume status; + yield; + return; + + B: + assume !status; + goto L; +} + +procedure {:yields} {:layer 0,2} CAS(prev: bool, next: bool) returns (status: bool); +ensures {:atomic} |{ +A: goto B, C; +B: assume b == prev; b := next; status := true; return true; +C: status := false; return true; +}|; + +procedure {:yields} {:layer 0,2} Leave(); +ensures {:atomic} |{ A: b := false; return true; }|; diff --git a/Test/civl/lock.bpl.expect b/Test/civl/lock.bpl.expect new file mode 100644 index 00000000..76a9a2bf --- /dev/null +++ b/Test/civl/lock.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 8 verified, 0 errors diff --git a/Test/civl/lock2.bpl b/Test/civl/lock2.bpl new file mode 100644 index 00000000..e84d0a6f --- /dev/null +++ b/Test/civl/lock2.bpl @@ -0,0 +1,63 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var {:layer 0,2} b: int; + +procedure {:yields} {:layer 2} main() +{ + yield; + while (*) + { + async call Customer(); + yield; + } + yield; +} + +procedure {:yields} {:layer 2} Customer() +{ + yield; + while (*) + { + call Enter(); + yield; + call Leave(); + yield; + } + yield; +} + +procedure {:yields} {:layer 1,2} Enter() +ensures {:atomic} |{ A: assume b == 0; b := 1; return true; }|; +{ + var _old, curr: int; + yield; + while (true) { + call _old := CAS(0, 1); + yield; + if (_old == 0) { + break; + } + while (true) { + call curr := Read(); + yield; + if (curr == 0) { + break; + } + } + yield; + } + yield; +} + +procedure {:yields} {:layer 0,2} Read() returns (val: int); +ensures {:atomic} |{ A: val := b; return true; }|; + +procedure {:yields} {:layer 0,2} CAS(prev: int, next: int) returns (_old: int); +ensures {:atomic} |{ +A: _old := b; goto B, C; +B: assume _old == prev; b := next; return true; +C: assume _old != prev; return true; +}|; + +procedure {:yields} {:layer 0,2} Leave(); +ensures {:atomic} |{ A: b := 0; return true; }|; diff --git a/Test/civl/lock2.bpl.expect b/Test/civl/lock2.bpl.expect new file mode 100644 index 00000000..76a9a2bf --- /dev/null +++ b/Test/civl/lock2.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 8 verified, 0 errors diff --git a/Test/civl/multiset.bpl b/Test/civl/multiset.bpl new file mode 100644 index 00000000..ec391380 --- /dev/null +++ b/Test/civl/multiset.bpl @@ -0,0 +1,324 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +type X; + +const unique null : int; +const unique nil: X; +const unique done: X; + +var {:layer 0} elt : [int]int; +var {:layer 0} valid : [int]bool; +var {:layer 0} lock : [int]X; +var {:layer 0} owner : [int]X; +const max : int; + +function {:builtin "MapConst"} MapConstBool(bool) : [X]bool; +function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool +{ + MapConstBool(false)[x := true] +} + +axiom (max > 0); + +procedure {:yields} {:layer 0} acquire(i : int, {:linear "tid"} tid: X); +ensures {:right} |{ A: + assert 0 <= i && i < max; + assert tid != nil && tid != done; + assume lock[i] == nil; + lock[i] := tid; + return true; + }|; + + +procedure {:yields} {:layer 0} release(i : int, {:linear "tid"} tid: X); +ensures {:left} |{ A: + assert 0 <= i && i < max; + assert lock[i] == tid; + assert tid != nil && tid != done; + lock[i] := nil; + return true; + }|; + + +procedure {:yields} {:layer 0,1} getElt(j : int, {:linear "tid"} tid: X) returns (elt_j:int); +ensures {:both} |{ A: + assert 0 <= j && j < max; + assert lock[j] == tid; + assert tid != nil && tid != done; + elt_j := elt[j]; + return true; + }|; + + +procedure {:yields} {:layer 0,1} setElt(j : int, x : int, {:linear "tid"} tid: X); +ensures {:both} |{ A: + assert x != null; + assert owner[j] == nil; + assert 0 <= j && j < max; + assert lock[j] == tid; + assert tid != nil && tid != done; + elt[j] := x; + owner[j] := tid; + return true; + }|; + + +procedure {:yields} {:layer 0,2} setEltToNull(j : int, {:linear "tid"} tid: X); +ensures {:left} |{ A: + assert owner[j] == tid; + assert 0 <= j && j < max; + assert lock[j] == tid; + assert !valid[j]; + assert tid != nil && tid != done; + elt[j] := null; + owner[j] := nil; + return true; + }|; + +procedure {:yields} {:layer 0,2} setValid(j : int, {:linear "tid"} tid: X); +ensures {:both} |{ A: + assert 0 <= j && j < max; + assert lock[j] == tid; + assert tid != nil && tid != done; + assert owner[j] == tid; + valid[j] := true; + owner[j] := done; + return true; + }|; + +procedure {:yields} {:layer 0,2} isEltThereAndValid(j : int, x : int, {:linear "tid"} tid: X) returns (fnd:bool); +ensures {:both} |{ A: + assert 0 <= j && j < max; + assert lock[j] == tid; + assert tid != nil && tid != done; + fnd := (elt[j] == x) && valid[j]; + return true; + }|; + +procedure {:yields} {:layer 1,2} FindSlot(x : int, {:linear "tid"} tid: X) returns (r : int) +requires {:layer 1} Inv(valid, elt, owner) && x != null && tid != nil && tid != done; +ensures {:layer 1} Inv(valid, elt, owner); +ensures {:right} |{ A: assert tid != nil && tid != done; + assert x != null; + goto B, C; + B: assume (0 <= r && r < max); + assume elt[r] == null; + assume owner[r] == nil; + assume !valid[r]; + elt[r] := x; + owner[r] := tid; + return true; + C: assume (r == -1); return true; + }|; +{ + var j : int; + var elt_j : int; + + par Yield1(); + + j := 0; + while(j < max) + invariant {:layer 1} Inv(valid, elt, owner); + invariant {:layer 1} 0 <= j; + { + call acquire(j, tid); + call elt_j := getElt(j, tid); + if(elt_j == null) + { + call setElt(j, x, tid); + call release(j, tid); + r := j; + + par Yield1(); + return; + } + call release(j,tid); + + par Yield1(); + + j := j + 1; + } + r := -1; + + par Yield1(); + return; +} + +procedure {:yields} {:layer 2} Insert(x : int, {:linear "tid"} tid: X) returns (result : bool) +requires {:layer 1} Inv(valid, elt, owner) && x != null && tid != nil && tid != done; +ensures {:layer 1} Inv(valid, elt, owner); +requires {:layer 2} Inv(valid, elt, owner) && x != null && tid != nil && tid != done; +ensures {:layer 2} Inv(valid, elt, owner); +ensures {:atomic} |{ var r:int; + A: goto B, C; + B: assume (0 <= r && r < max); + assume valid[r] == false; + assume elt[r] == null; + assume owner[r] == nil; + elt[r] := x; valid[r] := true; owner[r] := done; + result := true; return true; + C: result := false; return true; + }|; + { + var i: int; + par Yield12(); + call i := FindSlot(x, tid); + + if(i == -1) + { + result := false; + par Yield12(); + return; + } + par Yield1(); + assert {:layer 1} i != -1; + assert {:layer 2} i != -1; + call acquire(i, tid); + assert {:layer 2} elt[i] == x; + assert {:layer 2} valid[i] == false; + call setValid(i, tid); + call release(i, tid); + result := true; + par Yield12(); + return; +} + +procedure {:yields} {:layer 2} InsertPair(x : int, y : int, {:linear "tid"} tid: X) returns (result : bool) +requires {:layer 1} Inv(valid, elt, owner) && x != null && y != null && tid != nil && tid != done; +ensures {:layer 1} Inv(valid, elt, owner); +requires {:layer 2} Inv(valid, elt, owner) && x != null && y != null && tid != nil && tid != done; +ensures {:layer 2} Inv(valid, elt, owner); +ensures {:atomic} |{ var rx:int; + var ry:int; + A: goto B, C; + B: assume (0 <= rx && rx < max && 0 <= ry && ry < max && rx != ry); + assume valid[rx] == false; + assume valid[ry] == false; + assume elt[rx] == null; + assume elt[rx] == null; + elt[rx] := x; + elt[ry] := y; + valid[rx] := true; + valid[ry] := true; + owner[rx] := done; + owner[ry] := done; + result := true; return true; + C: result := false; return true; + }|; + { + var i : int; + var j : int; + par Yield12(); + + call i := FindSlot(x, tid); + + if (i == -1) + { + result := false; + par Yield12(); + return; + } + + par Yield1(); + call j := FindSlot(y, tid); + + if(j == -1) + { + par Yield1(); + call acquire(i,tid); + call setEltToNull(i, tid); + call release(i,tid); + result := false; + par Yield12(); + return; + } + + par Yield1(); + assert {:layer 2} i != -1 && j != -1; + call acquire(i, tid); + call acquire(j, tid); + assert {:layer 2} elt[i] == x; + assert {:layer 2} elt[j] == y; + assert {:layer 2} valid[i] == false; + assert {:layer 2} valid[j] == false; + call setValid(i, tid); + call setValid(j, tid); + call release(j, tid); + call release(i, tid); + result := true; + par Yield12(); + return; +} + +procedure {:yields} {:layer 2} LookUp(x : int, {:linear "tid"} tid: X, old_valid:[int]bool, old_elt:[int]int) returns (found : bool) +requires {:layer 1} {:layer 2} old_valid == valid && old_elt == elt; +requires {:layer 1} {:layer 2} Inv(valid, elt, owner); +requires {:layer 1} {:layer 2} (tid != nil && tid != done); +ensures {:layer 1} {:layer 2} Inv(valid, elt, owner); +ensures {:atomic} |{ A: assert tid != nil && tid != done; + assert x != null; + assume found ==> (exists ii:int :: 0 <= ii && ii < max && valid[ii] && elt[ii] == x); + assume !found ==> (forall ii:int :: 0 <= ii && ii < max ==> !(old_valid[ii] && old_elt[ii] == x)); + return true; + }|; +{ + var j : int; + var isThere : bool; + + par Yield12() | YieldLookUp(old_valid, old_elt); + + j := 0; + + while(j < max) + invariant {:layer 1} {:layer 2} Inv(valid, elt, owner); + invariant {:layer 1} {:layer 2} (forall ii:int :: 0 <= ii && ii < j ==> !(old_valid[ii] && old_elt[ii] == x)); + invariant {:layer 1} {:layer 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]); + invariant {:layer 1} {:layer 2} 0 <= j; + { + call acquire(j, tid); + call isThere := isEltThereAndValid(j, x, tid); + if(isThere) + { + call release(j, tid); + found := true; + par Yield12() | YieldLookUp(old_valid, old_elt); + return; + } + call release(j,tid); + par Yield12() | YieldLookUp(old_valid, old_elt); + j := j + 1; + } + found := false; + + par Yield12() | YieldLookUp(old_valid, old_elt); + return; +} + +procedure {:yields} {:layer 1} Yield1() +requires {:layer 1} Inv(valid, elt, owner); +ensures {:layer 1} Inv(valid, elt, owner); +{ + yield; + assert {:layer 1} Inv(valid, elt, owner); +} + +procedure {:yields} {:layer 2} Yield12() +requires {:layer 1} {:layer 2} Inv(valid, elt, owner); +ensures {:layer 1} {:layer 2} Inv(valid, elt, owner); +{ + yield; + assert {:layer 1} {:layer 2} Inv(valid, elt, owner); +} + +function {:inline} Inv(valid: [int]bool, elt: [int]int, owner: [int]X): (bool) +{ + (forall i:int :: 0 <= i && i < max ==> (elt[i] == null <==> (!valid[i] && owner[i] == nil))) +} + +procedure {:yields} {:layer 2} YieldLookUp(old_valid: [int]bool, old_elt: [int]int) +requires {:layer 1} {:layer 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]); +ensures {:layer 1} {:layer 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]); +{ + yield; + assert {:layer 1} {:layer 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]); +} diff --git a/Test/civl/multiset.bpl.expect b/Test/civl/multiset.bpl.expect new file mode 100644 index 00000000..63682bb4 --- /dev/null +++ b/Test/civl/multiset.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 85 verified, 0 errors diff --git a/Test/civl/new1.bpl b/Test/civl/new1.bpl new file mode 100644 index 00000000..c2feb179 --- /dev/null +++ b/Test/civl/new1.bpl @@ -0,0 +1,42 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +function {:builtin "MapConst"} mapconstbool(x:bool): [int]bool; + +var {:layer 0,1} g:int; + +function {:inline} {:linear "Perm"} SetCollectorPerm(x: [int]bool) : [int]bool +{ + x +} + +procedure {:yields} {:layer 1} PB({:linear_in "Perm"} permVar_in:[int]bool) +requires {:layer 1} permVar_in[0] && g == 0; +{ + var {:linear "Perm"} permVar_out: [int]bool; + permVar_out := permVar_in; + + yield; + assert {:layer 1} permVar_out[0]; + assert {:layer 1} g == 0; + + call IncrG(); + + yield; + assert {:layer 1} permVar_out[0]; + assert {:layer 1} g == 1; +} + +procedure {:yields} {:layer 1} Main({:linear_in "Perm"} Permissions: [int]bool) +requires {:layer 1} Permissions == mapconstbool(true); +{ + yield; + call SetG(0); + async call PB(Permissions); + yield; +} + +procedure {:yields} {:layer 0,1} SetG(val:int); +ensures {:atomic} |{A: g := val; return true; }|; + +procedure {:yields} {:layer 0,1} IncrG(); +ensures {:atomic} |{A: g := g + 1; return true; }|; diff --git a/Test/civl/new1.bpl.expect b/Test/civl/new1.bpl.expect new file mode 100644 index 00000000..00ddb38b --- /dev/null +++ b/Test/civl/new1.bpl.expect @@ -0,0 +1,2 @@ + +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 b/Test/civl/one.bpl new file mode 100644 index 00000000..3b370fa7 --- /dev/null +++ b/Test/civl/one.bpl @@ -0,0 +1,18 @@ +// RUN: %boogie -noinfer "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var {:layer 0,1} x:int; + +procedure {:yields} {:layer 0,1} Set(v: int); +ensures {:atomic} +|{A: + x := v; return true; +}|; + +procedure {:yields} {:layer 1} B() +{ + yield; + call Set(5); + yield; + assert {:layer 1} x == 5; +} + diff --git a/Test/civl/one.bpl.expect b/Test/civl/one.bpl.expect new file mode 100644 index 00000000..41374b00 --- /dev/null +++ b/Test/civl/one.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 2 verified, 0 errors diff --git a/Test/civl/par-incr.bpl b/Test/civl/par-incr.bpl new file mode 100644 index 00000000..7be8f561 --- /dev/null +++ b/Test/civl/par-incr.bpl @@ -0,0 +1,31 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +var {:layer 0} x: int; + +procedure {:yields} {:layer 0,1} Incr(); +ensures {:right} |{ A: x := x + 1; return true; }|; + +procedure {:yields} {:layer 1,2} Incr2() +ensures {:right} |{ A: x := x + 2; return true; }|; +{ + yield; + par Incr() | Incr(); + yield; +} + +procedure {:yields} {:layer 1} Yield() +{ + yield; +} + +procedure {:yields} {:layer 2,3} Incr4() +ensures {:atomic} |{ A: x := x + 4; return true; }|; +{ + yield; + par Incr2() | Incr2() | Yield(); + yield; +} + + + diff --git a/Test/civl/par-incr.bpl.expect b/Test/civl/par-incr.bpl.expect new file mode 100644 index 00000000..3e3dc54b --- /dev/null +++ b/Test/civl/par-incr.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 7 verified, 0 errors diff --git a/Test/civl/parallel1.bpl b/Test/civl/parallel1.bpl new file mode 100644 index 00000000..ec24342e --- /dev/null +++ b/Test/civl/parallel1.bpl @@ -0,0 +1,48 @@ +// RUN: %boogie -noinfer "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var {:layer 0,1} g:int; + +procedure {:yields} {:layer 1} PB() +{ + yield; + call Incr(); + yield; +} + +procedure {:yields} {:layer 0,1} Incr(); +ensures {:atomic} +|{A: + g := g + 1; return true; +}|; + +procedure {:yields} {:layer 0,1} Set(v: int); +ensures {:atomic} +|{A: + g := v; return true; +}|; + +procedure {:yields} {:layer 1} PC() +ensures {:layer 1} g == 3; +{ + yield; + call Set(3); + yield; + assert {:layer 1} g == 3; +} + +procedure {:yields} {:layer 1} PD() +{ + call PC(); + assert {:layer 1} g == 3; + yield; +} + +procedure {:yields} {:layer 1} Main() +{ + yield; + while (*) + { + par PB() | PC() | PD(); + } + yield; +} diff --git a/Test/civl/parallel1.bpl.expect b/Test/civl/parallel1.bpl.expect new file mode 100644 index 00000000..fa974099 --- /dev/null +++ b/Test/civl/parallel1.bpl.expect @@ -0,0 +1,8 @@ +parallel1.bpl(30,3): Error: Non-interference check failed +Execution trace: + parallel1.bpl(7,3): anon0 + (0,0): anon00 + parallel1.bpl(14,3): inline$Incr_1$0$A + (0,0): inline$Impl_YieldChecker_PC_1$0$L0 + +Boogie program verifier finished with 7 verified, 1 error diff --git a/Test/civl/parallel2.bpl b/Test/civl/parallel2.bpl new file mode 100644 index 00000000..540e9810 --- /dev/null +++ b/Test/civl/parallel2.bpl @@ -0,0 +1,59 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var {:layer 0,1} a:[int]int; + +function {:builtin "MapConst"} MapConstBool(bool) : [int]bool; +function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool +{ + MapConstBool(false)[x := true] +} + +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: int) +{ + yield; + call tid := AllocateLow(); + yield; +} + +procedure {:yields} {:layer 0,1} Write(idx: int, val: int); +ensures {:atomic} |{A: a[idx] := val; return true; }|; + +procedure {:yields} {:layer 1} main() +{ + var {:linear "tid"} i: int; + var {:linear "tid"} j: int; + call i := Allocate(); + call j := Allocate(); + par i := t(i) | j := t(j); + par i := u(i) | j := u(j); +} + +procedure {:yields} {:layer 1} t({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int) +{ + i := i'; + + yield; + call Write(i, 42); + call Yield(i); + assert {:layer 1} a[i] == 42; +} + +procedure {:yields} {:layer 1} u({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int) +{ + i := i'; + + yield; + call Write(i, 42); + yield; + assert {:layer 1} a[i] == 42; +} + +procedure {:yields} {:layer 1} Yield({:linear "tid"} i: int) +ensures {:layer 1} old(a)[i] == a[i]; +{ + yield; + assert {:layer 1} old(a)[i] == a[i]; +} + +procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: int); +ensures {:atomic} |{ A: return true; }|; diff --git a/Test/civl/parallel2.bpl.expect b/Test/civl/parallel2.bpl.expect new file mode 100644 index 00000000..12041afe --- /dev/null +++ b/Test/civl/parallel2.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 10 verified, 0 errors diff --git a/Test/civl/parallel4.bpl b/Test/civl/parallel4.bpl new file mode 100644 index 00000000..33a21446 --- /dev/null +++ b/Test/civl/parallel4.bpl @@ -0,0 +1,45 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var {:layer 0,1} a:int; + +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: int) +{ + yield; + call tid := AllocateLow(); + yield; +} + +function {:builtin "MapConst"} MapConstBool(bool) : [int]bool; +function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool +{ + MapConstBool(false)[x := true] +} + +procedure {:yields} {:layer 1} main() +{ + var {:linear "tid"} i: int; + var {:linear "tid"} j: int; + call i := Allocate(); + call j := Allocate(); + par i := t(i) | j := t(j); +} + +procedure {:yields} {:layer 1} t({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int) +{ + i := i'; + call Yield(); + assert {:layer 1} a == old(a); + call Incr(); + yield; +} + +procedure {:yields} {:layer 0,1} Incr(); +ensures {:atomic} |{A: a := a + 1; return true; }|; + +procedure {:yields} {:layer 1} Yield() +{ + yield; +} + +procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: int); +ensures {:atomic} |{ A: return true; }|; diff --git a/Test/civl/parallel4.bpl.expect b/Test/civl/parallel4.bpl.expect new file mode 100644 index 00000000..baf228c8 --- /dev/null +++ b/Test/civl/parallel4.bpl.expect @@ -0,0 +1,6 @@ +parallel4.bpl(31,3): Error BP5001: This assertion might not hold. +Execution trace: + parallel4.bpl(29,5): anon0 + (0,0): anon01 + +Boogie program verifier finished with 7 verified, 1 error diff --git a/Test/civl/parallel5.bpl b/Test/civl/parallel5.bpl new file mode 100644 index 00000000..6d3deb8e --- /dev/null +++ b/Test/civl/parallel5.bpl @@ -0,0 +1,59 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var {:layer 0,1} a:[int]int; + +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: int) +{ + yield; + call tid := AllocateLow(); + yield; +} + +function {:builtin "MapConst"} MapConstBool(bool) : [int]bool; +function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool +{ + MapConstBool(false)[x := true] +} + +procedure {:yields} {:layer 0,1} Write(idx: int, val: int); +ensures {:atomic} |{A: a[idx] := val; return true; }|; + +procedure {:yields} {:layer 1} main() +{ + var {:linear "tid"} i: int; + var {:linear "tid"} j: int; + call i := Allocate(); + call j := Allocate(); + par i := t(i) | Yield(j); + par i := u(i) | j := u(j); +} + +procedure {:yields} {:layer 1} t({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int) +{ + i := i'; + + yield; + call Write(i, 42); + call Yield(i); + assert {:layer 1} a[i] == 42; +} + +procedure {:yields} {:layer 1} u({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int) +{ + i := i'; + + yield; + call Write(i, 42); + yield; + assert {:layer 1} a[i] == 42; +} + +procedure {:yields} {:layer 1} Yield({:linear "tid"} i: int) +ensures {:layer 1} old(a)[i] == a[i]; +{ + yield; + assert {:layer 1} old(a)[i] == a[i]; +} + +procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: int); +ensures {:atomic} |{ A: return true; }|; diff --git a/Test/civl/parallel5.bpl.expect b/Test/civl/parallel5.bpl.expect new file mode 100644 index 00000000..12041afe --- /dev/null +++ b/Test/civl/parallel5.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 10 verified, 0 errors diff --git a/Test/civl/perm.bpl b/Test/civl/perm.bpl new file mode 100644 index 00000000..5d6e0d21 --- /dev/null +++ b/Test/civl/perm.bpl @@ -0,0 +1,49 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var {:layer 0,1} x: int; +function {:builtin "MapConst"} ch_mapconstbool(x: bool) : [int]bool; + +function {:builtin "MapOr"} ch_mapunion(x: [int]bool, y: [int]bool) : [int]bool; + +function {:inline} {:linear "Perm"} SetCollectorPerm(x: [int]bool) : [int]bool +{ + x +} + +procedure {:yields} {:layer 1} mainE({:linear_in "Perm"} permVar_in: [int]bool) + requires {:layer 1} permVar_in == ch_mapconstbool(true); + requires {:layer 1} x == 0; +{ + var {:linear "Perm"} permVar_out: [int]bool; + + permVar_out := permVar_in; + + yield; + assert {:layer 1} x == 0; + assert {:layer 1} permVar_out == ch_mapconstbool(true); + + async call foo(permVar_out); + yield; +} + +procedure {:yields} {:layer 1} foo({:linear_in "Perm"} permVar_in: [int]bool) + requires {:layer 1} permVar_in != ch_mapconstbool(false); + requires {:layer 1} permVar_in[1]; + requires {:layer 1} x == 0; +{ + var {:linear "Perm"} permVar_out: [int]bool; + permVar_out := permVar_in; + + yield; + assert {:layer 1} permVar_out[1]; + assert {:layer 1} x == 0; + + call Incr(); + + yield; + assert {:layer 1} permVar_out[1]; + assert {:layer 1} x == 1; +} + +procedure {:yields} {:layer 0,1} Incr(); +ensures {:atomic} |{A: x := x + 1; return true; }|;
\ No newline at end of file diff --git a/Test/civl/perm.bpl.expect b/Test/civl/perm.bpl.expect new file mode 100644 index 00000000..00ddb38b --- /dev/null +++ b/Test/civl/perm.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 4 verified, 0 errors diff --git a/Test/civl/t1.bpl b/Test/civl/t1.bpl new file mode 100644 index 00000000..ef468347 --- /dev/null +++ b/Test/civl/t1.bpl @@ -0,0 +1,103 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +function {:builtin "MapConst"} mapconstbool(bool) : [int]bool; + +function {:builtin "MapConst"} MapConstBool(bool) : [int]bool; +function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool +{ + MapConstBool(false)[x := true] +} + +function {:inline} {:linear "1"} SetCollector1(x: [int]bool) : [int]bool +{ + x +} + +function {:inline} {:linear "2"} SetCollector2(x: [int]bool) : [int]bool +{ + x +} + +var {:layer 0,1} g: int; +var {:layer 0,1} h: int; + +procedure {:yields} {:layer 0,1} SetG(val:int); +ensures {:atomic} |{A: g := val; return true; }|; + +procedure {:yields} {:layer 0,1} SetH(val:int); +ensures {:atomic} |{A: h := val; return true; }|; + +procedure {:yields} {:layer 1} Yield({:linear "1"} x: [int]bool) +requires {:layer 1} x == mapconstbool(true) && g == 0; +ensures {:layer 1} x == mapconstbool(true) && g == 0; +{ + yield; + assert {:layer 1} x == mapconstbool(true) && g == 0; +} + +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xl: int) +ensures {:layer 1} xl != 0; +{ + yield; + call xl := AllocateLow(); + yield; +} + +procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xls: int); +ensures {:atomic} |{ A: assume xls != 0; return true; }|; + +procedure {:yields} {:layer 1} A({:linear_in "tid"} tid_in: int, {:linear_in "1"} x: [int]bool, {:linear_in "2"} y: [int]bool) returns ({:linear "tid"} tid_out: int) +requires {:layer 1} x == mapconstbool(true); +requires {:layer 1} y == mapconstbool(true); +{ + var {:linear "tid"} tid_child: int; + tid_out := tid_in; + + yield; + call SetG(0); + + par tid_child := Allocate() | Yield(x); + + async call B(tid_child, x); + + yield; + assert {:layer 1} x == mapconstbool(true); + assert {:layer 1} g == 0; + + call SetH(0); + + yield; + assert {:layer 1} h == 0 && y == mapconstbool(true); + + yield; + call tid_child := Allocate(); + async call C(tid_child, y); + + yield; +} + +procedure {:yields} {:layer 1} B({:linear_in "tid"} tid_in: int, {:linear_in "1"} x_in: [int]bool) +requires {:layer 1} x_in != mapconstbool(false); +{ + var {:linear "tid"} tid_out: int; + var {:linear "1"} x: [int]bool; + tid_out := tid_in; + x := x_in; + + yield; + call SetG(1); + yield; +} + +procedure {:yields} {:layer 1} C({:linear_in "tid"} tid_in: int, {:linear_in "2"} y_in: [int]bool) +requires {:layer 1} y_in != mapconstbool(false); +{ + var {:linear "tid"} tid_out: int; + var {:linear "2"} y: [int]bool; + tid_out := tid_in; + y := y_in; + + yield; + call SetH(1); + yield; +} diff --git a/Test/civl/t1.bpl.expect b/Test/civl/t1.bpl.expect new file mode 100644 index 00000000..27a208d4 --- /dev/null +++ b/Test/civl/t1.bpl.expect @@ -0,0 +1,9 @@ +t1.bpl(65,5): Error: Non-interference check failed +Execution trace: + t1.bpl(84,13): anon0 + (0,0): anon05 + (0,0): inline$SetG_1$0$Entry + t1.bpl(25,21): inline$SetG_1$0$A + (0,0): inline$Impl_YieldChecker_A_1$0$L1 + +Boogie program verifier finished with 9 verified, 1 error diff --git a/Test/civl/termination.bpl b/Test/civl/termination.bpl new file mode 100644 index 00000000..7741fd19 --- /dev/null +++ b/Test/civl/termination.bpl @@ -0,0 +1,18 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure {:yields} {:layer 0} X(); +ensures {:atomic} |{ A: return true; }|; + +procedure {:yields} {:layer 0} Y(); +ensures {:left} |{ A: return true; }|; + +procedure {:yields} {:layer 1} main() { + yield; + call X(); + while (*) + { + call Y(); + } + yield; + assert {:layer 1} true; +} diff --git a/Test/civl/termination.bpl.expect b/Test/civl/termination.bpl.expect new file mode 100644 index 00000000..adfbec48 --- /dev/null +++ b/Test/civl/termination.bpl.expect @@ -0,0 +1,3 @@ +termination.bpl(9,31): Error: Implementation main fails simulation check C at layer 1. Transactions must be separated by a yield. + +1 type checking errors detected in termination.bpl diff --git a/Test/civl/termination2.bpl b/Test/civl/termination2.bpl new file mode 100644 index 00000000..1743c6a1 --- /dev/null +++ b/Test/civl/termination2.bpl @@ -0,0 +1,19 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure {:yields} {:layer 0} X(); +ensures {:atomic} |{ A: return true; }|; + +procedure {:yields} {:layer 0} Y(); +ensures {:left} |{ A: return true; }|; + +procedure {:yields} {:layer 1} main() { + yield; + call X(); + while (*) + invariant {:terminates} {:layer 1} true; + { + call Y(); + } + yield; + assert {:layer 1} true; +} diff --git a/Test/civl/termination2.bpl.expect b/Test/civl/termination2.bpl.expect new file mode 100644 index 00000000..41374b00 --- /dev/null +++ b/Test/civl/termination2.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 2 verified, 0 errors diff --git a/Test/civl/ticket.bpl b/Test/civl/ticket.bpl new file mode 100644 index 00000000..df19aae4 --- /dev/null +++ b/Test/civl/ticket.bpl @@ -0,0 +1,146 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +function RightOpen(n: int) : [int]bool; +function RightClosed(n: int) : [int]bool; +axiom (forall x: int, y: int :: RightOpen(x)[y] <==> y < x); +axiom (forall x: int, y: int :: RightClosed(x)[y] <==> y <= x); + +type X; +const nil: X; +var {:layer 0,2} t: int; +var {:layer 0,2} s: int; +var {:layer 0,2} cs: X; +var {:layer 0,2} T: [int]bool; + +function {:builtin "MapConst"} MapConstBool(bool) : [X]bool; +function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool +{ + MapConstBool(false)[x := true] +} +function {:inline} {:linear "tid"} TidSetCollector(x: [X]bool) : [X]bool +{ + x +} + +function {:inline} Inv1(tickets: [int]bool, ticket: int): (bool) +{ + tickets == RightOpen(ticket) +} + +function {:inline} Inv2(tickets: [int]bool, ticket: int, lock: X): (bool) +{ + if (lock == nil) then tickets == RightOpen(ticket) else tickets == RightClosed(ticket) +} + +procedure {:yields} {:layer 2} Allocate({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X) +ensures {:layer 1} {:layer 2} xl != nil; +{ + yield; + call xls, xl := AllocateLow(xls'); + yield; +} + +procedure {:yields} {:layer 2} main({:linear_in "tid"} xls':[X]bool) +requires {:layer 2} xls' == MapConstBool(true); +{ + var {:linear "tid"} tid: X; + var {:linear "tid"} xls: [X]bool; + + yield; + + call Init(xls'); + xls := xls'; + + par Yield1() | Yield2(); + + while (*) + invariant {:layer 1} Inv1(T, t); + invariant {:layer 2} Inv2(T, s, cs); + { + par xls, tid := Allocate(xls) | Yield1() | Yield2(); + async call Customer(tid); + par Yield1() | Yield2(); + } + par Yield1() | Yield2(); +} + +procedure {:yields} {:layer 2} Customer({:linear_in "tid"} tid: X) +requires {:layer 1} Inv1(T, t); +requires {:layer 2} tid != nil && Inv2(T, s, cs); +{ + par Yield1() | Yield2(); + while (*) + invariant {:layer 1} Inv1(T, t); + invariant {:layer 2} Inv2(T, s, cs); + { + call Enter(tid); + par Yield1() | Yield2() | YieldSpec(tid); + call Leave(tid); + par Yield1() | Yield2(); + } + par Yield1() | Yield2(); +} + +procedure {:yields} {:layer 2} Enter({:linear "tid"} tid: X) +requires {:layer 1} Inv1(T, t); +ensures {:layer 1} Inv1(T,t); +requires {:layer 2} tid != nil && Inv2(T, s, cs); +ensures {:layer 2} Inv2(T, s, cs) && cs == tid; +{ + var m: int; + + par Yield1() | Yield2(); + call m := GetTicketAbstract(tid); + par Yield1(); + call WaitAndEnter(tid, m); + par Yield1() | Yield2() | YieldSpec(tid); +} + +procedure {:yields} {:layer 1,2} GetTicketAbstract({:linear "tid"} tid: X) returns (m: int) +requires {:layer 1} Inv1(T, t); +ensures {:layer 1} Inv1(T, t); +ensures {:right} |{ A: havoc m, t; assume !T[m]; T[m] := true; return true; }|; +{ + par Yield1(); + call m := GetTicket(tid); + par Yield1(); +} + +procedure {:yields} {:layer 2} YieldSpec({:linear "tid"} tid: X) +requires {:layer 2} tid != nil && cs == tid; +ensures {:layer 2} cs == tid; +{ + yield; + assert {:layer 2} tid != nil && cs == tid; +} + +procedure {:yields} {:layer 2} Yield2() +requires {:layer 2} Inv2(T, s, cs); +ensures {:layer 2} Inv2(T, s, cs); +{ + yield; + assert {:layer 2} Inv2(T, s, cs); +} + +procedure {:yields} {:layer 1} Yield1() +requires {:layer 1} Inv1(T, t); +ensures {:layer 1} Inv1(T,t); +{ + yield; + assert {: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; }|; + +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; }|; + +procedure {:yields} {:layer 0,2} WaitAndEnter({:linear "tid"} tid: X, m:int); +ensures {:atomic} |{ A: assume m <= s; cs := tid; return true; }|; + +procedure {:yields} {:layer 0,2} Leave({:linear "tid"} tid: X); +ensures {:atomic} |{ A: s := s + 1; cs := nil; return true; }|; + +procedure {:yields} {:layer 0,2} AllocateLow({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X); +ensures {:atomic} |{ A: assume xl != nil; return true; }|; diff --git a/Test/civl/ticket.bpl.expect b/Test/civl/ticket.bpl.expect new file mode 100644 index 00000000..dc45a0ee --- /dev/null +++ b/Test/civl/ticket.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 24 verified, 0 errors diff --git a/Test/civl/treiber-stack.bpl b/Test/civl/treiber-stack.bpl new file mode 100644 index 00000000..a184886d --- /dev/null +++ b/Test/civl/treiber-stack.bpl @@ -0,0 +1,207 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +const null: int; +type lmap; +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: 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: 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:int); +ensures {:right} |{ A: assume v == null || dom(Stack)[v] || Used[v]; return true; }|; + +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: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: 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: int, newVal: int) returns (r: bool); +ensures {:atomic} |{ A: goto B,C; + 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: int; +var {:linear "Node"} {:layer 0} Stack: lmap; + + +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: [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: 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: int; + var g: bool; + var {:linear "Node"} t_lmap: lmap; + + yield; + assert {:layer 1} Inv(TopOfStack, Stack); + t_lmap := x_lmap; + while (true) + invariant {:layer 1} dom(t_lmap) == dom(x_lmap); + invariant {:layer 1} Inv(TopOfStack, Stack); + { + call t := ReadTopOfStack(); + call t_lmap := Store(t_lmap, x, t); + call g, t_lmap := TransferToStack(t, x, t_lmap); + if (g) { + break; + } + yield; + assert {:layer 1} dom(t_lmap) == dom(x_lmap); + assert {:layer 1} Inv(TopOfStack, Stack); + } + yield; + assert {:expand} {:layer 1} Inv(TopOfStack, Stack); +} + +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[t] := true; TopOfStack := map(Stack)[t]; Stack := Remove(Stack, t); return true; }|; +{ + var g: bool; + var x: int; + + yield; + assert {:layer 1} Inv(TopOfStack, Stack); + while (true) + invariant {:layer 1} Inv(TopOfStack, Stack); + { + call t := ReadTopOfStack(); + if (t != null) { + call x := Load(t); + call g := TransferFromStack(t, x); + if (g) { + break; + } + } + yield; + assert {:layer 1} Inv(TopOfStack, Stack); + } + yield; + assert {:layer 1} Inv(TopOfStack, Stack); +} + +function Equal([int]bool, [int]bool) returns (bool); +function Subset([int]bool, [int]bool) returns (bool); + +function Empty() returns ([int]bool); +function Singleton(int) returns ([int]bool); +function Union([int]bool, [int]bool) returns ([int]bool); + +axiom(forall x:int :: !Empty()[x]); + +axiom(forall x:int, y:int :: {Singleton(y)[x]} Singleton(y)[x] <==> x == y); +axiom(forall y:int :: {Singleton(y)} Singleton(y)[y]); + +axiom(forall x:int, S:[int]bool, T:[int]bool :: {Union(S,T)[x]}{Union(S,T),S[x]}{Union(S,T),T[x]} Union(S,T)[x] <==> S[x] || T[x]); + +axiom(forall S:[int]bool, T:[int]bool :: {Equal(S,T)} Equal(S,T) <==> Subset(S,T) && Subset(T,S)); +axiom(forall x:int, S:[int]bool, T:[int]bool :: {S[x],Subset(S,T)}{T[x],Subset(S,T)} S[x] && Subset(S,T) ==> T[x]); +axiom(forall S:[int]bool, T:[int]bool :: {Subset(S,T)} Subset(S,T) || (exists x:int :: S[x] && !T[x])); + +//////////////////// +// Between predicate +//////////////////// +function Between(f: [int]int, x: int, y: int, z: int) returns (bool); +function Avoiding(f: [int]int, x: int, y: int, z: int) returns (bool); + + +////////////////////////// +// Between set constructor +////////////////////////// +function BetweenSet(f: [int]int, x: int, z: int) returns ([int]bool); + +//////////////////////////////////////////////////// +// axioms relating Between and BetweenSet +//////////////////////////////////////////////////// +axiom(forall f: [int]int, x: int, y: int, z: int :: {BetweenSet(f, x, z)[y]} BetweenSet(f, x, z)[y] <==> Between(f, x, y, z)); +axiom(forall f: [int]int, x: int, y: int, z: int :: {Between(f, x, y, z), BetweenSet(f, x, z)} Between(f, x, y, z) ==> BetweenSet(f, x, z)[y]); +axiom(forall f: [int]int, x: int, z: int :: {BetweenSet(f, x, z)} Between(f, x, x, x)); +axiom(forall f: [int]int, x: int, z: int :: {BetweenSet(f, x, z)} Between(f, z, z, z)); + + +////////////////////////// +// Axioms for Between +////////////////////////// + +// reflexive +axiom(forall f: [int]int, x: int :: Between(f, x, x, x)); + +// step +axiom(forall f: [int]int, x: int, y: int, z: int, w:int :: {Between(f, y, z, w), f[x]} Between(f, x, f[x], f[x])); + +// reach +axiom(forall f: [int]int, x: int, y: int :: {f[x], Between(f, x, y, y)} Between(f, x, y, y) ==> x == y || Between(f, x, f[x], y)); + +// cycle +axiom(forall f: [int]int, x: int, y:int :: {f[x], Between(f, x, y, y)} f[x] == x && Between(f, x, y, y) ==> x == y); + +// sandwich +axiom(forall f: [int]int, x: int, y: int :: {Between(f, x, y, x)} Between(f, x, y, x) ==> x == y); + +// order1 +axiom(forall f: [int]int, x: int, y: int, z: int :: {Between(f, x, y, y), Between(f, x, z, z)} Between(f, x, y, y) && Between(f, x, z, z) ==> Between(f, x, y, z) || Between(f, x, z, y)); + +// order2 +axiom(forall f: [int]int, x: int, y: int, z: int :: {Between(f, x, y, z)} Between(f, x, y, z) ==> Between(f, x, y, y) && Between(f, y, z, z)); + +// transitive1 +axiom(forall f: [int]int, x: int, y: int, z: int :: {Between(f, x, y, y), Between(f, y, z, z)} Between(f, x, y, y) && Between(f, y, z, z) ==> Between(f, x, z, z)); + +// transitive2 +axiom(forall f: [int]int, x: int, y: int, z: int, w: int :: {Between(f, x, y, z), Between(f, y, w, z)} Between(f, x, y, z) && Between(f, y, w, z) ==> Between(f, x, y, w) && Between(f, x, w, z)); + +// transitive3 +axiom(forall f: [int]int, x: int, y: int, z: int, w: int :: {Between(f, x, y, z), Between(f, x, w, y)} Between(f, x, y, z) && Between(f, x, w, y) ==> Between(f, x, w, z) && Between(f, w, y, z)); + +// This axiom is required to deal with the incompleteness of the trigger for the reflexive axiom. +// It cannot be proved using the rest of the axioms. +axiom(forall f: [int]int, u:int, x: int :: {Between(f, u, x, x)} Between(f, u, x, x) ==> Between(f, u, u, x)); + +// relation between Avoiding and Between +axiom(forall f: [int]int, x: int, y: int, z: int :: {Avoiding(f, x, y, z)} Avoiding(f, x, y, z) <==> (Between(f, x, y, z) || (Between(f, x, y, y) && !Between(f, x, z, z)))); +axiom(forall f: [int]int, x: int, y: int, z: int :: {Between(f, x, y, z)} Between(f, x, y, z) <==> (Avoiding(f, x, y, z) && Avoiding(f, x, z, z))); + +// update +axiom(forall f: [int]int, u: int, v: int, x: int, p: int, q: int :: {Avoiding(f[p := q], u, v, x)} Avoiding(f[p := q], u, v, x) <==> ((Avoiding(f, u, v, p) && Avoiding(f, u, v, x)) || (Avoiding(f, u, p, x) && p != x && Avoiding(f, q, v, p) && Avoiding(f, q, v, x)))); + +axiom (forall f: [int]int, p: int, q: int, u: int, w: int :: {BetweenSet(f[p := q], u, w)} Avoiding(f, u, w, p) ==> Equal(BetweenSet(f[p := q], u, w), BetweenSet(f, u, w))); +axiom (forall f: [int]int, p: int, q: int, u: int, w: int :: {BetweenSet(f[p := q], u, w)} p != w && Avoiding(f, u, p, w) && Avoiding(f, q, w, p) ==> Equal(BetweenSet(f[p := q], u, w), Union(BetweenSet(f, u, p), BetweenSet(f, q, w)))); +axiom (forall f: [int]int, p: int, q: int, u: int, w: int :: {BetweenSet(f[p := q], u, w)} Avoiding(f, u, w, p) || (p != w && Avoiding(f, u, p, w) && Avoiding(f, q, w, p)) || Equal(BetweenSet(f[p := q], u, w), Empty()));
\ No newline at end of file diff --git a/Test/civl/treiber-stack.bpl.expect b/Test/civl/treiber-stack.bpl.expect new file mode 100644 index 00000000..76a9a2bf --- /dev/null +++ b/Test/civl/treiber-stack.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 8 verified, 0 errors diff --git a/Test/civl/wsq.bpl b/Test/civl/wsq.bpl new file mode 100644 index 00000000..0a2227b6 --- /dev/null +++ b/Test/civl/wsq.bpl @@ -0,0 +1,544 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +type Tid; +const nil: Tid; + +function {:builtin "MapConst"} MapConstBool(bool) : [Tid]bool; +function {:inline} {:linear "tid"} TidCollector(x: Tid) : [Tid]bool +{ + MapConstBool(false)[x := true] +} + + + +var {:layer 0,3} H: int; +var {:layer 0,3} T: int; +var {:layer 0,3} items: [int]int; +var {:layer 0} status: [int]bool; +var {:layer 0,3} take_in_cs: bool; +var {:layer 0,3} put_in_cs: bool; +var {:layer 0,3} steal_in_cs: [Tid]bool; +var {:layer 0,3} h_ss: [Tid]int; +var {:layer 0,3} t_ss: [Tid]int; + +const IN_Q: bool; +const NOT_IN_Q: bool; +axiom IN_Q == true; +axiom NOT_IN_Q == false; + +const unique EMPTY: int; +const unique NIL: Tid; +const unique ptTid: Tid; +axiom ptTid != NIL; + +function {:inline} stealerTid(tid: Tid):(bool) { tid != NIL && tid != ptTid } + +function {:inline} ideasInv(put_in_cs:bool, + items:[int]int, + status: [int]bool, + H:int, T:int, + take_in_cs:bool, + steal_in_cs:[Tid]bool, + h_ss:[Tid]int, + t_ss:[Tid]int + ):(bool) +{ + ( + ( (take_in_cs) && h_ss[ptTid] < t_ss[ptTid] ==> (t_ss[ptTid] == T && H <= T && + items[T] != EMPTY && status[T] == IN_Q) ) && + (put_in_cs ==> !take_in_cs) && (take_in_cs ==> !put_in_cs) && + (( (take_in_cs) && H != h_ss[ptTid]) ==> H > h_ss[ptTid]) && + (forall td:Tid :: (stealerTid(td) && steal_in_cs[td] && H == h_ss[td] && H < t_ss[td]) ==> (items[H] != EMPTY && status[H] == IN_Q)) && + (forall td:Tid :: (stealerTid(td) && steal_in_cs[td] && H != h_ss[td]) ==> H > h_ss[td]) + ) +} + +function {:inline} queueInv(steal_in_cs:[Tid]bool, + put_in_cs:bool, + take_in_cs:bool, + items:[int]int, status: [int]bool, _H:int, _T:int):(bool) +{ + ( (forall i:int :: (_H <= i && i <= _T) ==> (status[i] == IN_Q && items[i] != EMPTY)) ) +} + +function {:inline} emptyInv(put_in_cs:bool, take_in_cs:bool, items:[int]int, status:[int]bool, T:int):(bool) +{ + (forall i:int :: (i>=T && !put_in_cs && !take_in_cs) ==> status[i] == NOT_IN_Q && items[i] == EMPTY) +} + +function {:inline} putInv(items:[int]int, status: [int]bool, H:int, T:int):(bool) +{ + (forall i:int :: (H <= i && i < T) ==> (status[i] == IN_Q && items[i] != EMPTY)) +} + +function {:inline} takeInv(items:[int]int, status: [int]bool, H:int, T:int, t:int, h:int):(bool) +{ + (forall i:int :: (h <= i && i <= t) ==> (status[i] == IN_Q && + items[i] != EMPTY) && + t == T + ) +} + +procedure {:yields} {:layer 3} put({:linear "tid"} tid:Tid, task: int) +requires {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && task != EMPTY && !take_in_cs && !put_in_cs; +requires {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); +requires {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T); +ensures {: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; +ensures {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); +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 {:layer 3} oldH:int; + var {:layer 3} oldT:int; + var {:layer 3} oldStatusT:bool; + + 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); + assert {:layer 3} oldH <= H && oldT == T; + assert {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T); + + call t := readT_put(tid); + + 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); + assert {:layer 3} tid == ptTid && t == T; + assert {:layer 3} oldH <= H && oldT == T; + assert {:layer 3} (forall i:int :: i>=T ==> status[i] == NOT_IN_Q && items[i] == EMPTY); + + call writeItems_put(tid,t, task); + + 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); + assert {:layer 3} items[t] == task; + assert {:layer 3} oldH <= H && oldT == T; + assert {:layer 3} (forall i:int :: i>T ==> status[i] == NOT_IN_Q && items[i] == EMPTY); + + + call writeT_put(tid, t+1); + + 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); + assert {:layer 3} T == t + 1; + assert {:layer 3} oldH <= H && oldT == T; + assert {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T); +} + +procedure {:yields} {:layer 3} take({:linear "tid"} tid:Tid) returns (task: int, taskstatus: bool) +requires {: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; +requires {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); +ensures {: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 && (task != EMPTY ==> taskstatus == IN_Q); +ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); +ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; status[i] := NOT_IN_Q; return true; C: return true;}|; +{ + var h, t: int; + var chk: bool; + var {:layer 3} oldH:int; + var {:layer 3} oldT:int; + + 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); + assert {:layer 3} oldH <= H && oldT == T; + + LOOP_ENTRY_1: + + while(true) + invariant {: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; + invariant {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + { + + 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); + assert {:layer 3} oldH <= H && oldT == T; + + call t := readT_take_init(tid); + + 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); + assert {:layer 3} t == T; + assert {:layer 3} items[t-1] == EMPTY ==> H > t-1; + assert {:layer 3} oldH <= H && oldT == T; + + t := t-1; + call writeT_take(tid, 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); + assert {:layer 3} t == T; + assert {:layer 3} items[t] == EMPTY ==> H > t; + assert {:layer 3} oldH <= H && oldT == T; + + call h := readH_take(tid); + + 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); + assert {:layer 3} t == T; + assert {:layer 3} h <= H; + assert {:layer 3} items[t] == EMPTY ==> H > t; + assert {:layer 3} oldH <= H; + assert {:layer 3} oldT == T; + assert {:layer 3} h <= H; + assert {:layer 3} oldH == h; + + if(t<h) { + + call writeT_take_abort(tid, h); + task := EMPTY; + + 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; + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} h == T; + assert {:layer 3} oldH <= H && oldT == T; + return; + } + + call task, taskstatus := readItems(tid, 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; + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} t == T && task == items[T]; + assert {:layer 3} T > H ==> items[T] != EMPTY; + assert {:layer 3} oldH <= H && oldT == T && !put_in_cs && take_in_cs; + + if(t>h) { + call takeExitCS(tid); + + 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); + assert {:layer 3} t == T && task == items[t] && task != EMPTY && taskstatus == IN_Q; + assert {:layer 3} oldH <= H && oldT == T && !put_in_cs && !take_in_cs; + return; + } + call writeT_take_eq(tid, h+1); + 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); + assert {:layer 3} T == h + 1; + assert {:layer 3} oldH <= H; + assert {:layer 3} oldT == T; + assert {:layer 3} task == items[t]; + assert {:layer 3} !put_in_cs; + + call chk := CAS_H_take(tid, h,h+1); + + + 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; + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} h+1 == T; + assert {:layer 3} task == items[t]; + assert {:layer 3} !take_in_cs; + assert {:layer 3} !put_in_cs; + assert {:layer 3} oldH <= H && oldT == T; + + if(!chk) { + + 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); + assert {:layer 3} h+1 == T && task == items[t] && !take_in_cs && !put_in_cs; + assert {:layer 3} oldH <= H && oldT == T; + + goto LOOP_ENTRY_1; + } + + 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); + assert {:layer 3} h+1 == T && task == items[t] && !take_in_cs && !put_in_cs; + assert {:layer 3} oldH <= H && oldT == T && task != EMPTY && taskstatus == IN_Q; + + return; + } + + 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); + assert {:layer 3} oldH <= H && oldT == T; + +} + + +procedure {:yields}{:layer 3} steal({:linear "tid"} tid:Tid) returns (task: int, taskstatus: bool) +requires {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && stealerTid(tid) && + !steal_in_cs[tid]; +requires {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); +ensures {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && + !steal_in_cs[tid] && (task != EMPTY ==> taskstatus == IN_Q); +ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); +ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; status[i] := NOT_IN_Q; return true; C: return true;}|; +{ + var h, t: int; + var chk: bool; + var {:layer 3} oldH:int; + var {:layer 3} oldT:int; + + 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); + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} oldH <= H; + assert {:layer 3} !steal_in_cs[tid]; + + LOOP_ENTRY_2: + while(true) + invariant {:layer 3} stealerTid(tid); + invariant {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); + 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]; + { + 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); + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} oldH <= H; + assert {:layer 3} !steal_in_cs[tid]; + + call h := readH_steal(tid); + + call oldH, oldT := GhostRead(); + yield; + assert {:layer 3} H >= h; + assert {:layer 3} !steal_in_cs[tid]; + assert {:layer 3} h_ss[tid] == h; + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); + assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} oldH <= H; + + call t := readT_steal(tid); + + + 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; + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} oldH <= H && t == t_ss[tid]; + assert {:layer 3} (h < t && take_in_cs && (h_ss[ptTid] < t_ss[ptTid]) && h == H) ==> (H < T); + assert {:layer 3} H >= h; + + if( h>= t) { + + task := EMPTY; + call stealExitCS(tid); + + 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; + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} oldH <= H; + return; + } + + call task, taskstatus := readItems(tid, h); + + + 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); + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} oldH <= H; + assert {:layer 3} oldH == H && H == h && h_ss[tid] == h ==> task != EMPTY; + assert {:layer 3} (take_in_cs && (h_ss[ptTid] < t_ss[ptTid]) && h == H) ==> (H < T); + assert {:layer 3} h == H ==> status[H] == IN_Q; + + call chk := CAS_H_steal(tid, h,h+1); + + 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); + assert {:layer 3} (take_in_cs && (h_ss[ptTid] < t_ss[ptTid]) && chk) ==> ((oldH-1) < T); + assert {:layer 3} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + 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); + assert {:layer 3} oldH <= H; + + if(!chk) { + goto LOOP_ENTRY_2; + } + + 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); + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} oldH <= H && task != EMPTY; + return; + } + + 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; + take_in_cs := true; + h_ss[tid] := H; + return true;}|; + +procedure {:yields}{:layer 0,3} readH_steal({:linear "tid"} tid:Tid) returns (y: int); +ensures {:atomic} |{A: assert stealerTid(tid); + assert !steal_in_cs[tid]; + y := H; + h_ss[tid] := H; + return true;}|; + +procedure {:yields}{:layer 0,3} readT_take_init({:linear "tid"} tid:Tid) returns (y: int); +ensures {:atomic} |{A: assert tid != NIL; assert tid == ptTid; y := T; return true;}|; + +procedure {:yields}{:layer 0,3} readT_put({:linear "tid"} tid:Tid) returns (y: int); +ensures {:atomic} |{A: assert tid != NIL; + assert tid == ptTid; + put_in_cs := true; + y := T; + return true;}|; + +procedure {:yields}{:layer 0,3} readT_steal({:linear "tid"} tid:Tid) returns (y: int); +ensures {:atomic} |{A: assert tid != NIL; + assert stealerTid(tid); + assert !steal_in_cs[tid]; + y := T; + t_ss[tid] := T; + steal_in_cs[tid] := true; + return true;}|; + +procedure {:yields}{:layer 0,3} readItems({:linear "tid"} tid:Tid, ind: int) returns (y: int, b:bool); +ensures {:atomic} |{A: y := items[ind]; b := status[ind]; return true; }|; + +procedure {:yields}{:layer 0,3} writeT_put({:linear "tid"} tid:Tid, val: int); +ensures {:atomic} |{A: assert tid == ptTid; + T := T+1; + put_in_cs := false; + return true; }|; + +procedure {:yields}{:layer 0,3} writeT_take({:linear "tid"} tid:Tid, val: int); +ensures {:atomic} |{A: assert tid == ptTid; + T := val; + t_ss[tid] := val; + return true; }|; + +procedure {:yields}{:layer 0,3} writeT_take_abort({:linear "tid"} tid:Tid, val: int); +ensures {:atomic} |{A: assert tid == ptTid; + assert take_in_cs; + T := val; + take_in_cs := false; + return true; }|; + +procedure {:yields}{:layer 0,3} writeT_take_eq({:linear "tid"} tid:Tid, val: int); +ensures {:atomic} |{A: assert tid == ptTid; + T := val; + return true; }|; + +procedure {:yields}{:layer 0,3} takeExitCS({:linear "tid"} tid:Tid); +ensures {:atomic} |{A: assert tid == ptTid; + take_in_cs := false; + return true; }|; + +procedure {:yields}{:layer 0,3} stealExitCS({:linear "tid"} tid:Tid); +ensures {:atomic} |{A: assert stealerTid(tid); + assert steal_in_cs[tid]; + steal_in_cs[tid] := false; + return true; }|; + + +procedure {:yields}{:layer 0,3} writeItems({:linear "tid"} tid:Tid, idx: int, val: int); +ensures {:atomic} |{A: assert tid == ptTid; + assert val != EMPTY; + items[idx] := val; + status[idx] := IN_Q; + return true; }|; + + +procedure {:yields}{:layer 0,3} writeItems_put({:linear "tid"} tid:Tid, idx: int, val: int); +ensures {:atomic} |{A: assert tid == ptTid; + assert val != EMPTY; + items[idx] := val; + status[idx] := IN_Q; + return true; }|; + +procedure {:yields}{:layer 0,3} CAS_H_take({:linear "tid"} tid:Tid, prevVal :int, val: int) + returns (result: bool); +ensures {:atomic} |{ A: assert tid == ptTid; + goto B, C; + B: assume H == prevVal; + take_in_cs := false; + status[H] := NOT_IN_Q; + H := H+1; + result := true; + return true; + C: assume H != prevVal; result := false; + take_in_cs := false; + return true; +}|; + +procedure {:yields}{:layer 0,3} CAS_H_steal({:linear "tid"} tid:Tid, prevVal :int, val: int) + returns (result: bool); +ensures {:atomic} |{ A: assert stealerTid(tid); + goto B, C; + B: assume H == prevVal; + status[H] := NOT_IN_Q; + H := H+1; + result := true; + steal_in_cs[tid] := false; + return true; + C: assume H != prevVal; + result := false; + steal_in_cs[tid] := false; + return true; + }|;
\ No newline at end of file diff --git a/Test/civl/wsq.bpl.expect b/Test/civl/wsq.bpl.expect new file mode 100644 index 00000000..9823d44a --- /dev/null +++ b/Test/civl/wsq.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 6 verified, 0 errors |