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 = Operand::Const(ScalarValue::Usize(offset).to_constant());
310                        subplace.project(
311                            ProjectionElem::Index {
312                                offset: Box::new(offset),
313                                from_end,
314                            },
315                            ty,
316                        )
317                    }
318                    &hax::ProjectionElem::Subslice { from, to, from_end } => {
319                        let from = Operand::Const(ScalarValue::Usize(from).to_constant());
320                        let to = Operand::Const(ScalarValue::Usize(to).to_constant());
321                        subplace.project(
322                            ProjectionElem::Subslice {
323                                from: Box::new(from),
324                                to: Box::new(to),
325                                from_end,
326                            },
327                            ty,
328                        )
329                    }
330                    hax::ProjectionElem::OpaqueCast => {
331                        // Don't know what that is
332                        raise_error!(self, span, "Unexpected ProjectionElem::OpaqueCast");
333                    }
334                };
335
336                // Return
337                Ok(place)
338            }
339        }
340    }
341
342    /// Translate an operand with its type
343    fn translate_operand_with_type(
344        &mut self,
345        span: Span,
346        operand: &hax::Operand,
347    ) -> Result<(Operand, Ty), Error> {
348        trace!();
349        match operand {
350            hax::Operand::Copy(place) => {
351                let p = self.translate_place(span, place)?;
352                let ty = p.ty().clone();
353                Ok((Operand::Copy(p), ty))
354            }
355            hax::Operand::Move(place) => {
356                let p = self.translate_place(span, place)?;
357                let ty = p.ty().clone();
358                Ok((Operand::Move(p), ty))
359            }
360            hax::Operand::Constant(const_op) => match &const_op.kind {
361                hax::ConstOperandKind::Value(constant) => {
362                    let constant = self.translate_constant_expr_to_constant_expr(span, constant)?;
363                    let ty = constant.ty.clone();
364                    Ok((Operand::Const(constant), ty))
365                }
366                hax::ConstOperandKind::Promoted {
367                    def_id,
368                    args,
369                    impl_exprs,
370                } => {
371                    let ty = self.translate_ty(span, &const_op.ty)?;
372                    // A promoted constant that could not be evaluated.
373                    let global_id = self.register_global_decl_id(span, def_id);
374                    let constant = ConstantExpr {
375                        value: RawConstantExpr::Global(GlobalDeclRef {
376                            id: global_id,
377                            generics: self.translate_generic_args(
378                                span,
379                                args,
380                                impl_exprs,
381                                None,
382                                GenericsSource::item(global_id),
383                            )?,
384                        }),
385                        ty: ty.clone(),
386                    };
387                    Ok((Operand::Const(constant), ty))
388                }
389            },
390        }
391    }
392
393    /// Translate an operand
394    fn translate_operand(&mut self, span: Span, operand: &hax::Operand) -> Result<Operand, Error> {
395        trace!();
396        Ok(self.translate_operand_with_type(span, operand)?.0)
397    }
398
399    /// Translate an rvalue
400    fn translate_rvalue(&mut self, span: Span, rvalue: &hax::Rvalue) -> Result<Rvalue, Error> {
401        match rvalue {
402            hax::Rvalue::Use(operand) => Ok(Rvalue::Use(self.translate_operand(span, operand)?)),
403            hax::Rvalue::CopyForDeref(place) => {
404                // According to the documentation, it seems to be an optimisation
405                // for drop elaboration. We treat it as a regular copy.
406                let place = self.translate_place(span, place)?;
407                Ok(Rvalue::Use(Operand::Copy(place)))
408            }
409            hax::Rvalue::Repeat(operand, cnst) => {
410                let c = self.translate_constant_expr_to_const_generic(span, cnst)?;
411                let (operand, t) = self.translate_operand_with_type(span, operand)?;
412                // Remark: we could desugar this into a function call later.
413                Ok(Rvalue::Repeat(operand, t, c))
414            }
415            hax::Rvalue::Ref(_region, borrow_kind, place) => {
416                let place = self.translate_place(span, place)?;
417                let borrow_kind = translate_borrow_kind(*borrow_kind);
418                Ok(Rvalue::Ref(place, borrow_kind))
419            }
420            hax::Rvalue::RawPtr(mtbl, place) => {
421                let mtbl = match mtbl {
422                    hax::RawPtrKind::Mut => RefKind::Mut,
423                    hax::RawPtrKind::Const => RefKind::Shared,
424                    hax::RawPtrKind::FakeForPtrMetadata => RefKind::Shared,
425                };
426                let place = self.translate_place(span, place)?;
427                Ok(Rvalue::RawPtr(place, mtbl))
428            }
429            hax::Rvalue::Len(place) => {
430                let place = self.translate_place(span, place)?;
431                let ty = place.ty().clone();
432                let cg = match ty.kind() {
433                    TyKind::Adt(
434                        TypeId::Builtin(aty @ (BuiltinTy::Array | BuiltinTy::Slice)),
435                        generics,
436                    ) => {
437                        if aty.is_array() {
438                            Some(generics.const_generics[0].clone())
439                        } else {
440                            None
441                        }
442                    }
443                    _ => unreachable!(),
444                };
445                Ok(Rvalue::Len(place, ty, cg))
446            }
447            hax::Rvalue::Cast(cast_kind, operand, tgt_ty) => {
448                trace!("Rvalue::Cast: {:?}", rvalue);
449                // Translate the target type
450                let tgt_ty = self.translate_ty(span, tgt_ty)?;
451
452                // Translate the operand
453                let (operand, src_ty) = self.translate_operand_with_type(span, operand)?;
454
455                match cast_kind {
456                    hax::CastKind::IntToInt
457                    | hax::CastKind::IntToFloat
458                    | hax::CastKind::FloatToInt
459                    | hax::CastKind::FloatToFloat => {
460                        let tgt_ty = *tgt_ty.kind().as_literal().unwrap();
461                        let src_ty = *src_ty.kind().as_literal().unwrap();
462                        Ok(Rvalue::UnaryOp(
463                            UnOp::Cast(CastKind::Scalar(src_ty, tgt_ty)),
464                            operand,
465                        ))
466                    }
467                    hax::CastKind::PtrToPtr
468                    | hax::CastKind::PointerCoercion(hax::PointerCoercion::MutToConstPointer, ..)
469                    | hax::CastKind::PointerCoercion(hax::PointerCoercion::ArrayToPointer, ..)
470                    | hax::CastKind::PointerCoercion(hax::PointerCoercion::DynStar, ..)
471                    | hax::CastKind::FnPtrToPtr
472                    | hax::CastKind::PointerExposeProvenance
473                    | hax::CastKind::PointerWithExposedProvenance => Ok(Rvalue::UnaryOp(
474                        UnOp::Cast(CastKind::RawPtr(src_ty, tgt_ty)),
475                        operand,
476                    )),
477                    hax::CastKind::PointerCoercion(
478                        hax::PointerCoercion::ClosureFnPointer(_)
479                        | hax::PointerCoercion::UnsafeFnPointer
480                        | hax::PointerCoercion::ReifyFnPointer,
481                        ..,
482                    ) => Ok(Rvalue::UnaryOp(
483                        UnOp::Cast(CastKind::FnPtr(src_ty, tgt_ty)),
484                        operand,
485                    )),
486                    hax::CastKind::Transmute => Ok(Rvalue::UnaryOp(
487                        UnOp::Cast(CastKind::Transmute(src_ty, tgt_ty)),
488                        operand,
489                    )),
490                    hax::CastKind::PointerCoercion(hax::PointerCoercion::Unsize, ..) => {
491                        let unop = if let (
492                            TyKind::Ref(
493                                _,
494                                deref!(TyKind::Adt(TypeId::Builtin(BuiltinTy::Array), generics)),
495                                kind1,
496                            ),
497                            TyKind::Ref(
498                                _,
499                                deref!(TyKind::Adt(TypeId::Builtin(BuiltinTy::Slice), generics1)),
500                                kind2,
501                            ),
502                        ) = (src_ty.kind(), tgt_ty.kind())
503                        {
504                            // In MIR terminology, we go from &[T; l] to &[T] which means we
505                            // effectively "unsize" the type, as `l` no longer appears in the
506                            // destination type. At runtime, the converse happens: the length
507                            // materializes into the fat pointer.
508                            assert!(
509                                generics.types.elem_count() == 1
510                                    && generics.const_generics.elem_count() == 1
511                            );
512                            assert!(generics.types[0] == generics1.types[0]);
513                            assert!(kind1 == kind2);
514                            UnOp::ArrayToSlice(
515                                *kind1,
516                                generics.types[0].clone(),
517                                generics.const_generics[0].clone(),
518                            )
519                        } else {
520                            UnOp::Cast(CastKind::Unsize(src_ty.clone(), tgt_ty.clone()))
521                        };
522                        Ok(Rvalue::UnaryOp(unop, operand))
523                    }
524                }
525            }
526            hax::Rvalue::BinaryOp(binop, (left, right)) => Ok(Rvalue::BinaryOp(
527                self.translate_binaryop_kind(span, *binop)?,
528                self.translate_operand(span, left)?,
529                self.translate_operand(span, right)?,
530            )),
531            hax::Rvalue::NullaryOp(nullop, ty) => {
532                trace!("NullOp: {:?}", nullop);
533                let ty = self.translate_ty(span, ty)?;
534                let op = match nullop {
535                    hax::NullOp::SizeOf => NullOp::SizeOf,
536                    hax::NullOp::AlignOf => NullOp::AlignOf,
537                    hax::NullOp::OffsetOf(fields) => NullOp::OffsetOf(
538                        fields
539                            .iter()
540                            .copied()
541                            .map(|(n, idx)| (n, translate_field_id(idx)))
542                            .collect(),
543                    ),
544                    hax::NullOp::UbChecks => NullOp::UbChecks,
545                    hax::NullOp::ContractChecks => {
546                        raise_error!(self, span, "charon does not support contracts");
547                    }
548                };
549                Ok(Rvalue::NullaryOp(op, ty))
550            }
551            hax::Rvalue::UnaryOp(unop, operand) => {
552                let unop = match unop {
553                    hax::UnOp::Not => UnOp::Not,
554                    hax::UnOp::Neg => UnOp::Neg,
555                    hax::UnOp::PtrMetadata => UnOp::PtrMetadata,
556                };
557                Ok(Rvalue::UnaryOp(
558                    unop,
559                    self.translate_operand(span, operand)?,
560                ))
561            }
562            hax::Rvalue::Discriminant(place) => {
563                let place = self.translate_place(span, place)?;
564                if let TyKind::Adt(TypeId::Adt(adt_id), _) = *place.ty().kind() {
565                    Ok(Rvalue::Discriminant(place, adt_id))
566                } else {
567                    raise_error!(
568                        self,
569                        span,
570                        "Unexpected scrutinee type for ReadDiscriminant: {}",
571                        place.ty().fmt_with_ctx(&self.into_fmt())
572                    )
573                }
574            }
575            hax::Rvalue::Aggregate(aggregate_kind, operands) => {
576                // It seems this instruction is not present in certain passes:
577                // for example, it seems it is not used in optimized MIR, where
578                // ADT initialization is split into several instructions, for
579                // instance:
580                // ```
581                // p = Pair { x:xv, y:yv };
582                // ```
583                // Might become:
584                // ```
585                // p.x = x;
586                // p.y = yv;
587                // ```
588
589                // First translate the operands
590                let operands_t: Vec<Operand> = operands
591                    .raw
592                    .iter()
593                    .map(|op| self.translate_operand(span, op))
594                    .try_collect()?;
595
596                match aggregate_kind {
597                    hax::AggregateKind::Array(ty) => {
598                        let t_ty = self.translate_ty(span, ty)?;
599                        let cg = ConstGeneric::Value(Literal::Scalar(ScalarValue::Usize(
600                            operands_t.len() as u64,
601                        )));
602                        Ok(Rvalue::Aggregate(
603                            AggregateKind::Array(t_ty, cg),
604                            operands_t,
605                        ))
606                    }
607                    hax::AggregateKind::Tuple => Ok(Rvalue::Aggregate(
608                        AggregateKind::Adt(
609                            TypeId::Tuple,
610                            None,
611                            None,
612                            GenericArgs::empty(GenericsSource::Builtin),
613                        ),
614                        operands_t,
615                    )),
616                    hax::AggregateKind::Adt(
617                        adt_id,
618                        variant_idx,
619                        kind,
620                        substs,
621                        trait_refs,
622                        user_annotation,
623                        field_index,
624                    ) => {
625                        trace!("{:?}", rvalue);
626
627                        // We ignore type annotations since rustc has already inferred all the
628                        // types we need.
629                        let _ = user_annotation;
630
631                        let type_id = self.translate_type_id(span, adt_id)?;
632                        // Sanity check
633                        assert!(matches!(&type_id, TypeId::Adt(_)));
634
635                        // Translate the substitution
636                        let generics = self.translate_generic_args(
637                            span,
638                            substs,
639                            trait_refs,
640                            None,
641                            type_id.generics_target(),
642                        )?;
643
644                        use hax::AdtKind;
645                        let variant_id = match kind {
646                            AdtKind::Struct | AdtKind::Union => None,
647                            AdtKind::Enum => Some(translate_variant_id(*variant_idx)),
648                        };
649                        let field_id = match kind {
650                            AdtKind::Struct | AdtKind::Enum => None,
651                            AdtKind::Union => Some(translate_field_id(field_index.unwrap())),
652                        };
653
654                        let akind = AggregateKind::Adt(type_id, variant_id, field_id, generics);
655                        Ok(Rvalue::Aggregate(akind, operands_t))
656                    }
657                    hax::AggregateKind::Closure(def_id, closure_args) => {
658                        trace!(
659                            "Closure:\n\n- def_id: {:?}\n\n- sig:\n{:?}",
660                            def_id,
661                            closure_args.tupled_sig
662                        );
663
664                        let fun_id = self.register_fun_decl_id(span, def_id);
665
666                        // Retrieve the late-bound variables.
667                        let binder = closure_args.tupled_sig.as_ref().rebind(());
668                        // Translate the substitution
669                        let generics = self.translate_generic_args(
670                            span,
671                            &closure_args.parent_args,
672                            &closure_args.parent_trait_refs,
673                            Some(binder),
674                            GenericsSource::item(fun_id),
675                        )?;
676
677                        let akind = AggregateKind::Closure(fun_id, generics);
678
679                        Ok(Rvalue::Aggregate(akind, operands_t))
680                    }
681                    hax::AggregateKind::RawPtr(ty, is_mut) => {
682                        // TODO: replace with a call to `ptr::from_raw_parts`.
683                        let t_ty = self.translate_ty(span, ty)?;
684                        let mutability = if *is_mut {
685                            RefKind::Mut
686                        } else {
687                            RefKind::Shared
688                        };
689
690                        let akind = AggregateKind::RawPtr(t_ty, mutability);
691
692                        Ok(Rvalue::Aggregate(akind, operands_t))
693                    }
694                    hax::AggregateKind::Coroutine(..)
695                    | hax::AggregateKind::CoroutineClosure(..) => {
696                        raise_error!(self, span, "Coroutines are not supported");
697                    }
698                }
699            }
700            hax::Rvalue::ShallowInitBox(op, ty) => {
701                let op = self.translate_operand(span, op)?;
702                let ty = self.translate_ty(span, ty)?;
703                Ok(Rvalue::ShallowInitBox(op, ty))
704            }
705            hax::Rvalue::ThreadLocalRef(_) => {
706                raise_error!(
707                    self,
708                    span,
709                    "charon does not support thread local references"
710                );
711            }
712            hax::Rvalue::WrapUnsafeBinder { .. } => {
713                raise_error!(
714                    self,
715                    span,
716                    "charon does not support unsafe lifetime binders"
717                );
718            }
719        }
720    }
721
722    /// Translate a statement
723    ///
724    /// We return an option, because we ignore some statements (`Nop`, `StorageLive`...)
725    fn translate_statement(
726        &mut self,
727        body: &hax::MirBody<()>,
728        statement: &hax::Statement,
729    ) -> Result<Option<Statement>, Error> {
730        trace!("About to translate statement (MIR) {:?}", statement);
731        let span = self
732            .t_ctx
733            .translate_span_from_source_info(&body.source_scopes, &statement.source_info);
734
735        use hax::StatementKind;
736        let t_statement: Option<RawStatement> = match &*statement.kind {
737            StatementKind::Assign((place, rvalue)) => {
738                let t_place = self.translate_place(span, place)?;
739                let t_rvalue = self.translate_rvalue(span, rvalue)?;
740                Some(RawStatement::Assign(t_place, t_rvalue))
741            }
742            StatementKind::SetDiscriminant {
743                place,
744                variant_index,
745            } => {
746                let t_place = self.translate_place(span, place)?;
747                let variant_id = translate_variant_id(*variant_index);
748                Some(RawStatement::SetDiscriminant(t_place, variant_id))
749            }
750            StatementKind::StorageLive(local) => {
751                let var_id = self.translate_local(local).unwrap();
752                Some(RawStatement::StorageLive(var_id))
753            }
754            StatementKind::StorageDead(local) => {
755                let var_id = self.translate_local(local).unwrap();
756                Some(RawStatement::StorageDead(var_id))
757            }
758            StatementKind::Deinit(place) => {
759                let t_place = self.translate_place(span, place)?;
760                Some(RawStatement::Deinit(t_place))
761            }
762            // This asserts the operand true on pain of UB. We treat it like a normal assertion.
763            StatementKind::Intrinsic(hax::NonDivergingIntrinsic::Assume(op)) => {
764                let op = self.translate_operand(span, op)?;
765                Some(RawStatement::Assert(Assert {
766                    cond: op,
767                    expected: true,
768                    on_failure: AbortKind::UndefinedBehavior,
769                }))
770            }
771            StatementKind::Intrinsic(hax::NonDivergingIntrinsic::CopyNonOverlapping(..)) => {
772                raise_error!(self, span, "Unsupported statement kind: CopyNonOverlapping");
773            }
774            // This is for the stacked borrows memory model.
775            StatementKind::Retag(_, _) => None,
776            // These two are only there to make borrow-checking accept less code, and are removed
777            // in later MIRs.
778            StatementKind::FakeRead(..) | StatementKind::PlaceMention(..) => None,
779            // There are user-provided type annotations with no semantic effect (since we get a
780            // fully-typechecked MIR (TODO: this isn't quite true with opaque types, we should
781            // really use promoted MIR)).
782            StatementKind::AscribeUserType(_, _) => None,
783            // Used for coverage instrumentation.
784            StatementKind::Coverage(_) => None,
785            // Used in the interpreter to check that const code doesn't run for too long or even
786            // indefinitely.
787            StatementKind::ConstEvalCounter => None,
788            // Semantically equivalent to `Nop`, used only for rustc lints.
789            StatementKind::BackwardIncompatibleDropHint { .. } => None,
790            StatementKind::Nop => None,
791        };
792
793        // Add the span information
794        Ok(t_statement.map(|kind| Statement::new(span, kind)))
795    }
796
797    /// Translate a terminator
798    fn translate_terminator(
799        &mut self,
800        body: &hax::MirBody<()>,
801        terminator: &hax::Terminator,
802        statements: &mut Vec<Statement>,
803    ) -> Result<Terminator, Error> {
804        trace!("About to translate terminator (MIR) {:?}", terminator);
805        // Compute the span information beforehand (we might need it to introduce
806        // intermediate statements - we desugar some terminators)
807        let span = self
808            .t_ctx
809            .translate_span_from_source_info(&body.source_scopes, &terminator.source_info);
810
811        // Translate the terminator
812        use hax::TerminatorKind;
813        let t_terminator: RawTerminator = match &terminator.kind {
814            TerminatorKind::Goto { target } => {
815                let target = self.translate_basic_block_id(*target);
816                RawTerminator::Goto { target }
817            }
818            TerminatorKind::SwitchInt {
819                discr,
820                targets,
821                otherwise,
822                ..
823            } => {
824                // Translate the operand which gives the discriminant
825                let (discr, discr_ty) = self.translate_operand_with_type(span, discr)?;
826
827                // Translate the switch targets
828                let targets = self.translate_switch_targets(span, &discr_ty, targets, otherwise)?;
829
830                RawTerminator::Switch { discr, targets }
831            }
832            TerminatorKind::UnwindResume => {
833                // This is used to correctly unwind. We shouldn't get there: if
834                // we panic, the state gets stuck.
835                raise_error!(self, span, "Unexpected terminator: UnwindResume");
836            }
837            TerminatorKind::UnwindTerminate { .. } => {
838                raise_error!(self, span, "Unexpected terminator: UnwindTerminate")
839            }
840            TerminatorKind::Return => RawTerminator::Return,
841            // A MIR `Unreachable` terminator indicates undefined behavior of the rust abstract
842            // machine.
843            TerminatorKind::Unreachable => RawTerminator::Abort(AbortKind::UndefinedBehavior),
844            TerminatorKind::Drop {
845                place,
846                target,
847                unwind: _, // We consider that panic is an error, and don't model unwinding
848                replace: _,
849            } => {
850                let place = self.translate_place(span, place)?;
851                statements.push(Statement::new(span, RawStatement::Drop(place)));
852                let target = self.translate_basic_block_id(*target);
853                RawTerminator::Goto { target }
854            }
855            TerminatorKind::Call {
856                fun,
857                args,
858                destination,
859                target,
860                unwind: _, // We model unwinding as an effet, we don't represent it in control flow
861                fn_span: _,
862                ..
863            } => self.translate_function_call(statements, span, fun, args, destination, target)?,
864            TerminatorKind::Assert {
865                cond,
866                expected,
867                msg: _,
868                target,
869                unwind: _, // We model unwinding as an effet, we don't represent it in control flow
870            } => {
871                let assert = Assert {
872                    cond: self.translate_operand(span, cond)?,
873                    expected: *expected,
874                    on_failure: AbortKind::Panic(None),
875                };
876                statements.push(Statement::new(span, RawStatement::Assert(assert)));
877                let target = self.translate_basic_block_id(*target);
878                RawTerminator::Goto { target }
879            }
880            TerminatorKind::FalseEdge {
881                real_target,
882                imaginary_target,
883            } => {
884                trace!(
885                    "False edge:\n- real target ({:?}):\n{:?}\n- imaginary target ({:?}):\n{:?}",
886                    real_target,
887                    body.basic_blocks.get(*real_target).unwrap(),
888                    imaginary_target,
889                    body.basic_blocks.get(*imaginary_target).unwrap(),
890                );
891
892                // False edges are used to make the borrow checker a bit conservative.
893                // We translate them as Gotos.
894                // Also note that they are used in some passes, and not in some others
895                // (they are present in mir_promoted, but not mir_optimized).
896                let target = self.translate_basic_block_id(*real_target);
897                RawTerminator::Goto { target }
898            }
899            TerminatorKind::FalseUnwind {
900                real_target,
901                unwind: _,
902            } => {
903                // We consider this to be a goto
904                let target = self.translate_basic_block_id(*real_target);
905                RawTerminator::Goto { target }
906            }
907            TerminatorKind::InlineAsm { .. } => {
908                raise_error!(self, span, "Inline assembly is not supported");
909            }
910            TerminatorKind::CoroutineDrop
911            | TerminatorKind::TailCall { .. }
912            | TerminatorKind::Yield { .. } => {
913                raise_error!(self, span, "Unsupported terminator: {:?}", terminator.kind);
914            }
915        };
916
917        // Add the span information
918        Ok(Terminator::new(span, t_terminator))
919    }
920
921    /// Translate switch targets
922    fn translate_switch_targets(
923        &mut self,
924        span: Span,
925        switch_ty: &Ty,
926        targets: &[(hax::ScalarInt, hax::BasicBlock)],
927        otherwise: &hax::BasicBlock,
928    ) -> Result<SwitchTargets, Error> {
929        trace!("targets: {:?}", targets);
930        let switch_ty = *switch_ty.kind().as_literal().unwrap();
931        match switch_ty {
932            LiteralTy::Bool => {
933                assert_eq!(targets.len(), 1);
934                let (val, target) = targets.first().unwrap();
935                // It seems the block targets are inverted
936                assert_eq!(val.data_le_bytes, [0; 16]);
937                let if_block = self.translate_basic_block_id(*otherwise);
938                let then_block = self.translate_basic_block_id(*target);
939                Ok(SwitchTargets::If(if_block, then_block))
940            }
941            LiteralTy::Integer(int_ty) => {
942                let targets: Vec<(ScalarValue, BlockId)> = targets
943                    .iter()
944                    .map(|(v, tgt)| {
945                        let v = ScalarValue::from_le_bytes(int_ty, v.data_le_bytes);
946                        let tgt = self.translate_basic_block_id(*tgt);
947                        Ok((v, tgt))
948                    })
949                    .try_collect()?;
950                let otherwise = self.translate_basic_block_id(*otherwise);
951                Ok(SwitchTargets::SwitchInt(int_ty, targets, otherwise))
952            }
953            _ => raise_error!(self, span, "Can't match on type {switch_ty}"),
954        }
955    }
956
957    /// Translate a function call statement.
958    /// Note that `body` is the body of the function being translated, not of the
959    /// function referenced in the function call: we need it in order to translate
960    /// the blocks we go to after the function call returns.
961    #[allow(clippy::too_many_arguments)]
962    fn translate_function_call(
963        &mut self,
964        statements: &mut Vec<Statement>,
965        span: Span,
966        fun: &hax::FunOperand,
967        args: &Vec<hax::Spanned<hax::Operand>>,
968        destination: &hax::Place,
969        target: &Option<hax::BasicBlock>,
970    ) -> Result<RawTerminator, Error> {
971        trace!();
972        // There are two cases, depending on whether this is a "regular"
973        // call to a top-level function identified by its id, or if we
974        // are using a local function pointer (i.e., the operand is a "move").
975        let lval = self.translate_place(span, destination)?;
976        // Translate the function operand.
977        let fn_operand = match fun {
978            hax::FunOperand::Static {
979                def_id,
980                generics,
981                trait_refs,
982                trait_info,
983            } => {
984                trace!("func: {:?}", def_id);
985                let fun_def = self.t_ctx.hax_def(def_id)?;
986                let name = self.t_ctx.hax_def_id_to_name(&fun_def.def_id)?;
987                let panic_lang_items = &["panic", "panic_fmt", "begin_panic"];
988                let panic_names = &[&["core", "panicking", "assert_failed"], EXPLICIT_PANIC_NAME];
989
990                if fun_def
991                    .lang_item
992                    .as_deref()
993                    .is_some_and(|lang_it| panic_lang_items.iter().contains(&lang_it))
994                    || panic_names.iter().any(|panic| name.equals_ref_name(panic))
995                {
996                    // If the call is `panic!`, then the target is `None`.
997                    // I don't know in which other cases it can be `None`.
998                    assert!(target.is_none());
999                    // We ignore the arguments
1000                    return Ok(RawTerminator::Abort(AbortKind::Panic(Some(name))));
1001                } else {
1002                    let fn_ptr =
1003                        self.translate_fn_ptr(span, def_id, generics, trait_refs, trait_info)?;
1004                    FnOperand::Regular(fn_ptr)
1005                }
1006            }
1007            hax::FunOperand::DynamicMove(p) => {
1008                // Call to a local function pointer
1009                let p = self.translate_place(span, p)?;
1010
1011                // TODO: we may have a problem here because as we don't
1012                // know which function is being called, we may not be
1013                // able to filter the arguments properly... But maybe
1014                // this is rather an issue for the statement which creates
1015                // the function pointer, by refering to a top-level function
1016                // for instance.
1017                FnOperand::Move(p)
1018            }
1019        };
1020        let args = self.translate_arguments(span, args)?;
1021        let call = Call {
1022            func: fn_operand,
1023            args,
1024            dest: lval,
1025        };
1026        statements.push(Statement::new(span, RawStatement::Call(call)));
1027        Ok(match target {
1028            Some(target) => {
1029                let target = self.translate_basic_block_id(*target);
1030                RawTerminator::Goto { target }
1031            }
1032            None => RawTerminator::Abort(AbortKind::UndefinedBehavior),
1033        })
1034    }
1035
1036    /// Evaluate function arguments in a context, and return the list of computed
1037    /// values.
1038    fn translate_arguments(
1039        &mut self,
1040        span: Span,
1041        args: &Vec<hax::Spanned<hax::Operand>>,
1042    ) -> Result<Vec<Operand>, Error> {
1043        let mut t_args: Vec<Operand> = Vec::new();
1044        for arg in args.iter().map(|x| &x.node) {
1045            // Translate
1046            let op = self.translate_operand(span, arg)?;
1047            t_args.push(op);
1048        }
1049        Ok(t_args)
1050    }
1051
1052    /// Gather all the lines that start with `//` inside the given span.
1053    fn translate_body_comments(
1054        &mut self,
1055        def: &hax::FullDef,
1056        charon_span: Span,
1057    ) -> Vec<(usize, Vec<String>)> {
1058        if let Some(body_text) = &def.source_text {
1059            let mut comments = body_text
1060                .lines()
1061                // Iter through the lines of this body in reverse order.
1062                .rev()
1063                .enumerate()
1064                // Compute the absolute line number
1065                .map(|(i, line)| (charon_span.span.end.line - i, line))
1066                // Extract the comment if this line starts with `//`
1067                .map(|(line_nbr, line)| (line_nbr, line.trim_start().strip_prefix("//")))
1068                .peekable()
1069                .batching(|iter| {
1070                    // Get the next line. This is not a comment: it's either the last line of the
1071                    // body or a line that wasn't consumed by `peeking_take_while`.
1072                    let (line_nbr, _first) = iter.next()?;
1073                    // Collect all the comments before this line.
1074                    let mut comments = iter
1075                        // `peeking_take_while` ensures we don't consume a line that returns
1076                        // `false`. It will be consumed by the next round of `batching`.
1077                        .peeking_take_while(|(_, opt_comment)| opt_comment.is_some())
1078                        .map(|(_, opt_comment)| opt_comment.unwrap())
1079                        .map(|s| s.strip_prefix(" ").unwrap_or(s))
1080                        .map(str::to_owned)
1081                        .collect_vec();
1082                    comments.reverse();
1083                    Some((line_nbr, comments))
1084                })
1085                .filter(|(_, comments)| !comments.is_empty())
1086                .collect_vec();
1087            comments.reverse();
1088            comments
1089        } else {
1090            Vec::new()
1091        }
1092    }
1093
1094    /// Translate a function body if we can (it has MIR) and we want to (we don't translate bodies
1095    /// declared opaque, and only translate non-local bodies if `extract_opaque_bodies` is set).
1096    pub fn translate_body(
1097        &mut self,
1098        span: Span,
1099        def: &hax::FullDef,
1100    ) -> Result<Result<Body, Opaque>, Error> {
1101        // Stopgap measure because there are still many panics in charon and hax.
1102        let mut this = panic::AssertUnwindSafe(&mut *self);
1103        let res = panic::catch_unwind(move || this.translate_body_aux(def, span));
1104        match res {
1105            Ok(Ok(body)) => Ok(body),
1106            // Translation error
1107            Ok(Err(e)) => Err(e),
1108            Err(_) => {
1109                raise_error!(self, span, "Thread panicked when extracting body.");
1110            }
1111        }
1112    }
1113
1114    fn translate_body_aux(
1115        &mut self,
1116        def: &hax::FullDef,
1117        span: Span,
1118    ) -> Result<Result<Body, Opaque>, Error> {
1119        // Retrieve the body
1120        let Some(body) = self.t_ctx.get_mir(&def.def_id, span)? else {
1121            return Ok(Err(Opaque));
1122        };
1123
1124        // Compute the span information
1125        let span = self.translate_span_from_hax(&body.span);
1126
1127        // Initialize the local variables
1128        trace!("Translating the body locals");
1129        self.locals.arg_count = body.arg_count;
1130        self.translate_body_locals(&body)?;
1131
1132        // Translate the expression body
1133        trace!("Translating the expression body");
1134
1135        // Register the start block
1136        let id = self.translate_basic_block_id(rustc_index::Idx::new(mir::START_BLOCK.as_usize()));
1137        assert!(id == START_BLOCK_ID);
1138
1139        // For as long as there are blocks in the stack, translate them
1140        while let Some(hax_block_id) = self.blocks_stack.pop_front() {
1141            let hax_block = body.basic_blocks.get(hax_block_id).unwrap();
1142            let block_id = self.translate_basic_block_id(hax_block_id);
1143            let block = self.translate_basic_block(&body, hax_block)?;
1144            self.blocks.set_slot(block_id, block);
1145        }
1146
1147        // Create the body
1148        Ok(Ok(Body::Unstructured(ExprBody {
1149            span,
1150            locals: mem::take(&mut self.locals),
1151            body: mem::take(&mut self.blocks),
1152            comments: self.translate_body_comments(def, span),
1153        })))
1154    }
1155}
1156
1157impl<'a> IntoFormatter for &'a BodyTransCtx<'_, '_, '_> {
1158    type C = FmtCtx<'a>;
1159    fn into_fmt(self) -> Self::C {
1160        FmtCtx {
1161            locals: Some(&self.locals),
1162            ..self.i_ctx.into_fmt()
1163        }
1164    }
1165}
charon_driver/translate/translate_bodies.rs

charon_driver/translate/
translate_bodies.rs
