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

charon_lib/
lib.rs
