13 files changed, 261 insertions, 11 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 55b37f13..fd62f334 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -1794,6 +1794,14 @@ namespace Microsoft.Boogie {
       this.OutParams = that.OutParams;
     }
 
+    public string Checksum
+    {
+      get
+      {
+        return FindStringAttribute("checksum");
+      }
+    }
+
     protected void EmitSignature(TokenTextWriter stream, bool shortRet) {
       Contract.Requires(stream != null);
       Type.EmitOptionalTypeParams(stream, TypeParameters);
@@ -2567,14 +2575,6 @@ namespace Microsoft.Boogie {
       }
     }
 
-    public string Checksum
-    {
-      get
-      {
-        return FindStringAttribute("checksum");
-      }
-    }
-
     public string Id
     {
       get
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index e87ea790..3c10116f 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -795,6 +795,11 @@ namespace Microsoft.Boogie
         }
 
         VCGen.Outcome outcome;
+        string depsChecksum = null;
+        if (CommandLineOptions.Clo.VerifySnapshots)
+        {
+          depsChecksum = DependenciesChecksum(impl);
+        }
         try
         {
           if (CommandLineOptions.Clo.inferLeastForUnsat != null)
@@ -819,7 +824,7 @@ namespace Microsoft.Boogie
           }
           else
           {
-            if (!VerificationResultCache.ContainsKey(impl.Id) || VerificationResultCache[impl.Id].Checksum != impl.Checksum)
+            if (!CommandLineOptions.Clo.VerifySnapshots || NeedsToBeVerified(impl))
             {
               outcome = vcgen.VerifyImplementation(impl, out errors);
             }
@@ -871,7 +876,7 @@ namespace Microsoft.Boogie
 
         if (CommandLineOptions.Clo.VerifySnapshots && !string.IsNullOrEmpty(impl.Checksum))
         {
-          var result = new VerificationResult(impl.Checksum, outcome, errors);
+          var result = new VerificationResult(impl.Checksum, depsChecksum, outcome, errors);
           VerificationResultCache[impl.Id] = result;
         }
 
@@ -1123,16 +1128,67 @@ namespace Microsoft.Boogie
 
     #region Verification result caching
 
+    class DependencyCollector : StandardVisitor
+    {
+      public HashSet<DeclWithFormals> dependencies;
+
+      public DependencyCollector()
+      {
+        dependencies = new HashSet<DeclWithFormals>();
+      }
+
+      public static void Collect(Absy node, out List<DeclWithFormals> dependencies)
+      {
+        var dc = new DependencyCollector();
+        dc.Visit(node);
+        dependencies = dc.dependencies.ToList();
+      }
+
+      public override Procedure VisitProcedure(Procedure node)
+      {
+        var result = base.VisitProcedure(node);
+
+        dependencies.Add(node);
+
+        return result;
+      }
+
+      public override Cmd VisitCallCmd(CallCmd node)
+      {
+        var result = base.VisitCallCmd(node);
+
+        dependencies.Add(node.Proc);
+
+        return result;
+      }
+
+      public override Expr VisitNAryExpr(NAryExpr node)
+      {
+        var result = base.VisitNAryExpr(node);
+
+        var funCall = node.Fun as FunctionCall;
+        if (funCall != null)
+        {
+          dependencies.Add(funCall.Func);
+        }
+
+        return result;
+      }
+    }
+
+
     private struct VerificationResult
     {
-      internal VerificationResult(string checksum, ConditionGeneration.Outcome outcome, List<Counterexample> errors)
+      internal VerificationResult(string checksum, string depsChecksum, ConditionGeneration.Outcome outcome, List<Counterexample> errors)
       {
         Checksum = checksum;
+        DependeciesChecksum = depsChecksum;
         Outcome = outcome;
         Errors = errors;
       }
 
       public readonly string Checksum;
+      public readonly string DependeciesChecksum;
       public readonly ConditionGeneration.Outcome Outcome;
       public readonly List<Counterexample> Errors;
     }
@@ -1140,6 +1196,37 @@ namespace Microsoft.Boogie
 
     private static readonly ConcurrentDictionary<string, VerificationResult> VerificationResultCache = new ConcurrentDictionary<string, VerificationResult>();
 
+
+    public static void EmptyCache()
+    {
+      VerificationResultCache.Clear();
+    }
+
+
+    private static string DependenciesChecksum(Implementation impl)
+    {
+      List<DeclWithFormals> deps;
+      DependencyCollector.Collect(impl, out deps);
+      if (deps.Any(dep => dep.Checksum == null))
+      {
+        return null;
+      }
+
+      return string.Join("", deps.Select(dep => dep.Checksum));
+    }
+
+    private static bool NeedsToBeVerified(Implementation impl)
+    {
+      if (!VerificationResultCache.ContainsKey(impl.Id)
+          || VerificationResultCache[impl.Id].Checksum != impl.Checksum)
+      {
+        return true;
+      }
+
+      var depsChecksum = DependenciesChecksum(impl);
+      return depsChecksum == null || VerificationResultCache[impl.Id].DependeciesChecksum != depsChecksum;
+    }
+
     #endregion
   }
 
diff --git a/Test/snapshots/Answer b/Test/snapshots/Answer
index 434cdfda..a7a6b0be 100644
--- a/Test/snapshots/Answer
+++ b/Test/snapshots/Answer
@@ -1,3 +1,4 @@
+-------------------- Snapshots0.bpl --------------------
 Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.
 Execution trace:
     Snapshots0.v0.bpl(41,5): anon0
@@ -25,3 +26,35 @@ Execution trace:
     Snapshots0.v0.bpl(41,5): anon0
 
 Boogie program verifier finished with 2 verified, 1 error
+
+-------------------- Snapshots1.bpl --------------------
+Snapshots1.v0.bpl(13,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    Snapshots1.v0.bpl(13,5): anon0
+
+Boogie program verifier finished with 1 verified, 1 error
+Snapshots1.v1.bpl(13,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    Snapshots1.v1.bpl(13,5): anon0
+
+Boogie program verifier finished with 1 verified, 1 error
+Snapshots1.v2.bpl(5,5): Error BP5002: A precondition for this call might not hold.
+Snapshots1.v2.bpl(10,3): Related location: This is the precondition that might not hold.
+Execution trace:
+    Snapshots1.v2.bpl(5,5): anon0
+
+Boogie program verifier finished with 1 verified, 1 error
+
+-------------------- Snapshots2.bpl --------------------
+
+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
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/snapshots/Snapshots1.v0.bpl b/Test/snapshots/Snapshots1.v0.bpl
new file mode 100644
index 00000000..d6d4332e
--- /dev/null
+++ b/Test/snapshots/Snapshots1.v0.bpl
@@ -0,0 +1,14 @@
+procedure {:checksum "P1$proc#0"} P1();
+// Action: verify
+implementation {:checksum "P1$impl#0"} P1()
+{
+    call P2();
+}
+
+
+procedure {:checksum "P2$proc#0"} P2();
+// Action: verify
+implementation {:checksum "P2$impl#0"} P2()
+{
+    assert 1 != 1;
+}
diff --git a/Test/snapshots/Snapshots1.v1.bpl b/Test/snapshots/Snapshots1.v1.bpl
new file mode 100644
index 00000000..c0014a03
--- /dev/null
+++ b/Test/snapshots/Snapshots1.v1.bpl
@@ -0,0 +1,14 @@
+procedure {:checksum "P1$proc#0"} P1();
+// Action: skip
+implementation {:checksum "P1$impl#0"} P1()
+{
+    call P2();
+}
+
+
+procedure {:checksum "P2$proc#0"} P2();
+// Action: verify
+implementation {:checksum "P2$impl#1"} P2()
+{
+    assert 2 != 2;
+}
diff --git a/Test/snapshots/Snapshots1.v2.bpl b/Test/snapshots/Snapshots1.v2.bpl
new file mode 100644
index 00000000..49e8b389
--- /dev/null
+++ b/Test/snapshots/Snapshots1.v2.bpl
@@ -0,0 +1,15 @@
+procedure {:checksum "P1$proc#0"} P1();
+// Action: verify
+implementation {:checksum "P1$impl#0"} P1()
+{
+    call P2();
+}
+
+
+procedure {:checksum "P2$proc#1"} P2();
+  requires false;
+// Action: verify
+implementation {:checksum "P2$impl#1"} P2()
+{
+    assert 2 != 2;
+}
diff --git a/Test/snapshots/Snapshots2.v0.bpl b/Test/snapshots/Snapshots2.v0.bpl
new file mode 100644
index 00000000..63f1995d
--- /dev/null
+++ b/Test/snapshots/Snapshots2.v0.bpl
@@ -0,0 +1,12 @@
+procedure {:checksum "P0$proc#0"} P0();
+// Action: verify
+implementation {:checksum "P0$impl#0"} P0()
+{
+    call P0();
+}
+
+
+function F0() : bool
+{
+    true
+}
diff --git a/Test/snapshots/Snapshots2.v1.bpl b/Test/snapshots/Snapshots2.v1.bpl
new file mode 100644
index 00000000..a00bdecb
--- /dev/null
+++ b/Test/snapshots/Snapshots2.v1.bpl
@@ -0,0 +1,12 @@
+procedure {:checksum "P0$proc#0"} P0();
+// Action: skip
+implementation {:checksum "P0$impl#0"} P0()
+{
+    call P0();
+}
+
+
+function F0() : bool
+{
+    true
+}
diff --git a/Test/snapshots/Snapshots2.v2.bpl b/Test/snapshots/Snapshots2.v2.bpl
new file mode 100644
index 00000000..02c5e6df
--- /dev/null
+++ b/Test/snapshots/Snapshots2.v2.bpl
@@ -0,0 +1,13 @@
+procedure {:checksum "P0$proc#2"} P0();
+requires F0();
+// Action: verify (procedure changed)
+implementation {:checksum "P0$impl#0"} P0()
+{
+    call P0();
+}
+
+
+function {:checksum "F0#0"} F0() : bool
+{
+    true
+}
diff --git a/Test/snapshots/Snapshots2.v3.bpl b/Test/snapshots/Snapshots2.v3.bpl
new file mode 100644
index 00000000..5bf59435
--- /dev/null
+++ b/Test/snapshots/Snapshots2.v3.bpl
@@ -0,0 +1,13 @@
+procedure {:checksum "P0$proc#2"} P0();
+requires F0();
+// Action: verify (function changed)
+implementation {:checksum "P0$impl#0"} P0()
+{
+    call P0();
+}
+
+
+function {:checksum "F0#1"} F0() : bool
+{
+    false
+}
diff --git a/Test/snapshots/Snapshots2.v4.bpl b/Test/snapshots/Snapshots2.v4.bpl
new file mode 100644
index 00000000..3d11ee27
--- /dev/null
+++ b/Test/snapshots/Snapshots2.v4.bpl
@@ -0,0 +1,13 @@
+procedure {:checksum "P0$proc#2"} P0();
+requires F0();
+// Action: skip
+implementation {:checksum "P0$impl#0"} P0()
+{
+    call P0();
+}
+
+
+function {:checksum "F0#1"} F0() : bool
+{
+    false
+}
diff --git a/Test/snapshots/Snapshots2.v5.bpl b/Test/snapshots/Snapshots2.v5.bpl
new file mode 100644
index 00000000..5ff7bb4d
--- /dev/null
+++ b/Test/snapshots/Snapshots2.v5.bpl
@@ -0,0 +1,14 @@
+procedure {:checksum "P0$proc#5"} P0();
+requires F0();
+ensures F0();
+// Action: verify (procedure changed)
+implementation {:checksum "P0$impl#0"} P0()
+{
+    call P0();
+}
+
+
+function {:checksum "F0#1"} F0() : bool
+{
+    false
+}
diff --git a/Test/snapshots/runtest.bat b/Test/snapshots/runtest.bat
index 05421b85..fa45d56a 100644
--- a/Test/snapshots/runtest.bat
+++ b/Test/snapshots/runtest.bat
@@ -1,7 +1,17 @@
+
 @echo off
 setlocal
 
 set BOOGIEDIR=..\..\Binaries
 set BGEXE=%BOOGIEDIR%\Boogie.exe
 
+echo -------------------- Snapshots0.bpl --------------------
 %BGEXE% %* /verifySnapshots Snapshots0.bpl
+
+echo.
+echo -------------------- Snapshots1.bpl --------------------
+%BGEXE% %* /verifySnapshots Snapshots1.bpl
+
+echo.
+echo -------------------- Snapshots2.bpl --------------------
+%BGEXE% %* /verifySnapshots Snapshots2.bpl