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 rustc_span::sym;
8
9use super::translate_ctx::*;
10use charon_lib::ast::*;
11
12impl<'tcx> ItemTransCtx<'tcx, '_> {
13    /// Checks whether the given id corresponds to a built-in type.
14    pub(crate) fn recognize_builtin_fun(
15        &mut self,
16        item: &hax::ItemRef,
17    ) -> Result<Option<BuiltinFunId>, Error> {
18        let def = self.hax_def(item)?;
19        let fun_id = if def.diagnostic_item == Some(sym::box_new)
20            && self.t_ctx.options.treat_box_as_builtin
21        {
22            Some(BuiltinFunId::BoxNew)
23        } else {
24            None
25        };
26        Ok(fun_id)
27    }
28
29    /// Translate the names of the arguments of this definition, if they are available,
30    /// otherwise naming arguments `arg0`, `arg1`, etc.
31    /// Note that the names of the arguments are not always available, even when
32    /// we can retrieve the MIR body, in which case we also fall back to `argN`.
33    pub fn translate_argument_names(
34        &mut self,
35        span: Span,
36        def: &hax::FullDef<'tcx>,
37        n_args: usize,
38    ) -> Vec<Option<String>> {
39        let Ok(Some(body)) = self.get_mir(def.this(), span) else {
40            return vec![None; n_args];
41        };
42        body.local_decls
43            .iter_enumerated()
44            .skip(1)
45            .take(body.arg_count)
46            .map(|(index, _)| hax::name_of_local(index, &body.var_debug_info))
47            .collect()
48    }
49}
charon_driver/translate/translate_functions.rs

charon_driver/translate/
translate_functions.rs
