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_ctx(&self, ctx: &mut TransformCtx<'_>) { ... }
fn name(&self) -> &str { ... }
fn log_before_body(
&self,
ctx: &TransformCtx<'_>,
name: &Name,
body: Result<&ExprBody, &Opaque>,
) { ... }
}
Expand description
A pass that modifies llbc bodies.
Provided Methods§
sourcefn transform_body(&self, _ctx: &mut TransformCtx<'_>, _body: &mut ExprBody)
fn transform_body(&self, _ctx: &mut TransformCtx<'_>, _body: &mut ExprBody)
Transform a body.
sourcefn transform_function(
&self,
ctx: &mut TransformCtx<'_>,
_decl: &mut FunDecl,
body: Result<&mut ExprBody, Opaque>,
)
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.
sourcefn transform_ctx(&self, ctx: &mut TransformCtx<'_>)
fn transform_ctx(&self, ctx: &mut TransformCtx<'_>)
Transform the given context. This forwards to the other methods by default.
sourcefn name(&self) -> &str
fn name(&self) -> &str
The name of the pass, used for debug logging. The default implementation uses the type name.
sourcefn log_before_body(
&self,
ctx: &TransformCtx<'_>,
name: &Name,
body: Result<&ExprBody, &Opaque>,
)
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_intermediate_assigns::Transform
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