1use super::translate_ctx::*;
2use charon_lib::ast::*;
3use charon_lib::options::{CliOpts, TranslateOptions};
4use charon_lib::transform::TransformCtx;
5use hax::FullDefKind;
6use hax_frontend_exporter::{self as hax, SInto};
7use itertools::Itertools;
8use macros::VariantIndexArity;
9use rustc_middle::ty::TyCtxt;
10use std::cell::RefCell;
11use std::path::PathBuf;
12
13#[derive(Clone, Debug, PartialEq, Eq, Hash, VariantIndexArity)]
17pub enum TransItemSource {
18 Global(hax::DefId),
19 TraitDecl(hax::DefId),
20 TraitImpl(hax::DefId),
21 Fun(hax::DefId),
22 Type(hax::DefId),
23 ClosureTraitImpl(hax::DefId, ClosureKind),
25 ClosureMethod(hax::DefId, ClosureKind),
27}
28
29impl TransItemSource {
30 pub(crate) fn as_def_id(&self) -> &hax::DefId {
31 match self {
32 TransItemSource::Global(id)
33 | TransItemSource::TraitDecl(id)
34 | TransItemSource::TraitImpl(id)
35 | TransItemSource::Fun(id)
36 | TransItemSource::Type(id)
37 | TransItemSource::ClosureTraitImpl(id, _)
38 | TransItemSource::ClosureMethod(id, _) => id,
39 }
40 }
41}
42
43impl TransItemSource {
44 fn sort_key(&self) -> impl Ord {
46 let (variant_index, _) = self.variant_index_arity();
47 let def_id = self.as_def_id();
48 let closure_kind = match self {
49 Self::ClosureTraitImpl(_, k) | Self::ClosureMethod(_, k) => match k {
50 ClosureKind::Fn => 1,
51 ClosureKind::FnMut => 2,
52 ClosureKind::FnOnce => 3,
53 },
54 _ => 0,
55 };
56 (def_id.index, variant_index, closure_kind)
57 }
58}
59
60impl PartialOrd for TransItemSource {
62 fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
63 Some(self.cmp(other))
64 }
65}
66impl Ord for TransItemSource {
67 fn cmp(&self, other: &Self) -> std::cmp::Ordering {
68 self.sort_key().cmp(&other.sort_key())
69 }
70}
71
72impl<'tcx, 'ctx> TranslateCtx<'tcx> {
73 fn register_module_item(&mut self, def_id: &hax::DefId) {
76 use hax::DefKind::*;
77 trace!("Registering {def_id:?}");
78
79 match &def_id.kind {
80 Enum { .. } | Struct { .. } | Union { .. } | TyAlias { .. } | ForeignTy => {
81 let _ = self.register_type_decl_id(&None, def_id);
82 }
83 Fn { .. } | AssocFn { .. } => {
84 let _ = self.register_fun_decl_id(&None, def_id);
85 }
86 Const { .. } | Static { .. } | AssocConst { .. } => {
87 let _ = self.register_global_decl_id(&None, def_id);
88 }
89
90 Trait { .. } => {
91 let _ = self.register_trait_decl_id(&None, def_id);
92 }
93 Impl { of_trait: true } => {
94 let _ = self.register_trait_impl_id(&None, def_id);
95 }
96 TraitAlias { .. } => {}
98
99 Impl { of_trait: false } | Mod { .. } | ForeignMod { .. } => {
100 let Ok(def) = self.hax_def(def_id) else {
101 return; };
103 let Ok(name) = self.def_id_to_name(&def.def_id) else {
104 return; };
106 let opacity = self.opacity_for_name(&name);
107 let trans_src = TransItemSource::TraitImpl(def.def_id.clone());
108 let item_meta = self.translate_item_meta(&def, &trans_src, name, opacity);
109 let _ = self.register_module(item_meta, &def);
110 }
111
112 ExternCrate { .. } | GlobalAsm { .. } | Macro { .. } | Use { .. } => {}
114 AnonConst { .. }
116 | AssocTy { .. }
117 | Closure { .. }
118 | ConstParam { .. }
119 | Ctor { .. }
120 | Field { .. }
121 | InlineConst { .. }
122 | PromotedConst { .. }
123 | LifetimeParam { .. }
124 | OpaqueTy { .. }
125 | SyntheticCoroutineBody { .. }
126 | TyParam { .. }
127 | Variant { .. } => {
128 let span = self.def_span(def_id);
129 register_error!(
130 self,
131 span,
132 "Cannot register item `{def_id:?}` with kind `{:?}`",
133 def_id.kind
134 );
135 }
136 }
137 }
138
139 fn register_module(&mut self, item_meta: ItemMeta, def: &hax::FullDef) -> Result<(), Error> {
143 let opacity = item_meta.opacity;
144 if !opacity.is_transparent() {
145 return Ok(());
146 }
147 match def.kind() {
148 FullDefKind::InherentImpl { items, .. } => {
149 for (_, item_def) in items {
150 self.register_module_item(&item_def.def_id);
151 }
152 }
153 FullDefKind::Mod { items, .. } => {
154 for (_, def_id) in items {
155 self.register_module_item(def_id);
156 }
157 }
158 FullDefKind::ForeignMod { items, .. } => {
159 for def_id in items {
161 self.register_module_item(def_id);
162 }
163 }
164 _ => panic!("Item should be a module but isn't: {def:?}"),
165 }
166 Ok(())
167 }
168
169 pub(crate) fn register_id_no_enqueue(
170 &mut self,
171 src: &Option<DepSource>,
172 id: TransItemSource,
173 ) -> AnyTransId {
174 let item_id = match self.id_map.get(&id) {
175 Some(tid) => *tid,
176 None => {
177 let trans_id = match id {
178 TransItemSource::Type(_) => {
179 AnyTransId::Type(self.translated.type_decls.reserve_slot())
180 }
181 TransItemSource::TraitDecl(_) => {
182 AnyTransId::TraitDecl(self.translated.trait_decls.reserve_slot())
183 }
184 TransItemSource::TraitImpl(_) | TransItemSource::ClosureTraitImpl(_, _) => {
185 AnyTransId::TraitImpl(self.translated.trait_impls.reserve_slot())
186 }
187 TransItemSource::Global(_) => {
188 AnyTransId::Global(self.translated.global_decls.reserve_slot())
189 }
190 TransItemSource::Fun(_) | TransItemSource::ClosureMethod(_, _) => {
191 AnyTransId::Fun(self.translated.fun_decls.reserve_slot())
192 }
193 };
194 self.id_map.insert(id.clone(), trans_id);
196 self.reverse_id_map.insert(trans_id, id.clone());
197 self.translated.all_ids.insert(trans_id);
198 if !matches!(id, TransItemSource::TraitImpl(_)) {
201 if let Ok(name) = self.def_id_to_name(id.as_def_id()) {
202 self.translated.item_names.insert(trans_id, name);
203 }
204 }
205 trans_id
206 }
207 };
208 self.errors
209 .borrow_mut()
210 .register_dep_source(src, item_id, id.as_def_id().is_local);
211 item_id
212 }
213
214 pub(crate) fn register_and_enqueue_id(
216 &mut self,
217 src: &Option<DepSource>,
218 id: TransItemSource,
219 ) -> AnyTransId {
220 self.items_to_translate.insert(id.clone());
221 self.register_id_no_enqueue(src, id)
222 }
223
224 pub(crate) fn register_type_decl_id(
225 &mut self,
226 src: &Option<DepSource>,
227 id: &hax::DefId,
228 ) -> TypeDeclId {
229 *self
230 .register_and_enqueue_id(src, TransItemSource::Type(id.clone()))
231 .as_type()
232 .unwrap()
233 }
234
235 pub(crate) fn register_fun_decl_id(
236 &mut self,
237 src: &Option<DepSource>,
238 id: &hax::DefId,
239 ) -> FunDeclId {
240 *self
241 .register_and_enqueue_id(src, TransItemSource::Fun(id.clone()))
242 .as_fun()
243 .unwrap()
244 }
245
246 pub(crate) fn register_trait_decl_id(
247 &mut self,
248 src: &Option<DepSource>,
249 id: &hax::DefId,
250 ) -> TraitDeclId {
251 *self
252 .register_and_enqueue_id(src, TransItemSource::TraitDecl(id.clone()))
253 .as_trait_decl()
254 .unwrap()
255 }
256
257 pub(crate) fn register_trait_impl_id(
258 &mut self,
259 src: &Option<DepSource>,
260 id: &hax::DefId,
261 ) -> TraitImplId {
262 if let Ok(def) = self.hax_def(id) {
264 let hax::FullDefKind::TraitImpl { trait_pred, .. } = def.kind() else {
265 unreachable!()
266 };
267 let trait_rust_id = &trait_pred.trait_ref.def_id;
268 let _ = self.register_trait_decl_id(src, trait_rust_id);
269 }
270
271 *self
272 .register_and_enqueue_id(src, TransItemSource::TraitImpl(id.clone()))
273 .as_trait_impl()
274 .unwrap()
275 }
276
277 pub(crate) fn register_closure_trait_impl_id(
278 &mut self,
279 src: &Option<DepSource>,
280 id: &hax::DefId,
281 kind: ClosureKind,
282 ) -> TraitImplId {
283 *self
284 .register_and_enqueue_id(src, TransItemSource::ClosureTraitImpl(id.clone(), kind))
285 .as_trait_impl()
286 .unwrap()
287 }
288
289 pub(crate) fn register_closure_method_decl_id(
290 &mut self,
291 src: &Option<DepSource>,
292 id: &hax::DefId,
293 kind: ClosureKind,
294 ) -> FunDeclId {
295 *self
296 .register_and_enqueue_id(src, TransItemSource::ClosureMethod(id.clone(), kind))
297 .as_fun()
298 .unwrap()
299 }
300
301 pub(crate) fn register_global_decl_id(
302 &mut self,
303 src: &Option<DepSource>,
304 id: &hax::DefId,
305 ) -> GlobalDeclId {
306 *self
307 .register_and_enqueue_id(src, TransItemSource::Global(id.clone()))
308 .as_global()
309 .unwrap()
310 }
311}
312
313impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
314 pub(crate) fn make_dep_source(&self, span: Span) -> Option<DepSource> {
315 Some(DepSource {
316 src_id: self.item_id?,
317 span: self.def_id.is_local.then_some(span),
318 })
319 }
320
321 pub(crate) fn register_id_no_enqueue(&mut self, span: Span, id: TransItemSource) -> AnyTransId {
322 let src = self.make_dep_source(span);
323 self.t_ctx.register_id_no_enqueue(&src, id)
324 }
325
326 pub(crate) fn register_type_decl_id(&mut self, span: Span, id: &hax::DefId) -> TypeDeclId {
327 let src = self.make_dep_source(span);
328 self.t_ctx.register_type_decl_id(&src, id)
329 }
330
331 pub(crate) fn register_fun_decl_id(&mut self, span: Span, id: &hax::DefId) -> FunDeclId {
332 let src = self.make_dep_source(span);
333 self.t_ctx.register_fun_decl_id(&src, id)
334 }
335
336 pub(crate) fn register_fun_decl_id_no_enqueue(
337 &mut self,
338 span: Span,
339 id: &hax::DefId,
340 ) -> FunDeclId {
341 self.register_id_no_enqueue(span, TransItemSource::Fun(id.clone()))
342 .as_fun()
343 .copied()
344 .unwrap()
345 }
346
347 pub(crate) fn register_global_decl_id(&mut self, span: Span, id: &hax::DefId) -> GlobalDeclId {
348 let src = self.make_dep_source(span);
349 self.t_ctx.register_global_decl_id(&src, id)
350 }
351
352 pub(crate) fn register_trait_decl_id(&mut self, span: Span, id: &hax::DefId) -> TraitDeclId {
353 let src = self.make_dep_source(span);
354 self.t_ctx.register_trait_decl_id(&src, id)
355 }
356
357 pub(crate) fn register_trait_impl_id(&mut self, span: Span, id: &hax::DefId) -> TraitImplId {
358 let src = self.make_dep_source(span);
359 self.t_ctx.register_trait_impl_id(&src, id)
360 }
361
362 pub(crate) fn register_closure_trait_impl_id(
363 &mut self,
364 span: Span,
365 id: &hax::DefId,
366 kind: ClosureKind,
367 ) -> TraitImplId {
368 let src = self.make_dep_source(span);
369 self.t_ctx.register_closure_trait_impl_id(&src, id, kind)
370 }
371
372 pub(crate) fn register_closure_method_decl_id(
373 &mut self,
374 span: Span,
375 id: &hax::DefId,
376 kind: ClosureKind,
377 ) -> FunDeclId {
378 let src = self.make_dep_source(span);
379 self.t_ctx.register_closure_method_decl_id(&src, id, kind)
380 }
381}
382
383#[tracing::instrument(skip(tcx))]
384pub fn translate<'tcx, 'ctx>(
385 options: &CliOpts,
386 tcx: TyCtxt<'tcx>,
387 sysroot: PathBuf,
388) -> TransformCtx {
389 let hax_state = hax::state::State::new(
390 tcx,
391 hax::options::Options {
392 inline_anon_consts: true,
393 },
394 );
395
396 let crate_def_id: hax::DefId = rustc_span::def_id::CRATE_DEF_ID
399 .to_def_id()
400 .sinto(&hax_state);
401 let crate_name = crate_def_id.krate.clone();
402 trace!("# Crate: {}", crate_name);
403
404 let mut error_ctx = ErrorCtx::new(!options.abort_on_error, options.error_on_warnings);
405 let translate_options = TranslateOptions::new(&mut error_ctx, options);
406 let mut ctx = TranslateCtx {
407 tcx,
408 sysroot,
409 hax_state,
410 options: translate_options,
411 errors: RefCell::new(error_ctx),
412 translated: TranslatedCrate {
413 crate_name,
414 options: options.clone(),
415 ..TranslatedCrate::default()
416 },
417 id_map: Default::default(),
418 reverse_id_map: Default::default(),
419 file_to_id: Default::default(),
420 items_to_translate: Default::default(),
421 processed: Default::default(),
422 cached_item_metas: Default::default(),
423 cached_names: Default::default(),
424 };
425
426 if options.start_from.is_empty() {
427 ctx.register_module_item(&crate_def_id);
429 } else {
430 for path in options.start_from.iter() {
432 let path = path.split("::").collect_vec();
433 let resolved = super::resolve_path::def_path_def_ids(&ctx.hax_state, &path);
434 match resolved {
435 Ok(resolved) => {
436 for def_id in resolved {
437 let def_id: hax::DefId = def_id.sinto(&ctx.hax_state);
438 ctx.register_module_item(&def_id);
439 }
440 }
441 Err(path) => {
442 let path = path.join("::");
443 register_error!(
444 ctx,
445 Span::dummy(),
446 "path {path} does not correspond to any item"
447 );
448 }
449 }
450 }
451 }
452
453 trace!(
454 "Queue after we explored the crate:\n{:?}",
455 &ctx.items_to_translate
456 );
457
458 while let Some(item_src) = ctx.items_to_translate.pop_first() {
468 trace!("About to translate item: {:?}", item_src);
469 if ctx.processed.insert(item_src.clone()) {
470 ctx.translate_item(&item_src);
471 }
472 }
473
474 TransformCtx {
476 options: ctx.options,
477 translated: ctx.translated,
478 errors: ctx.errors,
479 }
480}