Skip to content

Fix long double width on FreeBSD/PowerPC - #9148

Open
pkubaj wants to merge 1 commit into
diffblue:developfrom
pkubaj:patch-1
Open

Fix long double width on FreeBSD/PowerPC#9148
pkubaj wants to merge 1 commit into
diffblue:developfrom
pkubaj:patch-1

Conversation

@pkubaj

@pkubaj pkubaj commented Aug 3, 2026

Copy link
Copy Markdown

set_arch_spec_power() sets long_double_width to 16*8 for every PowerPC subarchitecture. That matches Linux, where long double is 128-bit IBM double-double, but not FreeBSD, where long double on PowerPC is the same as double -- with the exception of powerpc64le since FreeBSD 16.0, which uses IEEE binary128.

Because the width does not match the host, verifying natively on FreeBSD/powerpc64le aborts as soon as any tool configures itself:

--- begin invariant violation report ---
Invariant check failed
File: src/util/config.cpp:1132 function: set
Condition: ansi_c.long_double_width == sizeof(long double) * CHAR_BIT
Reason: long double width shall be equal to the system long double width
--- end invariant violation report ---
Abort trap (core dumped)

This is not hypothetical for a build either: the regression tests run the freshly built goto-gcc, so the build itself fails.

Neither constant is right for FreeBSD, as the width depends on the release:

FreeBSD 15.1, powerpc64le: sizeof(long double) * CHAR_BIT == 64
(LDBL_MANT_DIG 53)
FreeBSD 16.0, powerpc64le: sizeof(long double) * CHAR_BIT == 128
(LDBL_MANT_DIG 113, LONG_DOUBLE_IEEE128)

Take the width from the toolchain instead of hard-coding it, which is exactly the quantity the invariant compares against and stays correct across that transition. The override lives in configt::set() rather than in set_arch_spec_power(), which only receives the subarchitecture and has no way to know the target operating system; the neighbouring macos/arm64 case already sets long_double_width the same way.

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

set_arch_spec_power() sets long_double_width to 16*8 for every PowerPC
subarchitecture. That matches Linux, where long double is 128-bit IBM
double-double, but not FreeBSD, where long double on PowerPC is the same
as double -- with the exception of powerpc64le since FreeBSD 16.0, which
uses IEEE binary128.

Because the width does not match the host, verifying natively on
FreeBSD/powerpc64le aborts as soon as any tool configures itself:

  --- begin invariant violation report ---
  Invariant check failed
  File: src/util/config.cpp:1132 function: set
  Condition: ansi_c.long_double_width == sizeof(long double) * CHAR_BIT
  Reason: long double width shall be equal to the system long double width
  --- end invariant violation report ---
  Abort trap (core dumped)

This is not hypothetical for a build either: the regression tests run the
freshly built goto-gcc, so the build itself fails.

Neither constant is right for FreeBSD, as the width depends on the
release:

  FreeBSD 15.1, powerpc64le:  sizeof(long double) * CHAR_BIT == 64
                              (__LDBL_MANT_DIG__ 53)
  FreeBSD 16.0, powerpc64le:  sizeof(long double) * CHAR_BIT == 128
                              (__LDBL_MANT_DIG__ 113, __LONG_DOUBLE_IEEE128__)

Take the width from the toolchain instead of hard-coding it, which is
exactly the quantity the invariant compares against and stays correct
across that transition. The override lives in configt::set() rather than
in set_arch_spec_power(), which only receives the subarchitecture and has
no way to know the target operating system; the neighbouring
macos/arm64 case already sets long_double_width the same way.
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.

1 participant