Merge remote-tracking branch 'origin/main' into release-kani-0.57.0

cprover_bindings/Cargo.toml

@@ -17,7 +17,7 @@ lazy_static = "1.4.0"
 num = "0.4.0"
 num-traits = "0.2"
 serde = {version = "1", features = ["derive"]}
-string-interner = "0.17.0"
+string-interner = "0.18"
 tracing = "0.1"
 linear-map = {version = "1.2", features = ["serde_impl"]}
 

deny.toml

@@ -16,14 +16,13 @@ yanked = "deny"
 allow = [
     "MIT",
     "Apache-2.0",
-    "MPL-2.0",
 ]
 confidence-threshold = 0.8
 
 # All these exceptions should probably appear in: tools/build-kani/license-notes.txt
 exceptions = [
     { name = "unicode-ident", allow=["Unicode-3.0"] },
-    { name = "rustc_apfloat", allow=["Apache-2.0 WITH LLVM-exception"] },
+    { name = "foldhash", allow=["Zlib"] },
 ]
 
 [licenses.private]
@@ -43,4 +42,3 @@ wildcards = "allow"
 unknown-registry = "deny"
 unknown-git = "deny"
 allow-registry = ["https://github.com/rust-lang/crates.io-index"]
-allow-git = ["https://github.com/Nadrieril/tracing-tree"]

kani-driver/Cargo.toml

@@ -13,7 +13,7 @@ publish = false
 
 [dependencies]
 kani_metadata = { path = "../kani_metadata" }
-cargo_metadata = "0.18.0"
+cargo_metadata = "0.19"
 anyhow = "1"
 console = "0.15.1"
 once_cell = "1.19.0"
@@ -35,7 +35,7 @@ tempfile = "3"
 tracing = {version = "0.1", features = ["max_level_trace", "release_max_level_debug"]}
 tracing-subscriber = {version = "0.3.8", features = ["env-filter", "json", "fmt"]}
 rand = "0.8"
-which = "6"
+which = "7"
 time = {version = "0.3.36", features = ["formatting"]}
 tokio = { version = "1.40.0", features = ["io-util", "process", "rt", "time"] }
 

kani-driver/src/call_cargo.rs

@@ -9,7 +9,8 @@ use crate::util;
 use anyhow::{Context, Result, bail};
 use cargo_metadata::diagnostic::{Diagnostic, DiagnosticLevel};
 use cargo_metadata::{
-    Artifact as RustcArtifact, Message, Metadata, MetadataCommand, Package, PackageId, Target,
+    Artifact as RustcArtifact, CrateType, Message, Metadata, MetadataCommand, Package, PackageId,
+    Target, TargetKind,
 };
 use kani_metadata::{ArtifactType, CompilerArtifactStub};
 use std::collections::HashMap;
@@ -22,16 +23,6 @@ use std::path::{Path, PathBuf};
 use std::process::Command;
 use tracing::{debug, trace};
 
-//---- Crate types identifier used by cargo.
-const CRATE_TYPE_BIN: &str = "bin";
-const CRATE_TYPE_CDYLIB: &str = "cdylib";
-const CRATE_TYPE_DYLIB: &str = "dylib";
-const CRATE_TYPE_LIB: &str = "lib";
-const CRATE_TYPE_PROC_MACRO: &str = "proc-macro";
-const CRATE_TYPE_RLIB: &str = "rlib";
-const CRATE_TYPE_STATICLIB: &str = "staticlib";
-const CRATE_TYPE_TEST: &str = "test";
-
 /// The outputs of kani-compiler being invoked via cargo on a project.
 pub struct CargoOutputs {
     /// The directory where compiler outputs should be directed.
@@ -123,8 +114,8 @@ crate-type = ["lib"]
             .run_build(cmd)?
             .into_iter()
             .filter_map(|artifact| {
-                if artifact.target.crate_types.contains(&CRATE_TYPE_LIB.to_string())
-                    || artifact.target.crate_types.contains(&CRATE_TYPE_RLIB.to_string())
+                if artifact.target.crate_types.contains(&CrateType::Lib)
+                    || artifact.target.crate_types.contains(&CrateType::RLib)
                 {
                     map_kani_artifact(artifact)
                 } else {
@@ -576,26 +567,29 @@ fn package_targets(args: &VerificationArgs, package: &Package) -> Vec<Verificati
                 "package_targets");
         let (mut supported_lib, mut unsupported_lib) = (false, false);
         for kind in &target.kind {
-            match kind.as_str() {
-                CRATE_TYPE_BIN => {
+            match kind {
+                TargetKind::Bin => {
                     if args.target.include_bin(&target.name) {
                         // Binary targets.
                         verification_targets.push(VerificationTarget::Bin(target.clone()));
                     }
                 }
-                CRATE_TYPE_LIB | CRATE_TYPE_RLIB | CRATE_TYPE_CDYLIB | CRATE_TYPE_DYLIB
-                | CRATE_TYPE_STATICLIB => {
+                TargetKind::Lib
+                | TargetKind::RLib
+                | TargetKind::CDyLib
+                | TargetKind::DyLib
+                | TargetKind::StaticLib => {
                     if args.target.include_lib() {
                         supported_lib = true;
                     }
                 }
-                CRATE_TYPE_PROC_MACRO => {
+                TargetKind::ProcMacro => {
                     if args.target.include_lib() {
                         unsupported_lib = true;
                         ignored_unsupported.push(target.name.as_str());
                     }
                 }
-                CRATE_TYPE_TEST => {
+                TargetKind::Test => {
                     // Test target.
                     if args.target.include_tests() {
                         if args.tests {

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2024-12-13"
+channel = "nightly-2024-12-14"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

tools/build-kani/Cargo.toml

@@ -11,6 +11,6 @@ publish = false
 
 [dependencies]
 anyhow = "1"
-cargo_metadata = "0.18.0"
+cargo_metadata = "0.19"
 clap = { version = "4.4.11", features=["derive"] }
-which = "6"
+which = "7"

tools/build-kani/src/sysroot.rs

@@ -13,7 +13,7 @@
 
 use crate::{AutoRun, cp};
 use anyhow::{Result, bail, format_err};
-use cargo_metadata::{Artifact, Message};
+use cargo_metadata::{Artifact, Message, TargetKind};
 use std::ffi::OsStr;
 use std::fs;
 use std::io::BufReader;
@@ -194,9 +194,13 @@ fn copy_artifacts(artifacts: &[Artifact], sysroot_lib: &Path, copy_std: bool) ->
 /// Check if an artifact is a rust library that can be used by rustc on further crates compilations.
 /// This inspects the kind of targets that this artifact originates from.
 fn is_rust_lib(artifact: &Artifact) -> bool {
-    artifact.target.kind.iter().any(|kind| match kind.as_str() {
-        "lib" | "rlib" | "proc-macro" => true,
-        "bin" | "dylib" | "cdylib" | "staticlib" | "custom-build" => false,
+    artifact.target.kind.iter().any(|kind| match kind {
+        TargetKind::Lib | TargetKind::RLib | TargetKind::ProcMacro => true,
+        TargetKind::Bin
+        | TargetKind::DyLib
+        | TargetKind::CDyLib
+        | TargetKind::StaticLib
+        | TargetKind::CustomBuild => false,
         _ => unreachable!("Unknown crate type {kind}"),
     })
 }

tools/kani-cov/Cargo.toml

@@ -17,5 +17,5 @@ console = "0.15.8"
 serde = "1.0.197"
 serde_derive = "1.0.197"
 serde_json = "1.0.115"
-tree-sitter = "0.23.0"
-tree-sitter-rust = "0.21.2"
+tree-sitter = "0.24"
+tree-sitter-rust = "0.23"

tools/kani-cov/src/coverage.rs

@@ -154,7 +154,7 @@ pub struct FunctionInfo {
 pub fn function_info_from_file(filepath: &PathBuf) -> Vec<FunctionInfo> {
     let source_code = fs::read_to_string(filepath).expect("could not read source file");
     let mut parser = Parser::new();
-    parser.set_language(&tree_sitter_rust::language()).expect("Error loading Rust grammar");
+    parser.set_language(&tree_sitter_rust::LANGUAGE.into()).expect("Error loading Rust grammar");
 
     let tree = parser.parse(&source_code, None).expect("Failed to parse file");