Float % on x86 is a libcall, and the parity ruling is written down
This commit is contained in:
commit
7db5ec1885
59
FIX.org
59
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.
|
||||
|
||||
28
lib/x86.ml
28
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;
|
||||
(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;
|
||||
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
|
||||
|
||||
@ -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)
|
||||
|
||||
@ -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"
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user