charon_driver/translate/
translate_bodies.rs

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

charon_driver/translate/
translate_bodies.rs
