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

Upgrade toolchain to nightly-2023-01-23 #2149

Merged
merged 5 commits into from
Mar 8, 2023
Merged
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
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
zhassan-aws marked this conversation as resolved.
Show resolved Hide resolved
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]
celinval marked this conversation as resolved.
Show resolved Hide resolved
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
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;
celinval marked this conversation as resolved.
Show resolved Hide resolved
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
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