charon_lib/ast/
krate.rs

1use std::fmt;
2
3use derive_generic_visitor::{Drive, DriveMut, DriveTwo};
4use index_vec::Idx;
5use itertools::Itertools;
6use serde::{Deserialize, Serialize};
7use serde_state::{DeserializeState, SerializeState};
8
9use crate::ast::*;
10use crate::formatter::{FmtCtx, IntoFormatter};
11use crate::ids::{IndexMap, IndexVec};
12use crate::pretty::FmtWithCtx;
13use crate::utils::serialize_map_to_array::SeqHashMapToArray;
14use macros::{EnumAsGetters, EnumIsA, VariantIndexArity, VariantName};
15
16/// A target triple, e.g. `x86_64-unknown-linux-gnu`.
17pub type TargetTriple = String;
18
19/// The complete data of a Rust crate.
20///
21/// A crate is mainly composed of 5 kinds of items:
22/// - Functions;
23/// - Type definitions;
24/// - Globals (constants and statics);
25/// - Trait declarations;
26/// - Trait implementations.
27///
28/// These can each be found in the corresponding `IndexVec`. They are in an unspecified (though
29/// deterministic) order.
30/// If you need a more robust order, see `ordered_decls`.
31///
32/// To get a `TranslatedCrate`, run `charon cargo` inside a Rust crate, then deserialize
33/// the resulting `crate_name.llbc` file using [`crate::deserialize_llbc`].
34#[derive(Default, Clone, Drive, DriveMut, DriveTwo, SerializeState, DeserializeState)]
35#[serde_state(state_implements = HashConsSerializerState)]
36pub struct TranslatedCrate {
37    /// The name of the crate.
38    pub crate_name: String,
39
40    /// The options used when calling Charon. Can be used to check that Charon was called with the
41    /// options that a given consumer requires.
42    #[serde_state(stateless)]
43    pub options: crate::options::CliOpts,
44
45    /// Information about each target platform for which the crate was translated. When translating
46    /// a crate normally this will have a single entry; when using `--targets` this will have one
47    /// entry per chosen target.
48    #[serde(with = "SeqHashMapToArray::<TargetTriple, TargetInfo>")]
49    pub target_information: SeqHashMap<TargetTriple, TargetInfo>,
50
51    /// The source files composing the crate and its dependencies. Each [`Span`] refers to a byte
52    /// range within one of these files.
53    // This field must come before any field containing spans, as the OCaml deserialization of
54    // spans requires the files to be deserialized already.
55    #[serde_state(stateless)]
56    pub files: IndexVec<FileId, File>,
57
58    /// The names of all registered items. Available so we can know the names even of items that
59    /// failed to translate.
60    /// Invariant: after translation, any existing `ItemId` must have an associated name, even
61    /// if the corresponding item wasn't translated.
62    #[serde(with = "SeqHashMapToArray::<ItemId, Name>")]
63    pub item_names: SeqHashMap<ItemId, Name>,
64    /// The names of all the registered associated items. Available so we can know the names even
65    /// of items that failed to translate.
66    /// Invariant: after translation, any existing `AssocItemId` must have an associated name, even
67    /// if the corresponding item wasn't translated.
68    pub assoc_item_names: IndexMap<TraitDeclId, AssocItemNames>,
69    /// Short names, for items whose last PathElem is unique.
70    #[serde(with = "SeqHashMapToArray::<ItemId, Name>")]
71    pub short_names: SeqHashMap<ItemId, Name>,
72
73    /// The type definitions (structs, enums, ...).
74    pub type_decls: IndexMap<TypeDeclId, TypeDecl>,
75    /// The function definitions.
76    ///
77    /// Each item with a body becomes a function: actual functions, methods, and unevaluated
78    /// consts/statics.
79    pub fun_decls: IndexMap<FunDeclId, FunDecl>,
80    /// The global definitions, which are constants, statics, and thread locals.
81    pub global_decls: IndexMap<GlobalDeclId, GlobalDecl>,
82    /// The trait declarations.
83    pub trait_decls: IndexMap<TraitDeclId, TraitDecl>,
84    /// The trait implementations.
85    pub trait_impls: IndexMap<TraitImplId, TraitImpl>,
86    /// This contains a list of all the reachable items in the crate in a stable, logical order
87    /// based on crate and file order, then further grouped and sorted such that every item comes
88    /// after the items it depends on.
89    /// Mutually-dependent groups of items are identified as such.
90    /// This is meant for code-generation tools that want a stable output order.
91    ///
92    /// Not all the items in the `TranslatedCrate` are included: some trait impls are never
93    /// referred to by reachable items so could in principle be removed from the crate, but we keep
94    /// them around to be able to tell method implementations apart.
95    ///
96    /// `Some` after translation unless `--no-reorder-decls` is passed.
97    #[serde_state(stateless)]
98    pub ordered_decls: Option<Vec<DeclarationGroup>>,
99}
100
101/// A (group of) top-level declaration(s), properly reordered.
102/// "G" stands for "generic"
103#[derive(
104    Debug, Clone, VariantIndexArity, VariantName, EnumAsGetters, EnumIsA, Serialize, Deserialize,
105)]
106#[cfg_attr(feature = "charon_on_charon", charon::variants_suffix("Group"))]
107pub enum GDeclarationGroup<Id> {
108    /// A non-recursive declaration
109    NonRec(Id),
110    /// A (group of mutually) recursive declaration(s)
111    Rec(Vec<Id>),
112}
113
114/// A (group of) top-level declaration(s), properly reordered.
115#[derive(
116    Debug, Clone, VariantIndexArity, VariantName, EnumAsGetters, EnumIsA, Serialize, Deserialize,
117)]
118#[cfg_attr(feature = "charon_on_charon", charon::variants_suffix("Group"))]
119pub enum DeclarationGroup {
120    /// A type declaration group
121    Type(GDeclarationGroup<TypeDeclId>),
122    /// A function declaration group
123    Fun(GDeclarationGroup<FunDeclId>),
124    /// A global declaration group
125    Global(GDeclarationGroup<GlobalDeclId>),
126    TraitDecl(GDeclarationGroup<TraitDeclId>),
127    TraitImpl(GDeclarationGroup<TraitImplId>),
128    /// Anything that doesn't fit into these categories.
129    Mixed(GDeclarationGroup<ItemId>),
130}
131
132#[derive(Default, Clone, Drive, DriveMut, DriveTwo, SerializeState, DeserializeState)]
133pub struct AssocItemNames {
134    pub types: IndexVec<AssocTypeId, TraitItemName>,
135    pub methods: IndexVec<TraitMethodId, TraitItemName>,
136    pub consts: IndexVec<AssocConstId, TraitItemName>,
137}
138
139impl TranslatedCrate {
140    pub fn item_name(&self, id: impl Into<ItemId>) -> &Name {
141        // `unwrap` is ok because we ensure to translate the item name as soon as we create a new
142        // item id.
143        self.item_names.get(&id.into()).unwrap()
144    }
145    pub fn assoc_item_name(
146        &self,
147        trait_id: TraitDeclId,
148        id: impl Into<AssocItemId>,
149    ) -> TraitItemName {
150        let names = &self.assoc_item_names[trait_id];
151        match id.into() {
152            AssocItemId::Type(id) => names.types[id],
153            AssocItemId::Method(id) => names.methods[id],
154            AssocItemId::Const(id) => names.consts[id],
155        }
156    }
157
158    pub fn item_short_name(&self, id: impl Into<ItemId>) -> &Name {
159        let id = id.into();
160        self.short_names
161            .get(&id)
162            .unwrap_or_else(|| self.item_name(id))
163    }
164
165    pub fn get_item(&self, trans_id: impl Into<ItemId>) -> Option<ItemRef<'_>> {
166        match trans_id.into() {
167            ItemId::Type(id) => self.type_decls.get(id).map(ItemRef::Type),
168            ItemId::Fun(id) => self.fun_decls.get(id).map(ItemRef::Fun),
169            ItemId::Global(id) => self.global_decls.get(id).map(ItemRef::Global),
170            ItemId::TraitDecl(id) => self.trait_decls.get(id).map(ItemRef::TraitDecl),
171            ItemId::TraitImpl(id) => self.trait_impls.get(id).map(ItemRef::TraitImpl),
172        }
173    }
174    pub fn get_item_mut(&mut self, trans_id: ItemId) -> Option<ItemRefMut<'_>> {
175        match trans_id {
176            ItemId::Type(id) => self.type_decls.get_mut(id).map(ItemRefMut::Type),
177            ItemId::Fun(id) => self.fun_decls.get_mut(id).map(ItemRefMut::Fun),
178            ItemId::Global(id) => self.global_decls.get_mut(id).map(ItemRefMut::Global),
179            ItemId::TraitDecl(id) => self.trait_decls.get_mut(id).map(ItemRefMut::TraitDecl),
180            ItemId::TraitImpl(id) => self.trait_impls.get_mut(id).map(ItemRefMut::TraitImpl),
181        }
182    }
183
184    /// Remove this item from the crate, including the name information about it.
185    ///
186    /// See also [`TranslatedCrate::remove_item_temporarily`].
187    pub fn remove_item(&mut self, trans_id: ItemId) -> Option<ItemByVal> {
188        self.short_names.swap_remove(&trans_id);
189        self.item_names.swap_remove(&trans_id);
190        self.remove_item_temporarily(trans_id)
191    }
192    /// Insert a new item into a slot, and record its name in the name map.
193    pub fn set_new_item_slot(&mut self, id: ItemId, item: impl Into<ItemByVal>) {
194        let item = item.into();
195        self.item_names
196            .insert(id, item.as_ref().item_meta().name.clone());
197        self.put_item_back(id, item);
198    }
199    /// Remove this item from the crate without touching the name maps.
200    /// Useful for modifying items whilst being able to access the rest of the crate.
201    /// Put the item back using [`TranslatedCrate::put_item_back`].
202    ///
203    /// See also [`TranslatedCrate::remove_item`].
204    pub fn remove_item_temporarily(&mut self, trans_id: ItemId) -> Option<ItemByVal> {
205        match trans_id {
206            ItemId::Type(id) => self.type_decls.remove(id).map(ItemByVal::Type),
207            ItemId::Fun(id) => self.fun_decls.remove(id).map(ItemByVal::Fun),
208            ItemId::Global(id) => self.global_decls.remove(id).map(ItemByVal::Global),
209            ItemId::TraitDecl(id) => self.trait_decls.remove(id).map(ItemByVal::TraitDecl),
210            ItemId::TraitImpl(id) => self.trait_impls.remove(id).map(ItemByVal::TraitImpl),
211        }
212    }
213    /// Insert the item into the corresponding slot without recording its name in the name map.
214    /// Only use if the item already has its name registered, e.g. if you got it using
215    /// [`TranslatedCrate::remove_item_temporarily`].
216    pub fn put_item_back(&mut self, id: ItemId, item: impl Into<ItemByVal>) {
217        match item.into() {
218            ItemByVal::Type(decl) => self.type_decls.set_slot(*id.as_type().unwrap(), decl),
219            ItemByVal::Fun(decl) => self.fun_decls.set_slot(*id.as_fun().unwrap(), decl),
220            ItemByVal::Global(decl) => self.global_decls.set_slot(*id.as_global().unwrap(), decl),
221            ItemByVal::TraitDecl(decl) => self
222                .trait_decls
223                .set_slot(*id.as_trait_decl().unwrap(), decl),
224            ItemByVal::TraitImpl(decl) => self
225                .trait_impls
226                .set_slot(*id.as_trait_impl().unwrap(), decl),
227        }
228    }
229
230    pub fn all_ids(&self) -> impl Iterator<Item = ItemId> + use<> {
231        self.type_decls
232            .all_indices()
233            .map(ItemId::Type)
234            .chain(self.trait_decls.all_indices().map(ItemId::TraitDecl))
235            .chain(self.trait_impls.all_indices().map(ItemId::TraitImpl))
236            .chain(self.global_decls.all_indices().map(ItemId::Global))
237            .chain(self.fun_decls.all_indices().map(ItemId::Fun))
238    }
239    pub fn all_items(&self) -> impl Iterator<Item = ItemRef<'_>> {
240        self.type_decls
241            .iter()
242            .map(ItemRef::Type)
243            .chain(self.trait_decls.iter().map(ItemRef::TraitDecl))
244            .chain(self.trait_impls.iter().map(ItemRef::TraitImpl))
245            .chain(self.global_decls.iter().map(ItemRef::Global))
246            .chain(self.fun_decls.iter().map(ItemRef::Fun))
247    }
248    pub fn all_items_mut(&mut self) -> impl Iterator<Item = ItemRefMut<'_>> {
249        self.type_decls
250            .iter_mut()
251            .map(ItemRefMut::Type)
252            .chain(self.trait_impls.iter_mut().map(ItemRefMut::TraitImpl))
253            .chain(self.trait_decls.iter_mut().map(ItemRefMut::TraitDecl))
254            .chain(self.fun_decls.iter_mut().map(ItemRefMut::Fun))
255            .chain(self.global_decls.iter_mut().map(ItemRefMut::Global))
256    }
257    pub fn all_items_with_ids(&self) -> impl Iterator<Item = (ItemId, ItemRef<'_>)> {
258        self.all_items().map(|item| (item.id(), item))
259    }
260
261    /// When translating without `--target`, there's only one target information; this method
262    /// retrieves it.
263    /// Panics if this crate was translated in multi-target mode.
264    pub fn the_target_information(&self) -> &TargetInfo {
265        self.target_information
266            .values()
267            .exactly_one()
268            .ok()
269            .expect("called `the_target_information` on a multi-target crate")
270    }
271}
272
273impl fmt::Display for TranslatedCrate {
274    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
275        let fmt: &FmtCtx = &self.into_fmt();
276        match &self.ordered_decls {
277            None => {
278                // We do simple: types, globals, traits, functions
279                for d in &self.type_decls {
280                    writeln!(f, "{}\n", d.with_ctx(fmt))?
281                }
282                for d in &self.global_decls {
283                    writeln!(f, "{}\n", d.with_ctx(fmt))?
284                }
285                for d in &self.trait_decls {
286                    writeln!(f, "{}\n", d.with_ctx(fmt))?
287                }
288                for d in &self.trait_impls {
289                    writeln!(f, "{}\n", d.with_ctx(fmt))?
290                }
291                for d in &self.fun_decls {
292                    writeln!(f, "{}\n", d.with_ctx(fmt))?
293                }
294            }
295            Some(ordered_decls) => {
296                for gr in ordered_decls {
297                    for id in gr.get_ids() {
298                        writeln!(f, "{}\n", fmt.format_decl_id(id))?
299                    }
300                }
301            }
302        }
303        fmt::Result::Ok(())
304    }
305}
306
307impl<'a> IntoFormatter for &'a TranslatedCrate {
308    type C = FmtCtx<'a>;
309
310    fn into_fmt(self) -> Self::C {
311        FmtCtx {
312            translated: Some(self),
313            ..Default::default()
314        }
315    }
316}
317
318pub trait HasIdxMapOf<Id: Idx>: std::ops::Index<Id, Output: Sized> {
319    fn get_idx_map(&self) -> &IndexMap<Id, Self::Output>;
320    fn get_idx_map_mut(&mut self) -> &mut IndexMap<Id, Self::Output>;
321}
322
323/// Delegate `Index` implementations to subfields.
324macro_rules! mk_index_impls {
325    ($ty:ident.$field:ident[$idx:ty]: $output:ty) => {
326        impl std::ops::Index<$idx> for $ty {
327            type Output = $output;
328            fn index(&self, index: $idx) -> &Self::Output {
329                &self.$field[index]
330            }
331        }
332        impl std::ops::IndexMut<$idx> for $ty {
333            fn index_mut(&mut self, index: $idx) -> &mut Self::Output {
334                &mut self.$field[index]
335            }
336        }
337        impl HasIdxMapOf<$idx> for $ty {
338            fn get_idx_map(&self) -> &IndexMap<$idx, Self::Output> {
339                &self.$field
340            }
341            fn get_idx_map_mut(&mut self) -> &mut IndexMap<$idx, Self::Output> {
342                &mut self.$field
343            }
344        }
345    };
346}
347mk_index_impls!(TranslatedCrate.type_decls[TypeDeclId]: TypeDecl);
348mk_index_impls!(TranslatedCrate.fun_decls[FunDeclId]: FunDecl);
349mk_index_impls!(TranslatedCrate.global_decls[GlobalDeclId]: GlobalDecl);
350mk_index_impls!(TranslatedCrate.trait_decls[TraitDeclId]: TraitDecl);
351mk_index_impls!(TranslatedCrate.trait_impls[TraitImplId]: TraitImpl);
charon_lib/ast/krate.rs

charon_lib/ast/
krate.rs
