Cleanup USE_STD_STRING/USE_DSTRING configuration option #8040
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
tautschnig
requested review from
kroening,
peterschrammel,
thomasspriggs,
NlightNFotis,
TGWDB,
esteffin,
qinheping,
feliperodri,
remi-delmas-3000 and
martin-cs
as code owners
kroening
approved these changes
Nov 15, 2023
tautschnig
force-pushed
the
cleanup/dstring
branch
from
5e02a88 to
f33959c
Compare
Codecov ReportAttention:
Additional details and impacted files@@ Coverage Diff @@
## develop #8040 +/- ##
========================================
Coverage 79.08% 79.08%
========================================
Files 1696 1696
Lines 196423 196422 -1
========================================
+ Hits 155340 155342 +2
+ Misses 41083 41080 -3 ☔ View full report in Codecov by Sentry. |
TGWDB
approved these changes
Nov 20, 2023
tautschnig
force-pushed
the
cleanup/dstring
branch
from
f33959c to
6c21ed6
Compare
peterschrammel
approved these changes
Dec 15, 2023
tautschnig
force-pushed
the
cleanup/dstring
branch
from
6c21ed6 to
f060c2f
Compare
These headers are only brought in by dstring.h, which we don't use when building with `USE_STD_STRING` set.
We keep dstringt as an implementation detail.
`USE_STD_STRING` is to be set on the build command line, but internally we always check for `USE_DSTRING`.
We must not end up with two constructors that take the same argument type.
We want comments to start with `#` and not `C_`.
We want string numbering, not string hashing. For `dstringt` these are interchangeable, but that's not the case for `std::string`.
tautschnig
force-pushed
the
cleanup/dstring
branch
from
f060c2f to
c26d38c
Compare
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this pull request
Jan 10, 2024
While diffblue#8040 ensured we were still able to compile the code base with `irep_idt` typedef'd to `std::string` (via `USE_STD_STRING`), experiments at that time also demonstrated that performance is substantially worse, and not all tests would pass. This commit now removes this untested feature to pave the way for changes that may break `dstringt` to `std::string` compatibility.
4 tasks
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this pull request
Jan 11, 2024
While diffblue#8040 ensured we were still able to compile the code base with `irep_idt` typedef'd to `std::string` (via `USE_STD_STRING`), experiments at that time also demonstrated that performance is substantially worse, and not all tests would pass. This commit now removes this untested feature to pave the way for changes that may break `dstringt` to `std::string` compatibility.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The code is now back to a compilable state when
USE_STD_STRINGis set (i.e.,irep_idtarestd::stringinstead ofdstringt). Not all tests pass as some string output is different, and performance is substantially worse. This might be enough of a reason to follow up with a PR that completely removes the possibility of usingstd::string, but I'd recommend we do so from a state where that would still have worked, i.e., only after merging this PR.