1use 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
26pub(crate) struct BodyTransCtx<'tcx, 'tctx, 'ictx> {
28 pub i_ctx: &'ictx mut ItemTransCtx<'tcx, 'tctx>,
30
31 pub locals: Locals,
33 pub locals_map: HashMap<usize, LocalId>,
35 pub blocks: Vector<BlockId, BlockData>,
37 pub blocks_map: HashMap<hax::BasicBlock, BlockId>,
41 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
81fn 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 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 fn translate_body_locals(
143 &mut self,
144 body: &hax::MirBody<hax::mir_kinds::Unknown>,
145 ) -> Result<(), Error> {
146 for (index, var) in body.local_decls.raw.iter().enumerate() {
148 trace!("Translating local of index {} and type {:?}", index, var.ty);
149
150 let name: Option<String> = var.name.clone();
152
153 let span = self.translate_span_from_hax(&var.source_info.span);
155 let ty = self.translate_ty(span, &var.ty)?;
156
157 self.push_var(index, ty, name);
159 }
160
161 Ok(())
162 }
163
164 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 None => {
170 self.blocks_stack.push_back(block_id);
172 let id = self.blocks.reserve_slot();
173 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 let mut statements = Vec::new();
187 for statement in &block.statements {
188 trace!("statement: {:?}", statement);
189
190 let opt_statement = self.translate_statement(body, statement)?;
192 if let Some(statement) = opt_statement {
193 statements.push(statement)
194 }
195 }
196
197 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 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 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 assert!(generics.regions.is_empty());
261 assert!(generics.types.elem_count() == 2);
262 assert!(generics.const_generics.is_empty());
263 assert!(field_id == FieldId::ZERO);
264 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 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 raise_error!(self, span, "Unexpected ProjectionElem::OpaqueCast");
333 }
334 };
335
336 Ok(place)
338 }
339 }
340 }
341
342 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 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 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 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 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 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 let tgt_ty = self.translate_ty(span, tgt_ty)?;
433
434 let (mut operand, src_ty) = self.translate_operand_with_type(span, hax_operand)?;
436
437 let cast_kind = 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 CastKind::Scalar(src_ty, tgt_ty)
445 }
446 hax::CastKind::PtrToPtr
447 | hax::CastKind::PointerCoercion(hax::PointerCoercion::MutToConstPointer, ..)
448 | hax::CastKind::PointerCoercion(hax::PointerCoercion::ArrayToPointer, ..)
449 | hax::CastKind::FnPtrToPtr
450 | hax::CastKind::PointerExposeProvenance
451 | hax::CastKind::PointerWithExposedProvenance => {
452 CastKind::RawPtr(src_ty, tgt_ty)
453 }
454 hax::CastKind::PointerCoercion(
455 hax::PointerCoercion::ClosureFnPointer(_),
456 ..,
457 ) => {
458 let op_ty = match hax_operand {
461 hax::Operand::Move(p) | hax::Operand::Copy(p) => p.ty.kind(),
462 hax::Operand::Constant(c) => c.ty.kind(),
463 };
464 let hax::TyKind::Closure(closure) = op_ty else {
465 unreachable!("Non-closure type in PointerCoercion::ClosureFnPointer");
466 };
467 let fn_ref = self.translate_stateless_closure_as_fn_ref(span, closure)?;
468 let fn_ptr_bound = fn_ref.map(FunDeclRef::into);
469 let fn_ptr: FnPtr = fn_ptr_bound.clone().erase();
470 let src_ty = TyKind::FnDef(fn_ptr_bound).into_ty();
471 operand = Operand::Const(Box::new(ConstantExpr {
472 value: RawConstantExpr::FnPtr(fn_ptr),
473 ty: src_ty.clone(),
474 }));
475 CastKind::FnPtr(src_ty, tgt_ty)
476 }
477 hax::CastKind::PointerCoercion(
478 hax::PointerCoercion::UnsafeFnPointer
479 | hax::PointerCoercion::ReifyFnPointer,
480 ..,
481 ) => CastKind::FnPtr(src_ty, tgt_ty),
482 hax::CastKind::Transmute => CastKind::Transmute(src_ty, tgt_ty),
483 hax::CastKind::PointerCoercion(hax::PointerCoercion::Unsize(meta), ..) => {
484 let meta = match meta {
485 hax::UnsizingMetadata::Length(len) => {
486 let len =
487 self.translate_constant_expr_to_const_generic(span, len)?;
488 UnsizingMetadata::Length(len)
489 }
490 hax::UnsizingMetadata::VTablePtr(impl_expr) => {
491 let tref = self.translate_trait_impl_expr(span, impl_expr)?;
492 UnsizingMetadata::VTablePtr(tref)
493 }
494 hax::UnsizingMetadata::Unknown => UnsizingMetadata::Unknown,
495 };
496 CastKind::Unsize(src_ty.clone(), tgt_ty.clone(), meta)
497 }
498 };
499 let unop = UnOp::Cast(cast_kind);
500 Ok(Rvalue::UnaryOp(unop, operand))
501 }
502 hax::Rvalue::BinaryOp(binop, (left, right)) => Ok(Rvalue::BinaryOp(
503 self.translate_binaryop_kind(span, *binop)?,
504 self.translate_operand(span, left)?,
505 self.translate_operand(span, right)?,
506 )),
507 hax::Rvalue::NullaryOp(nullop, ty) => {
508 trace!("NullOp: {:?}", nullop);
509 let ty = self.translate_ty(span, ty)?;
510 let op = match nullop {
511 hax::NullOp::SizeOf => NullOp::SizeOf,
512 hax::NullOp::AlignOf => NullOp::AlignOf,
513 hax::NullOp::OffsetOf(fields) => NullOp::OffsetOf(
514 fields
515 .iter()
516 .copied()
517 .map(|(n, idx)| (n, translate_field_id(idx)))
518 .collect(),
519 ),
520 hax::NullOp::UbChecks => NullOp::UbChecks,
521 hax::NullOp::ContractChecks => {
522 raise_error!(self, span, "charon does not support contracts");
523 }
524 };
525 Ok(Rvalue::NullaryOp(op, ty))
526 }
527 hax::Rvalue::UnaryOp(unop, operand) => {
528 let unop = match unop {
529 hax::UnOp::Not => UnOp::Not,
530 hax::UnOp::Neg => UnOp::Neg(OverflowMode::Wrap),
531 hax::UnOp::PtrMetadata => UnOp::PtrMetadata,
532 };
533 Ok(Rvalue::UnaryOp(
534 unop,
535 self.translate_operand(span, operand)?,
536 ))
537 }
538 hax::Rvalue::Discriminant(place) => {
539 let place = self.translate_place(span, place)?;
540 if !place
542 .ty()
543 .kind()
544 .as_adt()
545 .is_some_and(|tref| tref.id.is_adt())
546 {
547 raise_error!(
548 self,
549 span,
550 "Unexpected scrutinee type for ReadDiscriminant: {}",
551 place.ty().with_ctx(&self.into_fmt())
552 )
553 }
554 Ok(Rvalue::Discriminant(place))
555 }
556 hax::Rvalue::Aggregate(aggregate_kind, operands) => {
557 let operands_t: Vec<Operand> = operands
572 .raw
573 .iter()
574 .map(|op| self.translate_operand(span, op))
575 .try_collect()?;
576
577 match aggregate_kind {
578 hax::AggregateKind::Array(ty) => {
579 let t_ty = self.translate_ty(span, ty)?;
580 let cg = ConstGeneric::Value(Literal::Scalar(ScalarValue::Usize(
581 operands_t.len() as u64,
582 )));
583 Ok(Rvalue::Aggregate(
584 AggregateKind::Array(t_ty, cg),
585 operands_t,
586 ))
587 }
588 hax::AggregateKind::Tuple => {
589 let tref = TypeDeclRef::new(TypeId::Tuple, GenericArgs::empty());
590 Ok(Rvalue::Aggregate(
591 AggregateKind::Adt(tref, None, None),
592 operands_t,
593 ))
594 }
595 hax::AggregateKind::Adt(
596 item,
597 variant_idx,
598 kind,
599 _user_annotation,
600 field_index,
601 ) => {
602 use hax::AdtKind;
603 trace!("{:?}", rvalue);
604
605 let tref = self.translate_type_decl_ref(span, item)?;
606 let variant_id = match kind {
607 AdtKind::Struct | AdtKind::Union => None,
608 AdtKind::Enum => Some(translate_variant_id(*variant_idx)),
609 };
610 let field_id = match kind {
611 AdtKind::Struct | AdtKind::Enum => None,
612 AdtKind::Union => Some(translate_field_id(field_index.unwrap())),
613 };
614
615 let akind = AggregateKind::Adt(tref, variant_id, field_id);
616 Ok(Rvalue::Aggregate(akind, operands_t))
617 }
618 hax::AggregateKind::Closure(closure_args) => {
619 trace!(
620 "Closure:\n\n- def_id: {:?}\n\n- sig:\n{:?}",
621 closure_args.item.def_id, closure_args.fn_sig
622 );
623 let tref = self.translate_closure_type_ref(span, closure_args)?;
624 let akind = AggregateKind::Adt(tref, None, None);
625 Ok(Rvalue::Aggregate(akind, operands_t))
626 }
627 hax::AggregateKind::RawPtr(ty, is_mut) => {
628 let t_ty = self.translate_ty(span, ty)?;
630 let mutability = if *is_mut {
631 RefKind::Mut
632 } else {
633 RefKind::Shared
634 };
635
636 let akind = AggregateKind::RawPtr(t_ty, mutability);
637
638 Ok(Rvalue::Aggregate(akind, operands_t))
639 }
640 hax::AggregateKind::Coroutine(..)
641 | hax::AggregateKind::CoroutineClosure(..) => {
642 raise_error!(self, span, "Coroutines are not supported");
643 }
644 }
645 }
646 hax::Rvalue::ShallowInitBox(op, ty) => {
647 let op = self.translate_operand(span, op)?;
648 let ty = self.translate_ty(span, ty)?;
649 Ok(Rvalue::ShallowInitBox(op, ty))
650 }
651 hax::Rvalue::ThreadLocalRef(_) => {
652 raise_error!(
653 self,
654 span,
655 "charon does not support thread local references"
656 );
657 }
658 hax::Rvalue::WrapUnsafeBinder { .. } => {
659 raise_error!(
660 self,
661 span,
662 "charon does not support unsafe lifetime binders"
663 );
664 }
665 }
666 }
667
668 fn translate_statement(
672 &mut self,
673 body: &hax::MirBody<hax::mir_kinds::Unknown>,
674 statement: &hax::Statement,
675 ) -> Result<Option<Statement>, Error> {
676 trace!("About to translate statement (MIR) {:?}", statement);
677 let span = self
678 .t_ctx
679 .translate_span_from_source_info(&body.source_scopes, &statement.source_info);
680
681 use hax::StatementKind;
682 let t_statement: Option<RawStatement> = match &*statement.kind {
683 StatementKind::Assign((place, rvalue)) => {
684 let t_place = self.translate_place(span, place)?;
685 let t_rvalue = self.translate_rvalue(span, rvalue)?;
686 Some(RawStatement::Assign(t_place, t_rvalue))
687 }
688 StatementKind::SetDiscriminant {
689 place,
690 variant_index,
691 } => {
692 let t_place = self.translate_place(span, place)?;
693 let variant_id = translate_variant_id(*variant_index);
694 Some(RawStatement::SetDiscriminant(t_place, variant_id))
695 }
696 StatementKind::StorageLive(local) => {
697 let var_id = self.translate_local(local).unwrap();
698 Some(RawStatement::StorageLive(var_id))
699 }
700 StatementKind::StorageDead(local) => {
701 let var_id = self.translate_local(local).unwrap();
702 Some(RawStatement::StorageDead(var_id))
703 }
704 StatementKind::Deinit(place) => {
705 let t_place = self.translate_place(span, place)?;
706 Some(RawStatement::Deinit(t_place))
707 }
708 StatementKind::Intrinsic(hax::NonDivergingIntrinsic::Assume(op)) => {
710 let op = self.translate_operand(span, op)?;
711 Some(RawStatement::Assert(Assert {
712 cond: op,
713 expected: true,
714 on_failure: AbortKind::UndefinedBehavior,
715 }))
716 }
717 StatementKind::Intrinsic(hax::NonDivergingIntrinsic::CopyNonOverlapping(
718 hax::CopyNonOverlapping { src, dst, count },
719 )) => {
720 let src = self.translate_operand(span, src)?;
721 let dst = self.translate_operand(span, dst)?;
722 let count = self.translate_operand(span, count)?;
723 Some(RawStatement::CopyNonOverlapping(Box::new(
724 CopyNonOverlapping { src, dst, count },
725 )))
726 }
727 StatementKind::Retag(_, _) => None,
729 StatementKind::FakeRead(..) | StatementKind::PlaceMention(..) => None,
732 StatementKind::AscribeUserType(_, _) => None,
736 StatementKind::Coverage(_) => None,
738 StatementKind::ConstEvalCounter => None,
741 StatementKind::BackwardIncompatibleDropHint { .. } => None,
743 StatementKind::Nop => None,
744 };
745
746 Ok(t_statement.map(|kind| Statement::new(span, kind)))
748 }
749
750 fn translate_terminator(
752 &mut self,
753 body: &hax::MirBody<hax::mir_kinds::Unknown>,
754 terminator: &hax::Terminator,
755 statements: &mut Vec<Statement>,
756 ) -> Result<Terminator, Error> {
757 trace!("About to translate terminator (MIR) {:?}", terminator);
758 let span = self
761 .t_ctx
762 .translate_span_from_source_info(&body.source_scopes, &terminator.source_info);
763
764 use hax::TerminatorKind;
766 let t_terminator: RawTerminator = match &terminator.kind {
767 TerminatorKind::Goto { target } => {
768 let target = self.translate_basic_block_id(*target);
769 RawTerminator::Goto { target }
770 }
771 TerminatorKind::SwitchInt {
772 discr,
773 targets,
774 otherwise,
775 ..
776 } => {
777 let (discr, discr_ty) = self.translate_operand_with_type(span, discr)?;
779
780 let targets = self.translate_switch_targets(span, &discr_ty, targets, otherwise)?;
782
783 RawTerminator::Switch { discr, targets }
784 }
785 TerminatorKind::UnwindResume => RawTerminator::UnwindResume,
786 TerminatorKind::UnwindTerminate { .. } => {
787 RawTerminator::Abort(AbortKind::UnwindTerminate)
788 }
789 TerminatorKind::Return => RawTerminator::Return,
790 TerminatorKind::Unreachable => RawTerminator::Abort(AbortKind::UndefinedBehavior),
793 TerminatorKind::Drop {
794 place,
795 impl_expr,
796 target,
797 unwind: _, ..
799 } => {
800 let place = self.translate_place(span, place)?;
801 let tref = self.translate_trait_impl_expr(span, impl_expr)?;
802 statements.push(Statement::new(span, RawStatement::Drop(place, tref)));
803 let target = self.translate_basic_block_id(*target);
804 RawTerminator::Goto { target }
805 }
806 TerminatorKind::Call {
807 fun,
808 args,
809 destination,
810 target,
811 unwind,
812 fn_span: _,
813 ..
814 } => self.translate_function_call(span, fun, args, destination, target, unwind)?,
815 TerminatorKind::Assert {
816 cond,
817 expected,
818 msg: _,
819 target,
820 unwind: _, } => {
822 let assert = Assert {
823 cond: self.translate_operand(span, cond)?,
824 expected: *expected,
825 on_failure: AbortKind::Panic(None),
826 };
827 statements.push(Statement::new(span, RawStatement::Assert(assert)));
828 let target = self.translate_basic_block_id(*target);
829 RawTerminator::Goto { target }
830 }
831 TerminatorKind::FalseEdge {
832 real_target,
833 imaginary_target,
834 } => {
835 trace!(
836 "False edge:\n- real target ({:?}):\n{:?}\n- imaginary target ({:?}):\n{:?}",
837 real_target,
838 body.basic_blocks.get(*real_target).unwrap(),
839 imaginary_target,
840 body.basic_blocks.get(*imaginary_target).unwrap(),
841 );
842
843 let target = self.translate_basic_block_id(*real_target);
848 RawTerminator::Goto { target }
849 }
850 TerminatorKind::FalseUnwind {
851 real_target,
852 unwind: _,
853 } => {
854 let target = self.translate_basic_block_id(*real_target);
856 RawTerminator::Goto { target }
857 }
858 TerminatorKind::InlineAsm { .. } => {
859 raise_error!(self, span, "Inline assembly is not supported");
860 }
861 TerminatorKind::CoroutineDrop
862 | TerminatorKind::TailCall { .. }
863 | TerminatorKind::Yield { .. } => {
864 raise_error!(self, span, "Unsupported terminator: {:?}", terminator.kind);
865 }
866 };
867
868 Ok(Terminator::new(span, t_terminator))
870 }
871
872 fn translate_switch_targets(
874 &mut self,
875 span: Span,
876 switch_ty: &Ty,
877 targets: &[(hax::ScalarInt, hax::BasicBlock)],
878 otherwise: &hax::BasicBlock,
879 ) -> Result<SwitchTargets, Error> {
880 trace!("targets: {:?}", targets);
881 let switch_ty = *switch_ty.kind().as_literal().unwrap();
882 match switch_ty {
883 LiteralTy::Bool => {
884 assert_eq!(targets.len(), 1);
885 let (val, target) = targets.first().unwrap();
886 assert_eq!(val.data_le_bytes, [0; 16]);
888 let if_block = self.translate_basic_block_id(*otherwise);
889 let then_block = self.translate_basic_block_id(*target);
890 Ok(SwitchTargets::If(if_block, then_block))
891 }
892 LiteralTy::Integer(int_ty) => {
893 let targets: Vec<(ScalarValue, BlockId)> = targets
894 .iter()
895 .map(|(v, tgt)| {
896 let v = ScalarValue::from_le_bytes(int_ty, v.data_le_bytes);
897 let tgt = self.translate_basic_block_id(*tgt);
898 Ok((v, tgt))
899 })
900 .try_collect()?;
901 let otherwise = self.translate_basic_block_id(*otherwise);
902 Ok(SwitchTargets::SwitchInt(int_ty, targets, otherwise))
903 }
904 _ => raise_error!(self, span, "Can't match on type {switch_ty}"),
905 }
906 }
907
908 #[allow(clippy::too_many_arguments)]
913 fn translate_function_call(
914 &mut self,
915 span: Span,
916 fun: &hax::FunOperand,
917 args: &Vec<hax::Spanned<hax::Operand>>,
918 destination: &hax::Place,
919 target: &Option<hax::BasicBlock>,
920 unwind: &UnwindAction,
921 ) -> Result<RawTerminator, Error> {
922 trace!();
923 let lval = self.translate_place(span, destination)?;
927 let fn_operand = match fun {
929 hax::FunOperand::Static(item) => {
930 trace!("func: {:?}", item.def_id);
931 let fun_def = self.hax_def(&item.def_id)?;
932 let fun_src = TransItemSource::new(item.def_id.clone(), TransItemSourceKind::Fun);
933 let name = self.t_ctx.translate_name(&fun_src)?;
934 let panic_lang_items = &["panic", "panic_fmt", "begin_panic"];
935 let panic_names = &[&["core", "panicking", "assert_failed"], EXPLICIT_PANIC_NAME];
936
937 if fun_def
938 .lang_item
939 .as_deref()
940 .is_some_and(|lang_it| panic_lang_items.iter().contains(&lang_it))
941 || panic_names.iter().any(|panic| name.equals_ref_name(panic))
942 {
943 assert!(target.is_none());
946 return Ok(RawTerminator::Abort(AbortKind::Panic(Some(name))));
948 } else {
949 let fn_ptr = self.translate_fn_ptr(span, item)?.erase();
950 FnOperand::Regular(fn_ptr)
951 }
952 }
953 hax::FunOperand::DynamicMove(p) => {
954 let p = self.translate_place(span, p)?;
956
957 FnOperand::Move(p)
964 }
965 };
966 let args = self.translate_arguments(span, args)?;
967 let call = Call {
968 func: fn_operand,
969 args,
970 dest: lval,
971 };
972
973 let target = match target {
974 Some(target) => self.translate_basic_block_id(*target),
975 None => {
976 let abort =
977 Terminator::new(span, RawTerminator::Abort(AbortKind::UndefinedBehavior));
978 self.blocks.push(abort.into_block())
979 }
980 };
981 let on_unwind = match unwind {
982 UnwindAction::Continue => {
983 let unwind_continue = Terminator::new(span, RawTerminator::UnwindResume);
984 self.blocks.push(unwind_continue.into_block())
985 }
986 UnwindAction::Unreachable => {
987 let abort =
988 Terminator::new(span, RawTerminator::Abort(AbortKind::UndefinedBehavior));
989 self.blocks.push(abort.into_block())
990 }
991 UnwindAction::Terminate(..) => {
992 let abort = Terminator::new(span, RawTerminator::Abort(AbortKind::UnwindTerminate));
993 self.blocks.push(abort.into_block())
994 }
995 UnwindAction::Cleanup(bb) => self.translate_basic_block_id(*bb),
996 };
997 Ok(RawTerminator::Call {
998 call,
999 target,
1000 on_unwind,
1001 })
1002 }
1003
1004 fn translate_arguments(
1007 &mut self,
1008 span: Span,
1009 args: &Vec<hax::Spanned<hax::Operand>>,
1010 ) -> Result<Vec<Operand>, Error> {
1011 let mut t_args: Vec<Operand> = Vec::new();
1012 for arg in args.iter().map(|x| &x.node) {
1013 let op = self.translate_operand(span, arg)?;
1015 t_args.push(op);
1016 }
1017 Ok(t_args)
1018 }
1019
1020 fn translate_body_comments(
1022 &mut self,
1023 source_text: &Option<String>,
1024 charon_span: Span,
1025 ) -> Vec<(usize, Vec<String>)> {
1026 if let Some(body_text) = source_text {
1027 let mut comments = body_text
1028 .lines()
1029 .rev()
1031 .enumerate()
1032 .map(|(i, line)| (charon_span.span.end.line - i, line))
1034 .map(|(line_nbr, line)| (line_nbr, line.trim_start().strip_prefix("//")))
1036 .peekable()
1037 .batching(|iter| {
1038 let (line_nbr, _first) = iter.next()?;
1041 let mut comments = iter
1043 .peeking_take_while(|(_, opt_comment)| opt_comment.is_some())
1046 .map(|(_, opt_comment)| opt_comment.unwrap())
1047 .map(|s| s.strip_prefix(" ").unwrap_or(s))
1048 .map(str::to_owned)
1049 .collect_vec();
1050 comments.reverse();
1051 Some((line_nbr, comments))
1052 })
1053 .filter(|(_, comments)| !comments.is_empty())
1054 .collect_vec();
1055 comments.reverse();
1056 comments
1057 } else {
1058 Vec::new()
1059 }
1060 }
1061
1062 pub fn translate_def_body(
1064 &mut self,
1065 span: Span,
1066 def: &hax::FullDef,
1067 ) -> Result<Result<Body, Opaque>, Error> {
1068 let Some(body) = self.t_ctx.get_mir(&def.def_id, span)? else {
1070 return Ok(Err(Opaque));
1071 };
1072 self.translate_body(span, &body, &def.source_text)
1073 }
1074
1075 pub fn translate_body(
1077 &mut self,
1078 span: Span,
1079 body: &hax::MirBody<hax::mir_kinds::Unknown>,
1080 source_text: &Option<String>,
1081 ) -> Result<Result<Body, Opaque>, Error> {
1082 let mut this = panic::AssertUnwindSafe(&mut *self);
1084 let res = panic::catch_unwind(move || this.translate_body_aux(body, source_text));
1085 match res {
1086 Ok(Ok(body)) => Ok(body),
1087 Ok(Err(e)) => Err(e),
1089 Err(_) => {
1090 raise_error!(self, span, "Thread panicked when extracting body.");
1091 }
1092 }
1093 }
1094
1095 fn translate_body_aux(
1096 &mut self,
1097 body: &hax::MirBody<hax::mir_kinds::Unknown>,
1098 source_text: &Option<String>,
1099 ) -> Result<Result<Body, Opaque>, Error> {
1100 let span = self.translate_span_from_hax(&body.span);
1102
1103 trace!("Translating the body locals");
1105 self.locals.arg_count = body.arg_count;
1106 self.translate_body_locals(&body)?;
1107
1108 trace!("Translating the expression body");
1110
1111 let id = self.translate_basic_block_id(rustc_index::Idx::new(mir::START_BLOCK.as_usize()));
1113 assert!(id == START_BLOCK_ID);
1114
1115 while let Some(hax_block_id) = self.blocks_stack.pop_front() {
1117 let hax_block = body.basic_blocks.get(hax_block_id).unwrap();
1118 let block_id = self.translate_basic_block_id(hax_block_id);
1119 let block = self.translate_basic_block(&body, hax_block)?;
1120 self.blocks.set_slot(block_id, block);
1121 }
1122
1123 Ok(Ok(Body::Unstructured(ExprBody {
1125 span,
1126 locals: mem::take(&mut self.locals),
1127 body: mem::take(&mut self.blocks),
1128 comments: self.translate_body_comments(source_text, span),
1129 })))
1130 }
1131}
1132
1133impl<'a> IntoFormatter for &'a BodyTransCtx<'_, '_, '_> {
1134 type C = FmtCtx<'a>;
1135 fn into_fmt(self) -> Self::C {
1136 FmtCtx {
1137 locals: Some(&self.locals),
1138 ..self.i_ctx.into_fmt()
1139 }
1140 }
1141}