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

charon_driver/translate/
translate_functions.rs
