Actually parse structured program elements (#777)

PR #776 had a fundamental bug which this fixes.

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.
+  /// <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('$');
@@ -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";
   }
 }

Source/ExecutionEngine/ExecutionEngine.cs

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

Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs

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

Source/VCGeneration/Split.cs

@@ -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();

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)

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)