Salto: A Static Analyser for OCaml programs

This web-page embeds static Analyser for OCaml programs, as part of the Salto project, based on the techniques described in the ESOP 2024 article Detection of Uncaught Exceptions in Functional Programs by Abstract Interpretation.

Warning: the analysers can take a very long time to run in your browser! Do not be surprised if your browser warns you that some script is taking a lot of time.

The output text displays the analysis result for each declaration of the program. It is possible to record every program point by enabling the Cache non calls options.

Documentation

Options

The available analyses are:

nabla-rec: ∇rec-CFA, a control-flow analysis based on widening, that employs abstract values that might be recursive. It reports possibly uncaught exceptions, and some warnings.

Other analyses might be added in the future.

You are free to choose the abstract domain to represent sets of integers:

two-points: ⊥ and ⊤.
flat: the flat domain of integers, with ⊥ and ⊤.
signs: the domain of signs. It has the abstract elements: ⊥, ⊤, ]-∞,0], ]-∞,-1], {0}, ]-∞,-1]∪[1,+∞[, [0,+∞[, and [1,+∞[.
intervals: the domain of intervals.

You are free to choose the following approximations for call sites:

last 0 call sites: no distinction of call sites, as in 0-CFA.
last 1 call sites: only the most recent call site is distinguished, as in 1-CFA.
last 2 call sites: only the two most recent call sites are distinguished, as in 2-CFA.
max 0 cyclic call sites: occurrences of call sites are limited to 0. This is the same as 0-CFA.
max 1 cyclic call sites: occurrences of call sites are limited to at most 1.
max 2 cyclic call sites: occurrences of call sites are limited to at most 2.
max 0 cyclic call sites + 1 last call sites: occurrences of call sites are limited to 0, and in addition the last 1 call site is distinguished.
max 1 cyclic call sites + 1 last call sites: occurrences of call sites are limited to at most 1, and in addition the last 1 call site is distinguished.
max 2 cyclic call sites + 1 last call sites: occurrences of call sites are limited to at most 2, and in addition the last 1 call site is distinguished.
max 0 cyclic call sites + 2 last call sites: occurrences of call sites are limited to 0, and in addition the last 2 call sites are distinguished.
max 1 cyclic call sites + 2 last call sites: occurrences of call sites are limited to at most 1, and in addition the last 2 call sites are distinguished.
max 2 cyclic call sites + 2 last call sites: occurrences of call sites are limited to at most 2, and in addition the last 2 call sites are distinguished.
max 0 cyclic call sites + dyn last call sites: occurrences of call sites are limited to 0, and in addition the number of the last call sites that are distinguished is dynamically computed (it is equal to the length of the call string where the last repeated call site occurs, starting from the end of the call string).
max 1 cyclic call sites + dyn last call sites: occurrences of call sites are limited to at most 1, and in addition the number of the last call sites that are distinguished is dynamically computed (it is equal to the length of the call string where the last repeated call site occurs, starting from the end of the call string).
max 2 cyclic call sites + dyn last call sites: occurrences of call sites are limited to at most 2, and in addition the number of the last call sites that are distinguished is dynamically computed (it is equal to the length of the call string where the last repeated call site occurs, starting from the end of the call string).

The following options are available:

Refine branches: refine the knowledge in the branches of a test.
Branch is context: consider branches (if ... then ... else ...) as a call site for the two branches.
Cache non calls: Record as well program points that are not calls. With this flag on, you will reduce the cached graph by a large amount, which can save space and time.
Cache widened calls only: among the calls, record only the widened calls in the cache (as opposed to all the calls). Without this flag off, you get a proper notion of abstract call graph. With this flag on, you might reduce the cached graph by a large amount, which can save space and time.
Disprove alarms: Try to disprove safety alarms by exploiting a backward analysis (for nabla/nabla-rec analyses only).
Minimize abstract values: minimize the representation of abstract values produced by the ∇-rec analyser. This produces more readable results.
Debug: print some statistics about the analyses.
Occurrence threshold: value that permits to delay the use of an aggressive widening, by permitting a maximum number of repetitions of some node along a path in abstract values.
Similarity threshold: value that permits to use several incomparable environments. This improves the accuracy of the widening on inputs at the cost of introducing some disjunctions.

Syntax of outputs

The results are of the form { ints = Int chars = Char strings = String extension_constructors = ExtCons closures = Clos constructs = Constr structurs = Struct}, where:

Int is the set of possible integers.
Char is the set of possible characters.
String is the set of possible strings.
ExtCons is the set of possible extension constructors. Such values represent the tags of extensible variants in OCaml, such as exceptions.
Clos is the set of possible closures or functors, that are composed of the piece of code of the closure and an abstract environment.
- For the λ-abstractions in closures, we display their code, and the location at which they occur in the program text.
  For example, λ[42:3] x -> x is the identify function that occurs at line 42, column 3 of the program text.
- The environments in closures differ, depending on the analysis and on the context sensitivity. The global and global-independent-attribute refer to pairs of a program point and an abstract call string.
  For example, the global analysis may return the abstract closure (λ[42:3] x -> y) {[y -> 6:8 @ 23:9], [y -> 6:8 @ 23:9 @ 10:4 # *]}. It is a closure with two possible environments, that give an abstract value to the local variable y. The first possible value is the instance of the binding variable at line 6 column 8 in the calling context composed of the single application site located at line 23 column 9. The second possible abstract value for y is the instance of the same binder for the call sites that is composed of at least two calls, and starting with a call at line 23 column 9, then a call at line 10 column 4.
- For functors, coercions on the arguments are also recorded.
Constr is the set of possible constructs (i.e. contructor/polymorphic variants, tuples, records or arrays), and are classified by their construct class. Constructor/polymorphic variants are classified by their head variant, for example, { A: { ints = ⊤ } B: . C: { constructs = { false: . } } } denotes either a variant A with an integer argument, or a variant B with no argument (as indicated by the dot), or a variant C whose argument is the boolean false (which actually is a constructor variant with no argument). Tuples/Arrays are classified by their width, for example, { 3: { ints = [0,6] } × { constructs = { true: . } } × ints = ⊤ } denotes a tuple whose width is 3, and whose first, second, and third arguments are an integer between 0 and 6, the true boolean, and any integer, respectively. Records are classified by their fields.
Struct is the set of module structures.

The symbols ⊥ or ∅ always indicates the empty set. The symbol ⊤ indicates the full set.

The inferred abstract values may contain cycles, thus denoting inductively defined sets of values. For example, the abstract value v = { variants = { Nil: . Cons: { tuples = {2: { ints = ⊤ } × 'a } } } } as 'a denotes lists of integers, where Nil is the constructor for the empty list, and Cons is the constructor for creating a non-empty list. The abstract value v is such that v = { variants = { Nil: . Cons: { tuples = {2: { ints = ⊤ } × v } } } }. The syntax for cyclic abstract values follows the style that is used in OCaml to display equi-recursive types.