package salto-analyzer

README.md

The Salto static analyser for OCaml programs

The Salto analyser is a static analyser for OCaml programs. It is a whole-program analyser that is based on the theory of abstract interpretation.

Not all features of the OCaml programming language or its standard library are supported right now.

The analyser can only analyse executables (as opposed to libraries). It will infer an over-approximation of the final value that is computed, of the heap that has been allocated, of the exceptions that might be raised, and of the exit codes that might be returned.

In its current state, this project should be considered experimental. It has been successfully tested on small projects (up to a few hundred lines). For larger projects or projects that involve generated code (such as parser generators like ocamlyacc or menhir), however, it is likely that the analyser takes very long time and consumes a very large amount of memory. Pieces of code that allocate a lot of mutable data are also likely to make the analysis costly. You have been warned.

Additional note: if your project depends on external libraries, those libraries must provide the .cmt and .cmti files of their implementation, so that the calls to such libraries can be analysed.

The supported features and analyses, command line options, and output format are subject to changes.

An early version of the analyser and the techniques it employs has been described in the research article:

"Detection of Uncaught Exceptions in Functional Programs by Abstract Interpretation", P. Lermusiaux and B. Montagu, ESOP 2024, DOI:10.1007/978-3-031-57267-8_15

How to build the project

To install the analyser, simply type

opam install salto-analyzer

If you want to compile it by hand, you will first need to install salto-IL and ez-dune-describe. Then, type make. This builds an executable salto and a JavaScript version that can be used in a local web page.

You can run the analyser binary by calling

dune exec --profile=release -- salto analyze FLAGS DIR

where DIR is a directory that contains an OCaml that is built using dune.

To print the documentation, type

dune exec -- salto analyze --help

The JavaScript demo is available in the file, that you should open in your preferred web browser:

demo/salto.html

In this demo, the OCaml standard library is not available.

How to run tests

To execute the tests, run the command

make test

This commands runs the analyser on the test suite located in the tests/analyze directory, with the exception of a few tests that are disabled, due to their long running time. See the file tests/analyze/generate_dune.ml to see which tests are disabled.

The directory tests/analyze also contains in the files *.expected the expected outputs of for each test file. If a test run produces a result that is not the expected result, then a diff is printed and an error is raised.

How to run benchmarks

There are two sets of benchmarks: the "short benchmarks", that should need a few minutes to complete, and the "long benchmarks", that need between 2 and 3 hours to complete. The benchmark files are selected from the test files found in tests/analyze.

To run the short benchmarks, type the command

make bench

To run the long benchmarks, type the command

make bench-long

The benchmarks create .csv, .txt and *.pdf files in the bench directory. The .txt file is a human friendly version of the .csv file. The *.pdf files are graphs that compare running time or memory consumption for two options of the analyser (with or without minimisation).

For every test file, the benchmarks measure:

• The number lines of code

• The time to complete the analysis when minimisation is disabled (in seconds)

• The maximum amount of memory consumed by the analysis when minimisation is disabled (in kilobytes)

• The time to complete the analysis when minimisation is enabled (in seconds)

• The maximum amount of memory consumed by the analysis when minimisation is enabled (in kilobytes)

Structure of the repository

• bench/: scripts to run benchmarks against the test suite of tests/analyze/. The outputs of the benchmark procedures are written in this directory.

• bin/: executables that call the analysis defined in src/analyzers/. The two executables analyze.exe and salto-analyzer.exe are produced, that can analyse, respectively, a .ml/.cmt file, and the executables produced by a dune project.

• demo/: a demo of the analyser, that runs in a browser, thanks to js_of_ocaml. To run the demo, visit the file salto.html with your favorite web browser.

• src/:

  • analyzers/: core of the static analyser

    • nablaCommon.ml: functor that performs the analysis of OCaml program (parameterised over several abstract domains)

    • OCamlDomain.ml: functor that implements the abstract domains for sets of OCaml values (parameterised over abstract domains for base types)

    • nablaHeap.ml: functor that implements a non-relational abstract heap

    • exceptional.ml: the abstract exception monad and abstract domain, to easily handle the analysis of exceptions

    • alarming.ml: another monad and abstract domain, that remembers alarms

  • arrayExtra/: library that provides useful functions on arrays

  • domains/: abstract domains for base types (characters, the flat domain for strings, intervals of integers, signs, the flat domain for integers...)

    • nablaRec/nablaRec.ml: functor that implements the abstract domains for inductively defined sets of trees (parameterised over abstract domains for base types). This module is generic, i.e., it does not depend on the specificities of OCaml.

  • hcons/: library that facilitates hash-consing of data-structures

  • listExtra/: library that provides useful functions on lists

  • memo/: library that facilitates the definition of memoized functions and that exposes dynamic fixpoint solvers

  • ralist/: random-access lists (a data-structure from Chris Okasaki)

• tests/:

  • analyze/: test suite composed of individual .ml files

  • analyze_dune/: test suite for dune projects