charon_lib/ast/bodies/
places.rs

1//! Implements expressions: paths, operands, rvalues, lvalues
2use crate::ast::*;
3use derive_generic_visitor::{Drive, DriveMut, DriveTwo};
4use macros::{EnumAsGetters, EnumIsA, EnumToGetters, VariantName};
5use serde_state::{DeserializeState, SerializeState};
6
7#[derive(
8    Debug, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut, DriveTwo,
9)]
10#[serde_state(state_implements = DedupSerializerState)] // Avoid corecursive impls due to perfect derive
11pub struct Place {
12    pub kind: PlaceKind,
13    pub ty: Ty,
14}
15
16#[derive(
17    Debug,
18    PartialEq,
19    Eq,
20    Clone,
21    EnumIsA,
22    EnumAsGetters,
23    EnumToGetters,
24    SerializeState,
25    DeserializeState,
26    Drive,
27    DriveMut,
28    DriveTwo,
29)]
30#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("Place"))]
31pub enum PlaceKind {
32    /// A local variable in a function body.
33    Local(LocalId),
34    /// A subplace of a place.
35    Projection(Box<Place>, ProjectionElem),
36    /// A global (const or static).
37    /// Not present in MIR; introduced in [simplify_constants.rs].
38    Global(GlobalDeclRef),
39}
40
41/// Projects a place to a subplace.
42#[derive(
43    Debug,
44    PartialEq,
45    Eq,
46    Clone,
47    EnumIsA,
48    EnumAsGetters,
49    EnumToGetters,
50    VariantName,
51    SerializeState,
52    DeserializeState,
53    Drive,
54    DriveMut,
55    DriveTwo,
56)]
57pub enum ProjectionElem {
58    /// Dereference a shared/mutable reference, a box, or a raw pointer.
59    Deref,
60    /// Project to the field of an ADT (struct, union, or enum).
61    Field(Option<VariantId>, FieldId),
62    /// A built-in pointer (a reference, raw pointer, or `Box`) in Rust is always a fat pointer: it
63    /// contains an address and metadata for the pointed-to place. This metadata is empty for sized
64    /// types, it's the length for slices, and the vtable for `dyn Trait`.
65    ///
66    /// We consider such pointers to be like a struct with two fields; this represent access to the
67    /// metadata "field".
68    PtrMetadata,
69    /// MIR imposes that the argument to an index projection be a local variable, meaning
70    /// that even constant indices into arrays are let-bound as separate variables.
71    /// We **eliminate** this variant in a micro-pass for LLBC.
72    #[cfg_attr(feature = "charon_on_charon", charon::rename("ProjIndex"))]
73    Index {
74        offset: Box<Operand>,
75        from_end: bool,
76    },
77    /// Take a subslice of a slice or array. If `from_end` is `true` this is
78    /// `slice[from..slice.len() - to]`, otherwise this is `slice[from..to]`.
79    /// We **eliminate** this variant in a micro-pass for LLBC.
80    Subslice {
81        from: Box<Operand>,
82        to: Box<Operand>,
83        from_end: bool,
84    },
85}
86
87impl Place {
88    pub fn new(local_id: LocalId, ty: Ty) -> Place {
89        Place {
90            kind: PlaceKind::Local(local_id),
91            ty,
92        }
93    }
94
95    pub fn new_global(global: GlobalDeclRef, ty: Ty) -> Place {
96        Place {
97            kind: PlaceKind::Global(global),
98            ty,
99        }
100    }
101
102    pub fn ty(&self) -> &Ty {
103        &self.ty
104    }
105
106    /// Whether this place corresponds to a local variable without any projections.
107    pub fn is_local(&self) -> bool {
108        self.as_local().is_some()
109    }
110
111    /// If this place corresponds to an unprojected local, return the variable id.
112    pub fn as_local(&self) -> Option<LocalId> {
113        self.kind.as_local().copied()
114    }
115
116    pub fn as_projection(&self) -> Option<(&Self, &ProjectionElem)> {
117        self.kind.as_projection().map(|(pl, pj)| (pl.as_ref(), pj))
118    }
119
120    #[deprecated(note = "use `local_id` instead")]
121    pub fn var_id(&self) -> Option<LocalId> {
122        self.local_id()
123    }
124    pub fn local_id(&self) -> Option<LocalId> {
125        match &self.kind {
126            PlaceKind::Local(var_id) => Some(*var_id),
127            PlaceKind::Projection(subplace, _) => subplace.local_id(),
128            PlaceKind::Global(_) => None,
129        }
130    }
131
132    pub fn project(self, elem: ProjectionElem, ty: Ty) -> Self {
133        Self {
134            kind: PlaceKind::Projection(Box::new(self), elem),
135            ty,
136        }
137    }
138
139    pub fn project_auto_ty(self, krate: &TranslatedCrate, proj: ProjectionElem) -> Option<Self> {
140        Some(Place {
141            ty: proj.project_type(krate, &self.ty)?,
142            kind: PlaceKind::Projection(Box::new(self), proj),
143        })
144    }
145
146    /// Dereferences the place. Panics if the type cannot be dereferenced.
147    pub fn deref(self) -> Place {
148        use TyKind::*;
149        let proj_ty = match self.ty.kind() {
150            Ref(_, ty, _) | RawPtr(ty, _) => ty.clone(),
151            Adt(tref) if tref.is_box() => tref.generics.types[0].clone(),
152            Adt(..) | TypeVar(_) | Scalar(_) | Never | TraitType(..) | DynTrait(..) | FnPtr(..)
153            | FnDef(..) | PtrMetadata(..) | Array(..) | Slice(..) | Pattern(..) | Error(..) => {
154                panic!("internal type error")
155            }
156        };
157        Place {
158            ty: proj_ty,
159            kind: PlaceKind::Projection(Box::new(self), ProjectionElem::Deref),
160        }
161    }
162
163    /// Iterate over the subplaces of this place, starting with the place itself.
164    pub fn subplaces(&self) -> impl Iterator<Item = &Self> {
165        std::iter::successors(Some(self), |place| Some(place.as_projection()?.0))
166    }
167
168    pub fn projections(&self) -> impl Iterator<Item = &ProjectionElem> {
169        self.subplaces()
170            .filter_map(|place| Some(place.as_projection()?.1))
171    }
172}
173
174impl ProjectionElem {
175    /// Compute the type obtained when applying the current projection to a place of type `ty`.
176    pub fn project_type(&self, krate: &TranslatedCrate, ty: &Ty) -> Option<Ty> {
177        use ProjectionElem::*;
178        Some(match self {
179            Deref => {
180                use TyKind::*;
181                match ty.kind() {
182                    Ref(_, ty, _) | RawPtr(ty, _) => ty.clone(),
183                    Adt(tref) if tref.is_box() => tref.generics.types[0].clone(),
184                    Adt(..) | TypeVar(_) | Scalar(_) | Never | TraitType(..) | DynTrait(..)
185                    | Array(..) | Slice(..) | FnPtr(..) | FnDef(..) | PtrMetadata(..)
186                    | Pattern(..) | Error(..) => {
187                        // Type error
188                        return None;
189                    }
190                }
191            }
192            Field(variant_id, field_id) => {
193                let tref = ty.as_adt().unwrap();
194                let type_decl = krate.type_decls.get(tref.id)?;
195                use TypeDeclKind::*;
196                match &type_decl.kind {
197                    Struct(fields) | Union(fields) => {
198                        if variant_id.is_some() {
199                            return None;
200                        };
201                        fields.get(*field_id)?.ty.clone().substitute(&tref.generics)
202                    }
203                    Enum(variants) => {
204                        let variant_id = (*variant_id)?;
205                        let variant = variants.get(variant_id)?;
206                        variant
207                            .fields
208                            .get(*field_id)?
209                            .ty
210                            .clone()
211                            .substitute(&tref.generics)
212                    }
213                    Opaque | Alias(_) | Error(_) => return None,
214                }
215            }
216            PtrMetadata => ty.get_ptr_metadata(krate).into_type(),
217            Index { .. } | Subslice { .. } => ty.as_array_or_slice()?.clone(),
218        })
219    }
220}
charon_lib/ast/bodies/places.rs

charon_lib/ast/bodies/
places.rs
