From c59c557c1b8e1a6b65b44aa2cea770e8e2fa0866 Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Thu, 7 Dec 2023 15:44:40 +0100 Subject: [PATCH 1/8] Bump actions/labeler from 4 to 5 (#2917) Bumps [actions/labeler](https://github.com/actions/labeler) from 4 to 5. --- .github/workflows/extra_jobs.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/extra_jobs.yml b/.github/workflows/extra_jobs.yml index d4da80fbe132..ea7508776f19 100644 --- a/.github/workflows/extra_jobs.yml +++ b/.github/workflows/extra_jobs.yml @@ -37,7 +37,7 @@ jobs: - name: Label PR id: labeler - uses: actions/labeler@v4 + uses: actions/labeler@v5 with: dot: true From b7968026573b2b142ac137ac739bcef8162686ec Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 7 Dec 2023 21:11:20 +0100 Subject: [PATCH 2/8] Revert "Bump actions/labeler from 4 to 5 (#2917)" (#2923) This reverts commit c59c557c1b8e1a6b65b44aa2cea770e8e2fa0866. See #2922. --- .github/workflows/extra_jobs.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/extra_jobs.yml b/.github/workflows/extra_jobs.yml index ea7508776f19..d4da80fbe132 100644 --- a/.github/workflows/extra_jobs.yml +++ b/.github/workflows/extra_jobs.yml @@ -37,7 +37,7 @@ jobs: - name: Label PR id: labeler - uses: actions/labeler@v5 + uses: actions/labeler@v4 with: dot: true From 2aca488ba9d64d2aaeae3b7774acf367bea42be9 Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Thu, 7 Dec 2023 23:09:48 +0100 Subject: [PATCH 3/8] Bump docker/build-push-action from 3 to 5 (#2921) Bumps [docker/build-push-action](https://github.com/docker/build-push-action) from 3 to 5. --- .github/workflows/release.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 74af1c0be544..5a37f5e5c03e 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -284,7 +284,7 @@ jobs: OWNER: '${{ github.repository_owner }}' - name: Build and push - uses: docker/build-push-action@v3 + uses: docker/build-push-action@v5 with: context: . file: scripts/ci/Dockerfile.bundle-release-20-04 From 01bf411b514836a25dc5a2f44b6b0cfbaeacfc36 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?O=C4=9Fuz=20A=C4=9Fcayaz=C4=B1?= Date: Fri, 8 Dec 2023 05:10:08 +0300 Subject: [PATCH 4/8] Stabilize `find_debug_info` (#2912) Last time we stabilized https://github.com/model-checking/kani/pull/2882, this continues the trend and stabilizes `find_debug_info` as well. --- .../src/codegen_cprover_gotoc/codegen/span.rs | 15 +++++++++------ .../src/codegen_cprover_gotoc/utils/names.rs | 2 +- 2 files changed, 10 insertions(+), 7 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs index 9f88bbbe7b55..3fbfd3629775 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs @@ -5,9 +5,10 @@ use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::goto_program::Location; -use rustc_middle::mir::{Local, VarDebugInfo, VarDebugInfoContents}; +use rustc_middle::mir::{Local, VarDebugInfoContents}; use rustc_smir::rustc_internal; use rustc_span::Span; +use stable_mir::mir::VarDebugInfo; impl<'tcx> GotocCtx<'tcx> { pub fn codegen_span(&self, sp: &Span) -> Location { @@ -43,10 +44,12 @@ impl<'tcx> GotocCtx<'tcx> { sp.map_or(Location::none(), |x| self.codegen_span(&x)) } - pub fn find_debug_info(&self, l: &Local) -> Option<&VarDebugInfo<'tcx>> { - self.current_fn().mir().var_debug_info.iter().find(|info| match info.value { - VarDebugInfoContents::Place(p) => p.local == *l && p.projection.len() == 0, - VarDebugInfoContents::Const(_) => false, - }) + pub fn find_debug_info(&self, l: &Local) -> Option { + rustc_internal::stable(self.current_fn().mir().var_debug_info.iter().find(|info| { + match info.value { + VarDebugInfoContents::Place(p) => p.local == *l && p.projection.len() == 0, + VarDebugInfoContents::Const(_) => false, + } + })) } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs index 98f6f533cd12..da684b601668 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs @@ -22,7 +22,7 @@ impl<'tcx> GotocCtx<'tcx> { pub fn codegen_var_base_name(&self, l: &Local) -> String { match self.find_debug_info(l) { None => format!("var_{}", l.index()), - Some(info) => format!("{}", info.name), + Some(info) => info.name, } } From 63af43d86b00ad1097ab8b6eec9daf276ab8b407 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 8 Dec 2023 08:51:10 +0100 Subject: [PATCH 5/8] Update the rust toolchain to nightly-2023-12-07 (#2913) Changes required due to: - rust-lang/rust@99ac405b96 Move MetadataLoader{,Dyn} to rustc_metadata. - rust-lang/rust@c997c6d822 Add more information to stable Instance - https://github.com/rust-lang/rust/pull/116915 This also fixes an issue in the `simd_shuffle` implementation that was exposed by the update. Resolves #2911 --------- Co-authored-by: Celina G. Val Co-authored-by: Adrian Palacios --- .../codegen/intrinsic.rs | 4 +- .../compiler_interface.rs | 2 +- kani-compiler/src/kani_middle/analysis.rs | 1 - kani-compiler/src/kani_middle/reachability.rs | 11 ++-- kani-compiler/src/kani_middle/stubbing/mod.rs | 1 + .../src/concrete_playback/test_generator.rs | 2 +- library/kani/src/models/mod.rs | 32 +++++++--- rust-toolchain.toml | 2 +- tests/expected/any_vec/exact_length.expected | 8 +-- tests/expected/any_vec/out_bounds.expected | 63 ++----------------- tests/kani/Intrinsics/SIMD/Shuffle/main.rs | 10 +++ tests/kani/SIMD/portable_simd.rs | 9 ++- tests/kani/SIMD/swizzle.rs | 31 +++++++++ 13 files changed, 94 insertions(+), 82 deletions(-) create mode 100644 tests/kani/SIMD/swizzle.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 5d60f15f69a5..11e4721dfb31 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -1729,7 +1729,7 @@ impl<'tcx> GotocCtx<'tcx> { // [u32; n]: translated wrapped in a struct let indexes = fargs.remove(0); - let (_, vec_subtype) = rust_arg_types[0].simd_size_and_type(self.tcx); + let (in_type_len, vec_subtype) = rust_arg_types[0].simd_size_and_type(self.tcx); let (ret_type_len, ret_type_subtype) = rust_ret_type.simd_size_and_type(self.tcx); if ret_type_len != n { let err_msg = format!( @@ -1749,7 +1749,7 @@ impl<'tcx> GotocCtx<'tcx> { // An unsigned type here causes an invariant violation in CBMC. // Issue: https://github.com/diffblue/cbmc/issues/6298 let st_rep = Type::ssize_t(); - let n_rep = Expr::int_constant(n, st_rep.clone()); + let n_rep = Expr::int_constant(in_type_len, st_rep.clone()); // P = indexes.expanded_map(v -> if v < N then vec1[v] else vec2[v-N]) let elems = (0..n) diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index df472518c9a3..7b94dad06db4 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -33,6 +33,7 @@ use rustc_data_structures::temp_dir::MaybeTempDir; use rustc_errors::{ErrorGuaranteed, DEFAULT_LOCALE_RESOURCE}; use rustc_hir::def_id::LOCAL_CRATE; use rustc_hir::definitions::DefPathHash; +use rustc_metadata::creader::MetadataLoaderDyn; use rustc_metadata::fs::{emit_wrapper_file, METADATA_FILENAME}; use rustc_metadata::EncodedMetadata; use rustc_middle::dep_graph::{WorkProduct, WorkProductId}; @@ -40,7 +41,6 @@ use rustc_middle::mir::mono::MonoItem; use rustc_middle::ty::TyCtxt; use rustc_middle::util::Providers; use rustc_session::config::{CrateType, OutputFilenames, OutputType}; -use rustc_session::cstore::MetadataLoaderDyn; use rustc_session::output::out_filename; use rustc_session::Session; use rustc_smir::rustc_internal; diff --git a/kani-compiler/src/kani_middle/analysis.rs b/kani-compiler/src/kani_middle/analysis.rs index 011907c14ea4..b23fb99f83ff 100644 --- a/kani-compiler/src/kani_middle/analysis.rs +++ b/kani-compiler/src/kani_middle/analysis.rs @@ -151,7 +151,6 @@ impl From<&Terminator> for Key { TerminatorKind::Assert { .. } => Key("Assert"), TerminatorKind::Call { .. } => Key("Call"), TerminatorKind::Drop { .. } => Key("Drop"), - TerminatorKind::CoroutineDrop => Key("CoroutineDrop"), TerminatorKind::Goto { .. } => Key("Goto"), TerminatorKind::InlineAsm { .. } => Key("InlineAsm"), TerminatorKind::Resume { .. } => Key("Resume"), diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index d56b7b5db65d..a8e7d9fe3f83 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -153,7 +153,11 @@ impl<'tcx> MonoItemsCollector<'tcx> { /// instruction looking for the items that should be included in the compilation. fn reachable_items(&mut self) { while let Some(to_visit) = self.queue.pop() { - if !self.collected.contains(&to_visit) { + // TODO: This should only check is_foreign_item() or even `has_body()`. + // We need https://github.com/rust-lang/rust/pull/118681 to land first. + if !self.collected.contains(&to_visit) + && !self.tcx.is_foreign_item(rustc_internal::internal(to_visit.clone()).def_id()) + { self.collected.insert(to_visit.clone()); let next_items = match &to_visit { MonoItem::Fn(instance) => self.visit_fn(*instance), @@ -266,7 +270,7 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> { /// Collect an instance depending on how it is used (invoked directly or via fn_ptr). fn collect_instance(&mut self, instance: Instance, is_direct_call: bool) { let should_collect = match instance.kind { - InstanceKind::Virtual | InstanceKind::Intrinsic => { + InstanceKind::Virtual { .. } | InstanceKind::Intrinsic => { // Instance definition has no body. assert!(is_direct_call, "Expected direct call {instance:?}"); false @@ -453,8 +457,7 @@ impl<'a, 'tcx> MirVisitor for MonoItemsFnCollector<'a, 'tcx> { TerminatorKind::Abort { .. } | TerminatorKind::Assert { .. } => { // We generate code for this without invoking any lang item. } - TerminatorKind::CoroutineDrop { .. } - | TerminatorKind::Goto { .. } + TerminatorKind::Goto { .. } | TerminatorKind::SwitchInt { .. } | TerminatorKind::Resume | TerminatorKind::Return diff --git a/kani-compiler/src/kani_middle/stubbing/mod.rs b/kani-compiler/src/kani_middle/stubbing/mod.rs index 03298456c522..6af0b442c8d4 100644 --- a/kani-compiler/src/kani_middle/stubbing/mod.rs +++ b/kani-compiler/src/kani_middle/stubbing/mod.rs @@ -46,6 +46,7 @@ pub fn harness_stub_map( pub fn validate_instance(tcx: TyCtxt, instance: Instance) -> bool { let internal_instance = rustc_internal::internal(instance); if get_stub(tcx, internal_instance.def_id()).is_some() { + debug!(?instance, "validate_instance"); let item = CrateItem::try_from(instance).unwrap(); let mut checker = StubConstChecker::new(tcx, internal_instance, item); checker.visit_body(&item.body()); diff --git a/kani-driver/src/concrete_playback/test_generator.rs b/kani-driver/src/concrete_playback/test_generator.rs index 492369fb32eb..53c3a92dd94c 100644 --- a/kani-driver/src/concrete_playback/test_generator.rs +++ b/kani-driver/src/concrete_playback/test_generator.rs @@ -163,7 +163,7 @@ impl KaniSession { let mut curr_line_num = 0; // Use a buffered reader/writer to generate the unit test line by line - for line in source_reader.lines().flatten() { + for line in source_reader.lines().map_while(Result::ok) { curr_line_num += 1; writeln!(temp_file, "{line}")?; if curr_line_num == proof_harness_end_line { diff --git a/library/kani/src/models/mod.rs b/library/kani/src/models/mod.rs index 8b3f771756dc..194f220595c0 100644 --- a/library/kani/src/models/mod.rs +++ b/library/kani/src/models/mod.rs @@ -137,8 +137,8 @@ mod test { /// masks with lanes represented using i16. #[test] fn test_bitmask_i16() { - check_portable_bitmask::<_, i16, 16>(mask16x16::splat(false)); - check_portable_bitmask::<_, i16, 16>(mask16x16::splat(true)); + check_portable_bitmask::<_, i16, 16, u16>(mask16x16::splat(false)); + check_portable_bitmask::<_, i16, 16, u16>(mask16x16::splat(true)); } /// Tests that the model correctly fails if an invalid value is given. @@ -165,11 +165,11 @@ mod test { /// These values shouldn't be symmetric and ensure that we also handle endianness correctly. #[test] fn test_bitmask_i32() { - check_portable_bitmask::<_, i32, 8>(mask32x8::from([ + check_portable_bitmask::<_, i32, 8, u8>(mask32x8::from([ true, true, false, true, false, false, false, true, ])); - check_portable_bitmask::<_, i32, 4>(mask32x4::from([true, false, false, true])); + check_portable_bitmask::<_, i32, 4, u8>(mask32x4::from([true, false, false, true])); } #[repr(simd)] @@ -185,15 +185,16 @@ mod test { } /// Compare the value returned by our model and the portable simd representation. - fn check_portable_bitmask(mask: T) + fn check_portable_bitmask(mask: Mask) where - T: ToBitMask + Clone, - T::BitMask: Debug + PartialEq, + T: std::simd::MaskElement, + LaneCount: SupportedLaneCount, E: kani_intrinsic::MaskElement, [u8; kani_intrinsic::mask_len(LANES)]: Sized, + u64: From, { assert_eq!( - unsafe { kani_intrinsic::simd_bitmask::<_, T::BitMask, E, LANES>(mask.clone()) }, + unsafe { u64::from(kani_intrinsic::simd_bitmask::<_, M, E, LANES>(mask.clone())) }, mask.to_bitmask() ); } @@ -211,4 +212,19 @@ mod test { unsafe { simd_bitmask::(mask) } ); } + + /// Similar to portable simd_harness. + #[test] + fn check_mask_harness() { + // From array doesn't work either. Manually build [false, true, false, true] + let mut mask = mask32x4::splat(false); + mask.set(1, true); + mask.set(3, true); + let bitmask = mask.to_bitmask(); + assert_eq!(bitmask, 0b1010); + + let kani_mask = + unsafe { u64::from(kani_intrinsic::simd_bitmask::<_, u8, u32, 4>(mask.clone())) }; + assert_eq!(kani_mask, bitmask); + } } diff --git a/rust-toolchain.toml b/rust-toolchain.toml index e016b6b50492..2bdb5cdf793a 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-12-01" +channel = "nightly-2023-12-07" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/expected/any_vec/exact_length.expected b/tests/expected/any_vec/exact_length.expected index 641db7843ff1..082f3fb61570 100644 --- a/tests/expected/any_vec/exact_length.expected +++ b/tests/expected/any_vec/exact_length.expected @@ -1,12 +1,12 @@ Checking harness check_access_length_17... -Failed Checks: dereference failure: pointer outside object bounds\ -in check_access_length_17 +Failed Checks: assumption failed\ +in >::get_unchecked Checking harness check_access_length_zero... -Failed Checks: dereference failure: pointer outside object bounds\ -in check_access_length_zero +Failed Checks: assumption failed\ +in >::get_unchecked Verification failed for - check_access_length_17 Verification failed for - check_access_length_zero diff --git a/tests/expected/any_vec/out_bounds.expected b/tests/expected/any_vec/out_bounds.expected index 167fefe6d6f4..24121aee4ee8 100644 --- a/tests/expected/any_vec/out_bounds.expected +++ b/tests/expected/any_vec/out_bounds.expected @@ -1,61 +1,6 @@ -check_always_out_bounds::check_0.pointer_dereference\ -Status: FAILURE\ -Description: "dereference failure: pointer NULL"\ -function check_always_out_bounds::check_0 - -check_always_out_bounds::check_0.pointer_dereference\ -Status: FAILURE\ -Description: "dereference failure: pointer outside object bounds"\ -function check_always_out_bounds::check_0 - -check_always_out_bounds::check_0.pointer_dereference\ -Status: FAILURE\ -Description: "dereference failure: invalid integer address"\ -function check_always_out_bounds::check_0 - -check_always_out_bounds::check_1.pointer_dereference\ -Status: FAILURE\ -Description: "dereference failure: pointer outside object bounds"\ -function check_always_out_bounds::check_1 - -check_always_out_bounds::check_2.pointer_dereference\ -Status: FAILURE\ -Description: "dereference failure: pointer outside object bounds"\ -function check_always_out_bounds::check_2 - -check_always_out_bounds::check_3.pointer_dereference\ -Status: FAILURE\ -Description: "dereference failure: pointer outside object bounds"\ -function check_always_out_bounds::check_3 - -check_always_out_bounds::check_4.pointer_dereference\ -Status: FAILURE\ -Description: "dereference failure: pointer outside object bounds"\ -function check_always_out_bounds::check_4 - -check_always_out_bounds::check_5.pointer_dereference\ -Status: FAILURE\ -Description: "dereference failure: pointer outside object bounds"\ -function check_always_out_bounds::check_5 - -check_always_out_bounds::check_6.pointer_dereference\ -Status: FAILURE\ -Description: "dereference failure: pointer outside object bounds"\ -function check_always_out_bounds::check_6 - -check_always_out_bounds::check_7.pointer_dereference\ -Status: FAILURE\ -Description: "dereference failure: pointer outside object bounds"\ -function check_always_out_bounds::check_7 - -check_always_out_bounds::check_8.pointer_dereference\ -Status: FAILURE\ -Description: "dereference failure: pointer outside object bounds"\ -function check_always_out_bounds::check_8 - -check_always_out_bounds::check_9.cover\ -Status: UNREACHABLE\ -Description: "cover condition: *val == 0"\ -function check_always_out_bounds::check_9 +Checking harness check_always_out_bounds... +Failed Checks: assumption failed +in >::get_unchecked +Verification failed for - check_always_out_bounds diff --git a/tests/kani/Intrinsics/SIMD/Shuffle/main.rs b/tests/kani/Intrinsics/SIMD/Shuffle/main.rs index b3b0d41f0dff..6d822a18bdc1 100644 --- a/tests/kani/Intrinsics/SIMD/Shuffle/main.rs +++ b/tests/kani/Intrinsics/SIMD/Shuffle/main.rs @@ -45,3 +45,13 @@ fn main() { assert!(c == i64x4(2, 4, 6, 8)); } } + +#[kani::proof] +fn check_shuffle() { + { + let y = i64x2(0, 1); + let z = i64x2(1, 2); + const I: [u32; 4] = [1, 2, 0, 3]; + let _x: i64x4 = unsafe { simd_shuffle(y, z, I) }; + } +} diff --git a/tests/kani/SIMD/portable_simd.rs b/tests/kani/SIMD/portable_simd.rs index c8995de410e0..64cfb4b1fcf3 100644 --- a/tests/kani/SIMD/portable_simd.rs +++ b/tests/kani/SIMD/portable_simd.rs @@ -4,7 +4,7 @@ //! Ensure we have basic support of portable SIMD. #![feature(portable_simd)] -use std::simd::{mask32x4, u64x16, ToBitMask}; +use std::simd::{mask32x4, u32x4, u64x16}; #[kani::proof] fn check_sum_any() { @@ -23,3 +23,10 @@ fn check_mask() { let bitmask = mask.to_bitmask(); assert_eq!(bitmask, 0b1010); } + +#[kani::proof] +fn check_resize() { + let x = u32x4::from_array([0, 1, 2, 3]); + assert_eq!(x.resize::<8>(9).to_array(), [0, 1, 2, 3, 9, 9, 9, 9]); + assert_eq!(x.resize::<2>(9).to_array(), [0, 1]); +} diff --git a/tests/kani/SIMD/swizzle.rs b/tests/kani/SIMD/swizzle.rs new file mode 100644 index 000000000000..26781743dbfa --- /dev/null +++ b/tests/kani/SIMD/swizzle.rs @@ -0,0 +1,31 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Ensure we can safely swizzle between SIMD types of different sizes. +#![feature(portable_simd)] + +use std::simd::{simd_swizzle, u32x4, u32x8}; + +#[kani::proof] +fn harness_from_u32x4_to_u32x4() { + let a = u32x4::from_array([0, 1, 2, 3]); + let b = u32x4::from_array([4, 5, 6, 7]); + let r: u32x4 = simd_swizzle!(a, b, [0, 1, 6, 7]); + assert_eq!(r.to_array(), [0, 1, 6, 7]); +} + +#[kani::proof] +fn harness_from_u32x4_to_u32x8() { + let a = u32x4::from_array([0, 1, 2, 3]); + let b = u32x4::from_array([4, 5, 6, 7]); + let r: u32x8 = simd_swizzle!(a, b, [0, 1, 2, 3, 4, 5, 6, 7]); + assert_eq!(r.to_array(), [0, 1, 2, 3, 4, 5, 6, 7]); +} + +#[kani::proof] +fn harness_from_u32x8_to_u32x4() { + let a = u32x8::from_array([0, 1, 2, 3, 4, 5, 6, 7]); + let b = u32x8::from_array([0, 1, 2, 3, 4, 5, 6, 7]); + let r: u32x4 = simd_swizzle!(a, b, [0, 1, 2, 3]); + assert_eq!(r.to_array(), [0, 1, 2, 3]); +} From d26485a3436ce96793a6e63aace0de6bd0d81810 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 8 Dec 2023 08:41:40 -0800 Subject: [PATCH 6/8] Remove doc build from regular regression (#2925) This check is redundant in our CI since the bookrunner job already builds the documentation. It is also often breaking the regression job. Co-authored-by: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com> --- scripts/kani-regression.sh | 8 -------- 1 file changed, 8 deletions(-) diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh index 161a96dbe1af..20782abe5cbc 100755 --- a/scripts/kani-regression.sh +++ b/scripts/kani-regression.sh @@ -100,14 +100,6 @@ FEATURES_MANIFEST_PATH="$KANI_DIR/tests/cargo-kani/cargo-features-flag/Cargo.tom cargo kani --manifest-path "$FEATURES_MANIFEST_PATH" --harness trivial_success cargo clean --manifest-path "$FEATURES_MANIFEST_PATH" -# Check that documentation compiles. -echo "Current disk usage:" -df -h -echo "Starting doc tests:" -cargo doc --workspace --no-deps --exclude std -echo "Disk usage after documentation build:" -df -h - echo echo "All Kani regression tests completed successfully." echo From d095367f33d582107a3e344b9008ffabc30cadf9 Mon Sep 17 00:00:00 2001 From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Date: Fri, 8 Dec 2023 14:17:47 -0500 Subject: [PATCH 7/8] Update Rust toolchain to `nightly-2023-12-08` (#2926) Updates the Rust toolchain to `nightly-2023-12-08`. The relevant changes are: * https://github.com/rust-lang/rust/pull/118324 * https://github.com/rust-lang/rust/pull/118684 --------- Co-authored-by: Celina G. Val --- .../src/codegen_cprover_gotoc/codegen/operand.rs | 6 ++++-- kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs | 9 ++++----- kani-compiler/src/kani_middle/reachability.rs | 6 +----- rust-toolchain.toml | 2 +- 4 files changed, 10 insertions(+), 13 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index d297d9d90a52..59a18348d582 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -421,7 +421,8 @@ impl<'tcx> GotocCtx<'tcx> { } (Scalar::Ptr(ptr, _size), _) => { let res_t = self.codegen_ty(ty); - let (alloc_id, offset) = ptr.into_parts(); + let (prov, offset) = ptr.into_parts(); + let alloc_id = prov.alloc_id(); self.codegen_alloc_pointer(res_t, alloc_id, offset, span) } _ => unimplemented!(), @@ -646,7 +647,8 @@ impl<'tcx> GotocCtx<'tcx> { Size::from_bytes(self.symbol_table.machine_model().pointer_width_in_bytes()); let mut next_offset = Size::ZERO; - for &(offset, alloc_id) in alloc.provenance().ptrs().iter() { + for &(offset, prov) in alloc.provenance().ptrs().iter() { + let alloc_id = prov.alloc_id(); if offset > next_offset { let bytes = alloc.inspect_with_uninit_and_ptr_outside_interpreter( next_offset.bytes_usize()..offset.bytes_usize(), diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index aec9d8143818..ec5756c4d09b 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -332,11 +332,11 @@ impl<'tcx> GotocCtx<'tcx> { ty: Ty<'tcx>, args: ty::GenericArgsRef<'tcx>, ) -> ty::PolyFnSig<'tcx> { - let sig = args.as_coroutine().poly_sig(); + let sig = args.as_coroutine().sig(); - let bound_vars = self.tcx.mk_bound_variable_kinds_from_iter( - sig.bound_vars().iter().chain(iter::once(ty::BoundVariableKind::Region(ty::BrEnv))), - ); + let bound_vars = self.tcx.mk_bound_variable_kinds_from_iter(iter::once( + ty::BoundVariableKind::Region(ty::BrEnv), + )); let br = ty::BoundRegion { var: ty::BoundVar::from_usize(bound_vars.len() - 1), kind: ty::BoundRegionKind::BrEnv, @@ -349,7 +349,6 @@ impl<'tcx> GotocCtx<'tcx> { let pin_args = self.tcx.mk_args(&[env_ty.into()]); let env_ty = Ty::new_adt(self.tcx, pin_adt_ref, pin_args); - let sig = sig.skip_binder(); // The `FnSig` and the `ret_ty` here is for a coroutines main // `coroutine::resume(...) -> CoroutineState` function in case we // have an ordinary coroutine, or the `Future::poll(...) -> Poll` diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index a8e7d9fe3f83..216feb66fb87 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -153,11 +153,7 @@ impl<'tcx> MonoItemsCollector<'tcx> { /// instruction looking for the items that should be included in the compilation. fn reachable_items(&mut self) { while let Some(to_visit) = self.queue.pop() { - // TODO: This should only check is_foreign_item() or even `has_body()`. - // We need https://github.com/rust-lang/rust/pull/118681 to land first. - if !self.collected.contains(&to_visit) - && !self.tcx.is_foreign_item(rustc_internal::internal(to_visit.clone()).def_id()) - { + if !self.collected.contains(&to_visit) { self.collected.insert(to_visit.clone()); let next_items = match &to_visit { MonoItem::Fn(instance) => self.visit_fn(*instance), diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 2bdb5cdf793a..6c7de32c5e63 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-12-07" +channel = "nightly-2023-12-08" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] From abd3690dce0445ab801b9c5c2bd249b2fb16a526 Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Fri, 8 Dec 2023 23:03:49 +0100 Subject: [PATCH 8/8] Bump docker/login-action from 2 to 3 (#2916) Bumps [docker/login-action](https://github.com/docker/login-action) from 2 to 3. --- .github/workflows/release.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 5a37f5e5c03e..cdc69479d961 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -271,7 +271,7 @@ jobs: cargo package -p kani-verifier - name: 'Login to GitHub Container Registry' - uses: docker/login-action@v2 + uses: docker/login-action@v3 with: registry: ghcr.io username: ${{ github.repository_owner }}