charon_lib/transform/resugar/
reconstruct_boxes.rs

1//! # Micro-pass: reconstruct piecewise box allocations using `malloc` and `ShallowInitBox`.
2
3use crate::register_error;
4use crate::transform::TransformCtx;
5use crate::ullbc_ast::*;
6
7use crate::transform::ctx::UllbcPass;
8
9pub struct Transform;
10
11/// The special `alloc::boxed::box_new(x)` intrinsic becomes the following:
12///
13/// ```text
14/// @2 := size_of<i32>
15/// @3 := align_of<i32>
16/// @4 := alloc::alloc::exchange_malloc(move (@2), move (@3))
17/// storage_live(@5)
18/// @5 := shallow_init_box::<i32>(move (@4))
19/// // possibly some intermediate statements
20/// *(@5) := x
21/// ```
22///
23/// We reconstruct this into a call to `Box::new(x)`.
24impl UllbcPass for Transform {
25    fn transform_body(&self, ctx: &mut TransformCtx, b: &mut ExprBody) {
26        if ctx.options.raw_boxes {
27            return;
28        }
29
30        // We need to find a block that has exchange_malloc as the following terminator:
31        // ```text
32        // @4 := alloc::alloc::exchange_malloc(move (@2), move (@3))
33        // ```
34        // We then chekc that that this block ends with two assignments:
35        // ```text
36        // @2 := size_of<i32>
37        // @3 := align_of<i32>
38        // ```
39        // If that is the case, we look at the target block and check that it starts with`
40        // ```text
41        // storage_live(@5)
42        // @5 := shallow_init_box::<i32>(move (@4))
43        // ```
44        // We then look for the assignment into the box and take a not of its index.
45        // ```text
46        // *(@5) := x
47        // ```
48        // Finally, we replace all these assignments with a call to `@5 = Box::new(x)`
49        // We do so by replacing the terminator (exchange_malloc) with the correct call
50        // and replacing the assignment @3 := align_of<i32> with the storage live.
51        // Everything else becomes Nop.
52
53        for candidate_block_idx in b.body.all_indices() {
54            let second_block;
55            let at_5;
56            let at_5_ty;
57            let box_generics;
58            let value_to_write;
59            let old_assign_idx;
60            let assign_span;
61            let unwind_target;
62
63            if let Some(candidate_block) = b.body.get(candidate_block_idx)
64                // If the terminator is a call
65                && let TerminatorKind::Call {
66                    target: target_block_idx,
67                    call:
68                        Call {
69                            args: malloc_args,
70                            func: _, // TODO: once we have a system to recognize intrinsics, check the call is to exchange_malloc.
71                            dest: malloc_dest,
72                        },
73                        on_unwind,
74                } = &candidate_block.terminator.kind
75                // The call has two move arguments
76                && let [Operand::Move(arg0), Operand::Move(arg1)] = malloc_args.as_slice()
77                && let [ .., Statement {
78                            kind: StatementKind::Assign(size, Rvalue::NullaryOp(NullOp::SizeOf, _)),
79                            ..
80                        }, Statement {
81                            kind: StatementKind::Assign(align, Rvalue::NullaryOp(NullOp::AlignOf, _)),
82                            ..
83                        }] = candidate_block.statements.as_slice()
84                && arg0 == size && arg1 == align
85                && let Some(target_block) = b.body.get(*target_block_idx)
86                && let [Statement {
87                            kind: StatementKind::StorageLive(target_var),
88                            ..
89                        }, Statement {
90                            kind:
91                                StatementKind::Assign(box_make, Rvalue::ShallowInitBox(Operand::Move(alloc_use), _)),
92                            ..
93                        }, rest @ ..] = target_block.statements.as_slice()
94                && alloc_use == malloc_dest
95                && let Some(local_id) = box_make.as_local()
96                && local_id == *target_var
97                && let TyKind::Adt(ty_ref) = b.locals[*target_var].ty.kind()
98                && let TypeId::Builtin(BuiltinTy::Box) = ty_ref.id
99                && let Some((assign_idx_in_rest, val, span)) = rest.iter().enumerate().find_map(|(idx, st)| {
100                    if let Statement {
101                            kind: StatementKind::Assign(box_deref, val),
102                            span,
103                            ..
104                        } = st
105                        && let Some((sub, ProjectionElem::Deref)) = box_deref.as_projection()
106                        && sub == box_make
107                    {
108                        Some((idx, val, span))
109                    } else {
110                        None
111                    }
112                })
113            {
114                at_5 = local_id;
115                at_5_ty = box_make.ty().clone();
116                old_assign_idx = assign_idx_in_rest + 2; // +2 because rest skips the first two statements
117                value_to_write = val.clone();
118                box_generics = ty_ref.generics.clone();
119                second_block = *target_block_idx;
120                assign_span = *span;
121                unwind_target = *on_unwind;
122            } else {
123                continue;
124            }
125
126            let first_block = b.body.get_mut(candidate_block_idx).unwrap();
127            // Remove the `size_of` and `align_of` assignments.
128            first_block.statements.pop();
129            first_block.statements.pop();
130            let value_to_write = match value_to_write {
131                Rvalue::Use(op) => op,
132                _ => {
133                    // We need to create a new variable to store the value.
134                    let name = b.locals[at_5].name.clone();
135                    let ty = box_generics.types[0].clone();
136                    let var = b.locals.new_var(name, ty);
137                    first_block.statements.push(Statement::new(
138                        assign_span,
139                        StatementKind::StorageLive(var.as_local().unwrap()),
140                    ));
141                    first_block.statements.push(Statement::new(
142                        assign_span,
143                        StatementKind::Assign(var.clone(), value_to_write),
144                    ));
145                    Operand::Move(var)
146                }
147            };
148            first_block.statements.push(Statement::new(
149                assign_span,
150                StatementKind::StorageLive(at_5),
151            ));
152            first_block.terminator.kind = TerminatorKind::Call {
153                call: Call {
154                    func: FnOperand::Regular(FnPtr {
155                        kind: Box::new(FnPtrKind::Fun(FunId::Builtin(BuiltinFunId::BoxNew))),
156                        generics: box_generics,
157                    }),
158                    args: vec![value_to_write],
159                    dest: Place::new(at_5, at_5_ty),
160                },
161                target: second_block,
162                on_unwind: unwind_target,
163            };
164
165            // We now update the statements in the second block.
166            let second_block = b.body.get_mut(second_block).unwrap();
167            second_block.statements.get_mut(0).unwrap().kind = StatementKind::Nop;
168            second_block.statements.get_mut(1).unwrap().kind = StatementKind::Nop;
169            second_block
170                .statements
171                .get_mut(old_assign_idx)
172                .unwrap()
173                .kind = StatementKind::Nop;
174        }
175
176        // Make sure we got all the `ShallowInitBox`es.
177        b.body.dyn_visit_in_body(|rvalue: &Rvalue| {
178            if rvalue.is_shallow_init_box() {
179                register_error!(
180                    ctx,
181                    b.span,
182                    "Could not reconstruct `Box` initialization; \
183                    branching during `Box` initialization is not supported."
184                );
185            }
186        });
187    }
188}