Compiling the OCaml runtime with compcert

Hello,

I am interested in using the verified optimising C compiler compcert to compiler the OCaml runtime. I tried to do this and failed during configure when system headers are included, and compcert seeems not to be able to use these system header.

I’m curious whether anyone attempted (and succeeded) to compile the OCaml runtime with compcert. I am aware that compcert itself needs a C compiler and an OCaml compiler (for coq) for bootstrapping.

5 Likes

(cc @xavierleroy, who is most likely to know about this.)

A few times in the past I managed to compile the OCaml runtime using CompCert, but that was before the new autoconf-based configuration system. Maybe I’ll try again in the coming weeks.

@hannes is right that system headers (/usr/include/*.h) often cause difficulties with CompCert, either because they are written for exclusive use with the system compiler (e.g. MacOS/Xcode), or because they have never been tested with any C compiler beyond GCC and Clang.

I’m pretty sure that the OCaml C sources fall squarely within the C11 subset supported by CompCert. I agree this claim needs experimental verification :slight_smile:

3 Likes

That’s great.

IIUC, autoconf should make it much easier to upstream an option for C compiler is compcert, may be great to have this as a CI job.

yes, on my FreeBSD system I have some early issues
sys/_types.h contains the following code:

#ifdef __GNUCLIKE_BUILTIN_VARARGS
typedef __builtin_va_list       __va_list;      /* internally known to gcc */
#else
#error "No support for your compiler for stdargs"
#endif

A workaround is to pass -D __GNUCLIKE_BUILTIN_VARARGS to the C compiler.

Then compcert cannot parse sys/_types.h:

sys/_types.h:106:25: syntax error after '__max_align1' and before '__aligned'.
Ill-formed struct declaration.
Up to this point, a declarator has been recognized:
  '__max_align1'
If this declarator is complete,
then at this point, one of the following is expected:
  a colon ':', followed with a constant expression; or
  a comma ',', followed with a struct declarator; or
  a semicolon ';'.
Fatal error; compilation aborted.

The C source at sys/types.h:106:

105:typedef struct {
106:        long long __max_align1 __aligned(_Alignof(long long));
107:#ifndef _STANDALONE
108:        long double __max_align2 __aligned(_Alignof(long double));
109:#endif
110:} __max_align_t;

I suspect, activating this macro (from sys/cdefs.h) #define __aligned(x) __attribute__((__aligned__(x))) may fix the above issue, but I wasn’t able to find out whether compcert defines a constant to #ifdef`` on (the Intel C compiler seems to defined(__INTEL_COMPILER)`), is there something similar for compcert?

That’s excellent news. :smiley:

1 Like

Totally agree it would be nice to have it as a CI job. Would help to keep both projects in check.

The macro __COMPCERT__ is predefined. Since release 3.6, there is also __COMPCERT_MAJOR__, __COMPCERT_MINOR__ and __COMPCERT_VERSION__ to test for specific versions of CompCert. I agree all this should be documented better :slight_smile:

So, I tried, and it works pretty well under Linux (Ubutu 18.04). I had to tweak configure options for a while, but the following gives good results:

./configure CC="ccomp -fall -D_REENTRANT -D_DEFAULT_SOURCE" --disable-shared

There are some failures in the test suite, but I suspect these are due to warnings that CompCert emits when called from OCaml in -custom mode, and that ocamltest interprets as failures.

4 Likes