diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 147 | ||||
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.csproj | 1 | ||||
| -rw-r--r-- | Source/ExecutionEngine/VerificationResultCache.cs | 165 |
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;
+ }
+
+ }
+
+}
|