Commit 8ab325cc authored by Andre Maroneze's avatar Andre Maroneze 💬

Merge branch 'blog-no-autoload-modules' into 'master'

[blog] add post about benchmarking and -no-autoload-plugins

See merge request !108
parents fa54240d 0072d3ff
Pipeline #32841 passed with stage
in 1 minute and 43 seconds
---
layout: post
author: André Maroneze
date: 2021-02-16 12:00 +0100
categories: benchmarks
title: "When benchmarking Frama-C, consider option -no-autoload-plugins"
---
When using Frama-C in a series of benchmarks or test suites, especially when
they consist of several small programs, consider using `-no-autoload-plugins`
for better performance. This post explains why it is useful, as well as its
downsides.
## Minimize startup time with `-no-autoload-plugins`
By default, running `frama-c` makes it load all of its plugins
(over 30 on version 22 - Titanium), resulting in a non-negligible startup
time: about 0.2 seconds on a fast laptop. For most uses of Frama-C, this
is dwarfed by the execution time of the plugins themselves.
However, when parsing hundreds or thousands of small test files
(such as those in the [Juliet test suite](https://samate.nist.gov/SARD/testsuite.php)),
this adds up. Adding option `-no-autoload-plugins` avoids this overhead, by
charging *no* plugins at all. This option is best combined with the explicit
loading of the plugins that are of interest to you, via option `-load-module`,
followed by the plugin module names.
For instance, to run Eva, the following list of plugins is sufficient in most
cases:
frama-c -no-autoload-plugins -load-modules eva,scope,variadic <other options, filenames, etc.>
Note: when `-no-autoload-plugins` is set, some plugin dependencies are *not*
loaded. This may result in failures when functions are requested from other
plugins; usually, running the analysis on a few examples is enough to detect
such cases, and the error message provides hints about which plugins are
missing. Here's a brief explanation why the above plugins are useful in
conjunction with Eva:
- `scope`: this plugin is used by Eva at the end of an analysis, when removing
(syntactically) redundant alarms, unless option
`-eva-no-remove-redundant-alarms` is used;
- `variadic`: during parsing, the Variadic plugin instantiates calls to variadic
functions such as `printf` and `scanf`, adding ACSL
specifications. Without Variadic, Eva will raise warnings when
these functions are called.
This usage of `-no-autoload-plugins` is present in several of Frama-C's
non-regression test suites, as well as in some
[open source case studies](https://git.frama-c.com/pub/open-source-case-studies)
composed of several small tests (e.g. `cerberus`).
## Finding Frama-C module names to use with `-load-module`
By giving Frama-C plugin names to `-load-module`, you can load the plugins
you need for your specific analysis, but you must know its module name.
This is often the plugin's *short name*, that is, the prefix of its options,
which you can consult via `frama-c -plugins`. For instance, Eva's module name
is `eva`, InOut's is `inout`, etc. Only a few plugins do not follow this rule,
mostly for historic reasons:
- Markdown report's module name is `markdown_report`, instead of `mdr`;
- RTE's module name is `rtegen`, instead of `rte`;
- Semantic constant folding is `constant_propagation`, instead of `scf`;
- Loop Analysis (deprecated) is `loopanalysis` and not `loop`;
- Callgraph is `callgraph`, not `cg`.
Overall, just remember that OCaml module names cannot contain hyphens `-`
nor spaces, only underscores.
Also, note that the *actual* name of these module is prefixed by `frama-c-`,
but `-load-module` automatically tries adding the prefix when it does not
find another module with the same name. Thus you can use
`-load-module frama-c-eva` instead of `-load-module eva`, for instance.
## Conclusion
Frama-C's default configuration is optimized for typical analysis tasks and
easier plugin integration; however, when running benchmarks with thousands
of small files, using `-no-autoload-plugins` and manually selecting plugins
via `-load-module` is a more efficient approach.
When running any kind of benchmarks or large-scale comparison between
Frama-C and other tools, do not hesitate to contact us; we may be able to
provide usage tips to help you get faster results, and we are always interested
in seeing how people use Frama-C.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment