merge

8 files changed, 351 insertions, 165 deletions

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index e88c000e..a3f266ef 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -4,6 +4,7 @@
 //

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

 using System;

+using System.Linq;

 using System.Collections;

 using System.Collections.Generic;

 using System.Threading;

@@ -14,8 +15,18 @@ using System.Diagnostics.Contracts;
 using Microsoft.Boogie.AbstractInterpretation;

 using Microsoft.Boogie.VCExprAST;

 using Microsoft.Basetypes;

+using System.Threading.Tasks;

 

 namespace Microsoft.Boogie {

+

+  enum CheckerStatus

+  {

+    Idle,

+    Ready,

+    Busy,

+    Closed

+  }

+

   /// <summary>

   /// Interface to the theorem prover specialized to Boogie.

   ///

@@ -27,7 +38,6 @@ namespace Microsoft.Boogie {
     void ObjectInvariant() {

       Contract.Invariant(gen != null);

       Contract.Invariant(thmProver != null);

-      Contract.Invariant(ProverDone != null);

     }

 

     private readonly VCExpressionGenerator gen;

@@ -37,18 +47,32 @@ namespace Microsoft.Boogie {
 

     // state for the async interface

     private volatile ProverInterface.Outcome outcome;

-    private volatile bool busy;

     private volatile bool hasOutput;

     private volatile UnexpectedProverOutputException outputExn;

     private DateTime proverStart;

     private TimeSpan proverRunTime;

     private volatile ProverInterface.ErrorHandler handler;

-    private volatile bool closed;

+    private volatile CheckerStatus status;

+    public readonly Program Program;

+

+    public void GetReady()

+    {

+      Contract.Requires(status == CheckerStatus.Idle);

+

+      status = CheckerStatus.Ready;

+    }

 

-    public readonly AutoResetEvent ProverDone = new AutoResetEvent(false);

+    public void GoBackToIdle()

+    {

+      Contract.Requires(IsBusy);

 

-    public bool WillingToHandle(Implementation impl, int timeout) {

-      return !closed && timeout == this.timeout;

+      status = CheckerStatus.Idle;

+    }

+

+    public Task ProverTask { get; set; }

+

+    public bool WillingToHandle(int timeout, Program prog) {

+      return status == CheckerStatus.Idle && timeout == this.timeout && (prog == null || Program == prog);

     }

 

     public VCExpressionGenerator VCExprGen {

@@ -106,6 +130,7 @@ namespace Microsoft.Boogie {
       Contract.Requires(vcgen != null);

       Contract.Requires(prog != null);

       this.timeout = timeout;

+      this.Program = prog;

 

       ProverOptions options = cce.NonNull(CommandLineOptions.Clo.TheProverFactory).BlankProverOptions();

 

@@ -137,40 +162,7 @@ namespace Microsoft.Boogie {
       } else {

         if (ctx == null) ctx = (ProverContext)CommandLineOptions.Clo.TheProverFactory.NewProverContext(options);

 

-        // set up the context

-        foreach (Declaration decl in prog.TopLevelDeclarations) {

-          Contract.Assert(decl != null);

-          TypeCtorDecl t = decl as TypeCtorDecl;

-          if (t != null) {

-            ctx.DeclareType(t, null);

-          }

-        }

-        foreach (Declaration decl in prog.TopLevelDeclarations) {

-          Contract.Assert(decl != null);

-          Constant c = decl as Constant;

-          if (c != null) {

-            ctx.DeclareConstant(c, c.Unique, null);

-          } else {

-            Function f = decl as Function;

-            if (f != null) {

-              ctx.DeclareFunction(f, null);

-            }

-          }

-        }

-        foreach (Declaration decl in prog.TopLevelDeclarations) {

-          Contract.Assert(decl != null);

-          Axiom ax = decl as Axiom;

-          if (ax != null) {

-            ctx.AddAxiom(ax, null);

-          }

-        }

-        foreach (Declaration decl in prog.TopLevelDeclarations) {

-          Contract.Assert(decl != null);

-          GlobalVariable v = decl as GlobalVariable;

-          if (v != null) {

-            ctx.DeclareGlobalVariable(v, null);

-          }

-        }

+        Setup(prog, ctx);

 

         // we first generate the prover and then store a clone of the

         // context in the cache, so that the prover can setup stuff in

@@ -184,13 +176,61 @@ namespace Microsoft.Boogie {
       this.gen = prover.VCExprGen;

     }

 

+    public void Retarget(Program prog, ProverContext ctx, int timeout = 0)

+    {

+        ctx.Clear();

+        Setup(prog, ctx);

+        if (0 < timeout)

+        {

+          TheoremProver.SetTimeOut(timeout * 1000);

+        }

+        else

+        {

+          TheoremProver.SetTimeOut(0);

+        }

+        TheoremProver.FullReset();

+    }

+

+    private static void Setup(Program prog, ProverContext ctx)

+    {

+      // set up the context

+      foreach (Declaration decl in prog.TopLevelDeclarations.ToList())

+      {

+        Contract.Assert(decl != null);

+        var typeDecl = decl as TypeCtorDecl;

+        var constDecl = decl as Constant;

+        var funDecl = decl as Function;

+        var axiomDecl = decl as Axiom;

+        var glVarDecl = decl as GlobalVariable;

+        if (typeDecl != null)

+        {

+          ctx.DeclareType(typeDecl, null);

+        }

+        else if (constDecl != null)

+        {

+          ctx.DeclareConstant(constDecl, constDecl.Unique, null);

+        }

+        else if (funDecl != null)

+        {

+          ctx.DeclareFunction(funDecl, null);

+        }

+        else if (axiomDecl != null)

+        {

+          ctx.AddAxiom(axiomDecl, null);

+        }

+        else if (glVarDecl != null)

+        {

+          ctx.DeclareGlobalVariable(glVarDecl, null);

+        }

+      }

+    }

 

     /// <summary>

     /// Clean-up.

     /// </summary>

-    public void Close() {

-      this.closed = true;

+    public void Close() {      

       thmProver.Close();

+      status = CheckerStatus.Closed;

     }

 

     /// <summary>

@@ -205,13 +245,21 @@ namespace Microsoft.Boogie {
 

     public bool IsBusy {

       get {

-        return busy;

+        return status == CheckerStatus.Busy;

       }

     }

 

-    public bool Closed {

+    public bool IsClosed {

       get {

-        return closed;

+        return status == CheckerStatus.Closed;

+      }

+    }

+

+    public bool IsIdle

+    {

+      get

+      {

+        return status == CheckerStatus.Idle;

       }

     }

 

@@ -252,39 +300,35 @@ namespace Microsoft.Boogie {
           break;

       }

 

-      Contract.Assert(busy);

       hasOutput = true;

       proverRunTime = DateTime.UtcNow - proverStart;

-

-      ProverDone.Set();

     }

 

     public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler) {

       Contract.Requires(descriptiveName != null);

       Contract.Requires(vc != null);

       Contract.Requires(handler != null);

+      Contract.Requires(status == CheckerStatus.Ready);

 

-      Contract.Requires(!IsBusy);

-      Contract.Assert(!busy);

-      busy = true;

+      status = CheckerStatus.Busy;

       hasOutput = false;

       outputExn = null;

       this.handler = handler;

 

+      thmProver.Reset();

       proverStart = DateTime.UtcNow;

       thmProver.BeginCheck(descriptiveName, vc, handler);

       //  gen.ClearSharedFormulas();    PR: don't know yet what to do with this guy

 

-      ThreadPool.QueueUserWorkItem(WaitForOutput);

+      ProverTask = Task.Factory.StartNew(() => { WaitForOutput(null); } , TaskCreationOptions.LongRunning);

     }

 

     public ProverInterface.Outcome ReadOutcome() {

-

       Contract.Requires(IsBusy);

       Contract.Requires(HasOutput);

       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

+

       hasOutput = false;

-      busy = false;

 

       if (outputExn != null) {

         throw outputExn;

@@ -423,6 +467,10 @@ namespace Microsoft.Boogie {
     public virtual void Close() {

     }

 

+    public abstract void Reset();

+

+    public abstract void FullReset();

+

     /// <summary>

     /// MSchaef: Allows to Push a VCExpression as Axiom on the prover stack (beta)

     /// for now it is only implemented by ProcessTheoremProver and still requires some

@@ -541,6 +589,16 @@ namespace Microsoft.Boogie {
       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

       throw new NotImplementedException();

     }

+

+    public override void Reset()

+    {

+      throw new NotImplementedException();

+    }

+

+    public override void FullReset()

+    {

+      throw new NotImplementedException();

+    }

   }

 

   public class ProverException : Exception {

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index a8a95f22..05e79fb0 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,20 +148,26 @@ namespace Microsoft.Boogie {
         return naryExpr.Fun.FunctionName;

     }

 

-    public void Print(int indent) {

+    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

           // introduced in the translation and do not give any useful feedback to the user

           if (!(CommandLineOptions.Clo.ErrorTrace == 1 && b.tok.line == -17 && b.tok.col == -4)) {

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

+            if (blockAction != null)

+            {

+                blockAction(b);

+            }

+

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

             {

                 var loc = new TraceLocation(numBlock, numInstr);

@@ -172,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);

                     }

                 }

             }

@@ -191,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;

@@ -199,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;

@@ -520,13 +527,13 @@ namespace VC {
       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

       throw new NotImplementedException();

     }

-    public ConditionGenerationContracts(Program p)

-      : base(p) {

+    public ConditionGenerationContracts(Program p, List<Checker> checkers)

+      : base(p, checkers) {

     }

   }

 

   [ContractClass(typeof(ConditionGenerationContracts))]

-  public abstract class ConditionGeneration {

+  public abstract class ConditionGeneration : IDisposable {

     protected internal object CheckerCommonState;

 

     public enum Outcome {

@@ -563,7 +570,10 @@ namespace VC {
 

     public int CumulativeAssertionCount;  // for statistics

 

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

+    protected readonly List<Checker>/*!>!*/ checkers;

+

+    private bool _disposed;

+

     protected VariableSeq CurrentLocalVariables = null;

 

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

@@ -576,9 +586,11 @@ namespace VC {
 

     public static List<Model> errorModelList;

 

-    public ConditionGeneration(Program p) {

-      Contract.Requires(p != null);

+    public ConditionGeneration(Program p, List<Checker> checkers) {

+      Contract.Requires(p != null && checkers != null && cce.NonNullElements(checkers));

       program = p;

+      this.checkers = checkers;

+      Cores = 1;

     }

 

     /// <summary>

@@ -960,35 +972,61 @@ namespace VC {
     #endregion

 

 

-    protected Checker FindCheckerFor(Implementation impl, int timeout) {

+    protected Checker FindCheckerFor(int timeout)

+    {

       Contract.Ensures(Contract.Result<Checker>() != null);

 

-      int i = 0;

-      while (i < checkers.Count) {

-        if (checkers[i].Closed) {

-          checkers.RemoveAt(i);

-          continue;

-        } else {

-          if (!checkers[i].IsBusy && checkers[i].WillingToHandle(impl, timeout))

-            return checkers[i];

+      lock (checkers)

+      {

+      retry:

+        // Look for existing checker.

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

+        {

+          var c = checkers.ElementAt(i);

+          lock (c)

+          {

+            if (c.WillingToHandle(timeout, program))

+            {

+              c.GetReady();

+              return c;

+            }

+            else if (c.IsIdle || c.IsClosed)

+            {

+              if (c.IsIdle)

+              {

+                c.Retarget(program, c.TheoremProver.Context, timeout);

+                return c;

+              }

+              else

+              {

+                checkers.RemoveAt(i);

+              }

+              continue;

+            }

+          }

         }

-        ++i;

-      }

-      string log = logFilePath;

-      if (log != null && !log.Contains("@PROC@") && checkers.Count > 0)

-        log = log + "." + checkers.Count;

-      Checker ch = new Checker(this, program, log, appendLogFile, timeout);

-      Contract.Assert(ch != null);

-      checkers.Add(ch);

-      return ch;

+

+        if (Cores <= checkers.Count)

+        {

+          Monitor.Wait(checkers, 50);

+          goto retry;

+        }

+

+        // Create a new checker.

+        string log = logFilePath;

+        if (log != null && !log.Contains("@PROC@") && checkers.Count > 0)

+        {

+          log = log + "." + checkers.Count;

+        }

+        Checker ch = new Checker(this, program, log, appendLogFile, timeout);

+        ch.GetReady();

+        checkers.Add(ch);

+        return ch;

+      }      

     }

 

 

     virtual public void Close() {

-      foreach (Checker checker in checkers) {

-        Contract.Assert(checker != null);

-        checker.Close();

-      }

     }

 

 

@@ -1620,6 +1658,26 @@ 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 int Cores { get; set; }

   }

 

   public class ModelViewInfo

@@ -1637,10 +1695,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

diff --git a/Source/VCGeneration/Context.cs b/Source/VCGeneration/Context.cs
index bf27144b..484ce226 100644
--- a/Source/VCGeneration/Context.cs
+++ b/Source/VCGeneration/Context.cs
@@ -34,6 +34,7 @@ namespace Microsoft.Boogie
     public abstract Boogie2VCExprTranslator BoogieExprTranslator { get; }

     public abstract VCGenerationOptions VCGenOptions { get; }

     public abstract object Clone();

+    public abstract void Clear();

   }

   

 [ContractClassFor(typeof(ProverContext))]

@@ -114,6 +115,12 @@ public abstract class ProverContextContracts:ProverContext{
       exprTranslator = null;

     }

 

+    public override void Clear()

+    {

+        distincts = new List<Variable>();

+        axiomConjuncts = new List<VCExpr>();

+    }

+

     protected DeclFreeProverContext(DeclFreeProverContext ctxt) {

       Contract.Requires(ctxt != null);

       this.gen = ctxt.gen;

diff --git a/Source/VCGeneration/ExprExtensions.cs b/Source/VCGeneration/ExprExtensions.cs
index d63f4fc2..7ebba061 100644
--- a/Source/VCGeneration/ExprExtensions.cs
+++ b/Source/VCGeneration/ExprExtensions.cs
@@ -21,6 +21,35 @@ using Microsoft.Boogie.VCExprAST;
 

 namespace Microsoft.Boogie.ExprExtensions

 {

+    class ReferenceComparer<T> : IEqualityComparer<T> where T : class

+    {

+        private static ReferenceComparer<T> m_instance;

+

+        public static ReferenceComparer<T> Instance

+        {

+            get

+            {

+                return m_instance ?? (m_instance = new ReferenceComparer<T>());

+            }

+        }

+

+        public bool Equals(T x, T y)

+        {

+            return ReferenceEquals(x, y);

+        }

+

+        public int GetHashCode(T obj)

+        {

+            return System.Runtime.CompilerServices.RuntimeHelpers.GetHashCode(obj);

+        }

+    }

+

+    public class TermDict<T> : Dictionary<Term, T> 

+    {

+        public TermDict() : base(ReferenceComparer<Term>.Instance) { }

+    }

+

+        

 

     public enum TermKind { App, Other };

 

@@ -229,9 +258,9 @@ namespace Microsoft.Boogie.ExprExtensions
             {

                 public int cnt = 0;

             }

-            Dictionary<Term, counter> refcnt = new Dictionary<Term, counter>();

+            TermDict<counter> refcnt = new TermDict<counter>();

             List<VCExprLetBinding> bindings = new List<VCExprLetBinding>();

-            Dictionary<Term, VCExprVar> bindingMap = new Dictionary<Term, VCExprVar>();

+            TermDict< VCExprVar> bindingMap = new TermDict< VCExprVar>();

             int letcnt = 0;

             Context ctx;

 

diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs
index e96499fe..3299ef76 100644
--- a/Source/VCGeneration/FixedpointVC.cs
+++ b/Source/VCGeneration/FixedpointVC.cs
@@ -76,8 +76,10 @@ namespace Microsoft.Boogie
         Mode mode;

         AnnotationStyle style;

 

-        public FixedpointVC( Program _program, string/*?*/ logFilePath, bool appendLogFile)

-            : base(_program, logFilePath, appendLogFile) 

+        private static Checker old_checker = null;

+

+        public FixedpointVC( Program _program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers)

+            : base(_program, logFilePath, appendLogFile, checkers) 

         {

             switch (CommandLineOptions.Clo.FixedPointMode)

             {

@@ -106,7 +108,13 @@ namespace Microsoft.Boogie
             rpfp = new RPFP(RPFP.CreateLogicSolver(ctx));

             program = _program;

             gen = ctx;

-            checker = new Checker(this, program, logFilePath, appendLogFile, 0, null);

+            if(old_checker == null)

+              checker = new Checker(this, program, logFilePath, appendLogFile, 0, null);

+            else {

+                checker = old_checker;

+                checker.Retarget(program,checker.TheoremProver.Context);

+            }

+            old_checker = checker;

             boogieContext = checker.TheoremProver.Context;

             linOptions = null; //  new Microsoft.Boogie.Z3.Z3LineariserOptions(false, options, new List<VCExprVar>());

         }

@@ -660,7 +668,7 @@ namespace Microsoft.Boogie
             }

         }

 

-        private Term ExtractSmallerVCsRec(Dictionary<Term, Term> memo, Term t, List<Term> small, Term lbl = null)

+        private Term ExtractSmallerVCsRec(TermDict< Term> memo, Term t, List<Term> small, Term lbl = null)

         {

             Term res;

             if (memo.TryGetValue(t, out res))

@@ -733,7 +741,7 @@ namespace Microsoft.Boogie
         }

 

         private void ExtractSmallerVCs(Term t, List<Term> small){

-            Dictionary<Term, Term> memo = new Dictionary<Term, Term>();

+            TermDict< Term> memo = new TermDict< Term>();

             Term top = ExtractSmallerVCsRec(memo, t, small);

             small.Add(top);

         }

@@ -763,7 +771,7 @@ namespace Microsoft.Boogie
             return ctx.MkImplies(ctx.MkAnd(eqns), ctx.MkApp(label, ctx.MkApp(f, tvars)));

         }

 

-        private Term MergeGoalsRec(Dictionary<Term, Term> memo, Term t)

+        private Term MergeGoalsRec(TermDict< Term> memo, Term t)

         {

             Term res;

             if (memo.TryGetValue(t, out res))

@@ -803,11 +811,11 @@ namespace Microsoft.Boogie
 

         private Term MergeGoals(Term t)

         {

-            Dictionary<Term, Term> memo = new Dictionary<Term, Term>();

+            TermDict< Term> memo = new TermDict< Term>();

             return MergeGoalsRec(memo, t);

         }

 

-        private Term CollectGoalsRec(Dictionary<Term, Term> memo, Term t, List<Term> goals, List<Term> cruft)

+        private Term CollectGoalsRec(TermDict< Term> memo, Term t, List<Term> goals, List<Term> cruft)

         {

             Term res;

             if (memo.TryGetValue(t, out res))

@@ -869,11 +877,11 @@ namespace Microsoft.Boogie
 

         private void CollectGoals(Term t, List<Term> goals, List<Term> cruft)

         {

-            Dictionary<Term, Term> memo = new Dictionary<Term, Term>();

+            TermDict< Term> memo = new TermDict< Term>();

             CollectGoalsRec(memo, t.GetAppArgs()[1], goals, cruft);

         }

 

-        private Term SubstRec(Dictionary<Term, Term> memo, Term t)

+        private Term SubstRec(TermDict< Term> memo, Term t)

         {

             Term res;

             if (memo.TryGetValue(t, out res))

@@ -890,7 +898,7 @@ namespace Microsoft.Boogie
             return res;

         }

 

-        private Term SubstRecGoals(Dictionary<Term, Term> memo, Term t)

+        private Term SubstRecGoals(TermDict< Term> memo, Term t)

         {

             Term res;

             if (memo.TryGetValue(t, out res))

@@ -957,7 +965,7 @@ namespace Microsoft.Boogie
                 CollectGoals(sm, goals,cruft);

                 foreach (var goal in goals)

                 {

-                    Dictionary<Term, Term> memo = new Dictionary<Term, Term>();

+                    TermDict< Term> memo = new TermDict< Term>();

                     foreach (var othergoal in goals)

                         memo.Add(othergoal, othergoal.Equals(goal) ? ctx.MkFalse() : ctx.MkTrue());

                     foreach (var thing in cruft)

@@ -967,7 +975,7 @@ namespace Microsoft.Boogie
                     vcs.Add(vc);

                 }

                 {

-                    Dictionary<Term, Term> memo = new Dictionary<Term, Term>();

+                    TermDict< Term> memo = new TermDict< Term>();

                     foreach (var othergoal in goals)

                         memo.Add(othergoal, ctx.MkTrue());

                     var vc = SubstRecGoals(memo, sm);

@@ -1078,7 +1086,7 @@ namespace Microsoft.Boogie
 

         // Collect the relational paremeters

 

-        private Term CollectParamsRec(Dictionary<Term, Term> memo, Term t, List<FuncDecl> parms, List<RPFP.Node> nodes)

+        private Term CollectParamsRec(TermDict<Term> memo, Term t, List<FuncDecl> parms, List<RPFP.Node> nodes, Dictionary<Term,Term> done)

         {

             Term res;

             if (memo.TryGetValue(t, out res))

@@ -1088,14 +1096,20 @@ namespace Microsoft.Boogie
             {

                 var f = t.GetAppDecl();

                 var args = t.GetAppArgs();

-                args = args.Select(x => CollectParamsRec(memo, x, parms, nodes)).ToArray();

+                args = args.Select(x => CollectParamsRec(memo, x, parms, nodes, done)).ToArray();

                 StratifiedInliningInfo info;

                 if (relationToProc.TryGetValue(f, out info))

                 {

-                    f = SuffixFuncDecl(t, parms.Count);

-                    parms.Add(f);

-                    nodes.Add(info.node);

-                    res = ctx.MkApp(f, args);

+                    if (done.ContainsKey(t))

+                        res = done[t];

+                    else

+                    {

+                        f = SuffixFuncDecl(t, parms.Count);

+                        parms.Add(f);

+                        nodes.Add(info.node);

+                        res = ctx.MkApp(f, args);

+                        done.Add(t,res); // don't count same expression twice!

+                    }

                 }

                 else

                     res = ctx.CloneApp(t, args);

@@ -1111,8 +1125,9 @@ namespace Microsoft.Boogie
             Term[] paramTerms = info.interfaceExprVars.Select(x => boogieContext.VCExprToTerm(x, linOptions)).ToArray();

             var relParams = new List<FuncDecl>();

             var nodeParams = new List<RPFP.Node>();

-            var memo = new Dictionary<Term, Term>();

-            vcTerm = CollectParamsRec(memo, vcTerm, relParams, nodeParams);

+            var memo = new TermDict< Term>();

+            var done = new Dictionary<Term,Term>(); // note this hashes on equality, not reference!

+            vcTerm = CollectParamsRec(memo, vcTerm, relParams, nodeParams,done);

             // var ops = new Util.ContextOps(ctx);

             // var foo = ops.simplify_lhs(vcTerm);

             // vcTerm = foo.Item1;

@@ -1430,7 +1445,7 @@ namespace Microsoft.Boogie
                         // start = DateTime.Now;

                         Counterexample cex = CreateBoogieCounterExample(cexroot.owner, cexroot, impl);

                         // cexroot.owner.DisposeDualModel();

-                        cex.Print(0);  // TODO: just for testing

+                        // cex.Print(0);  // just for testing

                         collector.OnCounterexample(cex, "assertion failure");

                         Console.WriteLine("cex: {0}s", (DateTime.Now - start).TotalSeconds);

                         return VC.ConditionGeneration.Outcome.Errors;

@@ -1471,7 +1486,7 @@ namespace Microsoft.Boogie
             labels = new Dictionary<string, Term>();

             foreach(var e in rpfp.edges){

                 int id = e.number;

-                HashSet<Term> memo = new HashSet<Term>();

+                HashSet<Term> memo = new HashSet<Term>(ReferenceComparer<Term>.Instance);

                 FindLabelsRec(memo, e.F.Formula, labels);

             }

         }

diff --git a/Source/VCGeneration/RPFP.cs b/Source/VCGeneration/RPFP.cs
index f6a42a43..e7df7be6 100644
--- a/Source/VCGeneration/RPFP.cs
+++ b/Source/VCGeneration/RPFP.cs
@@ -159,7 +159,7 @@ namespace Microsoft.Boogie
             public Edge map;

             public HashSet<string> labels;

             internal Term dual;

-            internal Dictionary<Term,Term> valuation;

+            internal TermDict<Term> valuation;

         }

 

         

@@ -263,7 +263,7 @@ namespace Microsoft.Boogie
         public Term Eval(Edge e, Term t)

         {

             if (e.valuation == null)

-                e.valuation = new Dictionary<Term, Term>();

+                e.valuation = new TermDict< Term>();

             if (e.valuation.ContainsKey(t))

                 return e.valuation[t];

             return null; // TODO

@@ -275,7 +275,7 @@ namespace Microsoft.Boogie
         public void SetValue(Edge e, Term variable, Term value)

         {

             if (e.valuation == null)

-                e.valuation = new Dictionary<Term, Term>(); 

+                e.valuation = new TermDict< Term>(); 

             e.valuation.Add(variable, value);

         }

 

@@ -369,8 +369,8 @@ namespace Microsoft.Boogie
         // Collect the relational paremeters

 

         Dictionary<FuncDecl, Node> relationToNode = new Dictionary<FuncDecl, Node>();

-        

-        private Term CollectParamsRec(Dictionary<Term, Term> memo, Term t, List<FuncDecl> parms, List<RPFP.Node> nodes)

+

+        private Term CollectParamsRec(TermDict<Term> memo, Term t, List<FuncDecl> parms, List<RPFP.Node> nodes, Dictionary<Term, Term> done)

         {

             Term res;

             if (memo.TryGetValue(t, out res))

@@ -381,12 +381,18 @@ namespace Microsoft.Boogie
                 Node node;

                 if (relationToNode.TryGetValue(f, out node))

                 {

-                    f = SuffixFuncDecl(t, parms.Count);

-                    parms.Add(f);

-                    nodes.Add(node);

+                    if (done.ContainsKey(t))

+                        res = done[t];

+                    else

+                    {

+                        f = SuffixFuncDecl(t, parms.Count);

+                        parms.Add(f);

+                        nodes.Add(node);

+                        done.Add(t,res); // don't count same expression twice!

+                    }

                 }

                 var args = t.GetAppArgs();

-                args = args.Select(x => CollectParamsRec(memo, x, parms, nodes)).ToArray();

+                args = args.Select(x => CollectParamsRec(memo, x, parms, nodes, done)).ToArray();

                 res = ctx.CloneApp(t, args);

             } // TODO: handle quantifiers

             else

@@ -399,7 +405,7 @@ namespace Microsoft.Boogie
         {

             // TODO: is this right?

             // return t.IsFunctionApp() && t.GetAppArgs().Length == 0;

-            return t is VCExprVar;

+            return t is VCExprVar && !(t is VCExprConstant);

         }

 

         private Edge GetEdgeFromClause(Term t, FuncDecl failName)

@@ -428,8 +434,9 @@ namespace Microsoft.Boogie
                 }

             var relParams = new List<FuncDecl>();

             var nodeParams = new List<RPFP.Node>();

-            var memo = new Dictionary<Term, Term>();

-            body = CollectParamsRec(memo, body, relParams, nodeParams);

+            var memo = new TermDict< Term>();

+            var done = new Dictionary<Term, Term>(); // note this hashes on equality, not reference!

+            body = CollectParamsRec(memo, body, relParams, nodeParams,done);

             Transformer F = CreateTransformer(relParams.ToArray(), _IndParams, body);

             Node parent = relationToNode[Name];

             return CreateEdge(parent, F, nodeParams.ToArray());

@@ -504,7 +511,7 @@ namespace Microsoft.Boogie
             return query;

         }

 

-        private void CollectVariables(Dictionary<Term, bool> memo, Term t, List<Term> vars)

+        private void CollectVariables(TermDict< bool> memo, Term t, List<Term> vars)

         {

             if (memo.ContainsKey(t))

                 return;

@@ -520,13 +527,13 @@ namespace Microsoft.Boogie
 

         private Term BindVariables(Term t, bool universal = true)

         {

-            Dictionary<Term, bool> memo = new Dictionary<Term,bool>();

+            TermDict< bool> memo = new TermDict<bool>();

             List<Term> vars = new List<Term>();

             CollectVariables(memo,t,vars);

             return universal ? ctx.MkForall(vars.ToArray(), t) : ctx.MkExists(vars.ToArray(), t);

         }

 

-        private Term SubstPredsRec(Dictionary<Term, Term> memo, Dictionary<FuncDecl,FuncDecl> subst, Term t)

+        private Term SubstPredsRec(TermDict< Term> memo, Dictionary<FuncDecl,FuncDecl> subst, Term t)

         {

             Term res;

             if (memo.TryGetValue(t, out res))

@@ -554,7 +561,7 @@ namespace Microsoft.Boogie
 

         private Term SubstPreds(Dictionary<FuncDecl, FuncDecl> subst, Term t)

         {

-            Dictionary<Term, Term> memo = new Dictionary<Term, Term>();

+            TermDict< Term> memo = new TermDict< Term>();

             return SubstPredsRec(memo, subst, t);

         }

 

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 81c37d8d..f90788d7 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -309,8 +309,8 @@ namespace VC {
     public Dictionary<string, StratifiedInliningInfo> implName2StratifiedInliningInfo;

     public ProverInterface prover;

 

-    public StratifiedVCGenBase(Program program, string/*?*/ logFilePath, bool appendLogFile)

-      : base(program, logFilePath, appendLogFile) {

+    public StratifiedVCGenBase(Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers)

+      : base(program, logFilePath, appendLogFile, checkers) {

       implName2StratifiedInliningInfo = new Dictionary<string, StratifiedInliningInfo>();

       prover = ProverInterface.CreateProver(program, logFilePath, appendLogFile, CommandLineOptions.Clo.ProverKillTime);

       foreach (Declaration decl in program.TopLevelDeclarations) {

@@ -510,8 +510,8 @@ namespace VC {
 

     public StratifiedVCGen(bool usePrevCallTree, Dictionary<string, int> prevCallTree, 

                            HashSet<string> procsToSkip, Dictionary<string, int> extraRecBound,

-                           Program program, string/*?*/ logFilePath, bool appendLogFile) 

-    : this(program, logFilePath, appendLogFile)

+                           Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers) 

+    : this(program, logFilePath, appendLogFile, checkers)

     {

       this.procsToSkip = new HashSet<string>(procsToSkip);

       this.extraRecBound = new Dictionary<string, int>(extraRecBound);

@@ -525,8 +525,8 @@ namespace VC {
       }

     }

 

-    public StratifiedVCGen(Program program, string/*?*/ logFilePath, bool appendLogFile)

-      : base(program, logFilePath, appendLogFile) {

+    public StratifiedVCGen(Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers)

+      : base(program, logFilePath, appendLogFile, checkers) {

       PersistCallTree = false;

       useSummary = false;

       procsThatReachedRecBound = new HashSet<string>();

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 6a0891b8..48b73bce 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -18,6 +18,7 @@ using Microsoft.Boogie.VCExprAST;
 

 namespace VC {

   using Bpl = Microsoft.Boogie;

+  using System.Threading.Tasks;

 

   public class VCGen : ConditionGeneration {

       private const bool _print_time = false;

@@ -25,8 +26,8 @@ namespace VC {
     /// Constructor.  Initializes the theorem prover.

     /// </summary>

     [NotDelayed]

-    public VCGen(Program program, string/*?*/ logFilePath, bool appendLogFile)

-      : base(program)

+    public VCGen(Program program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers)

+      : base(program, checkers)

     {

       Contract.Requires(program != null);

       this.appendLogFile = appendLogFile;

@@ -290,7 +291,7 @@ namespace VC {
         ModelViewInfo mvInfo;

         parent.PassifyImpl(impl, out mvInfo);

         Hashtable label2Absy;

-        Checker ch = parent.FindCheckerFor(impl, CommandLineOptions.Clo.SmokeTimeout);

+        Checker ch = parent.FindCheckerFor(CommandLineOptions.Clo.SmokeTimeout);

         Contract.Assert(ch != null);

 

         var exprGen = ch.TheoremProver.Context.ExprGen;

@@ -312,8 +313,9 @@ namespace VC {
           Emit();

         }

         ch.BeginCheck(cce.NonNull(impl.Name + "_smoke" + id++), vc, new ErrorHandler(label2Absy, this.callback));

-        ch.ProverDone.WaitOne();

+        ch.ProverTask.Wait();

         ProverInterface.Outcome outcome = ch.ReadOutcome();

+        ch.GoBackToIdle();

         parent.CurrentLocalVariables = null;

 

         DateTime end = DateTime.UtcNow;

@@ -1135,10 +1137,10 @@ namespace VC {
         }

       }

 

-      public WaitHandle ProverDone {

+      public Task ProverTask {

         get {

           Contract.Assert(checker != null);

-          return checker.ProverDone;

+          return checker.ProverTask;

         }

       }

 

@@ -1191,7 +1193,7 @@ namespace VC {
 

         impl.Blocks = blocks;

 

-        checker = parent.FindCheckerFor(impl, timeout);

+        checker = parent.FindCheckerFor(timeout);

         Hashtable/*<int, Absy!>*/ label2absy = new Hashtable/*<int, Absy!>*/();

 

         ProverInterface tp = checker.TheoremProver;

@@ -1200,7 +1202,7 @@ namespace VC {
         bet.SetCodeExprConverter(

           new CodeExprConverter(

           delegate (CodeExpr codeExpr, Hashtable/*<Block, VCExprVar!>*/ blockVariables, List<VCExprLetBinding/*!*/> bindings) {

-            VCGen vcgen = new VCGen(new Program(), null, false);

+            VCGen vcgen = new VCGen(new Program(), null, false, parent.checkers);

             vcgen.variable2SequenceNumber = new Hashtable/*Variable -> int*/();

             vcgen.incarnationOriginMap = new Dictionary<Incarnation, Absy>();

             vcgen.CurrentLocalVariables = codeExpr.LocVars;

@@ -1410,7 +1412,11 @@ namespace VC {
       }

 

       ModelViewInfo mvInfo;

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

+      Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins;

+      lock (program)

+      {

+        gotoCmdOrigins = PassifyImpl(impl, out mvInfo);

+      }

 

       double max_vc_cost = CommandLineOptions.Clo.VcsMaxCost;

       int tmp_max_vc_cost = -1, max_splits = CommandLineOptions.Clo.VcsMaxSplits, 

@@ -1424,7 +1430,7 @@ namespace VC {
 

       Outcome outcome = Outcome.Correct;

 

-      int cores = CommandLineOptions.Clo.VcsCores;

+      Cores = CommandLineOptions.Clo.VcsCores;

       Stack<Split> work = new Stack<Split>();

       List<Split> currently_running = new List<Split>();

       ResetPredecessors(impl.Blocks);

@@ -1441,11 +1447,11 @@ namespace VC {
         remaining_cost = work.Peek().Cost;

       }

 

-      while (work.Count > 0 || currently_running.Count > 0) {

+      while (work.Any() || currently_running.Any()) {

         bool prover_failed = false;

         Split s;

 

-        if (work.Count > 0 && currently_running.Count < cores) {

+        if (work.Any() && currently_running.Count < Cores) {

           s = work.Pop();

 

           if (first_round && max_splits > 1) {

@@ -1459,21 +1465,22 @@ namespace VC {
             callback.OnProgress("VCprove", no < 0 ? 0 : no, total, proven_cost / (remaining_cost + proven_cost));

 

             Contract.Assert(s.parent == this);

-            s.BeginCheck(callback, mvInfo, no, 

-              (keep_going && s.LastChance) ? CommandLineOptions.Clo.VcsFinalAssertTimeout :

-                keep_going ? CommandLineOptions.Clo.VcsKeepGoingTimeout :

-                             CommandLineOptions.Clo.ProverKillTime);

+            lock (program)

+            {

+              s.BeginCheck(callback, mvInfo, no,

+                (keep_going && s.LastChance) ? CommandLineOptions.Clo.VcsFinalAssertTimeout :

+                  keep_going ? CommandLineOptions.Clo.VcsKeepGoingTimeout :

+                               CommandLineOptions.Clo.ProverKillTime);

+            }

 

             no++;

 

             currently_running.Add(s);

           }

         } else {

-          WaitHandle[] handles = new WaitHandle[currently_running.Count];

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

-            handles[i] = currently_running[i].ProverDone;

-          }

-          int index = WaitHandle.WaitAny(handles);

+          // Wait for one split to terminate.

+          var tasks = currently_running.Select(splt => splt.ProverTask).ToArray();

+          int index = Task.WaitAny(tasks);          

           s = currently_running[index];

           currently_running.RemoveAt(index);

 

@@ -1504,6 +1511,8 @@ namespace VC {
             break;

           }

 

+          s.Checker.GoBackToIdle();

+

           Contract.Assert( prover_failed || outcome == Outcome.Correct || outcome == Outcome.Errors || outcome == Outcome.Inconclusive);

         }

 

@@ -1547,7 +1556,10 @@ namespace VC {
       }

 

       if (outcome == Outcome.Correct && smoke_tester != null) {

-        smoke_tester.Test();

+        lock (program)

+        {

+          smoke_tester.Test();

+        }

       }

 

       callback.OnProgress("done", 0, 0, 1.0);