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 hax_frontend_exporter as hax;
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| RegionVar { 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        let mk_stt = |content| Statement::new(span, content);
355        let mk_block = |statements, terminator| -> BlockData {
356            BlockData {
357                statements,
358                terminator: Terminator::new(span, terminator),
359            }
360        };
361
362        Ok(match (target_kind, closure_kind) {
363            (Fn, Fn) | (FnMut, FnMut) | (FnOnce, FnOnce) => {
364                // Translate the function's body normally
365                let mut bt_ctx = BodyTransCtx::new(&mut self);
366                match bt_ctx.translate_def_body(span, def) {
367                    Ok(Ok(mut body)) => {
368                        // The body is translated as if the locals are: ret value, state, arg-1,
369                        // ..., arg-N, rest...
370                        // However, there is only one argument with the tupled closure arguments;
371                        // we must thus shift all locals with index >=2 by 1, and add a new local
372                        // for the tupled arg, giving us: ret value, state, args, arg-1, ...,
373                        // arg-N, rest...
374                        // We then add N statements of the form `locals[N+3] := move locals[2].N`,
375                        // to destructure the arguments.
376                        let GExprBody {
377                            locals,
378                            body: blocks,
379                            ..
380                        } = body.as_unstructured_mut().unwrap();
381
382                        blocks.dyn_visit_mut(|local: &mut LocalId| {
383                            let idx = local.index();
384                            if idx >= 2 {
385                                *local = LocalId::new(idx + 1)
386                            }
387                        });
388
389                        let mut old_locals = mem::take(&mut locals.locals).into_iter();
390                        locals.arg_count = 2;
391                        locals.locals.push(old_locals.next().unwrap()); // ret
392                        locals.locals.push(old_locals.next().unwrap()); // state
393                        let tupled_arg = locals
394                            .new_var(Some("tupled_args".to_string()), signature.inputs[1].clone());
395                        locals.locals.extend(old_locals.map(|mut l| {
396                            l.index += 1;
397                            l
398                        }));
399
400                        let untupled_args = signature.inputs[1].as_tuple().unwrap();
401                        let closure_arg_count = untupled_args.elem_count();
402                        let new_stts = untupled_args.iter().cloned().enumerate().map(|(i, ty)| {
403                            let nth_field = tupled_arg.clone().project(
404                                ProjectionElem::Field(
405                                    FieldProjKind::Tuple(closure_arg_count),
406                                    FieldId::new(i),
407                                ),
408                                ty,
409                            );
410                            mk_stt(RawStatement::Assign(
411                                locals.place_for_var(LocalId::new(i + 3)),
412                                Rvalue::Use(Operand::Move(nth_field)),
413                            ))
414                        });
415                        blocks[BlockId::ZERO].statements.splice(0..0, new_stts);
416
417                        Ok(body)
418                    }
419                    Ok(Err(Opaque)) => Err(Opaque),
420                    Err(_) => Err(Opaque),
421                }
422            }
423            // Target translation:
424            //
425            // fn call_once(state: Self, args: Args) -> Output {
426            //   let temp_ref = &[mut] state;
427            //   let ret = self.call[_mut](temp, args);
428            //   drop state;
429            //   return ret;
430            // }
431            //
432            (FnOnce, Fn | FnMut) => {
433                // Hax (via rustc) gives us the MIR to do this.
434                let hax::FullDefKind::Closure {
435                    once_shim: Some(body),
436                    ..
437                } = &def.kind
438                else {
439                    panic!("missing shim for closure")
440                };
441                let mut bt_ctx = BodyTransCtx::new(&mut self);
442                match bt_ctx.translate_body(span, body, &def.source_text) {
443                    Ok(Ok(body)) => Ok(body),
444                    Ok(Err(Opaque)) => Err(Opaque),
445                    Err(_) => Err(Opaque),
446                }
447            }
448            // Target translation:
449            //
450            // fn call_mut(state: &mut Self, args: Args) -> Output {
451            //   let reborrow = &*state;
452            //   self.call(reborrow, args)
453            // }
454            (FnMut, Fn) => {
455                let fun_id: FunDeclId = self.register_item(
456                    span,
457                    def.this(),
458                    TransItemSourceKind::ClosureMethod(closure_kind),
459                );
460                let impl_ref = self.translate_closure_impl_ref(span, args, closure_kind)?;
461                // TODO: make a trait call to avoid needing to concatenate things ourselves.
462                // TODO: can we ask hax for the trait ref?
463                let fn_op = FnOperand::Regular(FnPtr {
464                    func: Box::new(fun_id.into()),
465                    generics: Box::new(impl_ref.generics.concat(&GenericArgs {
466                        regions: vec![Region::Erased].into(),
467                        ..GenericArgs::empty()
468                    })),
469                });
470
471                let mut locals = Locals {
472                    arg_count: 2,
473                    locals: Vector::new(),
474                };
475                let mut statements = vec![];
476                let mut blocks = Vector::default();
477
478                let output = locals.new_var(None, signature.output.clone());
479                let state = locals.new_var(Some("state".to_string()), signature.inputs[0].clone());
480                let args = locals.new_var(Some("args".to_string()), signature.inputs[1].clone());
481                let deref_state = state.deref();
482                let reborrow_ty =
483                    TyKind::Ref(Region::Erased, deref_state.ty.clone(), RefKind::Shared).into_ty();
484                let reborrow = locals.new_var(None, reborrow_ty);
485
486                statements.push(mk_stt(RawStatement::Assign(
487                    reborrow.clone(),
488                    Rvalue::Ref(deref_state, BorrowKind::Shared),
489                )));
490
491                let start_block = blocks.reserve_slot();
492                let ret_block = blocks.push(mk_block(vec![], RawTerminator::Return));
493                let unwind_block = blocks.push(mk_block(vec![], RawTerminator::UnwindResume));
494                let call = RawTerminator::Call {
495                    target: ret_block,
496                    call: Call {
497                        func: fn_op,
498                        args: vec![Operand::Move(reborrow), Operand::Move(args)],
499                        dest: output,
500                    },
501                    on_unwind: unwind_block,
502                };
503                blocks.set_slot(start_block, mk_block(statements, call));
504
505                let body: ExprBody = GExprBody {
506                    span,
507                    locals,
508                    comments: vec![],
509                    body: blocks,
510                };
511                Ok(Body::Unstructured(body))
512            }
513            (Fn, FnOnce) | (Fn, FnMut) | (FnMut, FnOnce) => {
514                panic!(
515                    "Can't make a closure body for a more restrictive kind \
516                    than the closure kind"
517                )
518            }
519        })
520    }
521
522    /// Given an item that is a closure, generate the `call_once`/`call_mut`/`call` method
523    /// (depending on `target_kind`).
524    #[tracing::instrument(skip(self, item_meta))]
525    pub fn translate_closure_method(
526        mut self,
527        def_id: FunDeclId,
528        item_meta: ItemMeta,
529        def: &hax::FullDef,
530        target_kind: ClosureKind,
531    ) -> Result<FunDecl, Error> {
532        let span = item_meta.span;
533        let hax::FullDefKind::Closure {
534            args,
535            fn_once_impl,
536            fn_mut_impl,
537            fn_impl,
538            ..
539        } = &def.kind
540        else {
541            unreachable!()
542        };
543
544        trace!("About to translate closure:\n{:?}", def.def_id());
545
546        self.translate_def_generics(span, def)?;
547        // Add the lifetime generics coming from the higher-kindedness of the signature.
548        assert!(self.innermost_binder_mut().bound_region_vars.is_empty(),);
549        self.innermost_binder_mut()
550            .push_params_from_binder(args.fn_sig.rebind(()))?;
551
552        // Hax gives us trait-related information for the impl we're building.
553        let vimpl = match target_kind {
554            ClosureKind::FnOnce => fn_once_impl,
555            ClosureKind::FnMut => fn_mut_impl.as_ref().unwrap(),
556            ClosureKind::Fn => fn_impl.as_ref().unwrap(),
557        };
558        let implemented_trait = self.translate_trait_predicate(span, &vimpl.trait_pred)?;
559
560        let impl_ref = self.translate_closure_impl_ref(span, args, target_kind)?;
561        let kind = ItemKind::TraitImpl {
562            impl_ref,
563            trait_ref: implemented_trait,
564            item_name: TraitItemName(target_kind.method_name().to_owned()),
565            reuses_default: false,
566        };
567
568        // Translate the function signature
569        let signature = self.translate_closure_method_sig(def, span, args, target_kind)?;
570
571        let body = if item_meta.opacity.with_private_contents().is_opaque() {
572            Err(Opaque)
573        } else {
574            self.translate_closure_method_body(span, def, target_kind, args, &signature)?
575        };
576
577        Ok(FunDecl {
578            def_id,
579            item_meta,
580            signature,
581            kind,
582            is_global_initializer: None,
583            body,
584        })
585    }
586
587    #[tracing::instrument(skip(self, item_meta))]
588    pub fn translate_closure_trait_impl(
589        mut self,
590        def_id: TraitImplId,
591        item_meta: ItemMeta,
592        def: &hax::FullDef,
593        target_kind: ClosureKind,
594    ) -> Result<TraitImpl, Error> {
595        let span = item_meta.span;
596        let hax::FullDefKind::Closure {
597            args,
598            fn_once_impl,
599            fn_mut_impl,
600            fn_impl,
601            ..
602        } = &def.kind
603        else {
604            unreachable!()
605        };
606
607        self.translate_def_generics(span, def)?;
608        // Add the lifetime generics coming from the higher-kindedness of the signature.
609        assert!(self.innermost_binder_mut().bound_region_vars.is_empty());
610        self.innermost_binder_mut()
611            .push_params_from_binder(args.fn_sig.rebind(()))?;
612
613        // Hax gives us trait-related information for the impl we're building.
614        let vimpl = match target_kind {
615            ClosureKind::FnOnce => fn_once_impl,
616            ClosureKind::FnMut => fn_mut_impl.as_ref().unwrap(),
617            ClosureKind::Fn => fn_impl.as_ref().unwrap(),
618        };
619        let mut timpl = self.translate_virtual_trait_impl(def_id, item_meta, vimpl)?;
620
621        // Construct the `call_*` method reference.
622        let call_fn_id = self.register_item(
623            span,
624            def.this(),
625            TransItemSourceKind::ClosureMethod(target_kind),
626        );
627        let call_fn_name = TraitItemName(target_kind.method_name().to_string());
628        let call_fn_binder = {
629            let mut method_params = GenericParams::empty();
630            match target_kind {
631                ClosureKind::FnOnce => {}
632                ClosureKind::FnMut | ClosureKind::Fn => {
633                    method_params
634                        .regions
635                        .push_with(|index| RegionVar { index, name: None });
636                }
637            };
638
639            let generics = self
640                .outermost_binder()
641                .params
642                .identity_args_at_depth(DeBruijnId::one())
643                .concat(&method_params.identity_args_at_depth(DeBruijnId::zero()));
644            Binder::new(
645                BinderKind::TraitMethod(timpl.impl_trait.id, call_fn_name.clone()),
646                method_params,
647                FunDeclRef {
648                    id: call_fn_id,
649                    generics: Box::new(generics),
650                },
651            )
652        };
653        timpl.methods.push((call_fn_name, call_fn_binder));
654
655        Ok(timpl)
656    }
657
658    /// Given an item that is a non-capturing closure, generate the equivalent function,
659    /// by removing the state from the parameters and untupling the arguments.
660    #[tracing::instrument(skip(self, item_meta))]
661    pub fn translate_stateless_closure_as_fn(
662        mut self,
663        def_id: FunDeclId,
664        item_meta: ItemMeta,
665        def: &hax::FullDef,
666    ) -> Result<FunDecl, Error> {
667        let span = item_meta.span;
668        let hax::FullDefKind::Closure { args: closure, .. } = &def.kind else {
669            unreachable!()
670        };
671
672        trace!("About to translate closure as fn:\n{:?}", def.def_id());
673
674        assert!(
675            closure.upvar_tys.is_empty(),
676            "Only stateless closures can be translated as functions"
677        );
678
679        self.translate_def_generics(span, def)?;
680        // Add the lifetime generics coming from the higher-kindedness of the signature.
681        assert!(self.innermost_binder_mut().bound_region_vars.is_empty(),);
682        self.innermost_binder_mut()
683            .push_params_from_binder(closure.fn_sig.rebind(()))?;
684
685        // Translate the function signature
686        let mut signature =
687            self.translate_closure_method_sig(def, span, closure, ClosureKind::FnOnce)?;
688        let state_ty = signature.inputs.remove(0);
689        let args_tuple_ty = signature.inputs.remove(0);
690        signature.inputs = args_tuple_ty.as_tuple().unwrap().iter().cloned().collect();
691
692        let body = if item_meta.opacity.with_private_contents().is_opaque() {
693            Err(Opaque)
694        } else {
695            // Target translation:
696            //
697            // fn call_fn(arg0: Args[0], ..., argN: Args[N]) -> Output {
698            //   let closure: Closure = {};
699            //   let args = (arg0, ..., argN);
700            //   closure.call(args)
701            // }
702            let mk_stt = |content| Statement::new(span, content);
703            let mk_block = |statements, terminator| -> BlockData {
704                BlockData {
705                    statements,
706                    terminator: Terminator::new(span, terminator),
707                }
708            };
709            let fun_id: FunDeclId = self.register_item(
710                span,
711                def.this(),
712                TransItemSourceKind::ClosureMethod(ClosureKind::FnOnce),
713            );
714            let impl_ref = self.translate_closure_impl_ref(span, closure, ClosureKind::FnOnce)?;
715            let fn_op = FnOperand::Regular(FnPtr {
716                func: Box::new(fun_id.into()),
717                generics: impl_ref.generics.clone(),
718            });
719
720            let mut locals = Locals {
721                arg_count: signature.inputs.len(),
722                locals: Vector::new(),
723            };
724            let mut statements = vec![];
725            let mut blocks = Vector::default();
726
727            let output = locals.new_var(None, signature.output.clone());
728            let args: Vec<Place> = signature
729                .inputs
730                .iter()
731                .enumerate()
732                .map(|(i, ty)| locals.new_var(Some(format!("arg{}", i + 1)), ty.clone()))
733                .collect();
734            let args_tupled = locals.new_var(Some("args".to_string()), args_tuple_ty.clone());
735            let state = locals.new_var(Some("state".to_string()), state_ty.clone());
736
737            statements.push(mk_stt(RawStatement::Assign(
738                args_tupled.clone(),
739                Rvalue::Aggregate(
740                    AggregateKind::Adt(args_tuple_ty.as_adt().unwrap().clone(), None, None),
741                    args.into_iter().map(Operand::Move).collect(),
742                ),
743            )));
744
745            let state_ty_adt = state_ty.as_adt().unwrap();
746            statements.push(mk_stt(RawStatement::Assign(
747                state.clone(),
748                Rvalue::Aggregate(AggregateKind::Adt(state_ty_adt.clone(), None, None), vec![]),
749            )));
750
751            let start_block = blocks.reserve_slot();
752            let ret_block = blocks.push(mk_block(vec![], RawTerminator::Return));
753            let unwind_block = blocks.push(mk_block(vec![], RawTerminator::UnwindResume));
754            let call = RawTerminator::Call {
755                target: ret_block,
756                call: Call {
757                    func: fn_op,
758                    args: vec![Operand::Move(state), Operand::Move(args_tupled)],
759                    dest: output,
760                },
761                on_unwind: unwind_block,
762            };
763            blocks.set_slot(start_block, mk_block(statements, call));
764
765            let body: ExprBody = GExprBody {
766                span,
767                locals,
768                comments: vec![],
769                body: blocks,
770            };
771            Ok(Body::Unstructured(body))
772        };
773
774        Ok(FunDecl {
775            def_id,
776            item_meta,
777            signature,
778            kind: ItemKind::TopLevel,
779            is_global_initializer: None,
780            body,
781        })
782    }
783}
charon_driver/translate/translate_closures.rs

charon_driver/translate/
translate_closures.rs
