Implement verification coverage analysis #741

atomb · 2023-06-01T00:13:21Z

This generalizes the previous feature of tracking "necessary assumptions".

That feature, previously enabled with -printNecessaryAssumptions, allowed each assume statement to be annotated with an {:id ...} attribute, and Boogie would then report which assumptions were necessary to complete the verification by requesting an unsat core from Z3.

Now that attribute can be placed on many other program elements:

assume statements
assert statements
assignments
calls
requires clauses
ensures clauses

Each of these is then labeled in the SMT encoding and will potentially show up in the unsat core.

The new -printVerificationCoverage option (which replaces the old one) prints the members of this broader set of program elements that show up in the unsat core. With -trace, it also prints the coverage information for each procedure as it finishes. The coverage information for each procedure is also available in the VCResult produced at the end of each verification.

Fixes #730.

This allows assignments to be treated as "necessary assumptions"

Allows them to be tracked in unseat cores.

Allows them to be tracked in unseat cores. Add a suffix to distinguish between the assumption and the assertion implied by an invariant, since we’ll be tracking assertions, too, in a later step.

keyboardDrummer · 2023-06-02T08:04:05Z

The new -printVerificationCoverage option prints the members of this broader set of program elements that show up in the unsat core.

Is there a need for a new option then? Why not expand the support of the existing option? (and possibly rename it)

keyboardDrummer

Is there existing documentation on the id attribute? If not could you add it?

keyboardDrummer · 2023-06-02T07:40:47Z

Source/Core/AST/AbsyCmd.cs

@@ -3720,6 +3720,7 @@ protected override Cmd ComputeDesugaring(PrintOptions options)
      Dictionary<Variable, Expr> substMapBound = new Dictionary<Variable, Expr>();
      List<Variable> /*!*/
        tempVars = new List<Variable>();
+      string idAttr = QKeyValue.FindStringAttribute(Attributes, "id");


Shouldn't this be named id, since it's a string not an attribute?

Good point.

keyboardDrummer · 2023-06-02T07:45:19Z

Source/Core/AST/AbsyCmd.cs

@@ -3846,6 +3848,11 @@ protected override Cmd ComputeDesugaring(PrintOptions options)
              a.Attributes = attrCopy;
            }

+            // Do this after copying the attributes so it doesn't get overwritten


The method being changed is very large, and uses regions instead of submethods to organize code. I want to ask you apply the boyscout principle of "leaving things behind nicer than they were", and to chop this method up into pieces, and also to move the class SugaredCmd out into it's own file, since it's in a file that's way too large.

Created #743 to track this, as I think we need to do it very carefully.

I think we need to do it very carefully

Why? Splitting a method up into pieces can be done in a mostly automated way using Rider. Same for moving a class into a separate file.

Yeah, but reorganizing those methods so that they are well-organized and use better abstractions, rather than just slicing them into pieces, would require more thought.

I'm paraphrasing an offline discussion I had with @atomb on the above, for the sake of getting some additional eyes on it.

@atomb prefers keeping the pacify implementations for various commands in a single method, since that allows having them be vertically adjacent to each other which follows the structure of Figure 3 in this paper, which is what the code is based on. Keeping the structure of the two most similar provides the best way of doing a side-by-side comparison.

I would prefer keeping the code for different commands separate. I would even prefer having an abstract Pacify method in the Cmd class, and having the commands in separate files. The number of commands is not fixed, we might add more in the future, and I think in this way the codebase scales well to that.

I believe that while the paper is structured by putting the concepts at the top-level, and then discussing all commands within each concept, this doesn't mean that's also the right structure for the code. It's easier to discuss just one pair of concept and command at a time, and while the paper doesn't have room to go that slow, in our codebase we can use as many separators, such as files and methods, as we like. Also, the code is more verbose so there is more need to keep the scope of each block to a minimum.

I don't think optimizing for comparability between the code and the paper is important. Modern IDEs make it easy to navigate between the code for various commands, so I don't think there's a particular difficulty in making the comparison in any case.

Source/VCGeneration/Wlp.cs

keyboardDrummer · 2023-06-02T07:54:26Z

Source/Provers/SMTLib/TypeDeclCollector.cs

@@ -270,7 +270,9 @@ public override bool Visit(VCExprVar node, bool arg)
        RegisterType(node.Type);
        string decl =
          "(declare-fun " + printedName + " () " + TypeToString(node.Type) + ")";
-        if (!(printedName.StartsWith("assume$$") || printedName.StartsWith("soft$$") ||
+        if (!(printedName.StartsWith("assume$$") ||


Where does this list of constants come from? Can they be injected from their origin instead of hardcoded here?

That certainly would be nicer.

keyboardDrummer · 2023-06-02T07:57:03Z

Source/ExecutionEngine/ExecutionEngine.csproj

@@ -21,6 +21,7 @@
    <ProjectReference Include="..\Houdini\Houdini.csproj" />
    <ProjectReference Include="..\Model\Model.csproj" />
    <ProjectReference Include="..\VCGeneration\VCGeneration.csproj" />
+    <ProjectReference Include="..\Provers\SMTLib\SMTLib.csproj" />


I think this can be removed.

The build of Boogie itself works without it, but I discovered it was necessary for Dafny (and presumably other Boogie clients?) to build against a Boogie source tree instead of a pre-built package.

OK, the alternative is that the Boogie clients such as Dafny also depend on SMTLib, but this seems like a nicer UX.

keyboardDrummer · 2023-06-02T08:33:22Z

Source/Core/AST/Absy.cs

+    {
+      var arg = QKeyValue.FindStringAttribute(src.Attributes, attr);
+      if (arg is not null) {
+        dest.Attributes = new QKeyValue(tok, attr, new List<object>( ){arg + suffix}, dest.Attributes);


Why did you create static methods instead of instance ones?

I suggest you move Declaration.FindStringAttribute to ICarriesAttributes.FindStringAttribute and add a method ICarriesAttributes.AddAttribute, then CopyStringAttributeWithSuffix becomes:

var arg = src.FindStringAttribute(attr); if (arg is not null) { dest.AddAttribute(tok, attr, arg + suffix); }

keyboardDrummer · 2023-06-02T08:41:23Z

Source/VCGeneration/VCGen.cs

@@ -729,7 +732,13 @@ private void ConvertCFG2DAGStandard(Implementation impl, Dictionary<Block, List<
                b = new LoopInitAssertCmd(c.tok, c.Expr, c);
              }

-              b.Attributes = c.Attributes;
+              b.Attributes = (QKeyValue)c.Attributes?.Clone();


Is this clone necessary? It doesn't seem like attributes are generally modified, instead they seem to be treated more as an immutable linked list.

Yes, it's necessary, since the id attribute on the new command will have a suffix appended. In principle, I guess the two commands could share an attribute list tail, but that seems more complex than it's worth.

Note that the original command is discarded so its attributes won't be used by it and you could get away with one less clone, but either is OK with me.

It feels fragile to me to depend on the fact that the original command is never re-used. I agree that it isn't at the moment, but future work could change that.

keyboardDrummer · 2023-06-02T08:48:14Z

Source/Core/AST/Absy.cs

+      }
+    }
+
+    public static void CopyStringAttributeWithSuffix(IToken tok, ICarriesAttributes src, string attr, string suffix, ICarriesAttributes dest)


This method is only used with id as a value for attr. I suggest you hardcode that in the implementation and remove the parameter, and rename to CopyIdWithSuffix

keyboardDrummer · 2023-06-02T08:52:44Z

Source/Core/AST/AbsyCmd.cs

@@ -4003,6 +4015,9 @@ protected override Cmd ComputeDesugaring(PrintOptions options)
        Contract.Assert(e != null);
        Expr copy = Substituter.ApplyReplacingOldExprs(calleeSubstitution, calleeSubstitutionOld, e.Condition);
        AssumeCmd assume = new AssumeCmd(this.tok, copy);
+        if (idAttr is not null) {
+          ICarriesAttributes.CopyStringAttributeWithSuffix(tok, e, "id", $"${idAttr}$ensures", assume);


On line 4026, the assume.Attributes can be overridden.

Oh, good catch. I should move this down.

keyboardDrummer · 2023-06-02T08:55:40Z

Source/Core/AST/AbsyCmd.cs

@@ -4003,6 +4015,9 @@ protected override Cmd ComputeDesugaring(PrintOptions options)
        Contract.Assert(e != null);
        Expr copy = Substituter.ApplyReplacingOldExprs(calleeSubstitution, calleeSubstitutionOld, e.Condition);
        AssumeCmd assume = new AssumeCmd(this.tok, copy);
+        if (idAttr is not null) {


Is this copying the id from the ensures clause of the callee, over to the assumes that placed after the call ? Doesn't that lead to duplicate ids if there is more than one call to a callee?

Can you add a test-case where there is more than 1 call to a callee, and the coverage results are different per call?

Also, what is the purpose of tracking coverage results for procedure calls? I would have expected tracking coverage for requires/ensures/assume/assert, but not call.

The id of the call statement itself is included in the id for the postcondition to avoid exactly that duplication.

It's useful to know whether a postcondition (or a precondition) from a particular call is used, rather than whether the postcondition is used in general. Some of the things that it can help you identify:

a context-dependent contradictory postcondition (and, in particular, what parts of it lead to a contradiction)

a postcondition that's only rarely used, and perhaps better established in other ways (such as by splitting a lemma into multiple lemmas)

When combined with split-on-every-assert, this can also help you identify exactly how each lemma you use contributes to each goal you're trying to prove. That could help in refactoring the lemmas you're using, or the structure of the current proof.

The id of the call statement itself is included in the id for the postcondition to avoid exactly that duplication.

I see! Could you rename id to callId ?

Can you add a test-case where there is more than 1 call to a callee, and the coverage results are different per call?

Consider still doing this.

atomb · 2023-06-02T15:14:04Z

The new -printVerificationCoverage option prints the members of this broader set of program elements that show up in the unsat core.

Is there a need for a new option then? Why not expand the support of the existing option? (and possibly rename it)

I indeed did that at first, but then decided that there may be cases where someone would want the old behavior so I decided not to break it. I'm quite happy to merge the two, with the new name.

Now `/printVerificationCoverage` subsumes it.

shazqadeer · 2023-06-03T14:27:52Z

Before this PR, I did not know about this "coverage" feature in Boogie. Interesting stuff! This PR would make the feature more obvious to Boogie users and also make the feature more comprehensive. Nice, @atomb .

Is the plan to land a PR addressing #743 first and then rebase this PR?

keyboardDrummer · 2023-06-05T09:13:16Z

I indeed did that at first, but then decided that there may be cases where someone would want the old behavior so I decided not to break it. I'm quite happy to merge the two, with the new name.

It seems to me that if you only have id attributes on places where the old option supported them, then the new option already gives the same behavior as the old one. In that case, let's merge them.

keyboardDrummer · 2023-06-05T09:19:21Z

Source/VCGeneration/VCGen.cs

@@ -729,7 +732,13 @@ private void ConvertCFG2DAGStandard(Implementation impl, Dictionary<Block, List<
                b = new LoopInitAssertCmd(c.tok, c.Expr, c);
              }

-              b.Attributes = c.Attributes;
+              b.Attributes = (QKeyValue)c.Attributes?.Clone();
+              if (Options.PrintVerificationCoverage) {


I don't think Print should be in the name of this field, since you should also be able to use it in a fully programmatic way in which the consumer never prints anything. Maybe the Dafny IDE presents it through some UI for example.

keyboardDrummer · 2023-06-05T09:26:26Z

Source/VCGeneration/VCGen.cs

@@ -749,9 +758,22 @@ private void ConvertCFG2DAGStandard(Implementation impl, Dictionary<Block, List<
                b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, c.Expr, c);
              }

-              b.Attributes = c.Attributes;
+              b.Attributes = (QKeyValue)c.Attributes?.Clone();


Could you improve the names of b and c and stop them from being assigned multiple times?

keyboardDrummer · 2023-06-05T11:21:45Z

Source/Core/AST/AbsyCmd.cs

@@ -4003,6 +4015,9 @@ protected override Cmd ComputeDesugaring(PrintOptions options)
        Contract.Assert(e != null);
        Expr copy = Substituter.ApplyReplacingOldExprs(calleeSubstitution, calleeSubstitutionOld, e.Condition);


I'd consider this a favor, but it would be amazing if you could follow-up this PR with one where many of the AST classes are moved to separate files. Here for example it's relatively difficult for me to see what this in this.Proc.Ensures points to, since CallCmd is not in its own file. Placing classes in separate files is a Rider supported refactoring, so it should be fairly trivial to do.

I can also do it if you like.

I can probably do this in a couple of weeks, but certainly wouldn't object if you did it sooner! :)

atomb · 2023-06-05T15:42:24Z

Is the plan to land a PR addressing #743 first and then rebase this PR?

My preference would be to address #743 later (though probably not a lot later).

* Use new option name * Depend on different postconditions from different calls to same target

keyboardDrummer · 2023-06-06T12:58:57Z

Source/Core/AST/Absy.cs

@@ -280,6 +280,33 @@ public List<int> FindLayers()
      }
      return layers.Distinct().OrderBy(l => l).ToList();
    }
+
+    // Look for {:name string} in list of attributes.
+    public string FindStringAttribute(string name)


If you define these methods as extension methods, then you can also call them without casting to ICarriesAttributes first.

keyboardDrummer · 2023-06-06T12:59:28Z

Source/Core/AST/Absy.cs

+      }
+    }
+
+    public void CopyIdWithSuffixFrom(IToken tok, ICarriesAttributes src, string suffix)


target.Copy reads strangely. I would expect the src to be on the left side of the copy verb

keyboardDrummer · 2023-06-06T13:03:07Z

Source/VCGeneration/VCGen.cs

          {
-            if (a is AssertCmd)
+            if (predicateCmd is AssertCmd)


You can use if (predicateCmd is AssertCmd assertCmd) here

keyboardDrummer · 2023-06-06T13:03:48Z

Source/VCGeneration/VCGen.cs

-          PredicateCmd a = header.Cmds[i] as PredicateCmd;
-          if (a != null)
+          PredicateCmd predicateCmd = header.Cmds[i] as PredicateCmd;
+          if (predicateCmd != null)


You can use if (header.Cmds[i] is PredicateCmd predicateCmd) here

atomb added 14 commits May 31, 2023 09:40

Recognize {:id ...} attributes on assignments

49d5d23

This allows assignments to be treated as "necessary assumptions"

Recognize {:id ...} on requires clauses

0ac0824

Allows them to be tracked in unseat cores.

Recognize {:id ...} on loop invariants

32398ee

Allows them to be tracked in unseat cores. Add a suffix to distinguish between the assumption and the assertion implied by an invariant, since we’ll be tracking assertions, too, in a later step.

Add a field to VCResult to track unsat cores

5c4afaf

Basic support for labeled assertions

e945230

Fix concurrency bug accidentally discovered

ac56302

Mostly complete verification coverage tracking

a97032b

Add initial test for verification coverage

5919289

Tweak RUN commands for verification coverage test

8ad7c16

Verification coverage unsupported in batch mode

e95aab5

Attempt to make timeouts test more robust

3ce4244

Another try for more deterministic timeout testing

950080b

Tiny tweaks to coverage tests

7b6679b

Merge remote-tracking branch 'upstream/master' into broader-unsat-cores

b67d227

atomb marked this pull request as ready for review June 1, 2023 18:19

atomb requested review from shazqadeer, keyboardDrummer and MikaelMayer June 1, 2023 18:19

keyboardDrummer reviewed Jun 2, 2023

View reviewed changes

atomb added 6 commits June 2, 2023 09:43

Rename variables

20e06a0

Adjust how IDs (and other attributes) are tracked

abcae74

Remove /printNecessaryAssumes option

6b48078

Now `/printVerificationCoverage` subsumes it.

Typo in comment

d1861c0

Documentation for /printVerificationCoverage, :id

a07fe28

Remove conditionals on magic variable prefixes

82e7e24

This was referenced Jun 2, 2023

Refactor call desugaring and passive command creation #743

Open

Format and move code in VCExpr project #738

Closed

Copy :id attributes unconditionally

98dcf9f

atomb requested a review from keyboardDrummer June 2, 2023 19:00

keyboardDrummer reviewed Jun 5, 2023

View reviewed changes

atomb added 7 commits June 5, 2023 09:11

Rename variable for id on CallCmds

d68b1f9

Add comment about dummy operators

6d48d32

PrintVerificationCoverage -> TrackVerificationCoverage

e43e4f2

CurrentCoveredElements -> ProofRun.CoveredElements

94cf1ea

Rename command variables in VCGen for loops

449364c

Update verification coverage test

725fe2d

* Use new option name * Depend on different postconditions from different calls to same target

Remove uses of /printVerificationCoverage

cd50eef

atomb requested a review from keyboardDrummer June 5, 2023 16:37

keyboardDrummer reviewed Jun 6, 2023

View reviewed changes

keyboardDrummer approved these changes Jun 6, 2023

View reviewed changes

Merge branch 'master' into broader-unsat-cores

70cd55d

keyboardDrummer merged commit ac9493b into boogie-org:master Jun 6, 2023

atomb deleted the broader-unsat-cores branch January 4, 2024 17:07

		@@ -4003,6 +4015,9 @@ protected override Cmd ComputeDesugaring(PrintOptions options)
		Contract.Assert(e != null);
		Expr copy = Substituter.ApplyReplacingOldExprs(calleeSubstitution, calleeSubstitutionOld, e.Condition);

Implement verification coverage analysis #741

Implement verification coverage analysis #741

Conversation

atomb commented Jun 1, 2023 • edited Loading

keyboardDrummer commented Jun 2, 2023

keyboardDrummer left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Jun 6, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Jun 5, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

atomb Jun 2, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

atomb commented Jun 2, 2023

shazqadeer commented Jun 3, 2023 • edited Loading

keyboardDrummer commented Jun 5, 2023

keyboardDrummer Jun 5, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Jun 5, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

atomb commented Jun 5, 2023

keyboardDrummer Jun 6, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Jun 6, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

atomb commented Jun 1, 2023 •

edited

Loading

keyboardDrummer Jun 6, 2023 •

edited

Loading

keyboardDrummer Jun 5, 2023 •

edited

Loading

atomb Jun 2, 2023 •

edited

Loading

shazqadeer commented Jun 3, 2023 •

edited

Loading

keyboardDrummer Jun 5, 2023 •

edited

Loading

keyboardDrummer Jun 5, 2023 •

edited

Loading

keyboardDrummer Jun 6, 2023 •

edited

Loading

keyboardDrummer Jun 6, 2023 •

edited

Loading