Minimal support for __builtin_unreachable
and for __builtin_expect
#394
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.
These two builtins are used by GCC and Clang as optimization hints. They occur frequently in open-source code.
This PR adds minimal support for both builtins. They are not taken into account by optimizations yet.
__builtin_unreachable
is transported all the way to assembly, where it generates no code. In the future, it could be used during the Linearize pass to remove more unreachable code.__builtin_expect
is currently removed during C2C elaboration, so it does not even enter the verified part of CompCert. If we keep it as a "no op" builtin, inefficient code is generated for comparisons on 64-bit platforms. (Because__builtin_expect
forces a conversion of its argument to typelong
.) More work is needed to take full advantage of this builtin.