Add /warnVacuousProofs option

Source/Core/CoverageAnnotator.cs

@@ -0,0 +1,115 @@
+using System.Collections.Generic;
+using System.Diagnostics;
+
+namespace Microsoft.Boogie;
+
+/// <summary>
+/// Add `{:id ...}` attributes to all assertions, assumptions, requires
+/// clauses, ensures clauses, and call statements so that verification
+/// coverage tracking is possible. This exists primarily to support the
+/// automatic detection of vacuous proofs in the case where no front
+/// end has added these already.
+/// </summary>
+public class CoverageAnnotator : StandardVisitor
+{
+  private int idCount = 0;
+  private string currentImplementation;
+  private Dictionary<string, ISet<string>> implementationGoalIds = new();
+  private Dictionary<string, Absy> idMap = new();
+
+  private void AddImplementationGoalId(string id)
+  {
+    implementationGoalIds[currentImplementation].Add(id);
+  }
+
+  private void AddIdIfMissing(ICarriesAttributes node, bool isGoal)
+  {
+    Absy absy = node as Absy;
+    if (absy == null) {
+      return;
+    }
+    var idStr = node.FindStringAttribute("id");
+    if (idStr == null) {
+      idStr = $"id_l{absy.tok.line}_c{absy.tok.col}_{NodeType(node)}_{idCount}";
+      idCount++;
+    }
+    idMap.Add(idStr, absy);
+    if (isGoal) {
+      AddImplementationGoalId(idStr);
+    }
+    node.AddStringAttribute(absy.tok, "id", idStr);
+  }
+
+  private string NodeType(ICarriesAttributes node)
+  {
+    return node switch
+    {
+      Requires _ => "requires",
+      Ensures _ => "ensures",
+      AssertCmd _ => "assert",
+      AssumeCmd _ => "assume",
+      CallCmd _ => "call",
+      _ => "other"
+    };
+  }
+
+  /// <summary>
+  /// Get the set of IDs that correspond to goals within the named
+  /// implementation.
+  /// </summary>
+  /// <param name="implName">The name of the implementation.</param>
+  /// <returns>The IDs for all goal elements within the implementation.</returns>
+  public ISet<string> GetImplementationGoalIds(string implName) => implementationGoalIds[implName];
+
+  /// <summary>
+  /// Get the AST node corresponding to the given ID.
+  /// </summary>
+  /// <param name="idStr">The `id` attribute placed on an AST node.</param>
+  /// <returns>The node where that `id` occurs.</returns>
+  public Absy GetIdNode(string idStr) => idMap[idStr];
+
+  public override Implementation VisitImplementation(Implementation node)
+  {
+    currentImplementation = node.Name;
+    implementationGoalIds.TryAdd(currentImplementation, new HashSet<string>());
+    return base.VisitImplementation(node);
+  }
+
+  public override Cmd VisitAssertCmd(AssertCmd node)
+  {
+    if (node.Expr is LiteralExpr {IsTrue: true}) {
+      return node;
+    }
+
+    AddIdIfMissing(node, true);
+    return base.VisitAssertCmd(node);
+  }
+
+  public override Cmd VisitAssumeCmd(AssumeCmd node)
+  {
+    AddIdIfMissing(node, false);
+    return base.VisitAssumeCmd(node);
+  }
+
+  public override Cmd VisitCallCmd(CallCmd node)
+  {
+    AddIdIfMissing(node, false);
+    return base.VisitCallCmd(node);
+  }
+
+  public override Requires VisitRequires(Requires requires)
+  {
+    AddIdIfMissing(requires, false);
+    return base.VisitRequires(requires);
+  }
+
+  public override Ensures VisitEnsures(Ensures ensures)
+  {
+    if (ensures.Free) {
+      return ensures;
+    }
+
+    AddIdIfMissing(ensures, true);
+    return base.VisitEnsures(ensures);
+  }
+}

Source/Directory.Build.props

@@ -2,7 +2,7 @@
 
   <!-- Target framework and package configuration -->
   <PropertyGroup>
-    <Version>3.5.1</Version>
+    <Version>3.5.2</Version>
     <TargetFramework>net8.0</TargetFramework>
     <GeneratePackageOnBuild>false</GeneratePackageOnBuild>
     <Authors>Boogie</Authors>

Source/ExecutionEngine/CommandLineOptions.cs

@@ -317,11 +317,14 @@ public bool UseUnsatCoreForContractInfer {
 
     public bool PrintAssignment  { get; set; }
 
-    public bool TrackVerificationCoverage {
-      get => trackVerificationCoverage;
+    public bool TrackVerificationCoverage
+    {
+      get => trackVerificationCoverage || WarnVacuousProofs;
       set => trackVerificationCoverage = value;
     }
 
+    public bool WarnVacuousProofs { get; set; }
+
     public int InlineDepth  { get; set; } = -1;
 
     public bool UseProverEvaluate {
@@ -1373,6 +1376,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 +2009,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 missing `{: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

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,

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; }

Test/coverage/verificationCoverage.bpl

@@ -100,8 +100,8 @@
 // RUN: %diff "%s.expect" "%t.coverage-p"
 // RUN: %boogie -trackVerificationCoverage -normalizeDeclarationOrder:1 -prune:1 "%s" > "%t.coverage-d"
 // RUN: %diff "%s.expect" "%t.coverage-d"
-// RUN: %boogie -trackVerificationCoverage -normalizeNames:1 -prune:1 "%s" > "%t.coverage-n"
-// RUN: %diff "%s.expect" "%t.coverage-n"
+// RUN: %boogie -trackVerificationCoverage -warnVacuousProofs -trace -normalizeNames:1 -prune:1 "%s" | grep -v "solver resource count" | grep -v "batch mode" > "%t.coverage-n"
+// RUN: %diff "%s.expect-trace" "%t.coverage-n"
 
 procedure testRequiresAssign(n: int)
   requires {:id "r0"} n > 0; // covered
@@ -216,4 +216,4 @@ procedure usesSomeInteger() returns (r: bool)
   ensures r;
 {
   r := someInteger(7) == 3;
-}
+}

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
+  assert_a0
+  assert_r0
+  r0
+
+Verifying sum ...
+Proof dependencies:
+  id_l127_c3_assume_0
+  id_l127_c3_assume_1
+  invariant sinv_not_1 established
+  invariant sinv_not_1 maintained
+  invariant sinv1 assumed in body
+  invariant sinv1 established
+  invariant sinv1 maintained
+  invariant sinv2 assumed in body
+  invariant sinv2 established
+  invariant sinv2 maintained
+  spost
+  spre1
+
+Verifying contradictoryAssume ...
+Proof dependencies:
+  cont_assume_1
+  cont_assume_2
+verificationCoverage.bpl(143,4): Warning: Proved vacuously
+
+Verifying falseRequires ...
+Proof dependencies:
+  false_req
+verificationCoverage.bpl(150,4): Warning: Proved vacuously
+
+Verifying contradictoryRequires ...
+Proof dependencies:
+  cont_req_1
+  cont_req_2
+verificationCoverage.bpl(158,4): Warning: Proved vacuously
+
+Verifying assumeFalse ...
+Proof dependencies:
+  assumeFalse
+verificationCoverage.bpl(163,2): Warning: Proved vacuously
+
+Verifying testEnsuresCallee ...
+Proof dependencies:
+  tee0
+  tee1
+  ter0
+
+Verifying testEnsuresCaller ...
+Proof dependencies:
+  call2_tee1
+  ensures clause tee0 from call call1
+  ensures clause tee0 from call call2
+  ensures clause tee1 from call call2
+  requires clause ter0 proved for call call1
+  requires clause ter0 proved for call call2
+  tee_not_1
+  ter1
+  xy_sum
+
+Verifying obviouslyUnconstrainedCode ...
+Proof dependencies:
+  a_gt_10
+  constrained
+  x_gt_10
+
+Verifying callContradictoryFunction ...
+Proof dependencies:
+  ensures clause cont_ens_abs from call call_cont
+  requires clause xpos_abs proved for call call_cont
+  xpos_caller
+verificationCoverage.bpl(203,2): Warning: Proved vacuously
+
+Verifying usesSomeInteger ...
+Proof dependencies:
+  id_l216_c3_ensures_2
+  someInteger_value_axiom
+Proof dependencies of whole program:
+  a_gt_10
+  a0
+  assert_a0
+  assert_r0
+  assumeFalse
+  call2_tee1
+  constrained
+  cont_assume_1
+  cont_assume_2
+  cont_req_1
+  cont_req_2
+  ensures clause cont_ens_abs from call call_cont
+  ensures clause tee0 from call call1
+  ensures clause tee0 from call call2
+  ensures clause tee1 from call call2
+  false_req
+  id_l127_c3_assume_0
+  id_l127_c3_assume_1
+  id_l216_c3_ensures_2
+  invariant sinv_not_1 established
+  invariant sinv_not_1 maintained
+  invariant sinv1 assumed in body
+  invariant sinv1 established
+  invariant sinv1 maintained
+  invariant sinv2 assumed in body
+  invariant sinv2 established
+  invariant sinv2 maintained
+  r0
+  requires clause ter0 proved for call call1
+  requires clause ter0 proved for call call2
+  requires clause xpos_abs proved for call call_cont
+  someInteger_value_axiom
+  spost
+  spre1
+  tee_not_1
+  tee0
+  tee1
+  ter0
+  ter1
+  x_gt_10
+  xpos_caller
+  xy_sum
+
+Boogie program verifier finished with 11 verified, 0 errors