new design for linear types + VCgen

ported all the examples
added the QED examples to runtest.bat

18 files changed, 135 insertions, 8 deletions

diff --git a/Test/linear/Answer b/Test/linear/Answer
index 2934d690..9219497b 100644
--- a/Test/linear/Answer
+++ b/Test/linear/Answer
@@ -1,7 +1,5 @@
 

 -------------------- typecheck.bpl --------------------

-typecheck.bpl(6,22): Error: Linear domain A must be consistently attached to variables of one type

-typecheck.bpl(18,22): Error: a linear domain can be attached to either a set or a scalar type

 typecheck.bpl(31,9): Error: Only simple assignment allowed on linear variable b

 typecheck.bpl(33,6): Error: Only variable can be assigned to linear variable a

 typecheck.bpl(35,6): Error: Only linear variable can be assigned to linear variable a

@@ -17,7 +15,7 @@ typecheck.bpl(67,0): Error: Output variable d must be available at a return
 typecheck.bpl(76,0): Error: Global variable g must be available at a return

 typecheck.bpl(81,7): Error: unavailable source for a linear read

 typecheck.bpl(82,0): Error: Output variable r must be available at a return

-17 type checking errors detected in typecheck.bpl

+15 type checking errors detected in typecheck.bpl

 

 -------------------- list.bpl --------------------

 

diff --git a/Test/linear/list.bpl b/Test/linear/list.bpl
index f4badca9..b0caa9e1 100644
--- a/Test/linear/list.bpl
+++ b/Test/linear/list.bpl
@@ -2,6 +2,11 @@ type X;
 function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

 function {:builtin "MapOr"} MapOr([X]bool, [X]bool) : [X]bool;

 

+function {:inline} {:linear "Mem"} MemCollector(xs: [X]bool) : [X]bool

+{

+  xs

+}

+

 var head: X;

 var tail: X;

 var {:linear "Mem"} D: [X]bool;

diff --git a/Test/og/Answer b/Test/og/Answer
index 067a6534..c9e349e1 100644
--- a/Test/og/Answer
+++ b/Test/og/Answer
@@ -56,10 +56,10 @@ Boogie program verifier finished with 5 verified, 0 errors
 Boogie program verifier finished with 4 verified, 0 errors

 

 -------------------- parallel4.bpl --------------------

-parallel4.bpl(18,3): Error BP5001: This assertion might not hold.

+parallel4.bpl(24,3): Error BP5001: This assertion might not hold.

 Execution trace:

     (0,0): og_init

-    parallel4.bpl(16,5): anon0$1

+    parallel4.bpl(22,5): anon0$1

 

 Boogie program verifier finished with 2 verified, 1 error

 

@@ -72,7 +72,7 @@ Boogie program verifier finished with 4 verified, 0 errors
 Boogie program verifier finished with 3 verified, 0 errors

 

 -------------------- t1.bpl --------------------

-t1.bpl(35,5): Error: Non-interference check failed

+t1.bpl(51,5): Error: Non-interference check failed

 Execution trace:

     (0,0): og_init

     (0,0): inline$Impl_YieldChecker_A_2147483647$0$L1

@@ -95,3 +95,19 @@ Execution trace:
     (0,0): inline$Proc_YieldChecker_P_2147483647$1$L0

 

 Boogie program verifier finished with 1 verified, 1 error

+

+-------------------- DeviceCache.bpl --------------------

+

+Boogie program verifier finished with 50 verified, 0 errors

+

+-------------------- ticket.bpl --------------------

+

+Boogie program verifier finished with 28 verified, 0 errors

+

+-------------------- lock.bpl --------------------

+

+Boogie program verifier finished with 6 verified, 0 errors

+

+-------------------- multiset.bpl --------------------

+

+Boogie program verifier finished with 102 verified, 0 errors

diff --git a/Test/og/DeviceCache.bpl b/Test/og/DeviceCache.bpl
index 730b1ce1..ec61e188 100644
--- a/Test/og/DeviceCache.bpl
+++ b/Test/og/DeviceCache.bpl
@@ -6,6 +6,16 @@ var {:qed} lock: X;
 var {:qed} currsize: int;

 var {:qed} newsize: int;

 

+function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

+function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool

+{

+  MapConstBool(false)[x := true]

+}

+function {:inline} {:linear "tid"} TidSetCollector(x: [X]bool) : [X]bool

+{

+  x

+}

+

 function {:inline} Inv(ghostLock: X, currsize: int, newsize: int) : (bool)

 {

     0 <= currsize && currsize <= newsize && 

diff --git a/Test/og/DeviceCacheSimplified.bpl b/Test/og/DeviceCacheSimplified.bpl
index 32fb25b7..28e8b662 100644
--- a/Test/og/DeviceCacheSimplified.bpl
+++ b/Test/og/DeviceCacheSimplified.bpl
@@ -1,5 +1,11 @@
 type X;

 

+function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

+function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool

+{

+  MapConstBool(false)[x := true]

+}

+

 function {:inline} Inv(ghostLock: X, currsize: int, newsize: int) : (bool)

 {

     currsize <= newsize && (ghostLock == nil <==> currsize == newsize)

diff --git a/Test/og/FlanaganQadeer.bpl b/Test/og/FlanaganQadeer.bpl
index 5985b6d6..a263467c 100644
--- a/Test/og/FlanaganQadeer.bpl
+++ b/Test/og/FlanaganQadeer.bpl
@@ -1,9 +1,14 @@
 type X;

-

 const nil: X;

 var l: X;

 var x: int;

 

+function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

+function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool

+{

+  MapConstBool(false)[x := true]

+}

+

 procedure Allocate() returns ({:linear "tid"} xls: X);

 ensures xls != nil;

 

diff --git a/Test/og/akash.bpl b/Test/og/akash.bpl
index eaa820b9..d31c20ee 100644
--- a/Test/og/akash.bpl
+++ b/Test/og/akash.bpl
@@ -1,5 +1,21 @@
 function {:builtin "MapConst"} mapconstbool(bool) : [int]bool;

 

+function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;

+function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool

+{

+  MapConstBool(false)[x := true]

+}

+

+function {:inline} {:linear "1"} SetCollector1(x: [int]bool) : [int]bool

+{

+  x

+}

+

+function {:inline} {:linear "2"} SetCollector2(x: [int]bool) : [int]bool

+{

+  x

+}

+

 procedure Allocate() returns ({:linear "tid"} xls: int);

 ensures xls != 0;

 

diff --git a/Test/og/linear-set.bpl b/Test/og/linear-set.bpl
index 96aca741..ff3f5b1e 100644
--- a/Test/og/linear-set.bpl
+++ b/Test/og/linear-set.bpl
@@ -13,6 +13,11 @@ function {:inline} All() : [X]bool
     MapConstBool(true)

 }

 

+function {:inline} {:linear "x"} XCollector(xs: [X]bool) : [X]bool

+{

+  xs

+}

+

 var x: int;

 var l: [X]bool;

 

diff --git a/Test/og/linear-set2.bpl b/Test/og/linear-set2.bpl
index 565cc82b..04406609 100644
--- a/Test/og/linear-set2.bpl
+++ b/Test/og/linear-set2.bpl
@@ -13,6 +13,11 @@ function {:inline} All() : [X]bool
     MapConstBool(true)

 }

 

+function {:inline} {:linear "x"} XCollector(xs: [X]bool) : [X]bool

+{

+  xs

+}

+

 var x: int;

 var l: X;

 const nil: X;

diff --git a/Test/og/multiset.bpl b/Test/og/multiset.bpl
index 047d25a6..161171bf 100644
--- a/Test/og/multiset.bpl
+++ b/Test/og/multiset.bpl
@@ -10,6 +10,12 @@ var {:qed} lock : [int]X;
 var {:qed} owner : [int]X;

 const max : int;

 

+function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

+function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool

+{

+  MapConstBool(false)[x := true]

+}

+

 axiom (max > 0);

 

 procedure {:yields} acquire(i : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);

diff --git a/Test/og/new1.bpl b/Test/og/new1.bpl
index 6ebb9cf1..64144ae9 100644
--- a/Test/og/new1.bpl
+++ b/Test/og/new1.bpl
@@ -2,6 +2,12 @@ function {:builtin "MapConst"} mapconstbool(x:bool): [int]bool;
 

 var g:int;

 

+function {:inline} {:linear "Perm"} SetCollectorPerm(x: [int]bool) : [int]bool

+{

+  x

+}

+

+

 var {:linear "Perm"} Permissions: [int]bool;

 

 procedure Allocate_Perm() returns ({:linear "Perm"} xls: [int]bool);

diff --git a/Test/og/parallel2.bpl b/Test/og/parallel2.bpl
index 6cc85131..07864511 100644
--- a/Test/og/parallel2.bpl
+++ b/Test/og/parallel2.bpl
@@ -1,5 +1,11 @@
 var a:[int]int;

 

+function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;

+function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool

+{

+  MapConstBool(false)[x := true]

+}

+

 procedure Allocate() returns ({:linear "tid"} xls: int);

 

 procedure {:entrypoint} {:yields} main() 

diff --git a/Test/og/parallel4.bpl b/Test/og/parallel4.bpl
index 22e7173f..1069399f 100644
--- a/Test/og/parallel4.bpl
+++ b/Test/og/parallel4.bpl
@@ -2,6 +2,12 @@ var a:int;
 

 procedure Allocate() returns ({:linear "tid"} xls: int);

 

+function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;

+function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool

+{

+  MapConstBool(false)[x := true]

+}

+

 procedure {:entrypoint} {:yields} main() 

 {

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

diff --git a/Test/og/parallel5.bpl b/Test/og/parallel5.bpl
index 34bb82a9..01bbe74d 100644
--- a/Test/og/parallel5.bpl
+++ b/Test/og/parallel5.bpl
@@ -2,6 +2,12 @@ var a:[int]int;
 

 procedure Allocate() returns ({:linear "tid"} xls: int);

 

+function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;

+function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool

+{

+  MapConstBool(false)[x := true]

+}

+

 procedure {:entrypoint} {:yields} main() 

 {

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

diff --git a/Test/og/perm.bpl b/Test/og/perm.bpl
index ad4123f9..8b77ce1b 100644
--- a/Test/og/perm.bpl
+++ b/Test/og/perm.bpl
@@ -3,6 +3,11 @@ function {:builtin "MapConst"} ch_mapconstbool(x: bool) : [int]bool;
 

 function {:builtin "MapOr"} ch_mapunion(x: [int]bool, y: [int]bool) : [int]bool;

 

+function {:inline} {:linear "Perm"} SetCollectorPerm(x: [int]bool) : [int]bool

+{

+  x

+}

+

 procedure Split({:linear "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);

 

diff --git a/Test/og/runtest.bat b/Test/og/runtest.bat
index 068f361f..30bd66cc 100644
--- a/Test/og/runtest.bat
+++ b/Test/og/runtest.bat
@@ -9,7 +9,7 @@ for %%f in (foo.bpl bar.bpl one.bpl parallel1.bpl) do (
   %BGEXE% %* /nologo /noinfer %%f

 )

 

-for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl DeviceCacheSimplified.bpl parallel2.bpl parallel4.bpl parallel5.bpl akash.bpl t1.bpl new1.bpl perm.bpl async.bpl) do (

+for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl DeviceCacheSimplified.bpl parallel2.bpl parallel4.bpl parallel5.bpl akash.bpl t1.bpl new1.bpl perm.bpl async.bpl DeviceCache.bpl ticket.bpl lock.bpl multiset.bpl) do (

   echo.

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

   %BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory %%f

diff --git a/Test/og/t1.bpl b/Test/og/t1.bpl
index 84ed3a35..43758a91 100644
--- a/Test/og/t1.bpl
+++ b/Test/og/t1.bpl
@@ -1,5 +1,21 @@
 function {:builtin "MapConst"} mapconstbool(bool) : [int]bool;

 

+function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;

+function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool

+{

+  MapConstBool(false)[x := true]

+}

+

+function {:inline} {:linear "1"} SetCollector1(x: [int]bool) : [int]bool

+{

+  x

+}

+

+function {:inline} {:linear "2"} SetCollector2(x: [int]bool) : [int]bool

+{

+  x

+}

+

 procedure Allocate() returns ({:linear "tid"} xls: int);

 ensures xls != 0;

 

diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl
index fe56fb27..3404f8e0 100644
--- a/Test/og/ticket.bpl
+++ b/Test/og/ticket.bpl
@@ -11,6 +11,16 @@ var {:qed} s: int;
 var {:qed} cs: X;

 var {:qed} T: [int]bool;

 

+function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

+function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool

+{

+  MapConstBool(false)[x := true]

+}

+function {:inline} {:linear "tid"} TidSetCollector(x: [X]bool) : [X]bool

+{

+  x

+}

+

 function {:inline} Inv1(tickets: [int]bool, ticket: int): (bool)

 {

     tickets == RightOpen(ticket)