Fix long double width on FreeBSD/PowerPC

[pkubaj]

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.

[kroening]

I appreciate that this will fix the assertion failure. However, please keep in mind that this code path is designed to allow "cross-architecture verification", much like "cross compilation". I would hence set the width to a constant based on the OS.

[pkubaj]

That is not really possible.

1. All powerpc64 use 64-bit long double - that can be hard coded just fine.
2. powerpc64le before 16.0 matches powerpc64.
3. However, powerpc64le has recently (in 16.0) switched to IEEE 128-bit long double, so hardcoding 64-bit will break it.

If you want it hardcoded, is it OK if I first check for powerpc64le on a recent 16.0 and set 128b if true and fall back to 64b on anything else?

[kroening]

That is not really possible.

1. All powerpc64 use 64-bit long double - that can be hard coded just fine.
2. powerpc64le before 16.0 matches powerpc64.
3. However, powerpc64le has recently (in 16.0) switched to IEEE 128-bit long double, so hardcoding 64-bit will break it.

If you want it hardcoded, is it OK if I first check for powerpc64le on a recent 16.0 and set 128b if true and fall back to 64b on anything else?

Indeed not easy to fix.

I am ok with dropping cross-verification support for FreeBSD prior to 16.0; i.e., you'd add a branch to the case where a) you are targeting FreeBSD, and b) running on FreeBSD, and then you use what sizeof says.

Cross-verification would use the FreeBSD 16.0 value.

[pkubaj]

Done - native path uses sizeof, cross-verification uses the FreeBSD 16.0 value (128-bit for ppc64le, 64-bit for powerpc/ppc64), so pre-16.0 cross-verification is dropped as you suggested.

One refinement: rather than checking "running on FreeBSD", I reused the existing arch == this_arch && os == this_os predicate that already guards the type-width invariants a few lines below. An OS-only check would misfire on
FreeBSD/amd64 targeting FreeBSD/ppc64 big-endian, where sizeof(long double) is 128 (x87 80-bit padded to 16 bytes) but the correct width is 64. Sharing the invariant's own predicate also means the two can't drift apart.

[kroening]

Looks good, thank you

[codecov]

Codecov Report

❌ Patch coverage is 25.00000% with 6 lines in your changes missing coverage. Please review.
✅ Project coverage is 80.83%. Comparing base (9e80cec) to head (fc53837).
⚠️ Report is 11 commits behind head on develop.

Files with missing lines	Patch %	Lines
src/util/config.cpp	25.00%	6 Missing ⚠️

Additional details and impacted files

@@            Coverage Diff            @@
##           develop    #9148    +/-   ##
=========================================
  Coverage    80.83%   80.83%            
=========================================
  Files         1715     1717     +2     
  Lines       189957   190069   +112     
  Branches        73       73            
=========================================
+ Hits        153549   153644    +95     
- Misses       36408    36425    +17     

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

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.