Hi !

Description

My project is twice as slow using ocaml 4.11 compared to ocaml 4.10, while changing 0 lines in the code.

It is a bit performance sensitive (low times are important when we try to defend our work..).
In particular, one run that is important for us now takes around 62s instead of 30s.

The issue is, the project is quite big, some of it is legacy code... I have no idea what feature is causing this.
If you have any pointers as to what could cause this, I would very gladly help in trying to track it down.

I don't mind staying on 4.10 (I'm a bit sad that I can't use memtrace but appart from that it's not an issue).
But I'm guessing this is something that is interesting to investigate.

If needed, here's the link to the project (and the specific commit where I revert the upgrade of ocaml).
https://github.com/GillianPlatform/Gillian/tree/gillian-c-2-with-amazon-and-invariants

EDIT: The following was added on request. Really sorry I didn't give it earlier, I should have.

Configuration

I just realised I forgot to add my configuration so here it is:

• macOS Big Sur 11.0.1
• MacBook Pro (16-inch 2016)
• CPU Intel Core i9, 8 cores
• 16Gb 2667MHz DDR4 ram

Building instructions

Installing esy, dependencies and building the project

Steps required to build the project. npm is required, since the project's dependencies are at managed by esy.

$ npm install -g esy@latest #first step is installing esy
$ esy # should install the dependencies and build the project

This will take quite a while as it's building ocaml and Z3...

Running the encryption header verification

Then, the execution I use to mesure the time, because it's quite long it's easier to see the difference :

# from the root folder of the project
$ esy x gillian-js verify Gillian-JS/Examples/Amazon/deserialize_factory.js -l disabled --no-lemma-proof --amazon

For the story, this is verifying some bit of code from Amazon's AWS Encryption SDK.

Changing the ocaml version

You can change the ocaml version by going into the esy.json file at the root and replacing both occurences of
4.10.x with 4.11.x (the x shouldn't be substituted but actually written like that in the file so that esy can simply find the latest patch.

Then you can rebuild using

$ esy

This will unfortunately rebuild all dependencies (including ocaml).

Uninstalling esy

If you're not an esy user, you might want to clean up after you're done, because esy keeps every version of the ocaml compiler it ever needed and that takes some space.

$ rm -rf ~/.esy
$ npm uninstall -g esy

Additional information - Exploring the project

The project is composed of several components:

The GillianCore folder contains the gillian library. It mostly exposes some big functors that helps building symbolic static analysis tools. In particular, the CLI folder builds a uniform cli to analyse programs.

The parameters to that functor are modules that represent an "instantiation" of Gillian. One instantiates Gillian to analyse programs written in a specific language. One has to plug a memory model into Gillian to be able to perform analysis. An instantiation is composed of 4 module : a concrete memory model, a symbolic memory model (both are modules following the right interface), a "parser and compiler" module that describes how to compile a program in your language into our intermediate representation (GIL, described in Gil_syntax) and a module called External that is barely used.

In the repo, you'll find 3 instantiations of Gillian:

• wisl, a small toy language we use to teach / understand things
• Gillian-C, an instantiation of Gillian for the C language, using bits of CompCert as compiler.
• Gillian-JS, an instantiation of Gillian for JavaScript, inherited from previous work.

For the execution I described above, one only needs to understand Gillian-JS.
The root of the program is the file Gillian-JS/bin/gillian_js.ml, which uses the CLI functor and calls its main function.
From that you should be able to follow execution if needed..

About the dependencies, the field "dependencies" of esy.json describes them, but note that Batteries and Compcert are only used in Gillian-C, and therefore can't be the linked to the issue.

Some more commands you can try

$ esy x gillian-js verify Gillian-JS/Examples/JaVerT/BST.js -l disabled --no-lemma-proof  
$ esy x gillian-c verify Gillian-C/examples/verification/sll.c -l disabled

Further information

That is really all I know. I can help when it comes to exploring the codebase more if needed, but I really have no clue of where to start looking for what causes the slow down.