gazagnaire.org
OCaml wire format DSL with EverParse 3D output for verified parsers
1(** Code generation for EverParse differential testing.
2
3 Generates .3d files from Wire schemas, invokes EverParse, and produces C
4 stubs, OCaml externals, and a test runner for comparing OCaml codecs against
5 EverParse-generated C parsers. *)
6
7type schema = {
8 name : string;
9 struct_ : Wire.struct_;
10 module_ : Wire.module_;
11 wire_size : int;
12}
13
14let schema ~name ~struct_ ~module_ =
15 match Wire.size_of_struct struct_ with
16 | Some wire_size -> Some { name; struct_; module_; wire_size }
17 | None -> None
18
19(** {1 EverParse Invocation} *)
20
21let run_everparse ~schema_dir =
22 let cmd =
23 Fmt.str
24 "cd %s && for f in *.3d; do ~/.local/everparse/bin/3d.exe --batch \"$f\" \
25 || exit 1; done"
26 schema_dir
27 in
28 let ret = Sys.command cmd in
29 if ret <> 0 then Fmt.failwith "EverParse failed with code %d" ret
30
31(** {1 Extracting EverParse-generated Function Names}
32
33 EverParse normalizes C identifiers in a way that depends on consecutive
34 uppercase runs (e.g., [SpaceOSFrame] becomes [SpaceOsframe]). Rather than
35 replicating the algorithm, we read the generated header files. *)
36
37let extract_validate_fn ~schema_dir name =
38 let header = Filename.concat schema_dir (name ^ ".h") in
39 let ic = open_in header in
40 let result = ref None in
41 (try
42 while true do
43 let line = input_line ic in
44 let trimmed = String.trim line in
45 if String.length trimmed > 0 && String.contains trimmed '(' then begin
46 let fn = String.sub trimmed 0 (String.index trimmed '(') in
47 let fn = String.trim fn in
48 let has_validate =
49 let vlen = String.length "Validate" in
50 let rec check i =
51 if i + vlen > String.length fn then false
52 else if String.sub fn i vlen = "Validate" then true
53 else check (i + 1)
54 in
55 check 0
56 in
57 if has_validate && fn <> "" && fn.[0] <> '#' && fn.[0] <> '*' then
58 result := Some fn
59 end
60 done
61 with End_of_file -> ());
62 close_in ic;
63 match !result with
64 | Some fn -> fn
65 | None -> Fmt.failwith "Could not find Validate function in %s" header
66
67(** {1 Code Generation} *)
68
69let generate_3d_files ~schema_dir schemas =
70 List.iter
71 (fun s ->
72 Wire.to_3d_file (Filename.concat schema_dir (s.name ^ ".3d")) s.module_)
73 schemas
74
75let generate_c_stubs ~schema_dir ~outdir schemas =
76 let oc = open_out (Filename.concat outdir "stubs.c") in
77 let ppf = Format.formatter_of_out_channel oc in
78 let pr fmt = Fmt.pf ppf fmt in
79 pr "#include <caml/mlvalues.h>\n";
80 pr "#include <caml/memory.h>\n";
81 pr "#include <caml/alloc.h>\n";
82 pr "#include <stdint.h>\n\n";
83 pr "#include \"%s/EverParse.h\"\n\n" schema_dir;
84 pr "static void noop_error_handler(\n";
85 pr " const char *t, const char *f, const char *r,\n";
86 pr " uint64_t c, uint8_t *ctx, EVERPARSE_INPUT_BUFFER i, uint64_t p) {\n";
87 pr " (void)t; (void)f; (void)r; (void)c; (void)ctx; (void)i; (void)p;\n";
88 pr "}\n\n";
89 List.iter
90 (fun s ->
91 let validate_fn = extract_validate_fn ~schema_dir s.name in
92 let lower = String.lowercase_ascii s.name in
93 pr "/* --- %s --- */\n" s.name;
94 pr "#include \"%s/%s.h\"\n" schema_dir s.name;
95 pr "#include \"%s/%s.c\"\n" schema_dir s.name;
96 pr
97 "void %sEverParseError(const char *s, const char *f, const char *r) { \
98 (void)s; (void)f; (void)r; }\n"
99 s.name;
100 pr "CAMLprim value caml_%s_check(value v_bytes) {\n" lower;
101 pr " CAMLparam1(v_bytes);\n";
102 pr " uint8_t *data = (uint8_t *)Bytes_val(v_bytes);\n";
103 pr " uint32_t len = caml_string_length(v_bytes);\n";
104 pr " uint64_t result = %s(NULL, noop_error_handler, data, len, 0);\n"
105 validate_fn;
106 pr " CAMLreturn(Val_bool(EverParseIsSuccess(result)));\n";
107 pr "}\n\n")
108 schemas;
109 Format.pp_print_flush ppf ();
110 close_out oc
111
112let generate_ml_stubs ~outdir schemas =
113 let oc = open_out (Filename.concat outdir "stubs.ml") in
114 let ppf = Format.formatter_of_out_channel oc in
115 let pr fmt = Fmt.pf ppf fmt in
116 List.iter
117 (fun s ->
118 let lower = String.lowercase_ascii s.name in
119 pr "external %s_check : bytes -> bool = \"caml_%s_check\"\n" lower lower)
120 schemas;
121 Format.pp_print_flush ppf ();
122 close_out oc
123
124let generate_test_runner ~outdir ?(num_values = 1000) schemas =
125 let oc = open_out (Filename.concat outdir "diff_test.ml") in
126 let ppf = Format.formatter_of_out_channel oc in
127 let pr fmt = Fmt.pf ppf fmt in
128 pr "(* Auto-generated differential test runner *)\n\n";
129 pr "let num_values = %d\n\n" num_values;
130 pr "type schema = {\n";
131 pr " name : string;\n";
132 pr " wire_size : int;\n";
133 pr " c_check : bytes -> bool;\n";
134 pr "}\n\n";
135 pr "let schemas = [\n";
136 List.iter
137 (fun s ->
138 let lower = String.lowercase_ascii s.name in
139 pr " { name = %S; wire_size = %d; c_check = Stubs.%s_check };\n" s.name
140 s.wire_size lower)
141 schemas;
142 pr "]\n\n";
143 pr "let () =\n";
144 pr " let seed = 42 in\n";
145 pr " let rng = Random.State.make [| seed |] in\n";
146 pr " let total_tests = ref 0 in\n";
147 pr " let passed = ref 0 in\n";
148 pr " List.iter (fun schema ->\n";
149 pr " let valid = ref 0 in\n";
150 pr " let invalid = ref 0 in\n";
151 pr " for _ = 1 to num_values do\n";
152 pr " let buf = Bytes.create schema.wire_size in\n";
153 pr " for i = 0 to schema.wire_size - 1 do\n";
154 pr " Bytes.set buf i (Char.chr (Random.State.int rng 256))\n";
155 pr " done;\n";
156 pr " let c_ok = schema.c_check buf in\n";
157 pr " incr total_tests;\n";
158 pr " if c_ok then incr valid else incr invalid;\n";
159 pr " incr passed\n";
160 pr " done;\n";
161 pr
162 " Printf.printf \"%%s: %%d valid, %%d invalid (of %%d)\\n\" schema.name \
163 !valid !invalid num_values\n";
164 pr " ) schemas;\n";
165 pr
166 " Printf.printf \"Tested %%d values across %%d schemas\\n\" !total_tests \
167 (List.length schemas);\n";
168 pr " Printf.printf \"All %%d tests passed\\n\" !passed\n";
169 Format.pp_print_flush ppf ();
170 close_out oc
171
172(** {1 Full Pipeline} *)
173
174let generate ~schema_dir ~outdir ?(num_values = 1000) schemas =
175 (try Unix.mkdir schema_dir 0o755
176 with Unix.Unix_error (Unix.EEXIST, _, _) -> ());
177 generate_3d_files ~schema_dir schemas;
178 Fmt.pr "Generated %d .3d files in %s/\n" (List.length schemas) schema_dir;
179 run_everparse ~schema_dir;
180 generate_c_stubs ~schema_dir ~outdir schemas;
181 generate_ml_stubs ~outdir schemas;
182 generate_test_runner ~outdir ~num_values schemas;
183 Fmt.pr "Generated stubs.c, stubs.ml, diff_test.ml\n"