diff --git a/.github/workflows/cbmc-update.yml b/.github/workflows/cbmc-update.yml index 7b63c0dae7de..8d0bc057da2f 100644 --- a/.github/workflows/cbmc-update.yml +++ b/.github/workflows/cbmc-update.yml @@ -51,6 +51,8 @@ jobs: sed -i "s/^CBMC_MINOR=.*/CBMC_MINOR=\"$CBMC_LATEST_MINOR\"/" kani-dependencies sed -i "s/^CBMC_VERSION=.*/CBMC_VERSION=\"$CBMC_LATEST\"/" kani-dependencies git diff + # install the newer CBMC version + ./scripts/setup/ubuntu/install_cbmc.sh if ! ./scripts/kani-regression.sh ; then echo "next_step=create_issue" >> $GITHUB_ENV else diff --git a/Cargo.lock b/Cargo.lock index 7e7beedabf4a..404d463ffd6d 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -156,9 +156,9 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" [[package]] name = "clap" -version = "4.5.17" +version = "4.5.18" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3e5a21b8495e732f1b3c364c9949b201ca7bae518c502c80256c96ad79eaf6ac" +checksum = "b0956a43b323ac1afaffc053ed5c4b7c1f1800bacd1683c353aabbb752515dd3" dependencies = [ "clap_builder", "clap_derive", @@ -166,9 +166,9 @@ dependencies = [ [[package]] name = "clap_builder" -version = "4.5.17" +version = "4.5.18" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8cf2dd12af7a047ad9d6da2b6b249759a22a7abc0f474c1dae1777afa4b21a73" +checksum = "4d72166dd41634086d5803a47eb71ae740e61d84709c36f3c34110173db3961b" dependencies = [ "anstream", "anstyle", @@ -178,9 +178,9 @@ dependencies = [ [[package]] name = "clap_derive" -version = "4.5.13" +version = "4.5.18" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "501d359d5f3dcaf6ecdeee48833ae73ec6e42723a1e52419c79abf9507eec0a0" +checksum = "4ac6a0c7b1a9e9a5186361f67dfa1b88213572f427fb9ab038efb2bd8c582dab" dependencies = [ "heck", "proc-macro2", @@ -1192,18 +1192,18 @@ dependencies = [ [[package]] name = "thiserror" -version = "1.0.63" +version = "1.0.64" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c0342370b38b6a11b6cc11d6a805569958d54cfa061a29969c3b5ce2ea405724" +checksum = "d50af8abc119fb8bb6dbabcfa89656f46f84aa0ac7688088608076ad2b459a84" dependencies = [ "thiserror-impl", ] [[package]] name = "thiserror-impl" -version = "1.0.63" +version = "1.0.64" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a4558b58466b9ad7ca0f102865eccc95938dca1a74a856f2b57b6629050da261" +checksum = "08904e7672f5eb876eaaf87e0ce17857500934f4981c4a0ab2b4aa98baac7fc3" dependencies = [ "proc-macro2", "quote", @@ -1274,9 +1274,9 @@ dependencies = [ [[package]] name = "toml_edit" -version = "0.22.20" +version = "0.22.21" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "583c44c02ad26b0c3f3066fe629275e50627026c51ac2e595cca4c230ce1ce1d" +checksum = "3b072cee73c449a636ffd6f32bd8de3a9f7119139aff882f44943ce2986dc5cf" dependencies = [ "indexmap", "serde", @@ -1408,9 +1408,9 @@ checksum = "e91b56cd4cadaeb79bbf1a5645f6b4f8dc5bde8834ad5894a8db35fda9efa1fe" [[package]] name = "unicode-width" -version = "0.1.13" +version = "0.1.14" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0336d538f7abc86d282a4189614dfaa90810dfc2c6f6427eaf88e16311dd225d" +checksum = "7dd6e30e90baa6f72411720665d41d89b9a3d039dc45b8faea1ddd07f617f6af" [[package]] name = "unsafe-libyaml" diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 1b4c0174d5ed..4b66d60e735b 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -1243,35 +1243,27 @@ impl<'tcx> GotocCtx<'tcx> { /// 1. `simd_shuffleN`, where `N` is a number which is part of the name /// (e.g., `simd_shuffle4`). /// 2. `simd_shuffle`, where `N` isn't specified and must be computed from - /// the length of the indexes array (the third argument). + /// the length of the indexes SIMD vector (the third argument). fn simd_shuffle_length(&mut self, stripped: &str, farg_types: &[Ty], span: Span) -> u64 { let n = if stripped.is_empty() { - // Make sure that this is an array, since only the + // Make sure that this is an SIMD vector, since only the // length-suffixed version of `simd_shuffle` (e.g., // `simd_shuffle4`) is type-checked - match farg_types[2].kind() { - TyKind::RigidTy(RigidTy::Array(ty, len)) - if matches!(ty.kind(), TyKind::RigidTy(RigidTy::Uint(UintTy::U32))) => - { - len.eval_target_usize().unwrap_or_else(|err| { - utils::span_err( - self.tcx, - span, - format!("could not evaluate shuffle index array length: {err}"), - ); - // Return a dummy value - u64::MIN - }) - } - _ => { - let err_msg = format!( - "simd_shuffle index must be an array of `u32`, got `{}`", - self.pretty_ty(farg_types[2]) - ); - utils::span_err(self.tcx, span, err_msg); - // Return a dummy value - u64::MIN - } + if farg_types[2].kind().is_simd() + && matches!( + self.simd_size_and_type(farg_types[2]).1.kind(), + TyKind::RigidTy(RigidTy::Uint(UintTy::U32)) + ) + { + self.simd_size_and_type(farg_types[2]).0 + } else { + let err_msg = format!( + "simd_shuffle index must be a SIMD vector of `u32`, got `{}`", + self.pretty_ty(farg_types[2]) + ); + utils::span_err(self.tcx, span, err_msg); + // Return a dummy value + u64::MIN } } else { stripped.parse().unwrap_or_else(|_| { diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index d2c9d50515c4..b808a5c5b8ee 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -60,7 +60,7 @@ pub fn collect_reachable_items( #[cfg(debug_assertions)] collector .call_graph - .dump_dot(tcx) + .dump_dot(tcx, starting_points.first().cloned()) .unwrap_or_else(|e| tracing::error!("Failed to dump call graph: {e}")); tcx.dcx().abort_if_errors(); @@ -579,12 +579,18 @@ impl CallGraph { /// Print the graph in DOT format to a file. /// See for more information. - fn dump_dot(&self, tcx: TyCtxt) -> std::io::Result<()> { + fn dump_dot(&self, tcx: TyCtxt, initial: Option) -> std::io::Result<()> { if let Ok(target) = std::env::var("KANI_REACH_DEBUG") { debug!(?target, "dump_dot"); + let name = initial.map(|item| Node(item).to_string()).unwrap_or_default(); let outputs = tcx.output_filenames(()); let base_path = outputs.path(OutputType::Metadata); - let path = base_path.as_path().with_extension("dot"); + let file_stem = format!( + "{}_{}.dot", + base_path.as_path().file_stem().unwrap().to_string_lossy(), + name + ); + let path = base_path.as_path().parent().unwrap().join(file_stem); let out_file = File::create(path)?; let mut writer = BufWriter::new(out_file); writeln!(writer, "digraph ReachabilityGraph {{")?; diff --git a/kani-dependencies b/kani-dependencies index 421188a08762..6f844839086c 100644 --- a/kani-dependencies +++ b/kani-dependencies @@ -1,6 +1,6 @@ CBMC_MAJOR="6" -CBMC_MINOR="1" -CBMC_VERSION="6.1.1" +CBMC_MINOR="3" +CBMC_VERSION="6.3.1" # If you update this version number, remember to bump it in `src/setup.rs` too CBMC_VIEWER_MAJOR="3" diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 934515867187..7cd260ede123 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2024-09-12" +channel = "nightly-2024-09-17" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] diff --git a/scripts/setup/al2/install_cbmc.sh b/scripts/setup/al2/install_cbmc.sh index 3bac22ace3db..81c476dab440 100755 --- a/scripts/setup/al2/install_cbmc.sh +++ b/scripts/setup/al2/install_cbmc.sh @@ -21,80 +21,6 @@ git clone \ pushd "${WORK_DIR}" -# apply workaround for https://github.com/diffblue/cbmc/issues/8357 until it is -# properly fixed in CBMC -cat > varargs.patch << "EOF" ---- a/src/ansi-c/library/stdio.c -+++ b/src/ansi-c/library/stdio.c -@@ -1135,7 +1135,7 @@ int vfscanf(FILE *restrict stream, const char *restrict format, va_list arg) - - (void)*format; - while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&arg) < -- __CPROVER_OBJECT_SIZE(arg)) -+ __CPROVER_OBJECT_SIZE(*(void **)&arg)) - { - void *a = va_arg(arg, void *); - __CPROVER_havoc_object(a); -@@ -1233,7 +1233,7 @@ int __stdio_common_vfscanf( - - (void)*format; - while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&args) < -- __CPROVER_OBJECT_SIZE(args)) -+ __CPROVER_OBJECT_SIZE(*(void **)&args)) - { - void *a = va_arg(args, void *); - __CPROVER_havoc_object(a); -@@ -1312,7 +1312,7 @@ __CPROVER_HIDE:; - (void)*s; - (void)*format; - while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&arg) < -- __CPROVER_OBJECT_SIZE(arg)) -+ __CPROVER_OBJECT_SIZE(*(void **)&arg)) - { - void *a = va_arg(arg, void *); - __CPROVER_havoc_object(a); -@@ -1388,7 +1388,7 @@ int __stdio_common_vsscanf( - (void)*s; - (void)*format; - while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&args) < -- __CPROVER_OBJECT_SIZE(args)) -+ __CPROVER_OBJECT_SIZE(*(void **)&args)) - { - void *a = va_arg(args, void *); - __CPROVER_havoc_object(a); -@@ -1774,12 +1774,12 @@ int vsnprintf(char *str, size_t size, const char *fmt, va_list ap) - (void)*fmt; - - while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&ap) < -- __CPROVER_OBJECT_SIZE(ap)) -+ __CPROVER_OBJECT_SIZE(*(void **)&ap)) - - { - (void)va_arg(ap, int); - __CPROVER_precondition( -- __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap), -+ __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(*(void **)&ap), - "vsnprintf object overlap"); - } - -@@ -1822,12 +1822,12 @@ int __builtin___vsnprintf_chk( - (void)*fmt; - - while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&ap) < -- __CPROVER_OBJECT_SIZE(ap)) -+ __CPROVER_OBJECT_SIZE(*(void **)&ap)) - - { - (void)va_arg(ap, int); - __CPROVER_precondition( -- __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap), -+ __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(*(void **)&ap), - "vsnprintf object overlap"); - } - -EOF -patch -p1 < varargs.patch - cmake3 -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical" \ -DCMAKE_C_COMPILER=gcc10-cc -DCMAKE_CXX_COMPILER=gcc10-c++ \ -DCMAKE_CXX_STANDARD_LIBRARIES=-lstdc++fs \ diff --git a/tests/expected/intrinsics/simd-shuffle-indexes-out/main.rs b/tests/expected/intrinsics/simd-shuffle-indexes-out/main.rs index b89f40369853..a9da5c773743 100644 --- a/tests/expected/intrinsics/simd-shuffle-indexes-out/main.rs +++ b/tests/expected/intrinsics/simd-shuffle-indexes-out/main.rs @@ -11,11 +11,14 @@ use std::intrinsics::simd::simd_shuffle; #[derive(Clone, Copy, PartialEq, Eq)] pub struct i64x2([i64; 2]); +#[repr(simd)] +struct SimdShuffleIdx([u32; LEN]); + #[kani::proof] fn main() { let y = i64x2([0, 1]); let z = i64x2([1, 2]); // Only [0, 3] are valid indexes, 4 is out of bounds - const I: [u32; 2] = [1, 4]; + const I: SimdShuffleIdx<2> = SimdShuffleIdx([1, 4]); let _: i64x2 = unsafe { simd_shuffle(y, z, I) }; } diff --git a/tests/expected/intrinsics/simd-shuffle-result-type-is-diff-size/main.rs b/tests/expected/intrinsics/simd-shuffle-result-type-is-diff-size/main.rs index 3fe534f3bc08..3936f39ed318 100644 --- a/tests/expected/intrinsics/simd-shuffle-result-type-is-diff-size/main.rs +++ b/tests/expected/intrinsics/simd-shuffle-result-type-is-diff-size/main.rs @@ -16,11 +16,14 @@ pub struct i64x2([i64; 2]); #[derive(Clone, Copy, PartialEq, Eq)] pub struct i64x4([i64; 4]); +#[repr(simd)] +struct SimdShuffleIdx([u32; LEN]); + #[kani::proof] fn main() { let y = i64x2([0, 1]); let z = i64x2([1, 2]); - const I: [u32; 4] = [1, 2, 1, 2]; + const I: SimdShuffleIdx<4> = SimdShuffleIdx([1, 2, 1, 2]); let x: i64x2 = unsafe { simd_shuffle(y, z, I) }; // ^^^^ The code above fails to type-check in Rust with the error: // ``` diff --git a/tests/expected/intrinsics/simd-shuffle-result-type-is-diff-type/main.rs b/tests/expected/intrinsics/simd-shuffle-result-type-is-diff-type/main.rs index 8c7cd5245cbe..7f8c511a96e5 100644 --- a/tests/expected/intrinsics/simd-shuffle-result-type-is-diff-type/main.rs +++ b/tests/expected/intrinsics/simd-shuffle-result-type-is-diff-type/main.rs @@ -16,11 +16,14 @@ pub struct i64x2([i64; 2]); #[derive(Clone, Copy, PartialEq)] pub struct f64x2([f64; 2]); +#[repr(simd)] +struct SimdShuffleIdx([u32; LEN]); + #[kani::proof] fn main() { let y = i64x2([0, 1]); let z = i64x2([1, 2]); - const I: [u32; 2] = [1, 2]; + const I: SimdShuffleIdx<2> = SimdShuffleIdx([1, 2]); let x: f64x2 = unsafe { simd_shuffle(y, z, I) }; // ^^^^ The code above fails to type-check in Rust with the error: // ``` diff --git a/tests/kani/Intrinsics/SIMD/Shuffle/main.rs b/tests/kani/Intrinsics/SIMD/Shuffle/main.rs index a105a3b1d81e..b20c16be5877 100644 --- a/tests/kani/Intrinsics/SIMD/Shuffle/main.rs +++ b/tests/kani/Intrinsics/SIMD/Shuffle/main.rs @@ -16,12 +16,15 @@ pub struct i64x2([i64; 2]); #[derive(Clone, Copy, PartialEq, Eq)] pub struct i64x4([i64; 4]); +#[repr(simd)] +struct SimdShuffleIdx([u32; LEN]); + #[kani::proof] fn main() { { let y = i64x2([0, 1]); let z = i64x2([1, 2]); - const I: [u32; 2] = [1, 2]; + const I: SimdShuffleIdx<2> = SimdShuffleIdx([1, 2]); let x: i64x2 = unsafe { simd_shuffle(y, z, I) }; assert!(x.0[0] == 1); assert!(x.0[1] == 1); @@ -29,7 +32,7 @@ fn main() { { let y = i64x2([0, 1]); let z = i64x2([1, 2]); - const I: [u32; 2] = [1, 2]; + const I: SimdShuffleIdx<2> = SimdShuffleIdx([1, 2]); let x: i64x2 = unsafe { simd_shuffle(y, z, I) }; assert!(x.0[0] == 1); assert!(x.0[1] == 1); @@ -37,7 +40,7 @@ fn main() { { let a = i64x4([1, 2, 3, 4]); let b = i64x4([5, 6, 7, 8]); - const I: [u32; 4] = [1, 3, 5, 7]; + const I: SimdShuffleIdx<4> = SimdShuffleIdx([1, 3, 5, 7]); let c: i64x4 = unsafe { simd_shuffle(a, b, I) }; assert!(c == i64x4([2, 4, 6, 8])); } @@ -48,7 +51,7 @@ fn check_shuffle() { { let y = i64x2([0, 1]); let z = i64x2([1, 2]); - const I: [u32; 4] = [1, 2, 0, 3]; + const I: SimdShuffleIdx<4> = SimdShuffleIdx([1, 2, 0, 3]); let _x: i64x4 = unsafe { simd_shuffle(y, z, I) }; } } diff --git a/tests/perf/s2n-quic b/tests/perf/s2n-quic index 132ba54b6ff7..a88ae4191af1 160000 --- a/tests/perf/s2n-quic +++ b/tests/perf/s2n-quic @@ -1 +1 @@ -Subproject commit 132ba54b6ff7406204b866eb644594201d6be8d7 +Subproject commit a88ae4191af100747404db207976c7da1a3b8370