Merge branch 'main' into kanicov-tool

.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

Cargo.lock

@@ -156,19 +156,19 @@ 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",
 ]
 
 [[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"

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(|_| {

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 <https://graphviz.org/doc/info/lang.html> for more information.
-    fn dump_dot(&self, tcx: TyCtxt) -> std::io::Result<()> {
+    fn dump_dot(&self, tcx: TyCtxt, initial: Option<MonoItem>) -> 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 {{")?;

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"

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"]

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 \

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<const LEN: usize>([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) };
 }

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<const LEN: usize>([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:
     // ```

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<const LEN: usize>([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:
     // ```

tests/kani/Intrinsics/SIMD/Shuffle/main.rs

@@ -16,28 +16,31 @@ pub struct i64x2([i64; 2]);
 #[derive(Clone, Copy, PartialEq, Eq)]
 pub struct i64x4([i64; 4]);
 
+#[repr(simd)]
+struct SimdShuffleIdx<const LEN: usize>([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);
     }
     {
         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);
     }
     {
         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) };
     }
 }