Changed the verification result cache to use the built-in 'MemoryCache' class.

3 files changed, 51 insertions, 52 deletions

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index cac56c4b..2b122f8f 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -1001,12 +1001,13 @@ namespace Microsoft.Boogie
       printer.Inform("", output);  // newline

       printer.Inform(string.Format("Verifying {0} ...", impl.Name), output);

 

+      int priority = 0;

       if (0 < CommandLineOptions.Clo.VerifySnapshots)

       {

-        verificationResult = Cache.Lookup(impl);

+        verificationResult = Cache.Lookup(impl, out priority);

       }

 

-      if (verificationResult != null)

+      if (verificationResult != null && priority == Priority.SKIP)

       {

         if (CommandLineOptions.Clo.XmlSink != null)

         {

@@ -1096,7 +1097,7 @@ namespace Microsoft.Boogie
 

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

         {

-          Cache.Insert(impl.Id, verificationResult);

+          Cache.Insert(impl, verificationResult);

         }

 

         #endregion

diff --git a/Source/ExecutionEngine/ExecutionEngine.csproj b/Source/ExecutionEngine/ExecutionEngine.csproj
index 5b854a40..84aa64d5 100644
--- a/Source/ExecutionEngine/ExecutionEngine.csproj
+++ b/Source/ExecutionEngine/ExecutionEngine.csproj
@@ -1,4 +1,4 @@
-<?xml version="1.0" encoding="utf-8"?>

+<?xml version="1.0" encoding="utf-8"?>

 <Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">

   <Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" />

   <PropertyGroup>

@@ -11,7 +11,7 @@
     <AssemblyName>ExecutionEngine</AssemblyName>

     <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>

     <FileAlignment>512</FileAlignment>

-    <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'" >Client</TargetFrameworkProfile>

+    <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'"></TargetFrameworkProfile>

     <SignAssembly>true</SignAssembly>

     <AssemblyOriginatorKeyFile>..\InterimKey.snk</AssemblyOriginatorKeyFile>

     <ProductVersion>12.0.0</ProductVersion>

@@ -81,6 +81,7 @@
   <ItemGroup>

     <Reference Include="System" />

     <Reference Include="System.Core" />

+    <Reference Include="System.Runtime.Caching" />

     <Reference Include="System.Xml.Linq" />

   </ItemGroup>

   <ItemGroup>

@@ -146,4 +147,4 @@
   <Target Name="AfterBuild">

   </Target>

   -->

-</Project>
\ No newline at end of file
+</Project>

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index 8578f144..6833f869 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -3,6 +3,7 @@ using System.Collections.Concurrent;
 using System.Collections.Generic;

 using System.Diagnostics.Contracts;

 using System.Linq;

+using System.Runtime.Caching;

 using System.Text;

 using System.Text.RegularExpressions;

 using VC;

@@ -61,11 +62,12 @@ namespace Microsoft.Boogie
 

       foreach (var impl in implementations)

       {

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

+        int priority;

+        var vr = ExecutionEngine.Cache.Lookup(impl, out priority);

+        if (vr != null && priority == 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 (0.0 < vr.End.Subtract(vr.Start).TotalMilliseconds)

           {

             if (vr.Errors != null)

             {

@@ -275,91 +277,86 @@ 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 static readonly int LOW = 1;

+    public static readonly int MEDIUM = 2;

+    public static readonly int HIGH = 3;

+    public static readonly int SKIP = int.MaxValue;

   }

 

 

   public class VerificationResultCache

   {

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

+    private readonly MemoryCache Cache = new MemoryCache("VerificationResultCache");

+    private readonly CacheItemPolicy Policy = new CacheItemPolicy();

 

 

-    public void Insert(string key, VerificationResult result)

+    public VerificationResultCache()

     {

-      Contract.Requires(key != null);

-      Contract.Requires(result != null);

-

-      Cache[key] = result;

+      Policy.SlidingExpiration = new TimeSpan(0, 5, 0);

     }

 

 

-    public VerificationResult Lookup(string key)

+    public void Insert(Implementation impl, VerificationResult result)

     {

-      VerificationResult result;

-      var success = Cache.TryGetValue(key, out result);

-      return success ? result : null;

+      Contract.Requires(impl != null);

+      Contract.Requires(result != null);

+

+      Cache.Set(impl.Id, result, Policy);

     }

 

 

-    public VerificationResult Lookup(Implementation impl)

+    public VerificationResult Lookup(Implementation impl, out int priority)

     {

-      if (!NeedsToBeVerified(impl))

+      Contract.Requires(impl != null);

+

+      var result = Cache.Get(impl.Id) as VerificationResult;

+      if (result == null)

+      {

+        priority = Priority.HIGH;  // high priority (has been never verified before)

+      }

+      else if (result.Checksum != impl.Checksum)

       {

-        return Lookup(impl.Id);

+        priority = Priority.MEDIUM;  // medium priority (old snapshot has been verified before)

+      }

+      else if (impl.DependenciesChecksum == null || result.DependeciesChecksum != impl.DependenciesChecksum)

+      {

+        priority = Priority.LOW;  // low priority (the same snapshot has been verified before, but a callee has changed)

       }

       else

       {

-        return null;

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

       }

+      return result;

     }

 

 

     public void Clear()

     {

-      Cache.Clear();

+      Cache.Trim(100);

     }

 

 

     public void RemoveMatchingKeys(Regex keyRegexp)

     {

+      Contract.Requires(keyRegexp != null);

+

       foreach (var kv in Cache)

       {

         if (keyRegexp.IsMatch(kv.Key))

         {

-          VerificationResult res;

-          Cache.TryRemove(kv.Key, out res);

+          Cache.Remove(kv.Key);

         }

       }

     }

 

 

-    public bool NeedsToBeVerified(Implementation impl)

-    {

-      return VerificationPriority(impl) < Priority.SKIP;

-    }

-

-

     public int VerificationPriority(Implementation impl)

     {

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

-      {

-        return Priority.HIGH;  // high priority (has been never verified before)

-      }

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

-      {

-        return Priority.MEDIUM;  // medium priority (old snapshot has been verified before)

-      }

-      else if (impl.DependenciesChecksum == null || Cache[impl.Id].DependeciesChecksum != impl.DependenciesChecksum)

-      {

-        return Priority.LOW;  // low priority (the same snapshot has been verified before, but a callee has changed)

-      }

-      else

-      {

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

-      }

+      Contract.Requires(impl != null);

+

+      int priority;

+      Lookup(impl, out priority);

+      return priority;

     }

   }