From 4d9ec68b4b038ff2e4fe91eec2e82b1d613ee3b0 Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Thu, 21 Jan 2016 21:28:00 -0800 Subject: improved some of the annotations --- Test/civl/Program4.bpl | 54 ++++++++++++++++++++++----------------------- Test/civl/treiber-stack.bpl | 4 ++-- 2 files changed, 29 insertions(+), 29 deletions(-) (limited to 'Test') diff --git a/Test/civl/Program4.bpl b/Test/civl/Program4.bpl index a6dfcb2a..11ba8afa 100644 --- a/Test/civl/Program4.bpl +++ b/Test/civl/Program4.bpl @@ -2,51 +2,51 @@ // RUN: %diff "%s.expect" "%t" var {:layer 0,2} a:[int]int; var {:layer 0,1} count: int; -var {:layer 1,1} {:linear "tid"} unallocated:[int]bool; +var {:layer 1,1} {:linear "tid"} allocated:[int]bool; procedure {:yields} {:layer 2} main() -requires {:layer 1} AllocInv(count, unallocated); +requires {:layer 1} allocated == MapConstBool(false); { var {:layer 1} {:linear "tid"} tid:int; var i: int; yield; - assert {:layer 1} AllocInv(count, unallocated); + assert {:layer 1} AllocInv(count, allocated); while (true) - invariant {:layer 1} AllocInv(count, unallocated); + invariant {:layer 1} AllocInv(count, allocated); { call tid, i := Allocate(); async call P(tid, i); yield; - assert {:layer 1} AllocInv(count, unallocated); + assert {:layer 1} AllocInv(count, allocated); } yield; } procedure {:yields} {:layer 2} P({:layer 1} {:linear "tid"} tid: int, i: int) requires {:layer 1} tid == i; -requires {:layer 1} AllocInv(count, unallocated); -ensures {:layer 1} AllocInv(count, unallocated); +requires {:layer 1} AllocInv(count, allocated); +ensures {:layer 1} AllocInv(count, allocated); ensures {:layer 2} a[tid] == old(a)[tid] + 1; { var t:int; yield; - assert {:layer 1} AllocInv(count, unallocated); + assert {:layer 1} AllocInv(count, allocated); assert {:layer 2} a[tid] == old(a)[tid]; call t := Read(tid, i); yield; - assert {:layer 1} AllocInv(count, unallocated); + assert {:layer 1} AllocInv(count, allocated); assert {:layer 2} a[tid] == t; call Write(tid, i, t + 1); yield; - assert {:layer 1} AllocInv(count, unallocated); + assert {:layer 1} AllocInv(count, allocated); assert {:layer 2} a[tid] == t + 1; } procedure {:yields} {:layer 1,2} Allocate() returns ({:layer 1} {:linear "tid"} tid: int, i: int) -requires {:layer 1} AllocInv(count, unallocated); -ensures {:layer 1} AllocInv(count, unallocated); +requires {:layer 1} AllocInv(count, allocated); +ensures {:layer 1} AllocInv(count, allocated); ensures {:layer 1} tid == i; ensures {:atomic} |{A: @@ -54,48 +54,48 @@ ensures {:atomic} }|; { yield; - assert {:layer 1} AllocInv(count, unallocated); + assert {:layer 1} AllocInv(count, allocated); call i := AllocateLow(); call tid := MakeLinear(i); yield; - assert {:layer 1} AllocInv(count, unallocated); + assert {:layer 1} AllocInv(count, allocated); } procedure {:yields} {:layer 1,2} Read({:layer 1} {:linear "tid"} tid: int, i: int) returns (val: int) requires {:layer 1} tid == i; -requires {:layer 1} AllocInv(count, unallocated); -ensures {:layer 1} AllocInv(count, unallocated); +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, unallocated); + assert {:layer 1} AllocInv(count, allocated); call val := ReadLow(i); yield; - assert {:layer 1} AllocInv(count, unallocated); + assert {:layer 1} AllocInv(count, allocated); } procedure {:yields} {:layer 1,2} Write({:layer 1} {:linear "tid"} tid: int, i: int, val: int) requires {:layer 1} tid == i; -requires {:layer 1} AllocInv(count, unallocated); -ensures {:layer 1} AllocInv(count, unallocated); +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, unallocated); + assert {:layer 1} AllocInv(count, allocated); call WriteLow(i, val); yield; - assert {:layer 1} AllocInv(count, unallocated); + assert {:layer 1} AllocInv(count, allocated); } -function {:inline} AllocInv(count: int, unallocated:[int]bool): (bool) +function {:inline} AllocInv(count: int, allocated:[int]bool): (bool) { - (forall x: int :: count <= x ==> unallocated[x]) + (forall x: int :: allocated[x] ==> x < count) } procedure {:yields} {:layer 0,1} ReadLow(i: int) returns (val: int); @@ -121,9 +121,9 @@ ensures {:atomic} // 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 unallocated[i]; -modifies unallocated; -ensures tid == i && unallocated == old(unallocated)[i := false]; +requires !allocated[i]; +modifies allocated; +ensures tid == i && allocated == old(allocated)[i := true]; function {:builtin "MapConst"} MapConstBool(bool): [int]bool; function {:builtin "MapOr"} MapOr([int]bool, [int]bool) : [int]bool; diff --git a/Test/civl/treiber-stack.bpl b/Test/civl/treiber-stack.bpl index bb0201a9..64e01c99 100644 --- a/Test/civl/treiber-stack.bpl +++ b/Test/civl/treiber-stack.bpl @@ -1,7 +1,7 @@ // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" // RUN: %diff "%s.expect" "%t" -const unique null: int; +const null: int; type lmap; function {:linear "Node"} dom(lmap): [int]bool; function map(lmap): [int]int; @@ -17,7 +17,7 @@ function Remove(x: lmap, i: int): (lmap); axiom (forall x: lmap, i: int :: dom(Remove(x, i)) == dom(x)[i:=false] && map(Remove(x, i)) == map(x)); procedure {:yields} {:layer 0,1} ReadTopOfStack() returns (v:int); -ensures {:right} |{ A: assume dom(Stack)[v] || Used[v]; return true; }|; +ensures {:right} |{ A: assume v == null || dom(Stack)[v] || Used[v]; return true; }|; procedure {:yields} {:layer 0,1} Load(i:int) returns (v:int); ensures {:right} |{ A: assert dom(Stack)[i] || Used[i]; goto B,C; -- cgit v1.2.3