gazagnaire.org
OCaml wire format DSL with EverParse 3D output for verified parsers
1(** Generic differential testing: OCaml codec vs wire-generated C code.
2
3 Each schema needs [c_read] and [c_write] functions (generated by
4 {!Wire.to_c_stubs} and {!Wire.to_ml_stub}). All diff logic is generic over
5 any record codec. *)
6
7type 'r schema = {
8 name : string;
9 c_read : string -> string option;
10 c_write : string -> string option;
11 equal : 'r -> 'r -> bool;
12 codec_decode : bytes -> int -> 'r;
13 codec_encode : 'r -> bytes -> int -> unit;
14 wire_size : int;
15}
16
17let schema ~name ~codec ~c_read ~c_write ~equal =
18 let wire_size = Wire.Codec.wire_size codec in
19 {
20 name;
21 c_read;
22 c_write;
23 equal;
24 codec_decode = Wire.Codec.decode codec;
25 codec_encode = Wire.Codec.encode codec;
26 wire_size;
27 }
28
29type result =
30 | Match
31 | Both_failed
32 | Value_mismatch of string
33 | Only_c_ok of string
34 | Only_ocaml_ok of string
35
36let c_roundtrip schema buf =
37 match schema.c_read buf with
38 | None -> None
39 | Some fields -> schema.c_write fields
40
41let encode_to_string schema v =
42 let buf = Bytes.create schema.wire_size in
43 schema.codec_encode v buf 0;
44 Bytes.unsafe_to_string buf
45
46let decode_from_string schema s = schema.codec_decode (Bytes.of_string s) 0
47
48let read schema buf =
49 let c_result = c_roundtrip schema buf in
50 let buf_too_short = String.length buf < schema.wire_size in
51 let ocaml_result =
52 if String.length buf = 0 || buf_too_short then None
53 else Some (decode_from_string schema buf)
54 in
55 match (c_result, ocaml_result) with
56 | Some c_bytes, Some v ->
57 let ocaml_bytes = encode_to_string schema v in
58 if c_bytes = ocaml_bytes then Match
59 else Value_mismatch "roundtrip bytes differ"
60 | None, None -> Both_failed
61 | Some _, None -> Only_c_ok "OCaml decode returned empty"
62 | None, Some _ -> Only_ocaml_ok "C roundtrip failed"
63
64let write schema value =
65 let ocaml_bytes = encode_to_string schema value in
66 match c_roundtrip schema ocaml_bytes with
67 | Some c_bytes ->
68 if c_bytes = ocaml_bytes then Match
69 else Value_mismatch "C roundtrip bytes differ from OCaml encoding"
70 | None -> Only_ocaml_ok "C rejected OCaml-encoded bytes"
71
72let full_roundtrip schema value =
73 let ocaml_bytes = encode_to_string schema value in
74 match c_roundtrip schema ocaml_bytes with
75 | None -> Only_c_ok "C rejected OCaml-encoded bytes"
76 | Some c_bytes ->
77 let final = decode_from_string schema c_bytes in
78 if schema.equal value final then Match
79 else Value_mismatch "values differ after full roundtrip"
80
81let roundtrip_struct s buf =
82 match Wire.read_struct s buf with
83 | Error e -> Error e
84 | Ok ps -> Wire.write_struct s ps
85
86type packed_test = {
87 name : string;
88 wire_size : int;
89 test_read : string -> result;
90 test_write : string -> result;
91 test_roundtrip : string -> result;
92}
93
94let pack (type r) (schema : r schema) ~wire_size =
95 let decode_value buf =
96 let padded =
97 if String.length buf >= wire_size then String.sub buf 0 wire_size
98 else
99 let b = Bytes.make wire_size '\000' in
100 Bytes.blit_string buf 0 b 0 (String.length buf);
101 Bytes.to_string b
102 in
103 if String.length padded = 0 then None
104 else Some (decode_from_string schema padded)
105 in
106 {
107 name = schema.name;
108 wire_size;
109 test_read = (fun buf -> read schema buf);
110 test_write =
111 (fun buf ->
112 match decode_value buf with
113 | Some v -> write schema v
114 | None -> Both_failed);
115 test_roundtrip =
116 (fun buf ->
117 match decode_value buf with
118 | Some v -> full_roundtrip schema v
119 | None -> Both_failed);
120 }