charon_lib

Module transform

source

Re-exports§

Modules§

  • check_generics
    Check that all supplied generic types match the corresponding generic parameters.
  • ctx
  • 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.
  • 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.
  • 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.
  • 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 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_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_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.
  • reorder_decls
  • 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.
  • ullbc_to_llbc
    ULLBC to LLBC
  • 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

Enums§

Statics§