[Test Generation] Change the set of coverage criteria that can be targeted #4326
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Dargones
force-pushed
the
InilneOptimization
branch
from
e1a37bf
to
1ca798e
Compare
Dargones
changed the title
atomb
previously approved these changes
Aug 9, 2023
| @@ -8,7 +8,7 @@ public class TestGenerationOptions { | |||
| public const string TestInlineAttribute = "testInline"; | |||
| public const string TestEntryAttribute = "testEntry"; | |||
| public bool WarnDeadCode = false; | |||
| public enum Modes { None, Block, Path }; | |||
| public enum Modes { None, Block, Branch, Path }; | |||
There was a problem hiding this comment.
You could call it CallGraph coverage?
There was a problem hiding this comment.
I think CallGraph works great, thank you! Have renamed it
| /// <summary> | ||
| /// Constructs a binary tree of disjunctions made up of <param name="clauses"></param> | ||
| /// This limits the depth of the resulting AST and prevents stack overflow during verification for large trees | ||
| /// </summary> |
There was a problem hiding this comment.
The fact that this is necessary suggests there's something in Boogie to fix.
There was a problem hiding this comment.
I only encountered a stack overflow once when I had to construct a conjunction of about 1000 variables, so I don't think this is a common scenario but yes, it should be possible to optimize Boogie to avoid this.
Co-authored-by: Aaron Tomb <[email protected]>
atomb
requested changes
Aug 9, 2023
| branch - Prints branch-coverage tests for the given program. | ||
| path - Prints path-coverage tests for the given program."); | ||
| Block - Prints block-coverage tests for the given program. | ||
| Branch - Prints call-graph-coverage tests for the given program. |
There was a problem hiding this comment.
Is this text right, now that you've renamed the constructor?
There was a problem hiding this comment.
Oh, right, thank you for catching this. Have fixed it in my latest commit.
atomb
approved these changes
Aug 9, 2023
keyboardDrummer
pushed a commit
to keyboardDrummer/dafny
that referenced
this pull request
Sep 15, 2023
…geted (dafny-lang#4326) This PR changes what coverage criteria a user of test generation may target. - Path coverage: Dafny will now attempt complete path coverage of the (inlined part of the) program as oppose to covering paths through each method in isolation. As a means of dealing with path explosion, Dafny will now try generating tests for increasingly longer paths, skipping over any paths whose subpaths have been found to be infeasible. - Branch coverage: As an middle ground between path coverage and block coverage, Dafny can now attempt call-graph-sensitive version of block coverage (i.e. it tries to cover every block in the program for every path through the call graph that can lead to that block). I call this "call-graph" coverage but am not sure this is the best way to call it - would be grateful for any suggestions. This PR relies on a [recent change](boogie-org/boogie#753) in Boogie that fixes a bug in how inlined programs are printed to a file. By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license. --------- Co-authored-by: Aleksandr Fedchin <[email protected]> Co-authored-by: Aaron Tomb <[email protected]>
keyboardDrummer
pushed a commit
that referenced
this pull request
Sep 19, 2023
…geted (#4326) This PR changes what coverage criteria a user of test generation may target. - Path coverage: Dafny will now attempt complete path coverage of the (inlined part of the) program as oppose to covering paths through each method in isolation. As a means of dealing with path explosion, Dafny will now try generating tests for increasingly longer paths, skipping over any paths whose subpaths have been found to be infeasible. - Branch coverage: As an middle ground between path coverage and block coverage, Dafny can now attempt call-graph-sensitive version of block coverage (i.e. it tries to cover every block in the program for every path through the call graph that can lead to that block). I call this "call-graph" coverage but am not sure this is the best way to call it - would be grateful for any suggestions. This PR relies on a [recent change](boogie-org/boogie#753) in Boogie that fixes a bug in how inlined programs are printed to a file. By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license. --------- Co-authored-by: Aleksandr Fedchin <[email protected]> Co-authored-by: Aaron Tomb <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR changes what coverage criteria a user of test generation may target.
Path coverage: Dafny will now attempt complete path coverage of the (inlined part of the) program as oppose to covering paths through each method in isolation. As a means of dealing with path explosion, Dafny will now try generating tests for increasingly longer paths, skipping over any paths whose subpaths have been found to be infeasible.
Branch coverage: As an middle ground between path coverage and block coverage, Dafny can now attempt call-graph-sensitive version of block coverage (i.e. it tries to cover every block in the program for every path through the call graph that can lead to that block). I call this "branch" coverage but am not sure this is the best way to call it - would be grateful for any suggestions.
This PR relies on a recent change in Boogie that fixes a bug in how inlined programs are printed to a file.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.