gazagnaire.org
Solo5 hvt ABI and MFT1/ABI1 note format as wire codecs
solo5: Generate eio unikernel build glue
Eio_solo5 callers declare devices at run, so the native binary can print the manifest used by the Solo5 build. The solo5 tool also emits the startup and manifest glue, and merlint ignores compiler-introduced wrapped module paths when the source path has no double underscore.
author
Thomas Gazagnaire
date
(Jun 18, 2026, 7:51 AM UTC)
commit
11bf9c85
11bf9c8514d0789d34757238a520481cdddba96b
parent
18ee2f79
18ee2f794fb594a656a12c45d9263e96065de89f
+276
-27
+100
bin/cmd_dune.ml
+100
bin/cmd_dune.ml
···
1
+
open Cmdliner
2
+
3
+
let err_invalid_lib lib =
4
+
Fmt.kstr (fun s -> Error s) "invalid Dune library name: %S" lib
5
+
6
+
let check_lib lib =
7
+
let invalid = function
8
+
| ' ' | '\t' | '\n' | '\r' | '(' | ')' -> true
9
+
| _ -> false
10
+
in
11
+
if lib = "" || String.exists invalid lib then err_invalid_lib lib else Ok lib
12
+
13
+
let emit_libraries libs =
14
+
match libs with
15
+
| [] -> Fmt.pr " (libraries)@."
16
+
| libs ->
17
+
Fmt.pr " (libraries@.";
18
+
let rec loop = function
19
+
| [] -> ()
20
+
| [ lib ] -> Fmt.pr " %s)@." lib
21
+
| lib :: libs ->
22
+
Fmt.pr " %s@." lib;
23
+
loop libs
24
+
in
25
+
loop libs
26
+
27
+
let emit_executable ~solo5 libs =
28
+
let env = if solo5 then "eio-solo5.solo5" else "eio-solo5.native" in
29
+
let libs = [ "eio"; "eio-solo5"; env ] @ libs in
30
+
print_endline "(executable";
31
+
print_endline " (name unikernel)";
32
+
if solo5 then
33
+
print_endline
34
+
" (enabled_if\n\
35
+
\ (or\n\
36
+
\ (= %{context_name} solo5)\n\
37
+
\ (= %{context_name} default.solo5)))"
38
+
else print_endline " (enabled_if\n (= %{context_name} default))";
39
+
print_endline " (modules unikernel)";
40
+
emit_libraries libs;
41
+
if solo5 then begin
42
+
print_endline " (link_flags\n (-cclib -z -cclib solo5-abi=hvt))";
43
+
print_endline " (foreign_stubs\n (language c)\n (names startup manifest))"
44
+
end;
45
+
print_endline ")\n"
46
+
47
+
let emit_manifest_rule () =
48
+
print_endline
49
+
"(rule\n\
50
+
\ (targets startup.c)\n\
51
+
\ (enabled_if\n\
52
+
\ (or\n\
53
+
\ (= %{context_name} solo5)\n\
54
+
\ (= %{context_name} default.solo5)))\n\
55
+
\ (action\n\
56
+
\ (with-stdout-to startup.c\n\
57
+
\ (run %{bin:solo5} startup))))\n\n\
58
+
(rule\n\
59
+
\ (targets manifest.json)\n\
60
+
\ (enabled_if\n\
61
+
\ (or\n\
62
+
\ (= %{context_name} solo5)\n\
63
+
\ (= %{context_name} default.solo5)))\n\
64
+
\ (action\n\
65
+
\ (with-stdout-to manifest.json\n\
66
+
\ (run %{exe:unikernel.exe} --manifest))))\n\n\
67
+
(rule\n\
68
+
\ (targets manifest.c)\n\
69
+
\ (enabled_if\n\
70
+
\ (or\n\
71
+
\ (= %{context_name} solo5)\n\
72
+
\ (= %{context_name} default.solo5)))\n\
73
+
\ (deps manifest.json)\n\
74
+
\ (action\n\
75
+
\ (run %{bin:solo5} manifest manifest.json manifest.c)))"
76
+
77
+
let run libs =
78
+
let libs =
79
+
List.fold_right
80
+
(fun lib acc ->
81
+
match (check_lib lib, acc) with
82
+
| Ok lib, Ok libs -> Ok (lib :: libs)
83
+
| Error e, _ | _, Error e -> Error e)
84
+
libs (Ok [])
85
+
in
86
+
match libs with
87
+
| Error msg -> `Error (false, msg)
88
+
| Ok libs ->
89
+
emit_executable ~solo5:false libs;
90
+
emit_executable ~solo5:true libs;
91
+
emit_manifest_rule ();
92
+
`Ok ()
93
+
94
+
let cmd =
95
+
let libs =
96
+
let doc = "Additional application libraries to add to both stanzas." in
97
+
Arg.(value & pos_all string [] & info [] ~docv:"LIB" ~doc)
98
+
in
99
+
let doc = "emit a dune.inc for an eio-solo5 unikernel" in
100
+
Cmd.v (Cmd.info "dune" ~doc) Term.(ret (const run $ libs))
+4
-2
bin/cmd_manifest.ml
+4
-2
bin/cmd_manifest.ml
···
1
1
module Manifest = Solo5_abi.Manifest
2
2
open Cmdliner
3
3
4
+
let write file data =
5
+
Out_channel.with_open_bin file (fun oc -> Out_channel.output_string oc data)
6
+
4
7
let run () input output =
5
8
let json = Common.read input in
6
9
match Json.of_string Common.devices_codec json with
···
8
11
| Ok devices -> (
9
12
match Manifest.c_of_devices devices with
10
13
| c ->
11
-
Out_channel.with_open_bin output (fun oc ->
12
-
Out_channel.output_string oc c);
14
+
write output c;
13
15
`Ok ()
14
16
| exception Failure msg -> `Error (false, Fmt.str "%s: %s" input msg))
15
17
+29
bin/cmd_startup.ml
+29
bin/cmd_startup.ml
···
1
+
open Cmdliner
2
+
3
+
let source =
4
+
{|/* Generated by solo5 startup, do not edit. */
5
+
6
+
#include <solo5.h>
7
+
8
+
#define CAML_NAME_SPACE
9
+
#include <caml/callback.h>
10
+
#include <caml/mlvalues.h>
11
+
12
+
static char *unused_argv[] = { "unikernel", NULL };
13
+
14
+
void _nolibc_init(uintptr_t heap_start, size_t heap_size);
15
+
16
+
int solo5_app_main(const struct solo5_start_info *si) {
17
+
_nolibc_init(si->heap_start, si->heap_size);
18
+
caml_startup(unused_argv);
19
+
return 0;
20
+
}
21
+
|}
22
+
23
+
let run () =
24
+
print_string source;
25
+
`Ok ()
26
+
27
+
let cmd =
28
+
let doc = "generate the OCaml/Solo5 startup C source" in
29
+
Cmd.v (Cmd.info "startup" ~doc) Term.(ret (const run $ Common.setup))
+84
bin/cmd_up.ml
+84
bin/cmd_up.ml
···
1
+
open Cmdliner
2
+
3
+
let workspace = "dune-workspace"
4
+
let header = "(lang dune 3.0)\n"
5
+
let host_context = "(context default)\n"
6
+
7
+
(* The Solo5 cross context: a `default`-based context that cross-compiles through
8
+
the `solo5` toolchain (from ocaml-solo5-cross-aarch64). *)
9
+
let solo5_context =
10
+
{|(context
11
+
(default
12
+
(name solo5)
13
+
(host default)
14
+
(toolchain solo5)
15
+
(merlin)
16
+
(disable_dynamically_linked_foreign_archives true)))
17
+
|}
18
+
19
+
(* The cross packages that install the `solo5` Dune toolchain. *)
20
+
let toolchain = [ "solo5-cross-aarch64"; "ocaml-solo5-cross-aarch64" ]
21
+
22
+
let has_default w =
23
+
List.exists
24
+
(fun (c : Dune.Workspace.Context.t) -> c.name = None)
25
+
(Dune.Workspace.contexts w)
26
+
27
+
let has_solo5 w =
28
+
List.exists
29
+
(fun (c : Dune.Workspace.Context.t) ->
30
+
match c.kind with
31
+
| Dune.Workspace.Context.Toolchain { name = "solo5" } -> true
32
+
| _ -> false)
33
+
(Dune.Workspace.contexts w)
34
+
35
+
let write path s =
36
+
let oc = open_out path in
37
+
output_string oc s;
38
+
close_out oc
39
+
40
+
(* Ensure the workspace declares the solo5 context, without ever clobbering one
41
+
the project already wrote: create it if absent, otherwise append the context
42
+
(plus an explicit host context if the file had only the implicit default). *)
43
+
let ensure_workspace () =
44
+
if not (Sys.file_exists workspace) then begin
45
+
write workspace (header ^ "\n" ^ host_context ^ "\n" ^ solo5_context);
46
+
Fmt.pr "Wrote %s with host and Solo5 contexts.@." workspace
47
+
end
48
+
else
49
+
let content = Common.read workspace in
50
+
match Dune.Workspace.of_string content with
51
+
| Error _ ->
52
+
Fmt.pr "%s exists but could not be parsed; leaving it untouched.@."
53
+
workspace
54
+
| Ok w when has_solo5 w ->
55
+
Fmt.pr "%s already declares the solo5 context.@." workspace
56
+
| Ok w ->
57
+
let host = if has_default w then "" else "\n" ^ host_context in
58
+
write workspace (content ^ host ^ "\n" ^ solo5_context);
59
+
Fmt.pr "Added the solo5 context to %s.@." workspace
60
+
61
+
let install_toolchain () =
62
+
let cmd = Filename.quote_command "opam" ("install" :: "-y" :: toolchain) in
63
+
Fmt.pr "Installing the Solo5 cross toolchain:@. %s@." cmd;
64
+
match Sys.command cmd with
65
+
| 0 -> ()
66
+
| n -> Fmt.pr "warning: opam exited with status %d@." n
67
+
68
+
(* The cross archiver wraps llvm-ar; on macOS it is often not on PATH, and the
69
+
failure (during the archive step, after the stubs compile) is opaque. *)
70
+
let check_llvm_ar () =
71
+
if Sys.command "command -v llvm-ar > /dev/null 2>&1" <> 0 then
72
+
Fmt.pr
73
+
"warning: llvm-ar is not on PATH; the cross archiver needs it. On \
74
+
macOS:@. export PATH=\"$(brew --prefix llvm)/bin:$PATH\"@."
75
+
76
+
let run () =
77
+
ensure_workspace ();
78
+
install_toolchain ();
79
+
check_llvm_ar ();
80
+
`Ok ()
81
+
82
+
let cmd =
83
+
let doc = "set up a Solo5 cross context and install the cross toolchain" in
84
+
Cmd.v (Cmd.info "up" ~doc) Term.(ret (const run $ Common.setup))
+1
-17
bin/common.ml
+1
-17
bin/common.ml
···
4
4
5
5
(* manifest.json, e.g. { "type": "solo5.manifest", "version": 1,
6
6
"devices": [ { "name": "disk", "type": "BLOCK_BASIC" } ] }. *)
7
-
let devices_codec : Manifest.device list Json.Codec.t =
8
-
let open Json.Codec in
9
-
let device =
10
-
Object.(
11
-
map (fun name typ ->
12
-
match typ with
13
-
| "BLOCK_BASIC" -> Manifest.Block_basic name
14
-
| "NET_BASIC" -> Manifest.Net_basic name
15
-
| t -> failwith ("unknown device type: " ^ t))
16
-
|> member "name" string |> member "type" string |> seal)
17
-
in
18
-
Object.(
19
-
map (fun (_ : string) (_ : int) devices -> devices)
20
-
|> member "type" string |> member "version" int
21
-
|> member "devices" (list device)
22
-
|> seal)
23
-
7
+
let devices_codec : Manifest.device list Json.Codec.t = Manifest.json_codec
24
8
let read file = In_channel.with_open_bin file In_channel.input_all
25
9
26
10
let with_elf file f =
+1
-1
bin/common.mli
+1
-1
bin/common.mli
···
4
4
(** [setup] configures logging from the standard observability flags. *)
5
5
6
6
val devices_codec : Solo5_abi.Manifest.device list Json.Codec.t
7
-
(** [devices_codec] decodes a manifest.json into the declared devices. *)
7
+
(** [devices_codec] encodes and decodes a manifest.json's declared devices. *)
8
8
9
9
val read : string -> string
10
10
(** [read file] is the whole contents of [file]. *)
+10
-2
bin/dune
+10
-2
bin/dune
···
16
16
(name solo5)
17
17
(public_name solo5)
18
18
(package solo5-tool)
19
-
(modules solo5 cmd_manifest cmd_query cmd_size common)
20
-
(libraries solo5-abi elf nox-json cmdliner fmt observe))
19
+
(modules
20
+
solo5
21
+
cmd_dune
22
+
cmd_manifest
23
+
cmd_query
24
+
cmd_size
25
+
cmd_startup
26
+
cmd_up
27
+
common)
28
+
(libraries solo5-abi elf nox-json nox-dune cmdliner fmt observe))
+13
-4
bin/solo5.ml
+13
-4
bin/solo5.ml
···
2
2
3
3
[manifest] turns a manifest.json (the device declarations a unikernel may
4
4
use) into the C source declaring the MFT1 ELF note, which the Solo5 loader
5
-
reads and a tender validates against the operator's granted devices. [query]
6
-
reads the ABI and manifest notes back out of a built unikernel, [size] its
7
-
section sizes. Pure OCaml: no C toolchain. *)
5
+
reads and a tender validates against the operator's granted devices.
6
+
[startup] emits the OCaml/Solo5 C entry point. [up] prepares the local Solo5
7
+
cross context. [query] reads the ABI and manifest notes back out of a built
8
+
unikernel, [size] its section sizes. Pure OCaml: no C toolchain for the
9
+
tooling itself. *)
8
10
9
11
let () =
10
12
let doc = "Solo5 unikernel manifest and inspection tool" in
11
13
let cmd =
12
14
Cmdliner.Cmd.group
13
15
(Cmdliner.Cmd.info "solo5" ~doc)
14
-
[ Cmd_manifest.cmd; Cmd_query.cmd; Cmd_size.cmd ]
16
+
[
17
+
Cmd_manifest.cmd;
18
+
Cmd_startup.cmd;
19
+
Cmd_up.cmd;
20
+
Cmd_query.cmd;
21
+
Cmd_size.cmd;
22
+
Cmd_dune.cmd;
23
+
]
15
24
in
16
25
exit (Cmdliner.Cmd.eval cmd)
+2
dune-project
+2
dune-project
···
21
21
(ocaml (>= 5.1))
22
22
(elf (>= 0.1))
23
23
(wire (>= 0.1))
24
+
(nox-json (>= 0.1))
24
25
(fmt (>= 0.9))
25
26
(alcotest :with-test)))
26
27
···
51
52
(solo5-abi (>= 0.1))
52
53
(elf (>= 0.1))
53
54
(nox-json (>= 0.1))
55
+
(nox-dune (>= 0.1))
54
56
(cmdliner (>= 1.2))
55
57
(fmt (>= 0.9))
56
58
(observe (>= 0.1))
+1
-1
lib/abi/dune
+1
-1
lib/abi/dune
+25
lib/abi/manifest.ml
+25
lib/abi/manifest.ml
···
45
45
46
46
type device = Block_basic of string | Net_basic of string
47
47
48
+
let json_codec : device list Json.Codec.t =
49
+
let open Json.Codec in
50
+
let name = function Block_basic name | Net_basic name -> name in
51
+
let typ = function
52
+
| Block_basic _ -> "BLOCK_BASIC"
53
+
| Net_basic _ -> "NET_BASIC"
54
+
in
55
+
let device =
56
+
Object.(
57
+
map (fun name typ ->
58
+
match typ with
59
+
| "BLOCK_BASIC" -> Block_basic name
60
+
| "NET_BASIC" -> Net_basic name
61
+
| t -> failwith ("unknown device type: " ^ t))
62
+
|> member "name" string ~enc:name
63
+
|> member "type" string ~enc:typ
64
+
|> seal)
65
+
in
66
+
Object.(
67
+
map (fun (_ : string) (_ : int) devices -> devices)
68
+
|> member "type" string ~enc:(fun _ -> "solo5.manifest")
69
+
|> member "version" int ~enc:(fun _ -> 1)
70
+
|> member "devices" (list device) ~enc:Fun.id
71
+
|> seal)
72
+
48
73
let trim_name s =
49
74
match String.index_opt s '\000' with Some i -> String.sub s 0 i | None -> s
50
75
+4
lib/abi/manifest.mli
+4
lib/abi/manifest.mli
···
21
21
for [devices], using Solo5's mft_abi.h macros (the build-time counterpart of
22
22
{!of_elf} / {!of_string}). *)
23
23
24
+
val json_codec : device list Json.Codec.t
25
+
(** [json_codec] encodes and decodes the manifest JSON format consumed by the
26
+
[solo5 manifest] tool and emitted by native unikernel probes. *)
27
+
24
28
(** {1 Wire codecs}
25
29
26
30
The wire codecs the EverParse 3D C validators in [c/] are generated from. *)
+1
solo5-abi.opam
+1
solo5-abi.opam