charon_driver/translate/
translate_functions_to_ullbc.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 crate::translate::translate_bodies::BodyTransCtx;
9
10use super::translate_ctx::*;
11use charon_lib::ast::*;
12use charon_lib::common::*;
13use charon_lib::formatter::{Formatter, IntoFormatter};
14use charon_lib::ids::Vector;
15use charon_lib::ullbc_ast::*;
16use hax_frontend_exporter as hax;
17use itertools::Itertools;
18
19impl ItemTransCtx<'_, '_> {
20    pub(crate) fn get_item_kind(
21        &mut self,
22        span: Span,
23        def: &hax::FullDef,
24    ) -> Result<ItemKind, Error> {
25        let assoc = match def.kind() {
26            hax::FullDefKind::AssocTy {
27                associated_item, ..
28            }
29            | hax::FullDefKind::AssocConst {
30                associated_item, ..
31            }
32            | hax::FullDefKind::AssocFn {
33                associated_item, ..
34            } => associated_item,
35            _ => return Ok(ItemKind::Regular),
36        };
37        Ok(match &assoc.container {
38            // E.g.:
39            // ```
40            // impl<T> List<T> {
41            //   fn new() -> Self { ... } <- inherent method
42            // }
43            // ```
44            hax::AssocItemContainer::InherentImplContainer { .. } => ItemKind::Regular,
45            // E.g.:
46            // ```
47            // impl Foo for Bar {
48            //   fn baz(...) { ... } // <- implementation of a trait method
49            // }
50            // ```
51            hax::AssocItemContainer::TraitImplContainer {
52                impl_id,
53                impl_generics,
54                impl_required_impl_exprs,
55                implemented_trait_ref,
56                implemented_trait_item,
57                overrides_default,
58                ..
59            } => {
60                let impl_id = self.register_trait_impl_id(span, impl_id);
61                let impl_ref = TraitImplRef {
62                    impl_id,
63                    generics: Box::new(self.translate_generic_args(
64                        span,
65                        impl_generics,
66                        impl_required_impl_exprs,
67                        None,
68                        GenericsSource::item(impl_id),
69                    )?),
70                };
71                let trait_ref = self.translate_trait_ref(span, implemented_trait_ref)?;
72                if matches!(def.kind(), hax::FullDefKind::AssocFn { .. }) {
73                    // Ensure we translate the corresponding decl signature.
74                    // FIXME(self_clause): also ensure we translate associated globals
75                    // consistently; to do once we have clearer `Self` clause handling.
76                    let _ = self.register_fun_decl_id(span, implemented_trait_item);
77                }
78                ItemKind::TraitImpl {
79                    impl_ref,
80                    trait_ref,
81                    item_name: TraitItemName(assoc.name.clone()),
82                    reuses_default: !overrides_default,
83                }
84            }
85            // This method is the *declaration* of a trait item
86            // E.g.:
87            // ```
88            // trait Foo {
89            //   fn baz(...); // <- declaration of a trait method
90            // }
91            // ```
92            hax::AssocItemContainer::TraitContainer { trait_ref, .. } => {
93                // The trait id should be Some(...): trait markers (that we may eliminate)
94                // don't have associated items.
95                let trait_ref = self.translate_trait_ref(span, trait_ref)?;
96                let item_name = TraitItemName(assoc.name.clone());
97                ItemKind::TraitDecl {
98                    trait_ref,
99                    item_name,
100                    has_default: assoc.has_value,
101                }
102            }
103        })
104    }
105
106    /// Translate a function's signature, and initialize a body translation context
107    /// at the same time - the function signature gives us the list of region and
108    /// type parameters, that we put in the translation context.
109    fn translate_function_signature(
110        &mut self,
111        def: &hax::FullDef,
112        item_meta: &ItemMeta,
113    ) -> Result<FunSig, Error> {
114        let span = item_meta.span;
115
116        self.translate_def_generics(span, def)?;
117
118        let signature = match &def.kind {
119            hax::FullDefKind::Closure { args, .. } => &args.tupled_sig,
120            hax::FullDefKind::Fn { sig, .. } => sig,
121            hax::FullDefKind::AssocFn { sig, .. } => sig,
122            hax::FullDefKind::Ctor {
123                fields, output_ty, ..
124            } => {
125                let sig = hax::TyFnSig {
126                    inputs: fields.iter().map(|field| field.ty.clone()).collect(),
127                    output: output_ty.clone(),
128                    c_variadic: false,
129                    safety: hax::Safety::Safe,
130                    abi: hax::ExternAbi::Rust,
131                };
132                &hax::Binder {
133                    value: sig,
134                    bound_vars: Default::default(),
135                }
136            }
137            hax::FullDefKind::Const { ty, .. }
138            | hax::FullDefKind::AssocConst { ty, .. }
139            | hax::FullDefKind::AnonConst { ty, .. }
140            | hax::FullDefKind::InlineConst { ty, .. }
141            | hax::FullDefKind::PromotedConst { ty, .. }
142            | hax::FullDefKind::Static { ty, .. } => {
143                let sig = hax::TyFnSig {
144                    inputs: vec![],
145                    output: ty.clone(),
146                    c_variadic: false,
147                    safety: hax::Safety::Safe,
148                    abi: hax::ExternAbi::Rust,
149                };
150                &hax::Binder {
151                    value: sig,
152                    bound_vars: Default::default(),
153                }
154            }
155            _ => panic!("Unexpected definition for function: {def:?}"),
156        };
157
158        // Translate the signature
159        trace!("signature of {:?}:\n{:?}", def.def_id, signature.value);
160        let mut inputs: Vec<Ty> = signature
161            .value
162            .inputs
163            .iter()
164            .map(|ty| self.translate_ty(span, ty))
165            .try_collect()?;
166        let output = self.translate_ty(span, &signature.value.output)?;
167
168        let fmt_ctx = self.into_fmt();
169        trace!(
170            "# Input variables types:\n{}",
171            pretty_display_list(|x| fmt_ctx.format_object(x), &inputs)
172        );
173        trace!(
174            "# Output variable type:\n{}",
175            fmt_ctx.format_object(&output)
176        );
177
178        let is_unsafe = match signature.value.safety {
179            hax::Safety::Unsafe => true,
180            hax::Safety::Safe => false,
181        };
182
183        let closure_info = match &def.kind {
184            hax::FullDefKind::Closure { args, .. } => {
185                let kind = match args.kind {
186                    hax::ClosureKind::Fn => ClosureKind::Fn,
187                    hax::ClosureKind::FnMut => ClosureKind::FnMut,
188                    hax::ClosureKind::FnOnce => ClosureKind::FnOnce,
189                };
190
191                assert_eq!(inputs.len(), 1);
192                let tuple_arg = inputs.pop().unwrap();
193
194                let state: Vector<TypeVarId, Ty> = args
195                    .upvar_tys
196                    .iter()
197                    .map(|ty| self.translate_ty(span, &ty))
198                    .try_collect()?;
199                // Add the state of the closure as first parameter.
200                let state_ty = {
201                    // Group the state types into a tuple
202                    let state_ty =
203                        TyKind::Adt(TypeId::Tuple, GenericArgs::new_for_builtin(state.clone()))
204                            .into_ty();
205                    // Depending on the kind of the closure, add a reference
206                    match &kind {
207                        ClosureKind::FnOnce => state_ty,
208                        ClosureKind::Fn | ClosureKind::FnMut => {
209                            let rid = self
210                                .innermost_generics_mut()
211                                .regions
212                                .push_with(|index| RegionVar { index, name: None });
213                            let r = Region::Var(DeBruijnVar::new_at_zero(rid));
214                            let mutability = if kind == ClosureKind::Fn {
215                                RefKind::Shared
216                            } else {
217                                RefKind::Mut
218                            };
219                            TyKind::Ref(r, state_ty, mutability).into_ty()
220                        }
221                    }
222                };
223                inputs.push(state_ty);
224
225                // Unpack the tupled arguments to match the body locals.
226                let TyKind::Adt(TypeId::Tuple, tuple_args) = tuple_arg.kind() else {
227                    raise_error!(self, span, "Closure argument is not a tuple")
228                };
229                inputs.extend(tuple_args.types.iter().cloned());
230
231                Some(ClosureInfo { kind, state })
232            }
233            _ => None,
234        };
235
236        Ok(FunSig {
237            generics: self.the_only_binder().params.clone(),
238            is_unsafe,
239            is_closure: matches!(&def.kind, hax::FullDefKind::Closure { .. }),
240            closure_info,
241            inputs,
242            output,
243        })
244    }
245
246    /// Generate a fake function body for ADT constructors.
247    fn build_ctor_body(
248        &mut self,
249        span: Span,
250        signature: &FunSig,
251        adt_def_id: &hax::DefId,
252        ctor_of: &hax::CtorOf,
253        variant_id: usize,
254        fields: &hax::IndexVec<hax::FieldIdx, hax::FieldDef>,
255        output_ty: &hax::Ty,
256    ) -> Result<Body, Error> {
257        let adt_decl_id = self.register_type_decl_id(span, adt_def_id);
258        let output_ty = self.translate_ty(span, output_ty)?;
259        let mut locals = Locals {
260            arg_count: fields.len(),
261            locals: Vector::new(),
262        };
263        locals.new_var(None, output_ty);
264        let args: Vec<_> = fields
265            .iter()
266            .map(|field| {
267                let ty = self.translate_ty(span, &field.ty)?;
268                let place = locals.new_var(None, ty);
269                Ok(Operand::Move(place))
270            })
271            .try_collect()?;
272        let variant = match ctor_of {
273            hax::CtorOf::Struct => None,
274            hax::CtorOf::Variant => Some(VariantId::from(variant_id)),
275        };
276        let st_kind = RawStatement::Assign(
277            locals.return_place(),
278            Rvalue::Aggregate(
279                AggregateKind::Adt(
280                    TypeId::Adt(adt_decl_id),
281                    variant,
282                    None,
283                    Box::new(
284                        signature
285                            .generics
286                            .identity_args(GenericsSource::item(adt_decl_id)),
287                    ),
288                ),
289                args,
290            ),
291        );
292        let statement = Statement::new(span, st_kind);
293        let block = BlockData {
294            statements: vec![statement],
295            terminator: Terminator::new(span, RawTerminator::Return),
296        };
297        let body = Body::Unstructured(GExprBody {
298            span,
299            locals,
300            comments: Default::default(),
301            body: [block].into_iter().collect(),
302        });
303        Ok(body)
304    }
305
306    /// Auxiliary function to translate function calls and references to functions.
307    /// Translate a function id applied with some substitutions.
308    ///
309    /// TODO: should we always erase the regions?
310    pub(crate) fn translate_fn_ptr(
311        &mut self,
312        span: Span,
313        def_id: &hax::DefId,
314        substs: &Vec<hax::GenericArg>,
315        trait_refs: &Vec<hax::ImplExpr>,
316        trait_info: &Option<hax::ImplExpr>,
317    ) -> Result<FnPtr, Error> {
318        let fun_def = self.t_ctx.hax_def(def_id)?;
319
320        // Trait information
321        trace!(
322            "Trait information:\n- def_id: {:?}\n- impl source:\n{:?}",
323            def_id,
324            trait_info
325        );
326        trace!(
327            "Method traits:\n- def_id: {:?}\n- traits:\n{:?}",
328            def_id,
329            trait_refs
330        );
331
332        // Check if the function is considered primitive: primitive
333        // functions benefit from special treatment.
334        let fun_id = if fun_def.diagnostic_item.as_deref() == Some("box_new") {
335            // Built-in function.
336            assert!(trait_info.is_none());
337            FunIdOrTraitMethodRef::Fun(FunId::Builtin(BuiltinFunId::BoxNew))
338        } else {
339            let fun_id = self.register_fun_decl_id(span, def_id);
340            // Two cases depending on whether we call a trait method or not
341            match trait_info {
342                // Direct function call
343                None => FunIdOrTraitMethodRef::Fun(FunId::Regular(fun_id)),
344                // Trait method
345                Some(trait_info) => {
346                    let impl_expr = self.translate_trait_impl_expr(span, trait_info)?;
347                    let method_name = self.t_ctx.translate_trait_item_name(def_id)?;
348                    FunIdOrTraitMethodRef::Trait(impl_expr, method_name, fun_id)
349                }
350            }
351        };
352
353        // Translate the type parameters
354        let binder = match fun_def.kind() {
355            hax::FullDefKind::Fn { sig, .. } | hax::FullDefKind::AssocFn { sig, .. } => {
356                Some(sig.as_ref().rebind(()))
357            }
358            _ => None,
359        };
360        let generics = self.translate_generic_args(
361            span,
362            substs,
363            trait_refs,
364            binder,
365            fun_id.generics_target(),
366        )?;
367
368        Ok(FnPtr {
369            func: Box::new(fun_id),
370            generics: Box::new(generics),
371        })
372    }
373
374    /// Translate one function.
375    #[tracing::instrument(skip(self, item_meta))]
376    pub fn translate_function(
377        mut self,
378        def_id: FunDeclId,
379        item_meta: ItemMeta,
380        def: &hax::FullDef,
381    ) -> Result<FunDecl, Error> {
382        trace!("About to translate function:\n{:?}", def.def_id);
383        let span = item_meta.span;
384
385        // Translate the function signature
386        trace!("Translating function signature");
387        let signature = self.translate_function_signature(def, &item_meta)?;
388
389        // Check whether this function is a method declaration for a trait definition.
390        // If this is the case, it shouldn't contain a body.
391        let kind = self.get_item_kind(span, def)?;
392        let is_trait_method_decl_without_default = match &kind {
393            ItemKind::Regular | ItemKind::TraitImpl { .. } => false,
394            ItemKind::TraitDecl { has_default, .. } => !has_default,
395        };
396
397        let is_global_initializer = matches!(
398            def.kind(),
399            hax::FullDefKind::Const { .. }
400                | hax::FullDefKind::AssocConst { .. }
401                | hax::FullDefKind::AnonConst { .. }
402                | hax::FullDefKind::InlineConst { .. }
403                | hax::FullDefKind::PromotedConst { .. }
404                | hax::FullDefKind::Static { .. }
405        );
406        let is_global_initializer =
407            is_global_initializer.then(|| self.register_global_decl_id(span, &def.def_id));
408
409        let body_id = if item_meta.opacity.with_private_contents().is_opaque()
410            || is_trait_method_decl_without_default
411        {
412            Err(Opaque)
413        } else if let hax::FullDefKind::Ctor {
414            adt_def_id,
415            ctor_of,
416            variant_id,
417            fields,
418            output_ty,
419            ..
420        } = def.kind()
421        {
422            let body = self.build_ctor_body(
423                span,
424                &signature,
425                adt_def_id,
426                ctor_of,
427                *variant_id,
428                fields,
429                output_ty,
430            )?;
431            Ok(body)
432        } else {
433            // Translate the body. This doesn't store anything if we can't/decide not to translate
434            // this body.
435            let mut bt_ctx = BodyTransCtx::new(&mut self);
436            match bt_ctx.translate_body(item_meta.span, def) {
437                Ok(Ok(body)) => Ok(body),
438                // Opaque declaration
439                Ok(Err(Opaque)) => Err(Opaque),
440                // Translation error.
441                // FIXME: handle error cases more explicitly.
442                Err(_) => Err(Opaque),
443            }
444        };
445        Ok(FunDecl {
446            def_id,
447            item_meta,
448            signature,
449            kind,
450            is_global_initializer,
451            body: body_id,
452        })
453    }
454
455    /// Translate one global.
456    #[tracing::instrument(skip(self, item_meta))]
457    pub fn translate_global(
458        mut self,
459        def_id: GlobalDeclId,
460        item_meta: ItemMeta,
461        def: &hax::FullDef,
462    ) -> Result<GlobalDecl, Error> {
463        trace!("About to translate global:\n{:?}", def.def_id);
464        let span = item_meta.span;
465
466        // Translate the generics and predicates - globals *can* have generics
467        // Ex.:
468        // ```
469        // impl<const N : usize> Foo<N> {
470        //   const LEN : usize = N;
471        // }
472        // ```
473        self.translate_def_generics(span, def)?;
474
475        // Retrieve the kind
476        let item_kind = self.get_item_kind(span, def)?;
477
478        trace!("Translating global type");
479        let ty = match &def.kind {
480            hax::FullDefKind::Const { ty, .. }
481            | hax::FullDefKind::AssocConst { ty, .. }
482            | hax::FullDefKind::AnonConst { ty, .. }
483            | hax::FullDefKind::InlineConst { ty, .. }
484            | hax::FullDefKind::PromotedConst { ty, .. }
485            | hax::FullDefKind::Static { ty, .. } => ty,
486            _ => panic!("Unexpected def for constant: {def:?}"),
487        };
488        let ty = self.translate_ty(span, ty)?;
489
490        let global_kind = match &def.kind {
491            hax::FullDefKind::Static { .. } => GlobalKind::Static,
492            hax::FullDefKind::Const { .. } | hax::FullDefKind::AssocConst { .. } => {
493                GlobalKind::NamedConst
494            }
495            hax::FullDefKind::AnonConst { .. }
496            | hax::FullDefKind::InlineConst { .. }
497            | hax::FullDefKind::PromotedConst { .. } => GlobalKind::AnonConst,
498            _ => panic!("Unexpected def for constant: {def:?}"),
499        };
500
501        let initializer = self.register_fun_decl_id(span, &def.def_id);
502
503        Ok(GlobalDecl {
504            def_id,
505            item_meta,
506            generics: self.into_generics(),
507            ty,
508            kind: item_kind,
509            global_kind,
510            init: initializer,
511        })
512    }
513}