Skip to content

Conversation

@martin-cs
Copy link
Collaborator

This PR consists of a series of commits taken from the variable-sensitivity-domain branch originally by @hannes-steffenhagen-diffblue and @chrisr-diffblue . I have separated out the commits (and parts of commits) that just affect the sharing map so these can be reviewed and merged separately.

  • 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.

@martin-cs
Copy link
Collaborator Author

Some of these changes might now be redundant and I think it might be best to squash the commits as the messages aren't particularly meaningful now de-contextualised but I figured looking at the code might be the place to start.

@martin-cs
Copy link
Collaborator Author

Note that the linter failures are unavoidable.

typename equalT> \
type sharing_mapt<keyT, valueT, fail_if_equal, hashT, equalT>

#define SHARING_MAPTV(return_type, V) \

Choose a reason for hiding this comment

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

Given that this is used in exactly one place I’d like to voice a strong preference for just inlining this macro.

Copy link
Contributor

Choose a reason for hiding this comment

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

The already existing macro SHARING_MAPT4 does just the same, so I'd vote for using that one instead.

void get_view(viewt &view) const;
template <class V>
void get_view(V &) const;
viewt get_view() const

Choose a reason for hiding this comment

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

I suppose technically this should be a template as well now.

}
};

namespace std
Copy link
Contributor

@hannes-steffenhagen-diffblue hannes-steffenhagen-diffblue Jan 24, 2020

Choose a reason for hiding this comment

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

This is probably harmless but I think it’d nevertheless be preferable if we could find a way to do without this.

(I.e. remove it going forward after VSD is merged, not necessarily here)

@hannes-steffenhagen-diffblue
Copy link
Contributor

Linter failures should be addressed with judicious use of // NOLINT to explicitly supress linting.

typename equalT> \
type sharing_mapt<keyT, valueT, fail_if_equal, hashT, equalT>

#define SHARING_MAPTV(return_type, V) \
Copy link
Contributor

Choose a reason for hiding this comment

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

The already existing macro SHARING_MAPT4 does just the same, so I'd vote for using that one instead.

static void insert_view_item(sorted_viewt &v, view_itemt &&vi)
{
v.insert(vi);
}
Copy link
Contributor

Choose a reason for hiding this comment

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

Can we use forwarding references for these two functions? I.e.:

template <typename itemT>
static void insert_view_item(viewt &v, itemT &&vi)
{
  v.push_back(std::forward<itemT>(vi));
}

#endif

SHARING_MAPT(void)::get_view(viewt &view) const
SHARING_MAPTV(void, view_type)::get_view(view_type &view) const
Copy link
Contributor

Choose a reason for hiding this comment

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

Use SHARING_MAPT4

SECTION("View")
{
typedef std::pair<std::string, std::string> pt;
typedef std::pair<irep_idt, std::string> pt;
Copy link
Contributor

Choose a reason for hiding this comment

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

Suggest changing this back to std::string. The intention was to sort the vector in lexicographic order. However, < for irep_idt sorts according to their sequence number AFAIK.

@martin-cs martin-cs force-pushed the VSD/sharing-map branch 2 times, most recently from b5818f4 to 951cb61 Compare June 18, 2020 16:39
@martin-cs martin-cs force-pushed the VSD/sharing-map branch 3 times, most recently from 3b13122 to df7cea1 Compare June 27, 2020 11:14
@martin-cs martin-cs closed this Sep 1, 2023
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.

3 participants