merge

2 files changed, 750 insertions, 426 deletions

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 110480b9..21d0c014 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -5,6 +5,8 @@ using System.Diagnostics.Contracts;
 using System.IO;

 using System.Linq;

 using System.Text.RegularExpressions;

+using System.Threading;

+using System.Threading.Tasks;

 using VC;

 using BoogiePL = Microsoft.Boogie;

 

@@ -16,23 +18,24 @@ namespace Microsoft.Boogie
 

   public interface OutputPrinter

   {

-    void ErrorWriteLine(string s);

-    void ErrorWriteLine(string format, params object[] args);

+    void ErrorWriteLine(TextWriter tw, string s);

+    void ErrorWriteLine(TextWriter tw, string format, params object[] args);

     void AdvisoryWriteLine(string format, params object[] args);

-    void Inform(string s);

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

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

+    void Inform(string s, TextWriter tw);

+    void WriteTrailer(PipelineStatistics stats);

+    void WriteErrorInformation(ErrorInformation errorInfo, TextWriter tw, bool skipExecutionTrace = true);

+    void ReportBplError(IToken tok, string message, bool error, TextWriter tw, string category = null);

   }

 

 

   public class ConsolePrinter : OutputPrinter

   {

-    public void ErrorWriteLine(string s)

+    public void ErrorWriteLine(TextWriter tw, string s)

     {

       Contract.Requires(s != null);

       if (!s.Contains("Error: ") && !s.Contains("Error BP"))

       {

-        Console.WriteLine(s);

+        tw.WriteLine(s);

         return;

       }

 

@@ -51,21 +54,21 @@ namespace Microsoft.Boogie
 

       ConsoleColor col = Console.ForegroundColor;

       Console.ForegroundColor = ConsoleColor.Red;

-      Console.WriteLine(s);

+      tw.WriteLine(s);

       Console.ForegroundColor = col;

 

       if (remaining != null)

       {

-        Console.WriteLine(remaining);

+        tw.WriteLine(remaining);

       }

     }

 

 

-    public void ErrorWriteLine(string format, params object[] args)

+    public void ErrorWriteLine(TextWriter tw, string format, params object[] args)

     {

       Contract.Requires(format != null);

       string s = string.Format(format, args);

-      ErrorWriteLine(s);

+      ErrorWriteLine(tw, s);

     }

 

 

@@ -83,49 +86,75 @@ namespace Microsoft.Boogie
     /// Inform the user about something and proceed with translation normally.

     /// Print newline after the message.

     /// </summary>

-    public void Inform(string s)

+    public void Inform(string s, TextWriter tw)

     {

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

       {

-        Console.WriteLine(s);

+        tw.WriteLine(s);

       }

     }

 

 

-    public void WriteTrailer(int verified, int errors, int inconclusives, int timeOuts, int outOfMemories)

+    public void WriteTrailer(PipelineStatistics stats)

     {

-      Contract.Requires(0 <= errors && 0 <= inconclusives && 0 <= timeOuts && 0 <= outOfMemories);

+      Contract.Requires(stats != null);

+      Contract.Requires(0 <= stats.VerifiedCount && 0 <= stats.ErrorCount && 0 <= stats.InconclusiveCount && 0 <= stats.TimeoutCount && 0 <= stats.OutOfMemoryCount);

+

       Console.WriteLine();

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

       {

-        Console.Write("{0} finished with {1} credible, {2} doomed{3}", CommandLineOptions.Clo.DescriptiveToolName, verified, errors, errors == 1 ? "" : "s");

+        Console.Write("{0} finished with {1} credible, {2} doomed{3}", CommandLineOptions.Clo.DescriptiveToolName, stats.VerifiedCount, stats.ErrorCount, stats.ErrorCount == 1 ? "" : "s");

       }

       else

       {

-        Console.Write("{0} finished with {1} verified, {2} error{3}", CommandLineOptions.Clo.DescriptiveToolName, verified, errors, errors == 1 ? "" : "s");

+        Console.Write("{0} finished with {1} verified, {2} error{3}", CommandLineOptions.Clo.DescriptiveToolName, stats.VerifiedCount, stats.ErrorCount, stats.ErrorCount == 1 ? "" : "s");

       }

-      if (inconclusives != 0)

+      if (stats.InconclusiveCount != 0)

       {

-        Console.Write(", {0} inconclusive{1}", inconclusives, inconclusives == 1 ? "" : "s");

+        Console.Write(", {0} inconclusive{1}", stats.InconclusiveCount, stats.InconclusiveCount == 1 ? "" : "s");

       }

-      if (timeOuts != 0)

+      if (stats.TimeoutCount != 0)

       {

-        Console.Write(", {0} time out{1}", timeOuts, timeOuts == 1 ? "" : "s");

+        Console.Write(", {0} time out{1}", stats.TimeoutCount, stats.TimeoutCount == 1 ? "" : "s");

       }

-      if (outOfMemories != 0)

+      if (stats.OutOfMemoryCount != 0)

       {

-        Console.Write(", {0} out of memory", outOfMemories);

+        Console.Write(", {0} out of memory", stats.OutOfMemoryCount);

       }

       Console.WriteLine();

       Console.Out.Flush();

     }

 

 

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

+    public void WriteErrorInformation(ErrorInformation errorInfo, TextWriter tw, bool skipExecutionTrace = true)

+    {

+      Contract.Requires(errorInfo != null);

+

+      ReportBplError(errorInfo.Tok, errorInfo.FullMsg, true, tw);

+

+      foreach (var e in errorInfo.Aux)

+      {

+        if (!(skipExecutionTrace && e.Category.Contains("Execution trace")))

+        {

+          ReportBplError(e.Tok, e.FullMsg, false, tw);

+        }

+      }

+

+      tw.Write(errorInfo.Out.ToString());

+      tw.Flush();

+    }

+

+

+    public virtual void ReportBplError(IToken tok, string message, bool error, TextWriter tw, string category = null)

     {

       Contract.Requires(message != null);

+

+      if (category != null)

+      {

+        message = string.Format("{0}: {1}", category, message);

+      }

       string s;

-      if (tok != null && showBplLocation)

+      if (tok != null)

       {

         s = string.Format("{0}({1},{2}): {3}", tok.filename, tok.line, tok.col, message);

       }

@@ -135,11 +164,11 @@ namespace Microsoft.Boogie
       }

       if (error)

       {

-        ErrorWriteLine(s);

+        ErrorWriteLine(tw, s);

       }

       else

       {

-        Console.WriteLine(s);

+        tw.WriteLine(s);

       }

     }

   }

@@ -158,40 +187,87 @@ namespace Microsoft.Boogie
   }

 

 

+  public class PipelineStatistics

+  {

+    public int ErrorCount;

+    public int VerifiedCount;

+    public int InconclusiveCount;

+    public int TimeoutCount;

+    public int OutOfMemoryCount;

+  }

+

+

   #region Error reporting

 

   public delegate void ErrorReporterDelegate(ErrorInformation errInfo);

 

 

+  public enum ErrorKind

+  {

+    Assertion,

+    Precondition,

+    Postcondition,

+    InvariantEntry,

+    InvariantMaintainance

+  }

+

+

   public class ErrorInformationFactory

   {

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

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

     {

-      Contract.Requires(tok != null);

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

       Contract.Requires(msg != null);

 

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

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

     }

   }

 

 

   public class ErrorInformation

   {

-    public IToken Tok;

+    public readonly IToken Tok;

     public string Msg;

+    public string Category { get; set; }

+    public string BoogieErrorCode { get; set; }

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

     public string RequestId { get; set; }

+    public ErrorKind Kind { get; set; }

+    public string ImplementationName { get; set; }

+    public TextWriter Out = new StringWriter();

+

+    public string FullMsg

+    {

+      get

+      {

+        var prefix = Category;

+        if (BoogieErrorCode != null)

+        {

+          prefix = prefix == null ? BoogieErrorCode : prefix + " " + BoogieErrorCode;

+        }

+        return prefix != null ? string.Format("{0}: {1}", prefix, Msg) : Msg;

+      }

+    }

 

     public struct AuxErrorInfo

     {

       public readonly IToken Tok;

       public readonly string Msg;

+      public readonly string Category;

 

-      public AuxErrorInfo(IToken tok, string msg)

+      public string FullMsg

+      {

+        get

+        {

+          return Category != null ? string.Format("{0}: {1}", Category, Msg) : Msg;

+        }

+      }

+

+      public AuxErrorInfo(IToken tok, string msg, string category = null)

       {

         Tok = tok;

         Msg = CleanUp(msg);

+        Category = category;

       }

     }

 

@@ -205,19 +281,20 @@ namespace Microsoft.Boogie
       Msg = CleanUp(msg);

     }

 

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

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

     {

       var result = new ErrorInformation(tok, msg);

       result.RequestId = requestId;

+      result.Category = category;

       return result;

     }

 

-    public virtual void AddAuxInfo(IToken tok, string msg)

+    public virtual void AddAuxInfo(IToken tok, string msg, string category = null)

     {

       Contract.Requires(tok != null);

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

       Contract.Requires(msg != null);

-      Aux.Add(new AuxErrorInfo(tok, msg));

+      Aux.Add(new AuxErrorInfo(tok, msg, category));

     }

 

     protected static string CleanUp(string msg)

@@ -236,6 +313,41 @@ 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 ConditionGeneration.Outcome Outcome;

+    public List<Counterexample> Errors;

+

+    public string ImplementationName { get; set; }

+    public IToken ImplementationToken { get; set; }

+

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

@@ -284,7 +396,6 @@ namespace Microsoft.Boogie
 

       using (XmlFileScope xf = new XmlFileScope(CommandLineOptions.Clo.XmlSink, fileNames[fileNames.Count - 1]))

       {

-        //BoogiePL.Errors.count = 0;

         Program program = ParseBoogieProgram(fileNames, false);

         if (program == null)

           return;

@@ -296,7 +407,6 @@ namespace Microsoft.Boogie
         PipelineOutcome oc = ResolveAndTypecheck(program, fileNames[fileNames.Count - 1]);

         if (oc != PipelineOutcome.ResolvedAndTypeChecked)

           return;

-        //BoogiePL.Errors.count = 0;

 

         // Do bitvector analysis

         if (CommandLineOptions.Clo.DoBitVectorAnalysis)

@@ -346,13 +456,13 @@ namespace Microsoft.Boogie
           }

         }

 

-        int errorCount, verified, inconclusives, timeOuts, outOfMemories;

-        oc = InferAndVerify(program, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories);

+        var stats = new PipelineStatistics();

+        oc = InferAndVerify(program, stats);

         switch (oc)

         {

           case PipelineOutcome.Done:

           case PipelineOutcome.VerificationCompleted:

-            printer.WriteTrailer(verified, errorCount, inconclusives, timeOuts, outOfMemories);

+            printer.WriteTrailer(stats);

             break;

           default:

             break;

@@ -393,7 +503,7 @@ namespace Microsoft.Boogie
     public static Program ParseBoogieProgram(List<string> fileNames, bool suppressTraceOutput)

     {

       Contract.Requires(cce.NonNullElements(fileNames));

-      //BoogiePL.Errors.count = 0;

+

       Program program = null;

       bool okay = true;

       for (int fileId = 0; fileId < fileNames.Count; fileId++)

@@ -426,7 +536,7 @@ namespace Microsoft.Boogie
         }

         catch (IOException e)

         {

-          printer.ErrorWriteLine("Error opening file \"{0}\": {1}", bplFileName, e.Message);

+          printer.ErrorWriteLine(Console.Out, "Error opening file \"{0}\": {1}", bplFileName, e.Message);

           okay = false;

           continue;

         }

@@ -551,31 +661,22 @@ namespace Microsoft.Boogie
         }

         if (inline)

         {

-          foreach (var d in TopLevelDeclarations)

+          foreach (var impl in TopLevelDeclarations.OfType<Implementation>())

           {

-            var impl = d as Implementation;

-            if (impl != null)

-            {

-              impl.OriginalBlocks = impl.Blocks;

-              impl.OriginalLocVars = impl.LocVars;

-            }

+            impl.OriginalBlocks = impl.Blocks;

+            impl.OriginalLocVars = impl.LocVars;

           }

-          foreach (var d in TopLevelDeclarations)

+          foreach (var impl in TopLevelDeclarations.OfType<Implementation>())

           {

-            var impl = d as Implementation;

-            if (impl != null && !impl.SkipVerification)

+            if (!impl.SkipVerification)

             {

               Inliner.ProcessImplementation(program, impl);

             }

           }

-          foreach (var d in TopLevelDeclarations)

+          foreach (var impl in TopLevelDeclarations.OfType<Implementation>())

           {

-            var impl = d as Implementation;

-            if (impl != null)

-            {

-              impl.OriginalBlocks = null;

-              impl.OriginalLocVars = null;

-            }

+            impl.OriginalBlocks = null;

+            impl.OriginalLocVars = null;

           }

         }

       }

@@ -591,17 +692,16 @@ namespace Microsoft.Boogie
     ///    parameters contain meaningful values

     /// </summary>

     public static PipelineOutcome InferAndVerify(Program program,

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

+                                                 PipelineStatistics stats,

                                                  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;

+      Contract.Requires(stats != null);

+      Contract.Ensures(0 <= Contract.ValueAtReturn(out stats.InconclusiveCount) && 0 <= Contract.ValueAtReturn(out stats.TimeoutCount));

 

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

@@ -612,6 +712,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);

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

       }

 

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

+      #endregion

 

       if (!CommandLineOptions.Clo.Verify)

       {

@@ -644,453 +748,666 @@ 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, stats, er);

       }

       #endregion

 

-      #region Verify each implementation

+      #region Select and prioritize implementations that should be verified

 

-      ConditionGeneration vcgen = null;

-      try

+      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

+      Implementation[] stablePrioritizedImpls = null;

+      if (CommandLineOptions.Clo.VerifySnapshots)

       {

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

-        {

-          vcgen = new DCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

-        }

-        else if (CommandLineOptions.Clo.FixedPointEngine != null)

-        {

-          vcgen = new FixedpointVC(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

-        }

-        else if (CommandLineOptions.Clo.StratifiedInlining > 0)

-        {

-          vcgen = new StratifiedVCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

-        }

-        else

-        {

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

-        }

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

+        stablePrioritizedImpls = impls.OrderByDescending(

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

       }

-      catch (ProverException e)

+      else

       {

-        printer.ErrorWriteLine("Fatal Error: ProverException: {0}", e);

-        return PipelineOutcome.FatalError;

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

       }

 

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

-      var decls = program.TopLevelDeclarations.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)

+      var outputCollector = new OutputCollector(stablePrioritizedImpls);

+      var outcome = PipelineOutcome.VerificationCompleted;

+      var checkers = new List<Checker>();

+      var tasks = new Task[stablePrioritizedImpls.Length];

+      for (int i = 0; i < stablePrioritizedImpls.Length && outcome != PipelineOutcome.FatalError; i++)

       {

-        int prevAssertionCount = vcgen.CumulativeAssertionCount;

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

-

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

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

+        var taskIndex = i;

+        var t = Task.Factory.StartNew(() =>

         {

-          start = DateTime.UtcNow;

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

+          VerifyImplementation(program, stats, er, requestId, extractLoopMappingInfo, stablePrioritizedImpls, taskIndex, outputCollector, checkers);

+        }, TaskCreationOptions.LongRunning);

+        tasks[taskIndex] = t;

+      }

+      try

+      {

+        Task.WaitAll(tasks);

+      }

+      catch (AggregateException ae)

+      {

+        ae.Handle(e =>

+        {

+          var pe = e as ProverException;

+          if (pe != null)

           {

-            Console.WriteLine();

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

+            printer.ErrorWriteLine(Console.Out, "Fatal Error: ProverException: {0}", e);

+            outcome = PipelineOutcome.FatalError;

+            return true;

           }

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

+          return false;

+        });

+      }

+      finally

+      {

+        lock (checkers)

+        {

+          foreach (Checker checker in checkers)

           {

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

+            Contract.Assert(checker != null);

+            checker.Close();

           }

         }

+      }

+

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

+

+      outputCollector.WriteMoreOutput();

+

+      #endregion

+

+      return outcome;

+    }

+

+

+    private static void VerifyImplementation(Program program, PipelineStatistics stats, ErrorReporterDelegate er, string requestId, Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo, Implementation[] stablePrioritizedImpls, int index, OutputCollector outputCollector, List<Checker> checkers)

+    {

+      Implementation impl = stablePrioritizedImpls[index];

+      VerificationResult verificationResult = null;

+      var output = new StringWriter();

+

+      printer.Inform("", output);  // newline

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

 

-        VCGen.Outcome outcome;

-        string depsChecksum = null;

-        if (CommandLineOptions.Clo.VerifySnapshots)

+      if (CommandLineOptions.Clo.VerifySnapshots)

+      {

+        verificationResult = Cache.Lookup(impl);

+      }

+

+      if (verificationResult != null)

+      {

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

         {

-          depsChecksum = DependencyCollector.DependenciesChecksum(impl);

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

         }

-        try

+

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

+      }

+      else

+      {

+        #region Verify the implementation

+

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

+        verificationResult.ImplementationName = impl.Name;

+        verificationResult.ImplementationToken = impl.tok;

+

+        using (var vcgen = CreateVCGen(program, checkers))

         {

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

+          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 (!CommandLineOptions.Clo.VerifySnapshots || Cache.NeedsToBeVerified(impl))

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

             {

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

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

+              }

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

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

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

             }

             else

             {

-              if (CommandLineOptions.Clo.Trace)

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

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

               {

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

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

+                  }

+                }

               }

-              var result = Cache.Lookup(impl.Id);

-              Contract.Assert(result != null);

-              outcome = result.Outcome;

-              errors = result.Errors;

             }

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

+          }

+          catch (VCGenException e)

+          {

+            var errorInfo = errorInformationFactory.CreateErrorInformation(impl.tok, String.Format("{0} (encountered in implementation {1}).", e.Message, impl.Name), requestId, "Error");

+            errorInfo.BoogieErrorCode = "BP5010";

+            errorInfo.ImplementationName = impl.Name;

+            printer.WriteErrorInformation(errorInfo, output);

+            if (er != null)

             {

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

+              lock (er)

               {

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

+                er(errorInfo);

               }

             }

+            verificationResult.Errors = null;

+            verificationResult.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);

-          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 (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;

+          }

+

+          verificationResult.ProofObligationCountAfter = vcgen.CumulativeAssertionCount;

+          verificationResult.End = DateTime.UtcNow;

         }

 

-        string timeIndication = "";

-        DateTime end = DateTime.UtcNow;

-        TimeSpan elapsed = end - start;

-        if (CommandLineOptions.Clo.Trace)

+        #endregion

+

+        #region Cache the verification result

+

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

         {

-          int poCount = vcgen.CumulativeAssertionCount - prevAssertionCount;

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

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

         }

-        else if (CommandLineOptions.Clo.TraceProofObligations)

+

+        #endregion

+      }

+

+      #region Process the verification results and statistics

+

+      ProcessOutcome(verificationResult.Outcome, verificationResult.Errors, TimeIndication(verificationResult), stats, output, er, verificationResult.ImplementationName, verificationResult.ImplementationToken, verificationResult.RequestId);

+

+      ProcessErrors(verificationResult.Errors, verificationResult.Outcome, output, er, impl);

+

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

+      {

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

+      }

+

+      outputCollector.Add(index, output);

+

+      outputCollector.WriteMoreOutput();

+

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

+      {

+        Console.Out.Flush();

+      }

+

+      #endregion

+    }

+

+

+    class OutputCollector

+    {

+      StringWriter[] outputs;

+

+      int nextPrintableIndex = 0;

+

+      public OutputCollector(Implementation[] implementations)

+      {

+        outputs = new StringWriter[implementations.Length];

+      }

+

+      public void WriteMoreOutput()

+      {

+        lock (outputs)

         {

-          int poCount = vcgen.CumulativeAssertionCount - prevAssertionCount;

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

+          for (; nextPrintableIndex < outputs.Count() && outputs[nextPrintableIndex] != null; nextPrintableIndex++)

+          {

+            Console.Write(outputs[nextPrintableIndex].ToString());

+            Console.Out.Flush();

+          }

         }

+      }

 

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

+      public void Add(int index, StringWriter output)

+      {

+        Contract.Requires(0 <= index && index < outputs.Length);

+        Contract.Requires(output != null);

+

+        lock (this)

         {

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

-          Cache.Insert(impl.Id, result);

+          outputs[index] = output;

         }

+      }

+    }

 

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

 

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

+    private static ConditionGeneration CreateVCGen(Program program, List<Checker> checkers)

+    {

+      ConditionGeneration vcgen = null;

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

+      {

+        vcgen = new DCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, checkers);

+      }

+      else if (CommandLineOptions.Clo.FixedPointEngine != null)

+      {

+        vcgen = new FixedpointVC(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, checkers);

+      }

+      else if (CommandLineOptions.Clo.StratifiedInlining > 0)

+      {

+        vcgen = new StratifiedVCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, checkers);

+      }

+      else

+      {

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

+      }

+      return vcgen;

+    }

+

+

+    #region Houdini

+

+    private static PipelineOutcome RunHoudini(Program program, PipelineStatistics stats, ErrorReporterDelegate er)

+    {

+      Contract.Requires(stats != null);

+

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

+      {

+        return RunAbstractHoudini(program, stats, 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)

         {

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

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

         }

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

+      }

+

+      if (CommandLineOptions.Clo.Trace)

+      {

+        int numTrueAssigns = 0;

+        foreach (var x in outcome.assignment)

         {

-          Console.Out.Flush();

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

       }

 

-      vcgen.Close();

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

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

+      {

+        ProcessOutcome(x.outcome, x.errors, "", stats, Console.Out, er);

+        ProcessErrors(x.errors, x.outcome, Console.Out, er);

+      }

+      //errorCount = outcome.ErrorCount;

+      //verified = outcome.Verified;

+      //inconclusives = outcome.Inconclusives;

+      //timeOuts = outcome.TimeOuts;

+      //outOfMemories = 0;

+      return PipelineOutcome.Done;

+    }

 

-      #endregion

 

-      return PipelineOutcome.VerificationCompleted;

+    private static PipelineOutcome RunAbstractHoudini(Program program, PipelineStatistics stats, ErrorReporterDelegate er)

+    {

+      Contract.Requires(stats != 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(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, "", stats, Console.Out, er);

+      ProcessErrors(absout.errors, absout.outcome, Console.Out, 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;

+    }

+

+    #endregion

+

+

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

+                                       PipelineStatistics stats, TextWriter tw, ErrorReporterDelegate er = null, string implName = null, IToken implTok = null, string requestId = null)

+    {

+      Contract.Requires(stats != null);

+

+      UpdateStatistics(stats, outcome, errors);

+

+      printer.Inform(timeIndication + OutcomeIndication(outcome, errors), tw);

+

+      ReportOutcome(outcome, er, implName, implTok, requestId, tw);

     }

 

 

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

+    private static void ReportOutcome(VC.VCGen.Outcome outcome, ErrorReporterDelegate er, string implName, IToken implTok, string requestId, TextWriter tw)

     {

+      ErrorInformation errorInfo = null;

+

       switch (outcome)

       {

-        default:

-          Contract.Assert(false);  // unexpected outcome

-          throw new cce.UnreachableException();

         case VCGen.Outcome.ReachedBound:

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

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

-          verified++;

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

           break;

-        case VCGen.Outcome.Correct:

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

+        case VCGen.Outcome.TimedOut:

+          if (implName != null && implTok != null)

           {

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

-            verified++;

+            errorInfo = errorInformationFactory.CreateErrorInformation(implTok, string.Format("Verification timed out after {0} seconds ({1})", CommandLineOptions.Clo.ProverKillTime, implName), requestId);

           }

-          else

+          break;

+        case VCGen.Outcome.OutOfMemory:

+          if (implName != null && implTok != null)

           {

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

-            verified++;

+            errorInfo = errorInformationFactory.CreateErrorInformation(implTok, "Verification out of memory (" + implName + ")", requestId);

           }

           break;

-        case VCGen.Outcome.TimedOut:

-          timeOuts++;

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

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

+        case VCGen.Outcome.Inconclusive:

+          if (implName != null && implTok != null)

           {

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

+            errorInfo = errorInformationFactory.CreateErrorInformation(implTok, "Verification inconclusive (" + implName + ")", requestId);

           }

           break;

-        case VCGen.Outcome.OutOfMemory:

-          outOfMemories++;

-          printer.Inform(String.Format("{0}out of memory", timeIndication));

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

+      }

+

+      if (errorInfo != null)

+      {

+        errorInfo.ImplementationName = implName;

+        if (er != null)

+        {

+          lock (er)

           {

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

+            er(errorInfo);

           }

+        }

+      }

+    }

+

+

+    private static string OutcomeIndication(VC.VCGen.Outcome outcome, List<Counterexample> errors)

+    {

+      string traceOutput = "";

+      switch (outcome)

+      {

+        default:

+          Contract.Assert(false);  // unexpected outcome

+          throw new cce.UnreachableException();

+        case VCGen.Outcome.ReachedBound:

+          traceOutput = "verified";

+          break;

+        case VCGen.Outcome.Correct:

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

+          break;

+        case VCGen.Outcome.TimedOut:

+          traceOutput = "timed out";

+          break;

+        case VCGen.Outcome.OutOfMemory:

+          traceOutput = "out of memory";

           break;

         case VCGen.Outcome.Inconclusive:

-          inconclusives++;

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

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

-          {

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

-          }

+          traceOutput = "inconclusive";

+          break;

+        case VCGen.Outcome.Errors:

+          Contract.Assert(errors != null);

+          traceOutput = (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed ? "doomed" : string.Format("error{0}", errors.Count == 1 ? "" : "s"));

+          break;

+      }

+      return traceOutput;

+    }

+

+

+    private static void UpdateStatistics(PipelineStatistics stats, VC.VCGen.Outcome outcome, List<Counterexample> errors)

+    {

+      Contract.Requires(stats != null);

+

+      switch (outcome)

+      {

+        default:

+          Contract.Assert(false);  // unexpected outcome

+          throw new cce.UnreachableException();

+        case VCGen.Outcome.ReachedBound:

+          Interlocked.Increment(ref stats.VerifiedCount);

+          break;

+        case VCGen.Outcome.Correct:

+          Interlocked.Increment(ref stats.VerifiedCount);

+          break;

+        case VCGen.Outcome.TimedOut:

+          Interlocked.Increment(ref stats.TimeoutCount);

+          break;

+        case VCGen.Outcome.OutOfMemory:

+          Interlocked.Increment(ref stats.OutOfMemoryCount);

+          break;

+        case VCGen.Outcome.Inconclusive:

+          Interlocked.Increment(ref stats.InconclusiveCount);

           break;

         case VCGen.Outcome.Errors:

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

           {

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

-            errorCount++;

+            Interlocked.Increment(ref stats.ErrorCount);

+          }

+          else

+          {

+            Interlocked.Add(ref stats.ErrorCount, errors.Count);

           }

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

           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)

-        {

-          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.

 

+    private static void ProcessErrors(List<Counterexample> errors, VC.VCGen.Outcome outcome, TextWriter tw, ErrorReporterDelegate er, Implementation impl = null)

+    {

+      var implName = impl != null ? impl.Name : null;

+

+      if (errors != null)

+      {

         errors.Sort(new CounterexampleComparer());

         foreach (Counterexample error in errors)

         {

-          ErrorInformation errorInfo;

+          var errorInfo = CreateErrorInformation(error, outcome);

+          errorInfo.ImplementationName = implName;

 

-          if (error is CallCounterexample)

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

           {

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

-            }

-

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

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

+            WriteErrorInformationToXmlSink(errorInfo, error.Trace);

+          }

 

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

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

+          {

+            foreach (string info in error.relatedInformation)

             {

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

+              Contract.Assert(info != null);

+              errorInfo.Out.WriteLine("       " + info);

             }

           }

-          else if (error is ReturnCounterexample)

+          if (CommandLineOptions.Clo.ErrorTrace > 0)

           {

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

-            }

+            errorInfo.Out.WriteLine("Execution trace:");

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

+          }

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

+          {

+            error.PrintModel(errorInfo.Out);

+          }

 

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

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

+          printer.WriteErrorInformation(errorInfo, tw);

 

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

+          if (er != null)

+          {

+            lock (er)

             {

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

+              er(errorInfo);

             }

           }

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

-

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

+        }

+      }

+    }

 

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

 

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

+    private static ErrorInformation CreateErrorInformation(Counterexample error, VC.VCGen.Outcome outcome)

+    {

+      // 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 cause = "Error";

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

+      {

+        cause = "Timed out on";

+      }

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

+      {

+        cause = "Out of memory on";

+      }

 

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

-              }

+      var callError = error as CallCounterexample;

+      var returnError = error as ReturnCounterexample;

+      var assertError = error as AssertCounterexample;

+      if (callError != null)

+      {

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

+        errorInfo.BoogieErrorCode = "BP5002";

+        errorInfo.Kind = ErrorKind.Precondition;

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

 

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

-              if (msg == null)

-              {

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

-              }

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

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

+        {

+          errorInfo = errorInformationFactory.CreateErrorInformation(null, callError.FailingRequires.ErrorMessage, callError.RequestId, cause);

+        }

+      }

+      else if (returnError != null)

+      {

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

+        errorInfo.BoogieErrorCode = "BP5003";

+        errorInfo.Kind = ErrorKind.Postcondition;

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

 

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

-              {

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

-              }

-            }

-          }

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

-          {

-            foreach (string info in error.relatedInformation)

-            {

-              Contract.Assert(info != null);

-              Console.WriteLine("       " + info);

-            }

-          }

-          if (CommandLineOptions.Clo.ErrorTrace > 0)

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

+        {

+          errorInfo = errorInformationFactory.CreateErrorInformation(null, returnError.FailingEnsures.ErrorMessage, returnError.RequestId, cause);

+        }

+      }

+      else // error is AssertCounterexample

+      {

+        if (assertError.FailingAssert is LoopInitAssertCmd)

+        {

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

+          errorInfo.BoogieErrorCode = "BP5004";

+          errorInfo.Kind = ErrorKind.InvariantEntry;

+        }

+        else if (assertError.FailingAssert is LoopInvMaintainedAssertCmd)

+        {

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

+          errorInfo.BoogieErrorCode = "BP5005";

+          errorInfo.Kind = ErrorKind.InvariantMaintainance;

+        }

+        else

+        {

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

+          var tok = assertError.FailingAssert.tok;

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

           {

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

-            error.Print(4);

-

-            foreach (Block b in error.Trace)

+            msg = assertError.FailingAssert.ErrorMessage;

+            tok = null;

+            if (cause == "Error")

             {

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

-              {

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

-              }

+              cause = null;

             }

           }

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

-          {

-            error.PrintModel();

-          }

-          if (cause == "Error")

+          string bec = null;

+          if (msg == null)

           {

-            errorCount++;

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

+            bec = "BP5001";

           }

-          if (er != null)

-          {

-            er(errorInfo);

-          }

-        }

-        if (cause == "Error")

-        {

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

+

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

+          errorInfo.BoogieErrorCode = bec;

+          errorInfo.Kind = ErrorKind.Assertion;

         }

       }

+

+      return errorInfo;

+    }

+

+

+    private static void WriteErrorInformationToXmlSink(ErrorInformation errorInfo, BlockSeq trace)

+    {

+      var msg = "assertion violation";

+      switch (errorInfo.Kind)

+      {

+        case ErrorKind.Precondition:

+          msg = "precondition violation";

+          break;

+

+        case ErrorKind.Postcondition:

+          msg = "postcondition violation";

+          break;

+

+        case ErrorKind.InvariantEntry:

+          msg = "loop invariant entry violation";

+          break;

+

+        case ErrorKind.InvariantMaintainance:

+          msg = "loop invariant maintenance violation";

+          break;

+      }

+

+      var relatedError = errorInfo.Aux.FirstOrDefault();

+      CommandLineOptions.Clo.XmlSink.WriteError(msg, errorInfo.Tok, relatedError.Tok, trace);

     }

 

   }

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index 14bb39ba..e3d3d109 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -91,25 +91,6 @@ namespace Microsoft.Boogie
   }

 

 

-  public class VerificationResult

-  {

-    public readonly string Checksum;

-    public readonly string DependeciesChecksum;

-    public readonly string RequestId;

-    public readonly ConditionGeneration.Outcome Outcome;

-    public readonly List<Counterexample> Errors;

-

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

-    {

-      Checksum = checksum;

-      DependeciesChecksum = depsChecksum;

-      Outcome = outcome;

-      Errors = errors;

-      RequestId = requestId;

-    }

-  }

-

-

   public class VerificationResultCache

   {

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

@@ -132,6 +113,19 @@ namespace Microsoft.Boogie
     }

 

 

+    public VerificationResult Lookup(Implementation impl)

+    {

+      if (!NeedsToBeVerified(impl))

+      {

+        return Lookup(impl.Id);

+      }

+      else

+      {

+        return null;

+      }

+    }

+

+

     public void Clear()

     {

       Cache.Clear();

@@ -153,16 +147,29 @@ namespace Microsoft.Boogie
 

     public bool NeedsToBeVerified(Implementation impl)

     {

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

-          || Cache[impl.Id].Checksum != impl.Checksum)

+      return VerificationPriority(impl) < int.MaxValue;

+    }

+

+

+    public int VerificationPriority(Implementation impl)

+    {

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

       {

-        return true;

+        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 int.MaxValue;  // skip verification (highest priority to get them done as soon as possible)

       }

-

-      var depsChecksum = DependencyCollector.DependenciesChecksum(impl);

-      return depsChecksum == null || Cache[impl.Id].DependeciesChecksum != depsChecksum;

     }

-

   }

 

 }