diff options
| -rw-r--r-- | Source/Core/Absy.cs | 127 | ||||
| -rw-r--r-- | Source/Core/AbsyCmd.cs | 6 | ||||
| -rw-r--r-- | Source/Core/AbsyExpr.cs | 8 | ||||
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 4 | ||||
| -rw-r--r-- | Source/ExecutionEngine/VerificationResultCache.cs | 106 |
5 files changed, 172 insertions, 79 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 7950feed..e256c7d9 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -1848,6 +1848,82 @@ namespace Microsoft.Boogie { this.OutParams = that.OutParams;
}
+ public byte[] MD5Checksum_;
+ public byte[] MD5Checksum
+ {
+ get
+ {
+ if (MD5Checksum_ == null)
+ {
+ var c = Checksum;
+ if (c != null)
+ {
+ MD5Checksum_ = System.Security.Cryptography.MD5.Create().ComputeHash(System.Text.Encoding.UTF8.GetBytes(c));
+ }
+ }
+ return MD5Checksum_;
+ }
+ }
+
+ public byte[] MD5DependenciesChecksum_;
+ public byte[] MD5DependenciesChecksum
+ {
+ get
+ {
+ Contract.Requires(DependenciesCollected);
+
+ if (MD5DependenciesChecksum_ == null && MD5Checksum != null)
+ {
+ var c = MD5Checksum;
+ var transFuncDeps = new HashSet<Function>();
+ if (procedureDependencies != null)
+ {
+ foreach (var p in procedureDependencies)
+ {
+ if (p.FunctionDependencies != null)
+ {
+ foreach (var f in p.FunctionDependencies)
+ {
+ transFuncDeps.Add(f);
+ }
+ }
+ var pc = p.MD5Checksum;
+ if (pc == null) { return null; }
+ c = ChecksumHelper.CombineChecksums(c, pc, true);
+ }
+ }
+ if (FunctionDependencies != null)
+ {
+ foreach (var f in FunctionDependencies)
+ {
+ transFuncDeps.Add(f);
+ }
+ }
+ var q = new Queue<Function>(transFuncDeps);
+ while (q.Any())
+ {
+ var f = q.Dequeue();
+ var fc = f.MD5Checksum;
+ if (fc == null) { return null; }
+ c = ChecksumHelper.CombineChecksums(c, fc, true);
+ if (f.FunctionDependencies != null)
+ {
+ foreach (var d in f.FunctionDependencies)
+ {
+ if (!transFuncDeps.Contains(d))
+ {
+ transFuncDeps.Add(d);
+ q.Enqueue(d);
+ }
+ }
+ }
+ }
+ MD5DependenciesChecksum_ = c;
+ }
+ return MD5DependenciesChecksum_;
+ }
+ }
+
public string Checksum
{
get
@@ -1856,7 +1932,56 @@ namespace Microsoft.Boogie { }
}
- public string DependenciesChecksum { get; set; }
+ string dependenciesChecksum;
+ public string DependenciesChecksum
+ {
+ get
+ {
+ if (dependenciesChecksum == null && MD5DependenciesChecksum != null)
+ {
+ dependenciesChecksum = BitConverter.ToString(MD5DependenciesChecksum);
+ }
+ return dependenciesChecksum;
+ }
+ }
+
+ public bool DependenciesCollected { get; set; }
+
+ ISet<Procedure> procedureDependencies;
+
+ public ISet<Procedure> ProcedureDependencies
+ {
+ get { return procedureDependencies; }
+ }
+
+ public void AddProcedureDependency(Procedure procedure)
+ {
+ Contract.Requires(procedure != null);
+
+ if (procedureDependencies == null)
+ {
+ procedureDependencies = new HashSet<Procedure>();
+ }
+ procedureDependencies.Add(procedure);
+ }
+
+ ISet<Function> functionDependencies;
+
+ public ISet<Function> FunctionDependencies
+ {
+ get { return functionDependencies; }
+ }
+
+ public void AddFunctionDependency(Function function)
+ {
+ Contract.Requires(function != null);
+
+ if (functionDependencies == null)
+ {
+ functionDependencies = new HashSet<Function>();
+ }
+ functionDependencies.Add(function);
+ }
protected void EmitSignature(TokenTextWriter stream, bool shortRet) {
Contract.Requires(stream != null);
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index fae4464a..cd017e5e 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -2089,7 +2089,11 @@ namespace Microsoft.Boogie { stream.Write(TokenTextWriter.SanitizeIdentifier(callee));
if (stream.UseForComputingChecksums && EmitDependenciesChecksum)
{
- stream.Write(string.Format("[dependencies_checksum:{0}]", Proc.DependenciesChecksum));
+ var c = Proc.DependenciesChecksum;
+ if (c != null)
+ {
+ stream.Write(string.Format("[dependencies_checksum:{0}]", c));
+ }
}
stream.Write("(");
sep = "";
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index ffd95f77..d928e536 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -1802,9 +1802,13 @@ namespace Microsoft.Boogie { //Contract.Requires(stream != null);
//Contract.Requires(args != null);
this.name.Emit(stream, 0xF0, false);
- if (stream.UseForComputingChecksums && Func.DependenciesChecksum != null)
+ if (stream.UseForComputingChecksums)
{
- stream.Write(string.Format("[dependencies_checksum:{0}]", Func.DependenciesChecksum));
+ var c = Func.DependenciesChecksum;
+ if (c != null)
+ {
+ stream.Write(string.Format("[dependencies_checksum:{0}]", c));
+ }
}
stream.Write("(");
args.Emit(stream);
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 1b799bd5..a568176b 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -880,9 +880,7 @@ namespace Microsoft.Boogie {
// TODO(wuestholz): Maybe we should speed up this lookup.
OtherDefinitionAxiomsCollector.Collect(program.TopLevelDeclarations.OfType<Axiom>());
- // TODO(wuestholz): Maybe we should speed up this lookup.
- program.TopLevelDeclarations.OfType<Function>().Iter(fun => { DependencyCollector.DependenciesChecksum(fun); });
- impls.Iter(impl => { DependencyCollector.DependenciesChecksum(impl); });
+ DependencyCollector.Collect(program);
stablePrioritizedImpls = impls.OrderByDescending(
impl => impl.Priority != 1 ? impl.Priority : Cache.VerificationPriority(impl)).ToArray();
}
diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs index b401ec67..44ca7da8 100644 --- a/Source/ExecutionEngine/VerificationResultCache.cs +++ b/Source/ExecutionEngine/VerificationResultCache.cs @@ -197,7 +197,7 @@ namespace Microsoft.Boogie // 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)
+ && oldProc.DependenciesChecksum != node.Proc.DependenciesChecksum
&& node.AssignedAssumptionVariable == null)
{
if (DependencyCollector.AllFunctionDependenciesAreDefinedAndUnchanged(oldProc, Program))
@@ -293,87 +293,44 @@ namespace Microsoft.Boogie sealed class DependencyCollector : ReadOnlyVisitor
{
- private HashSet<Procedure> procedureDependencies;
- private HashSet<Function> functionDependencies;
- private bool allDependenciesHaveChecksum = true;
+ private DeclWithFormals currentDeclaration;
- public DependencyCollector()
- {
- procedureDependencies = new HashSet<Procedure>();
- functionDependencies = new HashSet<Function>();
- }
-
- static bool Collect(Absy node, out ISet<Procedure> procedureDependencies, out ISet<Function> functionDependencies)
- {
- var dc = new DependencyCollector();
- dc.Visit(node);
- procedureDependencies = dc.procedureDependencies;
- functionDependencies = dc.functionDependencies;
- return dc.allDependenciesHaveChecksum;
- }
-
- static bool Collect(Procedure proc, out ISet<Function> functionDependencies)
+ public static void Collect(Program program)
{
var dc = new DependencyCollector();
- dc.Visit(proc);
- functionDependencies = dc.functionDependencies;
- return dc.allDependenciesHaveChecksum;
+ dc.VisitProgram(program);
}
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));
+ return oldProc.FunctionDependencies != null && oldProc.FunctionDependencies.All(dep => funcs.Any(f => f.Name == dep.Name && f.DependenciesChecksum == dep.DependenciesChecksum));
}
- public static string DependenciesChecksum(DeclWithFormals decl)
+ public override Procedure VisitProcedure(Procedure node)
{
- if (decl.DependenciesChecksum != null)
- {
- return decl.DependenciesChecksum;
- }
-
- ISet<Procedure> procDeps;
- ISet<Function> funcDeps;
- if (!DependencyCollector.Collect(decl, out procDeps, out funcDeps))
- {
- return null;
- }
+ currentDeclaration = node;
- string result = null;
- using (var ms = new System.IO.MemoryStream())
- using (var wr = new System.IO.BinaryWriter(ms))
+ foreach (var param in node.InParams)
{
- foreach (var dep in procDeps)
- {
- wr.Write(Encoding.UTF8.GetBytes(dep.Checksum));
- }
- foreach (var dep in funcDeps)
+ if (param.TypedIdent != null && param.TypedIdent.WhereExpr != null)
{
- wr.Write(Encoding.UTF8.GetBytes(dep.Checksum));
+ VisitExpr(param.TypedIdent.WhereExpr);
}
- wr.Flush();
- wr.BaseStream.Position = 0;
- var md5 = System.Security.Cryptography.MD5.Create();
- var hashedData = md5.ComputeHash(wr.BaseStream);
- result = BitConverter.ToString(hashedData);
}
- decl.DependenciesChecksum = result;
+
+ var result = base.VisitProcedure(node);
+ node.DependenciesCollected = true;
+ currentDeclaration = null;
return result;
}
- public override Procedure VisitProcedure(Procedure node)
+ public override Implementation VisitImplementation(Implementation node)
{
- procedureDependencies.Add(node);
- allDependenciesHaveChecksum &= node.Checksum != null;
+ currentDeclaration = node;
foreach (var param in node.InParams)
{
@@ -383,13 +340,20 @@ namespace Microsoft.Boogie }
}
- return base.VisitProcedure(node);
+ if (node.Proc != null)
+ {
+ node.AddProcedureDependency(node.Proc);
+ }
+
+ var result = base.VisitImplementation(node);
+ node.DependenciesCollected = true;
+ currentDeclaration = null;
+ return result;
}
public override Function VisitFunction(Function node)
{
- functionDependencies.Add(node);
- allDependenciesHaveChecksum &= node.Checksum != null;
+ currentDeclaration = node;
if (node.DefinitionAxiom != null)
{
@@ -406,15 +370,17 @@ namespace Microsoft.Boogie }
}
- return base.VisitFunction(node);
+ var result = base.VisitFunction(node);
+ node.DependenciesCollected = true;
+ currentDeclaration = null;
+ return result;
}
public override Cmd VisitCallCmd(CallCmd node)
{
- var visited = procedureDependencies.Contains(node.Proc);
- if (!visited)
+ if (currentDeclaration != null)
{
- VisitProcedure(node.Proc);
+ currentDeclaration.AddProcedureDependency(node.Proc);
}
return base.VisitCallCmd(node);
@@ -423,13 +389,9 @@ namespace Microsoft.Boogie public override Expr VisitNAryExpr(NAryExpr node)
{
var funCall = node.Fun as FunctionCall;
- if (funCall != null)
+ if (funCall != null && currentDeclaration != null)
{
- var visited = functionDependencies.Contains(funCall.Func);
- if (!visited)
- {
- VisitFunction(funCall.Func);
- }
+ currentDeclaration.AddFunctionDependency(funCall.Func);
}
return base.VisitNAryExpr(node);
|