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", feature(rustc_private))]
40#![cfg_attr(feature = "charon_on_charon", register_tool(charon))]
41
42#[cfg(feature = "charon_on_charon")]
43#[allow(unused_extern_crates)]
44extern crate rustc_hir;
45
46#[macro_use]
47pub mod ids;
48#[macro_use]
49pub mod logger;
50pub mod ast;
51pub mod common;
52pub mod errors;
53pub mod export;
54pub mod name_matcher;
55pub mod options;
56pub mod pretty;
57pub mod transform;
58
59// Re-export all the ast modules so we can keep the old import structure.
60pub use ast::{builtins, expressions, gast, llbc_ast, meta, names, types, ullbc_ast, values};
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}