charon_driver/translate/
translate_bodies.rs

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

charon_driver/translate/
translate_bodies.rs
