From 21f1cfff139759d9b9f91ed800da2158daca8ed4 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 27 Aug 2015 20:10:41 -0700 Subject: Added /verifySnapshots:3, which prints recycled errors messages with the source locations of the new code. --- Source/Core/CommandLineOptions.cs | 6 ++- Source/ExecutionEngine/ExecutionEngine.cs | 45 ++++++++++------------- Source/ExecutionEngine/VerificationResultCache.cs | 44 ++++++---------------- Source/VCGeneration/VC.cs | 40 ++++++++++++++++++-- 4 files changed, 73 insertions(+), 62 deletions(-) (limited to 'Source') diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index be371fcb..a17ff9c7 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -1492,7 +1492,7 @@ namespace Microsoft.Boogie { return true; case "verifySnapshots": - ps.GetNumericArgument(ref VerifySnapshots, 3); + ps.GetNumericArgument(ref VerifySnapshots, 4); return true; case "traceCaching": @@ -1944,6 +1944,10 @@ namespace Microsoft.Boogie { 0 - do not use any verification result caching (default) 1 - use the basic verification result caching 2 - use the more advanced verification result caching + 3 - use the more advanced caching and report errors according + to the new source locations for errors and their + related locations (but not /errorTrace and CaptureState + locations) /verifySeparately verify each input program separately /removeEmptyBlocks: diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 67ce49a5..a408642a 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -151,25 +151,18 @@ namespace Microsoft.Boogie { Contract.Requires(message != null); - if (category != null) - { + if (category != null) { message = string.Format("{0}: {1}", category, message); } string s; - if (tok != null) - { + if (tok != null) { s = string.Format("{0}({1},{2}): {3}", ExecutionEngine.GetFileNameForConsole(tok.filename), tok.line, tok.col, message); - } - else - { + } else { s = message; } - if (error) - { + if (error) { ErrorWriteLine(tw, s); - } - else - { + } else { tw.WriteLine(s); } } @@ -1114,23 +1107,23 @@ namespace Microsoft.Boogie printer.Inform(string.Format("Verifying {0} ...", impl.Name), output); int priority = 0; - if (0 < CommandLineOptions.Clo.VerifySnapshots) - { - verificationResult = Cache.Lookup(impl, out priority); - } - var wasCached = false; - if (verificationResult != null && priority == Priority.SKIP) - { - if (CommandLineOptions.Clo.XmlSink != null) - { - CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, verificationResult.Start); - } + if (0 < CommandLineOptions.Clo.VerifySnapshots) { + var cachedResults = Cache.Lookup(impl, out priority); + if (cachedResults != null && priority == Priority.SKIP) { + if (CommandLineOptions.Clo.XmlSink != null) { + CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, cachedResults.Start); + } - printer.Inform(string.Format("Retrieving cached verification result for implementation {0}...", impl.Name), output); - wasCached = true; + printer.Inform(string.Format("Retrieving cached verification result for implementation {0}...", impl.Name), output); + if (CommandLineOptions.Clo.VerifySnapshots < 3 || cachedResults.Outcome == ConditionGeneration.Outcome.Correct) { + verificationResult = cachedResults; + wasCached = true; + } + } } - else + + if (!wasCached) { #region Verify the implementation diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs index a18cee05..f8aca0e9 100644 --- a/Source/ExecutionEngine/VerificationResultCache.cs +++ b/Source/ExecutionEngine/VerificationResultCache.cs @@ -172,48 +172,28 @@ namespace Microsoft.Boogie var vr = ExecutionEngine.Cache.Lookup(impl, out priority); if (vr != null && vr.ProgramId == programId) { - if (priority == Priority.LOW) - { + if (priority == Priority.LOW) { run.LowPriorityImplementationCount++; - if (TimeThreshold < vr.End.Subtract(vr.Start).TotalMilliseconds) - { - SetErrorAndAssertionChecksumsInCachedSnapshot(impl, vr); - if (vr.ProgramId != null) - { - var p = ExecutionEngine.CachedProgram(vr.ProgramId); - if (p != null) - { - eai.Inject(impl, p); - run.TransformedImplementationCount++; - } - } - } - } - else if (priority == Priority.MEDIUM) - { + } else if (priority == Priority.MEDIUM) { run.MediumPriorityImplementationCount++; - if (TimeThreshold < vr.End.Subtract(vr.Start).TotalMilliseconds) - { + } else if (priority == Priority.HIGH) { + run.HighPriorityImplementationCount++; + } else if (priority == Priority.SKIP) { + run.SkippedImplementationCount++; + } + + if (priority == Priority.LOW || priority == Priority.MEDIUM || 3 <= CommandLineOptions.Clo.VerifySnapshots) { + if (TimeThreshold < vr.End.Subtract(vr.Start).TotalMilliseconds) { SetErrorAndAssertionChecksumsInCachedSnapshot(impl, vr); - if (vr.ProgramId != null) - { + if (vr.ProgramId != null) { var p = ExecutionEngine.CachedProgram(vr.ProgramId); - if (p != null) - { + if (p != null) { eai.Inject(impl, p); run.TransformedImplementationCount++; } } } } - else if (priority == Priority.HIGH) - { - run.HighPriorityImplementationCount++; - } - else if (priority == Priority.SKIP) - { - run.SkippedImplementationCount++; - } } } run.End = DateTime.UtcNow; diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 3a483a58..8e5c853c 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1763,9 +1763,18 @@ namespace VC { { var checksum = a.Checksum; var oldCex = impl.ErrorChecksumToCachedError[checksum] as Counterexample; - if (oldCex != null) - { - callback.OnCounterexample(oldCex, null); + if (oldCex != null) { + if (CommandLineOptions.Clo.VerifySnapshots < 3) { + callback.OnCounterexample(oldCex, null); + } else { + // If possible, we use the old counterexample, but with the location information of "a" + var cex = AssertCmdToCloneCounterexample(a, oldCex); + callback.OnCounterexample(cex, null); + // OnCounterexample may have had side effects on the RequestId and OriginalRequestId fields. We make + // any such updates available in oldCex. (Is this really a good design? --KRML) + oldCex.RequestId = cex.RequestId; + oldCex.OriginalRequestId = cex.OriginalRequestId; + } } } } @@ -3137,6 +3146,31 @@ namespace VC { } } + /// + /// Returns a clone of "cex", but with the location stored in "cex" replaced by those from "assrt". + /// + public static Counterexample AssertCmdToCloneCounterexample(AssertCmd assrt, Counterexample cex) { + Contract.Requires(assrt != null); + Contract.Requires(cex != null); + Contract.Ensures(Contract.Result() != null); + + List relatedInformation = new List(); + + Counterexample cc; + if (assrt is AssertRequiresCmd) { + var aa = (AssertRequiresCmd)assrt; + cc = new CallCounterexample(cex.Trace, aa.Call, aa.Requires, cex.Model, cex.MvInfo, cex.Context, aa.Checksum); + } else if (assrt is AssertEnsuresCmd && cex is ReturnCounterexample) { + var aa = (AssertEnsuresCmd)assrt; + var oldCex = (ReturnCounterexample)cex; + cc = new ReturnCounterexample(cex.Trace, oldCex.FailingReturn, aa.Ensures, cex.Model, cex.MvInfo, cex.Context, aa.Checksum); + } else { + cc = new AssertCounterexample(cex.Trace, assrt, cex.Model, cex.MvInfo, cex.Context); + } + cc.relatedInformation = relatedInformation; + return cc; + } + static VCExpr LetVC(Block startBlock, VCExpr controlFlowVariableExpr, Dictionary label2absy, -- cgit v1.2.3