Worked on improving program snapshot verification.

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