From 82bf08e30124735b41ea901530ce40ef4944c9c9 Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Fri, 5 Jun 2015 12:09:49 +0200 Subject: Improve support for diagnosing timeouts. --- Source/Core/CommandLineOptions.cs | 7 ++++++ Source/ExecutionEngine/ExecutionEngine.cs | 2 +- Source/Provers/SMTLib/ProverInterface.cs | 37 ++++++++++++++++++++++++++---- Source/VCGeneration/Check.cs | 3 ++- Source/VCGeneration/ConditionGeneration.cs | 11 ++++++--- 5 files changed, 51 insertions(+), 9 deletions(-) diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 03545cbf..b9684d04 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -558,6 +558,8 @@ namespace Microsoft.Boogie { public bool WeakArrayTheory = false; public bool UseLabels = true; public bool RunDiagnosticsOnTimeout = false; + public bool TraceDiagnosticsOnTimeout = false; + public int TimeLimitPerAssertionInMs = -1; public bool SIBoolControlVC = false; public bool MonomorphicArrays { get { @@ -1477,6 +1479,10 @@ namespace Microsoft.Boogie { ps.GetNumericArgument(ref ProverKillTime); return true; + case "timeLimitPerAssertionInMs": + ps.GetNumericArgument(ref TimeLimitPerAssertionInMs); + return true; + case "smokeTimeout": ps.GetNumericArgument(ref SmokeTimeout); return true; @@ -1587,6 +1593,7 @@ namespace Microsoft.Boogie { ps.CheckBooleanFlag("doModSetAnalysis", ref DoModSetAnalysis) || ps.CheckBooleanFlag("doNotUseLabels", ref UseLabels, false) || ps.CheckBooleanFlag("runDiagnosticsOnTimeout", ref RunDiagnosticsOnTimeout) || + ps.CheckBooleanFlag("traceDiagnosticsOnTimeout", ref RunDiagnosticsOnTimeout) || ps.CheckBooleanFlag("boolControlVC", ref SIBoolControlVC, true) || ps.CheckBooleanFlag("contractInfer", ref ContractInfer) || ps.CheckBooleanFlag("explainHoudini", ref ExplainHoudini) || diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 31a69c6e..67ce49a5 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -968,7 +968,7 @@ namespace Microsoft.Boogie { semaphore.Release(); } - }, cts.Token, TaskCreationOptions.LongRunning); + }, cts.Token, TaskCreationOptions.None); tasks[taskIndex] = t; } diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index c257ea14..e9cb9a08 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -454,7 +454,7 @@ namespace Microsoft.Boogie.SMTLib ctx.KnownDatatypeConstructors.Clear(); ctx.parent = this; DeclCollector.Reset(); - SendThisVC("; doing a full reset..."); + SendThisVC("; did a full reset"); } } @@ -1266,11 +1266,19 @@ namespace Microsoft.Boogie.SMTLib { #region Run timeout diagnostics + if (CommandLineOptions.Clo.TraceDiagnosticsOnTimeout) + { + Console.Out.WriteLine("Starting timeout diagnostics with initial time limit {0}.", options.TimeLimit); + } + + var start = DateTime.UtcNow; + SendThisVC("; begin timeout diagnostics"); var unverified = new SortedSet(ctx.TimeoutDiagnosticIDToAssertion.Keys); var lastCnt = 0; var timeLimit = options.TimeLimit; + var timeLimitPerAssertion = CommandLineOptions.Clo.TimeLimitPerAssertionInMs; var timeLimitFactor = 1; var frac = 2; while (true) @@ -1320,7 +1328,9 @@ namespace Microsoft.Boogie.SMTLib if (0 < split0.Count) { - var result0 = CheckSplit(split0, ref popLater, timeLimitFactor * timeLimit); + var tl = timeLimitFactor * timeLimit; + var tla = timeLimitPerAssertion * split0.Count; + var result0 = CheckSplit(split0, ref popLater, (0 < tla && tla < tl) ? tla : tl); if (result0 == Outcome.Valid) { unverified.ExceptWith(split0); @@ -1334,8 +1344,10 @@ namespace Microsoft.Boogie.SMTLib if (0 < split1.Count) { - var stl = 0 < timeLimit ? (frac - 1) * timeLimit : timeLimit; - var result1 = CheckSplit(split1, ref popLater, timeLimitFactor * stl); + var tl = 0 < timeLimit ? (frac - 1) * timeLimit : timeLimit; + tl = timeLimitFactor * tl; + var tla = timeLimitPerAssertion * split1.Count; + var result1 = CheckSplit(split1, ref popLater, (0 < tla && tla < tl) ? tla : tl); if (result1 == Outcome.Valid) { unverified.ExceptWith(split1); @@ -1350,6 +1362,23 @@ namespace Microsoft.Boogie.SMTLib SendThisVC("; end timeout diagnostics"); + var end = DateTime.UtcNow; + + if (CommandLineOptions.Clo.TraceDiagnosticsOnTimeout) + { + Console.Out.WriteLine("Terminated timeout diagnostics after {0:F0} ms.", end.Subtract(start).TotalMilliseconds); + Console.Out.WriteLine("Outcome: {0}", result); + Console.Out.WriteLine("Unverified assertions: {0} (of {1})", unverified.Count, ctx.TimeoutDiagnosticIDToAssertion.Keys.Count); + + string filename = "unknown"; + var assertion = ctx.TimeoutDiagnosticIDToAssertion.Values.Select(t => t.Item1).FirstOrDefault(a => a.tok != null && a.tok != Token.NoToken && a.tok.filename != null); + if (assertion != null) + { + filename = assertion.tok.filename; + } + File.AppendAllText("timeouts.csv", string.Format(";{0};{1};{2:F0};{3};{4};{5}\n", filename, options.TimeLimit, end.Subtract(start).TotalMilliseconds, result, unverified.Count, ctx.TimeoutDiagnosticIDToAssertion.Keys.Count)); + } + #endregion } diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index 7c690eff..33baf798 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -217,6 +217,7 @@ namespace Microsoft.Boogie { private void Setup(Program prog, ProverContext ctx) { Program = prog; + // TODO(wuestholz): Is this lock necessary? lock (Program.TopLevelDeclarations) { foreach (Declaration decl in Program.TopLevelDeclarations) @@ -362,7 +363,7 @@ namespace Microsoft.Boogie { thmProver.BeginCheck(descriptiveName, vc, handler); // gen.ClearSharedFormulas(); PR: don't know yet what to do with this guy - ProverTask = Task.Factory.StartNew(() => { WaitForOutput(null); } , TaskCreationOptions.LongRunning); + ProverTask = Task.Factory.StartNew(() => { WaitForOutput(null); }, TaskCreationOptions.LongRunning); } public ProverInterface.Outcome ReadOutcome() { diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index a19f983a..8d6606b6 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -983,11 +983,11 @@ namespace VC { #endregion - protected Checker FindCheckerFor(int timeout, bool isBlocking = true) + protected Checker FindCheckerFor(int timeout, bool isBlocking = true, int waitTimeinMs = 50, int maxRetries = 3) { + Contract.Requires(0 <= waitTimeinMs && 0 <= maxRetries); Contract.Ensures(!isBlocking || Contract.Result() != null); - var maxRetries = 3; lock (checkers) { retry: @@ -1015,6 +1015,8 @@ namespace VC { else { checkers.RemoveAt(i); + i--; + continue; } } } @@ -1029,7 +1031,10 @@ namespace VC { { if (isBlocking || 0 < maxRetries) { - Monitor.Wait(checkers, 50); + if (0 < waitTimeinMs) + { + Monitor.Wait(checkers, waitTimeinMs); + } maxRetries--; goto retry; } -- cgit v1.2.3