diff --git a/MATH.md b/MATH.md new file mode 100644 index 0000000..bca620b --- /dev/null +++ b/MATH.md @@ -0,0 +1,344 @@ +# Mathematical specification of Fpy + +## Scope + +This document defines the semantics of all mathematical actions and builtin functions in Fpy, including: +* Arithmetic +* Truncation, extension +* Casting +* Overflow, underflow +* NaN propagation +* Mathematical library functions + + +## Numerical types + +`U8`, `U16`, `U32`, and `U64` are the primitive unsigned integer types with bitwidths 8, 16, 32 and 64, respectively. They use the standard binary representation of unsigned integers. + +`I8`, `I16`, `I32`, and `I64` are the primitive signed integer types with bitwidths 8, 16, 32 and 64, respectively. They use the standard two's complement representation of signed integers. + +`F32`, and `F64` are the primitive IEEE floating-point types with bitwidths 32 and 64, respectively. + +## Call expressions + +callable_expr(argument_list) + +## Cast expression + +A cast expression is a call expression whose callable expression is an identifier naming a cast function definition. + +Each concrete numeric type with name `T` has an associated cast function definition with the same name. + +A cast function has one formal parameter of `Number` type, and returns a value of type `T`. + +Casts cannot end the program, and have no undefined behavior. + +* Casting from an integer to an integer wraps. + * Casting between integers of different signedness just reinterprets the binary representation + * `U8(255) == U8(-128)` +* Casting from an integer to a float rounds, with ties rounded to even. + * `0` is rounded to `+0` +* Casting from a float to a float rounds, with ties rounded to even. + * Positive or negative infinity and `NaN` round to themselves + * If the value exceeds the IEEE +1. `round_T(NaN) = NaN` +2. `round_T(+∞) = +∞`, `round_T(−∞) = −∞` +3. `round_T(0) = +0` +4. For nonzero real `r`: the value of `⟦T⟧` nearest to `r`, ties to the one + with even least significant mantissa digit. If `|r|` exceeds the IEEE + overflow threshold for `T`, the result is `+∞` or `−∞` with the sign of + `r` (**not** the largest finite value). If `r` rounds to zero, the result + is `+0` or `−0` with the sign of `r`. + +A cast of value `x` from type `S` to type `T` behaves as follows: + +| `S` | `T` | `cast_{S→T}(x)` | +|---|---|---| +| integer | integer | `wrap_T(x)` | +| integer | float | `round_T(x)` | +| float | float | `±0_T` if `x = ±0_S` (same sign); else `round_T(⟦x⟧)` | +| float | integer | `clamp_T(trunc(⟦x⟧))` | + +If T is a float type, then R is the nearest representable + +WIP +Integer to float and float to float rounds to nearest float (overflow just rounds to highest representable float?) +Float to integer overflow saturates the integer +Integer to integer overflow wraps +The reason arithmetic overflow ends the program but cast overflow does not is because casts are explicit, so the programmer is more aware that they are doing an operation which may involve truncation. If they want to handle an overflow differently than casting does, they can just check for overflow before the cast. + +An intermediate type is picked which is 64 bits. Both operands are coerced to the intermediate type. The result type of the operation, before coercion or casting, is also the intermediate type. + +Arithmetic on F64 +These operations on F64s are fully defined in all cases by IEEE 754 and produce the expected result. These operations never end the program at runtime. + +Arithmetic on I64, U64 +If the operation is division and the denominator is zero, the program ends with an error. + +See https://github.com/rust-lang/rfcs/blob/master/text/0560-integer-overflow.md + +Otherwise, let R be the mathematical result of the operation given the two operands. + +If R is not representable in the result type, the program ends with an error. This is called an underflow or overflow. + + +### `ln` +#### Signature + +`ln(operand: F64) -> F64` + +#### Semantics + +At evaluation: +1. If `operand` is outside the domain of the natural logarithm function, halt the program and display an error code. +2. The expression evaluates to the natural logarithm of `operand`. + +### `iabs` +#### Signature +`iabs(value: I64) -> I64` + +#### Semantics +At evaluation, the function call evaluates to the absolute value of `value`. + +TODO specify what happens if the abs value is outside of i64 + +### `fabs` +#### Signature +`fabs(value: F64) -> F64` + +#### Semantics +At evaluation, the function call evaluates to the absolute value of `value`. +TODO specify what happens if the abs value is outside of i64 + + + +## Type conversion + +TODO Type conversion is the process of converting an expression from one type to another. It can either be implicit, in which case it is called coercion, or explicit, in which case it is called casting. + +### Intermediate types + +The **intermediate type** of a binary or unary operator expression is the type to which all argument expressions will be coerced to. + +Intermediate types are picked via the following rules: + +1. The intermediate type of Boolean operators is always `bool`. +2. The intermediate type of `==` and `!=` may be any type, so long as the left and right hand sides are the same type. If both are numeric then continue. +3. If either argument is non-numeric, raise an error. +4. If the operator is unary `-` and the argument is an unsigned integer, raise an error: negation is undefined for unsigned types (the result would be negative for every nonzero operand). +5. If the operator is `/` or `**`, the intermediate type is always `F64`. +6. If either argument is a float, the intermediate type is `F64`. +7. If either argument is an unsigned integer, the intermediate type is `U64`. +8. Otherwise, the intermediate type is `I64`. + +If the expressions given to the operator are not of the intermediate type, type coercion rules are applied. + +## Result type + +The result type is the type of the value produced by the operator. +1. For numeric operators, the result type is the intermediate type. +2. For boolean and comparison operators, the result type is `bool`. + +Normal type coercion rules apply to the result, of course. Once the operator has produced a value, it may be coerced into some other type depending on context. + + +## Binary operator expressions + +A **binary operator expression** is an expression with a left and right-hand expression, and a binary operator in between, which acts on both values to produce a new value. + +The list of **binary operators** is: +* The [addition operator](#subtraction-semantics) `+` +* The [subtraction operator](#multiplication-semantics) `-` +* The [multiplication operator](#multiplication-semantics) `*` +* The [division operator](#division-semantics) `/` +* The [floor division operator](#floor-division-semantics) `//` +* The [modulus operator](#modulus-semantics) `%` +* The [exponentiation operator](#exponentiation-semantics) `**` +* The [Boolean operators](#boolean-operator-semantics) `and` and `or` +* The [comparison operators](#comparison-semantics) `>`, `>=`, `<`, and `<=` +* The [equality operator](#equality-semantics) `==` +* The [inequality operator](#inequality-semantics) `!=` +* The [range operator](#range-semantics) `..` + +### Syntax + +Rule: + +`binary_op: expr BINARY_OP expr` + +Name: + +`binary_op: lhs op rhs` + +`lhs` and `rhs` are resolved in the value name group. + +### Semantics + +For each use of a binary operator, an [intermediate type](#intermediate-types) is picked, as described in the operator's semantics. + +If `lhs` or `rhs` cannot be [coerced](#type-coercion) into the intermediate type, an error is raised. + +If `lhs` and `rhs` are constant expressions, the binary operator expression is a constant expression. + +At evaluation, for all operators besides the [Boolean operators](#boolean-operator-semantics): +1. `lhs` is evaluated and coerced into the intermediate type. +2. `rhs` is evaluated and coerced into the intermediate type. +3. The expression evaluates to a value of the intermediate type, as described in the operator's semantics. + +#### Addition semantics +The addition operator is `+`. + +If neither `lhs` nor `rhs` are expressions of a [numeric type](#types), an error is raised. + +The expression evaluates to the result of adding + +#### Subtraction semantics +#### Multiplication semantics + +These operators require numeric operands and produce a result in the chosen intermediate type. Addition, subtraction, and multiplication differ only in which arithmetic operation they perform. Integer overflow wraps according to the destination type when the result is ultimately stored, and floating-point operations follow IEEE-754 behavior. + +#### Division semantics +Both operands are promoted to `F64`, and the result is always an `F64`. This means you must explicitly cast the result to store it in an integer type. + +#### Floor division semantics +`//` floors its quotient toward negative infinity, for both integer and float operands. + +With integer operands it uses the signed or unsigned divide directive. Unsigned operands are non-negative, so the truncated quotient is already the floored one. Signed division truncates toward zero, which differs from flooring exactly when the operands have opposite signs and the division is inexact; there the quotient is one greater than the floor, and is decremented. + +With float operands the quotient is computed in `F64` and then floored: +* An infinite or NaN quotient is unchanged. +* A zero quotient is unchanged; the sign of zero is preserved, so a quotient of `-0.0` floors to `-0.0`. +* Otherwise the result is the largest integral `F64` value not greater than the quotient: a quotient of `0.5` floors to `0.0`, and a quotient of `-0.5` floors to `-1.0`. + +An integer zero divisor raises a runtime error (`DOMAIN_ERROR`). A float zero divisor does not: float division is IEEE, so the quotient is an infinity or a NaN and the floor passes it through. `(-2**63) // -1` raises `ARITHMETIC_OVERFLOW`: the mathematical quotient `2**63` is not representable in `I64`. + +### Modulus semantics +Modulus works for numeric operands. Signed operands use the signed modulo directive, unsigned operands use the unsigned directive, and floats use floating-point modulo. + +Signed integer and float modulus are *floored*, like `//` and like Python: a nonzero remainder has the same sign as the divisor. The directives compute a *truncated* remainder (the sign of the dividend), so the divisor is added back exactly once when the remainder is nonzero and its sign differs from the divisor's. For floats, an exact-multiple result is a zero carrying the divisor's sign. Unsigned operands are non-negative, so floored and truncated already agree. + +An integer zero divisor raises a runtime error (`DOMAIN_ERROR`). A float zero divisor does not: `x % 0.0` is NaN, as are `inf % y` and any modulus with a NaN operand. Float modulus never raises. `(-2**63) % -1` raises `ARITHMETIC_OVERFLOW`, halting on exactly the same operands as `(-2**63) // -1`, even though the mathematical remainder `0` is representable. + +#### Exponentiation semantics +Both operands are coerced to `F64`, the exponentiation happens in floating point, and the result type is `F64`. + +#### Boolean operator semantics +Operands must be `bool`. `not` negates a single operand. `and` evaluates the left operand first and only evaluates the right operand when the left operand is `True`. Conversely, `or` skips the right operand when the left operand is `True`. The result of every boolean operator is `bool`. + +#### Comparison semantics +Inequalities require numeric operands. Each operand is coerced to the intermediate type, the comparison runs in that type, and the result is `bool`. + +#### Equality semantics +If both operands are numeric, equality uses the same intermediate-type rules as arithmetic operators. Otherwise both operands must have the exact same concrete type (struct, array, enum, or `Fw.Time`). The compiler compares their serialized bytes. Strings cannot be compared. + +## Unary operators +### Syntax + +Rule: + +`unary_op: expr OP` + +Name: + +`unary_op: val op` + +### Negation operator semantics +### Identity operator semantics + +## Intermediate types + +The **intermediate type** of an operator expression is the type to which the operator's sub-expressions are [coerced](#type-coercion) to. + +If any sub-expression + +### Numeric intermediate types + +The numeric type hierarchy is as follows: +* + + + + # we split this algo up into two stages: picking the type category (float, uint or int), and picking the type bitwidth + + # pick the type category: + type_category = None + if op == BinaryStackOp.DIVIDE or op == BinaryStackOp.EXPONENT: + # always do true division and exponentiation over floats, python style + # this is because, for the given op, even with integer inputs, we might get + # float outputs + type_category = "float" + elif any(issubclass(t, FloatValue) for t in arg_types): + # otherwise if any args are floats, use float + type_category = "float" + elif any(t in UNSIGNED_INTEGER_TYPES for t in arg_types): + # otherwise if any args are unsigned, use unsigned + type_category = "uint" + else: + # otherwise use signed int + type_category = "int" + + # pick the bitwidth + # we only use the arb precision types for constants, so if theyre all arb precision, they're consts + constants = all(t in ARBITRARY_PRECISION_TYPES for t in arg_types) + + if constants: + # we can constant fold this, so use infinite bitwidth + if type_category == "float": + return FpyFloatValue + assert type_category == "int" or type_category == "uint" + return FpyIntegerValue + + # can't const fold + if type_category == "float": + return F64Value + if type_category == "uint": + return U64Value + assert type_category == "int" + return I64Value + + +## Type conversion + +**Type conversion** is the process by which values of one type are converted into values of another type. + +There are two kinds of type conversion: +* [Casting](#casting) +* [Coercion](#type-coercion) + +Type casting is merely an explicit flag for type coercion to take place + + +### Type coercion +**Type coercion** is type conversion that happens implicitly to an expression when required by that expression's semantic context. + + +Coercion happens when an expression of type *A* is used in a syntactic element which requires an expression of type *B*. For example, functions, operators and variable assignments all require specific input types, so type coercion happens in each of these. +In general, the rule of thumb is that coercion is allowed if the destination type can represent all possible values of the source type, with some exceptions. The following rules determine when type coercion can be performed: + +1. If the source and destination types are identical, no coercion is performed. +2. *LiteralString* values may be coerced into any FPP string type. No other string expression can be coerced. +3. Otherwise both source and destination must be numeric (`NumericalValue`). Numeric coercions obey these constraints: + * Floats never coerce to integers. + * Integers may always coerce to floats. + * Float-to-float coercions require a destination bit width greater than or equal to the source width. + * Integer-to-integer coercions require matching signedness and a destination bit width greater than or equal to the source width. + * Arbitrary-precision types (`Int`/`Float`) may coerce to any finite-width numeric type. +If no rule matches, the compiler raises an error. + +Compile-time constant floats (including literals and constant-folded expressions) can only be narrowed into a smaller floating-point type when the value lies inside the destination’s representable range. When the value fits, the compiler rounds it to the nearest representable floating-point number; otherwise compilation fails with an out-of-range error. + + +#### Order of operations +The order in which operations take precedence, from most strongly binding to least strongly binding, is: +1. [Exponentiation](#exponentiation-semantics) +2. [Negation](#negation-operator-semantics) and [identity](#identity-operator-semantics) +3. [Multiplication](#multiplication-semantics), [division](#division-semantics), [floor division](#floor-division-semantics), and [modulus](#modulus-semantics) +4. [Addition](#addition-semantics) and [subtraction](#subtraction-semantics) +5. [Range](#range-semantics) +6. [Comparison](#comparison-semantics) +7. [Not](#boolean-operator-semantics) +8. [And](#boolean-operator-semantics) +9. [Or](#boolean-operator-semantics) + +If two operators have the same precedence in the above list, then the leftmost operator binds more strongly. + diff --git a/MATH_CASTS_DRAFT.md b/MATH_CASTS_DRAFT.md new file mode 100644 index 0000000..406d756 --- /dev/null +++ b/MATH_CASTS_DRAFT.md @@ -0,0 +1,135 @@ +# Casts — draft normative section for MATH.md + +> Draft to be merged into MATH.md. + +## Value sets + +For each numeric type `T`, the **value set** `⟦T⟧` is the set of values an +expression of type `T` may evaluate to. + +For `n ∈ {8, 16, 32, 64}`: + +* `⟦Un⟧ = { z ∈ ℤ | 0 ≤ z ≤ 2ⁿ − 1 }` +* `⟦In⟧ = { z ∈ ℤ | −2ⁿ⁻¹ ≤ z ≤ 2ⁿ⁻¹ − 1 }` + +For `n ∈ {32, 64}`, `⟦Fn⟧` is the set of IEEE 754 binary-`n` data: + +* all finite values, including the two zeros `+0` and `−0`, +* the two infinities `+∞` and `−∞`, +* a single value `NaN`. + +Fpy does not distinguish NaN payloads and does not distinguish quiet from +signaling NaNs. Every operation that produces a NaN produces the **canonical +NaN** (sign bit 0, quiet bit set, payload 0); a NaN *input* may have any +encoding, and all encodings denote the single value `NaN`. + +> Note: canonical-NaN output matters because struct equality compares +> serialized bytes, so NaN payloads would otherwise be observable through +> `==` on aggregates even though float `==` is numeric. + +## Denotation + +The **denotation** `⟦x⟧` of a value `x` is the mathematical object it +represents. Let `ℝ* = ℝ ∪ {+∞, −∞, NaN}`. + +* If `x` is a value of an integer type: `⟦x⟧ = x ∈ ℤ`. +* If `x` is a finite float value: `⟦x⟧ ∈ ℝ` is the real number assigned by + IEEE 754. In particular `⟦+0⟧ = ⟦−0⟧ = 0` (the denotation is not injective + at zero; see the sign-of-zero clause below). +* `⟦+∞⟧ = +∞`, `⟦−∞⟧ = −∞`, `⟦NaN⟧ = NaN`, as elements of `ℝ*`. + +## Primitive conversion functions + +All casts are composed from four primitives. Each is **total** on its stated +domain; totality of every cast follows. + +**`round_T : ℝ* → ⟦T⟧`** for float `T` (IEEE 754 `convertFormat` / +`convertFromInt` with rounding attribute `roundTiesToEven`): + +1. `round_T(NaN) = NaN` +2. `round_T(+∞) = +∞`, `round_T(−∞) = −∞` +3. `round_T(0) = +0` +4. For nonzero real `r`: the value of `⟦T⟧` nearest to `r`, ties to the one + with even least significant mantissa digit. If `|r|` exceeds the IEEE + overflow threshold for `T`, the result is `+∞` or `−∞` with the sign of + `r` (**not** the largest finite value). If `r` rounds to zero, the result + is `+0` or `−0` with the sign of `r`. + +**`trunc : ℝ* → ℤ ∪ {+∞, −∞, NaN}`** (round toward zero): + +1. `trunc(NaN) = NaN`, `trunc(±∞) = ±∞` +2. For real `r`: the integer with largest magnitude such that + `|trunc(r)| ≤ |r|` and `sign(trunc(r)) ∈ {0, sign(r)}`. + +**`clamp_T : ℤ ∪ {+∞, −∞, NaN} → ⟦T⟧`** for integer `T` with bounds +`T_min`, `T_max`: + +1. `clamp_T(NaN) = 0` +2. `clamp_T(z) = T_min` if `z = −∞` or `z < T_min` +3. `clamp_T(z) = T_max` if `z = +∞` or `z > T_max` +4. `clamp_T(z) = z` otherwise + +**`wrap_T : ℤ → ⟦T⟧`** for integer `T` of bitwidth `n`: the unique +`r ∈ ⟦T⟧` with `r ≡ z (mod 2ⁿ)`. + +## Definition of cast + +A cast converts a value `x ∈ ⟦S⟧` to a value of type `T`. It is the total +function `cast_{S→T} : ⟦S⟧ → ⟦T⟧` defined by exactly one of the following +equations, selected by the kinds of `S` and `T`: + +| `S` | `T` | `cast_{S→T}(x)` | +|---|---|---| +| integer | integer | `wrap_T(x)` | +| integer | float | `round_T(x)` | +| float | float | `±0_T` if `x = ±0_S` (same sign); else `round_T(⟦x⟧)` | +| float | integer | `clamp_T(trunc(⟦x⟧))` | + +The sign-of-zero clause is required because `⟦·⟧` identifies `+0` and `−0`: +float→float casts preserve the sign of zero; float→integer casts map both +zeros to `0`. + +Integer→float casts are a **single direct rounding** into `T`. In +particular, `int → F32` is *not* defined as `int → F64 → F32`; the two +differ for some `|x| > 2⁵³` where the intermediate `F64` result lands +exactly on an `F32` tie (double rounding). + +> Note (rationale): casts never end the program. Arithmetic overflow ends +> the program, but a cast is an explicit request for conversion, so +> truncation/saturation is presumed intended; a program that wants different +> overflow handling can test the value before casting. +> +> Note (correspondence): these semantics coincide with Rust `as`, WASM +> `wrap`/`extend`/`convert`/`promote`/`demote`/`trunc_sat`, LLVM +> `trunc`/`sext`/`zext`/`sitofp`/`uitofp`/`fpext`/`fptrunc`/ +> `llvm.fptosi.sat`/`llvm.fptoui.sat`, and Java primitive conversions. +> They do **not** coincide with LLVM's plain `fptosi`/`fptoui` (poison on +> out-of-range) or WASM's plain `trunc` (traps). + +## Theorems + +The following hold for all numeric `S`, `T` and all `x ∈ ⟦S⟧`: + +* **T1 (totality, determinism).** `cast_{S→T}` assigns exactly one value of + `⟦T⟧` to every `x ∈ ⟦S⟧`. *(By construction: each equation is a + composition of total functions with exhaustive, mutually exclusive + cases.)* +* **T2 (identity).** `cast_{T→T}(x) = x`. +* **T3 (widening exactness).** If `⟦x⟧` is exactly representable in `T`, + then `⟦cast_{S→T}(x)⟧ = ⟦x⟧`. Consequences: `F32→F64` is exact; + integer→integer with same signedness and greater width is exact; + integer→float is exact when the integer fits in the mantissa + (`|x| ≤ 2²⁴` for `F32`, `|x| ≤ 2⁵³` for `F64`). +* **T4 (saturation boundaries).** For float→integer: + `cast(NaN) = 0`, `cast(+∞) = T_max`, `cast(−∞) = T_min`, `cast(±0) = 0`, + and for finite `x`, `cast(x) ∈ [T_min, T_max]` with equality at the + bounds exactly when `trunc(⟦x⟧)` is out of range on that side. +* **T5 (monotonicity).** Float→integer and integer→float casts are monotone + on non-NaN inputs: `x ≤ y ⇒ cast(x) ≤ cast(y)`. +* **T6 (round trips).** `S→T→S` is the identity when every value of `S` is + exactly representable in `T` (e.g. `I32→F64→I32`). It is **not** the + identity otherwise (e.g. `I64→F64→I64`, `I32→F32→I32`); the checker + exhibits counterexamples. +* **T7 (no double rounding).** Direct `U64→F32` differs from + `U64→F64→F32` for some inputs (the checker exhibits one); for `I32` and + narrower sources the two coincide. The spec mandates the direct form. diff --git a/MATH_COMPARISON.md b/MATH_COMPARISON.md new file mode 100644 index 0000000..6f350dc --- /dev/null +++ b/MATH_COMPARISON.md @@ -0,0 +1,261 @@ +# Fpy arithmetic semantics vs Rust and C# + +How fpy's arithmetic rules (MATH.md) compare to Rust and C#. **Every Rust and +C# claim in this document was verified empirically** by compiling and running +probe programs; the raw outputs are in the appendix. + +Verified with: + +* Rust: `rustc 1.96.0`, run twice: default profile (debug assertions ON) and + `-O` (debug assertions OFF), on x86-64 Linux. +* C#: .NET SDK `8.0.422` (RyuJIT, x86-64 Linux), default `unchecked` context + plus explicit `checked` expressions. + +## Integer arithmetic + +| Behavior | fpy | Rust | C# | +|---|---|---|---| +| `+ - *` overflow | halts, always | debug: panics; release: wraps (still defined as a bug; `checked_*`/`wrapping_*` express intent) | unchecked (default): wraps; `checked`: throws `OverflowException` | +| divide by zero | halts (`DOMAIN_ERROR`) | panics, **both profiles** | throws `DivideByZeroException`, always | +| remainder by zero | halts (`DOMAIN_ERROR`) | panics, both profiles | throws `DivideByZeroException`, always | +| `MIN / -1` (fpy `//`) | halts (`ARITHMETIC_OVERFLOW`) | panics, both profiles | throws `OverflowException`, **even unchecked** | +| `MIN % -1` | halts (`ARITHMETIC_OVERFLOW`) | panics, both profiles (`checked_rem` returns `None`) | throws `OverflowException`, even unchecked | +| division style | `//` floors toward -inf, `%` takes divisor's sign (Python) | `/` truncates toward zero, `%` takes dividend's sign (C); `div_euclid`/`rem_euclid` as methods | `/` truncates, `%` takes dividend's sign (C) | +| `/` on integers | always computes in F64 (true division) | stays integer | stays integer | + +Notes: + +* Both Rust and C# treat `+ - *` overflow checking as a *mode* (debug profile, + `checked` context) but check division unconditionally: div-by-zero and + `MIN/-1` are hard errors in every configuration, because the underlying + hardware/LLVM operation is undefined there. fpy's always-halt rule for + `+ - *` is Rust's debug behavior made permanent, which fpy's VM already + implements (`ARITHMETIC_OVERFLOW`/`UNDERFLOW`); the LLVM backend still wraps + instead of halting, so the two backends disagree here. Open. +* `MIN % -1` halting (rather than evaluating to 0) was decided 2026-07-06 to + match Rust and C#: **both** error here in every mode, even though the + mathematical remainder is 0. It also keeps `//` and `%` halting on exactly + the same inputs, so `a == (a // b) * b + (a % b)` holds wherever the pair is + defined. +* fpy is alone in floored division. Rust and C# are C-style truncating. fpy + follows Python because sequences are written by Python users; the VM, + the LLVM backend, and the spec all agree on floored. + +## Type discipline + +| Behavior | fpy | Rust | C# | +|---|---|---|---| +| unary `-` on unsigned | **compile error** (as of 2026-07-06) | compile error `E0600` (`wrapping_neg()` expresses intent) | `uint`: legal, **promotes to `long`** (result is correct, e.g. `-5`); `ulong`: compile error `CS0023` | +| mixed-width same-signedness (`u8 + u64`) | implicit widening to the 64-bit intermediate | compile error `E0277` (no implicit conversions at all) | implicit promotion (both sides widen) | +| mixed signedness (`i32 + u32`) | compile error | compile error `E0277` | promotes both to `long`; `ulong + int` is compile error `CS0034` (no type holds both) | +| int -> float implicit | allowed (RNE rounding, can be lossy for wide ints) | compile error `E0308` (`as` required) | allowed, even lossy `long -> float` | +| narrowing implicit (`i64 -> i32`) | compile error | compile error | compile error `CS0266` | + +Notes: + +* fpy sits between the two: stricter than C# (no signed/unsigned mixing) but + looser than Rust (implicit widening and int->float are allowed because the + 64-bit intermediate makes them value-preserving or explicitly rounding). +* C#'s `-uint -> long` promotion is the mathematically honest alternative to + rejecting unary minus on unsigned. fpy chose Rust's rule (reject) instead: + fpy's unsigned intermediate would have been U64, where C#'s trick has no + wider signed type to escape to -- exactly why C# rejects `-ulong`. + +## Floating point + +| Behavior | fpy | Rust | C# | +|---|---|---|---| +| `NaN != NaN` | True | true | True | +| `NaN == NaN`, `NaN < x` | False | false | False | +| `1.0 / 0.0` | +inf, no halt | inf, no panic | Infinity, no throw | +| `0.0 / 0.0` | NaN | NaN | NaN | +| float `%` style | floored, sign of divisor (`-7.5 % 2.0 == 0.5`, Python) | truncated fmod, sign of dividend (`-7.5 % 2.0 == -1.5`, C) | truncated fmod, sign of dividend (`-1.5`, C) | +| float `% 0.0` | NaN (never halts) | NaN, no panic | NaN, no throw | +| sign of an exact-multiple `%` zero | divisor's (`2.0 % -1.0 == -0.0`, Python) | dividend's (`2.0 % -1.0 == 0.0`, C fmod) | dividend's (`0.0`, C fmod) | +| overflow to +-inf, subnormals | IEEE-754 | IEEE-754 | IEEE-754 | + +Note on `% 0.0` (OQ-5, resolved 2026-07-06): Rust and C# both give NaN -- +float ops never trap in either language -- and fpy follows them: the spec, +the LLVM backend (frem), and the VM model all produce NaN. CPython raises +`ZeroDivisionError` instead; this is a deliberate divergence from Python. +The C++ `op_fmod` still returns DOMAIN_ERROR and needs the upstream fix +below. + +Note on the sign of a zero remainder (issue #129, settled 2026-08-06 when +`devel` merged in): fmod/frem give an exact-multiple remainder the *dividend's* +sign, but floored modulo takes it from the divisor, as CPython's `float_rem` +does with `copysign(0.0, divisor)`. fpy follows CPython here, so both the VM +model and the LLVM backend apply that `copysign` after the floor correction -- +a NaN remainder is excluded from it by testing `rem == 0` rather than the +correction's own `rem != 0`. This is the one place fpy's float `%` diverges +from plain C fmod beyond the floor correction itself. + +## Numeric casts + +| Behavior | fpy cast | Rust `as` | C# cast | +|---|---|---|---| +| int -> smaller int | wrap (truncate bits) | wrap (`-1i8 as u8 == 255`, `300i64 as u8 == 44`) | unchecked: wrap (`(byte)300 == 44`); checked: throws | +| float -> int, in range | truncate toward zero | truncate | truncate | +| float -> int, out of range | saturate to MIN/MAX | saturate (`300.0 as u8 == 255`, `-300.0 as i8 == -128`) | unchecked: **unspecified value** (measured on x64 .NET 8: sentinel `int.MinValue` for `(int)3e10`); checked: throws | +| NaN -> int | 0 | 0 | unchecked: measured `int.MinValue` (unspecified per spec); checked: throws | +| int -> float | round to nearest (RNE) | round to nearest | round to nearest | + +# TODO i think we might want to follow C# for the Nan-> int and float->int out of range + +fpy's cast spec (MATH_CASTS_DRAFT.md) is exactly Rust's `as` semantics -- Rust +moved float->int to saturating in 1.45 to remove the same UB fpy avoids. C# is +the outlier: its unchecked out-of-range float->int is explicitly "an +unspecified value of the destination type" (memory-safe UB), and on x64 .NET 8 +it produces a sentinel, not saturation. + +## User exit vs runtime fault + +Question: should a user-invoked `exit(code)` be distinguishable from a runtime +arithmetic fault, so a sequence cannot fake (or accidentally collide with) a +`DOMAIN_ERROR`? Precedent says yes, with one caveat about *where* the +distinction lives: + +* **Rust** separates *in process*: a panic runs the panic hook, prints + diagnostics, and can be observed by `catch_unwind`; `std::process::exit(n)` + does none of that. But at the OS level the channels collapse to one integer: + a panicking process exits with code 101, and `process::exit(101)` is + indistinguishable to the parent (verified). The separation is real only + because supervisors look at the panic diagnostics/hook, not the code. +* **C#** likewise: an unhandled exception has its own termination path, + diagnostics, and type; `Environment.Exit(n)` is just a code. In process the + channels are distinct; the integer alone is spoofable. +* **F Prime C++ FpySequencer already implements the separation correctly**: + `exit_directiveHandler` raises a dedicated event + (`SequenceExitedWithError(path, userCode)`) carrying the user's code, and + reports the directive error as `EXIT_WITH_ERROR` -- always. A user exit can + never surface as `DirectiveError::DOMAIN_ERROR`; the fault enum values are + reserved for actual faults. +* The **Python VM model** also keeps them apart: `handle_exit` sets + `error_code` (user-owned I32) and returns no directive error; faults return + a `DirectiveErrorCode` from the handler. +* The **LLVM/wasm backend** used to be the one place they were conflated (a + single `fpy_exit(i32)` host import shared by `exit()`, `assert`, and the + arithmetic guards). As of 2026-07-06 the wasm ABI has two noreturn host + imports: `fpy_exit(user_code)` for user-requested termination (exit(), + assert) and `fpy_fault(directive_error)` for runtime faults (division by + zero, arithmetic overflow). The test runner reports them as distinct + outcomes (`exit ` vs `fault `), and the test helpers refuse + cross-channel matches: `exit(10)` does not satisfy an expected + `DOMAIN_ERROR` even though `DOMAIN_ERROR`'s value is 10. + +The general lesson (which the Rust exit-code collision demonstrates): the +separation must live in the *channel*, not in an integer convention. + +## Known divergences to fix upstream (C++ FpySequencer) + +Found while verifying, in `Svc/FpySequencer/FpySequencerDirectives.cpp`: + +1. `op_sdiv` computes `lhs / rhs` with only a zero-divisor guard: + `INT64_MIN / -1` is C++ UB (SIGFPE on x86). Needs the overflow guard the + fpy model/backends now have. +2. `op_smod` computes `lhs % rhs` with only a zero-divisor guard: + `INT64_MIN % -1` is likewise UB. Same guard needed + (Rust/C# both error here; the fpy spec now halts with + `ARITHMETIC_OVERFLOW`). +3. `op_fmod` returns `DOMAIN_ERROR` on a zero divisor, but the fpy semantics + (spec, LLVM backend, VM model, Rust, C#, IEEE) is NaN with no halt. It + also computes `lhs - rhs * floor(lhs / rhs)`, which rounds at every step; + the spec's formula is exact truncated fmod plus at most one rounded + addition of the divisor (what `frem` + `fadd` and the VM model compute), + and the two differ in the last ulp for extreme operand ratios. +4. `exit_directiveHandler` pops the exit code as `U8`, while the fpy compiler + and Python model treat it as `I32` -- worth checking version alignment. + +## Appendix: probe outputs + +### Rust runtime (`rustc 1.96.0`) + +Left: default build (debug assertions on). Right: `-O` (off). Lines identical +between profiles are shown once. + +``` + debug release +i64_add_overflow_panics: true false +u64_sub_underflow_panics: true false +i64_mul_overflow_panics: true false +i64_div_by_zero_panics: true true +i64_rem_by_zero_panics: true true +i64_min_div_neg1_panics: true true +i64_min_rem_neg1_panics: true true +checked_rem_min_neg1: None +trunc_div_7_by_neg2: -3 +trunc_div_neg7_by_2: -3 +rem_neg7_by_2: -1 +rem_7_by_neg2: 1 +div_euclid_neg7_by_2: -4 +rem_euclid_neg7_by_2: 1 +wrapping_neg_5u32: 4294967291 +nan_ne_nan: true +nan_eq_nan: false +nan_lt_1: false +f64_1_div_0: inf +f64_0_div_0: NaN +f64_rem_neg7p5_by_2: -1.5 +f64_rem_7p5_by_neg2: 1.5 +f64_rem_1_by_0: NaN +as_sat_300f64_to_u8: 255 +as_sat_neg300f64_to_i8: -128 +as_nan_to_i32: 0 +as_wrap_neg1i8_to_u8: 255 +as_trunc_300i64_to_u8: 44 +as_2pow63_f64_to_i64_saturates: true +panic exit code: 101 +process::exit(101) exit code: 101 (indistinguishable to the parent) +``` + +Compile errors (all rejected): + +``` +-x where x: u32 error[E0600]: cannot apply unary operator `-` to type `u32` +i32 + u32 error[E0277]: cannot add `u32` to `i32` +u8 + u64 error[E0277]: cannot add `u64` to `u8` +let _: f64 = 1i64 error[E0308]: mismatched types +``` + +### C# runtime (.NET SDK 8.0.422, x64, default unchecked) + +``` +unchecked_add_wraps_to_min: True +checked_add: OverflowException +div_by_zero: DivideByZeroException +rem_by_zero: DivideByZeroException +min_div_neg1_unchecked: OverflowException +min_rem_neg1_unchecked: OverflowException +trunc_div_7_by_neg2: -3 +trunc_div_neg7_by_2: -3 +rem_neg7_by_2: -1 +rem_7_by_neg2: 1 +neg_uint_type: Int64 value -5 +uint_plus_int_type: Int64 value -1 +implicit_long_to_float: 9.223372E+18 +implicit_long_to_double: 9.223372036854776E+18 +nan_ne_nan: True +nan_eq_nan: False +nan_lt_1: False +f64_1_div_0: Infinity +f64_0_div_0: NaN +f64_rem_neg7p5_by_2: -1.5 +f64_rem_7p5_by_neg2: 1.5 +f64_rem_1_by_0: NaN +unchecked_double300_to_byte: 44 +unchecked_doubleNeg300_to_sbyte: -44 +unchecked_double3e10_to_int: -2147483648 +unchecked_nan_to_int: -2147483648 +checked_double3e10_to_int: OverflowException +unchecked_int300_to_byte: 44 +checked_int300_to_byte: OverflowException +long_to_double_rounds: True +``` + +Compile errors (all rejected): + +``` +-x where x: ulong error CS0023: Operator '-' cannot be applied to operand of type 'ulong' +ulong + int error CS0034: Operator '+' is ambiguous on operands of type 'ulong' and 'int' +int x = (long)y implicit error CS0266: Cannot implicitly convert type 'long' to 'int' +``` diff --git a/MATH_TODO.txt b/MATH_TODO.txt new file mode 100644 index 0000000..1c0fb46 --- /dev/null +++ b/MATH_TODO.txt @@ -0,0 +1,111 @@ +MATH_TODO: formal spec for numeric cast semantics +================================================== + +Goal +---- +Write a consistent, machine-checked spec for casting between numeric types +(U8-U64, I8-I64, F32, F64). "No undefined behavior" == the cast semantics is a +total, deterministic function: for every (source type S, target type T, value +v : S) the spec assigns exactly one result. Spec is written from scratch and is +normative; the current compiler, SPEC.md, MATH.md, and backends are NOT +authoritative and will be brought into line afterward. + +Chosen semantics (decided) +-------------------------- +Adopt the industry-consensus saturating conversion semantics. This is +simultaneously: WASM trunc_sat / promote / demote / convert, LLVM +llvm.fptosi.sat / fptoui.sat + fpext/fptrunc/sitofp/uitofp, Rust `as`, and +Java. LLVM and WASM do not meaningfully diverge on conversions once the +saturating variants are chosen; the only ecosystem split is trap-on-overflow +(WASM default trunc) vs saturate (everything else). We saturate, consistent +with the principle that casts never end the program. Never adopt LLVM's +default fptosi/fptoui -- out-of-range is poison, i.e. exactly the UB we are +eliminating. + +Per conversion class: +* int -> int: wrap (reduce mod 2^n, reinterpret as two's complement if T + signed). Total, no edge cases. +* int -> float: IEEE round-to-nearest-even, as a SINGLE direct rounding to + the target float type (int -> F32 does not go via F64; avoids double + rounding for |v| > 2^53 landing on F32 ties). Total. +* float -> float: widen is exact; narrow is IEEE RNE, overflow -> +/-inf + (NOT max-finite; resolves the open "?" in MATH.md draft). Total. +* float -> int: truncate toward zero, then clamp to [T::MIN, T::MAX]. + NaN -> 0. -0.0 -> 0. +/-inf clamp to max/min. Total, never traps. + +NaN policy: ignore signaling NaNs (like WASM). Stronger than WASM for +determinism: any operation producing NaN produces THE canonical quiet NaN +(sign 0, quiet bit set, payload 0). This matters because fpy struct equality +compares serialized bytes, so NaN payloads are observable through == on +structs even though float == is numeric. NaN inputs may be any NaN. + +Decided: int -> F32 is a direct single rounding +----------------------------------------------- +Spec = direct single RNE to F32 (what sitofp/convert do; standard). NOT the +composition int -> F64 -> F32: two roundings can double-round differently for +|v| > 2^53 when the F64 result lands exactly on an F32 tie. LLVM/WASM backends +already do direct conversion; the VM needs SITOFP/UITOFP variants targeting +F32 (+2 opcodes, see below). The Z3 harness should still encode both functions +and confirm they differ (produces the tie counterexample) as a sanity check. + +Current state (why change is needed) +------------------------------------ +* FpySequencer VM (../fprime-fpy-testbed/fprime/Svc/FpySequencer/ + FpySequencerDirectives.cpp, floatToWrappedIntBits): float->int truncates + then wraps mod 2^64, but returns DOMAIN_ERROR (sequence death) for NaN, + +/-inf, or magnitude >= 2^64. Matches no ecosystem semantics (I64(1e20) + wraps to garbage, I64(1e300) kills the sequence). Replace. +* Backends diverge today on float -> narrow int: LLVM saturates at target + width (fptosi.sat.i8: I8(300.0) == 127); bytecode saturates/wraps at 64-bit + then wrap-truncates (I8(300.0) == 44). Spec (saturate at target width) + ratifies the LLVM behavior; bytecode path must change. + +Bytecode (VM) changes +--------------------- +* Replace FPTOSI/FPTOUI with FTOI_SAT_{8,16,32,64}_{S,U} (8 opcodes, net +6): + pop F64, trunc toward zero, clamp to target range, NaN -> 0, push + sign/zero-extended to 64 bits. ~6 lines of C++ each; the mod-2^64 wrapping + logic goes away. DOMAIN_ERROR disappears from casts entirely. +* Add SITOFP_32/UITOFP_32 (or equivalent) for direct int -> F32 (+2 opcodes), + per the direct-rounding decision above. Result pushed as F32 extended to the + 64-bit stack slot via FPEXT semantics is NOT acceptable if it re-rounds; + push the F32 bit pattern / value such that the F32 result is exact. (An + fpext of the already-rounded F32 back to F64 is exact, so extending the + *result* to keep the 64-bit stack model is fine -- the rounding to F32 must + simply happen first.) +* Keep unchanged: FPEXT, FPTRUNC, SITOFP, UITOFP, SIEXT_*, ZIEXT_*, ITRUNC_* + (ITRUNC still correct for wrapping int->int casts). +* Rejected alternative: zero VM changes by emitting inline compare-and-clamp + before ITRUNC -- bloats every narrow cast site in uplinked sequences; + dedicated opcodes are easier to audit. +* LLVM backend: already correct (sat intrinsics). WASM backend: use + iN.trunc_sat_f64_s/u. Both get the spec essentially for free. + +Spec-writing plan +----------------- +1. Rewrite the Casts section of MATH.md denotationally, WASM-spec style: + define value sets (integers as subsets of Z; floats as finite IEEE values + plus +/-inf and canonical NaN), then two primitives round_T (RNE into a + float type) and clamp_T / wrap_T (into an int type), then each cast as a + total function composed from them. Crib definitional style from the WASM + Core spec numerics section (it is mechanized in Isabelle/Coq and already + written as total functions). +2. Mechanize in Z3 (Python bindings; native bitvector + IEEE-754 FloatingPoint + theories; everything finite so decidable/push-button). Encode each cast as + an ite-tree over total SMT ops -- total and deterministic by construction. + GOTCHA: SMT-LIB's fp.to_sbv/fp.to_ubv are themselves underspecified for + NaN/out-of-range; define our own total wrappers, use built-ins only on + their defined domain. +3. Check theorems for all (S, T) pairs: + - range soundness: result in [T::MIN, T::MAX] (the clamp actually clamps) + - identity: cast T -> T == id + - value preservation: if v exactly representable in T, cast preserves the + denoted real number (catches truncate-vs-round bugs) + - monotonicity of float->int and int->float on non-NaN inputs + - widening round-trips: I32 -> F64 -> I32 == id (holds); the checker + SHOULD produce a counterexample for I64 -> F64 -> I64 (that's it working) +4. Belt and suspenders: exhaustive enumeration for 8/16-bit types and + F32 -> * (2^32 inputs) against a reference implementation, in pytest. +5. Later / out of scope for now: per-backend "implements spec" checking + (translation validation); fixing the VM in fprime-fpy-testbed; arithmetic, + builtins (ln, iabs, fabs), overflow-traps-on-arithmetic rationale. diff --git a/src/fpy/codegen_llvm.py b/src/fpy/codegen_llvm.py index 08a67c6..1d3f3c5 100644 --- a/src/fpy/codegen_llvm.py +++ b/src/fpy/codegen_llvm.py @@ -211,10 +211,12 @@ def emit_AstBinaryOp(self, node: AstBinaryOp, state: CompileState) -> ir.Value: assert op in COMPARISON_OPS, op if is_float: - # IEEE `!=` is the negation of `==` and is therefore true when - # either operand is NaN (une, wasm's f64.ne, Python's !=). Every - # other comparison is ordered: false on NaN, like Python's. - if op == "!=": + # IEEE 754 defines != as the negation of ==, so it is true when + # either operand is NaN (une, wasm's f64.ne, Python's !=): that's + # fcmp une (unordered); fcmp_ordered would emit `one`, which is + # false on NaN. Every other comparison is ordered: false on NaN, + # like Python's. + if op == BinaryStackOp.NOT_EQUAL: return b.fcmp_unordered(op, lhs, rhs) return b.fcmp_ordered(op, lhs, rhs) # Enums and bools lower to integers too, so any integer-typed value @@ -230,6 +232,23 @@ def emit_AstBinaryOp(self, node: AstBinaryOp, state: CompileState) -> ir.Value: f"'{intermediate_type.display_name}' yet" ) + def _emit_halt_if(self, cond: ir.Value, code: DirectiveErrorCode) -> None: + """Guard an operation: end the whole sequence with the runtime fault + *code* when cond holds, otherwise fall through and continue lowering. + Faults go through the host's panic, not exit: they are runtime errors + raised by a check, not user exits.""" + b = self.builder + fail_block = b.append_basic_block("arith_fail") + ok_block = b.append_basic_block("arith_ok") + b.cbranch(cond, fail_block, ok_block) + b.position_at_end(fail_block) + b.call( + b.module.globals[HOST_PANIC_FUNC_NAME], + [ir.Constant(ERROR_CODE_TYPE, code.value)], + ) + b.unreachable() + b.position_at_end(ok_block) + def _emit_floor_divide( self, lhs: ir.Value, rhs: ir.Value, is_float: bool, is_signed: bool ) -> ir.Value: @@ -252,16 +271,26 @@ def _emit_floor_divide( quotient = b.fdiv(lhs, rhs) floor_fn = b.module.declare_intrinsic("llvm.floor", [quotient.type]) return b.call(floor_fn, [quotient]) - # The spec makes an integer zero divisor a DOMAIN_ERROR fault; wasm's - # integer div instructions would instead trap uncatchably, so guard - # first. - self._emit_zero_divisor_check(rhs, is_float=False) + # udiv/sdiv are immediate UB on a zero divisor in LLVM, and wasm's + # integer div instructions would trap uncatchably; the sequence must + # instead end with the same DOMAIN_ERROR the VM's handle_udiv / + # handle_sdiv return. + self._emit_zero_divisor_check(rhs) if not is_signed: # Unsigned operands are non-negative, so the exact quotient is too; # there's nothing below zero to floor toward, so udiv (which # truncates) already gives the floored result. return b.udiv(lhs, rhs) + # sdiv MIN,-1 is UB as well: the mathematical quotient 2^(n-1) is not + # representable, so the sequence ends with an overflow error. + int_min = ir.Constant(lhs.type, -(1 << (lhs.type.width - 1))) + minus_one = ir.Constant(lhs.type, -1) + overflow = b.and_( + b.icmp_signed("==", lhs, int_min), b.icmp_signed("==", rhs, minus_one) + ) + self._emit_halt_if(overflow, DirectiveErrorCode.ARITHMETIC_OVERFLOW) + # Signed integers have no floor instruction: sdiv truncates toward zero. # Truncation and floor agree except when the exact quotient is negative # and non-integer -- i.e. the operands have opposite signs (negative @@ -295,16 +324,19 @@ def _emit_modulo( lowers to an fmod libcall on wasm, hence the imported env.fmod.) """ b = self.builder - # The spec makes a zero divisor a DOMAIN_ERROR fault for *every* - # modulo, including floats (unlike float division, which is IEEE): - # wasm's integer rem instructions would trap uncatchably, and the - # host fmod would return NaN, so guard first. - self._emit_zero_divisor_check(rhs, is_float) + zero = ir.Constant(lhs.type, 0) + if not is_float: + # urem/srem are immediate UB on a zero divisor in LLVM, and wasm's + # integer rem instructions would trap uncatchably; the sequence + # must instead end with the same DOMAIN_ERROR the VM's + # handle_umod/handle_smod return. A *float* zero divisor is not + # guarded: `x % 0.0` is NaN and never halts (IEEE, Rust and C#; + # see MATH_COMPARISON.md), which is what frem/fmod already give. + self._emit_zero_divisor_check(rhs) if not is_float and not is_signed: # Unsigned operands are non-negative, so floored == truncated. return b.urem(lhs, rhs) - zero = ir.Constant(lhs.type, 0) if is_float: rem = b.frem(lhs, rhs) nonzero = b.fcmp_ordered("!=", rem, zero) @@ -313,39 +345,51 @@ def _emit_modulo( ) corrected = b.fadd(rem, rhs) else: + # srem MIN,-1 is UB (and errors in the VM and in Rust) even + # though the remainder itself would be 0: it halts exactly like + # MIN // -1 does. + int_min = ir.Constant(lhs.type, -(1 << (lhs.type.width - 1))) + minus_one = ir.Constant(lhs.type, -1) + overflow = b.and_( + b.icmp_signed("==", lhs, int_min), + b.icmp_signed("==", rhs, minus_one), + ) + self._emit_halt_if(overflow, DirectiveErrorCode.ARITHMETIC_OVERFLOW) rem = b.srem(lhs, rhs) nonzero = b.icmp_signed("!=", rem, zero) # rem and rhs have differing signs iff their xor is negative. signs_differ = b.icmp_signed("<", b.xor(rem, rhs), zero) corrected = b.add(rem, rhs) - return b.select(b.and_(nonzero, signs_differ), corrected, rem) + result = b.select(b.and_(nonzero, signs_differ), corrected, rem) + if is_float: + # An exact division leaves a zero whose sign frem takes from the + # *dividend*; floored modulo takes it from the divisor, as CPython's + # float_rem does with copysign(0.0, divisor) (issue #129). The test + # is `rem == 0` rather than `not nonzero` so a NaN remainder -- for + # which every ordered compare is false -- passes through untouched. + is_zero = b.fcmp_ordered("==", rem, zero) + # copysign is binary, so its signature has to be given explicitly: + # llvmlite only infers a unary one from the mangling type list. + copysign_fn = b.module.declare_intrinsic( + "llvm.copysign", + [rem.type], + ir.FunctionType(rem.type, [rem.type, rem.type]), + ) + signed_zero = b.call(copysign_fn, [zero, rhs]) + result = b.select(is_zero, signed_zero, result) + return result - def _emit_zero_divisor_check(self, rhs: ir.Value, is_float: bool) -> None: - """Fault with DOMAIN_ERROR when the divisor *rhs* is zero, per the - spec's modulus and floor-division semantics. (fcmp `==` treats -0.0 - as zero, so a -0.0 divisor faults too.)""" + def _emit_zero_divisor_check(self, rhs: ir.Value) -> None: + """Fault with DOMAIN_ERROR when the integer divisor *rhs* is zero, per + the spec's modulus and floor-division semantics. Floats never reach + here: they have no zero-divisor error at all.""" b = self.builder zero = ir.Constant(rhs.type, 0) - # A hardware float compare of a NaN operand against anything has no - # meaningful true/false answer, so every fcmp predicate must pick one - # up front, and that's the whole ordered/unordered split: *ordered* - # predicates answer false when an operand is NaN, *unordered* ones - # answer true. Concretely, with rhs = NaN: - # fcmp_ordered("==", NaN, 0.0) -> false (what we want: no fault) - # fcmp_unordered("==", NaN, 0.0) -> true (would fault on NaN!) - # A NaN divisor must not fault here: the spec faults only a *zero* - # divisor and defines `lhs % nan` as nan -- which is exactly what - # frem/fmod return. - # On the int side, signedness doesn't exist for equality: LLVM has a - # single `icmp eq` (signed/unsigned variants exist only for order - # predicates like slt/ult), so icmp_signed("==") and - # icmp_unsigned("==") emit the same instruction and unsigned operands - # are fine here. - is_zero = ( - b.fcmp_ordered("==", rhs, zero) - if is_float - else b.icmp_signed("==", rhs, zero) - ) + # Signedness doesn't exist for equality: LLVM has a single `icmp eq` + # (signed/unsigned variants exist only for order predicates like + # slt/ult), so icmp_signed("==") and icmp_unsigned("==") emit the same + # instruction and unsigned operands are fine here. + is_zero = b.icmp_signed("==", rhs, zero) fail_block = b.function.append_basic_block("div_zero") ok_block = b.function.append_basic_block("div_ok") b.cbranch(is_zero, fail_block, ok_block) diff --git a/src/fpy/semantics.py b/src/fpy/semantics.py index f1569bf..5fb45e3 100644 --- a/src/fpy/semantics.py +++ b/src/fpy/semantics.py @@ -1663,6 +1663,18 @@ def pick_intermediate_type( if not all(t.is_numerical for t in arg_types): return None + # negation is undefined for unsigned integers (as in Rust): the result + # is negative for every nonzero operand, which no unsigned type can + # represent. NOTE: the arity check is what distinguishes negation from + # subtraction -- ops are str-valued and both are "-" (and the AST + # carries plain strings, so an enum identity check won't work either) + if ( + len(arg_types) == 1 + and op == UnaryStackOp.NEGATE + and arg_types[0] in UNSIGNED_INTEGER_TYPES + ): + return None + # division and exponentiation always operate over floats if op in (BinaryStackOp.DIVIDE, BinaryStackOp.EXPONENT): if all(t in ARBITRARY_PRECISION_TYPES for t in arg_types): diff --git a/src/fpy/test_helpers.py b/src/fpy/test_helpers.py index 8c42e6b..e76964f 100644 --- a/src/fpy/test_helpers.py +++ b/src/fpy/test_helpers.py @@ -229,8 +229,8 @@ def _run_seq_wasm( failing_opcodes: set[int] = None, cmd_response: int = None, ) -> tuple[int, list[tuple[int, str]], list[bytes]]: - """Compile *seq* to wasm, run it through the spacewasm runner harness, and - return (error code, reported events, dispatched command buffers). + """Compile *seq* to wasm, run it through the wasm harness, and return + (error code, reported events, dispatched command buffers). The commands that fail are *failing_opcodes* plus the RUN commands that always fail when called from within a running sequence on the same @@ -689,6 +689,26 @@ def assert_run_failure( error_code is not None or validation_error ), "Must specify either error_code or validation_error" + # The expected failure's channel: a DirectiveErrorCode other than + # EXIT_WITH_ERROR is a runtime panic (a compiler-emitted guard); + # EXIT_WITH_ERROR (a bare assert) and raw ints (exit(n)) come through the + # exit channel. The channels must not cross-match: exit(10) does not + # satisfy an expected DOMAIN_ERROR even though DOMAIN_ERROR's value is 10. + expect_panic = ( + isinstance(error_code, DirectiveErrorCode) + and error_code != DirectiveErrorCode.EXIT_WITH_ERROR + ) + # ...except that the bytecode ISA has no panic-raising directive, so the + # compiler lowers ITS OWN runtime checks (array bounds, assert_cmd_success) + # to `PushVal(code); Exit` -- on the VM these semantically-panic codes ride + # the exit channel by construction. The wasm backend does the same for + # CMD_FAIL. TODO(upstream): give the FpySequencer ISA a panic directive so + # these stop being spoofable via exit(). + COMPILED_IN_CHECK_CODES = { + DirectiveErrorCode.ARRAY_OUT_OF_BOUNDS, + DirectiveErrorCode.CMD_FAIL, + } + if USE_WASM: if fprime_test_api is not None: # GDS mode: send the wasm module and assert that it fails via @@ -708,7 +728,9 @@ def assert_run_failure( return # The wasm backend has no separate validation step or VM-internal # faults: a failed sequence is one that reports a nonzero code - # through the exit/fault host imports. + # through the exit/panic host imports. The sequencer conflates the + # two imports into one exit code, so unlike the bytecode path below + # this can only compare codes, not channels. code = run_seq_wasm( seq, ground_binary_dir=ground_binary_dir, @@ -776,16 +798,28 @@ def assert_run_failure( if validation_error: raise RuntimeError("Expected ValidationError, got", type(e).__name__, e) - # The failure surfaces as either a DirectiveErrorCode trap or a raw exit - # code int; the expected value may likewise be either. Compare by integer - # value so e.g. an exit code of 7 matches DirectiveErrorCode.EXIT_WITH_ERROR. - def _as_int(v): - return v.value if isinstance(v, DirectiveErrorCode) else v - - if len(e.args) == 1 and _as_int(e.args[0]) != _as_int(error_code): - raise RuntimeError( - "run_seq failed with error", e.args[0], "expected", error_code - ) + # The failure's channel is encoded in the arg type: a runtime panic + # surfaces as a DirectiveErrorCode trap, a user exit as a raw int. + # The channels must not cross-match (see expect_panic above), except + # for the compiled-in checks that the bytecode ISA forces through the + # exit channel. + if len(e.args) == 1: + got = e.args[0] + if expect_panic: + ok = isinstance(got, DirectiveErrorCode) and got == error_code + if error_code in COMPILED_IN_CHECK_CODES: + ok = ok or got == error_code.value + else: + want = ( + error_code.value + if isinstance(error_code, DirectiveErrorCode) + else error_code + ) + ok = not isinstance(got, DirectiveErrorCode) and got == want + if not ok: + raise RuntimeError( + "run_seq failed with error", got, "expected", error_code + ) print(e) return diff --git a/test/fpy/test_arithmetic.py b/test/fpy/test_arithmetic.py index eee77a0..35e5da2 100644 --- a/test/fpy/test_arithmetic.py +++ b/test/fpy/test_arithmetic.py @@ -13,6 +13,12 @@ class TestConstantFolding: + def test_asdf(self, fprime_test_api): + seq = """ +""" + + assert_run_success(fprime_test_api, seq) + def test_overflow_compile_error(self, fprime_test_api): seq = """ val1: U8 = 256 # Should fail: value too large for U8 @@ -694,3 +700,159 @@ def test_float_floor_div_inf_nan_passthrough(self, fprime_test_api): assert q != q """ assert_run_success(fprime_test_api, seq) + + +class TestIntDivisionGuards: + """Runtime integer division/modulo must end the sequence instead of + hitting undefined behavior: zero divisors are a DOMAIN_ERROR (matching + the VM's handle_udiv/sdiv/umod/smod), and I64_MIN // -1 is an + ARITHMETIC_OVERFLOW (its quotient 2^63 is unrepresentable). Operands are + variables so the const folder can't resolve them at compile time.""" + + def test_signed_floor_div_by_zero_halts(self, fprime_test_api): + seq = """ +a: I64 = 1 +b: I64 = 0 +result: I64 = a // b +""" + assert_run_failure(fprime_test_api, seq, DirectiveErrorCode.DOMAIN_ERROR) + + def test_unsigned_floor_div_by_zero_halts(self, fprime_test_api): + seq = """ +a: U64 = 1 +b: U64 = 0 +result: U64 = a // b +""" + assert_run_failure(fprime_test_api, seq, DirectiveErrorCode.DOMAIN_ERROR) + + def test_signed_mod_by_zero_halts(self, fprime_test_api): + seq = """ +a: I64 = 1 +b: I64 = 0 +result: I64 = a % b +""" + assert_run_failure(fprime_test_api, seq, DirectiveErrorCode.DOMAIN_ERROR) + + def test_unsigned_mod_by_zero_halts(self, fprime_test_api): + seq = """ +a: U64 = 1 +b: U64 = 0 +result: U64 = a % b +""" + assert_run_failure(fprime_test_api, seq, DirectiveErrorCode.DOMAIN_ERROR) + + def test_int_min_floor_div_minus_one_halts(self, fprime_test_api): + seq = """ +a: I64 = -9223372036854775808 +b: I64 = -1 +result: I64 = a // b +""" + assert_run_failure(fprime_test_api, seq, DirectiveErrorCode.ARITHMETIC_OVERFLOW) + + def test_int_min_mod_minus_one_halts(self, fprime_test_api): + """I64_MIN % -1 halts like I64_MIN // -1 (Rust's rule): the + mathematical remainder would be 0, but the operation is UB in + C++/LLVM and // and % halt on exactly the same inputs.""" + seq = """ +a: I64 = -9223372036854775808 +b: I64 = -1 +result: I64 = a % b +""" + assert_run_failure(fprime_test_api, seq, DirectiveErrorCode.ARITHMETIC_OVERFLOW) + + +class TestUnaryMinusUnsigned: + """Unary minus is undefined for unsigned integer types (compile error, + as in Rust): the result is negative for every nonzero operand, which no + unsigned type can represent.""" + + def test_negate_unsigned_var_is_compile_error(self, fprime_test_api): + seq = """ +a: U32 = 5 +b: I64 = -a +""" + assert_compile_failure(fprime_test_api, seq, match="undefined") + + def test_negate_unsigned_const_is_compile_error(self, fprime_test_api): + seq = """ +a: I64 = -U8(5) +""" + assert_compile_failure(fprime_test_api, seq, match="undefined") + + def test_negate_signed_and_float_still_work(self, fprime_test_api): + seq = """ +a: I32 = 5 +b: F64 = 2.5 +assert -a == -5 +assert -b == -2.5 +""" + assert_run_success(fprime_test_api, seq) + + +class TestNaNComparisons: + """IEEE 754 comparisons with NaN: every comparison is false, except != + which is the negation of == and hence true. The NaN is produced at + runtime (0.0/0.0 of variables) so nothing is const-folded.""" + + def test_nan_neq_nan_is_true(self, fprime_test_api): + seq = """ +zero: F64 = 0.0 +nan: F64 = zero / zero +assert nan != nan +""" + assert_run_success(fprime_test_api, seq) + + def test_nan_eq_nan_is_false(self, fprime_test_api): + seq = """ +zero: F64 = 0.0 +nan: F64 = zero / zero +assert not (nan == nan) +""" + assert_run_success(fprime_test_api, seq) + + def test_nan_ordered_comparisons_are_false(self, fprime_test_api): + seq = """ +zero: F64 = 0.0 +nan: F64 = zero / zero +assert not (nan < 1.0) +assert not (nan <= 1.0) +assert not (nan > 1.0) +assert not (nan >= 1.0) +""" + assert_run_success(fprime_test_api, seq) + + +class TestFloatModIEEE: + """Float % follows IEEE (and Rust/C#): it never halts. x % 0.0 and + inf % y are NaN. (CPython raises ZeroDivisionError instead; fpy + deliberately follows IEEE -- see MATH_COMPARISON.md.) Operands are + variables so nothing is const-folded.""" + + def test_float_mod_by_zero_is_nan(self, fprime_test_api): + seq = """ +a: F64 = 1.0 +b: F64 = 0.0 +c: F64 = a % b +assert c != c +""" + assert_run_success(fprime_test_api, seq) + + def test_inf_mod_is_nan(self, fprime_test_api): + seq = """ +one: F64 = 1.0 +zero: F64 = 0.0 +inf: F64 = one / zero +c: F64 = inf % 2.0 +assert c != c +""" + assert_run_success(fprime_test_api, seq) + + def test_finite_mod_inf_is_identity(self, fprime_test_api): + seq = """ +one: F64 = 1.0 +zero: F64 = 0.0 +inf: F64 = one / zero +c: F64 = -5.0 % inf +assert c == inf +""" + assert_run_success(fprime_test_api, seq) diff --git a/test/fpy/test_assert.py b/test/fpy/test_assert.py index 45d001d..1e029c9 100644 --- a/test/fpy/test_assert.py +++ b/test/fpy/test_assert.py @@ -43,3 +43,19 @@ def test_assert_wrong_exit_code_type(self, fprime_test_api): """ assert_compile_failure(fprime_test_api, seq) + + def test_exit_code_does_not_impersonate_fault(self, fprime_test_api): + """User exits and runtime faults are separate channels: exit(10) + matches the raw code 10, but must NOT satisfy an expected + DOMAIN_ERROR fault even though DOMAIN_ERROR's value is also 10.""" + if fprime_test_api is not None: + return # GDS mode reports failures via events, not channels + assert_run_failure(fprime_test_api, "exit(10)", 10) + try: + assert_run_failure( + fprime_test_api, "exit(10)", DirectiveErrorCode.DOMAIN_ERROR + ) + except RuntimeError: + pass + else: + raise AssertionError("exit(10) was accepted as a DOMAIN_ERROR fault") diff --git a/test/fpy/test_wasm.py b/test/fpy/test_wasm.py index dc0c2d8..a95bb2a 100644 --- a/test/fpy/test_wasm.py +++ b/test/fpy/test_wasm.py @@ -418,12 +418,16 @@ def test_floor_divide_by_zero_faults(self): assert run_seq_wasm("z: I64 = 0\nx: I64 = 17 // z\n") == DOMAIN_ERROR def test_modulus_by_zero_faults(self): - # Like division -- and unlike float `/` -- a zero divisor in `%` is - # DOMAIN_ERROR even for floats (the VM checks it; libm fmod would - # quietly return NaN). + # Like division, an integer zero divisor in `%` is DOMAIN_ERROR. assert run_seq_wasm("z: U64 = 0\nx: U64 = 17 % z\n") == DOMAIN_ERROR assert run_seq_wasm("z: I64 = 0\nx: I64 = 17 % z\n") == DOMAIN_ERROR - assert run_seq_wasm("z: F64 = 0.0\nx: F64 = 5.5 % z\n") == DOMAIN_ERROR + + def test_float_modulus_by_zero_is_nan(self): + # A *float* zero divisor is not a fault: `x % 0.0` is NaN and never + # halts (IEEE, Rust and C#; see MATH_COMPARISON.md), which is what + # frem/fmod already give. NaN is observable as `c != c`. + seq = "z: F64 = 0.0\nc: F64 = 5.5 % z\nassert c != c\n" + assert run_seq_wasm(seq) == NO_ERROR def test_float_divide_by_zero_is_ieee(self): # Float `/` (and thus float `//`) by zero is IEEE inf, not a fault,