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 super::translate_ctx::*;
7use charon_lib::ast::ullbc_ast_utils::BodyBuilder;
8use charon_lib::ast::*;
9use charon_lib::ullbc_ast::*;
10use itertools::Itertools;
11
12impl ItemTransCtx<'_, '_> {
13    /// Generate a fake function body for ADT constructors.
14    pub(crate) fn build_ctor_body(
15        &mut self,
16        span: Span,
17        def: &hax::FullDef,
18    ) -> Result<Body, Error> {
19        let hax::FullDefKind::Ctor {
20            adt_def_id,
21            ctor_of,
22            variant_id,
23            fields,
24            output_ty,
25        } = def.kind()
26        else {
27            unreachable!()
28        };
29        let tref = self
30            .translate_type_decl_ref(span, &def.this().with_def_id(self.hax_state(), adt_def_id))?;
31        let output_ty = self.translate_ty(span, output_ty)?;
32
33        let mut builder = BodyBuilder::new(span, fields.len());
34        let return_place = builder.new_var(None, output_ty);
35        let args: Vec<_> = fields
36            .iter()
37            .map(|field| -> Result<Operand, Error> {
38                let ty = self.translate_ty(span, &field.ty)?;
39                let place = builder.new_var(None, ty);
40                Ok(Operand::Move(place))
41            })
42            .try_collect()?;
43        let variant = match ctor_of {
44            hax::CtorOf::Struct => None,
45            hax::CtorOf::Variant => Some(VariantId::from(*variant_id)),
46        };
47        builder.push_statement(StatementKind::Assign(
48            return_place,
49            Rvalue::Aggregate(AggregateKind::Adt(tref, variant, None), args),
50        ));
51        Ok(Body::Unstructured(builder.build()))
52    }
53
54    /// Checks whether the given id corresponds to a built-in type.
55    pub(crate) fn recognize_builtin_fun(
56        &mut self,
57        item: &hax::ItemRef,
58    ) -> Result<Option<BuiltinFunId>, Error> {
59        let def = self.hax_def(item)?;
60        let fun_id = if def.diagnostic_item.as_deref() == Some("box_new")
61            && self.t_ctx.options.treat_box_as_builtin
62        {
63            Some(BuiltinFunId::BoxNew)
64        } else {
65            None
66        };
67        Ok(fun_id)
68    }
69}
charon_driver/translate/translate_functions.rs

charon_driver/translate/
translate_functions.rs
