überSpark: Add compiler bridge for Compcert v3.1 (amd64/x86_32)

This task will add Compcert compiler bridges for x86_32 architecture and amd64 container within überSpark.

The versions of Compcert this task will add will be v3.1 through v3.6
See http://compcert.inria.fr/release/ for the releases. Can also be installed via opam

The bridges themselves will be in the following locations within the uberspark.git repository:

src-nextgen/bridges/cc-bridge/container/amd64/x86_32/generic/compcert/v3.1/
src-nextgen/bridges/cc-bridge/container/amd64/x86_32/generic/compcert/v3.2/
src-nextgen/bridges/cc-bridge/container/amd64/x86_32/generic/compcert/v3.3/
src-nextgen/bridges/cc-bridge/container/amd64/x86_32/generic/compcert/v3.4/
src-nextgen/bridges/cc-bridge/container/amd64/x86_32/generic/compcert/v3.5/
src-nextgen/bridges/cc-bridge/container/amd64/x86_32/generic/compcert/v3.6/

See

src-nextgen/bridges/cc-bridge/container/amd64/x86_32/generic/gcc/v5.4.0/

for an example of how this is done for the gcc v5.4.0 compiler.

Also useful is the uberspark manifest reference related to compiler bridges (uberspark-bridge-cc):
https://docs.uberspark.org/nextgen-toolkit/reference/manifest.html#uberspark-bridge-cc-manifest-node

Linked PR:

Should I be looking at the main or develop branch on UberSpark?

You mention using Ubuntu or Alpine, I would prefer Ubuntu if that’s ok. I note that you are using 16.04 in your Dockerfile for GCC. Is it ok if I use something newer, or did you have some specific reason for using 16.04?

Where can I look to see what your manifest is actually doing with the Dockerfile? I.e., I want to understand a bit more about how you’re integrating with the compiler tools, how the framework interacts with the container, from a life-cycle perspective. Does your framework spin up a new container every time? Do you keep persistent volumes around? etc.

Hi @daveman1010221,

Thanks for jumping in. All good questions, and probably need to be in the documentation at some point (in a section called “Bridges”). For now, please find my answers below:

Should I be looking at the main or develop branch on UberSpark?

develop

You mention using Ubuntu or Alpine, I would prefer Ubuntu if that’s ok

The only reason to pivot towards alpine might be the resulting sizes of the docker images tend to be much smaller. But Ubuntu would be fine too.

I note that you are using 16.04 in your Dockerfile for GCC. Is it ok if I use something newer, or did you have some specific reason for using 16.04?

16.04 LTS was still within EOL (April 2021) at that time. But please feel free to use a newer version. We might still want to stick with LTS editions just because of their long-lived support cycles.

Where can I look to see what your manifest is actually doing with the Dockerfile?

src-nextgen/tools/ is the home for the various OCaml sources to the next-gen überSpark toolkit. It includes a front-end, library and shared-definition pre-processor. The bridge logic which uses docker as its backend is found within: src-nextgen/tools/libs/uberspark_bridge_xxx with src-nextgen/tools/libs/uberspark_bridge_container exposing the three high-level intefraces (build image, list and run).

Does your framework spin up a new container every time? Do you keep persistent volumes around?

We spin up a new container every time and use host volume mounts to share host files (for compiling, assembling, linking, verifying etc.)

Hope this helps!

Hi @daveman1010221,

Thanks for the PR! I have linked the PR to the OP within this thread.

I do see a lot of extra files within the compiler bridge folder. All we require from the überSpark tool-kit perspective are two files:

  1. uberspark-bridge.Dockerfile – the dockerfile for the bridge
  2. uberspark.json – the überSpark JSON manifest describing the bridge and its use

I noticed your comment on testing the bridge before you move to the aforementioned adapter. You can test a bridge build using the überSpark command-line tool and specifically the uberspark bridge config command. Please see the following thread for more information:

The above thread should give you an idea of how to structure the bridge folder contents as well as how to test the bridge builds.

For now, it would suffice to test bridge execution (runs) via docker run on command line with ccomp as the starting executable. If that works, then we are good to go.

Please let me know when you have a revised PR for review. Thanks!

@daveman1010221, looking at your PR, I think that your dockerfile could be simplified by using an existing opam container as the base. Perhaps if you model your Dockerfile after the one in build-trusses/build-x86_64.Dockerfile where it starts from an opam base image (or an ubuntu version ocaml/opam:ubuntu-16.04_ocaml-4.05.0_flambda) would simplify this?

Agreed. Looking at the PR closer, it does seem like the dockerfile could benefit from the opam base image.

An experimental (working) version of a dockerfile with compcert and frama-c which was used to build an earlier version of the überSpark toolkit. Might be useful to grab some ideas from there:

In any case, we don’t need to be particular about a specific distro/image source, as long as we can construct different versions of the compcert compiler bridges in a reproducible manner.

Thanks!

Hi @daveman1010221,

I have added my review comments on the PR. Please take a look.

Also, can you confirm if you can build your new bridges via the uberspark bridge config command line?

For example, to build the compcert compiler bridge you would issue:

uberspark bridge config amd64/x86_32/generic/compcert/v3.1 --cc --build --root-dir=<root_dir>

where <root_dir> is where you installed überSpark within your development environment

Note: you will need to install the uberspark tool-kit before trying this out. See https://docs.uberspark.org/nextgen-toolkit/genuser-guide/install.html

Thanks!

Hi @daveman1010221,

Any updates on this PR per the previous post? I would like to merge this in once its ready :slight_smile: Thanks!

Ok, we’re good. Removing the root-dir, then doing ‘staging create…’, followed by a ‘bridge config…’, now results in the creation of a container. I’ve updated the pull request. The problem was apparently, I had named the Dockerfile as ‘uberspark_bridges.Dockerfile’, when the framework was expecting to find ‘uberspark-bridge.Dockerfile’. I named the file, based on an existing example, so I’d guess the example is broken, too.

That is interesting, that the uberspark.json file has the "container_fname" : "uberspark_bridges.Dockerfile" while the actual file is uberspark-bridges.Dockerfile

1 Like

@Cap, Indeed, container_fname is a defunct field and the tool-chain automatically looks for uberspark-bridge.Dockerfile.

@daveman1010221: Can you please remove:

src-nextgen/bridges/cc-bridge/container/amd64/x86_32/generic/compcert/v3.1/README.md

and update your PR? The README is describing general docker related stuff that is not really useful from the uberSpark tool-chain perspective.

I am happy to merge this once this has been resolved.

Thanks for getting this working.

As a side note: How hard is it to adapt this to support other Compcert compiler versions?

README file removed.

The main thing that must be addressed with each release of CompCert is that they update their OCaML dependencies. I started building this v3.1 container, using the latest documentation on CompCert’s website for building CompCert and found that the process had significantly diverged from their documented process. So it’s possible to get versions of the container for each CompCert, but it’s a process of figuring out the dependencies.

PR merged.

So it’s possible to get versions of the container for each CompCert, but it’s a process of figuring out the dependencies

Thanks @daveman1010221, let us work on a separate task to add support for other Compcert versions based on this PR.

I am locking this thread as this task is complete!