Add /warnVacuousProofs option

atomb · atomb · commit 1c749a62d0f9 · 2025-04-22T14:47:28.000-07:00
This option enables `/trackVerificationCoverage` and automatically warns
if it detects vacuous proofs. This is intended for the less-common case
where a front end doesn't add IDs to program elements and then post-
process the results.
diff --git a/Source/ExecutionEngine/CommandLineOptions.cs b/Source/ExecutionEngine/CommandLineOptions.cs
@@ -322,6 +322,15 @@ public bool TrackVerificationCoverage {
       set => trackVerificationCoverage = value;
     }
 
+    public bool WarnVacuousProofs
+    {
+      get => warnVacuousProofs;
+      set {
+        warnVacuousProofs = value;
+        if (warnVacuousProofs) { trackVerificationCoverage = true; }
+      }
+    }
+
     public int InlineDepth  { get; set; } = -1;
 
     public bool UseProverEvaluate {
@@ -605,6 +614,7 @@ void ObjectInvariant5()
     private bool normalizeNames;
     private bool normalizeDeclarationOrder = true;
     private bool keepQuantifier = false;
+    private bool warnVacuousProofs;
 
     public List<CoreOptions.ConcurrentHoudiniOptions> Cho { get; set; } = new();
 
@@ -1373,6 +1383,7 @@ protected override bool ParseOption(string name, CommandLineParseState ps)
               ps.CheckBooleanFlag("useUnsatCoreForContractInfer", x => useUnsatCoreForContractInfer = x) ||
               ps.CheckBooleanFlag("printAssignment", x => PrintAssignment = x) ||
               ps.CheckBooleanFlag("trackVerificationCoverage", x => trackVerificationCoverage = x) ||
+              ps.CheckBooleanFlag("warnVacuousProofs", x => WarnVacuousProofs = x) ||
               ps.CheckBooleanFlag("useProverEvaluate", x => useProverEvaluate = x) ||
               ps.CheckBooleanFlag("deterministicExtractLoops", x => DeterministicExtractLoops = x) ||
               ps.CheckBooleanFlag("verifySeparately", x => VerifySeparately = x) ||
@@ -2005,7 +2016,11 @@ Track and report which program elements labeled with an
                 assignments, and calls can be labeled for inclusion in this
                 report. This generalizes and replaces the previous
                 (undocumented) `/printNecessaryAssertions` option.
-
+  /warnVacuousProofs
+                Automatically add `{:id ...}` attributes to assumptions, assertions,
+                requires clauses, ensures clauses, and calls; enable the
+                `/trackVerificationCoverage` option; and warn when proof goals are
+                not covered by a proof.
   /keepQuantifier
                 If pool-based quantifier instantiation creates instances of a quantifier
                 then keep the quantifier along with the instances. By default, the quantifier
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -611,6 +611,9 @@ private Task<ProcessedProgram> PreProcessProgramVerification(Program program, Ca
         }
 
         var processedProgram = Options.ExtractLoops ? ExtractLoops(program) : new ProcessedProgram(program);
+        if (Options.WarnVacuousProofs) {
+          processedProgram = AddVacuityChecking(processedProgram);
+        }
 
         if (Options.PrintInstrumented)
         {
@@ -635,6 +638,55 @@ private ProcessedProgram ExtractLoops(Program program)
       });
     }
 
+    private ProcessedProgram AddVacuityChecking(ProcessedProgram processedProgram)
+    {
+      Program program = processedProgram.Program;
+      CoverageAnnotator annotator = new CoverageAnnotator();
+      foreach (var impl in program.Implementations) {
+        annotator.VisitImplementation(impl);
+      }
+      return new ProcessedProgram(program, (vcgen, impl, result) =>
+        {
+          CheckVacuity(annotator, impl, result);
+          processedProgram.PostProcessResult(vcgen, impl, result);
+        }
+      );
+    }
+
+    private void CheckVacuity(CoverageAnnotator annotator, Implementation impl, ImplementationRunResult verificationResult)
+    {
+      var covered = verificationResult
+        .RunResults
+        .SelectMany(r => r.CoveredElements)
+        .ToHashSet();
+      foreach (var goalId in annotator.GetImplementationGoalIds(impl.Name)) {
+        if (!CoveredId(goalId, covered)) {
+          var node = annotator.GetIdNode(goalId);
+          Options.Printer.AdvisoryWriteLine(Options.OutputWriter,
+            $"{node.tok.filename}({node.tok.line},{node.tok.col - 1}): Warning: Proved vacuously");
+        }
+      }
+    }
+
+    private static bool CoveredId(string goalId, HashSet<TrackedNodeComponent> covered)
+    {
+      foreach (var component in covered) {
+        if (component is LabeledNodeComponent { id: var id } && id == goalId) {
+          return true;
+        }
+
+        if (component is TrackedInvariantEstablished { invariantId: var eid } && eid == goalId) {
+          return true;
+        }
+
+        if (component is TrackedInvariantMaintained { invariantId: var mid } && mid == goalId) {
+          return true;
+        }
+      }
+
+      return false;
+    }
+
     private Implementation[] GetPrioritizedImplementations(Program program)
     {
       var impls = program.Implementations.Where(
@@ -964,7 +1016,6 @@ private Task<ImplementationRunResult> VerifyImplementationWithLargeThread(Proces
       return resultTask;
     }
 
-
     #region Houdini
 
     private async Task<PipelineOutcome> RunHoudini(Program program, PipelineStatistics stats, ErrorReporterDelegate er,
diff --git a/Source/Provers/SMTLib/SMTLibOptions.cs b/Source/Provers/SMTLib/SMTLibOptions.cs
@@ -14,6 +14,7 @@ public interface SMTLibOptions : CoreOptions
     bool ImmediatelyAcceptCommands { get; }
     bool RunningBoogieFromCommandLine { get; }
     bool TrackVerificationCoverage { get; }
+    bool WarnVacuousProofs { get; }
     string ProverPreamble { get; }
     bool TraceDiagnosticsOnTimeout { get; }
     uint TimeLimitPerAssertionInPercent { get; }
diff --git a/Test/coverage/verificationCoverage.bpl.expect-trace b/Test/coverage/verificationCoverage.bpl.expect-trace
@@ -0,0 +1,129 @@
+Parsing verificationCoverage.bpl
+Coalescing blocks...
+Inlining...
+
+Verifying testRequiresAssign ...
+[TRACE] Using prover: z3
+Proof dependencies:
+  a0
+  id0
+  id1
+  id2
+
+Verifying sum ...
+Proof dependencies:
+  id10
+  id7
+  id8
+  id9
+  invariant id4 assumed in body
+  invariant id4 established
+  invariant id4 maintained
+  invariant id5 assumed in body
+  invariant id5 established
+  invariant id5 maintained
+  invariant id6 established
+  invariant id6 maintained
+
+Verifying contradictoryAssume ...
+Proof dependencies:
+  id11
+  id12
+verificationCoverage.bpl(143,4): Warning: Proved vacuously
+
+Verifying falseRequires ...
+Proof dependencies:
+  id16
+verificationCoverage.bpl(150,4): Warning: Proved vacuously
+
+Verifying contradictoryRequires ...
+Proof dependencies:
+  id19
+  id20
+verificationCoverage.bpl(158,4): Warning: Proved vacuously
+
+Verifying assumeFalse ...
+Proof dependencies:
+  id21
+verificationCoverage.bpl(163,2): Warning: Proved vacuously
+
+Verifying testEnsuresCallee ...
+Proof dependencies:
+  id23
+  id24
+  id25
+
+Verifying testEnsuresCaller ...
+Proof dependencies:
+  ensures clause id23 from call id26
+  ensures clause id23 from call id27
+  ensures clause id24 from call id27
+  id28
+  id29
+  id30
+  requires clause id25 proved for call id26
+  requires clause id25 proved for call id27
+  xy_sum
+
+Verifying obviouslyUnconstrainedCode ...
+Proof dependencies:
+  constrained
+  id31
+  id32
+
+Verifying callContradictoryFunction ...
+Proof dependencies:
+  ensures clause cont_ens_abs from call id34
+  id36
+  requires clause xpos_abs proved for call id34
+verificationCoverage.bpl(203,2): Warning: Proved vacuously
+
+Verifying usesSomeInteger ...
+Proof dependencies:
+  id37
+  someInteger_value_axiom
+Proof dependencies of whole program:
+  a0
+  constrained
+  ensures clause cont_ens_abs from call id34
+  ensures clause id23 from call id26
+  ensures clause id23 from call id27
+  ensures clause id24 from call id27
+  id0
+  id1
+  id10
+  id11
+  id12
+  id16
+  id19
+  id2
+  id20
+  id21
+  id23
+  id24
+  id25
+  id28
+  id29
+  id30
+  id31
+  id32
+  id36
+  id37
+  id7
+  id8
+  id9
+  invariant id4 assumed in body
+  invariant id4 established
+  invariant id4 maintained
+  invariant id5 assumed in body
+  invariant id5 established
+  invariant id5 maintained
+  invariant id6 established
+  invariant id6 maintained
+  requires clause id25 proved for call id26
+  requires clause id25 proved for call id27
+  requires clause xpos_abs proved for call id34
+  someInteger_value_axiom
+  xy_sum
+
+Boogie program verifier finished with 11 verified, 0 errors
