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

charon_driver/translate/
translate_bodies.rs
