Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Rust 1.82.0 #1330

Draft
wants to merge 5 commits into
base: main
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion rust-toolchain.toml
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
[toolchain]
channel = "1.79.0"
channel = "1.82.0"
# channel = "nightly-2023-09-29" # TODO update to match 1.79.0 (not officially supported)
components = [ "rustc", "rust-std", "cargo", "rustfmt", "rustc-dev", "llvm-tools" ]
2 changes: 1 addition & 1 deletion source/builtin_macros/src/syntax.rs
Original file line number Diff line number Diff line change
Expand Up @@ -661,7 +661,7 @@ impl Visitor {
self.inside_ghost += 1;
self.visit_expr_mut(&mut expr);
self.inside_ghost -= 1;
stmts.push(Stmt::Expr(Expr::Verbatim(quote_spanned!(con_span => #[verus::internal(verus_macro)] #[verus::internal(const_body)] fn __VERUS_CONST_BODY__() -> #con_ty { #expr } ))));
stmts.push(Stmt::Expr(Expr::Verbatim(quote_spanned!(con_span => #[allow(non_snake_case)]#[verus::internal(verus_macro)] #[verus::internal(const_body)] fn __VERUS_CONST_BODY__() -> #con_ty { #expr } ))));
stmts.push(Stmt::Expr(Expr::Verbatim(
quote_spanned!(con_span => unsafe { core::mem::zeroed() }),
)));
Expand Down
3 changes: 2 additions & 1 deletion source/rust_verify/src/expand_errors_driver.rs
Original file line number Diff line number Diff line change
Expand Up @@ -550,7 +550,8 @@ impl ExpandErrorsDriver {
let s = if matches!(
error_format,
Some(rustc_session::config::ErrorOutputType::HumanReadable(
rustc_errors::emitter::HumanReadableErrorType::Short(_)
rustc_errors::emitter::HumanReadableErrorType::Short,
_
))
) {
"diagnostics via expansion".into()
Expand Down
4 changes: 2 additions & 2 deletions source/rust_verify/src/fn_call_to_vir.rs
Original file line number Diff line number Diff line change
Expand Up @@ -196,9 +196,9 @@ pub(crate) fn fn_call_to_vir<'tcx>(
let mut target_kind = vir::ast::CallTargetKind::Dynamic;
let param_env = tcx.param_env(bctx.fun_id);
let normalized_substs = tcx.normalize_erasing_regions(param_env, node_substs);
let inst = rustc_middle::ty::Instance::resolve(tcx, param_env, f, normalized_substs);
let inst = rustc_middle::ty::Instance::try_resolve(tcx, param_env, f, normalized_substs);
if let Ok(Some(inst)) = inst {
if let rustc_middle::ty::InstanceDef::Item(did) = inst.def {
if let rustc_middle::ty::InstanceKind::Item(did) = inst.def {
let typs = mk_typ_args(bctx, &inst.args, did, expr.span)?;
let mut f =
Arc::new(FunX { path: def_id_to_vir_path(tcx, &bctx.ctxt.verus_items, did) });
Expand Down
2 changes: 2 additions & 0 deletions source/rust_verify/src/lifetime.rs
Original file line number Diff line number Diff line change
Expand Up @@ -204,6 +204,8 @@ pub(crate) fn check<'tcx>(queries: &'tcx rustc_interface::Queries<'tcx>) {
}

const PRELUDE: &str = "\
#![feature(negative_impls)]
#![feature(with_negative_coherence)]
#![feature(box_patterns)]
#![feature(ptr_metadata)]
#![feature(never_type)]
Expand Down
1 change: 1 addition & 0 deletions source/rust_verify/src/lifetime_ast.rs
Original file line number Diff line number Diff line change
Expand Up @@ -181,6 +181,7 @@ pub(crate) struct TraitImpl {
pub(crate) generic_bounds: Vec<GenericBound>,
// use Datatype(Id, Vec<Typ>) to represent (trait_path, trait_typ_args)
pub(crate) trait_as_datatype: Typ,
pub(crate) trait_polarity: rustc_middle::ty::ImplPolarity,
pub(crate) assoc_typs: Vec<(Id, Vec<GenericParam>, Typ)>,
}

Expand Down
14 changes: 12 additions & 2 deletions source/rust_verify/src/lifetime_emit.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1068,14 +1068,24 @@ pub(crate) fn emit_datatype_decl(state: &mut EmitState, d: &DatatypeDecl) {
}

pub(crate) fn emit_trait_impl(state: &mut EmitState, t: &TraitImpl) {
let TraitImpl { span, trait_as_datatype, self_typ, generic_params, generic_bounds, assoc_typs } =
t;
let TraitImpl {
span,
trait_as_datatype,
self_typ,
generic_params,
generic_bounds,
assoc_typs,
trait_polarity,
} = t;
state.newdecl();
state.newline();
state.begin_span_opt(*span);
state.write("impl");
emit_generic_params(state, &generic_params);
state.write(" ");
if trait_polarity == &rustc_middle::ty::ImplPolarity::Negative {
state.write("!");
}
state.write(&trait_as_datatype.to_string());
state.write(" for ");
state.write(&self_typ.to_string());
Expand Down
89 changes: 60 additions & 29 deletions source/rust_verify/src/lifetime_generate.rs
Original file line number Diff line number Diff line change
Expand Up @@ -10,12 +10,12 @@ use rustc_hir::def::{CtorKind, DefKind, Res};
use rustc_hir::{
AssocItemKind, Block, BlockCheckMode, BodyId, Closure, Crate, Expr, ExprKind, FnSig, HirId,
Impl, ImplItem, ImplItemKind, ItemKind, LetExpr, LetStmt, MaybeOwner, Node, OpaqueTy,
OpaqueTyOrigin, OwnerNode, Pat, PatKind, Stmt, StmtKind, TraitFn, TraitItem, TraitItemKind,
TraitItemRef, UnOp, Unsafety,
OpaqueTyOrigin, OwnerNode, Pat, PatKind, Safety, Stmt, StmtKind, TraitFn, TraitItem,
TraitItemKind, TraitItemRef, UnOp,
};
use rustc_middle::ty::{
AdtDef, BoundRegionKind, BoundVariableKind, ClauseKind, Const, GenericArgKind,
GenericParamDefKind, RegionKind, Ty, TyCtxt, TyKind, TypeckResults, VariantDef,
GenericParamDefKind, RegionKind, TermKind, Ty, TyCtxt, TyKind, TypeckResults, VariantDef,
};
use rustc_span::def_id::DefId;
use rustc_span::symbol::kw;
Expand Down Expand Up @@ -341,8 +341,8 @@ fn add_copy_type(ctxt: &mut Context, state: &mut State, id: DefId) {
let did = adt_def_data.did;
let generics = tcx.generics_of(id);
let mut copy_bounds: Vec<(Id, bool)> = Vec::new();
if generics.params.len() == args.len() {
for (param, arg) in generics.params.iter().zip(args.iter()) {
if generics.own_params.len() == args.len() {
for (param, arg) in generics.own_params.iter().zip(args.iter()) {
let name = state.typ_param(param.name.to_string(), Some(param.index));
copy_bounds.push((name, false));
if let GenericArgKind::Type(arg_ty) = arg.unpack() {
Expand Down Expand Up @@ -555,7 +555,7 @@ fn erase_ty<'tcx>(ctxt: &Context<'tcx>, state: &mut State, ty: &Ty<'tcx>) -> Typ
};
Box::new(TypX::Datatype(datatype_name, Vec::new(), typ_args))
}
TyKind::Alias(rustc_middle::ty::AliasKind::Projection, t) => {
TyKind::Alias(rustc_middle::ty::AliasTyKind::Projection, t) => {
// Note: even if rust_to_vir_base decides to normalize t,
// we don't have to normalize t here, since we're generating Rust code, not VIR.
// However, normalizing means we might reach less stuff so it's
Expand Down Expand Up @@ -596,7 +596,7 @@ fn erase_ty<'tcx>(ctxt: &Context<'tcx>, state: &mut State, ty: &Ty<'tcx>) -> Typ
let projection_generics = ctxt.tcx.generics_of(t.def_id);
let trait_def = projection_generics.parent;
if let Some(trait_def) = trait_def {
let n = t.args.len() - projection_generics.params.len();
let n = t.args.len() - projection_generics.own_params.len();
let (trait_typ_args, self_typ) =
erase_generic_args(ctxt, state, &t.args[..n], true);
let (assoc_typ_args, _) = erase_generic_args(ctxt, state, &t.args[n..], false);
Expand Down Expand Up @@ -987,14 +987,14 @@ fn erase_call<'tcx>(
);

let normalized_substs = ctxt.tcx.normalize_erasing_regions(param_env, node_substs);
let inst = rustc_middle::ty::Instance::resolve(
let inst = rustc_middle::ty::Instance::try_resolve(
ctxt.tcx,
param_env,
fn_def_id,
normalized_substs,
);
if let Ok(Some(inst)) = inst {
if let rustc_middle::ty::InstanceDef::Item(did) = inst.def {
if let rustc_middle::ty::InstanceKind::Item(did) = inst.def {
node_substs = &inst.args;
fn_def_id = did;
}
Expand Down Expand Up @@ -1272,7 +1272,10 @@ fn erase_expr<'tcx>(
return mk_exp(ExpX::Call(fun_exp, vec![], vec![]));
}
}
Res::Def(DefKind::Static { mutability: Mutability::Not, nested: false }, id) => {
Res::Def(
DefKind::Static { mutability: Mutability::Not, nested: false, .. },
id,
) => {
if expect_spec || ctxt.var_modes[&expr.hir_id] == Mode::Spec {
None
} else {
Expand Down Expand Up @@ -1875,35 +1878,39 @@ fn erase_mir_predicates<'a, 'tcx>(
}
}
ClauseKind::Projection(pred) => {
if Some(pred.projection_ty.def_id) == tcx.lang_items().fn_once_output() {
assert!(pred.projection_ty.args.len() == 2);
let typ = erase_ty(ctxt, state, &pred.projection_ty.args[0].expect_ty());
let mut fn_params = match pred.projection_ty.args[1].unpack() {
if Some(pred.projection_term.def_id) == tcx.lang_items().fn_once_output() {
assert!(pred.projection_term.args.len() == 2);
let typ = erase_ty(ctxt, state, &pred.projection_term.args[0].expect_ty());
let mut fn_params = match pred.projection_term.args[1].unpack() {
GenericArgKind::Type(ty) => erase_ty(ctxt, state, &ty),
_ => panic!("unexpected fn projection"),
};
if !matches!(*fn_params, TypX::Tuple(_)) {
fn_params = Box::new(TypX::Tuple(vec![fn_params]));
}
let fn_ret = erase_ty(ctxt, state, &pred.term.ty().expect("fn_ret"));
let fn_ret = if let TermKind::Ty(ty) = pred.term.unpack() {
erase_ty(ctxt, state, &ty)
} else {
panic!("fn_ret");
};
fn_projections.insert(typ, (fn_params, fn_ret)).map(|_| panic!("{:?}", pred));
} else {
let typ0 = erase_ty(ctxt, state, &pred.projection_ty.args[0].expect_ty());
let typ_eq = if let Some(ty) = pred.term.ty() {
let typ0 = erase_ty(ctxt, state, &pred.projection_term.args[0].expect_ty());
let typ_eq = if let TermKind::Ty(ty) = pred.term.unpack() {
erase_ty(ctxt, state, &ty)
} else {
panic!("should have been disallowed by rust_verify_base.rs");
};
let trait_def_id = pred.projection_ty.trait_def_id(tcx);
let item_def_id = pred.projection_ty.def_id;
let trait_def_id = pred.projection_term.trait_def_id(tcx);
let item_def_id = pred.projection_term.def_id;
let assoc_item = tcx.associated_item(item_def_id);
let projection_generics = ctxt.tcx.generics_of(item_def_id);
let n = pred.projection_ty.args.len() - projection_generics.params.len();
let n = pred.projection_term.args.len() - projection_generics.own_params.len();
let mut bound =
erase_mir_bound(ctxt, state, trait_def_id, &pred.projection_ty.args[..n])
erase_mir_bound(ctxt, state, trait_def_id, &pred.projection_term.args[..n])
.expect("bound");
let (x_args, _) =
erase_generic_args(ctxt, state, &pred.projection_ty.args[n..], true);
erase_generic_args(ctxt, state, &pred.projection_term.args[n..], true);
let x_args = x_args.into_iter().map(|a| a.as_lifetime()).collect();
if let Bound::Trait { trait_path: _, args: _, equality } = &mut bound {
assert!(equality.is_none());
Expand Down Expand Up @@ -1956,7 +1963,7 @@ fn erase_mir_generics<'tcx>(
}
}
}
for gparam in &mir_generics.params {
for gparam in &mir_generics.own_params {
match gparam.kind {
GenericParamDefKind::Lifetime => {
let name = state.lifetime((gparam.name.to_string(), None));
Expand All @@ -1966,7 +1973,7 @@ fn erase_mir_generics<'tcx>(
let name = state.typ_param(gparam.name.to_string(), Some(gparam.index));
typ_params.push(GenericParam { name, const_typ: None });
}
GenericParamDefKind::Const { has_default: _, is_host_effect: false } => {
GenericParamDefKind::Const { has_default: _, is_host_effect: false, .. } => {
let name = state.typ_param(gparam.name.to_string(), None);
let t = erase_ty(ctxt, state, &ctxt.tcx.type_of(gparam.def_id).skip_binder());
typ_params.push(GenericParam { name, const_typ: Some(t) });
Expand Down Expand Up @@ -2242,14 +2249,39 @@ fn erase_impl_assocs<'tcx>(ctxt: &Context<'tcx>, state: &mut State, impl_id: Def
}
}

let trait_polarity = ctxt.tcx.impl_polarity(impl_id);
let trait_impl = TraitImpl {
span: Some(span),
generic_params,
generic_bounds,
self_typ,
self_typ: self_typ.clone(),
trait_polarity,
trait_as_datatype,
assoc_typs,
};

// v1.80 stablized Iterator and IntoIterator for Box.
// It needs to implement !Iterartor to avoid conflicts.
// The lifetime checking does not reserve polarity.
/*if matches!(name.raw_id.as_str(), "Iterator" | "IntoIterator") {
let skip = match self_typ.as_ref() {
// found both positive and negative implementation of trait `T55_Iterator` for type `&mut std::boxed::Box<[_], _>
TypX::Ref(r, ..) => {
if let TypX::Datatype(sid, ..) = r.as_ref() {
sid.raw_id == "Box"
} else {
false
}
}
TypX::Datatype(sid, ..) if sid.raw_id == "Box" => true,
_ => false,
};
if skip {
println!("skip = {:?} {:?} {:?}", self_typ, trait_polarity, name);
return;
}
}*/

state.trait_impls.push(trait_impl);
}

Expand Down Expand Up @@ -2570,7 +2602,7 @@ fn erase_variant_data<'tcx>(
fn erase_abstract_datatype<'tcx>(ctxt: &Context<'tcx>, state: &mut State, span: Span, id: DefId) {
let mut fields: Vec<Typ> = Vec::new();
let mir_generics = ctxt.tcx.generics_of(id);
for gparam in mir_generics.params.iter() {
for gparam in mir_generics.own_params.iter() {
// Rust requires all lifetime/type variables to be mentioned in the fields,
// so introduce a dummy field for each lifetime/type variable
match gparam.kind {
Expand Down Expand Up @@ -2775,7 +2807,7 @@ pub(crate) fn gen_check_tracked_lifetimes<'tcx>(
}
ItemKind::Trait(
IsAuto::No,
Unsafety::Normal,
Safety::Safe,
_trait_generics,
_bounds,
_trait_items,
Expand Down Expand Up @@ -2899,7 +2931,7 @@ pub(crate) fn gen_check_tracked_lifetimes<'tcx>(
}
ItemKind::Trait(
IsAuto::No,
Unsafety::Normal,
Safety::Safe,
_trait_generics,
_bounds,
trait_items,
Expand Down Expand Up @@ -2941,7 +2973,6 @@ pub(crate) fn gen_check_tracked_lifetimes<'tcx>(
origin: OpaqueTyOrigin::AsyncFn(_),
in_trait: _,
lifetime_mapping: _,
precise_capturing_args: None,
}) => {
continue;
}
Expand Down
17 changes: 3 additions & 14 deletions source/rust_verify/src/rust_to_vir.rs
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ use crate::{unsupported_err, unsupported_err_unless};
use rustc_ast::IsAuto;
use rustc_hir::{
ForeignItem, ForeignItemId, ForeignItemKind, ImplItemKind, Item, ItemId, ItemKind, MaybeOwner,
Mutability, OpaqueTy, OpaqueTyOrigin, OwnerNode, Unsafety,
Mutability, OpaqueTy, OpaqueTyOrigin, OwnerNode, Safety,
};
use vir::def::Spanned;

Expand Down Expand Up @@ -368,17 +368,7 @@ fn check_item<'tcx>(
unsupported_err!(item.span, "static mut");
}
ItemKind::Macro(_, _) => {}
ItemKind::Trait(IsAuto::No, Unsafety::Normal, trait_generics, _bounds, trait_items) => {
if vattrs.is_external(&ctxt.cmd_line_args) {
if vattrs.external_trait_specification.is_some() {
return err_span(
item.span,
"a trait cannot be marked both `external_trait_specification` and `external`",
);
}
return Ok(());
}

ItemKind::Trait(IsAuto::No, Safety::Safe, trait_generics, _bounds, trait_items) => {
let trait_def_id = item.owner_id.to_def_id();
crate::rust_to_vir_trait::translate_trait(
ctxt,
Expand Down Expand Up @@ -408,7 +398,6 @@ fn check_item<'tcx>(
origin: OpaqueTyOrigin::AsyncFn(_),
in_trait: _,
lifetime_mapping: _,
precise_capturing_args: None,
}) => {
return Ok(());
}
Expand All @@ -429,7 +418,7 @@ fn check_foreign_item<'tcx>(
item: &'tcx ForeignItem<'tcx>,
) -> Result<(), VirErr> {
match &item.kind {
ForeignItemKind::Fn(decl, idents, generics) => {
ForeignItemKind::Fn(rustc_hir::FnSig { decl, .. }, idents, generics) => {
check_foreign_item_fn(
ctxt,
vir,
Expand Down
4 changes: 4 additions & 0 deletions source/rust_verify/src/rust_to_vir_adts.rs
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,10 @@ where
Some(VariantData::Struct { fields, recovered }) => {
// 'recovered' means that it was recovered from a syntactic error.
// So we shouldn't get to this point if 'recovered' is true.
let recovered = match recovered {
rustc_ast::Recovered::No => false,
_ => true,
};
unsupported_err_unless!(!recovered, span, "recovered_struct", variant_data_opt);
Some(*fields)
}
Expand Down
Loading
Loading