Skip to content

fix(extF80): correct add/sub for valid inputs with J-bit clear#38

Closed
johnwbyrd wants to merge 1 commit into
ucb-bar:masterfrom
johnwbyrd:fix/extf80-add-sub
Closed

fix(extF80): correct add/sub for valid inputs with J-bit clear#38
johnwbyrd wants to merge 1 commit into
ucb-bar:masterfrom
johnwbyrd:fix/extf80-add-sub

Conversation

@johnwbyrd
Copy link
Copy Markdown

Summary

The extFloat80 format stores the integer bit (J, bit 63 of the significand) explicitly. Every combination of exponent and significand is a valid encoding with a defined mathematical value. The original Intel 8087 hardware defined and correctly processed all such encodings — unnormals, pseudo-denormals, pseudo-infinities, and pseudo-NaNs — as described in Intel's US Patent 4,325,120 and in every subsequent Intel architecture manual covering the x87 FPU.

extF80_add and extF80_sub produce wrong results for valid inputs where J disagrees with what the biased exponent implies. The other arithmetic functions (extF80_mul, extF80_div) already contain normalization guards that handle these inputs correctly; add and sub are missing the same guard.

Wrong results demonstrated

Expression SoftFloat returns Correct result
{exp=0x3FFF, sig=0} + itself {0x4000, 0x0} (= 2.0) {0x0000, 0x0} (= 0, since sig=0)
{exp=0x3FFF, sig=0x4000..0} + itself {0x4001, 0x4000..0} (= 3.0) {0x3FFF, 0x8000..0} (= 1.0, since the input is 0.5)
{exp=0x7FFE, sig=0x7FFF..F} + 0 {0x7FFF, 0x8000..0} (+Inf) finite (large but not infinite)
{exp=0, sig=0x8000..0} + itself {0x0000, 0x0} (= 0) {0x0002, 0x8000..0} (= 2^(-16381), since the input is the pseudo-denormal 2^(-16382))

A standalone program demonstrating all of these: https://gist.github.com/johnwbyrd/cb75a1844661677fe614bc39f171fe39

Root causes and fixes

s_addMagsExtF80.c:

  1. Missing normalization guard. extF80_mul and extF80_div normalize inputs whose J-bit is clear before performing arithmetic. s_addMagsExtF80 does not, so it interprets the raw significand bits at the wrong magnitude. The fix adds the same guard after field extraction, with additional logic for the subnormal boundary (exp=0 and exp=1 share the same emin, so normalizing an unnormal with exp=1 must not over-shift into the normal range).

  2. Carry overflow in equal-exponent subnormal addition. When both operands are pseudo-denormals with J=1 (e.g., {exp=0, sig=0x8000000000000000}), sigA + sigB overflows 64 bits and wraps to zero. The fix detects the carry (sigZ < sigA) and routes to the existing shiftRight1 path, which recovers the carry as the new J-bit.

  3. Carry overflow at newlyAligned. The same 64-bit overflow can occur after alignment when both significands have J=1 at the same effective exponent. The fix adds the same carry check.

  4. Pseudo-infinity passthrough. Three infinity-detection paths return uiA0 or uiB0 as the result significand, passing through whatever bit pattern was in the input. When the input is a pseudo-infinity ({exp=0x7FFF, sig=0}), the output is a non-canonical infinity encoding. The fix always returns the canonical infinity significand 0x8000000000000000.

s_subMagsExtF80.c:

  1. Same normalization guard as addMags.

  2. Magnitude reversal at newlyAligned{A,B}Bigger. When expDiff=1 and the smaller-exponent operand is subnormal (exp=0), the code adjusts expDiff to 0 and jumps to the newlyAligned label, which assumes the operand with the larger exponent has the larger value. After normalization of unnormal inputs, this assumption can be false. The fix re-checks significand magnitudes at both newlyAligned labels.

  3. Same pseudo-infinity passthrough fix (one location).

Related

Suggested test plan

  • Build SoftFloat with this patch, rebuild TestFloat with extF80 test generator: cover all valid J-bit encodings berkeley-testfloat-3#21, and run testsoftfloat -level 1 extF80_add and testsoftfloat -level 1 extF80_sub — both should pass across all precisions and rounding modes
  • Run testsoftfloat -level 1 extF80_div as a regression check (div already handles these inputs correctly and should remain clean)
  • Run testsoftfloat -level 1 f64_add and f32_mul to confirm non-extF80 operations are unaffected

The extFloat80 format stores the integer bit (J, bit 63) explicitly,
so every combination of exponent and significand has a defined
mathematical value.  When J disagrees with what the biased exponent
implies, the existing add/sub code produces wrong results.

Root causes and fixes in s_addMagsExtF80.c:

1. Missing normalization guard: extF80_mul and extF80_div already
   normalize inputs whose J-bit is clear before arithmetic, but
   s_addMagsExtF80 does not.  Add the same guard after field
   extraction.  The guard handles the subnormal boundary (exp=0 and
   exp=1 share the same emin) by limiting the left-shift so the
   result doesn't cross into the normal range.

2. Carry overflow in equal-exponent subnormal addition: when both
   operands are pseudo-denormals with J=1 (e.g., {exp=0, sig=0x8000...}),
   sigA + sigB overflows 64 bits.  Detect the carry (sigZ < sigA)
   and route to shiftRight1, which recovers the carry as the new
   J-bit.

3. Carry overflow at newlyAligned: the same 64-bit overflow can occur
   after alignment when both significands have J=1.  Add the same
   carry check.

4. Pseudo-infinity passthrough: three infinity-detection paths return
   uiA0 or uiB0 as the significand, passing through non-canonical
   encodings.  Always return the canonical infinity significand
   0x8000000000000000.

Corresponding fixes in s_subMagsExtF80.c:

1. Same normalization guard as addMags.

2. Magnitude reversal at newlyAligned{A,B}Bigger: when expDiff=1 and
   the smaller-exponent operand is subnormal (exp=0), the code adjusts
   expDiff to 0 and jumps to newlyAligned, which assumes the operand
   with the larger exponent has the larger value.  After normalization,
   this assumption can be wrong.  Re-check significand magnitudes.

3. Same pseudo-infinity passthrough fix (one location).

Demonstrated wrong results before this fix:

  {exp=0x3FFF, sig=0} + itself = {0x4000, 0x0} (= 2.0)
    Expected: 0  (sig=0 means the value is zero)

  {exp=0x3FFF, sig=0x4000..0} + itself = {0x4001, 0x4000..0} (= 3.0)
    Expected: 1.0  (the input value is 0.5)

  {exp=0x7FFE, sig=0x7FFF..F} + 0 = {0x7FFF, 0x8000..0} (= +Inf)
    Expected: finite  (large but not infinite)

  {exp=0, sig=0x8000..0} + itself = {0, 0} (= 0)
    Expected: 2^(-16381)  (the input is 2^(-16382))
@johnwbyrd
Copy link
Copy Markdown
Author

Closing this PR. The fix here is superseded by a later, more comprehensive PR that addresses non-canonical extFloat80 encodings across all extF80 operations.

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