Skip to content

Refactor in value_set #4702

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.

Sign up for GitHub

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

Jump to bottom
Merged
merged 5 commits into from
May 29, 2019
Merged

Refactor in value_set #4702

merged 5 commits into from
May 29, 2019

Conversation

romainbrenguier
Copy link
Contributor

This improves logging of debug information and clarifies the definition of values and retained_values

  • Each commit message has a non-empty body, explaining why the change was made.
  • [na] Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • [na] 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).
  • [na] My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • [na] White-space or formatting changes outside the feature-related changed lines are in commits of their own.

smowton
smowton approved these changes May 24, 2019
View reviewed changes
src/pointer-analysis/value_set_dereference.cpp
@@ -147,8 +146,9 @@ exprt value_set_dereferencet::dereference(const exprt &pointer)
std::cout << '}' << std::endl;
#endif

for(const auto &value : retained_values)
values.push_back(build_reference_to(value, compare_against_pointer, ns));
std::list<valuet> values =
Copy link
Contributor

Choose a reason for hiding this comment

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

While you're here: consider not using std::list, since we don't need any of the properties of a doubly-linked list here

Copy link
Contributor

Choose a reason for hiding this comment

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

To be clear, you're suggesting using std::forward_list, right?

Copy link
Contributor

Choose a reason for hiding this comment

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

I'm suggesting std::vector, as the default sequence container if you don't need particular insertion / deletion / iterator stability properties

owen-mc-diffblue
owen-mc-diffblue approved these changes May 24, 2019
View reviewed changes
src/pointer-analysis/value_set.h Outdated
void output(
const namespacet &ns,
std::ostream &out) const;
std::ostream &out,
std::string indent = "") const;
Copy link
Contributor

Choose a reason for hiding this comment

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

(a) const
(b) take by reference?

src/pointer-analysis/value_set_dereference.cpp
@@ -147,8 +146,9 @@ exprt value_set_dereferencet::dereference(const exprt &pointer)
std::cout << '}' << std::endl;
#endif

for(const auto &value : retained_values)
values.push_back(build_reference_to(value, compare_against_pointer, ns));
std::list<valuet> values =
Copy link
Contributor

Choose a reason for hiding this comment

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

To be clear, you're suggesting using std::forward_list, right?

src/pointer-analysis/value_set_dereference.cpp Outdated
values.push_back(build_reference_to(value, compare_against_pointer, ns));
std::list<valuet> values =
make_range(retained_values).map([&](const exprt &value){
return build_reference_to(value, compare_against_pointer, ns);});
Copy link
Contributor

@owen-mc-diffblue owen-mc-diffblue May 24, 2019 •
edited
Loading

Choose a reason for hiding this comment

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

Is this better than using std::transform with std::back_inserter(values) and the same lambda? I guess it lets you make it const, and it's slightly easier to read.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

It's mostly the same thing as std::transform but I find the range version clearer

src/pointer-analysis/value_set_dereference.cpp
const std::vector<exprt> retained_values =
make_range(points_to_set).filter([&](const exprt &value) {
return !should_ignore_value(value, exclude_null_derefs, language_mode);
});
Copy link
Contributor

Choose a reason for hiding this comment

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

Again, could use std::transform

Copy link
Contributor Author

Choose a reason for hiding this comment

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

you mean copy_if I think

@tautschnig
Copy link
Collaborator

@romainbrenguier clang-format and cpp-lint aren't happy.

@romainbrenguier romainbrenguier force-pushed the refactor/value-set branch 2 times, most recently from e7aca28 to 9293111 Compare May 28, 2019 10:08
@romainbrenguier
Improve debug logging of value_set_dereferencet
f2d42eb 
Use #ifdef DEBUG instead of #if 0 so that compilation of the code can be
tested on CI, and make the messages more explecit so that their origin
can be recovered when seen in the logs.
@romainbrenguier
Add indent argument to value_set output
bb9e9cc 
Allows to customize the indentation of the output, for clearer logging
of the value set.
@romainbrenguier
Improve debug logging in get_value_set
4e353d3 
Use #ifdef DEBUG instead of #if 0 so that compilation can be checked on
CI; give more information about what we are logging; which also makes it
easier to find the origin of the output when seen from logs.
@romainbrenguier
Use ranget map to get values
36e9770 
This allows `values` to be const and clarifies that this list is
a direct mapping from retained_values.
@romainbrenguier
Use ranget fiter for retained_values in dereference
4f40147 
This makes it clearer that retained_values corresponds to a filtered
`points_to_set` and allows retained values to be const.
allredj
allredj reviewed May 28, 2019
View reviewed changes
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.

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 4f40147).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/113459194
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

@romainbrenguier romainbrenguier merged commit abd2628 into diffblue:develop May 29, 2019
@romainbrenguier romainbrenguier deleted the refactor/value-set branch May 29, 2019 05:41
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@smowton smowton smowton approved these changes

@allredj allredj allredj left review comments

@owen-mc-diffblue owen-mc-diffblue owen-mc-diffblue approved these changes

@chrisr-diffblue chrisr-diffblue Awaiting requested review from chrisr-diffblue

@kroening kroening Awaiting requested review from kroening kroening is a code owner

@martin-cs martin-cs Awaiting requested review from martin-cs martin-cs is a code owner

@peterschrammel peterschrammel Awaiting requested review from peterschrammel peterschrammel is a code owner

@tautschnig tautschnig Awaiting requested review from tautschnig tautschnig is a code owner

Assignees

@romainbrenguier romainbrenguier

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@romainbrenguier @tautschnig @smowton @allredj @owen-mc-diffblue