Skip to main content

charon_lib/transform/
mod.rs

1pub mod ctx;
2pub mod typecheck_and_unify;
3pub mod utils;
4
5/// Passes that finish translation, i.e. required for the output to be a valid output.
6pub mod finish_translation {
7    pub mod filter_invisible_trait_impls;
8    pub mod insert_assign_return_unit;
9    pub mod insert_ptr_metadata;
10    pub mod insert_storage_statements;
11}
12
13/// Passes that compute extra info to be stored in the crate.
14pub mod add_missing_info {
15    pub mod add_implied_outlives;
16    pub mod add_missing_alias_clauses;
17    pub mod compute_short_names;
18    pub mod link_specs;
19    pub mod recover_body_comments;
20    pub mod reorder_decls;
21    pub mod sccs;
22}
23
24/// Passes that effect some kind of normalization on the crate.
25pub mod normalize {
26    pub mod desugar_drops;
27    pub mod expand_associated_types;
28    pub mod filter_unreachable_blocks;
29    pub mod partial_monomorphization;
30    pub mod skip_trait_refs_when_known;
31    pub mod transform_dyn_trait_calls;
32}
33
34/// Passes that undo some lowering done by rustc to recover an operation closer to what the user
35/// wrote.
36pub mod resugar {
37    pub mod move_asserts_to_statements;
38    pub mod reconstruct_asserts;
39    pub mod reconstruct_box_derefs;
40    pub mod reconstruct_fallible_operations;
41    pub mod reconstruct_intrinsics;
42    pub mod reconstruct_matches;
43    pub mod reconstruct_vec_boxes;
44}
45
46/// Passes that make the output simpler/easier to consume.
47pub mod simplify_output {
48    pub mod anon_const_to_call;
49    pub mod duplicate_defaulted_methods;
50    pub mod filter_trivial_drops;
51    pub mod hide_allocator_param;
52    pub mod index_intermediate_assigns;
53    pub mod index_to_function_calls;
54    pub mod inline_selected_functions;
55    pub mod lift_associated_item_clauses;
56    pub mod ops_to_function_calls;
57    pub mod remove_adt_clauses;
58    pub mod remove_nops;
59    pub mod remove_unit_locals;
60    pub mod remove_unused_clauses;
61    pub mod remove_unused_locals;
62    pub mod simplify_constants;
63    pub mod unbind_item_vars;
64    pub mod update_block_indices;
65}
66
67/// Passes that manipulate the control flow and reconstruct its structure.
68pub mod control_flow {
69    pub mod duplicate_return;
70    pub mod merge_goto_chains;
71    pub mod prettify_cfg;
72    pub mod ullbc_to_llbc;
73}
74
75pub use ctx::TransformCtx;
76use ctx::{LlbcPass, TransformPass, UllbcPass};
77
78use crate::options::CliOpts;
79
80/// Run transformation passes on the crate before outputting it.
81pub fn run_transformation_passes(options: &CliOpts, ctx: &mut TransformCtx) {
82    // Passes that apply to the whole crate at once, typically those that change item signatures.
83    let global = |x| Pass::NonBody(CowBox::Borrowed(x));
84    // Passes that apply to bodies but work on either kind.
85    let mixed_body = |x| Pass::NonBody(CowBox::Borrowed(x));
86
87    ctx.run_pass(Pass::NonBody(PrintCtxPass::new(
88        options.print_original_ullbc,
89        "# ULLBC after translation from MIR".to_string(),
90    )));
91
92    // Item and type cleanup passes.
93    ctx.run_passes([
94        // Link specification items and the items they specify in both directions.
95        global(&add_missing_info::link_specs::Transform),
96        // `--duplicate-defaulted-methods`: copy default method bodies into impls that use them.
97        global(&simplify_output::duplicate_defaulted_methods::Transform),
98        // Compute short names. We do it early to make pretty-printed output more legible in traces.
99        global(&add_missing_info::compute_short_names::Transform),
100        // Check that translation emitted consistent types, and unify body lifetimes (best-effort).
101        global(&typecheck_and_unify::Check::PostTranslation),
102        // Filter the trait impls that were marked invisible since we couldn't filter them out
103        // earlier.
104        global(&finish_translation::filter_invisible_trait_impls::Transform),
105        // Move clauses on associated types to be implied clauses of the trait.
106        global(&simplify_output::lift_associated_item_clauses::Transform),
107        // Type aliases may use associated types without declaring the corresponding trait
108        // such missing trait clauses.
109        global(&add_missing_info::add_missing_alias_clauses::Transform),
110        // Make explicit the outlives predicates implied by item signatures.
111        global(&add_missing_info::add_implied_outlives::Transform),
112    ]);
113
114    // Body cleanup passes on the ullbc.
115    let pass = Pass::FusedUnstructuredBody(Box::new([
116        // Compute the metadata & insert for Rvalue
117        CowBox::Borrowed(&finish_translation::insert_ptr_metadata::Transform),
118        // Add the missing assignments to the return value.
119        // When the function return type is unit, the generated MIR doesn't set the return value to
120        // `()`. This can be a concern: in the case of Aeneas, it means the return variable
121        // contains ⊥ upon returning. For this reason, when the function has return type unit, we
122        // insert an extra assignment just before returning.
123        CowBox::Borrowed(&finish_translation::insert_assign_return_unit::Transform),
124        // Insert storage markers for locals that don't have them (that's allowed in MIR).
125        CowBox::Borrowed(&finish_translation::insert_storage_statements::Transform),
126        // Transform Drops into Calls to drop_glue.
127        CowBox::Borrowed(&normalize::desugar_drops::Transform),
128        // Whenever we reference a trait method on a known type, refer to the method `FunDecl`
129        // directly instead of going via a `TraitRef`. This is done before associated-type lifting
130        // because it messes up generic args order.
131        CowBox::Borrowed(&normalize::skip_trait_refs_when_known::Transform),
132        // Transform dyn trait method calls to vtable function pointer calls.
133        // This should be early to handle the calls before other transformations.
134        CowBox::Borrowed(&normalize::transform_dyn_trait_calls::Transform),
135        // Replace promoted and inline consts with calls to their initializers.
136        simplify_output::anon_const_to_call::Transform::new(ctx),
137        // Inline promoted and inline consts, as well as dummy auto-generated panic functions.
138        simplify_output::inline_selected_functions::Transform::new(ctx),
139        // Remove drop statements that are noops.
140        CowBox::Borrowed(&simplify_output::filter_trivial_drops::Transform),
141        // Inline all asserts that correspond to dynamic checks into statements.
142        // The following pass will then merge the generated gotos as part of this substitution,
143        // and [reconstruct_fallible_operations] can then use the inlined asserts to
144        // reconstruct the fallible operations.
145        CowBox::Borrowed(&resugar::move_asserts_to_statements::Transform),
146        // Merge single-origin gotos into their parent. This drastically reduces the graph size
147        // of the CFG.
148        // This must be done early as some resugaring passes depend on it.
149        CowBox::Borrowed(&control_flow::merge_goto_chains::Transform),
150        // Remove overflow/div-by-zero/bounds checks since they are already part of the
151        // arithmetic/array operation in the semantics of (U)LLBC.
152        // **WARNING**: this pass uses the fact that the dynamic checks introduced by Rustc use a
153        // special "assert" construct. Because of this, it must happen *before* the
154        // [reconstruct_asserts] pass. See the comments in [crate::remove_dynamic_checks].
155        // **WARNING**: this pass relies on a precise structure of the MIR statements. Because of this,
156        // it must happen before passes that insert statements like [simplify_constants].
157        CowBox::Borrowed(&resugar::reconstruct_fallible_operations::Transform),
158        // Reconstruct `vec![x]` lowering to avoid unsafe operations.
159        // **WARNING**: this pass relies on a precise structure of the MIR statements. Because of
160        // this, it must happen before passes that insert statements like [simplify_constants].
161        // This must also happen after `inline_selected_functions`, and `merge_goto_chains`.
162        resugar::reconstruct_vec_boxes::Transform::new(ctx),
163        // Resugar the box derefs that got desugared in elaborated MIR.
164        CowBox::Borrowed(&resugar::reconstruct_box_derefs::Transform),
165        // Recognize calls to the `offset_of` intrinsics and replace them with the
166        // corresponding `NullOp`.
167        CowBox::Borrowed(&resugar::reconstruct_intrinsics::Transform),
168        // Reconstruct the asserts
169        CowBox::Borrowed(&resugar::reconstruct_asserts::Transform),
170        // Desugar the constants to other values/operands as much as possible.
171        CowBox::Borrowed(&simplify_output::simplify_constants::Transform),
172        // Introduce intermediate assignments in preparation of the [`index_to_function_calls`]
173        // pass.
174        CowBox::Borrowed(&simplify_output::index_intermediate_assigns::Transform),
175        // Remove locals of type `()` which show up a lot.
176        CowBox::Borrowed(&simplify_output::remove_unit_locals::Transform),
177        // Duplicate the return blocks
178        CowBox::Borrowed(&control_flow::duplicate_return::Transform),
179        // Remove the locals which are never used.
180        CowBox::Borrowed(&simplify_output::remove_unused_locals::Transform),
181        // Another round.
182        CowBox::Borrowed(&control_flow::merge_goto_chains::Transform),
183        // Filter the "dangling" blocks. Those might have been introduced by, for instance,
184        // [`merge_goto_chains`].
185        CowBox::Borrowed(&normalize::filter_unreachable_blocks::Transform),
186        // Make sure the block ids used in the ULLBC are consecutive
187        CowBox::Borrowed(&simplify_output::update_block_indices::Transform),
188    ]));
189    ctx.run_pass(pass);
190
191    if !options.ullbc {
192        // If we're reconstructing control-flow, print the ullbc here.
193        ctx.run_pass(Pass::NonBody(PrintCtxPass::new(
194            options.print_ullbc,
195            "# Final ULLBC before control-flow reconstruction".to_string(),
196        )));
197    }
198
199    if !options.ullbc {
200        // Go from ULLBC to LLBC (Low-Level Borrow Calculus) by reconstructing the control flow.
201        ctx.run_pass(mixed_body(&control_flow::ullbc_to_llbc::Transform));
202        // Body cleanup passes after control flow reconstruction.
203        let pass = Pass::FusedStructuredBody(Box::new([
204            // Reconstruct matches on enum variants.
205            resugar::reconstruct_matches::Transform::new(ctx),
206            // Cleanup the cfg.
207            CowBox::Borrowed(&control_flow::prettify_cfg::Transform),
208            // Replace some unops/binops and the array aggregates with
209            // function calls (introduces: ArrayToSlice, etc.)
210            CowBox::Borrowed(&simplify_output::ops_to_function_calls::Transform),
211            // Replace the arrays/slices index operations with function
212            // calls.
213            // (introduces: ArrayIndexShared, ArrayIndexMut, etc.)
214            CowBox::Borrowed(&simplify_output::index_to_function_calls::Transform),
215        ]));
216        ctx.run_pass(pass);
217    }
218    // Cleanup passes useful for both llbc and ullbc.
219    ctx.run_passes([
220        // Body passes may introduce fresh locals; make their storage markers explicit.
221        mixed_body(&finish_translation::insert_storage_statements::Transform),
222        // Change trait associated types to be type parameters instead. See the module for details.
223        // This also normalizes any use of an associated type that we can resolve.
224        global(&normalize::expand_associated_types::Transform),
225        // Remove the explicit `Self: Trait` clause of methods/assoc const declaration items if
226        // they're not used. This simplifies the graph of dependencies between definitions.
227        global(&simplify_output::remove_unused_clauses::Transform),
228        // `--remove-adt-clauses`: Remove all trait clauses from type declarations.
229        global(&simplify_output::remove_adt_clauses::Transform),
230        // Remove the locals which are never used.
231        mixed_body(&simplify_output::remove_unused_locals::Transform),
232        // Remove the useless `StatementKind::Nop`s.
233        mixed_body(&simplify_output::remove_nops::Transform),
234        // Take all the comments found in the original body and assign them to statements. This must be
235        // last after all the statement-affecting passes to avoid losing comments.
236        mixed_body(&add_missing_info::recover_body_comments::Transform),
237        // Hide the `A` type parameter on standard library containers (`Box`, `Vec`, etc).
238        global(&simplify_output::hide_allocator_param::Transform),
239        // Partially monomorphize items so that no item is ever instanciated with a mutable reference
240        // or a type containing one.
241        global(&normalize::partial_monomorphization::Transform),
242        // Reorder the graph of dependencies and compute the strictly connex components to:
243        // - compute the order in which to extract the definitions
244        // - find the recursive definitions
245        // - group the mutually recursive definitions
246        // This is done last to account for the final item graph, not the initial one.
247        global(&add_missing_info::reorder_decls::Transform),
248        // Check that types are still consistent after the transformation passes.
249        global(&typecheck_and_unify::Check::PostTransformation),
250        // Use `DeBruijnVar::Free` for the variables bound in item signatures.
251        mixed_body(&simplify_output::unbind_item_vars::Check),
252    ]);
253
254    if options.ullbc {
255        // If we're not reconstructing control-flow, print the ullbc after finalizing passes.
256        ctx.run_pass(Pass::NonBody(PrintCtxPass::new(
257            options.print_ullbc,
258            "# Final ULLBC before serialization".to_string(),
259        )));
260    } else {
261        ctx.run_pass(Pass::NonBody(PrintCtxPass::new(
262            options.print_llbc,
263            "# Final LLBC before serialization".to_string(),
264        )));
265    }
266}
267
268pub enum CowBox<T: ?Sized + 'static> {
269    Borrowed(&'static T),
270    Owned(Box<T>),
271}
272
273impl<T: ?Sized + 'static> std::ops::Deref for CowBox<T> {
274    type Target = T;
275    fn deref(&self) -> &Self::Target {
276        match self {
277            CowBox::Borrowed(x) => x,
278            CowBox::Owned(x) => x.as_ref(),
279        }
280    }
281}
282
283pub enum Pass {
284    NonBody(CowBox<dyn TransformPass>),
285    FusedUnstructuredBody(Box<[CowBox<dyn UllbcPass>]>),
286    FusedStructuredBody(Box<[CowBox<dyn LlbcPass>]>),
287}
288
289impl TransformCtx {
290    pub fn run_pass(&mut self, mut pass: Pass) {
291        match &mut pass {
292            Pass::NonBody(pass) => {
293                if pass.should_run(&self.options) {
294                    trace!("# Starting pass {}", pass.name());
295                    pass.transform_ctx(self)
296                }
297            }
298            Pass::FusedUnstructuredBody(passes) => {
299                // Some passes carry function bodies, which must also be transformed. This applies
300                // all the passes before pass `p` to the bodies potentially carried by pass `p`.
301                for i in 0..passes.len() {
302                    if let (first_passes, [pass, ..]) = passes.split_at_mut(i)
303                        && let CowBox::Owned(pass) = pass
304                    {
305                        pass.apply_preceding_passes(self, first_passes);
306                    }
307                }
308                self.for_each_item_mut(|ctx, mut item| {
309                    for pass in passes.iter() {
310                        if pass.should_run(&ctx.options) {
311                            trace!("# Starting pass {}", pass.name());
312                            pass.transform_item(ctx, item.reborrow());
313                        }
314                    }
315                });
316                for pass in passes.iter() {
317                    pass.finalize(self);
318                }
319            }
320            Pass::FusedStructuredBody(passes) => {
321                self.for_each_fun_decl(|ctx, decl| {
322                    for pass in passes.iter() {
323                        if pass.should_run(&ctx.options) {
324                            trace!("# Starting pass {}", pass.name());
325                            pass.transform_function(ctx, decl);
326                        }
327                    }
328                });
329            }
330        };
331    }
332    pub fn run_passes(&mut self, passes: impl IntoIterator<Item = Pass>) {
333        for pass in passes {
334            self.run_pass(pass);
335        }
336    }
337}
338
339pub struct PrintCtxPass {
340    pub message: String,
341    /// Whether we're printing to stdout or only logging.
342    pub to_stdout: bool,
343}
344
345impl PrintCtxPass {
346    pub fn new(to_stdout: bool, message: String) -> CowBox<dyn TransformPass> {
347        let ret = Self { message, to_stdout };
348        CowBox::Owned(Box::new(ret))
349    }
350}
351
352impl TransformPass for PrintCtxPass {
353    fn transform_ctx(&self, ctx: &mut TransformCtx) {
354        let message = &self.message;
355        if self.to_stdout {
356            println!("{message}:\n\n{ctx}\n");
357        } else {
358            trace!("{message}:\n\n{ctx}\n");
359        }
360    }
361}