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
3val roundtrip_struct :
4 Wire.struct_ -> string -> (string, Wire.parse_error) Stdlib.result
5(** [roundtrip_struct s buf] parses [buf] as struct [s] and re-encodes it.
6 Equivalent to [write_struct s (read_struct s buf)]. *)
7
8type 'r schema
9(** A schema bundles everything needed for differential testing. *)
10
11val schema :
12 name:string ->
13 codec:'r Wire.Codec.t ->
14 c_read:(string -> string option) ->
15 c_write:(string -> string option) ->
16 equal:('r -> 'r -> bool) ->
17 'r schema
18(** [schema ~name ~codec ~c_read ~c_write ~equal] creates a schema. *)
19
20type result =
21 | Match
22 | Both_failed
23 | Value_mismatch of string
24 | Only_c_ok of string
25 | Only_ocaml_ok of string
26
27val read : 'r schema -> string -> result
28(** [read s buf] parses [buf] with both OCaml and C, compares results. *)
29
30val write : 'r schema -> 'r -> result
31(** [write s v] encodes [v] with OCaml, roundtrips through C, compares. *)
32
33val full_roundtrip : 'r schema -> 'r -> result
34(** [full_roundtrip s v] encodes with OCaml, roundtrips through C, decodes with
35 OCaml, and compares the final value to the original. *)
36
37(** {1 Type-erased testing} *)
38
39type packed_test = {
40 name : string;
41 wire_size : int;
42 test_read : string -> result;
43 test_write : string -> result;
44 test_roundtrip : string -> result;
45}
46(** A type-erased test that can be used in generic test loops without knowing
47 the record type. *)
48
49val pack : 'r schema -> wire_size:int -> packed_test
50(** [pack schema ~wire_size] creates a type-erased test from a schema.
51 [test_write] and [test_roundtrip] decode random bytes via the OCaml codec to
52 get a valid value, then run the corresponding diff function. *)