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 std::panic;
7
8use super::translate_ctx::*;
9use charon_lib::ast::ullbc_ast_utils::BodyBuilder;
10use charon_lib::ast::*;
11use charon_lib::common::*;
12use charon_lib::formatter::IntoFormatter;
13use charon_lib::pretty::FmtWithCtx;
14use charon_lib::ullbc_ast::*;
15use itertools::Itertools;
16
17impl ItemTransCtx<'_, '_> {
18    /// Translate a function's signature, and initialize a body translation context
19    /// at the same time - the function signature gives us the list of region and
20    /// type parameters, that we put in the translation context.
21    pub(crate) fn translate_function_signature(
22        &mut self,
23        def: &hax::FullDef,
24        item_meta: &ItemMeta,
25    ) -> Result<FunSig, Error> {
26        let span = item_meta.span;
27
28        self.translate_def_generics(span, def)?;
29
30        let signature = match &def.kind {
31            hax::FullDefKind::Fn { sig, .. } => sig,
32            hax::FullDefKind::AssocFn { sig, .. } => sig,
33            hax::FullDefKind::Ctor {
34                fields, output_ty, ..
35            } => {
36                let sig = hax::TyFnSig {
37                    inputs: fields.iter().map(|field| field.ty.clone()).collect(),
38                    output: output_ty.clone(),
39                    c_variadic: false,
40                    safety: hax::Safety::Safe,
41                    abi: hax::ExternAbi::Rust,
42                };
43                &hax::Binder {
44                    value: sig,
45                    bound_vars: Default::default(),
46                }
47            }
48            hax::FullDefKind::Const { ty, .. }
49            | hax::FullDefKind::AssocConst { ty, .. }
50            | hax::FullDefKind::Static { ty, .. } => {
51                let sig = hax::TyFnSig {
52                    inputs: vec![],
53                    output: ty.clone(),
54                    c_variadic: false,
55                    safety: hax::Safety::Safe,
56                    abi: hax::ExternAbi::Rust,
57                };
58                &hax::Binder {
59                    value: sig,
60                    bound_vars: Default::default(),
61                }
62            }
63            _ => panic!("Unexpected definition for function: {def:?}"),
64        };
65
66        // Translate the signature
67        trace!("signature of {:?}:\n{:?}", def.def_id(), signature.value);
68        let inputs: Vec<Ty> = signature
69            .value
70            .inputs
71            .iter()
72            .map(|ty| self.translate_ty(span, ty))
73            .try_collect()?;
74        let output = self.translate_ty(span, &signature.value.output)?;
75
76        let fmt_ctx = &self.into_fmt();
77        trace!(
78            "# Input variables types:\n{}",
79            pretty_display_list(|x| x.to_string_with_ctx(fmt_ctx), &inputs)
80        );
81        trace!("# Output variable type:\n{}", output.with_ctx(fmt_ctx));
82
83        let is_unsafe = match signature.value.safety {
84            hax::Safety::Unsafe => true,
85            hax::Safety::Safe => false,
86        };
87
88        Ok(FunSig {
89            generics: self.the_only_binder().params.clone(),
90            is_unsafe,
91            inputs,
92            output,
93        })
94    }
95
96    /// Generate a fake function body for ADT constructors.
97    pub(crate) fn build_ctor_body(
98        &mut self,
99        span: Span,
100        def: &hax::FullDef,
101        adt_def_id: &hax::DefId,
102        ctor_of: &hax::CtorOf,
103        variant_id: usize,
104        fields: &hax::IndexVec<hax::FieldIdx, hax::FieldDef>,
105        output_ty: &hax::Ty,
106    ) -> Result<Body, Error> {
107        let tref = self
108            .translate_type_decl_ref(span, &def.this().with_def_id(self.hax_state(), adt_def_id))?;
109        let output_ty = self.translate_ty(span, output_ty)?;
110
111        let mut builder = BodyBuilder::new(span, fields.len());
112        let return_place = builder.new_var(None, output_ty);
113        let args: Vec<_> = fields
114            .iter()
115            .map(|field| -> Result<Operand, Error> {
116                let ty = self.translate_ty(span, &field.ty)?;
117                let place = builder.new_var(None, ty);
118                Ok(Operand::Move(place))
119            })
120            .try_collect()?;
121        let variant = match ctor_of {
122            hax::CtorOf::Struct => None,
123            hax::CtorOf::Variant => Some(VariantId::from(variant_id)),
124        };
125        builder.push_statement(StatementKind::Assign(
126            return_place,
127            Rvalue::Aggregate(AggregateKind::Adt(tref, variant, None), args),
128        ));
129        Ok(Body::Unstructured(builder.build()))
130    }
131
132    /// Checks whether the given id corresponds to a built-in type.
133    pub(crate) fn recognize_builtin_fun(
134        &mut self,
135        item: &hax::ItemRef,
136    ) -> Result<Option<BuiltinFunId>, Error> {
137        let def = self.hax_def(item)?;
138        let fun_id =
139            if def.diagnostic_item.as_deref() == Some("box_new") && !self.t_ctx.options.raw_boxes {
140                Some(BuiltinFunId::BoxNew)
141            } else {
142                None
143            };
144        Ok(fun_id)
145    }
146}
charon_driver/translate/translate_functions.rs

charon_driver/translate/
translate_functions.rs
