139 lines
8.3 KiB
Markdown
139 lines
8.3 KiB
Markdown
# Handoff — the pointer arm `agrees` already promised
|
|
|
|
`lib/cimport.ml`'s `agrees` decides whether a hand-written `declare-c` and the C header
|
|
say the same thing. Its comment had always listed three differences that are "expected and
|
|
are not reported"; the code implemented two of them. The missing one — *a `(Ptr T)` where
|
|
the header says `T *`* — is what `../PORTING.md` §A.1 and §A.2 ran into, and it is why
|
|
`GetCodepointPrevious` could not be bound honestly and why `UpdateTexture` had to be handed
|
|
`(addr (.r (at (slice-from-ptr pixels n) 0)))`.
|
|
|
|
The arm is built. This file is the record of what it accepts, what it still refuses, and
|
|
the one thing that turned out not to be its fault.
|
|
|
|
## What the arm is
|
|
|
|
`ptr_agrees` and `agrees_c` beside `agrees` in `lib/cimport.ml`, consulted only from the
|
|
two `declare-c` sites in `diff_bound`. It takes the **C spelling** and not only the
|
|
rendered Flan type, because by the time a parameter has been rendered the header's word is
|
|
gone: `param_ty` turns `const char *` into `string` and `value_ty` turns `void *` into
|
|
`(Ptr u8)`, and neither of those is what the header said. A hand-written line that
|
|
disagrees with a rendering is not disagreeing with the header, and that distinction is the
|
|
whole of the arm.
|
|
|
|
`agrees` itself is untouched. `check_structs` uses it for field **widths**, and a struct
|
|
field is about layout — every pointer in a struct is one word whatever it points at — so
|
|
widening it there would buy nothing and would cost the discipline the field check exists
|
|
to keep.
|
|
|
|
## What it accepts
|
|
|
|
- `(Ptr T)` against a C `T *` for the same `T`.
|
|
- `(Ptr u8)` against `char *` and `const char *`. Inside a pointer, `char` and
|
|
`unsigned char` are two spellings of one byte and the package uses `(Ptr u8)` for both.
|
|
The `i8`/`u8` tolerance is the **pointee's** and not the world's; as a scalar or a field
|
|
the two are still a real disagreement, and there is a test for that.
|
|
- `(Ptr T)` for **any** `T` against `void *` and `const void *`. This is the judgement
|
|
call and the reason is sharper than "it is opaque": `value_ty` *invents* the `(Ptr u8)`
|
|
it renders a `void *` as, so the check without this arm was enforcing cimport's own guess
|
|
as if the header had said it. What is **not** given up is that it is a pointer at all —
|
|
the Flan side must still be a `(Ptr _)`, so an `i32` or a `string` declared against a
|
|
`void *` is still a finding. raylib spells thirty-odd parameters `void *` and none of
|
|
them is a scalar.
|
|
- `(Ptr Key)` against a header's `int *`, through the existing enum arm. The same four
|
|
bytes through a pointer as beside one.
|
|
|
|
## What it refuses
|
|
|
|
- `(Ptr A)` against `B *` for different named `A` and `B`. Two structs of the same size
|
|
are still two different structs.
|
|
- Anything that is not a pointer on the Flan side against a C pointer, `void *` included.
|
|
- Everything `agrees` already refused, unchanged.
|
|
|
|
## What `const` does here: nothing, and the reason is invisible
|
|
|
|
Worth writing down because reading the code does not show it. A non-const `char *`
|
|
parameter makes `param_ty` **refuse**, and `diff_bound`'s `| None -> None` means a
|
|
parameter the importer cannot render at all is *skipped rather than compared*. So a
|
|
hand-written `(Ptr u8)` over a `char *` has always passed — unexamined, not approved. Only
|
|
`const char *` ever reaches the comparison, and that is the case the arm exists for. The
|
|
rewritten comment at the head of `diff_bound` now says so.
|
|
|
|
## The comment at `lib/cimport.ml:1291`
|
|
|
|
Rewritten from a promise into a description. The count it carried — "176 `declare-c`
|
|
lines", twenty short on the day it was read — is gone rather than corrected, and both
|
|
comments now name the `grep` that answers the question instead of recording an answer that
|
|
goes stale. `vendor/raylib/headers` carried the same rot, "425 declarations … 172
|
|
hand-written", and got the same treatment. Neither file states a number any more.
|
|
|
|
## Then it was used
|
|
|
|
**§A.1 came out entirely, and it is the arm's own case.**
|
|
`vendor/raylib/raylib.flan` has `get-codepoint-previous-raw` — `(Ptr u8)` over a
|
|
`const char *`, which is precisely what the arm was missing — and a `get-codepoint-previous`
|
|
wrapper that takes the bytes and an offset and builds the interior pointer itself.
|
|
`generated.flan` no longer carries the `string`-faced version: a binding that is wrong for
|
|
the only direction it reads in is worse than no binding, and the hand-written declaration
|
|
suppresses the generated one by C symbol. `examples/text-codepoints-loading.flan`'s
|
|
`step-back` is one call to it; the continuation-byte walk and `continuation?` are deleted.
|
|
The answer is 12356 and 3, verified by running it.
|
|
|
|
`test/programs/raylib-codepoints.flan` would have caught the old answer, verified by
|
|
perturbation rather than by argument: make `step-back` set `size` to 0 — which is exactly
|
|
what the broken string call produced — and both rows go red, because the backward walk
|
|
never reaches offset 0 and runs off the end of its array.
|
|
|
|
**§A.2's call site came out; the cast moved rather than vanished.** The header check does
|
|
accept the `(Ptr Color)` binding now. What the header check was masking is that
|
|
`lib/shim.ml:651` refuses a second `declare-c` for a C symbol the package already binds,
|
|
and that rule is right: a shim emits one C prototype per declaration, and two prototypes
|
|
for `UpdateTexture` that disagree about a parameter type is a C file that does not compile.
|
|
Its message says what to write instead — "another Flan name for it is a defn" — so
|
|
`raylib.flan` has `update-texture-colors`, a one-line defn over the generated
|
|
`update-texture`:
|
|
|
|
```flan
|
|
(defn update-texture-colors [texture Texture2D pixels (Ptr Color)] ()
|
|
(update-texture texture (addr (.r pixels))))
|
|
```
|
|
|
|
The `(Ptr u8)` face has to stay the declared one, because `(.data im-copy)` is already a
|
|
`(Ptr u8)` over the same bytes and `(Ptr u8)` → `(Ptr Color)` is the direction the language
|
|
cannot write. `(addr (.r pixels))` was checked against the bytes rather than reasoned
|
|
about: a `gen-image-color 2 1 red` through `load-image-colors`, read back through the `u8`
|
|
pointer, gives 230 41 55 255. So the honest statement is that §A.2 is half closed — the
|
|
example reads `(rl/update-texture-colors texture pixels)`, the cast exists once with a name
|
|
and a comment on it instead of once per call site, and the general gap the section is
|
|
actually about is a **pointer reinterpretation**, which is not a checker arm.
|
|
|
|
## Verification
|
|
|
|
- `dune build --root .` and `dune test --root .` clean; the dev suite is 232 checks, 0
|
|
failures, unchanged — the new checks are in `test_flan.ml`, which reports pass/fail
|
|
rather than a count.
|
|
- New checks in `test/test_flan.ml` over three new functions in `test/headers/sample.h`
|
|
(`blit`, `scratch`, `pair_len_p`): six declarations that must agree, five that must
|
|
still be reported, each asserting on the message and not on a count. All of them were
|
|
confirmed live by breaking `ptr_agrees` in three different directions and watching the
|
|
right subset go red — the negatives matter most, and they are why the arm can be widened
|
|
without the check becoming decoration.
|
|
- The raylib acceptance cases ran rather than skipped (`ldconfig` finds
|
|
`libraylib.so.550`); the only "skipping" line in the whole run is the web one, which
|
|
wants a wasm build of raylib that is not in this tree.
|
|
- `flan generate-c vendor/raylib` completes, which is itself the check: it compares every
|
|
`defstruct`, every hand-written `declare-c` and every mapped constant against
|
|
`raylib-5.5.h` and refuses to write when they disagree.
|
|
- `bash web/examples/check.sh` green.
|
|
- `spike/x86/survey.sh` on the finished tree: **103 MATCH, 0 DIFFER, 0 REFUSED** (38 skip
|
|
— 28 that do not compile on purpose, 8 with no main, 2 that run forever). Expected
|
|
rather than surprising: nothing here is below the IR, and the one surveyed program that
|
|
changed is `test/programs/raylib-codepoints.flan`. Run it detached — `setsid timeout
|
|
2400 spike/x86/survey.sh > log 2>&1 </dev/null` — because a foreground run takes the
|
|
signal sent to its process group and returns a spurious 143.
|
|
|
|
## Still open
|
|
|
|
- A pointer reinterpretation in the language. `(addr (.r p))` works when the first field
|
|
is the type you want and there is no general form of it. This is §A.2's real subject.
|
|
- Nothing else. The three differences the comment lists are now all three implemented.
|