Worked on improving program snapshot verification (automatic prioritization).

4 files changed, 117 insertions, 22 deletions

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index d5b449d0..c7e8f0cc 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -684,14 +684,22 @@ namespace Microsoft.Boogie
 

       #region Select and prioritize implementations that should be verified

 

-      var prioritizedImpls =

-        from impl in program.TopLevelDeclarations.OfType<Implementation>()

-        where impl != null && CommandLineOptions.Clo.UserWantsToCheckRoutine(cce.NonNull(impl.Name)) && !impl.SkipVerification

-        orderby impl.Priority descending

-        select impl;

+      var impls = program.TopLevelDeclarations.OfType<Implementation>().Where(

+        impl => impl != null && CommandLineOptions.Clo.UserWantsToCheckRoutine(cce.NonNull(impl.Name)) && !impl.SkipVerification);

 

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

-      var stablePrioritizedImpls = prioritizedImpls.ToArray();

+      Implementation[] stablePrioritizedImpls = null;

+      IDictionary<Implementation, string> depsChecksums = null;

+      if (CommandLineOptions.Clo.VerifySnapshots)

+      {

+        depsChecksums = impls.ToDictionary(impl => impl, impl => DependencyCollector.DependenciesChecksum(impl));

+        stablePrioritizedImpls = impls.OrderByDescending(

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

+      }

+      else

+      {

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

+      }

 

       #endregion

 

@@ -716,16 +724,6 @@ namespace Microsoft.Boogie
 

         #endregion

 

-        #region Record the checksum of the dependencies of this implementation

-

-        string depsChecksum = null;

-        if (CommandLineOptions.Clo.VerifySnapshots)

-        {

-          depsChecksum = DependencyCollector.DependenciesChecksum(impl);

-        }

-

-        #endregion

-

         #region Verify the implementation

 

         try

@@ -747,7 +745,7 @@ namespace Microsoft.Boogie
           }

           else

           {

-            if (!CommandLineOptions.Clo.VerifySnapshots || Cache.NeedsToBeVerified(impl, depsChecksum))

+            if (!CommandLineOptions.Clo.VerifySnapshots || Cache.NeedsToBeVerified(impl, depsChecksums[impl]))

             {

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

 

@@ -793,7 +791,7 @@ namespace Microsoft.Boogie
 

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

         {

-          Cache.Insert(impl.Id, new VerificationResult(requestId, impl.Checksum, depsChecksum, outcome, errors));

+          Cache.Insert(impl.Id, new VerificationResult(requestId, impl.Checksum, depsChecksums[impl], outcome, errors));

         }

 

         #endregion

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index 924d11bc..798411c8 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -153,12 +153,28 @@ namespace Microsoft.Boogie
 

     public bool NeedsToBeVerified(Implementation impl, string depsChecksumOfImpl)

     {

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

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

+      return 0 < VerificationPriority(impl, depsChecksumOfImpl);

+    }

+

+

+    public int VerificationPriority(Implementation impl, string depsChecksumOfImpl)

+    {

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

+      {

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

+      }

+      else if (Cache[impl.Id].Checksum != impl.Checksum)

+      {

+        return 2;  // medium priority (old snapshot has been verified before)

+      }

+      else if (depsChecksumOfImpl == null || Cache[impl.Id].DependeciesChecksum != depsChecksumOfImpl)

+      {

+        return 1;  // low priority (the same snapshot has been verified before, but a callee has changed)

+      }

+      else

       {

-        return true;

+        return 0;  // skip verification

       }

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

     }

 

   }

diff --git a/Test/snapshots/Snapshots4.v0.bpl b/Test/snapshots/Snapshots4.v0.bpl
new file mode 100644
index 00000000..430aee99
--- /dev/null
+++ b/Test/snapshots/Snapshots4.v0.bpl
@@ -0,0 +1,36 @@
+procedure {:checksum "P0$proc#0"} P0();

+// Action: verify

+implementation {:checksum "P0$impl#0"} P0()

+{

+}

+

+

+procedure {:checksum "P1$proc#0"} P1();

+// Action: verify

+implementation {:checksum "P1$impl#0"} P1()

+{

+    call P2();

+}

+

+

+procedure {:checksum "P2$proc#0"} P2();

+  ensures G();

+

+

+procedure {:checksum "P3$proc#0"} P3();

+// Action: verify

+implementation {:checksum "P3$impl#0"} P3()

+{

+}

+

+

+function {:checksum "G#0"} G() : bool

+{

+    F()

+}

+

+

+function {:checksum "F#0"} F() : bool

+{

+    true

+}

diff --git a/Test/snapshots/Snapshots4.v1.bpl b/Test/snapshots/Snapshots4.v1.bpl
new file mode 100644
index 00000000..025a3f5f
--- /dev/null
+++ b/Test/snapshots/Snapshots4.v1.bpl
@@ -0,0 +1,45 @@
+procedure {:checksum "P0$proc#0"} P0();

+// Action: skip

+// Priority: 0

+implementation {:checksum "P0$impl#0"} P0()

+{

+}

+

+

+procedure {:checksum "P1$proc#0"} P1();

+// Action: verify

+// Priority: 1

+implementation {:checksum "P1$impl#0"} P1()

+{

+    call P2();

+}

+

+

+procedure {:checksum "P3$proc#0"} P3();

+// Action: verify

+// Priority: 2

+implementation {:checksum "P3$impl#1"} P3()

+{

+    assert false;

+}

+

+

+procedure {:checksum "P2$proc#0"} P2();

+  ensures G();

+// Action: verify

+// Priority: 3

+implementation {:checksum "P2$impl#0"} P2()

+{

+}

+

+

+function {:checksum "G#0"} G() : bool

+{

+    F()

+}

+

+

+function {:checksum "F#1"} F() : bool

+{

+    false

+}