diff --git a/FIX.org b/FIX.org index bc346c3..8822689 100644 --- a/FIX.org +++ b/FIX.org @@ -747,3 +747,62 @@ immutability, and the discipline of planning a shape ahead of time that comes with it. The plan is to write imperative Flan as it stands and see whether the parens still grate once that variable is gone. Revisit this once that evidence exists. + +* The x86 backend tracks LLVM -O0, decided 2026-09-20 +The ruling, in the author's words: the x86 backend must behave as closely to +LLVM at -O0 as possible. A construct LLVM compiles, x86 compiles, and the two +must agree on what the program observably does. The backend is allowed to +refuse a node it does not lower — that is what X86.Unsupported is for and it +is how the survey reports a gap — but a refusal is a bug to be closed, not a +position. "LLVM takes this and x86 does not" is by itself a defect report. + +What made it a ruling was typed float %. emit.ml's prim arm emits frem for Rem +on a float, so (% 7.5 2) compiled under LLVM and printed 1.5; the matching arm +in x86.ml had no float Rem case and died at build time with an unlocated +internal error, "x86: that operator on f64". Dyn % on floats worked on both backends the whole time +— flan_dyn.c's arith implements the fmod identity — so deleting the +annotations made the program build again, which is exactly backwards. x86 is +the dev loop's default backend, which is what turned a backend gap into a +thing the author hit while writing ordinary code. + +Fixed by calling the same function LLVM calls. There is no SSE remainder +instruction and LLVM does not invent one: a frem that reaches the code +generator becomes a call to fmod or fmodf, which objdump shows as a call to +the PLT stub — fourteen of them in a build of the probe whose operands come +through globals, and none at all in one written with float literals, where the +pair is folded to its answer before any call exists. x86.ml now loads the two operands into xmm0 and +xmm1 — already the SysV argument registers — and calls fmod or fmodf by width. +Agreement is then by construction rather than by a second hand-written +identity that would have to get every rounding, every signed zero and every +infinity right on its own. Nothing new had to be arranged for the link: the +prelude already declares both symbols as fmod-f32 and fmod-f64, and every +link passes -lm. + +Rem was the only gap. Walking emit.ml's prim arm against x86.ml's: the whole +float surface is Add, Sub, Mul, Div, Rem and the six comparisons. x86 had four +of the five arithmetic operators and all six comparisons, and the comparisons +match LLVM's ordered predicates — oeq and one are built there from a setcc +against ucomis plus the setnp that rules out the unordered case, which is what +the o in the LLVM predicate means. The bitwise and shift arms are integer-only +on both sides. So nothing else was missing. + +** The aspiration: tests that say x86 still tracks -O0 +Wanted, and half of it exists. @x86 (test/dune:239) is already the diff: it +builds every program in test/programs, spike/x86 and spike/js twice — once +through LLVM, once through --x86 — runs both, and compares stdout, stderr and +the exit status. SURVEY_STRICT makes a DIFFER or a by-name refusal a failing +build. So a corpus program that exercises a construct is already a test that +the two backends agree about it, and the float % cases added to math3.flan are +in that set by being in test/programs. + +What @x86 does not do is pin the LLVM side at -O0. It builds both sides at the +default -O2, so a construct LLVM folds at compile time — a % over two float +literals is one: that build contains no fmod call — is compared as a constant +against the x86 backend's actual lowering. The float % block in math3.flan +goes through globals for that reason, the same reason arith.flan gives for its +own. Two things would close the rest of the gap: an -O0 pass of the sweep, so +the LLVM side emits the calls and branches rather than the answers — the +script already has SURVEY_FLAGS, which hands the same extra flags to both +sides, and both sides do accept -O0 — and something that walks the two prim +match arms mechanically rather than relying on somebody reading them side by +side, which is how this gap survived. Neither is queued. diff --git a/lib/x86.ml b/lib/x86.ml index 5bba15c..51439f5 100644 --- a/lib/x86.ml +++ b/lib/x86.ml @@ -2767,13 +2767,39 @@ and prim f (e : Tast.expr) (p : Tast.prim) (args : Tast.expr list) dst = let f64 = f64_of t in fload f.b ~dst:xmm0 ~mm:(lmem f la ~scratch:r11) ~f64; fload f.b ~dst:1 ~mm:(lmem f lb ~scratch:r11) ~f64; - let op = - match p with - | Tast.Add -> 0x58 | Tast.Sub -> 0x5c - | Tast.Mul -> 0x59 | Tast.Div -> 0x5e - | _ -> unsupported "that operator on %s" (Types.to_string t) - in - farith f.b ~op ~f64 ~dst:xmm0 ~src:1; + (match p with + (* There is no SSE remainder instruction, and LLVM does not pretend + otherwise: it lowers a [frem] that reaches the code generator to a + call to C's [fmod] or [fmodf], which is what `objdump -d` shows as a + [call fmod@plt] in a build whose operands come through globals. A + [%] over two float literals is folded on the way and contains no + call at all, which is why the corpus block that covers this uses + globals — a folded answer is evidence about the folder. + + Calling the same function is what makes the two backends agree by + construction + rather than by a hand-written identity that would have to get every + rounding, every sign of zero and every infinity right on its own. + The prelude already declares both symbols ([fmod-f32], + [fmod-f64]) and every link passes -lm, so nothing new has to be + arranged for the call to resolve. + + The two operands are already in xmm0 and xmm1, which are exactly + where SysV wants the arguments of [double fmod(double, double)], + and the result comes back in xmm0, which is where the store below + reads it. [rax] carries the count of SSE argument registers, the + same thing [call_c] puts there: a fixed-arity callee ignores it. *) + | Tast.Rem -> + imm_into f ~reg:rax 2L; + call_sym f.b (if f64 then "fmod" else "fmodf") + | _ -> + let op = + match p with + | Tast.Add -> 0x58 | Tast.Sub -> 0x5c + | Tast.Mul -> 0x59 | Tast.Div -> 0x5e + | _ -> unsupported "that operator on %s" (Types.to_string t) + in + farith f.b ~op ~f64 ~dst:xmm0 ~src:1); fstore f.b ~src:xmm0 ~mm:(lmem f dst ~scratch:r11) ~f64 end else begin let signed = signed_of t in diff --git a/test/programs/math3.flan b/test/programs/math3.flan index 7f8a381..3b8e8ac 100644 --- a/test/programs/math3.flan +++ b/test/programs/math3.flan @@ -19,6 +19,19 @@ (print x) (print " ")) +;;; The operands of the (% ...) block at the end. See the note there for why +;;; they are globals. +(defvar rem-a f64 7.5) +(defvar rem-na f64 -7.5) +(defvar rem-b f64 2.0) +(defvar rem-nb f64 -2.0) +(defvar rem-z f64 0.0) +(defvar rem-huge f64 1e300) +(defvar rem-a32 f32 7.5) +(defvar rem-na32 f32 -7.5) +(defvar rem-b32 f32 2.0) +(defvar rem-z32 f32 0.0) + (defn main [] i32 ;; The f32 half. tan, the three inverses, the three logarithms and exp. (show (tan-f32 0.0)) ; 0 @@ -89,4 +102,34 @@ ;; pi is the one value here that can be pinned without pinning a libm: it is ;; a literal the compiler rounds, so it is the same on every target. (println (and (> pi-f64 3.14159265) (< pi-f64 3.14159266))) + + ;; The operator spelling of the same function. A typed float (% x y) is + ;; fmod: LLVM lowers it to `frem`, which at -O0 becomes a call to fmod or + ;; fmodf, and the x86 backend calls the same two symbols. Everything here + ;; comes through a global rather than a literal for the reason arith.flan + ;; gives — a literal pair is folded before either backend sees an operator, + ;; and the folded answer would be evidence about the constant folder and + ;; not about the lowering. + ;; + ;; The four signs are the first line, because that is where a modulo + ;; written in place of a remainder disagrees: the sign follows the + ;; dividend. The second line is the two answers IEEE defines where an + ;; integer % would have died — a zero divisor and a NaN dividend are both + ;; NaN, not a signal. + (show64 (% rem-a rem-b)) ; 1.5 + (show64 (% rem-na rem-b)) ; -1.5 + (show64 (% rem-a rem-nb)) ; 1.5 + (show64 (% rem-na rem-nb)) ; -1.5 + (show (% rem-a32 rem-b32)) ; 1.5 + (show (% rem-na32 rem-b32)) ; -1.5 + (println "") + + (show64 (% rem-a rem-z)) ; nan + (show64 (% (/ rem-z rem-z) rem-b)) ; nan + (show (% rem-a32 rem-z32)) ; nan + ;; A quotient past anything an integer could name, which is where a + ;; remainder written as x - trunc(x/y)*y has nothing left to truncate. + (show64 (% rem-huge rem-b)) ; 0 + (show64 (% rem-b rem-huge)) ; 2 + (println "") 0) diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index 6037878..46f4fc2 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -542,7 +542,9 @@ let () = 0 10 2 1 1024 3 5 2 1.5 \n\ -3 -2 -3 3 \n\ 7 7 7 true true\n\ - true\n" + true\n\ + 1.5 -1.5 1.5 -1.5 1.5 -1.5 \n\ + nan nan nan 0 2 \n" in outputs "the rest of libm, both widths" "programs/math3.flan" math3_out; outputs ~opt:"-O0" "the rest of libm, both widths, -O0"