|
| 1 | +// SPDX-License-Identifier: AGPL-3.0-or-later |
| 2 | +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> |
| 3 | +// |
| 4 | +// gen_abi_expected.zig — extract the canonical C-ABI layout numbers from the |
| 5 | +// machine-checked Idris2 model (src/interface/abi/Layout.idr) and emit the Zig |
| 6 | +// source file (src/interface/ffi/src/abi_layout_expected.zig) consumed by the |
| 7 | +// Zig-side cross-check (abi_layout.zig). |
| 8 | +// |
| 9 | +// Layout.idr is the single source of truth: it carries the proofs (NoOverlap, |
| 10 | +// AllFieldsAligned, SizeAligned, SizeCoversFields). This tool lifts the same |
| 11 | +// `MkFieldDesc name offset size align` / `MkStructLayout [...] total align` |
| 12 | +// constants into Zig so the compiler can assert the canonical extern structs |
| 13 | +// agree with the proven model. |
| 14 | +// |
| 15 | +// Run from the repository root: |
| 16 | +// zig run scripts/gen_abi_expected.zig |
| 17 | +// (or `python3 -m ziglang run scripts/gen_abi_expected.zig`). CI re-runs this and |
| 18 | +// `git diff --exit-code`s the result so the Zig table never drifts from Layout.idr. |
| 19 | + |
| 20 | +const std = @import("std"); |
| 21 | + |
| 22 | +const LAYOUT_IDR = "src/interface/abi/Layout.idr"; |
| 23 | +const OUT_ZIG = "src/interface/ffi/src/abi_layout_expected.zig"; |
| 24 | + |
| 25 | +// Idris layout variable (without the "Layout" suffix) -> Zig struct type name. |
| 26 | +const Struct = struct { idris: []const u8, zig: []const u8 }; |
| 27 | +const structs = [_]Struct{ |
| 28 | + .{ .idris = "serverHandle", .zig = "ServerHandle" }, |
| 29 | + .{ .idris = "probeResult", .zig = "ProbeResult" }, |
| 30 | + .{ .idris = "configField", .zig = "ConfigField" }, |
| 31 | + .{ .idris = "a2mlConfig", .zig = "A2MLConfig" }, |
| 32 | + .{ .idris = "gameProfile", .zig = "GameProfile" }, |
| 33 | + .{ .idris = "serverOctad", .zig = "ServerOctad" }, |
| 34 | + .{ .idris = "fingerprint", .zig = "Fingerprint" }, |
| 35 | + .{ .idris = "driftReport", .zig = "DriftReport" }, |
| 36 | +}; |
| 37 | + |
| 38 | +const HEADER = |
| 39 | + \\// SPDX-License-Identifier: AGPL-3.0-or-later |
| 40 | + \\// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> |
| 41 | + \\// |
| 42 | + \\// @generated by scripts/gen_abi_expected.zig from src/interface/abi/Layout.idr |
| 43 | + \\// DO NOT EDIT. Regenerate with: zig run scripts/gen_abi_expected.zig |
| 44 | + \\// |
| 45 | + \\// Canonical C-ABI layout numbers lifted from the machine-checked Idris2 model |
| 46 | + \\// (GSA.ABI.Layout). Consumed by abi_layout.zig to assert that the Zig extern |
| 47 | + \\// structs agree, byte-for-byte, with the proven Idris layout. |
| 48 | + \\ |
| 49 | + \\pub const Field = struct { |
| 50 | + \\ name: []const u8, |
| 51 | + \\ offset: u32, |
| 52 | + \\ size: u32, |
| 53 | + \\ alignment: u32, |
| 54 | + \\}; |
| 55 | + \\ |
| 56 | + \\pub const StructExpect = struct { |
| 57 | + \\ name: []const u8, |
| 58 | + \\ total_size: u32, |
| 59 | + \\ struct_align: u32, |
| 60 | + \\ fields: []const Field, |
| 61 | + \\}; |
| 62 | + \\ |
| 63 | + \\ |
| 64 | +; |
| 65 | + |
| 66 | +fn nextUint(it: *std.mem.TokenIterator(u8, .any)) !u32 { |
| 67 | + return std.fmt.parseInt(u32, it.next() orelse return error.ParseFailed, 10); |
| 68 | +} |
| 69 | + |
| 70 | +fn emitStruct(out: *std.array_list.Managed(u8), src: []const u8, s: Struct) !void { |
| 71 | + var nbuf: [128]u8 = undefined; |
| 72 | + const needle = try std.fmt.bufPrint(&nbuf, "{s}Layout = MkStructLayout", .{s.idris}); |
| 73 | + const at = std.mem.indexOf(u8, src, needle) orelse return error.StructNotFound; |
| 74 | + const after = src[at + needle.len ..]; |
| 75 | + const lb = std.mem.indexOfScalar(u8, after, '[') orelse return error.NoFieldList; |
| 76 | + const rel_rb = std.mem.indexOfScalar(u8, after[lb..], ']') orelse return error.NoFieldList; |
| 77 | + const body = after[lb + 1 .. lb + rel_rb]; |
| 78 | + const tail = after[lb + rel_rb + 1 ..]; // "<total> <align>" follow the ']' |
| 79 | + |
| 80 | + var tit = std.mem.tokenizeAny(u8, tail, " \r\n\t"); |
| 81 | + const total = try nextUint(&tit); |
| 82 | + const salign = try nextUint(&tit); |
| 83 | + |
| 84 | + const w = out.writer(); |
| 85 | + try w.print( |
| 86 | + "pub const {s} = StructExpect{{\n .name = \"{s}\",\n .total_size = {d},\n .struct_align = {d},\n .fields = &.{{\n", |
| 87 | + .{ s.zig, s.zig, total, salign }, |
| 88 | + ); |
| 89 | + |
| 90 | + var rest = body; |
| 91 | + while (std.mem.indexOf(u8, rest, "MkFieldDesc")) |fi| { |
| 92 | + rest = rest[fi + "MkFieldDesc".len ..]; |
| 93 | + const q1 = std.mem.indexOfScalar(u8, rest, '"') orelse return error.BadField; |
| 94 | + const q2 = std.mem.indexOfScalarPos(u8, rest, q1 + 1, '"') orelse return error.BadField; |
| 95 | + const fname = rest[q1 + 1 .. q2]; |
| 96 | + rest = rest[q2 + 1 ..]; |
| 97 | + |
| 98 | + var fit = std.mem.tokenizeAny(u8, rest, " \r\n\t"); |
| 99 | + const foff = try nextUint(&fit); |
| 100 | + const fsize = try nextUint(&fit); |
| 101 | + const falign = try nextUint(&fit); |
| 102 | + |
| 103 | + if (!std.mem.startsWith(u8, fname, "padding")) { |
| 104 | + try w.print( |
| 105 | + " .{{ .name = \"{s}\", .offset = {d}, .size = {d}, .alignment = {d} }},\n", |
| 106 | + .{ fname, foff, fsize, falign }, |
| 107 | + ); |
| 108 | + } |
| 109 | + } |
| 110 | + try w.writeAll(" },\n};\n\n"); |
| 111 | +} |
| 112 | + |
| 113 | +pub fn main() !void { |
| 114 | + var gpa = std.heap.GeneralPurposeAllocator(.{}){}; |
| 115 | + defer _ = gpa.deinit(); |
| 116 | + const alloc = gpa.allocator(); |
| 117 | + |
| 118 | + const src = try std.fs.cwd().readFileAlloc(alloc, LAYOUT_IDR, 4 * 1024 * 1024); |
| 119 | + defer alloc.free(src); |
| 120 | + |
| 121 | + var out = std.array_list.Managed(u8).init(alloc); |
| 122 | + defer out.deinit(); |
| 123 | + |
| 124 | + try out.appendSlice(HEADER); |
| 125 | + for (structs) |s| try emitStruct(&out, src, s); |
| 126 | + |
| 127 | + try out.appendSlice("pub const all = [_]StructExpect{ "); |
| 128 | + for (structs, 0..) |s, i| { |
| 129 | + if (i != 0) try out.appendSlice(", "); |
| 130 | + try out.appendSlice(s.zig); |
| 131 | + } |
| 132 | + try out.appendSlice(" };\n"); |
| 133 | + |
| 134 | + try std.fs.cwd().writeFile(.{ .sub_path = OUT_ZIG, .data = out.items }); |
| 135 | + std.debug.print("wrote {s} ({d} structs)\n", .{ OUT_ZIG, structs.len }); |
| 136 | +} |
0 commit comments