Improve support for diagnosing timeouts.

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<int>(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<Checker>() != 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;

           }