gazagnaire.org
Solo5 hvt ABI and MFT1/ABI1 note format as wire codecs
9.5 kB
252 lines
1(* hvt ABI: the contract between the tender and a Solo5 hvt-ABI unikernel,
2 mirroring Solo5's include/hvt_abi.h and the aarch64 guest layout in
3 tenders/hvt/hvt_cpu_aarch64.h. The pinned upstream headers are vendored for
4 reference by scripts/import.ml; the structured fields use wire codecs. *)
5
6let version = 2
7
8(* {1 Hypercalls} *)
9
10type hypercall =
11 | Walltime
12 | Puts
13 | Poll
14 | Block_write
15 | Block_read
16 | Net_write
17 | Net_read
18 | Halt
19
20let hypercall_of_int = function
21 | 1 -> Some Walltime
22 | 2 -> Some Puts
23 | 3 -> Some Poll
24 | 4 -> Some Block_write
25 | 5 -> Some Block_read
26 | 6 -> Some Net_write
27 | 7 -> Some Net_read
28 | 8 -> Some Halt
29 | _ -> None
30
31let hypercall_max = 9 (* HVT_HYPERCALL_MAX *)
32
33(* {1 aarch64 guest layout} (hvt_cpu_aarch64.h)
34
35 RAM occupies [0, 4GB); the hypercall MMIO window starts at [mmio_base]. A
36 32-bit store to [hypercall_address nr] is left unmapped at stage 2, so it
37 faults and the tender services hypercall [nr]. *)
38
39let guest_min_base = 0x100000
40let boot_info_base = 0x10000
41let mmio_base = 0x100000000
42let mmio_size = 0x40000000
43
44(* The virtio-mmio device region, a device IPA just past the hypercall window.
45 Mapped device in the guest stage-1 tables but left unbacked, so an access
46 faults to the tender, which services it as a virtio-mmio register access. *)
47let virtio_base = mmio_base + mmio_size
48let virtio_size = 0x1000
49let guest_block_size = 0x200000
50let hypercall_address nr = mmio_base + (nr lsl 3)
51let hypercall_nr ipa = (ipa - mmio_base) asr 3
52
53(* The register offset of an access at guest-physical [ipa] in the virtio
54 region. *)
55let virtio_offset ipa = ipa - virtio_base
56let in_virtio ipa = ipa >= virtio_base && ipa < virtio_base + virtio_size
57
58(* Page-table region the tender writes into guest memory. *)
59let pgd_base = 0x1000
60let pud_base = 0x2000
61let pmd_base = 0x3000
62let pte_base = 0x7000
63
64(* {1 boot_info} (hvt_boot_info; a pointer to it is passed to the guest in
65 x0) *)
66
67type boot_info = {
68 mem_size : int64;
69 kernel_end : int64;
70 cpu_cycle_freq : int64;
71 cmdline : int64; (** Guest pointer to the command-line C string. *)
72 mft : int64; (** Guest pointer to the application manifest. *)
73 host_features : Optint.t;
74 (** Feature bits the tender offers, HVT_FEATURE_ ones. *)
75 guest_features : Optint.t; (** Feature bits the guest accepted. *)
76 net_ring : int64; (** Guest pointer to the net ring, 0 when not offered. *)
77}
78
79(* HVT_FEATURE_RING_IO: eventfd-kicked shared-ring net I/O. The tenders here
80 never offer it (host_features stays 0), so guests use hypercall I/O. *)
81let feature_ring_io = Optint.one
82
83let boot_info_codec =
84 Wire.Codec.v "Hvt_boot_info"
85 ~doc:
86 "Solo5 hvt ABI (struct hvt_boot_info): the boot record the tender places \
87 in guest memory and passes to the guest in x0 -- the RAM size, the \
88 kernel end address, the CPU cycle frequency, guest pointers to the \
89 command line and the application manifest, and the ring-I/O feature \
90 negotiation fields (host offer, guest acceptance, net ring address)."
91 (fun mem_size kernel_end cpu_cycle_freq cmdline mft host_features
92 guest_features net_ring ->
93 {
94 mem_size;
95 kernel_end;
96 cpu_cycle_freq;
97 cmdline;
98 mft;
99 host_features;
100 guest_features;
101 net_ring;
102 })
103 Wire.Codec.
104 [
105 (Wire.Field.v "mem_size" Wire.uint64 $ fun (b : boot_info) -> b.mem_size);
106 ( Wire.Field.v "kernel_end" Wire.uint64 $ fun (b : boot_info) ->
107 b.kernel_end );
108 ( Wire.Field.v "cpu_cycle_freq" Wire.uint64 $ fun (b : boot_info) ->
109 b.cpu_cycle_freq );
110 (Wire.Field.v "cmdline" Wire.uint64 $ fun (b : boot_info) -> b.cmdline);
111 (Wire.Field.v "mft" Wire.uint64 $ fun (b : boot_info) -> b.mft);
112 ( Wire.Field.v "host_features" Wire.uint32 $ fun (b : boot_info) ->
113 b.host_features );
114 ( Wire.Field.v "guest_features" Wire.uint32 $ fun (b : boot_info) ->
115 b.guest_features );
116 (Wire.Field.v "net_ring" Wire.uint64 $ fun (b : boot_info) -> b.net_ring);
117 ]
118
119(* sizeof(struct hvt_boot_info): five 64-bit fields, two 32-bit feature words,
120 and the 64-bit net-ring pointer -- no padding under aarch64 natural
121 alignment. Solo5's hvt_boot_info_init packs the manifest and command line
122 contiguously after the boot info in low memory, so this is also the offset
123 from [boot_info_base] to the manifest. *)
124let boot_info_size = (8 * 5) + (4 * 2) + 8
125
126(* {1 Hypercall argument structs}
127
128 Each lives in guest memory; the tender reads (and for OUT fields, writes)
129 them at the gpa the guest passes. Guest pointers and [size_t] are 64-bit. *)
130
131(* HVT_HYPERCALL_WALLTIME: OUT nsecs. *)
132type hc_walltime = { nsecs : int64 }
133
134let hc_walltime_codec =
135 Wire.Codec.v "Hvt_hc_walltime"
136 ~doc:
137 "Solo5 hvt ABI: the HVT_HYPERCALL_WALLTIME argument struct -- the OUT \
138 field carrying the current wall-clock time in nanoseconds the tender \
139 writes back to the guest."
140 (fun nsecs -> { nsecs })
141 Wire.Codec.
142 [ (Wire.Field.v "nsecs" Wire.uint64 $ fun (h : hc_walltime) -> h.nsecs) ]
143
144(* HVT_HYPERCALL_PUTS: IN data (guest pointer), len. *)
145type hc_puts = { data : int64; len : int64 }
146
147let hc_puts_codec =
148 Wire.Codec.v "Hvt_hc_puts"
149 ~doc:
150 "Solo5 hvt ABI: the HVT_HYPERCALL_PUTS argument struct -- the IN guest \
151 pointer to the bytes to write to the console and their length."
152 (fun data len -> { data; len })
153 Wire.Codec.
154 [
155 (Wire.Field.v "data" Wire.uint64 $ fun (h : hc_puts) -> h.data);
156 (Wire.Field.v "len" Wire.uint64 $ fun (h : hc_puts) -> h.len);
157 ]
158
159(* HVT_HYPERCALL_POLL: IN timeout_nsecs; OUT ready_set, ret. *)
160type hc_poll = { timeout_nsecs : int64; ready_set : int64; ret : int }
161
162let hc_poll_codec =
163 Wire.Codec.v "Hvt_hc_poll"
164 ~doc:
165 "Solo5 hvt ABI: the HVT_HYPERCALL_POLL argument struct -- the IN timeout \
166 in nanoseconds and the OUT bitset of devices that became ready and the \
167 return code the tender writes back."
168 (fun timeout_nsecs ready_set ret _pad -> { timeout_nsecs; ready_set; ret })
169 Wire.Codec.
170 [
171 ( Wire.Field.v "timeout_nsecs" Wire.uint64 $ fun (h : hc_poll) ->
172 h.timeout_nsecs );
173 (Wire.Field.v "ready_set" Wire.uint64 $ fun (h : hc_poll) -> h.ready_set);
174 (Wire.Field.v "ret" Wire.int32 $ fun (h : hc_poll) -> h.ret);
175 (Wire.Field.v "_pad" Wire.int32 $ fun _ -> 0);
176 ]
177
178(* HVT_HYPERCALL_HALT: IN cookie (guest pointer), exit_status. *)
179type hc_halt = { cookie : int64; exit_status : int }
180
181let hc_halt_codec =
182 Wire.Codec.v "Hvt_hc_halt"
183 ~doc:
184 "Solo5 hvt ABI: the HVT_HYPERCALL_HALT argument struct -- the IN guest \
185 pointer to a diagnostic cookie and the exit status the guest halts \
186 with."
187 (fun cookie exit_status _pad -> { cookie; exit_status })
188 Wire.Codec.
189 [
190 (Wire.Field.v "cookie" Wire.uint64 $ fun (h : hc_halt) -> h.cookie);
191 ( Wire.Field.v "exit_status" Wire.int32 $ fun (h : hc_halt) ->
192 h.exit_status );
193 (Wire.Field.v "_pad" Wire.int32 $ fun _ -> 0);
194 ]
195
196(* HVT_HYPERCALL_NET_WRITE / NET_READ share a layout: a device handle, a guest
197 pointer to the frame, its length (in/out for read), and a result. *)
198type hc_net = { handle : int64; data : int64; len : int64; ret : int }
199
200(* [ret] is a C [int] (signed 32-bit), represented directly by [Wire.int32]. *)
201
202let hc_net_codec =
203 Wire.Codec.v "Hvt_hc_net"
204 ~doc:
205 "Solo5 hvt ABI: the HVT_HYPERCALL_NET_WRITE / NET_READ argument struct \
206 -- the network device handle, the guest pointer to the frame, its \
207 length (in, and out for read), and the signed result code."
208 (fun handle data len ret _pad -> { handle; data; len; ret })
209 Wire.Codec.
210 [
211 (Wire.Field.v "handle" Wire.uint64 $ fun (h : hc_net) -> h.handle);
212 (Wire.Field.v "data" Wire.uint64 $ fun (h : hc_net) -> h.data);
213 (Wire.Field.v "len" Wire.uint64 $ fun (h : hc_net) -> h.len);
214 (Wire.Field.v "ret" Wire.int32 $ fun (h : hc_net) -> h.ret);
215 (Wire.Field.v "_pad" Wire.int32 $ fun _ -> 0);
216 ]
217
218(* {1 Result codes} (solo5.h solo5_result_t) *)
219
220let solo5_r_ok = 0
221let solo5_r_again = 1
222let solo5_r_einval = 2
223let solo5_r_eunspec = 3
224
225(* HVT_HYPERCALL_BLOCK_WRITE / BLOCK_READ share a layout: a device handle, a
226 byte offset, a guest pointer to the buffer, its length (in/out for read), and
227 a result. *)
228type hc_block = {
229 handle : int64;
230 offset : int64;
231 data : int64;
232 len : int64;
233 ret : int;
234}
235
236let hc_block_codec =
237 Wire.Codec.v "Hvt_hc_block"
238 ~doc:
239 "Solo5 hvt ABI: the HVT_HYPERCALL_BLOCK_WRITE / BLOCK_READ argument \
240 struct -- the block device handle, the byte offset, the guest pointer \
241 to the buffer, its length (in, and out for read), and the signed result \
242 code."
243 (fun handle offset data len ret _pad -> { handle; offset; data; len; ret })
244 Wire.Codec.
245 [
246 (Wire.Field.v "handle" Wire.uint64 $ fun (h : hc_block) -> h.handle);
247 (Wire.Field.v "offset" Wire.uint64 $ fun (h : hc_block) -> h.offset);
248 (Wire.Field.v "data" Wire.uint64 $ fun (h : hc_block) -> h.data);
249 (Wire.Field.v "len" Wire.uint64 $ fun (h : hc_block) -> h.len);
250 (Wire.Field.v "ret" Wire.int32 $ fun (h : hc_block) -> h.ret);
251 (Wire.Field.v "_pad" Wire.int32 $ fun _ -> 0);
252 ]