From 1830995cc5d0ddb6da07eb3cde7d66817a44b700 Mon Sep 17 00:00:00 2001 From: Greg Shuflin Date: Mon, 23 Mar 2026 13:41:24 -0700 Subject: [PATCH] Remove opaque Pixels type; add safe updateTexture and zero-copy updateTextureFromSurface The opaque Pixels type wrapped a void* pointing into an SDL_Surface's pixel buffer, but nothing tied the Pixels lifetime to the surface. If the GC collected the surface first, the Pixels pointer would dangle, causing use-after-free. Replace with two safe alternatives: - updateTexture now takes a ByteArray (Lean-owned, GC-managed buffer) plus pitch, matching how Haskell's sdl2 uses ByteString and Rust's rust-sdl2 uses &[u8]. This is faithful to SDL_UpdateTexture's general void* interface but requires copying pixels into a ByteArray first. - updateTextureFromSurface is a new zero-copy convenience that takes an SDLSurface directly. The C side extracts both pixels and pitch from the surface internally. Because the surface is borrowed (@&) for the call's duration, the GC cannot collect it mid-use. This is not strictly faithful to SDL_UpdateTexture's C API, but is the common case and avoids an unnecessary memcpy. Also removes: Pixels type, Pixels.nonemptyType, sdl_pixels_external_class, sdl_Surface_get_pixels, and the pixels_external_class registration in sdl_init. WebcamApp.lean is updated to use updateTextureFromSurface. Co-Authored-By: Claude Opus 4.6 --- SDL.lean | 18 ++++++++++-------- WebcamApp.lean | 6 ++---- c/sdl.c | 32 +++++++++++++++----------------- 3 files changed, 27 insertions(+), 29 deletions(-) diff --git a/SDL.lean b/SDL.lean index 419488d..20597dc 100644 --- a/SDL.lean +++ b/SDL.lean @@ -132,10 +132,6 @@ instance SDLSurface.instNonempty : Nonempty SDLSurface := SDLSurface.nonemptyTyp namespace SDLSurface -private opaque Pixels.nonemptyType : NonemptyType -def Pixels: Type := Pixels.nonemptyType.type -instance PIxels.instNonempty : Nonempty Pixels := Pixels.nonemptyType.property - @[extern "sdl_Surface_get_format"] opaque format : @& SDLSurface -> UInt32 @@ -145,9 +141,6 @@ opaque w : @& SDLSurface -> Int32 @[extern "sdl_Surface_get_h"] opaque h : @& SDLSurface -> Int32 -@[extern "sdl_Surface_get_pixels"] -opaque pixels : @& SDLSurface -> Pixels - @[extern "sdl_Surface_get_pitch"] opaque pitch : @& SDLSurface -> Int32 @@ -167,7 +160,16 @@ opaque createTextureFromSurface -- TODO handle SDLRect argument @[extern "sdl_update_texture"] -opaque updateTexture (texture: @& SDLTexture) (pixels: @& SDLSurface.Pixels) (pitch: Int32): SDLIO Bool +opaque updateTexture (texture: @& SDLTexture) (pixels: @& ByteArray) (pitch: Int32): SDLIO Bool + +-- Zero-copy optimization: updates a texture directly from an SDL_Surface's +-- pixel buffer, avoiding the intermediate ByteArray copy required by +-- updateTexture. This is not strictly faithful to the SDL_UpdateTexture C API +-- (which takes a generic void* for pixels), but is safe because the surface +-- is borrowed (@&) for the duration of the call, preventing the GC from +-- collecting the surface (and its pixel data) while the update is in progress. +@[extern "sdl_update_texture_from_surface"] +opaque updateTextureFromSurface (texture: @& SDLTexture) (surface: @& SDLSurface): SDLIO Bool def loadImageTexture diff --git a/WebcamApp.lean b/WebcamApp.lean index 97fad17..0d7e5c7 100644 --- a/WebcamApp.lean +++ b/WebcamApp.lean @@ -106,10 +106,8 @@ partial def webcamLoop (stateRef: IO.Ref WebcamState): IO Unit := do let cameraTexture ← SDL.createTexture state.renderer cameraFrame.format SDL.SDL_TEXTUREACCESS_STREAMING w h stateRef.modify fun s => { s with texture := some cameraTexture } | some tx => - -- Subsequent frames: update the texture - let pixels := cameraFrame.pixels - let pitch := cameraFrame.pitch - let _ ← SDL.updateTexture tx pixels pitch + -- Subsequent frames: update the texture directly from the camera frame + let _ ← SDL.updateTextureFromSurface tx cameraFrame SDL.releaseCameraFrame state.camera cameraFrame diff --git a/c/sdl.c b/c/sdl.c index 564a1e8..3bc1578 100644 --- a/c/sdl.c +++ b/c/sdl.c @@ -99,13 +99,6 @@ static void sdl_mixer_audio_foreach(void * val, lean_obj_arg fn) { } -static lean_external_class* sdl_pixels_external_class = NULL; -static void sdl_pixels_foreach(void* vald, lean_obj_arg fn) { -} -static void sdl_pixels_finalizer(void*h) { -} - - static lean_external_class * sdl_camera_external_class = NULL; static void sdl_camera_foreach(void * val, lean_obj_arg fn) { @@ -141,7 +134,6 @@ lean_obj_res sdl_init(uint32_t flags, lean_obj_arg w) { sdl_camera_external_class = lean_register_external_class(sdl_camera_finalizer, sdl_camera_foreach); sdl_camera_spec_external_class = lean_register_external_class(sdl_camera_spec_finalizer, sdl_camera_spec_foreach); sdl_camera_frame_external_class = lean_register_external_class(sdl_camera_frame_finalizer, sdl_camera_frame_foreach); - sdl_pixels_external_class = lean_register_external_class(sdl_pixels_finalizer, sdl_pixels_foreach); return lean_io_result_mk_ok(lean_box_uint32(result)); } @@ -312,13 +304,6 @@ int32_t sdl_Surface_get_h(b_lean_obj_arg surface_obj) { return (int32_t)surface->h; } -lean_object* sdl_Surface_get_pixels(b_lean_obj_arg surface_obj) { - SDL_Surface* surface = (SDL_Surface*)lean_get_external_data(surface_obj); - void* pixels = surface->pixels; - lean_object* external_pixels = lean_alloc_external(sdl_pixels_external_class, pixels); - return external_pixels; // Not wrapped in IO - Lean expects Pixels directly -} - int32_t sdl_Surface_get_pitch(b_lean_obj_arg surface_obj) { SDL_Surface* surface = (SDL_Surface*)lean_get_external_data(surface_obj); return (int32_t)surface->pitch; @@ -353,14 +338,27 @@ lean_obj_res sdl_create_texture_from_surface(b_lean_obj_arg g_renderer, b_lean_o return lean_io_result_mk_ok(external_texture); } -lean_obj_res sdl_update_texture(b_lean_obj_arg texture_obj, b_lean_obj_arg pixels_obj, int32_t pitch) { +lean_obj_res sdl_update_texture(b_lean_obj_arg texture_obj, b_lean_obj_arg byte_array, int32_t pitch) { SDL_Texture * texture = (SDL_Texture *)lean_get_external_data(texture_obj); - void* pixels = lean_get_external_data(pixels_obj); // Pixels is void*, not SDL_Surface* + void* pixels = (void*)lean_sarray_cptr(byte_array); bool result = SDL_UpdateTexture(texture, NULL, pixels, pitch); return lean_io_result_mk_ok(lean_box(result)); } +// Zero-copy optimization: updates a texture directly from an SDL_Surface's +// pixel buffer, avoiding the intermediate ByteArray copy. This is not +// strictly faithful to the SDL_UpdateTexture C API (which takes a void*), +// but is safe because the surface is borrowed for the duration of the call, +// preventing the GC from freeing the pixel data mid-use. +lean_obj_res sdl_update_texture_from_surface(b_lean_obj_arg texture_obj, b_lean_obj_arg surface_obj) { + SDL_Texture * texture = (SDL_Texture *)lean_get_external_data(texture_obj); + SDL_Surface * surface = (SDL_Surface *)lean_get_external_data(surface_obj); + + bool result = SDL_UpdateTexture(texture, NULL, surface->pixels, surface->pitch); + return lean_io_result_mk_ok(lean_box(result)); +} + lean_obj_res sdl_load_font(b_lean_obj_arg fontname, uint32_t font_size, lean_obj_arg w) { const char* fontname_str = lean_string_cstr(fontname); TTF_Font* font = TTF_OpenFont(fontname_str, font_size);