A painting-style depiction of an armored camel
standing in a desert. (image produced
by DALL·E)
The expressive type system
of OCaml brings strong
static safety guarantees by ensuring data is used in a
consistent way by a program. The Salto project aims at
providing OCaml programs with additional guarantees, by
answering questions such as:
Can a program raise an exception?
Can arithmetic operations overflow?
Are all the array accesses performed within the array bounds?
Can a program break some user-defined invariant or assertion?
Which data might be modified by a program?
Those questions are beyond the scope of the OCaml type system,
but are within reach of abstract interpretation-based static
analyses.
The goal of the Salto project is to define sound static
analyses that help answer the above questions as automatically
as possible. The analysis will help a programmer have better
confidence in her programs, by bringing increased safety and
security guarantees.
November 2025:Release of version
0.2! This version adds supports for when
guards in pattern matching.
March 2025: After 3 years of intensive efforts, we
are finally releasing a public version of the Salto analyzer!
It has already good (but still partial) support for OCaml
4.14. Disclaimer: The analyzer should still be considered
experimental.
Check out
the source
repository, or directly install it through OPAM,
with opam install salto-analyzer.
November 2024: The funding from Inria/Nomadic Labs
has ended. These two years have been fruitful, and the funding
helped the project make great progress. Great thanks!
The Salto project has received a 1 year funding from
the OCaml Software
Foundation. Many thanks to the foundation!
December 2023: release of salto-IL,
the intermediate language that is used by the Salto analyser,
and the transformation from the OCaml Typedtree to this
language. The intermediate language is still subject to changes,
so this should be considered as experimental. Any feedback is
welcome!
[ Repository ]
September 2023: research talk on Salto at
the ML
workshop (co-located
with ICFP'23,
Seattle)
The Design and Implementation of an Abstract
Interpreter for OCaml Programs: A Preliminary Report on the
Salto Analyser
[ Extended
abstract
| Slides
| Video
]
The Salto project initially started as a partnership
between
Nomadic Labs
and Inria, and was funded
for 2 years by the
Tezos Foundation.
Since November 2024, the Salto project was granted a 1
year funding from the OCaml
Software Foundation.
