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::ullbc_ast::StatementKind;
16use charon_lib::ast::*;
17use charon_lib::formatter::FmtCtx;
18use charon_lib::formatter::IntoFormatter;
19use charon_lib::ids::Vector;
20use charon_lib::pretty::FmtWithCtx;
21use charon_lib::ullbc_ast::*;
22use hax::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 ptr_size = self.t_ctx.translated.target_information.target_pointer_size;
225 let place = match kind {
226 hax::ProjectionElem::Deref => subplace.project(ProjectionElem::Deref, ty),
227 hax::ProjectionElem::Field(field_kind) => {
228 use hax::ProjectionElemFieldKind::*;
229 let proj_elem = match field_kind {
230 Tuple(id) => {
231 let tref = subplace.ty().kind().as_adt().unwrap();
232 let field_id = translate_field_id(*id);
233 let proj_kind =
234 FieldProjKind::Tuple(tref.generics.types.elem_count());
235 ProjectionElem::Field(proj_kind, field_id)
236 }
237 Adt {
238 typ: _,
239 variant,
240 index,
241 } => {
242 let field_id = translate_field_id(*index);
243 let variant_id = variant.map(translate_variant_id);
244 let tref = subplace.ty().kind().as_adt().unwrap();
245 let generics = &tref.generics;
246 match tref.id {
247 TypeId::Adt(type_id) => {
248 let proj_kind = FieldProjKind::Adt(type_id, variant_id);
249 ProjectionElem::Field(proj_kind, field_id)
250 }
251 TypeId::Tuple => {
252 assert!(generics.regions.is_empty());
253 assert!(variant.is_none());
254 assert!(generics.const_generics.is_empty());
255 let proj_kind =
256 FieldProjKind::Tuple(generics.types.elem_count());
257 ProjectionElem::Field(proj_kind, field_id)
258 }
259 TypeId::Builtin(BuiltinTy::Box) => {
260 assert!(generics.regions.is_empty());
262 assert!(generics.types.elem_count() == 2);
263 assert!(generics.const_generics.is_empty());
264 assert!(field_id == FieldId::ZERO);
265 ProjectionElem::Deref
267 }
268 _ => raise_error!(self, span, "Unexpected field projection"),
269 }
270 }
271 ClosureState(index) => {
272 let field_id = translate_field_id(*index);
273 let type_id = *subplace
274 .ty
275 .kind()
276 .as_adt()
277 .expect("ClosureState projection should apply to an Adt type")
278 .id
279 .as_adt()
280 .unwrap();
281 ProjectionElem::Field(FieldProjKind::Adt(type_id, None), 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 subplace
303 }
304 &hax::ProjectionElem::ConstantIndex {
305 offset,
306 from_end,
307 min_length: _,
308 } => {
309 let offset = Operand::Const(Box::new(
310 ScalarValue::from_uint(ptr_size, UIntTy::Usize, offset as u128)
311 .unwrap()
312 .to_constant(),
313 ));
314 subplace.project(
315 ProjectionElem::Index {
316 offset: Box::new(offset),
317 from_end,
318 },
319 ty,
320 )
321 }
322 &hax::ProjectionElem::Subslice { from, to, from_end } => {
323 let from = Operand::Const(Box::new(
324 ScalarValue::from_uint(ptr_size, UIntTy::Usize, from as u128)
325 .unwrap()
326 .to_constant(),
327 ));
328 let to = Operand::Const(Box::new(
329 ScalarValue::from_uint(ptr_size, UIntTy::Usize, to as u128)
330 .unwrap()
331 .to_constant(),
332 ));
333 subplace.project(
334 ProjectionElem::Subslice {
335 from: Box::new(from),
336 to: Box::new(to),
337 from_end,
338 },
339 ty,
340 )
341 }
342 hax::ProjectionElem::OpaqueCast => {
343 raise_error!(self, span, "Unexpected ProjectionElem::OpaqueCast");
345 }
346 };
347
348 Ok(place)
350 }
351 }
352 }
353
354 fn translate_operand_with_type(
356 &mut self,
357 span: Span,
358 operand: &hax::Operand,
359 ) -> Result<(Operand, Ty), Error> {
360 trace!();
361 match operand {
362 hax::Operand::Copy(place) => {
363 let p = self.translate_place(span, place)?;
364 let ty = p.ty().clone();
365 Ok((Operand::Copy(p), ty))
366 }
367 hax::Operand::Move(place) => {
368 let p = self.translate_place(span, place)?;
369 let ty = p.ty().clone();
370 Ok((Operand::Move(p), ty))
371 }
372 hax::Operand::Constant(const_op) => match &const_op.kind {
373 hax::ConstOperandKind::Value(constant) => {
374 let constant = self.translate_constant_expr_to_constant_expr(span, constant)?;
375 let ty = constant.ty.clone();
376 Ok((Operand::Const(Box::new(constant)), ty))
377 }
378 hax::ConstOperandKind::Promoted(item) => {
379 let ty = self.translate_ty(span, &const_op.ty)?;
380 let global_ref = self.translate_global_decl_ref(span, item)?;
382 let constant = ConstantExpr {
383 kind: ConstantExprKind::Global(global_ref),
384 ty: ty.clone(),
385 };
386 Ok((Operand::Const(Box::new(constant)), ty))
387 }
388 },
389 }
390 }
391
392 fn translate_operand(&mut self, span: Span, operand: &hax::Operand) -> Result<Operand, Error> {
394 trace!();
395 Ok(self.translate_operand_with_type(span, operand)?.0)
396 }
397
398 fn translate_rvalue(
400 &mut self,
401 span: Span,
402 rvalue: &hax::Rvalue,
403 tgt_ty: &Ty,
404 ) -> Result<Rvalue, Error> {
405 match rvalue {
406 hax::Rvalue::Use(operand) => Ok(Rvalue::Use(self.translate_operand(span, operand)?)),
407 hax::Rvalue::CopyForDeref(place) => {
408 let place = self.translate_place(span, place)?;
411 Ok(Rvalue::Use(Operand::Copy(place)))
412 }
413 hax::Rvalue::Repeat(operand, cnst) => {
414 let c = self.translate_constant_expr_to_const_generic(span, cnst)?;
415 let (operand, t) = self.translate_operand_with_type(span, operand)?;
416 Ok(Rvalue::Repeat(operand, t, c))
418 }
419 hax::Rvalue::Ref(_region, borrow_kind, place) => {
420 let place = self.translate_place(span, place)?;
421 let borrow_kind = translate_borrow_kind(*borrow_kind);
422 Ok(Rvalue::Ref {
423 place,
424 kind: borrow_kind,
425 ptr_metadata: Operand::mk_const_unit(),
428 })
429 }
430 hax::Rvalue::RawPtr(mtbl, place) => {
431 let mtbl = match mtbl {
432 hax::RawPtrKind::Mut => RefKind::Mut,
433 hax::RawPtrKind::Const => RefKind::Shared,
434 hax::RawPtrKind::FakeForPtrMetadata => RefKind::Shared,
435 };
436 let place = self.translate_place(span, place)?;
437 Ok(Rvalue::RawPtr {
438 place,
439 kind: mtbl,
440 ptr_metadata: Operand::mk_const_unit(),
443 })
444 }
445 hax::Rvalue::Len(place) => {
446 let place = self.translate_place(span, place)?;
447 let ty = place.ty().clone();
448 let tref = ty.as_adt().unwrap();
449 let cg = match tref.id {
450 TypeId::Builtin(BuiltinTy::Array) => {
451 Some(tref.generics.const_generics[0].clone())
452 }
453 TypeId::Builtin(BuiltinTy::Slice) => None,
454 _ => unreachable!(),
455 };
456 Ok(Rvalue::Len(place, ty, cg))
457 }
458 hax::Rvalue::Cast(cast_kind, hax_operand, tgt_ty) => {
459 trace!("Rvalue::Cast: {:?}", rvalue);
460 let tgt_ty = self.translate_ty(span, tgt_ty)?;
462
463 let (mut operand, src_ty) = self.translate_operand_with_type(span, hax_operand)?;
465
466 let cast_kind = match cast_kind {
467 hax::CastKind::IntToInt
468 | hax::CastKind::IntToFloat
469 | hax::CastKind::FloatToInt
470 | hax::CastKind::FloatToFloat => {
471 let tgt_ty = *tgt_ty.kind().as_literal().unwrap();
472 let src_ty = *src_ty.kind().as_literal().unwrap();
473 CastKind::Scalar(src_ty, tgt_ty)
474 }
475 hax::CastKind::PtrToPtr
476 | hax::CastKind::PointerCoercion(hax::PointerCoercion::MutToConstPointer, ..)
477 | hax::CastKind::PointerCoercion(hax::PointerCoercion::ArrayToPointer, ..)
478 | hax::CastKind::FnPtrToPtr
479 | hax::CastKind::PointerExposeProvenance
480 | hax::CastKind::PointerWithExposedProvenance => {
481 CastKind::RawPtr(src_ty, tgt_ty)
482 }
483 hax::CastKind::PointerCoercion(
484 hax::PointerCoercion::ClosureFnPointer(_),
485 ..,
486 ) => {
487 let op_ty = match hax_operand {
490 hax::Operand::Move(p) | hax::Operand::Copy(p) => p.ty.kind(),
491 hax::Operand::Constant(c) => c.ty.kind(),
492 };
493 let hax::TyKind::Closure(closure) = op_ty else {
494 unreachable!("Non-closure type in PointerCoercion::ClosureFnPointer");
495 };
496 let fn_ref = self.translate_stateless_closure_as_fn_ref(span, closure)?;
497 let fn_ptr_bound = fn_ref.map(FunDeclRef::into);
498 let fn_ptr: FnPtr = fn_ptr_bound.clone().erase();
499 let src_ty = TyKind::FnDef(fn_ptr_bound).into_ty();
500 operand = Operand::Const(Box::new(ConstantExpr {
501 kind: ConstantExprKind::FnPtr(fn_ptr),
502 ty: src_ty.clone(),
503 }));
504 CastKind::FnPtr(src_ty, tgt_ty)
505 }
506 hax::CastKind::PointerCoercion(
507 hax::PointerCoercion::UnsafeFnPointer
508 | hax::PointerCoercion::ReifyFnPointer,
509 ..,
510 ) => CastKind::FnPtr(src_ty, tgt_ty),
511 hax::CastKind::Transmute => CastKind::Transmute(src_ty, tgt_ty),
512 hax::CastKind::PointerCoercion(hax::PointerCoercion::Unsize(meta), ..) => {
513 let meta = match meta {
514 hax::UnsizingMetadata::Length(len) => {
515 let len =
516 self.translate_constant_expr_to_const_generic(span, len)?;
517 UnsizingMetadata::Length(len)
518 }
519 hax::UnsizingMetadata::VTablePtr(impl_expr) => {
520 let tref = self.translate_trait_impl_expr(span, impl_expr)?;
521 match &impl_expr.r#impl {
522 hax::ImplExprAtom::Concrete(tref) => {
523 let _: GlobalDeclId = self.register_item(
525 span,
526 tref,
527 TransItemSourceKind::VTableInstance(
528 TraitImplSource::Normal,
529 ),
530 );
531 }
532 _ => {
534 trace!(
535 "impl_expr not triggering registering vtable: {:?}",
536 impl_expr
537 )
538 }
539 };
540 UnsizingMetadata::VTablePtr(tref)
541 }
542 hax::UnsizingMetadata::Unknown => UnsizingMetadata::Unknown,
543 };
544 CastKind::Unsize(src_ty.clone(), tgt_ty.clone(), meta)
545 }
546 };
547 let unop = UnOp::Cast(cast_kind);
548 Ok(Rvalue::UnaryOp(unop, operand))
549 }
550 hax::Rvalue::BinaryOp(binop, (left, right)) => Ok(Rvalue::BinaryOp(
551 self.translate_binaryop_kind(span, *binop)?,
552 self.translate_operand(span, left)?,
553 self.translate_operand(span, right)?,
554 )),
555 hax::Rvalue::NullaryOp(nullop, ty) => {
556 trace!("NullOp: {:?}", nullop);
557 let ty = self.translate_ty(span, ty)?;
558 let op = match nullop {
559 hax::NullOp::SizeOf => NullOp::SizeOf,
560 hax::NullOp::AlignOf => NullOp::AlignOf,
561 hax::NullOp::OffsetOf(fields) => NullOp::OffsetOf(
562 fields
563 .iter()
564 .copied()
565 .map(|(n, idx)| (n, translate_field_id(idx)))
566 .collect(),
567 ),
568 hax::NullOp::UbChecks => NullOp::UbChecks,
569 hax::NullOp::ContractChecks => {
570 raise_error!(self, span, "charon does not support contracts");
571 }
572 };
573 Ok(Rvalue::NullaryOp(op, ty))
574 }
575 hax::Rvalue::UnaryOp(unop, operand) => {
576 let operand = self.translate_operand(span, operand)?;
577 let unop = match unop {
578 hax::UnOp::Not => UnOp::Not,
579 hax::UnOp::Neg => UnOp::Neg(OverflowMode::Wrap),
580 hax::UnOp::PtrMetadata => match operand {
581 Operand::Copy(p) | Operand::Move(p) => {
582 return Ok(Rvalue::Use(Operand::Copy(
583 p.project(ProjectionElem::PtrMetadata, tgt_ty.clone()),
584 )));
585 }
586 Operand::Const(_) => panic!("const metadata"),
587 },
588 };
589 Ok(Rvalue::UnaryOp(unop, operand))
590 }
591 hax::Rvalue::Discriminant(place) => {
592 let place = self.translate_place(span, place)?;
593 if !place
595 .ty()
596 .kind()
597 .as_adt()
598 .is_some_and(|tref| tref.id.is_adt())
599 {
600 raise_error!(
601 self,
602 span,
603 "Unexpected scrutinee type for ReadDiscriminant: {}",
604 place.ty().with_ctx(&self.into_fmt())
605 )
606 }
607 Ok(Rvalue::Discriminant(place))
608 }
609 hax::Rvalue::Aggregate(aggregate_kind, operands) => {
610 let operands_t: Vec<Operand> = operands
625 .raw
626 .iter()
627 .map(|op| self.translate_operand(span, op))
628 .try_collect()?;
629 let ptr_size = self.t_ctx.translated.target_information.target_pointer_size;
630
631 match aggregate_kind {
632 hax::AggregateKind::Array(ty) => {
633 let t_ty = self.translate_ty(span, ty)?;
634 let cg = ConstGeneric::Value(Literal::Scalar(
635 ScalarValue::from_uint(
636 ptr_size,
637 UIntTy::Usize,
638 operands_t.len() as u128,
639 )
640 .unwrap(),
641 ));
642 Ok(Rvalue::Aggregate(
643 AggregateKind::Array(t_ty, cg),
644 operands_t,
645 ))
646 }
647 hax::AggregateKind::Tuple => {
648 let tref = TypeDeclRef::new(TypeId::Tuple, GenericArgs::empty());
649 Ok(Rvalue::Aggregate(
650 AggregateKind::Adt(tref, None, None),
651 operands_t,
652 ))
653 }
654 hax::AggregateKind::Adt(
655 item,
656 variant_idx,
657 kind,
658 _user_annotation,
659 field_index,
660 ) => {
661 use hax::AdtKind;
662 trace!("{:?}", rvalue);
663
664 let tref = self.translate_type_decl_ref(span, item)?;
665 let variant_id = match kind {
666 AdtKind::Struct | AdtKind::Union => None,
667 AdtKind::Enum => Some(translate_variant_id(*variant_idx)),
668 };
669 let field_id = match kind {
670 AdtKind::Struct | AdtKind::Enum => None,
671 AdtKind::Union => Some(translate_field_id(field_index.unwrap())),
672 };
673
674 let akind = AggregateKind::Adt(tref, variant_id, field_id);
675 Ok(Rvalue::Aggregate(akind, operands_t))
676 }
677 hax::AggregateKind::Closure(closure_args) => {
678 trace!(
679 "Closure:\n\n- def_id: {:?}\n\n- sig:\n{:?}",
680 closure_args.item.def_id, closure_args.fn_sig
681 );
682 let tref = self.translate_closure_type_ref(span, closure_args)?;
683 let akind = AggregateKind::Adt(tref, None, None);
684 Ok(Rvalue::Aggregate(akind, operands_t))
685 }
686 hax::AggregateKind::RawPtr(ty, is_mut) => {
687 let t_ty = self.translate_ty(span, ty)?;
689 let mutability = if *is_mut {
690 RefKind::Mut
691 } else {
692 RefKind::Shared
693 };
694
695 let akind = AggregateKind::RawPtr(t_ty, mutability);
696
697 Ok(Rvalue::Aggregate(akind, operands_t))
698 }
699 hax::AggregateKind::Coroutine(..)
700 | hax::AggregateKind::CoroutineClosure(..) => {
701 raise_error!(self, span, "Coroutines are not supported");
702 }
703 }
704 }
705 hax::Rvalue::ShallowInitBox(op, ty) => {
706 let op = self.translate_operand(span, op)?;
707 let ty = self.translate_ty(span, ty)?;
708 Ok(Rvalue::ShallowInitBox(op, ty))
709 }
710 hax::Rvalue::ThreadLocalRef(_) => {
711 raise_error!(
712 self,
713 span,
714 "charon does not support thread local references"
715 );
716 }
717 hax::Rvalue::WrapUnsafeBinder { .. } => {
718 raise_error!(
719 self,
720 span,
721 "charon does not support unsafe lifetime binders"
722 );
723 }
724 }
725 }
726
727 fn translate_statement(
731 &mut self,
732 body: &hax::MirBody<hax::mir_kinds::Unknown>,
733 statement: &hax::Statement,
734 ) -> Result<Option<Statement>, Error> {
735 trace!("About to translate statement (MIR) {:?}", statement);
736 let span = self
737 .t_ctx
738 .translate_span_from_source_info(&body.source_scopes, &statement.source_info);
739
740 let t_statement: Option<StatementKind> = match &*statement.kind {
741 hax::StatementKind::Assign((place, rvalue)) => {
742 let t_place = self.translate_place(span, place)?;
743 let t_rvalue = self.translate_rvalue(span, rvalue, t_place.ty())?;
744 Some(StatementKind::Assign(t_place, t_rvalue))
745 }
746 hax::StatementKind::SetDiscriminant {
747 place,
748 variant_index,
749 } => {
750 let t_place = self.translate_place(span, place)?;
751 let variant_id = translate_variant_id(*variant_index);
752 Some(StatementKind::SetDiscriminant(t_place, variant_id))
753 }
754 hax::StatementKind::StorageLive(local) => {
755 let var_id = self.translate_local(local).unwrap();
756 Some(StatementKind::StorageLive(var_id))
757 }
758 hax::StatementKind::StorageDead(local) => {
759 let var_id = self.translate_local(local).unwrap();
760 Some(StatementKind::StorageDead(var_id))
761 }
762 hax::StatementKind::Deinit(place) => {
763 let t_place = self.translate_place(span, place)?;
764 Some(StatementKind::Deinit(t_place))
765 }
766 hax::StatementKind::Intrinsic(hax::NonDivergingIntrinsic::Assume(op)) => {
768 let op = self.translate_operand(span, op)?;
769 Some(StatementKind::Assert(Assert {
770 cond: op,
771 expected: true,
772 on_failure: AbortKind::UndefinedBehavior,
773 }))
774 }
775 hax::StatementKind::Intrinsic(hax::NonDivergingIntrinsic::CopyNonOverlapping(
776 hax::CopyNonOverlapping { src, dst, count },
777 )) => {
778 let src = self.translate_operand(span, src)?;
779 let dst = self.translate_operand(span, dst)?;
780 let count = self.translate_operand(span, count)?;
781 Some(StatementKind::CopyNonOverlapping(Box::new(
782 CopyNonOverlapping { src, dst, count },
783 )))
784 }
785 hax::StatementKind::Retag(_, _) => None,
787 hax::StatementKind::FakeRead(..) | hax::StatementKind::PlaceMention(..) => None,
790 hax::StatementKind::AscribeUserType(_, _) => None,
794 hax::StatementKind::Coverage(_) => None,
796 hax::StatementKind::ConstEvalCounter => None,
799 hax::StatementKind::BackwardIncompatibleDropHint { .. } => None,
801 hax::StatementKind::Nop => None,
802 };
803
804 Ok(t_statement.map(|kind| Statement::new(span, kind)))
806 }
807
808 fn translate_terminator(
810 &mut self,
811 body: &hax::MirBody<hax::mir_kinds::Unknown>,
812 terminator: &hax::Terminator,
813 statements: &mut Vec<Statement>,
814 ) -> Result<Terminator, Error> {
815 trace!("About to translate terminator (MIR) {:?}", terminator);
816 let span = self
819 .t_ctx
820 .translate_span_from_source_info(&body.source_scopes, &terminator.source_info);
821
822 use hax::TerminatorKind;
824 let t_terminator: ullbc_ast::TerminatorKind = match &terminator.kind {
825 TerminatorKind::Goto { target } => {
826 let target = self.translate_basic_block_id(*target);
827 ullbc_ast::TerminatorKind::Goto { target }
828 }
829 TerminatorKind::SwitchInt {
830 discr,
831 targets,
832 otherwise,
833 ..
834 } => {
835 let (discr, discr_ty) = self.translate_operand_with_type(span, discr)?;
837
838 let targets = self.translate_switch_targets(span, &discr_ty, targets, otherwise)?;
840
841 ullbc_ast::TerminatorKind::Switch { discr, targets }
842 }
843 TerminatorKind::UnwindResume => ullbc_ast::TerminatorKind::UnwindResume,
844 TerminatorKind::UnwindTerminate { .. } => {
845 ullbc_ast::TerminatorKind::Abort(AbortKind::UnwindTerminate)
846 }
847 TerminatorKind::Return => ullbc_ast::TerminatorKind::Return,
848 TerminatorKind::Unreachable => {
851 ullbc_ast::TerminatorKind::Abort(AbortKind::UndefinedBehavior)
852 }
853 TerminatorKind::Drop {
854 place,
855 impl_expr,
856 target,
857 unwind: _, ..
859 } => {
860 let place = self.translate_place(span, place)?;
861 let tref = self.translate_trait_impl_expr(span, impl_expr)?;
862 statements.push(Statement::new(span, StatementKind::Drop(place, tref)));
863 let target = self.translate_basic_block_id(*target);
864 ullbc_ast::TerminatorKind::Goto { target }
865 }
866 TerminatorKind::Call {
867 fun,
868 args,
869 destination,
870 target,
871 unwind,
872 fn_span: _,
873 ..
874 } => self.translate_function_call(span, fun, args, destination, target, unwind)?,
875 TerminatorKind::Assert {
876 cond,
877 expected,
878 msg: _,
879 target,
880 unwind: _, } => {
882 let assert = Assert {
883 cond: self.translate_operand(span, cond)?,
884 expected: *expected,
885 on_failure: AbortKind::Panic(None),
886 };
887 statements.push(Statement::new(span, StatementKind::Assert(assert)));
888 let target = self.translate_basic_block_id(*target);
889 ullbc_ast::TerminatorKind::Goto { target }
890 }
891 TerminatorKind::FalseEdge {
892 real_target,
893 imaginary_target,
894 } => {
895 trace!(
896 "False edge:\n- real target ({:?}):\n{:?}\n- imaginary target ({:?}):\n{:?}",
897 real_target,
898 body.basic_blocks.get(*real_target).unwrap(),
899 imaginary_target,
900 body.basic_blocks.get(*imaginary_target).unwrap(),
901 );
902
903 let target = self.translate_basic_block_id(*real_target);
908 ullbc_ast::TerminatorKind::Goto { target }
909 }
910 TerminatorKind::FalseUnwind {
911 real_target,
912 unwind: _,
913 } => {
914 let target = self.translate_basic_block_id(*real_target);
916 ullbc_ast::TerminatorKind::Goto { target }
917 }
918 TerminatorKind::InlineAsm { .. } => {
919 raise_error!(self, span, "Inline assembly is not supported");
920 }
921 TerminatorKind::CoroutineDrop
922 | TerminatorKind::TailCall { .. }
923 | TerminatorKind::Yield { .. } => {
924 raise_error!(self, span, "Unsupported terminator: {:?}", terminator.kind);
925 }
926 };
927
928 Ok(Terminator::new(span, t_terminator))
930 }
931
932 fn translate_switch_targets(
934 &mut self,
935 span: Span,
936 switch_ty: &Ty,
937 targets: &[(hax::ScalarInt, hax::BasicBlock)],
938 otherwise: &hax::BasicBlock,
939 ) -> Result<SwitchTargets, Error> {
940 trace!("targets: {:?}", targets);
941 let switch_ty = *switch_ty.kind().as_literal().unwrap();
942 match switch_ty {
943 LiteralTy::Bool => {
944 assert_eq!(targets.len(), 1);
945 let (val, target) = targets.first().unwrap();
946 assert_eq!(val.data_le_bytes, [0; 16]);
948 let if_block = self.translate_basic_block_id(*otherwise);
949 let then_block = self.translate_basic_block_id(*target);
950 Ok(SwitchTargets::If(if_block, then_block))
951 }
952 LiteralTy::Char => {
953 let targets: Vec<(Literal, BlockId)> = targets
954 .iter()
955 .map(|(v, tgt)| {
956 let b: u128 = u128::from_le_bytes(v.data_le_bytes);
957 let v = Literal::char_from_le_bytes(b);
958 let tgt = self.translate_basic_block_id(*tgt);
959 (v, tgt)
960 })
961 .collect();
962 let otherwise = self.translate_basic_block_id(*otherwise);
963 Ok(SwitchTargets::SwitchInt(
964 LiteralTy::Char,
965 targets,
966 otherwise,
967 ))
968 }
969 LiteralTy::Int(int_ty) => {
970 let targets: Vec<(Literal, BlockId)> = targets
971 .iter()
972 .map(|(v, tgt)| {
973 let v = Literal::Scalar(ScalarValue::from_le_bytes(
974 IntegerTy::Signed(int_ty),
975 v.data_le_bytes,
976 ));
977 let tgt = self.translate_basic_block_id(*tgt);
978 (v, tgt)
979 })
980 .collect();
981 let otherwise = self.translate_basic_block_id(*otherwise);
982 Ok(SwitchTargets::SwitchInt(switch_ty, targets, otherwise))
983 }
984 LiteralTy::UInt(uint_ty) => {
985 let targets: Vec<(Literal, BlockId)> = targets
986 .iter()
987 .map(|(v, tgt)| {
988 let v = Literal::Scalar(ScalarValue::from_le_bytes(
989 IntegerTy::Unsigned(uint_ty),
990 v.data_le_bytes,
991 ));
992 let tgt = self.translate_basic_block_id(*tgt);
993 (v, tgt)
994 })
995 .collect();
996 let otherwise = self.translate_basic_block_id(*otherwise);
997 Ok(SwitchTargets::SwitchInt(
998 LiteralTy::UInt(uint_ty),
999 targets,
1000 otherwise,
1001 ))
1002 }
1003 _ => raise_error!(self, span, "Can't match on type {switch_ty}"),
1004 }
1005 }
1006
1007 #[allow(clippy::too_many_arguments)]
1012 fn translate_function_call(
1013 &mut self,
1014 span: Span,
1015 fun: &hax::FunOperand,
1016 args: &Vec<hax::Spanned<hax::Operand>>,
1017 destination: &hax::Place,
1018 target: &Option<hax::BasicBlock>,
1019 unwind: &UnwindAction,
1020 ) -> Result<TerminatorKind, Error> {
1021 trace!();
1022 let lval = self.translate_place(span, destination)?;
1026 let fn_operand = match fun {
1028 hax::FunOperand::Static(item) => {
1029 trace!("func: {:?}", item.def_id);
1030 let fun_def = self.hax_def(item)?;
1031 let name = self.t_ctx.translate_name(&TransItemSource::polymorphic(
1032 &item.def_id,
1033 TransItemSourceKind::Fun,
1034 ))?;
1035 let panic_lang_items = &["panic", "panic_fmt", "begin_panic"];
1036 let panic_names = &[&["core", "panicking", "assert_failed"], EXPLICIT_PANIC_NAME];
1037
1038 if fun_def
1039 .lang_item
1040 .as_deref()
1041 .is_some_and(|lang_it| panic_lang_items.iter().contains(&lang_it))
1042 || panic_names.iter().any(|panic| name.equals_ref_name(panic))
1043 {
1044 assert!(target.is_none());
1047 return Ok(TerminatorKind::Abort(AbortKind::Panic(Some(name))));
1049 } else {
1050 let fn_ptr = self
1051 .translate_fn_ptr(span, item, TransItemSourceKind::Fun)?
1052 .erase();
1053 FnOperand::Regular(fn_ptr)
1054 }
1055 }
1056 hax::FunOperand::DynamicMove(p) => {
1057 let p = self.translate_place(span, p)?;
1059
1060 FnOperand::Move(p)
1067 }
1068 };
1069 let args = self.translate_arguments(span, args)?;
1070 let call = Call {
1071 func: fn_operand,
1072 args,
1073 dest: lval,
1074 };
1075
1076 let target = match target {
1077 Some(target) => self.translate_basic_block_id(*target),
1078 None => {
1079 let abort =
1080 Terminator::new(span, TerminatorKind::Abort(AbortKind::UndefinedBehavior));
1081 self.blocks.push(abort.into_block())
1082 }
1083 };
1084 let on_unwind = match unwind {
1085 UnwindAction::Continue => {
1086 let unwind_continue = Terminator::new(span, TerminatorKind::UnwindResume);
1087 self.blocks.push(unwind_continue.into_block())
1088 }
1089 UnwindAction::Unreachable => {
1090 let abort =
1091 Terminator::new(span, TerminatorKind::Abort(AbortKind::UndefinedBehavior));
1092 self.blocks.push(abort.into_block())
1093 }
1094 UnwindAction::Terminate(..) => {
1095 let abort =
1096 Terminator::new(span, TerminatorKind::Abort(AbortKind::UnwindTerminate));
1097 self.blocks.push(abort.into_block())
1098 }
1099 UnwindAction::Cleanup(bb) => self.translate_basic_block_id(*bb),
1100 };
1101 Ok(TerminatorKind::Call {
1102 call,
1103 target,
1104 on_unwind,
1105 })
1106 }
1107
1108 fn translate_arguments(
1111 &mut self,
1112 span: Span,
1113 args: &Vec<hax::Spanned<hax::Operand>>,
1114 ) -> Result<Vec<Operand>, Error> {
1115 let mut t_args: Vec<Operand> = Vec::new();
1116 for arg in args.iter().map(|x| &x.node) {
1117 let op = self.translate_operand(span, arg)?;
1119 t_args.push(op);
1120 }
1121 Ok(t_args)
1122 }
1123
1124 fn translate_body_comments(
1126 &mut self,
1127 source_text: &Option<String>,
1128 charon_span: Span,
1129 ) -> Vec<(usize, Vec<String>)> {
1130 if let Some(body_text) = source_text {
1131 let mut comments = body_text
1132 .lines()
1133 .rev()
1135 .enumerate()
1136 .map(|(i, line)| (charon_span.data.end.line - i, line))
1138 .map(|(line_nbr, line)| (line_nbr, line.trim_start().strip_prefix("//")))
1140 .peekable()
1141 .batching(|iter| {
1142 let (line_nbr, _first) = iter.next()?;
1145 let mut comments = iter
1147 .peeking_take_while(|(_, opt_comment)| opt_comment.is_some())
1150 .map(|(_, opt_comment)| opt_comment.unwrap())
1151 .map(|s| s.strip_prefix(" ").unwrap_or(s))
1152 .map(str::to_owned)
1153 .collect_vec();
1154 comments.reverse();
1155 Some((line_nbr, comments))
1156 })
1157 .filter(|(_, comments)| !comments.is_empty())
1158 .collect_vec();
1159 comments.reverse();
1160 comments
1161 } else {
1162 Vec::new()
1163 }
1164 }
1165
1166 pub fn translate_def_body(
1168 &mut self,
1169 span: Span,
1170 def: &hax::FullDef,
1171 ) -> Result<Result<Body, Opaque>, Error> {
1172 let Some(body) = self.get_mir(def.this(), span)? else {
1174 return Ok(Err(Opaque));
1175 };
1176 self.translate_body(span, &body, &def.source_text)
1177 }
1178
1179 pub fn translate_body(
1181 &mut self,
1182 span: Span,
1183 body: &hax::MirBody<hax::mir_kinds::Unknown>,
1184 source_text: &Option<String>,
1185 ) -> Result<Result<Body, Opaque>, Error> {
1186 let mut this = panic::AssertUnwindSafe(&mut *self);
1188 let res = panic::catch_unwind(move || this.translate_body_aux(body, source_text));
1189 match res {
1190 Ok(Ok(body)) => Ok(body),
1191 Ok(Err(e)) => Err(e),
1193 Err(_) => {
1194 raise_error!(self, span, "Thread panicked when extracting body.");
1195 }
1196 }
1197 }
1198
1199 fn translate_body_aux(
1200 &mut self,
1201 body: &hax::MirBody<hax::mir_kinds::Unknown>,
1202 source_text: &Option<String>,
1203 ) -> Result<Result<Body, Opaque>, Error> {
1204 let span = self.translate_span_from_hax(&body.span);
1206
1207 trace!("Translating the body locals");
1209 self.locals.arg_count = body.arg_count;
1210 self.translate_body_locals(&body)?;
1211
1212 trace!("Translating the expression body");
1214
1215 let id = self.translate_basic_block_id(rustc_index::Idx::new(mir::START_BLOCK.as_usize()));
1217 assert!(id == START_BLOCK_ID);
1218
1219 while let Some(hax_block_id) = self.blocks_stack.pop_front() {
1221 let hax_block = body.basic_blocks.get(hax_block_id).unwrap();
1222 let block_id = self.translate_basic_block_id(hax_block_id);
1223 let block = self.translate_basic_block(&body, hax_block)?;
1224 self.blocks.set_slot(block_id, block);
1225 }
1226
1227 Ok(Ok(Body::Unstructured(ExprBody {
1229 span,
1230 locals: mem::take(&mut self.locals),
1231 body: mem::take(&mut self.blocks),
1232 comments: self.translate_body_comments(source_text, span),
1233 })))
1234 }
1235}
1236
1237impl<'a> IntoFormatter for &'a BodyTransCtx<'_, '_, '_> {
1238 type C = FmtCtx<'a>;
1239 fn into_fmt(self) -> Self::C {
1240 FmtCtx {
1241 locals: Some(&self.locals),
1242 ..self.i_ctx.into_fmt()
1243 }
1244 }
1245}