charon_driver/translate/
translate_closures.rs

1//! In rust, closures behave like ADTs that implement the FnOnce/FnMut/Fn traits automatically.
2//!
3//! Here we convert closures to a struct containing the closure's state (upvars), along with
4//! matching trait impls and fun decls (e.g. a Fn closure will have a trait impl for Fn, FnMut and
5//! FnOnce, along with 3 matching method implementations for call, call_mut and call_once).
6//!
7//! For example, given the following Rust code:
8//! ```rust
9//! pub fn test_closure_capture<T: Clone>() {
10//!     let mut v = vec![];
11//!     let mut add = |x: &u32| v.push(*x);
12//!     add(&0);
13//!     add(&1);
14//! }
15//! ```
16//!
17//! We generate the equivalent desugared code:
18//! ```rust
19//! struct {test_closure_capture::closure#0}<'a, T: Clone> (&'a mut Vec<u32>);
20//!
21//! // The 'a comes from captured variables, the 'b comes from the closure higher-kinded signature.
22//! impl<'a, 'b, T: Clone> FnMut<(&'b u32,)> for {test_closure_capture::closure#0}<'a, T> {
23//!     fn call_mut<'c>(&'c mut self, arg: (&'b u32,)) {
24//!         self.0.push(*arg.0);
25//!     }
26//! }
27//!
28//! impl<'a, 'b, T: Clone> FnOnce<(&'b u32,)> for {test_closure_capture::closure#0}<'a, T> {
29//!     type Output = ();
30//!     ...
31//! }
32//!
33//! pub fn test_closure_capture<T: Clone>() {
34//!     let mut v = vec![];
35//!     let mut add = {test_closure_capture::closure#0} (&mut v);
36//!     state.call_mut(&0);
37//!     state.call_mut(&1);
38//! }
39//! ```
40
41use std::mem;
42
43use crate::translate::translate_bodies::BodyTransCtx;
44
45use super::translate_crate::TransItemSourceKind;
46use super::translate_ctx::*;
47use charon_lib::ast::ullbc_ast_utils::BodyBuilder;
48use charon_lib::ast::*;
49use charon_lib::ids::Vector;
50use charon_lib::ullbc_ast::*;
51use itertools::Itertools;
52
53pub fn translate_closure_kind(kind: &hax::ClosureKind) -> ClosureKind {
54    match kind {
55        hax::ClosureKind::Fn => ClosureKind::Fn,
56        hax::ClosureKind::FnMut => ClosureKind::FnMut,
57        hax::ClosureKind::FnOnce => ClosureKind::FnOnce,
58    }
59}
60
61impl ItemTransCtx<'_, '_> {
62    pub fn translate_closure_info(
63        &mut self,
64        span: Span,
65        args: &hax::ClosureArgs,
66    ) -> Result<ClosureInfo, Error> {
67        use ClosureKind::*;
68        let kind = translate_closure_kind(&args.kind);
69
70        let fn_once_impl = self.translate_closure_bound_impl_ref(span, args, FnOnce)?;
71        let fn_mut_impl = if matches!(kind, FnMut | Fn) {
72            Some(self.translate_closure_bound_impl_ref(span, args, FnMut)?)
73        } else {
74            None
75        };
76        let fn_impl = if matches!(kind, Fn) {
77            Some(self.translate_closure_bound_impl_ref(span, args, Fn)?)
78        } else {
79            None
80        };
81        let signature = self.translate_fun_sig(span, &args.fn_sig)?;
82        Ok(ClosureInfo {
83            kind,
84            fn_once_impl,
85            fn_mut_impl,
86            fn_impl,
87            signature,
88        })
89    }
90
91    /// Translate a reference to the closure ADT. The resulting type needs lifetime arguments for
92    /// the upvars (captured variables). If you don't know what to do about the bound lifetimes,
93    /// use `translate_closure_type_ref` instead.
94    pub fn translate_closure_bound_type_ref(
95        &mut self,
96        span: Span,
97        closure: &hax::ClosureArgs,
98    ) -> Result<RegionBinder<TypeDeclRef>, Error> {
99        // We add lifetime args for each borrowing upvar, gotta supply them here.
100        let upvar_binder = hax::Binder {
101            value: (),
102            bound_vars: closure
103                .upvar_tys
104                .iter()
105                .filter(|ty| {
106                    matches!(
107                        ty.kind(),
108                        hax::TyKind::Ref(
109                            hax::Region {
110                                kind: hax::RegionKind::ReErased
111                            },
112                            ..
113                        )
114                    )
115                })
116                .map(|_| hax::BoundVariableKind::Region(hax::BoundRegionKind::Anon))
117                .collect(),
118        };
119        let tref = self.translate_type_decl_ref(span, &closure.item)?;
120        self.translate_region_binder(span, &upvar_binder, |ctx, _| {
121            let mut tref = tref.move_under_binder();
122            tref.generics.regions.extend(
123                ctx.innermost_binder()
124                    .params
125                    .identity_args()
126                    .regions
127                    .into_iter(),
128            );
129            Ok(tref)
130        })
131    }
132
133    /// Translate a reference to the closure ADT.
134    pub fn translate_closure_type_ref(
135        &mut self,
136        span: Span,
137        closure: &hax::ClosureArgs,
138    ) -> Result<TypeDeclRef, Error> {
139        let bound_tref = self.translate_closure_bound_type_ref(span, closure)?;
140        let tref = if self.item_src.def_id() == &closure.item.def_id {
141            // We have fresh upvar regions in scope.
142            bound_tref.apply(
143                self.outermost_binder()
144                    .by_ref_upvar_regions
145                    .iter()
146                    .map(|r| Region::Var(DeBruijnVar::bound(self.binding_levels.depth(), *r)))
147                    .collect(),
148            )
149        } else {
150            // No upvar lifetimes in scope, we supply erased regions instead.
151            bound_tref.erase()
152        };
153        Ok(tref)
154    }
155
156    /// For stateless closures, translate a function reference to the top-level function that
157    /// executes the closure code without taking the state as parameter.
158    pub fn translate_stateless_closure_as_fn_ref(
159        &mut self,
160        span: Span,
161        closure: &hax::ClosureArgs,
162    ) -> Result<RegionBinder<FunDeclRef>, Error> {
163        let id = self.register_item(span, &closure.item, TransItemSourceKind::ClosureAsFnCast);
164        let TypeDeclRef { generics, .. } = self.translate_closure_type_ref(span, closure)?;
165        self.translate_region_binder(span, &closure.fn_sig, |ctx, _| {
166            let mut generics = generics.move_under_binder();
167            generics.regions.extend(
168                ctx.innermost_binder()
169                    .params
170                    .identity_args()
171                    .regions
172                    .into_iter(),
173            );
174            Ok(FunDeclRef { id, generics })
175        })
176    }
177
178    /// Translate a reference to the chosen closure impl. The resulting value needs lifetime
179    /// arguments for late-bound lifetimes. If you don't know what to do about the bound lifetimes,
180    /// use `translate_closure_impl_ref` instead.
181    pub fn translate_closure_bound_impl_ref(
182        &mut self,
183        span: Span,
184        closure: &hax::ClosureArgs,
185        target_kind: ClosureKind,
186    ) -> Result<RegionBinder<TraitImplRef>, Error> {
187        let impl_id = self.register_item(
188            span,
189            &closure.item,
190            TransItemSourceKind::TraitImpl(TraitImplSource::Closure(target_kind)),
191        );
192        let adt_ref = self.translate_closure_type_ref(span, closure)?;
193        let impl_ref = TraitImplRef {
194            id: impl_id,
195            generics: adt_ref.generics,
196        };
197        self.translate_region_binder(span, &closure.fn_sig, |ctx, _| {
198            let mut impl_ref = impl_ref.move_under_binder();
199            impl_ref.generics.regions.extend(
200                ctx.innermost_binder()
201                    .params
202                    .identity_args()
203                    .regions
204                    .into_iter(),
205            );
206            Ok(impl_ref)
207        })
208    }
209
210    /// Translate a reference to the chosen closure impl.
211    pub fn translate_closure_impl_ref(
212        &mut self,
213        span: Span,
214        closure: &hax::ClosureArgs,
215        target_kind: ClosureKind,
216    ) -> Result<TraitImplRef, Error> {
217        let bound_impl_ref = self.translate_closure_bound_impl_ref(span, closure, target_kind)?;
218        let impl_ref = if self.item_src.def_id() == &closure.item.def_id {
219            // We have fresh regions in scope.
220            bound_impl_ref.apply(
221                self.outermost_binder()
222                    .bound_region_vars
223                    .iter()
224                    .map(|r| Region::Var(DeBruijnVar::bound(self.binding_levels.depth(), *r)))
225                    .collect(),
226            )
227        } else {
228            bound_impl_ref.erase()
229        };
230        Ok(impl_ref)
231    }
232
233    pub fn get_closure_state_ty(
234        &mut self,
235        span: Span,
236        args: &hax::ClosureArgs,
237    ) -> Result<Ty, Error> {
238        let tref = self.translate_closure_type_ref(span, args)?;
239        Ok(TyKind::Adt(tref).into_ty())
240    }
241
242    pub fn translate_closure_adt(
243        &mut self,
244        _trans_id: TypeDeclId,
245        span: Span,
246        args: &hax::ClosureArgs,
247    ) -> Result<TypeDeclKind, Error> {
248        let mut by_ref_upvar_regions = self
249            .the_only_binder()
250            .by_ref_upvar_regions
251            .clone()
252            .into_iter();
253        let fields: Vector<FieldId, Field> = args
254            .upvar_tys
255            .iter()
256            .map(|ty| -> Result<Field, Error> {
257                let mut ty = self.translate_ty(span, ty)?;
258                // We supply fresh regions for the by-ref upvars.
259                if let TyKind::Ref(Region::Erased, deref_ty, kind) = ty.kind() {
260                    let region_id = by_ref_upvar_regions.next().unwrap();
261                    ty = TyKind::Ref(
262                        Region::Var(DeBruijnVar::new_at_zero(region_id)),
263                        deref_ty.clone(),
264                        *kind,
265                    )
266                    .into_ty();
267                }
268                Ok(Field {
269                    span,
270                    attr_info: AttrInfo {
271                        attributes: vec![],
272                        inline: None,
273                        rename: None,
274                        public: false,
275                    },
276                    name: None,
277                    ty,
278                })
279            })
280            .try_collect()?;
281        Ok(TypeDeclKind::Struct(fields))
282    }
283
284    /// Given an item that is a closure, generate the signature of the
285    /// `call_once`/`call_mut`/`call` method (depending on `target_kind`).
286    fn translate_closure_method_sig(
287        &mut self,
288        def: &hax::FullDef,
289        span: Span,
290        args: &hax::ClosureArgs,
291        target_kind: ClosureKind,
292    ) -> Result<FunSig, Error> {
293        let signature = &args.fn_sig;
294        trace!(
295            "signature of closure {:?}:\n{:?}",
296            def.def_id(),
297            signature.value,
298        );
299
300        let is_unsafe = match signature.value.safety {
301            hax::Safety::Unsafe => true,
302            hax::Safety::Safe => false,
303        };
304
305        let state_ty = self.get_closure_state_ty(span, args)?;
306
307        // Depending on the kind of the closure generated, add a reference
308        let state_ty = match target_kind {
309            ClosureKind::FnOnce => state_ty,
310            ClosureKind::Fn | ClosureKind::FnMut => {
311                let rid = self
312                    .innermost_generics_mut()
313                    .regions
314                    .push_with(|index| RegionParam { index, name: None });
315                let r = Region::Var(DeBruijnVar::new_at_zero(rid));
316                let mutability = if target_kind == ClosureKind::Fn {
317                    RefKind::Shared
318                } else {
319                    RefKind::Mut
320                };
321                TyKind::Ref(r, state_ty, mutability).into_ty()
322            }
323        };
324
325        // The types that the closure takes as input.
326        let input_tys: Vec<Ty> = signature
327            .value
328            .inputs
329            .iter()
330            .map(|ty| self.translate_ty(span, ty))
331            .try_collect()?;
332        // The method takes `self` and the closure inputs as a tuple.
333        let inputs = vec![state_ty, Ty::mk_tuple(input_tys)];
334        let output = self.translate_ty(span, &signature.value.output)?;
335
336        Ok(FunSig {
337            generics: self.the_only_binder().params.clone(),
338            is_unsafe,
339            inputs,
340            output,
341        })
342    }
343
344    fn translate_closure_method_body(
345        mut self,
346        span: Span,
347        def: &hax::FullDef,
348        target_kind: ClosureKind,
349        args: &hax::ClosureArgs,
350        signature: &FunSig,
351    ) -> Result<Result<Body, Opaque>, Error> {
352        use ClosureKind::*;
353        let closure_kind = translate_closure_kind(&args.kind);
354        Ok(match (target_kind, closure_kind) {
355            (Fn, Fn) | (FnMut, FnMut) | (FnOnce, FnOnce) => {
356                // Translate the function's body normally
357                let mut bt_ctx = BodyTransCtx::new(&mut self);
358                match bt_ctx.translate_def_body(span, def) {
359                    Ok(Ok(mut body)) => {
360                        // The body is translated as if the locals are: ret value, state, arg-1,
361                        // ..., arg-N, rest...
362                        // However, there is only one argument with the tupled closure arguments;
363                        // we must thus shift all locals with index >=2 by 1, and add a new local
364                        // for the tupled arg, giving us: ret value, state, args, arg-1, ...,
365                        // arg-N, rest...
366                        // We then add N statements of the form `locals[N+3] := move locals[2].N`,
367                        // to destructure the arguments.
368                        let GExprBody {
369                            locals,
370                            body: blocks,
371                            ..
372                        } = body.as_unstructured_mut().unwrap();
373
374                        blocks.dyn_visit_mut(|local: &mut LocalId| {
375                            if local.index() >= 2 {
376                                *local += 1;
377                            }
378                        });
379
380                        let mut old_locals = mem::take(&mut locals.locals).into_iter();
381                        locals.arg_count = 2;
382                        locals.locals.push(old_locals.next().unwrap()); // ret
383                        locals.locals.push(old_locals.next().unwrap()); // state
384                        let tupled_arg = locals
385                            .new_var(Some("tupled_args".to_string()), signature.inputs[1].clone());
386                        locals.locals.extend(old_locals.map(|mut l| {
387                            l.index += 1;
388                            l
389                        }));
390
391                        let untupled_args = signature.inputs[1].as_tuple().unwrap();
392                        let closure_arg_count = untupled_args.elem_count();
393                        let new_stts = untupled_args.iter().cloned().enumerate().map(|(i, ty)| {
394                            let nth_field = tupled_arg.clone().project(
395                                ProjectionElem::Field(
396                                    FieldProjKind::Tuple(closure_arg_count),
397                                    FieldId::new(i),
398                                ),
399                                ty,
400                            );
401                            let local_id = LocalId::new(i + 3);
402                            Statement::new(
403                                span,
404                                StatementKind::Assign(
405                                    locals.place_for_var(local_id),
406                                    Rvalue::Use(Operand::Move(nth_field)),
407                                ),
408                            )
409                        });
410                        blocks[BlockId::ZERO].statements.splice(0..0, new_stts);
411
412                        Ok(body)
413                    }
414                    Ok(Err(Opaque)) => Err(Opaque),
415                    Err(_) => Err(Opaque),
416                }
417            }
418            // Target translation:
419            //
420            // fn call_once(state: Self, args: Args) -> Output {
421            //   let temp_ref = &[mut] state;
422            //   let ret = self.call[_mut](temp, args);
423            //   drop state;
424            //   return ret;
425            // }
426            //
427            (FnOnce, Fn | FnMut) => {
428                // Hax (via rustc) gives us the MIR to do this.
429                let hax::FullDefKind::Closure {
430                    once_shim: Some(body),
431                    ..
432                } = &def.kind
433                else {
434                    panic!("missing shim for closure")
435                };
436                let mut bt_ctx = BodyTransCtx::new(&mut self);
437                match bt_ctx.translate_body(span, body, &def.source_text) {
438                    Ok(Ok(body)) => Ok(body),
439                    Ok(Err(Opaque)) => Err(Opaque),
440                    Err(_) => Err(Opaque),
441                }
442            }
443            // Target translation:
444            //
445            // fn call_mut(state: &mut Self, args: Args) -> Output {
446            //   let reborrow = &*state;
447            //   self.call(reborrow, args)
448            // }
449            (FnMut, Fn) => {
450                let fun_id: FunDeclId = self.register_item(
451                    span,
452                    def.this(),
453                    TransItemSourceKind::ClosureMethod(closure_kind),
454                );
455                let impl_ref = self.translate_closure_impl_ref(span, args, closure_kind)?;
456                // TODO: make a trait call to avoid needing to concatenate things ourselves.
457                // TODO: can we ask hax for the trait ref?
458                let fn_op = FnOperand::Regular(FnPtr::new(
459                    fun_id.into(),
460                    impl_ref.generics.concat(&GenericArgs {
461                        regions: vec![Region::Erased].into(),
462                        ..GenericArgs::empty()
463                    }),
464                ));
465
466                let mut builder = BodyBuilder::new(span, 2);
467
468                let output = builder.new_var(None, signature.output.clone());
469                let state = builder.new_var(Some("state".to_string()), signature.inputs[0].clone());
470                let args = builder.new_var(Some("args".to_string()), signature.inputs[1].clone());
471                let deref_state = state.deref();
472                let reborrow_ty =
473                    TyKind::Ref(Region::Erased, deref_state.ty.clone(), RefKind::Shared).into_ty();
474                let reborrow = builder.new_var(None, reborrow_ty);
475
476                builder.push_statement(StatementKind::Assign(
477                    reborrow.clone(),
478                    // the state must be Sized, hence `()` as ptr-metadata
479                    Rvalue::Ref {
480                        place: deref_state,
481                        kind: BorrowKind::Shared,
482                        ptr_metadata: Operand::mk_const_unit(),
483                    },
484                ));
485
486                builder.call(Call {
487                    func: fn_op,
488                    args: vec![Operand::Move(reborrow), Operand::Move(args)],
489                    dest: output,
490                });
491
492                Ok(Body::Unstructured(builder.build()))
493            }
494            (Fn, FnOnce) | (Fn, FnMut) | (FnMut, FnOnce) => {
495                panic!(
496                    "Can't make a closure body for a more restrictive kind \
497                    than the closure kind"
498                )
499            }
500        })
501    }
502
503    /// Given an item that is a closure, generate the `call_once`/`call_mut`/`call` method
504    /// (depending on `target_kind`).
505    #[tracing::instrument(skip(self, item_meta))]
506    pub fn translate_closure_method(
507        mut self,
508        def_id: FunDeclId,
509        item_meta: ItemMeta,
510        def: &hax::FullDef,
511        target_kind: ClosureKind,
512    ) -> Result<FunDecl, Error> {
513        let span = item_meta.span;
514        let hax::FullDefKind::Closure {
515            args,
516            fn_once_impl,
517            fn_mut_impl,
518            fn_impl,
519            ..
520        } = &def.kind
521        else {
522            unreachable!()
523        };
524
525        trace!("About to translate closure:\n{:?}", def.def_id());
526
527        self.translate_def_generics(span, def)?;
528        // Add the lifetime generics coming from the higher-kindedness of the signature.
529        assert!(self.innermost_binder_mut().bound_region_vars.is_empty(),);
530        self.innermost_binder_mut()
531            .push_params_from_binder(args.fn_sig.rebind(()))?;
532
533        // Hax gives us trait-related information for the impl we're building.
534        let vimpl = match target_kind {
535            ClosureKind::FnOnce => fn_once_impl,
536            ClosureKind::FnMut => fn_mut_impl.as_ref().unwrap(),
537            ClosureKind::Fn => fn_impl.as_ref().unwrap(),
538        };
539        let implemented_trait = self.translate_trait_predicate(span, &vimpl.trait_pred)?;
540
541        let impl_ref = self.translate_closure_impl_ref(span, args, target_kind)?;
542        let src = ItemSource::TraitImpl {
543            impl_ref,
544            trait_ref: implemented_trait,
545            item_name: TraitItemName(target_kind.method_name().to_owned()),
546            reuses_default: false,
547        };
548
549        // Translate the function signature
550        let signature = self.translate_closure_method_sig(def, span, args, target_kind)?;
551
552        let body = if item_meta.opacity.with_private_contents().is_opaque() {
553            Err(Opaque)
554        } else {
555            self.translate_closure_method_body(span, def, target_kind, args, &signature)?
556        };
557
558        Ok(FunDecl {
559            def_id,
560            item_meta,
561            signature,
562            src,
563            is_global_initializer: None,
564            body,
565        })
566    }
567
568    #[tracing::instrument(skip(self, item_meta))]
569    pub fn translate_closure_trait_impl(
570        mut self,
571        def_id: TraitImplId,
572        item_meta: ItemMeta,
573        def: &hax::FullDef,
574        target_kind: ClosureKind,
575    ) -> Result<TraitImpl, Error> {
576        let span = item_meta.span;
577        let hax::FullDefKind::Closure {
578            args,
579            fn_once_impl,
580            fn_mut_impl,
581            fn_impl,
582            ..
583        } = &def.kind
584        else {
585            unreachable!()
586        };
587
588        self.translate_def_generics(span, def)?;
589        // Add the lifetime generics coming from the higher-kindedness of the signature.
590        assert!(self.innermost_binder_mut().bound_region_vars.is_empty());
591        self.innermost_binder_mut()
592            .push_params_from_binder(args.fn_sig.rebind(()))?;
593
594        // Hax gives us trait-related information for the impl we're building.
595        let vimpl = match target_kind {
596            ClosureKind::FnOnce => fn_once_impl,
597            ClosureKind::FnMut => fn_mut_impl.as_ref().unwrap(),
598            ClosureKind::Fn => fn_impl.as_ref().unwrap(),
599        };
600        let mut timpl = self.translate_virtual_trait_impl(def_id, item_meta, vimpl)?;
601
602        // Construct the `call_*` method reference.
603        let call_fn_id = self.register_item(
604            span,
605            def.this(),
606            TransItemSourceKind::ClosureMethod(target_kind),
607        );
608        let call_fn_name = TraitItemName(target_kind.method_name().to_string());
609        let call_fn_binder = {
610            let mut method_params = GenericParams::empty();
611            match target_kind {
612                ClosureKind::FnOnce => {}
613                ClosureKind::FnMut | ClosureKind::Fn => {
614                    method_params
615                        .regions
616                        .push_with(|index| RegionParam { index, name: None });
617                }
618            };
619
620            let generics = self
621                .outermost_binder()
622                .params
623                .identity_args_at_depth(DeBruijnId::one())
624                .concat(&method_params.identity_args_at_depth(DeBruijnId::zero()));
625            Binder::new(
626                BinderKind::TraitMethod(timpl.impl_trait.id, call_fn_name.clone()),
627                method_params,
628                FunDeclRef {
629                    id: call_fn_id,
630                    generics: Box::new(generics),
631                },
632            )
633        };
634        timpl.methods.push((call_fn_name, call_fn_binder));
635
636        Ok(timpl)
637    }
638
639    /// Given an item that is a non-capturing closure, generate the equivalent function,
640    /// by removing the state from the parameters and untupling the arguments.
641    #[tracing::instrument(skip(self, item_meta))]
642    pub fn translate_stateless_closure_as_fn(
643        mut self,
644        def_id: FunDeclId,
645        item_meta: ItemMeta,
646        def: &hax::FullDef,
647    ) -> Result<FunDecl, Error> {
648        let span = item_meta.span;
649        let hax::FullDefKind::Closure { args: closure, .. } = &def.kind else {
650            unreachable!()
651        };
652
653        trace!("About to translate closure as fn:\n{:?}", def.def_id());
654
655        assert!(
656            closure.upvar_tys.is_empty(),
657            "Only stateless closures can be translated as functions"
658        );
659
660        self.translate_def_generics(span, def)?;
661        // Add the lifetime generics coming from the higher-kindedness of the signature.
662        assert!(self.innermost_binder_mut().bound_region_vars.is_empty(),);
663        self.innermost_binder_mut()
664            .push_params_from_binder(closure.fn_sig.rebind(()))?;
665
666        // Translate the function signature
667        let mut signature =
668            self.translate_closure_method_sig(def, span, closure, ClosureKind::FnOnce)?;
669        let state_ty = signature.inputs.remove(0);
670        let args_tuple_ty = signature.inputs.remove(0);
671        signature.inputs = args_tuple_ty.as_tuple().unwrap().iter().cloned().collect();
672
673        let body = if item_meta.opacity.with_private_contents().is_opaque() {
674            Err(Opaque)
675        } else {
676            // Target translation:
677            //
678            // fn call_fn(arg0: Args[0], ..., argN: Args[N]) -> Output {
679            //   let closure: Closure = {};
680            //   let args = (arg0, ..., argN);
681            //   closure.call(args)
682            // }
683            let fun_id: FunDeclId = self.register_item(
684                span,
685                def.this(),
686                TransItemSourceKind::ClosureMethod(ClosureKind::FnOnce),
687            );
688            let impl_ref = self.translate_closure_impl_ref(span, closure, ClosureKind::FnOnce)?;
689            let fn_op = FnOperand::Regular(FnPtr::new(fun_id.into(), impl_ref.generics.clone()));
690
691            let mut builder = BodyBuilder::new(span, signature.inputs.len());
692
693            let output = builder.new_var(None, signature.output.clone());
694            let args: Vec<Place> = signature
695                .inputs
696                .iter()
697                .enumerate()
698                .map(|(i, ty)| builder.new_var(Some(format!("arg{}", i + 1)), ty.clone()))
699                .collect();
700            let args_tupled = builder.new_var(Some("args".to_string()), args_tuple_ty.clone());
701            let state = builder.new_var(Some("state".to_string()), state_ty.clone());
702
703            builder.push_statement(StatementKind::Assign(
704                args_tupled.clone(),
705                Rvalue::Aggregate(
706                    AggregateKind::Adt(args_tuple_ty.as_adt().unwrap().clone(), None, None),
707                    args.into_iter().map(Operand::Move).collect(),
708                ),
709            ));
710
711            let state_ty_adt = state_ty.as_adt().unwrap();
712            builder.push_statement(StatementKind::Assign(
713                state.clone(),
714                Rvalue::Aggregate(AggregateKind::Adt(state_ty_adt.clone(), None, None), vec![]),
715            ));
716
717            builder.call(Call {
718                func: fn_op,
719                args: vec![Operand::Move(state), Operand::Move(args_tupled)],
720                dest: output,
721            });
722
723            Ok(Body::Unstructured(builder.build()))
724        };
725
726        Ok(FunDecl {
727            def_id,
728            item_meta,
729            signature,
730            src: ItemSource::TopLevel,
731            is_global_initializer: None,
732            body,
733        })
734    }
735}
charon_driver/translate/translate_closures.rs

charon_driver/translate/
translate_closures.rs
