diff --git a/charon-ml/src/Expressions.ml b/charon-ml/src/Expressions.ml index 5d8b3480..e6e4825a 100644 --- a/charon-ml/src/Expressions.ml +++ b/charon-ml/src/Expressions.ml @@ -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 diff --git a/charon-ml/src/GAstOfJson.ml b/charon-ml/src/GAstOfJson.ml index c8e8e446..90f183a5 100644 --- a/charon-ml/src/GAstOfJson.ml +++ b/charon-ml/src/GAstOfJson.ml @@ -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 = diff --git a/charon/src/ast/expressions.rs b/charon/src/ast/expressions.rs index d5823c98..737d855c 100644 --- a/charon/src/ast/expressions.rs +++ b/charon/src/ast/expressions.rs @@ -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( @@ -69,8 +70,6 @@ pub enum ProjectionElem { Index { offset: Box, 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]`. @@ -80,8 +79,6 @@ pub enum ProjectionElem { from: Box, to: Box, from_end: bool, - // Type of the array/slice that we index into. - ty: Ty, }, } diff --git a/charon/src/ast/expressions_utils.rs b/charon/src/ast/expressions_utils.rs index f5b9f7f4..0161c64a 100644 --- a/charon/src/ast/expressions_utils.rs +++ b/charon/src/ast/expressions_utils.rs @@ -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() @@ -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, } } } @@ -47,19 +53,6 @@ impl BorrowKind { } } -impl Place { - /// Compute the type of a place. - pub fn ty(&self, type_decls: &Vector, locals: &Locals) -> Result { - 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( @@ -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(), }) } } diff --git a/charon/src/ast/gast_utils.rs b/charon/src/ast/gast_utils.rs index 15eb2d4e..abbca24b 100644 --- a/charon/src/ast/gast_utils.rs +++ b/charon/src/ast/gast_utils.rs @@ -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, 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. diff --git a/charon/src/bin/charon-driver/translate/translate_ctx.rs b/charon/src/bin/charon-driver/translate/translate_ctx.rs index d646c058..40009794 100644 --- a/charon/src/bin/charon-driver/translate/translate_ctx.rs +++ b/charon/src/bin/charon-driver/translate/translate_ctx.rs @@ -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 { + pub(crate) fn translate_local(&self, local: &hax::Local) -> Option { use rustc_index::Idx; self.vars_map.get(&local.index()).copied() } diff --git a/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs b/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs index e73c167c..dd701e81 100644 --- a/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs +++ b/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs @@ -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 { 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) @@ -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) @@ -350,22 +342,25 @@ 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, @@ -373,21 +368,25 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { 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 @@ -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) => { @@ -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)), @@ -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()) ) ) } @@ -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) => { diff --git a/charon/src/transform/index_intermediate_assigns.rs b/charon/src/transform/index_intermediate_assigns.rs index 48548427..04917a45 100644 --- a/charon/src/transform/index_intermediate_assigns.rs +++ b/charon/src/transform/index_intermediate_assigns.rs @@ -74,46 +74,26 @@ impl Rvalue { } } -fn introduce_intermediate_let_binding( - ctx: &mut TransformCtx<'_>, - span: Span, - locals: &mut Locals, - lhs: &mut Place, - rhs: &mut Rvalue, -) -> Vec { - // Compute the type of the lhs - let Ok(lhs_ty) = lhs.ty(&ctx.translated.type_decls, locals) else { - use crate::pretty::fmt_with_ctx::FmtWithCtx; - use crate::pretty::formatter::IntoFormatter; - let msg = format!( - "Could not compute the type of place: {}", - lhs.fmt_with_ctx(&ctx.into_fmt()) - ); - crate::register_error_or_panic!(ctx, span, msg); - return vec![]; - }; - - // Introduce a fresh local variable, for the temporary assignment - let tmp_var = locals.new_var(None, lhs_ty); - - // Update the rhs - let tmp_rhs = std::mem::replace(rhs, Rvalue::Use(Operand::Move(tmp_var.clone()))); - - // Introduce the intermediate let-binding - vec![Statement::new(span, RawStatement::Assign(tmp_var, tmp_rhs))] -} - pub struct Transform; impl LlbcPass for Transform { - fn transform_body(&self, ctx: &mut TransformCtx<'_>, b: &mut ExprBody) { + fn transform_body(&self, _ctx: &mut TransformCtx<'_>, b: &mut ExprBody) { b.body.transform(&mut |st: &mut Statement| { match &mut st.content { RawStatement::Assign(lhs, rhs) if lhs.contains_index() && rhs.contains_index() => { // Introduce an intermediate statement if both the rhs and the lhs contain an // "index" projection element (this way we avoid introducing too many // intermediate assignments). - introduce_intermediate_let_binding(ctx, st.span, &mut b.locals, lhs, rhs) + + // Fresh local variable for the temporary assignment + let tmp_var = b.locals.new_var(None, lhs.ty().clone()); + let tmp_rhs = + std::mem::replace(rhs, Rvalue::Use(Operand::Move(tmp_var.clone()))); + // Introduce the intermediate let-binding + vec![Statement::new( + st.span, + RawStatement::Assign(tmp_var, tmp_rhs), + )] } _ => vec![], } diff --git a/charon/src/transform/index_to_function_calls.rs b/charon/src/transform/index_to_function_calls.rs index be3bf3e3..2220c1be 100644 --- a/charon/src/transform/index_to_function_calls.rs +++ b/charon/src/transform/index_to_function_calls.rs @@ -35,12 +35,10 @@ impl<'a> Visitor<'a> { fn transform_place(&mut self, mut_access: bool, place: &mut Place) { use ProjectionElem::*; - let PlaceKind::Projection(subplace, pe @ (Index { ty, .. } | Subslice { ty, .. })) = - &place.kind - else { + let Some((subplace, pe @ (Index { .. } | Subslice { .. }))) = place.as_projection() else { return; }; - let TyKind::Adt(TypeId::Builtin(builtin_ty), generics) = ty.kind() else { + let TyKind::Adt(TypeId::Builtin(builtin_ty), generics) = subplace.ty().kind() else { unreachable!() }; @@ -62,23 +60,27 @@ impl<'a> Visitor<'a> { }) }; - let input_ty = - TyKind::Ref(Region::Erased, ty.clone(), RefKind::mutable(mut_access)).into_ty(); + let input_ty = TyKind::Ref( + Region::Erased, + subplace.ty().clone(), + RefKind::mutable(mut_access), + ) + .into_ty(); + let elem_ty = generics.types[0].clone(); + let output_inner_ty = if matches!(pe, Index { .. }) { + elem_ty + } else { + TyKind::Adt( + TypeId::Builtin(BuiltinTy::Slice), + GenericArgs::new_from_types(vec![elem_ty].into()), + ) + .into_ty() + }; let output_ty = { - let elem_ty = generics.types[0].clone(); - let output_inner_ty = if matches!(pe, Index { .. }) { - elem_ty - } else { - TyKind::Adt( - TypeId::Builtin(BuiltinTy::Slice), - GenericArgs::new_from_types(vec![elem_ty].into()), - ) - .into_ty() - }; TyKind::Ref( Region::Erased, - output_inner_ty, + output_inner_ty.clone(), RefKind::mutable(mut_access), ) .into_ty() @@ -90,7 +92,7 @@ impl<'a> Visitor<'a> { let input_var = self.fresh_var(None, input_ty); let kind = RawStatement::Assign( input_var.clone(), - Rvalue::Ref(subplace.as_ref().clone(), BorrowKind::mutable(mut_access)), + Rvalue::Ref(subplace.clone(), BorrowKind::mutable(mut_access)), ); self.statements.push(Statement::new(self.span, kind)); input_var @@ -118,8 +120,8 @@ impl<'a> Visitor<'a> { let kind = RawStatement::Assign( len_var.clone(), Rvalue::Len( - subplace.as_ref().clone(), - ty.clone(), + subplace.clone(), + subplace.ty().clone(), generics.const_generics.get(0.into()).cloned(), ), ); @@ -151,7 +153,7 @@ impl<'a> Visitor<'a> { }; // Update the place. - *place = output_var.project(ProjectionElem::Deref); + *place = output_var.project(ProjectionElem::Deref, output_inner_ty); } }