From e37366f8dd9f62bc2d8d60927a3fc7dc4cde4ef2 Mon Sep 17 00:00:00 2001 From: Brummel Date: Sun, 10 May 2026 14:14:54 +0200 Subject: [PATCH] =?UTF-8?q?spec:=20floats=20LLVM-IR=20fixes=20=E2=80=94=20?= =?UTF-8?q?fcmp=20une=20for=20!=3D,=20synth.rs=20sites,=20container-slot?= =?UTF-8?q?=20precision?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Three classes of fix from the LLVM-IR audit: 1. != on Float: fcmp une, NOT fcmp one. one is 'ordered and not equal' (false for nan!=nan, breaks IEEE / user-fixed constraint). une is 'unordered or not equal' (true for nan!=nan, matches IEEE and Rust f64::ne). 2. crates/ailang-codegen/src/synth.rs touches the Float primitive at five sites the original spec missed: llvm_type, builtin_ail_type, builtin_effect_op_ret, type_descriptor (descriptor 'Fl' to avoid collision with ADT-name F-prefix), builtin_binop (becomes a transitional artefact, replaced by type-dispatched helper). 3. Float literals lower as LLVM hex-float syntax (double 0x4014...); nan/inf/neg_inf as direct SSA double constants at use site (NOT via the __unreachable__ analogue, which is a terminator instruction not a value); container slot layout precision (monomorphisation vs bitcast). --- docs/specs/2026-05-10-floats.md | 146 +++++++++++++++++++++++++------- 1 file changed, 115 insertions(+), 31 deletions(-) diff --git a/docs/specs/2026-05-10-floats.md b/docs/specs/2026-05-10-floats.md index b6dc1f7..4be11e9 100644 --- a/docs/specs/2026-05-10-floats.md +++ b/docs/specs/2026-05-10-floats.md @@ -133,12 +133,23 @@ lib.rs:2244-2266`): | `*` | `mul i64` | `fmul double` | | `/` | `sdiv i64` | `fdiv double` | | `==` | existing `icmp eq i64` / `i1` / `@strcmp` / `i1 1` | `fcmp oeq double` | -| `!=` | derived from `==` | `fcmp one double` | +| `!=` | existing `icmp ne i64` etc. | `fcmp une double` | | `<` | `icmp slt i64` | `fcmp olt double` | | `<=` | `icmp sle i64` | `fcmp ole double` | | `>` | `icmp sgt i64` | `fcmp ogt double` | | `>=` | `icmp sge i64` | `fcmp oge double` | +**Note on `!=`:** the LLVM `fcmp` predicate for IEEE-`!=` is +`une` ("unordered or not equal"), **not** `one` ("ordered and +not equal"). `one` would return `false` for `nan != nan`, which +contradicts user-fixed constraint #2 (NaN ≠ NaN per IEEE). +`une` matches Rust's `f64::ne` and IEEE 754 `!=` exactly. + +**Note on `==`:** `fcmp oeq` returns `false` whenever either +operand is NaN, which is the IEEE-`==` semantics we want. +Bit-level NaN-detection is separate and uses `is_nan` (below) +or `fcmp uno`. + Non-{Int,Float} resolutions for `+`/`-`/`*`/`/`/`<`/`<=`/`>`/`>=` get rejected at codegen with the same diagnostic shape the `==` path uses today (`"+ not supported for type X"`). The reject @@ -356,50 +367,123 @@ the plan for iteration boundaries. ### `crates/ailang-codegen/` -- `lib.rs` (2877 LoC) — six lowering changes: +- `synth.rs` (218 LoC) — five sites mirroring the Float + primitive into the codegen-side type/op tables: + 1. `llvm_type` (line 14): add `"Float" => Ok("double".into())` + arm parallel to the existing Int/Bool/Str/Unit arms. + 2. `builtin_ail_type` (line 61): widen the `+`/`-`/`*`/`/`, + `<`/`<=`/`>`/`>=`, `!=` entries from `int_int_int` / + `int_int_bool` to the polymorphic `forall a. (a, a) -> a` + / `forall a. (a, a) -> Bool` shape (mirrors what + `check/builtins.rs` installs). Add new entries for `neg` + (polymorphic), `int_to_float`, `float_to_int_truncate`, + `float_to_str`, `is_nan`, `nan`/`inf`/`neg_inf` (the + constants resolve as zero-arg "values", not fns — the + branch returns the bare `Type::float()` like + `__unreachable__` returns `forall a. a`). + 3. `builtin_effect_op_ret` (line 118): add + `"io/print_float" => Type::unit()`. + 4. `type_descriptor` (line 129): add `"Float" => "Fl"` arm. + Two letters because the single letter `F` is taken as + the ADT-name prefix (`FList`, `FFoo`); `Fl` is unambiguous + and short. + 5. `builtin_binop` (line 167): this monomorphic-Int table + becomes a transitional artefact. Either convert it into a + type-dispatched helper that takes the operand `Type` and + returns the matching `(instr, llvm_ty)` pair, or remove + the table entirely and let the new dispatch helper in + `lib.rs` handle every site. Plan-time call. + +- `lib.rs` (2877 LoC) — seven lowering changes: 1. **Float literal** (`Literal::Float { bits }`) → emit - `double` constant via LLVM hex-float syntax - `0x1p+0`-style or via `bitcast i64 0x... to double`. - Sites: every place `Literal::Int { value }` is matched - today (lines 918, 1215). + a `double` constant. The idiomatic LLVM form for a + bit-exact float constant is the hex-float literal + `double 0x4014000000000000` (LangRef: "the only time + hexadecimal floating point constants are required ... + is when a floating point constant must be emitted but + it cannot be represented as a decimal floating point + number in a reasonable number of digits", which covers + NaN, ±Inf, and any non-trivial decimal). Use this form + uniformly so every Float literal in the IR has the same + shape. Sites: every place `Literal::Int { value }` is + matched today (lines 918, 1215). 2. **Widen arithmetic dispatch.** `+`/`-`/`*`/`/` are today lowered as monomorphic Int instructions - (line 1745 region). Convert the lowering site into a - type-dispatched helper analogous to the existing `==` - dispatch (`lib.rs:2244-2266`): Int arm emits - `add/sub/mul/sdiv i64`, Float arm emits - `fadd/fsub/fmul/fdiv double`, anything else fails with - `" not supported for type X"`. - 3. **Widen comparison dispatch.** `<`/`<=`/`>`/`>=` get the - same treatment: Int arm `icmp s{lt,le,gt,ge} i64`, Float - arm `fcmp o{lt,le,gt,ge} double`, reject otherwise. - 4. **`==` / `!=` Float arm** in the existing dispatch - (line 2263 region) → `fcmp oeq` / `fcmp one` for the - `Float` case, alongside the existing arms. + (line 1745 region) using the `synth::builtin_binop` + table. Convert the lowering site into a type-dispatched + helper analogous to the existing `==` dispatch + (`lib.rs:2244-2266`): Int arm emits `add/sub/mul/sdiv + i64`, Float arm emits `fadd/fsub/fmul/fdiv double`, + anything else fails with `" not supported for type + X"`. The existing test at `lib.rs:2627-2630` (which + pins `define i64 @ail_t_add(i64 %arg_a, i64 %arg_b)` and + `add i64 %arg_a, %arg_b`) must stay GREEN. + 3. **Widen comparison dispatch.** `<`/`<=`/`>`/`>=`/`!=` + get the same treatment: Int arm `icmp s{lt,le,gt,ge} i64` + / `icmp ne i64`, Float arm `fcmp o{lt,le,gt,ge} double` + / **`fcmp une double` for `!=`** (NOT `fcmp one` — + `one` is "ordered and not equal" and returns `false` + for `nan != nan`, which violates IEEE; `une` is + "unordered or not equal" and matches IEEE / Rust). + 4. **`==` Float arm** in the existing dispatch + (line 2263 region) → `fcmp oeq double` for the `Float` + case, alongside the existing arms. (`!=` is handled + under #3 above.) 5. **`neg` polymorphic** — Int arm `sub i64 0, %x`, Float - arm `fneg double %x` (correct for `-0.0`, unlike a - hypothetical `(- 0.0 x)` desugar). Reject other types. + arm `fneg double %x`. The `fneg` instruction (LLVM 8+) + correctly handles `-0.0` — `0.0 - 0.0` is `+0.0` per + IEEE rounding, so a `fsub double 0.0, %x` desugar would + wrongly produce `+0.0` for `neg(+0.0)` instead of + `-0.0`. Reject other types with the dispatch's standard + diagnostic. 6. **Conversions and IO**: - `int_to_float` → `sitofp i64 ... to double`. - `float_to_int_truncate` → `@llvm.fptosi.sat.i64.f64` - intrinsic (or the legalised cast sequence if the - target backend doesn't expose it directly). + intrinsic (LLVM 12+; AILang targets clang 22, so + always available). Spec semantics — NaN → 0, + +∞ → i64::MAX, -∞ → i64::MIN, finite-out-of-range + saturates, finite-in-range truncates toward zero — + are exactly the intrinsic's documented semantics, no + wrapping needed. - `is_nan` → `fcmp uno double %x, %x` (returns `i1`, - which already coerces to AILang `Bool`). + which is AILang `Bool` directly per `synth.rs:18`). - `float_to_str` → call into runtime C glue `@ail_float_to_str`. - `io/print_float` → parallel to `io/print_int` (line 2150 region) → call into runtime C glue `@ail_print_float`. 7. **Float constants** `nan`/`inf`/`neg_inf` lower as - `Term::Var` references resolving to compile-time `double` - constants (the codegen path that resolves `Var "x"` to - the SSA value of a global gets a builtin-constant arm, - same way `__unreachable__` resolves to `unreachable`). -- ADT / container layout — `double` is 8 bytes, fits the - existing 8-byte slot used for `i64` and `ptr`. **No layout - change.** Confirm this by inspecting how `List` lowers - today and verifying the same layout works for `List`. + `Term::Var` references resolving directly to a `double` + SSA constant at the use site (LLVM hex-float literal): + - `nan` → `double 0x7FF8000000000000` (canonical qNaN) + - `inf` → `double 0x7FF0000000000000` + - `neg_inf` → `double 0xFFF0000000000000` + + This is **unlike** the `__unreachable__` lowering, which + emits the `unreachable` *terminator instruction*. + Constants are SSA *values*, so the dispatch arm in + `lower_var` (or wherever `Var` resolution lives) returns + `(value-string, "double")` directly without going through + a global declaration. + +- **ADT / container slot layout** — both `i64` and `double` + occupy 8 bytes, but they are distinct LLVM types. Two cases: + - **Monomorphisation produces concrete slot types.** If the + mono pass (`crates/ailang-check/src/mono.rs`) lowers + `List` to a concrete `List_Fl` whose field type is + `double`, no bitcast is needed. The `type_descriptor` + extension above (`Fl`) ensures the mangled name is + distinct from `List` (`List_I`). + - **Polymorphic / type-erased slots, if any.** If any + container path uses `i64` or `ptr` as a generic 8-byte + slot (e.g. an erased `Box` that doesn't get + monomorphised), Float values traversing it need + `bitcast double to i64` going in and `bitcast i64 to + double` coming out. The plan verifies which case applies + by reading `mono.rs` and `lib.rs::lower_ctor` / + `lower_field_access`. The expected outcome is "fully + monomorphised, no bitcasts needed", but this is a + *check*, not an assumption. ### `crates/ailang-prose/`