diff options
| author |  wuestholz <unknown> | 2015-01-26 16:34:54 +0100 |
|---|---|---|
| committer | wuestholz <unknown> | 2015-01-26 16:34:54 +0100 |
| commit | 40537b5a8339208370894ef0771d288fda351068 (patch) | |
| tree | 38e0d7f0db0473293dac9f636a5284198e96673b | |
| parent | ca82edae68c55548b70530f02a7d346870aece04 (diff) | |
Worked on the verification result caching (trace output).
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 23 | ||||
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 4 | ||||
| -rw-r--r-- | Source/ExecutionEngine/VerificationResultCache.cs | 6 | ||||
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 15 |
4 files changed, 35 insertions, 13 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 072e0323..3559e0c9 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -431,7 +431,28 @@ namespace Microsoft.Boogie { public bool Trace = false;
public bool TraceTimes = false;
public bool TraceProofObligations = false;
- public int TraceCaching = 0;
+ public bool TraceCachingForTesting
+ {
+ get
+ {
+ return TraceCaching == 1 || TraceCaching == 3;
+ }
+ }
+ public bool TraceCachingForBenchmarking
+ {
+ get
+ {
+ return TraceCaching == 2 || TraceCaching == 3;
+ }
+ }
+ public bool TraceCachingForDebugging
+ {
+ get
+ {
+ return TraceCaching == 3;
+ }
+ }
+ internal int TraceCaching = 0;
public bool NoResolve = false;
public bool NoTypecheck = false;
public bool OverlookBoogieTypeErrors = false;
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index c0d66720..0874addc 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -1020,7 +1020,7 @@ namespace Microsoft.Boogie programCache.Set(programId, program, policy);
}
- if (0 <= CommandLineOptions.Clo.VerifySnapshots && 2 <= CommandLineOptions.Clo.TraceCaching)
+ if (0 <= CommandLineOptions.Clo.VerifySnapshots && CommandLineOptions.Clo.TraceCachingForBenchmarking)
{
var end = DateTime.UtcNow;
if (TimePerRequest.Count == 0)
@@ -1030,7 +1030,7 @@ namespace Microsoft.Boogie TimePerRequest[requestId] = end.Subtract(start);
StatisticsPerRequest[requestId] = stats;
- var printTimes = 3 <= CommandLineOptions.Clo.TraceCaching;
+ var printTimes = true;
Console.Out.WriteLine(CachedVerificationResultInjector.Statistics.Output(printTimes));
diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs index 48b5a94d..5d20e6e8 100644 --- a/Source/ExecutionEngine/VerificationResultCache.cs +++ b/Source/ExecutionEngine/VerificationResultCache.cs @@ -247,7 +247,7 @@ namespace Microsoft.Boogie }
node.ExtendDesugaring(before, beforePrecondtionCheck, after);
- if (1 <= CommandLineOptions.Clo.TraceCaching)
+ if (CommandLineOptions.Clo.TraceCachingForTesting || CommandLineOptions.Clo.TraceCachingForBenchmarking)
{
using (var tokTxtWr = new TokenTextWriter("<console>", Console.Out, false, false))
{
@@ -376,7 +376,7 @@ namespace Microsoft.Boogie }
var end = DateTime.UtcNow;
- if (3 <= CommandLineOptions.Clo.TraceCaching)
+ if (CommandLineOptions.Clo.TraceCachingForDebugging)
{
Console.Out.WriteLine("Collected other definition axioms within {0:F0} ms.", end.Subtract(start).TotalMilliseconds);
}
@@ -425,7 +425,7 @@ namespace Microsoft.Boogie dc.VisitProgram(program);
var end = DateTime.UtcNow;
- if (3 <= CommandLineOptions.Clo.TraceCaching)
+ if (CommandLineOptions.Clo.TraceCachingForDebugging)
{
Console.Out.WriteLine("Collected dependencies within {0:F0} ms.", end.Subtract(start).TotalMilliseconds);
}
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index bc535404..d72a9d0e 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -1328,12 +1328,12 @@ namespace VC { var end = DateTime.UtcNow;
- if (3 <= CommandLineOptions.Clo.TraceCaching)
+ if (CommandLineOptions.Clo.TraceCachingForDebugging)
{
Console.Out.WriteLine("Turned implementation into passive commands within {0:F0} ms.\n", end.Subtract(start).TotalMilliseconds);
}
- if (2 <= CommandLineOptions.Clo.TraceCaching)
+ if (CommandLineOptions.Clo.TraceCachingForDebugging)
{
using (var tokTxtWr = new TokenTextWriter("<console>", Console.Out, false, false))
{
@@ -1480,7 +1480,7 @@ namespace VC { void TraceCachingAction(Cmd cmd, CachingAction action)
{
- if (1 <= CommandLineOptions.Clo.TraceCaching)
+ if (CommandLineOptions.Clo.TraceCachingForTesting)
{
using (var tokTxtWr = new TokenTextWriter("<console>", Console.Out, false, false))
{
@@ -1489,10 +1489,11 @@ namespace VC { cmd.Emit(tokTxtWr, 0);
Console.Out.WriteLine(" >>> {0}", action);
}
- if (CachingActionCounts != null)
- {
- Interlocked.Increment(ref CachingActionCounts[(int)action]);
- }
+ }
+
+ if (CommandLineOptions.Clo.TraceCachingForBenchmarking && CachingActionCounts != null)
+ {
+ Interlocked.Increment(ref CachingActionCounts[(int)action]);
}
}
|