From c36b3d93a9c55dcb1d37d8b6ca09ae0b5114ec0b Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Tue, 19 Jan 2016 15:07:06 -0800 Subject: some fixes --- Test/civl/treiber-stack.bpl | 59 ++++++++++++++++++++++++++------------------- 1 file changed, 34 insertions(+), 25 deletions(-) (limited to 'Test/civl/treiber-stack.bpl') diff --git a/Test/civl/treiber-stack.bpl b/Test/civl/treiber-stack.bpl index 751ce861..bb0201a9 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 unique 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 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; @@ -82,13 +91,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); -- cgit v1.2.3 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/civl/treiber-stack.bpl') 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 From 1e0f2b1ea7e9cbfd1c7923674c0ed4601263d09a Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Tue, 26 Jan 2016 10:11:24 -0800 Subject: another fix --- Test/civl/treiber-stack.bpl | 2 -- 1 file changed, 2 deletions(-) (limited to 'Test/civl/treiber-stack.bpl') diff --git a/Test/civl/treiber-stack.bpl b/Test/civl/treiber-stack.bpl index 64e01c99..a184886d 100644 --- a/Test/civl/treiber-stack.bpl +++ b/Test/civl/treiber-stack.bpl @@ -80,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; @@ -124,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]); -- cgit v1.2.3