Patinir, E., 1515-1524, Landscape with Charon crossing the Styx [Oil on wood].
Museo del Prado, Madrid.
Source
Charon (pronounced "Ka-ron") extracts the complete contents of a Rust crate (and its dependencies) into a JSON file:
{
"crate_name": "...",
"type_decls": [ ... ],
"fun_decls": [ ... ],
"global_decls": [ ... ],
"trait_decls": [ ... ],
"trait_impls": [ ... ],
}The output contains the types, functions and traits of the crate and its dependencies, the simplified MIR bodies of functions, source information for each item, and other semantic information described below.
We are open to contributions! Please contact us so that we can coordinate ourselves, if you are willing to contribute. Discussions happen on Zulip.
Run charon inside the crate of interest, much like you would call cargo build. It will produce
a crate_name.llbc file.
The charon-lib crate can read this file and let you manipulate its contents. Parse the file using
serde_json::from_reader::<charon_lib::export::CrateData>(file). OCaml bindings are also available
in the charon-ml folder.
For more detailed usage instructions, see the documentation.
The output of Charon looks simple but constructing the relevant information is hard. The purpose of Charon is to centralize the efforts of extracting information from rustc internals and turning them into a uniform and usable shape. See the documentation for an overview of what Charon has to do today.
If you're writing a rustc driver, chances are you could use Charon instead. Charon is however geared towards semantic analyses; it likely won't help you for syntactic analyses like many lints.
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 cross the river of compiler internals to go from the world of Rust programs to the world of code analysis and verification.
Charon is alpha software. While it works quite well for a large number of crates, it has not reached the full set of features we intend, incorrectly translates code in some edge cases, and a number of breaking changes in its API are planned. See the limitations for details.
If you use nix, you can directly run nix run github:AeneasVerif/charon. Otherwise, read on.
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), run make build-charon-rust in the root directory. The resulting charon binary can be found in bin/charon,
from where you can use it.
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 opam install . --deps-only.
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 and all dependencies should be made available.
You can access the (work-in-progress) 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).
