Skip to content

Commit

Permalink
Merge pull request #876 from Nadrieril/unsafe
Browse files Browse the repository at this point in the history 
Translate additional unsafe MIR operations
  • Loading branch information
@franziskuskiefer
franziskuskiefer authored Sep 5, 2024
2 parents 46ea40a + a5b1903 commit 5ac5c22
Show file tree
Hide file tree
Showing 4 changed files with 70 additions and 28 deletions.
5 changes: 3 additions & 2 deletions engine/lib/import_thir.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -806,8 +806,9 @@ end) : EXPR = struct
| Borrow arg ->
Borrow { arg = constant_expr_to_expr arg; borrow_kind = Thir.Shared }
| ConstRef { id } -> ConstRef { id }
| TraitConst _ | FnPtr _ ->
unimplemented [ span ] "constant_lit_to_lit: TraitConst | FnPtr"
| MutPtr _ | TraitConst _ | FnPtr _ ->
unimplemented [ span ]
"constant_lit_to_lit: TraitConst | FnPtr | MutPtr"
| Todo _ -> unimplemented [ span ] "ConstantExpr::Todo"
and constant_lit_to_lit (l : Thir.constant_literal) : Thir.lit_kind * bool =
match l with
Expand Down
64 changes: 44 additions & 20 deletions frontend/exporter/src/constant_utils.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,10 @@ pub enum ConstantExprKind {
impl_expr: ImplExpr,
name: String,
},
/// A shared reference to a static variable.
Borrow(ConstantExpr),
/// A `*mut` pointer to a static mutable variable.
MutPtr(ConstantExpr),
ConstRef {
id: ParamConst,
},
Expand Down Expand Up @@ -176,6 +179,10 @@ mod rustc {
borrow_kind: BorrowKind::Shared,
arg: e.into(),
},
MutPtr(e) => ExprKind::AddressOf {
mutability: true,
arg: e.into(),
},
ConstRef { id } => ExprKind::ConstRef { id },
Array { fields } => ExprKind::Array {
fields: fields.into_iter().map(|field| field.into()).collect(),
Expand Down Expand Up @@ -242,38 +249,53 @@ mod rustc {
let scalar_int = scalar.try_to_scalar_int().unwrap_or_else(|_| {
fatal!(
s[span],
"Type is primitive, but the scalar {:#?} is not a [Int]",
"Type is primitive, but the scalar {:#?} is not an [Int]",
scalar
)
});
ConstantExprKind::Literal(scalar_int_to_constant_literal(s, scalar_int, ty))
}
ty::Ref(region, ty, Mutability::Not) if region.is_erased() => {
ty::Ref(_, inner_ty, Mutability::Not) | ty::RawPtr(inner_ty, Mutability::Mut) => {
let tcx = s.base().tcx;
let pointer = scalar.to_pointer(&tcx).unwrap_or_else(|_| {
fatal!(
s[span],
"Type is [Ref], but the scalar {:#?} is not a [Pointer]",
"Type is [Ref] or [RawPtr], but the scalar {:#?} is not a [Pointer]",
scalar
)
});
use rustc_middle::mir::interpret::GlobalAlloc;
let contents = match tcx.global_alloc(pointer.provenance.s_unwrap(s).alloc_id()) {
GlobalAlloc::Static(did) => ConstantExprKind::GlobalName { id: did.sinto(s), generics: Vec::new(), trait_refs: Vec::new() },
GlobalAlloc::Memory(alloc) => {
let values = alloc.inner().get_bytes_unchecked(rustc_middle::mir::interpret::AllocRange {
start: rustc_abi::Size::from_bits(0),
size: rustc_abi::Size::from_bits(alloc.inner().len() * 8)
});
ConstantExprKind::Literal (ConstantLiteral::ByteStr(values.iter().copied().collect(), StrStyle::Cooked))
},
provenance => fatal!(
s[span],
"Expected provenance to be `GlobalAlloc::Static` or `GlobalAlloc::Memory`, got {:#?} instead",
provenance
)
};
ConstantExprKind::Borrow(contents.decorate(ty.sinto(s), cspan.clone()))
GlobalAlloc::Static(did) => ConstantExprKind::GlobalName {
id: did.sinto(s),
generics: Vec::new(),
trait_refs: Vec::new(),
},
GlobalAlloc::Memory(alloc) => {
let values = alloc.inner().get_bytes_unchecked(
rustc_middle::mir::interpret::AllocRange {
start: rustc_abi::Size::ZERO,
size: alloc.inner().size(),
},
);
ConstantExprKind::Literal(ConstantLiteral::ByteStr(
values.iter().copied().collect(),
StrStyle::Cooked,
))
}
provenance => fatal!(
s[span],
"Expected provenance to be `GlobalAlloc::Static` or \
`GlobalAlloc::Memory`, got {:#?} instead",
provenance
),
};
let contents = contents.decorate(inner_ty.sinto(s), cspan.clone());
match ty.kind() {
ty::Ref(..) => ConstantExprKind::Borrow(contents),
ty::RawPtr(..) => ConstantExprKind::MutPtr(contents),
_ => unreachable!(),
}
}
// A [Scalar] might also be any zero-sized [Adt] or [Tuple] (i.e., unit)
ty::Tuple(ty) if ty.is_empty() => ConstantExprKind::Tuple { fields: vec![] },
Expand All @@ -288,14 +310,16 @@ mod rustc {
} else {
fatal!(
s[span],
"Unexpected type `ty` for scalar `scalar`. Case `ty::Adt(def, _)`: `variant_def.fields` was not empty";
"Unexpected type `ty` for scalar `scalar`. Case `ty::Adt(def, _)`: \
`variant_def.fields` was not empty";
{ty, scalar, def, variant_def}
)
}
} else {
fatal!(
s[span],
"Unexpected type `ty` for scalar `scalar`. Case `ty::Adt(def, _)`: `def.variants().raw` was supposed to contain exactly one variant.";
"Unexpected type `ty` for scalar `scalar`. Case `ty::Adt(def, _)`: \
`def.variants().raw` was supposed to contain exactly one variant.";
{ty, scalar, def, &def.variants().raw}
)
}
Expand Down
25 changes: 21 additions & 4 deletions frontend/exporter/src/types/mir.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -639,6 +639,23 @@ pub enum StatementKind {
Nop,
}

#[derive_group(Serializers)]
#[derive(AdtInto, Clone, Debug, JsonSchema)]
#[args(<'tcx, S: UnderOwnerState<'tcx> + HasMir<'tcx>>, from: rustc_middle::mir::NonDivergingIntrinsic<'tcx>, state: S as s)]
pub enum NonDivergingIntrinsic {
Assume(Operand),
CopyNonOverlapping(CopyNonOverlapping),
}

#[derive_group(Serializers)]
#[derive(AdtInto, Clone, Debug, JsonSchema)]
#[args(<'tcx, S: UnderOwnerState<'tcx> + HasMir<'tcx>>, from: rustc_middle::mir::CopyNonOverlapping<'tcx>, state: S as s)]
pub struct CopyNonOverlapping {
pub src: Operand,
pub dst: Operand,
pub count: Operand,
}

#[derive_group(Serializers)]
#[derive(Clone, Debug, JsonSchema)]
pub struct Place {
Expand Down Expand Up @@ -713,7 +730,8 @@ impl<'tcx, S: UnderOwnerState<'tcx> + HasMir<'tcx>> SInto<S, Place>
ProjectionElem::Field(match cur_ty.kind() {
TyKind::Adt(adt_def, _) => {
assert!(
(adt_def.is_struct() && variant_idx.is_none())
((adt_def.is_struct() || adt_def.is_union())
&& variant_idx.is_none())
|| (adt_def.is_enum() && variant_idx.is_some())
);
ProjectionElemFieldKind::Adt {
Expand Down Expand Up @@ -744,10 +762,10 @@ impl<'tcx, S: UnderOwnerState<'tcx> + HasMir<'tcx>> SInto<S, Place>
match elem {
Deref => {
current_ty = match current_ty.kind() {
TyKind::Ref(_, ty, _) => ty.clone(),
TyKind::Ref(_, ty, _) | TyKind::RawPtr(ty, _) => ty.clone(),
TyKind::Adt(def, generics) if def.is_box() => generics.type_at(0),
_ => supposely_unreachable_fatal!(
s, "PlaceDerefNotRefNorBox";
s, "PlaceDerefNotRefNorPtrNorBox";
{current_ty, current_kind, elem}
),
};
Expand Down Expand Up @@ -985,7 +1003,6 @@ sinto_todo!(rustc_middle::mir, AssertMessage<'tcx>);
sinto_todo!(rustc_middle::mir, UnwindAction);
sinto_todo!(rustc_middle::mir, FakeReadCause);
sinto_todo!(rustc_middle::mir, RetagKind);
sinto_todo!(rustc_middle::mir, NonDivergingIntrinsic<'tcx>);
sinto_todo!(rustc_middle::mir, UserTypeProjection);
sinto_todo!(rustc_middle::mir, MirSource<'tcx>);
sinto_todo!(rustc_middle::mir, CoroutineInfo<'tcx>);
Expand Down
4 changes: 2 additions & 2 deletions test-harness/src/snapshots/toolchain__traits into-fstar.snap
View file
Original file line number Diff line number Diff line change
Expand Up @@ -329,11 +329,11 @@ let impl (#v_TypeArg: Type0) (v_ConstArg: usize) : t_Trait Prims.unit v_TypeArg
}

class t_SubTrait (v_Self: Type0) (v_TypeArg: Type0) (v_ConstArg: usize) = {
[@@@ FStar.Tactics.Typeclasses.no_method]_super_2645671271498264788:t_Trait v_Self
[@@@ FStar.Tactics.Typeclasses.no_method]_super_8779313392680198588:t_Trait v_Self
v_TypeArg
v_ConstArg;
f_AssocType:Type0;
f_AssocType_1171953828677564027:t_Trait f_AssocType v_TypeArg v_ConstArg
f_AssocType_17640019108099318278:t_Trait f_AssocType v_TypeArg v_ConstArg
}

let associated_function_caller
Expand Down

0 comments on commit 5ac5c22

Please sign in to comment.