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

charon_driver/translate/
translate_bodies.rs
