fixed bugs in typechecking of linear sets

added regressions to linear sets
removed the need to supply the builtin map operations manually

11 files changed, 104 insertions, 69 deletions

diff --git a/Test/linear/Answer b/Test/linear/Answer
new file mode 100644
index 00000000..86e42862
--- /dev/null
+++ b/Test/linear/Answer
@@ -0,0 +1,20 @@
+

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

+typecheck.bpl(6,22): Error: a linear domain must be consistently attached to variables of a particular 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 sets

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

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

+typecheck.bpl(39,6): Error: Variable of one domain being assigned to a variable of another domain

+typecheck.bpl(45,9): Error: A linear set can occur only once in the rhs

+typecheck.bpl(49,4): Error: A linear set can occur only once as an in parameter

+typecheck.bpl(51,4): Error: Only variable can be assigned to a linear variable

+typecheck.bpl(53,4): Error: The domains of formal and actual parameters must be the same

+typecheck.bpl(55,4): Error: The domains of formal and actual parameters must be the same

+typecheck.bpl(57,4): Error: Only a linear argument can be passed to a linear parameter

+typecheck.bpl(64,6): Error: Only linear variable can be assigned to another linear variable

+0 type checking errors detected in typecheck.bpl

+

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

+

+Boogie program verifier finished with 2 verified, 0 errors

diff --git a/Test/linear/Maps.bpl b/Test/linear/Maps.bpl
deleted file mode 100644
index 5f302034..00000000
--- a/Test/linear/Maps.bpl
+++ /dev/null
@@ -1,24 +0,0 @@
-type X;

-

-function {:builtin "MapAdd"} MapAdd([X]int, [X]int) : [X]int;

-function {:builtin "MapSub"} MapSub([X]int, [X]int) : [X]int;

-function {:builtin "MapMul"} MapMul([X]int, [X]int) : [X]int;

-function {:builtin "MapDiv"} MapDiv([X]int, [X]int) : [X]int;

-function {:builtin "MapMod"} MapMod([X]int, [X]int) : [X]int;

-function {:builtin "MapConst"} MapConstInt(int) : [X]int;

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

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

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

-function {:builtin "MapNot"} MapNot([X]bool) : [X]bool;

-function {:builtin "MapIte"} MapIteInt([X]bool, [X]int, [X]int) : [X]int;

-function {:builtin "MapIte"} MapIteBool([X]bool, [X]bool, [X]bool) : [X]bool;

-function {:builtin "MapLe"} MapLe([X]int, [X]int) : [X]bool;

-function {:builtin "MapLt"} MapLt([X]int, [X]int) : [X]bool;

-function {:builtin "MapGe"} MapGe([X]int, [X]int) : [X]bool;

-function {:builtin "MapGt"} MapGt([X]int, [X]int) : [X]bool;

-function {:builtin "MapEq"} MapEq([X]int, [X]int) : [X]bool;

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

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

-

-

-

diff --git a/Test/linear/list.bpl b/Test/linear/list.bpl
index 9a333351..f4badca9 100644
--- a/Test/linear/list.bpl
+++ b/Test/linear/list.bpl
@@ -1,3 +1,7 @@
+type X;

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

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

+

 var head: X;

 var tail: X;

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

diff --git a/Test/linear/runtest.bat b/Test/linear/runtest.bat
index 28c91996..df176994 100644
--- a/Test/linear/runtest.bat
+++ b/Test/linear/runtest.bat
@@ -3,9 +3,9 @@ setlocal
 

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

 

-for %%f in (list.bpl) do (

+for %%f in (typecheck.bpl list.bpl) do (

   echo.

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

-  %BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory /doModSetAnalysis %%f Maps.bpl

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

 )

 

diff --git a/Test/linear/typecheck.bpl b/Test/linear/typecheck.bpl
new file mode 100644
index 00000000..f79f8fb5
--- /dev/null
+++ b/Test/linear/typecheck.bpl
@@ -0,0 +1,65 @@
+type X;

+

+procedure A()

+{

+    var {:linear "A"} a: X;

+    var {:linear "A"} b: int;

+}

+

+procedure B()

+{

+    var {:linear "B"} a: X;

+    var {:linear "B"} b: [X]bool;

+}

+

+procedure C()

+{

+    var {:linear "C"} a: X;

+    var {:linear "C"} c: [X]int;

+}

+

+function f(X): X;

+

+procedure D()

+{

+    var {:linear "D"} a: X;

+    var {:linear "D"} x: X;

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

+    var c: X;

+    var {:linear "D2"} d: X;

+

+    b[a] := true;

+

+    a := f(a);

+

+    a := c;

+

+    c := a;

+

+    a := d;

+

+    a := a;

+

+    a, x := x, a;

+

+    a, x := x, x;

+

+    call a, x := E(a, x);

+

+    call a, x := E(a, a);

+

+    call a, x := E(a, f(a));

+

+    call a, x := E(a, d);

+

+    call d, x := E(a, x);

+

+    call a, x := E(c, x);

+

+    call c, x := E(a, x);

+}

+

+procedure E({:linear "D"} a: X, {:linear "D"} b: X) returns ({:linear "D"} c: X, {:linear "D"} d: X)

+{

+    c := a;

+}
\ No newline at end of file
diff --git a/Test/og/DeviceCacheSimplified.bpl b/Test/og/DeviceCacheSimplified.bpl
index 40a0ab1c..c89bd793 100644
--- a/Test/og/DeviceCacheSimplified.bpl
+++ b/Test/og/DeviceCacheSimplified.bpl
@@ -1,3 +1,5 @@
+type X;

+

 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 63a7fc0d..8379925f 100644
--- a/Test/og/FlanaganQadeer.bpl
+++ b/Test/og/FlanaganQadeer.bpl
@@ -1,3 +1,5 @@
+type X;

+

 const nil: X;

 var l: X;

 var x: int;

diff --git a/Test/og/Maps.bpl b/Test/og/Maps.bpl
deleted file mode 100644
index 5f302034..00000000
--- a/Test/og/Maps.bpl
+++ /dev/null
@@ -1,24 +0,0 @@
-type X;

-

-function {:builtin "MapAdd"} MapAdd([X]int, [X]int) : [X]int;

-function {:builtin "MapSub"} MapSub([X]int, [X]int) : [X]int;

-function {:builtin "MapMul"} MapMul([X]int, [X]int) : [X]int;

-function {:builtin "MapDiv"} MapDiv([X]int, [X]int) : [X]int;

-function {:builtin "MapMod"} MapMod([X]int, [X]int) : [X]int;

-function {:builtin "MapConst"} MapConstInt(int) : [X]int;

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

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

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

-function {:builtin "MapNot"} MapNot([X]bool) : [X]bool;

-function {:builtin "MapIte"} MapIteInt([X]bool, [X]int, [X]int) : [X]int;

-function {:builtin "MapIte"} MapIteBool([X]bool, [X]bool, [X]bool) : [X]bool;

-function {:builtin "MapLe"} MapLe([X]int, [X]int) : [X]bool;

-function {:builtin "MapLt"} MapLt([X]int, [X]int) : [X]bool;

-function {:builtin "MapGe"} MapGe([X]int, [X]int) : [X]bool;

-function {:builtin "MapGt"} MapGt([X]int, [X]int) : [X]bool;

-function {:builtin "MapEq"} MapEq([X]int, [X]int) : [X]bool;

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

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

-

-

-

diff --git a/Test/og/linear-set.bpl b/Test/og/linear-set.bpl
index 1a0cde42..04ad0df2 100644
--- a/Test/og/linear-set.bpl
+++ b/Test/og/linear-set.bpl
@@ -1,12 +1,7 @@
-function {:inline} Subset(a: [X]bool, b: [X]bool) : bool

-{

-    MapImp(a, b) == MapConstBool(true)

-}

-

-function {:inline} In(a: X, b: [X]bool) : bool

-{

-    b[a]

-}

+type X;

+function {:builtin "MapConst"} MapConstInt(int) : [X]int;

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

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

 

 function {:inline} None() : [X]bool

 {

diff --git a/Test/og/linear-set2.bpl b/Test/og/linear-set2.bpl
index a91100b6..0df45254 100644
--- a/Test/og/linear-set2.bpl
+++ b/Test/og/linear-set2.bpl
@@ -1,12 +1,7 @@
-function {:inline} Subset(a: [X]bool, b: [X]bool) : bool

-{

-    MapImp(a, b) == MapConstBool(true)

-}

-

-function {:inline} In(a: X, b: [X]bool) : bool

-{

-    b[a]

-}

+type X;

+function {:builtin "MapConst"} MapConstInt(int) : [X]int;

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

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

 

 function {:inline} None() : [X]bool

 {

diff --git a/Test/og/runtest.bat b/Test/og/runtest.bat
index 197f33f7..b00a3dda 100644
--- a/Test/og/runtest.bat
+++ b/Test/og/runtest.bat
@@ -12,6 +12,6 @@ for %%f in (foo.bpl bar.bpl one.bpl) do (
 for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl DeviceCacheSimplified.bpl) do (

   echo.

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

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

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

 )