Crate charon_lib

This library contains utilities to extract the MIR from a Rust project, by compiling it to an easy-to-use AST called LLBC (Low-Level Borrow Calculus). This AST is serialized into JSON files.

A good entry point to explore the project is driver, and in particular driver::CharonCallbacks, which implements the callback which we provide to Rustc.

The ASTs are in ullbc_ast (Unstructured LLBC - basically a cleaned-up version of MIR) and llbc_ast (same as ULLBC, but we reconstructed the control-flow to have if ... then ... else ..., loops, etc. instead of GOTOs).

Re-exports

pub use ast::builtins;

pub use ast::expressions;

pub use ast::gast;

pub use ast::llbc_ast;

pub use ast::meta;

pub use ast::names;

pub use ast::types;

pub use ast::ullbc_ast;

pub use ast::values;

pub use pretty::formatter;

pub use transform::graphs;

pub use transform::reorder_decls;

pub use transform::ullbc_to_llbc;

Modules

ast

common

errors

Utilities to generate error reports about the external dependencies.

export

ids

logger

name_matcher

options

The options that control charon behavior.

pretty

This module contains functions to pretty-print charon types.

transform

Macros

code_location

This macro computes the name of the function in which it is called and the line number. We adapted it from: https://stackoverflow.com/questions/38088067/equivalent-of-func-or-function-in-rust

error

A custom log error macro. Uses the log crate.

error_assert

Custom assert to either panic or return an error

generate_index_type

Generate an Index index type. We use it because we need manipulate a lot of different indices (for various kinds of declarations, variables, blocks, etc.). For sanity, we prevent any confusion between the different kinds of indices by using different types. The following macro allows us to easily derive those types.

info

A custom log info macro. Uses the log crate.

raise_error

Macro to either panic or return on error, depending on the CLI options

register_error

sanity_check

Custom assert to report an error and optionally panic

trace

A custom log trace macro. Uses the log crate.

warn

A custom log warn macro. Uses the log crate.

Constants

VERSION 🔒

The version of the crate, as defined in Cargo.toml.

Functions

deserialize_llbc

Read a .llbc file.