From cb4d41266301c26b9c863561df57ffd30ae0ec6f Mon Sep 17 00:00:00 2001 From: wuestholz Date: Sat, 18 Oct 2014 00:10:25 +0200 Subject: Made it produce more trace output for the verification result caching. --- Source/ExecutionEngine/ExecutionEngine.cs | 36 ++++++++++++++------- Source/ExecutionEngine/VerificationResultCache.cs | 39 ++++++++++++++++------- 2 files changed, 53 insertions(+), 22 deletions(-) (limited to 'Source/ExecutionEngine') diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index e0c3e006..76caa5d3 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -1017,11 +1017,8 @@ namespace Microsoft.Boogie programCache.Set(programId, program, policy); } - if (0 <= CommandLineOptions.Clo.VerifySnapshots && CommandLineOptions.Clo.TraceCaching) + if (0 <= CommandLineOptions.Clo.VerifySnapshots && 2 <= CommandLineOptions.Clo.TraceCaching) { - Console.Out.WriteLine(""); - Console.Out.WriteLine(""); - var end = DateTime.UtcNow; if (TimePerRequest.Count == 0) { @@ -1030,20 +1027,37 @@ namespace Microsoft.Boogie TimePerRequest[requestId] = end.Subtract(start); StatisticsPerRequest[requestId] = stats; - Console.Out.WriteLine(CachedVerificationResultInjector.Statistics.Output(true)); + var printTimes = 3 <= CommandLineOptions.Clo.TraceCaching; + + Console.Out.WriteLine(CachedVerificationResultInjector.Statistics.Output(printTimes)); Console.Out.WriteLine("Statistics per request as CSV:"); - Console.Out.WriteLine("Request ID, Time (ms), Error, Inconclusive, Out of Memory, Timeout, Verified"); + 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"); + } foreach (var kv in TimePerRequest.OrderBy(kv => ExecutionEngine.AutoRequestId(kv.Key))) { var s = StatisticsPerRequest[kv.Key]; - 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); + 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); + } } - Console.Out.WriteLine(""); - Console.Out.WriteLine("Total time (ms) since first request: {0:F0}", end.Subtract(FirstRequestStart).TotalMilliseconds); - - Console.Out.WriteLine(""); + if (printTimes) + { + Console.Out.WriteLine(""); + Console.Out.WriteLine("Total time (ms) since first request: {0:F0}", end.Subtract(FirstRequestStart).TotalMilliseconds); + } } #endregion diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs index ba995cba..268ab9bd 100644 --- a/Source/ExecutionEngine/VerificationResultCache.cs +++ b/Source/ExecutionEngine/VerificationResultCache.cs @@ -39,7 +39,7 @@ namespace Microsoft.Boogie var wr = new StringWriter(); if (runs.Any()) { - wr.WriteLine("Cached verification result injector statistics as CSV:"); + wr.WriteLine("\nCached 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"); @@ -269,7 +269,30 @@ namespace Microsoft.Boogie var assumed = new AssignCmd(Token.NoToken, new List { lhs }, new List { rhs }); after.Add(assumed); } + node.ExtendDesugaring(before, beforePrecondtionCheck, after); + if (1 <= CommandLineOptions.Clo.TraceCaching) + { + using (var tokTxtWr = new TokenTextWriter("", Console.Out, false, false)) + { + Console.Out.WriteLine("\nFor call to {0} in {1}:", node.Proc.Name, currentImplementation.Name); + foreach (var b in before) + { + Console.Out.Write("+ Added before: "); + b.Emit(tokTxtWr, 0); + } + foreach (var b in beforePrecondtionCheck) + { + Console.Out.Write("+ Added before precondition check: "); + b.Emit(tokTxtWr, 0); + } + foreach (var a in after) + { + Console.Out.Write("+ Added after: "); + a.Emit(tokTxtWr, 0); + } + } + } } return result; @@ -295,12 +318,9 @@ namespace Microsoft.Boogie } var end = DateTime.UtcNow; - if (CommandLineOptions.Clo.TraceCaching) + if (3 <= CommandLineOptions.Clo.TraceCaching) { - Console.Out.WriteLine(""); - Console.Out.WriteLine(""); - Console.Out.WriteLine("Collected other definition axioms within {0:F0} ms.", end.Subtract(start).TotalMilliseconds); - Console.Out.WriteLine(""); + Console.Out.WriteLine("\nCollected other definition axioms within {0:F0} ms.", end.Subtract(start).TotalMilliseconds); } } @@ -346,12 +366,9 @@ namespace Microsoft.Boogie dc.VisitProgram(program); var end = DateTime.UtcNow; - if (CommandLineOptions.Clo.TraceCaching) + if (3 <= CommandLineOptions.Clo.TraceCaching) { - Console.Out.WriteLine(""); - Console.Out.WriteLine(""); - Console.Out.WriteLine("Collected dependencies within {0:F0} ms.", end.Subtract(start).TotalMilliseconds); - Console.Out.WriteLine(""); + Console.Out.WriteLine("\nCollected dependencies within {0:F0} ms.", end.Subtract(start).TotalMilliseconds); } } -- cgit v1.2.3