From 85191e1555506e1b5bce65b42266f58045222dd2 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 5 Sep 2023 15:59:44 -0700 Subject: [PATCH] Actually parse structured program elements (#777) PR #776 had a fundamental bug which this fixes. --- Source/Core/TrackedNodeComponent.cs | 64 ++++++++--- Source/ExecutionEngine/ExecutionEngine.cs | 6 +- .../SMTLib/SMTLibInteractiveTheoremProver.cs | 4 +- Source/VCGeneration/Split.cs | 4 +- Test/coverage/verificationCoverage.bpl | 104 +++++++++++++++--- .../unnecessaryassumes1.bpl | 12 +- 6 files changed, 155 insertions(+), 39 deletions(-) diff --git a/Source/Core/TrackedNodeComponent.cs b/Source/Core/TrackedNodeComponent.cs index fac55433f..2f25f518e 100644 --- a/Source/Core/TrackedNodeComponent.cs +++ b/Source/Core/TrackedNodeComponent.cs @@ -2,37 +2,64 @@ namespace Microsoft.Boogie { - // Represents an AST node, or component of a node, that is being - // tracked during the proof process to determine whether it was - // used as part of a completed proof. + /// + /// Represents an AST node, or component of a node, that is being + /// tracked during the proof process to determine whether it was + /// used as part of a completed proof. + /// public abstract record TrackedNodeComponent() { + /// + /// The string used to represent this component in the solver. + /// public abstract string SolverLabel { get; } - // This suffix indicates that an ID string represents the assumption of - // a specific ensures clause after a specific call. + /// + /// A human-readable description of this component in terms of + /// user-provided :id attributes. + /// + public abstract string Description { get; } + + /// + /// This suffix indicates that an ID string represents the assumption of + /// a specific ensures clause after a specific call. + /// protected const string ensuresSuffix = "ensures"; - // This suffix indicates that an ID string represents the goal of - // proving a specific requires clause before a specific call. + /// + /// This suffix indicates that an ID string represents the goal of + /// proving a specific requires clause before a specific call. + /// protected const string requiresSuffix = "requires"; - // This suffix indicates that an ID string represents the assumption - // of a specific requires clause after a specific call. + /// + /// This suffix indicates that an ID string represents the assumption + /// of a specific requires clause after a specific call. + /// protected const string requiresAssumedSuffix = "requires_assumed"; - // This suffix indicates that an ID string represents the goal of - // proving that a specific loop invariant is established. + /// + /// This suffix indicates that an ID string represents the goal of + /// proving that a specific loop invariant is established. + /// protected const string establishedSuffix = "established"; - // This suffix indicates that an ID string represents the goal of - // proving that a specific loop invariant is maintained. + /// + /// This suffix indicates that an ID string represents the goal of + /// proving that a specific loop invariant is maintained. + /// protected const string maintainedSuffix = "maintained"; - // This suffix indicates that an ID string represents the asssumption - // of a specific loop invariant in the body of the loop. + /// + /// This suffix indicates that an ID string represents the asssumption + /// of a specific loop invariant in the body of the loop. + /// protected const string assumeInBodySuffix = "assume_in_body"; + /// + /// Reverse the transformation of TrackedNodeComponent to string + /// done by the SolverLabel attribute. + /// public static TrackedNodeComponent ParseSolverString(string idString) { var parts = idString.Split('$'); @@ -72,35 +99,42 @@ public static TrackedNodeComponent ParseSolverString(string idString) public record LabeledNodeComponent(string id) : TrackedNodeComponent() { public override string SolverLabel => id; + public override string Description => id; } public record TrackedCallRequiresGoal(string callId, string requiresId) : TrackedNodeComponent() { public override string SolverLabel => $"{requiresId}${callId}${requiresSuffix}"; + public override string Description => $"requires clause {requiresId} proved for call {callId}"; } public record TrackedCallRequiresAssumed(string callId, string requiresId) : TrackedNodeComponent() { public override string SolverLabel => $"{requiresId}${callId}${requiresAssumedSuffix}"; + public override string Description => $"requires clause {requiresId} assumed from call {callId}"; } public record TrackedCallEnsures(string callId, string ensuresId) : TrackedNodeComponent() { public override string SolverLabel => $"{ensuresId}${callId}${ensuresSuffix}"; + public override string Description => $"ensures clause {ensuresId} from call {callId}"; } public record TrackedInvariantAssumed(string invariantId) : TrackedNodeComponent() { public override string SolverLabel => $"{invariantId}${assumeInBodySuffix}"; + public override string Description => $"invariant {invariantId} assumed in body"; } public record TrackedInvariantEstablished(string invariantId) : TrackedNodeComponent() { public override string SolverLabel => $"{invariantId}${establishedSuffix}"; + public override string Description => $"invariant {invariantId} established"; } public record TrackedInvariantMaintained(string invariantId) : TrackedNodeComponent() { public override string SolverLabel => $"{invariantId}${maintainedSuffix}"; + public override string Description => $"invariant {invariantId} maintained"; } } \ No newline at end of file diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 16c338ffe..9b7c3e925 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -674,12 +674,12 @@ private async Task VerifyEachImplementation(TextWriter output, } if (Options.Trace && Options.TrackVerificationCoverage && processedProgram.Program.AllCoveredElements.Any()) { - Options.OutputWriter.WriteLine("Elements covered by verification: {0}", - string.Join(", ", + Options.OutputWriter.WriteLine("Proof dependencies of whole program:\n {0}", + string.Join("\n ", processedProgram .Program .AllCoveredElements - .Select(elt => elt.SolverLabel) + .Select(elt => elt.Description) .OrderBy(s => s))); } diff --git a/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs b/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs index 8a8aef2b7..a23a437f9 100644 --- a/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs +++ b/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs @@ -224,7 +224,7 @@ public async Task CheckSat(CancellationToken cancellationToken, { usedNamedAssumes.Add(resp.Name); if (libOptions.TrackVerificationCoverage) { - reporter.AddCoveredElement(new LabeledNodeComponent(resp.Name.Substring("aux$$assume$$".Length))); + reporter.AddCoveredElement(TrackedNodeComponent.ParseSolverString(resp.Name.Substring("aux$$assume$$".Length))); } } @@ -233,7 +233,7 @@ public async Task CheckSat(CancellationToken cancellationToken, usedNamedAssumes.Add(arg.Name); if (libOptions.TrackVerificationCoverage) { - reporter.AddCoveredElement(new LabeledNodeComponent(arg.Name.Substring("aux$$assume$$".Length))); + reporter.AddCoveredElement(TrackedNodeComponent.ParseSolverString(arg.Name.Substring("aux$$assume$$".Length))); } } } diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs index 0e73b8e01..9b847c7ac 100644 --- a/Source/VCGeneration/Split.cs +++ b/Source/VCGeneration/Split.cs @@ -1280,8 +1280,8 @@ public int GetHashCode(List obj) checker.ProverRunTime.TotalSeconds, outcome); } if (options.Trace && options.TrackVerificationCoverage) { - run.OutputWriter.WriteLine("Covered elements: {0}", - string.Join(", ", CoveredElements.Select(s => s.SolverLabel).OrderBy(s => s))); + run.OutputWriter.WriteLine("Proof dependencies:\n {0}", + string.Join("\n ", CoveredElements.Select(s => s.Description).OrderBy(s => s))); } var resourceCount = await checker.GetProverResourceCount(); diff --git a/Test/coverage/verificationCoverage.bpl b/Test/coverage/verificationCoverage.bpl index d2a38020a..e19d1aace 100644 --- a/Test/coverage/verificationCoverage.bpl +++ b/Test/coverage/verificationCoverage.bpl @@ -1,18 +1,94 @@ // RUN: %boogie "%s" > "%t.plain" // RUN: %diff "%s.expect" "%t.plain" // RUN: %boogie -trackVerificationCoverage -trace "%s" > "%t.coverage" -// RUN %OutputCheck "%s" --file-to-check="%t.coverage" -// CHECK: Covered elements: a0, assert_a0, assert_r0, r0 -// CHECK: Covered elements: sinv_not_1$established, sinv_not_1$maintained, sinv1$assume_in_body, sinv1$established, sinv1$maintained, sinv2$assume_in_body, sinv2$established, sinv2$maintained, spost, spre1 -// CHECK: Covered elements: cont_assume_1, cont_assume_2 -// CHECK: Covered elements: false_req -// CHECK: Covered elements: cont_req_1, cont_req_2 -// CHECK: Covered elements: assumeFalse -// CHECK: Covered elements: tee0, tee1, ter0 -// CHECK: Covered elements: call2_tee1, tee_not_1, tee0$call1$ensures, tee0$call2$ensures, tee1$call2$ensures, ter0$call1$requires, ter0$call2$requires, ter1, xy_sum -// CHECK: Covered elements: a_gt_10, constrained, x_gt_10 -// CHECK: Covered elements: cont_ens_abs$call_cont$ensures, xpos_abs$call_cont$requires, xpos_caller -// CHECK: Elements covered by verification: a_gt_10, a0, assert_a0, assert_r0, assumeFalse, call2_tee1, constrained, cont_assume_1, cont_assume_2, cont_ens_abs$call_cont$ensures, cont_req_1, cont_req_2, false_req, r0, sinv_not_1$established, sinv_not_1$maintained, sinv1$assume_in_body, sinv1$established, sinv1$maintained, sinv2$assume_in_body, sinv2$established, sinv2$maintained, spost, spre1, tee_not_1, tee0, tee0$call1$ensures, tee0$call2$ensures, tee1, tee1$call2$ensures, ter0, ter0$call1$requires, ter0$call2$requires, ter1, x_gt_10, xpos_abs$call_cont$requires, xpos_caller, xy_sum +// RUN: %OutputCheck "%s" --file-to-check="%t.coverage" +// CHECK: Proof dependencies: +// CHECK: a0 +// CHECK: assert_a0 +// CHECK: assert_r0 +// CHECK: r0 +// CHECK: Proof dependencies: +// CHECK: invariant sinv_not_1 established +// CHECK: invariant sinv_not_1 maintained +// CHECK: invariant sinv1 assumed in body +// CHECK: invariant sinv1 established +// CHECK: invariant sinv1 maintained +// CHECK: invariant sinv2 assumed in body +// CHECK: invariant sinv2 established +// CHECK: invariant sinv2 maintained +// CHECK: spost +// CHECK: spre1 +// CHECK: Proof dependencies: +// CHECK: cont_assume_1 +// CHECK: cont_assume_2 +// CHECK: Proof dependencies: +// CHECK: false_req +// CHECK: Proof dependencies: +// CHECK: cont_req_1 +// CHECK: cont_req_2 +// CHECK: Proof dependencies: +// CHECK: assumeFalse +// CHECK: Proof dependencies: +// CHECK: tee0 +// CHECK: tee1 +// CHECK: ter0 +// CHECK: Proof dependencies: +// CHECK: call2_tee1 +// CHECK: ensures clause tee0 from call call1 +// CHECK: ensures clause tee0 from call call2 +// CHECK: ensures clause tee1 from call call2 +// CHECK: requires clause ter0 proved for call call1 +// CHECK: requires clause ter0 proved for call call2 +// CHECK: tee_not_1 +// CHECK: ter1 +// CHECK: xy_sum +// CHECK: Proof dependencies: +// CHECK: a_gt_10 +// CHECK: constrained +// CHECK: x_gt_10 +// CHECK: Proof dependencies: +// 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 of whole program: +// CHECK: a_gt_10 +// CHECK: a0 +// CHECK: assert_a0 +// CHECK: assert_r0 +// CHECK: assumeFalse +// CHECK: call2_tee1 +// CHECK: constrained +// CHECK: cont_assume_1 +// CHECK: cont_assume_2 +// CHECK: cont_req_1 +// CHECK: cont_req_2 +// CHECK: ensures clause cont_ens_abs from call call_cont +// CHECK: ensures clause tee0 from call call1 +// CHECK: ensures clause tee0 from call call2 +// CHECK: ensures clause tee1 from call call2 +// CHECK: false_req +// CHECK: invariant sinv_not_1 established +// CHECK: invariant sinv_not_1 maintained +// CHECK: invariant sinv1 assumed in body +// CHECK: invariant sinv1 established +// CHECK: invariant sinv1 maintained +// CHECK: invariant sinv2 assumed in body +// CHECK: invariant sinv2 established +// CHECK: invariant sinv2 maintained +// CHECK: r0 +// 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: spost +// CHECK: spre1 +// CHECK: tee_not_1 +// CHECK: tee0 +// CHECK: tee1 +// CHECK: ter0 +// CHECK: ter1 +// CHECK: x_gt_10 +// CHECK: xpos_caller +// CHECK: xy_sum // RUN: %boogie -trackVerificationCoverage "%s" > "%t.coverage" // RUN: %diff "%s.expect" "%t.coverage" // RUN: %boogie -trackVerificationCoverage -typeEncoding:a -prune "%s" > "%t.coverage-a" @@ -21,8 +97,8 @@ // RUN: %diff "%s.expect" "%t.coverage-p" // RUN: %boogie -trackVerificationCoverage -normalizeDeclarationOrder:1 -prune "%s" > "%t.coverage-d" // RUN: %diff "%s.expect" "%t.coverage-d" -// RUN %boogie -trackVerificationCoverage -normalizeNames:1 -prune "%s" > "%t.coverage-n" -// RUN %diff "%s.expect" "%t.coverage-n" +// RUN: %boogie -trackVerificationCoverage -normalizeNames:1 -prune "%s" > "%t.coverage-n" +// RUN: %diff "%s.expect" "%t.coverage-n" // UNSUPPORTED: batch_mode procedure testRequiresAssign(n: int) diff --git a/Test/unnecessaryassumes/unnecessaryassumes1.bpl b/Test/unnecessaryassumes/unnecessaryassumes1.bpl index e5ec0bbbe..70c9a2bd3 100644 --- a/Test/unnecessaryassumes/unnecessaryassumes1.bpl +++ b/Test/unnecessaryassumes/unnecessaryassumes1.bpl @@ -1,9 +1,15 @@ // We use boogie instead of parallel-boogie here to fix the order of the output from /trackVerificationCoverage // RUN: %boogie -trackVerificationCoverage -trace "%s" > "%t" // RUN: %OutputCheck "%s" --file-to-check="%t" -// CHECK: Covered elements: s0 -// CHECK: Covered elements: s2, s3 -// CHECK: Elements covered by verification: s0, s2, s3 +// CHECK: Proof dependencies: +// CHECK: s0 +// CHECK: Proof dependencies: +// CHECK: s2 +// CHECK: s3 +// CHECK: Proof dependencies of whole program: +// CHECK: s0 +// CHECK: s2 +// CHECK: s3 // UNSUPPORTED: batch_mode procedure test0(n: int)