charon_lib/transform/mod.rs
1pub mod check_generics;
2pub mod ctx;
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 duplicate_defaulted_methods;
8 pub mod filter_invisible_trait_impls;
9 pub mod insert_assign_return_unit;
10 pub mod insert_ptr_metadata;
11 pub mod insert_storage_lives;
12 pub mod remove_unused_methods;
13}
14
15/// Passes that compute extra info to be stored in the crate.
16pub mod add_missing_info {
17 pub mod compute_short_names;
18 pub mod recover_body_comments;
19 pub mod reorder_decls;
20 pub mod sccs;
21}
22
23/// Passes that effect some kind of normalization on the crate.
24pub mod normalize {
25 pub mod expand_associated_types;
26 pub mod filter_unreachable_blocks;
27 pub mod skip_trait_refs_when_known;
28 pub mod transform_dyn_trait_calls;
29}
30
31/// Passes that undo some lowering done by rustc to recover an operation closer to what the user
32/// wrote.
33pub mod resugar {
34 pub mod inline_local_panic_functions;
35 pub mod reconstruct_asserts;
36 pub mod reconstruct_boxes;
37 pub mod reconstruct_fallible_operations;
38 pub mod reconstruct_matches;
39}
40
41/// Passes that make the output simpler/easier to consume.
42pub mod simplify_output {
43 pub mod hide_allocator_param;
44 pub mod hide_marker_traits;
45 pub mod index_intermediate_assigns;
46 pub mod index_to_function_calls;
47 pub mod inline_promoted_consts;
48 pub mod lift_associated_item_clauses;
49 pub mod ops_to_function_calls;
50 pub mod remove_nops;
51 pub mod remove_unit_locals;
52 pub mod remove_unused_locals;
53 pub mod remove_unused_self_clause;
54 pub mod simplify_constants;
55 pub mod unbind_item_vars;
56 pub mod update_block_indices;
57}
58
59/// Passes that manipulate the control flow and reconstruct its structure.
60pub mod control_flow {
61 pub mod duplicate_return;
62 pub mod merge_goto_chains;
63 pub mod prettify_cfg;
64 pub mod ullbc_to_llbc;
65}
66
67use Pass::*;
68pub use ctx::TransformCtx;
69use ctx::{LlbcPass, TransformPass, UllbcPass};
70
71/// Item and type cleanup passes.
72pub static INITIAL_CLEANUP_PASSES: &[Pass] = &[
73 // Compute short names. We do it early to make pretty-printed output more legible in traces.
74 NonBody(&add_missing_info::compute_short_names::Transform),
75 // Check that translation emitted consistent generics.
76 NonBody(&check_generics::Check("after translation")),
77 // # Micro-pass: filter the trait impls that were marked invisible since we couldn't filter
78 // them out earlier.
79 NonBody(&finish_translation::filter_invisible_trait_impls::Transform),
80 // Remove the trait/impl methods that were not translated (because not used).
81 NonBody(&finish_translation::remove_unused_methods::Transform),
82 // Add missing methods to trait impls by duplicating the default method.
83 NonBody(&finish_translation::duplicate_defaulted_methods::Transform),
84 // Compute the metadata & insert for Rvalue
85 UnstructuredBody(&finish_translation::insert_ptr_metadata::Transform),
86 // # Micro-pass: add the missing assignments to the return value.
87 // When the function return type is unit, the generated MIR doesn't
88 // set the return value to `()`. This can be a concern: in the case
89 // of Aeneas, it means the return variable contains ⊥ upon returning.
90 // For this reason, when the function has return type unit, we insert
91 // an extra assignment just before returning.
92 UnstructuredBody(&finish_translation::insert_assign_return_unit::Transform),
93 // Insert `StorageLive` for locals that don't have one (that's allowed in MIR).
94 NonBody(&finish_translation::insert_storage_lives::Transform),
95 // Move clauses on associated types to be parent clauses
96 NonBody(&simplify_output::lift_associated_item_clauses::Transform),
97 // # Micro-pass: hide some overly-common traits we don't need: Sized, Sync, Allocator, etc..
98 NonBody(&simplify_output::hide_marker_traits::Transform),
99 // Hide the `A` type parameter on standard library containers (`Box`, `Vec`, etc).
100 NonBody(&simplify_output::hide_allocator_param::Transform),
101 // # Micro-pass: remove the explicit `Self: Trait` clause of methods/assoc const declaration
102 // items if they're not used. This simplifies the graph of dependencies between definitions.
103 NonBody(&simplify_output::remove_unused_self_clause::Transform),
104 // # Micro-pass: whenever we reference a trait method on a known type, refer to the method
105 // `FunDecl` directly instead of going via a `TraitRef`. This is done before `reorder_decls` to
106 // remove some sources of mutual recursion.
107 NonBody(&normalize::skip_trait_refs_when_known::Transform),
108 // Transform dyn trait method calls to vtable function pointer calls
109 // This should be early to handle the calls before other transformations
110 UnstructuredBody(&normalize::transform_dyn_trait_calls::Transform),
111 // Change trait associated types to be type parameters instead. See the module for details.
112 // This also normalizes any use of an associated type that we can resolve.
113 NonBody(&normalize::expand_associated_types::Transform),
114];
115
116/// Body cleanup passes on the ullbc.
117pub static ULLBC_PASSES: &[Pass] = &[
118 // Inline promoted consts into their parent bodies.
119 UnstructuredBody(&simplify_output::inline_promoted_consts::Transform),
120 // # Micro-pass: merge single-origin gotos into their parent. This drastically reduces the
121 // graph size of the CFG.
122 // This must be done early as some resugaring passes depend on it.
123 UnstructuredBody(&control_flow::merge_goto_chains::Transform),
124 // # Micro-pass: Remove overflow/div-by-zero/bounds checks since they are already part of the
125 // arithmetic/array operation in the semantics of (U)LLBC.
126 // **WARNING**: this pass uses the fact that the dynamic checks introduced by Rustc use a
127 // special "assert" construct. Because of this, it must happen *before* the
128 // [reconstruct_asserts] pass. See the comments in [crate::remove_dynamic_checks].
129 // **WARNING**: this pass relies on a precise structure of the MIR statements. Because of this,
130 // it must happen before passes that insert statements like [simplify_constants].
131 UnstructuredBody(&resugar::reconstruct_fallible_operations::Transform),
132 // # Micro-pass: reconstruct the special `Box::new` operations inserted e.g. in the `vec![]`
133 // macro.
134 // **WARNING**: this pass relies on a precise structure of the MIR statements. Because of this,
135 // it must happen before passes that insert statements like [simplify_constants].
136 // **WARNING**: this pass works across calls, hence must happen after `merge_goto_chains`,
137 UnstructuredBody(&resugar::reconstruct_boxes::Transform),
138 // # Micro-pass: reconstruct the asserts
139 UnstructuredBody(&resugar::reconstruct_asserts::Transform),
140 // # Micro-pass: `panic!()` expands to a new function definition each time. This pass cleans
141 // those up.
142 UnstructuredBody(&resugar::inline_local_panic_functions::Transform),
143 // # Micro-pass: desugar the constants to other values/operands as much
144 // as possible.
145 UnstructuredBody(&simplify_output::simplify_constants::Transform),
146 // # Micro-pass: introduce intermediate assignments in preparation of the
147 // [`index_to_function_calls`] pass.
148 UnstructuredBody(&simplify_output::index_intermediate_assigns::Transform),
149 // # Micro-pass: remove locals of type `()` which show up a lot.
150 UnstructuredBody(&simplify_output::remove_unit_locals::Transform),
151 // # Micro-pass: duplicate the return blocks
152 UnstructuredBody(&control_flow::duplicate_return::Transform),
153 // # Micro-pass: filter the "dangling" blocks. Those might have been introduced by,
154 // for instance, [`reconstruct_asserts`].
155 UnstructuredBody(&normalize::filter_unreachable_blocks::Transform),
156 // # Micro-pass: make sure the block ids used in the ULLBC are consecutive
157 UnstructuredBody(&simplify_output::update_block_indices::Transform),
158];
159
160/// Body cleanup passes after control flow reconstruction.
161pub static LLBC_PASSES: &[Pass] = &[
162 // # Go from ULLBC to LLBC (Low-Level Borrow Calculus) by reconstructing the control flow.
163 NonBody(&control_flow::ullbc_to_llbc::Transform),
164 // Reconstruct matches on enum variants.
165 StructuredBody(&resugar::reconstruct_matches::Transform),
166 // Cleanup the cfg.
167 StructuredBody(&control_flow::prettify_cfg::Transform),
168 // # Micro-pass: replace some unops/binops and the array aggregates with
169 // function calls (introduces: ArrayToSlice, etc.)
170 StructuredBody(&simplify_output::ops_to_function_calls::Transform),
171 // # Micro-pass: replace the arrays/slices index operations with function
172 // calls.
173 // (introduces: ArrayIndexShared, ArrayIndexMut, etc.)
174 StructuredBody(&simplify_output::index_to_function_calls::Transform),
175];
176
177/// Cleanup passes useful for both llbc and ullbc.
178pub static SHARED_FINALIZING_PASSES: &[Pass] = &[
179 // # Micro-pass: remove the locals which are never used.
180 NonBody(&simplify_output::remove_unused_locals::Transform),
181 // # Micro-pass: remove the useless `StatementKind::Nop`s.
182 NonBody(&simplify_output::remove_nops::Transform),
183 // # Micro-pass: take all the comments found in the original body and assign them to
184 // statements. This must be last after all the statement-affecting passes to avoid losing
185 // comments.
186 NonBody(&add_missing_info::recover_body_comments::Transform),
187 // # Reorder the graph of dependencies and compute the strictly connex components to:
188 // - compute the order in which to extract the definitions
189 // - find the recursive definitions
190 // - group the mutually recursive definitions
191 // This is done last to account for the final item graph, not the initial one.
192 NonBody(&add_missing_info::reorder_decls::Transform),
193];
194
195/// Final passes to run at the end, after pretty-printing the llbc if applicable. These are only
196/// split from the above list to get test outputs even when generics fail to match.
197pub static FINAL_CLEANUP_PASSES: &[Pass] = &[
198 // Check that all supplied generic types match the corresponding generic parameters.
199 // Check that generics are still consistent after the transformation passes.
200 NonBody(&check_generics::Check("after transformations")),
201 // Use `DeBruijnVar::Free` for the variables bound in item signatures.
202 NonBody(&simplify_output::unbind_item_vars::Check),
203];
204
205#[derive(Clone, Copy)]
206pub enum Pass {
207 NonBody(&'static dyn TransformPass),
208 UnstructuredBody(&'static dyn UllbcPass),
209 StructuredBody(&'static dyn LlbcPass),
210}
211
212impl Pass {
213 pub fn run(self, ctx: &mut TransformCtx) {
214 match self {
215 NonBody(pass) => pass.transform_ctx(ctx),
216 UnstructuredBody(pass) => pass.transform_ctx(ctx),
217 StructuredBody(pass) => pass.transform_ctx(ctx),
218 }
219 }
220
221 pub fn name(&self) -> &str {
222 match self {
223 NonBody(pass) => pass.name(),
224 UnstructuredBody(pass) => pass.name(),
225 StructuredBody(pass) => pass.name(),
226 }
227 }
228}
229
230pub struct PrintCtxPass {
231 pub message: String,
232 /// Whether we're printing to stdout or only logging.
233 pub to_stdout: bool,
234}
235
236impl PrintCtxPass {
237 pub fn new(to_stdout: bool, message: String) -> &'static Self {
238 let ret = Self { message, to_stdout };
239 Box::leak(Box::new(ret))
240 }
241}
242
243impl TransformPass for PrintCtxPass {
244 fn transform_ctx(&self, ctx: &mut TransformCtx) {
245 let message = &self.message;
246 if self.to_stdout {
247 println!("{message}:\n\n{ctx}\n");
248 } else {
249 trace!("{message}:\n\n{ctx}\n");
250 }
251 }
252}