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}
62
63impl Place {
64    pub fn new(local_id: LocalId, ty: Ty) -> Place {
65        Place {
66            kind: PlaceKind::Local(local_id),
67            ty,
68        }
69    }
70
71    pub fn new_global(global: GlobalDeclRef, ty: Ty) -> Place {
72        Place {
73            kind: PlaceKind::Global(global),
74            ty,
75        }
76    }
77
78    pub fn ty(&self) -> &Ty {
79        &self.ty
80    }
81
82    /// Whether this place corresponds to a local variable without any projections.
83    pub fn is_local(&self) -> bool {
84        self.as_local().is_some()
85    }
86
87    /// If this place corresponds to an unprojected local, return the variable id.
88    pub fn as_local(&self) -> Option<LocalId> {
89        self.kind.as_local().copied()
90    }
91
92    pub fn as_projection(&self) -> Option<(&Self, &ProjectionElem)> {
93        self.kind.as_projection().map(|(pl, pj)| (pl.as_ref(), pj))
94    }
95
96    #[deprecated(note = "use `local_id` instead")]
97    pub fn var_id(&self) -> Option<LocalId> {
98        self.local_id()
99    }
100    pub fn local_id(&self) -> Option<LocalId> {
101        match &self.kind {
102            PlaceKind::Local(var_id) => Some(*var_id),
103            PlaceKind::Projection(subplace, _) => subplace.local_id(),
104            PlaceKind::Global(_) => None,
105        }
106    }
107
108    pub fn project(self, elem: ProjectionElem, ty: Ty) -> Self {
109        Self {
110            kind: PlaceKind::Projection(Box::new(self), elem),
111            ty,
112        }
113    }
114
115    pub fn project_auto_ty(self, krate: &TranslatedCrate, proj: ProjectionElem) -> Option<Self> {
116        Some(Place {
117            ty: proj.project_type(krate, &self.ty)?,
118            kind: PlaceKind::Projection(Box::new(self), proj),
119        })
120    }
121
122    /// Dereferences the place. Panics if the type cannot be dereferenced.
123    pub fn deref(self) -> Place {
124        use TyKind::*;
125        let proj_ty = match self.ty.kind() {
126            Ref(_, ty, _) | RawPtr(ty, _) => ty.clone(),
127            Adt(tref) if tref.is_box() => tref.generics.types[0].clone(),
128            Adt(..) | TypeVar(_) | Scalar(_) | Never | TraitType(..) | DynTrait(..) | FnPtr(..)
129            | FnDef(..) | PtrMetadata(..) | Array(..) | Slice(..) | Pattern(..) | Error(..) => {
130                panic!("internal type error")
131            }
132        };
133        Place {
134            ty: proj_ty,
135            kind: PlaceKind::Projection(Box::new(self), ProjectionElem::Deref),
136        }
137    }
138
139    /// Iterate over the subplaces of this place, starting with the place itself.
140    pub fn subplaces(&self) -> impl Iterator<Item = &Self> {
141        std::iter::successors(Some(self), |place| Some(place.as_projection()?.0))
142    }
143
144    /// Whether `self` is the same place as, or a projection of, `parent`.
145    pub fn is_subplace(&self, parent: &Self) -> bool {
146        self.subplaces().any(|place| place == parent)
147    }
148
149    pub fn projections(&self) -> impl Iterator<Item = &ProjectionElem> {
150        self.subplaces()
151            .filter_map(|place| Some(place.as_projection()?.1))
152    }
153}
154
155impl ProjectionElem {
156    /// Compute the type obtained when applying the current projection to a place of type `ty`.
157    pub fn project_type(&self, krate: &TranslatedCrate, ty: &Ty) -> Option<Ty> {
158        use ProjectionElem::*;
159        Some(match self {
160            Deref => {
161                use TyKind::*;
162                match ty.kind() {
163                    Ref(_, ty, _) | RawPtr(ty, _) => ty.clone(),
164                    Adt(tref) if tref.is_box() => tref.generics.types[0].clone(),
165                    Adt(..) | TypeVar(_) | Scalar(_) | Never | TraitType(..) | DynTrait(..)
166                    | Array(..) | Slice(..) | FnPtr(..) | FnDef(..) | PtrMetadata(..)
167                    | Pattern(..) | Error(..) => {
168                        // Type error
169                        return None;
170                    }
171                }
172            }
173            Field(variant_id, field_id) => {
174                let tref = ty.as_adt().unwrap();
175                let type_decl = krate.type_decls.get(tref.id)?;
176                use TypeDeclKind::*;
177                match &type_decl.kind {
178                    Struct(fields) | Union(fields) => {
179                        if variant_id.is_some() {
180                            return None;
181                        };
182                        fields.get(*field_id)?.ty.clone().substitute(&tref.generics)
183                    }
184                    Enum(variants) => {
185                        let variant_id = (*variant_id)?;
186                        let variant = variants.get(variant_id)?;
187                        variant
188                            .fields
189                            .get(*field_id)?
190                            .ty
191                            .clone()
192                            .substitute(&tref.generics)
193                    }
194                    Opaque | Alias(_) | Error(_) => return None,
195                }
196            }
197            PtrMetadata => ty.get_ptr_metadata(krate).into_type(),
198            Index { .. } | Subslice { .. } => ty.as_array_or_slice()?.clone(),
199        })
200    }
201}
charon_lib/ast/bodies/places.rs

charon_lib/ast/bodies/
places.rs
