Frama‐C module implementation

Discussions and open questions

This Wiki is made in order to discuss the way to integrate a Frama-C modulle into meson, and how to define the exported API (function signatures and logic) to meson users

Module conception model, question to solve:

Module integration:

1. Do we consider the module as a test() derivative ? (i.e. triggered by meson test ?
2. Do we support specific meson target (i.e. new meson proof target) ?
3. Do we define the module API as generic targets, that can be a dependency of any others (like custom_target() meaning that the user is free to describe dependencies in other targets such as test() but also other ones.

The third solution seems better as it is less intrusive into meson core, and leave the integration model into projects to project's developers.

Module import is a standard meson mechanism:

framac = import('framac')

About potential module API and signatures

API signature definition. Required fields are prefixed by *

Frama-C execution configuration API

parsing signature:

void parse(
  *str: name,                                    # unique identifier
  *input: list(files|source_set|build_tgt)       # source to parse (list of sources, being a configured source set, files or files list
                                                 # supporting generated sources is clearly a requirements (through, for e.g. build_tgt)
  *entrypoint: str,                              # entrypoint from which the kernel start analysis
  timeout: int                                   # analysis timeout (default 300 ?)
  machdep: str                                   # str is not strict enough... default to x86_32 ?
  cpp_extra_flags: list(str),                    # extra CPP cflags if needed, should be, most of the time, useless
  depends: list(build_dep)                       # target dependencies if required (source generation, etc.)
)

To note: the input would probably be only a build-target, at least to start with, because:

• in a given repository, multiple build target exists
• given a repo, we may which to parse:
  • sources associated to a given executable() (being the executable build target)
  • sources associated to a given library()

This is logic to require to analyse a build target, as associated to it, all derivative dependencies being reachable through the meson internals. In that case, this is normal to consider that:

• considering a target (executable or library, this information being useful as it impacts the frama-c options)
• getting the overall sources (known by meson)
• considering the associated API (for libraries, being defined in the library infos, through include_directory field

We can:

• use a given entrypoint (may be manually written)
• reduce WP analysis to the API functions (setting the -wp-fct flag) when being a library

For example, considering the following library:

my_lib = static_library(
    'mylib',
    sources: [
        mylib_set_config.sources(),
        mylib_header_set_config.sources(),
    ],
    include_directories: mylib_inc,
    c_args: [ target_arch_args, global_build_args ],
    install: false,
    dependencies: [ mylib_source_set_config.dependencies(), external_deps],
)

the sources and include directories are useful for Frama-C, while some others can also be acceded through the meson internal informations used to generate the build_command.json file. As a consequence, the build_command.json is no more needed as the frama-c plugin has access to the meson current context.

We then can imagine:

framac = import('frama-c')
enrypoint = files('mylib_eva_main.c')

framac.parse(
   'frama-c-mylib-parse',
   input: my_lib,
   entrypoint: entrypoint,
   timeout: 300,
   machdep: 'x86_32.gcc'
)

If a part of the sources have dependencies in order to be generated, this can be, probably, naturally handled by meson, as the lib being an input of the function, all its own dependencies would be resolved and build for those for which it is required.

the session output dir can easily be forged in the same way meson targets do: using, in the above case, a frama-c-arch-eva.session.p, for example, in the build directory in a similar path to the source directory (meson keeping homogeneous hierarchy between source and build directories).

Link between meson frama-c plugin and Frama-C

There are two ways, it seems, to interact with Frama-C:

• detect the Frama-C binary (in the way find_program() meson function does) and use it directly through python
• using the Frama-C server associated to Ivette, in order to use a programmatic mechanism. In that later case:
  1. the server is started by the module
  2. the module check for server existence, then, if needed, start it
  3. the server start is under the user's responsability
  4. it is possible to start (and configure the server's IP/port) in the plugin, and instead fallbacking to manual or spawning mode

This needs to be analyzed afterward. The configurable server interface may be interesting for various use cases, such as using a remote service for analysis, supporting a SAAS at cloud or local LAN level, and so on. This is mostly dependent of what CEA-LSL wish to do