diff options
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 2 | ||||
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 38 | ||||
| -rw-r--r-- | Source/ExecutionEngine/VerificationResultCache.cs | 5 |
3 files changed, 37 insertions, 8 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index e9e6b60e..60e0bdc0 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -389,6 +389,7 @@ namespace Microsoft.Boogie { public bool Trace = false;
public bool TraceTimes = false;
public bool TraceProofObligations = false;
+ public bool TraceCaching = false;
public bool NoResolve = false;
public bool NoTypecheck = false;
public bool OverlookBoogieTypeErrors = false;
@@ -1392,6 +1393,7 @@ namespace Microsoft.Boogie { ps.CheckBooleanFlag("wait", ref Wait) ||
ps.CheckBooleanFlag("trace", ref Trace) ||
ps.CheckBooleanFlag("traceTimes", ref TraceTimes) ||
+ ps.CheckBooleanFlag("traceCaching", ref TraceCaching) ||
ps.CheckBooleanFlag("tracePOs", ref TraceProofObligations) ||
ps.CheckBooleanFlag("noResolve", ref NoResolve) ||
ps.CheckBooleanFlag("noTypecheck", ref NoTypecheck) ||
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index b5f4f87b..44b8719a 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -417,6 +417,10 @@ namespace Microsoft.Boogie static List<Checker> Checkers = new List<Checker>();
+ static DateTime FirstRequestStart;
+
+ static readonly ConcurrentDictionary<string, TimeSpan> TimePerRequest = new ConcurrentDictionary<string, TimeSpan>();
+
static readonly ConcurrentDictionary<string, CancellationTokenSource> ImplIdToCancellationTokenSource = new ConcurrentDictionary<string, CancellationTokenSource>();
static readonly ConcurrentDictionary<string, CancellationTokenSource> RequestIdToCancellationTokenSource = new ConcurrentDictionary<string, CancellationTokenSource>();
@@ -810,6 +814,8 @@ namespace Microsoft.Boogie requestId = FreshRequestId();
}
+ var start = DateTime.UtcNow;
+
#region Do some pre-abstract-interpretation preprocessing on the program
// Doing lambda expansion before abstract interpretation means that the abstract interpreter
// never needs to see any lambda expressions. (On the other hand, if it were useful for it
@@ -993,6 +999,33 @@ namespace Microsoft.Boogie {
program.FreezeTopLevelDeclarations();
programCache.Set(programId, program, policy);
+
+ if (CommandLineOptions.Clo.TraceCaching)
+ {
+ Console.Out.WriteLine("");
+ Console.Out.WriteLine("<trace caching>");
+
+ var end = DateTime.UtcNow;
+ if (TimePerRequest.Count == 0)
+ {
+ FirstRequestStart = start;
+ }
+ TimePerRequest[requestId] = end.Subtract(start);
+
+ Console.Out.WriteLine(CachedVerificationResultInjector.Statistics.Output(true));
+
+ Console.Out.WriteLine("Times per request as CSV:");
+ Console.Out.WriteLine("Request ID, Time (ms)");
+ foreach (var kv in TimePerRequest.OrderBy(kv => kv.Key))
+ {
+ Console.Out.WriteLine("{0}, {1:F0}", kv.Key, kv.Value.TotalMilliseconds);
+ }
+
+ Console.Out.WriteLine("");
+ Console.Out.WriteLine("Total time (ms) since first request: {0:F0}", end.Subtract(FirstRequestStart).TotalMilliseconds);
+
+ Console.Out.WriteLine("</trace caching>");
+ }
}
#endregion
@@ -1394,11 +1427,6 @@ namespace Microsoft.Boogie printer.Inform(timeIndication + OutcomeIndication(outcome, errors), tw);
- if (1 < CommandLineOptions.Clo.VerifySnapshots && CommandLineOptions.Clo.Trace)
- {
- printer.Inform(CachedVerificationResultInjector.Statistics.Output(CommandLineOptions.Clo.TraceTimes), tw);
- }
-
ReportOutcome(outcome, er, implName, implTok, requestId, tw, timeLimit);
}
diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs index 67d6dde5..215731b0 100644 --- a/Source/ExecutionEngine/VerificationResultCache.cs +++ b/Source/ExecutionEngine/VerificationResultCache.cs @@ -37,7 +37,6 @@ namespace Microsoft.Boogie public string Output(bool printTime = false)
{
var wr = new StringWriter();
- wr.WriteLine("");
wr.WriteLine("Cached verification result injector statistics as CSV:");
if (printTime)
{
@@ -47,11 +46,11 @@ namespace Microsoft.Boogie {
wr.WriteLine("Request ID, Rewritten Implementations, Low Priority Implementations, Medium Priority Implementations, High Priority Implementations, Skipped Implementations, Implementations");
}
- foreach (var kv in runs)
+ foreach (var kv in runs.OrderBy(kv => kv.Key))
{
if (printTime)
{
- wr.WriteLine("{0}, {1}, {2}, {3}, {4}, {5}, {6}, {7}", 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);
+ wr.WriteLine("{0}, {1:F0}, {2}, {3}, {4}, {5}, {6}, {7}", 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
{
|