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

charon_driver/translate/
translate_bodies.rs
