Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Actually parse structured program elements #777

Merged
merged 11 commits into from
Sep 5, 2023
64 changes: 49 additions & 15 deletions Source/Core/TrackedNodeComponent.cs
Original file line number Diff line number Diff line change
Expand Up @@ -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.
/// <summary>
/// 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.
/// </summary>
public abstract record TrackedNodeComponent()
{
/// <summary>
/// The string used to represent this component in the solver.
/// </summary>
public abstract string SolverLabel { get; }

// This suffix indicates that an ID string represents the assumption of
// a specific ensures clause after a specific call.
/// <summary>
/// A human-readable description of this component in terms of
/// user-provided :id attributes.
/// </summary>
public abstract string Description { get; }

/// <summary>
/// This suffix indicates that an ID string represents the assumption of
/// a specific ensures clause after a specific call.
/// </summary>
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.
/// <summary>
/// This suffix indicates that an ID string represents the goal of
/// proving a specific requires clause before a specific call.
/// </summary>
protected const string requiresSuffix = "requires";

// This suffix indicates that an ID string represents the assumption
// of a specific requires clause after a specific call.
/// <summary>
/// This suffix indicates that an ID string represents the assumption
/// of a specific requires clause after a specific call.
/// </summary>
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.
/// <summary>
/// This suffix indicates that an ID string represents the goal of
/// proving that a specific loop invariant is established.
/// </summary>
protected const string establishedSuffix = "established";

// This suffix indicates that an ID string represents the goal of
// proving that a specific loop invariant is maintained.
/// <summary>
/// This suffix indicates that an ID string represents the goal of
/// proving that a specific loop invariant is maintained.
/// </summary>
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.
/// <summary>
/// This suffix indicates that an ID string represents the asssumption
/// of a specific loop invariant in the body of the loop.
/// </summary>
protected const string assumeInBodySuffix = "assume_in_body";

/// <summary>
/// Reverse the transformation of TrackedNodeComponent to string
/// done by the SolverLabel attribute.
/// </summary>
public static TrackedNodeComponent ParseSolverString(string idString)
{
var parts = idString.Split('$');
Expand Down Expand Up @@ -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";
}
}
6 changes: 3 additions & 3 deletions Source/ExecutionEngine/ExecutionEngine.cs
Original file line number Diff line number Diff line change
Expand Up @@ -674,12 +674,12 @@ private async Task<PipelineOutcome> 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)));
}

Expand Down
4 changes: 2 additions & 2 deletions Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs
Original file line number Diff line number Diff line change
Expand Up @@ -224,7 +224,7 @@ public async Task<Outcome> 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)));
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I take it these two lines were the fundamental bug?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yep.

}
}

Expand All @@ -233,7 +233,7 @@ public async Task<Outcome> 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)));
}
}
}
Expand Down
4 changes: 2 additions & 2 deletions Source/VCGeneration/Split.cs
Original file line number Diff line number Diff line change
Expand Up @@ -1280,8 +1280,8 @@ public int GetHashCode(List<Block> 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();
Expand Down
104 changes: 90 additions & 14 deletions Test/coverage/verificationCoverage.bpl
Original file line number Diff line number Diff line change
@@ -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:
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Side note: if you're checking for the literal output line-by-line without anything expected in between, it's more strict and probably more efficient to use CHECK-NEXT: - https://github.com/stp/OutputCheck#check-next-regex

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, yeah, it would probably make sense for some (but not all) of these to be CHECK-NEXT. However, I don't imagine the lack of that would cause us to miss bugs in this case.

// 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"
Expand All @@ -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"
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oof, I wish I had a concrete suggestion for how to catch this type of testing error. :P

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Me too!

// RUN: %diff "%s.expect" "%t.coverage-n"
// UNSUPPORTED: batch_mode

procedure testRequiresAssign(n: int)
Expand Down
Loading