Using Singularity/Apptainer for easy-to-use Docker images

The Frama-C Docker images are useful for continuous integration, but for interactive use, they are not very practical: by default, Docker does not provide access to the local filesystem, and running the Frama-C GUI requires using derived tools such as x11docker. In this post, we briefly show an alternative, with Singularity, which has the advantages of including, by default, host filesystem integration and graphical application support without additional configuration.

Singularity for Frama-C, in a nutshell

Singularity (now split in two projects, Apptainer and SingularityCE), in this post, is seen as a Linux-based application to run a Frama-C-based Docker image. Its advantage is that the user does not have to install and manage Frama-C and its dependencies (OCaml, opam, etc), like when using the Docker image; but also, when running frama-c or frama-c-gui, the user has direct access to the local filesystem and to the graphical interface, without having to use tools such as x11docker, or mounting volumes. This should, hopefully, make Frama-C very easy to test on simple examples, at the cost of increased disk space usage.

Instructions for running Frama-C via SingularityCE on a Ubuntu

The following has been tested on a Ubuntu 22.04 machine. Hopefully, similar steps should work for other versions of Ubuntu as well as for Debian-based systems. For other Linux distributions, such as Fedora, there are existing packages that allow skipping the first few steps.

For Ubuntu 22.04:

• Go to https://github.com/sylabs/singularity/releases and download the DEB package for your Ubuntu release (e.g., jammy for Ubuntu 22.04);

• Run sudo apt install ./<downloaded_file>.deb; this will install the locally-downloaded package. Note: in our test machine, we had to add --fix-broken to the above command, to make sure some required dependencies were also installed.

• Singularity can build its instances from several sources, such as local Docker images, or images from the Docker Hub. For the latter, we can run the following command:

    singularity instance start docker://framac/frama-c-gui:26.0 fc26

  This will (1) download the framac/frama-c-gui:26.0 image from the Docker Hub, then create an instance and name it fc26. You can change fc26 to the name you prefer; a short one should make it easier to type (as seen below). You can also use Frama-C’s dev images (replacing 26.0 with dev) to obtain an image based on the current development version of Frama-C (public Git).

• Now, whenever you want to run a command from the instance, such as frama-c file.c <options>, you just need to prefix it with singularity exec instance://fc26. For instance, inside the Frama-C source distribution there is a tests/idct directory. We can cd to it and run:

    singularity exec instance://fc26 frama-c-gui *.c -eva

  This should get the Frama-C GUI running, run Eva and then display the AST and analysis result.

Note: a similar setup has been tested on Arch Linux (with Sway), and on Fedora (with both X and Wayland). The Fedora + Wayland setup required changing some settings related to X (xhost +local:). All this to say, your mileage may vary, but hopefully it should be easier than using the Docker image directly.

Limits of the Singularity filesystem integration

Singularity tries to provide a seamless integration between its instance and the host system (including e.g. access to the filesystem), but some unexpected behaviors may happen; Frama-C has not been exhaustively tested inside this environment!

For instance, GTK applications may try to access data in temporary folders which are made read-only by Singularity, resulting in warnings and error messages. Still, in our (limited) tests, most GUI features seemed to work fine despite the warnings.

Also, note that the mixture between the “host” filesystem and the container’s can cause unintuitive behaviors. For instance, if you want to run WP (and thus need to run why3 config detect beforehand), the command singularity exec instance://fc26 why3 config detect will overwrite the ~/.why3.conf file in the host’s home directory, but the file will mention paths which only exist inside the container. This can lead to problematic situations, especially if you later install Frama-C in the host machine as well.

Conclusion

Singularity offers an easier approach to “running a container integrated with its host” than Docker: having access to the graphical interface and the host filesystem by default is extremely useful when trying to run Frama-C on Linux, without having to install and configure OCaml-related tools, or manage opam switches.