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.
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.
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.
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.
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.
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.
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.
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.