charon_lib/transform/
reconstruct_boxes.rs

1//! # Micro-pass: reconstruct piecewise box allocations using `malloc` and `ShallowInitBox`.
2use crate::register_error;
3use crate::transform::TransformCtx;
4use crate::ullbc_ast::*;
5
6use super::ctx::UllbcPass;
7
8pub struct Transform;
9
10impl Transform {
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)`.
24    fn update_statements(
25        locals: &mut Locals,
26        seq: &mut [Statement],
27    ) -> Vec<(usize, Vec<Statement>)> {
28        let seq_len = seq.len();
29        if let [Statement {
30            content: RawStatement::Assign(size, Rvalue::NullaryOp(NullOp::SizeOf, _)),
31            ..
32        }, Statement {
33            content: RawStatement::Assign(align, Rvalue::NullaryOp(NullOp::AlignOf, _)),
34            ..
35        }, Statement {
36            content: RawStatement::Call(call_malloc),
37            ..
38        }, Statement {
39            content: RawStatement::StorageLive(target_var),
40            ..
41        }, Statement {
42            content:
43                RawStatement::Assign(box_make, Rvalue::ShallowInitBox(Operand::Move(alloc_use), _)),
44            ..
45        }, rest @ ..] = seq
46        {
47            let prefix_len = seq_len - rest.len();
48            // TODO: once we have a system to recognize intrinsics, check the call is to exchange_malloc.
49            if let [Operand::Move(arg0), Operand::Move(arg1)] = call_malloc.args.as_slice()
50                && arg0 == size
51                && arg1 == align
52                && call_malloc.dest == *alloc_use
53                && let target_var = *target_var
54                && box_make.is_local()
55                && box_make.local_id() == target_var
56                && let TyKind::Adt(TypeId::Builtin(BuiltinTy::Box), generics) =
57                    locals[target_var].ty.kind()
58            {
59                // Find the assignment into the box.
60                for i in 0..rest.len() {
61                    if let Statement {
62                        content: RawStatement::Assign(box_deref, val),
63                        ..
64                    } = &mut rest[i]
65                        && let Some((sub, ProjectionElem::Deref)) = box_deref.as_projection()
66                        && sub == box_make
67                    {
68                        let real_i = prefix_len + i;
69                        let mut to_insert = Vec::new();
70                        let dest = box_make.clone();
71                        let val = val.clone();
72                        let generics = generics.clone();
73                        seq[0].content = RawStatement::Nop;
74                        seq[1].content = RawStatement::Nop;
75                        seq[2].content = RawStatement::Nop;
76                        seq[4].content = RawStatement::Nop;
77                        let val = match val {
78                            Rvalue::Use(op) => op,
79                            _ => {
80                                // We need to create a new variable to store the value.
81                                let name = locals[target_var].name.clone();
82                                let ty = generics.types[0].clone();
83                                let var = locals.new_var(name, ty);
84                                let st = Statement::new(
85                                    seq[real_i].span,
86                                    RawStatement::Assign(var.clone(), val),
87                                );
88                                to_insert.push((real_i, vec![st]));
89                                Operand::Move(var)
90                            }
91                        };
92                        seq[real_i].content = RawStatement::Call(Call {
93                            func: FnOperand::Regular(FnPtr {
94                                func: FunIdOrTraitMethodRef::Fun(FunId::Builtin(
95                                    BuiltinFunId::BoxNew,
96                                )),
97                                generics,
98                            }),
99                            args: vec![val],
100                            dest,
101                        });
102                        return to_insert;
103                    }
104                }
105            }
106        }
107        Vec::new()
108    }
109}
110
111impl UllbcPass for Transform {
112    fn transform_body(&self, ctx: &mut TransformCtx, b: &mut ExprBody) {
113        for block in &mut b.body {
114            block.transform_sequences(|seq| Transform::update_statements(&mut b.locals, seq));
115        }
116
117        // Make sure we got all the `ShallowInitBox`es.
118        b.body.dyn_visit_in_body(|rvalue: &Rvalue| {
119            if rvalue.is_shallow_init_box() {
120                register_error!(
121                    ctx,
122                    b.span,
123                    "Could not reconstruct `Box` initialization; \
124                    branching during `Box` initialization is not supported."
125                );
126            }
127        });
128    }
129}
charon_lib/transform/reconstruct_boxes.rs

charon_lib/transform/
reconstruct_boxes.rs
