diff options
Diffstat (limited to 'Test/og')
64 files changed, 0 insertions, 3234 deletions
diff --git a/Test/og/DeviceCache.bpl b/Test/og/DeviceCache.bpl deleted file mode 100644 index f439b607..00000000 --- a/Test/og/DeviceCache.bpl +++ /dev/null @@ -1,210 +0,0 @@ -// 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/og/DeviceCache.bpl.expect b/Test/og/DeviceCache.bpl.expect deleted file mode 100644 index 9ec7a92d..00000000 --- a/Test/og/DeviceCache.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ -
-Boogie program verifier finished with 30 verified, 0 errors
diff --git a/Test/og/FlanaganQadeer.bpl b/Test/og/FlanaganQadeer.bpl deleted file mode 100644 index 7345b5b2..00000000 --- a/Test/og/FlanaganQadeer.bpl +++ /dev/null @@ -1,75 +0,0 @@ -// 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/og/FlanaganQadeer.bpl.expect b/Test/og/FlanaganQadeer.bpl.expect deleted file mode 100644 index fef5ddc0..00000000 --- a/Test/og/FlanaganQadeer.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ -
-Boogie program verifier finished with 4 verified, 0 errors
diff --git a/Test/og/Program1.bpl b/Test/og/Program1.bpl deleted file mode 100644 index f405b92a..00000000 --- a/Test/og/Program1.bpl +++ /dev/null @@ -1,33 +0,0 @@ -// 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/og/Program1.bpl.expect b/Test/og/Program1.bpl.expect deleted file mode 100644 index 3de74d3e..00000000 --- a/Test/og/Program1.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ -
-Boogie program verifier finished with 2 verified, 0 errors
diff --git a/Test/og/Program2.bpl b/Test/og/Program2.bpl deleted file mode 100644 index 75c83c67..00000000 --- a/Test/og/Program2.bpl +++ /dev/null @@ -1,37 +0,0 @@ -// 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/og/Program2.bpl.expect b/Test/og/Program2.bpl.expect deleted file mode 100644 index 5b2909f1..00000000 --- a/Test/og/Program2.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ -
-Boogie program verifier finished with 3 verified, 0 errors
diff --git a/Test/og/Program3.bpl b/Test/og/Program3.bpl deleted file mode 100644 index f8c4e132..00000000 --- a/Test/og/Program3.bpl +++ /dev/null @@ -1,36 +0,0 @@ -// 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/og/Program3.bpl.expect b/Test/og/Program3.bpl.expect deleted file mode 100644 index 5b2909f1..00000000 --- a/Test/og/Program3.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ -
-Boogie program verifier finished with 3 verified, 0 errors
diff --git a/Test/og/Program4.bpl b/Test/og/Program4.bpl deleted file mode 100644 index 7f2f9c44..00000000 --- a/Test/og/Program4.bpl +++ /dev/null @@ -1,68 +0,0 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-type Tid;
-var {:layer 0,1} a:[Tid]int;
-
-procedure {:yields} {:layer 1} main() {
- var {:linear "tid"} tid:Tid;
-
- yield;
- while (true) {
- call tid := Allocate();
- async call P(tid);
- yield;
- }
- yield;
-}
-
-procedure {:yields} {:layer 1} P({:linear "tid"} tid: Tid)
-ensures {:layer 1} a[tid] == old(a)[tid] + 1;
-{
- var t:int;
-
- yield;
- assert {:layer 1} a[tid] == old(a)[tid];
- call t := Read(tid);
- yield;
- assert {:layer 1} a[tid] == t;
- call Write(tid, t + 1);
- yield;
- assert {:layer 1} a[tid] == t + 1;
-}
-
-procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: Tid)
-{
- yield;
- call tid := AllocateLow();
- yield;
-}
-
-procedure {:yields} {:layer 0,1} Read({:linear "tid"} tid: Tid) returns (val: int);
-ensures {:atomic}
-|{A:
- val := a[tid]; return true;
-}|;
-
-procedure {:yields} {:layer 0,1} Write({:linear "tid"} tid: Tid, val: int);
-ensures {:atomic}
-|{A:
- a[tid] := val; return true;
-}|;
-
-procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: Tid);
-ensures {:atomic} |{ A: return true; }|;
-
-
-
-function {:builtin "MapConst"} MapConstBool(bool): [Tid]bool;
-function {:builtin "MapOr"} MapOr([Tid]bool, [Tid]bool) : [Tid]bool;
-
-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/og/Program4.bpl.expect b/Test/og/Program4.bpl.expect deleted file mode 100644 index 5b2909f1..00000000 --- a/Test/og/Program4.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ -
-Boogie program verifier finished with 3 verified, 0 errors
diff --git a/Test/og/Program5.bpl b/Test/og/Program5.bpl deleted file mode 100644 index 7ede3124..00000000 --- a/Test/og/Program5.bpl +++ /dev/null @@ -1,79 +0,0 @@ -// 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} 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: return true;}|;
-{
- var colorLocal:int;
- yield;
- call colorLocal := GetColorNoLock();
- call YieldColorOnlyGetsDarker();
- if (White(colorLocal)) { call WriteBarrierSlow(tid); }
- yield;
-}
-
-procedure {:yields} {:layer 1,2} WriteBarrierSlow({:linear "tid"} tid:Tid)
-ensures {:atomic} |{ A: assert tid != nil; goto B, C;
- B: assume White(Color); Color := GRAY(); return true;
- C: return true; }|;
-{
- var colorLocal:int;
- yield;
- call AcquireLock(tid);
- call colorLocal := GetColorLocked(tid);
- if (White(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/og/Program5.bpl.expect b/Test/og/Program5.bpl.expect deleted file mode 100644 index d7c0ff95..00000000 --- a/Test/og/Program5.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ -
-Boogie program verifier finished with 18 verified, 0 errors
diff --git a/Test/og/akash.bpl b/Test/og/akash.bpl deleted file mode 100644 index c826b810..00000000 --- a/Test/og/akash.bpl +++ /dev/null @@ -1,106 +0,0 @@ -// 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/og/akash.bpl.expect b/Test/og/akash.bpl.expect deleted file mode 100644 index fef5ddc0..00000000 --- a/Test/og/akash.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ -
-Boogie program verifier finished with 4 verified, 0 errors
diff --git a/Test/og/bar.bpl b/Test/og/bar.bpl deleted file mode 100644 index 4eef8378..00000000 --- a/Test/og/bar.bpl +++ /dev/null @@ -1,57 +0,0 @@ -// 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/og/bar.bpl.expect b/Test/og/bar.bpl.expect deleted file mode 100644 index 8999ae7f..00000000 --- a/Test/og/bar.bpl.expect +++ /dev/null @@ -1,13 +0,0 @@ -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$this_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 3 verified, 2 errors
diff --git a/Test/og/chris.bpl b/Test/og/chris.bpl deleted file mode 100644 index b54292ef..00000000 --- a/Test/og/chris.bpl +++ /dev/null @@ -1,28 +0,0 @@ -// 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/og/chris.bpl.expect b/Test/og/chris.bpl.expect deleted file mode 100644 index be6b95ba..00000000 --- a/Test/og/chris.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ -
-Boogie program verifier finished with 6 verified, 0 errors
diff --git a/Test/og/chris2.bpl b/Test/og/chris2.bpl deleted file mode 100644 index 73f112ed..00000000 --- a/Test/og/chris2.bpl +++ /dev/null @@ -1,34 +0,0 @@ -// 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/og/chris2.bpl.expect b/Test/og/chris2.bpl.expect deleted file mode 100644 index 2bf339f7..00000000 --- a/Test/og/chris2.bpl.expect +++ /dev/null @@ -1,18 +0,0 @@ -(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 1 verified, 4 errors
diff --git a/Test/og/civl-paper.bpl b/Test/og/civl-paper.bpl deleted file mode 100644 index a7042c6a..00000000 --- a/Test/og/civl-paper.bpl +++ /dev/null @@ -1,175 +0,0 @@ -// 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/og/civl-paper.bpl.expect b/Test/og/civl-paper.bpl.expect deleted file mode 100644 index 4bcd03fb..00000000 --- a/Test/og/civl-paper.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ -
-Boogie program verifier finished with 35 verified, 0 errors
diff --git a/Test/og/foo.bpl b/Test/og/foo.bpl deleted file mode 100644 index 7eeab890..00000000 --- a/Test/og/foo.bpl +++ /dev/null @@ -1,57 +0,0 @@ -// 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/og/foo.bpl.expect b/Test/og/foo.bpl.expect deleted file mode 100644 index 0d9de9db..00000000 --- a/Test/og/foo.bpl.expect +++ /dev/null @@ -1,8 +0,0 @@ -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$this_A
- (0,0): inline$Impl_YieldChecker_PC_1$0$L0
-
-Boogie program verifier finished with 4 verified, 1 error
diff --git a/Test/og/linear-set.bpl b/Test/og/linear-set.bpl deleted file mode 100644 index e481291a..00000000 --- a/Test/og/linear-set.bpl +++ /dev/null @@ -1,105 +0,0 @@ -// 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/og/linear-set.bpl.expect b/Test/og/linear-set.bpl.expect deleted file mode 100644 index fef5ddc0..00000000 --- a/Test/og/linear-set.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ -
-Boogie program verifier finished with 4 verified, 0 errors
diff --git a/Test/og/linear-set2.bpl b/Test/og/linear-set2.bpl deleted file mode 100644 index 24d8a13a..00000000 --- a/Test/og/linear-set2.bpl +++ /dev/null @@ -1,106 +0,0 @@ -// 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/og/linear-set2.bpl.expect b/Test/og/linear-set2.bpl.expect deleted file mode 100644 index fef5ddc0..00000000 --- a/Test/og/linear-set2.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ -
-Boogie program verifier finished with 4 verified, 0 errors
diff --git a/Test/og/lock-introduced.bpl b/Test/og/lock-introduced.bpl deleted file mode 100644 index c9650215..00000000 --- a/Test/og/lock-introduced.bpl +++ /dev/null @@ -1,100 +0,0 @@ -// 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);
- 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);
- yield;
-}
-
-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/og/lock-introduced.bpl.expect b/Test/og/lock-introduced.bpl.expect deleted file mode 100644 index f62a8f46..00000000 --- a/Test/og/lock-introduced.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ -
-Boogie program verifier finished with 12 verified, 0 errors
diff --git a/Test/og/lock.bpl b/Test/og/lock.bpl deleted file mode 100644 index 9341591f..00000000 --- a/Test/og/lock.bpl +++ /dev/null @@ -1,57 +0,0 @@ -// 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/og/lock.bpl.expect b/Test/og/lock.bpl.expect deleted file mode 100644 index 05d394c7..00000000 --- a/Test/og/lock.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ -
-Boogie program verifier finished with 5 verified, 0 errors
diff --git a/Test/og/lock2.bpl b/Test/og/lock2.bpl deleted file mode 100644 index 4809a8f5..00000000 --- a/Test/og/lock2.bpl +++ /dev/null @@ -1,63 +0,0 @@ -// 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/og/lock2.bpl.expect b/Test/og/lock2.bpl.expect deleted file mode 100644 index 05d394c7..00000000 --- a/Test/og/lock2.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ -
-Boogie program verifier finished with 5 verified, 0 errors
diff --git a/Test/og/multiset.bpl b/Test/og/multiset.bpl deleted file mode 100644 index 7fb0a081..00000000 --- a/Test/og/multiset.bpl +++ /dev/null @@ -1,324 +0,0 @@ -// 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/og/multiset.bpl.expect b/Test/og/multiset.bpl.expect deleted file mode 100644 index d72077a6..00000000 --- a/Test/og/multiset.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ -
-Boogie program verifier finished with 78 verified, 0 errors
diff --git a/Test/og/new1.bpl b/Test/og/new1.bpl deleted file mode 100644 index b80b6315..00000000 --- a/Test/og/new1.bpl +++ /dev/null @@ -1,42 +0,0 @@ -// 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/og/new1.bpl.expect b/Test/og/new1.bpl.expect deleted file mode 100644 index 3de74d3e..00000000 --- a/Test/og/new1.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ -
-Boogie program verifier finished with 2 verified, 0 errors
diff --git a/Test/og/one.bpl b/Test/og/one.bpl deleted file mode 100644 index 663b2da0..00000000 --- a/Test/og/one.bpl +++ /dev/null @@ -1,18 +0,0 @@ -// 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/og/one.bpl.expect b/Test/og/one.bpl.expect deleted file mode 100644 index 6abb715b..00000000 --- a/Test/og/one.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ -
-Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/og/parallel1.bpl b/Test/og/parallel1.bpl deleted file mode 100644 index 20dd3c79..00000000 --- a/Test/og/parallel1.bpl +++ /dev/null @@ -1,48 +0,0 @@ -// 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/og/parallel1.bpl.expect b/Test/og/parallel1.bpl.expect deleted file mode 100644 index 588c9c5b..00000000 --- a/Test/og/parallel1.bpl.expect +++ /dev/null @@ -1,8 +0,0 @@ -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$this_A
- (0,0): inline$Impl_YieldChecker_PC_1$0$L0
-
-Boogie program verifier finished with 3 verified, 1 error
diff --git a/Test/og/parallel2.bpl b/Test/og/parallel2.bpl deleted file mode 100644 index c28edf2b..00000000 --- a/Test/og/parallel2.bpl +++ /dev/null @@ -1,59 +0,0 @@ -// 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/og/parallel2.bpl.expect b/Test/og/parallel2.bpl.expect deleted file mode 100644 index 05d394c7..00000000 --- a/Test/og/parallel2.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ -
-Boogie program verifier finished with 5 verified, 0 errors
diff --git a/Test/og/parallel4.bpl b/Test/og/parallel4.bpl deleted file mode 100644 index f06ff4b8..00000000 --- a/Test/og/parallel4.bpl +++ /dev/null @@ -1,45 +0,0 @@ -// 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/og/parallel4.bpl.expect b/Test/og/parallel4.bpl.expect deleted file mode 100644 index 25ad398c..00000000 --- a/Test/og/parallel4.bpl.expect +++ /dev/null @@ -1,6 +0,0 @@ -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 3 verified, 1 error
diff --git a/Test/og/parallel5.bpl b/Test/og/parallel5.bpl deleted file mode 100644 index 87afc888..00000000 --- a/Test/og/parallel5.bpl +++ /dev/null @@ -1,59 +0,0 @@ -// 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/og/parallel5.bpl.expect b/Test/og/parallel5.bpl.expect deleted file mode 100644 index 05d394c7..00000000 --- a/Test/og/parallel5.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ -
-Boogie program verifier finished with 5 verified, 0 errors
diff --git a/Test/og/perm.bpl b/Test/og/perm.bpl deleted file mode 100644 index 5bc75324..00000000 --- a/Test/og/perm.bpl +++ /dev/null @@ -1,49 +0,0 @@ -// 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/og/perm.bpl.expect b/Test/og/perm.bpl.expect deleted file mode 100644 index 3de74d3e..00000000 --- a/Test/og/perm.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ -
-Boogie program verifier finished with 2 verified, 0 errors
diff --git a/Test/og/t1.bpl b/Test/og/t1.bpl deleted file mode 100644 index 675b3842..00000000 --- a/Test/og/t1.bpl +++ /dev/null @@ -1,103 +0,0 @@ -// 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/og/t1.bpl.expect b/Test/og/t1.bpl.expect deleted file mode 100644 index 0b0c936e..00000000 --- a/Test/og/t1.bpl.expect +++ /dev/null @@ -1,9 +0,0 @@ -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$this_A
- (0,0): inline$Impl_YieldChecker_A_1$0$L1
-
-Boogie program verifier finished with 4 verified, 1 error
diff --git a/Test/og/termination.bpl b/Test/og/termination.bpl deleted file mode 100644 index 2d5542dd..00000000 --- a/Test/og/termination.bpl +++ /dev/null @@ -1,18 +0,0 @@ -// 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/og/termination.bpl.expect b/Test/og/termination.bpl.expect deleted file mode 100644 index d216a01d..00000000 --- a/Test/og/termination.bpl.expect +++ /dev/null @@ -1,3 +0,0 @@ -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/og/termination2.bpl b/Test/og/termination2.bpl deleted file mode 100644 index 840c27c1..00000000 --- a/Test/og/termination2.bpl +++ /dev/null @@ -1,19 +0,0 @@ -// 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/og/termination2.bpl.expect b/Test/og/termination2.bpl.expect deleted file mode 100644 index 6abb715b..00000000 --- a/Test/og/termination2.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ -
-Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl deleted file mode 100644 index 91863e1a..00000000 --- a/Test/og/ticket.bpl +++ /dev/null @@ -1,147 +0,0 @@ -// 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;
-function {:builtin "MapConst"} mapconstbool(bool): [X]bool;
-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/og/ticket.bpl.expect b/Test/og/ticket.bpl.expect deleted file mode 100644 index 28c26eab..00000000 --- a/Test/og/ticket.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ -
-Boogie program verifier finished with 16 verified, 0 errors
diff --git a/Test/og/treiber-stack.bpl b/Test/og/treiber-stack.bpl deleted file mode 100644 index e1c509ab..00000000 --- a/Test/og/treiber-stack.bpl +++ /dev/null @@ -1,202 +0,0 @@ -// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-type Node = int;
-const unique null: Node;
-type lmap;
-function {:linear "Node"} dom(lmap): [Node]bool;
-function map(lmap): [Node]Node;
-function {:builtin "MapConst"} MapConstBool(bool) : [Node]bool;
-
-function EmptyLmap(): (lmap);
-axiom (dom(EmptyLmap()) == MapConstBool(false));
-
-function Add(x: lmap, i: Node, v: Node): (lmap);
-axiom (forall x: lmap, i: Node, v: Node :: dom(Add(x, i, v)) == dom(x)[i:=true] && map(Add(x, i, v)) == map(x)[i := v]);
-
-function Remove(x: lmap, i: Node): (lmap);
-axiom (forall x: lmap, i: Node :: dom(Remove(x, i)) == dom(x)[i:=false] && map(Remove(x, i)) == map(x));
-
-procedure {:yields} {:layer 0,1} ReadTopOfStack() returns (v:Node);
-ensures {:right} |{ A: assume dom(Stack)[v] || dom(Used)[v]; return true; }|;
-
-procedure {:yields} {:layer 0,1} Load(i:Node) returns (v:Node);
-ensures {:right} |{ A: assert dom(Stack)[i] || dom(Used)[i]; goto B,C;
- B: assume dom(Stack)[i]; v := map(Stack)[i]; return true;
- C: assume !dom(Stack)[i]; return true; }|;
-
-procedure {:yields} {:layer 0,1} Store({:linear_in "Node"} l_in:lmap, i:Node, v:Node) returns ({:linear "Node"} l_out:lmap);
-ensures {:both} |{ A: assert dom(l_in)[i]; l_out := Add(l_in, i, v); return true; }|;
-
-procedure {:yields} {:layer 0,1} TransferToStack(oldVal: Node, newVal: Node, {:linear_in "Node"} l_in:lmap) returns (r: bool, {:linear "Node"} l_out:lmap);
-ensures {:atomic} |{ A: assert dom(l_in)[newVal];
- goto B,C;
- B: assume oldVal == TopOfStack; TopOfStack := newVal; l_out := EmptyLmap(); Stack := Add(Stack, newVal, map(l_in)[newVal]); r := true; return true;
- C: assume oldVal != TopOfStack; l_out := l_in; r := false; return true; }|;
-
-procedure {:yields} {:layer 0,1} TransferFromStack(oldVal: Node, newVal: Node) returns (r: bool);
-ensures {:atomic} |{ A: goto B,C;
- B: assume oldVal == TopOfStack; TopOfStack := newVal; Used := Add(Used, oldVal, map(Stack)[oldVal]); Stack := Remove(Stack, oldVal); r := true; return true;
- C: assume oldVal != TopOfStack; r := false; return true; }|;
-
-var {:layer 0} TopOfStack: Node;
-var {:linear "Node"} {:layer 0} Stack: lmap;
-
-
-function {:inline} Inv(TopOfStack: Node, Stack: lmap) : (bool)
-{
- BetweenSet(map(Stack), TopOfStack, null)[TopOfStack] &&
- Subset(BetweenSet(map(Stack), TopOfStack, null), Union(Singleton(null), dom(Stack)))
-}
-
-var {:linear "Node"} {:layer 0} Used: lmap;
-
-procedure {:yields} {:layer 1} push(x: Node, {:linear_in "Node"} x_lmap: lmap)
-requires {:layer 1} dom(x_lmap)[x];
-requires {:layer 1} Inv(TopOfStack, Stack);
-ensures {:layer 1} Inv(TopOfStack, Stack);
-ensures {:atomic} |{ A: Stack := Add(Stack, x, TopOfStack); TopOfStack := x; return true; }|;
-{
- var t: Node;
- var 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) {
- assert {:layer 1} map(Stack)[x] == t;
- 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()
-requires {:layer 1} Inv(TopOfStack, Stack);
-ensures {:layer 1} Inv(TopOfStack, Stack);
-ensures {:atomic} |{ var t: Node;
- A: assume TopOfStack != null; t := TopOfStack; Used := Add(Used, t, map(Stack)[t]); TopOfStack := map(Stack)[t]; Stack := Remove(Stack, t); return true; }|;
-{
- var g: bool;
- var x: Node;
- var t: Node;
-
- 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 Reachable([int,int]bool, 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/og/treiber-stack.bpl.expect b/Test/og/treiber-stack.bpl.expect deleted file mode 100644 index be6b95ba..00000000 --- a/Test/og/treiber-stack.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ -
-Boogie program verifier finished with 6 verified, 0 errors
diff --git a/Test/og/wsq.bpl b/Test/og/wsq.bpl deleted file mode 100644 index 9cb6a19b..00000000 --- a/Test/og/wsq.bpl +++ /dev/null @@ -1,560 +0,0 @@ -// 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 {:aux} oldH:int;
- var {:aux} oldT:int;
- var {:aux} oldStatusT:bool;
-
-
- oldH := H;
- oldT := T;
- 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);
-
- oldH := H;
- oldT := T;
- 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);
-
- oldH := H;
- oldT := T;
- oldStatusT := status[T];
- 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);
-
- oldH := H;
- oldT := T;
- 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 {:aux} oldH:int;
- var {:aux} oldT:int;
-
- oldH := H;
- oldT := T;
- 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);
- {
-
- oldH := H;
- oldT := T;
- 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);
-
- oldH := H;
- oldT := T;
- 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);
-
- oldH := H;
- oldT := T;
- 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);
-
- oldH := H;
- oldT := T;
- 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;
-
- oldH := H;
- oldT := T;
- 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);
-
- oldH := H;
- oldT := T;
- 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);
-
- oldH := H;
- oldT := T;
- 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);
- oldH := H;
- oldT := T;
-
- 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);
-
-
- oldH := H;
- oldT := T;
- 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) {
-
- oldH := H;
- oldT := T;
- 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;
- }
-
- oldH := H;
- oldT := T;
- 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;
- }
-
- oldH := H;
- oldT := T;
- 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 {:aux} oldH:int;
- var {:aux} oldT:int;
-
- oldH := H;
- oldT := T;
- 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];
- {
- oldH := H;
- oldT := T;
- 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);
-
- oldH := H;
- oldT := T;
- 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);
-
-
- oldH := H;
- oldT := T;
- 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);
-
- oldH := H;
- oldT := T;
- 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);
-
-
- oldH := H;
- oldT := T;
- 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);
-
- oldH := H;
- oldT := T;
- 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;
- }
-
- oldH := H;
- oldT := T;
- 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;
- }
-
- oldH := H;
- oldT := T;
- yield;
- assert {:layer 3} chk && task != EMPTY;
- assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid];
- assert {:layer 3} oldH <= H;
-}
-
-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/og/wsq.bpl.expect b/Test/og/wsq.bpl.expect deleted file mode 100644 index 5b2909f1..00000000 --- a/Test/og/wsq.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ -
-Boogie program verifier finished with 3 verified, 0 errors
|