From 0ed4ba928d57bf1f067c66d390ba1c147ef618f4 Mon Sep 17 00:00:00 2001 From: wuestholz Date: Wed, 5 Jun 2013 16:04:40 -0700 Subject: Worked on improving program snapshot verification. --- Source/Core/Absy.cs | 16 +++--- Source/ExecutionEngine/ExecutionEngine.cs | 93 ++++++++++++++++++++++++++++++- Test/snapshots/Answer | 33 +++++++++++ Test/snapshots/Snapshots1.v0.bpl | 14 +++++ Test/snapshots/Snapshots1.v1.bpl | 14 +++++ Test/snapshots/Snapshots1.v2.bpl | 15 +++++ Test/snapshots/Snapshots2.v0.bpl | 12 ++++ Test/snapshots/Snapshots2.v1.bpl | 12 ++++ Test/snapshots/Snapshots2.v2.bpl | 13 +++++ Test/snapshots/Snapshots2.v3.bpl | 13 +++++ Test/snapshots/Snapshots2.v4.bpl | 13 +++++ Test/snapshots/Snapshots2.v5.bpl | 14 +++++ Test/snapshots/runtest.bat | 10 ++++ 13 files changed, 261 insertions(+), 11 deletions(-) create mode 100644 Test/snapshots/Snapshots1.v0.bpl create mode 100644 Test/snapshots/Snapshots1.v1.bpl create mode 100644 Test/snapshots/Snapshots1.v2.bpl create mode 100644 Test/snapshots/Snapshots2.v0.bpl create mode 100644 Test/snapshots/Snapshots2.v1.bpl create mode 100644 Test/snapshots/Snapshots2.v2.bpl create mode 100644 Test/snapshots/Snapshots2.v3.bpl create mode 100644 Test/snapshots/Snapshots2.v4.bpl create mode 100644 Test/snapshots/Snapshots2.v5.bpl diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 55b37f13..fd62f334 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -1794,6 +1794,14 @@ namespace Microsoft.Boogie { this.OutParams = that.OutParams; } + public string Checksum + { + get + { + return FindStringAttribute("checksum"); + } + } + protected void EmitSignature(TokenTextWriter stream, bool shortRet) { Contract.Requires(stream != null); Type.EmitOptionalTypeParams(stream, TypeParameters); @@ -2567,14 +2575,6 @@ namespace Microsoft.Boogie { } } - public string Checksum - { - get - { - return FindStringAttribute("checksum"); - } - } - public string Id { get diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index e87ea790..3c10116f 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -795,6 +795,11 @@ namespace Microsoft.Boogie } VCGen.Outcome outcome; + string depsChecksum = null; + if (CommandLineOptions.Clo.VerifySnapshots) + { + depsChecksum = DependenciesChecksum(impl); + } try { if (CommandLineOptions.Clo.inferLeastForUnsat != null) @@ -819,7 +824,7 @@ namespace Microsoft.Boogie } else { - if (!VerificationResultCache.ContainsKey(impl.Id) || VerificationResultCache[impl.Id].Checksum != impl.Checksum) + if (!CommandLineOptions.Clo.VerifySnapshots || NeedsToBeVerified(impl)) { outcome = vcgen.VerifyImplementation(impl, out errors); } @@ -871,7 +876,7 @@ namespace Microsoft.Boogie if (CommandLineOptions.Clo.VerifySnapshots && !string.IsNullOrEmpty(impl.Checksum)) { - var result = new VerificationResult(impl.Checksum, outcome, errors); + var result = new VerificationResult(impl.Checksum, depsChecksum, outcome, errors); VerificationResultCache[impl.Id] = result; } @@ -1123,16 +1128,67 @@ 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) + { + var result = base.VisitProcedure(node); + + dependencies.Add(node); + + return result; + } + + public override Cmd VisitCallCmd(CallCmd node) + { + var result = base.VisitCallCmd(node); + + dependencies.Add(node.Proc); + + return result; + } + + public override Expr VisitNAryExpr(NAryExpr node) + { + var result = base.VisitNAryExpr(node); + + var funCall = node.Fun as FunctionCall; + if (funCall != null) + { + dependencies.Add(funCall.Func); + } + + return result; + } + } + + private struct VerificationResult { - internal VerificationResult(string checksum, ConditionGeneration.Outcome outcome, List errors) + internal VerificationResult(string checksum, string depsChecksum, ConditionGeneration.Outcome outcome, List errors) { Checksum = checksum; + DependeciesChecksum = depsChecksum; Outcome = outcome; Errors = errors; } public readonly string Checksum; + public readonly string DependeciesChecksum; public readonly ConditionGeneration.Outcome Outcome; public readonly List Errors; } @@ -1140,6 +1196,37 @@ namespace Microsoft.Boogie private static readonly ConcurrentDictionary VerificationResultCache = new ConcurrentDictionary(); + + public static void EmptyCache() + { + VerificationResultCache.Clear(); + } + + + 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/Test/snapshots/Answer b/Test/snapshots/Answer index 434cdfda..a7a6b0be 100644 --- a/Test/snapshots/Answer +++ b/Test/snapshots/Answer @@ -1,3 +1,4 @@ +-------------------- Snapshots0.bpl -------------------- Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold. Execution trace: Snapshots0.v0.bpl(41,5): anon0 @@ -25,3 +26,35 @@ Execution trace: Snapshots0.v0.bpl(41,5): anon0 Boogie program verifier finished with 2 verified, 1 error + +-------------------- Snapshots1.bpl -------------------- +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 + +-------------------- Snapshots2.bpl -------------------- + +Boogie program verifier finished with 1 verified, 0 errors + +Boogie program verifier finished with 1 verified, 0 errors + +Boogie program verifier finished with 1 verified, 0 errors + +Boogie program verifier finished with 1 verified, 0 errors + +Boogie program verifier finished with 1 verified, 0 errors + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/snapshots/Snapshots1.v0.bpl b/Test/snapshots/Snapshots1.v0.bpl new file mode 100644 index 00000000..d6d4332e --- /dev/null +++ b/Test/snapshots/Snapshots1.v0.bpl @@ -0,0 +1,14 @@ +procedure {:checksum "P1$proc#0"} P1(); +// Action: verify +implementation {:checksum "P1$impl#0"} P1() +{ + call P2(); +} + + +procedure {:checksum "P2$proc#0"} P2(); +// Action: verify +implementation {:checksum "P2$impl#0"} P2() +{ + assert 1 != 1; +} diff --git a/Test/snapshots/Snapshots1.v1.bpl b/Test/snapshots/Snapshots1.v1.bpl new file mode 100644 index 00000000..c0014a03 --- /dev/null +++ b/Test/snapshots/Snapshots1.v1.bpl @@ -0,0 +1,14 @@ +procedure {:checksum "P1$proc#0"} P1(); +// Action: skip +implementation {:checksum "P1$impl#0"} P1() +{ + call P2(); +} + + +procedure {:checksum "P2$proc#0"} P2(); +// Action: verify +implementation {:checksum "P2$impl#1"} P2() +{ + assert 2 != 2; +} diff --git a/Test/snapshots/Snapshots1.v2.bpl b/Test/snapshots/Snapshots1.v2.bpl new file mode 100644 index 00000000..49e8b389 --- /dev/null +++ b/Test/snapshots/Snapshots1.v2.bpl @@ -0,0 +1,15 @@ +procedure {:checksum "P1$proc#0"} P1(); +// Action: verify +implementation {:checksum "P1$impl#0"} P1() +{ + call P2(); +} + + +procedure {:checksum "P2$proc#1"} P2(); + requires false; +// Action: verify +implementation {:checksum "P2$impl#1"} P2() +{ + assert 2 != 2; +} diff --git a/Test/snapshots/Snapshots2.v0.bpl b/Test/snapshots/Snapshots2.v0.bpl new file mode 100644 index 00000000..63f1995d --- /dev/null +++ b/Test/snapshots/Snapshots2.v0.bpl @@ -0,0 +1,12 @@ +procedure {:checksum "P0$proc#0"} P0(); +// Action: verify +implementation {:checksum "P0$impl#0"} P0() +{ + call P0(); +} + + +function F0() : bool +{ + true +} diff --git a/Test/snapshots/Snapshots2.v1.bpl b/Test/snapshots/Snapshots2.v1.bpl new file mode 100644 index 00000000..a00bdecb --- /dev/null +++ b/Test/snapshots/Snapshots2.v1.bpl @@ -0,0 +1,12 @@ +procedure {:checksum "P0$proc#0"} P0(); +// Action: skip +implementation {:checksum "P0$impl#0"} P0() +{ + call P0(); +} + + +function F0() : bool +{ + true +} diff --git a/Test/snapshots/Snapshots2.v2.bpl b/Test/snapshots/Snapshots2.v2.bpl new file mode 100644 index 00000000..02c5e6df --- /dev/null +++ b/Test/snapshots/Snapshots2.v2.bpl @@ -0,0 +1,13 @@ +procedure {:checksum "P0$proc#2"} P0(); +requires F0(); +// Action: verify (procedure changed) +implementation {:checksum "P0$impl#0"} P0() +{ + call P0(); +} + + +function {:checksum "F0#0"} F0() : bool +{ + true +} diff --git a/Test/snapshots/Snapshots2.v3.bpl b/Test/snapshots/Snapshots2.v3.bpl new file mode 100644 index 00000000..5bf59435 --- /dev/null +++ b/Test/snapshots/Snapshots2.v3.bpl @@ -0,0 +1,13 @@ +procedure {:checksum "P0$proc#2"} P0(); +requires F0(); +// Action: verify (function changed) +implementation {:checksum "P0$impl#0"} P0() +{ + call P0(); +} + + +function {:checksum "F0#1"} F0() : bool +{ + false +} diff --git a/Test/snapshots/Snapshots2.v4.bpl b/Test/snapshots/Snapshots2.v4.bpl new file mode 100644 index 00000000..3d11ee27 --- /dev/null +++ b/Test/snapshots/Snapshots2.v4.bpl @@ -0,0 +1,13 @@ +procedure {:checksum "P0$proc#2"} P0(); +requires F0(); +// Action: skip +implementation {:checksum "P0$impl#0"} P0() +{ + call P0(); +} + + +function {:checksum "F0#1"} F0() : bool +{ + false +} diff --git a/Test/snapshots/Snapshots2.v5.bpl b/Test/snapshots/Snapshots2.v5.bpl new file mode 100644 index 00000000..5ff7bb4d --- /dev/null +++ b/Test/snapshots/Snapshots2.v5.bpl @@ -0,0 +1,14 @@ +procedure {:checksum "P0$proc#5"} P0(); +requires F0(); +ensures F0(); +// Action: verify (procedure changed) +implementation {:checksum "P0$impl#0"} P0() +{ + call P0(); +} + + +function {:checksum "F0#1"} F0() : bool +{ + false +} diff --git a/Test/snapshots/runtest.bat b/Test/snapshots/runtest.bat index 05421b85..fa45d56a 100644 --- a/Test/snapshots/runtest.bat +++ b/Test/snapshots/runtest.bat @@ -1,7 +1,17 @@ + @echo off setlocal set BOOGIEDIR=..\..\Binaries set BGEXE=%BOOGIEDIR%\Boogie.exe +echo -------------------- Snapshots0.bpl -------------------- %BGEXE% %* /verifySnapshots Snapshots0.bpl + +echo. +echo -------------------- Snapshots1.bpl -------------------- +%BGEXE% %* /verifySnapshots Snapshots1.bpl + +echo. +echo -------------------- Snapshots2.bpl -------------------- +%BGEXE% %* /verifySnapshots Snapshots2.bpl -- cgit v1.2.3