diff --git a/AstSemantics.md b/AstSemantics.md index f1031a83..0d230bec 100644 --- a/AstSemantics.md +++ b/AstSemantics.md @@ -426,9 +426,8 @@ The same operators are available on 64-bit integers as the those available for ## Floating point operators Floating point arithmetic follows the IEEE 754-2008 standard, except that: - - The sign bit and fraction field of any NaN value returned from a floating - point arithmetic operator are deterministic under more circumstances than - required by IEEE 754-2008. + - The IEEE 754-2008 section 6.2 recommendation that operations propagate NaN + bits from their operands is permitted but not required. - WebAssembly uses "non-stop" mode, and floating point exceptions are not otherwise observable. In particular, neither alternate floating point exception handling attributes nor the non-computational operators on status @@ -452,15 +451,14 @@ When the result of any arithmetic operation other than `neg`, `abs`, or the implicit leading digit of the significand) of the NaN are computed as follows: - - If the operation has exactly one NaN operand, the result NaN has the same - bits as that operand, except that the most significant bit of the - fraction field is 1. - - If the operation has multiple NaN input values, the result value is computed - as if one of the operands, selected nondeterministically, is the only NaN - operand (as described in the previous rule). - - If the operation has no NaN input values, the result value has a - nondeterministic sign bit, a fraction field with 1 in the most significant - bit and 0 in the remaining bits. + - If the operation has any NaN input values, implementations may select any of + them to be the result value, but with the most significant bit of the + fraction field overwritten to be 1. + + - If the implementation does not choose to use an input NaN as a result value, + or if there are no input NaNs, the result value has a nondeterministic sign + bit, a fraction field with 1 in the most significant bit and 0 in the + remaining bits. 32-bit floating point operations are as follows: @@ -546,15 +544,22 @@ Promotion and demotion of floating point values always succeed. Demotion of floating point values uses round-to-nearest ties-to-even rounding, and may overflow to infinity or negative infinity as specified by IEEE 754-2008. -If the operand of promotion is a NaN, the result is a NaN with the sign bit -of the operand and a fraction field consisting of 1 in the most significant bit, -followed by all but the most significant bits of the fraction field of the -operand, followed by all 0s. - -If the operand of demotion is a NaN, the result is a NaN with the sign bit -of the operand and a fraction field consisting of 1 in the most significant bit, -followed by as many of all but the most significant bit of the fraction field of -the operand as fit. +If the operand of promotion is a NaN, the result is nondeterministically chosen +between the following: + - a NaN with a nondeterministic sign bit and a fraction field with 1 in the + most significant bit and 0 in the remaining bits. + - a NaN with the sign bit of the operand and a fraction field consisting of + 1 in the most significant bit, followed by all but the most significant + bit of the fraction field of the operand, followed by all 0s. + +If the operand of demotion is a NaN, the result is nondeterministically chosen +between the following: + - a NaN with a nondeterministic sign bit and a fraction field with 1 in the + most significant bit and 0 in the remaining bits. + - a NaN with the sign bit of the operand and a fraction field consisting of + 1 in the most significant bit, followed by all but the most significant bit + of the fraction field of the operand, discarding the least significant bits + that don't fit. Reinterpretations always succeed. diff --git a/Nondeterminism.md b/Nondeterminism.md index 6a90e927..db738c97 100644 --- a/Nondeterminism.md +++ b/Nondeterminism.md @@ -30,11 +30,12 @@ currently admits nondeterminism: shared memory, nondeterminism will be visible through the global sequence of API calls. With shared memory, the result of load operators is nondeterministic. - * Except when otherwise specified, when an arithmetic operator with multiple - floating point operand types and a floating point result type receives - multiple NaN input values with differing bit patterns, it is nondeterministic - which bit pattern is used as the basis for the result (as it is in - IEEE 754-2008). + * Except when otherwise specified, when an arithmetic operator returns NaN, + there is nondeterminism in determining the specific bits of the NaN. However, + wasm does still provide the guarantee that NaN values returned from an operation + will not have 1 bits in their fraction field that aren't set in any NaN values + in the input operands, except for the most significant bit of the fraction field + (which most operators set to 1). * Except when otherwise specified, when an arithmetic operator with a floating point result type receives no NaN input values and produces a NaN result value, the sign bit of the NaN result value is nondeterministic. diff --git a/Rationale.md b/Rationale.md index c225d3a3..d4c17b55 100644 --- a/Rationale.md +++ b/Rationale.md @@ -323,11 +323,12 @@ architectures there may be a need to revisit some of the decisions: ## NaN bit pattern propagation -In general, WebAssembly's floating point operations propagate NaN bit patterns. -When an operation has a NaN operand, it returns a NaN result with the same bit -pattern. This is done in accordance with IEEE 754-2008, and it also has the -desirable property of making it easier to port interpreters to WebAssembly that -use NaN-boxing, because they can rely on the property that if an arithmetic +In general, WebAssembly's floating point operations provide the guarantee that +a NaN returned from an operation won't have new bits set in its fractional +field, except the most significant bit. + +This is intended to support interpreters running on WebAssembly that use +NaN-boxing, because they can rely on the property that if an arithmetic operation has no non-canonical NaNs as input, its output is also canonical. The specific bit-pattern rules are modeled after what numerous popular