My colleague just noticed that, when running Frama-C in a switch with OCaml.5.0.0~beta1, memory consumption of Frama-C is about 10x larger when loading dynamic modules (i.e., any of Frama-C's plug-ins).

I created a Dockerfile to test it on an isolated environment and obtained the same results.

When comparing the same code compiled under OCaml 4.14.0 and OCaml 5.0.0~beta1, I obtained the following differences:

The two first lines are the most important ones; the others are provided only as possible clues for further investigation.

Memory usage is obtained by running /usr/bin/time -f "%M" (it reports maximum resident set size). Note that this is not just a theoretical issue (e.g. memory reserved but unused in practice): my colleague had his PC start swapping heavily when running a few dozen parallel instances of Frama-C, which doesn't happen with OCaml <= 4.14. This is when we decided to measure it.

I compiled and installed Frama-C, then ran it under the following configurations:

• Without any modules dynamically loaded: frama-c -no-autoload-plugins
• Default (all modules): frama-c
• A single module per execution: frama-c -no-autoload-plugins -load-module <plugin>

We notice that, without any modules, memory usage is the same in both versions. But when all modules are loaded, it is almost 1GB in OCaml 5, versus less than 100 MB in OCaml 4.14.

Here's a hackish Dockerfile to help reproduce it:

# We don't actually use the Frama-C installed in this image, it serves only
# as a opam-ready base image
FROM framac/frama-c:dev-stripped.fedora

RUN opam update && opam switch create 5.0.0~beta1 -y
# why3 installation may fail, hence the "|| true" below
RUN opam install --deps-only frama-c --confirm-level=unsafe-yes || true
RUN opam install dune-site --confirm-level=unsafe-yes
RUN sudo dnf install time -y
RUN git clone https://git.frama-c.com/pub/frama-c.git --depth=1
RUN cd frama-c && eval $(opam env) && make && make install
RUN eval $(opam env) && /usr/bin/time -f "Memory: %M" frama-c -no-autoload-plugins
RUN eval $(opam env) && /usr/bin/time -f "Memory: %M" frama-c
RUN eval $(opam env) && for p in aorai callgraph dive e-acsl eva from impact inout instantiate loop-analysis markdown-report metrics nonterm obfuscator occurrence pdg postdominators reduc report rtegen scope server slicing sparecode studia users variadic; do /usr/bin/time -f "Plugin $p: Memory: %M" frama-c -no-autoload-plugins -load-module $p; done

In this Dockerfile, all we do is (1) install a new opam switch, (2) install Frama-C dependencies, then (3) clone and install Frama-C itself (currently, it is not possible to run opam install frama-c on a 5.0 switch due to the lack of a compatible Why3). Finally, (4) run Frama-C and measure memory usage.

I simply replaced 5.0.0~beta1 with 4.14.0 in the first RUN to compare it with OCaml 4.14.

If you have any clues on what could be causing it and how to further investigate, please tell us. We'll try to take a look into it ourselves.