From 24a49931e1c7d456008296e1255d8506d28cb18b Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Fri, 8 Jan 2016 11:36:11 -0800 Subject: added Free code --- Test/civl/alloc.bpl | 69 +++++++++++++++++++++++++++++++++-------------------- 1 file changed, 43 insertions(+), 26 deletions(-) (limited to 'Test') diff --git a/Test/civl/alloc.bpl b/Test/civl/alloc.bpl index 33535b00..56515ba8 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(pool)[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 -- cgit v1.2.3