Skip to content

ID_* symbols are now constexpr #2133

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

Closed
wants to merge 2 commits into from
Closed

ID_* symbols are now constexpr #2133

wants to merge 2 commits into from

Conversation

kroening
Copy link
Member

@kroening kroening commented Apr 28, 2018

This partially reverts 38782bd.

The idea is that the ID_* symbols can be constexpr, which may help a sophisticated compiler. The question whether it does should be investigated. A disadvantage is that the symbols need to be parsed twice, which may affect compile time.

@tautschnig
Copy link
Collaborator

My understanding of a past discussion of introducing constexpr on these was that we could do switch(id) { case ID_...: case ID_... } - is that genuinely the case with this patch applied? Else the value doesn't seem particularly obvious to me.

@kroening
Copy link
Member Author

Yes, you could, if you also enable the #if 0 in line 41 in src/util/dstring.h.

The key disadvantage is that this allows also all other conversions to int, e.g., in an if, or a plain assignment. The other problem is that this will never work with std::string, i.e., once we start using switch, then USE_DSTRING must be on from thereon.

It is not clear to me what the benefit of enabling the compiler to have more compile-time constants is in general. This may also change over time.

#include "irep_ids.def" // NOLINT(build/include)
};

#ifdef __GNUC__
Copy link
Contributor

Choose a reason for hiding this comment

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

Clang, MSVC 2015+ also have this. Suggest stealing the testing logic used at https://github.com/diffblue/cbmc/blob/develop/src/nonstd/optional.hpp#L87

@kroening
Copy link
Member Author

I've just added another commit that allows conversion to the enum class. This prevents accidental conversion to int, pointers, bool etc., but enables switch(some_id) { case ID_...:; }. This is a serious benefit in my view.

The price is that we have to ditch versions of Visual C++ prior to 2015. Also, we cannot use std::string any longer as alternative to the hashed strings.

Views?

@smowton
Copy link
Contributor

smowton commented May 29, 2018

Do you have any feel on how many Windows users are out there, and if so what their limitations are? We currently require MSVC2013, which is an odd version, having sort-of-but-broken C++11 support, so it would be a surprising place for people to be stuck

@kroening
Copy link
Member Author

There are some left, but are getting fewer and fewer. I'll send emails.

@kroening
Copy link
Member Author

My current view is to merge this, but not yet use switch(...) in cbmc itself for a release or two. Dependent software that is gcc/clang-only can then start using this now.

@tautschnig
Copy link
Collaborator

So what is the "enhancement" for now? Smaller binaries, faster code, something else? For sure theory tells us that the switch/case should be faster than a chain of if/else, but is this also true in practice? With dstringt being the most fundamental data structure, changes here should be accompanied by data.

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: b21d45b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85621224
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

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

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: 8765b34).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86396183
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

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

@kroening kroening force-pushed the ID_constexpr branch 2 times, most recently from 3376932 to 651af68 Compare October 11, 2018 10:16
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: 651af68).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87621638
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

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

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

@kroening kroening force-pushed the ID_constexpr branch 2 times, most recently from 4816beb to 00eb39b Compare December 9, 2018 14:03
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: 00eb39b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/94117295

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: a9af8bb).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/97924137

kroening pushed a commit that referenced this pull request Jan 22, 2019
Upgrading to VS2015 enables #3862, noexcept (e.g.  #2502), UTF8 strings and
constexpr (#2133).
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: d358fee).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98233189

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: 3ce1575).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99567549

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: c3ba809).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/100693494

@kroening kroening force-pushed the ID_constexpr branch 2 times, most recently from 65e7981 to 57751ae Compare March 17, 2019 14:06
@TGWDB
Copy link
Contributor

TGWDB commented May 3, 2023

Closing due to age (no further comment on PR content), please reopen with rebase on develop if you intent to continue this work.

@TGWDB TGWDB closed this May 3, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

6 participants