Trait LlbcPass

pub trait LlbcPass: Sync {
    // Provided methods
    fn transform_body(&self, _ctx: &mut TransformCtx<'_>, _body: &mut ExprBody) { ... }
    fn transform_function(
        &self,
        ctx: &mut TransformCtx<'_>,
        _decl: &mut FunDecl,
        body: Result<&mut ExprBody, Opaque>,
    ) { ... }
    fn transform_global(
        &self,
        ctx: &mut TransformCtx<'_>,
        _decl: &mut GlobalDecl,
        body: Result<&mut ExprBody, Opaque>,
    ) { ... }
    fn transform_ctx(&self, ctx: &mut TransformCtx<'_>) { ... }
    fn name(&self) -> &str { ... }
    fn log_before_body(
        &self,
        ctx: &TransformCtx<'_>,
        name: &Name,
        body: Result<&ExprBody, &Opaque>,
    ) { ... }
}

A pass that modifies llbc bodies.

Provided Methods

fn transform_body(&self, _ctx: &mut TransformCtx<'_>, _body: &mut ExprBody)

Transform a body.

fn transform_function( &self, ctx: &mut TransformCtx<'_>, _decl: &mut FunDecl, body: Result<&mut ExprBody, Opaque>, )

Transform a function declaration. This forwards to transform_body by default.

fn transform_global( &self, ctx: &mut TransformCtx<'_>, _decl: &mut GlobalDecl, body: Result<&mut ExprBody, Opaque>, )

Transform a global declaration. This forwards to transform_body by default.

fn transform_ctx(&self, ctx: &mut TransformCtx<'_>)

Transform the given context. This forwards to the other methods by default.

fn name(&self) -> &str

The name of the pass, used for debug logging. The default implementation uses the type name.

fn log_before_body( &self, ctx: &TransformCtx<'_>, name: &Name, body: Result<&ExprBody, &Opaque>, )

Log that the pass is about to be run on this body.

Implementors

impl LlbcPass for charon_lib::transform::index_to_function_calls::Transform

We do the following.

If p is a projection (for instance: var, *var, var.f, etc.), we detect:

• whether it operates on a slice or an array (we keep track of the types)
• whether the access might mutate the value or not (it is the case if it is in a move, &mut or at the lhs of an assignment), and do the following transformations

  // If array and mutable access:
  ... p[i] ...
     ~~>
  tmp0 = &mut p
  tmp1 = ArrayIndexMut(move p, i)
  ... *tmp1 ...

  // If array and non-mutable access:
  ... p[i] ...
     ~~>
  tmp0 := & p
  tmp1 := ArrayIndexShared(move tmp0, i)
  ... *tmp1 ...

  // Omitting the slice cases, which are similar

For instance, it leads to the following transformations:

  // x : [u32; N]
  y : u32 = copy x[i]
     ~~>
  tmp0 : & [u32; N] := &x
  tmp1 : &u32 = ArrayIndexShared(move tmp0, i)
  y : u32 = copy (*tmp1)

  // x : &[T; N]
  y : &T = & (*x)[i]
     ~~>
  tmp0 : & [T; N] := & (*x)
  tmp1 : &T = ArrayIndexShared(move tmp0, i)
  y : &T = & (*tmp1)

  // x : [u32; N]
  y = &mut x[i]
     ~~>
  tmp0 : &mut [u32; N] := &mut x
  tmp1 : &mut u32 := ArrayIndexMut(move tmp0, i)
  y = &mut (*tmp)

  // When using an index on the lhs:
  // y : [T; N]
  y[i] = x
     ~~>
  tmp0 : &mut [T; N] := &mut y;
  tmp1 : &mut T = ArrayIndexMut(move y, i)
  *tmp1 = x

impl LlbcPass for charon_lib::transform::inline_local_panic_functions::Transform

impl LlbcPass for charon_lib::transform::insert_assign_return_unit::Transform

impl LlbcPass for charon_lib::transform::prettify_cfg::Transform

impl LlbcPass for charon_lib::transform::reconstruct_asserts::Transform

impl LlbcPass for charon_lib::transform::recover_body_comments::Transform

impl LlbcPass for charon_lib::transform::remove_drop_never::Transform

impl LlbcPass for charon_lib::transform::remove_nops::Transform

impl LlbcPass for charon_lib::transform::remove_read_discriminant::Transform

impl LlbcPass for charon_lib::transform::remove_unused_locals::Transform