MOPSA is a research-oriented static analyzer which includes a tool called mopsa-build, a wrapper for build commands (esp. make) that helps the analysis. Frama-C can now use the same tool to help automate some parsing steps!

JSON Compilation Databases (JCDBs, a.k.a. compile-commands.json)

A JSON Compilation Database (referred from now on as JCDB) lists compilation commands used to build a given application. These commandes include, among others, preprocessing-related options such as -I and -D. Code analyzers for C (such as Frama-C and Mopsa) need this information before they can parse the code.

Several tools exist to store such data. In the past, we used mostly Build EAR (Bear) and CMake’s CMAKE_EXPORT_COMPILE_COMMANDS variable. Both tools produce a compile_commands.json file that Frama-C can read using option -json-compilation-database (this option has just been renamed -compilation-db).

Limitation of JCDBs

The main limitation of a JCDB is that is does not track relations between objects and sources. For instance, assume the following Makefile:

app: a.o b.o
    gcc a.o b.o -o app

a.o: a.c
    gcc -c a.c -o a.o -D FOO -I bar

b.o: b.c
    gcc -c b.c -o b.o -D BAZ -I qux

Its JCDB will contain three separate entries (one for each call to GCC). But a Frama-C user who wants to analyze the code of app must manually inspect the file to realize that app depends on a.c and b.c, so that they can run:

frama-c -compilation-db compile-commands.json a.c b.c

While, ideally, they would prefer something like this:

frama-c -compilation-db compile-commands.json -sources-from app

And let the tool find out which sources were used to build app.

Mopsa-Build and Mopsa-DB to the rescue

mopsa-build is a sophisticated wrapper for build tools: it intercepts calls to relevant build commands (mainly gcc, but also ar, mv, and others) and stores them in a database. Then, a companion tool mopsa-db converts the binary database into a JSON file, which is similar to a JCDB. Here is a mopsa-db.json file for the aforementioned Makefile:

{
  "dbfile": "/tmp/app/mopsa.db",
  "contents":
[  {
    "filename": "/tmp/app/a.o",
    "type": "object",
    "lang": "C",
    "source": "/tmp/app/a.c",
    "args": ["-D", "FOO", "-I", "/tmp/app/bar"],
    "path": "/tmp/app"
  },
  {
    "filename": "/tmp/app/b.o",
    "type": "object",
    "lang": "C",
    "source": "/tmp/app/b.c",
    "args": ["-D", "BAZ", "-I", "/tmp/app/qux"],
    "path": "/tmp/app"
  },
  {
    "filename": "/tmp/app/app",
    "type": "executable",
    "contents": ["/tmp/app/b.o", "/tmp/app/a.o"]
  }]
}

The relevant extra fields w.r.t. a JCDB are type and source. The former allows identifying useful targets (for instance, entries of type executable), while the latter maps the relation between an object and its sources (e.g. between a.o and a.c). Thanks to this, Frama-C’s new options -mopsa-db and -mopsa-target allow reading such databases, listing available targets, and selecting the sets of source files to be parsed.

Complete usage example of Mopsa-build and Frama-C

Assuming the same Makefile and sources as before, here is the complete list of commands to run:

$ mopsa-build make                # produces a mopsa.db (binary) file
$ mopsa-db -json > mopsa-db.json  # converts mopsa.db into a JSON file
$ frama-c -mopsa-db mopsa-db.json # lists available targets
[kernel] targets:
  [executable] app
$ frama-c -mopsa-db mopsa-db.json -mopsa-target app <other frama-c options>

Note that, in the last line, you can add extra sources (e.g. Frama-C’s standard library stubs) and options (e.g. -save parsed.sav).

For more details about -mopsa-*-related options, check the Frama-C user manual or run frama-c -kernel-help.

Note: as of this writing, this feature is not yet available in a stable Frama-C release, therefore you need to compile the development version of Frama-C (https://git.frama-c.com/pub/frama-c). It will be available in the next Frama-C release (32 - Germanium).

Conclusion

mopsa-build improves the usability of the analysis setup stage in Frama-C. By reusing the same format available in Mopsa, we avoid reinventing the wheel and hope this might help other tools converge towards a unified (maybe, one day, standardized?) format for such analyses.

A minor drawback is that this currently requires installing the whole Mopsa platform; but for those used to running opam install frama-c, there are but a few extra dependencies required by opam install mopsa. If other people become interested in this format, Mopsa developers might consider splitting it out of Mopsa in the future, as a standalone tool.

Acknowledgments

We would like to thank Antoine Miné for several minor fixes, improvements and tips concerning mopsa-build. And, of course, many thanks to all mopsa-db and mopsa-build developers.