Analysis scripts: helping automate case studies, part 1

(kindly reviewed by T. Antignac, D. Bühler and F. Kirchner)

Among Frama-C 16 Sulfur’s new features, one of them is dedicated to help setting up and iterating case studies. In this series of posts, we will explain how to use such scripts to save time when starting a new case study with EVA.

This series supposes some familiarity with EVA, as in, its basic usage is not detailed. Reading A simple EVA tutorial or the tutorial in the EVA user manual should be sufficient.

In this first part, we will explore the basics of the analysis-scripts framework and its use on an open source project. We will see how to get the preprocessor flags needed to prepare an analysis template. This template is in fact a Makefile which will be used to set up the analysis. It will enable us to define the sources to parse by editing its targets.

In the next post, we will see that, once the set-up is done, the analysis steps are similar to the ones presented in previous EVA tutorials: run a simple analysis, then refine, improve the precision, iterate. Once an analysis has been run, we will see how to track red alarms to improve the coverage. This will lead to some syntactic fixes that will allow the analysis to go further.

Analysis scripts

The release 16 (Sulfur) of Frama-C includes a small set of files, called analysis scripts, whose purpose is to help starting new analyses with Frama-C. It is currently focused on analyses with EVA, but other plug-ins such as WP and E-ACSL may incorporate it as well.

The new files are available in the analysis-scripts of Frama-C’s share directory. Use frama-c -print-share-path to obtain its exact location. This directory currently contains a README, two small Bash scripts and a Makefile (frama-c.mk) which contains the bulk of it.

Note: the README.md mentions fcscripts, the old name of this set of files (it was already being used by the open-source-case-studies Git repository, under that name, but now it is part of the Frama-C release). The upcoming Frama-C release will update that.

analysis-scripts relies on some GNU-specific, Make 4.0+ features. This version of Make (or a more recent one) is already available on most Linux distributions and on Homebrew for MacOS, but in the worst case, downloading and compiling GNU Make from source should be an option.

Basically, what these files provide is a set of semi-generated Makefile targets and rules that automate most of the steps typically used by Frama-C/EVA developers to set up a new case study. The scripts themselves are extensively used in the open-source-case-studies repository, which serves as use example.

Using analysis scripts

To illustrate the use of analysis-scripts, we picked one project from ffaraz’s awesome-cpp repository: GHamrouni’s Recommender, a library from the Machine Learning section.

We start by cloning the repository¹:

git clone git@github.com:GHamrouni/Recommender.git

¹ Note: at the time of this posting, the latest commit is 649fbfc. The results presented later in this tutorial may differ in the future. You can select this commit via git checkout 649fbfc in case this happens.

Then, inside the newly-created Recommender directory, we look for its build instructions. Many C open-source libraries and tools are based on autoconf/configure/make, which may require running some commands before all headers are available (e.g., ./configure often produces a config.h file from a config.h.in template). Frama-C does not require compiling the sources, so in most cases you can stop before running make. However, since Frama-C does require preprocessor flags, you can use existing Makefiles to cheaply obtain that information.

Obtaining preprocessor flags from a compile_commands.json

In order to find out which preprocessor flags are needed for a given program, you can use tools such as CMake or Build EAR to produce a JSON compilation database, commonly called compile_commands.json. This is a JSON file which contains the list of commands (including all of their arguments) to be given to the compiler. It contains many options which are irrelevant to Frama-C (such as warning and optimization flags, typically -W and -O), but it also contains preprocessor flags, mostly -I and -D, which we are interested in.

The compile_commands.json file can be produced as follows:

1. If the project is based on CMake, add -DCMAKE_EXPORT_COMPILE_COMMANDS=ON to the cmake command-line, e.g. instead of cmake <source dir>, use cmake <source dir> -DCMAKE_EXPORT_COMPILE_COMMANDS=ON.

2. If the project is based on Makefile, use Build EAR. After Build EAR is installed, you just have to prefix make with bear: typing bear make is usually enough to obtain the JSON database.

Note: Frama-C 17 (Chlorine) includes option -json-compilation-database, which allows using compile_commands.json directly, rendering the next step unnecessary.

Once you have the file, simply grep it for -I and -D flags, e.g:

grep '\-I\|\-D' compile_commands.json

Those flags should be added to the preprocessor flags in Frama-C’s Makefile (described in the next section), CPPFLAGS.

Note that these recommendations may not work in complex setups. Manual inspection of the commands used during compilation might be necessary to obtain all necessary flags.

Preparing an analysis template

We will create a Makefile for Frama-C, to manage dependencies and help re-run analyses. In order to avoid having to type make -f <name> each time, we will name it GNUmakefile, for the following reasons:

1. GNU Make gives preference to GNUmakefile over Makefile if both exist, so the default file used when typing make will be ours, even if the project already has its own Makefile;

2. This avoids having to rename/overwrite existing makefiles (or, worse, having Frama-C’s Makefile erased when re-running ./configure);

3. The analysis-scripts Makefile already relies on some features specific to GNU Make, so there is no compatibility downside here.

If you want to name your Makefile otherwise, just remember to always add -f <your makefile name> to the make commands presented in this tutorial.

Our GNUmakefile will be created with content based on the template (update: previously) available on Frama-C’s Github repository. (update: The template is now distributed with Frama-C).

In this tutorial, we consider that Frama-C is installed and in the PATH to keep the template concise.

include $(shell frama-c-config -print-share-path)/analysis-scripts/frama-c.mk

# Global parameters
CPPFLAGS     =
FCFLAGS     +=
EVAFLAGS    +=

export FRAMA_C_MEMORY_FOOTPRINT = 8

# Default targets
all: main.eva

# Input files
main.parse: <TO BE COMPLETED>

The essential element to complete this template is the list of files to be parsed. Other arguments, such as flags for the C preprocessor (CPPFLAGS), for the Frama-C kernel (FCFLAGS) and for the EVA plug-in (EVAFLAGS) are also to be filled by the user, when necessary.

Finally, note that the target name (main) is completely arbitrary. You can have multiple targets if your code contains multiple main functions. The important part is the use of the suffixes .parse and .eva, which are hard-coded in the analysis-scripts’ Makefile to generate targets with the appropriate dependencies and rules.

The .parse suffix is used by analysis-scripts to set the list of source files to be parsed. It is associated to an .eva target which runs the EVA analysis. This target is generated by analysis-scripts itself; we just need to tell the Makefile that it should be run when we run make all, or simply make, since all is the first rule in our Makefile.

Setting sources and testing parsing

The list of source files to be given to Frama-C can be obtained from the compile_commands.json file. However, it is often the case that the software under analysis contains several binaries, each requiring a different set of sources. The JSON compilation database does not map the sources used to produce each binary, so it is not always possible to entirely automate the process. You may have to manually adjust the sets of files to be given to Frama-C. For a whole-program analysis with EVA, in particular, you might want to ensure that there is exactly one file defining a main function.

In the case of Recommender, since it is a library, the src directory does not contain a main function. However, the test directory contains two files, each of them defining a main function. In this tutorial, we will use the test.c file as the main entry point of the analysis. We could also have used the -lib-entry option on one or more functions in the library. More advanced users of Frama-C may prefer this option though we will keep it simple and use the main function in test.c as unique entry point in this tutorial.

Therefore, the list of sources to be filled in the main.parse target is the following:

main.parse: src/*.c test/test.c

We can test that Frama-C is able to parse the sources:

make main.parse

If you are strictly following this tutorial, you should have the following error:

[kernel] Parsing test/test.c (with preprocessing)
test/test.c:1:25: fatal error: recommender.h: No such file or directory
 #include "recommender.h"
                         ^
compilation terminated.

This is because we never included the actual -I lines that we found in the compile_commands.json file. Note that they include flag -I../../src/, which is relative to one of the subdirectories in tools/*. Since our Makefile (and thus Frama-C) will run relative to the base directory in Recommender, the actual include directive needs to be -Isrc, which we add to CPPFLAGS:

CPPFLAGS= -Isrc

Running make main.parse now should succeed. Run it again. You will notice that nothing is done: thanks to the dependencies managed by analysis-scripts, unless you modify one of the source files, or the flags given to Frama-C (CPPFLAGS or FCFLAGS), Frama-C will not waste time reparsing the results: they have already been saved inside the main.parse directory.

Contents of the .parse directory

For each .parse target, analysis-scripts will create a corresponding directory with several files:

• command: the command-line arguments used by Frama-C;
• framac.ast: the pretty-printed normalized AST produced by Frama-C;
• stats.txt: performance information (user time and memory consumption);
• warnings.log: warnings emitted during parsing;
• framac.sav: a Frama-C save file (a binary) with the result of parsing;
• parse.log: the entire log of the parsing (includes the warnings in warnings.log).

All of these files are used internally by the analysis scripts or some other tools (notably for regression testing and profiling purposes), however only the last 2 files are occasionally relevant for the end user:

• framac.sav can be used with frama-c -load, for instance when trying different plug-ins;
• parse.log contains a copy of all messages emitted during parsing.

If we want to load the parsed files in the Frama-C GUI, we can use either frama-c -load framac.sav, or more conveniently, make main.parse.gui. The advantage of the latter is that it will generate the .parse directory if it has not been done already.

This concludes the first part of this tutorial. In the next post, we will run EVA using our Makefile, then iterate to improve the analysis.