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

charon_driver/translate/
translate_closures.rs
