charon_lib/transform/simplify_output/
anon_const_to_call.rs

1use std::collections::HashMap;
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 kind = body.body[block_id].kind;
57                // Move the current block out of the way.
58                let block = body.body[block_id].take();
59                let mut next_block = body.body.push(block);
60                // Each new block jumps to the previous one after completion
61                for (local_id, call) in new_calls {
62                    // Const eval mustn't unwind into runtime.
63                    let unwind = body
64                        .body
65                        .push(BlockData::new_unreachable(kind.further_unwind_kind()));
66                    next_block = body.body.push(BlockData {
67                        statements: vec![Statement::new(
68                            Span::dummy(),
69                            StatementKind::StorageLive(local_id),
70                        )],
71                        terminator: Terminator::new(
72                            Span::dummy(),
73                            TerminatorKind::Call {
74                                call,
75                                target: next_block,
76                                on_unwind: unwind,
77                            },
78                        ),
79                        kind,
80                    });
81                }
82                // Instead of the current block, start evaluating the new bodies.
83                body.body[block_id] = BlockData::new_goto(Span::dummy(), next_block, kind);
84            }
85        }
86    }
87    fn finalize(&self, ctx: &mut TransformCtx) {
88        for gid in self.anon_consts.keys() {
89            ctx.translated.global_decls.remove(*gid);
90        }
91    }
92}
charon_lib/transform/simplify_output/anon_const_to_call.rs

charon_lib/transform/simplify_output/
anon_const_to_call.rs
