Skip to content

Commit 870102f

Browse files
authored
Upgrade verus to use Rust 1.92.0 (#2056)
Updates Verus to use rustc-1.92.0
1 parent 3db55ce commit 870102f

29 files changed

Lines changed: 350 additions & 235 deletions

rust-toolchain.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
11
[toolchain]
2-
channel = "1.91.0"
2+
channel = "1.92.0"
33
components = [ "rustc", "rust-std", "cargo", "rustfmt", "rustc-dev", "llvm-tools" ]

source/rust_verify/src/boundary_suggestions.rs

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -161,7 +161,9 @@ pub(crate) fn build_fn_assume_specification_suggestion<'tcx>(
161161
"Cannot build specification for unresolved trait item. Consider an external_trait_specification declaration.",
162162
));
163163
} else if let Some(impl_def_id) = ctxt.tcx.impl_of_assoc(external_def_id) {
164-
if let Some(impl_trait) = ctxt.tcx.impl_trait_header(impl_def_id) {
164+
let of_trait = ctxt.tcx.impl_opt_trait_ref(impl_def_id).is_some();
165+
if of_trait {
166+
let impl_trait = ctxt.tcx.impl_trait_header(impl_def_id);
165167
let trait_ref = impl_trait.trait_ref.skip_binder();
166168
let self_ty = trait_ref.self_ty().fold_with(&mut region_renamer);
167169
format!(

source/rust_verify/src/rust_to_vir_base.rs

Lines changed: 16 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -11,9 +11,9 @@ use rustc_hir::definitions::DefPath;
1111
use rustc_hir::{GenericParam, GenericParamKind, Generics, HirId, LifetimeParamKind, QPath, Ty};
1212
use rustc_infer::infer::TyCtxtInferExt;
1313
use rustc_middle::ty::{
14-
AdtDef, BoundVarReplacerDelegate, Clause, ClauseKind, ConstKind, GenericArg, GenericArgKind,
15-
GenericParamDefKind, TermKind, TyCtxt, TyKind, TypeFoldable, TypeFolder, TypeSuperFoldable,
16-
TypeVisitableExt, TypingMode, ValTreeKind, Value, Visibility,
14+
AdtDef, BoundVarIndexKind, BoundVarReplacerDelegate, Clause, ClauseKind, ConstKind, GenericArg,
15+
GenericArgKind, GenericParamDefKind, TermKind, TyCtxt, TyKind, TypeFoldable, TypeFolder,
16+
TypeSuperFoldable, TypeVisitableExt, TypingMode, ValTreeKind, Value, Visibility,
1717
};
1818
use rustc_middle::ty::{TraitPredicate, TypingEnv};
1919
use rustc_span::Span;
@@ -322,7 +322,9 @@ where
322322

323323
fn fold_ty(&mut self, t: rustc_middle::ty::Ty<'tcx>) -> rustc_middle::ty::Ty<'tcx> {
324324
match *t.kind() {
325-
rustc_middle::ty::Bound(debruijn, bound_ty) if debruijn == self.current_index => {
325+
rustc_middle::ty::Bound(BoundVarIndexKind::Bound(debruijn), bound_ty)
326+
if debruijn == self.current_index =>
327+
{
326328
let ty = self.delegate.replace_ty(bound_ty);
327329
debug_assert!(!ty.has_vars_bound_above(rustc_middle::ty::INNERMOST));
328330
rustc_middle::ty::shift_vars(self.tcx, ty, self.current_index.as_u32())
@@ -335,9 +337,13 @@ where
335337
fn fold_region(&mut self, r: rustc_middle::ty::Region<'tcx>) -> rustc_middle::ty::Region<'tcx> {
336338
match r.kind() {
337339
// NOTE(verus): This is the one change, we replace == with >=
338-
rustc_middle::ty::ReBound(debruijn, br) if debruijn >= self.current_index => {
340+
rustc_middle::ty::ReBound(BoundVarIndexKind::Bound(debruijn), br)
341+
if debruijn >= self.current_index =>
342+
{
339343
let region = self.delegate.replace_region(br);
340-
if let rustc_middle::ty::ReBound(debruijn1, br) = region.kind() {
344+
if let rustc_middle::ty::ReBound(BoundVarIndexKind::Bound(debruijn1), br) =
345+
region.kind()
346+
{
341347
assert_eq!(debruijn1, rustc_middle::ty::INNERMOST);
342348
rustc_middle::ty::Region::new_bound(self.tcx, debruijn, br)
343349
} else {
@@ -350,7 +356,9 @@ where
350356

351357
fn fold_const(&mut self, ct: rustc_middle::ty::Const<'tcx>) -> rustc_middle::ty::Const<'tcx> {
352358
match ct.kind() {
353-
ConstKind::Bound(debruijn, bound_const) if debruijn == self.current_index => {
359+
ConstKind::Bound(BoundVarIndexKind::Bound(debruijn), bound_const)
360+
if debruijn == self.current_index =>
361+
{
354362
let ct = self.delegate.replace_const(bound_const);
355363
debug_assert!(!ct.has_vars_bound_above(rustc_middle::ty::INNERMOST));
356364
rustc_middle::ty::shift_vars(self.tcx, ct, self.current_index.as_u32())
@@ -1195,7 +1203,7 @@ pub(crate) fn mid_ty_to_vir_ghost<'tcx>(
11951203
let typx = TypX::FnDef(fun, Arc::new(typ_args), resolved);
11961204
(Arc::new(typx), false)
11971205
}
1198-
TyKind::Dynamic(preds, _, rustc_middle::ty::DynKind::Dyn) => {
1206+
TyKind::Dynamic(preds, _) => {
11991207
use rustc_middle::ty::ExistentialPredicate;
12001208
if preds.len() != 1 {
12011209
unsupported_err!(span, "dyn with more that one trait");

source/rust_verify/src/rust_to_vir_expr.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1368,7 +1368,7 @@ pub(crate) fn expr_to_vir_with_adjustments<'tcx>(
13681368

13691369
let (tyr1, tyr2) = remove_decoration_typs_for_unsizing(bctx.ctxt.tcx, ty1, ty2);
13701370
let op = match (tyr1.kind(), tyr2.kind()) {
1371-
(_, TyKind::Dynamic(_, _, rustc_middle::ty::DynKind::Dyn)) => Some(UnaryOp::ToDyn),
1371+
(_, TyKind::Dynamic(_, _)) => Some(UnaryOp::ToDyn),
13721372
_ => None,
13731373
};
13741374
if let Some(op) = op {

source/rust_verify/src/rust_to_vir_func.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2289,7 +2289,7 @@ pub(crate) fn get_external_def_id<'tcx>(
22892289

22902290
let mut types: Vec<Typ> = vec![];
22912291

2292-
let trait_ref = tcx.impl_trait_ref(impl_def_id).expect("impl_trait_ref");
2292+
let trait_ref = tcx.impl_trait_ref(impl_def_id);
22932293

22942294
for ty in trait_ref.instantiate(tcx, impl_args).args.types() {
22952295
types.push(ctxt.mid_ty_to_vir(impl_item_id, sig.span, &ty, false)?);

source/rust_verify/src/rust_to_vir_impl.rs

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -95,7 +95,7 @@ fn trait_impl_to_vir<'tcx>(
9595
return Ok(None);
9696
}
9797

98-
let trait_ref = ctxt.tcx.impl_trait_ref(impl_def_id).expect("impl_trait_ref");
98+
let trait_ref = ctxt.tcx.impl_trait_ref(impl_def_id);
9999
let trait_did = trait_ref.skip_binder().def_id;
100100
let impl_paths = crate::rust_to_vir_base::get_impl_paths(
101101
ctxt.tcx,
@@ -163,7 +163,7 @@ fn translate_assoc_type<'tcx>(
163163
trait_typ_args: Typs,
164164
) -> Result<AssocTypeImpl, VirErr> {
165165
let impl_path = ctxt.def_id_to_vir_path(impl_def_id);
166-
let trait_ref = ctxt.tcx.impl_trait_ref(impl_def_id).expect("impl_trait_ref");
166+
let trait_ref = ctxt.tcx.impl_trait_ref(impl_def_id);
167167
let ty = ctxt.tcx.type_of(impl_item_id).skip_binder();
168168
let typ = ctxt.mid_ty_to_vir(impl_item_id, impl_item_span, &ty, false)?;
169169
let (typ_params, typ_bounds) = crate::rust_to_vir_base::check_generics_bounds_no_polarity(
@@ -589,7 +589,7 @@ pub(crate) fn collect_external_trait_impls<'tcx>(
589589

590590
// Process only the new implementations that could be visible to Verus:
591591
'impls: for impl_def_id in auto_import_impls {
592-
let trait_ref = tcx.impl_trait_ref(&impl_def_id).expect("impl_trait_ref");
592+
let trait_ref = tcx.impl_trait_ref(&impl_def_id);
593593
for arg in trait_ref.skip_binder().args.iter() {
594594
if !crate::rust_to_vir_base::mid_arg_filter_for_external_impls(
595595
ctxt,
@@ -695,7 +695,7 @@ pub(crate) fn collect_external_trait_impls<'tcx>(
695695

696696
for (impl_path, (impl_def_id, funs)) in new_trait_impls.iter() {
697697
let trait_ref = tcx.impl_trait_ref(impl_def_id);
698-
let trait_did = trait_ref.expect("impl_trait_ref").skip_binder().def_id;
698+
let trait_did = trait_ref.skip_binder().def_id;
699699
let trait_path = ctxt.def_id_to_vir_path(trait_did);
700700
let Some(traitt) = trait_map.get(&trait_path) else {
701701
continue;

source/rust_verify/src/verifier.rs

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,7 @@ use vir::messages::{
2525

2626
use num_format::{Locale, ToFormattedString};
2727
use rustc_error_messages::MultiSpan;
28+
use rustc_index::bit_set::DenseBitSet;
2829
use rustc_middle::ty::TyCtxt;
2930
use rustc_span::Span;
3031
use rustc_span::def_id::LOCAL_CRATE;
@@ -3095,11 +3096,11 @@ impl rustc_driver::Callbacks for VerifierCallbacksEraseMacro {
30953096
providers.hir_crate = hir_crate;
30963097
providers.mir_const_qualif = |_, _| rustc_middle::mir::ConstQualifs::default();
30973098
providers.lint_mod = |_, _| {};
3098-
providers.check_liveness = |_, _| {};
3099+
providers.check_liveness = |_, _| DenseBitSet::new_empty(0);
30993100
providers.check_mod_deathness = |_, _| {};
31003101

31013102
providers.mir_borrowck = |tcx, _local_def_id| {
3102-
Ok(tcx.arena.alloc(rustc_middle::mir::ConcreteOpaqueTypes(
3103+
Ok(tcx.arena.alloc(rustc_middle::mir::DefinitionSiteHiddenTypes(
31033104
rustc_data_structures::fx::FxIndexMap::default(),
31043105
)))
31053106
};
@@ -3109,7 +3110,7 @@ impl rustc_driver::Callbacks for VerifierCallbacksEraseMacro {
31093110
providers.hir_crate = hir_crate;
31103111
providers.mir_const_qualif = |_, _| rustc_middle::mir::ConstQualifs::default();
31113112
providers.lint_mod = |_, _| {};
3112-
providers.check_liveness = |_, _| {};
3113+
providers.check_liveness = |_, _| DenseBitSet::new_empty(0);
31133114
providers.check_mod_deathness = |_, _| {};
31143115

31153116
rustc_mir_build_verus::verus_provide(providers);

source/rust_verify_test/tests/regression.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1459,7 +1459,7 @@ test_verify_one_file_with_options! {
14591459
extern "C" { type T; }
14601460

14611461
trait ToBool { fn to_bool(&self) -> bool; }
1462-
impl ToBool for Box<T> where { fn to_bool(&self) -> bool { todo!() } }
1462+
impl ToBool for *const T where { fn to_bool(&self) -> bool { todo!() } }
14631463
} => Ok(())
14641464
}
14651465

source/rustc_hir_typeck/src/upvar.rs

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1253,9 +1253,10 @@ fn restrict_precision_for_unsafe(
12531253
(place, curr_mode)
12541254
}
12551255

1256-
/// Truncate projections so that following rules are obeyed by the captured `place`:
1256+
/// Truncate projections so that the following rules are obeyed by the captured `place`:
12571257
/// - No Index projections are captured, since arrays are captured completely.
1258-
/// - No unsafe block is required to capture `place`
1258+
/// - No unsafe block is required to capture `place`.
1259+
///
12591260
/// Returns the truncated place and updated capture mode.
12601261
fn restrict_capture_precision(
12611262
place: Place<'_>,

source/rustc_mir_build/messages.ftl

Lines changed: 5 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -322,17 +322,6 @@ mir_build_pointer_pattern = function pointers and raw pointers not derived from
322322
323323
mir_build_privately_uninhabited = pattern `{$witness_1}` is currently uninhabited, but this variant contains private fields which may become inhabited in the future
324324
325-
mir_build_rust_2024_incompatible_pat = {$bad_modifiers ->
326-
*[true] binding modifiers{$bad_ref_pats ->
327-
*[true] {" "}and reference patterns
328-
[false] {""}
329-
}
330-
[false] reference patterns
331-
} may only be written when the default binding mode is `move`{$is_hard_error ->
332-
*[true] {""}
333-
[false] {" "}in Rust 2024
334-
}
335-
336325
mir_build_static_in_pattern = statics cannot be referenced in patterns
337326
.label = can't be used in patterns
338327
mir_build_static_in_pattern_def = `static` defined here
@@ -383,6 +372,11 @@ mir_build_union_field_requires_unsafe_unsafe_op_in_unsafe_fn_allowed =
383372
mir_build_union_pattern = cannot use unions in constant patterns
384373
.label = can't use a `union` here
385374
375+
mir_build_unreachable_due_to_uninhabited = unreachable {$descr}
376+
.label = unreachable {$descr}
377+
.label_orig = any code following this expression is unreachable
378+
.note = this expression has type `{$ty}`, which is uninhabited
379+
386380
mir_build_unreachable_making_this_unreachable = collectively making this unreachable
387381
388382
mir_build_unreachable_making_this_unreachable_n_more = ...and {$covered_by_many_n_more_count} other patterns collectively make this unreachable

0 commit comments

Comments
 (0)