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 target,
818 unwind: _, ..
820 } => {
821 let place = self.translate_place(span, place)?;
822 statements.push(Statement::new(span, RawStatement::Drop(place)));
823 let target = self.translate_basic_block_id(*target);
824 RawTerminator::Goto { target }
825 }
826 TerminatorKind::Call {
827 fun,
828 args,
829 destination,
830 target,
831 unwind,
832 fn_span: _,
833 ..
834 } => self.translate_function_call(span, fun, args, destination, target, unwind)?,
835 TerminatorKind::Assert {
836 cond,
837 expected,
838 msg: _,
839 target,
840 unwind: _, } => {
842 let assert = Assert {
843 cond: self.translate_operand(span, cond)?,
844 expected: *expected,
845 on_failure: AbortKind::Panic(None),
846 };
847 statements.push(Statement::new(span, RawStatement::Assert(assert)));
848 let target = self.translate_basic_block_id(*target);
849 RawTerminator::Goto { target }
850 }
851 TerminatorKind::FalseEdge {
852 real_target,
853 imaginary_target,
854 } => {
855 trace!(
856 "False edge:\n- real target ({:?}):\n{:?}\n- imaginary target ({:?}):\n{:?}",
857 real_target,
858 body.basic_blocks.get(*real_target).unwrap(),
859 imaginary_target,
860 body.basic_blocks.get(*imaginary_target).unwrap(),
861 );
862
863 let target = self.translate_basic_block_id(*real_target);
868 RawTerminator::Goto { target }
869 }
870 TerminatorKind::FalseUnwind {
871 real_target,
872 unwind: _,
873 } => {
874 let target = self.translate_basic_block_id(*real_target);
876 RawTerminator::Goto { target }
877 }
878 TerminatorKind::InlineAsm { .. } => {
879 raise_error!(self, span, "Inline assembly is not supported");
880 }
881 TerminatorKind::CoroutineDrop
882 | TerminatorKind::TailCall { .. }
883 | TerminatorKind::Yield { .. } => {
884 raise_error!(self, span, "Unsupported terminator: {:?}", terminator.kind);
885 }
886 };
887
888 Ok(Terminator::new(span, t_terminator))
890 }
891
892 fn translate_switch_targets(
894 &mut self,
895 span: Span,
896 switch_ty: &Ty,
897 targets: &[(hax::ScalarInt, hax::BasicBlock)],
898 otherwise: &hax::BasicBlock,
899 ) -> Result<SwitchTargets, Error> {
900 trace!("targets: {:?}", targets);
901 let switch_ty = *switch_ty.kind().as_literal().unwrap();
902 match switch_ty {
903 LiteralTy::Bool => {
904 assert_eq!(targets.len(), 1);
905 let (val, target) = targets.first().unwrap();
906 assert_eq!(val.data_le_bytes, [0; 16]);
908 let if_block = self.translate_basic_block_id(*otherwise);
909 let then_block = self.translate_basic_block_id(*target);
910 Ok(SwitchTargets::If(if_block, then_block))
911 }
912 LiteralTy::Integer(int_ty) => {
913 let targets: Vec<(ScalarValue, BlockId)> = targets
914 .iter()
915 .map(|(v, tgt)| {
916 let v = ScalarValue::from_le_bytes(int_ty, v.data_le_bytes);
917 let tgt = self.translate_basic_block_id(*tgt);
918 Ok((v, tgt))
919 })
920 .try_collect()?;
921 let otherwise = self.translate_basic_block_id(*otherwise);
922 Ok(SwitchTargets::SwitchInt(int_ty, targets, otherwise))
923 }
924 _ => raise_error!(self, span, "Can't match on type {switch_ty}"),
925 }
926 }
927
928 #[allow(clippy::too_many_arguments)]
933 fn translate_function_call(
934 &mut self,
935 span: Span,
936 fun: &hax::FunOperand,
937 args: &Vec<hax::Spanned<hax::Operand>>,
938 destination: &hax::Place,
939 target: &Option<hax::BasicBlock>,
940 unwind: &UnwindAction,
941 ) -> Result<RawTerminator, Error> {
942 trace!();
943 let lval = self.translate_place(span, destination)?;
947 let fn_operand = match fun {
949 hax::FunOperand::Static(item) => {
950 trace!("func: {:?}", item.def_id);
951 let fun_def = self.hax_def(&item.def_id)?;
952 let fun_src = TransItemSource::new(item.def_id.clone(), TransItemSourceKind::Fun);
953 let name = self.t_ctx.translate_name(&fun_src)?;
954 let panic_lang_items = &["panic", "panic_fmt", "begin_panic"];
955 let panic_names = &[&["core", "panicking", "assert_failed"], EXPLICIT_PANIC_NAME];
956
957 if fun_def
958 .lang_item
959 .as_deref()
960 .is_some_and(|lang_it| panic_lang_items.iter().contains(&lang_it))
961 || panic_names.iter().any(|panic| name.equals_ref_name(panic))
962 {
963 assert!(target.is_none());
966 return Ok(RawTerminator::Abort(AbortKind::Panic(Some(name))));
968 } else {
969 let fn_ptr = self.translate_fn_ptr(span, item)?.erase();
970 FnOperand::Regular(fn_ptr)
971 }
972 }
973 hax::FunOperand::DynamicMove(p) => {
974 let p = self.translate_place(span, p)?;
976
977 FnOperand::Move(p)
984 }
985 };
986 let args = self.translate_arguments(span, args)?;
987 let call = Call {
988 func: fn_operand,
989 args,
990 dest: lval,
991 };
992
993 let target = match target {
994 Some(target) => self.translate_basic_block_id(*target),
995 None => {
996 let abort =
997 Terminator::new(span, RawTerminator::Abort(AbortKind::UndefinedBehavior));
998 self.blocks.push(abort.into_block())
999 }
1000 };
1001 let on_unwind = match unwind {
1002 UnwindAction::Continue => {
1003 let unwind_continue = Terminator::new(span, RawTerminator::UnwindResume);
1004 self.blocks.push(unwind_continue.into_block())
1005 }
1006 UnwindAction::Unreachable => {
1007 let abort =
1008 Terminator::new(span, RawTerminator::Abort(AbortKind::UndefinedBehavior));
1009 self.blocks.push(abort.into_block())
1010 }
1011 UnwindAction::Terminate(..) => {
1012 let abort = Terminator::new(span, RawTerminator::Abort(AbortKind::UnwindTerminate));
1013 self.blocks.push(abort.into_block())
1014 }
1015 UnwindAction::Cleanup(bb) => self.translate_basic_block_id(*bb),
1016 };
1017 Ok(RawTerminator::Call {
1018 call,
1019 target,
1020 on_unwind,
1021 })
1022 }
1023
1024 fn translate_arguments(
1027 &mut self,
1028 span: Span,
1029 args: &Vec<hax::Spanned<hax::Operand>>,
1030 ) -> Result<Vec<Operand>, Error> {
1031 let mut t_args: Vec<Operand> = Vec::new();
1032 for arg in args.iter().map(|x| &x.node) {
1033 let op = self.translate_operand(span, arg)?;
1035 t_args.push(op);
1036 }
1037 Ok(t_args)
1038 }
1039
1040 fn translate_body_comments(
1042 &mut self,
1043 source_text: &Option<String>,
1044 charon_span: Span,
1045 ) -> Vec<(usize, Vec<String>)> {
1046 if let Some(body_text) = source_text {
1047 let mut comments = body_text
1048 .lines()
1049 .rev()
1051 .enumerate()
1052 .map(|(i, line)| (charon_span.span.end.line - i, line))
1054 .map(|(line_nbr, line)| (line_nbr, line.trim_start().strip_prefix("//")))
1056 .peekable()
1057 .batching(|iter| {
1058 let (line_nbr, _first) = iter.next()?;
1061 let mut comments = iter
1063 .peeking_take_while(|(_, opt_comment)| opt_comment.is_some())
1066 .map(|(_, opt_comment)| opt_comment.unwrap())
1067 .map(|s| s.strip_prefix(" ").unwrap_or(s))
1068 .map(str::to_owned)
1069 .collect_vec();
1070 comments.reverse();
1071 Some((line_nbr, comments))
1072 })
1073 .filter(|(_, comments)| !comments.is_empty())
1074 .collect_vec();
1075 comments.reverse();
1076 comments
1077 } else {
1078 Vec::new()
1079 }
1080 }
1081
1082 pub fn translate_def_body(
1084 &mut self,
1085 span: Span,
1086 def: &hax::FullDef,
1087 ) -> Result<Result<Body, Opaque>, Error> {
1088 let Some(body) = self.t_ctx.get_mir(&def.def_id, span)? else {
1090 return Ok(Err(Opaque));
1091 };
1092 self.translate_body(span, &body, &def.source_text)
1093 }
1094
1095 pub fn translate_body(
1097 &mut self,
1098 span: Span,
1099 body: &hax::MirBody<hax::mir_kinds::Unknown>,
1100 source_text: &Option<String>,
1101 ) -> Result<Result<Body, Opaque>, Error> {
1102 let mut this = panic::AssertUnwindSafe(&mut *self);
1104 let res = panic::catch_unwind(move || this.translate_body_aux(body, source_text));
1105 match res {
1106 Ok(Ok(body)) => Ok(body),
1107 Ok(Err(e)) => Err(e),
1109 Err(_) => {
1110 raise_error!(self, span, "Thread panicked when extracting body.");
1111 }
1112 }
1113 }
1114
1115 fn translate_body_aux(
1116 &mut self,
1117 body: &hax::MirBody<hax::mir_kinds::Unknown>,
1118 source_text: &Option<String>,
1119 ) -> Result<Result<Body, Opaque>, Error> {
1120 let span = self.translate_span_from_hax(&body.span);
1122
1123 trace!("Translating the body locals");
1125 self.locals.arg_count = body.arg_count;
1126 self.translate_body_locals(&body)?;
1127
1128 trace!("Translating the expression body");
1130
1131 let id = self.translate_basic_block_id(rustc_index::Idx::new(mir::START_BLOCK.as_usize()));
1133 assert!(id == START_BLOCK_ID);
1134
1135 while let Some(hax_block_id) = self.blocks_stack.pop_front() {
1137 let hax_block = body.basic_blocks.get(hax_block_id).unwrap();
1138 let block_id = self.translate_basic_block_id(hax_block_id);
1139 let block = self.translate_basic_block(&body, hax_block)?;
1140 self.blocks.set_slot(block_id, block);
1141 }
1142
1143 Ok(Ok(Body::Unstructured(ExprBody {
1145 span,
1146 locals: mem::take(&mut self.locals),
1147 body: mem::take(&mut self.blocks),
1148 comments: self.translate_body_comments(source_text, span),
1149 })))
1150 }
1151}
1152
1153impl<'a> IntoFormatter for &'a BodyTransCtx<'_, '_, '_> {
1154 type C = FmtCtx<'a>;
1155 fn into_fmt(self) -> Self::C {
1156 FmtCtx {
1157 locals: Some(&self.locals),
1158 ..self.i_ctx.into_fmt()
1159 }
1160 }
1161}