charon_lib/transform/finish_translation/
insert_ptr_metadata.rs

1use crate::transform::TransformCtx;
2use crate::transform::ctx::BodyTransformCtx;
3use crate::{transform::ctx::UllbcPass, ullbc_ast::*};
4
5pub struct Transform;
6
7/// This pass computes the metadata for Rvalue, which is used to create references and raw pointers.
8/// E.g., in cases like:
9/// ```ignore
10/// let x = &[mut] (*some_v).field;
11/// ```
12/// If the `(*some_v).field` is a DST, like `[i32]`, we will need to fetch the metadata, i.e., the length of the slice,
13/// and store it in a local variable, then we have:
14/// ```ignore
15/// let x = Rvalue::Ref { place:(*some_v).field, kind: [mut], ptr_metadata: PtrMetadata(some_v) };
16/// ```
17/// There should be a new local variable introduced to store `PtrMetadata(some_v)`.
18impl UllbcPass for Transform {
19    fn transform_function(&self, ctx: &mut TransformCtx, decl: &mut FunDecl) {
20        decl.transform_ullbc_statements(ctx, |ctx, st: &mut Statement| {
21            st.dyn_visit_in_body_mut(|x: &mut Rvalue| {
22                if let Rvalue::Ref {
23                    place,
24                    ptr_metadata,
25                    ..
26                }
27                | Rvalue::RawPtr {
28                    place,
29                    ptr_metadata,
30                    ..
31                } = x
32                {
33                    *ptr_metadata = ctx.compute_place_metadata(place);
34                }
35            });
36        })
37    }
38}

charon_lib/transform/finish_translation/insert_ptr_metadata.rs

charon_lib/transform/finish_translation/
insert_ptr_metadata.rs