From 216c71366e6fff4e225b68ef6ff69035c9542b4a Mon Sep 17 00:00:00 2001
From: Valentin Wüstholz <wuestholz@gmail.com>
Date: Mon, 18 May 2015 18:19:13 +0200
Subject: Add some experimental support for diagnosing timeouts.

---
 Source/VCGeneration/Check.cs        |  2 +-
 Source/VCGeneration/Context.cs      |  2 ++
 Source/VCGeneration/StratifiedVC.cs |  2 +-
 Source/VCGeneration/VC.cs           | 10 +++++++++-
 Source/VCGeneration/Wlp.cs          | 11 +++++++++++
 5 files changed, 24 insertions(+), 3 deletions(-)

(limited to 'Source/VCGeneration')

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index da8624e9..7c690eff 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -461,7 +461,7 @@ namespace Microsoft.Boogie {
         Contract.Requires(cce.NonNullElements(labels));
       }
 
-      public virtual void OnResourceExceeded(string message) {
+      public virtual void OnResourceExceeded(string message, IEnumerable<Tuple<AssertCmd, TransferCmd>> assertCmds = null) {
         Contract.Requires(message != null);
       }
 
diff --git a/Source/VCGeneration/Context.cs b/Source/VCGeneration/Context.cs
index 83787dc5..ddc34976 100644
--- a/Source/VCGeneration/Context.cs
+++ b/Source/VCGeneration/Context.cs
@@ -22,6 +22,8 @@ namespace Microsoft.Boogie
   /// </summary>
   [ContractClass(typeof(ProverContextContracts))]
   public abstract class ProverContext : ICloneable {
+    public int TimoutDiagnosticsCount { get; set; }
+    public readonly Dictionary<int, Tuple<AssertCmd, TransferCmd>> TimeoutDiagnosticIDToAssertion = new Dictionary<int, Tuple<AssertCmd, TransferCmd>>();
     protected virtual void ProcessDeclaration(Declaration decl) {Contract.Requires(decl != null);}
     public virtual void DeclareType(TypeCtorDecl t, string attributes) {Contract.Requires(t != null); ProcessDeclaration(t); }
     public virtual void DeclareConstant(Constant c, bool uniq, string attributes) {Contract.Requires(c != null); ProcessDeclaration(c); }
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index e88eb55e..69b7c8cc 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -2273,7 +2273,7 @@ namespace VC {
         return;
       }
 
-      public override void OnResourceExceeded(string message)
+      public override void OnResourceExceeded(string message, IEnumerable<Tuple<AssertCmd, TransferCmd>> assertCmds = null)
       {
           //Contract.Requires(message != null);
       }
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 560f55b4..3a483a58 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -2096,9 +2096,17 @@ namespace VC {
         return cce.NonNull((Absy)label2absy[id]);
       }
 
-      public override void OnResourceExceeded(string msg) {
+      public override void OnResourceExceeded(string msg, IEnumerable<Tuple<AssertCmd, TransferCmd>> assertCmds = null) {
         //Contract.Requires(msg != null);
         resourceExceededMessage = msg;
+        if (assertCmds != null)
+        {
+          foreach (var cmd in assertCmds)
+          {
+            Counterexample cex = AssertCmdToCounterexample(cmd.Item1, cmd.Item2 , new List<Block>(), null, null, context);
+            callback.OnCounterexample(cex, msg);
+          }
+        }
       }
 
       public override void OnProverWarning(string msg) {
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs
index 45e511f0..82d3b607 100644
--- a/Source/VCGeneration/Wlp.cs
+++ b/Source/VCGeneration/Wlp.cs
@@ -118,6 +118,17 @@ namespace VC {
           if (ac.VerifiedUnder != null)
           {
             VU = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.VerifiedUnder);
+
+            if (CommandLineOptions.Clo.RunDiagnosticsOnTimeout)
+            {
+              ctxt.Ctxt.TimeoutDiagnosticIDToAssertion[ctxt.Ctxt.TimoutDiagnosticsCount] = new Tuple<AssertCmd,TransferCmd>(ac, b.TransferCmd);
+              VU = gen.Or(VU, gen.Function(VCExpressionGenerator.TimeoutDiagnosticsOp, gen.Integer(BigNum.FromInt(ctxt.Ctxt.TimoutDiagnosticsCount++))));
+            }
+          }
+          else if (CommandLineOptions.Clo.RunDiagnosticsOnTimeout)
+          {
+            ctxt.Ctxt.TimeoutDiagnosticIDToAssertion[ctxt.Ctxt.TimoutDiagnosticsCount] = new Tuple<AssertCmd,TransferCmd>(ac, b.TransferCmd);
+            VU = gen.Function(VCExpressionGenerator.TimeoutDiagnosticsOp, gen.Integer(BigNum.FromInt(ctxt.Ctxt.TimoutDiagnosticsCount++)));
           }
           ctxt.Ctxt.BoogieExprTranslator.isPositiveContext = !ctxt.Ctxt.BoogieExprTranslator.isPositiveContext;
         }
-- 
cgit v1.2.3