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

charon_driver/translate/
translate_bodies.rs
