diff options
Diffstat (limited to 'Test')
33 files changed, 291 insertions, 125 deletions
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..f439b607 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,21 @@ 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;
+{
+ yield;
+ call xl := AllocateLow();
+ yield;
+}
-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 +71,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 +179,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);
@@ -194,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 9e5be400..9ec7a92d 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 30 verified, 0 errors
diff --git a/Test/og/FlanaganQadeer.bpl b/Test/og/FlanaganQadeer.bpl index 04255cf2..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 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 0228adc9..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 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 744029f1..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 Allocate() returns ({:linear "tid"} xls: int);
-ensures {:layer 1} xls != 0;
-
-procedure Allocate_1() returns ({:linear "1"} xls: [int]bool);
-ensures {:layer 1} xls == mapconstbool(true);
-
-procedure 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 73849250..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 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 Allocate() returns ({:linear "tid"} xls: [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)
+{
+ 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 81d30521..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 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();
+{
+ yield;
+ call xls1, xls2 := SplitLow(xls);
+ yield;
+}
-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;
+{
+ 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 a6b50215..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 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} 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 4f2cbd5b..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 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 41d45b79..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 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 bed51241..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 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/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..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 Allocate() returns ({:linear "tid"} xls: int);
-ensures {:layer 1} xls != 0;
-
-procedure Allocate_1() returns ({:linear "1"} xls: [int]bool);
-ensures {:layer 1} xls == mapconstbool(true);
-
-procedure 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,30 +27,43 @@ 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} 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} 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);
- 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..f0195727 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
+ t1.bpl(25,21): inline$SetG_1$0$this_A
+ (0,0): inline$Impl_YieldChecker_A_1$0$L1
-Boogie program verifier finished with 2 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 f875d6e5..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 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);
@@ -53,7 +58,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();
}
@@ -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; }|;
|