Patinir, E., 1515-1524, Landscape with Charon crossing the Styx [Oil on wood].
Museo del Prado, Madrid.
Source
Charon acts as an interface between the rustc compiler and program verification projects. Its purpose is to process Rust crates and convert them into files easy to handle by program verifiers. It is implemented as a custom driver for the rustc compiler.
Charon is, in Greek mythology, an old man carrying the souls of the deceased accross the Styx, a river separating the world of the living from the world of the dead. In the present context, Charon allows us to go from the world of Rust programs to the world of formal verification.
We are open to contributions! Please contact us so that we can coordinate ourselves, if you are willing to contribute. For this purpose you can join the Zulip.
Charon converts MIR code to ULLBC (Unstructured Low-Level Borrow Calculus) then to LLBC. Both ASTs can be output by Charon.
ULLBC is a slightly simplified MIR, where we try to remove as much redundancies as possible. For instance, we drastically simplify the representation of constants coming from the Rust compiler.
LLBC is ULLBC where we restructured the control-flow with loops, if ... then ... else ..., etc. instead of gotos. Consequently, we merge MIR
statements and terminators into a single LLBC statement type. We also perform
some additional modifications, some of which are listed below:
Remark: most of the transformations which transform the MIR to ULLBC then LLBC are
implemented by means of micro-passes. Depending on the need, we could make them optional
and control them with flags. If you want to know more about the details, see translate
in src/driver.rs, which applies the micro-passes one after the other.
Remark: if you want to know the full details of (U)LLBC, have a look at: types.rs,
values.rs, expressions.rs, ullbc_ast.rs and llbc_ast.rs.
The extracted AST is serialized in .ullbc and .llbc files (using the JSON format).
We extract a whole crate in one file.
charon: the Rust implementation.charon-ml: the ML library. Provides utilities to retrieve and manipulate the AST in OCaml (deserialization, printing, etc.).testsandtests-polonius: test files directories.tests-poloniuscontains code which requires the Polonius borrow checker.
You first need to install rustup.
As Charon is set up with cargo, rustup will automatically download and install the proper
packages upon building the project. If you only want to build the Rust project (in
./charon), simply run make build-charon-rust in the top directory.
If you also want to build the ML library (in ./charon-ml), you will need to
install OCaml and the proper dependencies.
We suggest you to follow those instructions, and install OPAM on the way (same instructions).
For Charon-ML, we use OCaml 4.13.1: opam switch create 4.13.1+options
The dependencies can be installed with the following command:
opam install ppx_deriving visitors easy_logging zarith yojson core_unix odoc menhir
You can then run make build-charon-ml to build the ML library, or even simply
make to build the whole project (Rust and OCaml). Finally, you can run the
tests with make test.
Alternatively, you can use Nix and do nix develop (or use https://direnv.net/ and direnv allow)
and all dependencies should be made available.
You can access the Rust documentation online.
You can also run make to generate the documentation locally.
It will generate a documentation accessible from
doc-rust.html (for the Rust project) and
doc-ml.html (for the ML library).
To run Charon, you should run the Charon binary from within the crate that you
want to compile, as if you wanted to build the crate with cargo build. The
Charon executable is located at bin/charon.
Charon will build the crate and its dependencies, then extract the AST. Charon
provides various options and flags to tweak its behaviour: you can display a
detailed documentation with --help.
In particular, you can print the LLBC generated by Charon with --print-llbc.
If there is a Charon.toml file at the root of your project, charon will also take options from it.
The file supports the same options at the cli interface, except for the options that relate to
input/output like --print-llbc. Example Charon.toml:
[charon]
extract_opaque_bodies = true
[rustc]
flags = ["--cfg", "abc"]Remark: because Charon is compiled with Rust nigthly (this is a requirement
to implement a rustc driver), it will build your crate with Rust nightly. You
can find the nightly version pinned for Charon in rust-toolchain.template.
