refactoring houdini so that it creates only a single instance of z3

4 files changed, 65 insertions, 81 deletions

diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs
index 519a01af..3cb27e14 100644
--- a/Source/Houdini/Checker.cs
+++ b/Source/Houdini/Checker.cs
@@ -17,54 +17,36 @@ using System.Threading;
 using VC;

 

 namespace Microsoft.Boogie.Houdini {

-  public class HoudiniVCGen : VCGen {

-    private Checker checker;

+  public class HoudiniSession {

     private string descriptiveName;

     private VCExpr conjecture;

     private ProverInterface.ErrorHandler handler;

-    CounterexampleCollector collector;

+    ConditionGeneration.CounterexampleCollector collector;

 

-    public VCExpressionGenerator VCExprGenerator {

-      get {

-        return checker.VCExprGen;

-      }

-    }

-

-    public Boogie2VCExprTranslator BooogieExprTranslator {

-      get {

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

-        return proverContext.BoogieExprTranslator;

-      }

-    }

-

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

-    : base(program, logFilePath, appendLogFile) {

+    public HoudiniSession(VCGen vcgen, Checker checker, Program program, Implementation impl, string logFilePath, bool appendLogFile) {

       descriptiveName = impl.Name;

-      collector = new CounterexampleCollector();

+      collector = new ConditionGeneration.CounterexampleCollector();

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

       if (CommandLineOptions.Clo.SoundnessSmokeTest) {

         throw new Exception("HoudiniVCGen does not support Soundness smoke test.");

       }

 

-      ConvertCFG2DAG(impl, program);

+      vcgen.ConvertCFG2DAG(impl, program);

       ModelViewInfo mvInfo;

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

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

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

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

-      if (!(checker.TheoremProver is Z3ProcessTheoremProver || checker.TheoremProver is SMTLibProcessTheoremProver)) {

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

-      }

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

+      

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

 

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

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

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

       }

       else {

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

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

       }

     }

 

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

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

       collector.examples.Clear();

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

       checker.BeginCheck(descriptiveName, vc, handler);

diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index 09017d20..06fd5502 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -193,7 +193,6 @@ namespace Microsoft.Boogie.Houdini {
 

   }

 

-

   public abstract class ObservableHoudini {

     private List<HoudiniObserver> observers = new List<HoudiniObserver>();

 

@@ -251,7 +250,9 @@ namespace Microsoft.Boogie.Houdini {
   public class Houdini : ObservableHoudini {

     private Program program;

     private ReadOnlyDictionary<string, IdentifierExpr> houdiniConstants;

-    private ReadOnlyDictionary<Implementation, HoudiniVCGen> vcgenSessions;

+    private ReadOnlyDictionary<Implementation, HoudiniSession> houdiniSessions;

+    private VCGen vcgen;

+    private Checker checker;

     private Graph<Implementation> callGraph;

     private bool continueAtError;

 

@@ -260,21 +261,20 @@ namespace Microsoft.Boogie.Houdini {
       this.callGraph = BuildCallGraph();

       this.continueAtError = continueAtError;

       this.houdiniConstants = CollectExistentialConstants();

-      this.vcgenSessions = PrepareVCGenSessions();

-    }

+      this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

+      this.checker = new Checker(vcgen, program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime);

 

-    private ReadOnlyDictionary<Implementation, HoudiniVCGen> PrepareVCGenSessions() {

-      Dictionary<Implementation, HoudiniVCGen> vcgenSessions = new Dictionary<Implementation, HoudiniVCGen>();

+      Dictionary<Implementation, HoudiniSession> houdiniSessions = new Dictionary<Implementation, HoudiniSession>();

       foreach (Implementation impl in callGraph.Nodes) {

         // make a different simplify log file for each function

         String simplifyLog = null;

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

           simplifyLog = impl.ToString() + CommandLineOptions.Clo.SimplifyLogFilePath;

         }

-        HoudiniVCGen vcgen = new HoudiniVCGen(program, impl, simplifyLog, CommandLineOptions.Clo.SimplifyLogFileAppend);

-        vcgenSessions.Add(impl, vcgen);

+        HoudiniSession session = new HoudiniSession(vcgen, checker, program, impl, simplifyLog, CommandLineOptions.Clo.SimplifyLogFileAppend);

+        houdiniSessions.Add(impl, session);

       }

-      return new ReadOnlyDictionary<Implementation, HoudiniVCGen>(vcgenSessions);

+      this.houdiniSessions = new ReadOnlyDictionary<Implementation, HoudiniSession>(houdiniSessions);

     }

 

     private ReadOnlyDictionary<string, IdentifierExpr> CollectExistentialConstants() {

@@ -362,9 +362,10 @@ namespace Microsoft.Boogie.Houdini {
       return false;

     }

 

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

-      Boogie2VCExprTranslator exprTranslator = vcgen.BooogieExprTranslator;

-      VCExpressionGenerator exprGen = vcgen.VCExprGenerator;

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

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

+      Boogie2VCExprTranslator exprTranslator = proverContext.BoogieExprTranslator;

+      VCExpressionGenerator exprGen = checker.VCExprGen;

 

       VCExpr expr = VCExpressionGenerator.True;

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

@@ -389,46 +390,44 @@ namespace Microsoft.Boogie.Houdini {
       return initial;

     }

 

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

-      HoudiniVCGen vcgen;

-      vcgenSessions.TryGetValue(implementation, out vcgen);

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

       if (vcgen == null)

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

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

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

       return outcome;

     }

 

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

     // assignment and the worklist

-    private ProverInterface.Outcome HoudiniVerifyCurrent(HoudiniState current,

+    private ProverInterface.Outcome HoudiniVerifyCurrent(

+                                        HoudiniSession session,

+                                        HoudiniState current,

                                         Program program,

                                         out List<Counterexample> errors,

                                         out bool exc) {

-      HoudiniVCGen vcgen;

       if (current.Implementation == null)

         throw new Exception("HoudiniVerifyCurrent has null implementation");

 

       Implementation implementation = current.Implementation;

-      vcgenSessions.TryGetValue(implementation, out vcgen);

       if (vcgen == null)

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

 

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

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

       return outcome;

     }

 

-    private ProverInterface.Outcome VerifyCurrent(HoudiniState current,

+    private ProverInterface.Outcome VerifyCurrent(

+                                        HoudiniSession session,

+                                        HoudiniState current,

                                         Program program,

                                         out List<Counterexample> errors,

                                         out bool exc) {

-      HoudiniVCGen vcgen;

       if (current.Implementation != null) {

         Implementation implementation = current.Implementation;

-        vcgenSessions.TryGetValue(implementation, out vcgen);

         if (vcgen == null)

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

 

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

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

         return outcome;

       }

       else {

@@ -494,17 +493,17 @@ namespace Microsoft.Boogie.Houdini {
 

     private void FlushWorkList(HoudiniState current) {

       this.NotifyFlushStart();

-      HoudiniVCGen vcgen;

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

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

+      VCExpr axiom = BuildAxiom(current.Assignment);

       while (current.WorkList.Count > 0) {

         this.NotifyIteration();

 

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

         this.NotifyImplementation(current.Implementation);

 

+        HoudiniSession session;

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

         List<Counterexample> errors;

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

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

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

         this.NotifyOutcome(outcome);

 

@@ -686,22 +685,20 @@ 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();

 

-        HoudiniVCGen vcgen;

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

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

+        VCExpr axiom = BuildAxiom(current.Assignment);

         this.NotifyAssignment(current.Assignment);

 

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

         this.NotifyImplementation(current.Implementation);

 

         List<Counterexample> errors;

-        ProverInterface.Outcome outcome = VerifyUsingAxiom(current.Implementation, axiom, out 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);

@@ -731,8 +728,10 @@ namespace Microsoft.Boogie.Houdini {
         current.Implementation = current.WorkList.Peek();

         this.NotifyImplementation(current.Implementation);

 

+        HoudiniSession session;

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

         List<Counterexample> errors;

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

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

@@ -771,7 +770,9 @@ namespace Microsoft.Boogie.Houdini {
         this.NotifyImplementation(current.Implementation);

 

         List<Counterexample> errors;

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

+        HoudiniSession session;

+        this.houdiniSessions.TryGetValue(current.Implementation, out session);

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

 

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

         if (exceptional) {

@@ -923,10 +924,10 @@ namespace Microsoft.Boogie.Houdini {
       return null;

     }

 

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

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

       ProverInterface.Outcome outcome;

       try {

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

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

       }

       catch (VCGenException e) {

         Contract.Assume(e != null);

@@ -943,9 +944,10 @@ namespace Microsoft.Boogie.Houdini {
 

     //version of TryCatchVerify that spins on the same function

     //as long as the current assignment is changing

-    private ProverInterface.Outcome TrySpinSameFunc(HoudiniState current,

+    private ProverInterface.Outcome TrySpinSameFunc(

+                                          HoudiniSession session,

+                                          HoudiniState current,

                                           Program program,

-                                          HoudiniVCGen vcgen,

                                           out List<Counterexample> errors,

                                           out bool exceptional) {

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

@@ -962,11 +964,10 @@ namespace Microsoft.Boogie.Houdini {
             this.NotifyIteration();

           }

 

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

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

+          VCExpr currentAx = BuildAxiom(current.Assignment);

           this.NotifyAssignment(current.Assignment);

 

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

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

           this.NotifyOutcome(outcome);

 

           DebugRefutedCandidates(current.Implementation, errors);

@@ -1004,9 +1005,10 @@ namespace Microsoft.Boogie.Houdini {
     }

 

     //Similar to TrySpinSameFunc except no Candidate logic

-    private ProverInterface.Outcome HoudiniVerifyCurrentAux(HoudiniState current,

+    private ProverInterface.Outcome HoudiniVerifyCurrentAux(

+                                          HoudiniSession session,

+                                          HoudiniState current,

                                           Program program,

-                                          HoudiniVCGen vcgen,

                                           out List<Counterexample> errors,

                                           out bool exceptional) {

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

@@ -1029,11 +1031,11 @@ namespace Microsoft.Boogie.Houdini {
             this.NotifyIteration();

           }

 

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

+          VCExpr currentAx = BuildAxiom(current.Assignment);

           this.NotifyAssignment(current.Assignment);

 

           //check the VC with the current assignment

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

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

           this.NotifyOutcome(outcome);

 

           DebugRefutedCandidates(current.Implementation, errors);

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index b8645cb0..cb28cd7d 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -909,7 +909,7 @@ namespace VC {
     }

 

 

-    protected class CounterexampleCollector : VerifierCallback {

+    public class CounterexampleCollector : VerifierCallback {

       [ContractInvariantMethod]

       void ObjectInvariant() {

         Contract.Invariant(cce.NonNullElements(examples));

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 0a59555e..6ab86854 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -177,7 +177,7 @@ namespace VC {
       Contract.Invariant(implName2LazyInliningInfo == null || cce.NonNullDictionaryAndValues(implName2LazyInliningInfo));

     }

 

-    protected Dictionary<string, LazyInliningInfo> implName2LazyInliningInfo;

+    public Dictionary<string, LazyInliningInfo> implName2LazyInliningInfo;

     protected GlobalVariable errorVariable;

 

     public void GenerateVCsForLazyInlining(Program program) {

@@ -1611,7 +1611,7 @@ namespace VC {
     }

     #endregion

 

-    protected VCExpr GenerateVC(Implementation/*!*/ impl, Variable controlFlowVariable, out Hashtable/*<int, Absy!>*//*!*/ label2absy, Checker/*!*/ ch)

+    public VCExpr GenerateVC(Implementation/*!*/ impl, Variable controlFlowVariable, out Hashtable/*<int, Absy!>*//*!*/ label2absy, Checker/*!*/ ch)

     {

       Contract.Requires(impl != null);

       Contract.Requires(ch != null);

@@ -2059,7 +2059,7 @@ namespace VC {
         }

       }

     }

-    protected void ConvertCFG2DAG(Implementation impl, Program program)

+    public void ConvertCFG2DAG(Implementation impl, Program program)

     {

     Contract.Requires(impl != null);

     Contract.Requires(program != null);

@@ -2274,7 +2274,7 @@ namespace VC {
       #endregion

     }

 

-    protected Hashtable/*TransferCmd->ReturnCmd*/ PassifyImpl(Implementation impl, Program program, out ModelViewInfo mvInfo)

+    public Hashtable/*TransferCmd->ReturnCmd*/ PassifyImpl(Implementation impl, Program program, out ModelViewInfo mvInfo)

     {

       Contract.Requires(impl != null);

       Contract.Requires(program != null);