further changes for making houdini work

5 files changed, 132 insertions, 219 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 35c0832a..82c864d5 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -431,7 +431,17 @@ namespace Microsoft.Boogie {
 

       if (CommandLineOptions.Clo.ContractInfer) {

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

-        houdini.PerformHoudiniInference();

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

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

+        foreach (var x in outcome.assignment) {

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

+        }

+        errorCount = outcome.ErrorCount;

+        verified = outcome.Verified;

+        inconclusives = outcome.Inconclusives;

+        timeOuts = outcome.TimeOuts;

+        outOfMemories = 0;

+        return PipelineOutcome.Done;

       }

 

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

diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs
index 294f5d1b..437dbc98 100644
--- a/Source/Houdini/Checker.cs
+++ b/Source/Houdini/Checker.cs
@@ -16,84 +16,29 @@ using System.Threading;
 using VC;

 

 namespace Microsoft.Boogie.Houdini {

-  class HoudiniChecker {

-    private Stack<VCExpr> axioms = new Stack<VCExpr>();

+  public class HoudiniVCGen : VCGen {

     private Checker checker;

     private string descriptiveName;

     private VCExpr conjecture;

     private ProverInterface.ErrorHandler handler;

+    CounterexampleCollector collector;

 

-    internal HoudiniChecker(Checker checker, string _descriptiveName, VCExpr _vc, ProverInterface.ErrorHandler _handler) 

-    {

-      Contract.Requires(checker.TheoremProver != null);

-      Contract.Requires(checker.TheoremProver is Z3ProcessTheoremProver);

-      this.checker = checker;

-      this.descriptiveName = _descriptiveName;

-      this.conjecture = _vc;

-      this.handler = _handler;

-    }

-    

-    public void PushAxiom(Axiom axiom) {

-      DeclFreeProverContext proverContext = (DeclFreeProverContext) checker.TheoremProver.Context;

-      VCExpr vc = proverContext.BoogieExprTranslator.Translate(axiom.Expr);

-      axioms.Push(vc);

-    }

-

-    public void Pop() {

-      axioms.Pop();

-    }    

-

-    private VCExpr BuildVCAxioms(Stack<VCExpr> axioms) 

-    {

-      Contract.Requires(axioms.Count > 0);

-      VCExpr vc_axioms = null;

-      foreach (VCExpr axiom in axioms) {

-        if (vc_axioms == null)

-          vc_axioms = axiom;

-        else

-          vc_axioms = checker.VCExprGen.And(vc_axioms, axiom);

-      }

-      return vc_axioms;

-    }

-    

-    public void Check() 

-    {

-      Contract.Assert (descriptiveName != null);

-      Contract.Assert (conjecture != null);

-      Contract.Assert (handler != null);

-      outcome = ProverInterface.Outcome.Undetermined;

-      

-      VCExpr vc;

-      if (axioms.Count > 0) {

-        VCExpr vc_axioms = BuildVCAxioms(axioms);

-        vc = checker.VCExprGen.Implies(vc_axioms, conjecture);

-      }

-      else {

-        vc = conjecture;

+    public VCExpressionGenerator VCExprGenerator {

+      get {

+        return checker.VCExprGen;

       }

-      checker.BeginCheck(descriptiveName, vc, handler);

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

     }

-   

-    private ProverInterface.Outcome outcome;

 

-    public ProverInterface.Outcome ReadOutcome()

-    {

-      try {

-        outcome = checker.ReadOutcome();

-      } catch (UnexpectedProverOutputException e) {

-        throw e;

+    public Boogie2VCExprTranslator BooogieExprTranslator {

+      get {

+        DeclFreeProverContext proverContext = (DeclFreeProverContext)checker.TheoremProver.Context;

+        return proverContext.BoogieExprTranslator;

       }

-      return outcome;

     }

-  }

 

-  public class HoudiniVCGen : VCGen {

-    private HoudiniChecker hdnChecker;

-    CounterexampleCollector collector;

-

-    public HoudiniVCGen(Program program, Implementation impl, string logFilePath, bool appendLogFile)

-      : base(program, logFilePath, appendLogFile) {

+    public HoudiniVCGen(Program program, Implementation impl, string logFilePath, bool appendLogFile) 

+    : base(program, logFilePath, appendLogFile) {

+      descriptiveName = impl.Name;

       collector = new CounterexampleCollector();

       collector.OnProgress("HdnVCGen", 0, 0, 0.0);

       if (CommandLineOptions.Clo.SoundnessSmokeTest) {

@@ -104,37 +49,28 @@ namespace Microsoft.Boogie.Houdini {
       ModelViewInfo mvInfo;

       Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = PassifyImpl(impl, program, out mvInfo);

       Hashtable/*<int, Absy!>*/ label2absy;

-      Checker checker = new Checker(this, program, this.logFilePath, this.appendLogFile, impl, CommandLineOptions.Clo.ProverKillTime);

-      VCExpr vc = GenerateVC(impl, null, out label2absy, checker);

+      checker = new Checker(this, program, logFilePath, appendLogFile, impl, CommandLineOptions.Clo.ProverKillTime);

+      if (!(checker.TheoremProver is Z3ProcessTheoremProver)) {

+        throw new Exception("HdnChecker only works with z3");

+      }

+      conjecture = GenerateVC(impl, null, out label2absy, checker);

 

-      ErrorReporter reporter;

       if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) {

-        reporter = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, incarnationOriginMap, collector, mvInfo, null, checker.TheoremProver.Context, program);

+        handler = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, incarnationOriginMap, collector, mvInfo, implName2LazyInliningInfo, checker.TheoremProver.Context, program);

       }

       else {

-        reporter = new ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, incarnationOriginMap, collector, mvInfo, null, checker.TheoremProver.Context, program);

+        handler = new ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, incarnationOriginMap, collector, mvInfo, implName2LazyInliningInfo, checker.TheoremProver.Context, program);

       }

-      if (checker.TheoremProver is Z3ProcessTheoremProver)

-        this.hdnChecker = new HoudiniChecker(checker, impl.Name, vc, reporter);

-      else

-        throw new Exception("HdnChecker only works with z3");

     }

 

-    public void PushAxiom(Axiom axiom) {

-      this.hdnChecker.PushAxiom(axiom);

-    }

-

-    public void Pop() {

-      hdnChecker.Pop();

-    }

-

-    public Outcome Verify(out List<Counterexample> errors) {

+    public ProverInterface.Outcome Verify(VCExpr axiom, out List<Counterexample> errors) {

       collector.examples.Clear();

-      hdnChecker.Check();

-      ProverInterface.Outcome proverOutcome;

-      proverOutcome = hdnChecker.ReadOutcome();

-      Outcome verifyOutcome = ReadOutcome(proverOutcome);

-      if (verifyOutcome == Outcome.Errors) {

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

+      checker.BeginCheck(descriptiveName, vc, handler);

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

+

+      ProverInterface.Outcome proverOutcome = checker.ReadOutcome();

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

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

         if (collector.examples.Count == 0) {

           string memStr = System.Convert.ToString(System.GC.GetTotalMemory(false));

@@ -147,24 +83,8 @@ namespace Microsoft.Boogie.Houdini {
       else {

         errors = null;

       }

-      return verifyOutcome;

-    }

-

-    private Outcome ReadOutcome(ProverInterface.Outcome proverOutcome) {

-      switch (proverOutcome) {

-        case ProverInterface.Outcome.Valid:

-          return Outcome.Correct;

-        case ProverInterface.Outcome.Invalid:

-          return Outcome.Errors;

-        case ProverInterface.Outcome.TimeOut:

-          return Outcome.TimedOut;

-        case ProverInterface.Outcome.Undetermined:

-          return Outcome.Inconclusive;

-        default:

-          throw new Exception("Unknown Prover Interface outcome while reading outcome.");

-      }

+      return proverOutcome;

     }

 

   }

-  

 }
\ No newline at end of file
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index 1efc0e91..714ecd3b 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -42,7 +42,7 @@ namespace Microsoft.Boogie.Houdini {
     public virtual void UpdateIteration() { }

     public virtual void UpdateImplementation(Implementation implementation) { }

     public virtual void UpdateAssignment(Dictionary<string, bool> assignment) { }

-    public virtual void UpdateOutcome(VCGen.Outcome outcome) { }

+    public virtual void UpdateOutcome(ProverInterface.Outcome outcome) { }

     public virtual void UpdateEnqueue(Implementation implementation) { }

     public virtual void UpdateDequeue() { }

     public virtual void UpdateConstant(string constantName) { }

@@ -108,7 +108,7 @@ namespace Microsoft.Boogie.Houdini {
     public override void UpdateImplementation(Implementation implementation) {

       curImp = implementation;

     }

-    public override void UpdateOutcome(VCGen.Outcome o) {

+    public override void UpdateOutcome(ProverInterface.Outcome o) {

       Contract.Assert(curImp != null);

       DateTime endT = DateTime.Now;

       times.AddTime(curImp.Name, (endT - startT).TotalMilliseconds); // assuming names are unique

@@ -155,7 +155,7 @@ namespace Microsoft.Boogie.Houdini {
       wr.WriteLine(");");

       wr.Flush();

     }

-    public override void UpdateOutcome(VCGen.Outcome outcome) {

+    public override void UpdateOutcome(ProverInterface.Outcome outcome) {

       wr.WriteLine("analysis outcome :" + outcome);

       wr.Flush();

     }

@@ -221,7 +221,7 @@ namespace Microsoft.Boogie.Houdini {
     protected void NotifyAssignment(Dictionary<string, bool> assignment) {

       Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateAssignment(assignment); });

     }

-    protected void NotifyOutcome(VCGen.Outcome outcome) {

+    protected void NotifyOutcome(ProverInterface.Outcome outcome) {

       Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateOutcome(outcome); });

     }

     protected void NotifyEnqueue(Implementation implementation) {

@@ -300,15 +300,19 @@ namespace Microsoft.Boogie.Houdini {
     }

 

     private Graph<Implementation> BuildCallGraph() {

+      Graph<Implementation> callGraph = new Graph<Implementation>();

       Dictionary<Procedure, HashSet<Implementation>> procToImpls = new Dictionary<Procedure, HashSet<Implementation>>();

       foreach (Declaration decl in program.TopLevelDeclarations) {

+        Procedure proc = decl as Procedure;

+        if (proc == null) continue;

+        procToImpls[proc] = new HashSet<Implementation>();

+      } 

+      foreach (Declaration decl in program.TopLevelDeclarations) {

         Implementation impl = decl as Implementation;

         if (impl == null) continue;

-        if (!procToImpls.ContainsKey(impl.Proc))

-          procToImpls[impl.Proc] = new HashSet<Implementation>();

+        callGraph.AddSource(impl);

         procToImpls[impl.Proc].Add(impl);

       }

-      Graph<Implementation> callGraph = new Graph<Implementation>();

       foreach (Declaration decl in program.TopLevelDeclarations) {

         Implementation impl = decl as Implementation;

         if (impl == null) continue;

@@ -350,21 +354,24 @@ namespace Microsoft.Boogie.Houdini {
       return false;

     }

 

-    private Axiom BuildAxiom(Dictionary<string, bool> currentAssignment, Boogie2VCExprTranslator exprTranslator) {

-      Expr expr = new LiteralExpr(Token.NoToken, true);

-      expr.Type = Type.Bool;

+    private VCExpr BuildAxiom(HoudiniVCGen vcgen, Dictionary<string, bool> currentAssignment) {

+      Boogie2VCExprTranslator exprTranslator = vcgen.BooogieExprTranslator;

+      VCExpressionGenerator exprGen = vcgen.VCExprGenerator;

+

+      VCExpr expr = VCExpressionGenerator.True;

       foreach (KeyValuePair<string, bool> kv in currentAssignment) {

         IdentifierExpr constantExpr;

         houdiniConstants.TryGetValue(kv.Key, out constantExpr);

         Contract.Assume(constantExpr != null);

-        Expr valueExpr = new LiteralExpr(Token.NoToken, kv.Value);

-        valueExpr.Type = Type.Bool;

-        Expr constantAssignment = Expr.Binary(Token.NoToken, BinaryOperator.Opcode.Eq, constantExpr, valueExpr);

-        constantAssignment.Type = Type.Bool;

-        expr = Expr.Binary(Token.NoToken, BinaryOperator.Opcode.And, expr, constantAssignment);

-        expr.Type = Type.Bool;

+        VCExprVar exprVar = exprTranslator.LookupVariable(constantExpr.Decl);

+        if (kv.Value) {

+          expr = exprGen.And(expr, exprVar);

+        }

+        else {

+          expr = exprGen.And(expr, exprGen.Not(exprVar));

+        }

       }

-      return new Axiom(Token.NoToken, expr);

+      return expr;

     }

 

     private Dictionary<string, bool> BuildAssignment(Dictionary<string, IdentifierExpr>.KeyCollection constants) {

@@ -374,20 +381,18 @@ namespace Microsoft.Boogie.Houdini {
       return initial;

     }

 

-    private VCGen.Outcome VerifyUsingAxiom(Implementation implementation, Axiom axiom, out List<Counterexample> errors) {

+    private ProverInterface.Outcome VerifyUsingAxiom(Implementation implementation, VCExpr axiom, out List<Counterexample> errors) {

       HoudiniVCGen vcgen;

       vcgenSessions.TryGetValue(implementation, out vcgen);

       if (vcgen == null)

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

-      vcgen.PushAxiom(axiom);

-      VCGen.Outcome outcome = TryCatchVerify(vcgen, out errors);

-      vcgen.Pop();

+      ProverInterface.Outcome outcome = TryCatchVerify(vcgen, axiom, out errors);

       return outcome;

     }

 

     // the main procedure that checks a procedure and updates the

     // assignment and the worklist

-    private VCGen.Outcome HoudiniVerifyCurrent(HoudiniState current,

+    private ProverInterface.Outcome HoudiniVerifyCurrent(HoudiniState current,

                                         Program program,

                                         out List<Counterexample> errors,

                                         out bool exc) {

@@ -400,11 +405,11 @@ namespace Microsoft.Boogie.Houdini {
       if (vcgen == null)

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

 

-      VCGen.Outcome outcome = HoudiniVerifyCurrentAux(current, program, vcgen, out errors, out exc);

+      ProverInterface.Outcome outcome = HoudiniVerifyCurrentAux(current, program, vcgen, out errors, out exc);

       return outcome;

     }

 

-    private VCGen.Outcome VerifyCurrent(HoudiniState current,

+    private ProverInterface.Outcome VerifyCurrent(HoudiniState current,

                                         Program program,

                                         out List<Counterexample> errors,

                                         out bool exc) {

@@ -415,7 +420,7 @@ namespace Microsoft.Boogie.Houdini {
         if (vcgen == null)

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

 

-        VCGen.Outcome outcome = TrySpinSameFunc(current, program, vcgen, out errors, out exc);

+        ProverInterface.Outcome outcome = TrySpinSameFunc(current, program, vcgen, out errors, out exc);

         return outcome;

       }

       else {

@@ -423,37 +428,32 @@ namespace Microsoft.Boogie.Houdini {
       }

     }

 

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

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

       switch (outcome) {

-        case VCGen.Outcome.Correct:

+        case ProverInterface.Outcome.Valid:

           return false;

-        case VCGen.Outcome.Errors:

+        case ProverInterface.Outcome.Invalid:

           Contract.Assume(errors != null);

           foreach (Counterexample error in errors) {

             if (ExtractRefutedAnnotation(error) == null)

               return true;

           }

           return false;

-        case VCGen.Outcome.TimedOut:

-        case VCGen.Outcome.Inconclusive:

         default:

           return true;

       }

     }

 

     // returns true if at least one of the violations is non-candidate

-    private bool AnyNonCandidateViolation(VCGen.Outcome outcome, List<Counterexample> errors) {

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

       switch (outcome) {

-        case VCGen.Outcome.Errors:

+        case ProverInterface.Outcome.Invalid:

           Contract.Assert(errors != null);

           foreach (Counterexample error in errors) {

             if (ExtractRefutedAnnotation(error) == null)

               return true;

           }

           return false;

-        case VCGen.Outcome.Correct:

-        case VCGen.Outcome.TimedOut:

-        case VCGen.Outcome.Inconclusive:

         default:

           return false;

       }

@@ -464,23 +464,20 @@ namespace Microsoft.Boogie.Houdini {
     // Record most current Non-Candidate errors found by Boogie, etc.

     private void UpdateHoudiniOutcome(HoudiniOutcome houdiniOutcome,

                                       Implementation implementation,

-                                      VCGen.Outcome verificationOutcome,

+                                      ProverInterface.Outcome verificationOutcome,

                                       List<Counterexample> errors) {

       string implName = implementation.ToString();

       houdiniOutcome.implementationOutcomes.Remove(implName);

       List<Counterexample> nonCandidateErrors = new List<Counterexample>();

 

       switch (verificationOutcome) {

-        case VCGen.Outcome.Errors:

+        case ProverInterface.Outcome.Invalid:

           Contract.Assume(errors != null);

           foreach (Counterexample error in errors) {

             if (ExtractRefutedAnnotation(error) == null)

               nonCandidateErrors.Add(error);

           }

           break;

-        case VCGen.Outcome.TimedOut:

-        case VCGen.Outcome.Correct:

-        case VCGen.Outcome.Inconclusive:

         default:

           break;

       }

@@ -489,7 +486,9 @@ namespace Microsoft.Boogie.Houdini {
 

     private void FlushWorkList(HoudiniState current) {

       this.NotifyFlushStart();

-      Axiom axiom = BuildAxiom(current.Assignment);

+      HoudiniVCGen vcgen;

+      vcgenSessions.TryGetValue(current.Implementation, out vcgen);

+      VCExpr axiom = BuildAxiom(vcgen, current.Assignment);

       while (current.WorkList.Count > 0) {

         this.NotifyIteration();

 

@@ -497,7 +496,7 @@ namespace Microsoft.Boogie.Houdini {
         this.NotifyImplementation(current.Implementation);

 

         List<Counterexample> errors;

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

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

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

         this.NotifyOutcome(outcome);

 

@@ -522,16 +521,16 @@ namespace Microsoft.Boogie.Houdini {
     }

 

     private void UpdateWorkList(HoudiniState current,

-                                VCGen.Outcome outcome,

+                                ProverInterface.Outcome outcome,

                                 List<Counterexample> errors) {

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

 

       switch (outcome) {

-        case VCGen.Outcome.Correct:

+        case ProverInterface.Outcome.Valid:

           current.WorkList.Dequeue();

           this.NotifyDequeue();

           break;

-        case VCGen.Outcome.Errors:

+        case ProverInterface.Outcome.Invalid:

           Contract.Assume(errors != null);

           bool dequeue = false;

           foreach (Counterexample error in errors) {

@@ -549,14 +548,14 @@ namespace Microsoft.Boogie.Houdini {
             this.NotifyDequeue();

           }

           break;

-        case VCGen.Outcome.TimedOut:

+        case ProverInterface.Outcome.TimeOut:

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

           current.addToBlackList(current.Implementation.Name);

           current.WorkList.Dequeue();

           this.NotifyDequeue();

           break;

-        case VCGen.Outcome.OutOfMemory:

-        case VCGen.Outcome.Inconclusive:

+        case ProverInterface.Outcome.OutOfMemory:

+        case ProverInterface.Outcome.Undetermined:

           current.WorkList.Dequeue();

           this.NotifyDequeue();

           break;

@@ -577,16 +576,16 @@ namespace Microsoft.Boogie.Houdini {
     // Updates the worklist and current assignment

     // @return true if the current function is kept on the queue

     private bool UpdateAssignmentWorkList(HoudiniState current,

-                                          VCGen.Outcome outcome,

+                                          ProverInterface.Outcome outcome,

                                           List<Counterexample> errors) {

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

       bool dequeue = true;

 

       switch (outcome) {

-        case VCGen.Outcome.Correct:

+        case ProverInterface.Outcome.Valid:

           //yeah, dequeue

           break;

-        case VCGen.Outcome.Errors:

+        case ProverInterface.Outcome.Invalid:

           Contract.Assume(errors != null);

           foreach (Counterexample error in errors) {

             RefutedAnnotation refutedAnnotation = ExtractRefutedAnnotation(error);

@@ -598,12 +597,12 @@ namespace Microsoft.Boogie.Houdini {
           }

           break;

 

-        case VCGen.Outcome.TimedOut:

+        case ProverInterface.Outcome.TimeOut:

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

           current.addToBlackList(current.Implementation.Name);

           break;

-        case VCGen.Outcome.Inconclusive:

-        case VCGen.Outcome.OutOfMemory:

+        case ProverInterface.Outcome.Undetermined:

+        case ProverInterface.Outcome.OutOfMemory:

           break;

         default:

           throw new Exception("Unknown vcgen outcome");

@@ -679,18 +678,22 @@ namespace Microsoft.Boogie.Houdini {
       HoudiniState current = new HoudiniState(BuildWorkList(program), BuildAssignment(houdiniConstants.Keys));

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

 

+      

+

       while (current.WorkList.Count > 0) {

         System.GC.Collect();

         this.NotifyIteration();

 

-        Axiom axiom = BuildAxiom(current.Assignment);

+        HoudiniVCGen vcgen;

+        vcgenSessions.TryGetValue(current.Implementation, out vcgen);

+        VCExpr axiom = BuildAxiom(vcgen, current.Assignment);

         this.NotifyAssignment(current.Assignment);

 

         current.Implementation = current.WorkList.Peek();

         this.NotifyImplementation(current.Implementation);

 

         List<Counterexample> errors;

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

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

         this.NotifyOutcome(outcome);

 

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

@@ -721,7 +724,7 @@ namespace Microsoft.Boogie.Houdini {
         this.NotifyImplementation(current.Implementation);

 

         List<Counterexample> errors;

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

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

 

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

         if (exceptional) {

@@ -762,7 +765,7 @@ namespace Microsoft.Boogie.Houdini {
         this.NotifyImplementation(current.Implementation);

 

         List<Counterexample> errors;

-        VCGen.Outcome outcome = HoudiniVerifyCurrent(current, program, out errors, out exceptional);

+        ProverInterface.Outcome outcome = HoudiniVerifyCurrent(current, program, out errors, out exceptional);

 

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

         if (exceptional) {

@@ -914,36 +917,35 @@ namespace Microsoft.Boogie.Houdini {
       return null;

     }

 

-    private VCGen.Outcome TryCatchVerify(HoudiniVCGen vcgen, out List<Counterexample> errors) {

-      VCGen.Outcome outcome;

+    private ProverInterface.Outcome TryCatchVerify(HoudiniVCGen vcgen, VCExpr axiom, out List<Counterexample> errors) {

+      ProverInterface.Outcome outcome;

       try {

-        outcome = vcgen.Verify(out errors);

+        outcome = vcgen.Verify(axiom, out errors);

       }

       catch (VCGenException e) {

         Contract.Assume(e != null);

         errors = null;

-        outcome = VCGen.Outcome.Inconclusive;

+        outcome = ProverInterface.Outcome.Undetermined;

       }

       catch (UnexpectedProverOutputException upo) {

         Contract.Assume(upo != null);

         errors = null;

-        outcome = VCGen.Outcome.Inconclusive;

+        outcome = ProverInterface.Outcome.Undetermined;

       }

       return outcome;

     }

 

     //version of TryCatchVerify that spins on the same function

     //as long as the current assignment is changing

-    private VCGen.Outcome TrySpinSameFunc(HoudiniState current,

+    private ProverInterface.Outcome TrySpinSameFunc(HoudiniState current,

                                           Program program,

                                           HoudiniVCGen vcgen,

                                           out List<Counterexample> errors,

                                           out bool exceptional) {

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

-      VCGen.Outcome outcome;

-      bool pushed = false;

+      ProverInterface.Outcome outcome;

       errors = null;

-      outcome = VCGen.Outcome.Inconclusive;

+      outcome = ProverInterface.Outcome.Undetermined;

       try {

         bool trySameFunc = true;

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

@@ -953,14 +955,12 @@ namespace Microsoft.Boogie.Houdini {
             System.GC.Collect();

             this.NotifyIteration();

           }

-          Axiom currentAx = BuildAxiom(current.Assignment);

+

+          this.vcgenSessions.TryGetValue(current.Implementation, out vcgen);

+          VCExpr currentAx = BuildAxiom(vcgen, current.Assignment);

           this.NotifyAssignment(current.Assignment);

 

-          vcgen.PushAxiom(currentAx);

-          pushed = true;

-          outcome = vcgen.Verify(out errors);

-          vcgen.Pop();

-          pushed = false;

+          outcome = vcgen.Verify(currentAx, out errors);

           this.NotifyOutcome(outcome);

 

           DebugRefutedCandidates(current.Implementation, errors);

@@ -975,7 +975,7 @@ namespace Microsoft.Boogie.Houdini {
             trySameFunc = UpdateAssignmentWorkList(current, outcome, errors);

             //reset for the next round

             errors = null;

-            outcome = VCGen.Outcome.Inconclusive;

+            outcome = ProverInterface.Outcome.Undetermined;

           }

           pastFirstIter = true;

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

@@ -983,18 +983,12 @@ namespace Microsoft.Boogie.Houdini {
       }

       catch (VCGenException e) {

         Contract.Assume(e != null);

-        if (pushed) {

-          vcgen.Pop(); // what if session is dead?

-        }

         NotifyException("VCGen");

         exceptional = true;

         return outcome;

       }

       catch (UnexpectedProverOutputException upo) {

         Contract.Assume(upo != null);

-        if (pushed) {

-          vcgen.Pop();

-        }

         NotifyException("UnexpectedProverOutput");

         exceptional = true;

         return outcome;

@@ -1004,16 +998,15 @@ namespace Microsoft.Boogie.Houdini {
     }

 

     //Similar to TrySpinSameFunc except no Candidate logic

-    private VCGen.Outcome HoudiniVerifyCurrentAux(HoudiniState current,

+    private ProverInterface.Outcome HoudiniVerifyCurrentAux(HoudiniState current,

                                           Program program,

                                           HoudiniVCGen vcgen,

                                           out List<Counterexample> errors,

                                           out bool exceptional) {

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

-      VCGen.Outcome outcome;

-      bool pushed = false;

+      ProverInterface.Outcome outcome;

       errors = null;

-      outcome = VCGen.Outcome.Inconclusive;

+      outcome = ProverInterface.Outcome.Undetermined;

       try {

         bool trySameFunc = true;

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

@@ -1024,15 +1017,11 @@ namespace Microsoft.Boogie.Houdini {
             this.NotifyIteration();

           }

 

-          Axiom currentAx = BuildAxiom(current.Assignment);

+          VCExpr currentAx = BuildAxiom(vcgen, current.Assignment);

           this.NotifyAssignment(current.Assignment);

 

           //check the VC with the current assignment

-          vcgen.PushAxiom(currentAx);

-          pushed = true;

-          outcome = vcgen.Verify(out errors);

-          vcgen.Pop();

-          pushed = false;

+          outcome = vcgen.Verify(currentAx, out errors);

           this.NotifyOutcome(outcome);

 

           DebugRefutedCandidates(current.Implementation, errors);

@@ -1048,7 +1037,7 @@ namespace Microsoft.Boogie.Houdini {
             trySameFunc = UpdateAssignmentWorkList(current, outcome, errors);

             //reset for the next round

             errors = null;

-            outcome = VCGen.Outcome.Inconclusive;

+            outcome = ProverInterface.Outcome.Undetermined;

           }

           pastFirstIter = true;

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

@@ -1056,18 +1045,12 @@ namespace Microsoft.Boogie.Houdini {
       }

       catch (VCGenException e) {

         Contract.Assume(e != null);

-        if (pushed) {

-          vcgen.Pop(); // what if session is dead?

-        }

         NotifyException("VCGen");

         exceptional = true;

         return outcome;

       }

       catch (UnexpectedProverOutputException upo) {

         Contract.Assume(upo != null);

-        if (pushed) {

-          vcgen.Pop();

-        }

         NotifyException("UnexpectedProverOutput");

         exceptional = true;

         return outcome;

@@ -1080,9 +1063,9 @@ namespace Microsoft.Boogie.Houdini {
   public enum HoudiniOutcomeKind { Done, FatalError, VerificationCompleted }

 

   public class VCGenOutcome {

-    public VCGen.Outcome outcome;

+    public ProverInterface.Outcome outcome;

     public List<Counterexample> errors;

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

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

       this.outcome = outcome;

       this.errors = errors;

     }

@@ -1098,7 +1081,7 @@ namespace Microsoft.Boogie.Houdini {
 

     // statistics 

 

-    private int CountResults(VCGen.Outcome outcome) {

+    private int CountResults(ProverInterface.Outcome outcome) {

       int outcomeCount = 0;

       foreach (VCGenOutcome verifyOutcome in implementationOutcomes.Values) {

         if (verifyOutcome.outcome == outcome)

@@ -1107,7 +1090,7 @@ namespace Microsoft.Boogie.Houdini {
       return outcomeCount;

     }

 

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

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

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

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

         if (kvpair.Value.outcome == outcome)

@@ -1118,37 +1101,37 @@ namespace Microsoft.Boogie.Houdini {
 

     public int ErrorCount {

       get {

-        return CountResults(VCGen.Outcome.Errors);

+        return CountResults(ProverInterface.Outcome.Invalid);

       }

     }

     public int Verified {

       get {

-        return CountResults(VCGen.Outcome.Correct);

+        return CountResults(ProverInterface.Outcome.Valid);

       }

     }

     public int Inconclusives {

       get {

-        return CountResults(VCGen.Outcome.Inconclusive);

+        return CountResults(ProverInterface.Outcome.Undetermined);

       }

     }

     public int TimeOuts {

       get {

-        return CountResults(VCGen.Outcome.TimedOut);

+        return CountResults(ProverInterface.Outcome.TimeOut);

       }

     }

     public List<string> ListOfTimeouts {

       get {

-        return ListOutcomeMatches(VCGen.Outcome.TimedOut);

+        return ListOutcomeMatches(ProverInterface.Outcome.TimeOut);

       }

     }

     public List<string> ListOfInconclusives {

       get {

-        return ListOutcomeMatches(VCGen.Outcome.Inconclusive);

+        return ListOutcomeMatches(ProverInterface.Outcome.Undetermined);

       }

     }

     public List<string> ListOfErrors {

       get {

-        return ListOutcomeMatches(VCGen.Outcome.Errors);

+        return ListOutcomeMatches(ProverInterface.Outcome.Invalid);

       }

     }

   }

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index ff106380..87ab590d 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -164,8 +164,8 @@ namespace VC {
       Contract.Invariant(implName2LazyInliningInfo == null || cce.NonNullDictionaryAndValues(implName2LazyInliningInfo));

     }

 

-    private Dictionary<string, LazyInliningInfo> implName2LazyInliningInfo;

-    private GlobalVariable errorVariable;

+    protected Dictionary<string, LazyInliningInfo> implName2LazyInliningInfo;

+    protected GlobalVariable errorVariable;

 

     public void GenerateVCsForLazyInlining(Program program) {

       Contract.Requires(program != null);

diff --git a/Test/houdini/houd6.bpl b/Test/houdini/houd6.bpl
index 09f2dd0e..820d2d73 100644
--- a/Test/houdini/houd6.bpl
+++ b/Test/houdini/houd6.bpl
@@ -41,4 +41,4 @@ modifies array;
 }

 

 // expected outcome: Correct

-// expected assigment: bi->True forall i
\ No newline at end of file
+// expected assigment: bi->False forall i
\ No newline at end of file