From 8f64d5c104efe69c5d561c1b22c3e1320bba04fa Mon Sep 17 00:00:00 2001 From: Valentin Wüstholz Date: Mon, 8 Jun 2015 00:15:01 +0200 Subject: Improve support for diagnosing timeouts. --- Source/Core/CommandLineOptions.cs | 6 +- Source/Provers/SMTLib/ProverInterface.cs | 131 ++++++++++++++----------------- 2 files changed, 64 insertions(+), 73 deletions(-) (limited to 'Source') diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 675ac6a5..be371fcb 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -559,7 +559,7 @@ namespace Microsoft.Boogie { public bool UseLabels = true; public bool RunDiagnosticsOnTimeout = false; public bool TraceDiagnosticsOnTimeout = false; - public int TimeLimitPerAssertionInMs = -1; + public int TimeLimitPerAssertionInPercent = 20; public bool SIBoolControlVC = false; public bool MonomorphicArrays { get { @@ -1479,8 +1479,8 @@ namespace Microsoft.Boogie { ps.GetNumericArgument(ref ProverKillTime); return true; - case "timeLimitPerAssertionInMs": - ps.GetNumericArgument(ref TimeLimitPerAssertionInMs); + case "timeLimitPerAssertionInPercent": + ps.GetNumericArgument(ref TimeLimitPerAssertionInPercent, a => 0 < a); return true; case "smokeTimeout": diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index e9cb9a08..afb38986 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -1271,102 +1271,90 @@ namespace Microsoft.Boogie.SMTLib Console.Out.WriteLine("Starting timeout diagnostics with initial time limit {0}.", options.TimeLimit); } - var start = DateTime.UtcNow; - SendThisVC("; begin timeout diagnostics"); + var start = DateTime.UtcNow; 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; + var timedOut = new SortedSet(); + int frac = 2; + int queries = 0; + int timeLimitPerAssertion = 0 < options.TimeLimit ? (options.TimeLimit / 100) * CommandLineOptions.Clo.TimeLimitPerAssertionInPercent : 1000; while (true) { - int cnt = unverified.Count; - if (cnt == 0) + int rem = unverified.Count; + if (rem == 0) { - result = Outcome.Valid; - break; - } - - if (lastCnt == cnt) - { - if (frac < (cnt / 2)) + if (0 < timedOut.Count) { - frac *= 2; - } - else if (0 < timeLimit && timeLimitFactor <= 4) - { - // TODO(wuestholz): Add a commandline option to control this. - timeLimitFactor *= 2; - } - else - { - // Give up and report which assertions were not verified. - var cmds = unverified.Select(id => ctx.TimeoutDiagnosticIDToAssertion[id]); - - if (cmds.Any()) + result = CheckSplit(timedOut, ref popLater, options.TimeLimit, timeLimitPerAssertion, ref queries); + if (result == Outcome.Valid) { - handler.OnResourceExceeded("timeout after running diagnostics", cmds); + timedOut.Clear(); } + else if (result == Outcome.TimeOut) + { + // Give up and report which assertions were not verified. + var cmds = timedOut.Select(id => ctx.TimeoutDiagnosticIDToAssertion[id]); - break; + if (cmds.Any()) + { + handler.OnResourceExceeded("timeout after running diagnostics", cmds); + } + } } + else + { + result = Outcome.Valid; + } + break; } - else - { - frac = 2; - timeLimitFactor = 1; - } - lastCnt = cnt; // TODO(wuestholz): Try out different ways for splitting up the work (e.g., randomly). - var cnt0 = cnt / frac; - var split0 = new SortedSet(unverified.Where((val, idx) => idx < cnt0)); - var split1 = new SortedSet(unverified.Except(split0)); - - if (0 < split0.Count) + var split = new SortedSet(unverified.Where((val, idx) => idx < ((rem - 1) / frac + 1))); + Contract.Assert(0 < split.Count); + var splitRes = CheckSplit(split, ref popLater, timeLimitPerAssertion, timeLimitPerAssertion, ref queries); + if (splitRes == Outcome.Valid) { - 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); - } - else if (result0 == Outcome.Invalid) - { - result = result0; - break; - } + unverified.ExceptWith(split); + frac = 1; } - - if (0 < split1.Count) + else if (splitRes == Outcome.Invalid) + { + result = splitRes; + break; + } + else if (splitRes == Outcome.TimeOut) { - 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) + if (1 < frac && frac <= (rem / 4)) { - unverified.ExceptWith(split1); + frac *= 4; } - else if (result1 == Outcome.Invalid) + else if (frac <= (rem / 2)) { - result = result1; - break; + frac *= 2; + } + else + { + timedOut.UnionWith(split); + unverified.ExceptWith(split); + frac = 1; } } + else + { + break; + } } - SendThisVC("; end timeout diagnostics"); + unverified.UnionWith(timedOut); var end = DateTime.UtcNow; + SendThisVC("; end timeout diagnostics"); + if (CommandLineOptions.Clo.TraceDiagnosticsOnTimeout) { - Console.Out.WriteLine("Terminated timeout diagnostics after {0:F0} ms.", end.Subtract(start).TotalMilliseconds); + Console.Out.WriteLine("Terminated timeout diagnostics after {0:F0} ms and {1} prover queries.", end.Subtract(start).TotalMilliseconds, queries); Console.Out.WriteLine("Outcome: {0}", result); Console.Out.WriteLine("Unverified assertions: {0} (of {1})", unverified.Count, ctx.TimeoutDiagnosticIDToAssertion.Keys.Count); @@ -1376,7 +1364,7 @@ namespace Microsoft.Boogie.SMTLib { 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)); + File.AppendAllText("timeouts.csv", string.Format(";{0};{1};{2:F0};{3};{4};{5};{6}\n", filename, options.TimeLimit, end.Subtract(start).TotalMilliseconds, queries, result, unverified.Count, ctx.TimeoutDiagnosticIDToAssertion.Keys.Count)); } #endregion @@ -1453,15 +1441,17 @@ namespace Microsoft.Boogie.SMTLib } } - private Outcome CheckSplit(SortedSet split, ref bool popLater, int timeLimit) + private Outcome CheckSplit(SortedSet split, ref bool popLater, int timeLimit, int timeLimitPerAssertion, ref int queries) { + var tla = timeLimitPerAssertion * split.Count; + if (popLater) { SendThisVC("(pop 1)"); } SendThisVC("(push 1)"); - SendThisVC(string.Format("(set-option :{0} {1})", Z3.SetTimeoutOption(), timeLimit)); + SendThisVC(string.Format("(set-option :{0} {1})", Z3.SetTimeoutOption(), (0 < tla && tla < timeLimit) ? tla : timeLimit)); popLater = true; SendThisVC(string.Format("; checking split VC with {0} unverified assertions", split.Count)); @@ -1481,6 +1471,7 @@ namespace Microsoft.Boogie.SMTLib } FlushLogFile(); SendThisVC("(check-sat)"); + queries++; return GetResponse(); } -- cgit v1.2.3