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

charon_driver/translate/
translate_functions.rs
