Add some experimental support for diagnosing timeouts.

8 files changed, 186 insertions, 3 deletions

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index dbbb6fd0..03545cbf 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -557,6 +557,7 @@ namespace Microsoft.Boogie {
     public bool UseSmtOutputFormat = false;

     public bool WeakArrayTheory = false;

     public bool UseLabels = true;

+    public bool RunDiagnosticsOnTimeout = false;

     public bool SIBoolControlVC = false;

     public bool MonomorphicArrays {

       get {

@@ -1585,6 +1586,7 @@ namespace Microsoft.Boogie {
               ps.CheckBooleanFlag("weakArrayTheory", ref WeakArrayTheory) || 

               ps.CheckBooleanFlag("doModSetAnalysis", ref DoModSetAnalysis) ||

               ps.CheckBooleanFlag("doNotUseLabels", ref UseLabels, false) ||

+              ps.CheckBooleanFlag("runDiagnosticsOnTimeout", ref RunDiagnosticsOnTimeout) ||

               ps.CheckBooleanFlag("boolControlVC", ref SIBoolControlVC, true) ||

               ps.CheckBooleanFlag("contractInfer", ref ContractInfer) ||

               ps.CheckBooleanFlag("explainHoudini", ref ExplainHoudini) ||

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 868b9ee3..4a9ba929 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -30,6 +30,8 @@ namespace Microsoft.Boogie.SMTLib
     private readonly SMTLibProverOptions options;

     private bool usingUnsatCore;

     private RPFP rpfp = null;

+    private string currentVC;

+    private string currentDescriptiveName;

 

     [ContractInvariantMethod]

     void ObjectInvariant()

@@ -261,6 +263,11 @@ namespace Microsoft.Boogie.SMTLib
           SendCommon("(assert (and (tickleBool true) (tickleBool false)))");

         }

 

+        if (CommandLineOptions.Clo.RunDiagnosticsOnTimeout)

+        {

+          SendCommon("(declare-fun timeoutDiagnostics (Int) Bool)");

+        }

+

         if (ctx.KnownDatatypeConstructors.Count > 0)

         {

           GraphUtil.Graph<CtorType> dependencyGraph = new GraphUtil.Graph<CtorType>();

@@ -393,7 +400,10 @@ namespace Microsoft.Boogie.SMTLib
       }

 

       PrepareCommon();

+

       string vcString = "(assert (not\n" + VCExpr2String(vc, 1) + "\n))";

+      currentVC = vcString;

+      currentDescriptiveName = descriptiveName;

       FlushAxioms();

 

       PossiblyRestart();

@@ -1246,6 +1256,7 @@ namespace Microsoft.Boogie.SMTLib
         var globalResult = Outcome.Undetermined;

 

         while (true) {

+          bool popLater = false;

           errorsLeft--;

           string[] labels = null;

 

@@ -1254,6 +1265,111 @@ namespace Microsoft.Boogie.SMTLib
             globalResult = result;

 

           if (result == Outcome.Invalid || result == Outcome.TimeOut || result == Outcome.OutOfMemory) {

+

+            if (CommandLineOptions.Clo.RunDiagnosticsOnTimeout && (result == Outcome.TimeOut || result == Outcome.OutOfMemory))

+            {

+              SendThisVC("; begin timeout diagnostics");

+

+              var verified = new bool[Context.TimoutDiagnosticsCount];

+              var lastCnt = verified.Length + 1;

+              var mod = 2;

+              while (true)

+              {

+                var split0 = verified.ToArray();

+                var split1 = verified.ToArray();

+                int cnt0 = 0;

+                int cnt1 = 0;

+                for (int i = 0; i < split0.Length; i++)

+                {

+                  if (!split0[i])

+                  {

+                    // TODO(wuestholz): Try out different ways for splitting up the work.

+                    if ((cnt0 + cnt1) % mod == 0)

+                    {

+                      split0[i] = true;

+                      cnt1++;

+                    }

+                    else

+                    {

+                      split1[i] = true;

+                      cnt0++;

+                    }

+                  }

+                }

+

+                bool doReset = false;

+                var cnt = cnt0 + cnt1;

+                if (cnt == 0)

+                {

+                  return Outcome.Valid;

+                }

+                else if (lastCnt <= cnt)

+                {

+                  doReset = true;

+                  if (mod < cnt)

+                  {

+                    mod++;

+                  }

+                  else

+                  {

+                    // Give up and report which assertions were not verified.

+                    var cmds = new List<Tuple<AssertCmd, TransferCmd>>();

+                    for (int i = 0; i < verified.Length; i++)

+                    {

+                      if (!verified[i])

+                      {

+                        cmds.Add(ctx.TimeoutDiagnosticIDToAssertion[i]);

+                      }

+                    }

+

+                    if (cmds.Any())

+                    {

+                      handler.OnResourceExceeded("timeout after running diagnostics", cmds);

+                    }

+

+                    break;

+                  }

+                }

+                lastCnt = cnt;

+

+                if (0 < cnt0)

+                {

+                  var result0 = CheckSplit(split0, cnt0, ref popLater, doReset);

+                  if (result0 == Outcome.Valid)

+                  {

+                    for (int i = 0; i < split0.Length; i++)

+                    {

+                      verified[i] = verified[i] || !split0[i];

+                    }

+                  }

+                  else if (result0 == Outcome.Invalid)

+                  {

+                    result = result0;

+                    break;

+                  }

+                }

+

+                if (0 < cnt1)

+                {

+                  var result1 = CheckSplit(split1, cnt1, ref popLater, doReset);

+                  if (result1 == Outcome.Valid)

+                  {

+                    for (int i = 0; i < split1.Length; i++)

+                    {

+                      verified[i] = verified[i] || !split1[i];

+                    }

+                  }

+                  else if (result1 == Outcome.Invalid)

+                  {

+                    result = result1;

+                    break;

+                  }

+                }

+              }

+

+              SendThisVC("; end timeout diagnostics");

+            }

+

             IList<string> xlabels;

             if (CommandLineOptions.Clo.UseLabels) {

               labels = GetLabelsInfo();

@@ -1301,6 +1417,11 @@ namespace Microsoft.Boogie.SMTLib
             SendThisVC("(assert (not (= (ControlFlow 0 " + source + ") (- " + target + "))))");

             SendThisVC("(check-sat)");

           }

+

+          if (popLater)

+          {

+            SendThisVC("(pop 1)");

+          }

         }

 

         FlushLogFile();

@@ -1315,6 +1436,43 @@ namespace Microsoft.Boogie.SMTLib
       }

     }

 

+    private Outcome CheckSplit(bool[] split, int unverifiedCount, ref bool popLater, bool doReset = false)

+    {

+      if (doReset)

+      {

+        Reset(gen);

+        PossiblyRestart();

+        SendThisVC("(push 1)");

+        SendThisVC("(set-info :boogie-vc-id " + SMTLibNamer.QuoteId(currentDescriptiveName) + ")");

+        SendThisVC(currentVC);

+        popLater = false;

+      }

+      else

+      {

+        if (popLater)

+        {

+          SendThisVC("(pop 1)");

+        }

+        SendThisVC("(push 1)");

+        SendThisVC(string.Format("(set-option :{0} {1})", Z3.SetTimeoutOption(), options.TimeLimit));

+        popLater = true;

+      }

+      SendThisVC(string.Format("; checking split VC with {0} unverified assertions", unverifiedCount));

+      var expr = VCExpressionGenerator.True;

+      for (int i = 0; i < split.Length; i++)

+      {

+        var lit = VCExprGen.Function(VCExpressionGenerator.TimeoutDiagnosticsOp, VCExprGen.Integer(Microsoft.Basetypes.BigNum.FromInt(i)));

+        if (!split[i]) {

+          lit = VCExprGen.Not(lit);

+        }

+        expr = VCExprGen.AndSimp(expr, lit);

+      }

+      SendThisVC("(assert " + VCExpr2String(expr, 1) + ")");

+      FlushLogFile();

+      SendThisVC("(check-sat)");

+      return GetResponse();

+    }

+

     public override string[] CalculatePath(int controlFlowConstant) {

       SendThisVC("(get-value ((ControlFlow " + controlFlowConstant + " 0)))");

       var path = new List<string>();

diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs
index 4f8dc08e..15573f5b 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -339,6 +339,8 @@ namespace Microsoft.Boogie {
 

     public static readonly VCExprOp TickleBoolOp = new VCExprCustomOp("tickleBool", 1, Type.Bool);

 

+    public static readonly VCExprOp TimeoutDiagnosticsOp = new VCExprCustomOp("timeoutDiagnostics", 1, Type.Bool);

+

     public VCExprOp BoogieFunctionOp(Function func) {

       Contract.Requires(func != null);

       Contract.Ensures(Contract.Result<VCExprOp>() != null);

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;

         }