Skip to content

Commit

Permalink
Store the type of each place
Browse files Browse the repository at this point in the history
  • Loading branch information
@Nadrieril
Nadrieril committed Nov 12, 2024
1 parent 61e7cbc commit 5c37521
Show file tree
Hide file tree
Showing 9 changed files with 111 additions and 140 deletions.
2 changes: 1 addition & 1 deletion charon-ml/src/Expressions.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ class ['self] map_rvalue_base =
method visit_field_id : 'env -> field_id -> field_id = fun _ x -> x
end

type place = { kind : place_kind }
type place = { kind : place_kind; ty : ty }

and place_kind =
| PlaceBase of var_id
Expand Down
5 changes: 3 additions & 2 deletions charon-ml/src/GAstOfJson.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,9 +44,10 @@ let rec ___ = ()
and place_of_json (js : json) : (place, string) result =
combine_error_msgs js __FUNCTION__
(match js with
| `Assoc [ ("kind", kind) ] ->
| `Assoc [ ("kind", kind); ("ty", ty) ] ->
let* kind = place_kind_of_json kind in
Ok ({ kind } : place)
let* ty = ty_of_json ty in
Ok ({ kind; ty } : place)
| _ -> Error "")

and place_kind_of_json (js : json) : (place_kind, string) result =
Expand Down
5 changes: 1 addition & 4 deletions charon/src/ast/expressions.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ use std::vec::Vec;
#[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize, Drive, DriveMut)]
pub struct Place {
pub kind: PlaceKind,
pub ty: Ty,
}

#[derive(
Expand Down Expand Up @@ -69,8 +70,6 @@ pub enum ProjectionElem {
Index {
offset: Box<Operand>,
from_end: bool,
// Type of the array/slice that we index into.
ty: Ty,
},
/// Take a subslice of a slice or array. If `from_end` is `true` this is
/// `slice[from..slice.len() - to]`, otherwise this is `slice[from..to]`.
Expand All @@ -80,8 +79,6 @@ pub enum ProjectionElem {
from: Box<Operand>,
to: Box<Operand>,
from_end: bool,
// Type of the array/slice that we index into.
ty: Ty,
},
}

Expand Down
34 changes: 9 additions & 25 deletions charon/src/ast/expressions_utils.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,12 +3,17 @@ use crate::ast::*;
use crate::ids::Vector;

impl Place {
pub fn new(var_id: VarId) -> Place {
pub fn new(var_id: VarId, ty: Ty) -> Place {
Place {
kind: PlaceKind::Base(var_id),
ty,
}
}

pub fn ty(&self) -> &Ty {
&self.ty
}

/// Whether this place corresponds to a local variable without any projections.
pub fn is_local(&self) -> bool {
self.as_local().is_some()
Expand All @@ -30,9 +35,10 @@ impl Place {
}
}

pub fn project(self, elem: ProjectionElem) -> Self {
pub fn project(self, elem: ProjectionElem, ty: Ty) -> Self {
Self {
kind: PlaceKind::Projection(Box::new(self), elem),
ty,
}
}
}
Expand All @@ -47,19 +53,6 @@ impl BorrowKind {
}
}

impl Place {
/// Compute the type of a place.
pub fn ty(&self, type_decls: &Vector<TypeDeclId, TypeDecl>, locals: &Locals) -> Result<Ty, ()> {
Ok(match &self.kind {
PlaceKind::Base(var_id) => locals.vars.get(*var_id).ok_or(())?.ty.clone(),
PlaceKind::Projection(sub_place, proj) => {
let sub_ty = sub_place.ty(type_decls, locals)?;
proj.project_type(type_decls, &sub_ty)?
}
})
}
}

impl ProjectionElem {
/// Compute the type obtained when applying the current projection to a place of type `ty`.
pub fn project_type(
Expand Down Expand Up @@ -130,16 +123,7 @@ impl ProjectionElem {
ClosureState => return Err(()),
}
}
Index { ty, .. } | Subslice { ty, .. } => {
let expected_ty = ty.as_array_or_slice().ok_or(())?;
let ty = ty.as_array_or_slice().ok_or(())?;
// Sanity check: ensure we're using the same types.
if expected_ty == ty {
ty.clone()
} else {
return Err(());
}
}
Index { .. } | Subslice { .. } => ty.as_array_or_slice().ok_or(())?.clone(),
})
}
}
11 changes: 8 additions & 3 deletions charon/src/ast/gast_utils.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -45,13 +45,18 @@ impl Body {
impl Locals {
/// Creates a new variable and returns a place pointing to it.
pub fn new_var(&mut self, name: Option<String>, ty: Ty) -> Place {
let var_id = self.vars.push_with(|index| Var { index, name, ty });
Place::new(var_id)
let var_id = self.vars.push_with(|index| Var {
index,
name,
ty: ty.clone(),
});
Place::new(var_id, ty)
}

/// Gets a place pointing to the corresponding variable.
pub fn place_for_var(&self, var_id: VarId) -> Place {
Place::new(var_id)
let ty = self.vars[var_id].ty.clone();
Place::new(var_id, ty)
}

/// The place where we write the return value.
Expand Down
2 changes: 1 addition & 1 deletion charon/src/bin/charon-driver/translate/translate_ctx.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -929,7 +929,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
self.t_ctx.def_span(def_id)
}

pub(crate) fn get_local(&self, local: &hax::Local) -> Option<VarId> {
pub(crate) fn translate_local(&self, local: &hax::Local) -> Option<VarId> {
use rustc_index::Idx;
self.vars_map.get(&local.index()).copied()
}
Expand Down
106 changes: 54 additions & 52 deletions charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -252,58 +252,50 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
Ok(())
}

/// Translate a place and return its type
fn translate_place_with_type(
&mut self,
span: Span,
place: &hax::Place,
) -> Result<(Place, Ty), Error> {
let ty = self.translate_ty(span, &place.ty)?;
let place = self.translate_place(span, place)?;
Ok((place, ty))
}

/// Translate a place
/// TODO: Hax represents places in a different manner than MIR. We should
/// update our representation of places to match the Hax representation.
fn translate_place(&mut self, span: Span, place: &hax::Place) -> Result<Place, Error> {
match &place.kind {
hax::PlaceKind::Local(local) => {
let var_id = self.get_local(local).unwrap();
Ok(Place::new(var_id))
let var_id = self.translate_local(local).unwrap();
Ok(self.locals.place_for_var(var_id))
}
hax::PlaceKind::Projection { place, kind } => {
hax::PlaceKind::Projection {
place: subplace,
kind,
} => {
let ty = self.translate_ty(span, &place.ty)?;
// Compute the type of the value *before* projection - we use this
// to disambiguate
let (place, current_ty) = self.translate_place_with_type(span, place)?;
let subplace = self.translate_place(span, subplace)?;
let place = match kind {
hax::ProjectionElem::Deref => {
// We use the type to disambiguate
match current_ty.kind() {
TyKind::Ref(_, _, _) | TyKind::RawPtr(_, _) => {
place.project(ProjectionElem::Deref)
}
match subplace.ty().kind() {
TyKind::Ref(_, _, _) | TyKind::RawPtr(_, _) => {}
TyKind::Adt(TypeId::Builtin(BuiltinTy::Box), generics) => {
// This case only happens in some MIR levels
assert!(!boxes_are_desugared(self.t_ctx.options.mir_level));
assert!(generics.regions.is_empty());
assert!(generics.types.len() == 1);
assert!(generics.const_generics.is_empty());
place.project(ProjectionElem::Deref)
}
_ => {
unreachable!(
"\n- place.kind: {:?}\n- current_ty: {:?}",
kind, current_ty
"\n- place.kind: {:?}\n- subplace.ty(): {:?}",
kind,
subplace.ty()
)
}
}
subplace.project(ProjectionElem::Deref, ty)
}
hax::ProjectionElem::Field(field_kind) => {
use hax::ProjectionElemFieldKind::*;
let proj_elem = match field_kind {
Tuple(id) => {
let (_, generics) = current_ty.kind().as_adt().unwrap();
let (_, generics) = subplace.ty().kind().as_adt().unwrap();
let field_id = translate_field_id(*id);
let proj_kind = FieldProjKind::Tuple(generics.types.len());
ProjectionElem::Field(proj_kind, field_id)
Expand All @@ -315,7 +307,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
} => {
let field_id = translate_field_id(*index);
let variant_id = variant.map(translate_variant_id);
match current_ty.kind() {
match subplace.ty().kind() {
TyKind::Adt(TypeId::Adt(type_id), ..) => {
let proj_kind = FieldProjKind::Adt(*type_id, variant_id);
ProjectionElem::Field(proj_kind, field_id)
Expand Down Expand Up @@ -350,44 +342,51 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
ProjectionElem::Field(FieldProjKind::ClosureState, field_id)
}
};
place.project(proj_elem)
subplace.project(proj_elem, ty)
}
hax::ProjectionElem::Index(local) => {
let local = self.get_local(local).unwrap();
let offset = Operand::Copy(Place::new(local));
place.project(ProjectionElem::Index {
offset: Box::new(offset),
from_end: false,
ty: current_ty,
})
let var_id = self.translate_local(local).unwrap();
let local = self.locals.place_for_var(var_id);
let offset = Operand::Copy(local);
subplace.project(
ProjectionElem::Index {
offset: Box::new(offset),
from_end: false,
},
ty,
)
}
hax::ProjectionElem::Downcast(..) => {
// We view it as a nop (the information from the
// downcast has been propagated to the other
// projection elements by Hax)
place
subplace
}
&hax::ProjectionElem::ConstantIndex {
offset,
from_end,
min_length: _,
} => {
let offset = Operand::Const(ScalarValue::Usize(offset).to_constant());
place.project(ProjectionElem::Index {
offset: Box::new(offset),
from_end,
ty: current_ty,
})
subplace.project(
ProjectionElem::Index {
offset: Box::new(offset),
from_end,
},
ty,
)
}
&hax::ProjectionElem::Subslice { from, to, from_end } => {
let from = Operand::Const(ScalarValue::Usize(from).to_constant());
let to = Operand::Const(ScalarValue::Usize(to).to_constant());
place.project(ProjectionElem::Subslice {
from: Box::new(from),
to: Box::new(to),
from_end,
ty: current_ty,
})
subplace.project(
ProjectionElem::Subslice {
from: Box::new(from),
to: Box::new(to),
from_end,
},
ty,
)
}
hax::ProjectionElem::OpaqueCast => {
// Don't know what that is
Expand All @@ -410,11 +409,13 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
trace!();
match operand {
hax::Operand::Copy(place) => {
let (p, ty) = self.translate_place_with_type(span, place)?;
let p = self.translate_place(span, place)?;
let ty = p.ty().clone();
Ok((Operand::Copy(p), ty))
}
hax::Operand::Move(place) => {
let (p, ty) = self.translate_place_with_type(span, place)?;
let p = self.translate_place(span, place)?;
let ty = p.ty().clone();
Ok((Operand::Move(p), ty))
}
hax::Operand::Constant(constant) => {
Expand Down Expand Up @@ -465,7 +466,8 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
Ok(Rvalue::RawPtr(place, mtbl))
}
hax::Rvalue::Len(place) => {
let (place, ty) = self.translate_place_with_type(span, place)?;
let place = self.translate_place(span, place)?;
let ty = place.ty().clone();
let cg = match ty.kind() {
TyKind::Adt(
TypeId::Builtin(aty @ (BuiltinTy::Array | BuiltinTy::Slice)),
Expand Down Expand Up @@ -595,16 +597,16 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
))
}
hax::Rvalue::Discriminant(place) => {
let (place, ty) = self.translate_place_with_type(span, place)?;
if let TyKind::Adt(TypeId::Adt(adt_id), _) = ty.kind() {
Ok(Rvalue::Discriminant(place, *adt_id))
let place = self.translate_place(span, place)?;
if let TyKind::Adt(TypeId::Adt(adt_id), _) = *place.ty().kind() {
Ok(Rvalue::Discriminant(place, adt_id))
} else {
error_or_panic!(
self,
span,
format!(
"Unexpected scrutinee type for ReadDiscriminant: {}",
ty.fmt_with_ctx(&self.into_fmt())
place.ty().fmt_with_ctx(&self.into_fmt())
)
)
}
Expand Down Expand Up @@ -885,7 +887,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
// We ignore StorageLive
StatementKind::StorageLive(_) => None,
StatementKind::StorageDead(local) => {
let var_id = self.get_local(local).unwrap();
let var_id = self.translate_local(local).unwrap();
Some(RawStatement::StorageDead(var_id))
}
StatementKind::Deinit(place) => {
Expand Down
Loading

0 comments on commit 5c37521

Please sign in to comment.