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