charon_lib/transform/simplify_output/
anon_const_to_call.rs

1use std::{collections::HashMap, mem};
2
3use crate::transform::CowBox;
4use crate::transform::{TransformCtx, ctx::UllbcPass};
5use crate::ullbc_ast::*;
6
7pub struct Transform {
8    anon_consts: HashMap<GlobalDeclId, FunDeclId>,
9}
10
11impl Transform {
12    pub fn new(ctx: &mut TransformCtx) -> CowBox<dyn UllbcPass> {
13        // Map each anon const id to its initializer.
14        let anon_consts = ctx
15            .translated
16            .global_decls
17            .iter()
18            .filter(|gdecl| matches!(gdecl.global_kind, GlobalKind::AnonConst))
19            .filter_map(|gdecl| Some((gdecl.def_id, gdecl.init_fun_id()?)))
20            .collect();
21        CowBox::Owned(Box::new(Transform { anon_consts }))
22    }
23}
24impl UllbcPass for Transform {
25    fn should_run(&self, options: &crate::options::TranslateOptions) -> bool {
26        options.inline_anon_consts && !self.anon_consts.is_empty()
27    }
28    fn transform_body(&self, _ctx: &mut TransformCtx, body: &mut ullbc_ast::ExprBody) {
29        for block_id in body.body.indices() {
30            let Some(block) = body.body.get_mut(block_id) else {
31                continue;
32            };
33            let mut new_calls: Vec<(LocalId, Call)> = vec![];
34            block.dyn_visit_in_body_mut(|op: &mut Operand| {
35                if let Operand::Const(c) = op
36                    && let ConstantExprKind::Global(gref) = c.kind()
37                    && let Some(initializer) = self.anon_consts.get(&gref.id)
38                {
39                    let return_place = body.locals.new_var(None, c.ty().clone());
40                    new_calls.push((
41                        return_place.as_local().unwrap(),
42                        Call {
43                            func: FnOperand::Regular(FnPtr::new(
44                                FnPtrKind::Fun(*initializer),
45                                gref.generics.clone(),
46                            )),
47                            args: vec![],
48                            dest: return_place.clone(),
49                            safety: CallSafety::Inherit,
50                        },
51                    ));
52                    *op = Operand::Move(return_place);
53                }
54            });
55            if !new_calls.is_empty() {
56                let is_cleanup = body.body[block_id].is_cleanup;
57                // Move the current block out of the way.
58                let block =
59                    mem::replace(&mut body.body[block_id], BlockData::new_unreachable(false));
60                let mut next_block = body.body.push(block);
61                // Each new block jumps to the previous one after completion
62                for (local_id, call) in new_calls {
63                    // Const eval mustn't unwind into runtime.
64                    let unwind = body.body.push(BlockData::new_unreachable(true));
65                    next_block = body.body.push(BlockData {
66                        statements: vec![Statement::new(
67                            Span::dummy(),
68                            StatementKind::StorageLive(local_id),
69                        )],
70                        terminator: Terminator::new(
71                            Span::dummy(),
72                            TerminatorKind::Call {
73                                call,
74                                target: next_block,
75                                on_unwind: unwind,
76                            },
77                        ),
78                        is_cleanup,
79                    });
80                }
81                // Instead of the current block, start evaluating the new bodies.
82                body.body[block_id] = BlockData::new_goto(Span::dummy(), next_block, is_cleanup);
83            }
84        }
85    }
86    fn finalize(&self, ctx: &mut TransformCtx) {
87        for gid in self.anon_consts.keys() {
88            ctx.translated.global_decls.remove(*gid);
89        }
90    }
91}
charon_lib/transform/simplify_output/anon_const_to_call.rs

charon_lib/transform/simplify_output/
anon_const_to_call.rs
