charon_lib/
lib.rs

1//! This library contains the definitions of the "LLBC" (Low-Level Borrow Calculus)
2//! AST, which faithfully captures the full and explicit contents of a Rust crate.
3//! The `charon` binary can translate any Rust crate to this AST, which can then be consumed for
4//! all sorts of purposes (most notably analysis, code generation, and execution).
5//!
6//! The main type of this crate is [`ast::TranslatedCrate`].
7//! To get one, call `charon` to get a serialized crate, then deserialize it using using
8//! [`deserialize_llbc`].
9//! A crate is mainly composed of 5 kinds of items:
10//! - Functions;
11//! - Type definitions;
12//! - Globals (constants and statics);
13//! - Trait declarations;
14//! - Trait implementations.
15//!
16//! Each of these items is identified internally by a unique [`ast::ItemId`],
17//! and externally by its [`ast::Name`], such as "`core::result::Result`".
18//! To find an item with a given name, have a look at the name matcher [`name_matcher::Pattern`]s.
19//!
20//! Function bodies come in two forms: "structured" or "unstructured", depending on whether their
21//! control-flow is syntax-like (with blocks and scopes) or control-flow-like (with gotos).
22//! This can be chosen during translation. The corresponding ASTs can be found respectively in
23//! [`llbc_ast`] and [`ullbc_ast`].
24// For rustdoc: prevents overflows
25#![recursion_limit = "256"]
26#![allow(
27    clippy::borrowed_box,
28    clippy::derivable_impls,
29    clippy::field_reassign_with_default,
30    clippy::manual_map,
31    clippy::mem_replace_with_default,
32    clippy::new_ret_no_self,
33    clippy::new_without_default,
34    clippy::redundant_field_names,
35    clippy::should_implement_trait,
36    clippy::useless_format
37)]
38// For when we use charon on itself :3
39#![cfg_attr(feature = "charon_on_charon", feature(register_tool))]
40#![cfg_attr(feature = "charon_on_charon", feature(rustc_private))]
41#![cfg_attr(feature = "charon_on_charon", register_tool(charon))]
42
43#[cfg(feature = "charon_on_charon")]
44#[allow(unused_extern_crates)]
45extern crate rustc_hir;
46
47#[macro_use]
48pub mod ids;
49#[macro_use]
50pub mod logger;
51pub mod ast;
52pub mod errors;
53pub mod export;
54pub mod name_matcher;
55pub mod options;
56pub mod pretty;
57pub mod transform;
58pub mod utils;
59
60pub use ast::{llbc_ast, ullbc_ast};
61pub use pretty::formatter;
62
63/// The version of the crate, as defined in `Cargo.toml`.
64pub const VERSION: &str = env!("CARGO_PKG_VERSION");
65
66/// Read a `.llbc` file.
67pub fn deserialize_llbc(path: &std::path::Path) -> anyhow::Result<ast::TranslatedCrate> {
68    deserialize_llbc_with_format(path, options::SerializationFormat::Json)
69}
70
71/// Read a serialized (U)LLBC file.
72pub fn deserialize_llbc_with_format(
73    path: &std::path::Path,
74    format: options::SerializationFormat,
75) -> anyhow::Result<ast::TranslatedCrate> {
76    use crate::export::CrateData;
77    Ok(CrateData::deserialize_from_file(path, format)?.translated)
78}
charon_lib/lib.rs

charon_lib/
lib.rs
