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 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        let mut locals = Locals {
111            arg_count: fields.len(),
112            locals: Vector::new(),
113        };
114        locals.new_var(None, output_ty);
115        let args: Vec<_> = fields
116            .iter()
117            .map(|field| -> Result<Operand, Error> {
118                let ty = self.translate_ty(span, &field.ty)?;
119                let place = locals.new_var(None, ty);
120                Ok(Operand::Move(place))
121            })
122            .try_collect()?;
123        let variant = match ctor_of {
124            hax::CtorOf::Struct => None,
125            hax::CtorOf::Variant => Some(VariantId::from(variant_id)),
126        };
127        let st_kind = StatementKind::Assign(
128            locals.return_place(),
129            Rvalue::Aggregate(AggregateKind::Adt(tref, variant, None), args),
130        );
131        let statement = Statement::new(span, st_kind);
132        let block = BlockData {
133            statements: vec![statement],
134            terminator: Terminator::new(span, TerminatorKind::Return),
135        };
136        let body = Body::Unstructured(GExprBody {
137            span,
138            locals,
139            comments: Default::default(),
140            body: [block].into_iter().collect(),
141        });
142        Ok(body)
143    }
144
145    /// Checks whether the given id corresponds to a built-in type.
146    pub(crate) fn recognize_builtin_fun(
147        &mut self,
148        item: &hax::ItemRef,
149    ) -> Result<Option<BuiltinFunId>, Error> {
150        let def = self.hax_def(item)?;
151        let fun_id =
152            if def.diagnostic_item.as_deref() == Some("box_new") && !self.t_ctx.options.raw_boxes {
153                Some(BuiltinFunId::BoxNew)
154            } else {
155                None
156            };
157        Ok(fun_id)
158    }
159}
charon_driver/translate/translate_functions.rs

charon_driver/translate/
translate_functions.rs
