charon_lib/transform/normalize/
desugar_drops.rs

1use crate::{
2    transform::{
3        TransformCtx,
4        ctx::{BodyTransformCtx, UllbcPass, UllbcStatementTransformCtx},
5    },
6    ullbc_ast::*,
7};
8
9fn is_noop_destruct(glue: &FnPtr) -> bool {
10    match glue.kind.as_ref() {
11        FnPtrKind::Trait(tref, _) => matches!(
12            &tref.kind,
13            TraitRefKind::BuiltinOrAuto {
14                builtin_data: BuiltinImplData::NoopDestruct,
15                ..
16            }
17        ),
18        _ => false,
19    }
20}
21
22impl<'a> UllbcStatementTransformCtx<'a> {
23    /// Transform a Drop to a Call that calls the drop_glue method.
24    /// If we cannot desugar this drop, we just leave it unchanged.
25    fn transform_drop_to_call(&mut self, term: &mut Terminator) {
26        if let TerminatorKind::Drop {
27            kind: DropKind::Precise,
28            place,
29            fn_ptr,
30            target,
31            on_unwind,
32        } = &mut term.kind
33        {
34            // check if this drop is noop
35            if is_noop_destruct(fn_ptr) {
36                term.kind = TerminatorKind::Goto { target: *target };
37                return;
38            }
39
40            // assign `&mut place` to a new variable
41            let drop_arg =
42                self.borrow_to_new_var(place.clone(), BorrowKind::Mut, Some("drop_arg".into()));
43
44            let drop_ret = self.fresh_var(Some("drop_ret".into()), Ty::mk_unit());
45            let call = Call {
46                func: FnOperand::Regular(fn_ptr.clone()),
47                args: Vec::from([Operand::Move(drop_arg)]),
48                dest: drop_ret,
49            };
50            term.kind = TerminatorKind::Call {
51                call,
52                target: *target,
53                on_unwind: *on_unwind,
54            };
55        }
56    }
57}
58
59pub struct Transform;
60
61impl UllbcPass for Transform {
62    fn should_run(&self, options: &crate::options::TranslateOptions) -> bool {
63        options.desugar_drops
64    }
65    fn transform_function(&self, ctx: &mut TransformCtx, decl: &mut FunDecl) {
66        decl.transform_ullbc_terminators(ctx, |ctx, term| {
67            ctx.transform_drop_to_call(term);
68        });
69    }
70}
charon_lib/transform/normalize/desugar_drops.rs

charon_lib/transform/normalize/
desugar_drops.rs
