diff --git a/Cargo.lock b/Cargo.lock index b56cc313e481..f80547d4edcd 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -25,9 +25,9 @@ dependencies = [ [[package]] name = "aho-corasick" -version = "1.0.1" +version = "1.0.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "67fc08ce920c31afb70f013dcce1bfc3a3195de6a228474e45e1f145b36f8d04" +checksum = "43f6cb1bf222025340178f382c426f13757b2960e89779dfcb319c32542a5a41" dependencies = [ "memchr", ] @@ -179,9 +179,9 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" [[package]] name = "clap" -version = "4.3.0" +version = "4.3.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "93aae7a4192245f70fe75dd9157fc7b4a5bf53e88d30bd4396f7d8f9284d5acc" +checksum = "80672091db20273a15cf9fdd4e47ed43b5091ec9841bf4c6145c9dfbbcae09ed" dependencies = [ "clap_builder", "clap_derive", @@ -190,9 +190,9 @@ dependencies = [ [[package]] name = "clap_builder" -version = "4.3.0" +version = "4.3.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4f423e341edefb78c9caba2d9c7f7687d0e72e89df3ce3394554754393ac3990" +checksum = "c1458a1df40e1e2afebb7ab60ce55c1fa8f431146205aa5f4887e0b111c27636" dependencies = [ "anstream", "anstyle", @@ -204,9 +204,9 @@ dependencies = [ [[package]] name = "clap_derive" -version = "4.3.0" +version = "4.3.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "191d9573962933b4027f932c600cd252ce27a8ad5979418fe78e43c07996f27b" +checksum = "b8cd2b2a819ad6eec39e8f1d6b53001af1e5469f8c177579cdaeb313115b825f" dependencies = [ "heck", "proc-macro2", @@ -306,9 +306,9 @@ dependencies = [ [[package]] name = "crossbeam-epoch" -version = "0.9.14" +version = "0.9.15" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "46bd5f3f85273295a9d14aedfb86f6aadbff6d8f5295c4a9edb08e819dcf5695" +checksum = "ae211234986c545741a7dc064309f67ee1e5ad243d0e48335adc0484d960bcc7" dependencies = [ "autocfg", "cfg-if", @@ -319,9 +319,9 @@ dependencies = [ [[package]] name = "crossbeam-utils" -version = "0.8.15" +version = "0.8.16" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3c063cd8cc95f5c377ed0d4b49a4b21f632396ff690e8470c29b3359b346984b" +checksum = "5a22b2d63d4d1dc0b7f1b6b2747dd0088008a9be28b6ddf0b1e7d335e3037294" dependencies = [ "cfg-if", ] @@ -344,9 +344,9 @@ dependencies = [ [[package]] name = "crossterm_winapi" -version = "0.9.0" +version = "0.9.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2ae1b35a484aa10e07fe0638d02301c5ad24de82d310ccbd2f3693da5f09bf1c" +checksum = "acdd7c62a3665c7f6830a51635d9ac9b23ed385797f70a83bb8bafe9c572ab2b" dependencies = [ "winapi", ] @@ -395,9 +395,9 @@ dependencies = [ [[package]] name = "getrandom" -version = "0.2.9" +version = "0.2.10" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c85e1d9ab2eadba7e5040d4e09cbd6d072b76a557ad64e797c2cb9d4da21d7e4" +checksum = "be4136b2a15dd319360be1c07d9933517ccf0be8f16bf62a3bee4f0d618df427" dependencies = [ "cfg-if", "libc", @@ -608,9 +608,9 @@ checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646" [[package]] name = "libc" -version = "0.2.144" +version = "0.2.146" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2b00cc1c228a6782d0f076e7b232802e0c5689d41bb5df366f2a6b6621cfdfe1" +checksum = "f92be4933c13fd498862a9e02a3055f8a8d9c039ce33db97306fd5a6caa7f29b" [[package]] name = "linear-map" @@ -630,9 +630,9 @@ checksum = "ef53942eb7bf7ff43a617b3e2c1c4a5ecf5944a7c1bc12d7ee39bbb15e5c1519" [[package]] name = "lock_api" -version = "0.4.9" +version = "0.4.10" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "435011366fe56583b16cf956f9df0095b405b82d76425bc8981c0e22e60ec4df" +checksum = "c1cc9717a20b1bb222f333e6a92fd32f7d8a18ddc5a3191a11af45dcbf4dcd16" dependencies = [ "autocfg", "scopeguard", @@ -640,9 +640,9 @@ dependencies = [ [[package]] name = "log" -version = "0.4.18" +version = "0.4.19" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "518ef76f2f87365916b142844c16d8fefd85039bc5699050210a7778ee1cd1de" +checksum = "b06a4cde4c0f271a446782e3eff8de789548ce57dbc8eca9292c27f4a42004b4" [[package]] name = "matchers" @@ -661,9 +661,9 @@ checksum = "2dffe52ecf27772e601905b7522cb4ef790d2cc203488bbd0e2fe85fcb74566d" [[package]] name = "memoffset" -version = "0.8.0" +version = "0.9.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d61c719bcfbcf5d62b3a09efa6088de8c54bc0bfcd3ea7ae39fcc186108b8de1" +checksum = "5a634b1c61a95585bd15607c6ab0c4e5b226e695ff2800ba0cdccddf208c406c" dependencies = [ "autocfg", ] @@ -676,9 +676,9 @@ checksum = "2145869435ace5ea6ea3d35f59be559317ec9a0d04e1812d5f185a87b6d36f1a" [[package]] name = "mio" -version = "0.8.7" +version = "0.8.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "eebffdb73fe72e917997fad08bdbf31ac50b0fa91cec93e69a0662e4264d454c" +checksum = "927a765cd3fc26206e66b296465fa9d3e5ab003e651c1b3c060e7956d96b19d2" dependencies = [ "libc", "log", @@ -784,9 +784,9 @@ dependencies = [ [[package]] name = "once_cell" -version = "1.17.2" +version = "1.18.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9670a07f94779e00908f3e686eab508878ebb390ba6e604d3a284c00e8d0487b" +checksum = "dd8b5dd2ae5ed71462c540258bedcb51965123ad7e7ccf4b9a8cafaa4a63576d" [[package]] name = "os_info" @@ -816,15 +816,15 @@ dependencies = [ [[package]] name = "parking_lot_core" -version = "0.9.7" +version = "0.9.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9069cbb9f99e3a5083476ccb29ceb1de18b9118cafa53e90c9551235de2b9521" +checksum = "93f00c865fe7cabf650081affecd3871070f26767e7b2070a3ffae14c654b447" dependencies = [ "cfg-if", "libc", "redox_syscall", "smallvec", - "windows-sys 0.45.0", + "windows-targets 0.48.0", ] [[package]] @@ -871,9 +871,9 @@ dependencies = [ [[package]] name = "proc-macro2" -version = "1.0.59" +version = "1.0.60" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6aeca18b86b413c660b781aa319e4e2648a3e6f9eadc9b47e9038e6fe9f3451b" +checksum = "dec2b086b7a862cf4de201096214fa870344cf922b2b30c167badb3af3195406" dependencies = [ "unicode-ident", ] @@ -952,18 +952,18 @@ dependencies = [ [[package]] name = "redox_syscall" -version = "0.2.16" +version = "0.3.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fb5a58c1855b4b6819d59012155603f0b22ad30cad752600aadfcb695265519a" +checksum = "567664f262709473930a4bf9e51bf2ebf3348f2e748ccc50dea20646858f8f29" dependencies = [ "bitflags", ] [[package]] name = "regex" -version = "1.8.3" +version = "1.8.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "81ca098a9821bd52d6b24fd8b10bd081f47d39c22778cafaa75a2857a62c6390" +checksum = "d0ab3ca65655bb1e41f2a8c8cd662eb4fb035e67c3f78da1d61dffe89d07300f" dependencies = [ "aho-corasick", "memchr", @@ -1006,9 +1006,9 @@ dependencies = [ [[package]] name = "rustix" -version = "0.37.19" +version = "0.37.20" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "acf8729d8542766f1b2cf77eb034d52f40d375bb8b615d0b147089946e16613d" +checksum = "b96e891d04aa506a6d1f318d2771bcb1c7dfda84e126660ace067c9b474bb2c0" dependencies = [ "bitflags", "errno", @@ -1056,18 +1056,18 @@ dependencies = [ [[package]] name = "serde" -version = "1.0.163" +version = "1.0.164" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2113ab51b87a539ae008b5c6c02dc020ffa39afd2d83cffcb3f4eb2722cebec2" +checksum = "9e8c8cf938e98f769bc164923b06dce91cea1751522f46f8466461af04c9027d" dependencies = [ "serde_derive", ] [[package]] name = "serde_derive" -version = "1.0.163" +version = "1.0.164" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8c805777e3930c8883389c602315a24224bcc738b63905ef87cd1420353ea93e" +checksum = "d9735b638ccc51c28bf6914d90a2e9725b377144fc612c49a611fddd1b631d68" dependencies = [ "proc-macro2", "quote", @@ -1096,9 +1096,9 @@ dependencies = [ [[package]] name = "serde_test" -version = "1.0.163" +version = "1.0.164" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "100168a8017b89fd4bcbeb8d857d95a8cfcbde829a7147c09cc82d3ab8d8cb41" +checksum = "797c38160e2546a56e1e3439496439597e938669673ffd8af02a12f070da648f" dependencies = [ "serde", ] @@ -1631,9 +1631,9 @@ checksum = "1a515f5799fe4961cb532f983ce2b23082366b898e52ffbce459c86f67c8378a" [[package]] name = "winnow" -version = "0.4.6" +version = "0.4.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "61de7bac303dc551fe038e2b3cef0f571087a47571ea6e79a87692ac99b99699" +checksum = "ca0ace3845f0d96209f0375e6d367e3eb87eb65d27d445bdc9f1843a26f39448" dependencies = [ "memchr", ] diff --git a/README.md b/README.md index 58d30fa09f3a..74364caeae0a 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,6 @@ ![](./kani-logo.png) -![Kani regression](https://github.com/model-checking/kani/actions/workflows/kani.yml/badge.svg) -![Nightly: CBMC Latest](https://github.com/model-checking/kani/actions/workflows/cbmc-latest.yml/badge.svg) +[![Kani regression](https://github.com/model-checking/kani/actions/workflows/kani.yml/badge.svg)](https://github.com/model-checking/kani/actions/workflows/kani.yml) +[![Nightly: CBMC Latest](https://github.com/model-checking/kani/actions/workflows/cbmc-latest.yml/badge.svg)](https://github.com/model-checking/kani/actions/workflows/cbmc-latest.yml) The Kani Rust Verifier is a bit-precise model checker for Rust. diff --git a/tests/perf/overlays/s2n-quic/quic/s2n-quic-platform/expected b/tests/perf/overlays/s2n-quic/quic/s2n-quic-platform/expected new file mode 100644 index 000000000000..610b05dc4e67 --- /dev/null +++ b/tests/perf/overlays/s2n-quic/quic/s2n-quic-platform/expected @@ -0,0 +1 @@ +successfully verified harnesses, 0 failures diff --git a/tests/perf/overlays/s2n-quic/tools/xdp/s2n-quic-xdp/expected b/tests/perf/overlays/s2n-quic/tools/xdp/s2n-quic-xdp/expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/perf/overlays/s2n-quic/tools/xdp/s2n-quic-xdp/expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/perf/s2n-quic b/tests/perf/s2n-quic index 222bc54f8222..f1df2d64083e 160000 --- a/tests/perf/s2n-quic +++ b/tests/perf/s2n-quic @@ -1 +1 @@ -Subproject commit 222bc54f82224e2bc7ff73346c40eb3c163f08d2 +Subproject commit f1df2d64083e4d1b0f56dc0a298066fdef062bcb diff --git a/tools/build-kani/src/main.rs b/tools/build-kani/src/main.rs index 5c1200e63180..e781f3ceb942 100644 --- a/tools/build-kani/src/main.rs +++ b/tools/build-kani/src/main.rs @@ -19,7 +19,7 @@ fn main() -> Result<()> { let args = parser::ArgParser::parse(); match args.subcommand { - parser::Commands::BuildDev(build_parser) => build_lib().and(build_bin(&build_parser.args)), + parser::Commands::BuildDev(build_parser) => build_lib(&build_bin(&build_parser.args)?), parser::Commands::Bundle(bundle_parser) => { let version_string = bundle_parser.version; let kani_string = format!("kani-{version_string}"); @@ -67,9 +67,8 @@ fn prebundle(dir: &Path) -> Result<()> { } // Before we begin, ensure Kani is built successfully in release mode. - build_bin(&["--release"]) - // And that libraries have been built too. - .and(build_lib()) + // And that libraries have been built too. + build_lib(&build_bin(&["--release"])?) } /// Copy Kani files into `dir` diff --git a/tools/build-kani/src/sysroot.rs b/tools/build-kani/src/sysroot.rs index dc508b8f62ee..3d7e2d1dd5dd 100644 --- a/tools/build-kani/src/sysroot.rs +++ b/tools/build-kani/src/sysroot.rs @@ -56,35 +56,42 @@ pub fn kani_playback_lib() -> PathBuf { } /// Returns the path to where Kani's pre-compiled binaries are stored. -pub fn kani_sysroot_bin() -> PathBuf { +fn kani_sysroot_bin() -> PathBuf { path_buf!(kani_sysroot(), "bin") } /// Build the `lib/` folder and `lib-playback/` for the new sysroot. /// - The `lib/` folder contains the sysroot for verification. /// - The `lib-playback/` folder contains the sysroot used for playback. -pub fn build_lib() -> Result<()> { - build_verification_lib()?; - build_playback_lib() +pub fn build_lib(bin_folder: &Path) -> Result<()> { + let compiler_path = bin_folder.join("kani-compiler"); + build_verification_lib(&compiler_path)?; + build_playback_lib(&compiler_path) } /// Build the `lib/` folder for the new sysroot used during verification. /// This will include Kani's libraries as well as the standard libraries compiled with --emit-mir. -fn build_verification_lib() -> Result<()> { +fn build_verification_lib(compiler_path: &Path) -> Result<()> { let extra_args = ["-Z", "build-std=panic_abort,std,test", "--config", "profile.dev.panic=\"abort\""]; - build_kani_lib(&kani_sysroot_lib(), &extra_args) + let compiler_args = ["--kani-compiler", "-Cllvm-args=--ignore-global-asm"]; + build_kani_lib(compiler_path, &kani_sysroot_lib(), &extra_args, &compiler_args) } /// Build the `lib-playback/` folder that will be used during counter example playback. /// This will include Kani's libraries compiled with `concrete-playback` feature enabled. -fn build_playback_lib() -> Result<()> { +fn build_playback_lib(compiler_path: &Path) -> Result<()> { let extra_args = ["--features=std/concrete_playback,kani/concrete_playback", "-Z", "build-std=std,test"]; - build_kani_lib(&kani_playback_lib(), &extra_args) + build_kani_lib(compiler_path, &kani_playback_lib(), &extra_args, &[]) } -fn build_kani_lib(path: &Path, extra_args: &[&str]) -> Result<()> { +fn build_kani_lib( + compiler_path: &Path, + output_path: &Path, + extra_cargo_args: &[&str], + extra_rustc_args: &[&str], +) -> Result<()> { // Run cargo build with -Z build-std let target = env!("TARGET"); let target_dir = env!("KANI_BUILD_LIBS"); @@ -117,13 +124,13 @@ fn build_kani_lib(path: &Path, extra_args: &[&str]) -> Result<()> { "--message-format", "json-diagnostic-rendered-ansi", ]; + let mut rustc_args = vec!["--cfg=kani", "--cfg=kani_sysroot", "-Z", "always-encode-mir"]; + rustc_args.extend_from_slice(extra_rustc_args); let mut cmd = Command::new("cargo") - .env( - "CARGO_ENCODED_RUSTFLAGS", - ["--cfg=kani", "--cfg=kani_sysroot", "-Z", "always-encode-mir"].join("\x1f"), - ) + .env("CARGO_ENCODED_RUSTFLAGS", rustc_args.join("\x1f")) + .env("RUSTC", compiler_path) .args(args) - .args(extra_args) + .args(extra_cargo_args) .stdout(Stdio::piped()) .spawn() .expect("Failed to run `cargo build`."); @@ -138,7 +145,7 @@ fn build_kani_lib(path: &Path, extra_args: &[&str]) -> Result<()> { } // Create sysroot folder hierarchy. - copy_artifacts(&artifacts, path, target) + copy_artifacts(&artifacts, output_path, target) } /// Copy all the artifacts to their correct place to generate a valid sysroot. @@ -225,18 +232,20 @@ fn build_artifacts(cargo_cmd: &mut Child) -> Vec { .collect() } +/// Build Kani binaries with the extra arguments provided and return the path to the binaries folder. /// Extra arguments to be given to `cargo build` while building Kani's binaries. /// Note that the following arguments are always provided: /// ```bash /// cargo build --bins -Z unstable-options --out-dir $KANI_SYSROOT/bin/ /// ``` -pub fn build_bin>(extra_args: &[T]) -> Result<()> { +pub fn build_bin>(extra_args: &[T]) -> Result { let out_dir = kani_sysroot_bin(); let args = ["--bins", "-Z", "unstable-options", "--out-dir", out_dir.to_str().unwrap()]; Command::new("cargo") .arg("build") - .args(args) .args(extra_args) + .args(args) .run() - .or(Err(format_err!("Failed to build binaries."))) + .or(Err(format_err!("Failed to build binaries.")))?; + Ok(out_dir) }