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::{
8 TransformCtx,
9 ctx::{BodyTransformCtx, UllbcPass},
10};
11use crate::ullbc_ast::*;
12
13pub struct Transform;
14
15impl UllbcPass for Transform {
16 fn transform_function(&self, ctx: &mut TransformCtx, decl: &mut FunDecl) {
17 decl.transform_ullbc_statements(ctx, |ctx, st: &mut Statement| {
18 st.dyn_visit_in_body_mut(|x: &mut Rvalue| {
19 if let Rvalue::Ref {
20 place,
21 ptr_metadata,
22 ..
23 }
24 | Rvalue::RawPtr {
25 place,
26 ptr_metadata,
27 ..
28 } = x
29 {
30 *ptr_metadata = ctx.compute_place_metadata(place);
31 }
32 });
33 })
34 }
35}