added some more statistics to houdini

added a coupe more regressions for houdini+inlineDepth

6 files changed, 99 insertions, 1 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 7e2ea87a..ed61b709 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -439,12 +439,18 @@ namespace Microsoft.Boogie {
       if (CommandLineOptions.Clo.ContractInfer) {

         Houdini.Houdini houdini = new Houdini.Houdini(program, true);

         Houdini.HoudiniOutcome outcome = houdini.PerformHoudiniInference();

+        int numTrueAssigns = 0;

         Console.WriteLine("Assignment computed by Houdini:");

         foreach (var x in outcome.assignment) {

           Console.WriteLine(x.Key + " = " + x.Value);

+          if (x.Value)

+            numTrueAssigns++;

         }

         if (CommandLineOptions.Clo.Trace) {

+          Console.WriteLine("Number of true assignments = " + numTrueAssigns);

+          Console.WriteLine("Number of false assignments = " + (outcome.assignment.Count - numTrueAssigns));

           Console.WriteLine("Prover time = " + Houdini.HoudiniSession.proverTime);

+          Console.WriteLine("Number of prover queries = " + Houdini.HoudiniSession.numProverQueries);

         }

         errorCount = outcome.ErrorCount;

         verified = outcome.Verified;

diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs
index b0c8fabf..e36d32ef 100644
--- a/Source/Houdini/Checker.cs
+++ b/Source/Houdini/Checker.cs
@@ -19,6 +19,7 @@ using VC;
 namespace Microsoft.Boogie.Houdini {

   public class HoudiniSession {

     public static double proverTime = 0;

+    public static int numProverQueries = 0;

     private string descriptiveName;

     private VCExpr conjecture;

     private ProverInterface.ErrorHandler handler;

@@ -56,6 +57,7 @@ namespace Microsoft.Boogie.Houdini {
       WaitHandle.WaitAny(new WaitHandle[] { checker.ProverDone });

       ProverInterface.Outcome proverOutcome = checker.ReadOutcome();

       proverTime += (DateTime.Now - now).TotalSeconds;

+      numProverQueries++;

 

       if (proverOutcome == ProverInterface.Outcome.Invalid) {

         Contract.Assume(collector.examples != null);

diff --git a/Test/houdini/Answer b/Test/houdini/Answer
index 60ae7d80..474d1b09 100644
--- a/Test/houdini/Answer
+++ b/Test/houdini/Answer
@@ -100,6 +100,22 @@ b7 = False
 

 Boogie program verifier finished with 1 verified, 0 errors

 .

+-------------------- test1.bpl --------------------

+Assignment computed by Houdini:

+b0 = True

+b1 = False

+b2 = False

+

+Boogie program verifier finished with 4 verified, 0 errors

+.

+-------------------- test2.bpl --------------------

+Assignment computed by Houdini:

+b0 = True

+b1 = False

+b2 = False

+

+Boogie program verifier finished with 4 verified, 0 errors

+.

 -------------------- test7.bpl --------------------

 Assignment computed by Houdini:

 

diff --git a/Test/houdini/runtest.bat b/Test/houdini/runtest.bat
index 40f8cea0..aeffcd12 100644
--- a/Test/houdini/runtest.bat
+++ b/Test/houdini/runtest.bat
@@ -9,7 +9,7 @@ for %%f in (houd1.bpl houd2.bpl houd3.bpl houd4.bpl houd5.bpl houd6.bpl houd7.bp
   %BGEXE% %* /nologo /noinfer /contractInfer %%f

 )

 

-for %%f in (test7.bpl test8.bpl) do (

+for %%f in (test1.bpl test2.bpl test7.bpl test8.bpl) do (

   echo .

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

   %BGEXE% %* /nologo /noinfer /contractInfer /inline:spec /inlineDepth:1 %%f

diff --git a/Test/houdini/test1.bpl b/Test/houdini/test1.bpl
new file mode 100644
index 00000000..e6ce06c9
--- /dev/null
+++ b/Test/houdini/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/houdini/test2.bpl b/Test/houdini/test2.bpl
new file mode 100644
index 00000000..febb28e6
--- /dev/null
+++ b/Test/houdini/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;

+