handling old() in stable assertions

bug fix in linear

9 files changed, 311 insertions, 0 deletions

diff --git a/Test/linear/Maps.bpl b/Test/linear/Maps.bpl
new file mode 100644
index 00000000..5f302034
--- /dev/null
+++ b/Test/linear/Maps.bpl
@@ -0,0 +1,24 @@
+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
new file mode 100644
index 00000000..9a333351
--- /dev/null
+++ b/Test/linear/list.bpl
@@ -0,0 +1,39 @@
+var head: X;

+var tail: X;

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

+var Next:[X]X;

+const nil: X;

+

+procedure malloc() returns (x: X, {:linear "Mem"} M: [X]bool);

+ensures M == MapConstBool(false)[x := true];

+

+procedure Join({:linear "Mem"} A: [X]bool);

+modifies D;

+ensures MapOr(old(D), A) == D;

+

+procedure one()

+requires D[head] && D[tail];

+requires (forall d: X :: {D[d]} D[d] ==> D[Next[d]] || d == tail);

+ensures D[head] && D[tail];

+ensures (forall d: X :: {D[d]} D[d] ==> D[Next[d]] || d == tail);

+ensures head != tail;

+{

+    var x: X;

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

+

+    call x, M := malloc();

+    call Join(M);

+    Next[tail] := x;

+    tail := x;

+    Next[tail] := nil;

+}

+

+procedure two()

+requires head != tail;

+requires D[head] && D[tail];

+requires (forall d: X :: {D[d]} D[d] ==> D[Next[d]] || d == tail);

+ensures (forall d: X :: {D[d]} D[d] ==> D[Next[d]] || d == tail);

+ensures D[head] && D[tail];

+{

+    head := Next[head];

+}

diff --git a/Test/linear/runtest.bat b/Test/linear/runtest.bat
new file mode 100644
index 00000000..28c91996
--- /dev/null
+++ b/Test/linear/runtest.bat
@@ -0,0 +1,11 @@
+@echo off

+setlocal

+

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

+

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

+  echo.

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

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

+)

+

diff --git a/Test/og/Maps.bpl b/Test/og/Maps.bpl
new file mode 100644
index 00000000..5f302034
--- /dev/null
+++ b/Test/og/Maps.bpl
@@ -0,0 +1,24 @@
+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/bar.bpl b/Test/og/bar.bpl
new file mode 100644
index 00000000..cddc5338
--- /dev/null
+++ b/Test/og/bar.bpl
@@ -0,0 +1,29 @@
+var g:int;

+

+procedure PB()

+{

+  g := g + 1;

+}

+

+procedure PC()

+  ensures g == old(g);

+{

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

+}

+

+procedure PD()

+{

+  g := 3;

+  call PC();

+  assert g == 3;

+}

+

+procedure{:entrypoint} Main2()

+{

+  while (true)

+  {

+    call{:async} PB();

+    call{:async} PC();

+    call{:async} PD();

+  }

+}

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

+

+procedure PB()

+{

+  g := g + 1;

+}

+

+procedure PC()

+  ensures g == 3;

+{

+  g := 3;

+  assert{:yield} g == 3;

+}

+

+procedure PD()

+{

+  call PC();

+  assert g == 3;

+  assert{:yield} true;

+}

+

+procedure{:entrypoint} Main()

+{

+  while (true)

+  {

+    call{:async} PB();

+    call{:async} PC();

+    call{:async} PD();

+  }

+}

diff --git a/Test/og/linear-set.bpl b/Test/og/linear-set.bpl
new file mode 100644
index 00000000..1a0cde42
--- /dev/null
+++ b/Test/og/linear-set.bpl
@@ -0,0 +1,68 @@
+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]

+}

+

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

+{

+    MapConstBool(false)

+}

+

+function {:inline} All() : [X]bool

+{

+    MapConstBool(true)

+}

+

+var x: int;

+var l: [X]bool;

+

+procedure Split({:linear "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 {:entrypoint} main({:linear "tid"} tidls': [X]bool, {:linear "x"} xls': [X]bool) 

+requires tidls' != None() && xls' == All();

+{

+    var {:linear "tid"} tidls: [X]bool;

+    var {:linear "x"} xls: [X]bool;

+    var {:linear "tid"} lsChild: [X]bool;

+    var {:linear "x"} xls1: [X]bool;

+    var {:linear "x"} xls2: [X]bool;

+

+    havoc tidls, xls;

+    assume tidls' == tidls && xls' == xls;

+

+    x := 42;

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

+    assert x == 42;

+    call xls1, xls2 := Split(xls);

+    havoc lsChild;

+    assume (lsChild != None());

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

+    havoc lsChild;

+    assume (lsChild != None());

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

+}

+

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

+requires tidls' != None() && xls' != None();

+{

+    var {:linear "x"} xls: [X]bool;

+    var {:linear "tid"} tidls: [X]bool;

+

+    havoc tidls, xls;

+    assume tidls' == tidls && xls' == xls;

+

+    assume l == None();

+    l := tidls;

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

+    x := 0;

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

+    assert x == 0;

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

+    l := None();

+}

diff --git a/Test/og/linear-set2.bpl b/Test/og/linear-set2.bpl
new file mode 100644
index 00000000..a91100b6
--- /dev/null
+++ b/Test/og/linear-set2.bpl
@@ -0,0 +1,69 @@
+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]

+}

+

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

+{

+    MapConstBool(false)

+}

+

+function {:inline} All() : [X]bool

+{

+    MapConstBool(true)

+}

+

+var x: int;

+var l: X;

+const nil: X;

+

+procedure Split({:linear "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 {:entrypoint} main({:linear "tid"} tidls': X, {:linear "x"} xls': [X]bool) 

+requires tidls' != nil && xls' == All();

+{

+    var {:linear "tid"} tidls: X;

+    var {:linear "x"} xls: [X]bool;

+    var {:linear "tid"} lsChild: X;

+    var {:linear "x"} xls1: [X]bool;

+    var {:linear "x"} xls2: [X]bool;

+

+    havoc tidls, xls;

+    assume tidls' == tidls && xls' == xls;

+

+    x := 42;

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

+    assert x == 42;

+    call xls1, xls2 := Split(xls);

+    havoc lsChild;

+    assume (lsChild != nil);

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

+    havoc lsChild;

+    assume (lsChild != nil);

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

+}

+

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

+requires tidls' != nil && xls' != None();

+{

+    var {:linear "x"} xls: [X]bool;

+    var {:linear "tid"} tidls: X;

+

+    havoc tidls, xls;

+    assume tidls' == tidls && xls' == xls;

+

+    assume l == nil;

+    l := tidls;

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

+    x := 0;

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

+    assert x == 0;

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

+    l := nil;

+}

diff --git a/Test/og/runtest.bat b/Test/og/runtest.bat
new file mode 100644
index 00000000..353097c1
--- /dev/null
+++ b/Test/og/runtest.bat
@@ -0,0 +1,17 @@
+@echo off

+setlocal

+

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

+

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

+  echo.

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

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

+)

+

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

+  echo.

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

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

+)

+