charon_driver/translate/
translate_bodies.rs

1//! Translate functions from the rust compiler MIR to our internal representation.
2//! Our internal representation is very close to MIR, but is more convenient for
3//! us to handle, and easier to maintain - rustc's representation can evolve
4//! independently.
5
6use std::collections::HashMap;
7use std::collections::VecDeque;
8use std::mem;
9use std::ops::Deref;
10use std::ops::DerefMut;
11use std::panic;
12
13use super::translate_crate::*;
14use super::translate_ctx::*;
15use charon_lib::ast::ullbc_ast::StatementKind;
16use charon_lib::ast::*;
17use charon_lib::formatter::FmtCtx;
18use charon_lib::formatter::IntoFormatter;
19use charon_lib::ids::Vector;
20use charon_lib::pretty::FmtWithCtx;
21use charon_lib::ullbc_ast::*;
22use hax::UnwindAction;
23use itertools::Itertools;
24use rustc_middle::mir;
25
26/// A translation context for function bodies.
27pub(crate) struct BodyTransCtx<'tcx, 'tctx, 'ictx> {
28    /// The translation context for the item.
29    pub i_ctx: &'ictx mut ItemTransCtx<'tcx, 'tctx>,
30
31    /// The (regular) variables in the current function body.
32    pub locals: Locals,
33    /// The map from rust variable indices to translated variables indices.
34    pub locals_map: HashMap<usize, LocalId>,
35    /// The translated blocks.
36    pub blocks: Vector<BlockId, BlockData>,
37    /// The map from rust blocks to translated blocks.
38    /// Note that when translating terminators like DropAndReplace, we might have
39    /// to introduce new blocks which don't appear in the original MIR.
40    pub blocks_map: HashMap<hax::BasicBlock, BlockId>,
41    /// We register the blocks to translate in a stack, so as to avoid
42    /// writing the translation functions as recursive functions. We do
43    /// so because we had stack overflows in the past.
44    pub blocks_stack: VecDeque<hax::BasicBlock>,
45}
46
47impl<'tcx, 'tctx, 'ictx> BodyTransCtx<'tcx, 'tctx, 'ictx> {
48    pub(crate) fn new(i_ctx: &'ictx mut ItemTransCtx<'tcx, 'tctx>) -> Self {
49        BodyTransCtx {
50            i_ctx,
51            locals: Default::default(),
52            locals_map: Default::default(),
53            blocks: Default::default(),
54            blocks_map: Default::default(),
55            blocks_stack: Default::default(),
56        }
57    }
58}
59
60impl<'tcx, 'tctx, 'ictx> Deref for BodyTransCtx<'tcx, 'tctx, 'ictx> {
61    type Target = ItemTransCtx<'tcx, 'tctx>;
62    fn deref(&self) -> &Self::Target {
63        self.i_ctx
64    }
65}
66impl<'tcx, 'tctx, 'ictx> DerefMut for BodyTransCtx<'tcx, 'tctx, 'ictx> {
67    fn deref_mut(&mut self) -> &mut Self::Target {
68        self.i_ctx
69    }
70}
71
72fn translate_variant_id(id: hax::VariantIdx) -> VariantId {
73    VariantId::new(id)
74}
75
76fn translate_field_id(id: hax::FieldIdx) -> FieldId {
77    use rustc_index::Idx;
78    FieldId::new(id.index())
79}
80
81/// Translate a `BorrowKind`
82fn translate_borrow_kind(borrow_kind: hax::BorrowKind) -> BorrowKind {
83    match borrow_kind {
84        hax::BorrowKind::Shared => BorrowKind::Shared,
85        hax::BorrowKind::Mut { kind } => match kind {
86            hax::MutBorrowKind::Default => BorrowKind::Mut,
87            hax::MutBorrowKind::TwoPhaseBorrow => BorrowKind::TwoPhaseMut,
88            hax::MutBorrowKind::ClosureCapture => BorrowKind::UniqueImmutable,
89        },
90        hax::BorrowKind::Fake(hax::FakeBorrowKind::Shallow) => BorrowKind::Shallow,
91        // This one is used only in deref patterns.
92        hax::BorrowKind::Fake(hax::FakeBorrowKind::Deep) => unimplemented!(),
93    }
94}
95
96impl BodyTransCtx<'_, '_, '_> {
97    pub(crate) fn translate_local(&self, local: &hax::Local) -> Option<LocalId> {
98        use rustc_index::Idx;
99        self.locals_map.get(&local.index()).copied()
100    }
101
102    pub(crate) fn push_var(&mut self, rid: usize, ty: Ty, name: Option<String>) {
103        let local_id = self
104            .locals
105            .locals
106            .push_with(|index| Local { index, name, ty });
107        self.locals_map.insert(rid, local_id);
108    }
109
110    fn translate_binaryop_kind(&mut self, _span: Span, binop: hax::BinOp) -> Result<BinOp, Error> {
111        Ok(match binop {
112            hax::BinOp::BitXor => BinOp::BitXor,
113            hax::BinOp::BitAnd => BinOp::BitAnd,
114            hax::BinOp::BitOr => BinOp::BitOr,
115            hax::BinOp::Eq => BinOp::Eq,
116            hax::BinOp::Lt => BinOp::Lt,
117            hax::BinOp::Le => BinOp::Le,
118            hax::BinOp::Ne => BinOp::Ne,
119            hax::BinOp::Ge => BinOp::Ge,
120            hax::BinOp::Gt => BinOp::Gt,
121            hax::BinOp::Add => BinOp::Add(OverflowMode::Wrap),
122            hax::BinOp::AddUnchecked => BinOp::Add(OverflowMode::UB),
123            hax::BinOp::Sub => BinOp::Sub(OverflowMode::Wrap),
124            hax::BinOp::SubUnchecked => BinOp::Sub(OverflowMode::UB),
125            hax::BinOp::Mul => BinOp::Mul(OverflowMode::Wrap),
126            hax::BinOp::MulUnchecked => BinOp::Mul(OverflowMode::UB),
127            hax::BinOp::Div => BinOp::Div(OverflowMode::UB),
128            hax::BinOp::Rem => BinOp::Rem(OverflowMode::UB),
129            hax::BinOp::AddWithOverflow => BinOp::AddChecked,
130            hax::BinOp::SubWithOverflow => BinOp::SubChecked,
131            hax::BinOp::MulWithOverflow => BinOp::MulChecked,
132            hax::BinOp::Shl => BinOp::Shl(OverflowMode::Wrap),
133            hax::BinOp::ShlUnchecked => BinOp::Shl(OverflowMode::UB),
134            hax::BinOp::Shr => BinOp::Shr(OverflowMode::Wrap),
135            hax::BinOp::ShrUnchecked => BinOp::Shr(OverflowMode::UB),
136            hax::BinOp::Cmp => BinOp::Cmp,
137            hax::BinOp::Offset => BinOp::Offset,
138        })
139    }
140
141    /// Translate a function's local variables by adding them in the environment.
142    fn translate_body_locals(
143        &mut self,
144        body: &hax::MirBody<hax::mir_kinds::Unknown>,
145    ) -> Result<(), Error> {
146        // Translate the parameters
147        for (index, var) in body.local_decls.raw.iter().enumerate() {
148            trace!("Translating local of index {} and type {:?}", index, var.ty);
149
150            // Find the name of the variable
151            let name: Option<String> = var.name.clone();
152
153            // Translate the type
154            let span = self.translate_span_from_hax(&var.source_info.span);
155            let ty = self.translate_ty(span, &var.ty)?;
156
157            // Add the variable to the environment
158            self.push_var(index, ty, name);
159        }
160
161        Ok(())
162    }
163
164    /// Translate a basic block id and register it, if it hasn't been done.
165    fn translate_basic_block_id(&mut self, block_id: hax::BasicBlock) -> BlockId {
166        match self.blocks_map.get(&block_id) {
167            Some(id) => *id,
168            // Generate a fresh id - this also registers the block
169            None => {
170                // Push to the stack of blocks awaiting translation
171                self.blocks_stack.push_back(block_id);
172                let id = self.blocks.reserve_slot();
173                // Insert in the map
174                self.blocks_map.insert(block_id, id);
175                id
176            }
177        }
178    }
179
180    fn translate_basic_block(
181        &mut self,
182        body: &hax::MirBody<hax::mir_kinds::Unknown>,
183        block: &hax::BasicBlockData,
184    ) -> Result<BlockData, Error> {
185        // Translate the statements
186        let mut statements = Vec::new();
187        for statement in &block.statements {
188            trace!("statement: {:?}", statement);
189
190            // Some statements might be ignored, hence the optional returned value
191            let opt_statement = self.translate_statement(body, statement)?;
192            if let Some(statement) = opt_statement {
193                statements.push(statement)
194            }
195        }
196
197        // Translate the terminator
198        let terminator = block.terminator.as_ref().unwrap();
199        let terminator = self.translate_terminator(body, terminator, &mut statements)?;
200
201        Ok(BlockData {
202            statements,
203            terminator,
204        })
205    }
206
207    /// Translate a place
208    /// TODO: Hax represents places in a different manner than MIR. We should
209    /// update our representation of places to match the Hax representation.
210    fn translate_place(&mut self, span: Span, place: &hax::Place) -> Result<Place, Error> {
211        match &place.kind {
212            hax::PlaceKind::Local(local) => {
213                let var_id = self.translate_local(local).unwrap();
214                Ok(self.locals.place_for_var(var_id))
215            }
216            hax::PlaceKind::Projection {
217                place: hax_subplace,
218                kind,
219            } => {
220                let ty = self.translate_ty(span, &place.ty)?;
221                // Compute the type of the value *before* projection - we use this
222                // to disambiguate
223                let subplace = self.translate_place(span, hax_subplace)?;
224                let ptr_size = self.t_ctx.translated.target_information.target_pointer_size;
225                let place = match kind {
226                    hax::ProjectionElem::Deref => subplace.project(ProjectionElem::Deref, ty),
227                    hax::ProjectionElem::Field(field_kind) => {
228                        use hax::ProjectionElemFieldKind::*;
229                        let proj_elem = match field_kind {
230                            Tuple(id) => {
231                                let tref = subplace.ty().kind().as_adt().unwrap();
232                                let field_id = translate_field_id(*id);
233                                let proj_kind =
234                                    FieldProjKind::Tuple(tref.generics.types.elem_count());
235                                ProjectionElem::Field(proj_kind, field_id)
236                            }
237                            Adt {
238                                typ: _,
239                                variant,
240                                index,
241                            } => {
242                                let field_id = translate_field_id(*index);
243                                let variant_id = variant.map(translate_variant_id);
244                                let tref = subplace.ty().kind().as_adt().unwrap();
245                                let generics = &tref.generics;
246                                match tref.id {
247                                    TypeId::Adt(type_id) => {
248                                        let proj_kind = FieldProjKind::Adt(type_id, variant_id);
249                                        ProjectionElem::Field(proj_kind, field_id)
250                                    }
251                                    TypeId::Tuple => {
252                                        assert!(generics.regions.is_empty());
253                                        assert!(variant.is_none());
254                                        assert!(generics.const_generics.is_empty());
255                                        let proj_kind =
256                                            FieldProjKind::Tuple(generics.types.elem_count());
257                                        ProjectionElem::Field(proj_kind, field_id)
258                                    }
259                                    TypeId::Builtin(BuiltinTy::Box) => {
260                                        // Some sanity checks
261                                        assert!(generics.regions.is_empty());
262                                        assert!(generics.types.elem_count() == 2);
263                                        assert!(generics.const_generics.is_empty());
264                                        assert!(field_id == FieldId::ZERO);
265                                        // We pretend this is a deref.
266                                        ProjectionElem::Deref
267                                    }
268                                    _ => raise_error!(self, span, "Unexpected field projection"),
269                                }
270                            }
271                            ClosureState(index) => {
272                                let field_id = translate_field_id(*index);
273                                let type_id = *subplace
274                                    .ty
275                                    .kind()
276                                    .as_adt()
277                                    .expect("ClosureState projection should apply to an Adt type")
278                                    .id
279                                    .as_adt()
280                                    .unwrap();
281                                ProjectionElem::Field(FieldProjKind::Adt(type_id, None), field_id)
282                            }
283                        };
284                        subplace.project(proj_elem, ty)
285                    }
286                    hax::ProjectionElem::Index(local) => {
287                        let var_id = self.translate_local(local).unwrap();
288                        let local = self.locals.place_for_var(var_id);
289                        let offset = Operand::Copy(local);
290                        subplace.project(
291                            ProjectionElem::Index {
292                                offset: Box::new(offset),
293                                from_end: false,
294                            },
295                            ty,
296                        )
297                    }
298                    hax::ProjectionElem::Downcast(..) => {
299                        // We view it as a nop (the information from the
300                        // downcast has been propagated to the other
301                        // projection elements by Hax)
302                        subplace
303                    }
304                    &hax::ProjectionElem::ConstantIndex {
305                        offset,
306                        from_end,
307                        min_length: _,
308                    } => {
309                        let offset = Operand::Const(Box::new(
310                            ScalarValue::from_uint(ptr_size, UIntTy::Usize, offset as u128)
311                                .unwrap()
312                                .to_constant(),
313                        ));
314                        subplace.project(
315                            ProjectionElem::Index {
316                                offset: Box::new(offset),
317                                from_end,
318                            },
319                            ty,
320                        )
321                    }
322                    &hax::ProjectionElem::Subslice { from, to, from_end } => {
323                        let from = Operand::Const(Box::new(
324                            ScalarValue::from_uint(ptr_size, UIntTy::Usize, from as u128)
325                                .unwrap()
326                                .to_constant(),
327                        ));
328                        let to = Operand::Const(Box::new(
329                            ScalarValue::from_uint(ptr_size, UIntTy::Usize, to as u128)
330                                .unwrap()
331                                .to_constant(),
332                        ));
333                        subplace.project(
334                            ProjectionElem::Subslice {
335                                from: Box::new(from),
336                                to: Box::new(to),
337                                from_end,
338                            },
339                            ty,
340                        )
341                    }
342                    hax::ProjectionElem::OpaqueCast => {
343                        // Don't know what that is
344                        raise_error!(self, span, "Unexpected ProjectionElem::OpaqueCast");
345                    }
346                };
347
348                // Return
349                Ok(place)
350            }
351        }
352    }
353
354    /// Translate an operand with its type
355    fn translate_operand_with_type(
356        &mut self,
357        span: Span,
358        operand: &hax::Operand,
359    ) -> Result<(Operand, Ty), Error> {
360        trace!();
361        match operand {
362            hax::Operand::Copy(place) => {
363                let p = self.translate_place(span, place)?;
364                let ty = p.ty().clone();
365                Ok((Operand::Copy(p), ty))
366            }
367            hax::Operand::Move(place) => {
368                let p = self.translate_place(span, place)?;
369                let ty = p.ty().clone();
370                Ok((Operand::Move(p), ty))
371            }
372            hax::Operand::Constant(const_op) => match &const_op.kind {
373                hax::ConstOperandKind::Value(constant) => {
374                    let constant = self.translate_constant_expr_to_constant_expr(span, constant)?;
375                    let ty = constant.ty.clone();
376                    Ok((Operand::Const(Box::new(constant)), ty))
377                }
378                hax::ConstOperandKind::Promoted(item) => {
379                    let ty = self.translate_ty(span, &const_op.ty)?;
380                    // A promoted constant that could not be evaluated.
381                    let global_ref = self.translate_global_decl_ref(span, item)?;
382                    let constant = ConstantExpr {
383                        kind: ConstantExprKind::Global(global_ref),
384                        ty: ty.clone(),
385                    };
386                    Ok((Operand::Const(Box::new(constant)), ty))
387                }
388            },
389        }
390    }
391
392    /// Translate an operand
393    fn translate_operand(&mut self, span: Span, operand: &hax::Operand) -> Result<Operand, Error> {
394        trace!();
395        Ok(self.translate_operand_with_type(span, operand)?.0)
396    }
397
398    /// Translate an rvalue
399    fn translate_rvalue(
400        &mut self,
401        span: Span,
402        rvalue: &hax::Rvalue,
403        tgt_ty: &Ty,
404    ) -> Result<Rvalue, Error> {
405        match rvalue {
406            hax::Rvalue::Use(operand) => Ok(Rvalue::Use(self.translate_operand(span, operand)?)),
407            hax::Rvalue::CopyForDeref(place) => {
408                // According to the documentation, it seems to be an optimisation
409                // for drop elaboration. We treat it as a regular copy.
410                let place = self.translate_place(span, place)?;
411                Ok(Rvalue::Use(Operand::Copy(place)))
412            }
413            hax::Rvalue::Repeat(operand, cnst) => {
414                let c = self.translate_constant_expr_to_const_generic(span, cnst)?;
415                let (operand, t) = self.translate_operand_with_type(span, operand)?;
416                // Remark: we could desugar this into a function call later.
417                Ok(Rvalue::Repeat(operand, t, c))
418            }
419            hax::Rvalue::Ref(_region, borrow_kind, place) => {
420                let place = self.translate_place(span, place)?;
421                let borrow_kind = translate_borrow_kind(*borrow_kind);
422                Ok(Rvalue::Ref {
423                    place,
424                    kind: borrow_kind,
425                    // Use `()` as a placeholder now.
426                    // Will be fixed by the cleanup pass `insert_ptr_metadata`.
427                    ptr_metadata: Operand::mk_const_unit(),
428                })
429            }
430            hax::Rvalue::RawPtr(mtbl, place) => {
431                let mtbl = match mtbl {
432                    hax::RawPtrKind::Mut => RefKind::Mut,
433                    hax::RawPtrKind::Const => RefKind::Shared,
434                    hax::RawPtrKind::FakeForPtrMetadata => RefKind::Shared,
435                };
436                let place = self.translate_place(span, place)?;
437                Ok(Rvalue::RawPtr {
438                    place,
439                    kind: mtbl,
440                    // Use `()` as a placeholder now.
441                    // Will be fixed by the cleanup pass `insert_ptr_metadata`.
442                    ptr_metadata: Operand::mk_const_unit(),
443                })
444            }
445            hax::Rvalue::Len(place) => {
446                let place = self.translate_place(span, place)?;
447                let ty = place.ty().clone();
448                let tref = ty.as_adt().unwrap();
449                let cg = match tref.id {
450                    TypeId::Builtin(BuiltinTy::Array) => {
451                        Some(tref.generics.const_generics[0].clone())
452                    }
453                    TypeId::Builtin(BuiltinTy::Slice) => None,
454                    _ => unreachable!(),
455                };
456                Ok(Rvalue::Len(place, ty, cg))
457            }
458            hax::Rvalue::Cast(cast_kind, hax_operand, tgt_ty) => {
459                trace!("Rvalue::Cast: {:?}", rvalue);
460                // Translate the target type
461                let tgt_ty = self.translate_ty(span, tgt_ty)?;
462
463                // Translate the operand
464                let (mut operand, src_ty) = self.translate_operand_with_type(span, hax_operand)?;
465
466                let cast_kind = match cast_kind {
467                    hax::CastKind::IntToInt
468                    | hax::CastKind::IntToFloat
469                    | hax::CastKind::FloatToInt
470                    | hax::CastKind::FloatToFloat => {
471                        let tgt_ty = *tgt_ty.kind().as_literal().unwrap();
472                        let src_ty = *src_ty.kind().as_literal().unwrap();
473                        CastKind::Scalar(src_ty, tgt_ty)
474                    }
475                    hax::CastKind::PtrToPtr
476                    | hax::CastKind::PointerCoercion(hax::PointerCoercion::MutToConstPointer, ..)
477                    | hax::CastKind::PointerCoercion(hax::PointerCoercion::ArrayToPointer, ..)
478                    | hax::CastKind::FnPtrToPtr
479                    | hax::CastKind::PointerExposeProvenance
480                    | hax::CastKind::PointerWithExposedProvenance => {
481                        CastKind::RawPtr(src_ty, tgt_ty)
482                    }
483                    hax::CastKind::PointerCoercion(
484                        hax::PointerCoercion::ClosureFnPointer(_),
485                        ..,
486                    ) => {
487                        // We model casts of closures to function pointers by generating a new
488                        // function item without the closure's state, that calls the actual closure.
489                        let op_ty = match hax_operand {
490                            hax::Operand::Move(p) | hax::Operand::Copy(p) => p.ty.kind(),
491                            hax::Operand::Constant(c) => c.ty.kind(),
492                        };
493                        let hax::TyKind::Closure(closure) = op_ty else {
494                            unreachable!("Non-closure type in PointerCoercion::ClosureFnPointer");
495                        };
496                        let fn_ref = self.translate_stateless_closure_as_fn_ref(span, closure)?;
497                        let fn_ptr_bound = fn_ref.map(FunDeclRef::into);
498                        let fn_ptr: FnPtr = fn_ptr_bound.clone().erase();
499                        let src_ty = TyKind::FnDef(fn_ptr_bound).into_ty();
500                        operand = Operand::Const(Box::new(ConstantExpr {
501                            kind: ConstantExprKind::FnPtr(fn_ptr),
502                            ty: src_ty.clone(),
503                        }));
504                        CastKind::FnPtr(src_ty, tgt_ty)
505                    }
506                    hax::CastKind::PointerCoercion(
507                        hax::PointerCoercion::UnsafeFnPointer
508                        | hax::PointerCoercion::ReifyFnPointer,
509                        ..,
510                    ) => CastKind::FnPtr(src_ty, tgt_ty),
511                    hax::CastKind::Transmute => CastKind::Transmute(src_ty, tgt_ty),
512                    hax::CastKind::PointerCoercion(hax::PointerCoercion::Unsize(meta), ..) => {
513                        let meta = match meta {
514                            hax::UnsizingMetadata::Length(len) => {
515                                let len =
516                                    self.translate_constant_expr_to_const_generic(span, len)?;
517                                UnsizingMetadata::Length(len)
518                            }
519                            hax::UnsizingMetadata::VTablePtr(impl_expr) => {
520                                let tref = self.translate_trait_impl_expr(span, impl_expr)?;
521                                match &impl_expr.r#impl {
522                                    hax::ImplExprAtom::Concrete(tref) => {
523                                        // Ensure the vtable type is translated.
524                                        let _: GlobalDeclId = self.register_item(
525                                            span,
526                                            tref,
527                                            TransItemSourceKind::VTableInstance(
528                                                TraitImplSource::Normal,
529                                            ),
530                                        );
531                                    }
532                                    // TODO(dyn): more ways of registering vtable instance?
533                                    _ => {
534                                        trace!(
535                                            "impl_expr not triggering registering vtable: {:?}",
536                                            impl_expr
537                                        )
538                                    }
539                                };
540                                UnsizingMetadata::VTablePtr(tref)
541                            }
542                            hax::UnsizingMetadata::Unknown => UnsizingMetadata::Unknown,
543                        };
544                        CastKind::Unsize(src_ty.clone(), tgt_ty.clone(), meta)
545                    }
546                };
547                let unop = UnOp::Cast(cast_kind);
548                Ok(Rvalue::UnaryOp(unop, operand))
549            }
550            hax::Rvalue::BinaryOp(binop, (left, right)) => Ok(Rvalue::BinaryOp(
551                self.translate_binaryop_kind(span, *binop)?,
552                self.translate_operand(span, left)?,
553                self.translate_operand(span, right)?,
554            )),
555            hax::Rvalue::NullaryOp(nullop, ty) => {
556                trace!("NullOp: {:?}", nullop);
557                let ty = self.translate_ty(span, ty)?;
558                let op = match nullop {
559                    hax::NullOp::SizeOf => NullOp::SizeOf,
560                    hax::NullOp::AlignOf => NullOp::AlignOf,
561                    hax::NullOp::OffsetOf(fields) => NullOp::OffsetOf(
562                        fields
563                            .iter()
564                            .copied()
565                            .map(|(n, idx)| (n, translate_field_id(idx)))
566                            .collect(),
567                    ),
568                    hax::NullOp::UbChecks => NullOp::UbChecks,
569                    hax::NullOp::ContractChecks => {
570                        raise_error!(self, span, "charon does not support contracts");
571                    }
572                };
573                Ok(Rvalue::NullaryOp(op, ty))
574            }
575            hax::Rvalue::UnaryOp(unop, operand) => {
576                let operand = self.translate_operand(span, operand)?;
577                let unop = match unop {
578                    hax::UnOp::Not => UnOp::Not,
579                    hax::UnOp::Neg => UnOp::Neg(OverflowMode::Wrap),
580                    hax::UnOp::PtrMetadata => match operand {
581                        Operand::Copy(p) | Operand::Move(p) => {
582                            return Ok(Rvalue::Use(Operand::Copy(
583                                p.project(ProjectionElem::PtrMetadata, tgt_ty.clone()),
584                            )));
585                        }
586                        Operand::Const(_) => panic!("const metadata"),
587                    },
588                };
589                Ok(Rvalue::UnaryOp(unop, operand))
590            }
591            hax::Rvalue::Discriminant(place) => {
592                let place = self.translate_place(span, place)?;
593                // We should always know the enum type; it can't be a generic.
594                if !place
595                    .ty()
596                    .kind()
597                    .as_adt()
598                    .is_some_and(|tref| tref.id.is_adt())
599                {
600                    raise_error!(
601                        self,
602                        span,
603                        "Unexpected scrutinee type for ReadDiscriminant: {}",
604                        place.ty().with_ctx(&self.into_fmt())
605                    )
606                }
607                Ok(Rvalue::Discriminant(place))
608            }
609            hax::Rvalue::Aggregate(aggregate_kind, operands) => {
610                // It seems this instruction is not present in certain passes:
611                // for example, it seems it is not used in optimized MIR, where
612                // ADT initialization is split into several instructions, for
613                // instance:
614                // ```
615                // p = Pair { x:xv, y:yv };
616                // ```
617                // Might become:
618                // ```
619                // p.x = x;
620                // p.y = yv;
621                // ```
622
623                // First translate the operands
624                let operands_t: Vec<Operand> = operands
625                    .raw
626                    .iter()
627                    .map(|op| self.translate_operand(span, op))
628                    .try_collect()?;
629                let ptr_size = self.t_ctx.translated.target_information.target_pointer_size;
630
631                match aggregate_kind {
632                    hax::AggregateKind::Array(ty) => {
633                        let t_ty = self.translate_ty(span, ty)?;
634                        let cg = ConstGeneric::Value(Literal::Scalar(
635                            ScalarValue::from_uint(
636                                ptr_size,
637                                UIntTy::Usize,
638                                operands_t.len() as u128,
639                            )
640                            .unwrap(),
641                        ));
642                        Ok(Rvalue::Aggregate(
643                            AggregateKind::Array(t_ty, cg),
644                            operands_t,
645                        ))
646                    }
647                    hax::AggregateKind::Tuple => {
648                        let tref = TypeDeclRef::new(TypeId::Tuple, GenericArgs::empty());
649                        Ok(Rvalue::Aggregate(
650                            AggregateKind::Adt(tref, None, None),
651                            operands_t,
652                        ))
653                    }
654                    hax::AggregateKind::Adt(
655                        item,
656                        variant_idx,
657                        kind,
658                        _user_annotation,
659                        field_index,
660                    ) => {
661                        use hax::AdtKind;
662                        trace!("{:?}", rvalue);
663
664                        let tref = self.translate_type_decl_ref(span, item)?;
665                        let variant_id = match kind {
666                            AdtKind::Struct | AdtKind::Union => None,
667                            AdtKind::Enum => Some(translate_variant_id(*variant_idx)),
668                            // The rest are fake adt kinds that won't reach here.
669                            _ => unreachable!(),
670                        };
671                        let field_id = match kind {
672                            AdtKind::Struct | AdtKind::Enum => None,
673                            AdtKind::Union => Some(translate_field_id(field_index.unwrap())),
674                            // The rest are fake adt kinds that won't reach here.
675                            _ => unreachable!(),
676                        };
677
678                        let akind = AggregateKind::Adt(tref, variant_id, field_id);
679                        Ok(Rvalue::Aggregate(akind, operands_t))
680                    }
681                    hax::AggregateKind::Closure(closure_args) => {
682                        trace!(
683                            "Closure:\n\n- def_id: {:?}\n\n- sig:\n{:?}",
684                            closure_args.item.def_id, closure_args.fn_sig
685                        );
686                        let tref = self.translate_closure_type_ref(span, closure_args)?;
687                        let akind = AggregateKind::Adt(tref, None, None);
688                        Ok(Rvalue::Aggregate(akind, operands_t))
689                    }
690                    hax::AggregateKind::RawPtr(ty, is_mut) => {
691                        // TODO: replace with a call to `ptr::from_raw_parts`.
692                        let t_ty = self.translate_ty(span, ty)?;
693                        let mutability = if *is_mut {
694                            RefKind::Mut
695                        } else {
696                            RefKind::Shared
697                        };
698
699                        let akind = AggregateKind::RawPtr(t_ty, mutability);
700
701                        Ok(Rvalue::Aggregate(akind, operands_t))
702                    }
703                    hax::AggregateKind::Coroutine(..)
704                    | hax::AggregateKind::CoroutineClosure(..) => {
705                        raise_error!(self, span, "Coroutines are not supported");
706                    }
707                }
708            }
709            hax::Rvalue::ShallowInitBox(op, ty) => {
710                let op = self.translate_operand(span, op)?;
711                let ty = self.translate_ty(span, ty)?;
712                Ok(Rvalue::ShallowInitBox(op, ty))
713            }
714            hax::Rvalue::ThreadLocalRef(_) => {
715                raise_error!(
716                    self,
717                    span,
718                    "charon does not support thread local references"
719                );
720            }
721            hax::Rvalue::WrapUnsafeBinder { .. } => {
722                raise_error!(
723                    self,
724                    span,
725                    "charon does not support unsafe lifetime binders"
726                );
727            }
728        }
729    }
730
731    /// Translate a statement
732    ///
733    /// We return an option, because we ignore some statements (`Nop`, `StorageLive`...)
734    fn translate_statement(
735        &mut self,
736        body: &hax::MirBody<hax::mir_kinds::Unknown>,
737        statement: &hax::Statement,
738    ) -> Result<Option<Statement>, Error> {
739        trace!("About to translate statement (MIR) {:?}", statement);
740        let span = self
741            .t_ctx
742            .translate_span_from_source_info(&body.source_scopes, &statement.source_info);
743
744        let t_statement: Option<StatementKind> = match &*statement.kind {
745            hax::StatementKind::Assign((place, rvalue)) => {
746                let t_place = self.translate_place(span, place)?;
747                let t_rvalue = self.translate_rvalue(span, rvalue, t_place.ty())?;
748                Some(StatementKind::Assign(t_place, t_rvalue))
749            }
750            hax::StatementKind::SetDiscriminant {
751                place,
752                variant_index,
753            } => {
754                let t_place = self.translate_place(span, place)?;
755                let variant_id = translate_variant_id(*variant_index);
756                Some(StatementKind::SetDiscriminant(t_place, variant_id))
757            }
758            hax::StatementKind::StorageLive(local) => {
759                let var_id = self.translate_local(local).unwrap();
760                Some(StatementKind::StorageLive(var_id))
761            }
762            hax::StatementKind::StorageDead(local) => {
763                let var_id = self.translate_local(local).unwrap();
764                Some(StatementKind::StorageDead(var_id))
765            }
766            hax::StatementKind::Deinit(place) => {
767                let t_place = self.translate_place(span, place)?;
768                Some(StatementKind::Deinit(t_place))
769            }
770            // This asserts the operand true on pain of UB. We treat it like a normal assertion.
771            hax::StatementKind::Intrinsic(hax::NonDivergingIntrinsic::Assume(op)) => {
772                let op = self.translate_operand(span, op)?;
773                Some(StatementKind::Assert(Assert {
774                    cond: op,
775                    expected: true,
776                    on_failure: AbortKind::UndefinedBehavior,
777                }))
778            }
779            hax::StatementKind::Intrinsic(hax::NonDivergingIntrinsic::CopyNonOverlapping(
780                hax::CopyNonOverlapping { src, dst, count },
781            )) => {
782                let src = self.translate_operand(span, src)?;
783                let dst = self.translate_operand(span, dst)?;
784                let count = self.translate_operand(span, count)?;
785                Some(StatementKind::CopyNonOverlapping(Box::new(
786                    CopyNonOverlapping { src, dst, count },
787                )))
788            }
789            // This is for the stacked borrows memory model.
790            hax::StatementKind::Retag(_, _) => None,
791            // These two are only there to make borrow-checking accept less code, and are removed
792            // in later MIRs.
793            hax::StatementKind::FakeRead(..) | hax::StatementKind::PlaceMention(..) => None,
794            // There are user-provided type annotations with no semantic effect (since we get a
795            // fully-typechecked MIR (TODO: this isn't quite true with opaque types, we should
796            // really use promoted MIR)).
797            hax::StatementKind::AscribeUserType(_, _) => None,
798            // Used for coverage instrumentation.
799            hax::StatementKind::Coverage(_) => None,
800            // Used in the interpreter to check that const code doesn't run for too long or even
801            // indefinitely.
802            hax::StatementKind::ConstEvalCounter => None,
803            // Semantically equivalent to `Nop`, used only for rustc lints.
804            hax::StatementKind::BackwardIncompatibleDropHint { .. } => None,
805            hax::StatementKind::Nop => None,
806        };
807
808        // Add the span information
809        Ok(t_statement.map(|kind| Statement::new(span, kind)))
810    }
811
812    /// Translate a terminator
813    fn translate_terminator(
814        &mut self,
815        body: &hax::MirBody<hax::mir_kinds::Unknown>,
816        terminator: &hax::Terminator,
817        statements: &mut Vec<Statement>,
818    ) -> Result<Terminator, Error> {
819        trace!("About to translate terminator (MIR) {:?}", terminator);
820        // Compute the span information beforehand (we might need it to introduce
821        // intermediate statements - we desugar some terminators)
822        let span = self
823            .t_ctx
824            .translate_span_from_source_info(&body.source_scopes, &terminator.source_info);
825
826        // Translate the terminator
827        use hax::TerminatorKind;
828        let t_terminator: ullbc_ast::TerminatorKind = match &terminator.kind {
829            TerminatorKind::Goto { target } => {
830                let target = self.translate_basic_block_id(*target);
831                ullbc_ast::TerminatorKind::Goto { target }
832            }
833            TerminatorKind::SwitchInt {
834                discr,
835                targets,
836                otherwise,
837                ..
838            } => {
839                // Translate the operand which gives the discriminant
840                let (discr, discr_ty) = self.translate_operand_with_type(span, discr)?;
841
842                // Translate the switch targets
843                let targets = self.translate_switch_targets(span, &discr_ty, targets, otherwise)?;
844
845                ullbc_ast::TerminatorKind::Switch { discr, targets }
846            }
847            TerminatorKind::UnwindResume => ullbc_ast::TerminatorKind::UnwindResume,
848            TerminatorKind::UnwindTerminate { .. } => {
849                ullbc_ast::TerminatorKind::Abort(AbortKind::UnwindTerminate)
850            }
851            TerminatorKind::Return => ullbc_ast::TerminatorKind::Return,
852            // A MIR `Unreachable` terminator indicates undefined behavior of the rust abstract
853            // machine.
854            TerminatorKind::Unreachable => {
855                ullbc_ast::TerminatorKind::Abort(AbortKind::UndefinedBehavior)
856            }
857            TerminatorKind::Drop {
858                place,
859                impl_expr,
860                target,
861                unwind: _, // We consider that panic is an error, and don't model unwinding
862                ..
863            } => {
864                let place = self.translate_place(span, place)?;
865                let tref = self.translate_trait_impl_expr(span, impl_expr)?;
866                statements.push(Statement::new(span, StatementKind::Drop(place, tref)));
867                let target = self.translate_basic_block_id(*target);
868                ullbc_ast::TerminatorKind::Goto { target }
869            }
870            TerminatorKind::Call {
871                fun,
872                args,
873                destination,
874                target,
875                unwind,
876                fn_span: _,
877                ..
878            } => self.translate_function_call(span, fun, args, destination, target, unwind)?,
879            TerminatorKind::Assert {
880                cond,
881                expected,
882                msg: _,
883                target,
884                unwind: _, // We model unwinding as an effet, we don't represent it in control flow
885            } => {
886                let assert = Assert {
887                    cond: self.translate_operand(span, cond)?,
888                    expected: *expected,
889                    on_failure: AbortKind::Panic(None),
890                };
891                statements.push(Statement::new(span, StatementKind::Assert(assert)));
892                let target = self.translate_basic_block_id(*target);
893                ullbc_ast::TerminatorKind::Goto { target }
894            }
895            TerminatorKind::FalseEdge {
896                real_target,
897                imaginary_target,
898            } => {
899                trace!(
900                    "False edge:\n- real target ({:?}):\n{:?}\n- imaginary target ({:?}):\n{:?}",
901                    real_target,
902                    body.basic_blocks.get(*real_target).unwrap(),
903                    imaginary_target,
904                    body.basic_blocks.get(*imaginary_target).unwrap(),
905                );
906
907                // False edges are used to make the borrow checker a bit conservative.
908                // We translate them as Gotos.
909                // Also note that they are used in some passes, and not in some others
910                // (they are present in mir_promoted, but not mir_optimized).
911                let target = self.translate_basic_block_id(*real_target);
912                ullbc_ast::TerminatorKind::Goto { target }
913            }
914            TerminatorKind::FalseUnwind {
915                real_target,
916                unwind: _,
917            } => {
918                // We consider this to be a goto
919                let target = self.translate_basic_block_id(*real_target);
920                ullbc_ast::TerminatorKind::Goto { target }
921            }
922            TerminatorKind::InlineAsm { .. } => {
923                raise_error!(self, span, "Inline assembly is not supported");
924            }
925            TerminatorKind::CoroutineDrop
926            | TerminatorKind::TailCall { .. }
927            | TerminatorKind::Yield { .. } => {
928                raise_error!(self, span, "Unsupported terminator: {:?}", terminator.kind);
929            }
930        };
931
932        // Add the span information
933        Ok(Terminator::new(span, t_terminator))
934    }
935
936    /// Translate switch targets
937    fn translate_switch_targets(
938        &mut self,
939        span: Span,
940        switch_ty: &Ty,
941        targets: &[(hax::ScalarInt, hax::BasicBlock)],
942        otherwise: &hax::BasicBlock,
943    ) -> Result<SwitchTargets, Error> {
944        trace!("targets: {:?}", targets);
945        let switch_ty = *switch_ty.kind().as_literal().unwrap();
946        match switch_ty {
947            LiteralTy::Bool => {
948                assert_eq!(targets.len(), 1);
949                let (val, target) = targets.first().unwrap();
950                // It seems the block targets are inverted
951                assert_eq!(val.data_le_bytes, [0; 16]);
952                let if_block = self.translate_basic_block_id(*otherwise);
953                let then_block = self.translate_basic_block_id(*target);
954                Ok(SwitchTargets::If(if_block, then_block))
955            }
956            LiteralTy::Char => {
957                let targets: Vec<(Literal, BlockId)> = targets
958                    .iter()
959                    .map(|(v, tgt)| {
960                        let b: u128 = u128::from_le_bytes(v.data_le_bytes);
961                        let v = Literal::char_from_le_bytes(b);
962                        let tgt = self.translate_basic_block_id(*tgt);
963                        (v, tgt)
964                    })
965                    .collect();
966                let otherwise = self.translate_basic_block_id(*otherwise);
967                Ok(SwitchTargets::SwitchInt(
968                    LiteralTy::Char,
969                    targets,
970                    otherwise,
971                ))
972            }
973            LiteralTy::Int(int_ty) => {
974                let targets: Vec<(Literal, BlockId)> = targets
975                    .iter()
976                    .map(|(v, tgt)| {
977                        let v = Literal::Scalar(ScalarValue::from_le_bytes(
978                            IntegerTy::Signed(int_ty),
979                            v.data_le_bytes,
980                        ));
981                        let tgt = self.translate_basic_block_id(*tgt);
982                        (v, tgt)
983                    })
984                    .collect();
985                let otherwise = self.translate_basic_block_id(*otherwise);
986                Ok(SwitchTargets::SwitchInt(switch_ty, targets, otherwise))
987            }
988            LiteralTy::UInt(uint_ty) => {
989                let targets: Vec<(Literal, BlockId)> = targets
990                    .iter()
991                    .map(|(v, tgt)| {
992                        let v = Literal::Scalar(ScalarValue::from_le_bytes(
993                            IntegerTy::Unsigned(uint_ty),
994                            v.data_le_bytes,
995                        ));
996                        let tgt = self.translate_basic_block_id(*tgt);
997                        (v, tgt)
998                    })
999                    .collect();
1000                let otherwise = self.translate_basic_block_id(*otherwise);
1001                Ok(SwitchTargets::SwitchInt(
1002                    LiteralTy::UInt(uint_ty),
1003                    targets,
1004                    otherwise,
1005                ))
1006            }
1007            _ => raise_error!(self, span, "Can't match on type {switch_ty}"),
1008        }
1009    }
1010
1011    /// Translate a function call statement.
1012    /// Note that `body` is the body of the function being translated, not of the
1013    /// function referenced in the function call: we need it in order to translate
1014    /// the blocks we go to after the function call returns.
1015    #[allow(clippy::too_many_arguments)]
1016    fn translate_function_call(
1017        &mut self,
1018        span: Span,
1019        fun: &hax::FunOperand,
1020        args: &Vec<hax::Spanned<hax::Operand>>,
1021        destination: &hax::Place,
1022        target: &Option<hax::BasicBlock>,
1023        unwind: &UnwindAction,
1024    ) -> Result<TerminatorKind, Error> {
1025        trace!();
1026        // There are two cases, depending on whether this is a "regular"
1027        // call to a top-level function identified by its id, or if we
1028        // are using a local function pointer (i.e., the operand is a "move").
1029        let lval = self.translate_place(span, destination)?;
1030        // Translate the function operand.
1031        let fn_operand = match fun {
1032            hax::FunOperand::Static(item) => {
1033                trace!("func: {:?}", item.def_id);
1034                let fun_def = self.hax_def(item)?;
1035                let item_src =
1036                    TransItemSource::from_item(item, TransItemSourceKind::Fun, self.monomorphize());
1037                let name = self.t_ctx.translate_name(&item_src)?;
1038                let panic_lang_items = &["panic", "panic_fmt", "begin_panic"];
1039                let panic_names = &[&["core", "panicking", "assert_failed"], EXPLICIT_PANIC_NAME];
1040
1041                if fun_def
1042                    .lang_item
1043                    .as_deref()
1044                    .is_some_and(|lang_it| panic_lang_items.iter().contains(&lang_it))
1045                    || panic_names.iter().any(|panic| name.equals_ref_name(panic))
1046                {
1047                    // If the call is `panic!`, then the target is `None`.
1048                    // I don't know in which other cases it can be `None`.
1049                    assert!(target.is_none());
1050                    // We ignore the arguments
1051                    return Ok(TerminatorKind::Abort(AbortKind::Panic(Some(name))));
1052                } else {
1053                    let fn_ptr = self
1054                        .translate_fn_ptr(span, item, TransItemSourceKind::Fun)?
1055                        .erase();
1056                    FnOperand::Regular(fn_ptr)
1057                }
1058            }
1059            hax::FunOperand::DynamicMove(p) => {
1060                // Call to a local function pointer
1061                let p = self.translate_place(span, p)?;
1062
1063                // TODO: we may have a problem here because as we don't
1064                // know which function is being called, we may not be
1065                // able to filter the arguments properly... But maybe
1066                // this is rather an issue for the statement which creates
1067                // the function pointer, by refering to a top-level function
1068                // for instance.
1069                FnOperand::Move(p)
1070            }
1071        };
1072        let args = self.translate_arguments(span, args)?;
1073        let call = Call {
1074            func: fn_operand,
1075            args,
1076            dest: lval,
1077        };
1078
1079        let target = match target {
1080            Some(target) => self.translate_basic_block_id(*target),
1081            None => {
1082                let abort =
1083                    Terminator::new(span, TerminatorKind::Abort(AbortKind::UndefinedBehavior));
1084                self.blocks.push(abort.into_block())
1085            }
1086        };
1087        let on_unwind = match unwind {
1088            UnwindAction::Continue => {
1089                let unwind_continue = Terminator::new(span, TerminatorKind::UnwindResume);
1090                self.blocks.push(unwind_continue.into_block())
1091            }
1092            UnwindAction::Unreachable => {
1093                let abort =
1094                    Terminator::new(span, TerminatorKind::Abort(AbortKind::UndefinedBehavior));
1095                self.blocks.push(abort.into_block())
1096            }
1097            UnwindAction::Terminate(..) => {
1098                let abort =
1099                    Terminator::new(span, TerminatorKind::Abort(AbortKind::UnwindTerminate));
1100                self.blocks.push(abort.into_block())
1101            }
1102            UnwindAction::Cleanup(bb) => self.translate_basic_block_id(*bb),
1103        };
1104        Ok(TerminatorKind::Call {
1105            call,
1106            target,
1107            on_unwind,
1108        })
1109    }
1110
1111    /// Evaluate function arguments in a context, and return the list of computed
1112    /// values.
1113    fn translate_arguments(
1114        &mut self,
1115        span: Span,
1116        args: &Vec<hax::Spanned<hax::Operand>>,
1117    ) -> Result<Vec<Operand>, Error> {
1118        let mut t_args: Vec<Operand> = Vec::new();
1119        for arg in args.iter().map(|x| &x.node) {
1120            // Translate
1121            let op = self.translate_operand(span, arg)?;
1122            t_args.push(op);
1123        }
1124        Ok(t_args)
1125    }
1126
1127    /// Gather all the lines that start with `//` inside the given span.
1128    fn translate_body_comments(
1129        &mut self,
1130        source_text: &Option<String>,
1131        charon_span: Span,
1132    ) -> Vec<(usize, Vec<String>)> {
1133        if let Some(body_text) = source_text {
1134            let mut comments = body_text
1135                .lines()
1136                // Iter through the lines of this body in reverse order.
1137                .rev()
1138                .enumerate()
1139                // Compute the absolute line number
1140                .map(|(i, line)| (charon_span.data.end.line - i, line))
1141                // Extract the comment if this line starts with `//`
1142                .map(|(line_nbr, line)| (line_nbr, line.trim_start().strip_prefix("//")))
1143                .peekable()
1144                .batching(|iter| {
1145                    // Get the next line. This is not a comment: it's either the last line of the
1146                    // body or a line that wasn't consumed by `peeking_take_while`.
1147                    let (line_nbr, _first) = iter.next()?;
1148                    // Collect all the comments before this line.
1149                    let mut comments = iter
1150                        // `peeking_take_while` ensures we don't consume a line that returns
1151                        // `false`. It will be consumed by the next round of `batching`.
1152                        .peeking_take_while(|(_, opt_comment)| opt_comment.is_some())
1153                        .map(|(_, opt_comment)| opt_comment.unwrap())
1154                        .map(|s| s.strip_prefix(" ").unwrap_or(s))
1155                        .map(str::to_owned)
1156                        .collect_vec();
1157                    comments.reverse();
1158                    Some((line_nbr, comments))
1159                })
1160                .filter(|(_, comments)| !comments.is_empty())
1161                .collect_vec();
1162            comments.reverse();
1163            comments
1164        } else {
1165            Vec::new()
1166        }
1167    }
1168
1169    /// Translate the MIR body of this definition if it has one.
1170    pub fn translate_def_body(
1171        &mut self,
1172        span: Span,
1173        def: &hax::FullDef,
1174    ) -> Result<Result<Body, Opaque>, Error> {
1175        // Retrieve the body
1176        let Some(body) = self.get_mir(def.this(), span)? else {
1177            return Ok(Err(Opaque));
1178        };
1179        self.translate_body(span, &body, &def.source_text)
1180    }
1181
1182    /// Translate a function body.
1183    pub fn translate_body(
1184        &mut self,
1185        span: Span,
1186        body: &hax::MirBody<hax::mir_kinds::Unknown>,
1187        source_text: &Option<String>,
1188    ) -> Result<Result<Body, Opaque>, Error> {
1189        // Stopgap measure because there are still many panics in charon and hax.
1190        let mut this = panic::AssertUnwindSafe(&mut *self);
1191        let res = panic::catch_unwind(move || this.translate_body_aux(body, source_text));
1192        match res {
1193            Ok(Ok(body)) => Ok(body),
1194            // Translation error
1195            Ok(Err(e)) => Err(e),
1196            Err(_) => {
1197                raise_error!(self, span, "Thread panicked when extracting body.");
1198            }
1199        }
1200    }
1201
1202    fn translate_body_aux(
1203        &mut self,
1204        body: &hax::MirBody<hax::mir_kinds::Unknown>,
1205        source_text: &Option<String>,
1206    ) -> Result<Result<Body, Opaque>, Error> {
1207        // Compute the span information
1208        let span = self.translate_span_from_hax(&body.span);
1209
1210        // Initialize the local variables
1211        trace!("Translating the body locals");
1212        self.locals.arg_count = body.arg_count;
1213        self.translate_body_locals(&body)?;
1214
1215        // Translate the expression body
1216        trace!("Translating the expression body");
1217
1218        // Register the start block
1219        let id = self.translate_basic_block_id(rustc_index::Idx::new(mir::START_BLOCK.as_usize()));
1220        assert!(id == START_BLOCK_ID);
1221
1222        // For as long as there are blocks in the stack, translate them
1223        while let Some(hax_block_id) = self.blocks_stack.pop_front() {
1224            let hax_block = body.basic_blocks.get(hax_block_id).unwrap();
1225            let block_id = self.translate_basic_block_id(hax_block_id);
1226            let block = self.translate_basic_block(&body, hax_block)?;
1227            self.blocks.set_slot(block_id, block);
1228        }
1229
1230        // Create the body
1231        Ok(Ok(Body::Unstructured(ExprBody {
1232            span,
1233            locals: mem::take(&mut self.locals),
1234            body: mem::take(&mut self.blocks),
1235            comments: self.translate_body_comments(source_text, span),
1236        })))
1237    }
1238}
1239
1240impl<'a> IntoFormatter for &'a BodyTransCtx<'_, '_, '_> {
1241    type C = FmtCtx<'a>;
1242    fn into_fmt(self) -> Self::C {
1243        FmtCtx {
1244            locals: Some(&self.locals),
1245            ..self.i_ctx.into_fmt()
1246        }
1247    }
1248}
charon_driver/translate/translate_bodies.rs

charon_driver/translate/
translate_bodies.rs
