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 received as input by cargo-charon
• 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.