charon_driver/translate/
translate_crate.rs

1//! This file governs the overall translation of items.
2//!
3//! Translation works as follows: we translate each `TransItemSource` of interest into an
4//! appropriate item. In the process of translating an item we may find more `hax::DefId`s of
5//! interest; we register those as an appropriate `TransItemSource`, which will 1/ enqueue the item
6//! so that it eventually gets translated too, and 2/ return an `AnyTransId` we can use to refer to
7//! it.
8//!
9//! We start with the DefId of the current crate (or of anything passed to `--start-from`) and
10//! recursively translate everything we find.
11//!
12//! There's another important component at play: opacity. Each item is assigned an opacity based on
13//! its name. By default, items from the local crate are transparent and items from foreign crates
14//! are opaque (this can be controlled with `--include`, `--opaque` and `--exclude`). If an item is
15//! opaque, its signature/"outer shell" will be translated (e.g. for functions that's the
16//! signature) but not its contents.
17use super::translate_ctx::*;
18use charon_lib::ast::*;
19use charon_lib::options::{CliOpts, TranslateOptions};
20use charon_lib::transform::TransformCtx;
21use hax_frontend_exporter::{self as hax, SInto};
22use itertools::Itertools;
23use macros::VariantIndexArity;
24use rustc_middle::ty::TyCtxt;
25use std::cell::RefCell;
26use std::path::PathBuf;
27
28/// The id of an untranslated item. Note that a given `DefId` may show up as multiple different
29/// item sources, e.g. a constant will have both a `Global` version (for the constant itself) and a
30/// `FunDecl` one (for its initializer function).
31#[derive(Clone, Debug, PartialEq, Eq, Hash)]
32pub struct TransItemSource {
33    pub def_id: hax::DefId,
34    pub kind: TransItemSourceKind,
35}
36
37#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, VariantIndexArity)]
38pub enum TransItemSourceKind {
39    Global,
40    TraitDecl,
41    TraitImpl,
42    Fun,
43    Type,
44    /// We don't translate these as proper items, but we translate them a bit in names.
45    InherentImpl,
46    /// We don't translate these as proper items, but we use them to explore the crate.
47    Module,
48    /// An impl of the appropriate `Fn*` trait for the given closure type.
49    ClosureTraitImpl(ClosureKind),
50    /// The `call_*` method of the appropriate `Fn*` trait.
51    ClosureMethod(ClosureKind),
52    /// A cast of a state-less closure as a function pointer.
53    ClosureAsFnCast,
54    /// A fictitious trait impl corresponding to the drop glue code for the given ADT.
55    DropGlueImpl,
56    /// The `drop` method for the impl above.
57    DropGlueMethod,
58}
59
60impl TransItemSource {
61    pub fn new(def_id: hax::DefId, kind: TransItemSourceKind) -> Self {
62        Self { def_id, kind }
63    }
64
65    pub fn as_def_id(&self) -> &hax::DefId {
66        &self.def_id
67    }
68
69    /// Whether this item is the "main" item for this def_id or not (e.g. drop impl/methods are not
70    /// the main item).
71    pub(crate) fn is_derived_item(&self) -> bool {
72        use TransItemSourceKind::*;
73        match self.kind {
74            Global | TraitDecl | TraitImpl | InherentImpl | Module | Fun | Type => false,
75            ClosureTraitImpl(..) | ClosureMethod(..) | ClosureAsFnCast | DropGlueImpl
76            | DropGlueMethod => true,
77        }
78    }
79
80    /// Value with which we order values.
81    fn sort_key(&self) -> impl Ord + '_ {
82        (self.def_id.index, &self.kind)
83    }
84}
85
86/// Manual impls because `DefId` is not orderable.
87impl PartialOrd for TransItemSource {
88    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
89        Some(self.cmp(other))
90    }
91}
92impl Ord for TransItemSource {
93    fn cmp(&self, other: &Self) -> std::cmp::Ordering {
94        self.sort_key().cmp(&other.sort_key())
95    }
96}
97
98impl<'tcx, 'ctx> TranslateCtx<'tcx> {
99    /// Returns the default translation kind for the given `DefId`. Returns `None` for items that
100    /// we don't translate. Errors on unexpected items.
101    pub fn base_kind_for_item(&mut self, def_id: &hax::DefId) -> Option<TransItemSourceKind> {
102        use hax::DefKind::*;
103        Some(match &def_id.kind {
104            Enum { .. } | Struct { .. } | Union { .. } | TyAlias { .. } | ForeignTy => {
105                TransItemSourceKind::Type
106            }
107            Fn { .. } | AssocFn { .. } => TransItemSourceKind::Fun,
108            Const { .. } | Static { .. } | AssocConst { .. } => TransItemSourceKind::Global,
109            Trait { .. } | TraitAlias { .. } => TransItemSourceKind::TraitDecl,
110            Impl { of_trait: true } => TransItemSourceKind::TraitImpl,
111            Impl { of_trait: false } => TransItemSourceKind::InherentImpl,
112            Mod { .. } | ForeignMod { .. } => TransItemSourceKind::Module,
113
114            // We skip these
115            ExternCrate { .. } | GlobalAsm { .. } | Macro { .. } | Use { .. } => return None,
116            // We cannot encounter these since they're not top-level items.
117            AnonConst { .. }
118            | AssocTy { .. }
119            | Closure { .. }
120            | ConstParam { .. }
121            | Ctor { .. }
122            | Field { .. }
123            | InlineConst { .. }
124            | PromotedConst { .. }
125            | LifetimeParam { .. }
126            | OpaqueTy { .. }
127            | SyntheticCoroutineBody { .. }
128            | TyParam { .. }
129            | Variant { .. } => {
130                let span = self.def_span(def_id);
131                register_error!(
132                    self,
133                    span,
134                    "Cannot register item `{def_id:?}` with kind `{:?}`",
135                    def_id.kind
136                );
137                return None;
138            }
139        })
140    }
141
142    /// Add this item to the queue of items to translate. Each translated item will then
143    /// recursively register the items it refers to. We call this on the crate root and end up
144    /// exploring the whole crate.
145    #[tracing::instrument(skip(self))]
146    pub fn enqueue_item(&mut self, def_id: &hax::DefId) -> Option<AnyTransId> {
147        let kind = self.base_kind_for_item(def_id)?;
148        self.register_and_enqueue_id(&None, def_id, kind)
149    }
150
151    pub(crate) fn register_id_no_enqueue(
152        &mut self,
153        dep_src: &Option<DepSource>,
154        src: &TransItemSource,
155    ) -> Option<AnyTransId> {
156        let item_id = match self.id_map.get(src) {
157            Some(tid) => *tid,
158            None => {
159                use TransItemSourceKind::*;
160                let trans_id = match src.kind {
161                    Type => AnyTransId::Type(self.translated.type_decls.reserve_slot()),
162                    TraitDecl => AnyTransId::TraitDecl(self.translated.trait_decls.reserve_slot()),
163                    TraitImpl | ClosureTraitImpl(..) | DropGlueImpl => {
164                        AnyTransId::TraitImpl(self.translated.trait_impls.reserve_slot())
165                    }
166                    Global => AnyTransId::Global(self.translated.global_decls.reserve_slot()),
167                    Fun | ClosureMethod(..) | ClosureAsFnCast | DropGlueMethod => {
168                        AnyTransId::Fun(self.translated.fun_decls.reserve_slot())
169                    }
170                    InherentImpl | Module => return None,
171                };
172                // Add the id to the queue of declarations to translate
173                self.id_map.insert(src.clone(), trans_id);
174                self.reverse_id_map.insert(trans_id, src.clone());
175                // Store the name early so the name matcher can identify paths. We can't to it for
176                // trait impls because they register themselves when computing their name.
177                if !matches!(src.kind, TraitImpl) {
178                    if let Ok(name) = self.def_id_to_name(src.as_def_id()) {
179                        self.translated.item_names.insert(trans_id, name);
180                    }
181                }
182                trans_id
183            }
184        };
185        self.errors
186            .borrow_mut()
187            .register_dep_source(dep_src, item_id, src.as_def_id().is_local);
188        Some(item_id)
189    }
190
191    /// Register this id and enqueue it for translation.
192    pub(crate) fn register_and_enqueue_id(
193        &mut self,
194        dep_src: &Option<DepSource>,
195        def_id: &hax::DefId,
196        kind: TransItemSourceKind,
197    ) -> Option<AnyTransId> {
198        let item_src = TransItemSource::new(def_id.clone(), kind);
199        let id = self.register_id_no_enqueue(dep_src, &item_src);
200        self.items_to_translate.insert(item_src);
201        id
202    }
203
204    pub(crate) fn register_type_decl_id(
205        &mut self,
206        src: &Option<DepSource>,
207        def_id: &hax::DefId,
208    ) -> TypeDeclId {
209        *self
210            .register_and_enqueue_id(src, def_id, TransItemSourceKind::Type)
211            .unwrap()
212            .as_type()
213            .unwrap()
214    }
215
216    pub(crate) fn register_fun_decl_id(
217        &mut self,
218        src: &Option<DepSource>,
219        def_id: &hax::DefId,
220    ) -> FunDeclId {
221        *self
222            .register_and_enqueue_id(src, def_id, TransItemSourceKind::Fun)
223            .unwrap()
224            .as_fun()
225            .unwrap()
226    }
227
228    pub(crate) fn register_trait_decl_id(
229        &mut self,
230        src: &Option<DepSource>,
231        def_id: &hax::DefId,
232    ) -> TraitDeclId {
233        *self
234            .register_and_enqueue_id(src, def_id, TransItemSourceKind::TraitDecl)
235            .unwrap()
236            .as_trait_decl()
237            .unwrap()
238    }
239
240    pub(crate) fn register_trait_impl_id(
241        &mut self,
242        src: &Option<DepSource>,
243        def_id: &hax::DefId,
244    ) -> TraitImplId {
245        // Register the corresponding trait early so we can filter on its name.
246        if let Ok(def) = self.hax_def(def_id) {
247            let trait_id = match def.kind() {
248                hax::FullDefKind::TraitImpl { trait_pred, .. } => &trait_pred.trait_ref.def_id,
249                hax::FullDefKind::TraitAlias { .. } => def_id,
250                _ => unreachable!(),
251            };
252            let _ = self.register_trait_decl_id(src, trait_id);
253        }
254
255        *self
256            .register_and_enqueue_id(src, def_id, TransItemSourceKind::TraitImpl)
257            .unwrap()
258            .as_trait_impl()
259            .unwrap()
260    }
261
262    pub(crate) fn register_closure_trait_impl_id(
263        &mut self,
264        src: &Option<DepSource>,
265        def_id: &hax::DefId,
266        kind: ClosureKind,
267    ) -> TraitImplId {
268        *self
269            .register_and_enqueue_id(src, def_id, TransItemSourceKind::ClosureTraitImpl(kind))
270            .unwrap()
271            .as_trait_impl()
272            .unwrap()
273    }
274
275    pub(crate) fn register_closure_method_decl_id(
276        &mut self,
277        src: &Option<DepSource>,
278        def_id: &hax::DefId,
279        kind: ClosureKind,
280    ) -> FunDeclId {
281        *self
282            .register_and_enqueue_id(src, def_id, TransItemSourceKind::ClosureMethod(kind))
283            .unwrap()
284            .as_fun()
285            .unwrap()
286    }
287
288    pub(crate) fn register_closure_as_fun_decl_id(
289        &mut self,
290        src: &Option<DepSource>,
291        def_id: &hax::DefId,
292    ) -> FunDeclId {
293        *self
294            .register_and_enqueue_id(src, def_id, TransItemSourceKind::ClosureAsFnCast)
295            .unwrap()
296            .as_fun()
297            .unwrap()
298    }
299
300    pub(crate) fn register_global_decl_id(
301        &mut self,
302        src: &Option<DepSource>,
303        def_id: &hax::DefId,
304    ) -> GlobalDeclId {
305        *self
306            .register_and_enqueue_id(src, def_id, TransItemSourceKind::Global)
307            .unwrap()
308            .as_global()
309            .unwrap()
310    }
311
312    pub(crate) fn register_drop_trait_impl_id(
313        &mut self,
314        src: &Option<DepSource>,
315        def_id: &hax::DefId,
316    ) -> TraitImplId {
317        *self
318            .register_and_enqueue_id(src, def_id, TransItemSourceKind::DropGlueImpl)
319            .unwrap()
320            .as_trait_impl()
321            .unwrap()
322    }
323
324    pub(crate) fn register_drop_method_id(
325        &mut self,
326        src: &Option<DepSource>,
327        def_id: &hax::DefId,
328    ) -> FunDeclId {
329        *self
330            .register_and_enqueue_id(src, def_id, TransItemSourceKind::DropGlueMethod)
331            .unwrap()
332            .as_fun()
333            .unwrap()
334    }
335
336    pub(crate) fn register_target_info(&mut self) {
337        let target_data = &self.tcx.data_layout;
338        self.translated.target_information = krate::TargetInfo {
339            target_pointer_size: target_data.pointer_size().bytes(),
340            is_little_endian: matches!(target_data.endian, rustc_abi::Endian::Little),
341        }
342    }
343}
344
345// Id and item reference registration.
346impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
347    pub(crate) fn make_dep_source(&self, span: Span) -> Option<DepSource> {
348        Some(DepSource {
349            src_id: self.item_id?,
350            span: self.item_src.as_def_id().is_local.then_some(span),
351        })
352    }
353
354    pub(crate) fn register_id_no_enqueue(
355        &mut self,
356        span: Span,
357        id: TransItemSource,
358    ) -> Option<AnyTransId> {
359        let src = self.make_dep_source(span);
360        self.t_ctx.register_id_no_enqueue(&src, &id)
361    }
362
363    pub(crate) fn register_type_decl_id(&mut self, span: Span, id: &hax::DefId) -> TypeDeclId {
364        let src = self.make_dep_source(span);
365        self.t_ctx.register_type_decl_id(&src, id)
366    }
367
368    /// Translate a type def id
369    pub(crate) fn translate_type_id(
370        &mut self,
371        span: Span,
372        def_id: &hax::DefId,
373    ) -> Result<TypeId, Error> {
374        Ok(match self.recognize_builtin_type(def_id)? {
375            Some(id) => TypeId::Builtin(id),
376            None => TypeId::Adt(self.register_type_decl_id(span, def_id)),
377        })
378    }
379
380    pub(crate) fn translate_type_decl_ref(
381        &mut self,
382        span: Span,
383        item: &hax::ItemRef,
384    ) -> Result<TypeDeclRef, Error> {
385        let id = self.translate_type_id(span, &item.def_id)?;
386        let generics = self.translate_generic_args(span, &item.generic_args, &item.impl_exprs)?;
387        Ok(TypeDeclRef {
388            id,
389            generics: Box::new(generics),
390        })
391    }
392
393    pub(crate) fn register_fun_decl_id(&mut self, span: Span, id: &hax::DefId) -> FunDeclId {
394        let src = self.make_dep_source(span);
395        self.t_ctx.register_fun_decl_id(&src, id)
396    }
397
398    pub(crate) fn register_fun_decl_id_no_enqueue(
399        &mut self,
400        span: Span,
401        def_id: &hax::DefId,
402    ) -> FunDeclId {
403        self.register_id_no_enqueue(
404            span,
405            TransItemSource::new(def_id.clone(), TransItemSourceKind::Fun),
406        )
407        .unwrap()
408        .as_fun()
409        .copied()
410        .unwrap()
411    }
412
413    /// Translate a function def id
414    pub(crate) fn translate_fun_id(
415        &mut self,
416        span: Span,
417        def_id: &hax::DefId,
418    ) -> Result<FunId, Error> {
419        Ok(match self.recognize_builtin_fun(def_id)? {
420            Some(id) => FunId::Builtin(id),
421            None => FunId::Regular(self.register_fun_decl_id(span, def_id)),
422        })
423    }
424
425    /// Auxiliary function to translate function calls and references to functions.
426    /// Translate a function id applied with some substitutions.
427    #[tracing::instrument(skip(self, span))]
428    pub(crate) fn translate_fn_ptr(
429        &mut self,
430        span: Span,
431        item: &hax::ItemRef,
432    ) -> Result<RegionBinder<FnPtr>, Error> {
433        let fun_id = self.translate_fun_id(span, &item.def_id)?;
434        let late_bound = match self.hax_def(&item.def_id)?.kind() {
435            hax::FullDefKind::Fn { sig, .. } | hax::FullDefKind::AssocFn { sig, .. } => {
436                Some(sig.as_ref().rebind(()))
437            }
438            _ => None,
439        };
440        let bound_generics = self.translate_generic_args_with_late_bound(
441            span,
442            &item.generic_args,
443            &item.impl_exprs,
444            late_bound,
445        )?;
446        let fun_id = match &item.in_trait {
447            // Direct function call
448            None => FunIdOrTraitMethodRef::Fun(fun_id),
449            // Trait method
450            Some(impl_expr) => {
451                let trait_ref = self.translate_trait_impl_expr(span, impl_expr)?;
452                let name = self.t_ctx.translate_trait_item_name(&item.def_id)?;
453                let method_decl_id = *fun_id
454                    .as_regular()
455                    .expect("methods are not builtin functions");
456                FunIdOrTraitMethodRef::Trait(trait_ref.move_under_binder(), name, method_decl_id)
457            }
458        };
459        Ok(bound_generics.map(|generics| FnPtr {
460            func: Box::new(fun_id),
461            generics: Box::new(generics),
462        }))
463    }
464
465    pub(crate) fn register_global_decl_id(&mut self, span: Span, id: &hax::DefId) -> GlobalDeclId {
466        let src = self.make_dep_source(span);
467        self.t_ctx.register_global_decl_id(&src, id)
468    }
469
470    pub(crate) fn translate_global_decl_ref(
471        &mut self,
472        span: Span,
473        item: &hax::ItemRef,
474    ) -> Result<GlobalDeclRef, Error> {
475        let id = self.register_global_decl_id(span, &item.def_id);
476        let generics = self.translate_generic_args(span, &item.generic_args, &item.impl_exprs)?;
477        Ok(GlobalDeclRef {
478            id,
479            generics: Box::new(generics),
480        })
481    }
482
483    pub(crate) fn register_trait_decl_id(&mut self, span: Span, id: &hax::DefId) -> TraitDeclId {
484        let src = self.make_dep_source(span);
485        self.t_ctx.register_trait_decl_id(&src, id)
486    }
487
488    pub(crate) fn translate_trait_decl_ref(
489        &mut self,
490        span: Span,
491        item: &hax::ItemRef,
492    ) -> Result<TraitDeclRef, Error> {
493        let id = self.register_trait_decl_id(span, &item.def_id);
494        let generics = self.translate_generic_args(span, &item.generic_args, &item.impl_exprs)?;
495        Ok(TraitDeclRef {
496            id,
497            generics: Box::new(generics),
498        })
499    }
500
501    pub(crate) fn register_trait_impl_id(&mut self, span: Span, id: &hax::DefId) -> TraitImplId {
502        let src = self.make_dep_source(span);
503        self.t_ctx.register_trait_impl_id(&src, id)
504    }
505
506    pub(crate) fn translate_trait_impl_ref(
507        &mut self,
508        span: Span,
509        item: &hax::ItemRef,
510    ) -> Result<TraitImplRef, Error> {
511        let id = self.register_trait_impl_id(span, &item.def_id);
512        let generics = self.translate_generic_args(span, &item.generic_args, &item.impl_exprs)?;
513        Ok(TraitImplRef {
514            id,
515            generics: Box::new(generics),
516        })
517    }
518
519    pub(crate) fn register_closure_trait_impl_id(
520        &mut self,
521        span: Span,
522        id: &hax::DefId,
523        kind: ClosureKind,
524    ) -> TraitImplId {
525        let src = self.make_dep_source(span);
526        self.t_ctx.register_closure_trait_impl_id(&src, id, kind)
527    }
528
529    pub(crate) fn register_closure_method_decl_id(
530        &mut self,
531        span: Span,
532        id: &hax::DefId,
533        kind: ClosureKind,
534    ) -> FunDeclId {
535        let src = self.make_dep_source(span);
536        self.t_ctx.register_closure_method_decl_id(&src, id, kind)
537    }
538
539    pub(crate) fn register_closure_as_fun_decl_id(
540        &mut self,
541        span: Span,
542        id: &hax::DefId,
543    ) -> FunDeclId {
544        let src = self.make_dep_source(span);
545        self.t_ctx.register_closure_as_fun_decl_id(&src, id)
546    }
547
548    pub(crate) fn register_drop_trait_impl_id(
549        &mut self,
550        span: Span,
551        id: &hax::DefId,
552    ) -> TraitImplId {
553        let src = self.make_dep_source(span);
554        self.t_ctx.register_drop_trait_impl_id(&src, id)
555    }
556
557    pub(crate) fn translate_drop_trait_impl_ref(
558        &mut self,
559        span: Span,
560        item: &hax::ItemRef,
561    ) -> Result<TraitImplRef, Error> {
562        let id = self.register_drop_trait_impl_id(span, &item.def_id);
563        let generics = self.translate_generic_args(span, &item.generic_args, &item.impl_exprs)?;
564        Ok(TraitImplRef {
565            id,
566            generics: Box::new(generics),
567        })
568    }
569
570    pub(crate) fn register_drop_method_id(&mut self, span: Span, id: &hax::DefId) -> FunDeclId {
571        let src = self.make_dep_source(span);
572        self.t_ctx.register_drop_method_id(&src, id)
573    }
574}
575
576#[tracing::instrument(skip(tcx))]
577pub fn translate<'tcx, 'ctx>(
578    options: &CliOpts,
579    tcx: TyCtxt<'tcx>,
580    sysroot: PathBuf,
581) -> TransformCtx {
582    let hax_state = hax::state::State::new(
583        tcx,
584        hax::options::Options {
585            inline_anon_consts: true,
586            resolve_drop_bounds: options.add_drop_bounds,
587        },
588    );
589
590    let crate_def_id: hax::DefId = rustc_span::def_id::CRATE_DEF_ID
591        .to_def_id()
592        .sinto(&hax_state);
593    let crate_name = crate_def_id.krate.clone();
594    trace!("# Crate: {}", crate_name);
595
596    let mut error_ctx = ErrorCtx::new(!options.abort_on_error, options.error_on_warnings);
597    let translate_options = TranslateOptions::new(&mut error_ctx, options);
598    let mut ctx = TranslateCtx {
599        tcx,
600        sysroot,
601        hax_state,
602        options: translate_options,
603        errors: RefCell::new(error_ctx),
604        translated: TranslatedCrate {
605            crate_name,
606            options: options.clone(),
607            ..TranslatedCrate::default()
608        },
609        id_map: Default::default(),
610        reverse_id_map: Default::default(),
611        file_to_id: Default::default(),
612        items_to_translate: Default::default(),
613        processed: Default::default(),
614        cached_item_metas: Default::default(),
615        cached_names: Default::default(),
616    };
617    ctx.register_target_info();
618
619    if options.start_from.is_empty() {
620        // Recursively register all the items in the crate, starting from the crate root.
621        ctx.enqueue_item(&crate_def_id);
622    } else {
623        // Start translating from the selected items.
624        for path in options.start_from.iter() {
625            let path = path.split("::").collect_vec();
626            let resolved = super::resolve_path::def_path_def_ids(&ctx.hax_state, &path);
627            match resolved {
628                Ok(resolved) => {
629                    for def_id in resolved {
630                        let def_id: hax::DefId = def_id.sinto(&ctx.hax_state);
631                        ctx.enqueue_item(&def_id);
632                    }
633                }
634                Err(path) => {
635                    let path = path.join("::");
636                    register_error!(
637                        ctx,
638                        Span::dummy(),
639                        "path {path} does not correspond to any item"
640                    );
641                }
642            }
643        }
644    }
645
646    trace!(
647        "Queue after we explored the crate:\n{:?}",
648        &ctx.items_to_translate
649    );
650
651    // Translate.
652    //
653    // For as long as the queue of items to translate is not empty, we pop the top item and
654    // translate it. If an item refers to non-translated (potentially external) items, we add them
655    // to the queue.
656    //
657    // Note that the order in which we translate the definitions doesn't matter:
658    // we never need to lookup a translated definition, and only use the map
659    // from Rust ids to translated ids.
660    while let Some(item_src) = ctx.items_to_translate.pop_first() {
661        trace!("About to translate item: {:?}", item_src);
662        if ctx.processed.insert(item_src.clone()) {
663            ctx.translate_item(&item_src);
664        }
665    }
666
667    // Return the context, dropping the hax state and rustc `tcx`.
668    TransformCtx {
669        options: ctx.options,
670        translated: ctx.translated,
671        errors: ctx.errors,
672    }
673}