Portable build of progs/ and progs64/ directories

[andrew-appel]

At present, it's difficult to run clightgen on the .c files in progs/ and progs64/ unless one has an installation of CompCert for x86_32 and for x86_64, with the standard set of include directories. Essentially, that means one needs Linux, either native or in a VM. That's because Cygwin and MacOS no longer support 32-bit mode, and future MacOS support for x86 is iffy.

It would useful to have a portable build for VST, including all the test cases in progs and progs64. I

Up to this point, the .c files in progs/ are assumed to be compiled (with clightgen) for x86_32, and the .c files in progs64 are assumed to be for x86_64. Up until now, that has meant one needs an x86_32 or x86_64 installation of CompCert. And it's almost easy to configure CompCert to cross-compile (e.g., run CompCert on a 64-bit ARM in MacOS, compiling for 32-bit x86 in Linux), but the difficulty is that one needs the target-machine's include directories. As the CompCert manual says, "Cross-compilation (e.g. generating PowerPC code from an x86 host) is possible but requires the installation of a matching GCC or Diab cross compiler and cross libraries."

I propose that we can do this without installing GCC cross libraries. The use of system include files in progs64 and progs is very limited: we only use limited subsets of stddef.h, stdio.h, limits.h, and (in one case) stdint.h. It should be possible to create test-case-specific include directories, progs/include and progs64/include, that have subset implementations of these header files.

Then anyone can install two local CompCert builds, one configured as x86_64-linux, the other as x86_32-linux. In both cases the CompCert ./configure should be with -no-runtime-lib and -no-standard-headers.

The VST Makefile, when the CLIGHTGEN symbol is defined, can also check that clightgen has been configured properly, though this is a bit clumsy: run clightgen on any .c file (even an empty one), and the resulting .v file has an Info struct that describes the configuration.

So, this worth the trouble to implement?

[MSoegtropIMC]

I also came across this and wanted to create a CompCert and VST ARM Opam package. I dropped it since Timothy Carstens (@intoverflow) wanted to look into it, but since there is apparently no progress, I can pick this up again.

A mechanism to install multiple CompCert and VST versions is already prepared, although I still would like to have the discussed -V option in Coq to drag in variants without system dependent -Q paths.

Ideally we should also provide a simple emulator.

[andrew-appel]

Actually, I had in mind something different. This is only for the purpose of building the test cases in progs/ and progs64/ (and also sha, tweetnacl, etc.); and only for running clightgen, not for compiling to executable code. Once the .c files are clightgenned into .v files (and checked into the github repo), we don't need the underlying target-specific CompCert anymore; we can run the verifications of the testcases in a VST build with the internal "bundled" CompCert (which does not have a clightgen in it). This means that a person wanting to rebuild the .c->.v files will just need to build two CompCert directories enough for clightgen, but will not need to install them in user-contrib. And the users of those .v files will not even need those clightgens. What you suggest is perfectly reasonable, but it would be for a different purpose, I think

[MSoegtropIMC]

That doesn't seem to be very modular. Things should be done such that users can go through example files with checked in clightgen generated files with an installed VST (from CoqPlatform e.g.). As far as I can see what you suggest will only work with VST compiled from sources.

[andrew-appel]

Whether or not the clightgen comes from a platform-installed VST, there is still the other issue of include files. If I'm running on a Mac, using a clightgen built to target x86_32, where do the include files come from? My original note points out that CompCert suggests using a gcc cross-compile installation, but I'm suggesting intead that we build a special-purpose include directory for 32-bit test cases (progs/, sha/, etc.) and another for 64-bit test cases (progs64/, etc.).

[MSoegtropIMC]

Indeed the CompCert opam package would depend on a cross gcc opam package (which I would also provide).

With the process you suggest I see the issue that it will make it much harder for people to use VST on their own code (and compile it in the end). One would have to switch the header files then. Also one has to be very careful then to be sure about the meaning of the verification one did.

[andrew-appel]

OK, your plan looks good. It's not urgent, there are probably higher-priority things to worry about first. I will leave this issue open for now.