From 447caeeb7a6abf3e99c3d42499d353285cba304e Mon Sep 17 00:00:00 2001 From: wuestholz Date: Tue, 11 Jun 2013 13:59:30 -0700 Subject: Worked on improving program snapshot verification. --- Source/ExecutionEngine/ExecutionEngine.cs | 147 +------------------ Source/ExecutionEngine/ExecutionEngine.csproj | 1 + Source/ExecutionEngine/VerificationResultCache.cs | 165 ++++++++++++++++++++++ 3 files changed, 173 insertions(+), 140 deletions(-) create mode 100644 Source/ExecutionEngine/VerificationResultCache.cs 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 dependencies; - - public DependencyCollector() - { - dependencies = new HashSet(); - } - - public static void Collect(Absy node, out List 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 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 Errors; - } - - - private static readonly ConcurrentDictionary VerificationResultCache = new ConcurrentDictionary(); - - - 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 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 @@ + 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 dependencies; + + public DependencyCollector() + { + dependencies = new HashSet(); + } + + public static void Collect(Absy node, out List dependencies) + { + var dc = new DependencyCollector(); + dc.Visit(node); + dependencies = dc.dependencies.ToList(); + } + + public static string DependenciesChecksum(Implementation impl) + { + List 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 Errors; + + public VerificationResult(string requestId, string checksum, string depsChecksum, ConditionGeneration.Outcome outcome, List errors) + { + Checksum = checksum; + DependeciesChecksum = depsChecksum; + Outcome = outcome; + Errors = errors; + RequestId = requestId; + } + } + + + public class VerificationResultCache + { + private readonly ConcurrentDictionary Cache = new ConcurrentDictionary(); + + + 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; + } + + } + +} -- cgit v1.2.3