diff --git a/_posts/2021-02-16-benchmarking-frama-c.md b/_posts/2021-02-16-benchmarking-frama-c.md new file mode 100644 index 0000000000000000000000000000000000000000..9a32ace15c1988745f1d9c7839932b58813028b9 --- /dev/null +++ b/_posts/2021-02-16-benchmarking-frama-c.md @@ -0,0 +1,85 @@ +--- +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.