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.raw_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) = &mut 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(FunId::Regular(*initializer)),
45                                gref.generics.clone(),
46                            )),
47                            args: vec![],
48                            dest: return_place.clone(),
49                        },
50                    ));
51                    *op = Operand::Move(return_place);
52                }
53            });
54            if !new_calls.is_empty() {
55                // Move the current block out of the way.
56                let block = mem::replace(&mut body.body[block_id], BlockData::new_unreachable());
57                let mut next_block = body.body.push(block);
58                // Each new block jumps to the previous one after completion
59                for (local_id, call) in new_calls {
60                    // Const eval mustn't unwind into runtime.
61                    let unwind = body.body.push(BlockData::new_unreachable());
62                    next_block = body.body.push(BlockData {
63                        statements: vec![Statement::new(
64                            Span::dummy(),
65                            StatementKind::StorageLive(local_id),
66                        )],
67                        terminator: Terminator::new(
68                            Span::dummy(),
69                            TerminatorKind::Call {
70                                call,
71                                target: next_block,
72                                on_unwind: unwind,
73                            },
74                        ),
75                    });
76                }
77                // Instead of the current block, start evaluating the new bodies.
78                body.body[block_id] = BlockData::new_goto(Span::dummy(), next_block);
79            }
80        }
81    }
82    fn finalize(&self, ctx: &mut TransformCtx) {
83        for gid in self.anon_consts.keys() {
84            ctx.translated.global_decls.remove(*gid);
85        }
86    }
87}
charon_lib/transform/simplify_output/anon_const_to_call.rs

charon_lib/transform/simplify_output/
anon_const_to_call.rs
