-
Notifications
You must be signed in to change notification settings - Fork 266
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
[Test Generation] Change the set of coverage criteria that can be targeted #4326
Conversation
e1a37bf
to
1ca798e
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I made one suggestion about the name for the new mode. I'm not sure if it's a good one. ;)
@@ -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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You could call it CallGraph
coverage?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The fact that this is necessary suggests there's something in Boogie to fix.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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 <aarontomb@gmail.com>
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
One tiny change!
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is this text right, now that you've renamed the constructor?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Oh, right, thank you for catching this. Have fixed it in my latest commit.
…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 <fedchina@amazon.com> Co-authored-by: Aaron Tomb <aarontomb@gmail.com>
…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 <fedchina@amazon.com> Co-authored-by: Aaron Tomb <aarontomb@gmail.com>
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.