pub trait UllbcPass: Sync {
// Provided methods
fn transform_body(&self, _ctx: &mut TransformCtx, _body: &mut ExprBody) { ... }
fn transform_function(&self, ctx: &mut TransformCtx, decl: &mut FunDecl) { ... }
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 ullbc 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)
fn transform_function(&self, ctx: &mut TransformCtx, decl: &mut FunDecl)
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 UllbcPass for charon_lib::transform::control_flow::duplicate_return::Transform
impl UllbcPass for charon_lib::transform::control_flow::merge_goto_chains::Transform
impl UllbcPass for charon_lib::transform::finish_translation::insert_assign_return_unit::Transform
impl UllbcPass for charon_lib::transform::finish_translation::insert_ptr_metadata::Transform
This pass computes the metadata for Rvalue, which is used to create references and raw pointers. E.g., in cases like:
let x = &[mut] (*some_v).field;
If the (*some_v).field
is a DST, like [i32]
, we will need to fetch the metadata, i.e., the length of the slice,
and store it in a local variable, then we have:
let x = Rvalue::Ref { place:(*some_v).field, kind: [mut], ptr_metadata: PtrMetadata(some_v) };
There should be a new local variable introduced to store PtrMetadata(some_v)
.
impl UllbcPass for charon_lib::transform::normalize::filter_unreachable_blocks::Transform
impl UllbcPass for charon_lib::transform::normalize::skip_trait_refs_when_known::Transform
impl UllbcPass for charon_lib::transform::normalize::transform_dyn_trait_calls::Transform
impl UllbcPass for charon_lib::transform::resugar::inline_local_panic_functions::Transform
impl UllbcPass for charon_lib::transform::resugar::reconstruct_asserts::Transform
impl UllbcPass for charon_lib::transform::resugar::reconstruct_boxes::Transform
The special alloc::boxed::box_new(x)
intrinsic becomes the following:
@2 := size_of<i32>
@3 := align_of<i32>
@4 := alloc::alloc::exchange_malloc(move (@2), move (@3))
storage_live(@5)
@5 := shallow_init_box::<i32>(move (@4))
// possibly some intermediate statements
*(@5) := x
We reconstruct this into a call to Box::new(x)
.