Analyzing Rust programs with Charon

Nadrieril is a long-time Rust contributor, and the maintainer of the rustc pattern-matching infrastructure. During his involvement with Rust, he has noticed a problem with the usability of the language: it is difficult to automatically extract information from a Rust crate for use with other tooling. The Charon project aims to fix that by providing a stable API for accessing internal information from the Rust compiler.

A lot of features in Rust are implicit or automatic, he explained, so it's hard to make a tool that interprets what Rust code does without reimplementing large parts of the Rust compiler (rustc). The normal way for tools to work around that is by using rustc's internal interfaces, but those interfaces can sometimes break without warning. The compiler binary is a thin wrapper around a library that can theoretically be linked to and used by other applications, but the entry points are explicitly documented to be unstable.

The aim of Charon is to "show you what rustc sees" in a stable way, centralizing all of the development work needed to keep up with changes in rustc's internal interfaces. Nadrieril thought that the Rust developers working on the kernel might have a particular use for that when writing custom tooling that works as part of the kernel build. To demonstrate exactly what Charon can do, Nadrieril had a series of demos that started with a tiny crate that "does basically nothing". Running "charon cargo" will compile a Rust project as cargo normally would, but with an extra output: a .llbc file containing JSON that has the complete contents of the crate in readable form. That includes defined types, traits, and functions.

Charon can also pretty-print that JSON output for human readers. This output takes the form of a Rust-like language that marks the source of the program with additional comments and statements to show implicit features explicitly. For example, the output uses lightning bolt (⚡) symbols to show where control flow will go during stack unwinding. Even the output from the minimal example was a bit verbose, but it showed where values were dropped, the types of the variables involved, and even preserved comments from the source. The Rust function

    fn consume(_: String) {}

becomes:

    // Full name: use_threads::consume
    fn consume(_1: String)
    {
        let _0: (); // return
        let _1: String; // arg #1

        storage_live(_0)
        _0 = ()
        _0 = ()
        conditional_drop[impl_Destruct_for_String::drop_glue<'0>] _1
        ↳⚡ unwind_continue
        return
    }

Nadrieril then went on to show how this kind of analysis can be useful for the kernel specifically. For one thing, Charon can be used to see how rustc has interpreted the output of bindgen, the program that generates Rust versions of the kernel's C structures. Charon's output shows both the specific layout that rustc chose, and which pieces of that layout are guaranteed to remain stable between compiler versions. As an example, he showed this piece of Charon's output for the kernel's list_head structure:

    // Full name: bindings::bindings_raw::list_head
    pub struct list_head {
      next: *mut list_head,
      prev: *mut list_head,
    }
    // layout:
    //     size: 16usize (guaranteed:
    //         at_least(align_to(max(size_of::<*mut list_head>(),
    //                               size_of::<*mut list_head>()),
    //                           max(align_of::<*mut list_head>(),
    //                               align_of::<*mut list_head>())))),
    //     align: 8usize (guaranteed:
    //         at_least(max(align_of::<*mut list_head>(),
    //                      align_of::<*mut list_head>()))),
    //     discriminator: _,
    //     inhabited: true,
    //     variants: [
    //         _: {
    //             offset of next: 0,
    //             offset of prev: 8,
    //             inhabited: true,
    //             tagger: [],
    //         },
    //     ],
    //     repr(C),

That information contains several redundant pieces, such as the variant information for a structure that is not an enumeration, and therefore only has one variant. The advantage is that the structure of the JSON Charon emits is extremely regular, which makes it easy to write simple tools that use it. Structures and enumerations always provide the same set of information. The same is true for functions, regardless of whether they are defined as closures, methods, or top-level functions. That makes code to iterate over the produced JSON simpler to write. For example, a custom linter that checks that a program does not call std::thread::spawn() comes to about 60 lines.

"If you've ever tried to look at rustc's ABI, you might be crying now. This is not easy," Nadrieril said. Gary Guo asked how Charon compared to the rustc_public project, which has a similar goal. The two projects are two ends of a spectrum, Nadrieril replied. The rustc_public project does the minimum amount of work necessary to expose rustc's interfaces, and also provides the minimum level of abstraction. Charon does a certain amount of work to wrap the information that rustc's interfaces provide in a nice, simplified, easy-to-parse format, and to provide better tooling to work with it. Guo agreed that Charon's approach was better.

Miguel Ojeda suggested that the Coccinelle for Rust project might want to use Charon in place of rust-analyzer. Nadrieril agreed that Charon would be a good fit for that use case. Kent Overstreet asked whether Charon could show what different optimization passes do to Rust code, which he thought would be useful for squeezing optimal performance out of the language without taking years to completely understand how the optimizations affect code generation. Nadrieril agreed that it would be useful, he just hadn't thought of that, so Charon doesn't do it yet. He didn't think it would be hard to add, however.

He had a few more demos of what is possible with Charon. One of them was to take a simple Rust function that performs 128-bit multiplication, and translate it to Python. That specific case is somewhat useless, because Python has native big integers, but it is sometimes useful to translate an algorithm from Rust to another language. For example, Charon exposes OCaml bindings that are generated by running Charon on its own source code. It has also been used to translate Rust into C or Lean.

Hindborg asked how good the Rust-to-C translation was. Nadrieril said that the tool only targets safe Rust, but within that domain it does pretty well, and generates legible C code. Microsoft has used it to translate some cryptography primitives implemented in Rust into C. Xong Fei Ding noted that BoringSSL had received a patch to convert libcrux from Rust to C and use it in place of BoringSSL's cryptographic code, but that it was rejected because the C version did not perform as well. Nadrieril said that there is a mismatch between which patterns are fast in Rust versus C, and that generating fast C code from Rust is much harder than generating readable C code.

Guo asked whether Charon based its output on the intermediate representation that rustc constructs just after parsing the Rust code (medium-level intermediate representation, abbreviated as MIR) or after it has performed type checking and some optimizations (elaborated MIR). Charon can use either — the former by default, and the latter when the user requests it with the --precise-drops flag, since some optimizations can change where drops occur, Nadrieril said. Guo explained that his interest came from having to "hack around" some of rustc's internals to make the klint tool work. After some back and forth, Guo concluded that Charon would not be able to completely replace klint, but only because klint also checks some properties of the generated binary.

Nadrieril concluded his presentation by saying that Charon has been in development for just over four years, and supports all Rust features except asynchronous code. There are still bugs, but other than the bugs, Charon produces correct output. The project will be ready for a 1.0 release soon. He requested that people try using Charon for their own use cases. The point of the project is to centralize the needed logic to interface with the compiler in one place; he would be pleased to see it adopted by all kinds of tools.

Did you like this article? Please accept our trial subscription offer to be able to see more content like it and to participate in the discussion.