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::Static { ty, .. } => {
52                let sig = hax::TyFnSig {
53                    inputs: vec![],
54                    output: ty.clone(),
55                    c_variadic: false,
56                    safety: hax::Safety::Safe,
57                    abi: hax::ExternAbi::Rust,
58                };
59                &hax::Binder {
60                    value: sig,
61                    bound_vars: Default::default(),
62                }
63            }
64            _ => panic!("Unexpected definition for function: {def:?}"),
65        };
66
67        // Translate the signature
68        trace!("signature of {:?}:\n{:?}", def.def_id(), signature.value);
69        let inputs: Vec<Ty> = signature
70            .value
71            .inputs
72            .iter()
73            .map(|ty| self.translate_ty(span, ty))
74            .try_collect()?;
75        let output = self.translate_ty(span, &signature.value.output)?;
76
77        let fmt_ctx = &self.into_fmt();
78        trace!(
79            "# Input variables types:\n{}",
80            pretty_display_list(|x| x.to_string_with_ctx(fmt_ctx), &inputs)
81        );
82        trace!("# Output variable type:\n{}", output.with_ctx(fmt_ctx));
83
84        let is_unsafe = match signature.value.safety {
85            hax::Safety::Unsafe => true,
86            hax::Safety::Safe => false,
87        };
88
89        Ok(FunSig {
90            generics: self.the_only_binder().params.clone(),
91            is_unsafe,
92            inputs,
93            output,
94        })
95    }
96
97    /// Generate a fake function body for ADT constructors.
98    pub(crate) fn build_ctor_body(
99        &mut self,
100        span: Span,
101        def: &hax::FullDef,
102        adt_def_id: &hax::DefId,
103        ctor_of: &hax::CtorOf,
104        variant_id: usize,
105        fields: &hax::IndexVec<hax::FieldIdx, hax::FieldDef>,
106        output_ty: &hax::Ty,
107    ) -> Result<Body, Error> {
108        let tref = self
109            .translate_type_decl_ref(span, &def.this().with_def_id(self.hax_state(), adt_def_id))?;
110        let output_ty = self.translate_ty(span, output_ty)?;
111        let mut locals = Locals {
112            arg_count: fields.len(),
113            locals: Vector::new(),
114        };
115        locals.new_var(None, output_ty);
116        let args: Vec<_> = fields
117            .iter()
118            .map(|field| {
119                let ty = self.translate_ty(span, &field.ty)?;
120                let place = locals.new_var(None, ty);
121                Ok(Operand::Move(place))
122            })
123            .try_collect()?;
124        let variant = match ctor_of {
125            hax::CtorOf::Struct => None,
126            hax::CtorOf::Variant => Some(VariantId::from(variant_id)),
127        };
128        let st_kind = RawStatement::Assign(
129            locals.return_place(),
130            Rvalue::Aggregate(AggregateKind::Adt(tref, variant, None), args),
131        );
132        let statement = Statement::new(span, st_kind);
133        let block = BlockData {
134            statements: vec![statement],
135            terminator: Terminator::new(span, RawTerminator::Return),
136        };
137        let body = Body::Unstructured(GExprBody {
138            span,
139            locals,
140            comments: Default::default(),
141            body: [block].into_iter().collect(),
142        });
143        Ok(body)
144    }
145
146    /// Checks whether the given id corresponds to a built-in type.
147    pub(crate) fn recognize_builtin_fun(
148        &mut self,
149        item: &hax::ItemRef,
150    ) -> Result<Option<BuiltinFunId>, Error> {
151        let def = self.hax_def(item)?;
152        let fun_id =
153            if def.diagnostic_item.as_deref() == Some("box_new") && !self.t_ctx.options.raw_boxes {
154                Some(BuiltinFunId::BoxNew)
155            } else {
156                None
157            };
158        Ok(fun_id)
159    }
160}
charon_driver/translate/translate_functions.rs

charon_driver/translate/
translate_functions.rs
