From 37d94ed66f775f2d8100c1ed0ad3838f7bfd91bd Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Mon, 14 Sep 2026 08:25:24 +0700 Subject: [PATCH] The pointer arm agrees promised, and the comment stops promising it --- lib/cimport.ml | 110 +++++++++++++++++++++++++++++++++++++----- test/headers/sample.h | 10 ++++ test/test_flan.ml | 51 ++++++++++++++++++++ 3 files changed, 160 insertions(+), 11 deletions(-) diff --git a/lib/cimport.ml b/lib/cimport.ml index 4f8c2e1..f1f5ca7 100644 --- a/lib/cimport.ml +++ b/lib/cimport.ml @@ -856,6 +856,78 @@ let agrees env (a : Ast.texpr) (b : Ast.texpr) = || (enum_like env a && int32_like nb) || (enum_like env b && int32_like na) +(* ── A hand-written pointer, against the pointer the header spells ── + + The second tolerance, and the one [agrees] cannot express on its own. By the + time a C parameter has become a Flan type, what the header actually said + about it is gone: [param_ty] renders [const char *] as [string] and + [value_ty] renders [void *] as [(Ptr u8)], and both of those are the + importer's own choice rather than the header's word. A hand-written line + that says [(Ptr u8)] over a [const char *] is not disagreeing with the + header — it is disagreeing with a rendering — so the comparison has to be + made against the C spelling, which is why this takes the string and [agrees] + does not. + + It is consulted only from the [declare-c] check below, never from + [check_structs]. A struct field is about *layout*, and every pointer in a + struct is one word whatever it points at, so the element type is not the + thing that check is for; widening it there would buy nothing and would cost + the width discipline the field check exists to keep. + + The [i8]/[u8] tolerance likewise lives here and not in [agrees]. Inside a + pointer, [char] and [unsigned char] are two spellings of one byte and the + package uses [(Ptr u8)] for both — [Image.data] is [void *] in the header. + As a *field* or a *scalar* they are still a real disagreement and [agrees] + goes on saying so. *) + +let byte s = String.equal s "i8" || String.equal s "u8" + +(* [const int *] → [Some "const int"]. Anything that is not a pointer, [None]. + Only the outermost [*] comes off, so [void **] arrives here as a pointer to + [void *], which is a pointer to something and not a [void *]. *) +let c_pointee (s : string) : string option = + let s = String.trim s in + if String.length s > 0 && s.[String.length s - 1] = '*' then + Some (String.trim (String.sub s 0 (String.length s - 1))) + else None + +let ptr_agrees env ~(c : string) (t : Ast.texpr) = + match (c_pointee c, t.Ast.t) with + | Some inner, Ast.Tapp ("Ptr", [ elem ]) -> + (* [void *] agrees with a pointer to anything, and this is the judgement + call of the arm. C's [void *] is opaque about *what it points at* — that + is the whole of what the spelling means — so there is no element type in + the header to disagree with, and a check that reported one would be + reporting [value_ty]'s guess of [u8] back at the author as if the header + had said it. What is *not* given up is that it is a pointer at all: the + match above requires [(Ptr _)] on the Flan side, so an [i32] or a + [string] declared against a [void *] is still a finding. That + asymmetry is the point — raylib spells thirty-odd parameters [void *] + and none of them is a scalar. *) + let b = bare inner in + if String.equal b "void" then true + else ( + match (try Some (value_ty env inner) with Refused _ -> None) with + | None -> + (* A pointee this cannot render says nothing, exactly as an + unrenderable field type says nothing in [check_structs]. *) + false + | Some want -> + let a = ty_source want and b = ty_source elem in + (* [agrees] and not [String.equal], so a [(Ptr Key)] against the + header's [(Ptr int)] lands on the enum arm. The four bytes are the + same four bytes through a pointer as they are beside one. *) + agrees env want elem || (byte a && byte b)) + | _ -> false + +(* The two together, for the one caller that still has the C spelling. A + [(Ptr A)] against a [B *] for unrelated named [A] and [B] falls through + both and stays a finding: two structs of the same size are still two + different structs, and a binding that says the wrong one reads a + plausible picture out of the wrong offsets. *) +let agrees_c env ~(c : string) (want : Ast.texpr) (got : Ast.texpr) = + agrees env want got || ptr_agrees env ~c got + let check_structs ~env ~(structs : (string * Ast.field list) list) (d : dump) = let record n = match List.find_opt (fun r -> r.rname = n) d.records with @@ -1291,22 +1363,38 @@ let decl_source (d : Ast.decl) = (* ── A hand-written binding, against the header's own signature ────── *) (* The other half of closing the trusted gap, and the one that pays off - immediately: [vendor/raylib] carries 176 [declare-c] lines that were - transcribed by hand from raylib's documentation, and until now nothing could - say whether any of them was right. This says so, one at a time. + immediately: every [declare-c] line in [vendor/raylib] was transcribed by + hand from raylib's documentation, and until this nothing could say whether + any of them was right. This says so, one at a time. (There is no count here + on purpose. The last one written down said 176 when there were 196, which is + the only thing a hand-maintained census of a growing file ever does.) - Compared as *rendered Flan types*, not as C spellings, because the two sides - are not written in the same language and only the Flan rendering is - commensurable. Three differences are expected and are not reported: + Compared as *rendered Flan types* wherever the rendering is the whole story, + and against the C spelling where it is not. Three differences are expected + and are not reported, and all three are now implemented rather than + promised: - the Flan name. [IsKeyPressed] is [key-pressed?] by hand and [is-key-pressed] by rule, and the hand-written one is better. The C symbol is what identifies the function here, not the name. - an enum parameter. The header says [KeyboardKey] and the importer has no way to know the package calls that [Key], so it says [i32]; the - hand-written [Key] is the same int with a better face. + hand-written [Key] is the same int with a better face. That is [agrees]. - a [(Ptr T)] where the header says [T *] and the hand-written line chose - something more specific for a reason it recorded. + something more specific for a reason it recorded. That is [ptr_agrees], + and it needs the C spelling because the rendering has already thrown the + answer away: [param_ty] turns [const char *] into [string] and [value_ty] + turns [void *] into [(Ptr u8)], neither of which is what the header said. + [(Ptr u8)] over a [char *], and [(Ptr] anything[)] over a [void *], now + agree; [(Ptr A)] over a [B *] does not. + + What [const] does here, since the arm above says nothing about it: nothing, + and the reason is worth knowing because it is invisible. A non-const + [char *] parameter makes [param_ty] *refuse*, and the [| None -> None] below + 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 pointer arm exists for. What is left after those is a real disagreement about a width, an arity or a direction — which is exactly the class of bug docs/BUILT.md warns about, where @@ -1331,7 +1419,7 @@ let diff_bound ~env ~(bound : (Ast.fn * string) list) (d : dump) = integer is the expected difference and not a finding, and an enum against anything else still is one. *) let norm (t : Ast.texpr) = ty_source t in - let same a b = agrees env a b in + let same ~c a b = agrees_c env ~c a b in if c.cvariadic then None else if List.length fn.Ast.params <> List.length c.cparams then say @@ -1345,7 +1433,7 @@ let diff_bound ~env ~(bound : (Ast.fn * string) list) (d : dump) = match (try Some (param_ty env ct) with Refused _ -> None) with | None -> None | Some want -> - if same want p.Ast.fty then None + if same ~c:ct want p.Ast.fty then None else Some (Printf.sprintf "parameter %s is %s and the header says %s (%s)" @@ -1361,7 +1449,7 @@ let diff_bound ~env ~(bound : (Ast.fn * string) list) (d : dump) = let agrees = match (want, fn.Ast.ret) with | None, None -> true - | Some a, Some b -> same a b + | Some a, Some b -> same ~c:c.cret a b | _ -> false in if agrees then None diff --git a/test/headers/sample.h b/test/headers/sample.h index a006ebb..e578c86 100644 --- a/test/headers/sample.h +++ b/test/headers/sample.h @@ -59,6 +59,16 @@ Pair point_of(Point p); /* the second typedef name */ int mood_value(Mood m); /* a C enum is an int */ void take_nothing(void); +/* The pointer arm of the declare-c check, which compares against the C + * spelling because the rendering has thrown the answer away. blit's two + * parameters are void *, which is opaque about what it points at and so + * agrees with a pointer to anything; scratch is the same question in return + * position. pair_len_p is a pointer to a *named* type, which is what has to go + * on being refused when a hand-written line names a different one. */ +void blit(void *dst, const void *src, int n); +void *scratch(int n); +float pair_len_p(const Pair *p); + /* --- refused, one per reason --- */ const char *name_of(int which); /* returns char * */ void fill_buffer(char *out, int cap); /* non-const char *: C writes it */ diff --git a/test/test_flan.ml b/test/test_flan.ml index 84c1c12..ce15c6c 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -1910,6 +1910,57 @@ let () = ~bound:(bound_of "(declare-c mv [m Mood] i32 \"mood_value\")") dump = []); + (* The pointer arm. The importer renders a C pointer into whichever Flan type + it thinks is the nicest face — [const char *] becomes [string], [void *] + becomes [(Ptr u8)] — and a hand-written line that wants the raw address + instead is disagreeing with that choice rather than with the header. These + say which of those disagreements are real. *) + let agreed name src = + check ("declare-c against the header: " ^ name) + (Cimport.diff_bound ~env ~bound:(bound_of src) dump = []) + in + (* The case docs/PORTING.md §A.1 could not write: GetCodepointPrevious reads + backwards from its pointer, so a Flan string — which crosses as a + NUL-terminated copy — is the one thing it must not be handed. *) + agreed "a (Ptr u8) where the header says const char *" + "(declare-c name-length [text (Ptr u8)] i32 \"name_length\")"; + (* And the string face goes on being right, because this is an addition. *) + agreed "a string where the header says const char *" + "(declare-c name-length [text string] i32 \"name_length\")"; + agreed "a pointer that matches the header exactly" + "(declare-c count-at [values (Ptr i32) n i32] i32 \"count_at\")"; + (* void * is opaque about what it points at, so there is no element type in + the header to disagree with — §A.2's LoadImageColors → UpdateTexture. *) + agreed "any pointer where the header says void *" + "(declare-c blit [dst (Ptr Pair) src (Ptr Shade) n i32] \"blit\")"; + agreed "any pointer where the header returns void *" + "(declare-c scratch [n i32] (Ptr Pair) \"scratch\")"; + (* An enum through a pointer is the same four bytes an enum is beside one. *) + agreed "a (Ptr enum) where the header says a pointer to int" + "(declare-c count-at [values (Ptr Mood) n i32] i32 \"count_at\")"; + + (* And the refusals, which are the whole value of the arm: a binding that + lies about the header still has to be caught, and the message still has to + name the disagreement. *) + differs "a pointer to the wrong named type" + "(declare-c pair-len-p [p (Ptr Shade)] f32 \"pair_len_p\")" + "parameter p is (Ptr Shade) and the header says (Ptr Pair)"; + differs "a pointer to the wrong width" + "(declare-c count-at [values (Ptr f64) n i32] i32 \"count_at\")" + "parameter values is (Ptr f64)"; + (* void * gives up the element type and nothing else. It is still a pointer, + and a scalar declared against one is still a finding. *) + differs "a scalar where the header says void *" + "(declare-c blit [dst i64 src (Ptr u8) n i32] \"blit\")" + "parameter dst is i64"; + differs "a scalar where the header says a pointer" + "(declare-c count-at [values i32 n i32] i32 \"count_at\")" + "parameter values is i32"; + (* The byte tolerance is the pointee's and not the world's: inside a pointer + i8 and u8 are two spellings of one byte, and as a scalar they are not. *) + differs "a byte where the header says a wider integer" + "(declare-c add [a u8 b i32] i32 \"add_ints\")" "parameter a is u8"; + (* The name rule. Reversibility is by storage — the C symbol is kept verbatim in the declaration — so what the rule has to be is injective over one header, which the collision case above asserts. These pin its shape. *)