Skip to content

Commit 458701d

Browse files
P1: implement real Zig FFI matching the Idris2 ABI (#42)
## What was wrong The Zig FFI at `src/interface/ffi/src/main.zig` did **not compile**. The analysis-engine handle was declared as: ```zig pub const Handle = opaque { allocator: std.mem.Allocator, initialized: bool, ... }; ``` Zig rejects this with `error: opaque types cannot have fields`. The file was effectively a half-/unrendered template that never built, so it could not honour the ABI contract defined by the Idris2 ABI (the source of truth). ## The fix `main.zig` is rewritten as a self-contained, compiling reference FFI driven by `src/interface/abi/Atsiser/ABI/Foreign.idr` and `Types.idr`: - **Exact symbols**: exports all **20** `C:atsiser_*` symbols declared in `Foreign.idr`, verbatim (`atsiser_init`, `atsiser_free`, `atsiser_parse_header`, `atsiser_analyse_allocations`, `atsiser_build_ownership_graph`, `atsiser_detect_buffers`, `atsiser_generate_viewtypes`, `atsiser_generate_proofs`, `atsiser_generate_bounds_proofs`, `atsiser_compile_ats2`, `atsiser_verify_linkage`, `atsiser_allocation_count`, `atsiser_ownership_edge_count`, `atsiser_proof_count`, `atsiser_analysis_report`, `atsiser_free_string`, `atsiser_last_error`, `atsiser_version`, `atsiser_build_info`, `atsiser_is_initialized`). All `callconv(.C)`. - **Matching signatures**: Bits64 handle ↔ opaque `?*Engine`; Idris `String` arg ↔ `?[*:0]const u8`; returns-a-string Bits64 ↔ `?[*:0]const u8`; result-returning Bits32 ↔ `Result` enum as `c_int`; counts ↔ `c_uint`. - **Matching result codes**: `Result = enum(c_int)` whose values exactly match `Atsiser.ABI.Types.resultToInt` — Ok=0, Error=1 (`err`), InvalidParam=2, OutOfMemory=3, NullPointer=4, OwnershipViolation=5, BoundsViolation=6 (**7** codes). - **Memory-sane in-memory reference**: a real `Engine` tracking allocation sites, ownership edges, and buffer/proof counts via `std.heap.c_allocator`, with proper `deinit` and C-string ownership (`dup` / `std.mem.span` / `allocPrintZ` / `atsiser_free_string`). libclang parsing and `patsopt` (ATS2 → C) bridging remain stubs, but signatures, symbols, and result codes match the ABI. - **Tests**: two `test` blocks — the main analysis pipeline (parse → analyse → ownership graph → proofs → JSON report) and null-handle / invalid-param rejection. Only `src/interface/ffi/` (the Zig) was touched. The Idris ABI, Cargo, and other files are unchanged. ## Verification - `cd src/interface/ffi && zig test src/main.zig -lc` → **all tests pass**, zero errors/warnings: ``` 1/2 main.test.analysis pipeline and report...OK 2/2 main.test.null handle and invalid params are rejected...OK All 2 tests passed. ``` - `cd src/interface/abi && idris2 --build atsiser-abi.ipkg` → **exits 0 clean** (builds Types, Layout, Proofs, Foreign), build dir removed afterward. - Symbol cross-check: every `C:<name>` in `Foreign.idr` has a matching `export fn <name>` in `main.zig` (20/20, perfect diff match). - Result codes match `resultToInt` exactly (7/7). > Note: any rust-ci / Hypatia / governance CI reds are pre-existing estate-infra issues unrelated to this Zig-only change. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_019xMKB3T4Vo5FYC7Czx3JSH --- _Generated by [Claude Code](https://claude.ai/code/session_019xMKB3T4Vo5FYC7Czx3JSH)_ Co-authored-by: Claude <noreply@anthropic.com>
1 parent 6fe9694 commit 458701d

1 file changed

Lines changed: 297 additions & 269 deletions

File tree

0 commit comments

Comments
 (0)