charon_lib/transform/resugar/
reconstruct_box_derefs.rs

1//! Resugar the box derefs that got desugared in elaborated MIR.
2//!
3//! In elaborated MIR, box derefs become actual accesses to the contained raw pointer. Under
4//! `--treat-box-as-builtin`, we convert these back to derefs on the box.
5use std::ops::ControlFlow;
6
7use crate::transform::TransformCtx;
8use crate::transform::ctx::UllbcPass;
9use crate::ullbc_ast::*;
10
11pub struct Transform;
12
13/// Look for
14/// ```ignore
15/// transmute::<Unique<T>, *const T>(copy (*b))
16/// transmute::<NonNull<T>, *const T>(copy (*b).0)
17/// ```
18/// Returns `*b`
19fn box_pointee_pointer_assignment(rvalue: &Rvalue) -> Option<Place> {
20    let Rvalue::UnaryOp(UnOp::Cast(CastKind::Transmute(raw_ptr_ty)), Operand::Copy(hidden_pointer)) =
21        &rvalue
22    else {
23        return None;
24    };
25    let unique_place = match hidden_pointer.as_projection()? {
26        (field_base, ProjectionElem::Field(_, FieldId::ZERO)) => field_base,
27        _ => hidden_pointer,
28    };
29    let (box_place, ProjectionElem::Deref) = unique_place.as_projection()? else {
30        return None;
31    };
32    let TyKind::Adt(tref) = box_place.ty().kind() else {
33        return None;
34    };
35    if !tref.is_box() {
36        return None;
37    }
38    let box_generics = &tref.generics;
39    if &box_generics.types[0] != raw_ptr_ty.as_raw_ptr()?.0 {
40        return None;
41    }
42    Some(box_place.clone().deref())
43}
44
45#[derive(Default)]
46struct LocalStatus {
47    /// Whether that local is the target of the special `transmute` statement we're looking for.
48    /// Stores the `*b` where `b` is the Box.
49    box_pointee_assignment: Option<(StmtLoc, Place)>,
50    /// Whether that local is the target of more than one such special `transmute`.
51    ambiguous: bool,
52    /// Whether that local is ever used outside of a deref projection (apart from the initial
53    /// assignment).
54    used_outside_derefs: bool,
55}
56
57impl LocalStatus {
58    fn rewritable_box_pointee(&self) -> Option<&(StmtLoc, Place)> {
59        if self.ambiguous || self.used_outside_derefs {
60            return None;
61        }
62        self.box_pointee_assignment.as_ref()
63    }
64}
65
66struct LocalStatusCollector {
67    local_status: IndexVec<LocalId, LocalStatus>,
68    current_statement: Option<StmtLoc>,
69}
70
71impl Visitor for LocalStatusCollector {
72    type Break = std::convert::Infallible;
73}
74
75impl VisitBody for LocalStatusCollector {
76    fn visit_place(&mut self, place: &Place) -> ControlFlow<Self::Break> {
77        match &place.kind {
78            // Skip uses of a local where the last projection is a deref.
79            PlaceKind::Projection(subplace, pj) if subplace.is_local() && pj.is_deref() => {
80                return ControlFlow::Continue(());
81            }
82            // This didn't get caught by the branch above, so it's an invalid use.
83            PlaceKind::Local(local) => self.local_status[*local].used_outside_derefs = true,
84            _ => {}
85        }
86        self.visit_inner(place)
87    }
88
89    fn visit_ullbc_statement(&mut self, st: &ullbc_ast::Statement) -> ControlFlow<Self::Break> {
90        if let StatementKind::Assign(dst, rvalue) = &st.kind
91            && let Some(local) = dst.as_local()
92            && let Some(box_pointee) = box_pointee_pointer_assignment(rvalue)
93        {
94            let status = &mut self.local_status[local];
95            if status.box_pointee_assignment.is_some() {
96                status.ambiguous = true;
97            } else {
98                let loc = self.current_statement.unwrap();
99                status.box_pointee_assignment = Some((loc, box_pointee));
100            }
101            // Ignore the assignment destination: this initialization is the one non-deref
102            // interaction allowed for the temporary pointer.
103            self.visit(rvalue)
104        } else {
105            self.visit_inner(st)
106        }
107    }
108}
109
110fn collect_local_status(body: &ExprBody) -> IndexVec<LocalId, LocalStatus> {
111    let mut collector = LocalStatusCollector {
112        local_status: body.locals.locals.map_ref(|_| Default::default()),
113        current_statement: None,
114    };
115    for (block, block_data) in body.body.iter_enumerated() {
116        for (statement, st) in block_data.statements.iter().enumerate() {
117            collector.current_statement = Some(StmtLoc::new(block, statement));
118            let _ = collector.visit(st);
119        }
120        collector.current_statement = None;
121        let _ = collector.visit(&block_data.terminator);
122    }
123    collector.local_status
124}
125
126fn rewrite_place(place: &mut Place, local_status: &IndexVec<LocalId, LocalStatus>) {
127    let Some((subplace, projection)) = place.as_projection() else {
128        return;
129    };
130    if projection == &ProjectionElem::Deref
131        && let Some(local) = subplace.as_local()
132        && let Some((_, box_pointee)) = local_status[local].rewritable_box_pointee()
133    {
134        *place = box_pointee.clone();
135        return;
136    }
137
138    let PlaceKind::Projection(subplace, _) = &mut place.kind else {
139        unreachable!();
140    };
141    rewrite_place(subplace, local_status);
142}
143
144impl UllbcPass for Transform {
145    fn should_run(&self, options: &crate::options::TranslateOptions) -> bool {
146        options.treat_box_as_builtin
147    }
148
149    fn transform_body(&self, _ctx: &mut TransformCtx, body: &mut ExprBody) {
150        let local_status = collect_local_status(body);
151
152        body.body.dyn_visit_in_body_mut(|place: &mut Place| {
153            rewrite_place(place, &local_status);
154        });
155
156        for status in local_status {
157            if let Some((assign_loc, _)) = status.rewritable_box_pointee() {
158                body[*assign_loc].kind = StatementKind::Nop;
159            }
160        }
161    }
162}
charon_lib/transform/resugar/reconstruct_box_derefs.rs

charon_lib/transform/resugar/
reconstruct_box_derefs.rs
