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

charon_driver/translate/
translate_bodies.rs
