Setting up an analysis with the help of frama-c-script

Frama-C 18 (Argon) includes a new command, frama-c-script, which contains a set of helpful scripts for setting up new analyses. The available commands will likely expand in the future. We present here a quick overview of how to use them efficiently for a very fast setup.

Presentation of frama-c-script

frama-c-script is not a Frama-C plugin, but a command that is installed along with frama-c and frama-c-gui, starting from version 18.0 (Argon). Running frama-c-script on your terminal will output its usage messsage, which includes the list of available commands (which may change in the future):

usage: frama-c-script cmd [args]

  where cmd is:

  - make-template [dir]
      Interactively prepares a template for running analysis scripts,
      writing it to [dir/GNUmakefile]. [dir] is [.] if omitted.

  - make-path
      [for Frama-C developers and advanced users without Frama-C in the path]
      Creates a frama-c-path.mk file in the current working directory.

  - list-files [path/to/compile_commands.json]
      Lists all sources in the given compile_commands.json
      (defaults to './compile_commands.json' if omitted).
      Also lists files defining a 'main' function
      (heuristics-based; neither correct nor complete).

  - flamegraph <flamegraph.txt> [dir]
      Generates flamegraph.svg and flamegraph.html in [dir]
      (or in the FRAMAC_SESSION directory by default).
      Also opens it in a browser, unless variable NOGUI is set.

These commands are often related to the analysis scripts described in previous blog posts, but independent; frama-c-script facilitates the usage of analysis-scripts, but it also has commands which do not require them.

Each command is actually a script in itself, and may thus require other interpreters (e.g. Python or Perl).

Standard usage of frama-c-script

The diagram below illustrates where frama-c-script participates in the workflow of an analysis: in the creation of a makefile template, and also after the analysis, for profiling. Both usages will be detailed in this post.

Currently, frama-c-script is ideally used in conjunction with a JSON compilation database. As described in a previous blog post, CMake, Build EAR or other tools can be used to produce a compile_commands.json file, containing the list of compilation commands along with their arguments.

Once you have a compile_commands.json file, run:

frama-c-script list-files

It will parse the file and list all sources in it, in a Makefile-compatible syntax. It will also output the list of files containing definitions for a main function. This typically includes the main application itself, but also test cases or secondary applications, which can all be useful entry points for an analysis with Eva.

frama-c-script does not parse the source files to find function definitions; instead, it uses regular expressions to identify likely definitions, which can give both false positives and false negatives. This is a necessary approach since, during this stage, it is too early to have a full, parsable AST to begin with.

With the list of source files, we can now easily create a Makefile template for our application. The make-template command will interactively create a new GNUmakefile in the current directory, after asking for some data:

• Name of the main make target;
• List of source files.

The name of the main target is usually the application name. It is also the default Makefile target and the prefix of the directories where the results will be stored (both for parsing and for the analysis with Eva).

The list of source files can be as simple as *.c, or more sophisticated for projects with subdirectories and multiple main functions, in which case some source files must not be included in the list. The list-files command will produce the list of sources when a compile_commands.json file is present.

After these values are filled in, the script will create a GNUmakefile in the current directory. The values are simply written inside the makefile to help kickstart it, but they can be manually edited afterwards.

Ideally, this should be enough to try parsing the source files by running simply make. From then on, the analysis-scripts methodology takes over, and the usual commands (make parse, make, make gui) work as usual.

Easily visualizing flamegraphs

One of the options in frama-c-script is related to flamegraphs.

Flamegraphs are stack trace visualizations which, in Frama-C/Eva, are used to help understand in which functions the analysis spends most of its time. Option -eva-flamegraph has been added in Frama-C 14 (Silicon), and it activates the generation of a flamegraph trace file during the analysis. This file can then be given to the flamegraph.pl Perl script developed by Brendan Gregg to produce an image in SVG format.

The image below provides an example of a flamegraph for the PolarSSL code in Frama-C’s open-source-case-studies repository. The stacks start from the top, with the main function, and then each called function is stacked underneath. The length of the bar is the amount of time spent in it. Hovering over a bar shows the function name and the percentage of time spent in the function. Clicking on a bar will zoom on it, increasing the size of its children for better readability. Note that bar colors do not have any special meaning.

The flamegraph command available in frama-c-script is simply a shortcut to help generate the image file for the flamegraph (along with an HTML wrapper) and open it in a browser. The flamegraph.pl script itself is distributed in the Frama-C share directory, which simplifies its usage.

Since the analysis-scripts options already include the generation of flamegraphs by default (option -eva-flamegraph is set by FRAMAC_SHARE/analysis-scripts/frama-c.mk), the user simply needs to run:

frama-c-script flamegraph <target>.eva/flamegraph.txt

And the user’s default browser should display the flamegraph generated during the analysis.

Note that flamegraphs can be generated while the analysis is still running; this is useful, for instance, when the analysis is seemingly “frozen” in a given point, without emitting any messages. Running frama-c-script flamegraph will create a flamegraph of the current state of the analysis, while the trace file is still updated by the ongoing analysis.

Conclusion

The features currently available in frama-c-script offer extra comfort when setting up new analyses, by minimizing the amount of repetitive or hard-to-memorize tasks.

list-files requires a JSON compilation database, but it helps obtain the information for creating a GNUmakefile. make-template creates a GNUmakefile which can be manually edited later. flamegraph helps visualize the performance of the analysis, either while it is running, or afterwards.

One of the new commands expected for Frama-C 19 (Potassium) will help find which files in a directory declare and/or define a given function. This will help, for instance, when trying to identify which .c file to include to obtain the body of a function that is called from another source.