Added ability to cancel the program verification.

dafny-lang · Nov 9, 2020 · 0d7b55d · 0d7b55d
1 parent aa2829d
commit 0d7b55d
Showing 1 changed file with 10 additions and 3 deletions.
diff --git a/Source/DafnyLS/Language/DafnyProgramVerifier.cs b/Source/DafnyLS/Language/DafnyProgramVerifier.cs
@@ -61,11 +61,11 @@ public async Task VerifyAsync(Microsoft.Dafny.Program program, CancellationToken
       // It appears that boogie is thread-safe.
       foreach(var (_, boogieProgram) in translated) {
         cancellationToken.ThrowIfCancellationRequested();
-        VerifyWithBoogie(boogieProgram, program.reporter);
+        VerifyWithBoogie(boogieProgram, program.reporter, cancellationToken);
       }
     }
 
-    private void VerifyWithBoogie(Microsoft.Boogie.Program program, ErrorReporter reporter) {
+    private void VerifyWithBoogie(Microsoft.Boogie.Program program, ErrorReporter reporter, CancellationToken cancellationToken) {
       program.Resolve();
       program.Typecheck();
 
@@ -76,7 +76,14 @@ private void VerifyWithBoogie(Microsoft.Boogie.Program program, ErrorReporter re
       // TODO Are the programId and requestId of any relevance?
       var uniqueId = Guid.NewGuid().ToString();
       // TODO any use of the verification state?
-      ExecutionEngine.InferAndVerify(program, new PipelineStatistics(), uniqueId, error => CaptureVerificationError(reporter, error), uniqueId);
+      using(cancellationToken.Register(() => CancelVerification(uniqueId))) { 
+        ExecutionEngine.InferAndVerify(program, new PipelineStatistics(), uniqueId, error => CaptureVerificationError(reporter, error), uniqueId);
+      }
+    }
+
+    private void CancelVerification(string requestId) {
+      _logger.LogDebug("requesting verification cancellation of {}", requestId);
+      ExecutionEngine.CancelRequest(requestId);
     }
 
     private void CaptureVerificationError(ErrorReporter reporter, ErrorInformation error) {