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

charon_driver/translate/
translate_bodies.rs
