Skip to content

C front-end: evaluate __builtin_clz over constants #5735

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.

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

Merged
merged 2 commits into from
Jan 13, 2021

Conversation

tautschnig
Copy link
Collaborator

The Linux kernel uses __builtin_clz(ll) in expressions that are expected
to be compile-time constants. To support this, evaluate such expressions
during type checking.

  • Each commit message has a non-empty body, explaining why the change was made.
  • n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • n/a 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).
  • n/a My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@codecov
Copy link

codecov bot commented Jan 10, 2021

Codecov Report

Merging #5735 (fef9e89) into develop (291c973) will decrease coverage by 37.32%.
The diff coverage is 18.75%.

Impacted file tree graph

@@             Coverage Diff              @@
##           develop    #5735       +/-   ##
============================================
- Coverage    69.54%   32.22%   -37.33%     
============================================
  Files         1243      985      -258     
  Lines       100700    83689    -17011     
============================================
- Hits         70036    26970    -43066     
- Misses       30664    56719    +26055     
Flag Coverage Δ
cproversmt2 ?
regression ?
unit 32.22% <18.75%> (-0.01%) ⬇️

Flags with carried forward coverage won't be shown. Click here to find out more.

Impacted Files Coverage Δ
src/ansi-c/c_typecheck_expr.cpp 22.33% <18.75%> (-53.59%) ⬇️
src/cpp/cpp_id.h 0.00% <0.00%> (-100.00%) ⬇️
src/cpp/cpp_scope.h 0.00% <0.00%> (-100.00%) ⬇️
src/cpp/cpp_token.h 0.00% <0.00%> (-100.00%) ⬇️
src/cpp/cpp_name.cpp 0.00% <0.00%> (-100.00%) ⬇️
src/cpp/cpp_util.cpp 0.00% <0.00%> (-100.00%) ⬇️
src/util/identifier.h 0.00% <0.00%> (-100.00%) ⬇️
src/xmllang/graphml.h 0.00% <0.00%> (-100.00%) ⬇️
src/cpp/cpp_is_pod.cpp 0.00% <0.00%> (-100.00%) ⬇️
src/cpp/template_map.h 0.00% <0.00%> (-100.00%) ⬇️
... and 946 more

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 291c973...fef9e89. Read the comment docs.

@kroening
Copy link
Member

We seem to have a variety of ways to assert that something can be simplified, and perhaps we should consolidate. This test, I believe, introduces a new way.
Would using static_assert be a good, standard-compilant alternative here?

@tautschnig
Copy link
Collaborator Author

We seem to have a variety of ways to assert that something can be simplified, and perhaps we should consolidate. This test, I believe, introduces a new way.
Would using static_assert be a good, standard-compilant alternative here?

You're of course right, this is a much better approach. Done.

!int_constant.has_value() || *int_constant == 0 ||
argument.type().id() != ID_unsignedbv)
{
return nil_exprt{};
Copy link
Member

Choose a reason for hiding this comment

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

What happens here?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

That just means it will be treated as a regular function call, not a "special function." So we fall back to using the library implementation.

^warning: ignoring
--
For this example, __builtin_clz is fully evaluated in the front-end. This test
ensures that the function call no longer shows up.
Copy link
Collaborator

Choose a reason for hiding this comment

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

Does it actually check that the function call is gone?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Thank you for pointing out this outdated comment! This is now fixed.

This avoids warnings about missing declarations.
The Linux kernel uses __builtin_clz{,l,ll} in expressions that are expected
to be compile-time constants. To support this, evaluate such expressions
during type checking.
@kroening kroening merged commit 0312102 into diffblue:develop Jan 13, 2021
@tautschnig tautschnig deleted the clz-cmopile-time branch January 13, 2021 15:59
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants