Worked on improving program snapshot verification.

3 files changed, 173 insertions, 140 deletions

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 6c823870..110480b9 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -242,6 +242,8 @@ namespace Microsoft.Boogie
 

     public static ErrorInformationFactory errorInformationFactory = new ErrorInformationFactory();

 

+    public readonly static VerificationResultCache Cache = new VerificationResultCache();

+

     static LinearTypechecker linearTypechecker;

 

 

@@ -768,7 +770,7 @@ namespace Microsoft.Boogie
         string depsChecksum = null;

         if (CommandLineOptions.Clo.VerifySnapshots)

         {

-          depsChecksum = DependenciesChecksum(impl);

+          depsChecksum = DependencyCollector.DependenciesChecksum(impl);

         }

         try

         {

@@ -794,7 +796,7 @@ namespace Microsoft.Boogie
           }

           else

           {

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

+            if (!CommandLineOptions.Clo.VerifySnapshots || Cache.NeedsToBeVerified(impl))

             {

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

             }

@@ -804,7 +806,8 @@ namespace Microsoft.Boogie
               {

                 Console.WriteLine("Retrieving cached verification result for implementation {0}...", impl.Name);

               }

-              var result = VerificationResultCache[impl.Id];

+              var result = Cache.Lookup(impl.Id);

+              Contract.Assert(result != null);

               outcome = result.Outcome;

               errors = result.Errors;

             }

@@ -847,7 +850,7 @@ namespace Microsoft.Boogie
         if (CommandLineOptions.Clo.VerifySnapshots && !string.IsNullOrEmpty(impl.Checksum))

         {

           var result = new VerificationResult(requestId, impl.Checksum, depsChecksum, outcome, errors);

-          VerificationResultCache[impl.Id] = result;

+          Cache.Insert(impl.Id, result);

         }

 

         ProcessOutcome(outcome, errors, timeIndication, ref errorCount, ref verified, ref inconclusives, ref timeOuts, ref outOfMemories, er, impl, requestId);

@@ -865,7 +868,6 @@ namespace Microsoft.Boogie
       vcgen.Close();

       cce.NonNull(CommandLineOptions.Clo.TheProverFactory).Close();

 

-

       #endregion

 

       return PipelineOutcome.VerificationCompleted;

@@ -1091,141 +1093,6 @@ 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)

-      {

-        dependencies.Add(node);

-

-        return base.VisitProcedure(node);

-      }

-

-      public override Function VisitFunction(Function node)

-      {

-        dependencies.Add(node);

-

-        return base.VisitFunction(node);

-      }

-

-      public override Cmd VisitCallCmd(CallCmd node)

-      {

-        var result = base.VisitCallCmd(node);

-

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

-        if (!visited)

-        {

-          VisitProcedure(node.Proc);

-        }

-

-        return result;

-      }

-

-      public override Expr VisitNAryExpr(NAryExpr node)

-      {

-        var result = base.VisitNAryExpr(node);

-

-        var funCall = node.Fun as FunctionCall;

-        if (funCall != null)

-        {

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

-          if (!visited)

-          {

-            VisitFunction(funCall.Func);

-            if (funCall.Func.DefinitionAxiom != null)

-            {

-              VisitAxiom(funCall.Func.DefinitionAxiom);

-            }

-          }

-        }

-

-        return result;

-      }

-    }

-

-

-    private struct VerificationResult

-    {

-      internal VerificationResult(string requestId, string checksum, string depsChecksum, ConditionGeneration.Outcome outcome, List<Counterexample> errors)

-      {

-        Checksum = checksum;

-        DependeciesChecksum = depsChecksum;

-        Outcome = outcome;

-        Errors = errors;

-        RequestId = requestId;

-      }

-

-      public readonly string Checksum;

-      public readonly string DependeciesChecksum;

-      public readonly string RequestId;

-      public readonly ConditionGeneration.Outcome Outcome;

-      public readonly List<Counterexample> Errors;

-    }

-

-

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

-

-

-    public static void EmptyCache()

-    {

-      VerificationResultCache.Clear();

-    }

-

-

-    public static void RemoveMatchingKeysFromCache(Regex pattern)

-    {

-      foreach (var kv in VerificationResultCache)

-      {

-        if (pattern.IsMatch(kv.Key))

-        {

-          VerificationResult res;

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

-        }

-      }

-    }

-

-

-    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/Source/ExecutionEngine/ExecutionEngine.csproj b/Source/ExecutionEngine/ExecutionEngine.csproj
index a614da12..91f13ed4 100644
--- a/Source/ExecutionEngine/ExecutionEngine.csproj
+++ b/Source/ExecutionEngine/ExecutionEngine.csproj
@@ -40,6 +40,7 @@
   <ItemGroup>

     <Compile Include="ExecutionEngine.cs" />

     <Compile Include="Properties\AssemblyInfo.cs" />

+    <Compile Include="VerificationResultCache.cs" />

   </ItemGroup>

   <ItemGroup>

     <ProjectReference Include="..\AbsInt\AbsInt.csproj">

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
new file mode 100644
index 00000000..ce87fa25
--- /dev/null
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -0,0 +1,165 @@
+using System;

+using System.Collections.Concurrent;

+using System.Collections.Generic;

+using System.Diagnostics.Contracts;

+using System.Linq;

+using System.Text;

+using System.Text.RegularExpressions;

+using VC;

+

+namespace Microsoft.Boogie

+{

+

+  class DependencyCollector : StandardVisitor

+  {

+    private 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 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));

+    }

+

+    public override Procedure VisitProcedure(Procedure node)

+    {

+      dependencies.Add(node);

+

+      return base.VisitProcedure(node);

+    }

+

+    public override Function VisitFunction(Function node)

+    {

+      dependencies.Add(node);

+

+      return base.VisitFunction(node);

+    }

+

+    public override Cmd VisitCallCmd(CallCmd node)

+    {

+      var result = base.VisitCallCmd(node);

+

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

+      if (!visited)

+      {

+        VisitProcedure(node.Proc);

+      }

+

+      return result;

+    }

+

+    public override Expr VisitNAryExpr(NAryExpr node)

+    {

+      var result = base.VisitNAryExpr(node);

+

+      var funCall = node.Fun as FunctionCall;

+      if (funCall != null)

+      {

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

+        if (!visited)

+        {

+          VisitFunction(funCall.Func);

+          if (funCall.Func.DefinitionAxiom != null)

+          {

+            VisitAxiom(funCall.Func.DefinitionAxiom);

+          }

+        }

+      }

+

+      return result;

+    }

+  }

+

+

+  public class VerificationResult

+  {

+    public readonly string Checksum;

+    public readonly string DependeciesChecksum;

+    public readonly string RequestId;

+    public readonly ConditionGeneration.Outcome Outcome;

+    public readonly List<Counterexample> Errors;

+

+    public VerificationResult(string requestId, string checksum, string depsChecksum, ConditionGeneration.Outcome outcome, List<Counterexample> errors)

+    {

+      Checksum = checksum;

+      DependeciesChecksum = depsChecksum;

+      Outcome = outcome;

+      Errors = errors;

+      RequestId = requestId;

+    }

+  }

+

+

+  public class VerificationResultCache

+  {

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

+

+

+    public void Insert(string key, VerificationResult result)

+    {

+      Contract.Requires(key != null);

+      Contract.Requires(result != null);

+

+      Cache[key] = result;

+    }

+

+

+    public VerificationResult Lookup(string key)

+    {

+      VerificationResult result;

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

+      return success ? result : null;

+    }

+

+

+    public void Clear()

+    {

+      Cache.Clear();

+    }

+

+

+    public void RemoveMatchingKeys(Regex keyRegexp)

+    {

+      foreach (var kv in Cache)

+      {

+        if (keyRegexp.IsMatch(kv.Key))

+        {

+          VerificationResult res;

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

+        }

+      }

+    }

+

+

+    public bool NeedsToBeVerified(Implementation impl)

+    {

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

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

+      {

+        return true;

+      }

+

+      var depsChecksum = DependencyCollector.DependenciesChecksum(impl);

+      return depsChecksum == null || Cache[impl.Id].DependeciesChecksum != depsChecksum;

+    }

+

+  }

+

+}