nolibc: format printf floats as double, not long double

[samoht]

Split out of #171 for focused review, per @dinosaure.

nolibc's printf (vfprintf.c) reads float arguments as long double, but its fmt_fp already takes a double, so the value round-trips double -> long double -> double through __extenddftf2/__trunctfdf2. On aarch64-linux-gnu (the freestanding cross target) long double is IEEE binary128 (quad), so those are soft-float routines; the round-trip pulls them into every freestanding link that uses printf, even for integer-only formats.

This makes the union field double. %f/%g/%e are unaffected (already formatted at double precision, since fmt_fp takes double); only %Lf/%Le/%Lg change, from quad to double, and OCaml never emits those. Freestanding aarch64 unikernels then link with no compiler runtime library, which is what the LLVM-only macOS cross toolchain in #171 needs (it has no libgcc).

[shym]

Nice catch of (yet another) instance of implicit casts between number types being harmful! Looks good to me.

(I wondered whether the removal of EXTRALIBS in #171 would belong in that PR also? Or is that related to some other change?)

[hannesm]

please rebase for improved CI experience (#178)

[samoht]

Rebased and just kept the long double -> double commit as per @dinosaure request.

[hannesm]

I've not much knowledge about the C code, I guess it is taken from some other library.

What I wonder about is your comment:

only %Lf/%Le/%Lg change, from quad to double, and OCaml never emits those

So, why then not remove the support for these entirely? And have a comment in the source file that support has been removed since OCaml doesn't use them?
Introducing changes to vendored code without any comment makes updating (if there's need for it) cumbersome. At least from my perspective, MirageOS (and thus ocaml-solo5) goal is to be minimal -- so removing any unnecessary code should be the top priority.

Maybe noteworthy that 86493fb as well modified fmt_fp to avoid faults on Xen (by changing long double to double).

Has there been precision lost? I don't know. I usually avoid floating point numbers.

[shym]

I've not much knowledge about the C code, I guess it is taken from some other library.

It comes from musl (thanks to the LICENSE file!). And it has indeed a few differences with the one in the latest musl release.

Maybe noteworthy that 86493fb as well modified fmt_fp to avoid faults on Xen (by changing long double to double).

Interesting! I see two (non-exclusive) possibilities:

• we could go with that proposed patch, as it doesn’t change the current behaviour,
• try to get back on musl’s printf (which implies to test whether the Xen bug is still present and find another way to build it on macOS).

At least from my perspective, MirageOS (and thus ocaml-solo5) goal is to be minimal -- so removing any unnecessary code should be the top priority.

This made me wonder whether there would be a better-fitted printf implementation (especially after noticing that Solo5 bindings also vendor a different printf implementation, where I didn’t find support for L* at a quick glance; but I’m not sure it deserves the same trust as musl, I’d say)… But that’s getting me well beyond the scope of that PR.

[hannesm]

@shym this is a good question, as far as I can tell:

• solo5 printf is https://github.com/mpaland/printf
• this printf is from musl

In solo5, the floating point printing is disabled (see additionally the commit c298e69a8cedb4867252bbb1ae73d5eb4eb51af4).

Size-wise and support-wise, someone should measure whether the mpaland/printf is sufficient (and smaller?) or the musl printf is needed. Keeping that up to date with the latest upstream is of course a good idea.

---

At the same time, if there's no interest / lack of time to look deeper, if this PR fixes something and there are no regressions, we can as well integrate it. As indicated above, I'm not an expert in this area, and appreciate if someone else takes a decision and does the merge & release work.

[dinosaure]

especially after noticing that Solo5 bindings also vendor a different printf implementation, where I didn’t find support for L* at a quick glance; but I’m not sure it deserves the same trust as musl, I’d say

This is a very basic implementation that uses a fixed amount of memory, as malloc() does not exist in Solo5. The constraints on the printf function in Solo5 are not the same as those in ocaml-solo5. However, I would find it difficult to explain the underlying mechanism that leads to the use of the printf function from nolibc.

All in all, I’m not against this PR in its current form.

[hannesm]

ok, so I can see that there's sufficient support for this change, and I'll merge that. Putting the burden to review printf differences (between solo5 and ocaml-solo5), updating from upstream printf, ... should not be onto who proposes this PR -- but may be interesting to do separately.

EDIT: I opened #184 to remember that we should look into that.