charon_lib/transform/normalize/
desugar_drops.rs

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

charon_lib/transform/normalize/
desugar_drops.rs
