From 5edb0b7cdaeae035968945cfda687c2ba1d7967a Mon Sep 17 00:00:00 2001 From: wuestholz Date: Sun, 2 Nov 2014 15:33:12 +0100 Subject: Made it produce more trace output for the verification result caching. --- Source/ExecutionEngine/ExecutionEngine.cs | 24 +++++------------- Source/ExecutionEngine/VerificationResultCache.cs | 31 ++++++++--------------- 2 files changed, 17 insertions(+), 38 deletions(-) (limited to 'Source/ExecutionEngine') diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 0c027f5c..eb871ac3 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -196,6 +196,7 @@ namespace Microsoft.Boogie public int InconclusiveCount; public int TimeoutCount; public int OutOfMemoryCount; + public long[] CachingActionCounts; } @@ -914,7 +915,7 @@ namespace Microsoft.Boogie if (1 < CommandLineOptions.Clo.VerifySnapshots) { - CachedVerificationResultInjector.Inject(program, stablePrioritizedImpls, requestId, programId); + CachedVerificationResultInjector.Inject(program, stablePrioritizedImpls, requestId, programId, out stats.CachingActionCounts); } #region Verify each implementation @@ -1035,25 +1036,13 @@ namespace Microsoft.Boogie Console.Out.WriteLine(CachedVerificationResultInjector.Statistics.Output(printTimes)); Console.Out.WriteLine("Statistics per request as CSV:"); - if (printTimes) - { - Console.Out.WriteLine("Request ID, Time (ms), Error, Inconclusive, Out of Memory, Timeout, Verified"); - } - else - { - Console.Out.WriteLine("Request ID, Error, Inconclusive, Out of Memory, Timeout, Verified"); - } + Console.Out.WriteLine("Request ID{0}, Error, Inconclusive, Out of Memory, Timeout, Verified, DoNothing, MarkAsPartiallyVerified, MarkAsFullyVerified, RecycleError, AssumeNegationOfAssumptionVariable, Drop", printTimes ? ", Time (ms)" : ""); foreach (var kv in TimePerRequest.OrderBy(kv => ExecutionEngine.AutoRequestId(kv.Key))) { var s = StatisticsPerRequest[kv.Key]; - if (printTimes) - { - Console.Out.WriteLine("{0,-19}, {1,8:F0}, {2,2}, {3,2}, {4,2}, {5,2}, {6,2}", kv.Key, kv.Value.TotalMilliseconds, s.ErrorCount, s.InconclusiveCount, s.OutOfMemoryCount, s.TimeoutCount, s.VerifiedCount); - } - else - { - Console.Out.WriteLine("{0,-19}, {2,2}, {3,2}, {4,2}, {5,2}, {6,2}", kv.Key, kv.Value.TotalMilliseconds, s.ErrorCount, s.InconclusiveCount, s.OutOfMemoryCount, s.TimeoutCount, s.VerifiedCount); - } + var cacs = s.CachingActionCounts; + var t = printTimes ? string.Format(", {0,8:F0}", kv.Value.TotalMilliseconds) : ""; + Console.Out.WriteLine("{0,-19}{1}, {2,2}, {3,2}, {4,2}, {5,2}, {6,2}, {7,3}, {8,3}, {9,3}, {10,3}, {11,3}, {12,3}", kv.Key, t, s.ErrorCount, s.InconclusiveCount, s.OutOfMemoryCount, s.TimeoutCount, s.VerifiedCount, cacs[0], cacs[1], cacs[2], cacs[3], cacs[4], cacs[5]); } if (printTimes) @@ -1138,6 +1127,7 @@ namespace Microsoft.Boogie using (var vcgen = CreateVCGen(program, checkers)) { + vcgen.CachingActionCounts = stats.CachingActionCounts; verificationResult.ProofObligationCountBefore = vcgen.CumulativeAssertionCount; verificationResult.Start = DateTime.UtcNow; diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs index 091ccc25..c75bd52f 100644 --- a/Source/ExecutionEngine/VerificationResultCache.cs +++ b/Source/ExecutionEngine/VerificationResultCache.cs @@ -16,12 +16,13 @@ namespace Microsoft.Boogie { public DateTime Start { get; internal set; } public DateTime End { get; internal set; } - public int RewrittenImplementationCount { get; internal set; } + public int TransformedImplementationCount { get; internal set; } public int ImplementationCount { get; internal set; } public int SkippedImplementationCount { get; set; } public int LowPriorityImplementationCount { get; set; } public int MediumPriorityImplementationCount { get; set; } public int HighPriorityImplementationCount { get; set; } + public long[] CachingActionCounts { get; set; } } @@ -40,24 +41,11 @@ namespace Microsoft.Boogie if (runs.Any()) { wr.WriteLine("Cached verification result injector statistics as CSV:"); - if (printTime) - { - wr.WriteLine("Request ID, Time (ms), Rewritten Implementations, Low Priority Implementations, Medium Priority Implementations, High Priority Implementations, Skipped Implementations, Implementations"); - } - else - { - wr.WriteLine("Request ID, Rewritten Implementations, Low Priority Implementations, Medium Priority Implementations, High Priority Implementations, Skipped Implementations, Implementations"); - } + wr.WriteLine("Request ID, Transformed, Low, Medium, High, Skipped{0}", printTime ? ", Time (ms)" : ""); foreach (var kv in runs.OrderBy(kv => ExecutionEngine.AutoRequestId(kv.Key))) { - if (printTime) - { - wr.WriteLine("{0,-19}, {1,5:F0}, {2,3}, {3,3}, {4,3}, {5,3}, {6,3}, {7,3}", kv.Key, kv.Value.End.Subtract(kv.Value.Start).TotalMilliseconds, kv.Value.RewrittenImplementationCount, kv.Value.LowPriorityImplementationCount, kv.Value.MediumPriorityImplementationCount, kv.Value.HighPriorityImplementationCount, kv.Value.SkippedImplementationCount, kv.Value.ImplementationCount); - } - else - { - wr.WriteLine("{0,-19}, {1,3}, {2,3}, {3,3}, {4,3}, {5,3}, {6,3}", kv.Key, kv.Value.RewrittenImplementationCount, kv.Value.LowPriorityImplementationCount, kv.Value.MediumPriorityImplementationCount, kv.Value.HighPriorityImplementationCount, kv.Value.SkippedImplementationCount, kv.Value.ImplementationCount); - } + var t = printTime ? string.Format(", {0,8:F0}", kv.Value.End.Subtract(kv.Value.Start).TotalMilliseconds) : ""; + wr.WriteLine("{0,-19}, {1,3}, {2,3}, {3,3}, {4,3}, {5,3}{6}", kv.Key, kv.Value.TransformedImplementationCount, kv.Value.LowPriorityImplementationCount, kv.Value.MediumPriorityImplementationCount, kv.Value.HighPriorityImplementationCount, kv.Value.SkippedImplementationCount, t); } } return wr.ToString(); @@ -114,11 +102,12 @@ namespace Microsoft.Boogie return result; } - public static void Inject(Program program, IEnumerable implementations, string requestId, string programId) + public static void Inject(Program program, IEnumerable implementations, string requestId, string programId, out long[] cachingActionCounts) { var eai = new CachedVerificationResultInjector(program, implementations); - var run = new CachedVerificationResultInjectorRun { Start = DateTime.UtcNow, ImplementationCount = implementations.Count() }; + cachingActionCounts = new long[Enum.GetNames(typeof(VC.ConditionGeneration.CachingAction)).Length]; + var run = new CachedVerificationResultInjectorRun { Start = DateTime.UtcNow, ImplementationCount = implementations.Count(), CachingActionCounts = cachingActionCounts }; foreach (var impl in implementations) { int priority; @@ -137,7 +126,7 @@ namespace Microsoft.Boogie if (p != null) { eai.Inject(impl, p); - run.RewrittenImplementationCount++; + run.TransformedImplementationCount++; } } } @@ -154,7 +143,7 @@ namespace Microsoft.Boogie if (p != null) { eai.Inject(impl, p); - run.RewrittenImplementationCount++; + run.TransformedImplementationCount++; } } } -- cgit v1.2.3