summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
authorGravatar Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com>2013-02-13 13:19:38 -0800
committerGravatar Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com>2013-02-13 13:19:38 -0800
commit6204a4510168dbcd95a0e9e0ec255fb58bb44d87 (patch)
tree57a538891cb769aa6771f16f37a918d5ac03aced /Test
parent1ca4bdc8652046f902b50820c1c250148e1abe25 (diff)
fixed bugs in typechecking of linear sets
added regressions to linear sets removed the need to supply the builtin map operations manually
Diffstat (limited to 'Test')
-rw-r--r--Test/linear/Answer20
-rw-r--r--Test/linear/Maps.bpl24
-rw-r--r--Test/linear/list.bpl4
-rw-r--r--Test/linear/runtest.bat4
-rw-r--r--Test/linear/typecheck.bpl65
-rw-r--r--Test/og/DeviceCacheSimplified.bpl2
-rw-r--r--Test/og/FlanaganQadeer.bpl2
-rw-r--r--Test/og/Maps.bpl24
-rw-r--r--Test/og/linear-set.bpl13
-rw-r--r--Test/og/linear-set2.bpl13
-rw-r--r--Test/og/runtest.bat2
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
)