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

charon_driver/translate/
translate_closures.rs
