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

charon_lib/ast/
krate.rs
