From 379413fc0b8feeb758bd241a8a41855068d9bb43 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 23 Jan 2023 12:39:55 -0800 Subject: [PATCH 1/4] Upgrade toolchain to nightly-2023-01-16 This commit fixes compilation errors but not runtime ones. Related changes: https://github.com/rust-lang/rust/pull/104986 https://github.com/rust-lang/rust/pull/105657 https://github.com/rust-lang/rust/pull/105603 https://github.com/rust-lang/rust/pull/105613 --- .../src/codegen_cprover_gotoc/codegen/intrinsic.rs | 4 +++- kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs | 5 ++--- kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs | 4 ++-- kani-compiler/src/kani_middle/coercion.rs | 9 ++++----- kani-compiler/src/kani_middle/stubbing/annotations.rs | 2 +- rust-toolchain.toml | 2 +- 6 files changed, 13 insertions(+), 13 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 910a842e61d0..98ed0421e05d 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -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. diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 97d0c225c963..67801f747acc 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -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(_) @@ -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), diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index f315e1795fa9..339c0cbc1de4 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -813,7 +813,7 @@ impl<'tcx> GotocCtx<'tcx> { ) } } - ty::Projection(_) | ty::Opaque(_, _) => { + ty::Alias(..) => { unreachable!("Type should've been normalized already") } @@ -1226,7 +1226,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") } diff --git a/kani-compiler/src/kani_middle/coercion.rs b/kani-compiler/src/kani_middle/coercion.rs index 799ba3b4766c..71ddd457e075 100644 --- a/kani-compiler/src/kani_middle/coercion.rs +++ b/kani-compiler/src/kani_middle/coercion.rs @@ -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; @@ -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, .. })) => { diff --git a/kani-compiler/src/kani_middle/stubbing/annotations.rs b/kani-compiler/src/kani_middle/stubbing/annotations.rs index 16079efde4c5..cc4befdcae5d 100644 --- a/kani-compiler/src/kani_middle/stubbing/annotations.rs +++ b/kani-compiler/src/kani_middle/stubbing/annotations.rs @@ -40,7 +40,7 @@ impl Callbacks for CollectorCallbacks { _compiler: &Compiler, queries: &'tcx Queries<'tcx>, ) -> Compilation { - queries.global_ctxt().unwrap().peek_mut().enter(|tcx| { + queries.global_ctxt().unwrap().enter(|tcx| { for item in tcx.hir_crate_items(()).items() { let local_def_id = item.owner_id.def_id; let def_id = local_def_id.to_def_id(); diff --git a/rust-toolchain.toml b/rust-toolchain.toml index aa6a41cddcbb..4a47bd63038b 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2022-12-11" +channel = "nightly-2023-01-16" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] From c5db1df8302cd3c0e5171d4941377f8e664f1de4 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 23 Jan 2023 18:50:41 -0800 Subject: [PATCH 2/4] Upgrade toolchain to nightly-2023-01-23 to overcome an issue with async generators. Updated the codegen_generator to follow the new logic implemented in https://github.com/rust-lang/rust/pull/105977 --- kani-compiler/kani_queries/src/lib.rs | 9 +--- .../src/codegen_cprover_gotoc/codegen/typ.rs | 43 ++++++++++++++----- rust-toolchain.toml | 2 +- .../vecdeque-cve/src/abstract_vecdeque.rs | 4 +- tests/ui/code-location/expected | 2 +- 5 files changed, 38 insertions(+), 22 deletions(-) diff --git a/kani-compiler/kani_queries/src/lib.rs b/kani-compiler/kani_queries/src/lib.rs index cfb0cff3c8ea..b3993595eb00 100644 --- a/kani-compiler/kani_queries/src/lib.rs +++ b/kani-compiler/kani_queries/src/lib.rs @@ -15,7 +15,7 @@ use { std::sync::{Arc, Mutex}, }; -#[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. @@ -23,6 +23,7 @@ pub enum ReachabilityType { /// 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, @@ -30,12 +31,6 @@ pub enum ReachabilityType { 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; diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 339c0cbc1de4..fca6ffe5db61 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -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` + 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` + 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, diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 4a47bd63038b..185bd4ff4136 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2023-01-16" +channel = "nightly-2023-01-23" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/cargo-kani/vecdeque-cve/src/abstract_vecdeque.rs b/tests/cargo-kani/vecdeque-cve/src/abstract_vecdeque.rs index c128b57dbb59..8bcc44742ed9 100644 --- a/tests/cargo-kani/vecdeque-cve/src/abstract_vecdeque.rs +++ b/tests/cargo-kani/vecdeque-cve/src/abstract_vecdeque.rs @@ -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 */ } } } diff --git a/tests/ui/code-location/expected b/tests/ui/code-location/expected index 20d7f40879bc..1d188e17314a 100644 --- a/tests/ui/code-location/expected +++ b/tests/ui/code-location/expected @@ -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 as std::ops::Drop>::drop +alloc/src/vec/mod.rs:3059:81 in function as std::ops::Drop>::drop VERIFICATION:- SUCCESSFUL From 4d3bed28d3b68f32ef91de6c33b167025d25e52e Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 8 Mar 2023 12:48:03 -0800 Subject: [PATCH 3/4] Mark performance regressions as ignored for now and enable them to be executed as part of CBMC nightly --- .github/workflows/cbmc-latest.yml | 5 ++++ .../Cargo.toml | 0 .../expected | 0 .../src/main.rs | 0 .../vec/{string => ignore_string}/Cargo.toml | 0 .../{ => ignore_string}/box_dyn/Cargo.toml | 0 .../vec/{ => ignore_string}/box_dyn/expected | 0 .../{ => ignore_string}/box_dyn/src/main.rs | 0 .../vec/{string => ignore_string}/expected | 0 .../vec/{string => ignore_string}/src/main.rs | 0 tools/compiletest/src/header.rs | 26 +++++++++---------- 11 files changed, 17 insertions(+), 14 deletions(-) rename tests/perf/btreeset/{insert_same => ignore_insert_same}/Cargo.toml (100%) rename tests/perf/btreeset/{insert_same => ignore_insert_same}/expected (100%) rename tests/perf/btreeset/{insert_same => ignore_insert_same}/src/main.rs (100%) rename tests/perf/vec/{string => ignore_string}/Cargo.toml (100%) rename tests/perf/vec/{ => ignore_string}/box_dyn/Cargo.toml (100%) rename tests/perf/vec/{ => ignore_string}/box_dyn/expected (100%) rename tests/perf/vec/{ => ignore_string}/box_dyn/src/main.rs (100%) rename tests/perf/vec/{string => ignore_string}/expected (100%) rename tests/perf/vec/{string => ignore_string}/src/main.rs (100%) diff --git a/.github/workflows/cbmc-latest.yml b/.github/workflows/cbmc-latest.yml index 9191e8250550..4ce5be4bed8b 100644 --- a/.github/workflows/cbmc-latest.yml +++ b/.github/workflows/cbmc-latest.yml @@ -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 diff --git a/tests/perf/btreeset/insert_same/Cargo.toml b/tests/perf/btreeset/ignore_insert_same/Cargo.toml similarity index 100% rename from tests/perf/btreeset/insert_same/Cargo.toml rename to tests/perf/btreeset/ignore_insert_same/Cargo.toml diff --git a/tests/perf/btreeset/insert_same/expected b/tests/perf/btreeset/ignore_insert_same/expected similarity index 100% rename from tests/perf/btreeset/insert_same/expected rename to tests/perf/btreeset/ignore_insert_same/expected diff --git a/tests/perf/btreeset/insert_same/src/main.rs b/tests/perf/btreeset/ignore_insert_same/src/main.rs similarity index 100% rename from tests/perf/btreeset/insert_same/src/main.rs rename to tests/perf/btreeset/ignore_insert_same/src/main.rs diff --git a/tests/perf/vec/string/Cargo.toml b/tests/perf/vec/ignore_string/Cargo.toml similarity index 100% rename from tests/perf/vec/string/Cargo.toml rename to tests/perf/vec/ignore_string/Cargo.toml diff --git a/tests/perf/vec/box_dyn/Cargo.toml b/tests/perf/vec/ignore_string/box_dyn/Cargo.toml similarity index 100% rename from tests/perf/vec/box_dyn/Cargo.toml rename to tests/perf/vec/ignore_string/box_dyn/Cargo.toml diff --git a/tests/perf/vec/box_dyn/expected b/tests/perf/vec/ignore_string/box_dyn/expected similarity index 100% rename from tests/perf/vec/box_dyn/expected rename to tests/perf/vec/ignore_string/box_dyn/expected diff --git a/tests/perf/vec/box_dyn/src/main.rs b/tests/perf/vec/ignore_string/box_dyn/src/main.rs similarity index 100% rename from tests/perf/vec/box_dyn/src/main.rs rename to tests/perf/vec/ignore_string/box_dyn/src/main.rs diff --git a/tests/perf/vec/string/expected b/tests/perf/vec/ignore_string/expected similarity index 100% rename from tests/perf/vec/string/expected rename to tests/perf/vec/ignore_string/expected diff --git a/tests/perf/vec/string/src/main.rs b/tests/perf/vec/ignore_string/src/main.rs similarity index 100% rename from tests/perf/vec/string/src/main.rs rename to tests/perf/vec/ignore_string/src/main.rs diff --git a/tools/compiletest/src/header.rs b/tools/compiletest/src/header.rs index fc7ac84b5680..afb9057ad451 100644 --- a/tools/compiletest/src/header.rs +++ b/tools/compiletest/src/header.rs @@ -180,21 +180,17 @@ pub fn make_test_description( 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 { @@ -207,8 +203,10 @@ pub fn make_test_description( // 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")) }; From e7bc03ab1d0ab1f24a963f8c45213f3430d3b7bb Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 6 Feb 2023 19:36:00 +0000 Subject: [PATCH 4/4] Change performance test to always run all tests Added --no-fail-fast to the script --- .github/workflows/cbmc-latest.yml | 2 +- scripts/kani-perf.sh | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/cbmc-latest.yml b/.github/workflows/cbmc-latest.yml index 4ce5be4bed8b..71806f0a0cca 100644 --- a/.github/workflows/cbmc-latest.yml +++ b/.github/workflows/cbmc-latest.yml @@ -93,4 +93,4 @@ jobs: - 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 + run: cargo run -p compiletest -- --suite perf --mode cargo-kani-test ignore --ignored --no-fail-fast diff --git a/scripts/kani-perf.sh b/scripts/kani-perf.sh index e73986a32ae2..a7e2710773aa 100755 --- a/scripts/kani-perf.sh +++ b/scripts/kani-perf.sh @@ -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..."