Introduction

Charon is a CLI tool that helps other tools analyze Rust code. Its basic function is that you call charon cargo on a Rust crate, and Charon produces a crate_name.llbc file which contains all the information you could possibly hope to get from the crate¹.

This manual is a bare-bones draft that we plan to improve over time. In the meantime, if there’s something you want to know about, come ask on Zulip! We also welcome help here: writing is hard, a PR that adds even an incomplete page to this manual can be a good prompt for us to fill the gaps.

Semantic information only however; we do not preserve syntactic information like scopes nor distinguish say while from loop. ↩

Usage

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 pretty-print the translated crate with both --print-ullbc and --print-llbc, depending on the Charon intermediate representation you wish to use.

Charon supports per-crate configuration via the [package.metadata.charon] section in Cargo.toml. The exact list can be found by looking at src/bin/charon/toml_config.rs. If an option is set both as a CLI flag and as a toml value and we can’t merge them, the CLI flag wins.

Remark: because Charon is compiled with Rust nightly (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.

Names

Each item (function, trait decl, type decl etc) in Charon has a unique name, that looks like a Rust path (e.g., std::boxed::Box). This name can be used to uniquely identify items using patterns.

These patterns are used most notably for the --include/--exclude cli options, and made available in Rust and OCaml with NameMatcher. Caveat: the Rust and OCaml name matchers differ in input syntax and behavior; this is tracked in https://github.com/AeneasVerif/charon/issues/319.

TODO: explain syntax and behavior.

Note: for well-known built-in items, you can often use ItemMeta.lang_item instead; it contains an identifier meant for this purpose, documented here.

CLI options

TODO: explain the main options, and LLBC vs ULLBC

In short: LLBC is the name we give to the output of Charon. It stands for Low-Level Borrow Calculus and is the name used in the formalisations of the Aeneas project. Charon was initially created as part of the Aeneas project, and therefore inherits that name. ULLBC means Unstructured LLBC, i.e., LLBC without the control-flow reconstruction.

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.

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 transformation_passes in src/bin/charon-driver/driver.rs, which applies the micro-passes one after the other.

Running Charon on Rust-for-Linux’s `kernel`

Rust-for-Linux’s kernel crate is built by Kbuild rather than Cargo. Running Charon on it requires some acrobatics.

You must be able to build the kernel crate, and have charon in your PATH.

Setup

The following assumes that the current directory is a clone of the kernel.

Pick an output path and some options to pass to Charon:

$ export CHARON_OUTPUT="$PWD/kernel.llbc"
$ export CHARON_OPTIONS="--extract-opaque-bodies --monomorphize"

Find Charon and the toolchain it needs:

$ export CHARON_BIN="$(command -v charon)"
$ export CHARON_RUSTC="$(charon toolchain-path)/bin/rustc"

Prepare a build directory and enable rust support:

$ mkdir -p ../linux-build
$ export KERNEL_BUILD_DIR="$(realpath ../linux-build)"
$ make LLVM=1 O="$KERNEL_BUILD_DIR" RUSTC="$CHARON_RUSTC" rustavailable
$ make LLVM=1 O="$KERNEL_BUILD_DIR" RUSTC="$CHARON_RUSTC" defconfig
$ scripts/config --file "$KERNEL_BUILD_DIR/.config" -e RUST
$ make LLVM=1 O="$KERNEL_BUILD_DIR" RUSTC="$CHARON_RUSTC" olddefconfig

Write the following script to $KERNEL_BUILD_DIR/charon-rustc:

#!/usr/bin/env sh
set -eu

is_kernel=false
previous=
for argument in "$@"; do
    if [ "$previous" = "--crate-name" ] && [ "$argument" = "kernel" ]; then
        is_kernel=true
        break
    fi
    previous=$argument
done

if [ "$is_kernel" = true ]; then
    export CHARON_EMIT_ARTIFACTS=1
    exec "$CHARON_BIN" rustc \
        $CHARON_OPTIONS \
        --sysroot default \
        --dest-file "$CHARON_OUTPUT" \
        -- "$@"
else
    exec "$CHARON_RUSTC" "$@"
fi

and make it executable:

$ chmod +x "$KERNEL_BUILD_DIR/charon-rustc"

The wrapper acts just like rustc except that if we’re compiling a crate called kernel, it will also extract it via Charon into the $CHARON_OUTPUT file.

Run Charon

Build the kernel crate with the wrapper:

$ touch rust/kernel/lib.rs
$ make LLVM=1 \
    O="$KERNEL_BUILD_DIR" \
    RUSTC="$KERNEL_BUILD_DIR/charon-rustc" \
    rust/kernel.o

The output llbc file can then be found in $CHARON_OUTPUT.

For example, the layout of Linux’s C struct list_head can be inspected with:

$ charon pretty-print --include-layouts "$CHARON_OUTPUT" > kernel.pretty
$ rg -A24 \
    'Full name: bindings::bindings_raw::list_head$' \
    kernel.pretty

What Charon Does For You

The purpose of Charon is to centralize the efforts of extracting information from rustc internals and turning them into a uniform and usable shape. Here are some things that Charon does once so you don’t have to do it yourself:

TODO: explain each item

Trait resolution (explicitly track how each trait bound was proven to hold);
Reconstruct expressions from all the various constant representations;
Hide the distinction between early- and late-bound lifetime variables;
Make non-overriden default methods in impl blocks appear as normal methods;
Handle trait method implementations that have a more general signature than as declared in the trait (WIP: https://github.com/AeneasVerif/charon/issues/513);
Represent closures as normal structs that implement the Fn* traits;
Represent VTables as normal structs stored in statics;
Represent drop glue via the Destruct trait;
Many useful post-processing transformations to make the output more usable; see the dedicated file.

Charon item selection

Items and opacity

An item is a module, function, type decl, static, const, trait decl, or trait impl. A crate is considered a module.

Each item has an opacity level¹:

Transparent — the item is fully translated.
Foreign — the default for items outside the current crate. Translation depends on normal Rust visibility: for types, translate fully if it’s a struct with all-public fields or an enum; for other items this is equivalent to Opaque.
Opaque — only the name and signature are translated, not the contents. For functions and globals, the body is not translated. For types (structs, enums, unions), the fields/variants are not translated. For traits and trait impls, methods with a default body are only translated if mentioned (used or overridden) anywhere in the final crate. For modules, the contents are not explored (but items referenced from elsewhere are still translated).
Invisible — nothing is translated for this item. The corresponding map will not have an entry for the item ID. Useful when even the signature causes errors.

Selection process

Charon starts from a set of entry points and explores outward using a work-queue:

The entry point items are enqueued for processing.
Each item is processed according to its opacity:
- Transparent module: enqueue all items directly inside it.
- Non-transparent module: do nothing (contents are not explored).
- Transparent non-module item: translate it fully (including body).
- Foreign or opaque non-module item: translate only the signature.
- Invisible item: do nothing.
Whenever processing an item encounters a reference to a new item, that new item is enqueued for processing.

This is a dependency-driven algorithm that pulls in items as they are needed. With the default settings, the entry point is the current crate (a module), which is transparent, so all its direct items are enqueued. Those items reference foreign items from dependencies, which get enqueued as foreign (signatures only). The result: the whole current crate is translated, plus the signatures of all foreign items it references.

Opacity vs reachability: An item’s opacity (how much of it is translated) is determined solely by its own name and annotations — it does not inherit from the item that references it. But reachability (whether the item is queued at all) does depend on the exploration path: an item only reachable through an opaque item’s body will not be queued, since opaque bodies are not explored. In the default setup (the whole crate as a transparent entry point), all current-crate items are enqueued via module traversal regardless of call-graph structure. This distinction matters mainly when using custom --start-from patterns or opaque modules.

How opacity is determined

Each item’s opacity is calculated from its name by matching against a list of patterns. The patterns come from two sources: CLI flags and source annotations.

Source annotations

The source-level attributes #[charon::opaque] and #[charon::exclude] set the opacity of individual items. They can only make items more opaque, never less².

When both a source annotation and a CLI pattern apply, the more opaque of the two wins (Transparent < Foreign < Opaque < Invisible). This means --include cannot override a #[charon::opaque] annotation.

Scope difference: #[charon::opaque] applies only to the annotated item itself. Items nested within it — functions in a module, methods in an impl block — are separate items with their own opacity, which for current-crate items defaults to Transparent. By contrast, --opaque crate::module uses prefix matching³, so it makes crate::module and every item whose path starts with crate::module (e.g. crate::module::foo) Opaque.

Concretely: if a module is annotated #[charon::opaque], a function inside it that is called from outside the module will still be translated fully (body included), because the function’s own opacity is Transparent. Using --opaque crate::that_module instead would make that nested function Opaque (signature only).

CLI flags

--start-from <PATTERN> — Entry points for translation. Can be specified multiple times. Default: crate (the entire current crate).
--start-from-attribute[=<ATTR>] — Use items annotated with a given attribute as entry points. Default attribute if none specified: verify::start_from.
--start-from-pub — Use all pub items from the current crate as entry points
--include <PATTERN> — Set matched items to transparent.
--opaque <PATTERN> — Set matched items to opaque.
--exclude <PATTERN> — Set matched items to invisible.
--extract-opaque-bodies — Makes all items transparent. Internally changes the base pattern from _ → Foreign to _ → Transparent (see Pattern list below), so it affects all items including external ones.
--translate-all-methods — Include provided trait methods even if unused. Equivalent to making all trait declarations transparent.

Pattern list

Charon builds an ordered list of (pattern, opacity) pairs from the CLI flags⁴:

_              → Foreign      (default: everything starts as foreign)
crate          → Transparent  (current crate is always transparent)
<--include>    → Transparent  (user whitelist)
<--opaque>     → Opaque       (user blacklist)
<--exclude>    → Invisible    (user exclusion)

In the default setup, everything outside the current crate is treated as Foreign and items in the current crate are Transparent. Note: there is no --foreign CLI flag, so this cannot be expressed directly via CLI flags — --opaque would make external items Opaque (signature only), which differs from Foreign for types (Foreign types with all-public fields are fully translated).

Pattern syntax

Patterns use a name-matcher syntax (charon/src/name_matcher/). Examples:

crate::module::item — matches this item and all its subitems
crate::module::item::_ — matches only the subitems (not the item itself)
core::convert::{impl core::convert::Into<_> for _} — a specific trait impl
_ or * — glob, matches any single path segment
{impl core::convert::Into<_> for _} works without the core::convert prefix, in this case we do a global search for impls.

Patterns are prefix matches: crate::foo matches crate::foo, crate::foo::bar, crate::foo::bar::baz, etc.³

Currently matching on inherent impl blocks isn’t supported, writing crate::module::_::method is the standard workaround.

Precedence

When multiple patterns match the same item, the most precise pattern wins⁵:

Longer patterns beat shorter ones.
Among equal-length patterns, a non-glob final element beats a glob.

Example with --opaque crate::module --include crate::module::_:

Item	Matching patterns	Most precise	Result
`crate::module`	`_`, `crate`, `crate::module`	`crate::module` (length 2)	Opaque
`crate::module::foo`	`_`, `crate`, `crate::module`, `crate::module::_`	`crate::module::_` (length 3)	Transparent

Note: pattern matching currently has limitations — e.g. it parses u64 as a path instead of the built-in type, and it is not possible to filter a trait impl (only its methods)⁶.

charon/src/ast/meta.rs:191 ↩
charon/src/bin/charon-driver/translate/translate_meta.rs:776-785 ↩
charon/src/name_matcher/mod.rs:51-125 ↩ ↩2
charon/src/options.rs:534-570 ↩
charon/src/name_matcher/mod.rs:189-221 ↩
charon/src/options.rs:112 ↩

Charon transformations

Charon has options to make the generated code easier to use. Some are currently not optional but could be made so on request.

Control-flow reconstruction

The MIR we get from rustc is a control-flow graph (CFG), where control-flow happens with gotos that can jump arbitrarily around the code.

Charon by default transforms this CFG into structured control-flow, i.e. with nested match/if/loop constructs.

To turn this off, pass --ullbc to charon (ULLBC stands for Unstructured LLBC).

`--hide-marker-traits`

This option removes mentions of the following built-in traits from the output crate:

core::marker::Sized
core::marker::Tuple
core::marker::Send
core::marker::Sync
core::marker::Unpin

This is a convenience option, meant to reduce noise for Charon consumers that output user-readable things.

Note that for historical reasons Charon removes mentions of the Allocator trait regardless of this setting. This should eventually be changed, open an issue if you have a need for it.

Note that today this is implemented by calling IndexMap::remove to remove the entry in the trait_clauses/trait_refs vectors. This abuses the confusion between newtype-indexed vectors and newtype-indexed maps we have in Charon, which can cause annoying footguns. See https://github.com/AeneasVerif/charon/issues/490.

`--remove-associated-types`

This option takes a pattern, and transforms the associated types of all the traits that match the pattern. This transforms code like:

#![allow(unused)]
fn main() {
trait Iterator {
  type Item;
  fn next(&mut self) -> Option<Self::Item>;
}
fn use_iterator<I: Iterator>(it: I) { ... }
}

into:

#![allow(unused)]
fn main() {
trait Iterator<Item> {
  fn next(&mut self) -> Option<Item>;
}
fn use_iterator<I: Iterator<Clause0Item>, Clause0Item>(it: I) { ... }
}

This transformation has limitations:

GATs cannot be transformed this way;
Some recursive traits cannot be transformed this way, e.g.:

#![allow(unused)]
fn main() {
trait Bar {
    type BarTy;
}
trait Foo {
    type FooTy: Foo + Bar;
}
// becomes:
trait Bar<BarTy> {}
trait Foo {
    type FooTy: Foo + Bar<Self::FooTy_BarTy>;
    // We need to supply an argument to `Bar` but we can't add a type parameter, so we add a
    // new associated type.
    type FooTy_BarTy;
}
}

We’re currently missing assoc type information to transform dyn Trait (https://github.com/AeneasVerif/charon/issues/123).
We currently don’t track bound lifetimes in quantified clauses properly (https://github.com/AeneasVerif/charon/issues/534).
Type aliases don’t have the correct clauses in scope (https://github.com/AeneasVerif/charon/issues/531).
We don’t take into account unicity of trait implementations. This means we won’t detect type equalities due to the same trait predicate appearing twice, or a trait predicate coinciding with an existing trait impl. See the dictionary_passing_style_woes.rs test file for an example.

Make implied bounds explicit

WIP: https://github.com/AeneasVerif/charon/issues/585

Current limitations of Charon

Charon is beta software. It works well but it is currently poorly documented, doesn’t support all the Rust features we’d like, and has several breaking changes planned in the near future.

Planned breaking changes

https://github.com/AeneasVerif/charon/issues/287
https://github.com/AeneasVerif/charon/issues?q=sort%3Aupdated-desc%20is%3Aissue%20state%3Aopen%20label%3AS-representation
Name matcher behavior likely to change in subtle ways (https://github.com/AeneasVerif/charon/issues/319).

Known unsoundnesses

https://github.com/AeneasVerif/charon/issues/583

Unsupported Rust features

Tracked here: https://github.com/AeneasVerif/charon/issues/142

Missing information in the translated output

Lifetime information about captured closure variables https://github.com/AeneasVerif/charon/issues/1040;
Precise lifetimes for higher-ranked trait predicates https://github.com/AeneasVerif/charon/issues/1143;
Lifetime information inside function bodies (not planned).

By-design limitations

Charon’s output contains little syntactic information. Stuff like scopes, or distinguishing between loop, while and for, is not kept; only semantic information is kept. This can impede lints. We do keep good spans for error reporting however.
It’s not possible to do trait solving on the output of Charon. Charon simply does not have all the type system logic needed to do that, nor would I want to try and reimplement that.

Frequently Asked Questions

I can’t find a definition/what’s this `<opaque>`

Try --extract-opaque-bodies; then try --start-from=path::to::definition.

Charon by default only translates the items of the current crate. Any items from other crates are treated as “opaque”, which means that they will be listed but without their contents (e.g. without a function body, or a type definition).

--extract-opaque-bodies is the hammer that removes this filter. Now all definitions reachable from the current crate will be translated in full.

That will still not include a foreign definition if it’s not used (even indirectly) by the current crate. To translate such a definition, you have to tell Charon explicitly, using --start-from=path::to::definition. Now instead of starting from the current crate, it will start from the definition listed. If you want both, pass --start-from=crate --start-from=path::to::definition.

Finally, note that --extract-opaque-bodies can cause a lot of code to be translated, which can be slow and/or hit some cases that Charon doesn’t support. You can have finer control over what gets translated using --include/--opaque.

See What Charon Translates for more details on how Charon decides what to translate and how to control it.

This trait doesn’t have all the methods it should have

Try --translate-all-methods.

By default Charon only translates a default method if it is used anywhere. E.g. this way Iterator only has next until another of its methods is used¹. --translate-all-methods instead always translates the full list of methods.

What is the difference between Charon and `rustc_public`?

Both projects aim at making it easy to analyze Rust code. Beyond that, they sit at two ends of the spectrum of “do extra work”: rustc_public intentionally stays close to the compiler’s representations, adding just enough abstraction to absorb changes as they occur between compiler versions.

In contrast, Charon aims for the most straightforward yet complete representation. For that, we do quite a lot of work of reconstructing information coming from various places in the compiler and hiding away any detail that’s not relevant to the semantics.

See What Charon does for you and Transformations to get an idea of the kinds of reconstructions we do.

How much can I trust what Charon outputs

Short answer: a fair amount

Longer answer: it depends on the kind of data. Some kinds of data are translated pretty much verbatim from what rustc gives us, and thus can be fully trusted. Conversely, some bits involve more Charon-specific abstractions, which leaves more room for errors.

Probably the most reliable part of Charon is the semantics of function bodies: not only is it converted rather directly from rustc’s MIR, but it is also interpreted and compared against Miri by the Soteria Rust project, which uses Charon.

Probably the least reliable part of Charon is lifetime generics: this is where we do the most work on top of rustc to get what we want; so mistakes there are likelier.

Another domain that doesn’t rely on rustc is layout guarantees. We compute them ourselves, based on the guarantees given by the Rust Reference.

Overall Charon is well-tested, and its authors are experts in the semantics of Rust. If you find a bug please report it, so we can incrementally make Charon more robust for everyone!

The whole “lazy method list” feature was pretty much made specifically for Iterator with its gajillion default methods and helper types. ↩

Keyboard shortcuts

The Charon Manual