Skip to content

Add __builtin_add_overflow primitives #5233

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.

Sign up for GitHub

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

Jump to bottom
Merged
merged 2 commits into from
Feb 14, 2020
Merged

Add __builtin_add_overflow primitives #5233

merged 2 commits into from
Feb 14, 2020

Conversation

hannes-steffenhagen-diffblue
Copy link
Contributor

@hannes-steffenhagen-diffblue hannes-steffenhagen-diffblue commented Feb 13, 2020 •
edited
Loading

This addresses part of #4701. Only add primitives in this PR. Note gcc also has a generic __builtin_add_overflow which isn’t implemented here. The issue also has some discussion about making overflow checks faster, this also isn’t implemented here.

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

@hannes-steffenhagen-diffblue
Fix cprover_library.inc dependencies in CMake
fa1f359 
`cprover_library.inc` should depend on the *.c files, not just the converter
itself.
xbauch
xbauch approved these changes Feb 13, 2020
View reviewed changes
Copy link
Contributor

@xbauch xbauch left a comment

Choose a reason for hiding this comment

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

Looks good.

chrisr-diffblue
chrisr-diffblue reviewed Feb 13, 2020
View reviewed changes
regression/cbmc/gcc_builtin_add_overflow/main.c
@@ -0,0 +1,80 @@
#include <limits.h>
#include <assert.h>

Copy link
Contributor

Choose a reason for hiding this comment

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

Tests look good, but could we add a few more cases? In particular, these tests only cover some of the "easily optimised" cases (e.g value of 1, adding/subtracting to MAX/MIN), but it would be great to see some tests that also cover "mid-range value x + mid-range value y == overflow" and "slightly smaller mid-range value x + mid-range value y != overflow" cases.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

@chrisr-diffblue I’ve added some more cases to that end

chrisr-diffblue
chrisr-diffblue approved these changes Feb 13, 2020
View reviewed changes
Copy link
Contributor

@chrisr-diffblue chrisr-diffblue left a comment

Choose a reason for hiding this comment

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

Looks good, and thanks for expanding the tests.

@codecov-io
Copy link

codecov-io commented Feb 13, 2020 •
edited
Loading

Codecov Report

Merging #5233 into develop will increase coverage by <.01%.
The diff coverage is n/a.

Impacted file tree graph

@@             Coverage Diff             @@
##           develop    #5233      +/-   ##
===========================================
+ Coverage    67.51%   67.51%   +<.01%     
===========================================
  Files         1161     1161              
  Lines        95501    95501              
===========================================
+ Hits         64479    64481       +2     
+ Misses       31022    31020       -2
Flag Coverage Δ
#cproversmt2 42.6% <ø> (+0.01%) ⬆️
#regression 64.04% <ø> (ø) ⬆️
#unit 31.9% <ø> (ø) ⬆️
Impacted Files Coverage Δ
src/ansi-c/c_typecheck_expr.cpp 74.18% <0%> (+0.15%) ⬆️

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 86d36f6...448906f. Read the comment docs.

@NlightNFotis NlightNFotis merged commit ef623c2 into diffblue:develop Feb 14, 2020
@hannes-steffenhagen-diffblue hannes-steffenhagen-diffblue mentioned this pull request Feb 17, 2020
Merged
7 tasks
@danpoe danpoe mentioned this pull request Jul 1, 2020
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@NlightNFotis NlightNFotis NlightNFotis approved these changes

@danpoe danpoe danpoe approved these changes

@xbauch xbauch xbauch approved these changes

@chrisr-diffblue chrisr-diffblue chrisr-diffblue approved these changes

@kroening kroening Awaiting requested review from kroening kroening is a code owner

@tautschnig tautschnig Awaiting requested review from tautschnig tautschnig is a code owner

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
6 participants
@hannes-steffenhagen-diffblue @codecov-io @NlightNFotis @danpoe @xbauch @chrisr-diffblue