Skip to content

Goto-harness support to selectively havoc struct members #5183

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

Conversation

xbauch
Copy link
Contributor

@xbauch xbauch commented Nov 13, 2019

By means of a new option havoc-member the user can now specify a struct-within-struct path, e.g. struct_outer.struct_inner.data to specify only which member they want to havoc.

Includes a test.

  • Each commit message has a non-empty body, explaining why the change was made.
  • Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • White-space or formatting changes outside the feature-related changed lines are in commits of their own.

Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

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

✔️
Passed Diffblue compatibility checks (cbmc commit: d9a1bb4).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/136301109

Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

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

✔️
Passed Diffblue compatibility checks (cbmc commit: f096f4d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/136317859

@@ -16,6 +16,7 @@ Author: Diffblue Ltd.
#define COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT "max-array-size"
#define COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT \
"function-pointer-can-be-null"
#define COMMON_HARNESS_GENERATOR_MEMBER_SELECTION_OPT "member-selection"

Choose a reason for hiding this comment

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

I don’t really like the name member-selection, following the pattern it should be called something like nondet-member or havoc-member

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Done.

@@ -85,6 +86,22 @@ bool recursive_initialization_configt::handle_option(
[](const std::string &opt) -> irep_idt { return irep_idt{opt}; });
return true;
}
else if(option == COMMON_HARNESS_GENERATOR_MEMBER_SELECTION_OPT)

Choose a reason for hiding this comment

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

Correct me if I’m wrong, but this looks as if you can only have one member havoc'd at a time? Because that shouldn’t be the case.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Done.

to goto-harness. By means of a new option `member-selection` the user can now
specify a struct-within-struct path, e.g. `struct_outer.struct_inner.data` to
specify only which member they want to havoc. Includes a test.
via a comma-separated list. Plus one more test.
@xbauch xbauch force-pushed the feature/selective-struct-havoc branch from f096f4d to 65bfa60 Compare January 28, 2020 12:54
@xbauch xbauch changed the title Goto-harness support to selectively havoc struct members [depends-on: #5176] Goto-harness support to selectively havoc struct members Jan 28, 2020
@xbauch xbauch marked this pull request as ready for review January 28, 2020 12:54
Copy link
Contributor

@NlightNFotis NlightNFotis left a comment

Choose a reason for hiding this comment

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

LGTM

Copy link
Contributor

Choose a reason for hiding this comment

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

👍

@hannes-steffenhagen-diffblue
Copy link
Contributor

Now we’d probably also want things like “these two fields in this struct can point to the same variable” or “this field in that struct is the length of the array in that struct”, but not in this PR

@hannes-steffenhagen-diffblue hannes-steffenhagen-diffblue merged commit dbac963 into diffblue:develop Jan 28, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants