Merge

15 files changed, 367 insertions, 141 deletions

diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs
index 69e6b318..964bf024 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/OwickiGries.cs
@@ -19,7 +19,6 @@ namespace Microsoft.Boogie
         Implementation enclosingImpl;

         public Dictionary<Procedure, Procedure> procMap; /* Original -> Duplicate */

         public Dictionary<Absy, Absy> absyMap; /* Duplicate -> Original */

-        public Dictionary<Block, Block> blockMap; /* Original -> Duplicate */

         public Dictionary<Implementation, Implementation> implMap; /* Duplicate -> Original */

         public HashSet<Procedure> yieldingProcs;

         public List<Implementation> impls;

@@ -32,7 +31,6 @@ namespace Microsoft.Boogie
             this.enclosingImpl = null;

             this.procMap = new Dictionary<Procedure, Procedure>();

             this.absyMap = new Dictionary<Absy, Absy>();

-            this.blockMap = new Dictionary<Block, Block>();

             this.implMap = new Dictionary<Implementation, Implementation>();

             this.yieldingProcs = new HashSet<Procedure>();

             this.impls = new List<Implementation>();

@@ -124,7 +122,6 @@ namespace Microsoft.Boogie
         public override Block VisitBlock(Block node)

         {

             Block block = base.VisitBlock(node);

-            blockMap[node] = block;

             absyMap[block] = node;

             return block;

         }

@@ -215,21 +212,6 @@ namespace Microsoft.Boogie
             implMap[impl] = node;

             impl.LocVars.Add(dummyLocalVar);

             impl.Name = impl.Proc.Name;

-            foreach (Block block in impl.Blocks)

-            {

-                GotoCmd gotoCmd = block.TransferCmd as GotoCmd;

-                if (gotoCmd == null) continue;

-                List<Block> labelTargets = new List<Block>();

-                List<string> labelNames = new List<string>();

-                foreach (Block x in gotoCmd.labelTargets)

-                {

-                    Block y = (Block)blockMap[x];

-                    labelTargets.Add(y);

-                    labelNames.Add(y.Label);

-                }

-                gotoCmd.labelTargets = labelTargets;

-                gotoCmd.labelNames = labelNames;

-            }

             return impl;

         }

 

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index cd0c810c..a419fead 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -189,7 +189,7 @@ namespace Microsoft.Boogie {
     /// The numbered meta data enumerable that looks like the Enumerable

     /// of a dictionary.

     /// </value>

-    public IEnumerable<KeyValuePair<int, Object>> NumberedMetaData

+    public IEnumerable<KeyValuePair<int, Object>> NumberedMetadata

     {

       get {

         if (InternalNumberedMetadata == null)

@@ -207,7 +207,7 @@ namespace Microsoft.Boogie {
     /// <returns>The stored metadata of type T</returns>

     /// <param name="index">The index of the metadata</param>

     /// <typeparam name="T">The type of the metadata object required</typeparam>

-    public T GetMetatdata<T>(int index) {

+    public T GetMetadata<T>(int index) {

       // We aren't using NumberedMetadataLock for speed. Perhaps we should be using it?

       if (InternalNumberedMetadata == null)

         throw new ArgumentOutOfRangeException();

@@ -4074,7 +4074,7 @@ namespace Microsoft.Boogie {
     public override void Emit(TokenTextWriter stream, int level) {

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

       stream.WriteLine();

-      stream.WriteLine("{0};", Indent(level));

+      stream.WriteLine("{0};", Indent(stream.UseForComputingChecksums ? 0 : level));

       first.Emit(stream, level + 1);

       second.Emit(stream, level + 1);

     }

@@ -4099,7 +4099,7 @@ namespace Microsoft.Boogie {
     public override void Emit(TokenTextWriter stream, int level) {

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

       stream.WriteLine();

-      stream.WriteLine("{0}[]", Indent(level));

+      stream.WriteLine("{0}[]", Indent(stream.UseForComputingChecksums ? 0 : level));

       foreach (RE/*!*/ r in rs) {

         Contract.Assert(r != null);

         r.Emit(stream, level + 1);

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index c7edbc68..838699c1 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -2867,7 +2867,10 @@ namespace Microsoft.Boogie {
       if (stream.UseForComputingChecksums && QKeyValue.FindBoolAttribute(Attributes, "precondition_previous_snapshot")) { return; }

 

       stream.Write(this, level, "assume ");

-      EmitAttributes(stream, Attributes);

+      if (!stream.UseForComputingChecksums)

+      {

+        EmitAttributes(stream, Attributes);

+      }

       this.Expr.Emit(stream);

       stream.WriteLine(";");

     }

@@ -2988,6 +2991,16 @@ namespace Microsoft.Boogie {
       //Contract.Requires(tc != null);

       // nothing to typecheck

     }

+

+    public override string ToString()

+    {

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

+        System.IO.StringWriter buffer = new System.IO.StringWriter();

+        using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, /*setTokens=*/ false , /*pretty=*/ false)) {

+            this.Emit(stream, 0);

+        }

+        return buffer.ToString();

+    }

   }

   [ContractClassFor(typeof(TransferCmd))]

   public abstract class TransferCmdContracts : TransferCmd {

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index e9e6b60e..c49b3b3c 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -364,7 +364,7 @@ namespace Microsoft.Boogie {
       Contract.Invariant(0 <= PrintUnstructured && PrintUnstructured < 3);  // 0 = print only structured,  1 = both structured and unstructured,  2 = only unstructured

     }

 

-    public int VerifySnapshots = 0;

+    public int VerifySnapshots = -1;

     public bool VerifySeparately = false;

     public string PrintFile = null;

     public int PrintUnstructured = 0;

@@ -389,6 +389,7 @@ namespace Microsoft.Boogie {
     public bool Trace = false;

     public bool TraceTimes = false;

     public bool TraceProofObligations = false;

+    public bool TraceCaching = false;

     public bool NoResolve = false;

     public bool NoTypecheck = false;

     public bool OverlookBoogieTypeErrors = false;

@@ -1392,6 +1393,7 @@ namespace Microsoft.Boogie {
               ps.CheckBooleanFlag("wait", ref Wait) ||

               ps.CheckBooleanFlag("trace", ref Trace) ||

               ps.CheckBooleanFlag("traceTimes", ref TraceTimes) ||

+              ps.CheckBooleanFlag("traceCaching", ref TraceCaching) ||

               ps.CheckBooleanFlag("tracePOs", ref TraceProofObligations) ||

               ps.CheckBooleanFlag("noResolve", ref NoResolve) ||

               ps.CheckBooleanFlag("noTypecheck", ref NoTypecheck) ||

diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs
index b275288a..565b2f06 100644
--- a/Source/Core/Duplicator.cs
+++ b/Source/Core/Duplicator.cs
@@ -14,6 +14,11 @@ using System.Linq;
 

 namespace Microsoft.Boogie {

   public class Duplicator : StandardVisitor {

+    // This is used to ensure that Procedures get duplicated only once

+    // and that Implementation.Proc is resolved to the correct duplicated

+    // Procedure.

+    private Dictionary<Procedure,Procedure> OldToNewProcedureMap = null;

+

     public override Absy Visit(Absy node) {

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

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

@@ -70,7 +75,7 @@ namespace Microsoft.Boogie {
     public override Block VisitBlock(Block node) {

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

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

-      return base.VisitBlock((Block)node.Clone());

+      return base.VisitBlock((Block) node.Clone());

     }

     public override BvConcatExpr VisitBvConcatExpr (BvConcatExpr node) {

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

@@ -163,7 +168,24 @@ namespace Microsoft.Boogie {
     public override List<Declaration/*!*/>/*!*/ VisitDeclarationList(List<Declaration/*!*/>/*!*/ declarationList) {

       //Contract.Requires(cce.NonNullElements(declarationList));

       Contract.Ensures(cce.NonNullElements(Contract.Result<List<Declaration>>()));

-      return base.VisitDeclarationList(declarationList);

+

+      // For Implementation.Proc to resolve correctly to duplicated Procedures

+      // we need to visit the procedures first

+      for (int i = 0, n = declarationList.Count; i < n; i++) {

+        if (!( declarationList[i] is Procedure ))

+          continue;

+

+        declarationList[i] = cce.NonNull((Declaration) this.Visit(declarationList[i]));

+      }

+

+      // Now visit everything else

+      for (int i = 0, n = declarationList.Count; i < n; i++) {

+        if (declarationList[i] is Procedure)

+          continue;

+

+        declarationList[i] = cce.NonNull((Declaration) this.Visit(declarationList[i]));

+      }

+      return declarationList;

     }

     public override DeclWithFormals VisitDeclWithFormals(DeclWithFormals node) {

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

@@ -220,7 +242,10 @@ namespace Microsoft.Boogie {
     public override GotoCmd VisitGotoCmd(GotoCmd node) {

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

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

-      return base.VisitGotoCmd((GotoCmd)node.Clone());

+      // NOTE: This doesn't duplicate the labelTarget basic blocks

+      // or resolve them to the new blocks

+      // VisitImplementation() and VisitBlock() handle this

+      return base.VisitGotoCmd( (GotoCmd)node.Clone());

     }

     public override Cmd VisitHavocCmd(HavocCmd node) {

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

@@ -240,7 +265,30 @@ namespace Microsoft.Boogie {
     public override Implementation VisitImplementation(Implementation node) {

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

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

-      return base.VisitImplementation((Implementation)node.Clone());

+      var impl = base.VisitImplementation((Implementation)node.Clone());

+      var blockDuplicationMapping = new Dictionary<Block, Block>();

+

+      // Compute the mapping between the blocks of the old implementation (node)

+      // and the new implementation (impl).

+      foreach (var blockPair in node.Blocks.Zip(impl.Blocks)) {

+        blockDuplicationMapping.Add(blockPair.Item1, blockPair.Item2);

+      }

+

+      // The GotoCmds and blocks have now been duplicated.

+      // Resolve GotoCmd targets to the duplicated blocks

+      foreach (GotoCmd gotoCmd in impl.Blocks.Select( bb => bb.TransferCmd).OfType<GotoCmd>()) {

+        var newLabelTargets = new List<Block>();

+        var newLabelNames = new List<string>();

+        for (int index = 0; index < gotoCmd.labelTargets.Count; ++index) {

+          var newBlock = blockDuplicationMapping[gotoCmd.labelTargets[index]];

+          newLabelTargets.Add(newBlock);

+          newLabelNames.Add(newBlock.Label);

+        }

+        gotoCmd.labelTargets = newLabelTargets;

+        gotoCmd.labelNames = newLabelNames;

+      }

+

+      return impl;

     }

     public override LiteralExpr VisitLiteralExpr(LiteralExpr node) {

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

@@ -286,12 +334,37 @@ namespace Microsoft.Boogie {
     public override Procedure VisitProcedure(Procedure node) {

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

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

-      return base.VisitProcedure((Procedure)node.Clone());

+      Procedure newProcedure = null;

+      if (OldToNewProcedureMap != null && OldToNewProcedureMap.ContainsKey(node)) {

+        newProcedure = OldToNewProcedureMap[node];

+      } else {

+        newProcedure = base.VisitProcedure((Procedure) node.Clone());

+        if (OldToNewProcedureMap != null)

+          OldToNewProcedureMap[node] = newProcedure;

+      }

+      return newProcedure;

     }

     public override Program VisitProgram(Program node) {

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

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

-      return base.VisitProgram((Program)node.Clone());

+

+      // If cloning an entire program we need to ensure that

+      // Implementation.Proc gets resolved to the right Procedure

+      // (i.e. we don't duplicate Procedure twice) and CallCmds

+      // call the right Procedure.

+      // The map below is used to achieve this.

+      OldToNewProcedureMap = new Dictionary<Procedure, Procedure>();

+      var newProgram = base.VisitProgram((Program)node.Clone());

+

+      // We need to make sure that CallCmds get resolved to call Procedures we duplicated

+      // instead of pointing to procedures in the old program

+      var callCmds = newProgram.Blocks().SelectMany(b => b.Cmds).OfType<CallCmd>();

+      foreach (var callCmd in callCmds) {

+          callCmd.Proc = OldToNewProcedureMap[callCmd.Proc];

+      }

+

+      OldToNewProcedureMap = null; // This Visitor could be used for other things later so remove the map.

+      return newProgram;

     }

     public override QKeyValue VisitQKeyValue(QKeyValue node) {

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

@@ -694,4 +767,4 @@ namespace Microsoft.Boogie {
     }

   }

   #endregion

-}
\ No newline at end of file
+}

diff --git a/Source/Core/Util.cs b/Source/Core/Util.cs
index 0a2e5a22..06e4fcf0 100644
--- a/Source/Core/Util.cs
+++ b/Source/Core/Util.cs
@@ -313,7 +313,10 @@ namespace Microsoft.Boogie {
     }

 

     public void WriteIndent(int level) {

-      this.Write(Indent(level));

+      if (!UseForComputingChecksums)

+      {

+        this.Write(Indent(level));

+      }

     }

 

     public void Write(string text, params object[] args) {

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index b5f4f87b..e00b9b7a 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -398,10 +398,25 @@ namespace Microsoft.Boogie
 

     static int autoRequestIdCount;

 

+    static readonly string AutoRequestIdPrefix = "auto_request_id_";

+

     public static string FreshRequestId()

     {

       var id = Interlocked.Increment(ref autoRequestIdCount);

-      return string.Format("auto_request_id_{0}", id);

+      return AutoRequestIdPrefix + id;

+    }

+

+    public static int AutoRequestId(string id)

+    {

+      if (id.StartsWith(AutoRequestIdPrefix))

+      {

+        int result;

+        if (int.TryParse(id.Substring(AutoRequestIdPrefix.Length), out result))

+        {

+          return result;

+        }

+      }

+      return -1;

     }

 

     public readonly static VerificationResultCache Cache = new VerificationResultCache();

@@ -417,6 +432,11 @@ namespace Microsoft.Boogie
     

     static List<Checker> Checkers = new List<Checker>();

 

+    static DateTime FirstRequestStart;

+

+    static readonly ConcurrentDictionary<string, TimeSpan> TimePerRequest = new ConcurrentDictionary<string, TimeSpan>();

+    static readonly ConcurrentDictionary<string, PipelineStatistics> StatisticsPerRequest = new ConcurrentDictionary<string, PipelineStatistics>();

+

     static readonly ConcurrentDictionary<string, CancellationTokenSource> ImplIdToCancellationTokenSource = new ConcurrentDictionary<string, CancellationTokenSource>();

 

     static readonly ConcurrentDictionary<string, CancellationTokenSource> RequestIdToCancellationTokenSource = new ConcurrentDictionary<string, CancellationTokenSource>();

@@ -439,7 +459,7 @@ namespace Microsoft.Boogie
         return;

       }

 

-      if (0 < CommandLineOptions.Clo.VerifySnapshots && lookForSnapshots)

+      if (0 <= CommandLineOptions.Clo.VerifySnapshots && lookForSnapshots)

       {

         var snapshotsByVersion = LookForSnapshots(fileNames);

         foreach (var s in snapshotsByVersion)

@@ -810,6 +830,8 @@ namespace Microsoft.Boogie
         requestId = FreshRequestId();

       }

 

+      var start = DateTime.UtcNow;

+

       #region Do some pre-abstract-interpretation preprocessing on the program

       // Doing lambda expansion before abstract interpretation means that the abstract interpreter

       // never needs to see any lambda expressions.  (On the other hand, if it were useful for it

@@ -995,6 +1017,35 @@ namespace Microsoft.Boogie
         programCache.Set(programId, program, policy);

       }

 

+      if (0 <= CommandLineOptions.Clo.VerifySnapshots && CommandLineOptions.Clo.TraceCaching)

+      {

+        Console.Out.WriteLine("");

+        Console.Out.WriteLine("<trace caching>");

+

+        var end = DateTime.UtcNow;

+        if (TimePerRequest.Count == 0)

+        {

+          FirstRequestStart = start;

+        }

+        TimePerRequest[requestId] = end.Subtract(start);

+        StatisticsPerRequest[requestId] = stats;

+

+        Console.Out.WriteLine(CachedVerificationResultInjector.Statistics.Output(true));

+

+        Console.Out.WriteLine("Statistics per request as CSV:");

+        Console.Out.WriteLine("Request ID, Time (ms), Error, Inconclusive, Out of Memory, Timeout, Verified");

+        foreach (var kv in TimePerRequest.OrderBy(kv => ExecutionEngine.AutoRequestId(kv.Key)))

+        {

+          var s = StatisticsPerRequest[kv.Key];

+          Console.Out.WriteLine("{0}, {1:F0}, {2}, {3}, {4}, {5}, {6}", kv.Key, kv.Value.TotalMilliseconds, s.ErrorCount, s.InconclusiveCount, s.OutOfMemoryCount, s.TimeoutCount, s.VerifiedCount);

+        }

+

+        Console.Out.WriteLine("");

+        Console.Out.WriteLine("Total time (ms) since first request: {0:F0}", end.Subtract(FirstRequestStart).TotalMilliseconds);

+

+        Console.Out.WriteLine("</trace caching>");

+      }

+

       #endregion

 

       return outcome;

@@ -1394,11 +1445,6 @@ namespace Microsoft.Boogie
 

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

 

-      if (1 < CommandLineOptions.Clo.VerifySnapshots && CommandLineOptions.Clo.Trace)

-      {

-        printer.Inform(CachedVerificationResultInjector.Statistics.Output(CommandLineOptions.Clo.TraceTimes), tw);

-      }

-

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

     }

 

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index 67d6dde5..1de1a0ce 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -37,25 +37,27 @@ namespace Microsoft.Boogie
     public string Output(bool printTime = false)

     {

       var wr = new StringWriter();

-      wr.WriteLine("");

-      wr.WriteLine("Cached verification result injector statistics as CSV:");

-      if (printTime)

-      {

-        wr.WriteLine("Request ID, Time (ms), Rewritten Implementations, Low Priority Implementations, Medium Priority Implementations, High Priority Implementations, Skipped Implementations, Implementations");

-      }

-      else

-      {

-        wr.WriteLine("Request ID, Rewritten Implementations, Low Priority Implementations, Medium Priority Implementations, High Priority Implementations, Skipped Implementations, Implementations");

-      }

-      foreach (var kv in runs)

+      if (runs.Any())

       {

+        wr.WriteLine("Cached verification result injector statistics as CSV:");

         if (printTime)

         {

-          wr.WriteLine("{0}, {1}, {2}, {3}, {4}, {5}, {6}, {7}", kv.Key, kv.Value.End.Subtract(kv.Value.Start).TotalMilliseconds, kv.Value.RewrittenImplementationCount, kv.Value.LowPriorityImplementationCount, kv.Value.MediumPriorityImplementationCount, kv.Value.HighPriorityImplementationCount, kv.Value.SkippedImplementationCount, kv.Value.ImplementationCount);

+          wr.WriteLine("Request ID, Time (ms), Rewritten Implementations, Low Priority Implementations, Medium Priority Implementations, High Priority Implementations, Skipped Implementations, Implementations");

         }

         else

         {

-          wr.WriteLine("{0}, {1}, {2}, {3}, {4}, {5}, {6}", kv.Key, kv.Value.RewrittenImplementationCount, kv.Value.LowPriorityImplementationCount, kv.Value.MediumPriorityImplementationCount, kv.Value.HighPriorityImplementationCount, kv.Value.SkippedImplementationCount, kv.Value.ImplementationCount);

+          wr.WriteLine("Request ID, Rewritten Implementations, Low Priority Implementations, Medium Priority Implementations, High Priority Implementations, Skipped Implementations, Implementations");

+        }

+        foreach (var kv in runs.OrderBy(kv => ExecutionEngine.AutoRequestId(kv.Key)))

+        {

+          if (printTime)

+          {

+            wr.WriteLine("{0}, {1:F0}, {2}, {3}, {4}, {5}, {6}, {7}", kv.Key, kv.Value.End.Subtract(kv.Value.Start).TotalMilliseconds, kv.Value.RewrittenImplementationCount, kv.Value.LowPriorityImplementationCount, kv.Value.MediumPriorityImplementationCount, kv.Value.HighPriorityImplementationCount, kv.Value.SkippedImplementationCount, kv.Value.ImplementationCount);

+          }

+          else

+          {

+            wr.WriteLine("{0}, {1}, {2}, {3}, {4}, {5}, {6}", kv.Key, kv.Value.RewrittenImplementationCount, kv.Value.LowPriorityImplementationCount, kv.Value.MediumPriorityImplementationCount, kv.Value.HighPriorityImplementationCount, kv.Value.SkippedImplementationCount, kv.Value.ImplementationCount);

+          }

         }

       }

       return wr.ToString();

@@ -181,7 +183,7 @@ namespace Microsoft.Boogie
 

     private static void SetErrorChecksumsInCachedSnapshot(Implementation implementation, VerificationResult result)

     {

-      if (result.Errors != null && result.Errors.Count < CommandLineOptions.Clo.ProverCCLimit)

+      if (result.Outcome == ConditionGeneration.Outcome.Errors && result.Errors != null && result.Errors.Count < CommandLineOptions.Clo.ProverCCLimit)

       {

         implementation.SetErrorChecksumToCachedError(result.Errors.Select(cex => new Tuple<byte[], object>(cex.Checksum, cex)));

       }

@@ -270,6 +272,8 @@ namespace Microsoft.Boogie
 

     public static void Collect(IEnumerable<Axiom> axioms)

     {

+      var start = DateTime.UtcNow;

+

       var v = new OtherDefinitionAxiomsCollector();

       foreach (var a in axioms)

       {

@@ -277,6 +281,15 @@ namespace Microsoft.Boogie
         v.VisitExpr(a.Expr);

         v.currentAxiom = null;

       }

+

+      var end = DateTime.UtcNow;

+      if (CommandLineOptions.Clo.TraceCaching)

+      {

+        Console.Out.WriteLine("");

+        Console.Out.WriteLine("<trace caching>");

+        Console.Out.WriteLine("Collected other definition axioms within {0:F0} ms.", end.Subtract(start).TotalMilliseconds);

+        Console.Out.WriteLine("</trace caching>");

+      }

     }

 

     public override QuantifierExpr VisitQuantifierExpr(QuantifierExpr node)

@@ -315,8 +328,19 @@ namespace Microsoft.Boogie
 

     public static void Collect(Program program)

     {

+      var start = DateTime.UtcNow;

+

       var dc = new DependencyCollector();

       dc.VisitProgram(program);

+

+      var end = DateTime.UtcNow;

+      if (CommandLineOptions.Clo.TraceCaching)

+      {

+        Console.Out.WriteLine("");

+        Console.Out.WriteLine("<trace caching>");

+        Console.Out.WriteLine("Collected dependencies within {0:F0} ms.", end.Subtract(start).TotalMilliseconds);

+        Console.Out.WriteLine("</trace caching>");

+      }

     }

 

     public static bool AllFunctionDependenciesAreDefinedAndUnchanged(Procedure oldProc, Program newProg)

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 01b8f3f6..1b52d797 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -163,7 +163,7 @@ namespace Microsoft.Boogie.SMTLib
     readonly List<string> proverErrors = new List<string>();

     readonly List<string> proverWarnings = new List<string>();

     readonly StringBuilder common = new StringBuilder();

-    TextWriter currentLogFile;

+    protected TextWriter currentLogFile;

     protected volatile ErrorHandler currentErrorHandler;

 

     private void FeedTypeDeclsToProver()

@@ -2102,9 +2102,18 @@ namespace Microsoft.Boogie.SMTLib
   {

       public SMTLibInterpolatingProcessTheoremProver(ProverOptions options, VCExpressionGenerator gen,

                                         SMTLibProverContext ctx)

-          : base(options, gen, ctx)

+          : base(AddInterpOption(options), gen, ctx)

       {

-          // anything else?

+

+      }

+

+      private static ProverOptions AddInterpOption(ProverOptions options)

+      {

+          var opts = (SMTLibProverOptions)options;

+          opts.AddSmtOption("produce-interpolants", "true");

+          if (CommandLineOptions.Clo.PrintFixedPoint == null)

+              CommandLineOptions.Clo.PrintFixedPoint = "itp.fixedpoint.bpl";

+          return opts;

       }

 

       public override void AssertNamed(VCExpr vc, bool polarity, string name)

@@ -2232,12 +2241,10 @@ namespace Microsoft.Boogie.SMTLib
 

           vcStr = "(get-interpolant (and\r\n" + vcStr + "\r\n))";

           SendThisVC(vcStr);

+          if(currentLogFile != null) currentLogFile.Flush();

 

           List<SExpr> interpolantList;

-          Outcome result2 = GetTreeInterpolantResponse(out interpolantList);

-

-          if (result2 != Outcome.Valid)

-              return null;

+          GetTreeInterpolantResponse(out interpolantList);

 

           Dictionary<string, VCExpr> bound = new Dictionary<string, VCExpr>();

           foreach (SExpr sexpr in interpolantList)

@@ -2249,10 +2256,8 @@ namespace Microsoft.Boogie.SMTLib
           return result;

       }

 

-      private Outcome GetTreeInterpolantResponse(out List<SExpr> interpolantList)

+      private void GetTreeInterpolantResponse(out List<SExpr> interpolantList)

       {

-          var result = Outcome.Undetermined;

-          var wasUnknown = false;

           interpolantList = new List<SExpr>();

 

           Process.Ping();

@@ -2262,69 +2267,12 @@ namespace Microsoft.Boogie.SMTLib
               var resp = Process.GetProverResponse();

               if (resp == null || Process.IsPong(resp))

                   break;

-

-              switch (resp.Name)

-              {

-                  case "unsat":

-                      result = Outcome.Valid;

-                      break;

-                  case "sat":

-                      result = Outcome.Invalid;

-                      break;

-                  case "unknown":

-                      result = Outcome.Invalid;

-                      wasUnknown = true;

-                      break;

-                  default:

-                      if (result == Outcome.Valid)

-                      {

-                          SExpr interpolant = resp as SExpr;

-                          interpolantList.Add(interpolant);

-                          continue;

-                          //return result;

-                      }

-                      HandleProverError("Unexpected prover response: " + resp.ToString());

-                      break;

-              }

+              

+              SExpr interpolant = resp as SExpr;

+              if(interpolant == null)

+                  HandleProverError("Unexpected prover response: got null for interpolant!");

+              interpolantList.Add(interpolant);

           }

-

-          if (wasUnknown)

-          {

-              SendThisVC("(get-info :reason-unknown)");

-              Process.Ping();

-

-              while (true)

-              {

-                  var resp = Process.GetProverResponse();

-                  if (resp == null || Process.IsPong(resp))

-                      break;

-

-                  if (resp.ArgCount == 1 && resp.Name == ":reason-unknown")

-                  {

-                      switch (resp[0].Name)

-                      {

-                          case "memout":

-                              currentErrorHandler.OnResourceExceeded("memory");

-                              result = Outcome.OutOfMemory;

-                              Process.NeedsRestart = true;

-                              break;

-                          case "timeout":

-                          case "canceled":

-                              currentErrorHandler.OnResourceExceeded("timeout");

-                              result = Outcome.TimeOut;

-                              break;

-                          default:

-                              break;

-                      }

-                  }

-                  else

-                  {

-                      HandleProverError("Unexpected prover response (getting info about 'unknown' response): " + resp.ToString());

-                  }

-              }

-          }

-

-          return result;

       }

   }

 

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 60a54346..52db07d9 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1330,7 +1330,20 @@ namespace VC {
 

       currentImplementation = impl;

       currentTemporaryVariableForAssertions = null;

+

+      var start = DateTime.UtcNow;

+

       Dictionary<Variable, Expr> r = ConvertBlocks2PassiveCmd(impl.Blocks, impl.Proc.Modifies, mvInfo);

+      

+      var end = DateTime.UtcNow;

+      if (CommandLineOptions.Clo.TraceCaching)

+      {

+        Console.Out.WriteLine("");

+        Console.Out.WriteLine("<trace caching>");

+        Console.Out.WriteLine("Turned implementation into passive commands within {0:F0} ms.", end.Subtract(start).TotalMilliseconds);

+        Console.Out.WriteLine("</trace caching>");

+      }

+

       currentTemporaryVariableForAssertions = null;

       currentImplementation = null;

 

@@ -1475,14 +1488,17 @@ namespace VC {
           }

         }

         Contract.Assert(copy != null);

-        var isAssumePre = false;

+        var dropCmd = false;

         if (pc is AssertCmd) {

           var ac = (AssertCmd)pc;

           ac.OrigExpr = ac.Expr;

           Contract.Assert(ac.IncarnationMap == null);

           ac.IncarnationMap = (Dictionary<Variable, Expr>)cce.NonNull(new Dictionary<Variable, Expr>(incarnationMap));

 

-          if (currentImplementation != null

+          var subsumption = Wlp.Subsumption(ac);

+          var alwaysUseSubsumption = subsumption == CommandLineOptions.SubsumptionOption.Always;

+          if (alwaysUseSubsumption

+              && currentImplementation != null

               && ((currentImplementation.NoErrorsInCachedSnapshot

                    && currentImplementation.InjectedAssumptionVariables != null

                    && 2 <= currentImplementation.InjectedAssumptionVariables.Count)

@@ -1510,9 +1526,13 @@ namespace VC {
                    && !currentImplementation.ErrorChecksumToCachedError.ContainsKey(ac.Checksum)

                    && (currentImplementation.InjectedAssumptionVariables == null || !currentImplementation.InjectedAssumptionVariables.Any(v => incarnationMap.ContainsKey(v))))

           {

-            // Turn it into an assume statement.

-            pc = new AssumeCmd(ac.tok, copy);

-            pc.Attributes = new QKeyValue(Token.NoToken, "verified_assertion", new List<object>(), pc.Attributes);

+            if (alwaysUseSubsumption)

+            {

+              // Turn it into an assume statement.

+              pc = new AssumeCmd(ac.tok, copy);

+              pc.Attributes = new QKeyValue(Token.NoToken, "verified_assertion", new List<object>(), pc.Attributes);

+            }

+            dropCmd = subsumption == CommandLineOptions.SubsumptionOption.Never;

           }

           else if (currentImplementation != null

                    && currentImplementation.AnyErrorsInCachedSnapshot

@@ -1521,10 +1541,17 @@ namespace VC {
                    && currentImplementation.ErrorChecksumToCachedError.ContainsKey(ac.Checksum)

                    && (currentImplementation.InjectedAssumptionVariables == null || !currentImplementation.InjectedAssumptionVariables.Any(v => incarnationMap.ContainsKey(v))))

           {

-            // Turn it into an assume statement.

-            pc = new AssumeCmd(ac.tok, copy);

-            pc.Attributes = new QKeyValue(Token.NoToken, "recycled_failing_assertion", new List<object>(), pc.Attributes);

-            currentImplementation.AddRecycledFailingAssertion(ac);

+            if (alwaysUseSubsumption)

+            {

+              // Turn it into an assume statement.

+              pc = new AssumeCmd(ac.tok, copy);

+              pc.Attributes = new QKeyValue(Token.NoToken, "recycled_failing_assertion", new List<object>(), pc.Attributes);

+            }

+            dropCmd = subsumption == CommandLineOptions.SubsumptionOption.Never;

+            if (dropCmd || alwaysUseSubsumption)

+            {

+              currentImplementation.AddRecycledFailingAssertion(ac);

+            }

           }

         }

         else if (pc is AssumeCmd

@@ -1533,10 +1560,10 @@ namespace VC {
                  && currentImplementation.InjectedAssumptionVariables.Any())

         {

           copy = LiteralExpr.Imp(currentImplementation.ConjunctionOfInjectedAssumptionVariables(incarnationMap), copy);

-          isAssumePre = true;

+          dropCmd = true;

         }

         pc.Expr = copy;

-        if (!isAssumePre

+        if (!dropCmd

             || currentImplementation.NoErrorsInCachedSnapshot

             || (currentImplementation.AnyErrorsInCachedSnapshot

                 && pc.Checksum != null

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index d7f282fa..1471f30f 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -34,7 +34,7 @@ namespace VC {
     public Dictionary<Block, Macro> reachMacros;

     public Dictionary<Block, VCExpr> reachMacroDefinitions;

 

-    public StratifiedVC(StratifiedInliningInfo siInfo) {

+    public StratifiedVC(StratifiedInliningInfo siInfo, HashSet<string> procCalls) {

       info = siInfo;

       info.GenerateVC();

       var vcgen = info.vcgen;

@@ -75,6 +75,10 @@ namespace VC {
           vcexpr = RenameVCExprLabels.Apply(vcexpr, info.vcgen.prover.VCExprGen, info.label2absy, block2label);

       }

 

+      if(procCalls != null)

+         vcexpr = RemoveProcedureCalls.Apply(vcexpr, info.vcgen.prover.VCExprGen, procCalls);

+

+      #if false

       var impl = info.impl;

       reachMacros = new Dictionary<Block, Macro>();

       reachMacroDefinitions = new Dictionary<Block, VCExpr>();

@@ -93,6 +97,7 @@ namespace VC {
           reachMacroDefinitions[successorBlock] = gen.Or(reachMacroDefinitions[successorBlock], gen.And(gen.Function(reachMacros[currBlock]), controlTransferExpr));

         }

       }

+      #endif

 

       callSites = new Dictionary<Block, List<StratifiedCallSite>>();

       foreach (Block b in info.callSites.Keys) {

@@ -141,6 +146,7 @@ namespace VC {
     }

   }

 

+  // Rename all labels in a VC to (globally) fresh labels

   class RenameVCExprLabels : MutatingVCExprVisitor<bool>

   {

       Dictionary<int, Absy> label2absy;

@@ -203,6 +209,50 @@ namespace VC {
       }

   }

 

+  // Remove the uninterpreted function calls that substitute procedure calls

+  class RemoveProcedureCalls : MutatingVCExprVisitor<bool>

+  {

+      HashSet<string> procNames;

+

+      RemoveProcedureCalls(VCExpressionGenerator gen, HashSet<string> procNames)

+          : base(gen)

+      {

+          this.procNames = procNames;

+      }

+

+      public static VCExpr Apply(VCExpr expr, VCExpressionGenerator gen, HashSet<string> procNames)

+      {

+          return (new RemoveProcedureCalls(gen, procNames)).Mutate(expr, true);

+      }

+

+      // Finds labels and changes them to a globally unique label:

+      protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode,

+                                                    List<VCExpr/*!*/>/*!*/ newSubExprs,

+                                                    bool changed,

+                                                    bool arg)

+      {

+          //Contract.Ensures(Contract.Result<VCExpr>() != null);

+

+          VCExpr ret;

+          if (changed)

+              ret = Gen.Function(originalNode.Op,

+                                 newSubExprs, originalNode.TypeArguments);

+          else

+              ret = originalNode;

+

+          if (!(ret is VCExprNAry)) return ret;

+          VCExprNAry retnary = (VCExprNAry)ret;

+          if (!(retnary.Op is VCExprBoogieFunctionOp))

+              return ret;

+

+          var fcall = (retnary.Op as VCExprBoogieFunctionOp).Func.Name;

+          if (procNames.Contains(fcall))

+              return VCExpressionGenerator.True;

+          return ret;

+      }

+  }

+

+

   public class CallSite {

     public string calleeName;

     public List<VCExpr> interfaceExprs;

@@ -614,7 +664,7 @@ namespace VC {
           NAryExpr naryExpr = assumeCmd.Expr as NAryExpr;

           if (naryExpr == null) continue;

           if (!implName2StratifiedInliningInfo.ContainsKey(naryExpr.Fun.FunctionName)) continue;

-          Variable callSiteVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "StratifiedInliningCallSite" + callSiteId, Microsoft.Boogie.Type.Bool));

+          Variable callSiteVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "SICS" + callSiteId, Microsoft.Boogie.Type.Bool));

           implementation.LocVars.Add(callSiteVar);

           newCmds.Add(new AssumeCmd(Token.NoToken, new IdentifierExpr(Token.NoToken, callSiteVar)));

           callSiteId++;

@@ -674,13 +724,13 @@ namespace VC {
 

     private int macroCountForStratifiedInlining = 0;

     public Macro CreateNewMacro() {

-      string newName = "StratifiedInliningMacro@" + macroCountForStratifiedInlining.ToString();

+      string newName = "SIMacro@" + macroCountForStratifiedInlining.ToString();

       macroCountForStratifiedInlining++;

       return new Macro(Token.NoToken, newName, new List<Variable>(), new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Bool), false));

     }

     private int varCountForStratifiedInlining = 0;

     public VCExprVar CreateNewVar(Microsoft.Boogie.Type type) {

-      string newName = "StratifiedInliningVar@" + varCountForStratifiedInlining.ToString();

+      string newName = "SIV@" + varCountForStratifiedInlining.ToString();

       varCountForStratifiedInlining++;

       Constant newVar = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, newName, type));

       prover.Context.DeclareConstant(newVar, false, null);

diff --git a/Test/snapshots/Snapshots24.v0.bpl b/Test/snapshots/Snapshots24.v0.bpl
new file mode 100644
index 00000000..1289399b
--- /dev/null
+++ b/Test/snapshots/Snapshots24.v0.bpl
@@ -0,0 +1,25 @@
+procedure {:checksum "0"} M();

+

+implementation {:id "M"} {:checksum "1"} M()

+{

+    if (*)

+    {

+        assert {:subsumption 0} 1 != 1;  // error

+    }

+    else if (*)

+    {

+        assert {:subsumption 1} 5 != 5;  // error

+    }

+    else if (*)

+    {

+        assert {:subsumption 2} 6 != 6;  // error

+    }

+    else

+    {

+        assert {:subsumption 1} 2 == 2;

+        assert {:subsumption 2} 4 == 4;

+        assert 5 == 5;

+    }

+

+    assert {:subsumption 0} 3 == 3;

+}

diff --git a/Test/snapshots/Snapshots24.v1.bpl b/Test/snapshots/Snapshots24.v1.bpl
new file mode 100644
index 00000000..00d65961
--- /dev/null
+++ b/Test/snapshots/Snapshots24.v1.bpl
@@ -0,0 +1,25 @@
+procedure {:checksum "0"} M();

+

+implementation {:id "M"} {:checksum "2"} M()

+{

+    if (*)

+    {

+        assert {:subsumption 0} 1 == 1;

+    }

+    else if (*)

+    {

+        assert {:subsumption 1} 5 == 5;

+    }

+    else if (*)

+    {

+        assert {:subsumption 2} 6 != 6;  // error

+    }

+    else

+    {

+        assert {:subsumption 1} 2 == 2;

+        assert {:subsumption 2} 4 == 4;

+        assert 5 == 5;

+    }

+

+    assert {:subsumption 0} 3 == 3;

+}

diff --git a/Test/snapshots/runtest.snapshot b/Test/snapshots/runtest.snapshot
index 32c88216..04943c25 100644
--- a/Test/snapshots/runtest.snapshot
+++ b/Test/snapshots/runtest.snapshot
@@ -1,2 +1,2 @@
-// RUN: %boogie -errorTrace:0 -verifySnapshots:2 -verifySeparately Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl Snapshots8.bpl Snapshots9.bpl Snapshots10.bpl Snapshots11.bpl Snapshots12.bpl Snapshots13.bpl Snapshots14.bpl Snapshots15.bpl Snapshots16.bpl Snapshots17.bpl Snapshots18.bpl Snapshots19.bpl Snapshots20.bpl Snapshots21.bpl Snapshots22.bpl Snapshots23.bpl > "%t"
+// RUN: %boogie -errorTrace:0 -verifySnapshots:2 -verifySeparately Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl Snapshots8.bpl Snapshots9.bpl Snapshots10.bpl Snapshots11.bpl Snapshots12.bpl Snapshots13.bpl Snapshots14.bpl Snapshots15.bpl Snapshots16.bpl Snapshots17.bpl Snapshots18.bpl Snapshots19.bpl Snapshots20.bpl Snapshots21.bpl Snapshots22.bpl Snapshots23.bpl Snapshots24.bpl > "%t"
 // RUN: %diff "%s.expect" "%t"
diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect
index fd054579..899cd914 100644
--- a/Test/snapshots/runtest.snapshot.expect
+++ b/Test/snapshots/runtest.snapshot.expect
@@ -152,3 +152,11 @@ Boogie program verifier finished with 1 verified, 1 error
 Snapshots23.v0.bpl(7,9): Error BP5001: This assertion might not hold.

 

 Boogie program verifier finished with 1 verified, 1 error

+Snapshots24.v0.bpl(7,9): Error BP5001: This assertion might not hold.

+Snapshots24.v0.bpl(11,9): Error BP5001: This assertion might not hold.

+Snapshots24.v0.bpl(15,9): Error BP5001: This assertion might not hold.

+

+Boogie program verifier finished with 0 verified, 3 errors

+Snapshots24.v0.bpl(15,9): Error BP5001: This assertion might not hold.

+

+Boogie program verifier finished with 0 verified, 1 error