gazagnaire.org
OCaml wire format DSL with EverParse 3D output for verified parsers
feat(wire.c): extract verified C libraries for all CCSDS protocols via EverParse
Add wire.c library with generate_3d (pure OCaml, fast) and generate_c
(EverParse pipeline, slow) split so dune only re-runs EverParse when
.3d schemas change. Build rules, tests, and install stanzas are generated
into dune.inc to minimize per-package boilerplate.
Each package gets a self-contained C library (header + single .c file)
with ~2000 validation tests covering position tracking, truncation,
boundary conditions, and fuzz.
+185
-67
+157
-58
lib/c/wire_c.ml
+157
-58
lib/c/wire_c.ml
···
10
10
Wire.to_3d_file (Filename.concat outdir (s.name ^ ".3d")) s.module_)
11
11
schemas
12
12
13
+
let 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
+
23
+
let find_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
+
29
+
let 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 = find_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 failwith (Fmt.str "Cannot find EverParseEndianness.h at %s" src)
36
+
end
37
+
13
38
let run_everparse ~outdir schemas =
14
39
List.iter
15
40
(fun s ->
···
18
43
let ret = Sys.command cmd in
19
44
if ret <> 0 then
20
45
failwith (Fmt.str "EverParse failed on %s with code %d" f ret))
21
-
schemas
46
+
schemas;
47
+
copy_everparse_endianness ~outdir
22
48
23
49
(** Extract the validate function name from an EverParse-generated header.
24
50
···
62
88
pr "#include <stdlib.h>\n";
63
89
pr "#include <stdint.h>\n";
64
90
pr "#include <string.h>\n";
65
-
pr "#include \"EverParse.h\"\n\n";
66
-
pr "static void noop_error_handler(\n";
67
-
pr " const char *t, const char *f, const char *r,\n";
68
-
pr " uint64_t c, uint8_t *ctx, EVERPARSE_INPUT_BUFFER i, uint64_t p) {\n";
91
+
pr "#include \"EverParse.h\"\n";
92
+
List.iter (fun s -> pr "#include \"%s.h\"\n" s.name) schemas;
93
+
pr "\nstatic int error_count;\n\n";
94
+
pr "static void counting_error_handler(\n";
95
+
pr " EVERPARSE_STRING t, EVERPARSE_STRING f, EVERPARSE_STRING r,\n";
96
+
pr " uint64_t c, uint8_t *ctx, uint8_t *i, uint64_t p) {\n";
69
97
pr " (void)t; (void)f; (void)r; (void)c; (void)ctx; (void)i; (void)p;\n";
70
-
pr "}\n\n";
71
-
List.iter
72
-
(fun s ->
73
-
pr "#include \"%s.h\"\n" s.name;
74
-
pr "#include \"%s.c\"\n" s.name;
75
-
pr
76
-
"void %sEverParseError(const char *s, const char *f, const char *r) { \
77
-
(void)s; (void)f; (void)r; }\n\n"
78
-
s.name)
79
-
schemas;
80
-
pr "static int test_validate(const char *name,\n";
81
-
pr
82
-
" uint64_t (*validate)(uint8_t *, void (*)(const char *, const char *, \
83
-
const char *, uint64_t, uint8_t *, EVERPARSE_INPUT_BUFFER, uint64_t), \
84
-
uint8_t *, uint32_t, uint64_t),\n";
85
-
pr " uint32_t wire_size) {\n";
86
-
pr " int pass = 0, fail = 0;\n";
87
-
pr " uint8_t *buf = calloc(wire_size, 1);\n";
88
-
pr " if (!buf) return 1;\n\n";
89
-
pr " /* zero-filled buffer should validate */\n";
90
-
pr " uint64_t r = validate(NULL, noop_error_handler, buf, wire_size, 0);\n";
91
-
pr " if (EverParseIsSuccess(r)) pass++; else fail++;\n\n";
92
-
pr " /* truncated buffer should fail */\n";
93
-
pr " if (wire_size > 0) {\n";
94
-
pr " r = validate(NULL, noop_error_handler, buf, wire_size - 1, 0);\n";
95
-
pr " if (!EverParseIsSuccess(r)) pass++; else fail++;\n";
96
-
pr " }\n\n";
97
-
pr " /* random buffers: ensure no crash */\n";
98
-
pr " srand(42);\n";
99
-
pr " for (int i = 0; i < 1000; i++) {\n";
100
-
pr " for (uint32_t j = 0; j < wire_size; j++)\n";
101
-
pr " buf[j] = (uint8_t)(rand() & 0xff);\n";
102
-
pr " r = validate(NULL, noop_error_handler, buf, wire_size, 0);\n";
103
-
pr " (void)r;\n";
104
-
pr " pass++;\n";
105
-
pr " }\n\n";
106
-
pr " free(buf);\n";
107
-
pr " printf(\"%%s: %%d passed, %%d failed\\n\", name, pass, fail);\n";
108
-
pr " return fail;\n";
98
+
pr " error_count++;\n";
109
99
pr "}\n\n";
100
+
pr "#define CHECK(msg, cond) do { \\\n";
101
+
pr " if (cond) { pass++; } \\\n";
102
+
pr " else { fail++; fprintf(stderr, \" FAIL: %%s\\n\", msg); } \\\n";
103
+
pr "} while(0)\n\n";
110
104
pr "int main(void) {\n";
111
105
pr " int failures = 0;\n";
112
106
List.iter
113
107
(fun s ->
114
108
let validate_fn = extract_validate_fn ~outdir s.name in
115
-
pr " failures += test_validate(\"%s\", %s, %d);\n" s.name validate_fn
116
-
s.wire_size)
109
+
let lower = String.lowercase_ascii s.name in
110
+
pr "\n /* %s (%d bytes) */\n" s.name s.wire_size;
111
+
pr " {\n";
112
+
pr " int pass = 0, fail = 0;\n";
113
+
pr " uint8_t buf[%d];\n" s.wire_size;
114
+
pr " uint64_t r;\n\n";
115
+
(* Test 1: zero-filled buffer validates *)
116
+
pr " memset(buf, 0, %d);\n" s.wire_size;
117
+
pr " r = %s(NULL, counting_error_handler, buf, %d, 0);\n" validate_fn
118
+
s.wire_size;
119
+
pr " CHECK(\"zero buffer validates\", EverParseIsSuccess(r));\n";
120
+
pr " CHECK(\"position advanced to %d\", r == %d);\n" s.wire_size
121
+
s.wire_size;
122
+
pr "\n";
123
+
(* Test 2: exact size with non-zero start position *)
124
+
pr " r = %s(NULL, counting_error_handler, buf, %d, 0);\n" validate_fn
125
+
(s.wire_size * 2);
126
+
pr " CHECK(\"larger buffer validates\", EverParseIsSuccess(r));\n";
127
+
pr " CHECK(\"position is %d not %d\", r == %d);\n" s.wire_size
128
+
(s.wire_size * 2) s.wire_size;
129
+
pr "\n";
130
+
(* Test 3: truncated buffers fail *)
131
+
pr " for (uint64_t len = 0; len < %d; len++) {\n" s.wire_size;
132
+
pr " error_count = 0;\n";
133
+
pr " r = %s(NULL, counting_error_handler, buf, len, 0);\n"
134
+
validate_fn;
135
+
pr " CHECK(\"truncated to len fails\", EverParseIsError(r));\n";
136
+
pr " }\n";
137
+
pr "\n";
138
+
(* Test 4: empty input returns error *)
139
+
pr " r = %s(NULL, counting_error_handler, buf, 0, 0);\n" validate_fn;
140
+
pr " CHECK(\"empty input fails\", EverParseIsError(r));\n";
141
+
pr "\n";
142
+
(* Test 5: fuzz — random buffers never crash *)
143
+
pr " srand(42);\n";
144
+
pr " for (int i = 0; i < 1000; i++) {\n";
145
+
pr " for (int j = 0; j < %d; j++)\n" s.wire_size;
146
+
pr " buf[j] = (uint8_t)(rand() & 0xff);\n";
147
+
pr " r = %s(NULL, counting_error_handler, buf, %d, 0);\n" validate_fn
148
+
s.wire_size;
149
+
pr " CHECK(\"random buffer validates\", EverParseIsSuccess(r));\n";
150
+
pr " CHECK(\"random position correct\", r == %d);\n" s.wire_size;
151
+
pr " }\n";
152
+
pr "\n";
153
+
pr " printf(\"%s: %%d passed, %%d failed\\n\", pass, fail);\n" lower;
154
+
pr " failures += fail;\n";
155
+
pr " }\n")
117
156
schemas;
118
-
pr " if (failures == 0)\n";
157
+
pr "\n if (failures == 0)\n";
119
158
pr " printf(\"All tests passed.\\n\");\n";
120
159
pr " else\n";
121
160
pr " printf(\"%%d test(s) failed.\\n\", failures);\n";
122
-
pr " return failures;\n";
161
+
pr " return failures ? 1 : 0;\n";
123
162
pr "}\n";
124
163
close_out oc
125
164
165
+
let ensure_dir outdir =
166
+
try Unix.mkdir outdir 0o755 with Unix.Unix_error (Unix.EEXIST, _, _) -> ()
167
+
168
+
let generate_3d ~outdir schemas =
169
+
ensure_dir outdir;
170
+
generate_3d_files ~outdir schemas
171
+
172
+
let generate_c ~outdir schemas =
173
+
ensure_dir outdir;
174
+
run_everparse ~outdir schemas;
175
+
generate_test ~outdir schemas
176
+
126
177
let generate ~outdir schemas =
127
-
(try Unix.mkdir outdir 0o755 with Unix.Unix_error (Unix.EEXIST, _, _) -> ());
128
-
generate_3d_files ~outdir schemas;
129
-
run_everparse ~outdir schemas;
130
-
generate_test ~outdir schemas;
131
-
(* Clean up intermediate .3d files *)
132
-
List.iter
133
-
(fun s ->
134
-
let f = Filename.concat outdir (s.name ^ ".3d") in
135
-
try Unix.unlink f with Unix.Unix_error _ -> ())
136
-
schemas
178
+
generate_3d ~outdir schemas;
179
+
generate_c ~outdir schemas
180
+
181
+
let generate_dune ~outdir ~package schemas =
182
+
let oc = open_out (Filename.concat outdir "dune.inc") in
183
+
let pr fmt = Printf.fprintf oc fmt in
184
+
let names = List.map (fun s -> s.name) schemas in
185
+
let c_files = List.concat_map (fun n -> [ n ^ ".h"; n ^ ".c" ]) names in
186
+
let three_d_files = List.map (fun n -> n ^ ".3d") names in
187
+
let test_bin =
188
+
"test_" ^ String.map (fun c -> if c = '-' then '_' else c) package
189
+
in
190
+
(* Rule: ml → .3d *)
191
+
pr "(rule\n";
192
+
pr " (alias gen)\n";
193
+
pr " (mode promote)\n";
194
+
pr " (targets %s)\n" (String.concat " " three_d_files);
195
+
pr " (deps gen.exe)\n";
196
+
pr " (action\n";
197
+
pr " (run ./gen.exe 3d)))\n\n";
198
+
(* Rule: .3d → C *)
199
+
pr "(rule\n";
200
+
pr " (alias gen)\n";
201
+
pr " (mode promote)\n";
202
+
pr " (targets EverParse.h EverParseEndianness.h %s test.c)\n"
203
+
(String.concat " " c_files);
204
+
pr " (deps gen.exe %s)\n" (String.concat " " three_d_files);
205
+
pr " (action\n";
206
+
pr " (run ./gen.exe c)))\n\n";
207
+
(* Rule: runtest *)
208
+
let all_deps =
209
+
[ "test.c"; "EverParse.h"; "EverParseEndianness.h" ] @ c_files
210
+
in
211
+
let c_srcs = List.map (fun n -> n ^ ".c") names in
212
+
pr "(rule\n";
213
+
pr " (alias runtest)\n";
214
+
pr " (deps %s)\n" (String.concat " " all_deps);
215
+
pr " (action\n";
216
+
pr " (system\n";
217
+
pr " \"cc -std=c11 -Wall -Wextra -Werror -o %s test.c %s && ./%s\")))\n\n"
218
+
test_bin (String.concat " " c_srcs) test_bin;
219
+
(* Install *)
220
+
pr "(install\n";
221
+
pr " (package %s)\n" package;
222
+
pr " (section lib)\n";
223
+
pr " (files\n";
224
+
List.iter (fun f -> pr " (%s as c/%s)\n" f f) three_d_files;
225
+
List.iter (fun f -> pr " (%s as c/%s)\n" f f) c_files;
226
+
pr " (EverParse.h as c/EverParse.h)\n";
227
+
pr " (EverParseEndianness.h as c/EverParseEndianness.h)))\n";
228
+
close_out oc
229
+
230
+
let main ~package schemas =
231
+
match Array.to_list Sys.argv with
232
+
| [ _; "3d" ] -> generate_3d ~outdir:"." schemas
233
+
| [ _; "c" ] -> generate_c ~outdir:"." schemas
234
+
| [ _; "dune" ] -> generate_dune ~outdir:"." ~package schemas
235
+
| _ -> generate ~outdir:"." schemas
+28
-9
lib/c/wire_c.mli
+28
-9
lib/c/wire_c.mli
···
5
5
self-contained C library: [EverParse.h], [<Name>.h], [<Name>.c], and a
6
6
[test.c] that exercises the validators.
7
7
8
-
{b Typical usage:}
8
+
{b Typical usage} ([gen.ml]):
9
9
{[
10
10
let () =
11
-
let outdir = if Array.length Sys.argv > 1 then Sys.argv.(1) else "." in
12
-
Wire_c.generate ~outdir
11
+
Wire_c.main ~package:"clcw"
13
12
[
14
13
Wire_c.schema ~name:"Clcw" ~module_:Clcw.module_
15
14
~wire_size:(Wire.Codec.wire_size Clcw.codec);
16
15
]
17
-
]} *)
16
+
]}
17
+
18
+
With a minimal [dune] that includes the generated rules:
19
+
{v
20
+
(executable (name gen) (modules gen) (libraries clcw wire.c))
21
+
(rule (mode promote) (alias gen)
22
+
(targets dune.inc) (deps gen.exe) (action (run ./gen.exe dune)))
23
+
(include dune.inc)
24
+
v} *)
18
25
19
26
type schema
20
27
(** A schema bundles a name, Wire module, and wire size. *)
···
23
30
(** [schema ~name ~module_ ~wire_size] creates a schema for C library
24
31
generation. *)
25
32
26
-
val generate : outdir:string -> schema list -> unit
27
-
(** [generate ~outdir schemas] runs the full pipeline:
28
-
+ Generates .3d files in [outdir]
29
-
+ Invokes EverParse to produce C parsers
30
-
+ Generates [test.c] that exercises the validators
33
+
val generate_3d : outdir:string -> schema list -> unit
34
+
(** [generate_3d ~outdir schemas] generates [.3d] files from Wire modules. *)
35
+
36
+
val generate_c : outdir:string -> schema list -> unit
37
+
(** [generate_c ~outdir schemas] invokes EverParse on existing [.3d] files to
38
+
produce C parsers and generates [test.c].
31
39
32
40
Requires [3d.exe] (EverParse) in PATH. *)
41
+
42
+
val generate : outdir:string -> schema list -> unit
43
+
(** [generate ~outdir schemas] runs both steps: {!generate_3d} then
44
+
{!generate_c}. *)
45
+
46
+
val main : package:string -> schema list -> unit
47
+
(** [main ~package schemas] dispatches based on [Sys.argv]:
48
+
- [3d] runs {!generate_3d}
49
+
- [c] runs {!generate_c}
50
+
- [dune] generates [dune.inc] with build rules, test, and install stanzas
51
+
- otherwise runs {!generate} *)