Nice clean re-implementation of AbstractHoudini. And tests

18 files changed, 566 insertions, 2 deletions

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();

+}

+