feat: Verification coverage analysis for axioms (#948)

This PR enables verification coverage analysis for axioms.
boogie-org · Oct 7, 2024 · 475faa0 · 475faa0
1 parent 2ea9a43
commit 475faa0
Show file tree

Hide file tree

Showing 7 changed files with 32 additions and 9 deletions.
diff --git a/Source/Core/Monomorphization.cs b/Source/Core/Monomorphization.cs
@@ -649,7 +649,7 @@ public override Axiom VisitAxiom(Axiom node)
         }
         else
         {
-          var newAxiom = new Axiom(axiom.tok, expr);
+          var newAxiom = new Axiom(axiom.tok, expr, axiom.Comment, axiom.Attributes);
           if (monomorphizationVisitor.originalAxiomToSplitAxioms.ContainsKey(axiom)) {
             monomorphizationVisitor.originalAxiomToSplitAxioms[axiom].Add(newAxiom);
           }

diff --git a/Source/Provers/SMTLib/ProverContext.cs b/Source/Provers/SMTLib/ProverContext.cs
@@ -226,7 +226,15 @@ public override void AddAxiom(Axiom ax, string attributes)
       //Contract.Requires(ax != null);
       base.AddAxiom(ax, attributes);
 
-      axiomConjuncts.Add(translator.Translate(ax.Expr));
+      var expr = translator.Translate(ax.Expr);
+      var assumeId = QKeyValue.FindStringAttribute(ax.Attributes, "id");
+      if (assumeId != null && options.TrackVerificationCoverage)
+      {
+        var v = gen.Variable(assumeId, Microsoft.Boogie.Type.Bool, VCExprVarKind.Assume);
+        expr = gen.Function(VCExpressionGenerator.NamedAssumeOp, v, gen.ImpliesSimp(v, expr));
+      }
+
+      axiomConjuncts.Add(expr);
     }
 
     public override void AddAxiom(VCExpr vc)

diff --git a/Source/VCGeneration/BlockTransformations.cs b/Source/VCGeneration/BlockTransformations.cs
@@ -100,11 +100,8 @@ private static bool ContainsAssert(Block b)
   public static bool IsNonTrivialAssert (Cmd c) { return c is AssertCmd { Expr: not LiteralExpr { asBool: true } }; }
 
   private static void DeleteUselessBlocks(List<Block> blocks) {
-    var toVisit = new HashSet<Block>();
+    var toVisit = new HashSet<Block>(blocks);
     var removed = new HashSet<Block>();
-    foreach (var block in blocks) {
-      toVisit.Add(block);
-    }
     while(toVisit.Count > 0) {
       var block = toVisit.First();
       toVisit.Remove(block);

diff --git a/Source/VCGeneration/Splits/Split.cs b/Source/VCGeneration/Splits/Split.cs
@@ -897,7 +897,9 @@ public VerificationRunResult ReadOutcome(int iteration, Checker checker, Verifie
           Asserts: Asserts,
           CoveredElements: CoveredElements,
           ResourceCount: resourceCount,
-          SolverUsed: (Options as SMTLibSolverOptions)?.Solver);
+          SolverUsed: (Options as SMTLibSolverOptions)?.Solver,
+          DeclarationsAfterPruning: PrunedDeclarations
+          );
         callback.OnVCResult(result);
 
         if (Options.VcsDumpSplits)

diff --git a/Source/VCGeneration/VerificationRunResult.cs b/Source/VCGeneration/VerificationRunResult.cs
@@ -18,7 +18,8 @@ public record VerificationRunResult
     List<AssertCmd> Asserts,
     IEnumerable<TrackedNodeComponent> CoveredElements,
     int ResourceCount,
-    SolverKind? SolverUsed
+    SolverKind? SolverUsed,
+    IReadOnlyList<Declaration> DeclarationsAfterPruning
   ) {
     public void ComputePerAssertOutcomes(out Dictionary<AssertCmd, SolverOutcome> perAssertOutcome,
       out Dictionary<AssertCmd, Counterexample> perAssertCounterExamples) {

diff --git a/Test/coverage/verificationCoverage.bpl b/Test/coverage/verificationCoverage.bpl
@@ -50,6 +50,8 @@
 // CHECK:   ensures clause cont_ens_abs from call call_cont
 // CHECK:   requires clause xpos_abs proved for call call_cont
 // CHECK:   xpos_caller
+// CHECK: Proof dependencies:
+// CHECK:   someInteger_value_axiom
 // CHECK: Proof dependencies of whole program:
 // CHECK:   a_gt_10
 // CHECK:   a0
@@ -79,6 +81,7 @@
 // CHECK:   requires clause ter0 proved for call call1
 // CHECK:   requires clause ter0 proved for call call2
 // CHECK:   requires clause xpos_abs proved for call call_cont
+// CHECK:   someInteger_value_axiom
 // CHECK:   spost
 // CHECK:   spre1
 // CHECK:   tee_not_1
@@ -202,3 +205,15 @@ procedure callContradictoryFunction(x: int) returns (r: int)
   call {:id "call_cont"} r := contradictoryEnsuresClause(x); // requires and ensures covered
   r := {:id "unreachable_assignment"} r - 1; // not covered
 }
+
+function someInteger(i: int) : int uses {
+  axiom {:id "someInteger_value_axiom"} (forall i: int :: someInteger(i) == 3);
+
+  axiom {:id "uselessAxiom"} (3 == 3);
+}
+
+procedure usesSomeInteger() returns (r: bool)
+  ensures r;
+{
+  r := someInteger(7) == 3;
+}
diff --git a/Test/coverage/verificationCoverage.bpl.expect b/Test/coverage/verificationCoverage.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 10 verified, 0 errors
+Boogie program verifier finished with 11 verified, 0 errors