Skip to main content

charon_lib/transform/add_missing_info/
reorder_decls.rs

1//! Compute an ordering on declarations that:
2//! - Detects mutually-recursive groups;
3//! - Always orders an item before any of its uses (except for recursive cases);
4//! - Otherwise keeps a stable order.
5//!
6//! Aeneas needs this because proof assistant languages are sensitive to declaration order and need
7//! to be explicit about mutual recursion. This should come useful for translation to any other
8//! language with these properties.
9use crate::options::TranslateOptions;
10use crate::transform::TransformCtx;
11use crate::ullbc_ast::*;
12use crate::utils::*;
13use derive_generic_visitor::*;
14use itertools::Itertools;
15use petgraph::graphmap::DiGraphMap;
16use rustc_hash::{FxHashMap as HashMap, FxHashSet as HashSet};
17use std::fmt::{Debug, Display, Error};
18use std::vec::Vec;
19
20use crate::transform::ctx::TransformPass;
21
22impl<Id: Copy> GDeclarationGroup<Id> {
23    pub fn get_ids(&self) -> &[Id] {
24        use GDeclarationGroup::*;
25        match self {
26            NonRec(id) => std::slice::from_ref(id),
27            Rec(ids) => ids.as_slice(),
28        }
29    }
30
31    pub fn get_any_trans_ids(&self) -> Vec<ItemId>
32    where
33        Id: Into<ItemId>,
34    {
35        self.get_ids().iter().copied().map(|id| id.into()).collect()
36    }
37
38    fn make_group(is_rec: bool, ids: Vec<ItemId>) -> Self
39    where
40        Id: TryFrom<ItemId>,
41        Id::Error: Debug,
42    {
43        let ids: Vec<_> = ids.into_iter().map(|x| x.try_into().unwrap()).collect();
44        if is_rec {
45            GDeclarationGroup::Rec(ids)
46        } else {
47            assert!(ids.len() == 1);
48            GDeclarationGroup::NonRec(ids[0])
49        }
50    }
51
52    fn to_mixed(&self) -> GDeclarationGroup<ItemId>
53    where
54        Id: Into<ItemId>,
55    {
56        match self {
57            GDeclarationGroup::NonRec(x) => GDeclarationGroup::NonRec((*x).into()),
58            GDeclarationGroup::Rec(_) => GDeclarationGroup::Rec(self.get_any_trans_ids()),
59        }
60    }
61}
62
63impl DeclarationGroup {
64    fn make_group(is_rec: bool, ids: Vec<ItemId>) -> Self {
65        let id0 = ids[0];
66        let all_same_kind = ids
67            .iter()
68            .all(|id| id0.variant_index_arity() == id.variant_index_arity());
69        match id0 {
70            _ if !all_same_kind => {
71                DeclarationGroup::Mixed(GDeclarationGroup::make_group(is_rec, ids))
72            }
73            ItemId::Type(_) => DeclarationGroup::Type(GDeclarationGroup::make_group(is_rec, ids)),
74            ItemId::Fun(_) => DeclarationGroup::Fun(GDeclarationGroup::make_group(is_rec, ids)),
75            ItemId::Global(_) => {
76                DeclarationGroup::Global(GDeclarationGroup::make_group(is_rec, ids))
77            }
78            ItemId::TraitDecl(_) => {
79                DeclarationGroup::TraitDecl(GDeclarationGroup::make_group(is_rec, ids))
80            }
81            ItemId::TraitImpl(_) => {
82                DeclarationGroup::TraitImpl(GDeclarationGroup::make_group(is_rec, ids))
83            }
84        }
85    }
86
87    pub fn to_mixed_group(&self) -> GDeclarationGroup<ItemId> {
88        use DeclarationGroup::*;
89        match self {
90            Type(gr) => gr.to_mixed(),
91            Fun(gr) => gr.to_mixed(),
92            Global(gr) => gr.to_mixed(),
93            TraitDecl(gr) => gr.to_mixed(),
94            TraitImpl(gr) => gr.to_mixed(),
95            Mixed(gr) => gr.clone(),
96        }
97    }
98
99    pub fn get_ids(&self) -> Vec<ItemId> {
100        use DeclarationGroup::*;
101        match self {
102            Type(gr) => gr.get_any_trans_ids(),
103            Fun(gr) => gr.get_any_trans_ids(),
104            Global(gr) => gr.get_any_trans_ids(),
105            TraitDecl(gr) => gr.get_any_trans_ids(),
106            TraitImpl(gr) => gr.get_any_trans_ids(),
107            Mixed(gr) => gr.get_any_trans_ids(),
108        }
109    }
110}
111
112impl<Id: Display> Display for GDeclarationGroup<Id> {
113    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), Error> {
114        match self {
115            GDeclarationGroup::NonRec(id) => write!(f, "non-rec: {id}"),
116            GDeclarationGroup::Rec(ids) => {
117                write!(
118                    f,
119                    "rec: {}",
120                    pretty_display_list(|id| format!("    {id}"), ids)
121                )
122            }
123        }
124    }
125}
126
127impl Display for DeclarationGroup {
128    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::result::Result<(), Error> {
129        match self {
130            DeclarationGroup::Type(decl) => write!(f, "{{ Type(s): {decl} }}"),
131            DeclarationGroup::Fun(decl) => write!(f, "{{ Fun(s): {decl} }}"),
132            DeclarationGroup::Global(decl) => write!(f, "{{ Global(s): {decl} }}"),
133            DeclarationGroup::TraitDecl(decl) => write!(f, "{{ Trait decls(s): {decl} }}"),
134            DeclarationGroup::TraitImpl(decl) => write!(f, "{{ Trait impl(s): {decl} }}"),
135            DeclarationGroup::Mixed(decl) => write!(f, "{{ Mixed items: {decl} }}"),
136        }
137    }
138}
139
140#[derive(Default)]
141pub struct Deps {
142    /// The dependency graph between translated items. We're careful to only add items that got
143    /// translated.
144    graph: DiGraphMap<ItemId, ()>,
145    unprocessed: Vec<ItemId>,
146    visited: HashSet<ItemId>,
147}
148
149/// We use this when computing the graph
150#[derive(Visitor)]
151pub struct DepsForItem<'a> {
152    ctx: &'a TransformCtx,
153    deps: &'a mut Deps,
154    current_id: ItemId,
155    // Each item countains its own id; we dont' want to count that as a self-reference. Hence the
156    // first time we see its own id, we skip.
157    seen_current_id: bool,
158    // We use this to track the trait impl block the current item belongs to
159    // (if relevant).
160    //
161    // We use this to ignore the references to the parent impl block.
162    //
163    // If we don't do so, when computing our dependency graph we end up with
164    // mutually recursive trait impl blocks/trait method impls in the presence
165    // of associated types (the deepest reason is that we don't normalize the
166    // types we query from rustc when translating the types from function
167    // signatures - we avoid doing so because as of now it makes resolving
168    // the trait params harder: if we get normalized types, we have to
169    // implement a normalizer on our side to make sure we correctly match
170    // types...).
171    //
172    //
173    // For instance, the problem happens if in Rust we have:
174    // ```text
175    // pub trait WithConstTy {
176    //     type W;
177    //     fn f(x: &mut Self::W);
178    // }
179    //
180    // impl WithConstTy for bool {
181    //     type W = u64;
182    //     fn f(_: &mut Self::W) {}
183    // }
184    // ```
185    //
186    // In LLBC we get:
187    //
188    // ```text
189    // impl traits::Bool::0 : traits::WithConstTy<bool>
190    // {
191    //     type W = u64 with []
192    //     fn f = traits::Bool::0::f
193    // }
194    //
195    // fn traits::Bool::0::f<@R0>(@1: &@R0 mut (traits::Bool::0::W)) { .. }
196    // //                                       ^^^^^^^^^^^^^^^
197    // //                                    refers to the trait impl
198    // ```
199    parent_trait_impl: Option<TraitImplId>,
200    parent_trait_decl: Option<TraitDeclId>,
201}
202
203impl Deps {
204    fn visitor_for_item<'a>(
205        &'a mut self,
206        ctx: &'a TransformCtx,
207        item: ItemRef<'_>,
208    ) -> DepsForItem<'a> {
209        let current_id = item.id();
210        self.graph.add_node(current_id);
211
212        let mut for_item = DepsForItem {
213            ctx,
214            deps: self,
215            seen_current_id: false,
216            current_id,
217            parent_trait_impl: None,
218            parent_trait_decl: None,
219        };
220
221        // Add the id of the impl/trait this item belongs to, if necessary
222        match item {
223            ItemRef::Fun(FunDecl {
224                src: FunSource::TraitDefault { trait_ref, .. },
225                ..
226            })
227            | ItemRef::Global(GlobalDecl {
228                src: GlobalSource::TraitDefault { trait_ref, .. },
229                ..
230            }) => for_item.parent_trait_decl = Some(trait_ref.id),
231            ItemRef::Fun(FunDecl {
232                src: FunSource::TraitImpl { impl_ref, .. },
233                ..
234            })
235            | ItemRef::Global(GlobalDecl {
236                src: GlobalSource::TraitImpl { impl_ref, .. },
237                ..
238            }) => for_item.parent_trait_impl = Some(impl_ref.id),
239            // An associated const's initializer belongs to the same impl as the const.
240            ItemRef::Fun(FunDecl {
241                src: FunSource::GlobalInitializer(global_ref),
242                ..
243            }) => {
244                if let Some(GlobalDecl {
245                    src: GlobalSource::TraitImpl { impl_ref, .. },
246                    ..
247                }) = ctx.translated.global_decls.get(global_ref.id)
248                {
249                    for_item.parent_trait_impl = Some(impl_ref.id);
250                }
251            }
252            _ => {}
253        }
254
255        for_item
256    }
257}
258
259impl DepsForItem<'_> {
260    fn insert_node(&mut self, tgt: impl Into<ItemId>) {
261        let tgt = tgt.into();
262        // Only add translated items.
263        if self.ctx.translated.get_item(tgt).is_some() && !self.deps.visited.contains(&tgt) {
264            self.deps.unprocessed.push(tgt);
265        }
266    }
267    fn insert_edge(&mut self, tgt: impl Into<ItemId>) {
268        let tgt = tgt.into();
269        if tgt == self.current_id && !self.seen_current_id {
270            // Each item contains its own id; this is a hack to avoid considering that as a self
271            // loop.
272            self.seen_current_id = true;
273            return;
274        }
275        self.insert_node(tgt);
276        // Only add translated items.
277        if self.ctx.translated.get_item(tgt).is_some() {
278            self.deps.graph.add_edge(self.current_id, tgt, ());
279        }
280    }
281}
282
283impl VisitAst for DepsForItem<'_> {
284    fn enter_type_decl_id(&mut self, id: &TypeDeclId) {
285        self.insert_edge(*id);
286    }
287
288    fn enter_global_decl_id(&mut self, id: &GlobalDeclId) {
289        self.insert_edge(*id);
290    }
291
292    fn enter_trait_impl_id(&mut self, id: &TraitImplId) {
293        // If the impl is the impl this item belongs to, we ignore it
294        // TODO: this is not very satisfying but this is the only way we have of preventing
295        // mutually recursive groups between method impls and trait impls in the presence of
296        // associated types...
297        if self.parent_trait_impl != Some(*id) {
298            self.insert_edge(*id);
299        }
300    }
301
302    fn enter_trait_decl_id(&mut self, id: &TraitDeclId) {
303        // If the trait is the trait this item belongs to, we ignore it. This is to avoid mutually
304        // recursive groups between e.g. traits decls and their globals. We treat methods
305        // specifically.
306        if self.parent_trait_decl != Some(*id) {
307            self.insert_edge(*id);
308        }
309    }
310
311    fn enter_fun_decl_id(&mut self, id: &FunDeclId) {
312        self.insert_edge(*id);
313    }
314
315    fn visit_trait_assoc_const(
316        &mut self,
317        assoc_const: &TraitAssocConst,
318    ) -> ControlFlow<Self::Break> {
319        let TraitAssocConst {
320            name: _,
321            attr_info: _,
322            ty,
323            default,
324        } = assoc_const;
325        ty.drive(self)?;
326        // We consider that a trait decl only contains the method/constant signatures.
327        // Therefore we don't explore the default method/const ids.
328        if let Some(gref) = default {
329            self.insert_node(gref.id); // Still count the item as reachable.
330            gref.generics.drive(self)?;
331        }
332        Continue(())
333    }
334
335    fn visit_trait_method(&mut self, method: &TraitMethod) -> ControlFlow<Self::Break> {
336        let TraitMethod {
337            name: _,
338            item_meta: _,
339            signature,
340            default,
341        } = method;
342        // We consider that a trait decl only contains the method/constant signatures.
343        // Therefore we don't explore the default method/const ids.
344        signature.drive(self)?;
345        if let Some(funref) = default {
346            self.insert_node(funref.id); // Still count the item as reachable.
347            funref.generics.drive(self)?;
348        }
349        Continue(())
350    }
351
352    fn visit_item_meta(&mut self, meta: &ItemMeta) -> ControlFlow<Self::Break> {
353        // Don't visit the name because trait impls contain their own id in it. Attributes however
354        // can contain genuine dependencies, notably between an item and its specifications.
355        meta.attr_info.drive(self)
356    }
357
358    fn visit_attribute(&mut self, attr: &Attribute) -> ControlFlow<Self::Break> {
359        // An item depends on its contracts, not the other way around.
360        match attr {
361            Attribute::IsContract { .. } => Continue(()),
362            _ => self.visit_inner(attr),
363        }
364    }
365
366    // The layout guarantees of a type mention the type itself -- we ignore those.
367    fn visit_layout(&mut self, _: &Layout) -> ControlFlow<Self::Break> {
368        Continue(())
369    }
370    // Sources are reverse dependencies; exploring them is likely to create dependency cycles.
371    fn visit_type_source(&mut self, src: &TypeSource) -> ControlFlow<Self::Break> {
372        if let TypeSource::Closure { info } = src {
373            // Make the closure body reachable but don't consider the closure struct to depend on it.
374            self.insert_node(info.closure_body.id);
375            info.closure_body.generics.drive(self)?;
376        }
377        Continue(())
378    }
379    fn visit_fun_source(&mut self, src: &FunSource) -> ControlFlow<Self::Break> {
380        if let FunSource::TraitDefault { trait_ref, .. } = src {
381            self.insert_edge(trait_ref.id);
382        }
383        Continue(())
384    }
385    fn visit_global_source(&mut self, _: &GlobalSource) -> ControlFlow<Self::Break> {
386        Continue(())
387    }
388    fn visit_trait_decl_source(&mut self, _: &TraitDeclSource) -> ControlFlow<Self::Break> {
389        Continue(())
390    }
391    fn visit_trait_impl_source(&mut self, _: &TraitImplSource) -> ControlFlow<Self::Break> {
392        Continue(())
393    }
394}
395
396fn compute_declarations_graph(ctx: &TransformCtx) -> DiGraphMap<ItemId, ()> {
397    let mut deps = Deps::default();
398    // Start from the items selected as starting points. We've mostly only translated items
399    // accessible from those, but some passes render items inaccessible again, which we filter out
400    // here.
401    deps.unprocessed = ctx
402        .translated
403        .all_items()
404        .filter(|item| item.item_meta().started_from)
405        .map(|item| item.id())
406        .collect();
407
408    // Explore reachable items.
409    while let Some(id) = deps.unprocessed.pop() {
410        if deps.visited.insert(id)
411            && let Some(item) = ctx.translated.get_item(id)
412        {
413            let mut visitor = deps.visitor_for_item(ctx, item);
414            item.drive(&mut visitor);
415        }
416    }
417    deps.graph
418}
419
420fn compute_reordered_decls(ctx: &mut TransformCtx) -> Vec<DeclarationGroup> {
421    // Build the graph of dependencies between items.
422    let graph = compute_declarations_graph(ctx);
423
424    // Pre-sort files to limit the number of costly string comparisons. Maps file ids to an index
425    // that reflects ordering on the crates (with `core` and `std` sorted first) and file names.
426    let sorted_file_ids: IndexMap<FileId, usize> = ctx
427        .translated
428        .files
429        .indices()
430        .sorted_by_cached_key(|&file_id| {
431            let file = &ctx.translated.files[file_id];
432            let is_std = file.crate_name == "std" || file.crate_name == "core";
433            (!is_std, &file.crate_name, &file.name)
434        })
435        .enumerate()
436        .sorted_by_key(|(_i, file_id)| *file_id)
437        .map(|(i, _file_id)| i)
438        .collect();
439    assert_eq!(ctx.translated.files.len(), sorted_file_ids.slot_count());
440
441    // We sort items as follows: std items, then items from foreign crates (sorted by crate name),
442    // then local items. Within a crate, we sort by file then by source order.
443    let sort_by = |item: &ItemRef| {
444        let item_meta = item.item_meta();
445        let span = item_meta.span.data();
446        let file_name_order = sorted_file_ids.get(span.file_id);
447        (
448            item_meta.is_local,
449            file_name_order,
450            span.beg,
451            item_meta.name.mono_args().cloned(),
452            item.id(),
453        )
454    };
455    // We record for each item the order in which we're sorting it, to make `sort_by` cheap.
456    let item_sorted_index: HashMap<ItemId, usize> = ctx
457        .translated
458        .all_items()
459        .sorted_by_cached_key(sort_by)
460        .enumerate()
461        .map(|(i, item)| (item.id(), i))
462        .collect();
463    let sort_by = |id: &ItemId| item_sorted_index.get(id).unwrap();
464
465    // Compute SCCs (Strongly Connected Components) for the graph in a way that matches the chosen
466    // order as much as possible.
467    let reordered_sccs = super::sccs::ordered_scc(&graph, sort_by);
468
469    // Convert to a list of declarations.
470    let reordered_decls = reordered_sccs
471        .into_iter()
472        // This can happen if we failed to translate the item in this group.
473        .filter(|scc| !scc.is_empty())
474        .map(|scc| {
475            // If an SCC has length one, the declaration may be simply recursive: we determine whether
476            // it is the case by checking if the def id is in its own set of dependencies.
477            // Trait declarations often refer to `Self`, which means they are often considered as
478            // recursive by our analysis. So we cheat an declare them non-recursive.
479            // TODO: do something more precise. What is important is that we never use the "whole" self
480            // clause as argument, but rather projections over the self clause (like `<Self as
481            // Foo>::u`, in the declaration for `Foo`).
482            let id0 = scc[0];
483            let is_non_rec =
484                scc.len() == 1 && (id0.is_trait_decl() || !graph.neighbors(id0).contains(&id0));
485
486            DeclarationGroup::make_group(!is_non_rec, scc)
487        })
488        .collect();
489
490    trace!("{:?}", reordered_decls);
491    reordered_decls
492}
493
494pub struct Transform;
495impl TransformPass for Transform {
496    fn should_run(&self, options: &TranslateOptions) -> bool {
497        !options.no_reorder_decls
498    }
499
500    fn transform_ctx(&self, ctx: &mut TransformCtx) {
501        let reordered_decls = compute_reordered_decls(ctx);
502        ctx.translated.ordered_decls = Some(reordered_decls);
503    }
504}