gazagnaire.org
Solo5 hvt ABI and MFT1/ABI1 note format as wire codecs
6.0 kB
135 lines
1(** The hypervisor boundary a tender backend supplies.
2
3 The aarch64 hvt tender core ({!Cpu}, {!Tender}) is a functor over this
4 signature: it sets up the boot block, page tables and CPU state and drives
5 the guest, while a backend (solo5-hvf on Hypervisor.framework, solo5-kvm on
6 Linux [/dev/kvm]) provides the single VM, its registers, and the run/exit
7 boundary. The register selectors and the {!exit} are normalised here so the
8 core is identical across backends -- a backend that decodes an exception
9 syndrome (HVF) and one whose hypervisor hands back the MMIO access already
10 decoded (KVM) both present the same {!Mmio}. *)
11
12type reg = X of int (** [x0]-[x30] *) | Pc | Cpsr (** A core register. *)
13
14type sysreg =
15 | Sctlr_el1
16 | Mair_el1
17 | Tcr_el1
18 | Ttbr0_el1
19 | Cpacr_el1
20 | Sp_el1 (** A system register. *)
21
22type exit =
23 | Mmio
24 (** A guest MMIO access. Its details are read after the fact through the
25 allocation-free accessors [mmio_addr] and [mmio_write], so an exit
26 carries no payload and the boundary allocates nothing per exit. *)
27 | Vtimer (** The virtual timer fired. *)
28 | Canceled (** The run was interrupted (a delivered signal). *)
29 | Fatal
30 (** An exit the core cannot service (an unexpected exception or a
31 hypervisor entry failure); the diagnostic is read with
32 [fatal_message]. *)
33
34exception Backend_error of string
35(** Raised when a backend's hypervisor call fails; the message names the call
36 and the failure. *)
37
38val reg_code : reg -> int
39(** [reg_code r] is the small integer a backend's C stub maps to its native core
40 register. *)
41
42val sysreg_code : sysreg -> int
43(** [sysreg_code r] is the small integer a backend's C stub maps to its native
44 system register. *)
45
46(** A tender backend: the single VM and vCPU, its registers, and the run/exit
47 boundary the {!Cpu} and {!Tender} functors drive. *)
48module type S = sig
49 val init : bytes:int -> Guest.t
50 (** [init ~bytes] creates the VM and vCPU and maps [bytes] of guest RAM at
51 guest-physical address 0, returning a view of it. Raises {!Backend_error}
52 on failure. *)
53
54 val set_reg : reg -> int64 -> unit
55 (** [set_reg r v] sets core register [r] to [v]. *)
56
57 val reg : reg -> int64
58 (** [reg r] reads core register [r]. *)
59
60 val set_sysreg : sysreg -> int64 -> unit
61 (** [set_sysreg r v] sets system register [r] to [v]. *)
62
63 val sysreg : sysreg -> int64
64 (** [sysreg r] reads system register [r]. *)
65
66 val counter_frequency : unit -> int64
67 (** [counter_frequency ()] is the host counter frequency (CNTFRQ_EL0) in Hz.
68 *)
69
70 val run : unit -> exit
71 (** [run ()] enters the guest and returns at the next VM exit, normalised to
72 an {!exit}. The exit is a constant constructor, and the MMIO details are
73 read through {!mmio_addr} / {!mmio_write} and a fatal diagnostic through
74 {!fatal_message}, so the run boundary allocates nothing per exit. *)
75
76 val mmio_addr : unit -> int
77 (** [mmio_addr ()] is the guest-physical address of the access {!run} last
78 reported as {!Mmio}. *)
79
80 val mmio_write : unit -> int
81 (** [mmio_write ()] is the value of the {!Mmio} access {!run} last reported: a
82 32-bit store value, or [-1] for a load (whose result {!complete}
83 supplies). *)
84
85 val fatal_message : unit -> string
86 (** [fatal_message ()] is the diagnostic for the exit {!run} last reported as
87 {!Fatal}. *)
88
89 val complete : read:int -> unit
90 (** [complete ~read] finishes servicing the current {!Mmio} and prepares the
91 vCPU to resume: for a load, [read] is the value the load reads back; for a
92 store (or any access with no value to return) it is [-1]. *)
93
94 val mask_vtimer : bool -> unit
95 (** [mask_vtimer m] masks ([true]) or unmasks the virtual timer. *)
96
97 val watchdog : float -> unit
98 (** [watchdog secs] arms the runaway-guest watchdog: from then on, every
99 {!run} entry must exit within [secs] seconds, or the backend cancels the
100 vCPU run and {!watchdog_fired} becomes true. The budget covers time spent
101 inside the guest only -- host-side time servicing an exit (a hypercall, a
102 POLL wait) does not count -- so a guest legitimately blocked in a long
103 POLL is never killed; only one that spins or fault-loops at EL1 without
104 ever exiting is. [secs <= 0] is a no-op. Call before {!sandbox}: the
105 backend spawns its watchdog thread here, which the sandbox would deny
106 later. Expiry detection is polled, so a cancel can lag [secs] by a
107 fraction of it. *)
108
109 val watchdog_fired : unit -> bool
110 (** [watchdog_fired ()] is [true] once the watchdog canceled a run; the
111 {!Canceled} exit the tender core then sees is the guest's death notice
112 rather than an operator interrupt. *)
113
114 val sandbox : unit -> unit
115 (** [sandbox ()] narrows the tender process once the VM and devices are set
116 up: it denies opening new files, spawning processes, and the network,
117 while leaving descriptors opened before this call usable. The tender needs
118 no host network of its own -- a slirp gateway, when used, runs in a
119 separate process and the tender only reads and writes its end of the
120 socketpair. Fails closed, raising on error. *)
121
122 val poll_add : Unix.file_descr -> unit
123 (** [poll_add fd] registers [fd] to be watched for readability by
124 {!poll_wait}. Call it before {!sandbox}: on Linux it does the epoll
125 registration (epoll_ctl), which the sandbox allowlist does not permit at
126 runtime. *)
127
128 val poll_wait : float -> bool
129 (** [poll_wait timeout] blocks up to [timeout] seconds and returns whether a
130 descriptor registered with {!poll_add} is readable; with none registered
131 it is a bounded sleep returning [false]. It is the POLL hypercall's wait,
132 using only allowlisted syscalls -- [epoll_pwait] on Linux (as upstream
133 Solo5's [hvt_core.c] does), [select] on macOS, where the Seatbelt sandbox
134 does not filter syscalls. *)
135end