Model x86 80-bit extended long double precisely#9023
Open
tautschnig wants to merge 4 commits into
Open
Conversation
tautschnig
requested review from
TGWDB,
jimgrundy,
kroening,
martin-cs and
peterschrammel
as code owners
There was a problem hiding this comment.
Pull request overview
This PR updates CBMC’s modelling of long double on x86 to match real x87 80-bit extended-precision object representation (80-bit value stored in 12/16 bytes with padding), so byte-level observations (e.g., macOS SDK signbitl union patterns) behave correctly.
Changes:
- Introduces explicit “value width” vs “storage width” handling in
ieee_float_spect, and updates constant pack/unpack for x86-extended encodings. - Updates FloatBV expression/SAT encoders and
ID_signhandling to use the correct sign/exponent positions for x86-extendedlong double. - Adds regression + unit tests and documents the x86
long doublelayout; marks several long-double math models asKNOWNBUGdue to binary128-specific bit tricks.
Reviewed changes
Copilot reviewed 25 out of 25 changed files in this pull request and generated 10 comments.
Show a summary per file
| File | Description |
|---|---|
| unit/util/ieee_float.cpp | Adds unit tests for x86-extended specs and pack/unpack round-trips. |
| src/util/ieee_float.h | Adds storage_width_bits and value_width() vs width() distinction; adds x86 spec factories. |
| src/util/ieee_float.cpp | Updates from_type and implements x86-extended pack/unpack layout handling. |
| src/util/c_types.cpp | Selects x86-extended long double specs for x86_64/i386 configurations. |
| src/solvers/floatbv/float_utils.h | Adjusts float sign-bit access for x86-extended padded storage. |
| src/solvers/floatbv/float_utils.cpp | Updates SAT-level float ops/classification for x86-extended layout and integer bit semantics. |
| src/solvers/floatbv/float_bv.cpp | Updates expression-level float ops/classification for x86-extended layout (sign/exponent/integer bit). |
| src/solvers/flattening/boolbv.cpp | Fixes ID_sign extraction for floatbv when sign isn’t at the storage MSB. |
| regression/cbmc/long-double-x86-bytes/test.desc | New regression test descriptor for x86_64 byte layout; SMT backend tagged broken. |
| regression/cbmc/long-double-x86-bytes/main.c | New regression test asserting exact x86_64 long double bytes/mantissa/sexp fields. |
| regression/cbmc/long-double-signbit-x86/test.desc | New regression test descriptor for macOS-style signbitl pattern; SMT backend tagged broken. |
| regression/cbmc/long-double-signbit-x86/main.c | New regression test replicating the macOS SDK union-based signbit extraction. |
| regression/cbmc/long-double-roundtrip-x86/test.desc | New regression test descriptor for double↔long double round-trip; SMT backend tagged broken. |
| regression/cbmc/long-double-roundtrip-x86/main.c | New regression test for constant + symbolic double↔long double round-trips. |
| regression/cbmc/long-double-pseudo-encodings/test.desc | New regression test descriptor for rejecting x86 pseudo-encodings; SMT backend tagged broken. |
| regression/cbmc/long-double-pseudo-encodings/main.c | New regression test ensuring isnan/isinf/isnormal reject x86 pseudo-encodings. |
| regression/cbmc/long-double-i386-bytes/test.desc | New regression test descriptor for i386 12-byte storage layout; SMT backend tagged broken. |
| regression/cbmc/long-double-i386-bytes/main.c | New regression test asserting i386 long double size/layout. |
| regression/cbmc-library/logl/test.desc | Marks logl model test as KNOWNBUG under new layout; adds explanation. |
| regression/cbmc-library/log2l/test.desc | Marks log2l model test as KNOWNBUG under new layout; adds explanation. |
| regression/cbmc-library/log10l/test.desc | Marks log10l model test as KNOWNBUG under new layout; adds explanation. |
| regression/cbmc-library/expl/test.desc | Marks expl model test as KNOWNBUG under new layout; adds explanation. |
| regression/cbmc-library/exp2l/test.desc | Marks exp2l model test as KNOWNBUG under new layout; adds explanation. |
| regression/cbmc-library/__builtin_powil/test.desc | Marks __builtin_powil model test as KNOWNBUG under new layout; adds explanation. |
| doc/architectural/x86-long-double.md | Adds architectural documentation for x86 long double modelling and code paths. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
823
to
830
| // Check all value bits except the sign bit are zero. | ||
| // For x86 extended in padded storage, the sign is at value_width()-1 | ||
| // and padding bits above are always zero (so we can just check all | ||
| // bits except the sign position). | ||
| bvt all_but_sign = src; | ||
| const std::size_t sign_pos = spec.value_width() - 1; | ||
| all_but_sign.erase(all_but_sign.begin() + sign_pos); | ||
| return bv_utils.is_zero(all_but_sign); |
Comment on lines
259
to
262
| const mp_integer all_ones = power(2, width) - 1; | ||
| const mp_integer sign_bit_mask = power(2, spec.value_width() - 1); | ||
| const mp_integer v = all_ones - sign_bit_mask; | ||
|
|
Comment on lines
+196
to
+219
| // x86_64 typically stores `long double` as the x87 80-bit extended | ||
| // format in 16 bytes (Linux, macOS, FreeBSD). i386 stores it in 12 | ||
| // bytes. Accurate modelling matters because programs (notably the | ||
| // Apple SDK's <math.h> inline helpers) read the bytes via union-based | ||
| // bit twiddling. | ||
| const auto &c = config.ansi_c; | ||
| if(c.long_double_width == 128 && (c.arch == "x86_64" || c.arch == "i386")) | ||
| { | ||
| // x86 extended precision has 80 bits in total, and | ||
| // deviating from IEEE, does not use a hidden bit. | ||
| // We use the closest we have got, but the below isn't accurate. | ||
| result=ieee_float_spect(63, 15).to_type(); | ||
| result = ieee_float_spect::x86_128().to_type(); | ||
| } | ||
| else if(config.ansi_c.long_double_width==96) | ||
| else if(c.long_double_width == 96 && c.arch == "i386") | ||
| { | ||
| result=ieee_float_spect(80, 15).to_type(); | ||
| // not quite right. The extra bits beyond 80 are usually padded. | ||
| result = ieee_float_spect::x86_96().to_type(); | ||
| } | ||
| else if(c.long_double_width == 80) | ||
| { | ||
| result = ieee_float_spect::x86_80().to_type(); | ||
| } | ||
| else if(c.long_double_width == 128) | ||
| { | ||
| // Non-x86 128-bit long double: IEEE 754 binary128 (PowerPC, AArch64 | ||
| // when configured that way, etc.). | ||
| result = ieee_float_spect::quadruple_precision().to_type(); | ||
| } |
Comment on lines
823
to
830
| // Check all value bits except the sign bit are zero. | ||
| // For x86 extended in padded storage, the sign is at value_width()-1 | ||
| // and padding bits above are always zero (so we can just check all | ||
| // bits except the sign position). | ||
| bvt all_but_sign = src; | ||
| const std::size_t sign_pos = spec.value_width() - 1; | ||
| all_but_sign.erase(all_but_sign.begin() + sign_pos); | ||
| return bv_utils.is_zero(all_but_sign); |
Comment on lines
259
to
262
| const mp_integer all_ones = power(2, width) - 1; | ||
| const mp_integer sign_bit_mask = power(2, spec.value_width() - 1); | ||
| const mp_integer v = all_ones - sign_bit_mask; | ||
|
|
Comment on lines
+196
to
+219
| // x86_64 typically stores `long double` as the x87 80-bit extended | ||
| // format in 16 bytes (Linux, macOS, FreeBSD). i386 stores it in 12 | ||
| // bytes. Accurate modelling matters because programs (notably the | ||
| // Apple SDK's <math.h> inline helpers) read the bytes via union-based | ||
| // bit twiddling. | ||
| const auto &c = config.ansi_c; | ||
| if(c.long_double_width == 128 && (c.arch == "x86_64" || c.arch == "i386")) | ||
| { | ||
| // x86 extended precision has 80 bits in total, and | ||
| // deviating from IEEE, does not use a hidden bit. | ||
| // We use the closest we have got, but the below isn't accurate. | ||
| result=ieee_float_spect(63, 15).to_type(); | ||
| result = ieee_float_spect::x86_128().to_type(); | ||
| } | ||
| else if(config.ansi_c.long_double_width==96) | ||
| else if(c.long_double_width == 96 && c.arch == "i386") | ||
| { | ||
| result=ieee_float_spect(80, 15).to_type(); | ||
| // not quite right. The extra bits beyond 80 are usually padded. | ||
| result = ieee_float_spect::x86_96().to_type(); | ||
| } | ||
| else if(c.long_double_width == 80) | ||
| { | ||
| result = ieee_float_spect::x86_80().to_type(); | ||
| } | ||
| else if(c.long_double_width == 128) | ||
| { | ||
| // Non-x86 128-bit long double: IEEE 754 binary128 (PowerPC, AArch64 | ||
| // when configured that way, etc.). | ||
| result = ieee_float_spect::quadruple_precision().to_type(); | ||
| } |
Comment on lines
823
to
830
| // Check all value bits except the sign bit are zero. | ||
| // For x86 extended in padded storage, the sign is at value_width()-1 | ||
| // and padding bits above are always zero (so we can just check all | ||
| // bits except the sign position). | ||
| bvt all_but_sign = src; | ||
| const std::size_t sign_pos = spec.value_width() - 1; | ||
| all_but_sign.erase(all_but_sign.begin() + sign_pos); | ||
| return bv_utils.is_zero(all_but_sign); |
Comment on lines
259
to
262
| const mp_integer all_ones = power(2, width) - 1; | ||
| const mp_integer sign_bit_mask = power(2, spec.value_width() - 1); | ||
| const mp_integer v = all_ones - sign_bit_mask; | ||
|
|
Comment on lines
+196
to
+219
| // x86_64 typically stores `long double` as the x87 80-bit extended | ||
| // format in 16 bytes (Linux, macOS, FreeBSD). i386 stores it in 12 | ||
| // bytes. Accurate modelling matters because programs (notably the | ||
| // Apple SDK's <math.h> inline helpers) read the bytes via union-based | ||
| // bit twiddling. | ||
| const auto &c = config.ansi_c; | ||
| if(c.long_double_width == 128 && (c.arch == "x86_64" || c.arch == "i386")) | ||
| { | ||
| // x86 extended precision has 80 bits in total, and | ||
| // deviating from IEEE, does not use a hidden bit. | ||
| // We use the closest we have got, but the below isn't accurate. | ||
| result=ieee_float_spect(63, 15).to_type(); | ||
| result = ieee_float_spect::x86_128().to_type(); | ||
| } | ||
| else if(config.ansi_c.long_double_width==96) | ||
| else if(c.long_double_width == 96 && c.arch == "i386") | ||
| { | ||
| result=ieee_float_spect(80, 15).to_type(); | ||
| // not quite right. The extra bits beyond 80 are usually padded. | ||
| result = ieee_float_spect::x86_96().to_type(); | ||
| } | ||
| else if(c.long_double_width == 80) | ||
| { | ||
| result = ieee_float_spect::x86_80().to_type(); | ||
| } | ||
| else if(c.long_double_width == 128) | ||
| { | ||
| // Non-x86 128-bit long double: IEEE 754 binary128 (PowerPC, AArch64 | ||
| // when configured that way, etc.). | ||
| result = ieee_float_spect::quadruple_precision().to_type(); | ||
| } |
Comment on lines
+319
to
+323
| // for x86 extended in padded storage the sign bit lives at the top of | ||
| // the encoded value (value_width()-1), not at the top of the storage | ||
| // container. | ||
| const floatbv_typet &type = to_floatbv_type(op.type()); | ||
| const ieee_float_spect spec(type); |
On x86 hardware (i386 and x86_64) the C `long double` type is the
x87 80-bit extended-precision floating-point format, not an IEEE 754
binary type. The 80-bit value is stored in a 12-byte (i386) or
16-byte (x86_64) memory location with the upper bits as padding,
and -- unlike IEEE binary formats -- the leading integer bit of the
significand is stored explicitly in the encoding. See Intel SDM
vol. 1 §4.2.2 for the hardware reference and the new
`doc/architectural/x86-long-double.md` for the modelling notes.
Programs in the wild observe these bytes directly. The most
prominent case is the macOS SDK's `<math.h>` inline classification
helpers (`__inline_signbitl`, `__inline_isnan`, ...): they cast a
`long double` to a struct `{ uint64_t mantissa; uint16_t sexp; }`
and shift the sign out of `sexp`. CBMC previously modelled
`long double` on x86_64 as IEEE binary128, which placed the sign at
bit 127 instead of bit 79; in that model `sexp` (bytes 8-9) is
always zero and `signbit` evaluates to 0 for negative values.
This commit teaches `ieee_float_spect` to carry an optional
`storage_width_bits` separately from the value width, and adds
`x86_128()` and `x86_96()` factory methods. `long_double_type()`
selects `x86_128`/`x86_96` for x86_64/i386 and keeps IEEE
binary128 for non-x86 targets that use it (e.g. ppc64le). The
exponent-width helper `floatbv_typet::get_e()` is updated to
respect the `ID_x86_extended` flag and return 15 for x86 extended
types -- without this fix the SMT2 back-ends would compute an
exponent width of 64 (= storage_width - f - 1) and emit invalid
SMT-LIB FP sorts whenever the program references `long double`,
even via the unused `__CPROVER_*ld` prelude declarations.
`ieee_float_valuet::pack` / `unpack` produce and consume the
correct x86 byte layout: sign at bit 79, biased 15-bit exponent at
bits 64-78, explicit integer bit at bit 63, fraction at bits 0-62,
and zero padding above bit 79. The expression-level encoder
(`float_bvt` in `src/solvers/floatbv/float_bv.cpp`) and the
SAT-level encoder (`float_utilst` in
`src/solvers/floatbv/float_utils.cpp`) lower floats to bit-vectors
under the same layout, including for `abs`, `negation`,
`is_zero`, `get_exponent`, `unpack` (read the explicit integer
bit rather than synthesising it), and `pack` (zero-pad above the
80-bit value). `boolbvt::convert_rest` reads the sign of a
`floatbv` operand from `value_width()-1` rather than the top of
the storage container. `float_utilst::sign_bit` becomes a
non-static member because it now needs the spec; the integer-input
`from_signed_integer` path uses `src.back()` directly because
its argument is an integer, not a float. `float_bvt::sign_bit`
is kept polymorphic for non-floatbv operands so that callers like
`from_signed_integer` (which pass a signedbv) continue to work.
The classification helpers `is_NaN`, `is_infinity`, `is_normal`
(and the corresponding `isnan` / `isinf` / `isnormal` in
`float_bvt`) additionally require the explicit integer bit to be
1 for x86 80-bit extended. This is consistent with modern x86
hardware, which treats the so-called "pseudo" encodings
(pseudo-NaN, pseudo-Infinity, pseudo-denormal-with-non-zero
exponent) as invalid and raises FE_INVALID rather than
classifying them as a normal value of the corresponding category.
With the same change `is_plus_inf` / `is_minus_inf` are
simplified to reuse `is_infinity`, and `exponent_all_ones` /
`exponent_all_zeros` are simplified to reuse `get_exponent`,
keeping the offset arithmetic in a single place.
`is_zero` (in both `float_utilst` and `float_bvt`) drops the
storage padding before testing the value bits; without this,
symbolic inputs with unconstrained padding bits could spuriously
fail an is_zero query because the solver could pick non-zero
padding even when the encoded value is zero.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
x86-long-double-extended
branch
from
48deaed to
67ee35e
Compare
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## develop #9023 +/- ##
=========================================
Coverage 80.59% 80.60%
=========================================
Files 1711 1711
Lines 189454 189630 +176
Branches 73 73
=========================================
+ Hits 152697 152846 +149
- Misses 36757 36784 +27 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
Adds regression tests that pin down the byte layout, the FP arithmetic, and the key behaviours that motivated the fix. Pure FP arithmetic, runs under all four back-ends: - regression/cbmc/long-double-arithmetic-x86 exercises long-double addition, multiplication, division, sign behaviour, mantissa precision (>= 64 bits, well above double's 53), and large-range reciprocals. Passes under SAT, --z3, --cprover-smt2 and --incremental-smt2-solver. Byte-layout tests, restricted to back-ends that fully support the FP<->bv boundary (SAT and --z3): - regression/cbmc/long-double-x86-bytes covers the 16-byte little-endian byte layout for representative values (1.0L, -1.0L, 2.0L, 0.5L, 0.0L) against ground-truth byte sequences captured on real macOS-15 x86_64 hardware (Apple clang 17.0.0). - regression/cbmc/long-double-i386-bytes covers the analogous 12-byte storage container on i386. The test is hermetic (no system headers) so it works on hosts without i386 multilib development packages installed. - regression/cbmc/long-double-signbit-x86 replicates the union-based signbit helper that the macOS SDK's <math.h> uses, which is the failure that originally triggered the investigation. - regression/cbmc/long-double-roundtrip-x86 exercises double <-> long double conversion both at compile time (constant samples) and symbolically (a nondet finite double). - regression/cbmc/long-double-pseudo-encodings constructs the x86 pseudo-NaN, pseudo-Infinity and pseudo-denormal encodings via union and confirms that __CPROVER_isnanld / __CPROVER_isinfld / __CPROVER_isnormalld reject them (matching modern Intel/AMD hardware which raises FE_INVALID for these patterns). The test deliberately avoids <math.h> because mingw's <math.h> contains constructs the CBMC C front-end cannot parse. Adds two unit tests in unit/util/ieee_float.cpp: - ieee_float_spect: x86 extended specs verifies the new x86_80(), x86_96() and x86_128() factories produce the expected value_width / width / bias. - ieee_float_valuet: pack/unpack on x86 80-bit extended rounds-trips integer values through pack/unpack and matches the same hardware byte sequences used by the regression tests. The byte-layout tests are tagged broken-cprover-smt-backend and no-new-smt because those back-ends have pre-existing limitations on FP<->bv conversion patterns (flatten2bv invariant, missing concatenation lowering); these limitations also affect existing Float-* tests in the same way. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The CBMC models for expl, exp2l, logl, log2l, log10l and __builtin_powil in src/ansi-c/library/math.c implement their long-double-only fast paths via Schraudolph-style bit-pattern manipulation that targets IEEE 754 binary128 layout (it places or reads an int32 in the upper 32 bits of the storage of `long double`). On x86 80-bit extended (the real layout of `long double` on x86_64 Linux/macOS/FreeBSD and on i386 -- as corrected in the preceding commit) those upper bits are storage padding and the trick targets the wrong bits. The models therefore produce wrong values under the new, hardware-faithful layout; this was silently masked by CBMC's previous incorrect binary128 model. Mark these six tests KNOWNBUG with explanatory test.desc comments so they remain visible (and verifiable at level KNOWNBUG) without blocking CORE CI. The corresponding double and float models (exp, exp2, log, log2, log10, __builtin_powi, __builtin_powif) are unaffected and continue to pass. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Document the hardware reference (Intel SDM vol. 1 §4.2.2, IA-32 ABI), the byte-level layout, and how the CBMC `ieee_float_spect` machinery, the constant pack/unpack path, the expression-level `float_bvt` encoder, the SAT-level `float_utilst` encoder and the boolbv ID_sign handler all participate in the encoding. Includes a worked example of the byte sequence for 1.0L on real hardware and an explanation of why the previous binary128 model was unsafe for code that observes `long double` bytes (notably the macOS SDK's classification helpers). Cross-references the regression tests added alongside the fix. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
x86-long-double-extended
branch
from
67ee35e to
0425f0f
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Summary
CBMC currently models
long doubleon x86_64 as IEEE 754 binary128 (quadruple precision). On real x86_64 hardware (Linux, macOS, FreeBSD)long doubleis the x87 80-bit extended-precision format, stored in 16 bytes of memory with the upper 48 bits as padding. The two formats agree on the value of representable numbers but disagree on every individual bit position.This PR teaches CBMC the actual byte layout used by hardware so that programs that observe
long doublebytes -- most prominently the macOS SDK's<math.h>inline classification helpers -- get correct results.Motivation
The macOS SDK ships an inline
signbithelper forlong doubleof the form (Xcode 16,<math.h>):__sexplives in bytes 8-9 of the storage and is expected to contain the 16-bitsign|exponentwindow of the x86 80-bit extended encoding. With the previous binary128 model those bytes were always zero, sosignbit(-1.0L)evaluated to0for any negative value and any branch guarded by the SDK's classification helpers took the wrong path. This manifested as a regression on macOS x86_64 in the CBMC test suite that callssignbitonlong double.Hardware reference
Captured on real macOS-15 x86_64 (Xcode 16.4, Apple clang 17.0.0):
1.0L00 00 00 00 00 00 00 80 ff 3f 00 00 00 00 00 00-1.0L00 00 00 00 00 00 00 80 ff bf 00 00 00 00 00 002.0L00 00 00 00 00 00 00 80 00 40 00 00 00 00 00 000.5L00 00 00 00 00 00 00 80 fe 3f 00 00 00 00 00 000.0L00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00Byte layout:
Sources: Intel® 64 and IA-32 Architectures Software Developer's Manual, vol. 1, §4.2.2; System V AMD64 ABI; System V i386 ABI.
Changes
The PR is structured as four reviewable commits:
ieee_float, solvers: model x86 80-bit extended long double preciselyThe substantive fix. Touches the type-system spec (ieee_float_spect), the constantpack/unpackpath (ieee_float_valuet), the expression-level encoder (float_bvt), the SAT-level encoder (float_utilst), and the boolbv handler forID_sign. Each layer agrees on the same byte layout. See the commit message for the per-function summary.Tests: x86 80-bit extended long double layout and round-tripsAdds four regression tests pinning the byte layout against the hardware reference (long-double-x86-bytes,long-double-i386-bytes), the union-based signbit pattern from the macOS SDK (long-double-signbit-x86), and round-trip casts betweendoubleandlong double(long-double-roundtrip-x86). Adds two unit tests coveringieee_float_spect::x86_*()factories and the constantpack/unpackround-trip.cbmc-library: mark long-double Schraudolph-style models KNOWNBUGSix existing library models (expl,exp2l,logl,log2l,log10l,__builtin_powil) implement their long-double-only fast paths via Schraudolph-style bit-pattern manipulation that targets IEEE 754 binary128 layout. Under the corrected x86-extended layout the trick targets storage padding and the models produce wrong values. This was silently masked by CBMC's previous incorrect model. These six tests are downgraded toKNOWNBUGwith explanatorytest.desccomments; the correspondingdoubleandfloatmodels are unaffected and continue to pass. Fixing these models is follow-up work.doc: architectural notes on x86 80-bit extended long doubleNewdoc/architectural/x86-long-double.mddocumenting the hardware reference, the byte layout, and how each CBMC code layer participates.Verification
Hardware byte sequences vs CBMC output
The new
long-double-x86-bytesregression test asserts on the exact byte sequences captured above and passes:Documentation
doc/architectural/x86-long-double.md(new) -- modelling notes, byte-layout table, per-layer code paths, links to the regression and unit tests.src/util/ieee_float.h-- inline doxygen comments on the newstorage_width_bitsfield, thevalue_width()/width()accessors, and thex86_80()/x86_96()/x86_128()factories.Backend and platform coverage
--cprover-smt2,--incremental-smt2-solver): the new tests are taggedbroken-cprover-smt-backendandno-new-smt. The SMT2 back-ends still encodelong doubleas binary128; that's tracked separately.x86_64Linux/macOS/FreeBSD: x86 80-bit extended in 16 bytes (this PR).i386Linux: x86 80-bit extended in 12 bytes (this PR).arm64/aarch64macOS, Windows MSVC:long double == double(unchanged).ppc64le,aarch64Linux with binary128: IEEE binary128 (unchanged).Follow-up
KNOWNBUGin commit 3. The Schraudolph-style approximations need to be adapted for the x86-extended layout (or replaced with a portable fallback).