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

charon_driver/translate/
translate_bodies.rs
