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

charon_driver/translate/
translate_closures.rs
