diff options
Diffstat (limited to 'Source/ExecutionEngine')
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 56 | ||||
| -rw-r--r-- | Source/ExecutionEngine/VerificationResultCache.cs | 212 |
2 files changed, 232 insertions, 36 deletions
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 6a4dbc07..925b414b 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -317,9 +317,32 @@ namespace Microsoft.Boogie public class VerificationResult
{
+ public readonly string RequestId;
public readonly string Checksum;
public readonly string DependeciesChecksum;
- public readonly string RequestId;
+ public readonly string ImplementationName;
+ public readonly IToken ImplementationToken;
+
+ private readonly WeakReference program;
+ public Program Program
+ {
+ get
+ {
+ if (program == null)
+ {
+ return null;
+ }
+ try
+ {
+ var p = program.Target as Program;
+ return p;
+ }
+ catch (InvalidOperationException)
+ {
+ return null;
+ }
+ }
+ }
public DateTime Start { get; set; }
public DateTime End { get; set; }
@@ -328,24 +351,20 @@ namespace Microsoft.Boogie public int ProofObligationCountBefore { get; set; }
public int ProofObligationCountAfter { get; set; }
- public ConditionGeneration.Outcome Outcome;
+ public ConditionGeneration.Outcome Outcome { get; set; }
public List<Counterexample> Errors;
- public string ImplementationName { get; set; }
- public IToken ImplementationToken { get; set; }
-
- public VerificationResult(string requestId, string checksum, string depsChecksum, ConditionGeneration.Outcome outcome, List<Counterexample> errors)
- : this(requestId, checksum, depsChecksum)
- {
- Outcome = outcome;
- Errors = errors;
- }
-
- public VerificationResult(string requestId, string checksum, string depsChecksum)
+ public VerificationResult(string requestId, string checksum, string depsChecksum, string implementationName, IToken implementationToken, Program program = null)
{
Checksum = checksum;
DependeciesChecksum = depsChecksum;
RequestId = requestId;
+ ImplementationName = implementationName;
+ ImplementationToken = implementationToken;
+ if (program != null)
+ {
+ this.program = new WeakReference(program);
+ }
}
}
@@ -844,7 +863,7 @@ namespace Microsoft.Boogie Implementation[] stablePrioritizedImpls = null;
if (0 < CommandLineOptions.Clo.VerifySnapshots)
{
- impls.Iter(impl => { impl.DependenciesChecksum = DependencyCollector.DependenciesChecksum(impl); });
+ impls.Iter(impl => { DependencyCollector.DependenciesChecksum(impl); });
stablePrioritizedImpls = impls.OrderByDescending(
impl => impl.Priority != 1 ? impl.Priority : Cache.VerificationPriority(impl)).ToArray();
}
@@ -855,6 +874,11 @@ namespace Microsoft.Boogie #endregion
+ if (1 < CommandLineOptions.Clo.VerifySnapshots)
+ {
+ CachedVerificationResultInjector.Inject(program, stablePrioritizedImpls);
+ }
+
#region Verify each implementation
var outputCollector = new OutputCollector(stablePrioritizedImpls);
@@ -995,9 +1019,7 @@ namespace Microsoft.Boogie {
#region Verify the implementation
- verificationResult = new VerificationResult(requestId, impl.Checksum, impl.DependenciesChecksum);
- verificationResult.ImplementationName = impl.Name;
- verificationResult.ImplementationToken = impl.tok;
+ verificationResult = new VerificationResult(requestId, impl.Checksum, impl.DependenciesChecksum, impl.Name, impl.tok, 1 < CommandLineOptions.Clo.VerifySnapshots ? program : null);
using (var vcgen = CreateVCGen(program, checkers))
{
diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs index 044d84fe..a0dba9d2 100644 --- a/Source/ExecutionEngine/VerificationResultCache.cs +++ b/Source/ExecutionEngine/VerificationResultCache.cs @@ -10,40 +10,204 @@ using VC; namespace Microsoft.Boogie
{
+ class CachedVerificationResultInjector : StandardVisitor
+ {
+ readonly IEnumerable<Implementation> Implementations;
+ readonly Program Program;
+ Program programInCachedSnapshot;
+ Implementation currentImplementation;
+ int assumptionVariableCount;
+ int temporaryVariableCount;
+
+ int FreshAssumptionVariableName
+ {
+ get
+ {
+ return assumptionVariableCount++;
+ }
+ }
+
+ int FreshTemporaryVariableName
+ {
+ get
+ {
+ return temporaryVariableCount++;
+ }
+ }
+
+ protected CachedVerificationResultInjector(Program program, IEnumerable<Implementation> implementations)
+ {
+ Implementations = implementations;
+ Program = program;
+ }
+
+ public Implementation Inject(Implementation implementation, Program programInCachedSnapshot)
+ {
+ Contract.Requires(implementation != null && programInCachedSnapshot != null);
+
+ this.programInCachedSnapshot = programInCachedSnapshot;
+ assumptionVariableCount = 0;
+ temporaryVariableCount = 0;
+ currentImplementation = implementation;
+ var result = VisitImplementation(implementation);
+ currentImplementation = null;
+ this.programInCachedSnapshot = null;
+ return result;
+ }
+
+ public static void Inject(Program program, IEnumerable<Implementation> implementations)
+ {
+ var eai = new CachedVerificationResultInjector(program, implementations);
+
+ foreach (var impl in implementations)
+ {
+ if (ExecutionEngine.Cache.VerificationPriority(impl) == 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 (vr.Errors != null)
+ {
+ impl.ErrorsInCachedSnapshot = vr.Errors.ToList<object>();
+ }
+ else if (vr.Outcome == ConditionGeneration.Outcome.Correct)
+ {
+ impl.ErrorsInCachedSnapshot = new List<object>();
+ }
+ var p = vr.Program;
+ if (p != null)
+ {
+ eai.Inject(impl, p);
+ }
+ }
+ }
+ }
+ }
+
+ public override Cmd VisitCallCmd(CallCmd node)
+ {
+ var result = base.VisitCallCmd(node);
+
+ // TODO(wuestholz): Maybe we should speed up this lookup.
+ var oldProc = programInCachedSnapshot.TopLevelDeclarations.OfType<Procedure>().FirstOrDefault(p => p.Name == node.Proc.Name);
+ if (oldProc != null
+ && DependencyCollector.DependenciesChecksum(oldProc) != DependencyCollector.DependenciesChecksum(node.Proc)
+ && DependencyCollector.AllFunctionDependenciesAreDefinedAndUnchanged(oldProc, Program))
+ {
+ var lv = new LocalVariable(Token.NoToken,
+ new TypedIdent(Token.NoToken, string.Format("a##post##{0}", FreshAssumptionVariableName), Type.Bool),
+ new QKeyValue(Token.NoToken, "assumption", new List<object>(), null));
+ currentImplementation.InjectAssumptionVariable(lv);
+
+ var before = new List<Cmd>();
+ if (currentImplementation.NoErrorsInCachedSnapshot
+ && oldProc.Requires.Any())
+ {
+ var pre = node.Precondition(oldProc, Program);
+ var assume = new AssumeCmd(Token.NoToken, pre, new QKeyValue(Token.NoToken, "precondition_previous_snapshot", new List<object>(), null));
+ before.Add(assume);
+ }
+ else if (currentImplementation.AnyErrorsInCachedSnapshot)
+ {
+ // TODO(wuestholz): Add an assume statement if the precondition was verified in the previous snapshot.
+ }
+
+ var post = node.Postcondition(oldProc, Program);
+ var mods = node.UnmodifiedBefore(oldProc);
+ foreach (var m in mods)
+ {
+ var mPre = new LocalVariable(Token.NoToken,
+ new TypedIdent(Token.NoToken, string.Format("{0}##pre##{1}", m.Name, FreshTemporaryVariableName), m.Type));
+ before.Add(new AssignCmd(Token.NoToken,
+ new List<AssignLhs> { new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, mPre)) },
+ new List<Expr> { new IdentifierExpr(Token.NoToken, m.Decl) }));
+ var eq = LiteralExpr.Eq(new IdentifierExpr(Token.NoToken, mPre), new IdentifierExpr(Token.NoToken, m.Decl));
+ post = LiteralExpr.And(post, eq);
+ }
+ var lhs = new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, lv));
+ var rhs = LiteralExpr.And(new IdentifierExpr(Token.NoToken, lv), post);
+ var assumed = new AssignCmd(Token.NoToken, new List<AssignLhs> { lhs }, new List<Expr> { rhs });
+
+ node.ExtendDesugaring(before, new List<Cmd> { assumed });
+ }
+
+ return result;
+ }
+ }
+
+
class DependencyCollector : ReadOnlyVisitor
{
- private HashSet<DeclWithFormals> dependencies;
+ private HashSet<Procedure> procedureDependencies;
+ private HashSet<Function> functionDependencies;
+ private bool allDependenciesHaveChecksum = true;
public DependencyCollector()
{
- dependencies = new HashSet<DeclWithFormals>();
+ procedureDependencies = new HashSet<Procedure>();
+ functionDependencies = new HashSet<Function>();
}
- public static void Collect(Absy node, out List<DeclWithFormals> dependencies)
+ static bool Collect(Absy node, out ISet<Procedure> procedureDependencies, out ISet<Function> functionDependencies)
{
var dc = new DependencyCollector();
dc.Visit(node);
- dependencies = dc.dependencies.ToList();
+ procedureDependencies = dc.procedureDependencies;
+ functionDependencies = dc.functionDependencies;
+ return dc.allDependenciesHaveChecksum;
+ }
+
+ static bool Collect(Procedure proc, out ISet<Function> functionDependencies)
+ {
+ var dc = new DependencyCollector();
+ dc.Visit(proc);
+ functionDependencies = dc.functionDependencies;
+ return dc.allDependenciesHaveChecksum;
+ }
+
+ public static bool AllFunctionDependenciesAreDefinedAndUnchanged(Procedure oldProc, Program newProg)
+ {
+ Contract.Requires(oldProc != null && newProg != null);
+
+ ISet<Function> oldDeps;
+ if (!Collect(oldProc, out oldDeps))
+ {
+ return false;
+ }
+ // TODO(wuestholz): Maybe we should speed up this lookup.
+ var funcs = newProg.TopLevelDeclarations.OfType<Function>();
+ return oldDeps.All(dep => funcs.Any(f => f.Name == dep.Name && f.Checksum == dep.Checksum));
}
- public static string DependenciesChecksum(Implementation impl)
+ public static string DependenciesChecksum(DeclWithFormals decl)
{
- List<DeclWithFormals> deps;
- DependencyCollector.Collect(impl, out deps);
- if (deps.Any(dep => dep.Checksum == null))
+ if (decl.DependenciesChecksum != null)
+ {
+ return decl.DependenciesChecksum;
+ }
+
+ ISet<Procedure> procDeps;
+ ISet<Function> funcDeps;
+ if (!DependencyCollector.Collect(decl, out procDeps, out funcDeps))
{
return null;
}
var md5 = System.Security.Cryptography.MD5.Create();
- var data = Encoding.UTF8.GetBytes(deps.MapConcat(dep => dep.Checksum, ""));
+ var procChecksums = procDeps.MapConcat(dep => dep.Checksum, "");
+ var funcChecksums = funcDeps.MapConcat(dep => dep.Checksum, "");
+ var data = Encoding.UTF8.GetBytes(procChecksums + funcChecksums);
var hashedData = md5.ComputeHash(data);
- return BitConverter.ToString(hashedData);
+ var result = BitConverter.ToString(hashedData);
+ decl.DependenciesChecksum = result;
+ return result;
}
public override Procedure VisitProcedure(Procedure node)
{
- dependencies.Add(node);
+ procedureDependencies.Add(node);
+ allDependenciesHaveChecksum &= node.Checksum != null;
foreach (var param in node.InParams)
{
@@ -58,7 +222,8 @@ namespace Microsoft.Boogie public override Function VisitFunction(Function node)
{
- dependencies.Add(node);
+ functionDependencies.Add(node);
+ allDependenciesHaveChecksum &= node.Checksum != null;
if (node.DefinitionAxiom != null)
{
@@ -70,7 +235,7 @@ namespace Microsoft.Boogie public override Cmd VisitCallCmd(CallCmd node)
{
- var visited = dependencies.Contains(node.Proc);
+ var visited = procedureDependencies.Contains(node.Proc);
if (!visited)
{
VisitProcedure(node.Proc);
@@ -84,7 +249,7 @@ namespace Microsoft.Boogie var funCall = node.Fun as FunctionCall;
if (funCall != null)
{
- var visited = dependencies.Contains(funCall.Func);
+ var visited = functionDependencies.Contains(funCall.Func);
if (!visited)
{
VisitFunction(funCall.Func);
@@ -96,6 +261,15 @@ 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 class VerificationResultCache
{
private readonly ConcurrentDictionary<string, VerificationResult> Cache = new ConcurrentDictionary<string, VerificationResult>();
@@ -152,7 +326,7 @@ namespace Microsoft.Boogie public bool NeedsToBeVerified(Implementation impl)
{
- return VerificationPriority(impl) < int.MaxValue;
+ return VerificationPriority(impl) < Priority.SKIP;
}
@@ -160,19 +334,19 @@ namespace Microsoft.Boogie {
if (!Cache.ContainsKey(impl.Id))
{
- return 3; // high priority (has been never verified before)
+ return Priority.HIGH; // 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)
+ return Priority.MEDIUM; // medium priority (old snapshot has been verified before)
}
else if (impl.DependenciesChecksum == null || Cache[impl.Id].DependeciesChecksum != impl.DependenciesChecksum)
{
- return 1; // low priority (the same snapshot has been verified before, but a callee has changed)
+ return Priority.LOW; // low priority (the same snapshot has been verified before, but a callee has changed)
}
else
{
- return int.MaxValue; // skip verification (highest priority to get them done as soon as possible)
+ return Priority.SKIP; // skip verification (highest priority to get them done as soon as possible)
}
}
}
|