charon_driver/translate/
translate_types.rs

1use super::translate_ctx::*;
2use charon_lib::ast::*;
3use charon_lib::builtins;
4use charon_lib::common::hash_by_addr::HashByAddr;
5use charon_lib::ids::Vector;
6use core::convert::*;
7use hax::HasParamEnv;
8use hax::Visibility;
9use hax_frontend_exporter as hax;
10use itertools::Itertools;
11
12impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
13    // Translate a region
14    pub(crate) fn translate_region(
15        &mut self,
16        span: Span,
17        region: &hax::Region,
18    ) -> Result<Region, Error> {
19        use hax::RegionKind::*;
20        match &region.kind {
21            ReErased => Ok(Region::Erased),
22            ReStatic => Ok(Region::Static),
23            ReBound(id, br) => {
24                let var = self.lookup_bound_region(span, *id, br.var)?;
25                Ok(Region::Var(var))
26            }
27            ReEarlyParam(region) => {
28                let var = self.lookup_early_region(span, region)?;
29                Ok(Region::Var(var))
30            }
31            ReVar(..) | RePlaceholder(..) => {
32                // Shouldn't exist outside of type inference.
33                raise_error!(
34                    self,
35                    span,
36                    "Should not exist outside of type inference: {region:?}"
37                )
38            }
39            ReLateParam(..) | ReError(..) => {
40                raise_error!(self, span, "Unexpected region kind: {region:?}")
41            }
42        }
43    }
44
45    /// Translate a Ty.
46    ///
47    /// Typically used in this module to translate the fields of a structure/
48    /// enumeration definition, or later to translate the type of a variable.
49    ///
50    /// Note that we take as parameter a function to translate regions, because
51    /// regions can be translated in several manners (non-erased region or erased
52    /// regions), in which case the return type is different.
53    #[tracing::instrument(skip(self, span))]
54    pub(crate) fn translate_ty(&mut self, span: Span, ty: &hax::Ty) -> Result<Ty, Error> {
55        trace!("{:?}", ty);
56        let cache_key = HashByAddr(ty.inner().clone());
57        if let Some(ty) = self
58            .innermost_binder()
59            .type_trans_cache
60            .get(&cache_key)
61            .cloned()
62        {
63            return Ok(ty.clone());
64        }
65
66        let kind = match ty.kind() {
67            hax::TyKind::Bool => TyKind::Literal(LiteralTy::Bool),
68            hax::TyKind::Char => TyKind::Literal(LiteralTy::Char),
69            hax::TyKind::Int(int_ty) => {
70                use hax::IntTy;
71                TyKind::Literal(LiteralTy::Integer(match int_ty {
72                    IntTy::Isize => IntegerTy::Isize,
73                    IntTy::I8 => IntegerTy::I8,
74                    IntTy::I16 => IntegerTy::I16,
75                    IntTy::I32 => IntegerTy::I32,
76                    IntTy::I64 => IntegerTy::I64,
77                    IntTy::I128 => IntegerTy::I128,
78                }))
79            }
80            hax::TyKind::Uint(int_ty) => {
81                use hax::UintTy;
82                TyKind::Literal(LiteralTy::Integer(match int_ty {
83                    UintTy::Usize => IntegerTy::Usize,
84                    UintTy::U8 => IntegerTy::U8,
85                    UintTy::U16 => IntegerTy::U16,
86                    UintTy::U32 => IntegerTy::U32,
87                    UintTy::U64 => IntegerTy::U64,
88                    UintTy::U128 => IntegerTy::U128,
89                }))
90            }
91            hax::TyKind::Float(float_ty) => {
92                use hax::FloatTy;
93                TyKind::Literal(LiteralTy::Float(match float_ty {
94                    FloatTy::F16 => charon_lib::ast::types::FloatTy::F16,
95                    FloatTy::F32 => charon_lib::ast::types::FloatTy::F32,
96                    FloatTy::F64 => charon_lib::ast::types::FloatTy::F64,
97                    FloatTy::F128 => charon_lib::ast::types::FloatTy::F128,
98                }))
99            }
100            hax::TyKind::Never => TyKind::Never,
101
102            hax::TyKind::Alias(alias) => match &alias.kind {
103                hax::AliasKind::Projection {
104                    impl_expr,
105                    assoc_item,
106                } => {
107                    let trait_ref = self.translate_trait_impl_expr(span, impl_expr)?;
108                    let name = self.t_ctx.translate_trait_item_name(&assoc_item.def_id)?;
109                    TyKind::TraitType(trait_ref, name)
110                }
111                hax::AliasKind::Opaque { hidden_ty, .. } => {
112                    return self.translate_ty(span, hidden_ty)
113                }
114                _ => {
115                    raise_error!(self, span, "Unsupported alias type: {:?}", alias.kind)
116                }
117            },
118
119            hax::TyKind::Adt {
120                generic_args: substs,
121                trait_refs,
122                def_id,
123            } => {
124                trace!("Adt: {:?}", def_id);
125
126                // Retrieve the type identifier
127                let type_id = self.translate_type_id(span, def_id)?;
128
129                // Translate the type parameters instantiation
130                let mut generics = self.translate_generic_args(
131                    span,
132                    substs,
133                    trait_refs,
134                    None,
135                    type_id.generics_target(),
136                )?;
137
138                // Filter the type arguments.
139                // TODO: do this in a micro-pass
140                if let TypeId::Builtin(builtin_ty) = type_id {
141                    let used_args = builtins::type_to_used_params(builtin_ty);
142                    error_assert!(self, span, generics.types.elem_count() == used_args.len());
143                    let types = std::mem::take(&mut generics.types)
144                        .into_iter()
145                        .zip(used_args)
146                        .filter(|(_, used)| *used)
147                        .map(|(ty, _)| ty)
148                        .collect();
149                    generics.types = types;
150                }
151
152                // Return the instantiated ADT
153                TyKind::Adt(type_id, generics)
154            }
155            hax::TyKind::Str => {
156                trace!("Str");
157
158                let id = TypeId::Builtin(BuiltinTy::Str);
159                TyKind::Adt(id, GenericArgs::empty(GenericsSource::Builtin))
160            }
161            hax::TyKind::Array(ty, const_param) => {
162                trace!("Array");
163
164                let c = self.translate_constant_expr_to_const_generic(span, const_param)?;
165                let tys = vec![self.translate_ty(span, ty)?].into();
166                let cgs = vec![c].into();
167                let id = TypeId::Builtin(BuiltinTy::Array);
168                TyKind::Adt(
169                    id,
170                    GenericArgs::new(
171                        Vector::new(),
172                        tys,
173                        cgs,
174                        Vector::new(),
175                        GenericsSource::Builtin,
176                    ),
177                )
178            }
179            hax::TyKind::Slice(ty) => {
180                trace!("Slice");
181
182                let tys = vec![self.translate_ty(span, ty)?].into();
183                let id = TypeId::Builtin(BuiltinTy::Slice);
184                TyKind::Adt(id, GenericArgs::new_for_builtin(tys))
185            }
186            hax::TyKind::Ref(region, ty, mutability) => {
187                trace!("Ref");
188
189                let region = self.translate_region(span, region)?;
190                let ty = self.translate_ty(span, ty)?;
191                let kind = if *mutability {
192                    RefKind::Mut
193                } else {
194                    RefKind::Shared
195                };
196                TyKind::Ref(region, ty, kind)
197            }
198            hax::TyKind::RawPtr(ty, mutbl) => {
199                trace!("RawPtr: {:?}", (ty, mutbl));
200                let ty = self.translate_ty(span, ty)?;
201                let kind = if *mutbl {
202                    RefKind::Mut
203                } else {
204                    RefKind::Shared
205                };
206                TyKind::RawPtr(ty, kind)
207            }
208            hax::TyKind::Tuple(substs) => {
209                trace!("Tuple");
210
211                let mut params = Vector::new();
212                for param in substs.iter() {
213                    let param_ty = self.translate_ty(span, param)?;
214                    params.push(param_ty);
215                }
216
217                TyKind::Adt(TypeId::Tuple, GenericArgs::new_for_builtin(params))
218            }
219
220            hax::TyKind::Param(param) => {
221                // A type parameter, for example `T` in `fn f<T>(x : T) {}`.
222                // Note that this type parameter may actually have been
223                // instantiated (in our environment, we may map it to another
224                // type): we just have to look it up.
225                // Note that if we are using this function to translate a field
226                // type in a type definition, it should actually map to a type
227                // parameter.
228                trace!("Param");
229
230                // Retrieve the translation of the substituted type:
231                let var = self.lookup_type_var(span, param)?;
232                TyKind::TypeVar(var)
233            }
234
235            hax::TyKind::Foreign(def_id) => {
236                trace!("Foreign");
237                let adt_id = self.translate_type_id(span, def_id)?;
238                TyKind::Adt(adt_id, GenericArgs::empty(adt_id.generics_target()))
239            }
240            hax::TyKind::Infer(_) => {
241                trace!("Infer");
242                raise_error!(self, span, "Unsupported type: infer type")
243            }
244
245            hax::TyKind::Dynamic(_existential_preds, _region, _) => {
246                // TODO: we don't translate the predicates yet because our machinery can't handle
247                // it.
248                trace!("Dynamic");
249                TyKind::DynTrait(ExistentialPredicate)
250            }
251
252            hax::TyKind::Coroutine(..) => {
253                trace!("Coroutine");
254                raise_error!(self, span, "Coroutine types are not supported yet")
255            }
256
257            hax::TyKind::Bound(_, _) => {
258                trace!("Bound");
259                raise_error!(self, span, "Unexpected type kind: bound")
260            }
261            hax::TyKind::Placeholder(_) => {
262                trace!("PlaceHolder");
263                raise_error!(self, span, "Unsupported type: placeholder")
264            }
265            hax::TyKind::Arrow(box sig) => {
266                trace!("Arrow");
267                trace!("bound vars: {:?}", sig.bound_vars);
268                let sig = self.translate_region_binder(span, sig, |ctx, sig| {
269                    let inputs = sig
270                        .inputs
271                        .iter()
272                        .map(|x| ctx.translate_ty(span, x))
273                        .try_collect()?;
274                    let output = ctx.translate_ty(span, &sig.output)?;
275                    Ok((inputs, output))
276                })?;
277                TyKind::Arrow(sig)
278            }
279            hax::TyKind::Closure(def_id, args) => {
280                let type_ref = self.translate_closure_type_ref(span, def_id, args)?;
281                TyKind::Adt(type_ref.id, *type_ref.generics)
282            }
283            hax::TyKind::Error => {
284                trace!("Error");
285                raise_error!(self, span, "Type checking error")
286            }
287            hax::TyKind::Todo(s) => {
288                trace!("Todo: {s}");
289                raise_error!(self, span, "Unsupported type: {:?}", s)
290            }
291        };
292        let ty = kind.into_ty();
293        self.innermost_binder_mut()
294            .type_trans_cache
295            .insert(cache_key, ty.clone());
296        Ok(ty)
297    }
298
299    pub fn translate_generic_args(
300        &mut self,
301        span: Span,
302        substs: &[hax::GenericArg],
303        trait_refs: &[hax::ImplExpr],
304        late_bound: Option<hax::Binder<()>>,
305        target: GenericsSource,
306    ) -> Result<GenericArgs, Error> {
307        use hax::GenericArg::*;
308        trace!("{:?}", substs);
309
310        let mut regions = Vector::new();
311        let mut types = Vector::new();
312        let mut const_generics = Vector::new();
313        for param in substs {
314            match param {
315                Type(param_ty) => {
316                    types.push(self.translate_ty(span, param_ty)?);
317                }
318                Lifetime(region) => {
319                    regions.push(self.translate_region(span, region)?);
320                }
321                Const(c) => {
322                    const_generics.push(self.translate_constant_expr_to_const_generic(span, c)?);
323                }
324            }
325        }
326        // Add the late-bounds lifetimes if any.
327        if let Some(binder) = late_bound {
328            for v in &binder.bound_vars {
329                match v {
330                    hax::BoundVariableKind::Region(_) => {
331                        regions.push(Region::Erased);
332                    }
333                    hax::BoundVariableKind::Ty(_) => {
334                        raise_error!(self, span, "Unexpected locally bound type variable")
335                    }
336                    hax::BoundVariableKind::Const => {
337                        raise_error!(self, span, "Unexpected locally bound const generic")
338                    }
339                }
340            }
341        }
342        let trait_refs = self.translate_trait_impl_exprs(span, trait_refs)?;
343
344        Ok(GenericArgs {
345            regions,
346            types,
347            const_generics,
348            trait_refs,
349            target,
350        })
351    }
352
353    /// Checks whether the given id corresponds to a built-in type.
354    fn recognize_builtin_type(&mut self, def_id: &hax::DefId) -> Result<Option<BuiltinTy>, Error> {
355        let def = self.hax_def(def_id)?;
356        let ty = if def.lang_item.as_deref() == Some("owned_box") && !self.t_ctx.options.raw_boxes {
357            Some(BuiltinTy::Box)
358        } else {
359            None
360        };
361        Ok(ty)
362    }
363
364    /// Translate a type def id
365    pub(crate) fn translate_type_id(
366        &mut self,
367        span: Span,
368        def_id: &hax::DefId,
369    ) -> Result<TypeId, Error> {
370        trace!("{:?}", def_id);
371        let type_id = match self.recognize_builtin_type(def_id)? {
372            Some(id) => TypeId::Builtin(id),
373            None => TypeId::Adt(self.register_type_decl_id(span, def_id)),
374        };
375        Ok(type_id)
376    }
377
378    /// Translate a Dynamically Sized Type metadata kind.
379    ///
380    /// Returns `None` if the type is generic, or if it is not a DST.
381    pub fn translate_ptr_metadata(&self) -> Option<PtrMetadata> {
382        // prepare the call to the method
383        use rustc_middle::ty;
384        let tcx = self.t_ctx.tcx;
385        let rdefid = self.def_id.as_rust_def_id().unwrap();
386        let ty_env = hax::State::new_from_state_and_id(&self.t_ctx.hax_state, rdefid).typing_env();
387        // This `skip_binder` is ok because it's an `EarlyBinder`.
388        let ty = tcx.type_of(rdefid).skip_binder();
389
390        // call the key method
391        match tcx
392            .struct_tail_raw(
393                ty,
394                |ty| tcx.try_normalize_erasing_regions(ty_env, ty).unwrap_or(ty),
395                || {},
396            )
397            .kind()
398        {
399            ty::Foreign(..) => Some(PtrMetadata::None),
400            ty::Str | ty::Slice(..) => Some(PtrMetadata::Length),
401            ty::Dynamic(..) => Some(PtrMetadata::VTable(VTable)),
402            // This is NOT accurate -- if there is no generic clause that states `?Sized`
403            // Then it will be safe to return `Some(PtrMetadata::None)`.
404            // TODO: inquire the generic clause to get the accurate info.
405            ty::Placeholder(..) | ty::Infer(..) | ty::Param(..) | ty::Bound(..) => None,
406            _ => Some(PtrMetadata::None),
407        }
408    }
409
410    /// Translate a type layout.
411    ///
412    /// Translates the layout as queried from rustc into
413    /// the more restricted [`Layout`].
414    #[tracing::instrument(skip(self))]
415    pub fn translate_layout(&self) -> Option<Layout> {
416        use rustc_abi as r_abi;
417        // Panics if the fields layout is not `Arbitrary`.
418        fn translate_variant_layout(
419            variant_layout: &r_abi::LayoutData<r_abi::FieldIdx, r_abi::VariantIdx>,
420        ) -> VariantLayout {
421            match &variant_layout.fields {
422                r_abi::FieldsShape::Arbitrary { offsets, .. } => {
423                    let mut v = Vector::with_capacity(offsets.len());
424                    for o in offsets.iter() {
425                        v.push(o.bytes());
426                    }
427                    VariantLayout { field_offsets: v }
428                }
429                r_abi::FieldsShape::Primitive
430                | r_abi::FieldsShape::Union(_)
431                | r_abi::FieldsShape::Array { .. } => panic!("Unexpected layout shape"),
432            }
433        }
434
435        fn translate_primitive_int(int_ty: r_abi::Integer, signed: bool) -> IntegerTy {
436            if signed {
437                match int_ty {
438                    r_abi::Integer::I8 => IntegerTy::I8,
439                    r_abi::Integer::I16 => IntegerTy::I16,
440                    r_abi::Integer::I32 => IntegerTy::I32,
441                    r_abi::Integer::I64 => IntegerTy::I64,
442                    r_abi::Integer::I128 => IntegerTy::I128,
443                }
444            } else {
445                match int_ty {
446                    r_abi::Integer::I8 => IntegerTy::U8,
447                    r_abi::Integer::I16 => IntegerTy::U16,
448                    r_abi::Integer::I32 => IntegerTy::U32,
449                    r_abi::Integer::I64 => IntegerTy::U64,
450                    r_abi::Integer::I128 => IntegerTy::U128,
451                }
452            }
453        }
454
455        let tcx = self.t_ctx.tcx;
456        let rdefid = self.def_id.as_rust_def_id().unwrap();
457        let ty_env = hax::State::new_from_state_and_id(&self.t_ctx.hax_state, rdefid).typing_env();
458        // This `skip_binder` is ok because it's an `EarlyBinder`.
459        let ty = tcx.type_of(rdefid).skip_binder();
460        let pseudo_input = ty_env.as_query_input(ty);
461
462        // If layout computation returns an error, we return `None`.
463        let layout = tcx.layout_of(pseudo_input).ok()?.layout;
464        let (size, align) = if layout.is_sized() {
465            (
466                Some(layout.size().bytes()),
467                Some(layout.align().abi.bytes()),
468            )
469        } else {
470            (None, None)
471        };
472
473        let mut variant_layouts = Vector::new();
474        match layout.variants() {
475            r_abi::Variants::Multiple { variants, .. } => {
476                for variant_layout in variants.iter() {
477                    variant_layouts.push(translate_variant_layout(variant_layout));
478                }
479            }
480            r_abi::Variants::Single { index } => {
481                assert!(*index == r_abi::VariantIdx::ZERO);
482                // For structs we add a single variant that has the field offsets. Unions don't
483                // have field offsets.
484                if let r_abi::FieldsShape::Arbitrary { .. } = layout.fields() {
485                    variant_layouts.push(translate_variant_layout(&layout));
486                }
487            }
488            r_abi::Variants::Empty => {}
489        }
490
491        // Get the offset of the discriminant when there is one.
492        let discriminant_layout = match layout.variants() {
493            r_abi::Variants::Multiple {
494                tag,
495                tag_encoding,
496                tag_field,
497                ..
498            } => {
499                match tag_encoding {
500                    r_abi::TagEncoding::Direct => {
501                        // The tag_field is the index into the `offsets` vector.
502                        let r_abi::FieldsShape::Arbitrary { offsets, .. } = layout.fields() else {
503                            unreachable!()
504                        };
505
506                        // Only translates the representation if it is an integer.
507                        let repr = match tag.primitive() {
508                            r_abi::Primitive::Int(int_ty, signed) => {
509                                translate_primitive_int(int_ty, signed)
510                            }
511                            _ => unreachable!(),
512                        };
513                        offsets
514                            .get(r_abi::FieldIdx::from_usize(*tag_field))
515                            .map(|s| DiscriminantLayout::Direct {
516                                offset: r_abi::Size::bytes(*s),
517                                repr,
518                            })
519                    }
520                    r_abi::TagEncoding::Niche { .. } => Some(DiscriminantLayout::Niche),
521                }
522            }
523            r_abi::Variants::Single { .. } | r_abi::Variants::Empty => None,
524        };
525
526        Some(Layout {
527            size,
528            align,
529            discriminant_layout,
530            uninhabited: layout.is_uninhabited(),
531            variant_layouts,
532        })
533    }
534
535    /// Translate the body of a type declaration.
536    ///
537    /// Note that the type may be external, in which case we translate the body
538    /// only if it is public (i.e., it is a public enumeration, or it is a
539    /// struct with only public fields).
540    pub(crate) fn translate_adt_def(
541        &mut self,
542        trans_id: TypeDeclId,
543        def_span: Span,
544        item_meta: &ItemMeta,
545        adt: &hax::AdtDef,
546    ) -> Result<TypeDeclKind, Error> {
547        use hax::AdtKind;
548
549        if item_meta.opacity.is_opaque() {
550            return Ok(TypeDeclKind::Opaque);
551        }
552
553        trace!("{}", trans_id);
554
555        // In case the type is external, check if we should consider the type as
556        // transparent (i.e., extract its body). If it is an enumeration, then yes
557        // (because the variants of public enumerations are public, together with their
558        // fields). If it is a structure, we check if all the fields are public.
559        let contents_are_public = match adt.adt_kind {
560            AdtKind::Enum => true,
561            AdtKind::Struct | AdtKind::Union => {
562                // Check the unique variant
563                error_assert!(self, def_span, adt.variants.len() == 1);
564                adt.variants[0]
565                    .fields
566                    .iter()
567                    .all(|f| matches!(f.vis, Visibility::Public))
568            }
569        };
570
571        if item_meta
572            .opacity
573            .with_content_visibility(contents_are_public)
574            .is_opaque()
575        {
576            return Ok(TypeDeclKind::Opaque);
577        }
578
579        // The type is transparent: explore the variants
580        let mut variants: Vector<VariantId, Variant> = Default::default();
581        for (i, var_def) in adt.variants.iter().enumerate() {
582            trace!("variant {i}: {var_def:?}");
583
584            let mut fields: Vector<FieldId, Field> = Default::default();
585            /* This is for sanity: check that either all the fields have names, or
586             * none of them has */
587            let mut have_names: Option<bool> = None;
588            for (j, field_def) in var_def.fields.iter().enumerate() {
589                trace!("variant {i}: field {j}: {field_def:?}");
590                let field_span = self.t_ctx.translate_span_from_hax(&field_def.span);
591                // Translate the field type
592                let ty = self.translate_ty(field_span, &field_def.ty)?;
593                let field_full_def = self.hax_def(&field_def.did)?;
594                let field_attrs = self.t_ctx.translate_attr_info(&field_full_def);
595
596                // Retrieve the field name.
597                let field_name = field_def.name.clone();
598                // Sanity check
599                match &have_names {
600                    None => {
601                        have_names = match &field_name {
602                            None => Some(false),
603                            Some(_) => Some(true),
604                        }
605                    }
606                    Some(b) => {
607                        error_assert!(self, field_span, *b == field_name.is_some());
608                    }
609                };
610
611                // Store the field
612                let field = Field {
613                    span: field_span,
614                    attr_info: field_attrs,
615                    name: field_name.clone(),
616                    ty,
617                };
618                fields.push(field);
619            }
620
621            let discriminant = self.translate_discriminant(def_span, &var_def.discr_val)?;
622            let variant_span = self.t_ctx.translate_span_from_hax(&var_def.span);
623            let variant_name = var_def.name.clone();
624            let variant_full_def = self.hax_def(&var_def.def_id)?;
625            let variant_attrs = self.t_ctx.translate_attr_info(&variant_full_def);
626
627            let mut variant = Variant {
628                span: variant_span,
629                attr_info: variant_attrs,
630                name: variant_name,
631                fields,
632                discriminant,
633            };
634            // Propagate a `#[charon::variants_prefix(..)]` or `#[charon::variants_suffix(..)]` attribute to the variants.
635            if variant.attr_info.rename.is_none() {
636                let prefix = item_meta
637                    .attr_info
638                    .attributes
639                    .iter()
640                    .filter_map(|a| a.as_variants_prefix())
641                    .next()
642                    .map(|attr| attr.as_str());
643                let suffix = item_meta
644                    .attr_info
645                    .attributes
646                    .iter()
647                    .filter_map(|a| a.as_variants_suffix())
648                    .next()
649                    .map(|attr| attr.as_str());
650                if prefix.is_some() || suffix.is_some() {
651                    let prefix = prefix.unwrap_or_default();
652                    let suffix = suffix.unwrap_or_default();
653                    let name = &variant.name;
654                    variant.attr_info.rename = Some(format!("{prefix}{name}{suffix}"));
655                }
656            }
657            variants.push(variant);
658        }
659
660        // Register the type
661        let type_def_kind: TypeDeclKind = match adt.adt_kind {
662            AdtKind::Struct => TypeDeclKind::Struct(variants[0].fields.clone()),
663            AdtKind::Enum => TypeDeclKind::Enum(variants),
664            AdtKind::Union => TypeDeclKind::Union(variants[0].fields.clone()),
665        };
666
667        Ok(type_def_kind)
668    }
669
670    fn translate_discriminant(
671        &mut self,
672        def_span: Span,
673        discr: &hax::DiscriminantValue,
674    ) -> Result<ScalarValue, Error> {
675        let ty = self.translate_ty(def_span, &discr.ty)?;
676        let int_ty = *ty.kind().as_literal().unwrap().as_integer().unwrap();
677        Ok(ScalarValue::from_bits(int_ty, discr.val))
678    }
679}
charon_driver/translate/translate_types.rs

charon_driver/translate/
translate_types.rs
