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

charon_driver/translate/
translate_bodies.rs
