From b51853c76700bb76e51e6f48b02994cef9c6461b Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Tue, 17 Sep 2024 19:11:49 +0200 Subject: [PATCH 1/5] feat: verification coverage analysis for axioms --- Source/Provers/SMTLib/ProverContext.cs | 10 +++++++++- Test/coverage/verificationCoverage.bpl | 15 +++++++++++++++ Test/coverage/verificationCoverage.bpl.expect | 2 +- 3 files changed, 25 insertions(+), 2 deletions(-) diff --git a/Source/Provers/SMTLib/ProverContext.cs b/Source/Provers/SMTLib/ProverContext.cs index adb7465eb..ec14b55e4 100644 --- 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/Test/coverage/verificationCoverage.bpl b/Test/coverage/verificationCoverage.bpl index 8fbc5a243..250ef54ba 100644 --- 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; +} \ No newline at end of file diff --git a/Test/coverage/verificationCoverage.bpl.expect b/Test/coverage/verificationCoverage.bpl.expect index 12041afe1..cccffe05d 100644 --- 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 From 4efba3d0f2b91cdba2330e6f1e77d32278e9f8f9 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Wed, 18 Sep 2024 23:48:14 +0200 Subject: [PATCH 2/5] inherit attributes --- Source/Core/Monomorphization.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/Core/Monomorphization.cs b/Source/Core/Monomorphization.cs index 4c5b2c36d..215b79493 100644 --- 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); } From 4d2b06528b2ff44ca24563ea48c483cf82ef8ac7 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Fri, 4 Oct 2024 00:23:58 +0200 Subject: [PATCH 3/5] expose PrunedDeclarations --- Source/VCGeneration/Split.cs | 4 +++- Source/VCGeneration/VerificationRunResult.cs | 3 ++- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs index 7cf747118..f063c2215 100644 --- a/Source/VCGeneration/Split.cs +++ b/Source/VCGeneration/Split.cs @@ -899,7 +899,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, + PrunedDeclarations: PrunedDeclarations + ); callback.OnVCResult(result); if (Options.VcsDumpSplits) diff --git a/Source/VCGeneration/VerificationRunResult.cs b/Source/VCGeneration/VerificationRunResult.cs index b2566f93e..89d511672 100644 --- a/Source/VCGeneration/VerificationRunResult.cs +++ b/Source/VCGeneration/VerificationRunResult.cs @@ -18,7 +18,8 @@ public record VerificationRunResult List Asserts, IEnumerable CoveredElements, int ResourceCount, - SolverKind? SolverUsed + SolverKind? SolverUsed, + IReadOnlyList PrunedDeclarations ) { public void ComputePerAssertOutcomes(out Dictionary perAssertOutcome, out Dictionary perAssertCounterExamples) { From 9141641c86431d020d2de2afe71802fe609a873e Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Fri, 4 Oct 2024 00:46:24 +0200 Subject: [PATCH 4/5] different init --- Source/VCGeneration/BlockTransformations.cs | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/Source/VCGeneration/BlockTransformations.cs b/Source/VCGeneration/BlockTransformations.cs index 95e0d7788..b0e72c7f3 100644 --- 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 blocks) { - var toVisit = new HashSet(); + var toVisit = new HashSet(blocks); var removed = new HashSet(); - foreach (var block in blocks) { - toVisit.Add(block); - } while(toVisit.Count > 0) { var block = toVisit.First(); toVisit.Remove(block); From 94cfc09f3e4fc86bcc3dccd9f4a610eb0422227a Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Sun, 6 Oct 2024 23:18:54 +0200 Subject: [PATCH 5/5] renamed PrunedDeclarations to DeclarationsAfterPruning --- Source/VCGeneration/Split.cs | 2 +- Source/VCGeneration/VerificationRunResult.cs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs index 6fc062bc6..3eac0cb51 100644 --- a/Source/VCGeneration/Split.cs +++ b/Source/VCGeneration/Split.cs @@ -898,7 +898,7 @@ public VerificationRunResult ReadOutcome(int iteration, Checker checker, Verifie CoveredElements: CoveredElements, ResourceCount: resourceCount, SolverUsed: (Options as SMTLibSolverOptions)?.Solver, - PrunedDeclarations: PrunedDeclarations + DeclarationsAfterPruning: PrunedDeclarations ); callback.OnVCResult(result); diff --git a/Source/VCGeneration/VerificationRunResult.cs b/Source/VCGeneration/VerificationRunResult.cs index 2ce3c752f..15e3a2cdb 100644 --- a/Source/VCGeneration/VerificationRunResult.cs +++ b/Source/VCGeneration/VerificationRunResult.cs @@ -19,7 +19,7 @@ public record VerificationRunResult IEnumerable CoveredElements, int ResourceCount, SolverKind? SolverUsed, - IReadOnlyList PrunedDeclarations + IReadOnlyList DeclarationsAfterPruning ) { public void ComputePerAssertOutcomes(out Dictionary perAssertOutcome, out Dictionary perAssertCounterExamples) {