charon_driver/translate/
translate_functions.rs

1//! Translate functions from the rust compiler MIR to our internal representation.
2//! Our internal representation is very close to MIR, but is more convenient for
3//! us to handle, and easier to maintain - rustc's representation can evolve
4//! independently.
5
6use crate::hax;
7use itertools::Itertools;
8use rustc_span::sym;
9
10use super::translate_bodies::translate_variant_id;
11use super::translate_ctx::*;
12use charon_lib::ast::ullbc_ast_utils::BodyBuilder;
13use charon_lib::ast::*;
14use charon_lib::ullbc_ast::*;
15
16impl ItemTransCtx<'_, '_> {
17    /// Generate a fake function body for ADT constructors.
18    pub(crate) fn build_ctor_body(
19        &mut self,
20        span: Span,
21        def: &hax::FullDef,
22    ) -> Result<Body, Error> {
23        let hax::FullDefKind::Ctor {
24            adt_def_id,
25            ctor_of,
26            variant_id,
27            fields,
28            output_ty,
29        } = def.kind()
30        else {
31            unreachable!()
32        };
33        let tref = self
34            .translate_type_decl_ref(span, &def.this().with_def_id(self.hax_state(), adt_def_id))?;
35        let output_ty = self.translate_ty(span, output_ty)?;
36
37        let mut builder = BodyBuilder::new(span, fields.len());
38        let return_place = builder.new_var(None, output_ty);
39        let args: Vec<_> = fields
40            .iter()
41            .map(|field| -> Result<Operand, Error> {
42                let ty = self.translate_ty(span, &field.ty)?;
43                let place = builder.new_var(None, ty);
44                Ok(Operand::Move(place))
45            })
46            .try_collect()?;
47        let variant = match ctor_of {
48            hax::CtorOf::Struct => None,
49            hax::CtorOf::Variant => Some(translate_variant_id(*variant_id)),
50        };
51        builder.push_statement(StatementKind::Assign(
52            return_place,
53            Rvalue::Aggregate(AggregateKind::Adt(tref, variant, None), args),
54        ));
55        Ok(Body::Unstructured(builder.build()))
56    }
57
58    /// Checks whether the given id corresponds to a built-in type.
59    pub(crate) fn recognize_builtin_fun(
60        &mut self,
61        item: &hax::ItemRef,
62    ) -> Result<Option<BuiltinFunId>, Error> {
63        let def = self.hax_def(item)?;
64        let fun_id = if def.diagnostic_item == Some(sym::box_new)
65            && self.t_ctx.options.treat_box_as_builtin
66        {
67            Some(BuiltinFunId::BoxNew)
68        } else {
69            None
70        };
71        Ok(fun_id)
72    }
73
74    /// Translate the names of the arguments of this definition, if they are available,
75    /// otherwise naming arguments `arg0`, `arg1`, etc.
76    /// Note that the names of the arguments are not always available, even when
77    /// we can retrieve the MIR body, in which case we also fall back to `argN`.
78    pub fn translate_argument_names(
79        &mut self,
80        span: Span,
81        def: &hax::FullDef,
82        n_args: usize,
83    ) -> Vec<Option<String>> {
84        let Ok(Some(body)) = self.get_mir(def.this(), span) else {
85            return vec![None; n_args];
86        };
87        body.local_decls
88            .iter_enumerated()
89            .skip(1)
90            .take(body.arg_count)
91            .map(|(index, _)| hax::name_of_local(index, &body.var_debug_info))
92            .collect()
93    }
94}
charon_driver/translate/translate_functions.rs

charon_driver/translate/
translate_functions.rs
