Check that all supplied generic types match the corresponding generic parameters.
Add missing methods to trait impls by duplicating the default method.
The MIR uses a unique return node, which can be an issue when reconstructing
the control-flow.
Change trait associated types to be type parameters instead. E.g.
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.
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.
This micro-pass introduces intermediate assignments in preparation of
[index_to_function_calls], so as to avoid borrow-checking errors.
Desugar array/slice index operations to function calls.
panic!() expands to:
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.
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.
Micro-pass: merge single-origin gotos into their parent to reduce CFG graph size.
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?
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.
Micro-pass: reconstruct piecewise box allocations using malloc and ShallowInitBox.
Take all the comments found in the original body and assign them to statements.
Micro-pass: remove the overflow checks for arithmetic operations we couldn’t remove in
The MIR code often contains variables with type ! that come from panic!s and similar
!-returning` functions.
Micro-pass: remove the dynamic checks for array/slice bounds, overflow, and division by zero.
Remove the useless no-ops.
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 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 the trait/impl methods that were not translated.
Compute an ordering on declarations that:
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.
ULLBC to LLBC
Replace variables bound at the top-level with Free vars. This is for convenience for
consumers of the charon ast.
Update the block indices to make sure they are consecutive
Micro-pass: the first local variable of closures is (a borrow to) the closure itself. This is