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}