added parallel calls

12 files changed, 125 insertions, 39 deletions

diff --git a/Test/og/Answer b/Test/og/Answer
index 712ebfd8..15dd93bd 100644
--- a/Test/og/Answer
+++ b/Test/og/Answer
@@ -1,9 +1,9 @@
 

 -------------------- foo.bpl --------------------

-OwickiGriesDesugared.bpl(179,4): Error BP5001: This assertion might not hold.

+OwickiGriesDesugared.bpl(171,4): Error BP5001: This assertion might not hold.

 Execution trace:

     OwickiGriesDesugared.bpl(17,0): anon0

-    OwickiGriesDesugared.bpl(177,0): inline$YieldChecker_PC$0$L1

+    OwickiGriesDesugared.bpl(169,0): inline$YieldChecker_PC$0$L1

 

 Boogie program verifier finished with 3 verified, 1 error

 

@@ -23,6 +23,10 @@ Boogie program verifier finished with 2 verified, 2 errors
 

 Boogie program verifier finished with 2 verified, 0 errors

 

+-------------------- parallel1.bpl --------------------

+

+Boogie program verifier finished with 4 verified, 0 errors

+

 -------------------- linear-set.bpl --------------------

 

 Boogie program verifier finished with 2 verified, 0 errors

@@ -38,3 +42,7 @@ Boogie program verifier finished with 3 verified, 0 errors
 -------------------- DeviceCacheSimplified.bpl --------------------

 

 Boogie program verifier finished with 5 verified, 0 errors

+

+-------------------- parallel2.bpl --------------------

+

+Boogie program verifier finished with 4 verified, 0 errors

diff --git a/Test/og/DeviceCacheSimplified.bpl b/Test/og/DeviceCacheSimplified.bpl
index c89bd793..68387356 100644
--- a/Test/og/DeviceCacheSimplified.bpl
+++ b/Test/og/DeviceCacheSimplified.bpl
@@ -13,7 +13,8 @@ ensures old(currsize) <= currsize;
 ensures tid == tid';

 {

     assume tid == tid';

-    assert {:yield} Inv(ghostLock, currsize, newsize);

+    yield;

+    assert Inv(ghostLock, currsize, newsize);

     assert old(currsize) <= currsize;

     assert tid != nil;

 }

@@ -31,7 +32,8 @@ ensures currsize <= i;
 ensures newsize == old(newsize);

 {

     assume tid == tid';

-    assert {:yield} Inv(ghostLock, currsize, newsize);

+    yield;

+    assert Inv(ghostLock, currsize, newsize);

     assert old(currsize) <= currsize;

     assert tid != nil;

     assert ghostLock == tid;

@@ -140,6 +142,6 @@ requires currsize == 0 && newsize == 0 && ghostLock == nil && lock == nil;
     {

         havoc tid;

 	assume tid != nil;

-        call {:async} thread(tid);

+        async call thread(tid);

     }

 }
\ No newline at end of file
diff --git a/Test/og/FlanaganQadeer.bpl b/Test/og/FlanaganQadeer.bpl
index 8379925f..217a0401 100644
--- a/Test/og/FlanaganQadeer.bpl
+++ b/Test/og/FlanaganQadeer.bpl
@@ -13,7 +13,7 @@ procedure {:entrypoint} main()
     {

         havoc tid, val;

 	assume tid != nil;

-        call {:async} foo(tid, val);

+        async call foo(tid, val);

     }

 }

 

@@ -39,6 +39,7 @@ ensures tid == tid';
 ensures old(l) == tid ==> old(l) == l && old(x) == x;

 {

     assume tid == tid';

-    assert {:yield} tid != nil;

+    yield;

+    assert tid != nil;

     assert (old(l) == tid ==> old(l) == l && old(x) == x);

 }
\ No newline at end of file
diff --git a/Test/og/bar.bpl b/Test/og/bar.bpl
index cddc5338..8c4586d3 100644
--- a/Test/og/bar.bpl
+++ b/Test/og/bar.bpl
@@ -8,7 +8,8 @@ procedure PB()
 procedure PC()

   ensures g == old(g);

 {

-  assert{:yield} g == old(g);

+  yield;

+  assert g == old(g);

 }

 

 procedure PD()

@@ -22,8 +23,8 @@ procedure{:entrypoint} Main2()
 {

   while (true)

   {

-    call{:async} PB();

-    call{:async} PC();

-    call{:async} PD();

+    async call PB();

+    async call PC();

+    async call PD();

   }

 }

diff --git a/Test/og/foo.bpl b/Test/og/foo.bpl
index d8d5bafd..776a165d 100644
--- a/Test/og/foo.bpl
+++ b/Test/og/foo.bpl
@@ -9,22 +9,23 @@ procedure PC()
   ensures g == 3;

 {

   g := 3;

-  assert{:yield} g == 3;

+  yield;

+  assert g == 3;

 }

 

 procedure PD()

 {

   call PC();

   assert g == 3;

-  assert{:yield} true;

+  yield;

 }

 

 procedure{:entrypoint} Main()

 {

   while (true)

   {

-    call{:async} PB();

-    call{:async} PC();

-    call{:async} PD();

+    async call PB();

+    async call PC();

+    async call PD();

   }

 }

diff --git a/Test/og/linear-set.bpl b/Test/og/linear-set.bpl
index 04ad0df2..d188db3a 100644
--- a/Test/og/linear-set.bpl
+++ b/Test/og/linear-set.bpl
@@ -32,15 +32,16 @@ requires tidls' != None() && xls' == All();
     assume tidls' == tidls && xls' == xls;

 

     x := 42;

-    assert {:yield} xls == All();

+    yield;

+    assert xls == All();

     assert x == 42;

     call xls1, xls2 := Split(xls);

     havoc lsChild;

     assume (lsChild != None());

-    call {:async} thread(lsChild, xls1);

+    async call thread(lsChild, xls1);

     havoc lsChild;

     assume (lsChild != None());

-    call {:async} thread(lsChild, xls2);

+    async call thread(lsChild, xls2);

 }

 

 procedure thread({:linear "tid"} tidls': [X]bool, {:linear "x"} xls': [X]bool)

@@ -54,10 +55,13 @@ requires tidls' != None() && xls' != None();
 

     assume l == None();

     l := tidls;

-    assert {:yield} tidls != None() && xls != None();

+    yield;

+    assert tidls != None() && xls != None();

     x := 0;

-    assert {:yield} tidls != None() && xls != None();

+    yield;

+    assert tidls != None() && xls != None();

     assert x == 0;

-    assert {:yield} tidls != None() && xls != None();

+    yield;

+    assert tidls != None() && xls != None();

     l := None();

 }

diff --git a/Test/og/linear-set2.bpl b/Test/og/linear-set2.bpl
index 0df45254..5d627348 100644
--- a/Test/og/linear-set2.bpl
+++ b/Test/og/linear-set2.bpl
@@ -33,15 +33,16 @@ requires tidls' != nil && xls' == All();
     assume tidls' == tidls && xls' == xls;

 

     x := 42;

-    assert {:yield} xls == All();

+    yield;

+    assert xls == All();

     assert x == 42;

     call xls1, xls2 := Split(xls);

     havoc lsChild;

     assume (lsChild != nil);

-    call {:async} thread(lsChild, xls1);

+    async call thread(lsChild, xls1);

     havoc lsChild;

     assume (lsChild != nil);

-    call {:async} thread(lsChild, xls2);

+    async call thread(lsChild, xls2);

 }

 

 procedure thread({:linear "tid"} tidls': X, {:linear "x"} xls': [X]bool)

@@ -55,10 +56,13 @@ requires tidls' != nil && xls' != None();
 

     assume l == nil;

     l := tidls;

-    assert {:yield} tidls != nil && xls != None();

+    yield;

+    assert tidls != nil && xls != None();

     x := 0;

-    assert {:yield} tidls != nil && xls != None();

+    yield;

+    assert tidls != nil && xls != None();

     assert x == 0;

-    assert {:yield} tidls != nil && xls != None();

+    yield;

+    assert tidls != nil && xls != None();

     l := nil;

 }

diff --git a/Test/og/one.bpl b/Test/og/one.bpl
index bb7b1d01..806a4178 100644
--- a/Test/og/one.bpl
+++ b/Test/og/one.bpl
@@ -8,6 +8,7 @@ procedure A()
 procedure B()

 {

   x := 5;

-  assert{:yield} x == 5;

+  yield;

+  assert x == 5;

 }

 

diff --git a/Test/og/parallel1.bpl b/Test/og/parallel1.bpl
new file mode 100644
index 00000000..cb3502b4
--- /dev/null
+++ b/Test/og/parallel1.bpl
@@ -0,0 +1,29 @@
+var g:int;

+

+procedure PB()

+{

+  g := g + 1;

+}

+

+procedure PC()

+  ensures g == 3;

+{

+  g := 3;

+  yield;

+  assert g == 3;

+}

+

+procedure PD()

+{

+  call PC();

+  assert g == 3;

+  yield;

+}

+

+procedure{:entrypoint} Main()

+{

+  while (true)

+  {

+    call PB() | PC() | PD();

+  }

+}

diff --git a/Test/og/parallel2.bpl b/Test/og/parallel2.bpl
new file mode 100644
index 00000000..444b9805
--- /dev/null
+++ b/Test/og/parallel2.bpl
@@ -0,0 +1,35 @@
+var a:[int]int;

+

+procedure {:entrypoint} main() 

+{

+    var {:linear "tid"} i: int;

+    var {:linear "tid"} j: int;

+    call i := t(i) | j := t(j);

+    call i := u(i) | j := u(j);

+}

+

+procedure t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

+{

+    assume i == i';

+

+    a[i] := 42;

+    call i := Yield(i);

+    assert a[i] == 42;

+}

+

+procedure u({:linear "tid"} i': int) returns ({:linear "tid"} i: int) 

+{

+    assume i == i';

+

+    a[i] := 42;

+    yield;

+    assert a[i] == 42;

+}

+

+procedure Yield({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

+ensures i == i';

+ensures old(a)[i] == a[i];

+{

+    assume i == i';

+    yield;

+}
\ No newline at end of file
diff --git a/Test/og/runtest.bat b/Test/og/runtest.bat
index b00a3dda..0cca4898 100644
--- a/Test/og/runtest.bat
+++ b/Test/og/runtest.bat
@@ -3,13 +3,13 @@ setlocal
 

 set BGEXE=..\..\Binaries\Boogie.exe

 

-for %%f in (foo.bpl bar.bpl one.bpl) do (

+for %%f in (foo.bpl bar.bpl one.bpl parallel1.bpl) do (

   echo.

   echo -------------------- %%f --------------------

   %BGEXE% %* /nologo /noinfer /doModSetAnalysis /OwickiGries:OwickiGriesDesugared.bpl %%f

 )

 

-for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl DeviceCacheSimplified.bpl) do (

+for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl DeviceCacheSimplified.bpl parallel2.bpl) do (

   echo.

   echo -------------------- %%f --------------------

   %BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory /doModSetAnalysis  /OwickiGries:OwickiGriesDesugared.bpl %%f

diff --git a/Test/prover/Answer b/Test/prover/Answer
index 688e6e6a..1ca6407c 100644
--- a/Test/prover/Answer
+++ b/Test/prover/Answer
@@ -4,7 +4,7 @@
 z3mutl.bpl(20,5): Error BP5001: This assertion might not hold.

 Execution trace:

     z3mutl.bpl(5,1): start

-    z3mutl.bpl(8,1): L1

+    z3mutl.bpl(14,1): L3

     z3mutl.bpl(20,1): L5

 z3mutl.bpl(20,5): Error BP5001: This assertion might not hold.

 Execution trace:

@@ -14,7 +14,7 @@ Execution trace:
 z3mutl.bpl(20,5): Error BP5001: This assertion might not hold.

 Execution trace:

     z3mutl.bpl(5,1): start

-    z3mutl.bpl(14,1): L3

+    z3mutl.bpl(8,1): L1

     z3mutl.bpl(20,1): L5

 

 Boogie program verifier finished with 0 verified, 3 errors

@@ -24,19 +24,19 @@ EQ_v2.Eval__v4.Eval_out.bpl(2101,5): Error BP5003: A postcondition might not hol
 EQ_v2.Eval__v4.Eval_out.bpl(1715,3): Related location: This is the postcondition that might not hold.

 Execution trace:

     EQ_v2.Eval__v4.Eval_out.bpl(1786,3): AA_INSTR_EQ_BODY

-    EQ_v2.Eval__v4.Eval_out.bpl(1875,3): inline$v2.Eval$0$label_11_case_1#2

+    EQ_v2.Eval__v4.Eval_out.bpl(1862,3): inline$v2.Eval$0$label_11_case_2#2

     EQ_v2.Eval__v4.Eval_out.bpl(1894,3): inline$v2.Eval$0$label_12#2

-    EQ_v2.Eval__v4.Eval_out.bpl(2032,3): inline$v4.Eval$0$label_11_case_1#2

-    EQ_v2.Eval__v4.Eval_out.bpl(2054,3): inline$v4.Eval$0$label_13_true#2

+    EQ_v2.Eval__v4.Eval_out.bpl(1989,3): inline$v4.Eval$0$label_11_case_2#2

+    EQ_v2.Eval__v4.Eval_out.bpl(2011,3): inline$v4.Eval$0$label_14_true#2

     EQ_v2.Eval__v4.Eval_out.bpl(2081,3): inline$v4.Eval$0$label_12#2

 EQ_v2.Eval__v4.Eval_out.bpl(2101,5): Error BP5003: A postcondition might not hold on this return path.

 EQ_v2.Eval__v4.Eval_out.bpl(1715,3): Related location: This is the postcondition that might not hold.

 Execution trace:

     EQ_v2.Eval__v4.Eval_out.bpl(1786,3): AA_INSTR_EQ_BODY

-    EQ_v2.Eval__v4.Eval_out.bpl(1862,3): inline$v2.Eval$0$label_11_case_2#2

+    EQ_v2.Eval__v4.Eval_out.bpl(1875,3): inline$v2.Eval$0$label_11_case_1#2

     EQ_v2.Eval__v4.Eval_out.bpl(1894,3): inline$v2.Eval$0$label_12#2

-    EQ_v2.Eval__v4.Eval_out.bpl(1989,3): inline$v4.Eval$0$label_11_case_2#2

-    EQ_v2.Eval__v4.Eval_out.bpl(2011,3): inline$v4.Eval$0$label_14_true#2

+    EQ_v2.Eval__v4.Eval_out.bpl(2032,3): inline$v4.Eval$0$label_11_case_1#2

+    EQ_v2.Eval__v4.Eval_out.bpl(2054,3): inline$v4.Eval$0$label_13_true#2

     EQ_v2.Eval__v4.Eval_out.bpl(2081,3): inline$v4.Eval$0$label_12#2

 EQ_v2.Eval__v4.Eval_out.bpl(2152,5): Error BP5003: A postcondition might not hold on this return path.

 EQ_v2.Eval__v4.Eval_out.bpl(2120,3): Related location: This is the postcondition that might not hold.