1use std::panic;
7
8use crate::translate::translate_bodies::BodyTransCtx;
9
10use super::translate_ctx::*;
11use charon_lib::ast::*;
12use charon_lib::common::*;
13use charon_lib::formatter::{Formatter, IntoFormatter};
14use charon_lib::ids::Vector;
15use charon_lib::ullbc_ast::*;
16use hax_frontend_exporter as hax;
17use itertools::Itertools;
18
19impl ItemTransCtx<'_, '_> {
20 pub(crate) fn get_item_kind(
21 &mut self,
22 span: Span,
23 def: &hax::FullDef,
24 ) -> Result<ItemKind, Error> {
25 let assoc = match def.kind() {
26 hax::FullDefKind::AssocTy {
27 associated_item, ..
28 }
29 | hax::FullDefKind::AssocConst {
30 associated_item, ..
31 }
32 | hax::FullDefKind::AssocFn {
33 associated_item, ..
34 } => associated_item,
35 _ => return Ok(ItemKind::Regular),
36 };
37 Ok(match &assoc.container {
38 hax::AssocItemContainer::InherentImplContainer { .. } => ItemKind::Regular,
45 hax::AssocItemContainer::TraitImplContainer {
52 impl_id,
53 impl_generics,
54 impl_required_impl_exprs,
55 implemented_trait_ref,
56 implemented_trait_item,
57 overrides_default,
58 ..
59 } => {
60 let impl_id = self.register_trait_impl_id(span, impl_id);
61 let impl_ref = TraitImplRef {
62 impl_id,
63 generics: Box::new(self.translate_generic_args(
64 span,
65 impl_generics,
66 impl_required_impl_exprs,
67 None,
68 GenericsSource::item(impl_id),
69 )?),
70 };
71 let trait_ref = self.translate_trait_ref(span, implemented_trait_ref)?;
72 if matches!(def.kind(), hax::FullDefKind::AssocFn { .. }) {
73 let _ = self.register_fun_decl_id(span, implemented_trait_item);
77 }
78 ItemKind::TraitImpl {
79 impl_ref,
80 trait_ref,
81 item_name: TraitItemName(assoc.name.clone()),
82 reuses_default: !overrides_default,
83 }
84 }
85 hax::AssocItemContainer::TraitContainer { trait_ref, .. } => {
93 let trait_ref = self.translate_trait_ref(span, trait_ref)?;
96 let item_name = TraitItemName(assoc.name.clone());
97 ItemKind::TraitDecl {
98 trait_ref,
99 item_name,
100 has_default: assoc.has_value,
101 }
102 }
103 })
104 }
105
106 fn translate_function_signature(
110 &mut self,
111 def: &hax::FullDef,
112 item_meta: &ItemMeta,
113 ) -> Result<FunSig, Error> {
114 let span = item_meta.span;
115
116 self.translate_def_generics(span, def)?;
117
118 let signature = match &def.kind {
119 hax::FullDefKind::Closure { args, .. } => &args.tupled_sig,
120 hax::FullDefKind::Fn { sig, .. } => sig,
121 hax::FullDefKind::AssocFn { sig, .. } => sig,
122 hax::FullDefKind::Ctor {
123 fields, output_ty, ..
124 } => {
125 let sig = hax::TyFnSig {
126 inputs: fields.iter().map(|field| field.ty.clone()).collect(),
127 output: output_ty.clone(),
128 c_variadic: false,
129 safety: hax::Safety::Safe,
130 abi: hax::ExternAbi::Rust,
131 };
132 &hax::Binder {
133 value: sig,
134 bound_vars: Default::default(),
135 }
136 }
137 hax::FullDefKind::Const { ty, .. }
138 | hax::FullDefKind::AssocConst { ty, .. }
139 | hax::FullDefKind::AnonConst { ty, .. }
140 | hax::FullDefKind::InlineConst { ty, .. }
141 | hax::FullDefKind::PromotedConst { ty, .. }
142 | hax::FullDefKind::Static { ty, .. } => {
143 let sig = hax::TyFnSig {
144 inputs: vec![],
145 output: ty.clone(),
146 c_variadic: false,
147 safety: hax::Safety::Safe,
148 abi: hax::ExternAbi::Rust,
149 };
150 &hax::Binder {
151 value: sig,
152 bound_vars: Default::default(),
153 }
154 }
155 _ => panic!("Unexpected definition for function: {def:?}"),
156 };
157
158 trace!("signature of {:?}:\n{:?}", def.def_id, signature.value);
160 let mut inputs: Vec<Ty> = signature
161 .value
162 .inputs
163 .iter()
164 .map(|ty| self.translate_ty(span, ty))
165 .try_collect()?;
166 let output = self.translate_ty(span, &signature.value.output)?;
167
168 let fmt_ctx = self.into_fmt();
169 trace!(
170 "# Input variables types:\n{}",
171 pretty_display_list(|x| fmt_ctx.format_object(x), &inputs)
172 );
173 trace!(
174 "# Output variable type:\n{}",
175 fmt_ctx.format_object(&output)
176 );
177
178 let is_unsafe = match signature.value.safety {
179 hax::Safety::Unsafe => true,
180 hax::Safety::Safe => false,
181 };
182
183 let closure_info = match &def.kind {
184 hax::FullDefKind::Closure { args, .. } => {
185 let kind = match args.kind {
186 hax::ClosureKind::Fn => ClosureKind::Fn,
187 hax::ClosureKind::FnMut => ClosureKind::FnMut,
188 hax::ClosureKind::FnOnce => ClosureKind::FnOnce,
189 };
190
191 assert_eq!(inputs.len(), 1);
192 let tuple_arg = inputs.pop().unwrap();
193
194 let state: Vector<TypeVarId, Ty> = args
195 .upvar_tys
196 .iter()
197 .map(|ty| self.translate_ty(span, &ty))
198 .try_collect()?;
199 let state_ty = {
201 let state_ty =
203 TyKind::Adt(TypeId::Tuple, GenericArgs::new_for_builtin(state.clone()))
204 .into_ty();
205 match &kind {
207 ClosureKind::FnOnce => state_ty,
208 ClosureKind::Fn | ClosureKind::FnMut => {
209 let rid = self
210 .innermost_generics_mut()
211 .regions
212 .push_with(|index| RegionVar { index, name: None });
213 let r = Region::Var(DeBruijnVar::new_at_zero(rid));
214 let mutability = if kind == ClosureKind::Fn {
215 RefKind::Shared
216 } else {
217 RefKind::Mut
218 };
219 TyKind::Ref(r, state_ty, mutability).into_ty()
220 }
221 }
222 };
223 inputs.push(state_ty);
224
225 let TyKind::Adt(TypeId::Tuple, tuple_args) = tuple_arg.kind() else {
227 raise_error!(self, span, "Closure argument is not a tuple")
228 };
229 inputs.extend(tuple_args.types.iter().cloned());
230
231 Some(ClosureInfo { kind, state })
232 }
233 _ => None,
234 };
235
236 Ok(FunSig {
237 generics: self.the_only_binder().params.clone(),
238 is_unsafe,
239 is_closure: matches!(&def.kind, hax::FullDefKind::Closure { .. }),
240 closure_info,
241 inputs,
242 output,
243 })
244 }
245
246 fn build_ctor_body(
248 &mut self,
249 span: Span,
250 signature: &FunSig,
251 adt_def_id: &hax::DefId,
252 ctor_of: &hax::CtorOf,
253 variant_id: usize,
254 fields: &hax::IndexVec<hax::FieldIdx, hax::FieldDef>,
255 output_ty: &hax::Ty,
256 ) -> Result<Body, Error> {
257 let adt_decl_id = self.register_type_decl_id(span, adt_def_id);
258 let output_ty = self.translate_ty(span, output_ty)?;
259 let mut locals = Locals {
260 arg_count: fields.len(),
261 locals: Vector::new(),
262 };
263 locals.new_var(None, output_ty);
264 let args: Vec<_> = fields
265 .iter()
266 .map(|field| {
267 let ty = self.translate_ty(span, &field.ty)?;
268 let place = locals.new_var(None, ty);
269 Ok(Operand::Move(place))
270 })
271 .try_collect()?;
272 let variant = match ctor_of {
273 hax::CtorOf::Struct => None,
274 hax::CtorOf::Variant => Some(VariantId::from(variant_id)),
275 };
276 let st_kind = RawStatement::Assign(
277 locals.return_place(),
278 Rvalue::Aggregate(
279 AggregateKind::Adt(
280 TypeId::Adt(adt_decl_id),
281 variant,
282 None,
283 Box::new(
284 signature
285 .generics
286 .identity_args(GenericsSource::item(adt_decl_id)),
287 ),
288 ),
289 args,
290 ),
291 );
292 let statement = Statement::new(span, st_kind);
293 let block = BlockData {
294 statements: vec![statement],
295 terminator: Terminator::new(span, RawTerminator::Return),
296 };
297 let body = Body::Unstructured(GExprBody {
298 span,
299 locals,
300 comments: Default::default(),
301 body: [block].into_iter().collect(),
302 });
303 Ok(body)
304 }
305
306 pub(crate) fn translate_fn_ptr(
311 &mut self,
312 span: Span,
313 def_id: &hax::DefId,
314 substs: &Vec<hax::GenericArg>,
315 trait_refs: &Vec<hax::ImplExpr>,
316 trait_info: &Option<hax::ImplExpr>,
317 ) -> Result<FnPtr, Error> {
318 let fun_def = self.t_ctx.hax_def(def_id)?;
319
320 trace!(
322 "Trait information:\n- def_id: {:?}\n- impl source:\n{:?}",
323 def_id,
324 trait_info
325 );
326 trace!(
327 "Method traits:\n- def_id: {:?}\n- traits:\n{:?}",
328 def_id,
329 trait_refs
330 );
331
332 let fun_id = if fun_def.diagnostic_item.as_deref() == Some("box_new") {
335 assert!(trait_info.is_none());
337 FunIdOrTraitMethodRef::Fun(FunId::Builtin(BuiltinFunId::BoxNew))
338 } else {
339 let fun_id = self.register_fun_decl_id(span, def_id);
340 match trait_info {
342 None => FunIdOrTraitMethodRef::Fun(FunId::Regular(fun_id)),
344 Some(trait_info) => {
346 let impl_expr = self.translate_trait_impl_expr(span, trait_info)?;
347 let method_name = self.t_ctx.translate_trait_item_name(def_id)?;
348 FunIdOrTraitMethodRef::Trait(impl_expr, method_name, fun_id)
349 }
350 }
351 };
352
353 let binder = match fun_def.kind() {
355 hax::FullDefKind::Fn { sig, .. } | hax::FullDefKind::AssocFn { sig, .. } => {
356 Some(sig.as_ref().rebind(()))
357 }
358 _ => None,
359 };
360 let generics = self.translate_generic_args(
361 span,
362 substs,
363 trait_refs,
364 binder,
365 fun_id.generics_target(),
366 )?;
367
368 Ok(FnPtr {
369 func: Box::new(fun_id),
370 generics: Box::new(generics),
371 })
372 }
373
374 #[tracing::instrument(skip(self, item_meta))]
376 pub fn translate_function(
377 mut self,
378 def_id: FunDeclId,
379 item_meta: ItemMeta,
380 def: &hax::FullDef,
381 ) -> Result<FunDecl, Error> {
382 trace!("About to translate function:\n{:?}", def.def_id);
383 let span = item_meta.span;
384
385 trace!("Translating function signature");
387 let signature = self.translate_function_signature(def, &item_meta)?;
388
389 let kind = self.get_item_kind(span, def)?;
392 let is_trait_method_decl_without_default = match &kind {
393 ItemKind::Regular | ItemKind::TraitImpl { .. } => false,
394 ItemKind::TraitDecl { has_default, .. } => !has_default,
395 };
396
397 let is_global_initializer = matches!(
398 def.kind(),
399 hax::FullDefKind::Const { .. }
400 | hax::FullDefKind::AssocConst { .. }
401 | hax::FullDefKind::AnonConst { .. }
402 | hax::FullDefKind::InlineConst { .. }
403 | hax::FullDefKind::PromotedConst { .. }
404 | hax::FullDefKind::Static { .. }
405 );
406 let is_global_initializer =
407 is_global_initializer.then(|| self.register_global_decl_id(span, &def.def_id));
408
409 let body_id = if item_meta.opacity.with_private_contents().is_opaque()
410 || is_trait_method_decl_without_default
411 {
412 Err(Opaque)
413 } else if let hax::FullDefKind::Ctor {
414 adt_def_id,
415 ctor_of,
416 variant_id,
417 fields,
418 output_ty,
419 ..
420 } = def.kind()
421 {
422 let body = self.build_ctor_body(
423 span,
424 &signature,
425 adt_def_id,
426 ctor_of,
427 *variant_id,
428 fields,
429 output_ty,
430 )?;
431 Ok(body)
432 } else {
433 let mut bt_ctx = BodyTransCtx::new(&mut self);
436 match bt_ctx.translate_body(item_meta.span, def) {
437 Ok(Ok(body)) => Ok(body),
438 Ok(Err(Opaque)) => Err(Opaque),
440 Err(_) => Err(Opaque),
443 }
444 };
445 Ok(FunDecl {
446 def_id,
447 item_meta,
448 signature,
449 kind,
450 is_global_initializer,
451 body: body_id,
452 })
453 }
454
455 #[tracing::instrument(skip(self, item_meta))]
457 pub fn translate_global(
458 mut self,
459 def_id: GlobalDeclId,
460 item_meta: ItemMeta,
461 def: &hax::FullDef,
462 ) -> Result<GlobalDecl, Error> {
463 trace!("About to translate global:\n{:?}", def.def_id);
464 let span = item_meta.span;
465
466 self.translate_def_generics(span, def)?;
474
475 let item_kind = self.get_item_kind(span, def)?;
477
478 trace!("Translating global type");
479 let ty = match &def.kind {
480 hax::FullDefKind::Const { ty, .. }
481 | hax::FullDefKind::AssocConst { ty, .. }
482 | hax::FullDefKind::AnonConst { ty, .. }
483 | hax::FullDefKind::InlineConst { ty, .. }
484 | hax::FullDefKind::PromotedConst { ty, .. }
485 | hax::FullDefKind::Static { ty, .. } => ty,
486 _ => panic!("Unexpected def for constant: {def:?}"),
487 };
488 let ty = self.translate_ty(span, ty)?;
489
490 let global_kind = match &def.kind {
491 hax::FullDefKind::Static { .. } => GlobalKind::Static,
492 hax::FullDefKind::Const { .. } | hax::FullDefKind::AssocConst { .. } => {
493 GlobalKind::NamedConst
494 }
495 hax::FullDefKind::AnonConst { .. }
496 | hax::FullDefKind::InlineConst { .. }
497 | hax::FullDefKind::PromotedConst { .. } => GlobalKind::AnonConst,
498 _ => panic!("Unexpected def for constant: {def:?}"),
499 };
500
501 let initializer = self.register_fun_decl_id(span, &def.def_id);
502
503 Ok(GlobalDecl {
504 def_id,
505 item_meta,
506 generics: self.into_generics(),
507 ty,
508 kind: item_kind,
509 global_kind,
510 init: initializer,
511 })
512 }
513}