Cleanup processing and use __builtin_X_overflow #6612
Merged
Conversation
This file contains hidden or 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
force-pushed
the
cleanup/c-library-overflow
branch
4 times, most recently
from
efd093d to
582644e
Compare
Codecov Report
@@ Coverage Diff @@
## develop #6612 +/- ##
========================================
Coverage 76.64% 76.65%
========================================
Files 1578 1578
Lines 181199 181219 +20
========================================
+ Hits 138875 138907 +32
+ Misses 42324 42312 -12
Continue to review full report at Codecov.
|
tautschnig
force-pushed
the
cleanup/c-library-overflow
branch
from
582644e to
a932759
Compare
chrisr-diffblue
approved these changes
Jan 27, 2022
tautschnig
force-pushed
the
cleanup/c-library-overflow
branch
from
a932759 to
1e8d3ab
Compare
Move the implementation to a method of its own. This avoids repeatedly testing the name to derive the underlying arithmetic operation. This change is to support upcoming extensions to handle further built-ins via this code path. No changes in behaviour intended with just this commit, and additional testing should ensure that this is also true for error handling. The function refactored from remains too large, and cpplint rightly complains about that, but this issue cannot be fixed in a single commit. Hence, adding an override.
…cker The models in the C library incurred unnecessary overhead in that they would do the arithmetic operation twice: once for the actual (possibly overflowing) result, and once for determining the overflow bit.
tautschnig
force-pushed
the
cleanup/c-library-overflow
branch
from
1e8d3ab to
9d91abc
Compare
We just need to provide the declarations in case the underlying compiler isn't GCC.
The use of GCC built-ins allows us to avoid the duplicate multiplication (and addition) that __CPROVER_overflow_OP plus the actual result computation would entail.
tautschnig
force-pushed
the
cleanup/c-library-overflow
branch
from
9d91abc to
291c72a
Compare
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.
With thanks to @danielsn for reminding me of this: on the back of #6607 we realised that our C front-end should also make use of those GCC built-ins to avoid doing duplicate work. For the C library this may improve performance when verification tasks use
callocorstrtol.Please review commit-by-commit.