Using Singularity/Apptainer for easy-to-use Docker imagesAndré Maroneze (kindly tested by D. Bühler, V. Prevosto et al) - 1st Feb 2023
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-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.,
jammyfor Ubuntu 22.04);
sudo apt install ./<downloaded_file>.deb; this will install the locally-downloaded package. Note: in our test machine, we had to add
--fix-brokento 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.0image from the Docker Hub, then create an instance and name it
fc26. You can change
fc26to the name you prefer; a short one should make it easier to type (as seen below). You can also use Frama-C’s
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/idctdirectory. We can
cdto 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.
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.