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 01/10] 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 02/10] 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 03/10] 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 04/10] 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 05/10] 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 06/10] 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 07/10] 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 08/10] 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 }} From b7ece82280fbfc5025fd6fe95f092728172c58a7 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 8 Dec 2023 23:30:27 -0800 Subject: [PATCH 09/10] Clean up some code before migrating rvalue (#2928) Clean up old unreachable check due to missing component which has been a long time by the MirLinker. Also remove an old TODO code to add the def name to virtual calls. This has regressed before, so the risk of regressing doesn't seem worth for debug purpose. --- .../codegen_cprover_gotoc/codegen/rvalue.rs | 36 ++++--------------- .../codegen/statement.rs | 15 ++------ .../src/codegen_cprover_gotoc/codegen/typ.rs | 2 +- .../codegen_cprover_gotoc/context/goto_ctx.rs | 5 --- .../src/codegen_cprover_gotoc/utils/names.rs | 9 ++--- 5 files changed, 12 insertions(+), 55 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index c781f272fb2d..8ded0b7f421a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -11,7 +11,7 @@ use crate::kani_middle::coercion::{ }; use crate::unwrap_or_return_codegen_unimplemented; use cbmc::goto_program::{ - arithmetic_overflow_result_type, BinaryOperator, Expr, Location, Stmt, Symbol, Type, + arithmetic_overflow_result_type, BinaryOperator, Expr, Location, Stmt, Type, ARITH_OVERFLOW_OVERFLOWED_FIELD, ARITH_OVERFLOW_RESULT_FIELD, }; use cbmc::MachineModel; @@ -1169,7 +1169,7 @@ impl<'tcx> GotocCtx<'tcx> { idx: usize, ) -> Expr { debug!(?instance, typ=?t, %idx, "codegen_vtable_method_field"); - let vtable_field_name = self.vtable_field_name(instance.def_id(), idx); + let vtable_field_name = self.vtable_field_name(idx); let vtable_type = Type::struct_tag(self.vtable_name(t)); let field_type = vtable_type.lookup_field_type(vtable_field_name, &self.symbol_table).unwrap(); @@ -1232,34 +1232,10 @@ impl<'tcx> GotocCtx<'tcx> { .address_of() .cast_to(trait_fn_ty) } else { - // We skip an entire submodule of the standard library, so drop is missing - // for it. Build and insert a function that just calls an unimplemented block - // to maintain soundness. - let drop_sym_name = format!("drop_unimplemented_{}", self.symbol_name(drop_instance)); - let pretty_name = - format!("drop_unimplemented<{}>", self.readable_instance_name(drop_instance)); - let drop_sym = self.ensure(&drop_sym_name, |ctx, name| { - // Function body - let unimplemented = ctx.codegen_unimplemented_stmt( - format!("drop_in_place for {drop_instance}").as_str(), - Location::none(), - "https://github.com/model-checking/kani/issues/281", - ); - - // Declare symbol for the single, self parameter - let param_typ = ctx.codegen_ty(trait_ty).to_pointer(); - let param_sym = ctx.gen_function_parameter(0, &drop_sym_name, param_typ); - - // Build and insert the function itself - Symbol::function( - name, - Type::code(vec![param_sym.to_function_parameter()], Type::empty()), - Some(Stmt::block(vec![unimplemented], Location::none())), - pretty_name, - Location::none(), - ) - }); - drop_sym.to_expr().address_of().cast_to(trait_fn_ty) + unreachable!( + "Missing drop implementation for {}", + self.readable_instance_name(drop_instance) + ); } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index a4597885716a..d673c7d37c83 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -6,7 +6,6 @@ use super::PropertyClass; use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx}; use crate::unwrap_or_return_codegen_unimplemented_stmt; use cbmc::goto_program::{Expr, Location, Stmt, Type}; -use rustc_hir::def_id::DefId; use rustc_middle::mir; use rustc_middle::mir::{ AssertKind, BasicBlock, NonDivergingIntrinsic, Operand, Place, Statement, StatementKind, @@ -541,16 +540,9 @@ impl<'tcx> GotocCtx<'tcx> { return Stmt::goto(self.current_fn().find_label(&target.unwrap()), loc); } // Handle a virtual function call via a vtable lookup - InstanceDef::Virtual(def_id, idx) => { + InstanceDef::Virtual(_, idx) => { let self_ty = self.operand_ty(&args[0]); - self.codegen_virtual_funcall( - self_ty, - def_id, - idx, - destination, - &mut fargs, - loc, - ) + self.codegen_virtual_funcall(self_ty, idx, destination, &mut fargs, loc) } // Normal, non-virtual function calls InstanceDef::Item(..) @@ -623,13 +615,12 @@ impl<'tcx> GotocCtx<'tcx> { fn codegen_virtual_funcall( &mut self, self_ty: Ty<'tcx>, - def_id: DefId, idx: usize, place: &Place<'tcx>, fargs: &mut [Expr], loc: Location, ) -> Vec { - let vtable_field_name = self.vtable_field_name(def_id, idx); + let vtable_field_name = self.vtable_field_name(idx); trace!(?self_ty, ?place, ?vtable_field_name, "codegen_virtual_funcall"); debug!(?fargs, "codegen_virtual_funcall"); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index ec5756c4d09b..3a9d54a384af 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -481,7 +481,7 @@ impl<'tcx> GotocCtx<'tcx> { let fn_ptr = fn_ty.to_pointer(); // vtable field name, i.e., 3_vol (idx_method) - let vtable_field_name = self.vtable_field_name(instance.def_id(), idx); + let vtable_field_name = self.vtable_field_name(idx); DatatypeComponent::field(vtable_field_name, fn_ptr) } diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs index 01fb198d16fa..6619a6949681 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -138,11 +138,6 @@ impl<'tcx> GotocCtx<'tcx> { self.gen_stack_variable(c, fname, "var", t, Location::none(), false) } - // Generate a Symbol Expression representing a function parameter from the MIR - pub fn gen_function_parameter(&mut self, c: u64, fname: &str, t: Type) -> Symbol { - self.gen_stack_variable(c, fname, "var", t, Location::none(), true) - } - /// Given a counter `c` a function name `fname, and a prefix `prefix`, generates a new function local variable /// It is an error to reuse an existing `c`, `fname` `prefix` tuple. fn gen_stack_variable( diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs index da684b601668..2782f2cee47c 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs @@ -5,7 +5,6 @@ use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::InternedString; -use rustc_hir::def_id::DefId; use rustc_hir::def_id::LOCAL_CRATE; use rustc_middle::mir::mono::CodegenUnitNameBuilder; use rustc_middle::mir::Local; @@ -83,12 +82,8 @@ impl<'tcx> GotocCtx<'tcx> { /// The name for the struct field on a vtable for a given function. Because generic /// functions can share the same name, we need to use the index of the entry in the /// vtable. This is the same index that will be passed in virtual function calls as - /// InstanceDef::Virtual(def_id, idx). We could use solely the index as a key into - /// the vtable struct, but we add the method name for debugging readability. - /// Example: 3_vol - pub fn vtable_field_name(&self, _def_id: DefId, idx: usize) -> InternedString { - // format!("{}_{}", idx, with_no_trimmed_paths!(|| self.tcx.item_name(def_id))) - // TODO: use def_id https://github.com/model-checking/kani/issues/364 + /// InstanceDef::Virtual(def_id, idx). + pub fn vtable_field_name(&self, idx: usize) -> InternedString { idx.to_string().into() } From 9e2b33578cd384c723c6dd0dad40256981b24adf Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Sat, 9 Dec 2023 14:04:12 +0100 Subject: [PATCH 10/10] Bump actions/checkout from 3 to 4 (#2918) Bumps [actions/checkout](https://github.com/actions/checkout) from 3 to 4. --- .github/workflows/audit.yml | 2 +- .github/workflows/bench.yml | 4 ++-- .github/workflows/cbmc-latest.yml | 8 ++++---- .github/workflows/cbmc-update.yml | 2 +- .github/workflows/extra_jobs.yml | 2 +- .github/workflows/format-check.yml | 4 ++-- .github/workflows/kani-m1.yml | 2 +- .github/workflows/kani.yml | 10 +++++----- .github/workflows/release.yml | 10 +++++----- .github/workflows/slow-tests.yml | 2 +- .github/workflows/toolchain-upgrade.yml | 2 +- 11 files changed, 24 insertions(+), 24 deletions(-) diff --git a/.github/workflows/audit.yml b/.github/workflows/audit.yml index bf852429459c..3ae9d192f376 100644 --- a/.github/workflows/audit.yml +++ b/.github/workflows/audit.yml @@ -16,7 +16,7 @@ jobs: audit: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 - uses: EmbarkStudios/cargo-deny-action@v1 with: arguments: --all-features --workspace diff --git a/.github/workflows/bench.yml b/.github/workflows/bench.yml index 615a8ff6c0aa..ad0bbf81f2c2 100644 --- a/.github/workflows/bench.yml +++ b/.github/workflows/bench.yml @@ -30,14 +30,14 @@ jobs: echo "NEW_REF=${{ github.event.pull_request.head.sha }}" | tee -a "$GITHUB_ENV" - name: Check out Kani (old variant) - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: path: ./old ref: ${{ env.OLD_REF }} fetch-depth: 2 - name: Check out Kani (new variant) - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: path: ./new ref: ${{ env.NEW_REF }} diff --git a/.github/workflows/cbmc-latest.yml b/.github/workflows/cbmc-latest.yml index 287215e554b7..9cb8082ae4b7 100644 --- a/.github/workflows/cbmc-latest.yml +++ b/.github/workflows/cbmc-latest.yml @@ -22,7 +22,7 @@ jobs: os: [macos-12, ubuntu-20.04, ubuntu-22.04] steps: - name: Checkout Kani under "kani" - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: path: kani @@ -37,7 +37,7 @@ jobs: run: cargo build-dev - name: Checkout CBMC under "cbmc" - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: repository: diffblue/cbmc path: cbmc @@ -58,7 +58,7 @@ jobs: runs-on: ubuntu-20.04 steps: - name: Checkout Kani under "kani" - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: path: kani @@ -73,7 +73,7 @@ jobs: run: cargo build-dev -- --release - name: Checkout CBMC under "cbmc" - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: repository: diffblue/cbmc path: cbmc diff --git a/.github/workflows/cbmc-update.yml b/.github/workflows/cbmc-update.yml index 3b8d6cbcd37e..e5f33e935e09 100644 --- a/.github/workflows/cbmc-update.yml +++ b/.github/workflows/cbmc-update.yml @@ -19,7 +19,7 @@ jobs: runs-on: ubuntu-22.04 steps: - name: Checkout Kani - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Setup Kani Dependencies uses: ./.github/actions/setup diff --git a/.github/workflows/extra_jobs.yml b/.github/workflows/extra_jobs.yml index d4da80fbe132..45ca6968c4ba 100644 --- a/.github/workflows/extra_jobs.yml +++ b/.github/workflows/extra_jobs.yml @@ -33,7 +33,7 @@ jobs: runs-on: ubuntu-latest steps: - name: Checkout Kani - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Label PR id: labeler diff --git a/.github/workflows/format-check.yml b/.github/workflows/format-check.yml index 6a8267b09231..5ab7dcb1b9c3 100644 --- a/.github/workflows/format-check.yml +++ b/.github/workflows/format-check.yml @@ -14,7 +14,7 @@ jobs: runs-on: ubuntu-latest steps: - name: Checkout Kani - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Execute copyright check run: ./scripts/ci/run-copyright-check.sh @@ -33,7 +33,7 @@ jobs: runs-on: ubuntu-20.04 steps: - name: Checkout Kani - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Setup Kani Dependencies uses: ./.github/actions/setup diff --git a/.github/workflows/kani-m1.yml b/.github/workflows/kani-m1.yml index e9f973c82919..36f2b615c4aa 100644 --- a/.github/workflows/kani-m1.yml +++ b/.github/workflows/kani-m1.yml @@ -16,7 +16,7 @@ jobs: runs-on: macos-13-xlarge steps: - name: Checkout Kani - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Setup Kani Dependencies uses: ./.github/actions/setup diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index a22ed971ec12..e866eaf635de 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -20,7 +20,7 @@ jobs: os: [macos-12, ubuntu-20.04, ubuntu-22.04] steps: - name: Checkout Kani - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Setup Kani Dependencies uses: ./.github/actions/setup @@ -37,7 +37,7 @@ jobs: runs-on: ubuntu-20.04 steps: - name: Checkout Kani - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Setup Kani Dependencies uses: ./.github/actions/setup @@ -58,7 +58,7 @@ jobs: runs-on: ubuntu-20.04 steps: - name: Checkout Kani - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Install benchcomp dependencies run: | @@ -81,7 +81,7 @@ jobs: runs-on: ubuntu-20.04 steps: - name: Checkout Kani - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Setup Kani Dependencies uses: ./.github/actions/setup @@ -102,7 +102,7 @@ jobs: contents: write steps: - name: Checkout Kani - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Setup Kani Dependencies uses: ./.github/actions/setup diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index cdc69479d961..81bbf5959347 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -30,7 +30,7 @@ jobs: crate_version: ${{ steps.bundle.outputs.crate_version }} steps: - name: Checkout code - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Setup Kani Dependencies uses: ./.github/actions/setup @@ -135,7 +135,7 @@ jobs: cargo kani setup --use-local-bundle ./${{ matrix.prev_job.bundle }} - name: Checkout tests - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Run tests # TODO: Customize compiletest to run custom kani. For now, just run a few cargo kani tests. @@ -160,7 +160,7 @@ jobs: KANI_SRC: ./kani_src steps: - name: Checkout Kani - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: path: ${{ env.KANI_SRC }} @@ -204,7 +204,7 @@ jobs: upload_url: ${{ steps.create_release.outputs.upload_url }} steps: - name: Checkout code - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Get version run: | @@ -258,7 +258,7 @@ jobs: target: x86_64-unknown-linux-gnu steps: - name: Checkout code - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Setup Kani Dependencies uses: ./.github/actions/setup diff --git a/.github/workflows/slow-tests.yml b/.github/workflows/slow-tests.yml index 2c0a4acd9564..b177b6d5f400 100644 --- a/.github/workflows/slow-tests.yml +++ b/.github/workflows/slow-tests.yml @@ -21,7 +21,7 @@ jobs: os: [macos-12, ubuntu-20.04, ubuntu-22.04] steps: - name: Checkout Kani - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Setup Kani Dependencies uses: ./.github/actions/setup diff --git a/.github/workflows/toolchain-upgrade.yml b/.github/workflows/toolchain-upgrade.yml index 8d54ebe189ff..32266375cb5f 100644 --- a/.github/workflows/toolchain-upgrade.yml +++ b/.github/workflows/toolchain-upgrade.yml @@ -19,7 +19,7 @@ jobs: runs-on: ubuntu-22.04 steps: - name: Checkout Kani - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Setup Kani Dependencies uses: ./.github/actions/setup