charon_lib/ast/items/
item_ids.rs

1use std::cmp::{Ord, PartialOrd};
2
3use derive_generic_visitor::{Drive, DriveMut, DriveTwo};
4use serde::{Deserialize, Serialize};
5use serde_state::{DeserializeState, SerializeState};
6
7use crate::ast::*;
8use macros::{EnumAsGetters, EnumIsA, VariantIndexArity, VariantName};
9
10generate_index_type!(FunDeclId, "Fun");
11generate_index_type!(TypeDeclId, "Adt");
12generate_index_type!(GlobalDeclId, "Global");
13generate_index_type!(TraitDeclId, "TraitDecl");
14generate_index_type!(TraitImplId, "TraitImpl");
15
16/// The id of a translated item.
17#[derive(
18    Copy,
19    Clone,
20    Debug,
21    PartialOrd,
22    Ord,
23    PartialEq,
24    Eq,
25    Hash,
26    EnumIsA,
27    EnumAsGetters,
28    VariantName,
29    VariantIndexArity,
30    Serialize,
31    Deserialize,
32    SerializeState,
33    DeserializeState,
34    Drive,
35    DriveMut,
36    DriveTwo,
37)]
38#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("Id"))]
39#[serde_state(stateless)]
40pub enum ItemId {
41    Type(TypeDeclId),
42    TraitDecl(TraitDeclId),
43    TraitImpl(TraitImplId),
44    Fun(FunDeclId),
45    Global(GlobalDeclId),
46}
47
48/// The id of an associated item within a trait.
49#[derive(
50    Copy,
51    Clone,
52    Debug,
53    PartialOrd,
54    Ord,
55    PartialEq,
56    Eq,
57    Hash,
58    EnumIsA,
59    EnumAsGetters,
60    VariantName,
61    VariantIndexArity,
62    Serialize,
63    Deserialize,
64    SerializeState,
65    DeserializeState,
66    Drive,
67    DriveMut,
68    DriveTwo,
69)]
70#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("AssocId"))]
71#[serde_state(stateless)]
72pub enum AssocItemId {
73    Type(AssocTypeId),
74    Method(TraitMethodId),
75    Const(AssocConstId),
76}
77
78/// The id of a translated item or associated item definition.
79#[derive(
80    Copy,
81    Clone,
82    Debug,
83    PartialOrd,
84    Ord,
85    PartialEq,
86    Eq,
87    Hash,
88    EnumIsA,
89    EnumAsGetters,
90    VariantName,
91    VariantIndexArity,
92    Serialize,
93    Deserialize,
94    SerializeState,
95    DeserializeState,
96    Drive,
97    DriveMut,
98    DriveTwo,
99)]
100#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("Item"))]
101#[serde_state(stateless)]
102pub enum MaybeAssocItemId {
103    Free(ItemId),
104    Assoc(TraitDeclId, AssocItemId),
105}
106
107/// Reference to a type declaration or builtin type.
108#[derive(
109    Debug,
110    Clone,
111    PartialEq,
112    Eq,
113    PartialOrd,
114    Ord,
115    Hash,
116    SerializeState,
117    DeserializeState,
118    Drive,
119    DriveMut,
120    DriveTwo,
121)]
122pub struct TypeDeclRef {
123    pub id: TypeId,
124    pub generics: BoxedArgs,
125}
126
127/// Type identifier.
128///
129/// Allows us to factorize the code for built-in types and ADTs.
130#[derive(
131    Debug,
132    PartialEq,
133    Eq,
134    Clone,
135    Copy,
136    VariantName,
137    EnumAsGetters,
138    EnumIsA,
139    SerializeState,
140    DeserializeState,
141    Drive,
142    DriveMut,
143    DriveTwo,
144    Hash,
145    Ord,
146    PartialOrd,
147)]
148#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("T"))]
149pub enum TypeId {
150    /// A "regular" ADT type.
151    ///
152    /// Includes transparent ADTs and opaque ADTs (local ADTs marked as opaque,
153    /// and external ADTs).
154    #[cfg_attr(feature = "charon_on_charon", charon::rename("TAdtId"))]
155    Adt(TypeDeclId),
156    /// Built-in type. Either a primitive type like array or slice, or a
157    /// non-primitive type coming from a standard library
158    /// and that we handle like a primitive type. Types falling into this
159    /// category include: Box, Vec, Cell...
160    /// The Array and Slice types were initially modelled as primitive in
161    /// the [Ty] type. We decided to move them to built-in types as it allows
162    /// for more uniform treatment throughout the codebase.
163    #[cfg_attr(feature = "charon_on_charon", charon::rename("TBuiltin"))]
164    #[serde_state(stateless)]
165    Builtin(BuiltinTy),
166}
167
168/// Reference to a function declaration.
169#[derive(
170    Debug,
171    Clone,
172    PartialEq,
173    Eq,
174    PartialOrd,
175    Ord,
176    Hash,
177    SerializeState,
178    DeserializeState,
179    Drive,
180    DriveMut,
181    DriveTwo,
182)]
183pub struct FunDeclRef {
184    pub id: FunDeclId,
185    /// Generic arguments passed to the function.
186    pub generics: BoxedArgs,
187}
188
189/// A regular or builtin function.
190#[derive(
191    Debug,
192    Clone,
193    PartialEq,
194    Eq,
195    PartialOrd,
196    Ord,
197    Hash,
198    EnumIsA,
199    EnumAsGetters,
200    VariantName,
201    SerializeState,
202    DeserializeState,
203    Drive,
204    DriveMut,
205    DriveTwo,
206)]
207#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("F"))]
208#[serde_state(stateless)]
209pub enum FunId {
210    /// A "regular" function (function local to the crate, external function
211    /// not treated as a primitive one).
212    Regular(FunDeclId),
213    /// A primitive function, coming from a standard library (for instance:
214    /// `alloc::boxed::Box::new`).
215    /// TODO: rename to "Primitive"
216    #[cfg_attr(feature = "charon_on_charon", charon::rename("FBuiltin"))]
217    Builtin(BuiltinFunId),
218}
219
220/// A built-in function, representing a specific built-in function that's part of the LLBC semantics.
221#[derive(
222    Debug,
223    Clone,
224    Copy,
225    PartialEq,
226    Eq,
227    PartialOrd,
228    Ord,
229    Hash,
230    EnumIsA,
231    EnumAsGetters,
232    VariantName,
233    Serialize,
234    Deserialize,
235    Drive,
236    DriveMut,
237    DriveTwo,
238)]
239pub enum BuiltinFunId {
240    /// Used instead of `alloc::boxed::Box::new` when `--treat-box-as-builtin` is set.
241    BoxNew,
242    /// Cast `&[T; N]` to `&[T]`.
243    ///
244    /// This is used instead of unsizing coercions when `--ops-to-function-calls` is set.
245    ArrayToSliceShared,
246    /// Cast `&mut [T; N]` to `&mut [T]`.
247    ///
248    /// This is used instead of unsizing coercions when `--ops-to-function-calls` is set.
249    ArrayToSliceMut,
250    /// `repeat(n, x)` returns an array where `x` has been replicated `n` times.
251    ///
252    /// This is used instead of `Rvalue::ArrayRepeat` when `--ops-to-function-calls` is set.
253    ArrayRepeat,
254    /// A built-in funciton introduced instead of array/slice place indexing when
255    /// `--index-to-function-calls` is set. The signature depends on the parameters. It could look
256    /// like:
257    /// - `fn ArrayIndexShared<T,N>(&[T;N], usize) -> &T`
258    /// - `fn SliceIndexShared<T>(&[T], usize) -> &T`
259    /// - `fn ArraySubSliceShared<T,N>(&[T;N], usize, usize) -> &[T]`
260    /// - `fn SliceSubSliceMut<T>(&mut [T], usize, usize) -> &mut [T]`
261    /// - etc
262    Index(BuiltinIndexOp),
263    /// Build a raw pointer, from a data pointer and metadata. The metadata can be unit, if
264    /// building a thin pointer.
265    ///
266    /// This is used instead of `AggregateKind::RawPtr` when `--ops-to-function-calls` is set.
267    PtrFromParts(RefKind),
268}
269
270/// One of 8 built-in indexing operations.
271#[derive(
272    Debug,
273    Clone,
274    Copy,
275    PartialEq,
276    Eq,
277    PartialOrd,
278    Ord,
279    Hash,
280    Serialize,
281    Deserialize,
282    Drive,
283    DriveMut,
284    DriveTwo,
285)]
286pub struct BuiltinIndexOp {
287    /// Whether this is a slice or array.
288    #[drive(skip)]
289    pub is_array: bool,
290    /// Whether we're indexing mutably or not. Determines the type ofreference of the input and
291    /// output.
292    pub mutability: RefKind,
293    /// Whether we're indexing a single element or a subrange. If `true`, the function takes
294    /// two indices and the output is a slice; otherwise, the function take one index and the
295    /// output is a reference to a single element.
296    #[drive(skip)]
297    pub is_range: bool,
298}
299
300#[derive(
301    Debug,
302    Clone,
303    PartialEq,
304    Eq,
305    PartialOrd,
306    Ord,
307    EnumAsGetters,
308    SerializeState,
309    DeserializeState,
310    Drive,
311    DriveMut,
312    DriveTwo,
313    Hash,
314)]
315pub enum FnPtrKind {
316    #[cfg_attr(feature = "charon_on_charon", charon::rename("FunId"))]
317    Fun(FunId),
318    /// If a trait: the reference to the trait and the id of the trait method.
319    #[cfg_attr(feature = "charon_on_charon", charon::rename("TraitMethod"))]
320    Trait(TraitRef, TraitMethodId),
321}
322
323/// Reference to a function, possibly indirected via a trait.
324#[derive(
325    Debug,
326    PartialEq,
327    Eq,
328    PartialOrd,
329    Ord,
330    Clone,
331    Hash,
332    SerializeState,
333    DeserializeState,
334    Drive,
335    DriveMut,
336    DriveTwo,
337)]
338pub struct FnPtr {
339    pub kind: Box<FnPtrKind>,
340    pub generics: BoxedArgs,
341}
342
343/// Reference to a function, possibly indirected via a trait.
344/// Used to convert from `DeclRef`.
345#[derive(
346    Debug, Clone, SerializeState, DeserializeState, PartialEq, Eq, Hash, Drive, DriveMut, DriveTwo,
347)]
348pub struct MaybeBuiltinFunDeclRef {
349    pub id: FunId,
350    pub generics: BoxedArgs,
351    pub trait_ref: Option<TraitRef>,
352}
353
354/// Reference to a global declaration.
355#[derive(
356    Debug,
357    Clone,
358    PartialEq,
359    Eq,
360    PartialOrd,
361    Ord,
362    Hash,
363    SerializeState,
364    DeserializeState,
365    Drive,
366    DriveMut,
367    DriveTwo,
368)]
369pub struct GlobalDeclRef {
370    pub id: GlobalDeclId,
371    pub generics: BoxedArgs,
372}
373
374/// A predicate of the form `Type: Trait<Args>`.
375///
376/// About the generics, if we write:
377/// ```text
378/// impl Foo<bool> for String { ... }
379/// ```
380///
381/// The substitution is: `[String, bool]`.
382#[derive(
383    Debug,
384    Clone,
385    PartialEq,
386    Eq,
387    PartialOrd,
388    Ord,
389    Hash,
390    SerializeState,
391    DeserializeState,
392    Drive,
393    DriveMut,
394    DriveTwo,
395)]
396pub struct TraitDeclRef {
397    pub id: TraitDeclId,
398    pub generics: BoxedArgs,
399}
400
401/// A reference to a tait impl, using the provided arguments.
402#[derive(
403    Debug,
404    Clone,
405    PartialEq,
406    Eq,
407    PartialOrd,
408    Ord,
409    Hash,
410    SerializeState,
411    DeserializeState,
412    Drive,
413    DriveMut,
414    DriveTwo,
415)]
416pub struct TraitImplRef {
417    pub id: TraitImplId,
418    pub generics: BoxedArgs,
419}
420
421impl TypeDeclRef {
422    pub fn new(id: TypeId, generics: GenericArgs) -> Self {
423        Self {
424            id,
425            generics: Box::new(generics),
426        }
427    }
428
429    pub fn as_builtin(&self) -> Option<BuiltinTy> {
430        self.id.as_builtin().copied()
431    }
432
433    pub fn as_adt(&self) -> Option<TypeDeclId> {
434        self.id.as_adt().copied()
435    }
436
437    pub fn as_adt_mut(&mut self) -> Option<&mut TypeDeclId> {
438        self.id.as_adt_mut()
439    }
440
441    #[track_caller]
442    pub fn adt_id(&self) -> TypeDeclId {
443        self.as_adt()
444            .expect("called `TypeDeclRef::adt_id` on a builtin type")
445    }
446
447    pub fn is_box(&self) -> bool {
448        self.as_builtin() == Some(BuiltinTy::Box)
449    }
450
451    pub fn is_tuple(&self) -> bool {
452        self.as_builtin() == Some(BuiltinTy::Tuple)
453    }
454
455    pub fn is_str(&self) -> bool {
456        self.as_builtin() == Some(BuiltinTy::Str)
457    }
458}
459
460impl TraitDeclRef {
461    pub fn self_ty<'a>(&'a self, krate: &'a TranslatedCrate) -> Option<&'a Ty> {
462        match self.generics.types.iter().next() {
463            Some(ty) => Some(ty),
464            // TODO(mono): A monomorphized trait takes no arguments.
465            None => {
466                let name = krate.item_name(self.id);
467                let args = name.name.last()?.as_monomorphized()?;
468                args.types.iter().next()
469            }
470        }
471    }
472}
473
474impl FnPtr {
475    pub fn new(kind: FnPtrKind, generics: impl Into<BoxedArgs>) -> Self {
476        Self {
477            kind: Box::new(kind),
478            generics: generics.into(),
479        }
480    }
481
482    /// Get the generics for the pre-monomorphization item.
483    pub fn pre_mono_generics<'a>(&'a self, krate: &'a TranslatedCrate) -> &'a GenericArgs {
484        match *self.kind {
485            FnPtrKind::Fun(FunId::Regular(fun_id)) => krate
486                .item_name(fun_id)
487                .mono_args()
488                .unwrap_or(&self.generics),
489            //  We don't mono builtins.
490            FnPtrKind::Fun(FunId::Builtin(..)) => &self.generics,
491            // Can't happen in mono mode.
492            FnPtrKind::Trait(..) => &self.generics,
493        }
494    }
495}
496
497impl FnPtrKind {
498    pub fn mk_builtin(aid: BuiltinFunId) -> Self {
499        Self::Fun(FunId::Builtin(aid))
500    }
501}
502
503/// A generic `*DeclRef`-shaped struct, used when we're generic over the type of item.
504#[derive(Debug, PartialEq, Eq, Clone, Drive, DriveMut, DriveTwo)]
505pub struct DeclRef<Id> {
506    pub id: Id,
507    pub generics: BoxedArgs,
508    /// If the item is a trait associated item, `generics` are only those of the item, and this
509    /// contains a reference to the trait.
510    // TODO: also store `AssocItemId` so that we can convert to `FnPtr` without
511    // `MaybeBuiltinFunDeclRef`.
512    pub trait_ref: Option<TraitRef>,
513}
514
515impl DeclRef<ItemId> {
516    pub fn try_convert_id<Id>(self) -> Result<DeclRef<Id>, <ItemId as TryInto<Id>>::Error>
517    where
518        ItemId: TryInto<Id>,
519    {
520        Ok(DeclRef {
521            id: self.id.try_into()?,
522            generics: self.generics,
523            trait_ref: self.trait_ref,
524        })
525    }
526}
527
528// Implement `DeclRef<_>` -> `FooDeclRef` conversions.
529macro_rules! convert_item_ref {
530    ($item_ref_ty:ident($id:ident)) => {
531        impl TryFrom<DeclRef<ItemId>> for $item_ref_ty {
532            type Error = ();
533            fn try_from(item: DeclRef<ItemId>) -> Result<Self, ()> {
534                assert!(item.trait_ref.is_none());
535                Ok($item_ref_ty {
536                    id: item.id.try_into()?,
537                    generics: item.generics,
538                })
539            }
540        }
541        impl From<DeclRef<$id>> for $item_ref_ty {
542            fn from(item: DeclRef<$id>) -> Self {
543                assert!(item.trait_ref.is_none());
544                $item_ref_ty {
545                    id: item.id,
546                    generics: item.generics,
547                }
548            }
549        }
550    };
551}
552convert_item_ref!(TypeDeclRef(TypeId));
553convert_item_ref!(FunDeclRef(FunDeclId));
554convert_item_ref!(GlobalDeclRef(GlobalDeclId));
555convert_item_ref!(TraitDeclRef(TraitDeclId));
556convert_item_ref!(TraitImplRef(TraitImplId));
557impl TryFrom<DeclRef<ItemId>> for FnPtr {
558    type Error = ();
559    fn try_from(item: DeclRef<ItemId>) -> Result<Self, ()> {
560        if item.trait_ref.is_some() {
561            panic!(
562                "converting `DeclRef<ItemId>` to `FnPtr` cannot
563                deal with the trait method case."
564            )
565        }
566        let id: FunId = item.id.try_into()?;
567        Ok(FnPtr::new(id.into(), item.generics))
568    }
569}
570impl From<FunDeclRef> for FnPtr {
571    fn from(fn_ref: FunDeclRef) -> Self {
572        FnPtr::new(fn_ref.id.into(), fn_ref.generics)
573    }
574}
575impl TryFrom<DeclRef<ItemId>> for MaybeBuiltinFunDeclRef {
576    type Error = ();
577    fn try_from(item: DeclRef<ItemId>) -> Result<Self, ()> {
578        Ok(item.try_convert_id::<FunId>()?.into())
579    }
580}
581impl From<DeclRef<FunId>> for MaybeBuiltinFunDeclRef {
582    fn from(item: DeclRef<FunId>) -> Self {
583        MaybeBuiltinFunDeclRef {
584            id: item.id,
585            generics: item.generics,
586            trait_ref: item.trait_ref,
587        }
588    }
589}
590
591/// Implement `TryFrom`  and `From` to convert between an enum and its variants.
592macro_rules! wrap_unwrap_enum {
593    ($enum:ident::$variant:ident($variant_ty:ident)) => {
594        impl TryFrom<$enum> for $variant_ty {
595            type Error = ();
596            fn try_from(x: $enum) -> Result<Self, Self::Error> {
597                match x {
598                    $enum::$variant(x) => Ok(x),
599                    _ => Err(()),
600                }
601            }
602        }
603
604        impl From<$variant_ty> for $enum {
605            fn from(x: $variant_ty) -> Self {
606                $enum::$variant(x)
607            }
608        }
609    };
610}
611
612wrap_unwrap_enum!(ItemId::Fun(FunDeclId));
613wrap_unwrap_enum!(ItemId::Global(GlobalDeclId));
614wrap_unwrap_enum!(ItemId::Type(TypeDeclId));
615wrap_unwrap_enum!(ItemId::TraitDecl(TraitDeclId));
616wrap_unwrap_enum!(ItemId::TraitImpl(TraitImplId));
617wrap_unwrap_enum!(AssocItemId::Type(AssocTypeId));
618wrap_unwrap_enum!(AssocItemId::Method(TraitMethodId));
619wrap_unwrap_enum!(AssocItemId::Const(AssocConstId));
620
621impl TryFrom<ItemId> for TypeId {
622    type Error = ();
623    fn try_from(x: ItemId) -> Result<Self, Self::Error> {
624        Ok(TypeId::Adt(x.try_into()?))
625    }
626}
627impl TryFrom<ItemId> for FunId {
628    type Error = ();
629    fn try_from(x: ItemId) -> Result<Self, Self::Error> {
630        Ok(FunId::Regular(x.try_into()?))
631    }
632}
633impl From<FunDeclId> for FunId {
634    fn from(id: FunDeclId) -> Self {
635        Self::Regular(id)
636    }
637}
638impl From<BuiltinFunId> for FunId {
639    fn from(id: BuiltinFunId) -> Self {
640        Self::Builtin(id)
641    }
642}
643impl From<FunDeclId> for FnPtrKind {
644    fn from(id: FunDeclId) -> Self {
645        Self::Fun(id.into())
646    }
647}
648impl From<FunId> for FnPtrKind {
649    fn from(id: FunId) -> Self {
650        Self::Fun(id)
651    }
652}
charon_lib/ast/items/item_ids.rs

charon_lib/ast/items/
item_ids.rs
