Skip to content
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

Support __float128 with GCC on Apple Silicon #8319

Closed
wants to merge 3 commits into from
Closed

Support __float128 with GCC on Apple Silicon #8319

wants to merge 3 commits into from

Conversation

tautschnig
Copy link
Collaborator

@tautschnig tautschnig commented Jun 11, 2024 •
edited
Loading

Although not officially documented it seems that GCC running on Apple Silicon accepts __float128 as a keyword.

Fixes: #8305

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

@tautschnig tautschnig mentioned this pull request Jun 11, 2024
Closed
@kroening
Copy link
Member

Is it a built-in typedef or a keyword?

kroening
kroening reviewed Jun 11, 2024
View reviewed changes
src/ansi-c/ansi_c_internal_additions.cpp Outdated
config.ansi_c.arch == "arm64" &&
config.ansi_c.os == configt::ansi_ct::ost::OS_MACOS &&
config.ansi_c.mode != configt::ansi_ct::flavourt::CLANG &&
config.ansi_c.gcc__float128_type)
Copy link
Member

Choose a reason for hiding this comment

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

Can gcc__float128_type be false when running GCC on ARM64 Macs?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

It is quite possible that no such (old) GCC version even builds on ARM64 Macs, so likely: no.

@tautschnig
Copy link
Collaborator Author

Is it a built-in typedef or a keyword?

Ah, it indeed appears to be a keyword. I have updated all comments to reflect this (and explain why we still handle it as if it were a typedef).

@codecov Codecov
Copy link

codecov bot commented Jun 11, 2024 •
edited
Loading

Codecov Report

Attention: Patch coverage is 44.00000% with 14 lines in your changes missing coverage. Please review.

Project coverage is 78.27%. Comparing base (2a5151c) to head (956a8f5).

Files Patch % Lines
src/util/config.cpp 7.69% 12 Missing ⚠️
src/ansi-c/gcc_version.cpp 66.66% 2 Missing ⚠️
Additional details and impacted files 
@@             Coverage Diff             @@
##           develop    #8319      +/-   ##
===========================================
- Coverage    78.32%   78.27%   -0.06%     
===========================================
  Files         1722     1722              
  Lines       188404   188546     +142     
  Branches     18454    18522      +68     
===========================================
+ Hits        147572   147582      +10     
- Misses       40832    40964     +132

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

@kroening
Copy link
Member

Is it a built-in typedef or a keyword?

Ah, it indeed appears to be a keyword. I have updated all comments to reflect this (and explain why we still handle it as if it were a typedef).

I'd be in favour of adding PARSER.__float128_keyword or the like.

@tautschnig
Copy link
Collaborator Author

I'd be in favour of adding PARSER.__float128_keyword or the like.

I've added a second commit that changes the approach implement your suggestion.

@kroening
Copy link
Member

There's lots of instances of getting the clang version here, which is expensive, and we don't appear to be using the version number of clang.

@tautschnig
Copy link
Collaborator Author

There's lots of instances of getting the clang version here, which is expensive, and we don't appear to be using the version number of clang.

We don't need the version number of clang for this one, but actually this amounts to a bugfix: https://github.com/diffblue/cbmc/blob/develop/src/ansi-c/gcc_version.cpp#L166-L183 actually want the version number.

@tautschnig tautschnig force-pushed the bugfixes/8305-__float128 branch 2 times, most recently from 1a66500 to 1a776dd Compare June 12, 2024 14:59
@tautschnig
Support __float128 with GCC on Apple Silicon
94bf7a5 
Although not officially documented it seems that GCC running on Apple
Silicon accepts __float128 as a keyword.

Fixes: diffblue#8305
@tautschnig
Be precise as to whether __float128 is a keyword or a typedef
39fc958 
Add a new parser configuration setting to correctly configure the
scanner.
@tautschnig
Clang configuration: apply defaults rather than using configure_gcc
956a8f5 
This isn't as precise, but will avoid the cost of process invocation.
Such cost is considerable on Windows and appears to be around 100ms on
macOS.
feliperodri
feliperodri approved these changes Jun 14, 2024
View reviewed changes
Copy link
Collaborator

@feliperodri feliperodri left a comment

Choose a reason for hiding this comment

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

I assume there are regression tests covering these cases.

@tautschnig
Copy link
Collaborator Author

I assume there are regression tests covering these cases.

With #8328 they will!

@tautschnig
Copy link
Collaborator Author

Closing as the commits are now part of #8328.

@tautschnig tautschnig closed this Jun 15, 2024
@tautschnig tautschnig deleted the bugfixes/8305-__float128 branch June 15, 2024 18:39
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kroening kroening kroening approved these changes

@feliperodri feliperodri feliperodri approved these changes

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

@remi-delmas-3000 remi-delmas-3000 Awaiting requested review from remi-delmas-3000 remi-delmas-3000 is a code owner

@qinheping qinheping Awaiting requested review from qinheping

@martin-cs martin-cs Awaiting requested review from martin-cs

@esteffin esteffin Awaiting requested review from esteffin

@TGWDB TGWDB Awaiting requested review from TGWDB

Assignees

@tautschnig tautschnig

@kroening kroening

Labels
bugfix C Front End
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

CBMC fails to co-exist with GCC 13
5 participants
@tautschnig @kroening @feliperodri @remi-delmas-3000 @peterschrammel