AstraVer Toolset » Deductive Verification Tools for Linux Kernel

For the attached input source files Frama-C (CIL) needs more than 1 GB or RAM on the following command:

toplevel.opt "-no-autoload-plugins" "-no-findlib" "-c11" "-kernel-warn-key" "CERT:MSC:38=active" "-keep-logical-operators" "-remove-unused-inline-functions" "-remove-unused-static-functions" "-print" "-print-lines" "-no-print-annot" "-ocode" "cil.i" ".tmp_ib_media.abs-paths.trimmed.i" ".tmp_msg.abs-paths.trimmed.i" ".tmp_node.abs-paths.trimmed.i" ".tmp_handler.abs-paths.trimmed.i" ".tmp_bcast.abs-paths.trimmed.i" ".tmp_node_subscr.abs-paths.trimmed.i" ".tmp_ref.abs-paths.trimmed.i" ".tmp_discover.abs-paths.trimmed.i" ".tmp_port.abs-paths.trimmed.i" ".tmp_server.abs-paths.trimmed.i" ".tmp_net.abs-paths.trimmed.i" ".tmp_config.abs-paths.trimmed.i" ".tmp_socket.abs-paths.trimmed.i" ".tmp_name_distr.abs-paths.trimmed.i" ".tmp_core.abs-paths.trimmed.i" ".tmp_bearer.abs-paths.trimmed.i" ".tmp_log.abs-paths.trimmed.i" ".tmp_subscr.abs-paths.trimmed.i" ".tmp_link.abs-paths.trimmed.i" ".tmp_name_table.abs-paths.trimmed.i" ".tmp_sysctl.abs-paths.trimmed.i" ".tmp_eth_media.abs-paths.trimmed.i" ".tmp_netlink.abs-paths.trimmed.i" ".tmp_addr.abs-paths.trimmed.i" "atomic.abs-paths.trimmed.i" "dd.abs-paths.trimmed.i" "spi.abs-paths.trimmed.i" "err.abs-paths.trimmed.i" "panic.abs-paths.trimmed.i" "common.abs-paths.trimmed.i" "slab.abs-paths.trimmed.i" "memory.abs-paths.trimmed.i" "gcc.abs-paths.trimmed.i" "nondet.abs-paths.trimmed.i" "reference memory.abs-paths.trimmed.i" "environment_model.abs-paths.trimmed.i" "spinlock.bk.abs-paths.trimmed.i" "bug kind funcs.trimmed.i" 

CIL 1.5.1 needed less than 140 MB of RAM.

I tried to investigate the allocation profile of Frama-C on a subset of the attached files with Spacetime (Spacetime incurs a very large memory overhead, so when the uninstrumented program takes ~1GB of RAM with spacetime it takes ~14GB and processing the collected profile takes more than 16GB and was unsuccessful on my machine, so I profiled for a small subset of files). Unfortunately, I couldn't discover any outstanding culprit. Here's an example of the profile:

The only suspicious blue stripe (in the center, the bottom one is for unknown allocation source, e.g. in the C bindings) is from varinfos (various data attached to variable definitions e.g. type, location, scope etc.), another light green stripe is from various locations i.e. source code location data attached to expressions, statements, variable definitions etc. Removing location information from expressions (CIL dosn't keep it and uses per-statement granularity) only reduces memory footprint by 100-200M on this set of files. There's also an option "-agressive-merging", which enables merging more similar function and composite type definitions and reduces memory consumption by ~50M in this case. But a larger gain in reducing the memory overhead can likely be achieved only by more drastic changes across the entire Frama-C codebase such as removing some data kept for variable definitions and functions, removing some internal caches etc.

Another profile:

Again, the widest stripes are for exprs (upper pale grayish violet), varinfos (lower pale grayish violet), locations (gray), statement chunks (in code blocks) (upper light gray) and call argument lists (lower light gray)

My observation regarding this issue is that for most even quite large source files Frama-C (CIL) does not need very much memory (you can find examples attached to other issues), but in some cases it is very greedy. Surprisingly they all are Linux loadable kernel modules from file system and networking subsystems that have quite many source files (they are prefixed with ".tmp_" in source file archives). But the number of source files does not matter much. I attached another example with a driver having many source files as well, but it is from the sound subsystem and Frama-C (CIL) didn't need very much memory to process it. Thus, there are some specific things in sources for which Frama-C (CIL) consumes very much memory.

Frama-C (CIL) command for the attached archive:

toplevel.opt "-no-autoload-plugins" "-no-findlib" "-machdep" "gcc_x86_64" "-c11" "-kernel-warn-key" "CERT:MSC:38=active" "-keep-logical-operators" "-remove-unused-inline-functions" "-remove-unused-static-functions" "-print" "-print-lines" "-no-print-annot" "-ocode" "cil.i" ".tmp_emumpu401.abs-paths.i" ".tmp_emu10k1_main.abs-paths.i" ".tmp_p16v.abs-paths.i" ".tmp_emuproc.abs-paths.i" ".tmp_emu10k1_patch.abs-paths.i" ".tmp_emufx.abs-paths.i" ".tmp_irq.abs-paths.i" ".tmp_emu10k1_callback.abs-paths.i" ".tmp_emu10k1.abs-paths.i" ".tmp_io.abs-paths.i" ".tmp_emu10k1_synth.abs-paths.i" ".tmp_timer.abs-paths.i" ".tmp_voice.abs-paths.i" ".tmp_memory.abs-paths.i" ".tmp_emumixer.abs-paths.i" ".tmp_emupcm.abs-paths.i" "atomic.abs-paths.i" "dd.abs-paths.i" "spi.abs-paths.i" "err.abs-paths.i" "panic.abs-paths.i" "common.abs-paths.i" "slab.abs-paths.i" "memory.abs-paths.i" "gcc.abs-paths.i" "nondet.abs-paths.i" "reference memory.abs-paths.i" "environment_model.abs-paths.i" "spinlock.bk.abs-paths.i"