Skip to main content

charon_lib/
lib.rs

1//! This library contains utilities to extract the MIR from a Rust project,
2//! by compiling it to an easy-to-use AST called LLBC (Low-Level Borrow Calculus).
3//! This AST is serialized into JSON files.
4//!
5//! A good entry point to explore the project is [`driver`](../charon_driver/index.html),
6//! and in particular [`driver::CharonCallbacks`](../charon_driver/driver/struct.CharonCallbacks.html),
7//! which implements the callback which we provide to Rustc.
8//!
9//! The ASTs are in [`ullbc_ast`] (Unstructured LLBC - basically
10//! a cleaned-up version of MIR) and [`llbc_ast`] (same as ULLBC, but
11//! we reconstructed the control-flow to have `if ... then ... else ...`,
12//! loops, etc. instead of `GOTO`s).
13
14// For rustdoc: prevents overflows
15#![recursion_limit = "256"]
16#![allow(
17    clippy::borrowed_box,
18    clippy::derivable_impls,
19    clippy::field_reassign_with_default,
20    clippy::manual_map,
21    clippy::mem_replace_with_default,
22    clippy::new_without_default,
23    clippy::should_implement_trait,
24    clippy::useless_format
25)]
26#![expect(incomplete_features)]
27#![feature(assert_matches)]
28#![feature(box_patterns)]
29#![feature(deref_patterns)]
30#![feature(deref_pure_trait)]
31#![feature(if_let_guard)]
32#![feature(impl_trait_in_assoc_type)]
33#![feature(iterator_try_collect)]
34#![feature(register_tool)]
35#![feature(trait_alias)]
36#![feature(trivial_bounds)]
37// For when we use charon on itself :3
38#![register_tool(charon)]
39
40#[macro_use]
41pub mod ids;
42#[macro_use]
43pub mod logger;
44pub mod ast;
45pub mod common;
46pub mod errors;
47pub mod export;
48pub mod name_matcher;
49pub mod options;
50pub mod pretty;
51pub mod transform;
52
53// Re-export all the ast modules so we can keep the old import structure.
54pub use ast::{builtins, expressions, gast, llbc_ast, meta, names, types, ullbc_ast, values};
55pub use pretty::formatter;
56
57/// The version of the crate, as defined in `Cargo.toml`.
58pub const VERSION: &str = env!("CARGO_PKG_VERSION");
59
60/// Read a `.llbc` file.
61pub fn deserialize_llbc(path: &std::path::Path) -> anyhow::Result<ast::TranslatedCrate> {
62    deserialize_llbc_with_format(path, options::SerializationFormat::Json)
63}
64
65/// Read a serialized (U)LLBC file.
66pub fn deserialize_llbc_with_format(
67    path: &std::path::Path,
68    format: options::SerializationFormat,
69) -> anyhow::Result<ast::TranslatedCrate> {
70    use crate::export::CrateData;
71    Ok(CrateData::deserialize_from_file(path, format)?.translated)
72}