AbsHoudini: Added support for quantifiers

8 files changed, 135 insertions, 1 deletions

diff --git a/Test/AbsHoudini/Answer b/Test/AbsHoudini/Answer
index 58da416e..db2f6631 100644
--- a/Test/AbsHoudini/Answer
+++ b/Test/AbsHoudini/Answer
@@ -439,3 +439,51 @@ function {:existential true} {:absdomain "Intervals"} {:inline} b3(x: int) : boo
 }

 

 Boogie program verifier finished with 1 verified, 0 errors

+.

+-------------------- pred5.bpl --------------------

+function {:existential true} {:inline} b1(x: bool) : bool

+{

+  x

+}

+

+Boogie program verifier finished with 1 verified, 0 errors

+.

+-------------------- quant1.bpl --------------------

+function {:existential true} {:absdomain "IA[Intervals]"} {:inline} b1(x: int) : bool

+{

+  x >= 0 && x <= 2

+}

+

+Boogie program verifier finished with 1 verified, 0 errors

+.

+-------------------- quant2.bpl --------------------

+function {:existential true} {:absdomain "Intervals"} {:inline} b1(x: int) : bool

+{

+  x >= 0 && x <= 1

+}

+

+Boogie program verifier finished with 1 verified, 0 errors

+.

+-------------------- quant3.bpl --------------------

+function {:existential true} {:absdomain "Intervals"} {:inline} b1(x: int) : bool

+{

+  x >= 0 && x <= 0

+}

+

+Boogie program verifier finished with 1 verified, 0 errors

+.

+-------------------- quant4.bpl --------------------

+function {:existential true} {:absdomain "IA[HoudiniConst]"} {:inline} b1() : bool

+{

+  true

+}

+

+Boogie program verifier finished with 1 verified, 0 errors

+.

+-------------------- quant5.bpl --------------------

+function {:existential true} {:absdomain "Intervals"} {:inline} b1(x: int) : bool

+{

+  x >= 5 && x <= 5

+}

+

+Boogie program verifier finished with 1 verified, 0 errors

diff --git a/Test/AbsHoudini/pred5.bpl b/Test/AbsHoudini/pred5.bpl
new file mode 100644
index 00000000..6940e820
--- /dev/null
+++ b/Test/AbsHoudini/pred5.bpl
@@ -0,0 +1,24 @@
+function {:existential true} b1(x: bool) : bool;

+

+procedure main() 

+{

+   var i: int;

+   var x: int;

+   var arr: [int] int;

+

+   i := 0;

+

+   while(*) 

+     invariant b1((i >= 0) && (forall j: int :: (0 <= j && j < i) ==> arr[j] == 0));

+   {

+       havoc x;

+       assume x == 0;

+

+       arr[i] := x;

+       i := i + 1;

+   }

+

+   havoc x;

+   assume x >= 0 && x < i;

+   assert b1(arr[x] == 0);

+}

diff --git a/Test/AbsHoudini/quant1.bpl b/Test/AbsHoudini/quant1.bpl
new file mode 100644
index 00000000..e12525b6
--- /dev/null
+++ b/Test/AbsHoudini/quant1.bpl
@@ -0,0 +1,7 @@
+function {:existential true} {:absdomain "IA[Intervals]"} b1(x: int) : bool;

+

+procedure foo ()

+{

+  assert (forall x: int :: (0 <= x && x <= 2) ==> b1(x));

+}

+

diff --git a/Test/AbsHoudini/quant2.bpl b/Test/AbsHoudini/quant2.bpl
new file mode 100644
index 00000000..5a491877
--- /dev/null
+++ b/Test/AbsHoudini/quant2.bpl
@@ -0,0 +1,24 @@
+function {:existential true} {:absdomain "Intervals"} b1(x: int) : bool;

+

+procedure main() 

+{

+   var i: int;

+   var x: int;

+   var arr: [int] int;

+

+   i := 0;

+

+   while(*) 

+     invariant (i >= 0) && (forall j: int :: (0 <= j && j < i) ==> b1(arr[j]));

+   {

+       havoc x;

+       assume x == 0 || x == 1;

+

+       arr[i] := x;

+       i := i + 1;

+   }

+

+   havoc x;

+   assume x >= 0 && x < i;

+   assert arr[x] == 0 || arr[x] == 1;

+}

diff --git a/Test/AbsHoudini/quant3.bpl b/Test/AbsHoudini/quant3.bpl
new file mode 100644
index 00000000..cc0ef79e
--- /dev/null
+++ b/Test/AbsHoudini/quant3.bpl
@@ -0,0 +1,7 @@
+function {:existential true} {:absdomain "Intervals"} b1(x: int) : bool;

+

+procedure foo ()

+{

+  assert (exists x: int :: (0 <= x && x <= 2) && b1(x));

+}

+

diff --git a/Test/AbsHoudini/quant4.bpl b/Test/AbsHoudini/quant4.bpl
new file mode 100644
index 00000000..55947f1f
--- /dev/null
+++ b/Test/AbsHoudini/quant4.bpl
@@ -0,0 +1,7 @@
+function {:existential true} {:absdomain "IA[HoudiniConst]"} b1() : bool;

+

+procedure foo ()

+{

+  assert (exists x: int :: (0 <= x && x <= 2) && b1());

+}

+

diff --git a/Test/AbsHoudini/quant5.bpl b/Test/AbsHoudini/quant5.bpl
new file mode 100644
index 00000000..dfc44e47
--- /dev/null
+++ b/Test/AbsHoudini/quant5.bpl
@@ -0,0 +1,11 @@
+function {:existential true} {:absdomain "Intervals"} b1(x: int) : bool;

+

+procedure foo ()

+{

+  var arr: [int] int;

+  assume (forall x: int :: arr[x] == 0);

+  arr[5] := 1;

+

+  assert (exists x: int :: arr[x] == 1 && b1(x));

+}

+

diff --git a/Test/AbsHoudini/runtest.bat b/Test/AbsHoudini/runtest.bat
index 0bc74dfc..4d70be0e 100644
--- a/Test/AbsHoudini/runtest.bat
+++ b/Test/AbsHoudini/runtest.bat
@@ -15,8 +15,14 @@ for %%f in (test1.bpl test2.bpl test7.bpl test8.bpl test9.bpl test10.bpl) do (
   %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /inlineDepth:1  /abstractHoudini:IA[ConstantProp] %%f

 )

 

-for %%f in (pred1.bpl pred2.bpl pred3.bpl pred4.bpl) do (

+for %%f in (pred1.bpl pred2.bpl pred3.bpl pred4.bpl pred5.bpl) do (

   echo .

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

   %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /inlineDepth:1  /abstractHoudini:PredicateAbs %%f

 )

+

+for %%f in (quant1.bpl quant2.bpl quant3.bpl quant4.bpl quant5.bpl) do (

+  echo .

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

+  %BGEXE% %* /nologo /noinfer /contractInfer /printAssignment /abstractHoudini:HoudiniConst /z3opt:MBQI=true %%f

+)