From 9574a33565e42709260cb8f492ad62ff47dd64e2 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Mon, 14 Apr 2025 16:51:43 -0700 Subject: [PATCH 1/5] Update toolchain to 2025-04-14 --- rust-toolchain.toml | 2 +- tests/expected/uninit/intrinsics/expected | 4 --- .../FunctionContracts/modify_slice_elem.rs | 25 ------------------- 3 files changed, 1 insertion(+), 30 deletions(-) delete mode 100644 tests/kani/FunctionContracts/modify_slice_elem.rs diff --git a/rust-toolchain.toml b/rust-toolchain.toml index c1527c24328a..e3f058231d91 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2025-04-07" +channel = "nightly-2025-04-14" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/expected/uninit/intrinsics/expected b/tests/expected/uninit/intrinsics/expected index d19d694df75e..e2ca608475a1 100644 --- a/tests/expected/uninit/intrinsics/expected +++ b/tests/expected/uninit/intrinsics/expected @@ -1,7 +1,3 @@ -std::ptr::read::>.unsupported_construct.\ - - Status: FAILURE\ - - Description: "Interaction between raw pointers and unions is not yet supported." - check_typed_swap_nonoverlapping.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*mut u8`" diff --git a/tests/kani/FunctionContracts/modify_slice_elem.rs b/tests/kani/FunctionContracts/modify_slice_elem.rs deleted file mode 100644 index 50df13b45af3..000000000000 --- a/tests/kani/FunctionContracts/modify_slice_elem.rs +++ /dev/null @@ -1,25 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT -//! Check that Kani correctly verifies the contract that modifies slices. -//! -//! Note that this test used to crash while parsing the annotations. -// kani-flags: -Zfunction-contracts -extern crate kani; - -#[kani::requires(idx < slice.len())] -#[kani::modifies(slice.as_ptr().wrapping_add(idx))] -#[kani::ensures(|_| slice[idx] == new_val)] -fn modify_slice(slice: &mut [u32], idx: usize, new_val: u32) { - *slice.get_mut(idx).unwrap() = new_val; -} - -#[cfg(kani)] -mod verify { - use super::modify_slice; - - #[kani::proof_for_contract(modify_slice)] - fn check_modify_slice() { - let mut data = kani::vec::any_vec::(); - modify_slice(&mut data, kani::any(), kani::any()) - } -} From 890312a749b38730e8317d0922ba3fafc85227a2 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Tue, 15 Apr 2025 08:24:17 -0700 Subject: [PATCH 2/5] Fix ULLBC backend --- kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs index 219bc48c4d91..546a3aa4f127 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs @@ -813,7 +813,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { let disambiguator = CharonDisambiguator::new(data.disambiguator as usize); use rustc_hir::definitions::DefPathData; match &data.data { - DefPathData::TypeNs(Some(symbol)) => { + DefPathData::TypeNs(symbol) => { error_assert!(self, span, data.disambiguator == 0); // Sanity check name.push(CharonPathElem::Ident(symbol.to_string(), disambiguator)); } @@ -956,7 +956,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { let disambiguator = CharonDisambiguator::new(data.disambiguator as usize); use rustc_hir::definitions::DefPathData; match &data.data { - DefPathData::TypeNs(Some(symbol)) => { + DefPathData::TypeNs(symbol) => { error_assert!(self, span, data.disambiguator == 0); // Sanity check name.push(CharonPathElem::Ident(symbol.to_string(), disambiguator)); } @@ -1063,7 +1063,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { let disambiguator = CharonDisambiguator::new(data.disambiguator as usize); use rustc_hir::definitions::DefPathData; match &data.data { - DefPathData::TypeNs(Some(symbol)) => { + DefPathData::TypeNs(symbol) => { error_assert!(self, span, data.disambiguator == 0); // Sanity check name.push(CharonPathElem::Ident(symbol.to_string(), disambiguator)); } From 2944b46754822bf86519e69690fc1ca528670be7 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Tue, 15 Apr 2025 15:23:16 -0700 Subject: [PATCH 3/5] Rewrite test to reduce memory usage --- tests/perf/smol_str/src/lib.rs | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/tests/perf/smol_str/src/lib.rs b/tests/perf/smol_str/src/lib.rs index 7fe771c1fc07..01f1881bad03 100644 --- a/tests/perf/smol_str/src/lib.rs +++ b/tests/perf/smol_str/src/lib.rs @@ -5,9 +5,11 @@ //! #[kani::proof] -#[kani::unwind(4)] +#[kani::unwind(13)] fn check_new() { - let data: [char; 3] = kani::any(); - let input: String = data.iter().collect(); + let data: [u8; 12] = kani::any(); + let res = String::from_utf8(data.into()); + kani::assume(res.is_ok()); + let input: String = res.unwrap(); smol_str::SmolStr::new(&input); } From 47b38fa7d193d2e606ffd53c023172c9f911482a Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Thu, 17 Apr 2025 16:40:55 -0700 Subject: [PATCH 4/5] Add back test --- .../FunctionContracts/modify_slice_elem.rs | 25 +++++++++++++++++++ 1 file changed, 25 insertions(+) create mode 100644 tests/kani/FunctionContracts/modify_slice_elem.rs diff --git a/tests/kani/FunctionContracts/modify_slice_elem.rs b/tests/kani/FunctionContracts/modify_slice_elem.rs new file mode 100644 index 000000000000..50df13b45af3 --- /dev/null +++ b/tests/kani/FunctionContracts/modify_slice_elem.rs @@ -0,0 +1,25 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Check that Kani correctly verifies the contract that modifies slices. +//! +//! Note that this test used to crash while parsing the annotations. +// kani-flags: -Zfunction-contracts +extern crate kani; + +#[kani::requires(idx < slice.len())] +#[kani::modifies(slice.as_ptr().wrapping_add(idx))] +#[kani::ensures(|_| slice[idx] == new_val)] +fn modify_slice(slice: &mut [u32], idx: usize, new_val: u32) { + *slice.get_mut(idx).unwrap() = new_val; +} + +#[cfg(kani)] +mod verify { + use super::modify_slice; + + #[kani::proof_for_contract(modify_slice)] + fn check_modify_slice() { + let mut data = kani::vec::any_vec::(); + modify_slice(&mut data, kani::any(), kani::any()) + } +} From ca69e3cf6279cac62130cb713ecba54437220d15 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Thu, 17 Apr 2025 16:44:18 -0700 Subject: [PATCH 5/5] Turn into a fixme test --- .../{modify_slice_elem.rs => modify_slice_elem_fixme.rs} | 3 +++ 1 file changed, 3 insertions(+) rename tests/kani/FunctionContracts/{modify_slice_elem.rs => modify_slice_elem_fixme.rs} (84%) diff --git a/tests/kani/FunctionContracts/modify_slice_elem.rs b/tests/kani/FunctionContracts/modify_slice_elem_fixme.rs similarity index 84% rename from tests/kani/FunctionContracts/modify_slice_elem.rs rename to tests/kani/FunctionContracts/modify_slice_elem_fixme.rs index 50df13b45af3..385db9983d88 100644 --- a/tests/kani/FunctionContracts/modify_slice_elem.rs +++ b/tests/kani/FunctionContracts/modify_slice_elem_fixme.rs @@ -2,6 +2,9 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT //! Check that Kani correctly verifies the contract that modifies slices. //! +//! This started failing with the 2025-04-05 toolchain upgrade +//! Tracking issue: https://github.com/model-checking/kani/issues/4029 +//! //! Note that this test used to crash while parsing the annotations. // kani-flags: -Zfunction-contracts extern crate kani;