changed type checking of yield procedures so that they can only call other yielding procedures

17 files changed, 75 insertions, 71 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..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();

     }