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_ret_no_self,
23    clippy::new_without_default,
24    clippy::should_implement_trait,
25    clippy::useless_format
26)]
27// For when we use charon on itself :3
28#![cfg_attr(feature = "charon_on_charon", feature(register_tool))]
29#![cfg_attr(feature = "charon_on_charon", register_tool(charon))]
30
31#[macro_use]
32pub mod ids;
33#[macro_use]
34pub mod logger;
35pub mod ast;
36pub mod common;
37pub mod errors;
38pub mod export;
39pub mod name_matcher;
40pub mod options;
41pub mod pretty;
42pub mod transform;
43
44// Re-export all the ast modules so we can keep the old import structure.
45pub use ast::{builtins, expressions, gast, llbc_ast, meta, names, types, ullbc_ast, values};
46pub use pretty::formatter;
47
48/// The version of the crate, as defined in `Cargo.toml`.
49pub const VERSION: &str = env!("CARGO_PKG_VERSION");
50
51/// Read a `.llbc` file.
52pub fn deserialize_llbc(path: &std::path::Path) -> anyhow::Result<ast::TranslatedCrate> {
53    deserialize_llbc_with_format(path, options::SerializationFormat::Json)
54}
55
56/// Read a serialized (U)LLBC file.
57pub fn deserialize_llbc_with_format(
58    path: &std::path::Path,
59    format: options::SerializationFormat,
60) -> anyhow::Result<ast::TranslatedCrate> {
61    use crate::export::CrateData;
62    Ok(CrateData::deserialize_from_file(path, format)?.translated)
63}