various refactorings related to houdini

6 files changed, 246 insertions, 414 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 9a30401d..1a2af93b 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -429,6 +429,134 @@ namespace Microsoft.Boogie {
       }

     }

 

+    static void ProcessOutcome(VC.VCGen.Outcome outcome, List<Counterexample> errors, string timeIndication,

+                       ref int errorCount, ref int verified, ref int inconclusives, ref int timeOuts, ref int outOfMemories) {

+      switch (outcome) {

+        default:

+          Contract.Assert(false);  // unexpected outcome

+          throw new cce.UnreachableException();

+        case VCGen.Outcome.ReachedBound:

+          Inform(String.Format("{0}verified", timeIndication));

+          Console.WriteLine(string.Format("Stratified Inlining: Reached recursion bound of {0}", CommandLineOptions.Clo.RecursionBound));

+          verified++;

+          break;

+        case VCGen.Outcome.Correct:

+          if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {

+            Inform(String.Format("{0}credible", timeIndication));

+            verified++;

+          }

+          else {

+            Inform(String.Format("{0}verified", timeIndication));

+            verified++;

+          }

+          break;

+        case VCGen.Outcome.TimedOut:

+          timeOuts++;

+          Inform(String.Format("{0}timed out", timeIndication));

+          break;

+        case VCGen.Outcome.OutOfMemory:

+          outOfMemories++;

+          Inform(String.Format("{0}out of memory", timeIndication));

+          break;

+        case VCGen.Outcome.Inconclusive:

+          inconclusives++;

+          Inform(String.Format("{0}inconclusive", timeIndication));

+          break;

+        case VCGen.Outcome.Errors:

+          if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {

+            Inform(String.Format("{0}doomed", timeIndication));

+            errorCount++;

+          } //else {

+          Contract.Assert(errors != null);  // guaranteed by postcondition of VerifyImplementation

+

+              {

+            // BP1xxx: Parsing errors

+            // BP2xxx: Name resolution errors

+            // BP3xxx: Typechecking errors

+            // BP4xxx: Abstract interpretation errors (Is there such a thing?)

+            // BP5xxx: Verification errors

+

+            errors.Sort(new CounterexampleComparer());

+            foreach (Counterexample error in errors) {

+              if (error is CallCounterexample) {

+                CallCounterexample err = (CallCounterexample)error;

+                if (!CommandLineOptions.Clo.ForceBplErrors && err.FailingRequires.ErrorMessage != null) {

+                  ReportBplError(err.FailingRequires, err.FailingRequires.ErrorMessage, true, false);

+                }

+                else {

+                  ReportBplError(err.FailingCall, "Error BP5002: A precondition for this call might not hold.", true, true);

+                  ReportBplError(err.FailingRequires, "Related location: This is the precondition that might not hold.", false, true);

+                }

+                if (CommandLineOptions.Clo.XmlSink != null) {

+                  CommandLineOptions.Clo.XmlSink.WriteError("precondition violation", err.FailingCall.tok, err.FailingRequires.tok, error.Trace);

+                }

+              }

+              else if (error is ReturnCounterexample) {

+                ReturnCounterexample err = (ReturnCounterexample)error;

+                if (!CommandLineOptions.Clo.ForceBplErrors && err.FailingEnsures.ErrorMessage != null) {

+                  ReportBplError(err.FailingEnsures, err.FailingEnsures.ErrorMessage, true, false);

+                }

+                else {

+                  ReportBplError(err.FailingReturn, "Error BP5003: A postcondition might not hold on this return path.", true, true);

+                  ReportBplError(err.FailingEnsures, "Related location: This is the postcondition that might not hold.", false, true);

+                }

+                if (CommandLineOptions.Clo.XmlSink != null) {

+                  CommandLineOptions.Clo.XmlSink.WriteError("postcondition violation", err.FailingReturn.tok, err.FailingEnsures.tok, error.Trace);

+                }

+              }

+              else // error is AssertCounterexample

+                    {

+                AssertCounterexample err = (AssertCounterexample)error;

+                if (err.FailingAssert is LoopInitAssertCmd) {

+                  ReportBplError(err.FailingAssert, "Error BP5004: This loop invariant might not hold on entry.", true, true);

+                  if (CommandLineOptions.Clo.XmlSink != null) {

+                    CommandLineOptions.Clo.XmlSink.WriteError("loop invariant entry violation", err.FailingAssert.tok, null, error.Trace);

+                  }

+                }

+                else if (err.FailingAssert is LoopInvMaintainedAssertCmd) {

+                  // this assertion is a loop invariant which is not maintained

+                  ReportBplError(err.FailingAssert, "Error BP5005: This loop invariant might not be maintained by the loop.", true, true);

+                  if (CommandLineOptions.Clo.XmlSink != null) {

+                    CommandLineOptions.Clo.XmlSink.WriteError("loop invariant maintenance violation", err.FailingAssert.tok, null, error.Trace);

+                  }

+                }

+                else {

+                  if (!CommandLineOptions.Clo.ForceBplErrors && err.FailingAssert.ErrorMessage != null) {

+                    ReportBplError(err.FailingAssert, err.FailingAssert.ErrorMessage, true, false);

+                  }

+                  else if (err.FailingAssert.ErrorData is string) {

+                    ReportBplError(err.FailingAssert, (string)err.FailingAssert.ErrorData, true, true);

+                  }

+                  else {

+                    ReportBplError(err.FailingAssert, "Error BP5001: This assertion might not hold.", true, true);

+                  }

+                  if (CommandLineOptions.Clo.XmlSink != null) {

+                    CommandLineOptions.Clo.XmlSink.WriteError("assertion violation", err.FailingAssert.tok, null, error.Trace);

+                  }

+                }

+              }

+              if (CommandLineOptions.Clo.EnhancedErrorMessages == 1) {

+                foreach (string info in error.relatedInformation) {

+                  Contract.Assert(info != null);

+                  Console.WriteLine("       " + info);

+                }

+              }

+              if (CommandLineOptions.Clo.ErrorTrace > 0) {

+                Console.WriteLine("Execution trace:");

+                error.Print(4);

+              }

+              if (CommandLineOptions.Clo.ModelViewFile != null) {

+                error.PrintModel();

+              }

+              errorCount++;

+            }

+            //}

+            Inform(String.Format("{0}error{1}", timeIndication, errors.Count == 1 ? "" : "s"));

+          }

+              break;

+      }

+    }

+

     /// <summary>

     /// Given a resolved and type checked Boogie program, infers invariants for the program

     /// and then attempts to verify it.  Returns:

@@ -453,30 +581,6 @@ namespace Microsoft.Boogie {
         Microsoft.Boogie.AbstractInterpretation.AbstractInterpretation.RunAbstractInterpretation(program);

       }

 

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

-        inconclusives = outcome.Inconclusives;

-        timeOuts = outcome.TimeOuts;

-        outOfMemories = 0;

-        return PipelineOutcome.Done;

-      }

-

       if (CommandLineOptions.Clo.LoopUnrollCount != -1) {

         program.UnrollLoops(CommandLineOptions.Clo.LoopUnrollCount);

       }

@@ -502,6 +606,40 @@ namespace Microsoft.Boogie {
         return PipelineOutcome.Done;

       }

 

+      #region Run Houdini and verify

+      if (CommandLineOptions.Clo.ContractInfer) {

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

+        Houdini.HoudiniOutcome outcome = houdini.PerformHoudiniInference();

+        if (CommandLineOptions.Clo.PrintAssignment) {

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

+          foreach (var x in outcome.assignment) {

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

+          }

+        }

+        if (CommandLineOptions.Clo.Trace) {

+          int numTrueAssigns = 0;

+          foreach (var x in outcome.assignment) {

+            if (x.Value)

+              numTrueAssigns++;

+          }

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

+        }

+

+        foreach (Houdini.VCGenOutcome x in outcome.implementationOutcomes.Values) {

+          ProcessOutcome(x.outcome, x.errors, "", ref errorCount, ref verified, ref inconclusives, ref timeOuts, ref outOfMemories);

+        }

+        //errorCount = outcome.ErrorCount;

+        //verified = outcome.Verified;

+        //inconclusives = outcome.Inconclusives;

+        //timeOuts = outcome.TimeOuts;

+        //outOfMemories = 0;

+        return PipelineOutcome.Done;

+      }

+      #endregion

+

       #region Verify each implementation

 

       ConditionGeneration vcgen = null;

@@ -541,42 +679,39 @@ namespace Microsoft.Boogie {
 

           VCGen.Outcome outcome;

           try {

-              if (CommandLineOptions.Clo.inferLeastForUnsat != null)

-              {

-                  var svcgen = vcgen as VC.StratifiedVCGen;

-                  Contract.Assert(svcgen != null);

-                  var ss = new HashSet<string>();

-                  foreach (var tdecl in program.TopLevelDeclarations)

-                  {

-                      var c = tdecl as Constant;

-                      if (c == null || !c.Name.StartsWith(CommandLineOptions.Clo.inferLeastForUnsat)) continue;

-                      ss.Add(c.Name);

-                  }

-                  outcome = svcgen.FindLeastToVerify(impl, program, ref ss);

-                  errors = new List<Counterexample>();

-                  Console.Write("Result: ");

-                  foreach (var s in ss)

-                  {

-                      Console.Write("{0} ", s);

-                  }

-                  Console.WriteLine();

+            if (CommandLineOptions.Clo.inferLeastForUnsat != null) {

+              var svcgen = vcgen as VC.StratifiedVCGen;

+              Contract.Assert(svcgen != null);

+              var ss = new HashSet<string>();

+              foreach (var tdecl in program.TopLevelDeclarations) {

+                var c = tdecl as Constant;

+                if (c == null || !c.Name.StartsWith(CommandLineOptions.Clo.inferLeastForUnsat)) continue;

+                ss.Add(c.Name);

               }

-              else

-              {

-                  outcome = vcgen.VerifyImplementation(impl, program, out errors);

+              outcome = svcgen.FindLeastToVerify(impl, program, ref ss);

+              errors = new List<Counterexample>();

+              Console.Write("Result: ");

+              foreach (var s in ss) {

+                Console.Write("{0} ", s);

               }

-          } catch (VCGenException e) {

+              Console.WriteLine();

+            }

+            else {

+              outcome = vcgen.VerifyImplementation(impl, program, out errors);

+            }

+          }

+          catch (VCGenException e) {

             ReportBplError(impl, String.Format("Error BP5010: {0}  Encountered in implementation {1}.", e.Message, impl.Name), true, true);

             errors = null;

             outcome = VCGen.Outcome.Inconclusive;

-          } catch (UnexpectedProverOutputException upo) {

+          }

+          catch (UnexpectedProverOutputException upo) {

             AdvisoryWriteLine("Advisory: {0} SKIPPED because of internal error: unexpected prover output: {1}", impl.Name, upo.Message);

             errors = null;

             outcome = VCGen.Outcome.Inconclusive;

           }

 

           string timeIndication = "";

-

           DateTime end = DateTime.UtcNow;

           TimeSpan elapsed = end - start;

           if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.XmlSink != null) {

@@ -586,130 +721,14 @@ namespace Microsoft.Boogie {
             }

           }

 

-

-          switch (outcome) {

-            default:

-              Contract.Assert(false);  // unexpected outcome

-              throw new cce.UnreachableException();

-            case VCGen.Outcome.ReachedBound:

-              Inform(String.Format("{0}verified", timeIndication));

-              Console.WriteLine(string.Format("Stratified Inlining: Reached recursion bound of {0}", CommandLineOptions.Clo.RecursionBound));

-              verified++;

-              break;

-            case VCGen.Outcome.Correct:

-              if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {

-                Inform(String.Format("{0}credible", timeIndication));

-                verified++;

-              } else {

-                Inform(String.Format("{0}verified", timeIndication));

-                verified++;

+          if (CommandLineOptions.Clo.ExtractLoops && (vcgen is VCGen)) {

+              for (int i = 0; i < errors.Count; i++) {

+                errors[i] = (vcgen as VCGen).extractLoopTrace(errors[i], impl.Name, program, extractLoopMappingInfo);

               }

-              break;

-            case VCGen.Outcome.TimedOut:

-              timeOuts++;

-              Inform(String.Format("{0}timed out", timeIndication));

-              break;

-            case VCGen.Outcome.OutOfMemory:

-              outOfMemories++;

-              Inform(String.Format("{0}out of memory", timeIndication));

-              break;

-            case VCGen.Outcome.Inconclusive:

-              inconclusives++;

-              Inform(String.Format("{0}inconclusive", timeIndication));

-              break;

-            case VCGen.Outcome.Errors:

-              if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {

-                Inform(String.Format("{0}doomed", timeIndication));

-                errorCount++;

-              } //else {

-              Contract.Assert(errors != null);  // guaranteed by postcondition of VerifyImplementation

+          }

 

-              {

-                // BP1xxx: Parsing errors

-                // BP2xxx: Name resolution errors

-                // BP3xxx: Typechecking errors

-                // BP4xxx: Abstract interpretation errors (Is there such a thing?)

-                // BP5xxx: Verification errors

-

-                if (CommandLineOptions.Clo.ExtractLoops && (vcgen is VCGen))

-                {

-                    for (int i = 0; i < errors.Count; i++)

-                    {

-                        errors[i] = (vcgen as VCGen).extractLoopTrace(errors[i], impl.Name, program, extractLoopMappingInfo);

-                    }

-                }

+          ProcessOutcome(outcome, errors, timeIndication, ref errorCount, ref verified, ref inconclusives, ref timeOuts, ref outOfMemories);

 

-                errors.Sort(new CounterexampleComparer());

-                foreach (Counterexample error in errors) {

-                  if (error is CallCounterexample) {

-                    CallCounterexample err = (CallCounterexample)error;

-                    if (!CommandLineOptions.Clo.ForceBplErrors && err.FailingRequires.ErrorMessage != null) {

-                      ReportBplError(err.FailingRequires, err.FailingRequires.ErrorMessage, true, false);

-                    } else {

-                      ReportBplError(err.FailingCall, "Error BP5002: A precondition for this call might not hold.", true, true);

-                      ReportBplError(err.FailingRequires, "Related location: This is the precondition that might not hold.", false, true);

-                    }

-                    if (CommandLineOptions.Clo.XmlSink != null) {

-                      CommandLineOptions.Clo.XmlSink.WriteError("precondition violation", err.FailingCall.tok, err.FailingRequires.tok, error.Trace);

-                    }

-                  } else if (error is ReturnCounterexample) {

-                    ReturnCounterexample err = (ReturnCounterexample)error;

-                    if (!CommandLineOptions.Clo.ForceBplErrors && err.FailingEnsures.ErrorMessage != null) {

-                      ReportBplError(err.FailingEnsures, err.FailingEnsures.ErrorMessage, true, false);

-                    } else {

-                      ReportBplError(err.FailingReturn, "Error BP5003: A postcondition might not hold on this return path.", true, true);

-                      ReportBplError(err.FailingEnsures, "Related location: This is the postcondition that might not hold.", false, true);

-                    }

-                    if (CommandLineOptions.Clo.XmlSink != null) {

-                      CommandLineOptions.Clo.XmlSink.WriteError("postcondition violation", err.FailingReturn.tok, err.FailingEnsures.tok, error.Trace);

-                    }

-                  } else // error is AssertCounterexample

-                    {

-                    AssertCounterexample err = (AssertCounterexample)error;

-                    if (err.FailingAssert is LoopInitAssertCmd) {

-                      ReportBplError(err.FailingAssert, "Error BP5004: This loop invariant might not hold on entry.", true, true);

-                      if (CommandLineOptions.Clo.XmlSink != null) {

-                        CommandLineOptions.Clo.XmlSink.WriteError("loop invariant entry violation", err.FailingAssert.tok, null, error.Trace);

-                      }

-                    } else if (err.FailingAssert is LoopInvMaintainedAssertCmd) {

-                      // this assertion is a loop invariant which is not maintained

-                      ReportBplError(err.FailingAssert, "Error BP5005: This loop invariant might not be maintained by the loop.", true, true);

-                      if (CommandLineOptions.Clo.XmlSink != null) {

-                        CommandLineOptions.Clo.XmlSink.WriteError("loop invariant maintenance violation", err.FailingAssert.tok, null, error.Trace);

-                      }

-                    } else {

-                      if (!CommandLineOptions.Clo.ForceBplErrors && err.FailingAssert.ErrorMessage != null) {

-                        ReportBplError(err.FailingAssert, err.FailingAssert.ErrorMessage, true, false);

-                      } else if (err.FailingAssert.ErrorData is string) {

-                        ReportBplError(err.FailingAssert, (string)err.FailingAssert.ErrorData, true, true);

-                      } else {

-                        ReportBplError(err.FailingAssert, "Error BP5001: This assertion might not hold.", true, true);

-                      }

-                      if (CommandLineOptions.Clo.XmlSink != null) {

-                        CommandLineOptions.Clo.XmlSink.WriteError("assertion violation", err.FailingAssert.tok, null, error.Trace);

-                      }

-                    }

-                  }

-                  if (CommandLineOptions.Clo.EnhancedErrorMessages == 1) {

-                    foreach (string info in error.relatedInformation) {

-                      Contract.Assert(info != null);

-                      Console.WriteLine("       " + info);

-                    }

-                  }

-                  if (CommandLineOptions.Clo.ErrorTrace > 0) {

-                    Console.WriteLine("Execution trace:");

-                    error.Print(4);

-                  }

-                  if (CommandLineOptions.Clo.ModelViewFile != null) {

-                    error.PrintModel();

-                  }

-                  errorCount++;

-                }

-                //}

-                Inform(String.Format("{0}error{1}", timeIndication, errors.Count == 1 ? "" : "s"));

-              }

-              break;

-          }

           if (CommandLineOptions.Clo.XmlSink != null) {

             CommandLineOptions.Clo.XmlSink.WriteEndMethod(outcome.ToString().ToLowerInvariant(), end, elapsed);

           }

@@ -718,6 +737,7 @@ namespace Microsoft.Boogie {
           }

         }

       }

+        

       vcgen.Close();

       cce.NonNull(CommandLineOptions.Clo.TheProverFactory).Close();

 

@@ -726,6 +746,5 @@ namespace Microsoft.Boogie {
 

       return PipelineOutcome.VerificationCompleted;

     }

-

   }

 }

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 42155f45..1a2d7fda 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -389,6 +389,7 @@ namespace Microsoft.Boogie {
     public int /*(0:3)*/ ErrorTrace = 1;

     public bool IntraproceduralInfer = true;

     public bool ContractInfer = false;

+    public bool PrintAssignment = false;

     public int InlineDepth = -1;

     public bool UseUncheckedContracts = false;

     public bool SimplifyLogFileAppend = false;

@@ -830,10 +831,6 @@ namespace Microsoft.Boogie {
           ps.GetNumericArgument(ref EnhancedErrorMessages, 2);

           return true;

 

-        case "contractInfer":

-          ContractInfer = true;

-          return true;

-

         case "inlineDepth":

           ps.GetNumericArgument(ref InlineDepth);

           return true;

@@ -1229,7 +1226,9 @@ namespace Microsoft.Boogie {
               ps.CheckBooleanFlag("monomorphize", ref Monomorphize) ||

               ps.CheckBooleanFlag("useArrayTheory", ref UseArrayTheory) ||

               ps.CheckBooleanFlag("doModSetAnalysis", ref DoModSetAnalysis) ||

-              ps.CheckBooleanFlag("doNotUseLabels", ref UseLabels, false)

+              ps.CheckBooleanFlag("doNotUseLabels", ref UseLabels, false) ||

+              ps.CheckBooleanFlag("contractInfer", ref ContractInfer) ||

+              ps.CheckBooleanFlag("printAssignment", ref PrintAssignment)

               ) {

             // one of the boolean flags matched

             return true;

diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs
index a2bf0304..29357997 100644
--- a/Source/Houdini/Checker.cs
+++ b/Source/Houdini/Checker.cs
@@ -56,12 +56,19 @@ namespace Microsoft.Boogie.Houdini {
       collector.examples.Clear();

       VCExpr vc = checker.VCExprGen.Implies(axiom, conjecture);

 

+      if (CommandLineOptions.Clo.Trace) {

+        Console.WriteLine("Verifying " + descriptiveName);

+      }

       DateTime now = DateTime.UtcNow;

       checker.BeginCheck(descriptiveName, vc, handler);

       WaitHandle.WaitAny(new WaitHandle[] { checker.ProverDone });

       ProverInterface.Outcome proverOutcome = checker.ReadOutcome();

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

+      double queryTime = (DateTime.UtcNow - now).TotalSeconds;

+      proverTime += queryTime;

       numProverQueries++;

+      if (CommandLineOptions.Clo.Trace) {

+        Console.WriteLine("Time taken = " + queryTime);

+      }

 

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

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

diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index 68a8efb6..5ac78731 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -537,25 +537,6 @@ namespace Microsoft.Boogie.Houdini {
       return outcome;

     }

 

-    private ProverInterface.Outcome VerifyCurrent(

-                                        HoudiniSession session,

-                                        HoudiniState current,

-                                        Program program,

-                                        out List<Counterexample> errors,

-                                        out bool exc) {

-      if (current.Implementation != null) {

-        Implementation implementation = current.Implementation;

-        if (vcgen == null)

-          throw new Exception("HdnVCGen not found for implementation: " + implementation.Name);

-

-        ProverInterface.Outcome outcome = TrySpinSameFunc(session, current, program, out errors, out exc);

-        return outcome;

-      }

-      else {

-        throw new Exception("VerifyCurrent has null implementation");

-      }

-    }

-

     private bool IsOutcomeNotHoudini(ProverInterface.Outcome outcome, List<Counterexample> errors) {

       switch (outcome) {

         case ProverInterface.Outcome.Valid:

@@ -651,51 +632,6 @@ namespace Microsoft.Boogie.Houdini {
       }

     }

 

-    private void UpdateWorkList(HoudiniState current,

-                                ProverInterface.Outcome outcome,

-                                List<Counterexample> errors) {

-      Contract.Assume(current.Implementation != null);

-

-      switch (outcome) {

-        case ProverInterface.Outcome.Valid:

-          current.WorkQueue.Dequeue();

-          this.NotifyDequeue();

-          break;

-        case ProverInterface.Outcome.Invalid:

-          Contract.Assume(errors != null);

-          bool dequeue = false;

-          foreach (Counterexample error in errors) {

-            RefutedAnnotation refutedAnnotation = ExtractRefutedAnnotation(error);

-            if (refutedAnnotation != null) {

-              foreach (Implementation implementation in FindImplementationsToEnqueue(refutedAnnotation, current.Implementation)) { AddToWorkList(current, implementation); }

-              UpdateAssignment(current, refutedAnnotation);

-            }

-            else {

-              dequeue = true; //once one non-houdini error is hit dequeue?!

-            }

-          }

-          if (dequeue) {

-            current.WorkQueue.Dequeue();

-            this.NotifyDequeue();

-          }

-          break;

-        case ProverInterface.Outcome.TimeOut:

-          // TODO: reset session instead of blocking timed out funcs?

-          current.addToBlackList(current.Implementation.Name);

-          current.WorkQueue.Dequeue();

-          this.NotifyDequeue();

-          break;

-        case ProverInterface.Outcome.OutOfMemory:

-        case ProverInterface.Outcome.Undetermined:

-          current.WorkQueue.Dequeue();

-          this.NotifyDequeue();

-          break;

-        default:

-          throw new Exception("Unknown vcgen outcome");

-      }

-    }

-

-

     private void AddRelatedToWorkList(HoudiniState current, RefutedAnnotation refutedAnnotation) {

       Contract.Assume(current.Implementation != null);

       foreach (Implementation implementation in FindImplementationsToEnqueue(refutedAnnotation, current.Implementation)) {

@@ -810,102 +746,6 @@ namespace Microsoft.Boogie.Houdini {
       }

     }

 

-    private void PrintBadList(string kind, List<string> list) {

-      if (list.Count != 0) {

-        Console.WriteLine("----------------------------------------");

-        Console.WriteLine("Functions: {0}", kind);

-        foreach (string fname in list) {

-          Console.WriteLine("\t{0}", fname);

-        }

-        Console.WriteLine("----------------------------------------");

-      }

-    }

-

-    private void PrintBadOutcomes(List<string> timeouts, List<string> inconc, List<string> errors) {

-      PrintBadList("TimedOut", timeouts);

-      PrintBadList("Inconclusive", inconc);

-      PrintBadList("Errors", errors);

-    }

-

-    public HoudiniOutcome VerifyProgram() {

-      HoudiniOutcome outcome = VerifyProgramSameFuncFirst();

-      PrintBadOutcomes(outcome.ListOfTimeouts, outcome.ListOfInconclusives, outcome.ListOfErrors);

-      return outcome;

-    }

-

-    // Old main loop

-    public HoudiniOutcome VerifyProgramUnorderedWork() {

-      HoudiniState current = new HoudiniState(BuildWorkList(program), BuildAssignment(houdiniConstants.Keys));

-      this.NotifyStart(program, houdiniConstants.Keys.Count);

-

-      while (current.WorkQueue.Count > 0) {

-        //System.GC.Collect();

-        this.NotifyIteration();

-

-        VCExpr axiom = BuildAxiom(current.Assignment);

-        this.NotifyAssignment(current.Assignment);

-

-        current.Implementation = current.WorkQueue.Peek();

-        this.NotifyImplementation(current.Implementation);

-

-        List<Counterexample> errors;

-        HoudiniSession session;

-        houdiniSessions.TryGetValue(current.Implementation, out session);

-        ProverInterface.Outcome outcome = VerifyUsingAxiom(session, current.Implementation, axiom, out errors);

-        this.NotifyOutcome(outcome);

-

-        UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors);

-        if (IsOutcomeNotHoudini(outcome, errors) && !continueAtError) {

-          current.WorkQueue.Dequeue();

-          this.NotifyDequeue();

-          FlushWorkList(current);

-        }

-        else

-          UpdateWorkList(current, outcome, errors);

-      }

-      this.NotifyEnd(true);

-      current.Outcome.assignment = current.Assignment;

-      return current.Outcome;

-    }

-

-    // New main loop

-    public HoudiniOutcome VerifyProgramSameFuncFirst() {

-      HoudiniState current = new HoudiniState(BuildWorkList(program), BuildAssignment(houdiniConstants.Keys));

-      this.NotifyStart(program, houdiniConstants.Keys.Count);

-

-      while (current.WorkQueue.Count > 0) {

-        bool exceptional = false;

-        //System.GC.Collect();

-        this.NotifyIteration();

-

-        current.Implementation = current.WorkQueue.Peek();

-        this.NotifyImplementation(current.Implementation);

-

-        HoudiniSession session;

-        houdiniSessions.TryGetValue(current.Implementation, out session);

-        List<Counterexample> errors;

-        ProverInterface.Outcome outcome = VerifyCurrent(session, current, program, out errors, out exceptional);

-

-        // updates to worklist already done in VerifyCurrent, unless there was an exception

-        if (exceptional) {

-          this.NotifyOutcome(outcome);

-          UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors);

-          if (IsOutcomeNotHoudini(outcome, errors) && !continueAtError) {

-            current.WorkQueue.Dequeue();

-            this.NotifyDequeue();

-            FlushWorkList(current);

-          }

-          else {

-            UpdateAssignmentWorkList(current, outcome, errors);

-          }

-          exceptional = false;

-        }

-      }

-      this.NotifyEnd(true);

-      current.Outcome.assignment = current.Assignment;

-      return current.Outcome;

-    }

-

     //Clean houdini (Based on "Houdini Spec in Boogie" email 10/22/08

     //Aborts when there is a violation of non-candidate assertion

     //This can be used in eager mode (continueAfterError) by simply making

@@ -1098,67 +938,7 @@ namespace Microsoft.Boogie.Houdini {
       return outcome;

     }

 

-    //version of TryCatchVerify that spins on the same function

-    //as long as the current assignment is changing

-    private ProverInterface.Outcome TrySpinSameFunc(

-                                          HoudiniSession session,

-                                          HoudiniState current,

-                                          Program program,

-                                          out List<Counterexample> errors,

-                                          out bool exceptional) {

-      Contract.Assert(current.Implementation != null);

-      ProverInterface.Outcome outcome;

-      errors = null;

-      outcome = ProverInterface.Outcome.Undetermined;

-      try {

-        bool trySameFunc = true;

-        bool pastFirstIter = false; //see if this new loop is even helping

-

-        do {

-          if (pastFirstIter) {

-            //System.GC.Collect();

-            this.NotifyIteration();

-          }

-

-          VCExpr currentAx = BuildAxiom(current.Assignment);

-          this.NotifyAssignment(current.Assignment);

-

-          outcome = session.Verify(checker, currentAx, out errors);

-          this.NotifyOutcome(outcome);

-

-          DebugRefutedCandidates(current.Implementation, errors);

-          UpdateHoudiniOutcome(current.Outcome, current.Implementation, outcome, errors);

-          if (!continueAtError && IsOutcomeNotHoudini(outcome, errors)) {

-            current.WorkQueue.Dequeue();

-            this.NotifyDequeue();

-            trySameFunc = false;

-            FlushWorkList(current);

-          }

-          else {

-            trySameFunc = UpdateAssignmentWorkList(current, outcome, errors);

-            //reset for the next round

-            errors = null;

-            outcome = ProverInterface.Outcome.Undetermined;

-          }

-          pastFirstIter = true;

-        } while (trySameFunc && current.WorkQueue.Count > 0);

-

-      }

-      catch (VCGenException e) {

-        Contract.Assume(e != null);

-        NotifyException("VCGen");

-        exceptional = true;

-        return outcome;

-      }

-      catch (UnexpectedProverOutputException upo) {

-        Contract.Assume(upo != null);

-        NotifyException("UnexpectedProverOutput");

-        exceptional = true;

-        return outcome;

-      }

-      exceptional = false;

-      return outcome;

-    }

+    

 

     //Similar to TrySpinSameFunc except no Candidate logic

     private ProverInterface.Outcome HoudiniVerifyCurrentAux(

@@ -1191,9 +971,6 @@ namespace Microsoft.Boogie.Houdini {
           this.NotifyAssignment(current.Assignment);

 

           //check the VC with the current assignment

-          if (CommandLineOptions.Clo.Trace) {

-            Console.WriteLine("Verifying " + session.descriptiveName);

-          }

           outcome = session.Verify(checker, currentAx, out errors);

           this.NotifyOutcome(outcome);

 

@@ -1232,10 +1009,26 @@ namespace Microsoft.Boogie.Houdini {
   public enum HoudiniOutcomeKind { Done, FatalError, VerificationCompleted }

 

   public class VCGenOutcome {

-    public ProverInterface.Outcome outcome;

+    public VCGen.Outcome outcome;

     public List<Counterexample> errors;

     public VCGenOutcome(ProverInterface.Outcome outcome, List<Counterexample> errors) {

-      this.outcome = outcome;

+      switch (outcome) {

+        case ProverInterface.Outcome.Invalid:

+          this.outcome = ConditionGeneration.Outcome.Errors;

+          break;

+        case ProverInterface.Outcome.OutOfMemory:

+          this.outcome = ConditionGeneration.Outcome.OutOfMemory;

+          break;

+        case ProverInterface.Outcome.TimeOut:

+          this.outcome = ConditionGeneration.Outcome.TimedOut;

+          break;

+        case ProverInterface.Outcome.Undetermined:

+          this.outcome = ConditionGeneration.Outcome.Inconclusive;

+          break;

+        case ProverInterface.Outcome.Valid:

+          this.outcome = ConditionGeneration.Outcome.Correct;

+          break;

+      }

       this.errors = errors;

     }

   }

@@ -1250,7 +1043,7 @@ namespace Microsoft.Boogie.Houdini {
 

     // statistics 

 

-    private int CountResults(ProverInterface.Outcome outcome) {

+    private int CountResults(VCGen.Outcome outcome) {

       int outcomeCount = 0;

       foreach (VCGenOutcome verifyOutcome in implementationOutcomes.Values) {

         if (verifyOutcome.outcome == outcome)

@@ -1259,7 +1052,7 @@ namespace Microsoft.Boogie.Houdini {
       return outcomeCount;

     }

 

-    private List<string> ListOutcomeMatches(ProverInterface.Outcome outcome) {

+    private List<string> ListOutcomeMatches(VCGen.Outcome outcome) {

       List<string> result = new List<string>();

       foreach (KeyValuePair<string, VCGenOutcome> kvpair in implementationOutcomes) {

         if (kvpair.Value.outcome == outcome)

@@ -1270,37 +1063,37 @@ namespace Microsoft.Boogie.Houdini {
 

     public int ErrorCount {

       get {

-        return CountResults(ProverInterface.Outcome.Invalid);

+        return CountResults(VCGen.Outcome.Errors);

       }

     }

     public int Verified {

       get {

-        return CountResults(ProverInterface.Outcome.Valid);

+        return CountResults(VCGen.Outcome.Correct);

       }

     }

     public int Inconclusives {

       get {

-        return CountResults(ProverInterface.Outcome.Undetermined);

+        return CountResults(VCGen.Outcome.Inconclusive);

       }

     }

     public int TimeOuts {

       get {

-        return CountResults(ProverInterface.Outcome.TimeOut);

+        return CountResults(VCGen.Outcome.TimedOut);

       }

     }

     public List<string> ListOfTimeouts {

       get {

-        return ListOutcomeMatches(ProverInterface.Outcome.TimeOut);

+        return ListOutcomeMatches(VCGen.Outcome.TimedOut);

       }

     }

     public List<string> ListOfInconclusives {

       get {

-        return ListOutcomeMatches(ProverInterface.Outcome.Undetermined);

+        return ListOutcomeMatches(VCGen.Outcome.Inconclusive);

       }

     }

     public List<string> ListOfErrors {

       get {

-        return ListOutcomeMatches(ProverInterface.Outcome.Invalid);

+        return ListOutcomeMatches(VCGen.Outcome.Errors);

       }

     }

   }

diff --git a/Test/houdini/Answer b/Test/houdini/Answer
index 6053b442..d7edbce6 100644
--- a/Test/houdini/Answer
+++ b/Test/houdini/Answer
@@ -9,6 +9,10 @@ Boogie program verifier finished with 1 verified, 0 errors
 Assignment computed by Houdini:

 b1 = False

 b2 = True

+houd2.bpl(12,1): Error BP5003: A postcondition might not hold on this return path.

+houd2.bpl(9,1): Related location: This is the postcondition that might not hold.

+Execution trace:

+    houd2.bpl(11,3): anon0

 

 Boogie program verifier finished with 1 verified, 1 error

 

@@ -72,6 +76,9 @@ Assignment computed by Houdini:
 b1 = True

 b2 = True

 b3 = True

+houd9.bpl(19,3): Error BP5001: This assertion might not hold.

+Execution trace:

+    houd9.bpl(18,9): anon0

 

 Boogie program verifier finished with 0 verified, 1 error

 

@@ -80,11 +87,18 @@ Assignment computed by Houdini:
 b1 = True

 b2 = True

 b3 = True

+houd10.bpl(15,3): Error BP5002: A precondition for this call might not hold.

+houd10.bpl(20,1): Related location: This is the precondition that might not hold.

+Execution trace:

+    houd10.bpl(14,9): anon0

 

 Boogie program verifier finished with 0 verified, 1 error

 

 -------------------- houd11.bpl --------------------

 Assignment computed by Houdini:

+houd11.bpl(8,3): Error BP5001: This assertion might not hold.

+Execution trace:

+    houd11.bpl(7,9): anon0

 

 Boogie program verifier finished with 0 verified, 1 error

 

diff --git a/Test/houdini/runtest.bat b/Test/houdini/runtest.bat
index f0065b0d..b9816bb9 100644
--- a/Test/houdini/runtest.bat
+++ b/Test/houdini/runtest.bat
@@ -6,11 +6,11 @@ set BGEXE=..\..\Binaries\Boogie.exe
 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 %%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 /inlineDepth:1 %%f

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

 )