Refactored ConcurrentHoudini and Houdini to (significantly) reduce duplication of code

1 files changed, 20 insertions, 223 deletions

diff --git a/Source/Houdini/ConcurrentHoudini.cs b/Source/Houdini/ConcurrentHoudini.cs
index b92cb7bc..bfc96258 100644
--- a/Source/Houdini/ConcurrentHoudini.cs
+++ b/Source/Houdini/ConcurrentHoudini.cs
@@ -12,69 +12,19 @@ namespace Microsoft.Boogie.Houdini
 {
   public class ConcurrentHoudini : Houdini
   {
-    int id;
+
+    protected int taskID;
 
     private static ConcurrentDictionary<string, RefutedAnnotation> refutedSharedAnnotations;
 
     public static ConcurrentDictionary<string, RefutedAnnotation> RefutedSharedAnnotations { get { return refutedSharedAnnotations; } }
 
-    public ConcurrentHoudini(int id, Program program, HoudiniSession.HoudiniStatistics stats, string cexTraceFile = "houdiniCexTrace.bpl") {
-      Contract.Assert(id >= 0);
-
-      this.id = id;
+    public ConcurrentHoudini(int taskId, Program program, HoudiniSession.HoudiniStatistics stats, string cexTraceFile = "houdiniCexTrace.bpl") {
+      Contract.Assert(taskId >= 0);
       this.program = program;
       this.cexTraceFile = cexTraceFile;
-
-      if (CommandLineOptions.Clo.Trace)
-        Console.WriteLine("Collecting existential constants...");
-      this.houdiniConstants = CollectExistentialConstants();
-
-      if (CommandLineOptions.Clo.Trace)
-        Console.WriteLine("Building call graph...");
-      this.callGraph = Program.BuildCallGraph(program);
-      if (CommandLineOptions.Clo.Trace)
-        Console.WriteLine("Number of implementations = {0}", callGraph.Nodes.Count);
-
-      if (CommandLineOptions.Clo.HoudiniUseCrossDependencies)
-      {
-        if (CommandLineOptions.Clo.Trace) Console.WriteLine("Computing procedure cross dependencies ...");
-        this.crossDependencies = new CrossDependencies(this.houdiniConstants);
-        this.crossDependencies.Visit(program);
-      }
-
-      Inline();
-
-      this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, new List<Checker>());
-      this.proverInterface = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime, id);
-
-      vcgenFailures = new HashSet<Implementation>();
-      Dictionary<Implementation, HoudiniSession> houdiniSessions = new Dictionary<Implementation, HoudiniSession>();
-      if (CommandLineOptions.Clo.Trace)
-        Console.WriteLine("Beginning VC generation for Houdini...");
-      foreach (Implementation impl in callGraph.Nodes) {
-        try {
-          if (CommandLineOptions.Clo.Trace)
-            Console.WriteLine("Generating VC for {0}", impl.Name);
-          HoudiniSession session = new HoudiniSession(this, vcgen, proverInterface, program, impl, stats, taskID: id);
-          houdiniSessions.Add(impl, session);
-        }
-        catch (VCGenException) {
-          if (CommandLineOptions.Clo.Trace)
-            Console.WriteLine("VC generation failed");
-          vcgenFailures.Add(impl);
-        }
-      }
-      this.houdiniSessions = new ReadOnlyDictionary<Implementation, HoudiniSession>(houdiniSessions);
-
-      if (CommandLineOptions.Clo.ExplainHoudini)
-      {
-        // Print results of ExplainHoudini to a dotty file
-        explainHoudiniDottyFile = new StreamWriter("explainHoudini.dot");
-        explainHoudiniDottyFile.WriteLine("digraph explainHoudini {");
-        foreach (var constant in houdiniConstants)
-          explainHoudiniDottyFile.WriteLine("{0} [ label = \"{0}\" color=black ];", constant.Name);
-        explainHoudiniDottyFile.WriteLine("TimeOut [label = \"TimeOut\" color=red ];");
-      }
+      this.taskID = taskId;
+      Initialize(program, stats);
     }
 
     static ConcurrentHoudini()
@@ -82,7 +32,7 @@ namespace Microsoft.Boogie.Houdini
       refutedSharedAnnotations = new ConcurrentDictionary<string, RefutedAnnotation>();
     }
 
-    private bool ExchangeRefutedAnnotations()
+    protected override bool ExchangeRefutedAnnotations()
     {
       int count = 0;
 
@@ -132,176 +82,23 @@ namespace Microsoft.Boogie.Houdini
       return count > 0 ? true : false;
     }
 
-    protected override bool UpdateAssignmentWorkList(ProverInterface.Outcome outcome,
-                                                     List<Counterexample> errors)
-    {
-      Contract.Assume(currentHoudiniState.Implementation != null);
-      bool dequeue = true;
-
-      switch (outcome) {
-        case ProverInterface.Outcome.Valid:
-        //yeah, dequeue
-        break;
-
-        case ProverInterface.Outcome.Invalid:
-        Contract.Assume(errors != null);
-
-        foreach (Counterexample error in errors) {
-          RefutedAnnotation refutedAnnotation = ExtractRefutedAnnotation(error);
-          // some candidate annotation removed
-          if (refutedAnnotation != null) {
-            refutedSharedAnnotations.TryAdd(refutedAnnotation.Constant.Name, refutedAnnotation);
-            AddRelatedToWorkList(refutedAnnotation);
-            UpdateAssignment(refutedAnnotation);
-            dequeue = false;
-
-            #region Extra debugging output
-            if (CommandLineOptions.Clo.Trace) {
-              using (var cexWriter = new System.IO.StreamWriter(cexTraceFile, true)) {
-                cexWriter.WriteLine("Counter example for " + refutedAnnotation.Constant);
-                cexWriter.Write(error.ToString());
-                cexWriter.WriteLine();
-                using (var writer = new Microsoft.Boogie.TokenTextWriter(cexWriter))
-                  foreach (Microsoft.Boogie.Block blk in error.Trace)
-                    blk.Emit(writer, 15);
-                //cexWriter.WriteLine(); 
-              }
-            }
-            #endregion
-          }
-        }
-
-        if (ExchangeRefutedAnnotations()) dequeue = false;
-
-        break;
-        default:
-        if (CommandLineOptions.Clo.Trace) {
-          Console.WriteLine("Timeout/Spaceout while verifying " + currentHoudiniState.Implementation.Name);
-        }
-
-        HoudiniSession houdiniSession;
-        houdiniSessions.TryGetValue(currentHoudiniState.Implementation, out houdiniSession);
-
-        foreach (Variable v in houdiniSession.houdiniAssertConstants) {
-          if (CommandLineOptions.Clo.Trace) {
-            Console.WriteLine("Removing " + v);
-          }
-          currentHoudiniState.Assignment.Remove(v);
-          currentHoudiniState.Assignment.Add(v, false);
-          this.NotifyConstant(v.Name);
-        }
-
-        currentHoudiniState.addToBlackList(currentHoudiniState.Implementation.Name);
-        break;
-      }
-
-      return dequeue;
+    protected override void ShareRefutedAnnotation(RefutedAnnotation refutedAnnotation) {
+      refutedSharedAnnotations.TryAdd(refutedAnnotation.Constant.Name, refutedAnnotation);
     }
-
-    public override HoudiniOutcome PerformHoudiniInference(int stage = 0, 
-                                                           IEnumerable<int> completedStages = null,
-                                                           Dictionary<string, bool> initialAssignment = null)
-    {
-      this.NotifyStart(program, houdiniConstants.Count);
-
-      currentHoudiniState = new HoudiniState(BuildWorkList(program), BuildAssignment(houdiniConstants));
-
-      if (initialAssignment != null) {
-        foreach (var v in currentHoudiniState.Assignment.Keys.ToList()) {
-          currentHoudiniState.Assignment[v] = initialAssignment[v.Name];
-        }
-      }
-
-      if (refutedSharedAnnotations.Count > 0) {
-        foreach (var v in currentHoudiniState.Assignment.Keys.ToList()) {
-          if (refutedSharedAnnotations.ContainsKey(v.Name)) {
-            currentHoudiniState.Assignment[v] = false;
-          }
-        }
-      }
-
-      foreach (Implementation impl in vcgenFailures) {
-        currentHoudiniState.addToBlackList(impl.Name);
-      }
-
-      while (currentHoudiniState.WorkQueue.Count > 0) {
-        this.NotifyIteration();
-
-        currentHoudiniState.Implementation = currentHoudiniState.WorkQueue.Peek();
-        this.NotifyImplementation(currentHoudiniState.Implementation);
-
-        HoudiniSession session;
-        this.houdiniSessions.TryGetValue(currentHoudiniState.Implementation, out session);
-        HoudiniVerifyCurrent(session, stage, completedStages);
-      }
-
-      this.NotifyEnd(true);
-      Dictionary<string, bool> assignment = new Dictionary<string, bool>();
-      foreach (var x in currentHoudiniState.Assignment)
-        assignment[x.Key.Name] = x.Value;
-      currentHoudiniState.Outcome.assignment = assignment;
-      return currentHoudiniState.Outcome;
+

+    protected override void ApplyRefutedSharedAnnotations() {

+      if (refutedSharedAnnotations.Count > 0) {

+        foreach (var v in currentHoudiniState.Assignment.Keys.ToList()) {

+          if (refutedSharedAnnotations.ContainsKey(v.Name)) {

+            currentHoudiniState.Assignment[v] = false;

+          }

+        }

+      }

     }
 
-    protected override void HoudiniVerifyCurrent(HoudiniSession session, int stage, IEnumerable<int> completedStages)
-    {
-      while (true) {
-        this.NotifyAssignment(currentHoudiniState.Assignment);
-
-        //check the VC with the current assignment
-        List<Counterexample> errors;
-        ProverInterface.Outcome outcome = TryCatchVerify(session, stage, completedStages, out errors);
-        this.NotifyOutcome(outcome);
-
-        DebugRefutedCandidates(currentHoudiniState.Implementation, errors);
-
-        #region Explain Houdini
-        if (CommandLineOptions.Clo.ExplainHoudini && outcome == ProverInterface.Outcome.Invalid)
-        {
-          Contract.Assume(errors != null);
-          // make a copy of this variable
-          errors = new List<Counterexample>(errors);
-          var refutedAnnotations = new List<RefutedAnnotation>();
-          foreach (Counterexample error in errors)
-          {
-            RefutedAnnotation refutedAnnotation = ExtractRefutedAnnotation(error);
-            if (refutedAnnotation == null || refutedAnnotation.Kind == RefutedAnnotationKind.ASSERT) continue;
-            refutedAnnotations.Add(refutedAnnotation);
-          }
-          foreach (var refutedAnnotation in refutedAnnotations)
-          {
-            session.Explain(proverInterface, currentHoudiniState.Assignment, refutedAnnotation.Constant);
-          }
-        }
-        #endregion
-
-        if (UpdateHoudiniOutcome(currentHoudiniState.Outcome, currentHoudiniState.Implementation, outcome, errors)) { // abort
-          currentHoudiniState.WorkQueue.Dequeue();
-          this.NotifyDequeue();
-          FlushWorkList(stage, completedStages);
-          return;
-        }
-        else if (UpdateAssignmentWorkList(outcome, errors)) {
-          if (CommandLineOptions.Clo.UseUnsatCoreForContractInfer && outcome == ProverInterface.Outcome.Valid)
-            session.UpdateUnsatCore(proverInterface, currentHoudiniState.Assignment);
-          currentHoudiniState.WorkQueue.Dequeue();
-          this.NotifyDequeue();
-          return;
-        }
-      } 
+    protected override int GetTaskID() {
+      return taskID;
     }
 
-    protected override ProverInterface.Outcome TryCatchVerify(HoudiniSession session, int stage, IEnumerable<int> completedStages, out List<Counterexample> errors) {
-      ProverInterface.Outcome outcome;
-      try {
-        outcome = session.Verify(proverInterface, GetAssignmentWithStages(stage, completedStages), out errors, taskID: id);
-      }
-      catch (UnexpectedProverOutputException upo) {
-        Contract.Assume(upo != null);
-        errors = null;
-        outcome = ProverInterface.Outcome.Undetermined;
-      }
-      return outcome;
-    }
   }
 }