Merge

17 files changed, 1106 insertions, 484 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 7eacf697..7e0e9732 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -100,27 +100,5 @@ namespace Microsoft.Boogie {
         Console.ReadLine();

       }

     }

-    

-

-    #region // TODO: Is this still used?

-

-    enum FileType

-    {

-      Unknown,

-      Cil,

-      Bpl,

-      Dafny

-    };

-

-

-    static bool ProgramHasDebugInfo(Program program)

-    {

-      Contract.Requires(program != null);

-      // We inspect the last declaration because the first comes from the prelude and therefore always has source context.

-      return program.TopLevelDeclarations.Count > 0 &&

-          ((cce.NonNull(program.TopLevelDeclarations)[program.TopLevelDeclarations.Count - 1]).tok.IsValid);

-    }

-

-    #endregion

   }

 }

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 55b37f13..c20798b2 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -1794,6 +1794,16 @@ namespace Microsoft.Boogie {
       this.OutParams = that.OutParams;

     }

 

+    public string Checksum

+    {

+      get

+      {

+        return FindStringAttribute("checksum");

+      }

+    }

+

+    public string DependenciesChecksum { get; set; }

+

     protected void EmitSignature(TokenTextWriter stream, bool shortRet) {

       Contract.Requires(stream != null);

       Type.EmitOptionalTypeParams(stream, TypeParameters);

@@ -1945,6 +1955,7 @@ namespace Microsoft.Boogie {
 

     // the body is only set if the function is declared with {:inline}

     public Expr Body;

+    public Axiom DefinitionAxiom;

     public bool doingExpansion;

 

     private bool neverTrigger;

@@ -2115,7 +2126,8 @@ namespace Microsoft.Boogie {
                              new Trigger(tok, true, new ExprSeq(call), null),

                              def);

       }

-      return new Axiom(tok, def);

+      DefinitionAxiom = new Axiom(tok, def);

+      return DefinitionAxiom;

     }

   }

 

@@ -2567,14 +2579,6 @@ namespace Microsoft.Boogie {
       }

     }

 

-    public string Checksum

-    {

-      get

-      {

-        return FindStringAttribute("checksum");

-      }

-    }

-

     public string Id

     {

       get

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index dc69a3e8..fdd4d9e3 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -1451,6 +1451,9 @@ namespace Microsoft.Boogie {
       one of them to keep; otherwise, Boogie ignore the :extern declaration

       and keeps the other.

 

+    {:checksum <string>}

+      Attach a checksum to be used for verification result caching.

+

   ---- On implementations and procedures -------------------------------------

 

      {:inline N}

@@ -1478,6 +1481,14 @@ namespace Microsoft.Boogie {
        of ""assume false;"": the first one disables all verification before

        it, and the second one disables all verification after.

 

+     {:priority N}

+       Assign a positive priority 'N' to an implementation to control the order

+       in which implementations are verified (default: N = 1).

+

+     {:id <string>}

+       Assign a unique ID to an implementation to be used for verification

+       result caching (default: ""<impl. name>:0"").

+

   ---- On functions ----------------------------------------------------------

 

      {:builtin ""spec""}

@@ -1619,6 +1630,9 @@ namespace Microsoft.Boogie {
                 1 = perform live variable analysis (default)

                 2 = perform interprocedural live variable analysis

   /noVerify     skip VC generation and invocation of the theorem prover

+  /verifySnapshots

+                verify several program snapshots (named <filename>.v0.bpl

+                to <filename>.vN.bpl) using verification result caching

   /removeEmptyBlocks:<c>

                 0 - do not remove empty blocks during VC generation

                 1 - remove empty blocks (default)

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index e87ea790..2f1e4bdc 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -4,6 +4,7 @@ using System.Collections.Generic;
 using System.Diagnostics.Contracts;

 using System.IO;

 using System.Linq;

+using System.Text.RegularExpressions;

 using VC;

 using BoogiePL = Microsoft.Boogie;

 

@@ -20,7 +21,6 @@ namespace Microsoft.Boogie
     void AdvisoryWriteLine(string format, params object[] args);

     void Inform(string s);

     void WriteTrailer(int verified, int errors, int inconclusives, int timeOuts, int outOfMemories);

-    void ReportAllBplErrors(QKeyValue attr);

     void ReportBplError(IToken tok, string message, bool error, bool showBplLocation);

   }

 

@@ -121,23 +121,6 @@ namespace Microsoft.Boogie
     }

 

 

-    public void ReportAllBplErrors(QKeyValue attr)

-    {

-      while (attr != null)

-      {

-        if (attr.Key == "msg" && attr.Params.Count == 1)

-        {

-          var str = attr.Params[0] as string;

-          if (str != null)

-          {

-            ReportBplError(attr.tok, "Error: " + str, false, true);

-          }

-        }

-        attr = attr.Next;

-      }

-    }

-

-

     public virtual void ReportBplError(IToken tok, string message, bool error, bool showBplLocation)

     {

       Contract.Requires(message != null);

@@ -182,13 +165,13 @@ namespace Microsoft.Boogie
 

   public class ErrorInformationFactory

   {

-    public virtual ErrorInformation CreateErrorInformation(IToken tok, string msg)

+    public virtual ErrorInformation CreateErrorInformation(IToken tok, string msg, string requestId = null)

     {

       Contract.Requires(tok != null);

       Contract.Requires(1 <= tok.line && 1 <= tok.col);

       Contract.Requires(msg != null);

 

-      return ErrorInformation.CreateErrorInformation(tok, msg);

+      return ErrorInformation.CreateErrorInformation(tok, msg, requestId);

     }

   }

 

@@ -198,6 +181,7 @@ namespace Microsoft.Boogie
     public IToken Tok;

     public string Msg;

     public readonly List<AuxErrorInfo> Aux = new List<AuxErrorInfo>();

+    public string RequestId { get; set; }

 

     public struct AuxErrorInfo

     {

@@ -221,9 +205,11 @@ namespace Microsoft.Boogie
       Msg = CleanUp(msg);

     }

 

-    internal static ErrorInformation CreateErrorInformation(IToken tok, string msg)

+    internal static ErrorInformation CreateErrorInformation(IToken tok, string msg, string requestId = null)

     {

-      return new ErrorInformation(tok, msg);

+      var result = new ErrorInformation(tok, msg);

+      result.RequestId = requestId;

+      return result;

     }

 

     public virtual void AddAuxInfo(IToken tok, string msg)

@@ -234,22 +220,6 @@ namespace Microsoft.Boogie
       Aux.Add(new AuxErrorInfo(tok, msg));

     }

 

-    public void AddAuxInfo(QKeyValue attr)

-    {

-      while (attr != null)

-      {

-        if (attr.Key == "msg" && attr.Params.Count == 1 && attr.tok.line != 0 && attr.tok.col != 0)

-        {

-          var str = attr.Params[0] as string;

-          if (str != null)

-          {

-            AddAuxInfo(attr.tok, str);

-          }

-        }

-        attr = attr.Next;

-      }

-    }

-

     protected static string CleanUp(string msg)

     {

       if (msg.ToLower().StartsWith("error: "))

@@ -266,12 +236,51 @@ namespace Microsoft.Boogie
   #endregion

 

 

+  public class VerificationResult

+  {

+    public readonly string Checksum;

+    public readonly string DependeciesChecksum;

+    public readonly string RequestId;

+

+    public DateTime Start { get; set; }

+    public DateTime End { get; set; }

+

+    public int ProofObligationCount { get { return ProofObligationCountAfter - ProofObligationCountBefore; } }

+    public int ProofObligationCountBefore { get; set; }

+    public int ProofObligationCountAfter { get; set; }

+    public int ErrorCount { get; set; }

+    public int VerifiedCount { get; set; }

+    public int InconclusiveCount { get; set; }

+    public int TimeOutCount { get; set; }

+    public int OutOfMemoryCount { get; set; }

+

+    public ConditionGeneration.Outcome Outcome;

+    public List<Counterexample> Errors;

+

+    public VerificationResult(string requestId, string checksum, string depsChecksum, ConditionGeneration.Outcome outcome, List<Counterexample> errors)

+      : this(requestId, checksum, depsChecksum)

+    {

+      Outcome = outcome;

+      Errors = errors;

+    }

+

+    public VerificationResult(string requestId, string checksum, string depsChecksum)

+    {

+      Checksum = checksum;

+      DependeciesChecksum = depsChecksum;

+      RequestId = requestId;

+    }

+  }

+

+

   public class ExecutionEngine

   {

     public static OutputPrinter printer;

 

     public static ErrorInformationFactory errorInformationFactory = new ErrorInformationFactory();

 

+    public readonly static VerificationResultCache Cache = new VerificationResultCache();

+

     static LinearTypechecker linearTypechecker;

 

 

@@ -620,16 +629,16 @@ namespace Microsoft.Boogie
     /// </summary>

     public static PipelineOutcome InferAndVerify(Program program,

                                                  out int errorCount, out int verified, out int inconclusives, out int timeOuts, out int outOfMemories,

-                                                 ErrorReporterDelegate er = null)

+                                                 ErrorReporterDelegate er = null, string requestId = null)

     {

       Contract.Requires(program != null);

       Contract.Ensures(0 <= Contract.ValueAtReturn(out inconclusives) && 0 <= Contract.ValueAtReturn(out timeOuts));

 

       errorCount = verified = inconclusives = timeOuts = outOfMemories = 0;

 

-      // ---------- Infer invariants --------------------------------------------------------

+      #region Infer invariants using Abstract Interpretation

 

-      // Abstract interpretation -> Always use (at least) intervals, if not specified otherwise (e.g. with the "/noinfer" switch)

+      // Always use (at least) intervals, if not specified otherwise (e.g. with the "/noinfer" switch)

       if (CommandLineOptions.Clo.UseAbstractInterpretation)

       {

         if (!CommandLineOptions.Clo.Ai.J_Intervals && !CommandLineOptions.Clo.Ai.J_Trivial)

@@ -640,6 +649,10 @@ namespace Microsoft.Boogie
       }

       Microsoft.Boogie.AbstractInterpretation.NativeAbstractInterpretation.RunAbstractInterpretation(program);

 

+      #endregion

+

+      #region Do some preprocessing on the program (e.g., loop unrolling, lambda expansion)

+

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

       {

         program.UnrollLoops(CommandLineOptions.Clo.LoopUnrollCount, CommandLineOptions.Clo.SoundLoopUnrolling);

@@ -662,7 +675,7 @@ namespace Microsoft.Boogie
         //PrintBplFile ("-", program, true);

       }

 

-      // ---------- Verify ------------------------------------------------------------

+      #endregion

 

       if (!CommandLineOptions.Clo.Verify)

       {

@@ -672,68 +685,11 @@ namespace Microsoft.Boogie
       #region Run Houdini and verify

       if (CommandLineOptions.Clo.ContractInfer)

       {

-        if (CommandLineOptions.Clo.AbstractHoudini != null)

-        {

-          //CommandLineOptions.Clo.PrintErrorModel = 1;

-          CommandLineOptions.Clo.UseProverEvaluate = true;

-          CommandLineOptions.Clo.ModelViewFile = "z3model";

-          CommandLineOptions.Clo.UseArrayTheory = true;

-          CommandLineOptions.Clo.TypeEncodingMethod = CommandLineOptions.TypeEncoding.Monomorphic;

-          Houdini.AbstractDomainFactory.Initialize();

-          var domain = Houdini.AbstractDomainFactory.GetInstance(CommandLineOptions.Clo.AbstractHoudini);

-

-          // Run Abstract Houdini

-          var abs = new Houdini.AbsHoudini(program, domain);

-          var absout = abs.ComputeSummaries();

-          ProcessOutcome(absout.outcome, absout.errors, "", ref errorCount, ref verified, ref inconclusives, ref timeOuts, ref outOfMemories, er);

-

-          //Houdini.PredicateAbs.Initialize(program);

-          //var abs = new Houdini.AbstractHoudini(program);

-          //abs.computeSummaries(new Houdini.PredicateAbs(program.TopLevelDeclarations.OfType<Implementation>().First().Name));

-

-          return PipelineOutcome.Done;

-        }

-        Houdini.Houdini houdini = new Houdini.Houdini(program);

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

-        if (CommandLineOptions.Clo.PrintAssignment)

-        {

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

-          foreach (var x in outcome.assignment)

-          {

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

-          }

-        }

-        if (CommandLineOptions.Clo.Trace)

-        {

-          int numTrueAssigns = 0;

-          foreach (var x in outcome.assignment)

-          {

-            if (x.Value)

-              numTrueAssigns++;

-          }

-          Console.WriteLine("Number of true assignments = " + numTrueAssigns);

-          Console.WriteLine("Number of false assignments = " + (outcome.assignment.Count - numTrueAssigns));

-          Console.WriteLine("Prover time = " + Houdini.HoudiniSession.proverTime.ToString("F2"));

-          Console.WriteLine("Unsat core prover time = " + Houdini.HoudiniSession.unsatCoreProverTime.ToString("F2"));

-          Console.WriteLine("Number of prover queries = " + Houdini.HoudiniSession.numProverQueries);

-          Console.WriteLine("Number of unsat core prover queries = " + Houdini.HoudiniSession.numUnsatCoreProverQueries);

-          Console.WriteLine("Number of unsat core prunings = " + Houdini.HoudiniSession.numUnsatCorePrunings);

-        }

-

-        foreach (Houdini.VCGenOutcome x in outcome.implementationOutcomes.Values)

-        {

-          ProcessOutcome(x.outcome, x.errors, "", ref errorCount, ref verified, ref inconclusives, ref timeOuts, ref outOfMemories, er);

-        }

-        //errorCount = outcome.ErrorCount;

-        //verified = outcome.Verified;

-        //inconclusives = outcome.Inconclusives;

-        //timeOuts = outcome.TimeOuts;

-        //outOfMemories = 0;

-        return PipelineOutcome.Done;

+        return RunHoudini(program, ref errorCount, ref verified, ref inconclusives, ref timeOuts, ref outOfMemories, er);

       }

       #endregion

 

-      #region Verify each implementation

+      #region Set up the VC generation

 

       ConditionGeneration vcgen = null;

       try

@@ -761,144 +717,239 @@ namespace Microsoft.Boogie
         return PipelineOutcome.FatalError;

       }

 

+      #endregion

+

+      #region Select and prioritize implementations that should be verified

+

+      var impls = program.TopLevelDeclarations.OfType<Implementation>().Where(

+        impl => impl != null && CommandLineOptions.Clo.UserWantsToCheckRoutine(cce.NonNull(impl.Name)) && !impl.SkipVerification);

+

       // operate on a stable copy, in case it gets updated while we're running

-      var decls = program.TopLevelDeclarations.ToArray();

+      Implementation[] stablePrioritizedImpls = null;

+      if (CommandLineOptions.Clo.VerifySnapshots)

+      {

+        impls.Iter(impl => { impl.DependenciesChecksum = DependencyCollector.DependenciesChecksum(impl); });

+        stablePrioritizedImpls = impls.OrderByDescending(

+          impl => impl.Priority != 1 ? impl.Priority : Cache.VerificationPriority(impl)).ToArray();

+      }

+      else

+      {

+        stablePrioritizedImpls = impls.OrderByDescending(impl => impl.Priority).ToArray();

+      }

 

-      var impls =

-        from d in decls

-        where d != null && d is Implementation && CommandLineOptions.Clo.UserWantsToCheckRoutine(cce.NonNull(((Implementation)d).Name)) && !((Implementation)d).SkipVerification

-        select (Implementation)d;

+      #endregion

 

-      var prioritizedImpls =

-        from i in impls

-        orderby i.Priority descending

-        select i;

+      #region Verify each implementation

 

-      foreach (var impl in prioritizedImpls)

+      foreach (var impl in stablePrioritizedImpls)

       {

-        int prevAssertionCount = vcgen.CumulativeAssertionCount;

-        List<Counterexample/*!*/>/*?*/ errors;

+        VerificationResult verificationResult = null;

 

-        DateTime start = new DateTime();  // to please compiler's definite assignment rules

-        if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.TraceProofObligations || CommandLineOptions.Clo.XmlSink != null)

+        printer.Inform(string.Format("\nVerifying {0} ...", impl.Name));

+

+        if (CommandLineOptions.Clo.VerifySnapshots)

         {

-          start = DateTime.UtcNow;

-          if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.TraceProofObligations)

-          {

-            Console.WriteLine();

-            Console.WriteLine("Verifying {0} ...", impl.Name);

-          }

-          if (CommandLineOptions.Clo.XmlSink != null)

-          {

-            CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, start);

-          }

+          verificationResult = Cache.Lookup(impl);

         }

 

-        VCGen.Outcome outcome;

-        try

+        if (verificationResult == null)

         {

-          if (CommandLineOptions.Clo.inferLeastForUnsat != null)

+          #region Verify the implementation

+

+          verificationResult = new VerificationResult(requestId, impl.Checksum, impl.DependenciesChecksum);

+          verificationResult.ProofObligationCountBefore = vcgen.CumulativeAssertionCount;

+          verificationResult.Start = DateTime.UtcNow;

+

+          if (CommandLineOptions.Clo.XmlSink != null)

           {

-            var svcgen = vcgen as VC.StratifiedVCGen;

-            Contract.Assert(svcgen != null);

-            var ss = new HashSet<string>();

-            foreach (var tdecl in program.TopLevelDeclarations)

-            {

-              var c = tdecl as Constant;

-              if (c == null || !c.Name.StartsWith(CommandLineOptions.Clo.inferLeastForUnsat)) continue;

-              ss.Add(c.Name);

-            }

-            outcome = svcgen.FindLeastToVerify(impl, ref ss);

-            errors = new List<Counterexample>();

-            Console.Write("Result: ");

-            foreach (var s in ss)

-            {

-              Console.Write("{0} ", s);

-            }

-            Console.WriteLine();

+            CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, verificationResult.Start);

           }

-          else

+

+          try

           {

-            if (!VerificationResultCache.ContainsKey(impl.Id) || VerificationResultCache[impl.Id].Checksum != impl.Checksum)

-            {

-              outcome = vcgen.VerifyImplementation(impl, out errors);

-            }

-            else

+            if (CommandLineOptions.Clo.inferLeastForUnsat != null)

             {

-              if (CommandLineOptions.Clo.Trace)

+              var svcgen = vcgen as VC.StratifiedVCGen;

+              Contract.Assert(svcgen != null);

+              var ss = new HashSet<string>();

+              foreach (var tdecl in program.TopLevelDeclarations)

               {

-                Console.WriteLine("Retrieving cached verification result for implementation {0}...", impl.Name);

+                var c = tdecl as Constant;

+                if (c == null || !c.Name.StartsWith(CommandLineOptions.Clo.inferLeastForUnsat)) continue;

+                ss.Add(c.Name);

               }

-              var result = VerificationResultCache[impl.Id];

-              outcome = result.Outcome;

-              errors = result.Errors;

+              verificationResult.Outcome = svcgen.FindLeastToVerify(impl, ref ss);

+              verificationResult.Errors = new List<Counterexample>();

+              Console.WriteLine("Result: {0}", string.Join(" ", ss));

             }

-            if (CommandLineOptions.Clo.ExtractLoops && vcgen is VCGen && errors != null)

+            else

             {

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

+              verificationResult.Outcome = vcgen.VerifyImplementation(impl, out verificationResult.Errors, requestId);

+

+              if (CommandLineOptions.Clo.ExtractLoops && verificationResult.Errors != null)

               {

-                errors[i] = (vcgen as VCGen).extractLoopTrace(errors[i], impl.Name, program, extractLoopMappingInfo);

+                var vcg = vcgen as VCGen;

+                if (vcg != null)

+                {

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

+                  {

+                    verificationResult.Errors[i] = vcg.extractLoopTrace(verificationResult.Errors[i], impl.Name, program, extractLoopMappingInfo);

+                  }

+                }

               }

             }

           }

-        }

-        catch (VCGenException e)

-        {

-          printer.ReportBplError(impl.tok, String.Format("Error BP5010: {0}  Encountered in implementation {1}.", e.Message, impl.Name), true, true);

-          errors = null;

-          outcome = VCGen.Outcome.Inconclusive;

-        }

-        catch (UnexpectedProverOutputException upo)

-        {

-          printer.AdvisoryWriteLine("Advisory: {0} SKIPPED because of internal error: unexpected prover output: {1}", impl.Name, upo.Message);

-          errors = null;

-          outcome = VCGen.Outcome.Inconclusive;

-        }

+          catch (VCGenException e)

+          {

+            printer.ReportBplError(impl.tok, String.Format("Error BP5010: {0}  Encountered in implementation {1}.", e.Message, impl.Name), true, true);

+            verificationResult.Errors = null;

+            verificationResult.Outcome = VCGen.Outcome.Inconclusive;

+          }

+          catch (UnexpectedProverOutputException upo)

+          {

+            printer.AdvisoryWriteLine("Advisory: {0} SKIPPED because of internal error: unexpected prover output: {1}", impl.Name, upo.Message);

+            verificationResult.Errors = null;

+            verificationResult.Outcome = VCGen.Outcome.Inconclusive;

+          }

 

-        string timeIndication = "";

-        DateTime end = DateTime.UtcNow;

-        TimeSpan elapsed = end - start;

-        if (CommandLineOptions.Clo.Trace)

-        {

-          int poCount = vcgen.CumulativeAssertionCount - prevAssertionCount;

-          timeIndication = string.Format("  [{0:F3} s, {1} proof obligation{2}]  ", elapsed.TotalSeconds, poCount, poCount == 1 ? "" : "s");

+          verificationResult.ProofObligationCountAfter = vcgen.CumulativeAssertionCount;

+          verificationResult.End = DateTime.UtcNow;

+

+          #endregion

+

+          #region Cache the verification result

+

+          if (CommandLineOptions.Clo.VerifySnapshots && !string.IsNullOrEmpty(impl.Checksum))

+          {

+            Cache.Insert(impl.Id, verificationResult);

+          }

+

+          #endregion

         }

-        else if (CommandLineOptions.Clo.TraceProofObligations)

+        else

         {

-          int poCount = vcgen.CumulativeAssertionCount - prevAssertionCount;

-          timeIndication = string.Format("  [{0} proof obligation{1}]  ", poCount, poCount == 1 ? "" : "s");

-        }

+          if (CommandLineOptions.Clo.XmlSink != null)

+          {

+            CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, verificationResult.Start);

+          }

 

-        if (CommandLineOptions.Clo.VerifySnapshots && !string.IsNullOrEmpty(impl.Checksum))

-        {

-          var result = new VerificationResult(impl.Checksum, outcome, errors);

-          VerificationResultCache[impl.Id] = result;

+          printer.Inform(string.Format("Retrieving cached verification result for implementation {0}...", impl.Name));

         }

 

-        ProcessOutcome(outcome, errors, timeIndication, ref errorCount, ref verified, ref inconclusives, ref timeOuts, ref outOfMemories, er, impl);

+        #region Process the verification results and statistics

+

+        ProcessOutcome(verificationResult.Outcome, verificationResult.Errors, TimeIndication(verificationResult), ref errorCount, ref verified, ref inconclusives, ref timeOuts, ref outOfMemories, er, impl, verificationResult.RequestId);

 

         if (CommandLineOptions.Clo.XmlSink != null)

         {

-          CommandLineOptions.Clo.XmlSink.WriteEndMethod(outcome.ToString().ToLowerInvariant(), end, elapsed);

+          CommandLineOptions.Clo.XmlSink.WriteEndMethod(verificationResult.Outcome.ToString().ToLowerInvariant(), verificationResult.End, verificationResult.End - verificationResult.Start);

         }

-        if (outcome == VCGen.Outcome.Errors || CommandLineOptions.Clo.Trace)

+        if (verificationResult.Outcome == VCGen.Outcome.Errors || CommandLineOptions.Clo.Trace)

         {

           Console.Out.Flush();

         }

+

+        #endregion

       }

 

       vcgen.Close();

       cce.NonNull(CommandLineOptions.Clo.TheProverFactory).Close();

 

-

       #endregion

 

       return PipelineOutcome.VerificationCompleted;

     }

 

 

-    static void ProcessOutcome(VC.VCGen.Outcome outcome, List<Counterexample> errors, string timeIndication,

-                               ref int errorCount, ref int verified, ref int inconclusives, ref int timeOuts, ref int outOfMemories, ErrorReporterDelegate er = null, Implementation impl = null)

+    private static PipelineOutcome RunHoudini(Program program, ref int errorCount, ref int verified, ref int inconclusives, ref int timeOuts, ref int outOfMemories, ErrorReporterDelegate er)

+    {

+      if (CommandLineOptions.Clo.AbstractHoudini != null)

+      {

+        return RunAbstractHoudini(program, ref errorCount, ref verified, ref inconclusives, ref timeOuts, ref outOfMemories, er);

+      }

+

+      Houdini.Houdini houdini = new Houdini.Houdini(program);

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

+

+      if (CommandLineOptions.Clo.PrintAssignment)

+      {

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

+        foreach (var x in outcome.assignment)

+        {

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

+        }

+      }

+

+      if (CommandLineOptions.Clo.Trace)

+      {

+        int numTrueAssigns = 0;

+        foreach (var x in outcome.assignment)

+        {

+          if (x.Value)

+            numTrueAssigns++;

+        }

+        Console.WriteLine("Number of true assignments = " + numTrueAssigns);

+        Console.WriteLine("Number of false assignments = " + (outcome.assignment.Count - numTrueAssigns));

+        Console.WriteLine("Prover time = " + Houdini.HoudiniSession.proverTime.ToString("F2"));

+        Console.WriteLine("Unsat core prover time = " + Houdini.HoudiniSession.unsatCoreProverTime.ToString("F2"));

+        Console.WriteLine("Number of prover queries = " + Houdini.HoudiniSession.numProverQueries);

+        Console.WriteLine("Number of unsat core prover queries = " + Houdini.HoudiniSession.numUnsatCoreProverQueries);

+        Console.WriteLine("Number of unsat core prunings = " + Houdini.HoudiniSession.numUnsatCorePrunings);

+      }

+

+      foreach (Houdini.VCGenOutcome x in outcome.implementationOutcomes.Values)

+      {

+        ProcessOutcome(x.outcome, x.errors, "", ref errorCount, ref verified, ref inconclusives, ref timeOuts, ref outOfMemories, er);

+      }

+      //errorCount = outcome.ErrorCount;

+      //verified = outcome.Verified;

+      //inconclusives = outcome.Inconclusives;

+      //timeOuts = outcome.TimeOuts;

+      //outOfMemories = 0;

+      return PipelineOutcome.Done;

+    }

+

+

+    private static PipelineOutcome RunAbstractHoudini(Program program, ref int errorCount, ref int verified, ref int inconclusives, ref int timeOuts, ref int outOfMemories, ErrorReporterDelegate er)

+    {

+      //CommandLineOptions.Clo.PrintErrorModel = 1;

+      CommandLineOptions.Clo.UseProverEvaluate = true;

+      CommandLineOptions.Clo.ModelViewFile = "z3model";

+      CommandLineOptions.Clo.UseArrayTheory = true;

+      CommandLineOptions.Clo.TypeEncodingMethod = CommandLineOptions.TypeEncoding.Monomorphic;

+      Houdini.AbstractDomainFactory.Initialize(program);

+      var domain = Houdini.AbstractDomainFactory.GetInstance(CommandLineOptions.Clo.AbstractHoudini);

+

+      // Run Abstract Houdini

+      var abs = new Houdini.AbsHoudini(program, domain);

+      var absout = abs.ComputeSummaries();

+      ProcessOutcome(absout.outcome, absout.errors, "", ref errorCount, ref verified, ref inconclusives, ref timeOuts, ref outOfMemories, er);

+

+      //Houdini.PredicateAbs.Initialize(program);

+      //var abs = new Houdini.AbstractHoudini(program);

+      //abs.computeSummaries(new Houdini.PredicateAbs(program.TopLevelDeclarations.OfType<Implementation>().First().Name));

+

+      return PipelineOutcome.Done;

+    }

+

+

+    private static string TimeIndication(VerificationResult verificationResult)

+    {

+      var result = "";

+      if (CommandLineOptions.Clo.Trace)

+      {

+        result = string.Format("  [{0:F3} s, {1} proof obligation{2}]  ", (verificationResult.End - verificationResult.Start).TotalSeconds, verificationResult.ProofObligationCount, verificationResult.ProofObligationCount == 1 ? "" : "s");

+      }

+      else if (CommandLineOptions.Clo.TraceProofObligations)

+      {

+        result = string.Format("  [{0} proof obligation{1}]  ", verificationResult.ProofObligationCount, verificationResult.ProofObligationCount == 1 ? "" : "s");

+      }

+      return result;

+    }

+

+

+    private static void ProcessOutcome(VC.VCGen.Outcome outcome, List<Counterexample> errors, string timeIndication,

+                                       ref int errorCount, ref int verified, ref int inconclusives, ref int timeOuts, ref int outOfMemories, ErrorReporterDelegate er = null, Implementation impl = null, string requestId = null)

     {

       switch (outcome)

       {

@@ -906,28 +957,20 @@ namespace Microsoft.Boogie
           Contract.Assert(false);  // unexpected outcome

           throw new cce.UnreachableException();

         case VCGen.Outcome.ReachedBound:

+          verified++;

           printer.Inform(String.Format("{0}verified", timeIndication));

           Console.WriteLine(string.Format("Stratified Inlining: Reached recursion bound of {0}", CommandLineOptions.Clo.RecursionBound));

-          verified++;

           break;

         case VCGen.Outcome.Correct:

-          if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed)

-          {

-            printer.Inform(String.Format("{0}credible", timeIndication));

-            verified++;

-          }

-          else

-          {

-            printer.Inform(String.Format("{0}verified", timeIndication));

-            verified++;

-          }

+          verified++;

+          printer.Inform(timeIndication + (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed ? "credible" : "verified"));

           break;

         case VCGen.Outcome.TimedOut:

           timeOuts++;

           printer.Inform(String.Format("{0}timed out", timeIndication));

           if (er != null && impl != null)

           {

-            er(errorInformationFactory.CreateErrorInformation(impl.tok, string.Format("Verification timed out after {0} seconds ({1})", CommandLineOptions.Clo.ProverKillTime, impl.Name)));

+            er(errorInformationFactory.CreateErrorInformation(impl.tok, string.Format("Verification timed out after {0} seconds ({1})", CommandLineOptions.Clo.ProverKillTime, impl.Name), requestId));

           }

           break;

         case VCGen.Outcome.OutOfMemory:

@@ -935,7 +978,7 @@ namespace Microsoft.Boogie
           printer.Inform(String.Format("{0}out of memory", timeIndication));

           if (er != null && impl != null)

           {

-            er(errorInformationFactory.CreateErrorInformation(impl.tok, "Verification out of memory (" + impl.Name + ")"));

+            er(errorInformationFactory.CreateErrorInformation(impl.tok, "Verification out of memory (" + impl.Name + ")", requestId));

           }

           break;

         case VCGen.Outcome.Inconclusive:

@@ -943,204 +986,181 @@ namespace Microsoft.Boogie
           printer.Inform(String.Format("{0}inconclusive", timeIndication));

           if (er != null && impl != null)

           {

-            er(errorInformationFactory.CreateErrorInformation(impl.tok, "Verification inconclusive (" + impl.Name + ")"));

+            er(errorInformationFactory.CreateErrorInformation(impl.tok, "Verification inconclusive (" + impl.Name + ")", requestId));

           }

           break;

         case VCGen.Outcome.Errors:

+          Contract.Assert(errors != null);  // guaranteed by postcondition of VerifyImplementation

           if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed)

           {

-            printer.Inform(String.Format("{0}doomed", timeIndication));

             errorCount++;

+            printer.Inform(String.Format("{0}doomed", timeIndication));

           }

-          Contract.Assert(errors != null);  // guaranteed by postcondition of VerifyImplementation

+          else

+          {

+            errorCount += errors.Count;

+          }

+          printer.Inform(String.Format("{0}error{1}", timeIndication, errors.Count == 1 ? "" : "s"));

           break;

       }

       if (errors != null)

       {

-        // BP1xxx: Parsing errors

-        // BP2xxx: Name resolution errors

-        // BP3xxx: Typechecking errors

-        // BP4xxx: Abstract interpretation errors (Is there such a thing?)

-        // BP5xxx: Verification errors

-

-        var cause = "Error";

-        if (outcome == VCGen.Outcome.TimedOut)

+        ProcessErrors(outcome, errors, er);

+      }

+    }

+

+

+    private static void ProcessErrors(VC.VCGen.Outcome outcome, List<Counterexample> errors, ErrorReporterDelegate er)

+    {

+      Contract.Requires(errors != null);

+

+      var cause = "Error";

+      if (outcome == VCGen.Outcome.TimedOut)

+      {

+        cause = "Timed out on";

+      }

+      else if (outcome == VCGen.Outcome.OutOfMemory)

+      {

+        cause = "Out of memory on";

+      }

+      // TODO(wuestholz): Take the error cause into account when writing to the XML sink.

+

+      errors.Sort(new CounterexampleComparer());

+      foreach (Counterexample error in errors)

+      {

+        var errorInfo = ReportCounterexample(cause, error);

+

+        if (CommandLineOptions.Clo.EnhancedErrorMessages == 1)

         {

-          cause = "Timed out on";

+          foreach (string info in error.relatedInformation)

+          {

+            Contract.Assert(info != null);

+            Console.WriteLine("       " + info);

+          }

         }

-        else if (outcome == VCGen.Outcome.OutOfMemory)

+        if (CommandLineOptions.Clo.ErrorTrace > 0)

         {

-          cause = "Out of memory on";

+          Console.WriteLine("Execution trace:");

+          error.Print(4, b => { errorInfo.AddAuxInfo(b.tok, "Execution trace: " + b.Label); });

         }

-        // TODO(wuestholz): Take the error cause into account when writing to the XML sink.

-

-        errors.Sort(new CounterexampleComparer());

-        foreach (Counterexample error in errors)

+        if (CommandLineOptions.Clo.ModelViewFile != null)

         {

-          ErrorInformation errorInfo;

-

-          if (error is CallCounterexample)

-          {

-            CallCounterexample err = (CallCounterexample)error;

-            if (!CommandLineOptions.Clo.ForceBplErrors && err.FailingRequires.ErrorMessage != null)

-            {

-              printer.ReportBplError(err.FailingRequires.tok, err.FailingRequires.ErrorMessage, true, false);

-            }

-            else

-            {

-              printer.ReportBplError(err.FailingCall.tok, cause + " BP5002: A precondition for this call might not hold.", true, true);

-              printer.ReportBplError(err.FailingRequires.tok, "Related location: This is the precondition that might not hold.", false, true);

-            }

+          error.PrintModel();

+        }

+        if (er != null)

+        {

+          er(errorInfo);

+        }

+      }

+    }

 

-            errorInfo = errorInformationFactory.CreateErrorInformation(err.FailingCall.tok, cause + ": " + err.FailingCall.ErrorData as string ?? "A precondition for this call might not hold.");

-            errorInfo.AddAuxInfo(err.FailingRequires.tok, err.FailingRequires.ErrorData as string ?? "Related location: This is the precondition that might not hold.");

 

-            if (CommandLineOptions.Clo.XmlSink != null)

-            {

-              CommandLineOptions.Clo.XmlSink.WriteError("precondition violation", err.FailingCall.tok, err.FailingRequires.tok, error.Trace);

-            }

-          }

-          else if (error is ReturnCounterexample)

-          {

-            ReturnCounterexample err = (ReturnCounterexample)error;

-            if (!CommandLineOptions.Clo.ForceBplErrors && err.FailingEnsures.ErrorMessage != null)

-            {

-              printer.ReportBplError(err.FailingEnsures.tok, err.FailingEnsures.ErrorMessage, true, false);

-            }

-            else

-            {

-              printer.ReportBplError(err.FailingReturn.tok, cause + " BP5003: A postcondition might not hold on this return path.", true, true);

-              printer.ReportBplError(err.FailingEnsures.tok, "Related location: This is the postcondition that might not hold.", false, true);

-            }

-            printer.ReportAllBplErrors(err.FailingEnsures.Attributes);

+    private static ErrorInformation ReportCounterexample(string cause, Counterexample error)

+    {

+      // BP1xxx: Parsing errors

+      // BP2xxx: Name resolution errors

+      // BP3xxx: Typechecking errors

+      // BP4xxx: Abstract interpretation errors (Is there such a thing?)

+      // BP5xxx: Verification errors

+

+      ErrorInformation errorInfo;

+

+      var callError = error as CallCounterexample;

+      var returnError = error as ReturnCounterexample;

+      var assertError = error as AssertCounterexample;

+      if (callError != null)

+      {

+        if (!CommandLineOptions.Clo.ForceBplErrors && callError.FailingRequires.ErrorMessage != null)

+        {

+          printer.ReportBplError(callError.FailingRequires.tok, callError.FailingRequires.ErrorMessage, true, false);

+        }

+        else

+        {

+          printer.ReportBplError(callError.FailingCall.tok, cause + " BP5002: A precondition for this call might not hold.", true, true);

+          printer.ReportBplError(callError.FailingRequires.tok, "Related location: This is the precondition that might not hold.", false, true);

+        }

 

-            errorInfo = errorInformationFactory.CreateErrorInformation(err.FailingReturn.tok, cause + ": " + "A postcondition might not hold on this return path.");

-            errorInfo.AddAuxInfo(err.FailingEnsures.tok, err.FailingEnsures.ErrorData as string ?? "Related location: This is the postcondition that might not hold.");

-            errorInfo.AddAuxInfo(err.FailingEnsures.Attributes);

+        errorInfo = errorInformationFactory.CreateErrorInformation(callError.FailingCall.tok, cause + ": " + (callError.FailingCall.ErrorData as string ?? "A precondition for this call might not hold."), callError.RequestId);

+        errorInfo.AddAuxInfo(callError.FailingRequires.tok, callError.FailingRequires.ErrorData as string ?? "Related location: This is the precondition that might not hold.");

 

-            if (CommandLineOptions.Clo.XmlSink != null)

-            {

-              CommandLineOptions.Clo.XmlSink.WriteError("postcondition violation", err.FailingReturn.tok, err.FailingEnsures.tok, error.Trace);

-            }

-          }

-          else // error is AssertCounterexample

-          {

-            AssertCounterexample err = (AssertCounterexample)error;

-            if (err.FailingAssert is LoopInitAssertCmd)

-            {

-              printer.ReportBplError(err.FailingAssert.tok, cause + " BP5004: This loop invariant might not hold on entry.", true, true);

+        if (CommandLineOptions.Clo.XmlSink != null)

+        {

+          CommandLineOptions.Clo.XmlSink.WriteError("precondition violation", callError.FailingCall.tok, callError.FailingRequires.tok, error.Trace);

+        }

+      }

+      else if (returnError != null)

+      {

+        if (!CommandLineOptions.Clo.ForceBplErrors && returnError.FailingEnsures.ErrorMessage != null)

+        {

+          printer.ReportBplError(returnError.FailingEnsures.tok, returnError.FailingEnsures.ErrorMessage, true, false);

+        }

+        else

+        {

+          printer.ReportBplError(returnError.FailingReturn.tok, cause + " BP5003: A postcondition might not hold on this return path.", true, true);

+          printer.ReportBplError(returnError.FailingEnsures.tok, "Related location: This is the postcondition that might not hold.", false, true);

+        }

 

-              errorInfo = errorInformationFactory.CreateErrorInformation(err.FailingAssert.tok, cause + ": " + "This loop invariant might not hold on entry.");

+        errorInfo = errorInformationFactory.CreateErrorInformation(returnError.FailingReturn.tok, cause + ": " + "A postcondition might not hold on this return path.", returnError.RequestId);

+        errorInfo.AddAuxInfo(returnError.FailingEnsures.tok, returnError.FailingEnsures.ErrorData as string ?? "Related location: This is the postcondition that might not hold.");

 

-              if (CommandLineOptions.Clo.XmlSink != null)

-              {

-                CommandLineOptions.Clo.XmlSink.WriteError("loop invariant entry violation", err.FailingAssert.tok, null, error.Trace);

-              }

-            }

-            else if (err.FailingAssert is LoopInvMaintainedAssertCmd)

-            {

-              // this assertion is a loop invariant which is not maintained

-              printer.ReportBplError(err.FailingAssert.tok, cause + " BP5005: This loop invariant might not be maintained by the loop.", true, true);

+        if (CommandLineOptions.Clo.XmlSink != null)

+        {

+          CommandLineOptions.Clo.XmlSink.WriteError("postcondition violation", returnError.FailingReturn.tok, returnError.FailingEnsures.tok, error.Trace);

+        }

+      }

+      else // error is AssertCounterexample

+      {

+        if (assertError.FailingAssert is LoopInitAssertCmd)

+        {

+          printer.ReportBplError(assertError.FailingAssert.tok, cause + " BP5004: This loop invariant might not hold on entry.", true, true);

 

-              errorInfo = errorInformationFactory.CreateErrorInformation(err.FailingAssert.tok, cause + ": " + "This loop invariant might not be maintained by the loop.");

+          errorInfo = errorInformationFactory.CreateErrorInformation(assertError.FailingAssert.tok, cause + ": " + "This loop invariant might not hold on entry.", assertError.RequestId);

 

-              if (CommandLineOptions.Clo.XmlSink != null)

-              {

-                CommandLineOptions.Clo.XmlSink.WriteError("loop invariant maintenance violation", err.FailingAssert.tok, null, error.Trace);

-              }

-            }

-            else

-            {

-              if (!CommandLineOptions.Clo.ForceBplErrors && err.FailingAssert.ErrorMessage != null)

-              {

-                printer.ReportBplError(err.FailingAssert.tok, err.FailingAssert.ErrorMessage, true, false);

-              }

-              else if (err.FailingAssert.ErrorData is string)

-              {

-                printer.ReportBplError(err.FailingAssert.tok, (string)err.FailingAssert.ErrorData, true, true);

-              }

-              else

-              {

-                printer.ReportBplError(err.FailingAssert.tok, cause + " BP5001: This assertion might not hold.", true, true);

-              }

-              printer.ReportAllBplErrors(err.FailingAssert.Attributes);

+          if (CommandLineOptions.Clo.XmlSink != null)

+          {

+            CommandLineOptions.Clo.XmlSink.WriteError("loop invariant entry violation", assertError.FailingAssert.tok, null, error.Trace);

+          }

+        }

+        else if (assertError.FailingAssert is LoopInvMaintainedAssertCmd)

+        {

+          printer.ReportBplError(assertError.FailingAssert.tok, cause + " BP5005: This loop invariant might not be maintained by the loop.", true, true);

 

-              var msg = err.FailingAssert.ErrorData as string;

-              if (msg == null)

-              {

-                msg = "This assertion might not hold.";

-              }

-              errorInfo = errorInformationFactory.CreateErrorInformation(err.FailingAssert.tok, cause + ": " + msg);

-              errorInfo.AddAuxInfo(err.FailingAssert.Attributes);

+          errorInfo = errorInformationFactory.CreateErrorInformation(assertError.FailingAssert.tok, cause + ": " + "This loop invariant might not be maintained by the loop.", assertError.RequestId);

 

-              if (CommandLineOptions.Clo.XmlSink != null)

-              {

-                CommandLineOptions.Clo.XmlSink.WriteError("assertion violation", err.FailingAssert.tok, null, error.Trace);

-              }

-            }

-          }

-          if (CommandLineOptions.Clo.EnhancedErrorMessages == 1)

+          if (CommandLineOptions.Clo.XmlSink != null)

           {

-            foreach (string info in error.relatedInformation)

-            {

-              Contract.Assert(info != null);

-              Console.WriteLine("       " + info);

-            }

+            CommandLineOptions.Clo.XmlSink.WriteError("loop invariant maintenance violation", assertError.FailingAssert.tok, null, error.Trace);

           }

-          if (CommandLineOptions.Clo.ErrorTrace > 0)

-          {

-            Console.WriteLine("Execution trace:");

-            error.Print(4);

+        }

+        else

+        {

 

-            foreach (Block b in error.Trace)

-            {

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

-              {

-                errorInfo.AddAuxInfo(b.tok, "Execution trace: " + b.Label);

-              }

-            }

-          }

-          if (CommandLineOptions.Clo.ModelViewFile != null)

+          var msg = assertError.FailingAssert.ErrorData as string;

+          if (!CommandLineOptions.Clo.ForceBplErrors && assertError.FailingAssert.ErrorMessage != null)

           {

-            error.PrintModel();

+            printer.ReportBplError(assertError.FailingAssert.tok, assertError.FailingAssert.ErrorMessage, true, false);

           }

-          if (cause == "Error")

+          else if (msg != null)

           {

-            errorCount++;

+            printer.ReportBplError(assertError.FailingAssert.tok, msg, true, true);

           }

-          if (er != null)

+          else

           {

-            er(errorInfo);

+            msg = "This assertion might not hold.";

+            printer.ReportBplError(assertError.FailingAssert.tok, cause + " BP5001: " + msg, true, true);

           }

-        }

-        if (cause == "Error")

-        {

-          printer.Inform(String.Format("{0}error{1}", timeIndication, errors.Count == 1 ? "" : "s"));

-        }

-      }

-    }

 

+          errorInfo = errorInformationFactory.CreateErrorInformation(assertError.FailingAssert.tok, cause + ": " + msg, assertError.RequestId);

 

-    #region Verification result caching

-

-    private struct VerificationResult

-    {

-      internal VerificationResult(string checksum, ConditionGeneration.Outcome outcome, List<Counterexample> errors)

-      {

-        Checksum = checksum;

-        Outcome = outcome;

-        Errors = errors;

+          if (CommandLineOptions.Clo.XmlSink != null)

+          {

+            CommandLineOptions.Clo.XmlSink.WriteError("assertion violation", assertError.FailingAssert.tok, null, error.Trace);

+          }

+        }

       }

-

-      public readonly string Checksum;

-      public readonly ConditionGeneration.Outcome Outcome;

-      public readonly List<Counterexample> Errors;

+      return errorInfo;

     }

 

-

-    private static readonly ConcurrentDictionary<string, VerificationResult> VerificationResultCache = new ConcurrentDictionary<string, VerificationResult>();

-

-    #endregion

   }

 

 }

diff --git a/Source/ExecutionEngine/ExecutionEngine.csproj b/Source/ExecutionEngine/ExecutionEngine.csproj
index 60c9fee1..91f13ed4 100644
--- a/Source/ExecutionEngine/ExecutionEngine.csproj
+++ b/Source/ExecutionEngine/ExecutionEngine.csproj
@@ -40,6 +40,7 @@
   <ItemGroup>

     <Compile Include="ExecutionEngine.cs" />

     <Compile Include="Properties\AssemblyInfo.cs" />

+    <Compile Include="VerificationResultCache.cs" />

   </ItemGroup>

   <ItemGroup>

     <ProjectReference Include="..\AbsInt\AbsInt.csproj">

@@ -70,6 +71,10 @@
       <Project>{cf41e903-78eb-43ba-a355-e5feb5ececd4}</Project>

       <Name>Houdini</Name>

     </ProjectReference>

+    <ProjectReference Include="..\Model\Model.csproj">

+      <Project>{acef88d5-dadd-46da-bae1-2144d63f4c83}</Project>

+      <Name>Model</Name>

+    </ProjectReference>

     <ProjectReference Include="..\ParserHelper\ParserHelper.csproj">

       <Project>{fcd3ac7f-9dfd-46c8-ab1e-09f0b0f16dc5}</Project>

       <Name>ParserHelper</Name>

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
new file mode 100644
index 00000000..5527117e
--- /dev/null
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -0,0 +1,175 @@
+using System;

+using System.Collections.Concurrent;

+using System.Collections.Generic;

+using System.Diagnostics.Contracts;

+using System.Linq;

+using System.Text;

+using System.Text.RegularExpressions;

+using VC;

+

+namespace Microsoft.Boogie

+{

+

+  class DependencyCollector : StandardVisitor

+  {

+    private HashSet<DeclWithFormals> dependencies;

+

+    public DependencyCollector()

+    {

+      dependencies = new HashSet<DeclWithFormals>();

+    }

+

+    public static void Collect(Absy node, out List<DeclWithFormals> dependencies)

+    {

+      var dc = new DependencyCollector();

+      dc.Visit(node);

+      dependencies = dc.dependencies.ToList();

+    }

+

+    public static string DependenciesChecksum(Implementation impl)

+    {

+      List<DeclWithFormals> deps;

+      DependencyCollector.Collect(impl, out deps);

+      if (deps.Any(dep => dep.Checksum == null))

+      {

+        return null;

+      }

+

+      var md5 = System.Security.Cryptography.MD5.Create();

+      var data = Encoding.UTF8.GetBytes(deps.MapConcat(dep => dep.Checksum, ""));

+      var hashedData = md5.ComputeHash(data);

+      return BitConverter.ToString(hashedData);

+    }

+

+    public override Procedure VisitProcedure(Procedure node)

+    {

+      dependencies.Add(node);

+

+      return base.VisitProcedure(node);

+    }

+

+    public override Function VisitFunction(Function node)

+    {

+      dependencies.Add(node);

+

+      return base.VisitFunction(node);

+    }

+

+    public override Cmd VisitCallCmd(CallCmd node)

+    {

+      var result = base.VisitCallCmd(node);

+

+      var visited = dependencies.Contains(node.Proc);

+      if (!visited)

+      {

+        VisitProcedure(node.Proc);

+      }

+

+      return result;

+    }

+

+    public override Expr VisitNAryExpr(NAryExpr node)

+    {

+      var result = base.VisitNAryExpr(node);

+

+      var funCall = node.Fun as FunctionCall;

+      if (funCall != null)

+      {

+        var visited = dependencies.Contains(funCall.Func);

+        if (!visited)

+        {

+          VisitFunction(funCall.Func);

+          if (funCall.Func.DefinitionAxiom != null)

+          {

+            VisitAxiom(funCall.Func.DefinitionAxiom);

+          }

+        }

+      }

+

+      return result;

+    }

+  }

+

+

+  public class VerificationResultCache

+  {

+    private readonly ConcurrentDictionary<string, VerificationResult> Cache = new ConcurrentDictionary<string, VerificationResult>();

+

+

+    public void Insert(string key, VerificationResult result)

+    {

+      Contract.Requires(key != null);

+      Contract.Requires(result != null);

+

+      Cache[key] = result;

+    }

+

+

+    public VerificationResult Lookup(string key)

+    {

+      VerificationResult result;

+      var success = Cache.TryGetValue(key, out result);

+      return success ? result : null;

+    }

+

+

+    public VerificationResult Lookup(Implementation impl)

+    {

+      if (!NeedsToBeVerified(impl))

+      {

+        return Lookup(impl.Id);

+      }

+      else

+      {

+        return null;

+      }

+    }

+

+

+    public void Clear()

+    {

+      Cache.Clear();

+    }

+

+

+    public void RemoveMatchingKeys(Regex keyRegexp)

+    {

+      foreach (var kv in Cache)

+      {

+        if (keyRegexp.IsMatch(kv.Key))

+        {

+          VerificationResult res;

+          Cache.TryRemove(kv.Key, out res);

+        }

+      }

+    }

+

+

+    public bool NeedsToBeVerified(Implementation impl)

+    {

+      return 0 < VerificationPriority(impl);

+    }

+

+

+    public int VerificationPriority(Implementation impl)

+    {

+      if (!Cache.ContainsKey(impl.Id))

+      {

+        return 3;  // high priority (has been never verified before)

+      }

+      else if (Cache[impl.Id].Checksum != impl.Checksum)

+      {

+        return 2;  // medium priority (old snapshot has been verified before)

+      }

+      else if (impl.DependenciesChecksum == null || Cache[impl.Id].DependeciesChecksum != impl.DependenciesChecksum)

+      {

+        return 1;  // low priority (the same snapshot has been verified before, but a callee has changed)

+      }

+      else

+      {

+        return 0;  // skip verification

+      }

+    }

+  }

+

+}

diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs
index dd680509..1be24e20 100644
--- a/Source/Houdini/AbstractHoudini.cs
+++ b/Source/Houdini/AbstractHoudini.cs
@@ -1443,6 +1443,279 @@ namespace Microsoft.Boogie.Houdini {
         }

     }

 

+    // foo(x) = x < 2^j for some j <= 16

+    public class PowDomain : IAbstractDomain

+    {

+        enum Val { FALSE, NEITHER, TRUE };

+        Val tlevel;

+        bool isBottom { get { return tlevel == Val.FALSE; } }

+        bool isTop { get { return tlevel == Val.TRUE; } }

+

+        readonly int Max = 16;

+

+        int upper; // <= Max

+

+        private PowDomain(Val tlevel) :

+            this(tlevel, 0) { }

+

+        private PowDomain(Val tlevel, int upper)

+        {

+            this.tlevel = tlevel;

+            this.upper = upper;

+        }

+

+        public static IAbstractDomain GetBottom()

+        {

+            return new PowDomain(Val.FALSE) as IAbstractDomain;

+        }

+

+        IAbstractDomain IAbstractDomain.Bottom()

+        {

+            return GetBottom();

+        }

+

+        IAbstractDomain IAbstractDomain.Join(List<Model.Element> state)

+        {

+            if (isTop) return this;

+            

+            int v = 0;

+            if (state[0] is Model.BitVector)

+                v = (state[0] as Model.BitVector).AsInt();

+            else if (state[0] is Model.Integer)

+                v = (state[0] as Model.Integer).AsInt();

+            else Debug.Assert(false);

+

+            var nupper = upper;

+            while ((1 << nupper) < v) nupper++;

+            var ntlevel = Val.NEITHER;

+            if (nupper > Max) ntlevel = Val.TRUE;

+            return new PowDomain(ntlevel, nupper);

+        }

+

+        Expr IAbstractDomain.Gamma(List<Expr> vars)

+        {

+            if (isBottom) return Expr.False;

+            if (isTop) return Expr.True;

+            var v = vars[0];

+            if (v.Type.IsBv)

+            {

+                var bits = v.Type.BvBits;

+                if (!AbstractDomainFactory.bvslt.ContainsKey(bits))

+                    throw new AbsHoudiniInternalError("No builtin function found for bv" + bits.ToString());

+                var bvslt = AbstractDomainFactory.bvslt[bits];

+                return new NAryExpr(Token.NoToken, new FunctionCall(bvslt), new ExprSeq(v,

+                    new LiteralExpr(Token.NoToken, Basetypes.BigNum.FromInt(1 << (upper+1)), 32)));

+            }

+            else

+            {

+                return Expr.Lt(v, Expr.Literal(1 << (upper+1)));

+            }

+        }

+

+        bool IAbstractDomain.TypeCheck(List<Type> argTypes, out string msg)

+        {

+            msg = "";

+            if (argTypes.Count != 1)

+            {

+                msg = "Illegal number of arguments, expecting 1";

+                return false;

+            }

+            if (argTypes.Any(tt => !tt.IsInt && !tt.IsBv))

+            {

+                msg = "Illegal type, expecting int or bv";

+                return false;

+            }

+            return true;

+        }

+    }

+

+    // foo(x_i) = all equalities that hold

+    public class EqualitiesDomain : IAbstractDomain

+    {

+        bool isBottom;

+        List<HashSet<int>> equalities;

+

+        public EqualitiesDomain(bool isBottom, List<HashSet<int>> eq)

+        {

+            this.isBottom = isBottom;

+            this.equalities = eq;

+        }

+

+        public static IAbstractDomain GetBottom()

+        {

+            return new EqualitiesDomain(true, new List<HashSet<int>>());

+        }

+

+        IAbstractDomain IAbstractDomain.Bottom()

+        {

+            return GetBottom();

+        }

+

+        IAbstractDomain IAbstractDomain.Join(List<Model.Element> state)

+        {

+            // find the guys that are equal

+            var eq = new List<HashSet<int>>();

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

+            {

+                var added = false;

+                foreach (var s in eq)

+                {

+                    var sv = s.First();

+                    if (state[i].ToString() == state[sv].ToString())

+                    {

+                        s.Add(i);

+                        added = true;

+                        break;

+                    }

+                }

+                if (!added) eq.Add(new HashSet<int>(new int[] { i }));

+            }

+            

+            if (isBottom)

+            {

+                return new EqualitiesDomain(false, eq);

+            }

+

+            // intersect two partitions equalities and eq

+            var m1 = GetMap(equalities, state.Count);

+            var m2 = GetMap(eq, state.Count);

+

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

+                m2[i] = new HashSet<int>(m2[i].Intersect(m1[i]));

+

+

+            // map from representative to set

+            var repToSet = new Dictionary<int, HashSet<int>>();

+

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

+            {

+                var rep = m2[i].Min();

+                if (!repToSet.ContainsKey(rep))

+                    repToSet[rep] = m2[i];

+            }

+

+            var ret = new List<HashSet<int>>();

+            repToSet.Values.Iter(s => ret.Add(s));

+

+            return new EqualitiesDomain(false, ret);

+        }

+

+        Expr IAbstractDomain.Gamma(List<Expr> vars)

+        {

+            if (isBottom) return Expr.False;

+            Expr ret = Expr.True;

+            foreach (var eq in equalities.Select(hs => hs.ToList()))

+            {

+                if (eq.Count == 1) continue;

+                var prev = eq[0];

+                for (int i = 1; i < eq.Count; i++)

+                {

+                    ret = Expr.And(ret, Expr.Eq(vars[prev], vars[eq[i]]));

+                    prev = eq[i];

+                }

+            }

+            return ret;

+        }

+

+        bool IAbstractDomain.TypeCheck(List<Type> argTypes, out string msg)

+        {

+            msg = "";

+            if (argTypes.Count == 0) return true;

+            var ot = argTypes[0];

+

+            if (argTypes.Any(tt => !tt.Equals(ot)))

+            {

+                msg = string.Format("Illegal type, expecting type {0}, got {1}", ot, argTypes.First(tt => !tt.Equals(ot)));

+                return false;

+            }

+            return true;

+        }

+

+        private HashSet<int>[] GetMap(List<HashSet<int>> eq, int n)

+        {

+            var ret = new HashSet<int>[n];

+            foreach (var s in eq)

+            {

+                foreach (var i in s)

+                    ret[i] = s;

+            }

+            return ret;

+        }

+    }

+

+    // foo(a,b) \in {false, \not a, a ==> b, true}

+    public class ImplicationDomain : IAbstractDomain

+    {

+        enum Val {FALSE, NOT_A, A_IMP_B, TRUE};

+        Val val;

+

+        private ImplicationDomain(Val val)

+        {

+            this.val = val;

+        }

+

+        public static ImplicationDomain GetBottom()

+        {

+            return new ImplicationDomain(Val.FALSE);

+        }

+

+        public IAbstractDomain Bottom()

+        {

+            return GetBottom();

+        }

+

+        public IAbstractDomain Join(List<Model.Element> states)

+        {

+            Debug.Assert(states.Count == 2);

+            var v1 = (states[0] as Model.Boolean).Value;

+            var v2 = (states[1] as Model.Boolean).Value;

+

+            if (val == Val.TRUE) return this;

+

+            var that = Val.TRUE;

+            if (!v1) that = Val.NOT_A;

+            else if (!v1 || v2) that = Val.A_IMP_B;

+

+            if (that == Val.TRUE || val == Val.FALSE)

+                return new ImplicationDomain(that);

+

+            // Now, neither this or that is FALSE or TRUE

+            if (val == that)

+                return this;

+

+            Debug.Assert(val == Val.A_IMP_B || that == Val.A_IMP_B);

+            return new ImplicationDomain(Val.A_IMP_B);

+        }

+

+        public Expr Gamma(List<Expr> vars)

+        {

+            Debug.Assert(vars.Count == 2);

+

+            var v1 = vars[0];

+            var v2 = vars[1];

+

+            if (val == Val.FALSE) return Expr.False;

+            if (val == Val.TRUE) return Expr.True;

+            if (val == Val.NOT_A) return Expr.Not(v1);

+            return Expr.Imp(v1, v2);

+        }

+

+        public bool TypeCheck(List<Type> argTypes, out string msg)

+        {

+            msg = "";

+            if (argTypes.Count != 2)

+            {

+                msg = "Illegal number of arguments, expecting 2";

+                return false;

+            }

+            if (argTypes.Any(tt => !tt.IsBool))

+            {

+                msg = "Illegal type, expecting bool";

+                return false;

+            }

+            return true;

+        }

+    }

 

     public class ConstantProp : IAbstractDomain

     {

@@ -1653,6 +1926,9 @@ namespace Microsoft.Boogie.Houdini {
         // Type name -> Instance

         private static Dictionary<string, IAbstractDomain> abstractDomainInstances = new Dictionary<string, IAbstractDomain>();

         private static Dictionary<string, IAbstractDomain> abstractDomainInstancesFriendly = new Dictionary<string, IAbstractDomain>();

+        

+        // bitvector operations

+        public static Dictionary<int, Function> bvslt = new Dictionary<int, Function>();

 

         public static void Register(string friendlyName, IAbstractDomain instance)

         {

@@ -1681,7 +1957,7 @@ namespace Microsoft.Boogie.Houdini {
             return abstractDomainInstancesFriendly[friendlyName] as IAbstractDomain;

         }

 

-        public static void Initialize()

+        public static void Initialize(Program program)

         {

             // Declare abstract domains

             var domains = new List<System.Tuple<string, IAbstractDomain>>(new System.Tuple<string, IAbstractDomain>[] {

@@ -1689,14 +1965,26 @@ namespace Microsoft.Boogie.Houdini {
                   System.Tuple.Create("Intervals", new Intervals() as IAbstractDomain),

                   System.Tuple.Create("ConstantProp", ConstantProp.GetBottom() as IAbstractDomain),

                   System.Tuple.Create("PredicateAbs", new PredicateAbsElem() as IAbstractDomain),

+                  System.Tuple.Create("ImplicationDomain", ImplicationDomain.GetBottom() as IAbstractDomain),

+                  System.Tuple.Create("PowDomain", PowDomain.GetBottom() as IAbstractDomain),

+                  System.Tuple.Create("EqualitiesDomain", EqualitiesDomain.GetBottom() as IAbstractDomain),

                   System.Tuple.Create("IA[HoudiniConst]", new IndependentAttribute<HoudiniConst>()  as IAbstractDomain),

                   System.Tuple.Create("IA[ConstantProp]", new IndependentAttribute<ConstantProp>()  as IAbstractDomain),

-                  System.Tuple.Create("IA[Intervals]", new IndependentAttribute<Intervals>()  as IAbstractDomain)

+                  System.Tuple.Create("IA[Intervals]", new IndependentAttribute<Intervals>()  as IAbstractDomain),

+                  System.Tuple.Create("IA[PowDomain]", new IndependentAttribute<PowDomain>() as IAbstractDomain),

               });

 

             domains.Iter(tup => AbstractDomainFactory.Register(tup.Item1, tup.Item2));

+            program.TopLevelDeclarations.OfType<Function>()

+                .Iter(RegisterFunction);

         }

 

+        private static void RegisterFunction(Function func)

+        {

+            var attr = QKeyValue.FindStringAttribute(func.Attributes, "builtin");

+            if (attr != null && attr == "bvslt" && func.InParams.Count == 2 && func.InParams[0].TypedIdent.Type.IsBv)

+                bvslt.Add(func.InParams[0].TypedIdent.Type.BvBits, func);

+        }

     }

 

     public interface IAbstractDomain

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index de9be1b9..bc13927f 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -423,6 +423,12 @@ namespace Microsoft.Boogie.SMTLib
             var labs = line[4];

             var refs = line[5];

             var predName = conseq.Name;

+            {

+                string spacer = "@@"; // Hack! UniqueNamer is adding these and I can't stop it!

+                int pos = predName.LastIndexOf(spacer);

+                if (pos >= 0)

+                    predName = predName.Substring(0, pos);

+            }

             RPFP.Node node = null;

             if (!pmap.TryGetValue(predName, out node))

             {

@@ -461,7 +467,7 @@ namespace Microsoft.Boogie.SMTLib
                 return null;

             }

             int ruleNum = Convert.ToInt32(rule.Name.Substring(5)) - 1;

-            if(ruleNum < 0 || ruleNum > rpfp.edges.Count)

+            if (ruleNum < 0 || ruleNum > rpfp.edges.Count)

             {

                 HandleProverError("bad rule name from prover: " + refs.ToString());

                 return null;

@@ -489,7 +495,7 @@ namespace Microsoft.Boogie.SMTLib
             varSubst[e.number] = dict;

             foreach (var s in subst.Arguments)

             {

-                if(s.Name != "=" || s.Arguments.Length != 2)

+                if (s.Name != "=" || s.Arguments.Length != 2)

                 {

                     HandleProverError("bad equation from prover: " + s.ToString());

                     return null;

@@ -573,6 +579,7 @@ namespace Microsoft.Boogie.SMTLib
             currentLogFile.Write(common.ToString());

         }

 

+        Push();

         SendThisVC("(fixedpoint-push)");

         foreach (var node in rpfp.nodes)

         {

@@ -588,7 +595,15 @@ namespace Microsoft.Boogie.SMTLib
             string ruleString = "(rule " + QuantifiedVCExpr2String(rpfp.GetRule(edge)) + "\n)";

             ruleStrings.Add(ruleString);

         }

-        string queryString = "(query " + QuantifiedVCExpr2String(rpfp.GetQuery()) + "\n   :engine duality\n  :print-certificate true\n)";

+        string queryString = "(query " + QuantifiedVCExpr2String(rpfp.GetQuery()) + "\n   :engine duality\n  :print-certificate true\n";

+       

+#if true

+        if (CommandLineOptions.Clo.StratifiedInlining != 0)

+            queryString += "    :stratified-inlining true\n";

+        if (CommandLineOptions.Clo.RecursionBound > 0)

+            queryString += "    :recursion-bound " + Convert.ToString(CommandLineOptions.Clo.RecursionBound) + "\n";

+#endif

+        queryString += ")";

         LineariserOptions.Default.LabelsBelowQuantifiers = false;

         FlushAxioms();

 

@@ -672,6 +687,8 @@ namespace Microsoft.Boogie.SMTLib
 #endif

         }

         SendThisVC("(fixedpoint-pop)");

+        Pop();

+        AxiomsAreSetup = false;

         return result;

     }

 

@@ -780,7 +797,14 @@ namespace Microsoft.Boogie.SMTLib
             IList<string> xlabels;

             if (CommandLineOptions.Clo.UseLabels) {

               labels = GetLabelsInfo();

-              xlabels = labels.Select(a => a.Replace("@", "").Replace("+", "")).ToList();

+              if (labels == null)

+              {

+                xlabels = new string[] { };

+              }

+              else

+              {

+                xlabels = labels.Select(a => a.Replace("@", "").Replace("+", "")).ToList();

+              }

             }

             else {

               labels = CalculatePath(handler.StartingProcId());

@@ -799,7 +823,7 @@ namespace Microsoft.Boogie.SMTLib
             if (!options.MultiTraces)

               posLabels = Enumerable.Empty<string>();

             var conjuncts = posLabels.Select(s => "(not " + lbl(s) + ")").Concat(negLabels.Select(lbl)).ToArray();

-            var expr = conjuncts.Length == 1 ? conjuncts[0] : ("(or " + conjuncts.Concat(" ") + ")");

+            string expr = conjuncts.Length == 1 ? conjuncts[0] : ("(or " + conjuncts.Concat(" ") + ")"); ;

             if (!conjuncts.Any())

             {

               expr = "false";

@@ -960,7 +984,7 @@ namespace Microsoft.Boogie.SMTLib
                 result = Outcome.OutOfMemory;

                 Process.NeedsRestart = true;

                 break;

-              case "timeout":

+                case "timeout": case "canceled":

                 currentErrorHandler.OnResourceExceeded("timeout");

                 result = Outcome.TimeOut;

                 break;

@@ -1155,7 +1179,7 @@ namespace Microsoft.Boogie.SMTLib
 

     public override void SetTimeOut(int ms)

     {

-        SendThisVC("(set-option :SOFT_TIMEOUT " + ms.ToString() + ")\n");

+        SendThisVC("(set-option " + Z3.SetTimeoutOption() + "  " + ms.ToString() + ")\n");

     }

 

     public override object Evaluate(VCExpr expr)

diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs
index 81d5d5d1..bc9e6992 100644
--- a/Source/Provers/SMTLib/Z3.cs
+++ b/Source/Provers/SMTLib/Z3.cs
@@ -187,6 +187,16 @@ namespace Microsoft.Boogie.SMTLib
             minor = Z3MinorVersion;

         }

 

+        public static string SetTimeoutOption()

+        {

+            int major, minor;

+            GetVersion(out major, out minor);

+            if (major > 4 || major == 4 && minor >= 3)

+                return "TIMEOUT";

+            else

+                return "SOFT_TIMEOUT";

+        }

+

         // options that work only on the command line

         static string[] commandLineOnly = { "TRACE", "PROOF_MODE" };

 

@@ -251,7 +261,7 @@ namespace Microsoft.Boogie.SMTLib
 

                 if (options.TimeLimit > 0)

                 {

-                    options.AddWeakSmtOption("SOFT_TIMEOUT", options.TimeLimit.ToString());

+                    options.AddWeakSmtOption("TIMEOUT", options.TimeLimit.ToString());

                     // This kills the Z3 *instance* after the specified time, not a particular query, so we cannot use it.

                     // options.AddSolverArgument("/T:" + (options.TimeLimit + 1000) / 1000);

                 }

@@ -261,9 +271,8 @@ namespace Microsoft.Boogie.SMTLib
 

                 if (CommandLineOptions.Clo.WeakArrayTheory)

                 {

-                    // TODO: these options don't seem to exist in recent Z3

-                    // options.AddWeakSmtOption("ARRAY_WEAK", "true");

-                    // options.AddWeakSmtOption("ARRAY_EXTENSIONAL", "false");

+                    options.AddWeakSmtOption("smt.array.weak", "true");

+                    options.AddWeakSmtOption("smt.array.extensional", "false");

                 } 

             }

             else

diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index d08a4d4b..2ff93c54 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -272,7 +272,10 @@ namespace Microsoft.Boogie.VCExprAST {
       // global variables, local variables, incarnations, etc. are

       // bound the first time they occur

       if (!UnboundVariables.TryGetValue(boogieVar, out res)) {

-        res = new VCExprVar(boogieVar.Name, boogieVar.TypedIdent.Type);

+        if (boogieVar is Constant)

+          res = new VCExprConstant(boogieVar.Name, boogieVar.TypedIdent.Type);

+        else 

+          res = new VCExprVar(boogieVar.Name, boogieVar.TypedIdent.Type);

         UnboundVariables.Bind(boogieVar, res);

       }

       return cce.NonNull(res);

diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs
index 82bdebbe..f56b6978 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -1868,6 +1868,14 @@ namespace Microsoft.Boogie.VCExprAST {
     }

   }

 

+  public class VCExprConstant : VCExprVar

+  {

+      internal VCExprConstant(string name, Type type) : base(name,type) {

+      Contract.Requires(type != null);

+      Contract.Requires(name != null);

+    }

+  }

+

   public abstract class VCExprBinder : VCExpr {

     public readonly VCExpr/*!*/ Body;

     public readonly List<TypeVariable/*!*/>/*!*/ TypeParameters;

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index e88c000e..6897a982 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -137,40 +137,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,6 +151,61 @@ namespace Microsoft.Boogie {
       this.gen = prover.VCExprGen;

     }

 

+    public void Retarget(Program prog, ProverContext ctx)

+    {

+        ctx.Clear();

+        Setup(prog, ctx);

+    }

+

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

+    {

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

+            }

+        }

+    }

+

 

     /// <summary>

     /// Clean-up.

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index dc9f496b..3ae97bdd 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -80,6 +80,7 @@ namespace Microsoft.Boogie {
     public ProverContext Context;

     [Peer]

     public List<string>/*!>!*/ relatedInformation;

+    public string RequestId;

 

     public Dictionary<TraceLocation, CalleeCounterexampleInfo> calleeCounterexamples;

 

@@ -146,7 +147,7 @@ namespace Microsoft.Boogie {
         return naryExpr.Fun.FunctionName;

     }

 

-    public void Print(int indent) {

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

       int numBlock = -1;

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

       foreach (Block b in Trace) {

@@ -159,7 +160,13 @@ namespace Microsoft.Boogie {
           // 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)) {

+            if (blockAction != null)

+            {

+                blockAction(b);

+            }

+

             Console.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);

@@ -587,7 +594,7 @@ namespace VC {
     /// each counterexample consisting of an array of labels.

     /// </summary>

     /// <param name="impl"></param>

-    public Outcome VerifyImplementation(Implementation impl, out List<Counterexample>/*?*/ errors) {

+    public Outcome VerifyImplementation(Implementation impl, out List<Counterexample>/*?*/ errors, string requestId = null) {

       Contract.Requires(impl != null);

 

       Contract.Ensures(Contract.ValueAtReturn(out errors) == null || Contract.ForAll(Contract.ValueAtReturn(out errors), i => i != null));

@@ -596,6 +603,7 @@ namespace VC {
       Helpers.ExtraTraceInformation("Starting implementation verification");

 

       CounterexampleCollector collector = new CounterexampleCollector();

+      collector.RequestId = requestId;

       Outcome outcome = VerifyImplementation(impl, collector);

       if (outcome == Outcome.Errors || outcome == Outcome.TimedOut || outcome == Outcome.OutOfMemory) {

         errors = collector.examples;

@@ -996,9 +1004,15 @@ namespace VC {
         Contract.Invariant(cce.NonNullElements(examples));

       }

 

+      public string RequestId;

+

       public readonly List<Counterexample>/*!>!*/ examples = new List<Counterexample>();

       public override void OnCounterexample(Counterexample ce, string/*?*/ reason) {

         //Contract.Requires(ce != null);

+        if (RequestId != null)

+        {

+          ce.RequestId = RequestId;

+        }

         examples.Add(ce);

       }

 

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..19feabe9 100644
--- a/Source/VCGeneration/FixedpointVC.cs
+++ b/Source/VCGeneration/FixedpointVC.cs
@@ -76,6 +76,8 @@ namespace Microsoft.Boogie
         Mode mode;

         AnnotationStyle style;

 

+        private static Checker old_checker = null;

+

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

             : base(_program, logFilePath, appendLogFile) 

         {

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

         }