Did some refactoring in the execution engine and worked on the parallelization.

1 files changed, 37 insertions, 15 deletions

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 3ae97bdd..bcafb9cb 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -4,6 +4,7 @@
 //

 //-----------------------------------------------------------------------------

 using System;

+using System.Linq;

 using System.Collections;

 using System.Collections.Generic;

 using System.Diagnostics;

@@ -147,14 +148,14 @@ namespace Microsoft.Boogie {
         return naryExpr.Fun.FunctionName;

     }

 

-    public void Print(int indent, Action<Block> blockAction = null) {

+    public void Print(int indent, TextWriter tw, Action<Block> blockAction = null) {

       int numBlock = -1;

       string ind = new string(' ', indent);

       foreach (Block b in Trace) {

         Contract.Assert(b != null);

         numBlock++;

         if (b.tok == null) {

-          Console.WriteLine("{0}<intermediate block>", ind);

+          tw.WriteLine("{0}<intermediate block>", ind);

         } else {

           // for ErrorTrace == 1 restrict the output;

           // do not print tokens with -17:-4 as their location because they have been

@@ -165,7 +166,7 @@ namespace Microsoft.Boogie {
                 blockAction(b);

             }

 

-            Console.WriteLine("{4}{0}({1},{2}): {3}", b.tok.filename, b.tok.line, b.tok.col, b.Label, ind);

+            tw.WriteLine("{4}{0}({1},{2}): {3}", b.tok.filename, b.tok.line, b.tok.col, b.Label, ind);

 

             for (int numInstr = 0; numInstr < b.Cmds.Length; numInstr++)

             {

@@ -178,13 +179,13 @@ namespace Microsoft.Boogie {
                     {

                         Contract.Assert(calleeCounterexamples[loc].args.Count == 1);

                         var arg = calleeCounterexamples[loc].args[0];

-                        Console.WriteLine("{0}value = {1}", ind, arg.ToString());

+                        tw.WriteLine("{0}value = {1}", ind, arg.ToString());

                     }

                     else

                     {

-                        Console.WriteLine("{1}Inlined call to procedure {0} begins", calleeName, ind);

-                        calleeCounterexamples[loc].counterexample.Print(indent + 4);

-                        Console.WriteLine("{1}Inlined call to procedure {0} ends", calleeName, ind);

+                        tw.WriteLine("{1}Inlined call to procedure {0} begins", calleeName, ind);

+                        calleeCounterexamples[loc].counterexample.Print(indent + 4, tw);

+                        tw.WriteLine("{1}Inlined call to procedure {0} ends", calleeName, ind);

                     }

                 }

             }

@@ -197,7 +198,7 @@ namespace Microsoft.Boogie {
 

     public bool ModelHasStatesAlready = false;

 

-    public void PrintModel()

+    public void PrintModel(TextWriter tw)

     {

       var filename = CommandLineOptions.Clo.ModelViewFile;

       if (Model == null || filename == null || CommandLineOptions.Clo.StratifiedInlining > 0) return;

@@ -205,8 +206,8 @@ namespace Microsoft.Boogie {
       var m = ModelHasStatesAlready ? Model : this.GetModelWithStates();

 

       if (filename == "-") {

-        m.Write(Console.Out);

-        Console.Out.Flush();

+        m.Write(tw);

+        tw.Flush();

       } else {

         using (var wr = new StreamWriter(filename, !firstModelFile)) {

           firstModelFile = false;

@@ -532,7 +533,7 @@ namespace VC {
   }

 

   [ContractClass(typeof(ConditionGenerationContracts))]

-  public abstract class ConditionGeneration {

+  public abstract class ConditionGeneration : IDisposable {

     protected internal object CheckerCommonState;

 

     public enum Outcome {

@@ -570,6 +571,9 @@ namespace VC {
     public int CumulativeAssertionCount;  // for statistics

 

     protected readonly List<Checker>/*!>!*/ checkers = new List<Checker>();

+

+    private bool _disposed;

+

     protected VariableSeq CurrentLocalVariables = null;

 

     // shared across each implementation; created anew for each implementation

@@ -1626,6 +1630,24 @@ namespace VC {
       #endregion

     }

 

+

+    public void Dispose()

+    {

+      Dispose(true);

+      GC.SuppressFinalize(this);

+    }

+

+    protected virtual void Dispose(bool disposing)

+    {

+      if (!_disposed)

+      {

+        if (disposing)

+        {

+          Close();

+        }

+        _disposed = true;

+      }

+    }

   }

 

   public class ModelViewInfo

@@ -1643,10 +1665,10 @@ namespace VC {
       Contract.Requires(impl != null);

 

       // global variables

-      foreach (Declaration d in program.TopLevelDeclarations) {

-        if (d is Constant) continue;

-        if (d is Variable) {

-          AllVariables.Add((Variable)d);

+      foreach (Variable v in program.TopLevelDeclarations.OfType<Variable>()) {

+        if (!(v is Constant))

+        {

+          AllVariables.Add(v);

         }

       }

       // implementation parameters