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