From a2fcc9e7617800e2139a9cbbfa720222e4c1b6f5 Mon Sep 17 00:00:00 2001
From: akashlal <unknown>
Date: Thu, 18 Apr 2013 17:50:18 +0530
Subject: Nice clean re-implementation of AbstractHoudini. And tests

---
 Test/AbsHoudini/houd1.bpl   | 18 +++++++++++
 Test/AbsHoudini/houd10.bpl  | 22 ++++++++++++++
 Test/AbsHoudini/houd11.bpl  | 13 ++++++++
 Test/AbsHoudini/houd12.bpl  | 58 +++++++++++++++++++++++++++++++++++
 Test/AbsHoudini/houd2.bpl   | 27 +++++++++++++++++
 Test/AbsHoudini/houd3.bpl   | 27 +++++++++++++++++
 Test/AbsHoudini/houd4.bpl   | 27 +++++++++++++++++
 Test/AbsHoudini/houd5.bpl   | 29 ++++++++++++++++++
 Test/AbsHoudini/houd6.bpl   | 44 +++++++++++++++++++++++++++
 Test/AbsHoudini/houd7.bpl   | 35 ++++++++++++++++++++++
 Test/AbsHoudini/houd8.bpl   | 29 ++++++++++++++++++
 Test/AbsHoudini/runtest.bat |  9 ++++--
 Test/AbsHoudini/test1.bpl   | 36 ++++++++++++++++++++++
 Test/AbsHoudini/test10.bpl  | 47 +++++++++++++++++++++++++++++
 Test/AbsHoudini/test2.bpl   | 38 +++++++++++++++++++++++
 Test/AbsHoudini/test7.bpl   | 15 ++++++++++
 Test/AbsHoudini/test8.bpl   | 21 +++++++++++++
 Test/AbsHoudini/test9.bpl   | 73 +++++++++++++++++++++++++++++++++++++++++++++
 18 files changed, 566 insertions(+), 2 deletions(-)
 create mode 100644 Test/AbsHoudini/houd1.bpl
 create mode 100644 Test/AbsHoudini/houd10.bpl
 create mode 100644 Test/AbsHoudini/houd11.bpl
 create mode 100644 Test/AbsHoudini/houd12.bpl
 create mode 100644 Test/AbsHoudini/houd2.bpl
 create mode 100644 Test/AbsHoudini/houd3.bpl
 create mode 100644 Test/AbsHoudini/houd4.bpl
 create mode 100644 Test/AbsHoudini/houd5.bpl
 create mode 100644 Test/AbsHoudini/houd6.bpl
 create mode 100644 Test/AbsHoudini/houd7.bpl
 create mode 100644 Test/AbsHoudini/houd8.bpl
 create mode 100644 Test/AbsHoudini/test1.bpl
 create mode 100644 Test/AbsHoudini/test10.bpl
 create mode 100644 Test/AbsHoudini/test2.bpl
 create mode 100644 Test/AbsHoudini/test7.bpl
 create mode 100644 Test/AbsHoudini/test8.bpl
 create mode 100644 Test/AbsHoudini/test9.bpl

(limited to 'Test')

diff --git a/Test/AbsHoudini/houd1.bpl b/Test/AbsHoudini/houd1.bpl
new file mode 100644
index 00000000..099c6f09
--- /dev/null
+++ b/Test/AbsHoudini/houd1.bpl
@@ -0,0 +1,18 @@
+function {:existential true} b1(x: bool) : bool;
+
+var myVar: int;
+
+procedure foo (i:int)
+modifies myVar;
+// comment
+ensures b1(myVar>0);
+{
+  if (i>0) {
+    myVar := 5;
+  } else {
+    myVar := 0;
+  }
+}
+
+// expected output: Correct
+// expected end assigment: b1(x) = x
diff --git a/Test/AbsHoudini/houd10.bpl b/Test/AbsHoudini/houd10.bpl
new file mode 100644
index 00000000..bb0c65e7
--- /dev/null
+++ b/Test/AbsHoudini/houd10.bpl
@@ -0,0 +1,22 @@
+function {:existential true} b1():bool;
+function {:existential true} b2():bool;
+function {:existential true} b3():bool;
+function {:existential true} Assert(): bool;
+var fooVar: int;
+var xVar: int;
+
+procedure foo() 
+modifies fooVar;
+modifies xVar;
+ensures b1() || fooVar==0;
+ensures b3() || xVar<0;
+{
+  fooVar:=5; 
+  call bar();
+}
+
+procedure bar(); 
+modifies xVar;
+requires Assert() || fooVar!=5;
+
+// expected assigment: Assert->true,b1->True,b2->false,b3->True
diff --git a/Test/AbsHoudini/houd11.bpl b/Test/AbsHoudini/houd11.bpl
new file mode 100644
index 00000000..78087744
--- /dev/null
+++ b/Test/AbsHoudini/houd11.bpl
@@ -0,0 +1,13 @@
+function {:existential true} Assert() : bool;
+
+var fooVar: int;
+
+procedure foo() 
+modifies fooVar;
+{
+  fooVar:=5; 
+  assert Assert() || (fooVar==4);
+  assert Assert() || (fooVar==3);
+}
+
+// expected assigment: Assert -> true
diff --git a/Test/AbsHoudini/houd12.bpl b/Test/AbsHoudini/houd12.bpl
new file mode 100644
index 00000000..b3a1a6db
--- /dev/null
+++ b/Test/AbsHoudini/houd12.bpl
@@ -0,0 +1,58 @@
+// Example to test candidate annotations on loops
+
+function {:existential true} Assert(): bool;
+function {:existential true} b1():bool;
+function {:existential true} b2():bool;
+function {:existential true} b3():bool;
+function {:existential true} b4():bool;
+function {:existential true} b5():bool;
+function {:existential true} b6():bool;
+function {:existential true} b7():bool;
+
+var x: int;
+var y: int;
+
+
+procedure foo() 
+modifies x;
+modifies y;
+ensures (b4() || x == 0);
+ensures (b5() || y == 10);
+ensures (b6() || x == 10);
+ensures (b7() || y == 11);
+
+{
+  x := 10;
+  y := 0;
+
+  goto Head;
+
+Head: 
+
+  //loop invariants
+ assert (b1() || x < 0);
+ assert (b2() || x >= 0);
+ assert (b3() || x + y == 10);
+ goto Body, Exit;
+
+Body:
+  assume x > 0;
+  x := x - 1;
+  y := y + 1;
+
+
+  goto Head;
+
+Exit:
+  assume !(x > 0);
+  return;
+}
+
+// expected assigment: Assert -> false, b1->true,b2->false,b3->false,b4->false, b5->false, b6->true,b7->true
+
+
+
+
+
+
+
diff --git a/Test/AbsHoudini/houd2.bpl b/Test/AbsHoudini/houd2.bpl
new file mode 100644
index 00000000..fd2611e2
--- /dev/null
+++ b/Test/AbsHoudini/houd2.bpl
@@ -0,0 +1,27 @@
+function {:existential true} Assert(x:bool) : bool;
+function {:existential true} b1 (x:bool):bool;
+function {:existential true} b2 (x:bool):bool;
+
+
+var myVar: int;
+
+procedure bar(i:int) 
+modifies myVar;
+ensures Assert(myVar>0);
+{
+  call foo(5);
+}
+
+procedure foo (i:int)
+modifies myVar;
+ensures b1(myVar>0);
+ensures Assert(myVar!=-1);
+{
+  if (i>0) {
+    myVar := 5;
+  } else {
+    myVar := 0;
+  }
+}
+
+// expected end assigment: Assert(x) = true, b1(x) = true, b2(x) = false
diff --git a/Test/AbsHoudini/houd3.bpl b/Test/AbsHoudini/houd3.bpl
new file mode 100644
index 00000000..81f11018
--- /dev/null
+++ b/Test/AbsHoudini/houd3.bpl
@@ -0,0 +1,27 @@
+function {:existential true} Assert(x: bool) : bool;
+function {:existential true} b1(x: bool) : bool;
+function {:existential true} b2(x: bool) : bool;
+
+
+var myVar: int;
+
+procedure bar(i:int) 
+modifies myVar;
+ensures b2(myVar>0);
+{
+  call foo(5);
+}
+
+procedure foo (i:int)
+modifies myVar;
+ensures b1(myVar>0);
+ensures Assert(myVar!=-1);
+{
+  if (i>0) {
+    myVar := 5;
+  } else {
+    myVar := 0;
+  }
+}
+
+// expected end assigment: Assert(x) = x, b1(x) = True, b2(x) = True
diff --git a/Test/AbsHoudini/houd4.bpl b/Test/AbsHoudini/houd4.bpl
new file mode 100644
index 00000000..01ee6707
--- /dev/null
+++ b/Test/AbsHoudini/houd4.bpl
@@ -0,0 +1,27 @@
+function {:existential true} Assert() : bool;
+function {:existential true} b1():bool;
+function {:existential true} b2(x:bool):bool;
+function {:existential true} b3(x:bool):bool;
+function {:existential true} b4(x:bool):bool;
+
+var array:[int]int;
+
+procedure foo (i:int)
+requires b2(i > 0);
+ensures b3(array[i] > 0);
+modifies array;
+ensures Assert() || (forall x:int :: {array[x]} x == i || array[x] == old(array)[x]);
+{
+    array[i] := 2 * i;
+}
+
+procedure bar (j:int) returns (result:int)
+requires b4(j > 0);
+modifies array;
+ensures Assert() || (forall x:int :: {array[x]} (!b1() && x == j) || array[x] == old(array)[x]);
+{
+    call foo(j);
+    result := array[j];	
+}
+
+// expected assignment: Assert = false, b1(x) = false, b2(x) = false, b3(x) = false, b4(x) = false
diff --git a/Test/AbsHoudini/houd5.bpl b/Test/AbsHoudini/houd5.bpl
new file mode 100644
index 00000000..afbaa81c
--- /dev/null
+++ b/Test/AbsHoudini/houd5.bpl
@@ -0,0 +1,29 @@
+function {:existential true} b1(x:bool):bool;
+function {:existential true} b2(x:bool):bool;
+function {:existential true} b3(x:bool):bool;
+function {:existential true} b4(x:bool):bool;
+function {:existential true} b5():bool;
+function {:existential true} Assert():bool;
+
+var array:[int]int;
+
+procedure foo (i:int)
+requires b1(i == 0);
+requires b2(i > 0);
+requires b3(i < 0);
+ensures b4(array[i] > 0);
+modifies array;
+ensures Assert() || (forall x:int :: {array[x]} x == i || array[x] == old(array)[x]);
+{
+    array[i] := 2 * i;
+}
+
+procedure bar (j:int) returns (result:int)
+requires b5() || (j > 0);
+modifies array;
+{
+    call foo(j);
+    result := array[j];	
+}
+
+// expected assigment: assert = false, b1(x) = !x, b2(x) = x, b3(x) = !x, b4(x) = x, b5() = false
diff --git a/Test/AbsHoudini/houd6.bpl b/Test/AbsHoudini/houd6.bpl
new file mode 100644
index 00000000..e4927901
--- /dev/null
+++ b/Test/AbsHoudini/houd6.bpl
@@ -0,0 +1,44 @@
+function {:existential true} b1():bool;
+function {:existential true} b2():bool;
+function {:existential true} b3():bool;
+function {:existential true} b4():bool;
+function {:existential true} b5():bool;
+function {:existential true} b6():bool;
+function {:existential true} b7():bool;
+function {:existential true} b8():bool;
+function {:existential true} Assert(): bool;
+
+var array:[int]int;
+
+procedure foo (i:int)
+requires b6() || i < 0;
+requires b5() || i == 0;
+requires b2() || i > 0;
+ensures b3() || array[i] > 0;
+modifies array;
+ensures Assert() || (forall x:int :: {array[x]} x == i || array[x] == old(array)[x]);
+{
+    array[i] := 2 * i;
+}
+
+procedure bar (j:int) returns (result:int)
+requires b8() || j < 0;
+requires b7() || j == 0;
+requires b4() || j > 0;
+modifies array;
+ensures Assert() || (forall x:int :: {array[x]} (x == j) || array[x] == old(array)[x]);
+ensures b1() || array[j] == old(array)[j];
+{
+    call foo(j);
+    result := array[j];	
+}
+
+var p:int;
+
+procedure main() returns (result: int) 
+modifies array;
+{
+  call result:= bar(p);
+}
+
+// expected assigment: Assert -> false, bi->true forall i
diff --git a/Test/AbsHoudini/houd7.bpl b/Test/AbsHoudini/houd7.bpl
new file mode 100644
index 00000000..ef3293db
--- /dev/null
+++ b/Test/AbsHoudini/houd7.bpl
@@ -0,0 +1,35 @@
+function {:existential true} b1():bool;
+function {:existential true} b2():bool;
+function {:existential true} b3():bool;
+function {:existential true} Assert(): bool;
+var myVar: int;
+
+procedure foo(i:int) 
+requires b1() || i>0;
+requires b2() || i==0;
+requires b3() || i<0;
+modifies myVar;
+ensures Assert() || myVar>0;
+{
+  myVar:=5; 
+}
+
+procedure bar(i:int) 
+modifies myVar;
+{
+  call foo(5);
+}
+// expected outcome: Correct
+// expected Assigment: Assert = false, b1->false,b2->true,b3->true
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/Test/AbsHoudini/houd8.bpl b/Test/AbsHoudini/houd8.bpl
new file mode 100644
index 00000000..8be7f3db
--- /dev/null
+++ b/Test/AbsHoudini/houd8.bpl
@@ -0,0 +1,29 @@
+function {:existential true} b1():bool;
+function {:existential true} b2():bool;
+function {:existential true} b3():bool;
+
+var myVar: int;
+
+procedure foo(i:int) 
+modifies myVar;
+ensures b1() || myVar>0;
+ensures b2() || myVar==0;
+ensures b3() || myVar<0;
+{
+  myVar:=5; 
+}
+
+// expected assigment: b1->false,b2->true,b3->true
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/Test/AbsHoudini/runtest.bat b/Test/AbsHoudini/runtest.bat
index 34308e4e..b9816bb9 100644
--- a/Test/AbsHoudini/runtest.bat
+++ b/Test/AbsHoudini/runtest.bat
@@ -3,9 +3,14 @@ setlocal
 
 set BGEXE=..\..\Binaries\Boogie.exe
 
-for %%f in (f1.bpl) do (
+for %%f in (houd1.bpl houd2.bpl houd3.bpl houd4.bpl houd5.bpl houd6.bpl houd7.bpl houd8.bpl houd9.bpl houd10.bpl houd11.bpl houd12.bpl) do (
   echo.
   echo -------------------- %%f --------------------
-  %BGEXE% %* /nologo /noinfer /contractInfer /abstractHoudini:PredicateAbs %%f
+  %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment %%f
 )
 
+for %%f in (test1.bpl test2.bpl test7.bpl test8.bpl test9.bpl test10.bpl) do (
+  echo .
+  echo -------------------- %%f --------------------
+  %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /inlineDepth:1 %%f
+)
diff --git a/Test/AbsHoudini/test1.bpl b/Test/AbsHoudini/test1.bpl
new file mode 100644
index 00000000..e6ce06c9
--- /dev/null
+++ b/Test/AbsHoudini/test1.bpl
@@ -0,0 +1,36 @@
+var g: bool;
+
+procedure foo() 
+modifies g;
+ensures b0 ==> (!old(g) ==> old(g) == g);
+{
+  call AcquireLock();
+  call ReleaseLock();
+}
+
+procedure AcquireLock()
+modifies g;
+ensures b1 ==> old(g) == g;
+{
+  g := true;
+}
+
+procedure ReleaseLock()
+modifies g;
+ensures b2 ==> old(g) == g;
+{
+  g := false;
+}
+
+procedure main()
+modifies g;
+{
+  g := false;
+  call foo();
+  assert !g;
+}
+
+const {:existential true} b0: bool;
+const {:existential true} b1: bool;
+const {:existential true } b2: bool;
+
diff --git a/Test/AbsHoudini/test10.bpl b/Test/AbsHoudini/test10.bpl
new file mode 100644
index 00000000..abb993f7
--- /dev/null
+++ b/Test/AbsHoudini/test10.bpl
@@ -0,0 +1,47 @@
+var sdv_7: int;
+var sdv_21: int;
+const {:existential true} b1: bool;
+const{:existential true}  b2: bool;
+const{:existential true}  b3: bool;
+const{:existential true}  b4: bool;
+
+procedure push(a:int)
+modifies sdv_7, sdv_21;
+{
+   sdv_21 := sdv_7;
+   sdv_7 := a;
+}
+
+procedure pop()
+modifies sdv_7, sdv_21;
+{
+   sdv_7 := sdv_21;
+   havoc sdv_21;
+}
+
+procedure foo()
+modifies sdv_7, sdv_21;
+requires {:candidate} b1 ==> (sdv_7 == 0);
+ensures{:candidate}  b2 ==> (sdv_7 == old(sdv_7));
+{
+   call push(2);
+   call pop();
+   call bar();
+}
+
+procedure bar()
+requires{:candidate} b3 ==> (sdv_7 == 0);
+ensures{:candidate}  b4 ==> (sdv_7 == old(sdv_7));
+modifies sdv_7, sdv_21;
+{
+   call push(1);
+   call pop();
+}
+
+procedure main()
+modifies sdv_7, sdv_21;
+{
+   sdv_7 := 0;
+   call foo();
+}
+
diff --git a/Test/AbsHoudini/test2.bpl b/Test/AbsHoudini/test2.bpl
new file mode 100644
index 00000000..febb28e6
--- /dev/null
+++ b/Test/AbsHoudini/test2.bpl
@@ -0,0 +1,38 @@
+var g: int;
+var h: int;
+
+procedure foo() 
+modifies g, h;
+ensures b0 ==> old(g) == g;
+{
+  call AcquireLock();
+  call ReleaseLock();
+}
+
+procedure AcquireLock()
+modifies g, h;
+ensures b1 ==> old(g) == g;
+{
+  h := g;
+  g := 1;
+}
+
+procedure ReleaseLock()
+modifies g, h;
+ensures b2 ==> old(g) == g;
+{
+  g := h;
+}
+
+procedure main()
+modifies g, h;
+{
+  g := 0;
+  call foo();
+  assert g == 0;
+}
+
+const {:existential true} b0: bool;
+const {:existential true} b1: bool;
+const {:existential true } b2: bool;
+
diff --git a/Test/AbsHoudini/test7.bpl b/Test/AbsHoudini/test7.bpl
new file mode 100644
index 00000000..b5c6a4c6
--- /dev/null
+++ b/Test/AbsHoudini/test7.bpl
@@ -0,0 +1,15 @@
+var g: int;
+
+procedure main() 
+modifies g;
+{
+  g := 0;
+  call foo();
+  assert g == 1;
+}
+
+procedure foo() 
+modifies g;
+{
+  g := g + 1;
+}
\ No newline at end of file
diff --git a/Test/AbsHoudini/test8.bpl b/Test/AbsHoudini/test8.bpl
new file mode 100644
index 00000000..12eab481
--- /dev/null
+++ b/Test/AbsHoudini/test8.bpl
@@ -0,0 +1,21 @@
+var g: int;
+
+procedure main() 
+modifies g;
+{
+  g := 0;
+  call foo();
+  assert g == 1;
+}
+
+procedure {:inline 1} foo() 
+modifies g;
+{
+  call bar();
+}
+
+procedure bar()
+modifies g;
+{
+  g := g + 1;
+}
\ No newline at end of file
diff --git a/Test/AbsHoudini/test9.bpl b/Test/AbsHoudini/test9.bpl
new file mode 100644
index 00000000..24eb66e8
--- /dev/null
+++ b/Test/AbsHoudini/test9.bpl
@@ -0,0 +1,73 @@
+var v1: int;
+var v2: int;
+var v3: int;
+const{:existential true} b1: bool;
+const{:existential true} b2: bool;
+const{:existential true} b3: bool;
+const{:existential true} b4: bool;
+const{:existential true} b5: bool;
+const{:existential true} b6: bool;
+const{:existential true} b7: bool;
+const{:existential true} b8: bool;
+const{:existential true} b9: bool;
+const{:existential true} b10: bool;
+const{:existential true} b11: bool;
+const{:existential true} b12: bool;
+const{:existential true} b13: bool;
+const{:existential true} b14: bool;
+const{:existential true} b15: bool;
+const{:existential true} b16: bool;
+
+procedure push() 
+requires {:candidate} b1 ==> v1 == 0;
+requires {:candidate} b2 ==> v1 == 1;
+ensures  {:candidate} b3 ==> v1 == 0;
+ensures {:candidate}  b4 ==> v1 == 1;
+modifies v1,v2;
+{
+   v2 := v1;
+   v1 := 1;
+}
+
+procedure pop()
+modifies v1,v2;
+requires {:candidate} b5 ==> v1 == 0;
+requires {:candidate} b6 ==> v1 == 1;
+ensures  {:candidate} b7 ==> v1 == 0;
+ensures {:candidate}  b8 ==> v1 == 1;
+{
+   v1 := v2;
+   havoc v2;
+}
+
+procedure foo() 
+modifies v1,v2;
+requires {:candidate} b9 ==> v1 == 0;
+requires {:candidate} b10 ==> v1 == 1;
+ensures  {:candidate} b11 ==> v1 == 0;
+ensures {:candidate}  b12 ==> v1 == 1;
+{
+   call push();
+   call pop();
+}
+
+procedure bar()
+modifies v1,v2;
+requires {:candidate} b13 ==> v1 == 0;
+requires {:candidate} b14 ==> v1 == 1;
+ensures  {:candidate} b15 ==> v1 == 0;
+ensures {:candidate}  b16 ==> v1 == 1;
+{
+   call push();
+   call pop();
+}
+
+procedure main() 
+modifies v1,v2;
+{
+   v1 := 1;
+   call foo();
+   havoc v1;
+   call bar();
+}
+
-- 
cgit v1.2.3