Module transform

Source

Re-exports§

pub use ctx::TransformCtx;

Modules§

check_generics
Check that all supplied generic types match the corresponding generic parameters.
ctx
duplicate_defaulted_methods
Add missing methods to trait impls by duplicating the default method.
duplicate_return
The MIR uses a unique return node, which can be an issue when reconstructing the control-flow.
expand_associated_types
Change trait associated types to be type parameters instead. E.g.
filter_invisible_trait_impls
We cannot filter trait impls by name before translating them, because we need to know the trait/type pair that is being implemented. We therefore filter them in a post-processing pass.
filter_unreachable_blocks
Some passes like [reconstruct_assert] lead to the apparition of “dangling” blocks, which are referenced nowhere and thus become unreachable. This pass filters those out.
graphs
hide_marker_traits
index_intermediate_assigns
This micro-pass introduces intermediate assignments in preparation of [index_to_function_calls], so as to avoid borrow-checking errors.
index_to_function_calls
Desugar array/slice index operations to function calls.
inline_local_panic_functions
panic!() expands to:
insert_assign_return_unit
When the function’s return type is unit, the generated MIR doesn’t set the return value to (). This can be a concern: in the case of AENEAS, it means the return variable contains ⊥ upon returning. For this reason, when the function has return type unit, we insert an extra assignment just before returning.
insert_storage_lives
Add missing StorageLives – in MIR, some locals are considered “always” initialised, and have no StorageLive and StorageDead instructions associated; this always includes the arguments and the return value, but also sometimes includes other locals. We make sure these additional locals get initialised at the start of the function.
lift_associated_item_clauses
Move clauses on associated types to be parent clauses. The distinction is not semantically meaningful. We should ideally to this directly when translating but this is currently difficult; instead we do this as a post-processing pass.
merge_goto_chains
Micro-pass: merge single-origin gotos into their parent to reduce CFG graph size.
monomorphize
Micro-pass: monomorphize all functions and types; at the end of this pass, all functions and types are monomorphic.
ops_to_function_calls
Desugar some unary/binary operations and the array repeats to function calls. For instance, we desugar ArrayToSlice from an unop to a function call. This allows a more uniform treatment later on. TODO: actually transform all the unops and binops to function calls?
prettify_cfg
reconstruct_asserts
In the MIR AST, it seems assert are introduced to check preconditions (for the binops for example). The assert! introduced by the user introduce if ... then { panic!(...) } else { ...}. This pass introduces assert instead in order to make the code shorter.
reconstruct_boxes
Micro-pass: reconstruct piecewise box allocations using malloc and ShallowInitBox.
recover_body_comments
Take all the comments found in the original body and assign them to statements.
remove_arithmetic_overflow_checks
Micro-pass: remove the overflow checks for arithmetic operations we couldn’t remove in
remove_drop_never
The MIR code often contains variables with type ! that come from panic!s and similar !-returning` functions.
remove_dynamic_checks
Micro-pass: remove the dynamic checks for array/slice bounds, overflow, and division by zero.
remove_nops
Remove the useless no-ops.
remove_read_discriminant
The MIR code often contains variables with type Never, and we want to get rid of those. We proceed in two steps. First, we remove the instructions drop(v) where v has type Never (it can happen - this module does the filtering). Then, we filter the unused variables ([crate::remove_unused_locals]).
remove_unit_locals
remove_unused_locals
Remove the locals (which are not used for the input arguments) which are never used in the function bodies. This is useful to remove the locals with type Never. We actually check that there are no such local variables remaining afterwards.
remove_unused_methods
Remove the trait/impl methods that were not translated.
reorder_decls
Compute an ordering on declarations that:
simplify_constants
The MIR constant expressions lead to a lot of duplication: there are for instance constant ADTs which duplicate the “regular” aggregated ADTs in the operands, constant references, etc. This reduces the number of cases to handle and eases the function translation in Aeneas.
skip_trait_refs_when_known
ullbc_to_llbc
ULLBC to LLBC
unbind_item_vars
Replace variables bound at the top-level with Free vars. This is for convenience for consumers of the charon ast.
update_block_indices
Update the block indices to make sure they are consecutive
update_closure_signatures
Micro-pass: the first local variable of closures is (a borrow to) the closure itself. This is

Structs§

PrintCtxPass

Enums§

Pass

Statics§

FINAL_CLEANUP_PASSES
Final passes to run at the end, after pretty-printing the llbc if applicable. These are only split from the above list to get test outputs even when generics fail to match.
INITIAL_CLEANUP_PASSES
Item and type cleanup passes.
LLBC_PASSES
Body cleanup passes after control flow reconstruction.
SHARED_FINALIZING_PASSES
Cleanup passes useful for both llbc and ullbc.
ULLBC_PASSES
Body cleanup passes on the ullbc.