OCaml wire format DSL with EverParse 3D output for verified parsers
feat(wire): add diff-gen library for FFI stub generation
+228
+178
lib/diff-gen/diff_gen.ml
+178
lib/diff-gen/diff_gen.ml
···
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
+
7
+
type schema = {
8
+
name : string;
9
+
struct_ : Wire.struct_;
10
+
module_ : Wire.module_;
11
+
wire_size : int;
12
+
}
13
+
14
+
let schema ~name ~struct_ ~module_ =
15
+
match Wire.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
+
21
+
let 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 failwith (Fmt.str "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
+
37
+
let 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 -> failwith (Fmt.str "Could not find Validate function in %s" header)
66
+
67
+
(** {1 Code Generation} *)
68
+
69
+
let 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
+
75
+
let generate_c_stubs ~schema_dir ~outdir schemas =
76
+
let oc = open_out (Filename.concat outdir "stubs.c") in
77
+
let pr fmt = Printf.fprintf oc fmt in
78
+
pr "#include <caml/mlvalues.h>\n";
79
+
pr "#include <caml/memory.h>\n";
80
+
pr "#include <caml/alloc.h>\n";
81
+
pr "#include <stdint.h>\n\n";
82
+
pr "#include \"%s/EverParse.h\"\n\n" schema_dir;
83
+
pr "static void noop_error_handler(\n";
84
+
pr " const char *t, const char *f, const char *r,\n";
85
+
pr " uint64_t c, uint8_t *ctx, EVERPARSE_INPUT_BUFFER i, uint64_t p) {\n";
86
+
pr " (void)t; (void)f; (void)r; (void)c; (void)ctx; (void)i; (void)p;\n";
87
+
pr "}\n\n";
88
+
List.iter
89
+
(fun s ->
90
+
let validate_fn = extract_validate_fn ~schema_dir s.name in
91
+
let lower = String.lowercase_ascii s.name in
92
+
pr "/* --- %s --- */\n" s.name;
93
+
pr "#include \"%s/%s.h\"\n" schema_dir s.name;
94
+
pr "#include \"%s/%s.c\"\n" schema_dir s.name;
95
+
pr
96
+
"void %sEverParseError(const char *s, const char *f, const char *r) { \
97
+
(void)s; (void)f; (void)r; }\n"
98
+
s.name;
99
+
pr "CAMLprim value caml_%s_check(value v_bytes) {\n" lower;
100
+
pr " CAMLparam1(v_bytes);\n";
101
+
pr " uint8_t *data = (uint8_t *)Bytes_val(v_bytes);\n";
102
+
pr " uint32_t len = caml_string_length(v_bytes);\n";
103
+
pr " uint64_t result = %s(NULL, noop_error_handler, data, len, 0);\n"
104
+
validate_fn;
105
+
pr " CAMLreturn(Val_bool(EverParseIsSuccess(result)));\n";
106
+
pr "}\n\n")
107
+
schemas;
108
+
close_out oc
109
+
110
+
let generate_ml_stubs ~outdir schemas =
111
+
let oc = open_out (Filename.concat outdir "stubs.ml") in
112
+
let pr fmt = Printf.fprintf oc fmt in
113
+
List.iter
114
+
(fun s ->
115
+
let lower = String.lowercase_ascii s.name in
116
+
pr "external %s_check : bytes -> bool = \"caml_%s_check\"\n" lower lower)
117
+
schemas;
118
+
close_out oc
119
+
120
+
let generate_test_runner ~outdir ?(num_values = 1000) schemas =
121
+
let oc = open_out (Filename.concat outdir "diff_test.ml") in
122
+
let pr fmt = Printf.fprintf oc fmt in
123
+
pr "(* Auto-generated differential test runner *)\n\n";
124
+
pr "let num_values = %d\n\n" num_values;
125
+
pr "type schema = {\n";
126
+
pr " name : string;\n";
127
+
pr " wire_size : int;\n";
128
+
pr " c_check : bytes -> bool;\n";
129
+
pr "}\n\n";
130
+
pr "let schemas = [\n";
131
+
List.iter
132
+
(fun s ->
133
+
let lower = String.lowercase_ascii s.name in
134
+
pr " { name = %S; wire_size = %d; c_check = Stubs.%s_check };\n" s.name
135
+
s.wire_size lower)
136
+
schemas;
137
+
pr "]\n\n";
138
+
pr "let () =\n";
139
+
pr " let seed = 42 in\n";
140
+
pr " let rng = Random.State.make [| seed |] in\n";
141
+
pr " let total_tests = ref 0 in\n";
142
+
pr " let passed = ref 0 in\n";
143
+
pr " List.iter (fun schema ->\n";
144
+
pr " let valid = ref 0 in\n";
145
+
pr " let invalid = ref 0 in\n";
146
+
pr " for _ = 1 to num_values do\n";
147
+
pr " let buf = Bytes.create schema.wire_size in\n";
148
+
pr " for i = 0 to schema.wire_size - 1 do\n";
149
+
pr " Bytes.set buf i (Char.chr (Random.State.int rng 256))\n";
150
+
pr " done;\n";
151
+
pr " let c_ok = schema.c_check buf in\n";
152
+
pr " incr total_tests;\n";
153
+
pr " if c_ok then incr valid else incr invalid;\n";
154
+
pr " incr passed\n";
155
+
pr " done;\n";
156
+
pr
157
+
" Printf.printf \"%%s: %%d valid, %%d invalid (of %%d)\\n\" schema.name \
158
+
!valid !invalid num_values\n";
159
+
pr " ) schemas;\n";
160
+
pr
161
+
" Printf.printf \"Tested %%d values across %%d schemas\\n\" !total_tests \
162
+
(List.length schemas);\n";
163
+
pr " Printf.printf \"All %%d tests passed\\n\" !passed\n";
164
+
close_out oc
165
+
166
+
(** {1 Full Pipeline} *)
167
+
168
+
let generate ~schema_dir ~outdir ?(num_values = 1000) schemas =
169
+
(try Unix.mkdir schema_dir 0o755
170
+
with Unix.Unix_error (Unix.EEXIST, _, _) -> ());
171
+
generate_3d_files ~schema_dir schemas;
172
+
Printf.printf "Generated %d .3d files in %s/\n" (List.length schemas)
173
+
schema_dir;
174
+
run_everparse ~schema_dir;
175
+
generate_c_stubs ~schema_dir ~outdir schemas;
176
+
generate_ml_stubs ~outdir schemas;
177
+
generate_test_runner ~outdir ~num_values schemas;
178
+
Printf.printf "Generated stubs.c, stubs.ml, diff_test.ml\n"
+46
lib/diff-gen/diff_gen.mli
+46
lib/diff-gen/diff_gen.mli
···
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
+
7
+
{b Typical usage:}
8
+
{[
9
+
(* In gen_c.ml *)
10
+
let schemas =
11
+
[
12
+
Diff_gen.schema ~name:"MyFrame" ~struct_:My_3d.frame_struct
13
+
~module_:My_3d.frame_module
14
+
|> Option.get;
15
+
]
16
+
17
+
let () = Diff_gen.generate ~schema_dir:"schemas" ~outdir:"." schemas
18
+
]} *)
19
+
20
+
type schema
21
+
(** A schema bundles a Wire struct, module, and computed wire size. *)
22
+
23
+
val schema :
24
+
name:string -> struct_:Wire.struct_ -> module_:Wire.module_ -> schema option
25
+
(** [schema ~name ~struct_ ~module_] creates a schema if the struct has a known
26
+
fixed wire size. Returns [None] for variable-length structs. *)
27
+
28
+
(** {1 Full Pipeline} *)
29
+
30
+
val generate :
31
+
schema_dir:string -> outdir:string -> ?num_values:int -> schema list -> unit
32
+
(** [generate ~schema_dir ~outdir schemas] runs the full pipeline: 1. Generates
33
+
.3d files in [schema_dir] 2. Invokes EverParse to produce C parsers 3.
34
+
Generates [stubs.c], [stubs.ml], [diff_test.ml] in [outdir]
35
+
36
+
Requires EverParse installed at [~/.local/everparse/]. *)
37
+
38
+
(** {1 Individual Steps} *)
39
+
40
+
val generate_3d_files : schema_dir:string -> schema list -> unit
41
+
val run_everparse : schema_dir:string -> unit
42
+
val generate_c_stubs : schema_dir:string -> outdir:string -> schema list -> unit
43
+
val generate_ml_stubs : outdir:string -> schema list -> unit
44
+
45
+
val generate_test_runner :
46
+
outdir:string -> ?num_values:int -> schema list -> unit