Skip to content

Commit

Permalink
Merge pull request #454 from Nadrieril/erase_regions
Browse files Browse the repository at this point in the history
  • Loading branch information
@Nadrieril
Nadrieril authored Nov 5, 2024
2 parents 2193aa0 + 693392c commit 2f3f5a0
Show file tree
Hide file tree
Showing 6 changed files with 99 additions and 188 deletions.
24 changes: 5 additions & 19 deletions charon/src/bin/charon-driver/translate/translate_constants.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
) -> Result<ConstantExpr, Error> {
use hax::ConstantExprKind;
let ty = &v.ty;
let erase_regions = true;
let value = match &(*v.contents) {
ConstantExprKind::Literal(lit) => {
self.translate_constant_literal_to_raw_constant_expr(lit)?
Expand Down Expand Up @@ -98,7 +97,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
RawConstantExpr::Adt(None, fields)
}
ConstantExprKind::TraitConst { impl_expr, name } => {
let trait_ref = self.translate_trait_impl_expr(span, erase_regions, impl_expr)?;
let trait_ref = self.translate_trait_impl_expr(span, impl_expr)?;
let name = TraitItemName(name.clone());
RawConstantExpr::TraitConst(trait_ref, name)
}
Expand All @@ -113,15 +112,9 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
generics,
trait_refs
);
let erase_regions = true;
let used_params = None;
let generics = self.translate_substs_and_trait_refs(
span,
erase_regions,
used_params,
generics,
trait_refs,
)?;
let generics =
self.translate_substs_and_trait_refs(span, used_params, generics, trait_refs)?;

let global_id = self.register_global_decl_id(span, id);
RawConstantExpr::Global(GlobalDeclRef {
Expand Down Expand Up @@ -178,15 +171,8 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
method_impl: trait_info,
} => {
use super::translate_functions_to_ullbc::SubstFunIdOrPanic;
let erase_regions = true; // TODO: not sure
let fn_id = self.translate_fun_decl_id_with_args(
span,
erase_regions,
fn_id,
substs,
None,
trait_refs,
trait_info,
span, fn_id, substs, None, trait_refs, trait_info,
)?;
let SubstFunIdOrPanic::Fun(fn_id) = fn_id else {
unreachable!()
Expand All @@ -199,7 +185,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
}
};

let ty = self.translate_ty(span, erase_regions, ty)?;
let ty = self.translate_ty(span, ty)?;
Ok(ConstantExpr { value, ty })
}

Expand Down
4 changes: 1 addition & 3 deletions charon/src/bin/charon-driver/translate/translate_ctx.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -343,14 +343,12 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
let impl_elem = match full_def.kind() {
// Inherent impl ("regular" impl)
hax::FullDefKind::InherentImpl { ty, .. } => {
let erase_regions = false;

// We need to convert the type, which may contain quantified
// substs and bounds. In order to properly do so, we introduce
// a body translation context.
let mut bt_ctx = BodyTransCtx::new(def_id, None, self);
let generics = bt_ctx.translate_def_generics(span, &full_def)?;
let ty = bt_ctx.translate_ty(span, erase_regions, &ty)?;
let ty = bt_ctx.translate_ty(span, &ty)?;
ImplElem::Ty(generics, ty)
}
// Trait implementation
Expand Down
55 changes: 17 additions & 38 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 @@ -171,9 +171,8 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
let name: Option<String> = var.name.clone();

// Translate the type
let erase_regions = true;
let span = self.translate_span_from_hax(&var.source_info.span);
let ty = self.translate_ty(span, erase_regions, &var.ty)?;
let ty = self.translate_ty(span, &var.ty)?;

// Add the variable to the environment
self.push_var(index, ty, name);
Expand Down Expand Up @@ -259,8 +258,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
span: Span,
place: &hax::Place,
) -> Result<(Place, Ty), Error> {
let erase_regions = true;
let ty = self.translate_ty(span, erase_regions, &place.ty)?;
let ty = self.translate_ty(span, &place.ty)?;
let (var_id, projection) = self.translate_projection(span, place)?;
Ok((Place { var_id, projection }, ty))
}
Expand All @@ -278,7 +276,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
span: Span,
place: &hax::Place,
) -> Result<(VarId, Projection), Error> {
let erase_regions = true;
match &place.kind {
hax::PlaceKind::Local(local) => {
let var_id = self.get_local(local).unwrap();
Expand All @@ -288,7 +285,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
let (var_id, mut projection) = self.translate_projection(span, place)?;
// Compute the type of the value *before* projection - we use this
// to disambiguate
let current_ty = self.translate_ty(span, erase_regions, &place.ty)?;
let current_ty = self.translate_ty(span, &place.ty)?;
match kind {
hax::ProjectionElem::Deref => {
// We use the type to disambiguate
Expand Down Expand Up @@ -445,7 +442,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {

/// Translate an rvalue
fn translate_rvalue(&mut self, span: Span, rvalue: &hax::Rvalue) -> Result<Rvalue, Error> {
let erase_regions = true;
match rvalue {
hax::Rvalue::Use(operand) => Ok(Rvalue::Use(self.translate_operand(span, operand)?)),
hax::Rvalue::CopyForDeref(place) => {
Expand Down Expand Up @@ -497,7 +493,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
hax::Rvalue::Cast(cast_kind, operand, tgt_ty) => {
trace!("Rvalue::Cast: {:?}", rvalue);
// Translate the target type
let tgt_ty = self.translate_ty(span, erase_regions, tgt_ty)?;
let tgt_ty = self.translate_ty(span, tgt_ty)?;

// Translate the operand
let (operand, src_ty) = self.translate_operand_with_type(span, operand)?;
Expand Down Expand Up @@ -579,7 +575,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
)),
hax::Rvalue::NullaryOp(nullop, ty) => {
trace!("NullOp: {:?}", nullop);
let ty = self.translate_ty(span, erase_regions, ty)?;
let ty = self.translate_ty(span, ty)?;
let op = match nullop {
hax::NullOp::SizeOf => NullOp::SizeOf,
hax::NullOp::AlignOf => NullOp::AlignOf,
Expand Down Expand Up @@ -645,7 +641,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {

match aggregate_kind {
hax::AggregateKind::Array(ty) => {
let t_ty = self.translate_ty(span, erase_regions, ty)?;
let t_ty = self.translate_ty(span, ty)?;
let cg = ConstGeneric::Value(Literal::Scalar(ScalarValue::Usize(
operands_t.len() as u64,
)));
Expand Down Expand Up @@ -674,13 +670,8 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
let _ = user_annotation;

// Translate the substitution
let generics = self.translate_substs_and_trait_refs(
span,
erase_regions,
None,
substs,
trait_refs,
)?;
let generics =
self.translate_substs_and_trait_refs(span, None, substs, trait_refs)?;

let type_id = self.translate_type_id(span, adt_id)?;
// Sanity check
Expand All @@ -703,13 +694,8 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
trace!("Closure:\n\n- def_id: {:?}\n\n- sig:\n{:?}", def_id, sig);

// Translate the substitution
let generics = self.translate_substs_and_trait_refs(
span,
erase_regions,
None,
substs,
trait_refs,
)?;
let generics =
self.translate_substs_and_trait_refs(span, None, substs, trait_refs)?;

let def_id = self.register_fun_decl_id(span, def_id);
let akind = AggregateKind::Closure(def_id, generics);
Expand All @@ -728,7 +714,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
}
hax::Rvalue::ShallowInitBox(op, ty) => {
let op = self.translate_operand(span, op)?;
let ty = self.translate_ty(span, erase_regions, ty)?;
let ty = self.translate_ty(span, ty)?;
Ok(Rvalue::ShallowInitBox(op, ty))
}
}
Expand Down Expand Up @@ -768,7 +754,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
pub(crate) fn translate_fun_decl_id_with_args(
&mut self,
span: Span,
erase_regions: bool,
def_id: &hax::DefId,
substs: &Vec<hax::GenericArg>,
args: Option<&Vec<hax::Spanned<hax::Operand>>>,
Expand All @@ -783,8 +768,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
}

// Translate the type parameters
let generics =
self.translate_substs_and_trait_refs(span, erase_regions, None, substs, trait_refs)?;
let generics = self.translate_substs_and_trait_refs(span, None, substs, trait_refs)?;

// Translate the arguments
let args = args
Expand Down Expand Up @@ -854,8 +838,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
None => FunIdOrTraitMethodRef::Fun(FunId::Regular(fun_id)),
// Trait method
Some(trait_info) => {
let impl_expr =
self.translate_trait_impl_expr(span, erase_regions, trait_info)?;
let impl_expr = self.translate_trait_impl_expr(span, trait_info)?;
let method_name = self.t_ctx.translate_trait_item_name(def_id)?;
FunIdOrTraitMethodRef::Trait(impl_expr, method_name, fun_id)
}
Expand Down Expand Up @@ -1147,10 +1130,8 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
trace!("func: {:?}", def_id);

// Translate the function id, with its parameters
let erase_regions = true;
let fid = self.translate_fun_decl_id_with_args(
span,
erase_regions,
def_id,
generics,
Some(args),
Expand Down Expand Up @@ -1355,7 +1336,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
item_meta: &ItemMeta,
def: &hax::FullDef,
) -> Result<FunSig, Error> {
let erase_regions = false;
let span = item_meta.span;

let generics = self.translate_def_generics(span, def)?;
Expand All @@ -1380,9 +1360,9 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
.value
.inputs
.iter()
.map(|ty| self.translate_ty(span, erase_regions, ty))
.map(|ty| self.translate_ty(span, ty))
.try_collect()?;
let output = self.translate_ty(span, erase_regions, &signature.value.output)?;
let output = self.translate_ty(span, &signature.value.output)?;

let fmt_ctx = self.into_fmt();
trace!(
Expand All @@ -1409,7 +1389,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
let state: Vector<TypeVarId, Ty> = args
.upvar_tys
.iter()
.map(|ty| self.translate_ty(span, erase_regions, &ty))
.map(|ty| self.translate_ty(span, &ty))
.try_collect()?;
Some(ClosureInfo { kind, state })
}
Expand Down Expand Up @@ -1535,8 +1515,7 @@ impl BodyTransCtx<'_, '_, '_> {
| hax::FullDefKind::Static { ty, .. } => ty,
_ => panic!("Unexpected def for constant: {def:?}"),
};
let erase_regions = false; // This doesn't matter: there shouldn't be any regions
let ty = self.translate_ty(span, erase_regions, ty)?;
let ty = self.translate_ty(span, ty)?;

// Translate its body like the body of a function. This returns `Opaque if we can't/decide
// not to translate this body.
Expand Down
Loading

0 comments on commit 2f3f5a0

Please sign in to comment.