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

charon_lib/transform/resugar/
reconstruct_box_derefs.rs
