Review follow-ups: the default's payload, four wrong reasons, a doubled prefix
1. The bare (dead-beef) built its default with Int64.of_int32, which sign-extends 0xDEADBEEF to -559038737 on a node tagged u32 — where the spelled-out literal arrives as 3735928559, because in_range admits it as the unsigned value it is. Masked to 32 bits, so the two spellings really do carry one payload; verified by diffing the emitted bodies of (dead-beef) and (dead-beef 0xDEADBEEF), which are now identical instruction for instruction. 2. The refusal's catch-all told a union and a function value that they 'carry a tag that names a case'. Neither does: env.unions is the untagged unions, and an Fn is a code address. Split into one arm per reason — union, Fn, enum, Option, data type — and each is now pinned, so they cannot quietly re-merge. Same correction in FIX.org's bullet. 3. js.ml prefixed its own message with 'js: ', which bin/main.ml prepends too, giving 'js: js: ...'. Dropped, and the message now names the builtin it refuses, which its comment already claimed it did. 4. FIX.org said x86.ml reads both pattern helpers out of Emit. It reads only word_of_pattern; the tail walks rax with shr.
This commit is contained in:
parent
3c39354833
commit
2240100ee9
35
FIX.org
35
FIX.org
@ -1689,9 +1689,18 @@ this rule exists and ~zeroed~ needs none:
|
||||
one and true on the other. Byte-identical behaviour across the two backends
|
||||
is the property this feature is pinned on, so the divergence is refused
|
||||
rather than documented.
|
||||
- *enum, data type, union, Option, function value* — each carries a tag or a
|
||||
case index something later reads as a small number with a meaning, and no
|
||||
byte pattern names a real case.
|
||||
- *a data type* — a tag that names a case, and no byte pattern names a real
|
||||
one. *An ~(Option T)~* — the same, one bit of it: a filled tag says the
|
||||
value is there over a payload nobody wrote. *An enum* — its values are the
|
||||
members it declared, and no byte pattern is one of them.
|
||||
- *a union* — and this one is not about a tag, because ~env.unions~ is "the
|
||||
untagged unions". It is that a union's members overlay and ~unfillable~
|
||||
walks a struct's fields rather than a union's members, so nothing has
|
||||
shown every member is plain data; a member that is not would be filled
|
||||
through the one that is. Relaxable by walking the members, if anyone wants
|
||||
it.
|
||||
- *a function value* — a code address, and a call through a filled one jumps
|
||||
into whatever the pattern happens to address.
|
||||
|
||||
Floats are in: every bit pattern is a float, NaNs included, and both backends
|
||||
move one as bytes.
|
||||
@ -1710,10 +1719,15 @@ both arities.
|
||||
On a little-endian machine the word a 4-byte store must therefore leave is
|
||||
the *byte reversal* of the pattern, which is all ~Emit.word_of_pattern~ is
|
||||
(~bytes_of_pattern~ beside it is the ascending list). Those two are the one
|
||||
place the order is written; x86.ml reads them out of Emit rather than
|
||||
repeating them, and ~Tast.dead_beef_default~ is the one place 0xDEADBEEF is
|
||||
written. Three definitions, no duplicates, so the default and the
|
||||
parameterised case cannot drift.
|
||||
place the order is written, and ~Tast.dead_beef_default~ is the one place
|
||||
0xDEADBEEF is written, so the default and the parameterised case cannot
|
||||
drift.
|
||||
|
||||
x86.ml reads ~word_of_pattern~ out of Emit rather than repeating it. It does
|
||||
*not* use ~bytes_of_pattern~: its tail walks the bytes out of ~rax~ with
|
||||
~shr~, which is the same arithmetic the list encodes and is how the computed
|
||||
path has to do it anyway, so there was no second constant to share. emit.ml
|
||||
uses both — the list for a folded tail, the word for the loop.
|
||||
|
||||
A literal pattern is reversed at compile time and reaches the loop as an
|
||||
immediate — the default's generated code is exactly what it was before the
|
||||
@ -1765,9 +1779,10 @@ byte-identical, with a fourth build (~--dev~) added at the rename: four-way
|
||||
identical. The three rows were confirmed to actually run, by breaking one
|
||||
expectation on purpose and watching all three report. Seventeen checker rows
|
||||
in ~test_flan.ml~: four accepting (both ~dead-beef~ arities and a computed
|
||||
pattern among them), and thirteen refusals covering the boundary, both
|
||||
arities, both no-expected-type positions, the byte's range, the pattern's
|
||||
range and the ~defconst~ rule.
|
||||
pattern among them), and seventeen refusals covering the boundary — one per
|
||||
reason, since review found the tagged types were sharing a line that was
|
||||
false for two of them — both arities, both no-expected-type positions, the
|
||||
byte's range, the pattern's range and the ~defconst~ rule.
|
||||
|
||||
~dune test~ exits 1 on this branch roughly half the time, with *no FAIL line
|
||||
anywhere* — the ~Flan.Wire.Closed~ flake an earlier lane wrote up further up
|
||||
|
||||
41
lib/check.ml
41
lib/check.ml
@ -4921,8 +4921,29 @@ and named_call ctx ~want loc name args =
|
||||
"a bool is an i1 to LLVM and a whole byte to the x86 backend, \
|
||||
so a filled one would not even agree with itself across the \
|
||||
two"
|
||||
| _ -> "it carries a tag that names a case, and no byte pattern \
|
||||
names a real one")
|
||||
| Types.Option _ ->
|
||||
"it carries a tag saying whether the value is there, and a \
|
||||
filled one says yes over a payload nobody wrote"
|
||||
| Types.Fn _ ->
|
||||
"it is a code address, and a call through a filled one jumps \
|
||||
into whatever 0xDE bytes happen to address"
|
||||
| Types.Named n when Hashtbl.mem ctx.env.datas n ->
|
||||
"it carries a tag that names a case, and no byte pattern \
|
||||
names a real one"
|
||||
| Types.Named n when Hashtbl.mem ctx.env.unions n ->
|
||||
(* Untagged, per [env.unions]'s own note — so the reason is
|
||||
not a tag. It is that a union's members overlay, and this
|
||||
rule walks a struct's fields rather than a union's members:
|
||||
nothing here has shown they are all plain data, and a
|
||||
member that is not would be filled through the one that
|
||||
is. *)
|
||||
"a union's members overlay, and this rule does not walk them \
|
||||
— so nothing here has shown that every member is plain data"
|
||||
| Types.Enum _ ->
|
||||
"an enum's values are the members it declared, and no byte \
|
||||
pattern is one of them"
|
||||
| _ ->
|
||||
"it is not one of the types this rule admits")
|
||||
| None -> ());
|
||||
if is_byte then
|
||||
let b = check ctx ~want:(Types.Int Types.U8) (List.hd args) in
|
||||
@ -4934,10 +4955,22 @@ and named_call ctx ~want loc name args =
|
||||
(* The bare form, written out. Not a default a backend applies:
|
||||
the node that leaves here is the one the spelled-out call would
|
||||
have left, which is what makes the equivalence a fact about the
|
||||
IR rather than a promise two emitters keep separately. *)
|
||||
IR rather than a promise two emitters keep separately.
|
||||
|
||||
Masked to 32 bits, and that is the whole of why this is not
|
||||
[Int64.of_int32] on its own: [dead_beef_default] is an [int32]
|
||||
whose top bit is set, so widening it signed would put
|
||||
-559038737 on a node tagged [u32] — where the same pattern
|
||||
*written out* arrives as 3735928559, because [in_range] admits
|
||||
it as the unsigned value it is. Two spellings of one builtin
|
||||
would then carry two different payloads, and "the same node by
|
||||
construction" would be false for anything that reads one. *)
|
||||
| _ ->
|
||||
mk loc (Types.Int Types.U32)
|
||||
(Tast.Int (Int64.of_int32 Tast.dead_beef_default, Types.U32))
|
||||
(Tast.Int
|
||||
(Int64.logand
|
||||
(Int64.of_int32 Tast.dead_beef_default) 0xFFFFFFFFL,
|
||||
Types.U32))
|
||||
in
|
||||
mk loc ty (Tast.DeadBeef (ty, pat))
|
||||
| _ ->
|
||||
|
||||
14
lib/js.ml
14
lib/js.ml
@ -673,11 +673,19 @@ let rec value f (e : Tast.expr) : string =
|
||||
(* A fill is a byte pattern written over storage, and this backend has no
|
||||
storage to write over: a Flan struct is a JS object here, not a run of
|
||||
bytes, so there is nothing for 0xFF or DEADBEEF to mean. Refused by name
|
||||
rather than approximated, which is this file's rule. *)
|
||||
rather than approximated, which is this file's rule.
|
||||
|
||||
No "js: " on the front — [bin/main.ml] puts it there when it prints an
|
||||
[Unsupported], and every other refusal in this file leaves it to do
|
||||
that. *)
|
||||
| Tast.Fill _ | Tast.DeadBeef _ ->
|
||||
unsupported
|
||||
"js: a byte fill has no meaning on this backend — a struct is an \
|
||||
object here and not a run of bytes"
|
||||
"%s writes a byte pattern over storage, and the JS dialect has no \
|
||||
storage to write it over — a struct is an object here, not a run of \
|
||||
bytes"
|
||||
(match e.Tast.e with
|
||||
| Tast.Fill _ -> "(filled b)"
|
||||
| _ -> "(dead-beef)")
|
||||
(* [uninit] is the opt-out from zeroing. There is no uninitialised memory
|
||||
here to opt out of, so it is the zero — which is more than the program
|
||||
asked for and never less. *)
|
||||
|
||||
@ -2001,6 +2001,25 @@ let () =
|
||||
rejects_check "a bool cannot be filled"
|
||||
"(defn f [] () (let [b false] (set b (filled 0xFF))))"
|
||||
~needle:"would not even agree with itself";
|
||||
(* Each of the tagged and address-carrying types names its own reason. They
|
||||
shared one "it carries a tag that names a case" line until review caught
|
||||
that it was false for two of them — a union is untagged (env.unions is
|
||||
"the untagged unions") and a function value is a code pointer, not a
|
||||
tag. Pinned per type so the reasons cannot quietly re-merge. *)
|
||||
rejects_check "a union cannot be filled, and not because of a tag"
|
||||
"(defunion U [a i32 b f64]) \
|
||||
(defn f [] () (let [u (U {})] (set u (dead-beef))))"
|
||||
~needle:"a union's members overlay";
|
||||
rejects_check "a function value cannot be filled"
|
||||
"(defn g [] ()) (defn f [] () (let [h g] (set h (dead-beef))))"
|
||||
~needle:"it is a code address";
|
||||
rejects_check "an enum cannot be filled"
|
||||
"(defenum K [lo 0 hi 1]) \
|
||||
(defn f [k K] () (let [e k] (set e (dead-beef))))"
|
||||
~needle:"the members it declared";
|
||||
rejects_check "an Option cannot be filled"
|
||||
"(defn f [] () (let [o (Some 1)] (set o (dead-beef))))"
|
||||
~needle:"whether the value is there";
|
||||
(* A data type's tag is a case index, and no byte pattern names a real
|
||||
case. The type itself is what the message names, because a data type
|
||||
overlays its cases. *)
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user