summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar wuestholz <unknown>2014-07-10 10:25:53 +0200
committerGravatar wuestholz <unknown>2014-07-10 10:25:53 +0200
commite721ac469b8aa3f964ad24917757168288826da1 (patch)
treee9c1d877f54fa7000ff96bbcb90c5b79c1d63003
parent736eb8d7b2d80e7672fcdffba8d731c7bb9bb9d7 (diff)
Worked on the more advanced verification result caching.
-rw-r--r--Source/Core/AbsyCmd.cs5
-rw-r--r--Source/ExecutionEngine/ExecutionEngine.cs2
-rw-r--r--Source/ExecutionEngine/VerificationResultCache.cs62
-rw-r--r--Source/VCGeneration/ConditionGeneration.cs14
-rw-r--r--Test/snapshots/runtest.snapshot2
-rw-r--r--Test/snapshots/runtest.snapshot.expect92
6 files changed, 54 insertions, 123 deletions
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 466b2f0e..e2781b6f 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -1998,6 +1998,7 @@ namespace Microsoft.Boogie {
public string/*!*/ callee { get; set; }
public Procedure Proc;
public LocalVariable AssignedAssumptionVariable;
+ public bool EmitDependenciesChecksum;
// Element of the following lists can be null, which means that
// the call happens with * as these parameters
@@ -2085,6 +2086,10 @@ namespace Microsoft.Boogie {
stream.Write(" := ");
}
stream.Write(TokenTextWriter.SanitizeIdentifier(callee));
+ if (stream.UseForComputingChecksums && EmitDependenciesChecksum)
+ {
+ stream.Write(string.Format("[dependencies_checksum:{0}]", Proc.DependenciesChecksum));
+ }
stream.Write("(");
sep = "";
foreach (Expr arg in Ins) {
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index ea69b29e..1b799bd5 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -880,6 +880,8 @@ 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); });
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 b9c04661..b401ec67 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -198,40 +198,46 @@ namespace Microsoft.Boogie
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)
&& node.AssignedAssumptionVariable == null)
{
- 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));
- node.AssignedAssumptionVariable = lv;
- currentImplementation.InjectAssumptionVariable(lv);
-
- var before = new List<Cmd>();
- if (oldProc.Requires.Any())
+ if (DependencyCollector.AllFunctionDependenciesAreDefinedAndUnchanged(oldProc, Program))
{
- var pre = node.CheckedPrecondition(oldProc, Program);
- var assume = new AssumeCmd(Token.NoToken, pre, new QKeyValue(Token.NoToken, "precondition_previous_snapshot", new List<object>(), null));
- before.Add(assume);
- }
+ 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));
+ node.AssignedAssumptionVariable = lv;
+ currentImplementation.InjectAssumptionVariable(lv);
+
+ var before = new List<Cmd>();
+ if (oldProc.Requires.Any())
+ {
+ var pre = node.CheckedPrecondition(oldProc, Program);
+ var assume = new AssumeCmd(Token.NoToken, pre, new QKeyValue(Token.NoToken, "precondition_previous_snapshot", new List<object>(), null));
+ before.Add(assume);
+ }
- var post = node.Postcondition(oldProc, Program);
- var mods = node.UnmodifiedBefore(oldProc);
- foreach (var m in mods)
+ 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 });
+ }
+ else
{
- 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);
+ node.EmitDependenciesChecksum = true;
}
- 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;
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index cdeb6c2c..25ddc2c0 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1531,14 +1531,24 @@ namespace VC {
passiveCmds.Add(new AssumeCmd(Token.NoToken, expr));
}
else if (currentImplementation != null
+ && ac.Checksum != null
+ && (currentImplementation.AssertionChecksumsInPreviousSnapshot != null && currentImplementation.AssertionChecksumsInPreviousSnapshot.Contains(ac.Checksum))
+ && currentImplementation.ErrorChecksumToCachedError != null
+ && !currentImplementation.ErrorChecksumToCachedError.ContainsKey(ac.Checksum)
+ && (currentImplementation.InjectedAssumptionVariables == null || !currentImplementation.InjectedAssumptionVariables.Any(v => incarnationMap.ContainsKey(v))))
+ {
+ // Turn it into an assume statement.
+ // TODO(wuestholz): Uncomment this.
+ // pc = new AssumeCmd(ac.tok, copy);
+ pc.Attributes = new QKeyValue(Token.NoToken, "verified_assertion", new List<object>(), pc.Attributes);
+ }
+ else if (currentImplementation != null
&& currentImplementation.AnyErrorsInCachedSnapshot
&& ac.Checksum != null
&& (currentImplementation.AssertionChecksumsInPreviousSnapshot != null && currentImplementation.AssertionChecksumsInPreviousSnapshot.Contains(ac.Checksum))
&& currentImplementation.ErrorChecksumToCachedError.ContainsKey(ac.Checksum)
&& (currentImplementation.InjectedAssumptionVariables == null || !currentImplementation.InjectedAssumptionVariables.Any(v => incarnationMap.ContainsKey(v))))
{
- // TODO(wuestholz): Do the same for assertions if they have been proved in the previous snapshot.
-
// Turn it into an assume statement.
// TODO(wuestholz): Uncomment this.
// pc = new AssumeCmd(ac.tok, copy);
diff --git a/Test/snapshots/runtest.snapshot b/Test/snapshots/runtest.snapshot
index e3c00eee..4cd43022 100644
--- a/Test/snapshots/runtest.snapshot
+++ b/Test/snapshots/runtest.snapshot
@@ -1,2 +1,2 @@
-// RUN: %boogie -verifySnapshots:2 -verifySeparately Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl Snapshots8.bpl Snapshots9.bpl Snapshots10.bpl Snapshots11.bpl Snapshots12.bpl Snapshots13.bpl Snapshots14.bpl Snapshots15.bpl Snapshots16.bpl Snapshots17.bpl Snapshots18.bpl Snapshots19.bpl Snapshots20.bpl Snapshots21.bpl Snapshots22.bpl > "%t"
+// RUN: %boogie -errorTrace:0 -verifySnapshots:2 -verifySeparately Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl Snapshots8.bpl Snapshots9.bpl Snapshots10.bpl Snapshots11.bpl Snapshots12.bpl Snapshots13.bpl Snapshots14.bpl Snapshots15.bpl Snapshots16.bpl Snapshots17.bpl Snapshots18.bpl Snapshots19.bpl Snapshots20.bpl Snapshots21.bpl Snapshots22.bpl > "%t"
// RUN: %diff "%s.expect" "%t"
diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect
index f4ee0ca9..80325bea 100644
--- a/Test/snapshots/runtest.snapshot.expect
+++ b/Test/snapshots/runtest.snapshot.expect
@@ -1,44 +1,24 @@
Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.
-Execution trace:
- Snapshots0.v0.bpl(41,5): anon0
Snapshots0.v0.bpl(8,5): Error BP5001: This assertion might not hold.
-Execution trace:
- Snapshots0.v0.bpl(8,5): anon0
Snapshots0.v0.bpl(19,5): Error BP5001: This assertion might not hold.
-Execution trace:
- Snapshots0.v0.bpl(19,5): anon0
Snapshots0.v0.bpl(30,5): Error BP5001: This assertion might not hold.
-Execution trace:
- Snapshots0.v0.bpl(30,5): anon0
Boogie program verifier finished with 0 verified, 4 errors
Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.
-Execution trace:
- Snapshots0.v0.bpl(41,5): anon0
Snapshots0.v1.bpl(30,5): Error BP5001: This assertion might not hold.
-Execution trace:
- Snapshots0.v1.bpl(30,5): anon0
Boogie program verifier finished with 2 verified, 2 errors
Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.
-Execution trace:
- Snapshots0.v0.bpl(41,5): anon0
Boogie program verifier finished with 2 verified, 1 error
Snapshots1.v0.bpl(13,5): Error BP5001: This assertion might not hold.
-Execution trace:
- Snapshots1.v0.bpl(13,5): anon0
Boogie program verifier finished with 1 verified, 1 error
Snapshots1.v1.bpl(13,5): Error BP5001: This assertion might not hold.
-Execution trace:
- Snapshots1.v1.bpl(13,5): anon0
Boogie program verifier finished with 1 verified, 1 error
Snapshots1.v2.bpl(5,5): Error BP5002: A precondition for this call might not hold.
Snapshots1.v2.bpl(10,3): Related location: This is the precondition that might not hold.
-Execution trace:
- Snapshots1.v2.bpl(5,5): anon0
Boogie program verifier finished with 1 verified, 1 error
@@ -57,33 +37,23 @@ Boogie program verifier finished with 1 verified, 0 errors
Boogie program verifier finished with 1 verified, 0 errors
Snapshots3.v1.bpl(6,1): Error BP5003: A postcondition might not hold on this return path.
Snapshots3.v1.bpl(2,1): Related location: This is the postcondition that might not hold.
-Execution trace:
- Snapshots3.v1.bpl(6,1): anon0
Boogie program verifier finished with 0 verified, 1 error
Boogie program verifier finished with 3 verified, 0 errors
Snapshots4.v1.bpl(23,5): Error BP5001: This assertion might not hold.
-Execution trace:
- Snapshots4.v1.bpl(23,5): anon0
Snapshots4.v1.bpl(33,1): Error BP5003: A postcondition might not hold on this return path.
Snapshots4.v1.bpl(28,3): Related location: This is the postcondition that might not hold.
-Execution trace:
- Snapshots4.v1.bpl(33,1): anon0
Boogie program verifier finished with 2 verified, 2 errors
Boogie program verifier finished with 1 verified, 0 errors
Snapshots5.v1.bpl(5,5): Error BP5001: This assertion might not hold.
-Execution trace:
- Snapshots5.v1.bpl(5,5): anon0
Boogie program verifier finished with 0 verified, 1 error
Boogie program verifier finished with 1 verified, 0 errors
Snapshots6.v1.bpl(13,5): Error BP5001: This assertion might not hold.
-Execution trace:
- Snapshots6.v1.bpl(9,7): anon0
Boogie program verifier finished with 0 verified, 1 error
@@ -104,133 +74,71 @@ Boogie program verifier finished with 1 verified, 0 errors
Boogie program verifier finished with 1 verified, 0 errors
Snapshots11.v0.bpl(7,5): Error BP5002: A precondition for this call might not hold.
Snapshots11.v0.bpl(13,3): Related location: This is the precondition that might not hold.
-Execution trace:
- Snapshots11.v0.bpl(7,5): anon0
Boogie program verifier finished with 0 verified, 1 error
Snapshots11.v1.bpl(7,5): Error BP5002: A precondition for this call might not hold.
Snapshots11.v1.bpl(13,3): Related location: This is the precondition that might not hold.
-Execution trace:
- Snapshots11.v1.bpl(7,5): anon0
Boogie program verifier finished with 0 verified, 1 error
Boogie program verifier finished with 1 verified, 0 errors
Snapshots12.v1.bpl(7,5): Error BP5001: This assertion might not hold.
-Execution trace:
- Snapshots12.v1.bpl(5,5): anon0
Boogie program verifier finished with 0 verified, 1 error
Boogie program verifier finished with 1 verified, 0 errors
Snapshots13.v1.bpl(7,5): Error BP5001: This assertion might not hold.
-Execution trace:
- Snapshots13.v1.bpl(5,5): anon0
Boogie program verifier finished with 0 verified, 1 error
Boogie program verifier finished with 1 verified, 0 errors
Snapshots14.v1.bpl(7,5): Error BP5001: This assertion might not hold.
-Execution trace:
- Snapshots14.v1.bpl(5,5): anon0
Boogie program verifier finished with 0 verified, 1 error
Boogie program verifier finished with 1 verified, 0 errors
Snapshots15.v1.bpl(13,5): Error BP5001: This assertion might not hold.
-Execution trace:
- Snapshots15.v1.bpl(5,5): anon0
Boogie program verifier finished with 0 verified, 1 error
Boogie program verifier finished with 1 verified, 0 errors
Snapshots16.v1.bpl(14,5): Error BP5001: This assertion might not hold.
-Execution trace:
- Snapshots16.v1.bpl(14,5): anon0
Boogie program verifier finished with 0 verified, 1 error
Boogie program verifier finished with 1 verified, 0 errors
Snapshots17.v1.bpl(20,13): Error BP5001: This assertion might not hold.
-Execution trace:
- Snapshots17.v1.bpl(7,7): anon0
- Snapshots17.v1.bpl(10,9): anon6_LoopHead
- Snapshots17.v1.bpl(12,13): anon6_LoopBody
Snapshots17.v1.bpl(25,9): Error BP5001: This assertion might not hold.
-Execution trace:
- Snapshots17.v1.bpl(7,7): anon0
- Snapshots17.v1.bpl(10,9): anon6_LoopHead
- Snapshots17.v1.bpl(10,9): anon6_LoopDone
Boogie program verifier finished with 0 verified, 2 errors
Boogie program verifier finished with 1 verified, 0 errors
Snapshots18.v1.bpl(17,9): Error BP5001: This assertion might not hold.
-Execution trace:
- Snapshots18.v1.bpl(5,5): anon0
- Snapshots18.v1.bpl(5,5): anon5_LoopHead
- Snapshots18.v1.bpl(7,9): anon5_LoopBody
- Snapshots18.v1.bpl(12,9): anon6_Else
Snapshots18.v1.bpl(20,5): Error BP5001: This assertion might not hold.
-Execution trace:
- Snapshots18.v1.bpl(5,5): anon0
- Snapshots18.v1.bpl(5,5): anon5_LoopHead
- Snapshots18.v1.bpl(7,9): anon5_LoopBody
- Snapshots18.v1.bpl(14,13): anon6_Then
- Snapshots18.v1.bpl(20,5): anon4
Boogie program verifier finished with 0 verified, 2 errors
Snapshots19.v0.bpl(7,5): Error BP5001: This assertion might not hold.
-Execution trace:
- Snapshots19.v0.bpl(5,5): anon0
Boogie program verifier finished with 0 verified, 1 error
Snapshots19.v1.bpl(7,5): Error BP5001: This assertion might not hold.
-Execution trace:
- Snapshots19.v1.bpl(5,5): anon0
Boogie program verifier finished with 0 verified, 1 error
Snapshots20.v0.bpl(13,9): Error BP5001: This assertion might not hold.
-Execution trace:
- Snapshots20.v0.bpl(5,5): anon0
- Snapshots20.v0.bpl(13,9): anon4_Else
Boogie program verifier finished with 0 verified, 1 error
Snapshots20.v1.bpl(9,9): Error BP5001: This assertion might not hold.
-Execution trace:
- Snapshots20.v1.bpl(5,5): anon0
- Snapshots20.v1.bpl(7,9): anon4_Then
Snapshots20.v1.bpl(13,9): Error BP5001: This assertion might not hold.
-Execution trace:
- Snapshots20.v1.bpl(5,5): anon0
- Snapshots20.v1.bpl(13,9): anon4_Else
Boogie program verifier finished with 0 verified, 2 errors
Snapshots21.v0.bpl(7,9): Error BP5001: This assertion might not hold.
-Execution trace:
- Snapshots21.v0.bpl(5,5): anon0
- Snapshots21.v0.bpl(7,9): anon4_Then
Snapshots21.v0.bpl(11,9): Error BP5001: This assertion might not hold.
-Execution trace:
- Snapshots21.v0.bpl(5,5): anon0
- Snapshots21.v0.bpl(11,9): anon4_Else
Boogie program verifier finished with 0 verified, 2 errors
Snapshots21.v1.bpl(11,9): Error BP5001: This assertion might not hold.
-Execution trace:
- Snapshots21.v1.bpl(5,5): anon0
- Snapshots21.v1.bpl(11,9): anon4_Else
Snapshots21.v1.bpl(14,5): Error BP5001: This assertion might not hold.
-Execution trace:
- Snapshots21.v1.bpl(5,5): anon0
- Snapshots21.v1.bpl(7,9): anon4_Then
- Snapshots21.v1.bpl(14,5): anon3
Boogie program verifier finished with 0 verified, 2 errors
Snapshots22.v0.bpl(7,9): Error BP5001: This assertion might not hold.
-Execution trace:
- Snapshots22.v0.bpl(5,5): anon0
- Snapshots22.v0.bpl(7,9): anon4_Then
Boogie program verifier finished with 0 verified, 1 error