[Picolibc] Porting picolibc to CompCert

[Sebastian Meyer]

Hi Keith, and of course Hi everyone else interested :)

We're currently in the process of evaluating libc for use with the "CompCert formally-verified C Compiler" (public git at https://github.com/AbsInt/CompCert).
The aim is to have a libc which we can use for internal testing at AbsInt, and maybe have a libc to point customers/project partners to, when asked for a recommendation.
picolibc seems very promising in both regards.

My work is not yet ready: I only made the compile run through (and ported my changes to the latest main), but when I build the hello-world for rv32, there is no output (qemu just sits there at 100% load).
I've got some ideas what to do next (adapt crt0.c since CompCert doesn't support __naked__ while waiting for my colleagues to add strong/weak symbol support to CompCert).
In case you want to take a look at the current diff and/or give some early feedback (much appreciated!), I created a squash commit over at GitHub.
The commit comment also contains a lengthy list of the changes.
https://github.com/archi/picolibc/commit/95e36dcb433487100c60dbede471bc8d0a2feae4
Feel free to comment either at GitHub (I hope that's possible?) or via mail or both ;)

I've also added support for CompCert to meson.
My PR can be found here: https://github.com/mesonbuild/meson/pull/7674

@Keith: If you want to test the build, I could probably supply you a pre-built CompCert package for research/evaluation/personal purposes (of course you can also built it yourself from the public git).

I don't want to spam a huge wall of text, so I'll leave it at this ;)

Best regards,
Sebastian

-------------------------------------- Sebastian Meyer -------------
AbsInt Angewandte Informatik GmbH      Email: meyer at AbsInt.com
Science Park 1                         Tel:   +49-681-38360-58
66123 Saarbrücken                      Fax:   +49-681-38360-20
GERMANY                                WWW:   http://www.AbsInt.com
--------------------------------------------------------------------
Geschäftsführung: Dr.-Ing. Christian Ferdinand
Eingetragen im Handelsregister des Amtsgerichts Saarbrücken, HRB 11234