Enable IPO / LTO and -O3 #8146
Enable IPO / LTO and -O3 #8146
Conversation
rurban
commented
Dec 21, 2023
•
rurban
commented
- 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.
rurban
requested review from
peterschrammel,
tautschnig,
a team,
kroening and
remi-delmas-3000
as code owners
rurban
force-pushed
the
lto
branch
2 times, most recently
from
9c22da4 to
96e7413
Compare
rurban
force-pushed
the
lto
branch
2 times, most recently
from
162651f to
9d5b270
Compare
| #define YYEMPTY -2 | ||
| #define YYEOF 0 /* "end of file" */ | ||
| #define YYerror 256 /* error */ | ||
| #define YYUNDEF 257 /* "invalid token" */ |
There was a problem hiding this comment.
Could you please elaborate on what exactly was being warned about here?
| %token TOK_VOLATILE "volatile" | ||
| %token TOK_WCHAR_T "wchar_t" | ||
| %token TOK_WHILE "while" | ||
| %token ATOK_AUTO "auto" |
There was a problem hiding this comment.
Could you please elaborate as to why token names that ought to be local to a translation unit need to be renamed?
There was a problem hiding this comment.
Looks like %define api.token.prefix {prefix} would be the less-hacky solution, but that wouldn't work on macOS, which has bison < 3.0. So we will have to bite the bullet, thank you for coming up with this.
There was a problem hiding this comment.
Looks like
%define api.token.prefix {prefix}would be the less-hacky solution, but that wouldn't work on macOS, which has bison < 3.0. So we will have to bite the bullet, thank you for coming up with this.
The MacOS jobs in the CI pipeline are currently installing Bison version 3.8.2 from brew. There are commits following an api.token.prefix approach in this PR - #7878
|
https://lists.gnu.org/archive/html/bug-bison/2023-12/msg00001.html looks related, but hasn't seen a response as far as I can tell. |
rurban
force-pushed
the
lto
branch
4 times, most recently
from
998c03d to
2a37324
Compare
rurban
force-pushed
the
lto
branch
4 times, most recently
from
472fbfa to
7093b70
Compare
needed when doxygen is found
LTO and -O3 give a good performance improvement. I would not recommend -O3 with bad compiler versions though, such as gcc-9. WIP: GLOBAL properties are not enough, add the IPO property to all targets. Which leads to various problems still. See the next commit to fix yyalloc name collisions.
This is for CMake only as we haven't currently got an LTO set-up for Makefile builds.
to avoid -Wodr warnings
to avoid -Wodr with LTO.
to avoid LTO -Wodr warnings. yacc and flex don't support -P for these yet.
