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

charon_lib/transform/resugar/
reconstruct_boxes.rs
