charon_lib/transform/finish_translation/
insert_ptr_metadata.rs

1/// We leave dummy values for pointer metadata during translation; instead we add it in this pass.
2///
3/// The reason to keep this as a pass is that `compute_place_metadata` indirectly queries the whole
4/// crate to figure out the metadata, which we can't do during translation as some items may not be
5/// translated yet. We could fetch some of that info via hax but this would then duplicate the
6/// metadata computation code because it involves non-hax things like emitting new statements.
7use crate::transform::TransformCtx;
8use crate::transform::ctx::BodyTransformCtx;
9use crate::{transform::ctx::UllbcPass, ullbc_ast::*};
10
11pub struct Transform;
12
13impl UllbcPass for Transform {
14    fn transform_function(&self, ctx: &mut TransformCtx, decl: &mut FunDecl) {
15        decl.transform_ullbc_statements(ctx, |ctx, st: &mut Statement| {
16            st.dyn_visit_in_body_mut(|x: &mut Rvalue| {
17                if let Rvalue::Ref {
18                    place,
19                    ptr_metadata,
20                    ..
21                }
22                | Rvalue::RawPtr {
23                    place,
24                    ptr_metadata,
25                    ..
26                } = x
27                {
28                    *ptr_metadata = ctx.compute_place_metadata(place);
29                }
30            });
31        })
32    }
33}