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 (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 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_bound = fn_ref.map(FunDeclRef::into);
474 let fn_ptr: FnPtr = fn_ptr_bound.clone().erase();
475 let src_ty = TyKind::FnDef(fn_ptr_bound).into_ty();
476 let operand = Operand::Const(Box::new(ConstantExpr {
477 value: RawConstantExpr::FnPtr(fn_ptr),
478 ty: src_ty.clone(),
479 }));
480 Ok(Rvalue::UnaryOp(
481 UnOp::Cast(CastKind::FnPtr(src_ty, tgt_ty)),
482 operand,
483 ))
484 }
485 hax::CastKind::PointerCoercion(
486 hax::PointerCoercion::UnsafeFnPointer
487 | hax::PointerCoercion::ReifyFnPointer,
488 ..,
489 ) => Ok(Rvalue::UnaryOp(
490 UnOp::Cast(CastKind::FnPtr(src_ty, tgt_ty)),
491 operand,
492 )),
493 hax::CastKind::Transmute => Ok(Rvalue::UnaryOp(
494 UnOp::Cast(CastKind::Transmute(src_ty, tgt_ty)),
495 operand,
496 )),
497 hax::CastKind::PointerCoercion(hax::PointerCoercion::Unsize, ..) => {
498 let unop = if let (
499 TyKind::Ref(_, deref!(TyKind::Adt(tref1)), kind1),
500 TyKind::Ref(_, deref!(TyKind::Adt(tref2)), kind2),
501 ) = (src_ty.kind(), tgt_ty.kind())
502 && matches!(tref1.id, TypeId::Builtin(BuiltinTy::Array))
503 && matches!(tref2.id, TypeId::Builtin(BuiltinTy::Slice))
504 {
505 assert!(
510 tref1.generics.types.elem_count() == 1
511 && tref1.generics.const_generics.elem_count() == 1
512 );
513 assert!(tref1.generics.types[0] == tref2.generics.types[0]);
514 assert!(kind1 == kind2);
515 UnOp::ArrayToSlice(
516 *kind1,
517 tref1.generics.types[0].clone(),
518 tref1.generics.const_generics[0].clone(),
519 )
520 } else {
521 UnOp::Cast(CastKind::Unsize(src_ty.clone(), tgt_ty.clone()))
522 };
523 Ok(Rvalue::UnaryOp(unop, operand))
524 }
525 }
526 }
527 hax::Rvalue::BinaryOp(binop, (left, right)) => Ok(Rvalue::BinaryOp(
528 self.translate_binaryop_kind(span, *binop)?,
529 self.translate_operand(span, left)?,
530 self.translate_operand(span, right)?,
531 )),
532 hax::Rvalue::NullaryOp(nullop, ty) => {
533 trace!("NullOp: {:?}", nullop);
534 let ty = self.translate_ty(span, ty)?;
535 let op = match nullop {
536 hax::NullOp::SizeOf => NullOp::SizeOf,
537 hax::NullOp::AlignOf => NullOp::AlignOf,
538 hax::NullOp::OffsetOf(fields) => NullOp::OffsetOf(
539 fields
540 .iter()
541 .copied()
542 .map(|(n, idx)| (n, translate_field_id(idx)))
543 .collect(),
544 ),
545 hax::NullOp::UbChecks => NullOp::UbChecks,
546 hax::NullOp::ContractChecks => {
547 raise_error!(self, span, "charon does not support contracts");
548 }
549 };
550 Ok(Rvalue::NullaryOp(op, ty))
551 }
552 hax::Rvalue::UnaryOp(unop, operand) => {
553 let unop = match unop {
554 hax::UnOp::Not => UnOp::Not,
555 hax::UnOp::Neg => UnOp::Neg(OverflowMode::Wrap),
556 hax::UnOp::PtrMetadata => UnOp::PtrMetadata,
557 };
558 Ok(Rvalue::UnaryOp(
559 unop,
560 self.translate_operand(span, operand)?,
561 ))
562 }
563 hax::Rvalue::Discriminant(place) => {
564 let place = self.translate_place(span, place)?;
565 if let TyKind::Adt(tref) = place.ty().kind()
566 && let TypeId::Adt(adt_id) = tref.id
567 {
568 Ok(Rvalue::Discriminant(place, adt_id))
569 } else {
570 raise_error!(
571 self,
572 span,
573 "Unexpected scrutinee type for ReadDiscriminant: {}",
574 place.ty().with_ctx(&self.into_fmt())
575 )
576 }
577 }
578 hax::Rvalue::Aggregate(aggregate_kind, operands) => {
579 let operands_t: Vec<Operand> = operands
594 .raw
595 .iter()
596 .map(|op| self.translate_operand(span, op))
597 .try_collect()?;
598
599 match aggregate_kind {
600 hax::AggregateKind::Array(ty) => {
601 let t_ty = self.translate_ty(span, ty)?;
602 let cg = ConstGeneric::Value(Literal::Scalar(ScalarValue::Usize(
603 operands_t.len() as u64,
604 )));
605 Ok(Rvalue::Aggregate(
606 AggregateKind::Array(t_ty, cg),
607 operands_t,
608 ))
609 }
610 hax::AggregateKind::Tuple => {
611 let tref = TypeDeclRef::new(TypeId::Tuple, GenericArgs::empty());
612 Ok(Rvalue::Aggregate(
613 AggregateKind::Adt(tref, None, None),
614 operands_t,
615 ))
616 }
617 hax::AggregateKind::Adt(
618 item,
619 variant_idx,
620 kind,
621 _user_annotation,
622 field_index,
623 ) => {
624 use hax::AdtKind;
625 trace!("{:?}", rvalue);
626
627 let tref = self.translate_type_decl_ref(span, item)?;
628 let variant_id = match kind {
629 AdtKind::Struct | AdtKind::Union => None,
630 AdtKind::Enum => Some(translate_variant_id(*variant_idx)),
631 };
632 let field_id = match kind {
633 AdtKind::Struct | AdtKind::Enum => None,
634 AdtKind::Union => Some(translate_field_id(field_index.unwrap())),
635 };
636
637 let akind = AggregateKind::Adt(tref, variant_id, field_id);
638 Ok(Rvalue::Aggregate(akind, operands_t))
639 }
640 hax::AggregateKind::Closure(closure_args) => {
641 trace!(
642 "Closure:\n\n- def_id: {:?}\n\n- sig:\n{:?}",
643 closure_args.item.def_id,
644 closure_args.fn_sig
645 );
646 let tref = self.translate_closure_type_ref(span, closure_args)?;
647 let akind = AggregateKind::Adt(tref, None, None);
648 Ok(Rvalue::Aggregate(akind, operands_t))
649 }
650 hax::AggregateKind::RawPtr(ty, is_mut) => {
651 let t_ty = self.translate_ty(span, ty)?;
653 let mutability = if *is_mut {
654 RefKind::Mut
655 } else {
656 RefKind::Shared
657 };
658
659 let akind = AggregateKind::RawPtr(t_ty, mutability);
660
661 Ok(Rvalue::Aggregate(akind, operands_t))
662 }
663 hax::AggregateKind::Coroutine(..)
664 | hax::AggregateKind::CoroutineClosure(..) => {
665 raise_error!(self, span, "Coroutines are not supported");
666 }
667 }
668 }
669 hax::Rvalue::ShallowInitBox(op, ty) => {
670 let op = self.translate_operand(span, op)?;
671 let ty = self.translate_ty(span, ty)?;
672 Ok(Rvalue::ShallowInitBox(op, ty))
673 }
674 hax::Rvalue::ThreadLocalRef(_) => {
675 raise_error!(
676 self,
677 span,
678 "charon does not support thread local references"
679 );
680 }
681 hax::Rvalue::WrapUnsafeBinder { .. } => {
682 raise_error!(
683 self,
684 span,
685 "charon does not support unsafe lifetime binders"
686 );
687 }
688 }
689 }
690
691 fn translate_statement(
695 &mut self,
696 body: &hax::MirBody<hax::mir_kinds::Unknown>,
697 statement: &hax::Statement,
698 ) -> Result<Option<Statement>, Error> {
699 trace!("About to translate statement (MIR) {:?}", statement);
700 let span = self
701 .t_ctx
702 .translate_span_from_source_info(&body.source_scopes, &statement.source_info);
703
704 use hax::StatementKind;
705 let t_statement: Option<RawStatement> = match &*statement.kind {
706 StatementKind::Assign((place, rvalue)) => {
707 let t_place = self.translate_place(span, place)?;
708 let t_rvalue = self.translate_rvalue(span, rvalue)?;
709 Some(RawStatement::Assign(t_place, t_rvalue))
710 }
711 StatementKind::SetDiscriminant {
712 place,
713 variant_index,
714 } => {
715 let t_place = self.translate_place(span, place)?;
716 let variant_id = translate_variant_id(*variant_index);
717 Some(RawStatement::SetDiscriminant(t_place, variant_id))
718 }
719 StatementKind::StorageLive(local) => {
720 let var_id = self.translate_local(local).unwrap();
721 Some(RawStatement::StorageLive(var_id))
722 }
723 StatementKind::StorageDead(local) => {
724 let var_id = self.translate_local(local).unwrap();
725 Some(RawStatement::StorageDead(var_id))
726 }
727 StatementKind::Deinit(place) => {
728 let t_place = self.translate_place(span, place)?;
729 Some(RawStatement::Deinit(t_place))
730 }
731 StatementKind::Intrinsic(hax::NonDivergingIntrinsic::Assume(op)) => {
733 let op = self.translate_operand(span, op)?;
734 Some(RawStatement::Assert(Assert {
735 cond: op,
736 expected: true,
737 on_failure: AbortKind::UndefinedBehavior,
738 }))
739 }
740 StatementKind::Intrinsic(hax::NonDivergingIntrinsic::CopyNonOverlapping(
741 hax::CopyNonOverlapping { src, dst, count },
742 )) => {
743 let src = self.translate_operand(span, src)?;
744 let dst = self.translate_operand(span, dst)?;
745 let count = self.translate_operand(span, count)?;
746 Some(RawStatement::CopyNonOverlapping(Box::new(
747 CopyNonOverlapping { src, dst, count },
748 )))
749 }
750 StatementKind::Retag(_, _) => None,
752 StatementKind::FakeRead(..) | StatementKind::PlaceMention(..) => None,
755 StatementKind::AscribeUserType(_, _) => None,
759 StatementKind::Coverage(_) => None,
761 StatementKind::ConstEvalCounter => None,
764 StatementKind::BackwardIncompatibleDropHint { .. } => None,
766 StatementKind::Nop => None,
767 };
768
769 Ok(t_statement.map(|kind| Statement::new(span, kind)))
771 }
772
773 fn translate_terminator(
775 &mut self,
776 body: &hax::MirBody<hax::mir_kinds::Unknown>,
777 terminator: &hax::Terminator,
778 statements: &mut Vec<Statement>,
779 ) -> Result<Terminator, Error> {
780 trace!("About to translate terminator (MIR) {:?}", terminator);
781 let span = self
784 .t_ctx
785 .translate_span_from_source_info(&body.source_scopes, &terminator.source_info);
786
787 use hax::TerminatorKind;
789 let t_terminator: RawTerminator = match &terminator.kind {
790 TerminatorKind::Goto { target } => {
791 let target = self.translate_basic_block_id(*target);
792 RawTerminator::Goto { target }
793 }
794 TerminatorKind::SwitchInt {
795 discr,
796 targets,
797 otherwise,
798 ..
799 } => {
800 let (discr, discr_ty) = self.translate_operand_with_type(span, discr)?;
802
803 let targets = self.translate_switch_targets(span, &discr_ty, targets, otherwise)?;
805
806 RawTerminator::Switch { discr, targets }
807 }
808 TerminatorKind::UnwindResume => RawTerminator::UnwindResume,
809 TerminatorKind::UnwindTerminate { .. } => {
810 RawTerminator::Abort(AbortKind::UnwindTerminate)
811 }
812 TerminatorKind::Return => RawTerminator::Return,
813 TerminatorKind::Unreachable => RawTerminator::Abort(AbortKind::UndefinedBehavior),
816 TerminatorKind::Drop {
817 place,
818 impl_expr,
819 target,
820 unwind: _, ..
822 } => {
823 let place = self.translate_place(span, place)?;
824 let tref = self.translate_trait_impl_expr(span, impl_expr)?;
825 statements.push(Statement::new(span, RawStatement::Drop(place, tref)));
826 let target = self.translate_basic_block_id(*target);
827 RawTerminator::Goto { target }
828 }
829 TerminatorKind::Call {
830 fun,
831 args,
832 destination,
833 target,
834 unwind,
835 fn_span: _,
836 ..
837 } => self.translate_function_call(span, fun, args, destination, target, unwind)?,
838 TerminatorKind::Assert {
839 cond,
840 expected,
841 msg: _,
842 target,
843 unwind: _, } => {
845 let assert = Assert {
846 cond: self.translate_operand(span, cond)?,
847 expected: *expected,
848 on_failure: AbortKind::Panic(None),
849 };
850 statements.push(Statement::new(span, RawStatement::Assert(assert)));
851 let target = self.translate_basic_block_id(*target);
852 RawTerminator::Goto { target }
853 }
854 TerminatorKind::FalseEdge {
855 real_target,
856 imaginary_target,
857 } => {
858 trace!(
859 "False edge:\n- real target ({:?}):\n{:?}\n- imaginary target ({:?}):\n{:?}",
860 real_target,
861 body.basic_blocks.get(*real_target).unwrap(),
862 imaginary_target,
863 body.basic_blocks.get(*imaginary_target).unwrap(),
864 );
865
866 let target = self.translate_basic_block_id(*real_target);
871 RawTerminator::Goto { target }
872 }
873 TerminatorKind::FalseUnwind {
874 real_target,
875 unwind: _,
876 } => {
877 let target = self.translate_basic_block_id(*real_target);
879 RawTerminator::Goto { target }
880 }
881 TerminatorKind::InlineAsm { .. } => {
882 raise_error!(self, span, "Inline assembly is not supported");
883 }
884 TerminatorKind::CoroutineDrop
885 | TerminatorKind::TailCall { .. }
886 | TerminatorKind::Yield { .. } => {
887 raise_error!(self, span, "Unsupported terminator: {:?}", terminator.kind);
888 }
889 };
890
891 Ok(Terminator::new(span, t_terminator))
893 }
894
895 fn translate_switch_targets(
897 &mut self,
898 span: Span,
899 switch_ty: &Ty,
900 targets: &[(hax::ScalarInt, hax::BasicBlock)],
901 otherwise: &hax::BasicBlock,
902 ) -> Result<SwitchTargets, Error> {
903 trace!("targets: {:?}", targets);
904 let switch_ty = *switch_ty.kind().as_literal().unwrap();
905 match switch_ty {
906 LiteralTy::Bool => {
907 assert_eq!(targets.len(), 1);
908 let (val, target) = targets.first().unwrap();
909 assert_eq!(val.data_le_bytes, [0; 16]);
911 let if_block = self.translate_basic_block_id(*otherwise);
912 let then_block = self.translate_basic_block_id(*target);
913 Ok(SwitchTargets::If(if_block, then_block))
914 }
915 LiteralTy::Integer(int_ty) => {
916 let targets: Vec<(ScalarValue, BlockId)> = targets
917 .iter()
918 .map(|(v, tgt)| {
919 let v = ScalarValue::from_le_bytes(int_ty, v.data_le_bytes);
920 let tgt = self.translate_basic_block_id(*tgt);
921 Ok((v, tgt))
922 })
923 .try_collect()?;
924 let otherwise = self.translate_basic_block_id(*otherwise);
925 Ok(SwitchTargets::SwitchInt(int_ty, targets, otherwise))
926 }
927 _ => raise_error!(self, span, "Can't match on type {switch_ty}"),
928 }
929 }
930
931 #[allow(clippy::too_many_arguments)]
936 fn translate_function_call(
937 &mut self,
938 span: Span,
939 fun: &hax::FunOperand,
940 args: &Vec<hax::Spanned<hax::Operand>>,
941 destination: &hax::Place,
942 target: &Option<hax::BasicBlock>,
943 unwind: &UnwindAction,
944 ) -> Result<RawTerminator, Error> {
945 trace!();
946 let lval = self.translate_place(span, destination)?;
950 let fn_operand = match fun {
952 hax::FunOperand::Static(item) => {
953 trace!("func: {:?}", item.def_id);
954 let fun_def = self.hax_def(&item.def_id)?;
955 let fun_src = TransItemSource::new(item.def_id.clone(), TransItemSourceKind::Fun);
956 let name = self.t_ctx.translate_name(&fun_src)?;
957 let panic_lang_items = &["panic", "panic_fmt", "begin_panic"];
958 let panic_names = &[&["core", "panicking", "assert_failed"], EXPLICIT_PANIC_NAME];
959
960 if fun_def
961 .lang_item
962 .as_deref()
963 .is_some_and(|lang_it| panic_lang_items.iter().contains(&lang_it))
964 || panic_names.iter().any(|panic| name.equals_ref_name(panic))
965 {
966 assert!(target.is_none());
969 return Ok(RawTerminator::Abort(AbortKind::Panic(Some(name))));
971 } else {
972 let fn_ptr = self.translate_fn_ptr(span, item)?.erase();
973 FnOperand::Regular(fn_ptr)
974 }
975 }
976 hax::FunOperand::DynamicMove(p) => {
977 let p = self.translate_place(span, p)?;
979
980 FnOperand::Move(p)
987 }
988 };
989 let args = self.translate_arguments(span, args)?;
990 let call = Call {
991 func: fn_operand,
992 args,
993 dest: lval,
994 };
995
996 let target = match target {
997 Some(target) => self.translate_basic_block_id(*target),
998 None => {
999 let abort =
1000 Terminator::new(span, RawTerminator::Abort(AbortKind::UndefinedBehavior));
1001 self.blocks.push(abort.into_block())
1002 }
1003 };
1004 let on_unwind = match unwind {
1005 UnwindAction::Continue => {
1006 let unwind_continue = Terminator::new(span, RawTerminator::UnwindResume);
1007 self.blocks.push(unwind_continue.into_block())
1008 }
1009 UnwindAction::Unreachable => {
1010 let abort =
1011 Terminator::new(span, RawTerminator::Abort(AbortKind::UndefinedBehavior));
1012 self.blocks.push(abort.into_block())
1013 }
1014 UnwindAction::Terminate(..) => {
1015 let abort = Terminator::new(span, RawTerminator::Abort(AbortKind::UnwindTerminate));
1016 self.blocks.push(abort.into_block())
1017 }
1018 UnwindAction::Cleanup(bb) => self.translate_basic_block_id(*bb),
1019 };
1020 Ok(RawTerminator::Call {
1021 call,
1022 target,
1023 on_unwind,
1024 })
1025 }
1026
1027 fn translate_arguments(
1030 &mut self,
1031 span: Span,
1032 args: &Vec<hax::Spanned<hax::Operand>>,
1033 ) -> Result<Vec<Operand>, Error> {
1034 let mut t_args: Vec<Operand> = Vec::new();
1035 for arg in args.iter().map(|x| &x.node) {
1036 let op = self.translate_operand(span, arg)?;
1038 t_args.push(op);
1039 }
1040 Ok(t_args)
1041 }
1042
1043 fn translate_body_comments(
1045 &mut self,
1046 source_text: &Option<String>,
1047 charon_span: Span,
1048 ) -> Vec<(usize, Vec<String>)> {
1049 if let Some(body_text) = source_text {
1050 let mut comments = body_text
1051 .lines()
1052 .rev()
1054 .enumerate()
1055 .map(|(i, line)| (charon_span.span.end.line - i, line))
1057 .map(|(line_nbr, line)| (line_nbr, line.trim_start().strip_prefix("//")))
1059 .peekable()
1060 .batching(|iter| {
1061 let (line_nbr, _first) = iter.next()?;
1064 let mut comments = iter
1066 .peeking_take_while(|(_, opt_comment)| opt_comment.is_some())
1069 .map(|(_, opt_comment)| opt_comment.unwrap())
1070 .map(|s| s.strip_prefix(" ").unwrap_or(s))
1071 .map(str::to_owned)
1072 .collect_vec();
1073 comments.reverse();
1074 Some((line_nbr, comments))
1075 })
1076 .filter(|(_, comments)| !comments.is_empty())
1077 .collect_vec();
1078 comments.reverse();
1079 comments
1080 } else {
1081 Vec::new()
1082 }
1083 }
1084
1085 pub fn translate_def_body(
1087 &mut self,
1088 span: Span,
1089 def: &hax::FullDef,
1090 ) -> Result<Result<Body, Opaque>, Error> {
1091 let Some(body) = self.t_ctx.get_mir(&def.def_id, span)? else {
1093 return Ok(Err(Opaque));
1094 };
1095 self.translate_body(span, &body, &def.source_text)
1096 }
1097
1098 pub fn translate_body(
1100 &mut self,
1101 span: Span,
1102 body: &hax::MirBody<hax::mir_kinds::Unknown>,
1103 source_text: &Option<String>,
1104 ) -> Result<Result<Body, Opaque>, Error> {
1105 let mut this = panic::AssertUnwindSafe(&mut *self);
1107 let res = panic::catch_unwind(move || this.translate_body_aux(body, source_text));
1108 match res {
1109 Ok(Ok(body)) => Ok(body),
1110 Ok(Err(e)) => Err(e),
1112 Err(_) => {
1113 raise_error!(self, span, "Thread panicked when extracting body.");
1114 }
1115 }
1116 }
1117
1118 fn translate_body_aux(
1119 &mut self,
1120 body: &hax::MirBody<hax::mir_kinds::Unknown>,
1121 source_text: &Option<String>,
1122 ) -> Result<Result<Body, Opaque>, Error> {
1123 let span = self.translate_span_from_hax(&body.span);
1125
1126 trace!("Translating the body locals");
1128 self.locals.arg_count = body.arg_count;
1129 self.translate_body_locals(&body)?;
1130
1131 trace!("Translating the expression body");
1133
1134 let id = self.translate_basic_block_id(rustc_index::Idx::new(mir::START_BLOCK.as_usize()));
1136 assert!(id == START_BLOCK_ID);
1137
1138 while let Some(hax_block_id) = self.blocks_stack.pop_front() {
1140 let hax_block = body.basic_blocks.get(hax_block_id).unwrap();
1141 let block_id = self.translate_basic_block_id(hax_block_id);
1142 let block = self.translate_basic_block(&body, hax_block)?;
1143 self.blocks.set_slot(block_id, block);
1144 }
1145
1146 Ok(Ok(Body::Unstructured(ExprBody {
1148 span,
1149 locals: mem::take(&mut self.locals),
1150 body: mem::take(&mut self.blocks),
1151 comments: self.translate_body_comments(source_text, span),
1152 })))
1153 }
1154}
1155
1156impl<'a> IntoFormatter for &'a BodyTransCtx<'_, '_, '_> {
1157 type C = FmtCtx<'a>;
1158 fn into_fmt(self) -> Self::C {
1159 FmtCtx {
1160 locals: Some(&self.locals),
1161 ..self.i_ctx.into_fmt()
1162 }
1163 }
1164}