summaryrefslogtreecommitdiff
path: root/Test/civl
diff options
context:
space:
mode:
Diffstat (limited to 'Test/civl')
-rw-r--r--Test/civl/Program4.bpl119
-rw-r--r--Test/civl/Program4.bpl.expect2
-rw-r--r--Test/civl/alloc.bpl69
-rw-r--r--Test/civl/chris8.bpl15
-rw-r--r--Test/civl/chris8.bpl.expect2
-rw-r--r--Test/civl/funky.bpl133
-rw-r--r--Test/civl/funky.bpl.expect2
-rw-r--r--Test/civl/ticket.bpl5
-rw-r--r--Test/civl/treiber-stack.bpl61
-rw-r--r--Test/civl/wsq.bpl14
10 files changed, 334 insertions, 88 deletions
diff --git a/Test/civl/Program4.bpl b/Test/civl/Program4.bpl
index 68c2a5f3..11ba8afa 100644
--- a/Test/civl/Program4.bpl
+++ b/Test/civl/Program4.bpl
@@ -1,67 +1,138 @@
// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
-type Tid;
-var {:layer 0,1} a:[Tid]int;
+var {:layer 0,2} a:[int]int;
+var {:layer 0,1} count: int;
+var {:layer 1,1} {:linear "tid"} allocated:[int]bool;
-procedure {:yields} {:layer 1} main() {
- var {:linear "tid"} tid:Tid;
+procedure {:yields} {:layer 2} main()
+requires {:layer 1} allocated == MapConstBool(false);
+{
+ var {:layer 1} {:linear "tid"} tid:int;
+ var i: int;
yield;
- while (true) {
- call tid := Allocate();
- async call P(tid);
+ assert {:layer 1} AllocInv(count, allocated);
+ while (true)
+ invariant {:layer 1} AllocInv(count, allocated);
+ {
+ call tid, i := Allocate();
+ async call P(tid, i);
yield;
+ assert {:layer 1} AllocInv(count, allocated);
}
yield;
}
-procedure {:yields} {:layer 1} P({:linear "tid"} tid: Tid)
-ensures {:layer 1} a[tid] == old(a)[tid] + 1;
+procedure {:yields} {:layer 2} P({:layer 1} {:linear "tid"} tid: int, i: int)
+requires {:layer 1} tid == i;
+requires {:layer 1} AllocInv(count, allocated);
+ensures {:layer 1} AllocInv(count, allocated);
+ensures {:layer 2} a[tid] == old(a)[tid] + 1;
{
var t:int;
yield;
- assert {:layer 1} a[tid] == old(a)[tid];
- call t := Read(tid);
+ assert {:layer 1} AllocInv(count, allocated);
+ assert {:layer 2} a[tid] == old(a)[tid];
+ call t := Read(tid, i);
yield;
- assert {:layer 1} a[tid] == t;
- call Write(tid, t + 1);
+ assert {:layer 1} AllocInv(count, allocated);
+ assert {:layer 2} a[tid] == t;
+ call Write(tid, i, t + 1);
yield;
- assert {:layer 1} a[tid] == t + 1;
+ assert {:layer 1} AllocInv(count, allocated);
+ assert {:layer 2} a[tid] == t + 1;
}
-procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: Tid)
+procedure {:yields} {:layer 1,2} Allocate() returns ({:layer 1} {:linear "tid"} tid: int, i: int)
+requires {:layer 1} AllocInv(count, allocated);
+ensures {:layer 1} AllocInv(count, allocated);
+ensures {:layer 1} tid == i;
+ensures {:atomic}
+|{A:
+ return true;
+}|;
{
yield;
- call tid := AllocateLow();
+ assert {:layer 1} AllocInv(count, allocated);
+ call i := AllocateLow();
+ call tid := MakeLinear(i);
yield;
+ assert {:layer 1} AllocInv(count, allocated);
}
-procedure {:yields} {:layer 0,1} Read({:linear "tid"} tid: Tid) returns (val: int);
+procedure {:yields} {:layer 1,2} Read({:layer 1} {:linear "tid"} tid: int, i: int) returns (val: int)
+requires {:layer 1} tid == i;
+requires {:layer 1} AllocInv(count, allocated);
+ensures {:layer 1} AllocInv(count, allocated);
ensures {:atomic}
|{A:
val := a[tid]; return true;
}|;
+{
+ yield;
+ assert {:layer 1} AllocInv(count, allocated);
+ call val := ReadLow(i);
+ yield;
+ assert {:layer 1} AllocInv(count, allocated);
+}
-procedure {:yields} {:layer 0,1} Write({:linear "tid"} tid: Tid, val: int);
+procedure {:yields} {:layer 1,2} Write({:layer 1} {:linear "tid"} tid: int, i: int, val: int)
+requires {:layer 1} tid == i;
+requires {:layer 1} AllocInv(count, allocated);
+ensures {:layer 1} AllocInv(count, allocated);
ensures {:atomic}
|{A:
a[tid] := val; return true;
}|;
+{
+ yield;
+ assert {:layer 1} AllocInv(count, allocated);
+ call WriteLow(i, val);
+ yield;
+ assert {:layer 1} AllocInv(count, allocated);
+}
-procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: Tid);
-ensures {:atomic} |{ A: return true; }|;
+function {:inline} AllocInv(count: int, allocated:[int]bool): (bool)
+{
+ (forall x: int :: allocated[x] ==> x < count)
+}
+
+procedure {:yields} {:layer 0,1} ReadLow(i: int) returns (val: int);
+ensures {:atomic}
+|{A:
+ val := a[i]; return true;
+}|;
+
+procedure {:yields} {:layer 0,1} WriteLow(i: int, val: int);
+ensures {:atomic}
+|{A:
+ a[i] := val; return true;
+}|;
+procedure {:yields} {:layer 0,1} AllocateLow() returns (i: int);
+ensures {:atomic}
+|{A:
+ i := count;
+ count := i + 1;
+ return true;
+}|;
+// We can prove that this primitive procedure preserves the permission invariant locally.
+// We only need to using its specification and the definitions of TidCollector and TidSetCollector.
+procedure {:layer 1} MakeLinear(i: int) returns ({:linear "tid"} tid: int);
+requires !allocated[i];
+modifies allocated;
+ensures tid == i && allocated == old(allocated)[i := true];
-function {:builtin "MapConst"} MapConstBool(bool): [Tid]bool;
-function {:builtin "MapOr"} MapOr([Tid]bool, [Tid]bool) : [Tid]bool;
+function {:builtin "MapConst"} MapConstBool(bool): [int]bool;
+function {:builtin "MapOr"} MapOr([int]bool, [int]bool) : [int]bool;
-function {:inline} {:linear "tid"} TidCollector(x: Tid) : [Tid]bool
+function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool
{
MapConstBool(false)[x := true]
}
-function {:inline} {:linear "tid"} TidSetCollector(x: [Tid]bool) : [Tid]bool
+function {:inline} {:linear "tid"} TidSetCollector(x: [int]bool) : [int]bool
{
x
}
diff --git a/Test/civl/Program4.bpl.expect b/Test/civl/Program4.bpl.expect
index 9823d44a..f08c6e00 100644
--- a/Test/civl/Program4.bpl.expect
+++ b/Test/civl/Program4.bpl.expect
@@ -1,2 +1,2 @@
-Boogie program verifier finished with 6 verified, 0 errors
+Boogie program verifier finished with 12 verified, 0 errors
diff --git a/Test/civl/alloc.bpl b/Test/civl/alloc.bpl
index 33535b00..68b7e6c6 100644
--- a/Test/civl/alloc.bpl
+++ b/Test/civl/alloc.bpl
@@ -11,21 +11,26 @@ axiom (forall x: [int]bool, y: [int]int :: {cons(x,y)} dom(cons(x, y)) == x && m
function EmptyLmap(): (lmap);
axiom (dom(EmptyLmap()) == MapConstBool(false));
-function Add(x: lmap, i: int, v: int): (lmap);
-axiom (forall x: lmap, i: int, v: int :: dom(Add(x, i, v)) == dom(x)[i:=true] && map(Add(x, i, v)) == map(x)[i := v]);
+function Add(x: lmap, i: int): (lmap);
+axiom (forall x: lmap, i: int :: dom(Add(x, i)) == dom(x)[i:=true] && map(Add(x, i)) == map(x));
function Remove(x: lmap, i: int): (lmap);
axiom (forall x: lmap, i: int :: dom(Remove(x, i)) == dom(x)[i:=false] && map(Remove(x, i)) == map(x));
+function {:inline} PoolInv(unallocated:[int]bool, pool: lmap) : (bool)
+{
+ (forall x: int :: unallocated[x] ==> dom(pool)[x])
+}
+
procedure {:yields} {:layer 2} Main()
-requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
-ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+requires {:layer 1} PoolInv(unallocated, pool);
+ensures {:layer 1} PoolInv(unallocated, pool);
{
var {:layer 1} {:linear "mem"} l: lmap;
var i: int;
par Yield() | Dummy();
while (*)
- invariant {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+ invariant {:layer 1} PoolInv(unallocated, pool);
{
call l, i := Alloc();
async call Thread(l, i);
@@ -35,8 +40,8 @@ ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
}
procedure {:yields} {:layer 2} Thread({:layer 1} {:linear_in "mem"} local_in: lmap, i: int)
-requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
-ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+requires {:layer 1} PoolInv(unallocated, pool);
+ensures {:layer 1} PoolInv(unallocated, pool);
requires {:layer 1} dom(local_in)[i] && map(local_in)[i] == mem[i];
requires {:layer 2} dom(local_in)[i];
{
@@ -50,13 +55,13 @@ requires {:layer 2} dom(local_in)[i];
call o := Read(local, i);
assert {:layer 2} o == 42;
while (*)
- invariant {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+ invariant {:layer 1} PoolInv(unallocated, pool);
{
call l, y := Alloc();
call l := Write(l, y, 42);
call o := Read(l, y);
assert {:layer 2} o == 42;
- call Free(l);
+ call Free(l, y);
par Yield() | Dummy();
}
par Yield() | Dummy();
@@ -68,8 +73,8 @@ procedure {:pure} {:inline 1} Copy({:linear_in "mem"} l: lmap) returns ({:linear
}
procedure {:yields} {:layer 1,2} Alloc() returns ({:layer 1} {:linear "mem"} l: lmap, i: int)
-requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
-ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+requires {:layer 1} PoolInv(unallocated, pool);
+ensures {:layer 1} PoolInv(unallocated, pool);
ensures {:layer 1} dom(l)[i] && map(l)[i] == mem[i];
ensures {:right} |{ A: assume dom(l)[i]; return true; }|;
{
@@ -79,17 +84,21 @@ ensures {:right} |{ A: assume dom(l)[i]; return true; }|;
call YieldMem(l, i);
}
-procedure {:yields} {:layer 1,2} Free({:layer 1} {:linear_in "mem"} l: lmap)
-requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
-ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+procedure {:yields} {:layer 1,2} Free({:layer 1} {:linear_in "mem"} l: lmap, i: int)
+requires {:layer 1} PoolInv(unallocated, pool);
+ensures {:layer 1} PoolInv(unallocated, pool);
+requires {:layer 1} dom(l)[i];
ensures {:both} |{ A: return true; }|;
{
call Yield();
+ call FreeLinear(l, i);
+ call ReturnAddr(i);
+ call Yield();
}
procedure {:yields} {:layer 1,2} Read({:layer 1} {:linear "mem"} l: lmap, i: int) returns (o: int)
-requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
-ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+requires {:layer 1} PoolInv(unallocated, pool);
+ensures {:layer 1} PoolInv(unallocated, pool);
requires {:layer 1} dom(l)[i] && map(l)[i] == mem[i];
ensures {:both} |{ A: assert dom(l)[i]; o := map(l)[i]; return true; }|;
{
@@ -99,8 +108,8 @@ ensures {:both} |{ A: assert dom(l)[i]; o := map(l)[i]; return true; }|;
}
procedure {:yields} {:layer 1,2} Write({:layer 1} {:linear_in "mem"} l: lmap, i: int, o: int) returns ({:layer 1} {:linear "mem"} l': lmap)
-requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
-ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+requires {:layer 1} PoolInv(unallocated, pool);
+ensures {:layer 1} PoolInv(unallocated, pool);
requires {:layer 1} dom(l)[i] && map(l)[i] == mem[i];
ensures {:layer 1} dom(l')[i] && map(l')[i] == mem[i];
ensures {:both} |{ A: assert dom(l)[i]; l' := cons(dom(l), map(l)[i := o]); return true; }|;
@@ -116,26 +125,31 @@ modifies pool;
requires dom(pool)[i];
ensures pool == Remove(old(pool), i) && dom(l)[i] && map(l)[i] == mem[i];
+procedure {:layer 1} FreeLinear({:linear_in "mem"} l: lmap, i: int);
+modifies pool;
+requires dom(l)[i];
+ensures pool == Add(old(pool), i);
+
procedure {:layer 1} WriteLinear({:layer 1} {:linear_in "mem"} l: lmap, i: int, o: int) returns ({:layer 1} {:linear "mem"} l': lmap);
requires dom(l)[i];
ensures l' == cons(dom(l), map(l)[i := o]);
procedure {:yields} {:layer 1} Yield()
-requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
-ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+requires {:layer 1} PoolInv(unallocated, pool);
+ensures {:layer 1} PoolInv(unallocated, pool);
{
yield;
- assert {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+ assert {:layer 1} PoolInv(unallocated, pool);
}
procedure {:yields} {:layer 1} YieldMem({:layer 1} {:linear "mem"} l: lmap, i: int)
-requires {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
-ensures {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+requires {:layer 1} PoolInv(unallocated, pool);
+ensures {:layer 1} PoolInv(unallocated, pool);
requires {:layer 1} dom(l)[i] && map(l)[i] == mem[i];
ensures {:layer 1} dom(l)[i] && map(l)[i] == mem[i];
{
yield;
- assert {:layer 1} (forall x: int :: unallocated[x] ==> dom(pool)[x]);
+ assert {:layer 1} PoolInv(unallocated, pool);
assert {:layer 1} dom(l)[i] && map(l)[i] == mem[i];
}
@@ -144,7 +158,7 @@ procedure {:yields} {:layer 2} Dummy()
yield;
}
-var {:layer 1, 1} pool: lmap;
+var {:layer 1, 1} {:linear "mem"} pool: lmap;
var {:layer 0, 1} mem:[int]int;
var {:layer 0, 1} unallocated:[int]bool;
@@ -155,4 +169,7 @@ procedure {:yields} {:layer 0, 1} WriteLow(i: int, o: int);
ensures {:atomic} |{ A: mem[i] := o; return true; }|;
procedure {:yields} {:layer 0, 1} PickAddr() returns (i: int);
-ensures {:atomic} |{ A: assume unallocated[i]; unallocated[i] := false; return true; }|; \ No newline at end of file
+ensures {:atomic} |{ A: assume unallocated[i]; unallocated[i] := false; return true; }|;
+
+procedure {:yields} {:layer 0, 1} ReturnAddr(i: int);
+ensures {:atomic} |{ A: unallocated[i] := true; return true; }|; \ No newline at end of file
diff --git a/Test/civl/chris8.bpl b/Test/civl/chris8.bpl
new file mode 100644
index 00000000..070cfec4
--- /dev/null
+++ b/Test/civl/chris8.bpl
@@ -0,0 +1,15 @@
+// RUN: %boogie -noinfer -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var{:layer 1,1} x:int;
+
+procedure{:layer 1}{:extern} P1(i:int);
+procedure{:pure}{:extern} P2(j:int);
+
+procedure{:yields}{:layer 1,2} A1({:layer 1}i:int)
+ ensures {:atomic} |{ A: return true; }|;
+{
+ yield;
+ call P1(i);
+ call P2(i);
+ yield;
+}
diff --git a/Test/civl/chris8.bpl.expect b/Test/civl/chris8.bpl.expect
new file mode 100644
index 00000000..37fad75c
--- /dev/null
+++ b/Test/civl/chris8.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/civl/funky.bpl b/Test/civl/funky.bpl
new file mode 100644
index 00000000..ad5bf271
--- /dev/null
+++ b/Test/civl/funky.bpl
@@ -0,0 +1,133 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+type X;
+const nil: X;
+function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
+function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool
+{
+ MapConstBool(false)[x := true]
+}
+
+var {:layer 0, 3} A: X;
+var {:layer 0, 3} B: X;
+var {:layer 0, 3} counter: int;
+
+procedure {:yields} {:layer 0, 3} LockA({:linear "tid"} tid: X);
+ensures {:right} |{ A: assert tid != nil; assume A == nil; A := tid; return true; }|;
+
+procedure {:yields} {:layer 0, 1} IncrA({:linear "tid"} tid: X);
+ensures {:right} |{ A: assert tid != nil && A == tid; counter := counter + 1; return true; }|;
+
+procedure {:yields} {:layer 0, 1} DecrA({:linear "tid"} tid: X);
+ensures {:right} |{ A: assert tid != nil && A == tid; counter := counter - 1; return true; }|;
+
+procedure {:yields} {:layer 0, 3} UnlockA({:linear "tid"} tid: X);
+ensures {:left} |{ A: assert tid != nil && A == tid; A := nil; return true; }|;
+
+procedure {:yields} {:layer 0, 3} LockB({:linear "tid"} tid: X);
+ensures {:right} |{ A: assert tid != nil; assume B == nil; B := tid; return true; }|;
+
+procedure {:yields} {:layer 0, 2} IncrB({:linear "tid"} tid: X);
+ensures {:atomic} |{ A: assert tid != nil && B == tid; counter := counter + 1; return true; }|;
+
+procedure {:yields} {:layer 0, 1} DecrB({:linear "tid"} tid: X);
+ensures {:atomic} |{ A: assert tid != nil && B == tid; counter := counter - 1; return true; }|;
+
+procedure {:yields} {:layer 0, 3} UnlockB({:linear "tid"} tid: X);
+ensures {:left} |{ A: assert tid != nil && B == tid; B := nil; return true; }|;
+
+procedure {:yields} {:layer 0, 3} AssertA({:linear "tid"} tid: X);
+ensures {:atomic} |{ A: assert tid != nil && A == tid; assert counter >= -1; return true; }|;
+
+procedure {:yields} {:layer 0, 3} AssertB({:linear "tid"} tid: X);
+ensures {:atomic} |{ A: assert tid != nil && A == tid && B == tid; assert counter == 0; return true; }|;
+
+procedure {:pure} AllocTid() returns ({:linear "tid"} tid: X);
+ensures tid != nil;
+
+procedure {:yields} {:layer 1, 2} AbsDecrB({:linear "tid"} tid: X)
+ensures {:right} |{ A: assert tid != nil && B == tid && counter == 0; counter := counter - 1; return true; }|;
+{
+ yield;
+ call DecrB(tid);
+ yield;
+}
+
+procedure {:yields} {:layer 2, 3} AbsAssertA({:linear "tid"} tid: X)
+ensures {:both} |{ A: assert tid != nil && A == tid; assert counter >= -1; return true; }|;
+{
+ yield;
+ call AssertA(tid);
+ yield;
+}
+
+procedure {:yields} {:layer 2, 3} AbsAssertB({:linear "tid"} tid: X)
+ensures {:both} |{ A: assert tid != nil && A == tid && B == tid; assert counter == 0; return true; }|;
+{
+ yield;
+ call AssertB(tid);
+ yield;
+}
+
+procedure {:yields} {:layer 1} TA({:linear "tid"} tid: X)
+requires {:layer 1} tid != nil;
+{
+ yield;
+ call LockA(tid);
+ call IncrA(tid);
+ call DecrA(tid);
+ call UnlockA(tid);
+ yield;
+}
+
+procedure {:yields} {:layer 2, 3} TB({:linear "tid"} tid: X)
+ensures {:both} |{ A: assert tid != nil && counter == 0; return true; }|;
+{
+ yield;
+ call LockB(tid);
+ call AbsDecrB(tid);
+ call IncrB(tid);
+ call UnlockB(tid);
+ yield;
+}
+
+procedure {:yields} {:layer 3} AbsTB({:linear "tid"} tid: X)
+requires {:layer 3} tid != nil && counter == 0;
+{
+ yield;
+ assert {:layer 3} counter == 0;
+ call TB(tid);
+ yield;
+}
+
+procedure {:yields} {:layer 3} main({:linear "tid"} tid: X)
+requires {:layer 3} tid != nil && counter == 0;
+{
+ var {:linear "tid"} cid: X;
+
+ yield;
+ assert {:layer 3} counter == 0;
+ while (*)
+ invariant {:layer 3} counter == 0;
+ {
+ if (*) {
+ call cid := AllocTid();
+ async call TA(cid);
+ }
+ if (*) {
+ call cid := AllocTid();
+ async call AbsTB(cid);
+ }
+ yield;
+ assert {:layer 3} counter == 0;
+ call LockA(tid);
+ call AbsAssertA(tid);
+ call LockB(tid);
+ call AbsAssertB(tid);
+ call UnlockB(tid);
+ call UnlockA(tid);
+ yield;
+ assert {:layer 3} counter == 0;
+ }
+ yield;
+} \ No newline at end of file
diff --git a/Test/civl/funky.bpl.expect b/Test/civl/funky.bpl.expect
new file mode 100644
index 00000000..0a114594
--- /dev/null
+++ b/Test/civl/funky.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 75 verified, 0 errors
diff --git a/Test/civl/ticket.bpl b/Test/civl/ticket.bpl
index 9fc55646..df19aae4 100644
--- a/Test/civl/ticket.bpl
+++ b/Test/civl/ticket.bpl
@@ -6,7 +6,6 @@ axiom (forall x: int, y: int :: RightOpen(x)[y] <==> y < x);
axiom (forall x: int, y: int :: RightClosed(x)[y] <==> y <= x);
type X;
-function {:builtin "MapConst"} mapconstbool(bool): [X]bool;
const nil: X;
var {:layer 0,2} t: int;
var {:layer 0,2} s: int;
@@ -42,7 +41,7 @@ ensures {:layer 1} {:layer 2} xl != nil;
}
procedure {:yields} {:layer 2} main({:linear_in "tid"} xls':[X]bool)
-requires {:layer 2} xls' == mapconstbool(true);
+requires {:layer 2} xls' == MapConstBool(true);
{
var {:linear "tid"} tid: X;
var {:linear "tid"} xls: [X]bool;
@@ -132,7 +131,7 @@ ensures {:layer 1} Inv1(T,t);
}
procedure {:yields} {:layer 0,2} Init({:linear "tid"} xls:[X]bool);
-ensures {:atomic} |{ A: assert xls == mapconstbool(true); cs := nil; t := 0; s := 0; T := RightOpen(0); return true; }|;
+ensures {:atomic} |{ A: assert xls == MapConstBool(true); cs := nil; t := 0; s := 0; T := RightOpen(0); return true; }|;
procedure {:yields} {:layer 0,1} GetTicket({:linear "tid"} tid: X) returns (m: int);
ensures {:atomic} |{ A: m := t; t := t + 1; T[m] := true; return true; }|;
diff --git a/Test/civl/treiber-stack.bpl b/Test/civl/treiber-stack.bpl
index 751ce861..a184886d 100644
--- a/Test/civl/treiber-stack.bpl
+++ b/Test/civl/treiber-stack.bpl
@@ -1,62 +1,71 @@
// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
-type Node = int;
-const unique null: Node;
+
+const null: int;
type lmap;
-function {:linear "Node"} dom(lmap): [Node]bool;
-function map(lmap): [Node]Node;
-function {:builtin "MapConst"} MapConstBool(bool) : [Node]bool;
+function {:linear "Node"} dom(lmap): [int]bool;
+function map(lmap): [int]int;
+function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;
function EmptyLmap(): (lmap);
axiom (dom(EmptyLmap()) == MapConstBool(false));
-function Add(x: lmap, i: Node, v: Node): (lmap);
-axiom (forall x: lmap, i: Node, v: Node :: dom(Add(x, i, v)) == dom(x)[i:=true] && map(Add(x, i, v)) == map(x)[i := v]);
+function Add(x: lmap, i: int, v: int): (lmap);
+axiom (forall x: lmap, i: int, v: int :: dom(Add(x, i, v)) == dom(x)[i:=true] && map(Add(x, i, v)) == map(x)[i := v]);
-function Remove(x: lmap, i: Node): (lmap);
-axiom (forall x: lmap, i: Node :: dom(Remove(x, i)) == dom(x)[i:=false] && map(Remove(x, i)) == map(x));
+function Remove(x: lmap, i: int): (lmap);
+axiom (forall x: lmap, i: int :: dom(Remove(x, i)) == dom(x)[i:=false] && map(Remove(x, i)) == map(x));
-procedure {:yields} {:layer 0,1} ReadTopOfStack() returns (v:Node);
-ensures {:right} |{ A: assume dom(Stack)[v] || dom(Used)[v]; return true; }|;
+procedure {:yields} {:layer 0,1} ReadTopOfStack() returns (v:int);
+ensures {:right} |{ A: assume v == null || dom(Stack)[v] || Used[v]; return true; }|;
-procedure {:yields} {:layer 0,1} Load(i:Node) returns (v:Node);
-ensures {:right} |{ A: assert dom(Stack)[i] || dom(Used)[i]; goto B,C;
+procedure {:yields} {:layer 0,1} Load(i:int) returns (v:int);
+ensures {:right} |{ A: assert dom(Stack)[i] || Used[i]; goto B,C;
B: assume dom(Stack)[i]; v := map(Stack)[i]; return true;
C: assume !dom(Stack)[i]; return true; }|;
-procedure {:yields} {:layer 0,1} Store({:linear_in "Node"} l_in:lmap, i:Node, v:Node) returns ({:linear "Node"} l_out:lmap);
+procedure {:yields} {:layer 0,1} Store({:linear_in "Node"} l_in:lmap, i:int, v:int) returns ({:linear "Node"} l_out:lmap);
ensures {:both} |{ A: assert dom(l_in)[i]; l_out := Add(l_in, i, v); return true; }|;
-procedure {:yields} {:layer 0,1} TransferToStack(oldVal: Node, newVal: Node, {:linear_in "Node"} l_in:lmap) returns (r: bool, {:linear "Node"} l_out:lmap);
+procedure {:yields} {:layer 0,1} TransferToStack(oldVal: int, newVal: int, {:linear_in "Node"} l_in:lmap) returns (r: bool, {:linear "Node"} l_out:lmap);
ensures {:atomic} |{ A: assert dom(l_in)[newVal];
goto B,C;
B: assume oldVal == TopOfStack; TopOfStack := newVal; l_out := EmptyLmap(); Stack := Add(Stack, newVal, map(l_in)[newVal]); r := true; return true;
C: assume oldVal != TopOfStack; l_out := l_in; r := false; return true; }|;
-procedure {:yields} {:layer 0,1} TransferFromStack(oldVal: Node, newVal: Node) returns (r: bool);
+procedure {:yields} {:layer 0,1} TransferFromStack(oldVal: int, newVal: int) returns (r: bool);
ensures {:atomic} |{ A: goto B,C;
- B: assume oldVal == TopOfStack; TopOfStack := newVal; Used := Add(Used, oldVal, map(Stack)[oldVal]); Stack := Remove(Stack, oldVal); r := true; return true;
+ B: assume oldVal == TopOfStack; TopOfStack := newVal; Used[oldVal] := true; Stack := Remove(Stack, oldVal); r := true; return true;
C: assume oldVal != TopOfStack; r := false; return true; }|;
-var {:layer 0} TopOfStack: Node;
+var {:layer 0} TopOfStack: int;
var {:linear "Node"} {:layer 0} Stack: lmap;
-function {:inline} Inv(TopOfStack: Node, Stack: lmap) : (bool)
+function {:inline} Inv(TopOfStack: int, Stack: lmap) : (bool)
{
BetweenSet(map(Stack), TopOfStack, null)[TopOfStack] &&
Subset(BetweenSet(map(Stack), TopOfStack, null), Union(Singleton(null), dom(Stack)))
}
-var {:linear "Node"} {:layer 0} Used: lmap;
+var {:linear "Node"} {:layer 0} Used: [int]bool;
+
+function {:inline} {:linear "Node"} NodeCollector(x: int) : [int]bool
+{
+ MapConstBool(false)[x := true]
+}
+function {:inline} {:linear "Node"} NodeSetCollector(x: [int]bool) : [int]bool
+{
+ x
+}
-procedure {:yields} {:layer 1} push(x: Node, {:linear_in "Node"} x_lmap: lmap)
+procedure {:yields} {:layer 1} push(x: int, {:linear_in "Node"} x_lmap: lmap)
requires {:layer 1} dom(x_lmap)[x];
requires {:layer 1} Inv(TopOfStack, Stack);
ensures {:layer 1} Inv(TopOfStack, Stack);
ensures {:atomic} |{ A: Stack := Add(Stack, x, TopOfStack); TopOfStack := x; return true; }|;
{
- var t: Node;
+ var t: int;
var g: bool;
var {:linear "Node"} t_lmap: lmap;
@@ -71,7 +80,6 @@ ensures {:atomic} |{ A: Stack := Add(Stack, x, TopOfStack); TopOfStack := x; ret
call t_lmap := Store(t_lmap, x, t);
call g, t_lmap := TransferToStack(t, x, t_lmap);
if (g) {
- assert {:layer 1} map(Stack)[x] == t;
break;
}
yield;
@@ -82,13 +90,13 @@ ensures {:atomic} |{ A: Stack := Add(Stack, x, TopOfStack); TopOfStack := x; ret
assert {:expand} {:layer 1} Inv(TopOfStack, Stack);
}
-procedure {:yields} {:layer 1} pop() returns (t: Node)
+procedure {:yields} {:layer 1} pop() returns (t: int)
requires {:layer 1} Inv(TopOfStack, Stack);
ensures {:layer 1} Inv(TopOfStack, Stack);
-ensures {:atomic} |{ A: assume TopOfStack != null; t := TopOfStack; Used := Add(Used, t, map(Stack)[t]); TopOfStack := map(Stack)[t]; Stack := Remove(Stack, t); return true; }|;
+ensures {:atomic} |{ A: assume TopOfStack != null; t := TopOfStack; Used[t] := true; TopOfStack := map(Stack)[t]; Stack := Remove(Stack, t); return true; }|;
{
var g: bool;
- var x: Node;
+ var x: int;
yield;
assert {:layer 1} Inv(TopOfStack, Stack);
@@ -115,7 +123,6 @@ function Subset([int]bool, [int]bool) returns (bool);
function Empty() returns ([int]bool);
function Singleton(int) returns ([int]bool);
-function Reachable([int,int]bool, int) returns ([int]bool);
function Union([int]bool, [int]bool) returns ([int]bool);
axiom(forall x:int :: !Empty()[x]);
diff --git a/Test/civl/wsq.bpl b/Test/civl/wsq.bpl
index 39dad919..0a2227b6 100644
--- a/Test/civl/wsq.bpl
+++ b/Test/civl/wsq.bpl
@@ -89,9 +89,9 @@ ensures {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T);
ensures {:atomic} |{ var i: int; A: assume status[i] == NOT_IN_Q; status[i] := IN_Q; return true; }|;
{
var t: int;
- var {:ghost} {:layer 3} oldH:int;
- var {:ghost} {:layer 3} oldT:int;
- var {:ghost} {:layer 3} oldStatusT:bool;
+ var {:layer 3} oldH:int;
+ var {:layer 3} oldT:int;
+ var {:layer 3} oldStatusT:bool;
call oldH, oldT := GhostRead();
yield;
@@ -142,8 +142,8 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
{
var h, t: int;
var chk: bool;
- var {:ghost} {:layer 3} oldH:int;
- var {:ghost} {:layer 3} oldT:int;
+ var {:layer 3} oldH:int;
+ var {:layer 3} oldT:int;
call oldH, oldT := GhostRead();
yield;
@@ -304,8 +304,8 @@ ensures {:atomic} |{ var i: int; A: goto B,C; B: assume status[i] == IN_Q; statu
{
var h, t: int;
var chk: bool;
- var {:ghost} {:layer 3} oldH:int;
- var {:ghost} {:layer 3} oldT:int;
+ var {:layer 3} oldH:int;
+ var {:layer 3} oldT:int;
call oldH, oldT := GhostRead();
yield;
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 14:03:55 +0000