Worked on an extension of the existing verification result caching.

20 files changed, 662 insertions, 43 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 3b517c51..0026a3fe 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -2664,6 +2664,51 @@ namespace Microsoft.Boogie {
       }

     }

 

+    // TODO(wuestholz): Make this a 'List<Counterexample>'.

+    public IList<object> ErrorsInCachedSnapshot { get; set; }

+

+    public bool NoErrorsInCachedSnapshot

+    {

+      get

+      {

+        return ErrorsInCachedSnapshot != null && !ErrorsInCachedSnapshot.Any();

+      }

+    }

+

+    public bool AnyErrorsInCachedSnapshot

+    {

+      get

+      {

+        return ErrorsInCachedSnapshot != null && ErrorsInCachedSnapshot.Any();

+      }

+    }

+

+    IList<LocalVariable> injectedAssumptionVariables;

+    public IList<LocalVariable> InjectedAssumptionVariables

+    {

+      get

+      {

+        return injectedAssumptionVariables;

+      }

+    }

+

+    public Expr ConjunctionOfInjectedAssumptionVariables()

+    {

+      Contract.Requires(InjectedAssumptionVariables != null && InjectedAssumptionVariables.Any());

+

+      return LiteralExpr.BinaryTreeAnd(injectedAssumptionVariables.Select(v => (Expr)(new IdentifierExpr(Token.NoToken, v))).ToList());

+    }

+

+    public void InjectAssumptionVariable(LocalVariable variable)

+    {

+      if (injectedAssumptionVariables == null)

+      {

+        injectedAssumptionVariables = new List<LocalVariable>();

+      }

+      injectedAssumptionVariables.Add(variable);

+      LocVars.Add(variable);

+    }

+

     public Implementation(IToken tok, string name, List<TypeVariable> typeParams, List<Variable> inParams, List<Variable> outParams, List<Variable> localVariables, [Captured] StmtList structuredStmts, QKeyValue kv)

       : this(tok, name, typeParams, inParams, outParams, localVariables, structuredStmts, kv, new Errors()) {

       Contract.Requires(structuredStmts != null);

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 1922f977..c7ad0f11 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -1682,6 +1682,24 @@ namespace Microsoft.Boogie {
     }

     protected abstract Cmd/*!*/ ComputeDesugaring();

 

+    public void ExtendDesugaring(IEnumerable<Cmd> before, IEnumerable<Cmd> after)

+    {

+      var desug = Desugaring;

+      var stCmd = desug as StateCmd;

+      if (stCmd != null)

+      {

+        stCmd.Cmds.InsertRange(0, before);

+        stCmd.Cmds.AddRange(after);

+      }

+      else if (desug != null)

+      {

+        var cmds = new List<Cmd>(before);

+        cmds.Add(desug);

+        cmds.AddRange(after);

+        desugaring = new StateCmd(Token.NoToken, new List<Variable>(), cmds);

+      }

+    }

+

     public override void Emit(TokenTextWriter stream, int level) {

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

       if (CommandLineOptions.Clo.PrintDesugarings) {

@@ -2336,11 +2354,11 @@ namespace Microsoft.Boogie {
       #endregion

 

       #region assume Post[ins, outs, old(frame) := cins, couts, cframe]

-      Substitution s2 = Substituter.SubstitutionFromHashtable(substMap);

-      Substitution s2old = Substituter.SubstitutionFromHashtable(substMapOld);

+      calleeSubstitution = Substituter.SubstitutionFromHashtable(substMap);

+      calleeSubstitutionOld = Substituter.SubstitutionFromHashtable(substMapOld);

       foreach (Ensures/*!*/ e in this.Proc.Ensures) {

         Contract.Assert(e != null);

-        Expr copy = Substituter.ApplyReplacingOldExprs(s2, s2old, e.Condition);

+        Expr copy = Substituter.ApplyReplacingOldExprs(calleeSubstitution, calleeSubstitutionOld, e.Condition);

         AssumeCmd assume = new AssumeCmd(this.tok, copy);

         #region stratified inlining support

         if (QKeyValue.FindBoolAttribute(e.Attributes, "si_fcall"))

@@ -2373,6 +2391,69 @@ namespace Microsoft.Boogie {
       return new StateCmd(this.tok, tempVars, newBlockBody);

     }

 

+    class NameEqualityComparer : EqualityComparer<IdentifierExpr>

+    {

+      public override bool Equals(IdentifierExpr x, IdentifierExpr y)

+      {

+        return x.Name.Equals(y.Name);

+      }

+

+      public override int GetHashCode(IdentifierExpr obj)

+      {

+        return obj.Name.GetHashCode();

+      }

+    }

+

+    NameEqualityComparer comparer = new NameEqualityComparer();

+

+    Substitution calleeSubstitution;

+    Substitution calleeSubstitutionOld;

+

+    public IEnumerable<IdentifierExpr> UnmodifiedBefore(Procedure oldProcedure)

+    {

+      Contract.Requires(oldProcedure != null);

+

+      return Proc.Modifies.Except(oldProcedure.Modifies, comparer).Select(e => new IdentifierExpr(Token.NoToken, e.Decl));

+    }

+

+    public Expr Postcondition(Procedure procedure, Program program)

+    {

+      Contract.Requires(calleeSubstitution != null && calleeSubstitutionOld != null && program != null);

+

+      var ensures = procedure.Ensures.Select(e => Substituter.FunctionCallReresolvingApplyReplacingOldExprs(calleeSubstitution, calleeSubstitutionOld, e.Condition, program));

+      return Conjunction(ensures);

+    }

+

+    public Expr Precondition(Procedure procedure, Program program)

+    {

+      Contract.Requires(calleeSubstitution != null && calleeSubstitutionOld != null && program != null);

+

+      var requires = procedure.Requires.Select(r => Substituter.FunctionCallReresolvingApplyReplacingOldExprs(calleeSubstitution, calleeSubstitutionOld, r.Condition, program));

+      return Conjunction(requires);

+    }

+

+    private static Expr Conjunction(IEnumerable<Expr> conjuncts)

+    {

+      // TODO(wuestholz): Should we use 'LiteralExpr.BinaryTreeAnd' instead?      

+      Expr result = null;

+      foreach (var c in conjuncts)

+      {

+        if (result != null)

+        {

+          result = LiteralExpr.And(result, c);

+        }

+        else

+        {

+          result = c;

+        }

+      }

+      if (result == null)

+      {

+        result = new LiteralExpr(Token.NoToken, true);

+      }

+      return result;

+    }

+

     public override Absy StdDispatch(StandardVisitor visitor) {

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

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

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 2a995fc2..4f9488a3 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -1314,7 +1314,7 @@ namespace Microsoft.Boogie {
           return true;

 

         case "verifySnapshots":

-          ps.GetNumericArgument(ref VerifySnapshots, 2);

+          ps.GetNumericArgument(ref VerifySnapshots, 3);

           return true;

 		

 		case "useSmtOutputFormat": {

@@ -1750,7 +1750,8 @@ namespace Microsoft.Boogie {
                 verify several program snapshots (named <filename>.v0.bpl

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

                 0 - do not use any verification result caching (default)

-                1 - use verification result caching

+                1 - use the basic verification result caching

+                2 - use the more advanced verification result caching

   /verifySeparately

                 verify each input program separately

   /removeEmptyBlocks:<c>

diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs
index 70018a1a..86311d18 100644
--- a/Source/Core/Duplicator.cs
+++ b/Source/Core/Duplicator.cs
@@ -10,6 +10,7 @@
 using System.Collections;

 using System.Collections.Generic;

 using System.Diagnostics.Contracts;

+using System.Linq;

 

 namespace Microsoft.Boogie {

   public class Duplicator : StandardVisitor {

@@ -476,6 +477,15 @@ namespace Microsoft.Boogie {
       return (Expr)new ReplacingOldSubstituter(always, forOld).Visit(expr);

     }

 

+    public static Expr FunctionCallReresolvingApplyReplacingOldExprs(Substitution always, Substitution forOld, Expr expr, Program program)

+    {

+      Contract.Requires(always != null);

+      Contract.Requires(forOld != null);

+      Contract.Requires(expr != null);

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

+      return (Expr)new FunctionCallReresolvingReplacingOldSubstituter(program, always, forOld).Visit(expr);

+    }

+

     // ----------------------------- Substitutions for Cmd -------------------------------

 

     /// <summary>

@@ -611,7 +621,34 @@ namespace Microsoft.Boogie {
       }

     }

 

-    private sealed class ReplacingOldSubstituter : Duplicator {

+    private sealed class FunctionCallReresolvingReplacingOldSubstituter : ReplacingOldSubstituter

+    {

+      readonly Program Program;

+

+      public FunctionCallReresolvingReplacingOldSubstituter(Program program, Substitution always, Substitution forold)

+        : base(always, forold)

+      {

+        Program = program;

+      }

+

+      public override Expr VisitNAryExpr(NAryExpr node)

+      {

+        var result = base.VisitNAryExpr(node);

+        var nAryExpr = result as NAryExpr;

+        if (nAryExpr != null)

+        {

+          var funCall = nAryExpr.Fun as FunctionCall;

+          if (funCall != null)

+          {

+            // TODO(wuestholz): Maybe we should speed up this lookup.

+            funCall.Func = Program.TopLevelDeclarations.OfType<Function>().FirstOrDefault(f => f.Name == funCall.FunctionName);

+          }

+        }

+        return result;

+      }

+    }

+

+    private class ReplacingOldSubstituter : Duplicator {

       private readonly Substitution/*!*/ always;

       private readonly Substitution/*!*/ forold;

       [ContractInvariantMethod]

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 6a4dbc07..925b414b 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -317,9 +317,32 @@ namespace Microsoft.Boogie
 

   public class VerificationResult

   {

+    public readonly string RequestId;

     public readonly string Checksum;

     public readonly string DependeciesChecksum;

-    public readonly string RequestId;

+    public readonly string ImplementationName;

+    public readonly IToken ImplementationToken;

+

+    private readonly WeakReference program;

+    public Program Program

+    {

+      get

+      {

+        if (program == null)

+        {

+          return null;

+        }

+        try

+        {

+          var p = program.Target as Program;

+          return p;

+        }

+        catch (InvalidOperationException)

+        {

+          return null;

+        }

+      }

+    }

 

     public DateTime Start { get; set; }

     public DateTime End { get; set; }

@@ -328,24 +351,20 @@ namespace Microsoft.Boogie
     public int ProofObligationCountBefore { get; set; }

     public int ProofObligationCountAfter { get; set; }

 

-    public ConditionGeneration.Outcome Outcome;

+    public ConditionGeneration.Outcome Outcome { get; set; }

     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)

+    public VerificationResult(string requestId, string checksum, string depsChecksum, string implementationName, IToken implementationToken, Program program = null)

     {

       Checksum = checksum;

       DependeciesChecksum = depsChecksum;

       RequestId = requestId;

+      ImplementationName = implementationName;

+      ImplementationToken = implementationToken;

+      if (program != null)

+      {

+        this.program = new WeakReference(program);

+      }

     }

   }

 

@@ -844,7 +863,7 @@ namespace Microsoft.Boogie
       Implementation[] stablePrioritizedImpls = null;

       if (0 < CommandLineOptions.Clo.VerifySnapshots)

       {

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

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

         stablePrioritizedImpls = impls.OrderByDescending(

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

       }

@@ -855,6 +874,11 @@ namespace Microsoft.Boogie
 

       #endregion

 

+      if (1 < CommandLineOptions.Clo.VerifySnapshots)

+      {

+        CachedVerificationResultInjector.Inject(program, stablePrioritizedImpls);

+      }

+

       #region Verify each implementation

 

       var outputCollector = new OutputCollector(stablePrioritizedImpls);

@@ -995,9 +1019,7 @@ namespace Microsoft.Boogie
       {

         #region Verify the implementation

 

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

-        verificationResult.ImplementationName = impl.Name;

-        verificationResult.ImplementationToken = impl.tok;

+        verificationResult = new VerificationResult(requestId, impl.Checksum, impl.DependenciesChecksum, impl.Name, impl.tok, 1 < CommandLineOptions.Clo.VerifySnapshots ? program : null);

 

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

         {

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index 044d84fe..a0dba9d2 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -10,40 +10,204 @@ using VC;
 namespace Microsoft.Boogie

 {

 

+  class CachedVerificationResultInjector : StandardVisitor

+  {

+    readonly IEnumerable<Implementation> Implementations;

+    readonly Program Program;

+    Program programInCachedSnapshot;

+    Implementation currentImplementation;

+    int assumptionVariableCount;

+    int temporaryVariableCount;

+

+    int FreshAssumptionVariableName

+    {

+      get

+      {

+        return assumptionVariableCount++;

+      }

+    }

+

+    int FreshTemporaryVariableName

+    {

+      get

+      {

+        return temporaryVariableCount++;

+      }

+    }

+

+    protected CachedVerificationResultInjector(Program program, IEnumerable<Implementation> implementations)

+    {

+      Implementations = implementations;

+      Program = program;

+    }

+

+    public Implementation Inject(Implementation implementation, Program programInCachedSnapshot)

+    {

+      Contract.Requires(implementation != null && programInCachedSnapshot != null);

+

+      this.programInCachedSnapshot = programInCachedSnapshot;

+      assumptionVariableCount = 0;

+      temporaryVariableCount = 0;

+      currentImplementation = implementation;

+      var result = VisitImplementation(implementation);

+      currentImplementation = null;

+      this.programInCachedSnapshot = null;

+      return result;

+    }

+

+    public static void Inject(Program program, IEnumerable<Implementation> implementations)

+    {

+      var eai = new CachedVerificationResultInjector(program, implementations);

+

+      foreach (var impl in implementations)

+      {

+        if (ExecutionEngine.Cache.VerificationPriority(impl) == Priority.LOW)

+        {

+          var vr = ExecutionEngine.Cache.Lookup(impl.Id);

+          // TODO(wuestholz): We should probably increase the threshold to something like 2 seconds.

+          if (vr != null && 0.0 < vr.End.Subtract(vr.Start).TotalMilliseconds)

+          {

+            if (vr.Errors != null)

+            {

+              impl.ErrorsInCachedSnapshot = vr.Errors.ToList<object>();

+            }

+            else if (vr.Outcome == ConditionGeneration.Outcome.Correct)

+            {

+              impl.ErrorsInCachedSnapshot = new List<object>();

+            }

+            var p = vr.Program;

+            if (p != null)

+            {

+              eai.Inject(impl, p);

+            }

+          }

+        }

+      }

+    }

+

+    public override Cmd VisitCallCmd(CallCmd node)

+    {

+      var result = base.VisitCallCmd(node);

+

+      // TODO(wuestholz): Maybe we should speed up this lookup.

+      var oldProc = programInCachedSnapshot.TopLevelDeclarations.OfType<Procedure>().FirstOrDefault(p => p.Name == node.Proc.Name);

+      if (oldProc != null

+          && DependencyCollector.DependenciesChecksum(oldProc) != DependencyCollector.DependenciesChecksum(node.Proc)

+          && DependencyCollector.AllFunctionDependenciesAreDefinedAndUnchanged(oldProc, Program))

+      {

+        var lv = new LocalVariable(Token.NoToken,

+          new TypedIdent(Token.NoToken, string.Format("a##post##{0}", FreshAssumptionVariableName), Type.Bool),

+          new QKeyValue(Token.NoToken, "assumption", new List<object>(), null));

+        currentImplementation.InjectAssumptionVariable(lv);

+

+        var before = new List<Cmd>();

+        if (currentImplementation.NoErrorsInCachedSnapshot

+            && oldProc.Requires.Any())

+        {

+          var pre = node.Precondition(oldProc, Program);

+          var assume = new AssumeCmd(Token.NoToken, pre, new QKeyValue(Token.NoToken, "precondition_previous_snapshot", new List<object>(), null));

+          before.Add(assume);

+        }

+        else if (currentImplementation.AnyErrorsInCachedSnapshot)

+        {

+          // TODO(wuestholz): Add an assume statement if the precondition was verified in the previous snapshot.

+        }

+

+        var post = node.Postcondition(oldProc, Program);

+        var mods = node.UnmodifiedBefore(oldProc);

+        foreach (var m in mods)

+        {

+          var mPre = new LocalVariable(Token.NoToken,

+            new TypedIdent(Token.NoToken, string.Format("{0}##pre##{1}", m.Name, FreshTemporaryVariableName), m.Type));

+          before.Add(new AssignCmd(Token.NoToken,

+                       new List<AssignLhs> { new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, mPre)) },

+                       new List<Expr> { new IdentifierExpr(Token.NoToken, m.Decl) }));

+          var eq = LiteralExpr.Eq(new IdentifierExpr(Token.NoToken, mPre), new IdentifierExpr(Token.NoToken, m.Decl));

+          post = LiteralExpr.And(post, eq);

+        }

+        var lhs = new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, lv));

+        var rhs = LiteralExpr.And(new IdentifierExpr(Token.NoToken, lv), post);

+        var assumed = new AssignCmd(Token.NoToken, new List<AssignLhs> { lhs }, new List<Expr> { rhs });

+

+        node.ExtendDesugaring(before, new List<Cmd> { assumed });

+      }

+

+      return result;

+    }

+  }

+

+

   class DependencyCollector : ReadOnlyVisitor

   {

-    private HashSet<DeclWithFormals> dependencies;

+    private HashSet<Procedure> procedureDependencies;

+    private HashSet<Function> functionDependencies;

+    private bool allDependenciesHaveChecksum = true;

 

     public DependencyCollector()

     {

-      dependencies = new HashSet<DeclWithFormals>();

+      procedureDependencies = new HashSet<Procedure>();

+      functionDependencies = new HashSet<Function>();

     }

 

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

+    static bool Collect(Absy node, out ISet<Procedure> procedureDependencies, out ISet<Function> functionDependencies)

     {

       var dc = new DependencyCollector();

       dc.Visit(node);

-      dependencies = dc.dependencies.ToList();

+      procedureDependencies = dc.procedureDependencies;

+      functionDependencies = dc.functionDependencies;

+      return dc.allDependenciesHaveChecksum;

+    }

+

+    static bool Collect(Procedure proc, out ISet<Function> functionDependencies)

+    {

+      var dc = new DependencyCollector();

+      dc.Visit(proc);

+      functionDependencies = dc.functionDependencies;

+      return dc.allDependenciesHaveChecksum;

+    }

+

+    public static bool AllFunctionDependenciesAreDefinedAndUnchanged(Procedure oldProc, Program newProg)

+    {

+      Contract.Requires(oldProc != null && newProg != null);

+

+      ISet<Function> oldDeps;

+      if (!Collect(oldProc, out oldDeps))

+      {

+        return false;

+      }

+      // TODO(wuestholz): Maybe we should speed up this lookup.

+      var funcs = newProg.TopLevelDeclarations.OfType<Function>();

+      return oldDeps.All(dep => funcs.Any(f => f.Name == dep.Name && f.Checksum == dep.Checksum));

     }

 

-    public static string DependenciesChecksum(Implementation impl)

+    public static string DependenciesChecksum(DeclWithFormals decl)

     {

-      List<DeclWithFormals> deps;

-      DependencyCollector.Collect(impl, out deps);

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

+      if (decl.DependenciesChecksum != null)

+      {

+        return decl.DependenciesChecksum;

+      }

+

+      ISet<Procedure> procDeps;

+      ISet<Function> funcDeps;

+      if (!DependencyCollector.Collect(decl, out procDeps, out funcDeps))

       {

         return null;

       }

 

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

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

+      var procChecksums = procDeps.MapConcat(dep => dep.Checksum, "");

+      var funcChecksums = funcDeps.MapConcat(dep => dep.Checksum, "");

+      var data = Encoding.UTF8.GetBytes(procChecksums + funcChecksums);

       var hashedData = md5.ComputeHash(data);

-      return BitConverter.ToString(hashedData);

+      var result = BitConverter.ToString(hashedData);

+      decl.DependenciesChecksum = result;

+      return result;

     }

 

     public override Procedure VisitProcedure(Procedure node)

     {

-      dependencies.Add(node);

+      procedureDependencies.Add(node);

+      allDependenciesHaveChecksum &= node.Checksum != null;

 

       foreach (var param in node.InParams)

       {

@@ -58,7 +222,8 @@ namespace Microsoft.Boogie
 

     public override Function VisitFunction(Function node)

     {

-      dependencies.Add(node);

+      functionDependencies.Add(node);

+      allDependenciesHaveChecksum &= node.Checksum != null;

 

       if (node.DefinitionAxiom != null)

       {

@@ -70,7 +235,7 @@ namespace Microsoft.Boogie
 

     public override Cmd VisitCallCmd(CallCmd node)

     {

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

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

       if (!visited)

       {

         VisitProcedure(node.Proc);

@@ -84,7 +249,7 @@ namespace Microsoft.Boogie
       var funCall = node.Fun as FunctionCall;

       if (funCall != null)

       {

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

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

         if (!visited)

         {

           VisitFunction(funCall.Func);

@@ -96,6 +261,15 @@ namespace Microsoft.Boogie
   }

 

 

+  static internal class Priority

+  {

+    public static int LOW = 1;

+    public static int MEDIUM = 2;

+    public static int HIGH = 3;

+    public static int SKIP = int.MaxValue;

+  }

+

+

   public class VerificationResultCache

   {

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

@@ -152,7 +326,7 @@ namespace Microsoft.Boogie
 

     public bool NeedsToBeVerified(Implementation impl)

     {

-      return VerificationPriority(impl) < int.MaxValue;

+      return VerificationPriority(impl) < Priority.SKIP;

     }

 

 

@@ -160,19 +334,19 @@ namespace Microsoft.Boogie
     {

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

       {

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

+        return Priority.HIGH;  // 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)

+        return Priority.MEDIUM;  // 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)

+        return Priority.LOW;  // 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)

+        return Priority.SKIP;  // skip verification (highest priority to get them done as soon as possible)

       }

     }

   }

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 8fe4a5c6..afd2d3e6 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -576,6 +576,8 @@ namespace VC {
 

     private bool _disposed;

 

+    protected Implementation currentImplementation;

+

     protected List<Variable> CurrentLocalVariables = null;

 

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

@@ -1309,7 +1311,9 @@ namespace VC {
       Contract.Requires(impl != null);

       Contract.Requires(mvInfo != null);

 

+      currentImplementation = impl;

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

+      currentImplementation = null;

 

       RestoreParamWhereClauses(impl);

 

@@ -1448,6 +1452,28 @@ namespace VC {
           ((AssertCmd)pc).OrigExpr = pc.Expr;

           Contract.Assert(((AssertCmd)pc).IncarnationMap == null);

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

+

+          if (currentImplementation != null

+              && currentImplementation.NoErrorsInCachedSnapshot

+              && currentImplementation.InjectedAssumptionVariables != null

+              && 2 <= currentImplementation.InjectedAssumptionVariables.Count)

+          {

+            // TODO(wuestholz): Maybe store the assertion expression in a local variable.

+            var expr = LiteralExpr.Imp(currentImplementation.ConjunctionOfInjectedAssumptionVariables(), copy);

+            passiveCmds.Add(new AssumeCmd(Token.NoToken, expr));

+          }

+          else if (currentImplementation != null

+                   && currentImplementation.AnyErrorsInCachedSnapshot)

+          {

+            // TODO(wuestholz): Add an assume statement if the assertion was verified in the previous snapshot.

+          }

+        }

+        else if (pc is AssumeCmd

+                 && QKeyValue.FindStringAttribute(pc.Attributes, "precondition_previous_snapshot") != null

+                 && currentImplementation.InjectedAssumptionVariables != null

+                 && currentImplementation.InjectedAssumptionVariables.Any())

+        {

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

         }

         pc.Expr = copy;

         passiveCmds.Add(pc);

@@ -1521,6 +1547,19 @@ namespace VC {
           }

           passiveCmds.Add(new AssumeCmd(c.tok, assumption));

         }

+

+        if (currentImplementation != null

+            && currentImplementation.NoErrorsInCachedSnapshot

+            && currentImplementation.InjectedAssumptionVariables != null

+            && currentImplementation.InjectedAssumptionVariables.Count == 1

+            && assign.Lhss.Count == 1)

+        {

+          var identExpr = assign.Lhss[0].AsExpr as IdentifierExpr;

+          if (identExpr != null && identExpr.Decl != null && QKeyValue.FindBoolAttribute(identExpr.Decl.Attributes, "assumption"))

+          {

+            passiveCmds.Add(new AssumeCmd(c.tok, new IdentifierExpr(Token.NoToken, currentImplementation.InjectedAssumptionVariables.First())));

+          }

+        }

       }

       #endregion

       #region havoc w |--> assume whereClauses, out := in( w |-> w' )

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

+  requires 0 < n;

+

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

+{

+    var x: int;

+

+    call x := N(n);

+

+    call O();

+

+    assert 0 <= x;

+}

+

+procedure {:checksum "2"} N(n: int) returns (r: int);

+  requires 0 < n;

+  ensures 0 < r;

+

+procedure {:checksum "3"} O();

+  ensures true;

diff --git a/Test/snapshots/Snapshots10.v1.bpl b/Test/snapshots/Snapshots10.v1.bpl
new file mode 100644
index 00000000..d4c09a5f
--- /dev/null
+++ b/Test/snapshots/Snapshots10.v1.bpl
@@ -0,0 +1,21 @@
+procedure {:checksum "0"} M(n: int);

+  requires 0 < n;

+

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

+{

+    var x: int;

+

+    call x := N(n);

+

+    call O();

+

+    assert 0 <= x;

+}

+

+procedure {:checksum "4"} N(n: int) returns (r: int);

+  requires 0 < n;

+  // Change: stronger postcondition

+  ensures 42 < r;

+

+procedure {:checksum "3"} O();

+  ensures true;

diff --git a/Test/snapshots/Snapshots11.v0.bpl b/Test/snapshots/Snapshots11.v0.bpl
new file mode 100644
index 00000000..10b4ed43
--- /dev/null
+++ b/Test/snapshots/Snapshots11.v0.bpl
@@ -0,0 +1,14 @@
+procedure {:checksum "0"} M(n: int);

+

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

+{

+    var x: int;

+

+    call x := N(n);

+

+    assert 0 <= x;

+}

+

+procedure {:checksum "2"} N(n: int) returns (r: int);

+  requires 0 < n;

+  ensures 0 < r;

diff --git a/Test/snapshots/Snapshots11.v1.bpl b/Test/snapshots/Snapshots11.v1.bpl
new file mode 100644
index 00000000..3c3ea476
--- /dev/null
+++ b/Test/snapshots/Snapshots11.v1.bpl
@@ -0,0 +1,15 @@
+procedure {:checksum "0"} M(n: int);

+

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

+{

+    var x: int;

+

+    call x := N(n);

+

+    assert 0 <= x;

+}

+

+procedure {:checksum "3"} N(n: int) returns (r: int);

+  requires 0 < n;

+  // Change: weaker postcondition

+  ensures 0 <= r;

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

+

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

+{

+    call N();

+

+    assert false;

+}

+

+procedure {:checksum "2"} N();

+  ensures F();

+

+function {:checksum "3"} F() : bool

+{

+    false

+}

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

+

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

+{

+    call N();

+

+    assert false;

+}

+

+procedure {:checksum "2"} N();

+  ensures F();

+

+function {:checksum "4"} F() : bool

+{

+    true

+}

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

+

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

+{

+    call N();

+

+    assert false;

+}

+

+procedure {:checksum "2"} N();

+  ensures F() && G();

+

+function {:checksum "3"} F() : bool

+{

+    true

+}

+

+function {:checksum "4"} G() : bool

+{

+    false

+}

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

+

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

+{

+    call N();

+

+    assert false;

+}

+

+procedure {:checksum "2"} N();

+  ensures F();

+

+function {:checksum "3"} F() : bool

+{

+    true

+}

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

+

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

+{

+    call N();

+

+    assert false;

+}

+

+procedure {:checksum "2"} N();

+  ensures F() && G();

+

+function {:checksum "3"} F() : bool

+{

+    true

+}

+

+function {:checksum "4"} G() : bool

+{

+    false

+}

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

+

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

+{

+    call N();

+

+    assert false;

+}

+

+procedure {:checksum "2"} N();

+  ensures F();

+

+function {:checksum "3"} F() : bool

+{

+    true

+}

+

+function {:checksum "4"} G() : bool

+{

+    false

+}

diff --git a/Test/snapshots/Snapshots9.v0.bpl b/Test/snapshots/Snapshots9.v0.bpl
index 73dcd9aa..5b2cf68c 100644
--- a/Test/snapshots/Snapshots9.v0.bpl
+++ b/Test/snapshots/Snapshots9.v0.bpl
@@ -12,4 +12,6 @@ implementation {:id "M"} {:checksum "1"} M(n: int)
 

 procedure {:checksum "2"} N(n: int) returns (r: int);

   requires 0 < n;

+  requires true;

   ensures 0 < r;

+  ensures true;

diff --git a/Test/snapshots/runtest.snapshot b/Test/snapshots/runtest.snapshot
index 6646d9ea..d61e9e4a 100644
--- a/Test/snapshots/runtest.snapshot
+++ b/Test/snapshots/runtest.snapshot
@@ -1,2 +1,2 @@
-// RUN: %boogie -verifySnapshots:1 -verifySeparately Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl Snapshots8.bpl Snapshots9.bpl > "%t"
+// RUN: %boogie -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 > "%t"
 // RUN: %diff "%s.expect" "%t"
diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect
index c0a171c4..a370cbae 100644
--- a/Test/snapshots/runtest.snapshot.expect
+++ b/Test/snapshots/runtest.snapshot.expect
@@ -98,3 +98,40 @@ Boogie program verifier finished with 1 verified, 0 errors
 Boogie program verifier finished with 1 verified, 0 errors

 

 Boogie program verifier finished with 1 verified, 0 errors

+

+Boogie program verifier finished with 1 verified, 0 errors

+

+Boogie program verifier finished with 1 verified, 0 errors

+Snapshots11.v0.bpl(7,5): Error BP5002: A precondition for this call might not hold.

+Snapshots11.v0.bpl(13,3): Related location: This is the precondition that might not hold.

+Execution trace:

+    Snapshots11.v0.bpl(7,5): anon0

+

+Boogie program verifier finished with 0 verified, 1 error

+Snapshots11.v1.bpl(7,5): Error BP5002: A precondition for this call might not hold.

+Snapshots11.v1.bpl(13,3): Related location: This is the precondition that might not hold.

+Execution trace:

+    Snapshots11.v1.bpl(7,5): anon0

+

+Boogie program verifier finished with 0 verified, 1 error

+

+Boogie program verifier finished with 1 verified, 0 errors

+Snapshots12.v1.bpl(7,5): Error BP5001: This assertion might not hold.

+Execution trace:

+    Snapshots12.v1.bpl(5,5): anon0

+

+Boogie program verifier finished with 0 verified, 1 error

+

+Boogie program verifier finished with 1 verified, 0 errors

+Snapshots13.v1.bpl(7,5): Error BP5001: This assertion might not hold.

+Execution trace:

+    Snapshots13.v1.bpl(5,5): anon0

+

+Boogie program verifier finished with 0 verified, 1 error

+

+Boogie program verifier finished with 1 verified, 0 errors

+Snapshots14.v1.bpl(7,5): Error BP5001: This assertion might not hold.

+Execution trace:

+    Snapshots14.v1.bpl(5,5): anon0

+

+Boogie program verifier finished with 0 verified, 1 error