Support verification coverage in batch mode (#792)

Previously, the batch mode prover interface (selected with `-proverOpt:BATCH_MODE=true`) didn't support extracting unsat cores and therefore didn't support tracking verification coverage. This PR fixes that issue.
boogie-org · Oct 6, 2023 · afe8eb0 · afe8eb0
1 parent a74325d
commit afe8eb0
Show file tree

Hide file tree

Showing 4 changed files with 21 additions and 24 deletions.
diff --git a/Source/Provers/SMTLib/SMTLibBatchTheoremProver.cs b/Source/Provers/SMTLib/SMTLibBatchTheoremProver.cs
@@ -143,6 +143,9 @@ private async Task<Outcome> CheckSat(CancellationToken cancellationToken)
         requests.Add($"(get-info :{Z3.RlimitOption})");
       }
       requests.Add("(get-model)");
+      if (options.LibOptions.ProduceUnsatCores) {
+        requests.Add($"(get-unsat-core)");
+      }
 
       if (Process == null || HadErrors) {
         return Outcome.Undetermined;
@@ -176,6 +179,11 @@ private async Task<Outcome> CheckSat(CancellationToken cancellationToken)
         var modelSExp = responseStack.Pop();
         errorModel = ParseErrorModel(modelSExp);
 
+        if (options.LibOptions.ProduceUnsatCores) {
+          var unsatCoreSExp = responseStack.Pop();
+          ReportCoveredElements(unsatCoreSExp);
+        }
+
         if (result == Outcome.Invalid) {
           var labels = CalculatePath(currentErrorHandler.StartingProcId(), errorModel);
           if (labels.Length == 0) {

diff --git a/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs b/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs
@@ -18,7 +18,6 @@ public class SMTLibInteractiveTheoremProver : SMTLibProcessTheoremProver
     private bool processNeedsRestart;
     private ScopedNamer commonNamer;
     private ScopedNamer finalNamer;
-    private ISet<string> usedNamedAssumes;
 
     [NotDelayed]
     public SMTLibInteractiveTheoremProver(SMTLibOptions libOptions, SMTLibSolverOptions options, VCExpressionGenerator gen,
@@ -181,7 +180,6 @@ public override void FullReset(VCExpressionGenerator generator)
       ctx.parent = this;
       DeclCollector.Reset();
       NamedAssumes.Clear();
-      usedNamedAssumes = null;
       SendThisVC("; did a full reset");
     }
 
@@ -218,28 +216,8 @@ public async Task<Outcome> CheckSat(CancellationToken cancellationToken,
           {
             if (usingUnsatCore)
             {
-              usedNamedAssumes = new HashSet<string>();
               var resp = await SendVcRequest("(get-unsat-core)").WaitAsync(cancellationToken);
-              if (resp.Name != "")
-              {
-                usedNamedAssumes.Add(resp.Name);
-                if (libOptions.TrackVerificationCoverage) {
-                  reporter.AddCoveredElement(TrackedNodeComponent.ParseSolverString(resp.Name.Substring("aux$$assume$$".Length)));
-                }
-              }
-
-              foreach (var arg in resp.Arguments)
-              {
-                usedNamedAssumes.Add(arg.Name);
-                if (libOptions.TrackVerificationCoverage)
-                {
-                  reporter.AddCoveredElement(TrackedNodeComponent.ParseSolverString(arg.Name.Substring("aux$$assume$$".Length)));
-                }
-              }
-            }
-            else
-            {
-              usedNamedAssumes = null;
+              ReportCoveredElements(resp);
             }
           }
 

diff --git a/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs b/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs
@@ -1484,6 +1484,18 @@ private static Dictionary<string, object> ParseArrayFromArrayExpr(SExpr resp)
       return dict.Count > 0 ? dict : null;
     }
 
+    protected void ReportCoveredElements(SExpr unsatCoreSExp) {
+      if (libOptions.TrackVerificationCoverage && unsatCoreSExp.Name != "") {
+        currentErrorHandler.AddCoveredElement(TrackedNodeComponent.ParseSolverString(unsatCoreSExp.Name.Substring("aux$$assume$$".Length)));
+      }
+
+      foreach (var arg in unsatCoreSExp.Arguments) {
+        if (libOptions.TrackVerificationCoverage) {
+          currentErrorHandler.AddCoveredElement(TrackedNodeComponent.ParseSolverString(arg.Name.Substring("aux$$assume$$".Length)));
+        }
+      }
+    }
+
     protected List<string> ParseUnsatCore(string resp)
     {
       if (resp == "" || resp == "()")

diff --git a/Test/coverage/verificationCoverage.bpl b/Test/coverage/verificationCoverage.bpl
@@ -99,7 +99,6 @@
 // RUN: %diff "%s.expect" "%t.coverage-d"
 // RUN: %boogie -trackVerificationCoverage -normalizeNames:1 -prune "%s" > "%t.coverage-n"
 // RUN: %diff "%s.expect" "%t.coverage-n"
-// UNSUPPORTED: batch_mode
 
 procedure testRequiresAssign(n: int)
   requires {:id "r0"} n > 0; // covered