gazagnaire.org
OCaml wire format DSL with EverParse 3D output for verified parsers
1(** Generate verified C libraries from Wire codecs via EverParse. *)
2
3type schema = { name : string; module_ : Wire.module_; wire_size : int }
4
5let schema ~name ~module_ ~wire_size = { name; module_; wire_size }
6
7let generate_3d_files ~outdir schemas =
8 List.iter
9 (fun s ->
10 Wire.to_3d_file (Filename.concat outdir (s.name ^ ".3d")) s.module_)
11 schemas
12
13let copy_file ~src ~dst =
14 let ic = open_in_bin src in
15 let n = in_channel_length ic in
16 let buf = Bytes.create n in
17 really_input ic buf 0 n;
18 close_in ic;
19 let oc = open_out_bin dst in
20 output_bytes oc buf;
21 close_out oc
22
23let everparse_dir () =
24 let ic = Unix.open_process_in "which 3d.exe" in
25 let path = input_line ic in
26 ignore (Unix.close_process_in ic);
27 Filename.dirname path |> Filename.dirname
28
29let copy_everparse_endianness ~outdir =
30 let dst = Filename.concat outdir "EverParseEndianness.h" in
31 if not (Sys.file_exists dst) then begin
32 let ep_dir = everparse_dir () in
33 let src = Filename.concat ep_dir "src/3d/EverParseEndianness.h" in
34 if Sys.file_exists src then copy_file ~src ~dst
35 else Fmt.failwith "Cannot find EverParseEndianness.h at %s" src
36 end
37
38let has_3d_exe () = Sys.command "command -v 3d.exe > /dev/null 2>&1" = 0
39
40let run_everparse ~outdir schemas =
41 List.iter
42 (fun s ->
43 let f = s.name ^ ".3d" in
44 let cmd = Fmt.str "cd %s && 3d.exe --batch %s" outdir f in
45 let ret = Sys.command cmd in
46 if ret <> 0 then Fmt.failwith "EverParse failed on %s with code %d" f ret)
47 schemas;
48 copy_everparse_endianness ~outdir
49
50(** Extract the validate function name from an EverParse-generated header.
51
52 EverParse normalizes C identifiers in a way that depends on consecutive
53 uppercase runs (e.g., [SpaceOSFrame] becomes [SpaceOsframe]). Rather than
54 replicating the algorithm, we read the generated header files. *)
55let extract_validate_fn ~outdir name =
56 let header = Filename.concat outdir (name ^ ".h") in
57 let ic = open_in header in
58 let result = ref None in
59 (try
60 while true do
61 let line = input_line ic in
62 let trimmed = String.trim line in
63 if String.length trimmed > 0 && String.contains trimmed '(' then begin
64 let fn = String.sub trimmed 0 (String.index trimmed '(') in
65 let fn = String.trim fn in
66 let has_validate =
67 let vlen = String.length "Validate" in
68 let rec check i =
69 if i + vlen > String.length fn then false
70 else if String.sub fn i vlen = "Validate" then true
71 else check (i + 1)
72 in
73 check 0
74 in
75 if has_validate && fn <> "" && fn.[0] <> '#' && fn.[0] <> '*' then
76 result := Some fn
77 end
78 done
79 with End_of_file -> ());
80 close_in ic;
81 match !result with
82 | Some fn -> fn
83 | None -> Fmt.failwith "Could not find Validate function in %s" header
84
85let emit_schema_tests ppf ~outdir s =
86 let pr fmt = Fmt.pf ppf fmt in
87 let validate_fn = extract_validate_fn ~outdir s.name in
88 let lower = String.lowercase_ascii s.name in
89 pr "\n /* %s (%d bytes) */\n" s.name s.wire_size;
90 pr " {\n";
91 pr " int pass = 0, fail = 0;\n";
92 pr " uint8_t buf[%d];\n" s.wire_size;
93 pr " uint64_t r;\n\n";
94 pr " memset(buf, 0, %d);\n" s.wire_size;
95 pr " r = %s(NULL, counting_error_handler, buf, %d, 0);\n" validate_fn
96 s.wire_size;
97 pr " CHECK(\"zero buffer validates\", EverParseIsSuccess(r));\n";
98 pr " CHECK(\"position advanced to %d\", r == %d);\n" s.wire_size
99 s.wire_size;
100 pr "\n";
101 pr " r = %s(NULL, counting_error_handler, buf, %d, 0);\n" validate_fn
102 (s.wire_size * 2);
103 pr " CHECK(\"larger buffer validates\", EverParseIsSuccess(r));\n";
104 pr " CHECK(\"position is %d not %d\", r == %d);\n" s.wire_size
105 (s.wire_size * 2) s.wire_size;
106 pr "\n";
107 pr " for (uint64_t len = 0; len < %d; len++) {\n" s.wire_size;
108 pr " error_count = 0;\n";
109 pr " r = %s(NULL, counting_error_handler, buf, len, 0);\n" validate_fn;
110 pr " CHECK(\"truncated to len fails\", EverParseIsError(r));\n";
111 pr " }\n\n";
112 pr " r = %s(NULL, counting_error_handler, buf, 0, 0);\n" validate_fn;
113 pr " CHECK(\"empty input fails\", EverParseIsError(r));\n\n";
114 pr " srand(42);\n";
115 pr " for (int i = 0; i < 1000; i++) {\n";
116 pr " for (int j = 0; j < %d; j++)\n" s.wire_size;
117 pr " buf[j] = (uint8_t)(rand() & 0xff);\n";
118 pr " r = %s(NULL, counting_error_handler, buf, %d, 0);\n" validate_fn
119 s.wire_size;
120 pr " CHECK(\"random buffer validates\", EverParseIsSuccess(r));\n";
121 pr " CHECK(\"random position correct\", r == %d);\n" s.wire_size;
122 pr " }\n\n";
123 pr " printf(\"%s: %%d passed, %%d failed\\n\", pass, fail);\n" lower;
124 pr " failures += fail;\n";
125 pr " }\n"
126
127let generate_test ~outdir schemas =
128 let oc = open_out (Filename.concat outdir "test.c") in
129 let ppf = Format.formatter_of_out_channel oc in
130 let pr fmt = Fmt.pf ppf fmt in
131 pr "#include <stdio.h>\n";
132 pr "#include <stdlib.h>\n";
133 pr "#include <stdint.h>\n";
134 pr "#include <string.h>\n";
135 pr "#include \"EverParse.h\"\n";
136 List.iter (fun s -> pr "#include \"%s.h\"\n" s.name) schemas;
137 pr "\nstatic int error_count;\n\n";
138 pr "static void counting_error_handler(\n";
139 pr " EVERPARSE_STRING t, EVERPARSE_STRING f, EVERPARSE_STRING r,\n";
140 pr " uint64_t c, uint8_t *ctx, uint8_t *i, uint64_t p) {\n";
141 pr " (void)t; (void)f; (void)r; (void)c; (void)ctx; (void)i; (void)p;\n";
142 pr " error_count++;\n";
143 pr "}\n\n";
144 pr "#define CHECK(msg, cond) do { \\\n";
145 pr " if (cond) { pass++; } \\\n";
146 pr " else { fail++; fprintf(stderr, \" FAIL: %%s\\n\", msg); } \\\n";
147 pr "} while(0)\n\n";
148 pr "int main(void) {\n";
149 pr " int failures = 0;\n";
150 List.iter (emit_schema_tests ppf ~outdir) schemas;
151 pr "\n if (failures == 0)\n";
152 pr " printf(\"All tests passed.\\n\");\n";
153 pr " else\n";
154 pr " printf(\"%%d test(s) failed.\\n\", failures);\n";
155 pr " return failures ? 1 : 0;\n";
156 pr "}\n";
157 Format.pp_print_flush ppf ();
158 close_out oc
159
160let ensure_dir outdir =
161 try Unix.mkdir outdir 0o755 with Unix.Unix_error (Unix.EEXIST, _, _) -> ()
162
163let generate_3d ~outdir schemas =
164 ensure_dir outdir;
165 generate_3d_files ~outdir schemas
166
167let generate_c ~outdir schemas =
168 ensure_dir outdir;
169 if has_3d_exe () then begin
170 run_everparse ~outdir schemas;
171 generate_test ~outdir schemas
172 end
173 else
174 failwith
175 "3d.exe not found in PATH. Install EverParse to regenerate C files."
176
177let generate ~outdir schemas =
178 generate_3d ~outdir schemas;
179 generate_c ~outdir schemas
180
181let generate_dune ~outdir ~package schemas =
182 let oc = open_out (Filename.concat outdir "dune.inc") in
183 let ppf = Format.formatter_of_out_channel oc in
184 let pr fmt = Fmt.pf ppf fmt in
185 let names = List.map (fun s -> s.name) schemas in
186 let c_files = List.concat_map (fun n -> [ n ^ ".h"; n ^ ".c" ]) names in
187 let three_d_files = List.map (fun n -> n ^ ".3d") names in
188 let test_bin =
189 "test_" ^ String.map (fun c -> if c = '-' then '_' else c) package
190 in
191 (* Rule: ml → .3d *)
192 pr "(rule\n";
193 pr " (alias gen)\n";
194 pr " (mode promote)\n";
195 pr " (targets %s)\n" (String.concat " " three_d_files);
196 pr " (deps gen.exe)\n";
197 pr " (action\n";
198 pr " (run ./gen.exe 3d)))\n\n";
199 (* Rule: .3d → C (fallback: use existing promoted files unless deleted) *)
200 pr "(rule\n";
201 pr " (alias gen)\n";
202 pr " (mode fallback)\n";
203 pr " (targets EverParse.h EverParseEndianness.h %s test.c)\n"
204 (String.concat " " c_files);
205 pr " (deps gen.exe %s)\n" (String.concat " " three_d_files);
206 pr " (action\n";
207 pr " (run ./gen.exe c)))\n\n";
208 (* Rule: runtest *)
209 let all_deps =
210 [ "test.c"; "EverParse.h"; "EverParseEndianness.h" ] @ c_files
211 in
212 let c_srcs = List.map (fun n -> n ^ ".c") names in
213 pr "(rule\n";
214 pr " (alias runtest)\n";
215 pr " (deps %s)\n" (String.concat " " all_deps);
216 pr " (action\n";
217 pr " (system\n";
218 pr " \"cc -std=c11 -Wall -Wextra -Werror -o %s test.c %s && ./%s\")))\n\n"
219 test_bin (String.concat " " c_srcs) test_bin;
220 (* Install *)
221 pr "(install\n";
222 pr " (package %s)\n" package;
223 pr " (section lib)\n";
224 pr " (files\n";
225 List.iter (fun f -> pr " (%s as c/%s)\n" f f) three_d_files;
226 List.iter (fun f -> pr " (%s as c/%s)\n" f f) c_files;
227 pr " (EverParse.h as c/EverParse.h)\n";
228 pr " (EverParseEndianness.h as c/EverParseEndianness.h)))\n";
229 Format.pp_print_flush ppf ();
230 close_out oc
231
232let main ~package schemas =
233 match Array.to_list Sys.argv with
234 | [ _; "3d" ] -> generate_3d ~outdir:"." schemas
235 | [ _; "c" ] -> generate_c ~outdir:"." schemas
236 | [ _; "dune" ] -> generate_dune ~outdir:"." ~package schemas
237 | _ -> generate ~outdir:"." schemas