gazagnaire.org
OCaml wire format DSL with EverParse 3D output for verified parsers
1(** Schema definitions for differential testing.
2
3 These schemas are used to test that our OCaml parser produces the same
4 results as the EverParse-generated C parser. *)
5
6open Wire
7
8(* Simple header schema: version (u8) + length (u16) + flags (u8) *)
9type simple_header = { version : int; length : int; flags : int }
10
11let simple_header_codec =
12 let open Codec in
13 record "SimpleHeader" (fun version length flags -> { version; length; flags })
14 |+ field "version" uint8 (fun h -> h.version)
15 |+ field "length" uint16 (fun h -> h.length)
16 |+ field "flags" uint8 (fun h -> h.flags)
17 |> seal
18
19(* Generate 3D schema *)
20let simple_header_struct = Codec.to_struct simple_header_codec
21
22let simple_header_module =
23 module_ ~doc:"Simple header for differential testing" "SimpleHeader"
24 [ typedef ~entrypoint:true simple_header_struct ]
25
26(* Constrained schema - constraints are applied in 3D generation,
27 the OCaml parser doesn't validate constraints on individual fields.
28 For differential testing, we validate manually or use the C parser. *)
29type constrained_packet = { pkt_type : int; pkt_length : int }
30
31let constrained_packet_codec =
32 let open Codec in
33 record "ConstrainedPacket" (fun pkt_type pkt_length ->
34 { pkt_type; pkt_length })
35 |+ field "pkt_type" uint8 (fun p -> p.pkt_type)
36 |+ field "pkt_length" uint16 (fun p -> p.pkt_length)
37 |> seal
38
39let constrained_packet_module =
40 module_ ~doc:"Constrained packet for differential testing" "ConstrainedPacket"
41 [ typedef ~entrypoint:true (Codec.to_struct constrained_packet_codec) ]