summaryrefslogtreecommitdiff
path: root/Test/civl/alloc.bpl
diff options
context:
space:
mode:
authorGravatar Rustan Leino <leino@microsoft.com>2016-02-12 16:47:51 -0800
committerGravatar Rustan Leino <leino@microsoft.com>2016-02-12 16:47:51 -0800
commit7ce69481c0b6af79a6d6542989832cd90fc5690f (patch)
treea91488b8ad92bc69718f2d5fda1d44082a3959de /Test/civl/alloc.bpl
parentabee810ceedbf551194788164fdf723edc511c0c (diff)
parent5fb565e439255ede7dc3653708af41678b6c1062 (diff)
Merge branch 'master' of https://github.com/boogie-org/boogie
Diffstat (limited to 'Test/civl/alloc.bpl')
-rw-r--r--Test/civl/alloc.bpl69
1 files changed, 43 insertions, 26 deletions
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