|
| 1 | +// SPDX-License-Identifier: AGPL-3.0-or-later |
| 2 | +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 3 | += String-wall slices 9–10 + completion capstone (2026-06-14) |
| 4 | +:toc: macro |
| 5 | + |
| 6 | +toc::[] |
| 7 | + |
| 8 | +== Context |
| 9 | + |
| 10 | +The "string wall" is the family of `String`-typed operations that the wasm |
| 11 | +backend lowered to integer ops on the underlying `[len: i32][utf8 bytes]` |
| 12 | +*pointer* rather than on the string's bytes. A `String` value is an i32 pointer |
| 13 | +into linear memory, so any pointer-level integer op gives a wrong answer for two |
| 14 | +equal-valued strings that live at distinct heap addresses (e.g. a literal vs a |
| 15 | +string built at runtime). |
| 16 | + |
| 17 | +Slices 1–7 established the byte-level string primitives (length, indexing, |
| 18 | +byte-scan helpers, `startsWith`/`contains`, the WASI `env_at`/`arg_at` string |
| 19 | +builders). Slice 8 split into 8a (a *sound-rejection guard* that loudly refused |
| 20 | +the syntactically-obvious string `++` cases codegen could not yet lower) and 8b |
| 21 | +(the type-directed `ExprStringConcat` lowering). This document records slices |
| 22 | +9 (equality) and 10 (relational) — which complete the wall — and the final |
| 23 | +hardening. |
| 24 | + |
| 25 | +== The type-channel pattern (shared by 8b / 9 / 10) |
| 26 | + |
| 27 | +Codegen is type-blind; it cannot tell from `a == b` whether `a` is `Int` or |
| 28 | +`String`. The fix routes the decision through the type checker, which *does* |
| 29 | +know: |
| 30 | + |
| 31 | +1. *`Typecheck.synth`* records the physical AST node (`List.memq` identity) of |
| 32 | + every `String`-typed operator occurrence into a site list |
| 33 | + (`string_concat_sites` / `string_eq_sites` / `string_rel_sites`). |
| 34 | +2. *`Typecheck.elaborate_string_concat`* (run on the wasm-codegen path only) |
| 35 | + walks the program once and rewrites each recorded `ExprBinary` node into a |
| 36 | + dedicated AST node. |
| 37 | +3. *Codegen* lowers the dedicated node with a real byte-level routine. |
| 38 | + |
| 39 | +This keeps the interpreter and non-wasm backends untouched (they never run the |
| 40 | +elaboration and handle the original `ExprBinary` directly), and it is |
| 41 | +*complete* — variable-to-variable cases are covered because the recording is |
| 42 | +type-directed, not syntactic. |
| 43 | + |
| 44 | +== Slice 9 — `==` / `!=` (`ExprStringEq`) |
| 45 | + |
| 46 | +* Equality is polymorphic (`type_of_binop` gives `'a -> 'a -> Bool`), so a |
| 47 | + `String` `==` lands in `synth`'s general `else` branch; recorded there when |
| 48 | + `repr lhs_ty = TCon "String"`. |
| 49 | +* `ExprStringEq (expr, expr, bool)` — the `bool` is `true` for `!=`. |
| 50 | +* Lowering: length guard, then a byte loop bounded by the (equal) length; `!=` |
| 51 | + negates with `I32Eqz`. The loop runs only after lengths match, so it never |
| 52 | + reads past either string. |
| 53 | + |
| 54 | +== Slice 10 — `<` / `<=` / `>` / `>=` (`ExprStringRel`) |
| 55 | + |
| 56 | +* Relational ops land in `synth`'s `comparison` branch (which already returns |
| 57 | + `Bool` for `String` per #458); recorded there. |
| 58 | +* `ExprStringRel (expr, expr, binary_op)` carries the operator (always one of |
| 59 | + `OpLt`/`OpLe`/`OpGt`/`OpGe`). |
| 60 | +* Lowering: byte-wise *lexicographic* compare — compare the common prefix |
| 61 | + unsigned (`I32LtU`/`I32GtU`), and on a tie the shorter string is smaller; the |
| 62 | + result `cmp ∈ {-1,0,1}` maps onto `cmp <signed-op> 0`. The loop is bounded at |
| 63 | + `min(len_a, len_b)` (via `Select`), so it never reads out of bounds. |
| 64 | + |
| 65 | +== Final hardening |
| 66 | + |
| 67 | +`gen_binop`'s `| OpConcat -> I32Add (* Placeholder *)` arm — a latent landmine |
| 68 | +that would have silently summed two pointers — is now a `failwith` guard. It is |
| 69 | +provably unreachable (string `++` → `ExprStringConcat`/8a-guard; list `++` → |
| 70 | +its own arm; compound-assign maps only `+= -= *= /=`), so the change is pure |
| 71 | +defensive hardening: a regression that ever routed `++` through `gen_binop` |
| 72 | +surfaces as a loud failure instead of a wrong answer. |
| 73 | + |
| 74 | +== Verification |
| 75 | + |
| 76 | +* `test/e2e/fixtures/string_eq.affine`, `string_rel.affine` + the slice-9 / |
| 77 | + slice-10 cases in `test/test_e2e.ml` (compile-after-elaboration). |
| 78 | +* Value checks (out-of-band, via Deno): equality and lexicographic ordering |
| 79 | + verified across decisive-byte, prefix-ordering, empty-string, equality, and |
| 80 | + built-vs-literal cases. |
| 81 | +* No regression: tens of thousands of `Int`-`==`/relational parity cases across |
| 82 | + the idaptik migration corpus pass unchanged (only `String` operands are |
| 83 | + recorded for elaboration; `Int`/`Bool`/`Float` are untouched). |
| 84 | + |
| 85 | +== Status |
| 86 | + |
| 87 | +*The string wall is complete.* `++`, `==`/`!=`, and `<`/`<=`/`>`/`>=` all lower |
| 88 | +correctly on the wasm target. The remaining string surface (interpolation, |
| 89 | +`format`, richer stdlib string functions) is additive, not a correctness wall. |
| 90 | + |
| 91 | +NOTE: the parity harness passes integer arguments only, so brains compiled for |
| 92 | +it remain `Int(...)->Int`; exercising these string ops with real `String`-input |
| 93 | +consumers needs the string/float test-harness extension (separate work item). |
0 commit comments