Skip to content

Commit

Permalink
Upgrade toolchain to nightly-2023-01-23 (#2149)
Browse files Browse the repository at this point in the history
Upgrade our toolchain to `nightly-2023-01-23`. The changes here are related to the following changes:
- rust-lang/rust#104986
- rust-lang/rust#105657
- rust-lang/rust#105603
- rust-lang/rust#105613
- rust-lang/rust#105977
- rust-lang/rust#104645
  • Loading branch information
celinval authored Mar 8, 2023
1 parent bf5e697 commit 5195423
Show file tree
Hide file tree
Showing 23 changed files with 73 additions and 51 deletions.
5 changes: 5 additions & 0 deletions .github/workflows/cbmc-latest.yml
Original file line number Diff line number Diff line change
Expand Up @@ -89,3 +89,8 @@ jobs:
- name: Execute Kani performance tests
working-directory: ./kani
run: ./scripts/kani-perf.sh

- name: Execute Kani performance ignored tests
working-directory: ./kani
continue-on-error: true
run: cargo run -p compiletest -- --suite perf --mode cargo-kani-test ignore --ignored --no-fail-fast
9 changes: 2 additions & 7 deletions kani-compiler/kani_queries/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -10,27 +10,22 @@ mod unsound_experiments;
#[cfg(feature = "unsound_experiments")]
use crate::unsound_experiments::UnsoundExperiments;

#[derive(Debug, Clone, Copy, AsRefStr, EnumString, EnumVariantNames, PartialEq, Eq)]
#[derive(Debug, Default, Clone, Copy, AsRefStr, EnumString, EnumVariantNames, PartialEq, Eq)]
#[strum(serialize_all = "snake_case")]
pub enum ReachabilityType {
/// Start the cross-crate reachability analysis from all harnesses in the local crate.
Harnesses,
/// Use standard rustc monomorphizer algorithm.
Legacy,
/// Don't perform any reachability analysis. This will skip codegen for this crate.
#[default]
None,
/// Start the cross-crate reachability analysis from all public functions in the local crate.
PubFns,
/// Start the cross-crate reachability analysis from all *test* (i.e. `#[test]`) harnesses in the local crate.
Tests,
}

impl Default for ReachabilityType {
fn default() -> Self {
ReachabilityType::None
}
}

pub trait UserInput {
fn set_emit_vtable_restrictions(&mut self, restrictions: bool);
fn get_emit_vtable_restrictions(&self) -> bool;
Expand Down
4 changes: 3 additions & 1 deletion kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
Original file line number Diff line number Diff line change
Expand Up @@ -365,7 +365,9 @@ impl<'tcx> GotocCtx<'tcx> {
"add_with_overflow" => codegen_op_with_overflow!(add_overflow_result),
"arith_offset" => self.codegen_offset(intrinsic, instance, fargs, p, loc),
"assert_inhabited" => self.codegen_assert_intrinsic(instance, intrinsic, span),
"assert_uninit_valid" => self.codegen_assert_intrinsic(instance, intrinsic, span),
"assert_mem_uninitialized_valid" => {
self.codegen_assert_intrinsic(instance, intrinsic, span)
}
"assert_zero_valid" => self.codegen_assert_intrinsic(instance, intrinsic, span),
// https://doc.rust-lang.org/core/intrinsics/fn.assume.html
// Informs the optimizer that a condition is always true.
Expand Down
5 changes: 2 additions & 3 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
Original file line number Diff line number Diff line change
Expand Up @@ -243,7 +243,8 @@ impl<'tcx> GotocCtx<'tcx> {
match t {
TypeOrVariant::Type(t) => {
match t.kind() {
ty::Bool
ty::Alias(..)
| ty::Bool
| ty::Char
| ty::Int(_)
| ty::Uint(_)
Expand All @@ -254,10 +255,8 @@ impl<'tcx> GotocCtx<'tcx> {
| ty::GeneratorWitness(..)
| ty::Foreign(..)
| ty::Dynamic(..)
| ty::Projection(_)
| ty::Bound(..)
| ty::Placeholder(..)
| ty::Opaque(..)
| ty::Param(_)
| ty::Infer(_)
| ty::Error(_) => unreachable!("type {:?} does not have a field", t),
Expand Down
47 changes: 34 additions & 13 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
Original file line number Diff line number Diff line change
Expand Up @@ -358,20 +358,41 @@ impl<'tcx> GotocCtx<'tcx> {
// `Generator::resume(...) -> GeneratorState` function in case we
// have an ordinary generator, or the `Future::poll(...) -> Poll`
// function in case this is a special generator backing an async construct.
let ret_ty = if self.tcx.generator_is_async(*did) {
let state_did = self.tcx.require_lang_item(LangItem::Poll, None);
let state_adt_ref = self.tcx.adt_def(state_did);
let state_substs = self.tcx.intern_substs(&[sig.return_ty.into()]);
self.tcx.mk_adt(state_adt_ref, state_substs)
let tcx = self.tcx;
let (resume_ty, ret_ty) = if tcx.generator_is_async(*did) {
// The signature should be `Future::poll(_, &mut Context<'_>) -> Poll<Output>`
let poll_did = tcx.require_lang_item(LangItem::Poll, None);
let poll_adt_ref = tcx.adt_def(poll_did);
let poll_substs = tcx.intern_substs(&[sig.return_ty.into()]);
let ret_ty = tcx.mk_adt(poll_adt_ref, poll_substs);

// We have to replace the `ResumeTy` that is used for type and borrow checking
// with `&mut Context<'_>` which is used in codegen.
#[cfg(debug_assertions)]
{
if let ty::Adt(resume_ty_adt, _) = sig.resume_ty.kind() {
let expected_adt = tcx.adt_def(tcx.require_lang_item(LangItem::ResumeTy, None));
assert_eq!(*resume_ty_adt, expected_adt);
} else {
panic!("expected `ResumeTy`, found `{:?}`", sig.resume_ty);
};
}
let context_mut_ref = tcx.mk_task_context();

(context_mut_ref, ret_ty)
} else {
let state_did = self.tcx.require_lang_item(LangItem::GeneratorState, None);
let state_adt_ref = self.tcx.adt_def(state_did);
let state_substs = self.tcx.intern_substs(&[sig.yield_ty.into(), sig.return_ty.into()]);
self.tcx.mk_adt(state_adt_ref, state_substs)
// The signature should be `Generator::resume(_, Resume) -> GeneratorState<Yield, Return>`
let state_did = tcx.require_lang_item(LangItem::GeneratorState, None);
let state_adt_ref = tcx.adt_def(state_did);
let state_substs = tcx.intern_substs(&[sig.yield_ty.into(), sig.return_ty.into()]);
let ret_ty = tcx.mk_adt(state_adt_ref, state_substs);

(sig.resume_ty, ret_ty)
};

ty::Binder::bind_with_vars(
self.tcx.mk_fn_sig(
[env_ty, sig.resume_ty].iter(),
tcx.mk_fn_sig(
[env_ty, resume_ty].iter(),
&ret_ty,
false,
Unsafety::Normal,
Expand Down Expand Up @@ -813,7 +834,7 @@ impl<'tcx> GotocCtx<'tcx> {
)
}
}
ty::Projection(_) | ty::Opaque(_, _) => {
ty::Alias(..) => {
unreachable!("Type should've been normalized already")
}

Expand Down Expand Up @@ -1226,7 +1247,7 @@ impl<'tcx> GotocCtx<'tcx> {
ty::Dynamic(..) | ty::Slice(_) | ty::Str => {
unreachable!("Should have generated a fat pointer")
}
ty::Projection(_) | ty::Opaque(..) => {
ty::Alias(..) => {
unreachable!("Should have been removed by normalization")
}

Expand Down
2 changes: 1 addition & 1 deletion kani-compiler/src/kani_compiler.rs
Original file line number Diff line number Diff line change
Expand Up @@ -169,7 +169,7 @@ impl Callbacks for KaniCompiler {
rustc_queries: &'tcx rustc_interface::Queries<'tcx>,
) -> Compilation {
if self.stubs.is_none() && self.queries.lock().unwrap().get_stubbing_enabled() {
rustc_queries.global_ctxt().unwrap().peek_mut().enter(|tcx| {
rustc_queries.global_ctxt().unwrap().enter(|tcx| {
let stubs = self.stubs.insert(self.collect_stubs(tcx));
debug!(?stubs, "after_analysis");
if stubs.is_empty() { Compilation::Continue } else { Compilation::Stop }
Expand Down
2 changes: 1 addition & 1 deletion kani-compiler/src/kani_middle/attributes.rs
Original file line number Diff line number Diff line change
Expand Up @@ -276,7 +276,7 @@ fn parse_solver(tcx: TyCtxt, attr: &Attribute) -> Option<CbmcSolver> {
}
}
MetaItemKind::NameValue(lit) if ident_str == "bin" && lit.kind.is_str() => {
Some(CbmcSolver::Binary(lit.token_lit.symbol.to_string()))
Some(CbmcSolver::Binary(lit.symbol.to_string()))
}
_ => {
invalid_arg_err(attr);
Expand Down
9 changes: 4 additions & 5 deletions kani-compiler/src/kani_middle/coercion.rs
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ use rustc_hir::lang_items::LangItem;
use rustc_middle::traits::{ImplSource, ImplSourceUserDefinedData};
use rustc_middle::ty::adjustment::CustomCoerceUnsized;
use rustc_middle::ty::TypeAndMut;
use rustc_middle::ty::{self, ParamEnv, TraitRef, Ty, TyCtxt};
use rustc_middle::ty::{self, ParamEnv, Ty, TyCtxt};
use rustc_span::symbol::Symbol;
use tracing::trace;

Expand Down Expand Up @@ -213,10 +213,9 @@ fn custom_coerce_unsize_info<'tcx>(
) -> CustomCoerceUnsized {
let def_id = tcx.require_lang_item(LangItem::CoerceUnsized, None);

let trait_ref = ty::Binder::dummy(TraitRef {
def_id,
substs: tcx.mk_substs_trait(source_ty, [target_ty.into()]),
});
let trait_ref = ty::Binder::dummy(
tcx.mk_trait_ref(def_id, tcx.mk_substs_trait(source_ty, [target_ty.into()])),
);

match tcx.codegen_select_candidate((ParamEnv::reveal_all(), trait_ref)) {
Ok(ImplSource::UserDefined(ImplSourceUserDefinedData { impl_def_id, .. })) => {
Expand Down
5 changes: 4 additions & 1 deletion kani-compiler/src/session.rs
Original file line number Diff line number Diff line change
Expand Up @@ -70,7 +70,10 @@ pub fn init_session(args: &ArgMatches, json_hook: bool) {
// Initialize the rustc logger using value from RUSTC_LOG. We keep the log control separate
// because we cannot control the RUSTC log format unless if we match the exact tracing
// version used by RUSTC.
rustc_driver::init_rustc_env_logger();
// TODO: Enable rustc log when we upgrade the toolchain.
// <https://github.com/model-checking/kani/issues/2283>
//
// rustc_driver::init_rustc_env_logger();

// Install Kani panic hook.
if json_hook {
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-2022-12-11"
channel = "nightly-2023-01-23"
components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
2 changes: 1 addition & 1 deletion scripts/kani-perf.sh
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ done
suite="perf"
mode="cargo-kani-test"
echo "Check compiletest suite=$suite mode=$mode"
cargo run -p compiletest -- --suite $suite --mode $mode
cargo run -p compiletest -- --suite $suite --mode $mode --no-fail-fast
exit_code=$?

echo "Cleaning up..."
Expand Down
4 changes: 2 additions & 2 deletions tests/cargo-kani/vecdeque-cve/src/abstract_vecdeque.rs
Original file line number Diff line number Diff line change
Expand Up @@ -275,8 +275,8 @@ impl AbstractRawVec {

fn handle_reserve(result: Result<(), TryReserveError>) {
match result.map_err(|e| e.kind()) {
Err(CapacityOverflow) => capacity_overflow(),
Err(AllocError) => handle_alloc_error(),
Err(TryReserveErrorKind::CapacityOverflow) => capacity_overflow(),
Err(TryReserveErrorKind::AllocError) => handle_alloc_error(),
Ok(()) => { /* yay */ }
}
}
Expand Down
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
2 changes: 1 addition & 1 deletion tests/ui/code-location/expected
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
module/mod.rs:10:5 in function module::not_empty
main.rs:13:5 in function same_file
/toolchains/
alloc/src/vec/mod.rs:3054:81 in function <std::vec::Vec<i32> as std::ops::Drop>::drop
alloc/src/vec/mod.rs:3059:81 in function <std::vec::Vec<i32> as std::ops::Drop>::drop

VERIFICATION:- SUCCESSFUL
26 changes: 12 additions & 14 deletions tools/compiletest/src/header.rs
Original file line number Diff line number Diff line change
Expand Up @@ -180,21 +180,17 @@ pub fn make_test_description<R: Read>(
path: &Path,
src: R,
) -> test::TestDesc {
let mut ignore = false;
let mut should_fail = false;
let mut ignore_message = None;

if config.mode == Mode::Kani || config.mode == Mode::Stub {
// If the path to the test contains "fixme" or "ignore", skip it.
let file_path = path.to_str().unwrap();
(ignore, ignore_message) = if file_path.contains("fixme") {
(true, Some("fixme test"))
} else if file_path.contains("ignore") {
(true, Some("ignore test"))
} else {
(false, None)
};
}
// If the path to the test contains "fixme" or "ignore", skip it.
let file_path = path.to_str().unwrap();
let (mut ignore, mut ignore_message) = if file_path.contains("fixme") {
(true, Some("fixme test"))
} else if file_path.contains("ignore") {
(true, Some("ignore test"))
} else {
(false, None)
};

// The `KaniFixme` mode runs tests that are ignored in the `kani` suite
if config.mode == Mode::KaniFixme {
Expand All @@ -207,8 +203,10 @@ pub fn make_test_description<R: Read>(

// If the base name does NOT contain "fixme" or "ignore", we skip it.
// All "fixme" tests are expected to fail
(ignore, ignore_message) = if base_name.contains("fixme") || base_name.contains("ignore") {
(ignore, ignore_message) = if base_name.contains("fixme") {
(false, None)
} else if base_name.contains("ignore") {
(true, Some("ignore test"))
} else {
(true, Some("regular test"))
};
Expand Down

0 comments on commit 5195423

Please sign in to comment.