Skip to content

Commit

Permalink
Update the rust toolchain to nightly-2023-11-27
Browse files Browse the repository at this point in the history
  • Loading branch information
celinval committed Nov 27, 2023
1 parent 7bdafad commit 63795a0
Show file tree
Hide file tree
Showing 20 changed files with 40 additions and 46 deletions.
15 changes: 6 additions & 9 deletions kani-compiler/src/kani_middle/reachability.rs
Original file line number Diff line number Diff line change
Expand Up @@ -85,14 +85,11 @@ where
.iter()
.filter_map(|item| {
// Only collect monomorphic items.
Instance::try_from(*item)
.ok()
.map(|instance| {
let def_id = rustc_internal::internal(item);
predicate(tcx, def_id)
.then_some(InternalMonoItem::Fn(rustc_internal::internal(&instance)))
})
.flatten()
Instance::try_from(*item).ok().and_then(|instance| {
let def_id = rustc_internal::internal(item);
predicate(tcx, def_id)
.then_some(InternalMonoItem::Fn(rustc_internal::internal(&instance)))
})
})
.collect::<Vec<_>>()
})
Expand Down Expand Up @@ -500,7 +497,7 @@ fn to_fingerprint(tcx: TyCtxt, item: &InternalMonoItem) -> Fingerprint {
}

/// Return whether we should include the item into codegen.
fn should_codegen_locally<'tcx>(instance: &Instance) -> bool {
fn should_codegen_locally(instance: &Instance) -> bool {
!instance.is_foreign_item()
}

Expand Down
4 changes: 2 additions & 2 deletions kani-compiler/src/kani_middle/resolve.rs
Original file line number Diff line number Diff line change
Expand Up @@ -190,7 +190,7 @@ fn resolve_prefix<'tcx>(
CRATE => {
segments.next();
// Find the module at the root of the crate.
let current_module_hir_id = tcx.hir().local_def_id_to_hir_id(current_module);
let current_module_hir_id = tcx.local_def_id_to_hir_id(current_module);
let crate_root = match tcx.hir().parent_iter(current_module_hir_id).last() {
None => current_module,
Some((hir_id, _)) => hir_id.owner.def_id,
Expand Down Expand Up @@ -229,7 +229,7 @@ fn resolve_super<'tcx, I>(
where
I: Iterator<Item = String>,
{
let current_module_hir_id = tcx.hir().local_def_id_to_hir_id(current_module);
let current_module_hir_id = tcx.local_def_id_to_hir_id(current_module);
let mut parents = tcx.hir().parent_iter(current_module_hir_id);
let mut base_module = current_module;
while segments.next_if(|segment| segment == SUPER).is_some() {
Expand Down
33 changes: 15 additions & 18 deletions kani-compiler/src/kani_middle/stubbing/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -92,27 +92,24 @@ impl<'tcx> MirVisitor for StubConstChecker<'tcx> {
Const::Val(..) | Const::Ty(..) => {}
Const::Unevaluated(un_eval, _) => {
// Thread local fall into this category.
match self.tcx.const_eval_resolve(ParamEnv::reveal_all(), un_eval, None) {
if self.tcx.const_eval_resolve(ParamEnv::reveal_all(), un_eval, None).is_err() {
// The `monomorphize` call should have evaluated that constant already.
Err(_) => {
let tcx = self.tcx;
let mono_const = &un_eval;
let implementor = match mono_const.args.as_slice() {
[one] => one.as_type().unwrap(),
_ => unreachable!(),
};
let trait_ = tcx.trait_of_item(mono_const.def).unwrap();
let msg = format!(
"Type `{implementor}` does not implement trait `{}`. \
let tcx = self.tcx;
let mono_const = &un_eval;
let implementor = match mono_const.args.as_slice() {
[one] => one.as_type().unwrap(),
_ => unreachable!(),
};
let trait_ = tcx.trait_of_item(mono_const.def).unwrap();
let msg = format!(
"Type `{implementor}` does not implement trait `{}`. \
This is likely because `{}` is used as a stub but its \
generic bounds are not being met.",
tcx.def_path_str(trait_),
self.source.name()
);
tcx.sess.span_err(rustc_internal::internal(location.span()), msg);
self.is_valid = false;
}
_ => {}
tcx.def_path_str(trait_),
self.source.name()
);
tcx.sess.span_err(rustc_internal::internal(location.span()), msg);
self.is_valid = false;
}
}
};
Expand Down
2 changes: 1 addition & 1 deletion rust-toolchain.toml
Original file line number Diff line number Diff line change
Expand Up @@ -2,5 +2,5 @@
# SPDX-License-Identifier: Apache-2.0 OR MIT

[toolchain]
channel = "nightly-2023-11-22"
channel = "nightly-2023-11-27"
components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
Original file line number Diff line number Diff line change
@@ -1 +1 @@
error[E0391]: cycle detected when optimizing MIR for `crate_a::assert_true`
error[E0391]: cycle detected when optimizing MIR for `crate_b::assert_false`
2 changes: 1 addition & 1 deletion tests/expected/intrinsics/ctpop-ice/expected
Original file line number Diff line number Diff line change
Expand Up @@ -3,4 +3,4 @@ error: Type check failed for intrinsic `ctpop`: Expected integer type, found ()
12 | let n = ctpop(());
| ^^^^^^^^^

error: aborting due to previous error
error: aborting due to 1 previous error
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
expected return type with length 2 (same as input type `u64x2`), found `u32x4` with length 4
error: aborting due to previous error
error: aborting due to 1 previous error
2 changes: 1 addition & 1 deletion tests/expected/intrinsics/simd-extract-wrong-type/expected
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
expected return type `i64` (element of input `i64x2`), found `i32`
error: aborting due to previous error
error: aborting due to 1 previous error
2 changes: 1 addition & 1 deletion tests/expected/intrinsics/simd-insert-wrong-type/expected
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
expected inserted type `i64` (element of input `i64x2`), found `i32`
error: aborting due to previous error
error: aborting due to 1 previous error
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
expected return type with integer elements, found `f32x2` with non-integer `f32`
error: aborting due to previous error
error: aborting due to 1 previous error
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
expected return type of length 4, found `i64x2` with length 2
error: aborting due to previous error
error: aborting due to 1 previous error
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
expected return element type `i64` (element of input `i64x2`), found `f64x2` with element type `f64`
error: aborting due to previous error
error: aborting due to 1 previous error
2 changes: 1 addition & 1 deletion tests/expected/panic/arg-error/expected
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
error: 1 positional argument in format string, but no arguments were given
error: aborting due to previous error
error: aborting due to 1 previous error
2 changes: 1 addition & 1 deletion tests/ui/should-panic-attribute/multiple-attrs/expected
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
error: only one '#[kani::should_panic]' attribute is allowed per harness
error: aborting due to previous error
error: aborting due to 1 previous error
2 changes: 1 addition & 1 deletion tests/ui/should-panic-attribute/with-args/expected
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
error: custom attribute panicked
help: message: `#[kani::should_panic]` does not take any arguments currently
error: aborting due to previous error
error: aborting due to 1 previous error
2 changes: 1 addition & 1 deletion tests/ui/solver-attribute/invalid/expected
Original file line number Diff line number Diff line change
Expand Up @@ -3,4 +3,4 @@ test.rs:\
|\
| #[kani::solver(123)]\
| ^^^^^^^^^^^^^^^^^^^^
error: aborting due to previous error
error: aborting due to 1 previous error
2 changes: 1 addition & 1 deletion tests/ui/solver-attribute/multiple-args/expected
Original file line number Diff line number Diff line change
Expand Up @@ -3,4 +3,4 @@ test.rs:\
|\
| #[kani::solver(kissat, minisat)]\
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
error: aborting due to previous error
error: aborting due to 1 previous error
2 changes: 1 addition & 1 deletion tests/ui/solver-attribute/multiple-attrs/expected
Original file line number Diff line number Diff line change
Expand Up @@ -3,4 +3,4 @@ test.rs:\
|\
| #[kani::solver(kissat)]\
| ^^^^^^^^^^^^^^^^^^^^^^^
error: aborting due to previous error
error: aborting due to 1 previous error
2 changes: 1 addition & 1 deletion tests/ui/solver-attribute/no-arg/expected
Original file line number Diff line number Diff line change
Expand Up @@ -3,4 +3,4 @@ test.rs:\
|\
| #[kani::solver]\
| ^^^^^^^^^^^^^^^
error: aborting due to previous error
error: aborting due to 1 previous error
2 changes: 1 addition & 1 deletion tests/ui/solver-attribute/unknown/expected
Original file line number Diff line number Diff line change
Expand Up @@ -3,4 +3,4 @@ test.rs:\
|\
| #[kani::solver(foo)]\
| ^^^^^^^^^^^^^^^^^^^^
error: aborting due to previous error
error: aborting due to 1 previous error

0 comments on commit 63795a0

Please sign in to comment.