From c495d1fbe20d034a61d31898a138e0cf808b8122 Mon Sep 17 00:00:00 2001 From: Thomas Gazagnaire Date: Mon, 29 Jun 2026 14:31:02 -0700 Subject: [PATCH 1/7] nolibc: format printf floats as double, not long double On targets where long double is IEEE quad (aarch64), vfprintf's `union arg` held the float value as long double, so `%f` (and the fmt_fp call) round-tripped double -> long double -> double through __extenddftf2/__trunctfdf2. That pulls libgcc (or compiler-rt) soft-float into every freestanding link that uses printf, even for integer-only formats. fmt_fp already takes a double, so the long double was pure overhead. Use double for the field; %L float conversions are treated as double (never used by OCaml unikernels). aarch64 cross unikernels now link with no libgcc at all (clang already inlines the atomics). --- nolibc/vfprintf.c | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/nolibc/vfprintf.c b/nolibc/vfprintf.c index 9e886a0b..f852e9b8 100644 --- a/nolibc/vfprintf.c +++ b/nolibc/vfprintf.c @@ -121,7 +121,10 @@ static const unsigned char states[]['z'-'A'+1] = { union arg { uintmax_t i; - long double f; + /* double, not long double: avoids pulling libgcc soft-float (__extenddftf2, + __trunctfdf2) into freestanding links; %L is treated as double (fmt_fp + formats at double). */ + double f; void *p; }; @@ -151,7 +154,7 @@ static void pop_arg(union arg *arg, int type, va_list *ap) break; case UIPTR: arg->i = (uintptr_t)va_arg(*ap, void *); #endif break; case DBL: arg->f = va_arg(*ap, double); - break; case LDBL: arg->f = va_arg(*ap, long double); + break; case LDBL: arg->f = va_arg(*ap, double); } } From ac1fb9e3e04c6715de9ce91acb36baa38f7f99a8 Mon Sep 17 00:00:00 2001 From: Thomas Gazagnaire Date: Wed, 8 Jul 2026 12:33:10 -0700 Subject: [PATCH 2/7] toolchain: drop -lgcc, inline aarch64 atomics The aarch64 wrapper linked -lgcc for printf's long-double soft-float (now gone: printf formats as double) and for GCC's default outline atomics (-moutline-atomics lowers C11 atomics to __aarch64_* helpers in libgcc, which also pull __getauxval, absent on a freestanding solo5 target). Pass -mno-outline-atomics so atomics inline (LL/SC); the link then needs no compiler runtime, so drop -lgcc and let a pure-LLVM toolchain link aarch64 unikernels. --- gen_toolchain_tool.sh | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/gen_toolchain_tool.sh b/gen_toolchain_tool.sh index e711ad30..4ec13f81 100755 --- a/gen_toolchain_tool.sh +++ b/gen_toolchain_tool.sh @@ -14,11 +14,12 @@ gen_cc() { CFLAGS="$TOOL_CFLAGS" LDFLAGS="$TOOL_LDFLAGS" - EXTRALIBS="" + # GCC lowers aarch64 C11 atomics to libgcc __aarch64_* outline helpers by + # default; inline them so the freestanding link needs no compiler runtime. case "$ARCH" in aarch64) - EXTRALIBS="-lgcc" + CFLAGS="$CFLAGS -mno-outline-atomics" ;; esac @@ -60,7 +61,6 @@ if [ -z "\$compiling" ]; then -Wl,--start-group \\ -lnolibc \\ -lopenlibm \\ - $EXTRALIBS \\ -Wl,--end-group fi From b0c007e9e0c8c7110160808628871d0ec5058758 Mon Sep 17 00:00:00 2001 From: Samuel Hym Date: Wed, 15 Jul 2026 16:45:03 +0200 Subject: [PATCH 3/7] Add a `--path-prepend` configure option Add a new option so that the toolchain can invoke commands with an extended `PATH` --- Makefile | 8 ++++++-- configure.sh | 9 +++++++++ gen_toolchain_tool.sh | 4 ++++ 3 files changed, 19 insertions(+), 2 deletions(-) diff --git a/Makefile b/Makefile index add901bc..076a9b9e 100644 --- a/Makefile +++ b/Makefile @@ -26,7 +26,8 @@ nolibc/libnolibc.a: phony-nolibc .PHONY: phony-nolibc phony-nolibc: - $(MAKE) -C nolibc libnolibc.a \ + +env PATH="$(MAKECONF_PATH_PREPEND)$$PATH" \ + $(MAKE) -C nolibc libnolibc.a \ "CC=$(MAKECONF_TOOLCHAIN)-cc" \ "FREESTANDING_CFLAGS=$(NOLIBC_CFLAGS)" @@ -36,7 +37,8 @@ openlibm/libopenlibm.a: phony-openlibm .PHONY: phony-openlibm phony-openlibm: - $(MAKE) -C openlibm libopenlibm.a \ + +env PATH="$(MAKECONF_PATH_PREPEND)$$PATH" \ + $(MAKE) -C openlibm libopenlibm.a \ "CC=$(MAKECONF_TOOLCHAIN)-cc" \ "CPPFLAGS=$(LIB_CFLAGS)" @@ -72,6 +74,7 @@ $(TOOLDIR_FOR_BUILD)/$(MAKECONF_TARGET_ARCH)-solo5-ocaml-%: \ ARCH="$(MAKECONF_TARGET_ARCH)" \ SOLO5_TOOLCHAIN="$(MAKECONF_TOOLCHAIN)" \ OTHERTOOLPREFIX="$(MAKECONF_TOOLPREFIX)" \ + PATH_PREPEND="$(MAKECONF_PATH_PREPEND)" \ TOOL_CFLAGS="$(TOOLCHAIN_BUILD_CFLAGS)" \ TOOL_LDFLAGS="$(TOOLCHAIN_BUILD_LDFLAGS)" \ sh $< $* > $@ @@ -82,6 +85,7 @@ $(TOOLDIR_FINAL)/$(MAKECONF_TARGET_ARCH)-solo5-ocaml-%: \ ARCH="$(MAKECONF_TARGET_ARCH)" \ SOLO5_TOOLCHAIN="$(MAKECONF_TOOLCHAIN)" \ OTHERTOOLPREFIX="$(MAKECONF_TOOLPREFIX)" \ + PATH_PREPEND="$(MAKECONF_PATH_PREPEND)" \ TOOL_CFLAGS="$(TOOLCHAIN_FINAL_CFLAGS)" \ TOOL_LDFLAGS="$(TOOLCHAIN_FINAL_LDFLAGS)" \ sh $< $* > $@ diff --git a/configure.sh b/configure.sh index f9dfd870..179c1657 100755 --- a/configure.sh +++ b/configure.sh @@ -31,12 +31,17 @@ Options: (default: \`TARGET-cc -dumpmachine\`-). --ocaml-configure-option=OPTION Add an option to the OCaml compiler configuration. + --path-prepend=VAL + Prepend VAL to PATH in toolchain. For instance: + --path-prepend=/usr/local/llvm-21/bin: + (note the required explicit ':' separator at the end) EOM exit 1 } OCAML_CONFIGURE_OPTIONS= MAKECONF_PREFIX=/usr/local +MAKECONF_PATH_PREPEND= while [ $# -gt 0 ]; do OPT="$1" @@ -57,6 +62,9 @@ while [ $# -gt 0 ]; do --ocaml-configure-option=*) OCAML_CONFIGURE_OPTIONS="${OCAML_CONFIGURE_OPTIONS} ${OPT#*=}" ;; + --path-prepend=*) + MAKECONF_PATH_PREPEND="${OPT#*=}" + ;; --help) usage ;; @@ -96,4 +104,5 @@ MAKECONF_TOOLCHAIN=${CONFIG_TARGET} MAKECONF_TOOLPREFIX=${MAKECONF_TOOLPREFIX} MAKECONF_TARGET_ARCH=${TARGET_ARCH} MAKECONF_OCAML_CONFIGURE_OPTIONS=${OCAML_CONFIGURE_OPTIONS} +MAKECONF_PATH_PREPEND=${MAKECONF_PATH_PREPEND} EOM diff --git a/gen_toolchain_tool.sh b/gen_toolchain_tool.sh index e711ad30..386bbbd1 100755 --- a/gen_toolchain_tool.sh +++ b/gen_toolchain_tool.sh @@ -35,6 +35,7 @@ gen_cc() { # Just like the Solo5 cc, we assume that we are linking, unless we find an # argument suggesting we are compiling but we call Solo5' cc regardless +PATH="$PATH_PREPEND\$PATH" compiling= for arg in "\$@"; do case "\$arg" in @@ -119,10 +120,13 @@ gen_tool() { cat << EOF #!/bin/sh +PATH="$PATH_PREPEND\$PATH" exec $TOOL "\$@" EOF } +PATH="$PATH_PREPEND$PATH" + case "$1" in cc|gcc) gen_cc From d99a0ae0c997209d038e27deae2be5cf839cd346 Mon Sep 17 00:00:00 2001 From: Samuel Hym Date: Wed, 15 Jul 2026 16:49:15 +0200 Subject: [PATCH 4/7] Set `AR` and `RANLIB` to build support libraries --- Makefile | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Makefile b/Makefile index 076a9b9e..e45cb382 100644 --- a/Makefile +++ b/Makefile @@ -29,6 +29,8 @@ phony-nolibc: +env PATH="$(MAKECONF_PATH_PREPEND)$$PATH" \ $(MAKE) -C nolibc libnolibc.a \ "CC=$(MAKECONF_TOOLCHAIN)-cc" \ + "AR=$(MAKECONF_TOOLPREFIX)ar" \ + "RANLIB=$(MAKECONF_TOOLPREFIX)ranlib" \ "FREESTANDING_CFLAGS=$(NOLIBC_CFLAGS)" # OPENLIBM @@ -40,6 +42,8 @@ phony-openlibm: +env PATH="$(MAKECONF_PATH_PREPEND)$$PATH" \ $(MAKE) -C openlibm libopenlibm.a \ "CC=$(MAKECONF_TOOLCHAIN)-cc" \ + "AR=$(MAKECONF_TOOLPREFIX)ar" \ + "RANLIB=$(MAKECONF_TOOLPREFIX)ranlib" \ "CPPFLAGS=$(LIB_CFLAGS)" # TOOLCHAIN From 974d1a5ad6455c4fca8de773644ac46cb36f400d Mon Sep 17 00:00:00 2001 From: Samuel Hym Date: Thu, 16 Jul 2026 15:55:39 +0200 Subject: [PATCH 5/7] Promote `manifest.c` for when solo5-elftool is not available --- example/dune | 2 ++ example/dune-project | 2 +- example/manifest.c | 13 +++++++++++++ 3 files changed, 16 insertions(+), 1 deletion(-) create mode 100644 example/manifest.c diff --git a/example/dune b/example/dune index 2bcf60f9..6d6d7a60 100644 --- a/example/dune +++ b/example/dune @@ -26,6 +26,8 @@ (rule (targets manifest.c) (deps manifest.json) + (mode promote) + (enabled_if %{bin-available:solo5-elftool}) (action (run solo5-elftool gen-manifest manifest.json manifest.c))) diff --git a/example/dune-project b/example/dune-project index 45acd3f0..0c226b5b 100644 --- a/example/dune-project +++ b/example/dune-project @@ -1 +1 @@ -(lang dune 2.7) +(lang dune 3.2) diff --git a/example/manifest.c b/example/manifest.c new file mode 100644 index 00000000..b6ce6253 --- /dev/null +++ b/example/manifest.c @@ -0,0 +1,13 @@ +/* Generated by solo5-elftool version v0.12.0, do not edit */ + +#define MFT_ENTRIES 1 +#include "mft_abi.h" + +MFT1_NOTE_DECLARE_BEGIN +{ + .version = MFT_VERSION, .entries = 1, + .e = { + { .name = "", .type = MFT_RESERVED_FIRST }, + } +} +MFT1_NOTE_DECLARE_END From f1adcae78fb7a0dd94c5930db542810a75e45a9d Mon Sep 17 00:00:00 2001 From: Samuel Hym Date: Wed, 15 Jul 2026 17:49:29 +0200 Subject: [PATCH 6/7] AMEND Add a macOS CI workflow This CI workflow illustrates how this PR plays with changes from Solo5/solo5#656 and from #177 It should be amended to follow updates on those other changes --- .github/workflows/macos.yml | 118 ++++++++++++++++++++++++++++++++++++ 1 file changed, 118 insertions(+) create mode 100644 .github/workflows/macos.yml diff --git a/.github/workflows/macos.yml b/.github/workflows/macos.yml new file mode 100644 index 00000000..7aba9775 --- /dev/null +++ b/.github/workflows/macos.yml @@ -0,0 +1,118 @@ +name: macOS +on: + push: + branches: + - main + pull_request: +jobs: + build: + strategy: + matrix: + runner: + - macos-latest + ocaml-compiler: + - 5.5.0 + name: >- + OCaml ${{ matrix.ocaml-compiler }}, macOS arm64 + runs-on: ${{ matrix.runner }} + steps: + - uses: actions/checkout@v7 + - uses: ocaml/setup-ocaml@v3 + with: + ocaml-compiler: ${{ matrix.ocaml-compiler }} + opam-local-packages: + - name: Install opam packages + run: | + opam install dune ocamlfind ocaml-src opatch opam-installer + - name: Check out Solo5 + uses: actions/checkout@v7 + with: + repository: shym/solo5 + ref: macos + path: solo5 + - name: Install dependencies + run: brew install llvm lld + - name: Build and install Solo5 + run: | + set -x + cd solo5 + ./configure.sh --prefix="$(opam var prefix)" --disable-elftool \ + --path-prepend="$(brew --prefix llvm)/bin:$(brew --prefix lld)/bin:" + make -j2 + make install + - name: Build OCaml/Solo5 + run: | + set -x + eval $(opam env) + pfx="$(opam var prefix)" + ./configure.sh --prefix="$pfx" \ + --sysroot="$pfx/lib/ocaml-solo5" \ + --target=aarch64-solo5-none-static \ + --othertoolprefix=llvm- \ + --ocaml-configure-option=--disable-function-sections \ + --path-prepend="$(brew --prefix llvm)/bin:$(brew --prefix lld)/bin:" + make V=1 -j2 + make install + - name: Show the toolchain configuration + run: | + set -x + opam exec -- ocamlfind -toolchain solo5 opt -config + opam exec -- ocamlfind -toolchain solo5 printconf + opam exec -- ocamlfind -toolchain solo5 list + + # Do not build all the examples as hello is trying to link against an + # external fmt library and the opam-installed fmt is incompatible with the + # OCaml/Solo5 Stdlib (inconsistent assumptions...) + - name: Compile examples with hvt + run: | + MODE=hvt opam exec -- dune build --root example --display short \ + config.exe sysfail.exe + - name: Compile examples with spt + run: | + MODE=spt opam exec -- dune build --root example --display short \ + config.exe sysfail.exe + - name: Build an artifact of the spt executables + run: | + set -x + for e in config sysfail; do \ + cp example/_build/solo5/$e.exe /tmp/$e.spt ; \ + done + cd /tmp + tar caf unikernels.tar.zst *.spt + - name: Upload artifact + uses: actions/upload-artifact@v7 + with: + name: unikernels + path: /tmp/unikernels.tar.zst + retention-days: 1 + + run: + name: Run unikernels + needs: build + runs-on: ubuntu-24.04-arm + steps: + - name: Install dependencies + run: | + sudo apt-get install -y libseccomp-dev pkg-config + - name: Check out Solo5 + uses: actions/checkout@v7 + with: + repository: solo5/solo5 + ref: v0.12.0 + path: solo5 + - name: Build Solo5 tenders + run: | + set -x + cd solo5 + ./configure.sh --disable-toolchain + make -j3 + - name: Download artifact + uses: actions/download-artifact@v8 + with: + name: unikernels + - name: Run the spt unikernels + run: | + set -x + tar xaf unikernels.tar.zst + solo5/tenders/spt/solo5-spt config.spt + ! solo5/tenders/spt/solo5-spt sysfail.spt From 7f2f81e2e33ae3bd38f1f3f885d96a6faa55d5aa Mon Sep 17 00:00:00 2001 From: Samuel Hym Date: Thu, 16 Jul 2026 18:11:09 +0200 Subject: [PATCH 7/7] Add the OS in the CI workflow title --- .github/workflows/test.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 40c2dccf..256896e7 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -17,7 +17,7 @@ jobs: - runner: ubuntu-latest ocaml-compiler: 5.4.1 name: >- - OCaml ${{ matrix.ocaml-compiler }} + OCaml ${{ matrix.ocaml-compiler }}, Linux ${{ case(matrix.runner=='ubuntu-latest', 'x86_64', 'arm64') }} runs-on: ${{ matrix.runner }} steps: