From 84819ceb711f1ae83327e2006df9bb1003ccd65e Mon Sep 17 00:00:00 2001 From: qadeer Date: Thu, 18 Dec 2014 20:59:10 -0800 Subject: changed type checking of yield procedures so that they can only call other yielding procedures --- Source/Concurrency/TypeCheck.cs | 10 +++++++++- Test/linear/typecheck.bpl | 4 +++- Test/linear/typecheck.bpl.expect | 32 ++++++++++++++++---------------- Test/og/DeviceCache.bpl | 20 +++++++++++++------- Test/og/DeviceCache.bpl.expect | 2 +- Test/og/FlanaganQadeer.bpl | 2 +- Test/og/Program4.bpl | 2 +- Test/og/akash.bpl | 6 +++--- Test/og/linear-set.bpl | 6 +++--- Test/og/linear-set2.bpl | 8 ++++---- Test/og/new1.bpl | 6 +++--- Test/og/parallel2.bpl | 2 +- Test/og/parallel4.bpl | 2 +- Test/og/parallel5.bpl | 2 +- Test/og/perm.bpl | 18 +++++------------- Test/og/t1.bpl | 22 +++++++++++++--------- Test/og/t1.bpl.expect | 8 ++++---- Test/og/ticket.bpl | 4 ++-- 18 files changed, 84 insertions(+), 72 deletions(-) diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs index 22aae914..8eb93e09 100644 --- a/Source/Concurrency/TypeCheck.cs +++ b/Source/Concurrency/TypeCheck.cs @@ -453,6 +453,10 @@ namespace Microsoft.Boogie Error(node, "The callee is not available in the caller procedure"); } } + else + { + Error(node, "Yielding procedure can call only a yielding procedure"); + } return base.VisitCallCmd(node); } @@ -517,7 +521,7 @@ namespace Microsoft.Boogie { Error(node, "Shared variable can be accessed only in atomic actions or specifications"); } - else + else if (this.globalVarToSharedVarInfo.ContainsKey(node.Decl)) { if (this.globalVarToSharedVarInfo[node.Decl].hideLayerNum < minLayerNum) { @@ -528,6 +532,10 @@ namespace Microsoft.Boogie maxLayerNum = this.globalVarToSharedVarInfo[node.Decl].introLayerNum; } } + else + { + Error(node, "Accessed shared variable must have layer annotation"); + } } else if (node.Decl is LocalVariable && auxVars.Contains(node.Decl) && !canAccessAuxVars) { diff --git a/Test/linear/typecheck.bpl b/Test/linear/typecheck.bpl index 57080cb8..5c936dd0 100644 --- a/Test/linear/typecheck.bpl +++ b/Test/linear/typecheck.bpl @@ -65,9 +65,11 @@ procedure {:yields} {:layer 1} D() yield; } -procedure E({:linear_in "D"} a: X, {:linear_in "D"} b: X) returns ({:linear "D"} c: X, {:linear "D"} d: X) +procedure {:yields} {:layer 1} E({:linear_in "D"} a: X, {:linear_in "D"} b: X) returns ({:linear "D"} c: X, {:linear "D"} d: X) { + yield; c := a; + yield; } procedure {:yields} {:layer 0} F({:linear_in "D"} a: X) returns ({:linear "D"} c: X); diff --git a/Test/linear/typecheck.bpl.expect b/Test/linear/typecheck.bpl.expect index dddbd163..5466fe62 100644 --- a/Test/linear/typecheck.bpl.expect +++ b/Test/linear/typecheck.bpl.expect @@ -1,16 +1,16 @@ -typecheck.bpl(33,9): Error: Only simple assignment allowed on linear variable b -typecheck.bpl(35,6): Error: Only variable can be assigned to linear variable a -typecheck.bpl(37,6): Error: Only linear variable can be assigned to linear variable a -typecheck.bpl(41,6): Error: Linear variable of domain D2 cannot be assigned to linear variable of domain D -typecheck.bpl(47,9): Error: Linear variable x can occur only once in the right-hand-side of an assignment -typecheck.bpl(51,4): Error: Linear variable a can occur only once as an input parameter -typecheck.bpl(53,4): Error: Only variable can be passed to linear parameter b -typecheck.bpl(55,4): Error: The domains of formal and actual parameters must be the same -typecheck.bpl(57,4): Error: The domains of formal and actual parameters must be the same -typecheck.bpl(59,4): Error: Only a linear argument can be passed to linear parameter a -typecheck.bpl(64,4): Error: Linear variable a can occur only once as an input parameter of a parallel call -typecheck.bpl(71,0): Error: Output variable d must be available at a return -typecheck.bpl(80,0): Error: Global variable g must be available at a return -typecheck.bpl(85,7): Error: unavailable source for a linear read -typecheck.bpl(86,0): Error: Output variable r must be available at a return -15 type checking errors detected in typecheck.bpl +typecheck.bpl(33,9): Error: Only simple assignment allowed on linear variable b +typecheck.bpl(35,6): Error: Only variable can be assigned to linear variable a +typecheck.bpl(37,6): Error: Only linear variable can be assigned to linear variable a +typecheck.bpl(41,6): Error: Linear variable of domain D2 cannot be assigned to linear variable of domain D +typecheck.bpl(47,9): Error: Linear variable x can occur only once in the right-hand-side of an assignment +typecheck.bpl(51,4): Error: Linear variable a can occur only once as an input parameter +typecheck.bpl(53,4): Error: Only variable can be passed to linear parameter b +typecheck.bpl(55,4): Error: The domains of formal and actual parameters must be the same +typecheck.bpl(57,4): Error: The domains of formal and actual parameters must be the same +typecheck.bpl(59,4): Error: Only a linear argument can be passed to linear parameter a +typecheck.bpl(64,4): Error: Linear variable a can occur only once as an input parameter of a parallel call +typecheck.bpl(73,0): Error: Output variable d must be available at a return +typecheck.bpl(82,0): Error: Global variable g must be available at a return +typecheck.bpl(87,7): Error: unavailable source for a linear read +typecheck.bpl(88,0): Error: Output variable r must be available at a return +15 type checking errors detected in typecheck.bpl diff --git a/Test/og/DeviceCache.bpl b/Test/og/DeviceCache.bpl index 703456ef..b204d9de 100644 --- a/Test/og/DeviceCache.bpl +++ b/Test/og/DeviceCache.bpl @@ -24,6 +24,14 @@ function {:inline} Inv(ghostLock: X, currsize: int, newsize: int) : (bool) (ghostLock == nil <==> currsize == newsize) } +procedure {:yields} {:layer 1} Yield() +requires {:layer 1} Inv(ghostLock, currsize, newsize); +ensures {:layer 1} Inv(ghostLock, currsize, newsize); +{ + yield; + assert {:layer 1} Inv(ghostLock, currsize, newsize); +} + procedure {:yields} {:layer 1} YieldToReadCache({:linear "tid"} tid: X) requires {:layer 1} Inv(ghostLock, currsize, newsize) && tid != nil; ensures {:layer 1} Inv(ghostLock, currsize, newsize) && old(currsize) <= currsize; @@ -40,18 +48,16 @@ ensures {:layer 1} Inv(ghostLock, currsize, newsize) && ghostLock == tid && old( assert {:layer 1} Inv(ghostLock, currsize, newsize) && tid != nil && ghostLock == tid && old(currsize) == currsize && old(newsize) == newsize; } -procedure Allocate({:linear_in "tid"} xls': [X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X); +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xl: X); ensures {:layer 1} xl != nil; -procedure {:yields} {:layer 1} main({:linear_in "tid"} xls':[X]bool) -requires {:layer 1} xls' == mapconstbool(true); +procedure {:yields} {:layer 1} main({:linear_in "tid"} xls: [X]bool) +requires {:layer 1} xls == mapconstbool(true); { var {:linear "tid"} tid: X; - var {:linear "tid"} xls: [X]bool; yield; - xls := xls'; call Init(xls); yield; @@ -60,7 +66,7 @@ requires {:layer 1} xls' == mapconstbool(true); while (*) invariant {:layer 1} Inv(ghostLock, currsize, newsize); { - call xls, tid := Allocate(xls); + par tid := Allocate() | Yield(); yield; assert {:layer 1} Inv(ghostLock, currsize, newsize); async call Thread(tid); @@ -168,7 +174,7 @@ ensures {:layer 1} Inv(ghostLock, currsize, newsize); par YieldToReadCache(tid); } -procedure {:yields} {:layer 0,1} Init({:linear "tid"} xls:[X]bool); +procedure {:yields} {:layer 0,1} Init({:linear_in "tid"} xls:[X]bool); ensures {:atomic} |{ A: assert xls == mapconstbool(true); currsize := 0; newsize := 0; lock := nil; ghostLock := nil; return true; }|; procedure {:yields} {:layer 0,1} ReadCurrsize({:linear "tid"} tid: X) returns (val: int); diff --git a/Test/og/DeviceCache.bpl.expect b/Test/og/DeviceCache.bpl.expect index 9e5be400..8c696418 100644 --- a/Test/og/DeviceCache.bpl.expect +++ b/Test/og/DeviceCache.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 28 verified, 0 errors +Boogie program verifier finished with 29 verified, 0 errors diff --git a/Test/og/FlanaganQadeer.bpl b/Test/og/FlanaganQadeer.bpl index 04255cf2..a912a89a 100644 --- a/Test/og/FlanaganQadeer.bpl +++ b/Test/og/FlanaganQadeer.bpl @@ -11,7 +11,7 @@ function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool MapConstBool(false)[x := true] } -procedure Allocate() returns ({:linear "tid"} xls: X); +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: X); ensures {:layer 1} xls != nil; procedure {:yields} {:layer 1} main() diff --git a/Test/og/Program4.bpl b/Test/og/Program4.bpl index 0228adc9..b8406f2e 100644 --- a/Test/og/Program4.bpl +++ b/Test/og/Program4.bpl @@ -15,7 +15,7 @@ function {:inline} {:linear "tid"} TidSetCollector(x: [Tid]bool) : [Tid]bool var {:layer 0,1} a:[Tid]int; -procedure Allocate() returns ({:linear "tid"} tid:Tid); +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid:Tid); procedure {:yields} {:layer 1} main() { var {:linear "tid"} tid:Tid; diff --git a/Test/og/akash.bpl b/Test/og/akash.bpl index 744029f1..cfbeaf3a 100644 --- a/Test/og/akash.bpl +++ b/Test/og/akash.bpl @@ -18,13 +18,13 @@ function {:inline} {:linear "2"} SetCollector2(x: [int]bool) : [int]bool x } -procedure Allocate() returns ({:linear "tid"} xls: int); +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: int); ensures {:layer 1} xls != 0; -procedure Allocate_1() returns ({:linear "1"} xls: [int]bool); +procedure {:yields} {:layer 1} Allocate_1() returns ({:linear "1"} xls: [int]bool); ensures {:layer 1} xls == mapconstbool(true); -procedure Allocate_2() returns ({:linear "2"} xls: [int]bool); +procedure {:yields} {:layer 1} Allocate_2() returns ({:linear "2"} xls: [int]bool); ensures {:layer 1} xls == mapconstbool(true); var {:layer 0,1} g: int; diff --git a/Test/og/linear-set.bpl b/Test/og/linear-set.bpl index 73849250..8752d402 100644 --- a/Test/og/linear-set.bpl +++ b/Test/og/linear-set.bpl @@ -23,10 +23,10 @@ function {:inline} {:linear "x"} XCollector(xs: [X]bool) : [X]bool var {:layer 0,1} x: int; var {:layer 0,1} l: [X]bool; -procedure Split({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool); -ensures xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None(); +procedure {:yields} {:layer 1} Split({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool); +ensures {:layer 1} xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None(); -procedure Allocate() returns ({:linear "tid"} xls: [X]bool); +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: [X]bool); procedure {:yields} {:layer 0,1} Set(v: int); ensures {:atomic} |{A: x := v; return true; }|; diff --git a/Test/og/linear-set2.bpl b/Test/og/linear-set2.bpl index 81d30521..a3b84702 100644 --- a/Test/og/linear-set2.bpl +++ b/Test/og/linear-set2.bpl @@ -24,11 +24,11 @@ var {:layer 0,1} x: int; var {:layer 0,1} l: X; const nil: X; -procedure Split({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool); -ensures xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None(); +procedure {:yields} {:layer 1} Split({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool); +ensures {:layer 1} xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None(); -procedure Allocate() returns ({:linear "tid"} xls: X); -ensures xls != nil; +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: X); +ensures {:layer 1} xls != nil; procedure {:yields} {:layer 0,1} Set(v: int); ensures {:atomic} |{A: x := v; return true; }|; diff --git a/Test/og/new1.bpl b/Test/og/new1.bpl index a6b50215..74b738d6 100644 --- a/Test/og/new1.bpl +++ b/Test/og/new1.bpl @@ -9,9 +9,9 @@ function {:inline} {:linear "Perm"} SetCollectorPerm(x: [int]bool) : [int]bool x } -procedure Allocate_Perm({:linear_in "Perm"} Permissions: [int]bool) returns ({:linear "Perm"} xls: [int]bool); -requires Permissions == mapconstbool(true); -ensures xls == mapconstbool(true); +procedure {:yields} {:layer 1} Allocate_Perm({:linear_in "Perm"} Permissions: [int]bool) returns ({:linear "Perm"} xls: [int]bool); +requires {:layer 1} Permissions == mapconstbool(true); +ensures {:layer 1} xls == mapconstbool(true); procedure {:yields} {:layer 1} PB({:linear_in "Perm"} permVar_in:[int]bool) requires {:layer 1} permVar_in[0] && g == 0; diff --git a/Test/og/parallel2.bpl b/Test/og/parallel2.bpl index 4f2cbd5b..ad40ffa0 100644 --- a/Test/og/parallel2.bpl +++ b/Test/og/parallel2.bpl @@ -8,7 +8,7 @@ function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool MapConstBool(false)[x := true] } -procedure Allocate() returns ({:linear "tid"} xls: int); +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: int); procedure {:yields} {:layer 0,1} Write(idx: int, val: int); ensures {:atomic} |{A: a[idx] := val; return true; }|; diff --git a/Test/og/parallel4.bpl b/Test/og/parallel4.bpl index 41d45b79..5340c4c8 100644 --- a/Test/og/parallel4.bpl +++ b/Test/og/parallel4.bpl @@ -2,7 +2,7 @@ // RUN: %diff "%s.expect" "%t" var {:layer 0,1} a:int; -procedure Allocate() returns ({:linear "tid"} xls: int); +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: int); function {:builtin "MapConst"} MapConstBool(bool) : [int]bool; function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool diff --git a/Test/og/parallel5.bpl b/Test/og/parallel5.bpl index bed51241..ea35a3b2 100644 --- a/Test/og/parallel5.bpl +++ b/Test/og/parallel5.bpl @@ -2,7 +2,7 @@ // RUN: %diff "%s.expect" "%t" var {:layer 0,1} a:[int]int; -procedure Allocate() returns ({:linear "tid"} xls: int); +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: int); function {:builtin "MapConst"} MapConstBool(bool) : [int]bool; function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool diff --git a/Test/og/perm.bpl b/Test/og/perm.bpl index f0de76d5..5bc75324 100644 --- a/Test/og/perm.bpl +++ b/Test/og/perm.bpl @@ -10,33 +10,25 @@ function {:inline} {:linear "Perm"} SetCollectorPerm(x: [int]bool) : [int]bool x } -procedure Split({:linear_in "Perm"} xls: [int]bool) returns ({:linear "Perm"} xls1: [int]bool, {:linear "Perm"} xls2: [int]bool); - ensures xls == ch_mapunion(xls1, xls2) && xls1 != ch_mapconstbool(false) && xls2 != ch_mapconstbool(false); - - procedure {:yields} {:layer 1} mainE({:linear_in "Perm"} permVar_in: [int]bool) - free requires {:layer 1} permVar_in == ch_mapconstbool(true); - free requires {:layer 1} permVar_in[0]; - free requires {:layer 1} x == 0; + requires {:layer 1} permVar_in == ch_mapconstbool(true); + requires {:layer 1} x == 0; { var {:linear "Perm"} permVar_out: [int]bool; - var {:linear "Perm"} permVarOut2: [int]bool; permVar_out := permVar_in; yield; assert {:layer 1} x == 0; - assert {:layer 1} permVar_out[0]; assert {:layer 1} permVar_out == ch_mapconstbool(true); - call permVar_out, permVarOut2 := Split(permVar_out); - async call foo(permVarOut2); + async call foo(permVar_out); yield; } procedure {:yields} {:layer 1} foo({:linear_in "Perm"} permVar_in: [int]bool) - free requires {:layer 1} permVar_in != ch_mapconstbool(false); - free requires {:layer 1} permVar_in[1]; + requires {:layer 1} permVar_in != ch_mapconstbool(false); + requires {:layer 1} permVar_in[1]; requires {:layer 1} x == 0; { var {:linear "Perm"} permVar_out: [int]bool; diff --git a/Test/og/t1.bpl b/Test/og/t1.bpl index b2f02bda..cb3dd138 100644 --- a/Test/og/t1.bpl +++ b/Test/og/t1.bpl @@ -18,13 +18,13 @@ function {:inline} {:linear "2"} SetCollector2(x: [int]bool) : [int]bool x } -procedure Allocate() returns ({:linear "tid"} xls: int); +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: int); ensures {:layer 1} xls != 0; -procedure Allocate_1() returns ({:linear "1"} xls: [int]bool); +procedure {:yields} {:layer 1} Allocate_1() returns ({:linear "1"} xls: [int]bool); ensures {:layer 1} xls == mapconstbool(true); -procedure Allocate_2() returns ({:linear "2"} xls: [int]bool); +procedure {:yields} {:layer 1} Allocate_2() returns ({:linear "2"} xls: [int]bool); ensures {:layer 1} xls == mapconstbool(true); var {:layer 0,1} g: int; @@ -36,6 +36,14 @@ ensures {:atomic} |{A: g := val; return true; }|; procedure {:yields} {:layer 0,1} SetH(val:int); ensures {:atomic} |{A: h := val; return true; }|; +procedure {:yields} {:layer 1} Yield({:linear "1"} x: [int]bool) +requires {:layer 1} x == mapconstbool(true) && g == 0; +ensures {:layer 1} x == mapconstbool(true) && g == 0; +{ + yield; + assert {:layer 1} x == mapconstbool(true) && g == 0; +} + procedure {:yields} {:layer 1} A({:linear_in "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int) { var {:linear "1"} x: [int]bool; @@ -47,19 +55,15 @@ procedure {:yields} {:layer 1} A({:linear_in "tid"} tid_in: int) returns ({:line yield; call SetG(0); - yield; - assert {:layer 1} x == mapconstbool(true); - assert {:layer 1} g == 0; + + par tid_child := Allocate() | Yield(x); - yield; - call tid_child := Allocate(); async call B(tid_child, x); yield; assert {:layer 1} x == mapconstbool(true); assert {:layer 1} g == 0; - yield; call SetH(0); yield; diff --git a/Test/og/t1.bpl.expect b/Test/og/t1.bpl.expect index 7877cfd1..41fb28d9 100644 --- a/Test/og/t1.bpl.expect +++ b/Test/og/t1.bpl.expect @@ -1,10 +1,10 @@ -t1.bpl(60,5): Error: Non-interference check failed +t1.bpl(65,5): Error: Non-interference check failed Execution trace: (0,0): og_init - t1.bpl(80,13): anon0 + t1.bpl(84,13): anon0 (0,0): anon05 (0,0): inline$SetG_1$0$Entry t1.bpl(34,21): inline$SetG_1$0$this_A - (0,0): inline$Impl_YieldChecker_A_1$0$L2 + (0,0): inline$Impl_YieldChecker_A_1$0$L1 -Boogie program verifier finished with 2 verified, 1 error +Boogie program verifier finished with 3 verified, 1 error diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl index f875d6e5..68e308d0 100644 --- a/Test/og/ticket.bpl +++ b/Test/og/ticket.bpl @@ -33,7 +33,7 @@ function {:inline} Inv2(tickets: [int]bool, ticket: int, lock: X): (bool) if (lock == nil) then tickets == RightOpen(ticket) else tickets == RightClosed(ticket) } -procedure Allocate({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X); +procedure {:yields} {:layer 2} Allocate({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X); ensures {:layer 1} {:layer 2} xl != nil; procedure {:yields} {:layer 2} main({:linear_in "tid"} xls':[X]bool) @@ -53,7 +53,7 @@ requires {:layer 2} xls' == mapconstbool(true); invariant {:layer 1} Inv1(T, t); invariant {:layer 2} Inv2(T, s, cs); { - call xls, tid := Allocate(xls); + par xls, tid := Allocate(xls) | Yield1() | Yield2(); async call Customer(tid); par Yield1() | Yield2(); } -- cgit v1.2.3 From 71fc5f5b32a5939ad488d6070a6acaf4d7cb443a Mon Sep 17 00:00:00 2001 From: qadeer Date: Fri, 26 Dec 2014 00:56:32 -0800 Subject: strengthened type checking cleaned up the generation of mover checks (based on example from Chris) added two examples from Chris to regressions --- Source/Concurrency/MoverCheck.cs | 67 ++++++++------- Source/Concurrency/OwickiGries.cs | 2 +- Source/Concurrency/TypeCheck.cs | 145 ++++++++++++++++++++++----------- Source/Concurrency/YieldTypeChecker.cs | 4 +- Test/og/DeviceCache.bpl | 10 ++- Test/og/DeviceCache.bpl.expect | 2 +- Test/og/FlanaganQadeer.bpl | 12 ++- Test/og/FlanaganQadeer.bpl.expect | 2 +- Test/og/Program4.bpl | 10 ++- Test/og/Program4.bpl.expect | 2 +- Test/og/Program5.bpl | 6 +- Test/og/akash.bpl | 28 +++---- Test/og/akash.bpl.expect | 2 +- Test/og/chris.bpl | 28 +++++++ Test/og/chris.bpl.expect | 2 + Test/og/chris2.bpl | 34 ++++++++ Test/og/chris2.bpl.expect | 18 ++++ Test/og/linear-set.bpl | 20 ++++- Test/og/linear-set.bpl.expect | 2 +- Test/og/linear-set2.bpl | 20 ++++- Test/og/linear-set2.bpl.expect | 2 +- Test/og/multiset.bpl | 8 +- Test/og/new1.bpl | 11 +-- Test/og/parallel2.bpl | 12 ++- Test/og/parallel2.bpl.expect | 2 +- Test/og/parallel4.bpl | 10 ++- Test/og/parallel4.bpl.expect | 4 +- Test/og/parallel5.bpl | 12 ++- Test/og/parallel5.bpl.expect | 2 +- Test/og/t1.bpl | 28 +++---- Test/og/t1.bpl.expect | 4 +- Test/og/ticket.bpl | 9 +- Test/og/ticket.bpl.expect | 2 +- Test/og/treiber-stack.bpl | 10 +-- 34 files changed, 375 insertions(+), 157 deletions(-) create mode 100644 Test/og/chris.bpl create mode 100644 Test/og/chris.bpl.expect create mode 100644 Test/og/chris2.bpl create mode 100644 Test/og/chris2.bpl.expect diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs index b10cd6cd..971e7271 100644 --- a/Source/Concurrency/MoverCheck.cs +++ b/Source/Concurrency/MoverCheck.cs @@ -30,52 +30,57 @@ namespace Microsoft.Boogie if (moverTypeChecker.procToActionInfo.Count == 0) return; + List sortedByCreatedLayerNum = new List(moverTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo)); + sortedByCreatedLayerNum.Sort((x, y) => { return (x.createdAtLayerNum == y.createdAtLayerNum) ? 0 : (x.createdAtLayerNum < y.createdAtLayerNum) ? -1 : 1; }); + List sortedByAvailableUptoLayerNum = new List(moverTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo)); + sortedByAvailableUptoLayerNum.Sort((x, y) => { return (x.availableUptoLayerNum == y.availableUptoLayerNum) ? 0 : (x.availableUptoLayerNum < y.availableUptoLayerNum) ? -1 : 1; }); + Dictionary> pools = new Dictionary>(); - foreach (ActionInfo action in moverTypeChecker.procToActionInfo.Values) + int indexIntoSortedByCreatedLayerNum = 0; + int indexIntoSortedByAvailableUptoLayerNum = 0; + HashSet currPool = new HashSet(); + while (indexIntoSortedByCreatedLayerNum < sortedByCreatedLayerNum.Count) { - AtomicActionInfo atomicAction = action as AtomicActionInfo; - if (atomicAction == null) continue; - foreach (int layerNum in moverTypeChecker.AllLayerNums) + var currLayerNum = sortedByCreatedLayerNum[indexIntoSortedByCreatedLayerNum].createdAtLayerNum; + pools[currLayerNum] = new HashSet(currPool); + while (indexIntoSortedByCreatedLayerNum < sortedByCreatedLayerNum.Count) { - if (action.createdAtLayerNum < layerNum && layerNum <= action.availableUptoLayerNum) - { - if (!pools.ContainsKey(layerNum)) - { - pools[layerNum] = new HashSet(); - } - pools[layerNum].Add(atomicAction); - } + var actionInfo = sortedByCreatedLayerNum[indexIntoSortedByCreatedLayerNum] as AtomicActionInfo; + if (actionInfo.createdAtLayerNum > currLayerNum) break; + pools[currLayerNum].Add(actionInfo); + indexIntoSortedByCreatedLayerNum++; } + while (indexIntoSortedByAvailableUptoLayerNum < sortedByAvailableUptoLayerNum.Count) + { + var actionInfo = sortedByAvailableUptoLayerNum[indexIntoSortedByAvailableUptoLayerNum] as AtomicActionInfo; + if (actionInfo.availableUptoLayerNum > currLayerNum) break; + pools[currLayerNum].Remove(actionInfo); + indexIntoSortedByAvailableUptoLayerNum++; + } + currPool = pools[currLayerNum]; } Program program = moverTypeChecker.program; MoverCheck moverChecking = new MoverCheck(linearTypeChecker, moverTypeChecker, decls); - foreach (int layerNum1 in pools.Keys) + foreach (int layerNum in pools.Keys) { - foreach (AtomicActionInfo first in pools[layerNum1]) + foreach (AtomicActionInfo first in pools[layerNum]) { Debug.Assert(first.moverType != MoverType.Top); if (first.moverType == MoverType.Atomic) continue; - foreach (int layerNum2 in pools.Keys) + foreach (AtomicActionInfo second in pools[layerNum]) { - if (layerNum2 < layerNum1) continue; - foreach (AtomicActionInfo second in pools[layerNum2]) + if (first.IsRightMover) + { + moverChecking.CreateCommutativityChecker(program, first, second); + moverChecking.CreateGatePreservationChecker(program, second, first); + } + if (first.IsLeftMover) { - if (second.createdAtLayerNum < layerNum1) - { - if (first.IsRightMover) - { - moverChecking.CreateCommutativityChecker(program, first, second); - moverChecking.CreateGatePreservationChecker(program, second, first); - } - if (first.IsLeftMover) - { - moverChecking.CreateCommutativityChecker(program, second, first); - moverChecking.CreateGatePreservationChecker(program, first, second); - moverChecking.CreateFailurePreservationChecker(program, second, first); - } - } + moverChecking.CreateCommutativityChecker(program, second, first); + moverChecking.CreateGatePreservationChecker(program, first, second); + moverChecking.CreateFailurePreservationChecker(program, second, first); } } } diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs index 8865b69e..dbd1dcbd 100644 --- a/Source/Concurrency/OwickiGries.cs +++ b/Source/Concurrency/OwickiGries.cs @@ -1160,7 +1160,7 @@ namespace Microsoft.Boogie public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List decls) { Program program = linearTypeChecker.program; - foreach (int layerNum in moverTypeChecker.AllLayerNums.Except(new int[] { 0 })) + foreach (int layerNum in moverTypeChecker.AllCreatedLayerNums.Except(new int[] { moverTypeChecker.leastUnimplementedLayerNum })) { if (CommandLineOptions.Clo.TrustLayersDownto <= layerNum || layerNum <= CommandLineOptions.Clo.TrustLayersUpto) continue; diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs index 8eb93e09..13356aff 100644 --- a/Source/Concurrency/TypeCheck.cs +++ b/Source/Concurrency/TypeCheck.cs @@ -22,12 +22,14 @@ namespace Microsoft.Boogie public Procedure proc; public int createdAtLayerNum; public int availableUptoLayerNum; + public bool hasImplementation; public ActionInfo(Procedure proc, int createdAtLayerNum, int availableUptoLayerNum) { this.proc = proc; this.createdAtLayerNum = createdAtLayerNum; this.availableUptoLayerNum = availableUptoLayerNum; + this.hasImplementation = false; } public virtual bool IsRightMover @@ -226,6 +228,7 @@ namespace Microsoft.Boogie int maxLayerNum; public Dictionary> absyToLayerNums; HashSet auxVars; + public int leastUnimplementedLayerNum; private static List FindLayers(QKeyValue kv) { @@ -260,20 +263,58 @@ namespace Microsoft.Boogie return MoverType.Top; } - private HashSet allLayerNums; - public IEnumerable AllLayerNums + public MoverTypeChecker(Program program) + { + this.auxVars = new HashSet(); + this.absyToLayerNums = new Dictionary>(); + this.globalVarToSharedVarInfo = new Dictionary(); + this.procToActionInfo = new Dictionary(); + this.errorCount = 0; + this.checkingContext = new CheckingContext(null); + this.program = program; + this.enclosingProc = null; + this.enclosingImpl = null; + this.canAccessSharedVars = false; + this.canAccessAuxVars = false; + this.minLayerNum = int.MaxValue; + this.maxLayerNum = -1; + this.leastUnimplementedLayerNum = int.MaxValue; + foreach (var g in program.GlobalVariables) + { + List layerNums = FindLayers(g.Attributes); + if (layerNums.Count == 0) + { + // Cannot access atomic actions + } + else if (layerNums.Count == 1) + { + this.globalVarToSharedVarInfo[g] = new SharedVariableInfo(layerNums[0], int.MaxValue); + } + else if (layerNums.Count == 2) + { + this.globalVarToSharedVarInfo[g] = new SharedVariableInfo(layerNums[0], layerNums[1]); + } + else + { + Error(g, "Too many layer numbers"); + } + } + } + + private HashSet allCreatedLayerNums; + public IEnumerable AllCreatedLayerNums { get { - if (allLayerNums == null) + if (allCreatedLayerNums == null) { - allLayerNums = new HashSet(); + allCreatedLayerNums = new HashSet(); foreach (ActionInfo actionInfo in procToActionInfo.Values) { - allLayerNums.Add(actionInfo.createdAtLayerNum); + allCreatedLayerNums.Add(actionInfo.createdAtLayerNum); } } - return allLayerNums; + return allCreatedLayerNums; } } @@ -300,6 +341,11 @@ namespace Microsoft.Boogie Error(proc, "Incorrect number of layers"); continue; } + if (availableUptoLayerNum <= createdAtLayerNum) + { + Error(proc, "Creation layer number must be less than the available upto layer number"); + continue; + } foreach (Ensures e in proc.Ensures) { MoverType moverType = GetMoverType(e); @@ -323,68 +369,69 @@ namespace Microsoft.Boogie enclosingImpl = null; base.VisitEnsures(e); canAccessSharedVars = false; - if (maxLayerNum <= createdAtLayerNum && availableUptoLayerNum <= minLayerNum) + if (maxLayerNum > createdAtLayerNum) { - // ok + Error(e, "A variable being accessed is introduced after this action is created"); } - else + else if (availableUptoLayerNum > minLayerNum) { Error(e, "A variable being accessed is hidden before this action becomes unavailable"); } - - procToActionInfo[proc] = new AtomicActionInfo(proc, e, moverType, createdAtLayerNum, availableUptoLayerNum); + else + { + procToActionInfo[proc] = new AtomicActionInfo(proc, e, moverType, createdAtLayerNum, availableUptoLayerNum); + } } + if (errorCount > 0) continue; if (!procToActionInfo.ContainsKey(proc)) { procToActionInfo[proc] = new ActionInfo(proc, createdAtLayerNum, availableUptoLayerNum); } } if (errorCount > 0) return; - this.VisitProgram(program); - if (errorCount > 0) return; - YieldTypeChecker.PerformYieldSafeCheck(this); - } - - public IEnumerable SharedVariables - { - get { return this.globalVarToSharedVarInfo.Keys; } - } - - public MoverTypeChecker(Program program) - { - this.auxVars = new HashSet(); - this.absyToLayerNums = new Dictionary>(); - this.globalVarToSharedVarInfo = new Dictionary(); - this.procToActionInfo = new Dictionary(); - this.errorCount = 0; - this.checkingContext = new CheckingContext(null); - this.program = program; - this.enclosingProc = null; - this.enclosingImpl = null; - this.canAccessSharedVars = false; - this.canAccessAuxVars = false; - this.minLayerNum = int.MaxValue; - this.maxLayerNum = -1; - foreach (var g in program.GlobalVariables) + foreach (var impl in program.Implementations) { - List layerNums = FindLayers(g.Attributes); - if (layerNums.Count == 0) + if (!procToActionInfo.ContainsKey(impl.Proc)) continue; + procToActionInfo[impl.Proc].hasImplementation = true; + } + foreach (var proc in procToActionInfo.Keys) + { + ActionInfo actionInfo = procToActionInfo[proc]; + if (actionInfo.hasImplementation) continue; + if (leastUnimplementedLayerNum == int.MaxValue) { - // Cannot access atomic actions + leastUnimplementedLayerNum = actionInfo.createdAtLayerNum; } - else if (layerNums.Count == 1) + else if (leastUnimplementedLayerNum == actionInfo.createdAtLayerNum) { - this.globalVarToSharedVarInfo[g] = new SharedVariableInfo(layerNums[0], int.MaxValue); + // do nothing } - else if (layerNums.Count == 2) + else { - this.globalVarToSharedVarInfo[g] = new SharedVariableInfo(layerNums[0], layerNums[1]); + Error(proc, "All unimplemented atomic actions must be created at the same layer"); } - else + } + foreach (var g in this.globalVarToSharedVarInfo.Keys) + { + var info = globalVarToSharedVarInfo[g]; + if (!this.AllCreatedLayerNums.Contains(info.introLayerNum)) { - Error(g, "Too many layer numbers"); + Error(g, "Variable must be introduced with creation of some atomic action"); + } + if (info.hideLayerNum != int.MaxValue && !this.AllCreatedLayerNums.Contains(info.hideLayerNum)) + { + Error(g, "Variable must be hidden with creation of some atomic action"); } } + if (errorCount > 0) return; + this.VisitProgram(program); + if (errorCount > 0) return; + YieldTypeChecker.PerformYieldSafeCheck(this); + } + + public IEnumerable SharedVariables + { + get { return this.globalVarToSharedVarInfo.Keys; } } public override Implementation VisitImplementation(Implementation node) @@ -602,7 +649,11 @@ namespace Microsoft.Boogie absyToLayerNums[node] = new HashSet(); foreach (int layerNum in attrs) { - if (layerNum > enclosingProcLayerNum) + if (layerNum == leastUnimplementedLayerNum || !AllCreatedLayerNums.Contains(layerNum)) + { + Error(node, "Illegal layer number"); + } + else if (layerNum > enclosingProcLayerNum) { Error(node, "The layer cannot be greater than the layer of enclosing procedure"); } diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs index 8e844ede..95884626 100644 --- a/Source/Concurrency/YieldTypeChecker.cs +++ b/Source/Concurrency/YieldTypeChecker.cs @@ -136,12 +136,12 @@ namespace Microsoft.Boogie { foreach (var impl in moverTypeChecker.program.Implementations) { - if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || moverTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum == 0) continue; + if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc)) continue; impl.PruneUnreachableBlocks(); Graph implGraph = Program.GraphFromImpl(impl); implGraph.ComputeLoops(); int specLayerNum = moverTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum; - foreach (int layerNum in moverTypeChecker.AllLayerNums) + foreach (int layerNum in moverTypeChecker.AllCreatedLayerNums.Except(new int[] { moverTypeChecker.leastUnimplementedLayerNum })) { if (layerNum > specLayerNum) continue; YieldTypeChecker executor = new YieldTypeChecker(moverTypeChecker, impl, layerNum, implGraph.Headers); diff --git a/Test/og/DeviceCache.bpl b/Test/og/DeviceCache.bpl index b204d9de..f439b607 100644 --- a/Test/og/DeviceCache.bpl +++ b/Test/og/DeviceCache.bpl @@ -48,8 +48,13 @@ ensures {:layer 1} Inv(ghostLock, currsize, newsize) && ghostLock == tid && old( assert {:layer 1} Inv(ghostLock, currsize, newsize) && tid != nil && ghostLock == tid && old(currsize) == currsize && old(newsize) == newsize; } -procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xl: X); +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xl: X) ensures {:layer 1} xl != nil; +{ + yield; + call xl := AllocateLow(); + yield; +} procedure {:yields} {:layer 1} main({:linear_in "tid"} xls: [X]bool) requires {:layer 1} xls == mapconstbool(true); @@ -200,3 +205,6 @@ ensures {:right} |{ A: assert tid != nil; assume lock == nil; lock := tid; retur procedure {:yields} {:layer 0,1} release({:linear "tid"} tid: X); ensures {:left} |{ A: assert tid != nil; assert lock == tid; lock := nil; return true; }|; + +procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: X); +ensures {:atomic} |{ A: assume tid != nil; return true; }|; diff --git a/Test/og/DeviceCache.bpl.expect b/Test/og/DeviceCache.bpl.expect index 8c696418..9ec7a92d 100644 --- a/Test/og/DeviceCache.bpl.expect +++ b/Test/og/DeviceCache.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 29 verified, 0 errors +Boogie program verifier finished with 30 verified, 0 errors diff --git a/Test/og/FlanaganQadeer.bpl b/Test/og/FlanaganQadeer.bpl index a912a89a..7345b5b2 100644 --- a/Test/og/FlanaganQadeer.bpl +++ b/Test/og/FlanaganQadeer.bpl @@ -11,8 +11,13 @@ function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool MapConstBool(false)[x := true] } -procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: X); -ensures {:layer 1} xls != nil; +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xl: X) +ensures {:layer 1} xl != nil; +{ + yield; + call xl := AllocateLow(); + yield; +} procedure {:yields} {:layer 1} main() { @@ -38,6 +43,9 @@ ensures {:atomic} |{A: l := nil; return true; }|; procedure {:yields} {:layer 0,1} Set(val: int); ensures {:atomic} |{A: x := val; return true; }|; +procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xl: X); +ensures {:atomic} |{ A: assume xl != nil; return true; }|; + procedure {:yields} {:layer 1} foo({:linear_in "tid"} tid': X, val: int) requires {:layer 1} tid' != nil; { diff --git a/Test/og/FlanaganQadeer.bpl.expect b/Test/og/FlanaganQadeer.bpl.expect index 5b2909f1..fef5ddc0 100644 --- a/Test/og/FlanaganQadeer.bpl.expect +++ b/Test/og/FlanaganQadeer.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 3 verified, 0 errors +Boogie program verifier finished with 4 verified, 0 errors diff --git a/Test/og/Program4.bpl b/Test/og/Program4.bpl index b8406f2e..7767e179 100644 --- a/Test/og/Program4.bpl +++ b/Test/og/Program4.bpl @@ -15,7 +15,12 @@ function {:inline} {:linear "tid"} TidSetCollector(x: [Tid]bool) : [Tid]bool var {:layer 0,1} a:[Tid]int; -procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid:Tid); +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: Tid) +{ + yield; + call tid := AllocateLow(); + yield; +} procedure {:yields} {:layer 1} main() { var {:linear "tid"} tid:Tid; @@ -55,3 +60,6 @@ ensures {:atomic} |{A: a[tid] := val; return true; }|; + +procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: Tid); +ensures {:atomic} |{ A: return true; }|; diff --git a/Test/og/Program4.bpl.expect b/Test/og/Program4.bpl.expect index 3de74d3e..5b2909f1 100644 --- a/Test/og/Program4.bpl.expect +++ b/Test/og/Program4.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 2 verified, 0 errors +Boogie program verifier finished with 3 verified, 0 errors diff --git a/Test/og/Program5.bpl b/Test/og/Program5.bpl index af87eac5..55e4219f 100644 --- a/Test/og/Program5.bpl +++ b/Test/og/Program5.bpl @@ -5,8 +5,8 @@ const unique nil: Tid; function {:builtin "MapConst"} MapConstBool(bool): [Tid]bool; function {:builtin "MapOr"} MapOr([Tid]bool, [Tid]bool) : [Tid]bool; -var {:layer 0,3} Color:int; -var {:layer 0,3} lock:Tid; +var {:layer 0} Color:int; +var {:layer 0} lock:Tid; function {:inline} {:linear "tid"} TidCollector(x: Tid) : [Tid]bool { @@ -72,6 +72,6 @@ procedure {:yields} {:layer 0,1} SetColorLocked({:linear "tid"} tid:Tid, newCol: procedure {:yields} {:layer 0,1} GetColorLocked({:linear "tid"} tid:Tid) returns (col:int); ensures {:both} |{A: assert tid != nil; assert lock == tid; col := Color; return true;}|; -procedure {:yields} {:layer 1,2} GetColorNoLock() returns (col:int); +procedure {:yields} {:layer 0,2} GetColorNoLock() returns (col:int); ensures {:atomic} |{A: col := Color; return true;}|; diff --git a/Test/og/akash.bpl b/Test/og/akash.bpl index cfbeaf3a..c826b810 100644 --- a/Test/og/akash.bpl +++ b/Test/og/akash.bpl @@ -18,15 +18,6 @@ function {:inline} {:linear "2"} SetCollector2(x: [int]bool) : [int]bool x } -procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: int); -ensures {:layer 1} xls != 0; - -procedure {:yields} {:layer 1} Allocate_1() returns ({:linear "1"} xls: [int]bool); -ensures {:layer 1} xls == mapconstbool(true); - -procedure {:yields} {:layer 1} Allocate_2() returns ({:linear "2"} xls: [int]bool); -ensures {:layer 1} xls == mapconstbool(true); - var {:layer 0,1} g: int; var {:layer 0,1} h: int; @@ -36,14 +27,23 @@ ensures {:atomic} |{A: g := val; return true; }|; procedure {:yields} {:layer 0,1} SetH(val:int); ensures {:atomic} |{A: h := val; return true; }|; -procedure {:yields} {:layer 1} A({:linear_in "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int) +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xl: int) +ensures {:layer 1} xl != 0; +{ + yield; + call xl := AllocateLow(); + yield; +} + +procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xls: int); +ensures {:atomic} |{ A: assume xls != 0; return true; }|; + +procedure {:yields} {:layer 1} A({:linear_in "tid"} tid_in: int, {:linear_in "1"} x: [int]bool, {:linear_in "2"} y: [int]bool) returns ({:linear "tid"} tid_out: int) +requires {:layer 1} x == mapconstbool(true); +requires {:layer 1} y == mapconstbool(true); { - var {:linear "1"} x: [int]bool; - var {:linear "2"} y: [int]bool; var {:linear "tid"} tid_child: int; tid_out := tid_in; - call x := Allocate_1(); - call y := Allocate_2(); yield; call SetG(0); diff --git a/Test/og/akash.bpl.expect b/Test/og/akash.bpl.expect index 5b2909f1..fef5ddc0 100644 --- a/Test/og/akash.bpl.expect +++ b/Test/og/akash.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 3 verified, 0 errors +Boogie program verifier finished with 4 verified, 0 errors diff --git a/Test/og/chris.bpl b/Test/og/chris.bpl new file mode 100644 index 00000000..b54292ef --- /dev/null +++ b/Test/og/chris.bpl @@ -0,0 +1,28 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var{:layer 1} x:int; + +procedure{:yields}{:layer 2} Havoc() + ensures{:atomic} |{ A: return true; }|; +{ + yield; +} + +procedure{:yields}{:layer 1} Recover() + ensures{:atomic} |{ A: assert x == 5; return true; }|; +{ + yield; +} + +procedure{:yields}{:layer 3} P() + ensures{:atomic} |{ A: return true; }|; + requires{:layer 2,3} x == 5; + ensures {:layer 2,3} x == 5; +{ + + yield; assert{:layer 2,3} x == 5; + call Havoc(); + yield; assert{:layer 3} x == 5; + call Recover(); + yield; assert{:layer 2,3} x == 5; +} diff --git a/Test/og/chris.bpl.expect b/Test/og/chris.bpl.expect new file mode 100644 index 00000000..be6b95ba --- /dev/null +++ b/Test/og/chris.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 6 verified, 0 errors diff --git a/Test/og/chris2.bpl b/Test/og/chris2.bpl new file mode 100644 index 00000000..73f112ed --- /dev/null +++ b/Test/og/chris2.bpl @@ -0,0 +1,34 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var{:layer 20} x:int; + +procedure{:yields}{:layer 20,25} p_gt1_lower(); + ensures{:both} + |{ + A: + x := x + 1; + return true; + }|; + +procedure{:yields}{:layer 25,40} p_gt1() + ensures{:both} + |{ + A: + x := x + 1; + return true; + }|; +{ + yield; + call p_gt1_lower(); + yield; +} + +procedure{:yields}{:layer 20,40} p_gt2(); + ensures{:both} + |{ + A: + assert x == 0; + return true; + }|; + + diff --git a/Test/og/chris2.bpl.expect b/Test/og/chris2.bpl.expect new file mode 100644 index 00000000..2bf339f7 --- /dev/null +++ b/Test/og/chris2.bpl.expect @@ -0,0 +1,18 @@ +(0,0): Error BP5003: A postcondition might not hold on this return path. +chris2.bpl(30,5): Related location: Gate not preserved by p_gt1_lower +Execution trace: + (0,0): this_A +(0,0): Error BP5003: A postcondition might not hold on this return path. +(0,0): Related location: Gate failure of p_gt2 not preserved by p_gt1_lower +Execution trace: + (0,0): this_A +(0,0): Error BP5003: A postcondition might not hold on this return path. +chris2.bpl(30,5): Related location: Gate not preserved by p_gt1 +Execution trace: + (0,0): this_A +(0,0): Error BP5003: A postcondition might not hold on this return path. +(0,0): Related location: Gate failure of p_gt2 not preserved by p_gt1 +Execution trace: + (0,0): this_A + +Boogie program verifier finished with 1 verified, 4 errors diff --git a/Test/og/linear-set.bpl b/Test/og/linear-set.bpl index 8752d402..e481291a 100644 --- a/Test/og/linear-set.bpl +++ b/Test/og/linear-set.bpl @@ -23,10 +23,21 @@ function {:inline} {:linear "x"} XCollector(xs: [X]bool) : [X]bool var {:layer 0,1} x: int; var {:layer 0,1} l: [X]bool; -procedure {:yields} {:layer 1} Split({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool); + +procedure {:yields} {:layer 1} Split({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool) ensures {:layer 1} xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None(); +{ + yield; + call xls1, xls2 := SplitLow(xls); + yield; +} -procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: [X]bool); +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: [X]bool) +{ + yield; + call xls := AllocateLow(); + yield; +} procedure {:yields} {:layer 0,1} Set(v: int); ensures {:atomic} |{A: x := v; return true; }|; @@ -37,6 +48,11 @@ ensures {:atomic} |{A: assume l == None(); l := tidls; return true; }|; procedure {:yields} {:layer 0,1} Unlock(); ensures {:atomic} |{A: l := None(); return true; }|; +procedure {:yields} {:layer 0,1} SplitLow({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool); +ensures {:atomic} |{ A: assume xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None(); return true; }|; + +procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xls: [X]bool); +ensures {:atomic} |{ A: return true; }|; procedure {:yields} {:layer 1} main({:linear_in "tid"} tidls': [X]bool, {:linear_in "x"} xls': [X]bool) requires {:layer 1} tidls' != None() && xls' == All(); diff --git a/Test/og/linear-set.bpl.expect b/Test/og/linear-set.bpl.expect index 3de74d3e..fef5ddc0 100644 --- a/Test/og/linear-set.bpl.expect +++ b/Test/og/linear-set.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 2 verified, 0 errors +Boogie program verifier finished with 4 verified, 0 errors diff --git a/Test/og/linear-set2.bpl b/Test/og/linear-set2.bpl index a3b84702..24d8a13a 100644 --- a/Test/og/linear-set2.bpl +++ b/Test/og/linear-set2.bpl @@ -24,11 +24,21 @@ var {:layer 0,1} x: int; var {:layer 0,1} l: X; const nil: X; -procedure {:yields} {:layer 1} Split({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool); +procedure {:yields} {:layer 1} Split({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool) ensures {:layer 1} xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None(); +{ + yield; + call xls1, xls2 := SplitLow(xls); + yield; +} -procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: X); +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: X) ensures {:layer 1} xls != nil; +{ + yield; + call xls := AllocateLow(); + yield; +} procedure {:yields} {:layer 0,1} Set(v: int); ensures {:atomic} |{A: x := v; return true; }|; @@ -39,6 +49,12 @@ ensures {:atomic} |{A: assume l == nil; l := tidls; return true; }|; procedure {:yields} {:layer 0,1} Unlock(); ensures {:atomic} |{A: l := nil; return true; }|; +procedure {:yields} {:layer 0,1} SplitLow({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool); +ensures {:atomic} |{ A: assume xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None(); return true; }|; + +procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xls: X); +ensures {:atomic} |{ A: assume xls != nil; return true; }|; + procedure {:yields} {:layer 1} main({:linear_in "tid"} tidls': X, {:linear_in "x"} xls': [X]bool) requires {:layer 1} tidls' != nil && xls' == All(); { diff --git a/Test/og/linear-set2.bpl.expect b/Test/og/linear-set2.bpl.expect index 3de74d3e..fef5ddc0 100644 --- a/Test/og/linear-set2.bpl.expect +++ b/Test/og/linear-set2.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 2 verified, 0 errors +Boogie program verifier finished with 4 verified, 0 errors diff --git a/Test/og/multiset.bpl b/Test/og/multiset.bpl index 308e4b8b..7fb0a081 100644 --- a/Test/og/multiset.bpl +++ b/Test/og/multiset.bpl @@ -63,7 +63,7 @@ ensures {:both} |{ A: }|; -procedure {:yields} {:layer 0} setEltToNull(j : int, {:linear "tid"} tid: X); +procedure {:yields} {:layer 0,2} setEltToNull(j : int, {:linear "tid"} tid: X); ensures {:left} |{ A: assert owner[j] == tid; assert 0 <= j && j < max; @@ -75,7 +75,7 @@ ensures {:left} |{ A: return true; }|; -procedure {:yields} {:layer 0} setValid(j : int, {:linear "tid"} tid: X); +procedure {:yields} {:layer 0,2} setValid(j : int, {:linear "tid"} tid: X); ensures {:both} |{ A: assert 0 <= j && j < max; assert lock[j] == tid; @@ -86,7 +86,7 @@ ensures {:both} |{ A: return true; }|; -procedure {:yields} {:layer 0} isEltThereAndValid(j : int, x : int, {:linear "tid"} tid: X) returns (fnd:bool); +procedure {:yields} {:layer 0,2} isEltThereAndValid(j : int, x : int, {:linear "tid"} tid: X) returns (fnd:bool); ensures {:both} |{ A: assert 0 <= j && j < max; assert lock[j] == tid; @@ -95,7 +95,7 @@ ensures {:both} |{ A: return true; }|; -procedure {:yields} {:layer 1} FindSlot(x : int, {:linear "tid"} tid: X) returns (r : int) +procedure {:yields} {:layer 1,2} FindSlot(x : int, {:linear "tid"} tid: X) returns (r : int) requires {:layer 1} Inv(valid, elt, owner) && x != null && tid != nil && tid != done; ensures {:layer 1} Inv(valid, elt, owner); ensures {:right} |{ A: assert tid != nil && tid != done; diff --git a/Test/og/new1.bpl b/Test/og/new1.bpl index 74b738d6..b80b6315 100644 --- a/Test/og/new1.bpl +++ b/Test/og/new1.bpl @@ -9,10 +9,6 @@ function {:inline} {:linear "Perm"} SetCollectorPerm(x: [int]bool) : [int]bool x } -procedure {:yields} {:layer 1} Allocate_Perm({:linear_in "Perm"} Permissions: [int]bool) returns ({:linear "Perm"} xls: [int]bool); -requires {:layer 1} Permissions == mapconstbool(true); -ensures {:layer 1} xls == mapconstbool(true); - procedure {:yields} {:layer 1} PB({:linear_in "Perm"} permVar_in:[int]bool) requires {:layer 1} permVar_in[0] && g == 0; { @@ -31,14 +27,11 @@ requires {:layer 1} permVar_in[0] && g == 0; } procedure {:yields} {:layer 1} Main({:linear_in "Perm"} Permissions: [int]bool) -requires {:layer 0,1} Permissions == mapconstbool(true); +requires {:layer 1} Permissions == mapconstbool(true); { - var {:linear "Perm"} permVar_out: [int]bool; - - call permVar_out := Allocate_Perm(Permissions); yield; call SetG(0); - async call PB(permVar_out); + async call PB(Permissions); yield; } diff --git a/Test/og/parallel2.bpl b/Test/og/parallel2.bpl index ad40ffa0..c28edf2b 100644 --- a/Test/og/parallel2.bpl +++ b/Test/og/parallel2.bpl @@ -8,7 +8,12 @@ function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool MapConstBool(false)[x := true] } -procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: int); +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: int) +{ + yield; + call tid := AllocateLow(); + yield; +} procedure {:yields} {:layer 0,1} Write(idx: int, val: int); ensures {:atomic} |{A: a[idx] := val; return true; }|; @@ -48,4 +53,7 @@ ensures {:layer 1} old(a)[i] == a[i]; { yield; assert {:layer 1} old(a)[i] == a[i]; -} \ No newline at end of file +} + +procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: int); +ensures {:atomic} |{ A: return true; }|; diff --git a/Test/og/parallel2.bpl.expect b/Test/og/parallel2.bpl.expect index fef5ddc0..05d394c7 100644 --- a/Test/og/parallel2.bpl.expect +++ b/Test/og/parallel2.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 4 verified, 0 errors +Boogie program verifier finished with 5 verified, 0 errors diff --git a/Test/og/parallel4.bpl b/Test/og/parallel4.bpl index 5340c4c8..f06ff4b8 100644 --- a/Test/og/parallel4.bpl +++ b/Test/og/parallel4.bpl @@ -2,7 +2,12 @@ // RUN: %diff "%s.expect" "%t" var {:layer 0,1} a:int; -procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: int); +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: int) +{ + yield; + call tid := AllocateLow(); + yield; +} function {:builtin "MapConst"} MapConstBool(bool) : [int]bool; function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool @@ -35,3 +40,6 @@ procedure {:yields} {:layer 1} Yield() { yield; } + +procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: int); +ensures {:atomic} |{ A: return true; }|; diff --git a/Test/og/parallel4.bpl.expect b/Test/og/parallel4.bpl.expect index 0bef8d9e..eaead450 100644 --- a/Test/og/parallel4.bpl.expect +++ b/Test/og/parallel4.bpl.expect @@ -1,6 +1,6 @@ -parallel4.bpl(26,3): Error BP5001: This assertion might not hold. +parallel4.bpl(31,3): Error BP5001: This assertion might not hold. Execution trace: (0,0): og_init (0,0): anon01 -Boogie program verifier finished with 2 verified, 1 error +Boogie program verifier finished with 3 verified, 1 error diff --git a/Test/og/parallel5.bpl b/Test/og/parallel5.bpl index ea35a3b2..87afc888 100644 --- a/Test/og/parallel5.bpl +++ b/Test/og/parallel5.bpl @@ -2,7 +2,12 @@ // RUN: %diff "%s.expect" "%t" var {:layer 0,1} a:[int]int; -procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: int); +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: int) +{ + yield; + call tid := AllocateLow(); + yield; +} function {:builtin "MapConst"} MapConstBool(bool) : [int]bool; function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool @@ -48,4 +53,7 @@ ensures {:layer 1} old(a)[i] == a[i]; { yield; assert {:layer 1} old(a)[i] == a[i]; -} \ No newline at end of file +} + +procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: int); +ensures {:atomic} |{ A: return true; }|; diff --git a/Test/og/parallel5.bpl.expect b/Test/og/parallel5.bpl.expect index fef5ddc0..05d394c7 100644 --- a/Test/og/parallel5.bpl.expect +++ b/Test/og/parallel5.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 4 verified, 0 errors +Boogie program verifier finished with 5 verified, 0 errors diff --git a/Test/og/t1.bpl b/Test/og/t1.bpl index cb3dd138..675b3842 100644 --- a/Test/og/t1.bpl +++ b/Test/og/t1.bpl @@ -18,15 +18,6 @@ function {:inline} {:linear "2"} SetCollector2(x: [int]bool) : [int]bool x } -procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: int); -ensures {:layer 1} xls != 0; - -procedure {:yields} {:layer 1} Allocate_1() returns ({:linear "1"} xls: [int]bool); -ensures {:layer 1} xls == mapconstbool(true); - -procedure {:yields} {:layer 1} Allocate_2() returns ({:linear "2"} xls: [int]bool); -ensures {:layer 1} xls == mapconstbool(true); - var {:layer 0,1} g: int; var {:layer 0,1} h: int; @@ -44,14 +35,23 @@ ensures {:layer 1} x == mapconstbool(true) && g == 0; assert {:layer 1} x == mapconstbool(true) && g == 0; } -procedure {:yields} {:layer 1} A({:linear_in "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int) +procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xl: int) +ensures {:layer 1} xl != 0; +{ + yield; + call xl := AllocateLow(); + yield; +} + +procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xls: int); +ensures {:atomic} |{ A: assume xls != 0; return true; }|; + +procedure {:yields} {:layer 1} A({:linear_in "tid"} tid_in: int, {:linear_in "1"} x: [int]bool, {:linear_in "2"} y: [int]bool) returns ({:linear "tid"} tid_out: int) +requires {:layer 1} x == mapconstbool(true); +requires {:layer 1} y == mapconstbool(true); { - var {:linear "1"} x: [int]bool; - var {:linear "2"} y: [int]bool; var {:linear "tid"} tid_child: int; tid_out := tid_in; - call x := Allocate_1(); - call y := Allocate_2(); yield; call SetG(0); diff --git a/Test/og/t1.bpl.expect b/Test/og/t1.bpl.expect index 41fb28d9..f0195727 100644 --- a/Test/og/t1.bpl.expect +++ b/Test/og/t1.bpl.expect @@ -4,7 +4,7 @@ Execution trace: t1.bpl(84,13): anon0 (0,0): anon05 (0,0): inline$SetG_1$0$Entry - t1.bpl(34,21): inline$SetG_1$0$this_A + t1.bpl(25,21): inline$SetG_1$0$this_A (0,0): inline$Impl_YieldChecker_A_1$0$L1 -Boogie program verifier finished with 3 verified, 1 error +Boogie program verifier finished with 4 verified, 1 error diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl index 68e308d0..91863e1a 100644 --- a/Test/og/ticket.bpl +++ b/Test/og/ticket.bpl @@ -33,8 +33,13 @@ function {:inline} Inv2(tickets: [int]bool, ticket: int, lock: X): (bool) if (lock == nil) then tickets == RightOpen(ticket) else tickets == RightClosed(ticket) } -procedure {:yields} {:layer 2} Allocate({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X); +procedure {:yields} {:layer 2} Allocate({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X) ensures {:layer 1} {:layer 2} xl != nil; +{ + yield; + call xls, xl := AllocateLow(xls'); + yield; +} procedure {:yields} {:layer 2} main({:linear_in "tid"} xls':[X]bool) requires {:layer 2} xls' == mapconstbool(true); @@ -138,3 +143,5 @@ ensures {:atomic} |{ A: assume m <= s; cs := tid; return true; }|; procedure {:yields} {:layer 0,2} Leave({:linear "tid"} tid: X); ensures {:atomic} |{ A: s := s + 1; cs := nil; return true; }|; +procedure {:yields} {:layer 0,2} AllocateLow({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X); +ensures {:atomic} |{ A: assume xl != nil; return true; }|; diff --git a/Test/og/ticket.bpl.expect b/Test/og/ticket.bpl.expect index f7c1129d..28c26eab 100644 --- a/Test/og/ticket.bpl.expect +++ b/Test/og/ticket.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 14 verified, 0 errors +Boogie program verifier finished with 16 verified, 0 errors diff --git a/Test/og/treiber-stack.bpl b/Test/og/treiber-stack.bpl index 9a612eb2..8622dd9e 100644 --- a/Test/og/treiber-stack.bpl +++ b/Test/og/treiber-stack.bpl @@ -16,24 +16,24 @@ axiom (forall x: lmap, i: Node, v: Node :: dom(Add(x, i, v)) == dom(x)[i:=true] 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)); -procedure {:yields} {:layer 0} ReadTopOfStack() returns (v:Node); +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} Load(i:Node) returns (v:Node); +procedure {:yields} {:layer 0,1} Load(i:Node) returns (v:Node); ensures {:right} |{ A: assert dom(Stack)[i] || dom(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} 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:Node, v:Node) 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} 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: Node, newVal: Node, {: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} TransferFromStack(oldVal: Node, newVal: Node) returns (r: bool); +procedure {:yields} {:layer 0,1} TransferFromStack(oldVal: Node, newVal: Node) 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; C: assume oldVal != TopOfStack; r := false; return true; }|; -- cgit v1.2.3 From d41a7518de7fd135caf752824670723d06332298 Mon Sep 17 00:00:00 2001 From: wuestholz Date: Fri, 26 Dec 2014 10:41:10 +0100 Subject: Fixed a postcondition. --- Source/VCGeneration/VC.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index b989c029..8a549e9d 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1156,7 +1156,7 @@ namespace VC { public static List FindManualSplits(Implementation/*!*/ impl, Dictionary/*!*/ gotoCmdOrigins, VCGen/*!*/ par) { Contract.Requires(impl != null); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); + Contract.Ensures(Contract.Result>() == null || cce.NonNullElements(Contract.Result>())); var splitPoints = new Dictionary(); foreach (var b in impl.Blocks) { -- cgit v1.2.3 From 94c192b6e706fd296bae7d08fecab8dbc9592172 Mon Sep 17 00:00:00 2001 From: wuestholz Date: Fri, 26 Dec 2014 11:01:41 +0100 Subject: Minor change --- Source/ExecutionEngine/ExecutionEngine.cs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 92be2e0a..8187db01 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -536,11 +536,11 @@ namespace Microsoft.Boogie } } - public static List> LookForSnapshots(List fileNames) + public static IList> LookForSnapshots(IList fileNames) { Contract.Requires(fileNames != null); - var result = new List>(); + var result = new List>(); for (int version = 0; true; version++) { var nextSnapshot = new List(); -- cgit v1.2.3