From 597a558b2fde558b7f5c581481fd51258aa37c46 Mon Sep 17 00:00:00 2001
From: Valentin Wüstholz <wuestholz@gmail.com>
Date: Wed, 30 Sep 2015 21:53:31 +0200
Subject: Improve output for diagnosing timeouts.

---
 Source/ExecutionEngine/ExecutionEngine.cs  | 37 ++++++++++++++++++++++++++++--
 Source/VCGeneration/ConditionGeneration.cs | 13 ++++++++++-
 Source/VCGeneration/VC.cs                  |  1 +
 3 files changed, 48 insertions(+), 3 deletions(-)

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 15fdc081..4ab0a9c5 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -1459,11 +1459,11 @@ namespace Microsoft.Boogie
 
       printer.Inform(timeIndication + OutcomeIndication(outcome, errors), tw);
 
-      ReportOutcome(outcome, er, implName, implTok, requestId, tw, timeLimit);
+      ReportOutcome(outcome, er, implName, implTok, requestId, tw, timeLimit, errors);
     }
 
 
-    private static void ReportOutcome(VC.VCGen.Outcome outcome, ErrorReporterDelegate er, string implName, IToken implTok, string requestId, TextWriter tw, int timeLimit)
+    private static void ReportOutcome(VC.VCGen.Outcome outcome, ErrorReporterDelegate er, string implName, IToken implTok, string requestId, TextWriter tw, int timeLimit, List<Counterexample> errors)
     {
       ErrorInformation errorInfo = null;
 
@@ -1476,6 +1476,35 @@ namespace Microsoft.Boogie
           if (implName != null && implTok != null)
           {
             errorInfo = errorInformationFactory.CreateErrorInformation(implTok, string.Format("Verification timed out after {0} seconds ({1})", timeLimit, implName), requestId);
+            
+            //  Report timed out assertions as auxiliary info.
+            if (errors != null)
+            {
+              var cmpr = new CounterexampleComparer();
+              var timedOutAssertions = errors.Where(e => e.IsAuxiliaryCexForDiagnosingTimeouts).Distinct(cmpr).ToList();
+              timedOutAssertions.Sort(cmpr);
+              int idx = 1;
+              foreach (Counterexample error in timedOutAssertions)
+              {
+                var callError = error as CallCounterexample;
+                var returnError = error as ReturnCounterexample;
+                var assertError = error as AssertCounterexample;
+                IToken tok = null;
+                if (callError != null)
+                {
+                  tok = callError.FailingCall.tok;
+                }
+                else if (returnError != null)
+                {
+                  tok = returnError.FailingReturn.tok;
+                }
+                else
+                {
+                  tok = assertError.FailingAssert.tok;
+                }
+                errorInfo.AddAuxInfo(tok, string.Format("unverified assertion due to timeout ({0} of {1})", idx++, timedOutAssertions.Count));
+              }
+            }
           }
           break;
         case VCGen.Outcome.OutOfMemory:
@@ -1592,6 +1621,10 @@ namespace Microsoft.Boogie
         errors.Sort(new CounterexampleComparer());
         foreach (Counterexample error in errors)
         {
+          if (error.IsAuxiliaryCexForDiagnosingTimeouts)
+          {
+            continue;
+          }
           var errorInfo = CreateErrorInformation(error, outcome);
           errorInfo.ImplementationName = implName;
 
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 1f010757..ae0a1147 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -85,6 +85,7 @@ namespace Microsoft.Boogie {
     public string RequestId;
     public abstract byte[] Checksum { get; }
     public byte[] SugaredCmdChecksum;
+    public bool IsAuxiliaryCexForDiagnosingTimeouts;
 
     public Dictionary<TraceLocation, CalleeCounterexampleInfo> calleeCounterexamples;
 
@@ -313,7 +314,7 @@ namespace Microsoft.Boogie {
     public abstract int GetLocation();
   }
 
-  public class CounterexampleComparer : IComparer<Counterexample> {
+  public class CounterexampleComparer : IComparer<Counterexample>, IEqualityComparer<Counterexample> {
 
     private int Compare(List<Block> bs1, List<Block> bs2)
     {
@@ -375,6 +376,16 @@ namespace Microsoft.Boogie {
       }
       return -1;
     }
+
+    public bool Equals(Counterexample x, Counterexample y)
+    {
+      return Compare(x, y) == 0;
+    }
+
+    public int GetHashCode(Counterexample obj)
+    {
+      return 0;
+    }
   }
 
   public class AssertCounterexample : Counterexample {
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 94584027..33e2f928 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -2113,6 +2113,7 @@ namespace VC {
           foreach (var cmd in assertCmds)
           {
             Counterexample cex = AssertCmdToCounterexample(cmd.Item1, cmd.Item2 , new List<Block>(), null, null, context);
+            cex.IsAuxiliaryCexForDiagnosingTimeouts = true;
             callback.OnCounterexample(cex, msg);
           }
         }
-- 
cgit v1.2.3