fix: Cancellation tokens to cancel and restart checkers

Source/ExecutionEngine/ExecutionEngine.cs

@@ -1207,9 +1207,9 @@ private static void VerifyImplementation(Program program, PipelineStatistics sta
             CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, verificationResult.Start);
           }
 
-          try
-          {
-            verificationResult.Outcome = vcgen.VerifyImplementation(impl, out verificationResult.Errors, requestId);
+          try {
+            var cancellationToken = RequestIdToCancellationTokenSource[requestId].Token;
+            verificationResult.Outcome = vcgen.VerifyImplementation(impl, out verificationResult.Errors, requestId, cancellationToken);
             if (CommandLineOptions.Clo.ExtractLoops && verificationResult.Errors != null)
             {
               var vcg = vcgen as VCGen;

Source/Houdini/Checker.cs

@@ -5,6 +5,7 @@
 using Microsoft.BaseTypes;
 using VC;
 using System.Linq;
+using System.Threading;
 
 namespace Microsoft.Boogie.Houdini
 {
@@ -256,7 +257,7 @@ public ProverInterface.Outcome Verify(ProverInterface proverInterface, Dictionar
 
       VCExpr vc = proverInterface.VCExprGen.Implies(BuildAxiom(proverInterface, assignment), conjecture);
       proverInterface.BeginCheck(descriptiveName, vc, handler);
-      ProverInterface.Outcome proverOutcome = proverInterface.CheckOutcome(handler, errorLimit);
+      ProverInterface.Outcome proverOutcome = proverInterface.CheckOutcome(handler, errorLimit, CancellationToken.None).Result;
 
       double queryTime = (DateTime.UtcNow - now).TotalSeconds;
       stats.proverTime += queryTime;
@@ -388,8 +389,8 @@ public void Explain(ProverInterface proverInterface,
       do
       {
         hardAssumptions.Add(controlExprNoop);
-        outcome = proverInterface.CheckAssumptions(hardAssumptions, softAssumptions, out var unsatisfiedSoftAssumptions,
-          handler);
+        (outcome, var unsatisfiedSoftAssumptions) = proverInterface.CheckAssumptions(hardAssumptions, softAssumptions, 
+          handler, CancellationToken.None).Result;
         hardAssumptions.RemoveAt(hardAssumptions.Count - 1);
 
         if (outcome == ProverInterface.Outcome.TimeOut || outcome == ProverInterface.Outcome.OutOfMemory ||
@@ -423,9 +424,8 @@ public void Explain(ProverInterface proverInterface,
           hardAssumptions.Add(softAssumptions[i]);
         }
 
-        var unsatisfiedSoftAssumptions2 = new List<int>();
-        outcome = proverInterface.CheckAssumptions(hardAssumptions, softAssumptions2, out unsatisfiedSoftAssumptions2,
-          handler);
+        (outcome, var unsatisfiedSoftAssumptions2) = proverInterface.CheckAssumptions(hardAssumptions, softAssumptions2, 
+          handler, CancellationToken.None).Result;
 
         if (outcome == ProverInterface.Outcome.TimeOut || outcome == ProverInterface.Outcome.OutOfMemory ||
             outcome == ProverInterface.Outcome.OutOfResource || outcome == ProverInterface.Outcome.Undetermined)
@@ -506,7 +506,7 @@ public void UpdateUnsatCore(ProverInterface proverInterface, Dictionary<Variable
         assumptionExprs.Add(exprTranslator.LookupVariable(v));
       }
 
-      ProverInterface.Outcome tmp = proverInterface.CheckAssumptions(assumptionExprs, out var unsatCore, handler);
+      (ProverInterface.Outcome tmp, var unsatCore) = proverInterface.CheckAssumptions(assumptionExprs, handler, CancellationToken.None).Result;
       System.Diagnostics.Debug.Assert(tmp == ProverInterface.Outcome.Valid);
       unsatCoreSet = new HashSet<Variable>();
       foreach (int i in unsatCore)

Source/Provers/SMTLib/NoopSolver.cs

@@ -1,4 +1,6 @@
 using System;
+using System.Threading;
+using System.Threading.Tasks;
 
 namespace Microsoft.Boogie.SMTLib;
 
@@ -34,11 +36,11 @@ public override void Send(string cmd)
     }
   }
 
-  public override SExpr GetProverResponse()
+  public override Task<SExpr> GetProverResponse(CancellationToken cancellationToken)
   {
     var result = response;
     response = null;
-    return result;
+    return Task.FromResult(result);
   }
 
   public override void NewProblem(string descriptiveName)

Source/Provers/SMTLib/SMTLibProcess.cs

@@ -6,6 +6,7 @@
 using System.IO;
 using System.Threading;
 using System.Diagnostics.Contracts;
+using System.Threading.Tasks;
 
 namespace Microsoft.Boogie.SMTLib
 {
@@ -118,82 +119,67 @@ internal Inspector Inspector
       get { return inspector; }
     }
 
-    public override SExpr GetProverResponse()
+    public override Task<SExpr> GetProverResponse(CancellationToken cancellationToken)
     {
-      toProver.Flush();
+      return Task.Factory.StartNew(GetProverResponseSync, cancellationToken);
+    }
 
-      while (true)
-      {
-        var exprs = ParseSExprs(true).ToArray();
-        Contract.Assert(exprs.Length <= 1);
-        if (exprs.Length == 0)
-        {
-          return null;
-        }
+    private SExpr GetProverResponseSync()
+    {
+      toProver.Flush();
 
-        var resp = exprs[0];
-        if (resp.Name == "error")
-        {
-          if (resp.Arguments.Length == 1 && resp.Arguments[0].IsId)
-          {
-            if (resp.Arguments[0].Name.Contains("max. resource limit exceeded"))
-            {
-              return resp;
-            }
-            else {
-              HandleError(resp.Arguments[0].Name);
-              return null;
-            }
-          }
-          else {
-            HandleError(resp.ToString());
+      lock (this) {
+        while (true) {
+          var exprs = ParseSExprs(true).ToArray();
+          Contract.Assert(exprs.Length <= 1);
+          if (exprs.Length == 0) {
             return null;
           }
-        }
-        else if (resp.Name == "progress")
-        {
-          if (inspector != null)
-          {
-            var sb = new StringBuilder();
-            foreach (var a in resp.Arguments)
-            {
-              if (a.Name == "labels")
-              {
-                sb.Append("STATS LABELS");
-                foreach (var x in a.Arguments)
-                {
-                  sb.Append(" ").Append(x.Name);
-                }
+
+          var resp = exprs[0];
+          if (resp.Name == "error") {
+            if (resp.Arguments.Length == 1 && resp.Arguments[0].IsId) {
+              if (resp.Arguments[0].Name.Contains("max. resource limit exceeded")) {
+                return resp;
+              } else {
+                HandleError(resp.Arguments[0].Name);
+                return null;
               }
-              else if (a.Name.StartsWith(":"))
-              {
-                sb.Append("STATS NAMED_VALUES ").Append(a.Name);
-                foreach (var x in a.Arguments)
-                {
-                  sb.Append(" ").Append(x.Name);
+            } else {
+              HandleError(resp.ToString());
+              return null;
+            }
+          } else if (resp.Name == "progress") {
+            if (inspector != null) {
+              var sb = new StringBuilder();
+              foreach (var a in resp.Arguments) {
+                if (a.Name == "labels") {
+                  sb.Append("STATS LABELS");
+                  foreach (var x in a.Arguments) {
+                    sb.Append(" ").Append(x.Name);
+                  }
+                } else if (a.Name.StartsWith(":")) {
+                  sb.Append("STATS NAMED_VALUES ").Append(a.Name);
+                  foreach (var x in a.Arguments) {
+                    sb.Append(" ").Append(x.Name);
+                  }
+                } else {
+                  continue;
                 }
-              }
-              else
-              {
-                continue;
-              }
 
-              inspector.StatsLine(sb.ToString());
-              sb.Clear();
+                inspector.StatsLine(sb.ToString());
+                sb.Clear();
+              }
             }
+          } else if (resp.Name == "unsupported") {
+            // Skip -- this may be a benign "unsupported" from a previous command.
+            // Of course, this is suboptimal.  We should really be using
+            // print-success to identify the errant command and determine whether
+            // the response is benign.
+          } else {
+            return resp;
           }
         }
-        else if (resp.Name == "unsupported")
-        {
-          // Skip -- this may be a benign "unsupported" from a previous command.
-          // Of course, this is suboptimal.  We should really be using
-          // print-success to identify the errant command and determine whether
-          // the response is benign.
-        }
-        else
-        {
-          return resp;
-        }
       }
     }
 
@@ -428,29 +414,26 @@ string ReadProver()
           error = null;
         }
 
-        lock (this)
+        while (proverOutput.Count == 0 && proverErrors.Count == 0 && !prover.HasExited)
         {
-          while (proverOutput.Count == 0 && proverErrors.Count == 0 && !prover.HasExited)
-          {
-            Monitor.Wait(this, 100);
-          }
+          Monitor.Wait(this, 100);
+        }
 
-          if (proverErrors.Count > 0)
-          {
-            error = proverErrors.Dequeue();
-            continue;
-          }
+        if (proverErrors.Count > 0)
+        {
+          error = proverErrors.Dequeue();
+          continue;
+        }
 
-          if (proverOutput.Count > 0)
-          {
-            return proverOutput.Dequeue();
-          }
+        if (proverOutput.Count > 0)
+        {
+          return proverOutput.Dequeue();
+        }
 
-          if (prover.HasExited)
-          {
-            DisposeProver();
-            return null;
-          }
+        if (prover.HasExited)
+        {
+          DisposeProver();
+          return null;
         }
       }
     }