Detection of Uncaught Exceptions in Functional Programs by Abstract Interpretation: Software Artefact

This is the artefact that accompanies the ESOP24 article "Detection of Uncaught Exceptions in Functional Programs by Abstract Interpretation", by Pierre Lermusiaux and Benoît Montagu.

This work is part of the Salto Project, that aims at developing static analysers for OCaml programs.

Two versions of the artefact are available, in the form of two archives:

• esop_artefact-amd64.tar.bz2 if your computer architecture is amd64
• esop_artefact-arm64.tar.bz2 if your computer architecture is arm64

The artefact archive consists of the static analyser for OCaml programs that is described in the article. Two items are provided:

1. A self-contained Docker image where the analyser is already built and is ready for running. In this image, automated scripts are available to run the analyser against the test suite, and to run performance benchmarks against the same suite.
2. The source code of the analyser.

Only OCaml 4.14 is supported. Some features of OCaml are not supported: objects, recursive modules, general recursive definitions (e.g., cyclic immutable lists), laziness, arrays, hash tables, floats, conditional patterns, threads, the Unix module, the Obj module, the GC module, and all functions that interact with the operating system.

The instructions to run the artefact are written in the INSTALL file. In particular, the instructions to reproduce the benchmarks of the paper are described in step 7 of this file (`make bench-long`).

Contents of the artefact:

• README: this file
• LICENSE: how this software is licensed
• REQUIREMENTS: what is needed to run this software
• INSTALL: how to run this software
• STATUS: badges that the authors apply to for the current artefact
• esop-docker.tar: the Docker image that contain a self-contained, ready-to-run version of the static analyser.
• Makefile: file that contains targets for the `make` tool, to easily run the docker image. See the INSTALL file for details.
• Dockerfile: file that contain the directives to build the Docker image. This is useful if you want to build the analyser on your machine, or if you want to rebuild the Docker image.
• ez-dune-describe-main.tar: archive that contains the source code of the `ez-dune-describe` library (useful if you want to build the analyser on your machine). This library retrieves the dependencies between the files of an OCaml project that is based on the `dune` build system, and provides ways on iterate on those files in a topological order of their dependencies.
• salto-il-master.tar: archive that contains the source code of the `salto-IL` library (useful if you want to build the analyser on your machine). This library implements the translation of the OCaml Typedtree into a simplified intermediate language that shares the same features as the language of section 3. In particular, it features a single construct for exception handling, a single construct for pattern matching, and the order of evaluation is made explicit by `let ... in` nodes in programs. Moreover, patterns are non-ambiguous, as we computed the pattern complements.
• salto-analyzer-esop24.tar: archive that contains the source code of the static analyser (useful if you want to build the analyser on your machine).

The three tar archives of source code contain their own documentation in the form of README files.