From 9700eeafb48b1d9ccfb07ee4b4b5bf23fd310d4d Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Fri, 11 Sep 2026 19:35:19 +0700 Subject: [PATCH] Images, because pixels in RAM are what a headless test can argue with MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Every other struct in the package is handed to raylib and handed back, and that proves nothing: store-and-return is symmetric, so C writes and reads the same wrong slots for any field order. An Image is different. raylib computes with it, and two computations answer differently per axis. gen-image-color takes two scalars and returns a struct reading 4, 2, 1, 7 — four distinct values in four adjacent i32 slots, with no input struct for a permutation to cancel against. Texture2D never got that: nothing without a GPU reads its width, height or mipmaps at all. And get-image-color indexes y*width + x, so on a 4-wide, 2-tall image (3,0) exists and its transpose does not. That is the axis discriminator the collision family could not be — exchange x and y in the wrapper and the read goes out of bounds. The two flips say it twice more: on two rows, one moves a mark the other leaves alone. The PNG round trip is not the symmetric trap either. stb's encoder and decoder are external ground truth; they agree with each other, not with whatever field order Flan believes in. Verified to fail, each restored after: width against height, mipmaps against format, x against y in the shim, the two flips bound to each other, and the crop rectangle's width against its height. --- test/programs/raylib-image.flan | 160 ++++++++++++++++++++++++++++++++ test/test_acceptance.ml | 67 +++++++++++++ vendor/raylib/raylib.flan | 113 ++++++++++++++++++++++ vendor/raylib/shim.c | 67 +++++++++++++ 4 files changed, 407 insertions(+) create mode 100644 test/programs/raylib-image.flan diff --git a/test/programs/raylib-image.flan b/test/programs/raylib-image.flan new file mode 100644 index 0000000..7bfe9fd --- /dev/null +++ b/test/programs/raylib-image.flan @@ -0,0 +1,160 @@ +(import rl "vendor:raylib") + +;; raylib's Image family, headless. An Image is pixels in RAM: no window, no +;; GL context, and — unlike every other struct in the package — raylib will +;; *compute* with it. That is what makes this the strongest FFI case in the +;; project rather than another link check. +;; +;; Two things are being pinned here and they are different things: +;; +;; 1. **Flan's Image layout.** gen-image-color is handed two scalars and +;; answers with a struct whose four ints are 4, 2, 1 and 7 — all +;; distinct, so exchanging any two of width/height/mipmaps/format shows +;; up immediately. Scalars in, fields out: a permuted layout cannot +;; cancel itself the way store-and-return does, which is why this pins +;; more than the shapes texture ever could. It also pins `data`: drop it +;; from the defstruct and `width` reads the low half of raylib's pointer. +;; +;; 2. **The shim's argument order and raylib's own index arithmetic.** +;; get-image-color reads pixel y*width + x out of the buffer, so on a +;; 4-wide, 2-tall image the pixel at (3,0) exists and (0,3) does not. +;; Exchange x and y in the wrapper and the answer is transparent black. +;; This is the axis discriminator that no axis-aligned geometry can be: +;; the image is not square, so a reflection has nowhere to hide. +;; +;; The image is deliberately 4 x 2 throughout. A square one would let a +;; transposed read pass, and that is exactly the trap the collision cases fell +;; into. + +(defconst bg (rl/Color {:r 10 :g 20 :b 30 :a 255})) +(defconst mark-a (rl/Color {:r 200 :g 0 :b 0 :a 255})) +(defconst mark-b (rl/Color {:r 0 :g 200 :b 0 :a 255})) + +;; Where the export goes and comes back from. The two optimisation levels +;; write identical bytes, so sharing one path between runs is harmless. +(defconst png-path "/tmp/flan-raylib-image.png") + +(defn show-image [name string i rl/Image] + (print-str name) + (print-str " ") (print-i64 (i64 (.width i))) + (print-str " ") (print-i64 (i64 (.height i))) + (print-str " ") (print-i64 (i64 (.mipmaps i))) + (print-str " ") (print-i64 (i64 (.format i))) + (newline)) + +(defn show-color [name string c rl/Color] + (print-str name) + (print-str " ") (print-i64 (i64 (.r c))) + (print-str " ") (print-i64 (i64 (.g c))) + (print-str " ") (print-i64 (i64 (.b c))) + (print-str " ") (print-i64 (i64 (.a c))) + (newline)) + +(defn show-bool [name string b bool] + (print-str name) (print-str " ") + (print-line (if b "yes" "no"))) + +;; Every pixel read names its coordinates in the label, so a failure says +;; which one moved rather than only that something did. +(defn show-pixel [name string i rl/Image x i32 y i32] + (show-color name (rl/get-image-color i x y))) + +(defn main [] i32 + (rl/set-trace-log-level :warning) + + ;; ── The layout, from a struct raylib built ────────────────────────── + ;; + ;; 4 wide, 2 tall, 1 mipmap level, format 7 (uncompressed R8G8B8A8). Four + ;; different numbers in four adjacent i32 slots is the case Texture2D never + ;; got: there, nothing without a GPU read width, height or mipmaps at all. + (let [img (rl/gen-image-color 4 2 bg)] + (show-image "generated" img) + + ;; ── The axes, from raylib's own indexing ─────────────────────────── + ;; + ;; (3,0) is the last pixel of the first row and (0,1) the first of the + ;; second. On a 4 x 2 image neither coordinate pair is valid with x and y + ;; exchanged, so a wrapper with its arguments the wrong way round reads out + ;; of bounds and answers 0 0 0 0. + (rl/image-draw-pixel (addr img) 3 0 mark-a) + (rl/image-draw-pixel (addr img) 0 1 mark-b) + (show-pixel "at 3,0" img 3 0) + (show-pixel "at 0,1" img 0 1) + ;; And the two corners nothing was written to, because a get that ignored + ;; its coordinates and returned the last-written colour would pass above. + (show-pixel "at 0,0" img 0 0) + (show-pixel "at 3,1" img 3 1) + + ;; ── Flip horizontal, then vertical ───────────────────────────────── + ;; + ;; Horizontal moves x and leaves y: (3,0) becomes (0,0) and (0,1) becomes + ;; (3,1). Bind the two flips to each other's wrappers and this reads + ;; unchanged at (3,0) instead, because a vertical flip of a 2-row image + ;; would put the marks on the other rows entirely. + (rl/image-flip-horizontal (addr img)) + (show-pixel "flipped-h at 0,0" img 0 0) + (show-pixel "flipped-h at 3,1" img 3 1) + (show-pixel "flipped-h at 3,0" img 3 0) + + ;; Vertical moves y and leaves x, so the two marks swap rows: (0,0) goes to + ;; (0,1) and (3,1) to (3,0). + (rl/image-flip-vertical (addr img)) + (show-pixel "flipped-v at 0,1" img 0 1) + (show-pixel "flipped-v at 3,0" img 3 0) + (show-pixel "flipped-v at 0,0" img 0 0) + + ;; ── Out to a PNG and back ────────────────────────────────────────── + ;; + ;; The file is external ground truth, which is what stops this being the + ;; symmetric round trip the rest of the package has to avoid: the encoder + ;; and the decoder are stb's, they agree with each other and not with + ;; whatever field order Flan believes in. A path crosses as ptr+len and + ;; the shim NUL-terminates a copy, so this exercises the string half of + ;; the boundary too. + (show-bool "exported" (rl/export-image img png-path)) + (let [back (rl/load-image png-path)] + (show-bool "loaded valid" (rl/image-valid? back)) + (show-image "loaded" back) + (show-pixel "loaded at 0,1" back 0 1) + (show-pixel "loaded at 3,0" back 3 0) + (show-pixel "loaded at 0,0" back 0 0) + + ;; ── Nearest-neighbour resize ───────────────────────────────────── + ;; + ;; 4 x 2 to 8 x 2 doubles each pixel across, and leaves the rows alone. + ;; The colours survive exactly, which bicubic's would not, so this is + ;; the resize that can be asserted on content: the mark at (0,1) spreads + ;; to (0,1) and (1,1), the one at (3,0) to (6,0) and (7,0), and (2,1) is + ;; background between them. New width and height are 8 and 2 — distinct, + ;; so a wrapper that swapped them answers 2 and 8. + (rl/image-resize-nn (addr back) 8 2) + (show-image "resized-nn" back) + (show-pixel "nn at 0,1" back 0 1) + (show-pixel "nn at 1,1" back 1 1) + (show-pixel "nn at 6,0" back 6 0) + (show-pixel "nn at 7,0" back 7 0) + (show-pixel "nn at 2,1" back 2 1) + + ;; Bicubic. Its pixels are interpolated and not worth asserting, but the + ;; dimensions are, and 2 x 6 is asymmetric in both directions at once. + (rl/image-resize (addr back) 2 6) + (show-image "resized" back) + (rl/unload-image back)) + (rl/unload-image img)) + + ;; ── Crop, which is where Rectangle meets Image ────────────────────── + ;; + ;; A 6 x 3 image with one mark at (5,0), cropped to (x 4, y 0, w 2, h 1). + ;; The result is 2 x 1 and the mark has moved to (1,0) — it survived, so the + ;; crop's x really is 4 and not its width, and the region really is two wide + ;; and one tall and not the other way about. Exchange width and height in + ;; the Rectangle and the result is 1 x 2 with the mark gone. + (let [img (rl/gen-image-color 6 3 bg)] + (rl/image-draw-pixel (addr img) 5 0 mark-a) + (rl/image-crop (addr img) (rl/Rectangle {:x 4.0 :y 0.0 :width 2.0 :height 1.0})) + (show-image "cropped" img) + (show-pixel "cropped at 1,0" img 1 0) + (show-pixel "cropped at 0,0" img 0 0) + (rl/unload-image img)) + + 0) diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index a3c5e84..679c826 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -237,6 +237,73 @@ let () = else print_endline "acceptance: skipping the raylib FFI case (no libraylib)"; + (* raylib's Image family, headless, and the strongest FFI case here: an + Image is pixels in RAM, so raylib *computes* with it rather than + storing and returning it. + + Two separate things are pinned. gen-image-color is handed two scalars + and answers with a struct reading 4, 2, 1, 7 — four distinct values in + four adjacent i32 slots, so exchanging any two of width, height, + mipmaps and format is visible, and dropping `data` makes width the low + half of raylib's pointer. Scalars in and fields out is what makes that + work: a permuted layout has nothing to cancel against, unlike the + shapes texture, where nothing without a GPU read width, height or + mipmaps at all. + + The other is the axis, which the collision cases could not get. raylib + indexes a pixel as y*width + x, and the image is 4 wide by 2 tall, so + (3,0) exists and its transpose does not — exchange x and y in the shim + and the read is out of bounds and answers transparent black. The + horizontal and vertical flips are the same argument twice more: on two + rows, one of them moves a mark that the other leaves alone. + + The PNG round trip is not the symmetric trap either: stb's encoder and + decoder are external ground truth and agree with each other rather than + with whatever field order Flan believes in. It also crosses a path as + ptr+len. /tmp is written to, and both optimisation levels write the + same bytes, so the shared name is harmless. + + Trace logging stays at :warning and no read here is out of bounds, so + a warning appearing in this output is a real failure — [run] folds + stderr in. *) + let raylib_image_out = + "generated 4 2 1 7\n\ + at 3,0 200 0 0 255\n\ + at 0,1 0 200 0 255\n\ + at 0,0 10 20 30 255\n\ + at 3,1 10 20 30 255\n\ + flipped-h at 0,0 200 0 0 255\n\ + flipped-h at 3,1 0 200 0 255\n\ + flipped-h at 3,0 10 20 30 255\n\ + flipped-v at 0,1 200 0 0 255\n\ + flipped-v at 3,0 0 200 0 255\n\ + flipped-v at 0,0 10 20 30 255\n\ + exported yes\n\ + loaded valid yes\n\ + loaded 4 2 1 7\n\ + loaded at 0,1 200 0 0 255\n\ + loaded at 3,0 0 200 0 255\n\ + loaded at 0,0 10 20 30 255\n\ + resized-nn 8 2 1 7\n\ + nn at 0,1 200 0 0 255\n\ + nn at 1,1 200 0 0 255\n\ + nn at 6,0 0 200 0 255\n\ + nn at 7,0 0 200 0 255\n\ + nn at 2,1 10 20 30 255\n\ + resized 2 6 1 7\n\ + cropped 2 1 1 7\n\ + cropped at 1,0 200 0 0 255\n\ + cropped at 0,0 10 20 30 255\n" + in + if Sys.command "ldconfig -p 2>/dev/null | grep -q libraylib" = 0 then begin + outputs "raylib images, headless" "programs/raylib-image.flan" + raylib_image_out; + outputs ~opt:"-O0" "raylib images, headless, -O0" "programs/raylib-image.flan" + raylib_image_out + end + else + print_endline "acceptance: skipping the raylib Image case (no libraylib)"; + (* Again at -O0. Everything above runs through mem2reg, which launders a sloppy alloca; -O0 tests the IR actually emitted, so a disagreement between the two points at undefined behaviour rather than a typo. *) diff --git a/vendor/raylib/raylib.flan b/vendor/raylib/raylib.flan index 6e06e40..031df54 100644 --- a/vendor/raylib/raylib.flan +++ b/vendor/raylib/raylib.flan @@ -392,3 +392,116 @@ p position c tint] (draw-texture-rec-raw (addr t) (addr s) (addr p) (addr c)))) + +;; ── Images ────────────────────────────────────────────────────────── +;; +;; An Image is pixels in RAM. Nothing here touches the GPU, which makes it the +;; one corner of the 2D surface a headless test can assert properly — raylib +;; *computes* with these, and a wrong answer is a wrong number rather than the +;; struct handed back unchanged. +;; +;; `data` is raylib's buffer and Flan never reads through it; it is here so +;; the struct is the right size and the four ints that follow are at the right +;; offsets. `format` is a PixelFormat code — GenImageColor makes 7, which is +;; uncompressed R8G8B8A8, one byte per channel. +;; +;; The split between by-value and by-pointer here is raylib's own and worth +;; keeping: a call that *mutates* the image takes (Ptr Image) at the Flan +;; level too, so a caller can see which ones change what they are given. +(defstruct Image [data (Ptr u8) width i32 height i32 mipmaps i32 format i32]) + +(declare load-image-raw [path string out (Ptr Image)] "flan_rl_load_image") + +(defn load-image [path string] Image + (let [i (Image {})] + (load-image-raw path (addr i)) + i)) + +;; raylib 5.5 spells this IsImageValid. IsImageReady, which older code calls, +;; does not exist here — the same rename that took IsTextureReady. +(declare image-valid?-raw [image (Ptr Image)] bool "flan_rl_is_image_valid") + +(defn image-valid? [image Image] bool + (let [i image] + (image-valid?-raw (addr i)))) + +;; By value, as raylib has it. The caller's copy is dangling afterwards — +;; `data` pointed at the buffer this just freed — so an Image is used or +;; unloaded, never both. +(declare unload-image-raw [image (Ptr Image)] "flan_rl_unload_image") + +(defn unload-image [image Image] + (let [i image] + (unload-image-raw (addr i)))) + +;; The format is taken from the path's extension, so ".png" writes a PNG. +;; False means it could not be written. +(declare export-image-raw [image (Ptr Image) path string] bool + "flan_rl_export_image") + +(defn export-image [image Image path string] bool + (let [i image] + (export-image-raw (addr i) path))) + +(declare gen-image-color-raw + [width i32 height i32 color (Ptr Color) out (Ptr Image)] + "flan_rl_gen_image_color") + +(defn gen-image-color [width i32 height i32 color Color] Image + (let [c color + i (Image {})] + (gen-image-color-raw width height (addr c) (addr i)) + i)) + +;; Bicubic, so the pixels that come out are interpolated and only the new +;; width and height are exactly predictable. image-resize-nn is the +;; nearest-neighbour one, and it is the one to reach for when the colours +;; have to survive. +(declare image-resize [image (Ptr Image) width i32 height i32] + "flan_rl_image_resize") +(declare image-resize-nn [image (Ptr Image) width i32 height i32] + "flan_rl_image_resize_nn") + +(declare image-crop-raw [image (Ptr Image) crop (Ptr Rectangle)] + "flan_rl_image_crop") + +(defn image-crop [image (Ptr Image) crop Rectangle] + (let [r crop] + (image-crop-raw image (addr r)))) + +(declare image-flip-horizontal [image (Ptr Image)] + "flan_rl_image_flip_horizontal") +(declare image-flip-vertical [image (Ptr Image)] + "flan_rl_image_flip_vertical") + +(declare image-draw-pixel-raw + [image (Ptr Image) x i32 y i32 color (Ptr Color)] + "flan_rl_image_draw_pixel") + +(defn image-draw-pixel [image (Ptr Image) x i32 y i32 color Color] + (let [c color] + (image-draw-pixel-raw image x y (addr c)))) + +;; Out of bounds is not an error: raylib logs a warning and hands back a +;; transparent black, so a caller that is off by one gets zeroes rather than +;; somebody else's memory. +(declare get-image-color-raw + [image (Ptr Image) x i32 y i32 out (Ptr Color)] + "flan_rl_get_image_color") + +(defn get-image-color [image Image x i32 y i32] Color + (let [i image + c (Color {})] + (get-image-color-raw (addr i) x y (addr c)) + c)) + +;; The one call in this section that does need a GL context — it uploads. An +;; image loaded and edited on the CPU becomes something draw-texture can use. +(declare load-texture-from-image-raw [image (Ptr Image) out (Ptr Texture2D)] + "flan_rl_load_texture_from_image") + +(defn load-texture-from-image [image Image] Texture2D + (let [i image + t (Texture2D {})] + (load-texture-from-image-raw (addr i) (addr t)) + t)) diff --git a/vendor/raylib/shim.c b/vendor/raylib/shim.c index 1cd7e13..85b00c3 100644 --- a/vendor/raylib/shim.c +++ b/vendor/raylib/shim.c @@ -232,3 +232,70 @@ bool flan_rl_check_collision_lines(const Vector2 *a1, const Vector2 *a2, Vector2 *out) { return CheckCollisionLines(*a1, *a2, *b1, *b2, out); } + +/* ── Images ───────────────────────────────────────────────────────── + * + * An Image is pixels in RAM, so all of this runs with no window and no GL + * context — which is why it is the part of the package that a headless test + * can actually assert rather than merely link. `data` is the pixel buffer + * raylib owns; `format` is a PixelFormat enum and GenImageColor makes 7 + * (uncompressed R8G8B8A8). + * + * raylib 5.5 spells the predicate IsImageValid. IsImageReady, which the 5.1 + * header still had, is gone — checked with nm -D, not remembered. + */ +typedef struct { void *data; int width, height, mipmaps, format; } Image; + +extern Image LoadImage(const char *fileName); +extern bool IsImageValid(Image image); +extern void UnloadImage(Image image); +extern bool ExportImage(Image image, const char *fileName); +extern Image GenImageColor(int width, int height, Color color); +extern void ImageResize(Image *image, int newWidth, int newHeight); +extern void ImageResizeNN(Image *image, int newWidth, int newHeight); +extern void ImageCrop(Image *image, Rectangle crop); +extern void ImageFlipHorizontal(Image *image); +extern void ImageFlipVertical(Image *image); +extern void ImageDrawPixel(Image *dst, int posX, int posY, Color color); +extern Color GetImageColor(Image image, int x, int y); +extern Texture2D LoadTextureFromImage(Image image); + +void flan_rl_load_image(const char *path, long long n, Image *out) { + char buf[PATH_MAX]; + *out = LoadImage(cstr(path, n, buf, sizeof buf)); +} + +bool flan_rl_is_image_valid(const Image *image) { return IsImageValid(*image); } +void flan_rl_unload_image(const Image *image) { UnloadImage(*image); } + +bool flan_rl_export_image(const Image *image, const char *path, long long n) { + char buf[PATH_MAX]; + return ExportImage(*image, cstr(path, n, buf, sizeof buf)); +} + +void flan_rl_gen_image_color(int width, int height, const Color *color, + Image *out) { + *out = GenImageColor(width, height, *color); +} + +void flan_rl_image_resize(Image *image, int w, int h) { ImageResize(image, w, h); } +void flan_rl_image_resize_nn(Image *image, int w, int h) { ImageResizeNN(image, w, h); } + +void flan_rl_image_crop(Image *image, const Rectangle *crop) { + ImageCrop(image, *crop); +} + +void flan_rl_image_flip_horizontal(Image *image) { ImageFlipHorizontal(image); } +void flan_rl_image_flip_vertical(Image *image) { ImageFlipVertical(image); } + +void flan_rl_image_draw_pixel(Image *dst, int x, int y, const Color *color) { + ImageDrawPixel(dst, x, y, *color); +} + +void flan_rl_get_image_color(const Image *image, int x, int y, Color *out) { + *out = GetImageColor(*image, x, y); +} + +void flan_rl_load_texture_from_image(const Image *image, Texture2D *out) { + *out = LoadTextureFromImage(*image); +}