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

charon_lib/ast/bodies/
places.rs
