Use C++17 #6749

tautschnig · 2022-03-23T11:40:50Z

Use C++17 now that it has become a build requirement.

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.

thomasspriggs · 2022-03-23T11:53:00Z

I am in favour of moving to C++17. This will allow us to remove the library code which has been back ported C++11, which will reduce the maintenance needed. It would also support using std::variant without having to add a back port of it.

codecov · 2022-03-23T12:47:51Z

Codecov Report

Attention: 38 lines in your changes are missing coverage. Please review.

Comparison is base (a8de0b7) 79.10% compared to head (6b691bc) 79.07%.

❗ Current head 6b691bc differs from pull request most recent head 6e1615c. Consider uploading reports for the commit 6e1615c to get more accurate results

Files	Patch %	Lines
src/goto-cc/compile.cpp	62.50%	6 Missing ⚠️
src/goto-instrument/cover.cpp	80.00%	3 Missing ⚠️
src/util/source_location.cpp	50.00%	3 Missing ⚠️
jbmc/src/jbmc/jbmc_parse_options.cpp	66.66%	2 Missing ⚠️
src/analyses/invariant_propagation.cpp	0.00%	2 Missing ⚠️
src/goto-cc/as_mode.cpp	0.00%	2 Missing ⚠️
src/goto-cc/ld_mode.cpp	0.00%	2 Missing ⚠️
src/goto-cc/ms_cl_mode.cpp	0.00%	2 Missing ⚠️
src/goto-instrument/count_eloc.cpp	0.00%	2 Missing ⚠️
jbmc/src/java_bytecode/java_bytecode_language.h	0.00%	1 Missing ⚠️
... and 13 more

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #6749      +/-   ##
===========================================
- Coverage    79.10%   79.07%   -0.03%     
===========================================
  Files         1699     1694       -5     
  Lines       196508   196276     -232     
===========================================
- Hits        155443   155204     -239     
- Misses       41065    41072       +7

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

martin-cs

In principle... OK. But:

Are there any currently supported linux distros that don't have g++ --version >= 7.0? I don't think so but RedHat and derivatives do tend to ship surprisingly old versions of tools.
I am not seeing any changes to the CI set up. Is that because all of the tested platforms are already using a suitable version?

tautschnig · 2022-03-24T01:15:52Z

In principle... OK. But:

1. Are there any currently supported linux distros that don't have `g++ --version >= 7.0`?  I don't think so but RedHat and derivatives do tend to ship surprisingly old versions of tools.

According to https://access.redhat.com/solutions/19458, only RHEL 8 has a version of GCC new enough to build current CBMC (which requires GCC 5), but then that new-enough version is GCC 8, so we should be fine. But perhaps @TGWDB has an idea whether there might be any other users who might be unable to use a new-enough version of GCC.

2. I am not seeing any changes to the CI set up.  Is that because all of the tested platforms are already using a suitable version?

That's correct, no changes needed.

tautschnig · 2022-03-24T01:26:09Z

I am in favour of moving to C++17. This will allow us to remove the library code which has been back ported C++11, which will reduce the maintenance needed. It would also support using std::variant without having to add a back port of it.

Feel free to create a PR against my branch so as to introduce the use of std::variant: I've now added a bunch of commits that make good use of C++17, mostly by removing code.

TGWDB · 2022-03-24T11:43:14Z

According to https://access.redhat.com/solutions/19458, only RHEL 8 has a version of GCC new enough to build current CBMC (which requires GCC 5), but then that new-enough version is GCC 8, so we should be fine. But perhaps @TGWDB has an idea whether there might be any other users who might be unable to use a new-enough version of GCC.

I'm not aware of Linux users who might have issues, but we need to make sure MSVC builds work. I believe as long as we have support for MSVC 2019 (currently tested in CI) we are ok.

Add missing <functional> include [blocks: #6749]

CMake/macOS: upgrade minimum version to 10.15 [blocks: #6749]

goto_rw/range_spect: wrap in a class instead of using just a typedef [blocks: #6749, #6768]

Disambiguate overloaded insert(...) calls [blocks: #6749]

Remove unqualified use of nullopt [blocks: #6749]

Replace assert(...) by macros from invariant.h [blocks: #6749]

esteffin · 2023-11-08T17:26:38Z

As already agreed this now depends on #7989

Removes third-party code that is no longer necessary now that we use C++ 17 as build standard. Future uses of optionalt should instead use std::optional directly.

With the move to C++ 17 we can use std::make_unique instead.

With the move to C++ 17 we can use std::void_t instead.

With C++ 17 we can use the STL-provided implementation instead of rolling our own (platform-dependent) code.

Python warns about the use of `\d`: we should use raw strings here as that's not meant to be an escape sequence.

See https://github.com/diffblue/cbmc/actions/runs/6856483568/job/18643716705?pr=6749 for one example of the failure: cargo-induced clang runs (via the cc crate) weren't finding the C++ library (which ought to be libc++ and not libstdc++ on this MacOS target). This appears to be caused by the minimum build target being too low (where the cc crate is the one setting that minimum). Override that by setting an environment variable. See https://github.com/rust-lang/cc-rs/blob/2d6a3b2119cf5eacc01e1f2877e064a7aede7819/src/lib.rs#L3497C52-L3497C76 for the Rust code implementing the logic.

The prefix lookup resulted in picking up the Release-Glucose cache from check-macos-12-cmake-clang. This cache, however, was established with Glucose as a SAT solver, which implies different compiler command lines. Consequently, there would be 0 cache hits.

tautschnig · 2023-11-14T13:09:39Z

Closing as all commits have been moved into PRs of their own (#8028, #8031, #8032, #8033, #8034).

tautschnig added the Version 6 Pull requests and issues requiring a major version bump label Mar 23, 2022

tautschnig self-assigned this Mar 23, 2022

martin-cs approved these changes Mar 23, 2022

View reviewed changes

tautschnig force-pushed the version-6/c++-17 branch 2 times, most recently from 5f00f86 to c4a7735 Compare March 24, 2022 01:08

tautschnig force-pushed the version-6/c++-17 branch from c4a7735 to 58e085a Compare March 24, 2022 01:21

tautschnig force-pushed the version-6/c++-17 branch 4 times, most recently from 47b6b33 to 9ba2012 Compare March 24, 2022 03:12

tautschnig force-pushed the version-6/c++-17 branch 9 times, most recently from b03ffdb to 7ad368d Compare March 25, 2022 19:29

tautschnig changed the title ~~Build using C++17~~ Build using C++17 [depends-on: #6753, #6754, #6755, #6756, #6764, #6767] Mar 25, 2022

tautschnig force-pushed the version-6/c++-17 branch from dac9f4b to 137c742 Compare March 25, 2022 21:51

tautschnig added the dependent - do not merge label Mar 25, 2022

kroening added a commit that referenced this pull request Mar 26, 2022

Merge pull request #6764 from tautschnig/cleanup/functional

e0afa1f

Add missing <functional> include [blocks: #6749]

tautschnig changed the title ~~Build using C++17 [depends-on: #6753, #6754, #6755, #6756, #6764, #6767]~~ Build using C++17 [depends-on: #6753, #6754, #6755, #6756, #6767] Mar 26, 2022

tautschnig added a commit that referenced this pull request Mar 29, 2022

Merge pull request #6767 from tautschnig/cleanup/cmake-10-15

b04b4b5

CMake/macOS: upgrade minimum version to 10.15 [blocks: #6749]

tautschnig force-pushed the version-6/c++-17 branch from 137c742 to 6cea55c Compare April 26, 2022 12:39

tautschnig mentioned this pull request Apr 26, 2022

Add support for MergeSat #6439

Open

4 tasks

tautschnig added a commit that referenced this pull request May 10, 2022

Merge pull request #6753 from tautschnig/cleanup/no-minus-one

c83dada

goto_rw/range_spect: wrap in a class instead of using just a typedef [blocks: #6749, #6768]

tautschnig added a commit that referenced this pull request May 17, 2022

Merge pull request #6755 from tautschnig/cleanup/overload

e6b943f

Disambiguate overloaded insert(...) calls [blocks: #6749]

tautschnig added a commit that referenced this pull request May 27, 2022

Merge pull request #6756 from tautschnig/cleanup/nullopt

76897ae

Remove unqualified use of nullopt [blocks: #6749]

tautschnig mentioned this pull request Sep 30, 2022

Build using C++17 #7172

Closed

4 tasks

tautschnig changed the title ~~Build using C++17 [depends-on: #6753, #6754, #6755, #6756]~~ Build using C++17 [depends-on: #6754] Nov 9, 2022

tautschnig added the blocker label Nov 9, 2022

tautschnig added a commit that referenced this pull request Dec 1, 2022

Merge pull request #6754 from tautschnig/cleanup/assert-to-invariant

8ed5e40

Replace assert(...) by macros from invariant.h [blocks: #6749]

esteffin added the Needs rebase label Nov 8, 2023

tautschnig changed the title ~~Build using C++17 [depends-on: #6754]~~ Build using C++17 Nov 13, 2023

tautschnig changed the title ~~Build using C++17~~ Use C++17 Nov 13, 2023

tautschnig removed Needs rebase dependent - do not merge labels Nov 13, 2023

tautschnig force-pushed the version-6/c++-17 branch from 6cea55c to f153827 Compare November 13, 2023 15:59

tautschnig removed the blocker label Nov 13, 2023

tautschnig force-pushed the version-6/c++-17 branch 2 times, most recently from b1f2826 to 6b691bc Compare November 14, 2023 11:46

Replace nonstd::optional by C++17 std::optional

f0262af

Removes third-party code that is no longer necessary now that we use C++ 17 as build standard. Future uses of optionalt should instead use std::optional directly.

tautschnig force-pushed the version-6/c++-17 branch from 6b691bc to 84cf0a5 Compare November 14, 2023 12:10

tautschnig added 6 commits November 14, 2023 12:53

Remove util_make_unique

56046a5

With the move to C++ 17 we can use std::make_unique instead.

Remove local declaration of void_t

2d62871

With the move to C++ 17 we can use std::void_t instead.

Replace file_util.{h,cpp} by std::filesystem

0c33e41

With C++ 17 we can use the STL-provided implementation instead of rolling our own (platform-dependent) code.

Fix invalid-escape-sequence warning

130fd65

Python warns about the use of `\d`: we should use raw strings here as that's not meant to be an escape sequence.

tautschnig force-pushed the version-6/c++-17 branch from 84cf0a5 to 6e1615c Compare November 14, 2023 12:54

tautschnig closed this Nov 14, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Use C++17 #6749

Use C++17 #6749

tautschnig commented Mar 23, 2022 •

edited

Loading

thomasspriggs commented Mar 23, 2022

codecov bot commented Mar 23, 2022 •

edited

Loading

martin-cs left a comment

tautschnig commented Mar 24, 2022

tautschnig commented Mar 24, 2022

TGWDB commented Mar 24, 2022

esteffin commented Nov 8, 2023

tautschnig commented Nov 14, 2023

Use C++17 #6749

Use C++17 #6749

Conversation

tautschnig commented Mar 23, 2022 • edited Loading

thomasspriggs commented Mar 23, 2022

codecov bot commented Mar 23, 2022 • edited Loading

Codecov Report

martin-cs left a comment

Choose a reason for hiding this comment

tautschnig commented Mar 24, 2022

tautschnig commented Mar 24, 2022

TGWDB commented Mar 24, 2022

esteffin commented Nov 8, 2023

tautschnig commented Nov 14, 2023

tautschnig commented Mar 23, 2022 •

edited

Loading

codecov bot commented Mar 23, 2022 •

edited

Loading