diff --git a/CHANGELOG.md b/CHANGELOG.md index 37f29f7df732..659057b2a987 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,6 +4,20 @@ This file contains notable changes (e.g. breaking changes, major changes, etc.) This file was introduced starting Kani 0.23.0, so it only contains changes from version 0.23.0 onwards. +## [0.32.0] + +## What's Changed + +* Add kani::spawn and an executor to the Kani library by @fzaiser in https://github.com/model-checking/kani/pull/1659 +* Add "kani" configuration key to enable conditional compilation in build scripts by @celinval in https://github.com/model-checking/kani/pull/2297 +* Adds posix_memalign to the list of supported builtins by @feliperodri in https://github.com/model-checking/kani/pull/2601 +* Upgrade rust toolchain to nightly-2023-06-20 by @celinval in https://github.com/model-checking/kani/pull/2551 +* Update rust toolchain to 2023-06-22 by @celinval in https://github.com/model-checking/kani/pull/2588 +* Automatic toolchain upgrade to nightly-2023-06-24 by @github-actions in https://github.com/model-checking/kani/pull/2600 +* Bump CBMC version to 5.87.0 by @adpaco-aws in https://github.com/model-checking/kani/pull/2598 + +**Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.31.0...kani-0.32.0 + ## [0.31.0] ## What's Changed diff --git a/Cargo.lock b/Cargo.lock index 4660575954f2..0847cd2f318a 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -87,17 +87,6 @@ version = "1.0.71" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9c7d0618f0e0b7e8ff11427422b64564d5fb0be1940354bfe2e0529b18a9d9b8" -[[package]] -name = "atty" -version = "0.2.14" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d9b39be18770d11421cdb1b9947a45dd3f37e93092cbf377614828a319d5fee8" -dependencies = [ - "hermit-abi 0.1.19", - "libc", - "winapi", -] - [[package]] name = "autocfg" version = "1.1.0" @@ -110,6 +99,12 @@ version = "1.3.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a" +[[package]] +name = "bitflags" +version = "2.3.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "630be753d4e58660abd17930c71b647fe46c27ea6b63cc59e1e3851406972e42" + [[package]] name = "bookrunner" version = "0.1.0" @@ -125,7 +120,7 @@ dependencies = [ [[package]] name = "build-kani" -version = "0.31.0" +version = "0.32.0" dependencies = [ "anyhow", "cargo_metadata", @@ -179,9 +174,9 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" [[package]] name = "clap" -version = "4.3.8" +version = "4.3.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d9394150f5b4273a1763355bd1c2ec54cc5a2593f790587bcd6b2c947cfa9211" +checksum = "1640e5cc7fb47dbb8338fd471b105e7ed6c3cb2aeb00c2e067127ffd3764a05d" dependencies = [ "clap_builder", "clap_derive", @@ -190,13 +185,12 @@ dependencies = [ [[package]] name = "clap_builder" -version = "4.3.8" +version = "4.3.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9a78fbdd3cc2914ddf37ba444114bc7765bbdcb55ec9cbe6fa054f0137400717" +checksum = "98c59138d527eeaf9b53f35a77fcc1fad9d883116070c63d5de1c7dc7b00c72b" dependencies = [ "anstream", "anstyle", - "bitflags", "clap_lex", "once_cell", "strsim", @@ -211,7 +205,7 @@ dependencies = [ "heck", "proc-macro2", "quote", - "syn 2.0.22", + "syn 2.0.25", ] [[package]] @@ -270,7 +264,7 @@ dependencies = [ [[package]] name = "cprover_bindings" -version = "0.31.0" +version = "0.32.0" dependencies = [ "lazy_static", "linear-map", @@ -332,7 +326,7 @@ version = "0.26.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "a84cda67535339806297f1b331d6dd6320470d2a0fe65381e79ee9e156dd3d13" dependencies = [ - "bitflags", + "bitflags 1.3.2", "crossterm_winapi", "libc", "mio", @@ -439,27 +433,9 @@ checksum = "95505c38b4572b2d910cecb0281560f54b440a19336cbbcb27bf6ce6adc6f5a8" [[package]] name = "hermit-abi" -version = "0.1.19" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "62b467343b94ba476dcb2500d242dadbb39557df889310ac77c5d99100aaac33" -dependencies = [ - "libc", -] - -[[package]] -name = "hermit-abi" -version = "0.2.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ee512640fe35acbfb4bb779db6f0d80704c2cacfa2e39b601ef3e3f47d1ae4c7" -dependencies = [ - "libc", -] - -[[package]] -name = "hermit-abi" -version = "0.3.1" +version = "0.3.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fed44880c466736ef9a5c5b5facefb5ed0785676d0c02d612db14e54f0d84286" +checksum = "443144c8cdadd93ebf52ddb4056d257f5b52c04d3c804e657d19eb73fc33668b" [[package]] name = "home" @@ -480,25 +456,13 @@ dependencies = [ "hashbrown 0.14.0", ] -[[package]] -name = "io-lifetimes" -version = "1.0.11" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "eae7b9aee968036d54dce06cebaefd919e4472e753296daccd6d344e3e2df0c2" -dependencies = [ - "hermit-abi 0.3.1", - "libc", - "windows-sys 0.48.0", -] - [[package]] name = "is-terminal" -version = "0.4.7" +version = "0.4.9" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "adcf93614601c8129ddf72e2d5633df827ba6551541c6d8c59520a371475be1f" +checksum = "cb0889898416213fab133e1d33a0e5858a48177452750691bde3666d0fdbaf8b" dependencies = [ - "hermit-abi 0.3.1", - "io-lifetimes", + "hermit-abi", "rustix", "windows-sys 0.48.0", ] @@ -514,22 +478,21 @@ dependencies = [ [[package]] name = "itoa" -version = "1.0.6" +version = "1.0.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "453ad9f582a441959e5f0d088b02ce04cfe8d51a8eaf077f12ac6d3e94164ca6" +checksum = "62b02a5381cc465bd3041d84623d0fa3b66738b52b8e2fc3bab8ad63ab032f4a" [[package]] name = "kani" -version = "0.31.0" +version = "0.32.0" dependencies = [ "kani_macros", ] [[package]] name = "kani-compiler" -version = "0.31.0" +version = "0.32.0" dependencies = [ - "atty", "clap", "cprover_bindings", "home", @@ -545,15 +508,13 @@ dependencies = [ "strum_macros", "tracing", "tracing-subscriber", - "tracing-tree", ] [[package]] name = "kani-driver" -version = "0.31.0" +version = "0.32.0" dependencies = [ "anyhow", - "atty", "cargo_metadata", "clap", "comfy-table", @@ -573,13 +534,12 @@ dependencies = [ "toml", "tracing", "tracing-subscriber", - "tracing-tree", "which", ] [[package]] name = "kani-verifier" -version = "0.31.0" +version = "0.32.0" dependencies = [ "anyhow", "home", @@ -588,17 +548,17 @@ dependencies = [ [[package]] name = "kani_macros" -version = "0.31.0" +version = "0.32.0" dependencies = [ "proc-macro-error", "proc-macro2", "quote", - "syn 2.0.22", + "syn 2.0.25", ] [[package]] name = "kani_metadata" -version = "0.31.0" +version = "0.32.0" dependencies = [ "cprover_bindings", "serde", @@ -630,9 +590,9 @@ dependencies = [ [[package]] name = "linux-raw-sys" -version = "0.3.8" +version = "0.4.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ef53942eb7bf7ff43a617b3e2c1c4a5ecf5944a7c1bc12d7ee39bbb15e5c1519" +checksum = "09fc20d2ca12cb9f044c93e3bd6d32d523e6e2ec3db4f7b2939cd99026ecd3f0" [[package]] name = "lock_api" @@ -656,7 +616,7 @@ version = "0.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "8263075bb86c5a1b1427b5ae862e8889656f126e9f77c484496e8b47cf5c5558" dependencies = [ - "regex-automata", + "regex-automata 0.1.10", ] [[package]] @@ -780,11 +740,11 @@ dependencies = [ [[package]] name = "num_cpus" -version = "1.15.0" +version = "1.16.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0fac9e2da13b5eb447a6ce3d392f23a29d8694bff781bf03a16cd9ac8697593b" +checksum = "4161fcb6d602d4d2081af7c3a45852d875a03dd337a6bfdd6e06407b61342a43" dependencies = [ - "hermit-abi 0.2.6", + "hermit-abi", "libc", ] @@ -830,7 +790,7 @@ dependencies = [ "libc", "redox_syscall", "smallvec", - "windows-targets 0.48.0", + "windows-targets 0.48.1", ] [[package]] @@ -841,9 +801,9 @@ checksum = "8835116a5c179084a830efb3adc117ab007512b535bc1a21c991d3b32a6b44dd" [[package]] name = "pin-project-lite" -version = "0.2.9" +version = "0.2.10" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e0a7ae3ac2f1173085d398531c705756c94a4c56843785df85a60c1a0afac116" +checksum = "4c40d25201921e5ff0c862a505c6557ea88568a4e3ace775ab55e93f2f4f9d57" [[package]] name = "ppv-lite86" @@ -877,9 +837,9 @@ dependencies = [ [[package]] name = "proc-macro2" -version = "1.0.63" +version = "1.0.64" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7b368fba921b0dce7e60f5e04ec15e565b3303972b42bcfde1d0713b881959eb" +checksum = "78803b62cbf1f46fde80d7c0e803111524b9877184cfe7c3033659490ac7a7da" dependencies = [ "unicode-ident", ] @@ -890,16 +850,16 @@ version = "0.9.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "77a1a2f1f0a7ecff9c31abbe177637be0e97a0aef46cf8738ece09327985d998" dependencies = [ - "bitflags", + "bitflags 1.3.2", "memchr", "unicase", ] [[package]] name = "quote" -version = "1.0.28" +version = "1.0.29" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1b9ab9c7eadfd8df19006f1cf1a4aed13540ed5cbc047010ece5826e10825488" +checksum = "573015e8ab27661678357f27dc26460738fd2b6c86e46f386fde94cb5d913105" dependencies = [ "proc-macro2", ] @@ -962,18 +922,19 @@ version = "0.3.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "567664f262709473930a4bf9e51bf2ebf3348f2e748ccc50dea20646858f8f29" dependencies = [ - "bitflags", + "bitflags 1.3.2", ] [[package]] name = "regex" -version = "1.8.4" +version = "1.9.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d0ab3ca65655bb1e41f2a8c8cd662eb4fb035e67c3f78da1d61dffe89d07300f" +checksum = "b2eae68fc220f7cf2532e4494aded17545fce192d59cd996e0fe7887f4ceb575" dependencies = [ "aho-corasick", "memchr", - "regex-syntax 0.7.2", + "regex-automata 0.3.2", + "regex-syntax 0.7.3", ] [[package]] @@ -985,6 +946,17 @@ dependencies = [ "regex-syntax 0.6.29", ] +[[package]] +name = "regex-automata" +version = "0.3.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "83d3daa6976cffb758ec878f108ba0e062a45b2d6ca3a2cca965338855476caf" +dependencies = [ + "aho-corasick", + "memchr", + "regex-syntax 0.7.3", +] + [[package]] name = "regex-syntax" version = "0.6.29" @@ -993,9 +965,9 @@ checksum = "f162c6dd7b008981e4d40210aca20b4bd0f9b60ca9271061b07f78537722f2e1" [[package]] name = "regex-syntax" -version = "0.7.2" +version = "0.7.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "436b050e76ed2903236f032a59761c1eb99e1b0aead2c257922771dab1fc8c78" +checksum = "2ab07dc67230e4a4718e70fd5c20055a4334b121f1f9db8fe63ef39ce9b8c846" [[package]] name = "rustc-demangle" @@ -1012,13 +984,12 @@ dependencies = [ [[package]] name = "rustix" -version = "0.37.20" +version = "0.38.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b96e891d04aa506a6d1f318d2771bcb1c7dfda84e126660ace067c9b474bb2c0" +checksum = "ac5ffa1efe7548069688cd7028f32591853cd7b5b756d41bcffd2353e4fc75b4" dependencies = [ - "bitflags", + "bitflags 2.3.3", "errno", - "io-lifetimes", "libc", "linux-raw-sys", "windows-sys 0.48.0", @@ -1026,15 +997,15 @@ dependencies = [ [[package]] name = "rustversion" -version = "1.0.12" +version = "1.0.13" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4f3208ce4d8448b3f3e7d168a73f5e0c43a61e32930de3bceeccedb388b6bf06" +checksum = "dc31bd9b61a32c31f9650d18add92aa83a49ba979c143eefd27fe7177b05bd5f" [[package]] name = "ryu" -version = "1.0.13" +version = "1.0.14" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f91339c0467de62360649f8d3e185ca8de4224ff281f66000de5eb2a77a79041" +checksum = "fe232bdf6be8c8de797b22184ee71118d63780ea42ac85b61d1baa6d3b782ae9" [[package]] name = "same-file" @@ -1062,29 +1033,29 @@ dependencies = [ [[package]] name = "serde" -version = "1.0.164" +version = "1.0.171" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9e8c8cf938e98f769bc164923b06dce91cea1751522f46f8466461af04c9027d" +checksum = "30e27d1e4fd7659406c492fd6cfaf2066ba8773de45ca75e855590f856dc34a9" dependencies = [ "serde_derive", ] [[package]] name = "serde_derive" -version = "1.0.164" +version = "1.0.171" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d9735b638ccc51c28bf6914d90a2e9725b377144fc612c49a611fddd1b631d68" +checksum = "389894603bd18c46fa56231694f8d827779c0951a667087194cf9de94ed24682" dependencies = [ "proc-macro2", "quote", - "syn 2.0.22", + "syn 2.0.25", ] [[package]] name = "serde_json" -version = "1.0.99" +version = "1.0.100" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "46266871c240a00b8f503b877622fe33430b3c7d963bdc0f2adc511e54a1eae3" +checksum = "0f1e14e89be7aa4c4b78bdbdc9eb5bf8517829a600ae8eaa39a6e1d960b5185c" dependencies = [ "itoa", "ryu", @@ -1102,9 +1073,9 @@ dependencies = [ [[package]] name = "serde_test" -version = "1.0.164" +version = "1.0.171" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "797c38160e2546a56e1e3439496439597e938669673ffd8af02a12f070da648f" +checksum = "b6480a2f4e1449ec9757ea143362ad5cea79bc7f1cb7711c06e1c5d03b6b5a3a" dependencies = [ "serde", ] @@ -1169,13 +1140,13 @@ dependencies = [ [[package]] name = "smallvec" -version = "1.10.0" +version = "1.11.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a507befe795404456341dfab10cef66ead4c041f62b8b11bbb92bffe5d0953e0" +checksum = "62bb4feee49fdd9f707ef802e22365a35de4b7b299de4763d44bfea899442ff9" [[package]] name = "std" -version = "0.31.0" +version = "0.32.0" dependencies = [ "kani", ] @@ -1229,9 +1200,9 @@ dependencies = [ [[package]] name = "syn" -version = "2.0.22" +version = "2.0.25" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2efbeae7acf4eabd6bcdcbd11c92f45231ddda7539edc7806bd1a04a03b24616" +checksum = "15e3fc8c0c74267e2df136e5e5fb656a464158aa57624053375eb9c8c6e25ae2" dependencies = [ "proc-macro2", "quote", @@ -1240,22 +1211,22 @@ dependencies = [ [[package]] name = "thiserror" -version = "1.0.40" +version = "1.0.43" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "978c9a314bd8dc99be594bc3c175faaa9794be04a5a5e153caba6915336cebac" +checksum = "a35fc5b8971143ca348fa6df4f024d4d55264f3468c71ad1c2f365b0a4d58c42" dependencies = [ "thiserror-impl", ] [[package]] name = "thiserror-impl" -version = "1.0.40" +version = "1.0.43" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f9456a42c5b0d803c8cd86e73dd7cc9edd429499f37a3550d286d5e86720569f" +checksum = "463fe12d7993d3b327787537ce8dd4dfa058de32fc2b195ef3cde03dc4771e8f" dependencies = [ "proc-macro2", "quote", - "syn 2.0.22", + "syn 2.0.25", ] [[package]] @@ -1270,9 +1241,9 @@ dependencies = [ [[package]] name = "toml" -version = "0.7.5" +version = "0.7.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1ebafdf5ad1220cb59e7d17cf4d2c72015297b75b19a10472f99b89225089240" +checksum = "c17e963a819c331dcacd7ab957d80bc2b9a9c1e71c804826d2f283dd65306542" dependencies = [ "serde", "serde_spanned", @@ -1291,9 +1262,9 @@ dependencies = [ [[package]] name = "toml_edit" -version = "0.19.11" +version = "0.19.12" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "266f016b7f039eec8a1a80dfe6156b633d208b9fccca5e4db1d6775b0c4e34a7" +checksum = "c500344a19072298cd05a7224b3c0c629348b78692bf48466c5238656e315a78" dependencies = [ "indexmap", "serde", @@ -1322,7 +1293,7 @@ checksum = "5f4f31f56159e98206da9efd823404b79b6ef3143b4a7ab76e67b1751b25a4ab" dependencies = [ "proc-macro2", "quote", - "syn 2.0.22", + "syn 2.0.25", ] [[package]] @@ -1378,19 +1349,6 @@ dependencies = [ "tracing-serde", ] -[[package]] -name = "tracing-tree" -version = "0.2.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4f9742d8df709837409dbb22aa25dd7769c260406f20ff48a2320b80a4a6aed0" -dependencies = [ - "atty", - "nu-ansi-term", - "tracing-core", - "tracing-log", - "tracing-subscriber", -] - [[package]] name = "unicase" version = "2.6.0" @@ -1402,9 +1360,9 @@ dependencies = [ [[package]] name = "unicode-ident" -version = "1.0.9" +version = "1.0.10" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b15811caf2415fb889178633e7724bad2509101cde276048e013b9def5e51fa0" +checksum = "22049a19f4a68748a168c0fc439f9516686aa045927ff767eca0a85101fb6e73" [[package]] name = "unicode-width" @@ -1518,7 +1476,7 @@ version = "0.48.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "677d2418bec65e3338edb076e806bc1ec15693c5d0104683f2efe857f61056a9" dependencies = [ - "windows-targets 0.48.0", + "windows-targets 0.48.1", ] [[package]] @@ -1538,9 +1496,9 @@ dependencies = [ [[package]] name = "windows-targets" -version = "0.48.0" +version = "0.48.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7b1eb6f0cd7c80c79759c929114ef071b87354ce476d9d94271031c0497adfd5" +checksum = "05d4b17490f70499f20b9e791dcf6a299785ce8af4d709018206dc5b4953e95f" dependencies = [ "windows_aarch64_gnullvm 0.48.0", "windows_aarch64_msvc 0.48.0", @@ -1637,9 +1595,9 @@ checksum = "1a515f5799fe4961cb532f983ce2b23082366b898e52ffbce459c86f67c8378a" [[package]] name = "winnow" -version = "0.4.7" +version = "0.4.9" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ca0ace3845f0d96209f0375e6d367e3eb87eb65d27d445bdc9f1843a26f39448" +checksum = "81a2094c43cc94775293eaa0e499fbc30048a6d824ac82c0351a8c0bf9112529" dependencies = [ "memchr", ] diff --git a/Cargo.toml b/Cargo.toml index e87c98d5241a..bb0dffcfaf1f 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-verifier" -version = "0.31.0" +version = "0.32.0" edition = "2021" description = "A bit-precise model checker for Rust." readme = "README.md" diff --git a/cprover_bindings/Cargo.toml b/cprover_bindings/Cargo.toml index aad7ccc3c858..938b93606fd2 100644 --- a/cprover_bindings/Cargo.toml +++ b/cprover_bindings/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "cprover_bindings" -version = "0.31.0" +version = "0.32.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/cprover_bindings/src/goto_program/builtin.rs b/cprover_bindings/src/goto_program/builtin.rs index dc703ce83edc..258691b9ade4 100644 --- a/cprover_bindings/src/goto_program/builtin.rs +++ b/cprover_bindings/src/goto_program/builtin.rs @@ -47,6 +47,7 @@ pub enum BuiltinFn { Memset, Nearbyint, Nearbyintf, + Posixmemalign, Pow, Powf, Powi, @@ -109,6 +110,7 @@ impl ToString for BuiltinFn { Memset => "memset", Nearbyint => "nearbyint", Nearbyintf => "nearbyintf", + Posixmemalign => "posix_memalign", Pow => "pow", Powf => "powf", Powi => "__builtin_powi", @@ -173,6 +175,7 @@ impl BuiltinFn { Memset => vec![Type::void_pointer(), Type::c_int(), Type::size_t()], Nearbyint => vec![Type::double()], Nearbyintf => vec![Type::float()], + Posixmemalign => vec![Type::void_pointer(), Type::size_t(), Type::size_t()], Powf => vec![Type::float(), Type::float()], Powi => vec![Type::double(), Type::c_int()], Powif => vec![Type::float(), Type::c_int()], @@ -234,6 +237,7 @@ impl BuiltinFn { Memset => Type::void_pointer(), Nearbyint => Type::double(), Nearbyintf => Type::float(), + Posixmemalign => Type::c_int(), Pow => Type::double(), Powf => Type::float(), Powi => Type::double(), @@ -296,6 +300,7 @@ impl BuiltinFn { Memset, Nearbyint, Nearbyintf, + Posixmemalign, Pow, Powf, Powi, diff --git a/docs/src/dev-documentation.md b/docs/src/dev-documentation.md index d480c4340d19..639b7125ae78 100644 --- a/docs/src/dev-documentation.md +++ b/docs/src/dev-documentation.md @@ -9,10 +9,11 @@ we recommend looking into [these issues](https://github.com/model-checking/kani/ In this chapter, we provide documentation that might be helpful for Kani developers (including external contributors): - 1. [Suggested workarounds](./workarounds.md). + 1. [Coding conventions](./conventions.md). 2. [Useful command-line instructions for Kani/CBMC/Git](./cheat-sheets.md). - 3. [Development setup recommendations for working with `rustc`](./rustc-hacks.md). - 4. [Guide for testing in Kani](./testing.md). + 3. [Development setup recommendations for working with `cbmc`](./cbmc-hacks.md). + 4. [Development setup recommendations for working with `rustc`](./rustc-hacks.md). + 5. [Guide for testing in Kani](./testing.md). > **NOTE**: The developer documentation is intended for Kani developers and not users. At present, the project is under heavy development and some items diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index 65f018363990..f23fc40e4b8c 100644 --- a/kani-compiler/Cargo.toml +++ b/kani-compiler/Cargo.toml @@ -3,13 +3,12 @@ [package] name = "kani-compiler" -version = "0.31.0" +version = "0.32.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false [dependencies] -atty = "0.2.14" cbmc = { path = "../cprover_bindings", package = "cprover_bindings", optional = true } clap = { version = "4.1.3", features = ["cargo"] } home = "0.5" @@ -25,7 +24,6 @@ strum_macros = "0.24.0" shell-words = "1.0.0" tracing = {version = "0.1", features = ["max_level_trace", "release_max_level_debug"]} tracing-subscriber = {version = "0.3.8", features = ["env-filter", "json", "fmt"]} -tracing-tree = "0.2.2" # Future proofing: enable backend dependencies using feature. [features] diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 8c6674d26f26..4bd5566f9d7c 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -5,8 +5,7 @@ use super::typ::{self, pointee_type}; use super::PropertyClass; use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::goto_program::{ - arithmetic_overflow_result_type, ArithmeticOverflowResult, BinaryOperator, BuiltinFn, Expr, - Location, Stmt, Type, ARITH_OVERFLOW_OVERFLOWED_FIELD, ARITH_OVERFLOW_RESULT_FIELD, + ArithmeticOverflowResult, BinaryOperator, BuiltinFn, Expr, Location, Stmt, Type, }; use rustc_middle::mir::{BasicBlock, Operand, Place}; use rustc_middle::ty::layout::{LayoutOf, ValidityRequirement}; @@ -183,43 +182,6 @@ impl<'tcx> GotocCtx<'tcx> { }}; } - // Intrinsics which encode a simple arithmetic operation with overflow check - macro_rules! codegen_op_with_overflow_check { - ($f:ident) => {{ - let a = fargs.remove(0); - let b = fargs.remove(0); - let op_type = a.typ().clone(); - let res = a.$f(b); - // add to symbol table - let struct_tag = self.codegen_arithmetic_overflow_result_type(op_type.clone()); - assert_eq!(*res.typ(), struct_tag); - - // store the result in a temporary variable - let (var, decl) = self.decl_temp_variable(struct_tag, Some(res), loc); - let check = self.codegen_assert( - var.clone() - .member(ARITH_OVERFLOW_OVERFLOWED_FIELD, &self.symbol_table) - .cast_to(Type::c_bool()) - .not(), - PropertyClass::ArithmeticOverflow, - format!("attempt to compute {} which would overflow", intrinsic).as_str(), - loc, - ); - self.codegen_expr_to_place( - p, - Expr::statement_expression( - vec![ - decl, - check, - var.member(ARITH_OVERFLOW_RESULT_FIELD, &self.symbol_table) - .as_stmt(loc), - ], - op_type, - ), - ) - }}; - } - // Intrinsics which encode a division operation with overflow check macro_rules! codegen_op_with_div_overflow_check { ($f:ident) => {{ @@ -617,19 +579,12 @@ impl<'tcx> GotocCtx<'tcx> { "unaligned_volatile_load" => { unstable_codegen!(self.codegen_expr_to_place(p, fargs.remove(0).dereference())) } - "unchecked_add" => codegen_op_with_overflow_check!(add_overflow_result), + "unchecked_add" | "unchecked_mul" | "unchecked_shl" | "unchecked_shr" + | "unchecked_sub" => { + unreachable!("Expected intrinsic `{intrinsic}` to be lowered before codegen") + } "unchecked_div" => codegen_op_with_div_overflow_check!(div), - "unchecked_mul" => codegen_op_with_overflow_check!(mul_overflow_result), "unchecked_rem" => codegen_op_with_div_overflow_check!(rem), - "unchecked_shl" => codegen_intrinsic_binop!(shl), - "unchecked_shr" => { - if fargs[0].typ().is_signed(self.symbol_table.machine_model()) { - codegen_intrinsic_binop!(ashr) - } else { - codegen_intrinsic_binop!(lshr) - } - } - "unchecked_sub" => codegen_op_with_overflow_check!(sub_overflow_result), "unlikely" => self.codegen_expr_to_place(p, fargs.remove(0)), "unreachable" => unreachable!( "Expected `std::intrinsics::unreachable` to be handled by `TerminatorKind::Unreachable`" @@ -1808,19 +1763,4 @@ impl<'tcx> GotocCtx<'tcx> { ); (size_of_count_elems.result, assert_stmt) } - - /// Codegens the struct type that CBMC produces for its arithmetic with overflow operators: - /// ``` - /// struct overflow_result_ { - /// operand_type result; // the result of the operation - /// bool overflowed; // whether the operation overflowed - /// } - /// ``` - /// and adds the type to the symbol table - fn codegen_arithmetic_overflow_result_type(&mut self, operand_type: Type) -> Type { - let res_type = arithmetic_overflow_result_type(operand_type); - self.ensure_struct(res_type.tag().unwrap(), res_type.tag().unwrap(), |_, _| { - res_type.components().unwrap().clone() - }) - } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index a756a42b0388..23211f022b23 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -227,6 +227,19 @@ impl<'tcx> GotocCtx<'tcx> { ); } } + ty::Adt(def, _) if Some(def.did()) == self.tcx.lang_items().c_str() => { + // TODO: Handle CString + // + let loc = self.codegen_span_option(span.cloned()); + let typ = self.codegen_ty(lit_ty); + let operation_name = "C string literal"; + return self.codegen_unimplemented_expr( + &operation_name, + typ, + loc, + "https://github.com/model-checking/kani/issues/2549", + ); + } _ => {} } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 8a652f0833e1..22b26a3489b4 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -163,6 +163,52 @@ impl<'tcx> GotocCtx<'tcx> { } } + /// Generate code for a binary operation with an overflow check. + fn codegen_binop_with_overflow_check( + &mut self, + op: &BinOp, + left_op: &Operand<'tcx>, + right_op: &Operand<'tcx>, + loc: Location, + ) -> Expr { + debug!(?op, "codegen_binop_with_overflow_check"); + let left = self.codegen_operand(left_op); + let right = self.codegen_operand(right_op); + let ret_type = left.typ().clone(); + let (bin_op, op_name) = match op { + BinOp::AddUnchecked => (BinaryOperator::OverflowResultPlus, "unchecked_add"), + BinOp::SubUnchecked => (BinaryOperator::OverflowResultMinus, "unchecked_sub"), + BinOp::MulUnchecked => (BinaryOperator::OverflowResultMult, "unchecked_mul"), + _ => unreachable!("Expected Add/Sub/Mul but got {op:?}"), + }; + // Create CBMC result type and add to the symbol table. + let res_type = arithmetic_overflow_result_type(left.typ().clone()); + let tag = res_type.tag().unwrap(); + let struct_tag = + self.ensure_struct(tag, tag, |_, _| res_type.components().unwrap().clone()); + let res = left.overflow_op(bin_op, right); + // store the result in a temporary variable + let (var, decl) = self.decl_temp_variable(struct_tag, Some(res), loc); + // cast into result type + let check = self.codegen_assert( + var.clone() + .member(ARITH_OVERFLOW_OVERFLOWED_FIELD, &self.symbol_table) + .cast_to(Type::c_bool()) + .not(), + PropertyClass::ArithmeticOverflow, + format!("attempt to compute `{op_name}` which would overflow").as_str(), + loc, + ); + Expr::statement_expression( + vec![ + decl, + check, + var.member(ARITH_OVERFLOW_RESULT_FIELD, &self.symbol_table).as_stmt(loc), + ], + ret_type, + ) + } + /// Generate code for a binary operation with an overflow and returns a tuple (res, overflow). pub fn codegen_binop_with_overflow( &mut self, @@ -297,7 +343,28 @@ impl<'tcx> GotocCtx<'tcx> { BinOp::Add | BinOp::Sub | BinOp::Mul | BinOp::Shl | BinOp::Shr => { self.codegen_scalar_binop(op, e1, e2) } - BinOp::Div | BinOp::Rem | BinOp::BitXor | BinOp::BitAnd | BinOp::BitOr => { + // We currently rely on CBMC's UB checks for shift which isn't always accurate. + // We should implement the checks ourselves. + // See https://github.com/model-checking/kani/issues/2374 + BinOp::ShlUnchecked => self.codegen_scalar_binop(&BinOp::Shl, e1, e2), + BinOp::ShrUnchecked => self.codegen_scalar_binop(&BinOp::Shr, e1, e2), + BinOp::AddUnchecked | BinOp::MulUnchecked | BinOp::SubUnchecked => { + self.codegen_binop_with_overflow_check(op, e1, e2, loc) + } + BinOp::Div | BinOp::Rem => { + let result = self.codegen_unchecked_scalar_binop(op, e1, e2); + if self.operand_ty(e1).is_integral() { + let is_rem = matches!(op, BinOp::Rem); + let check = self.check_div_overflow(e1, e2, is_rem, loc); + Expr::statement_expression( + vec![check, result.clone().as_stmt(loc)], + result.typ().clone(), + ) + } else { + result + } + } + BinOp::BitXor | BinOp::BitAnd | BinOp::BitOr => { self.codegen_unchecked_scalar_binop(op, e1, e2) } BinOp::Eq | BinOp::Lt | BinOp::Le | BinOp::Ne | BinOp::Ge | BinOp::Gt => { @@ -341,6 +408,53 @@ impl<'tcx> GotocCtx<'tcx> { } } + /// Check that a division does not overflow. + /// For integer types, division by zero is UB, as is MIN / -1 for signed. + /// Note that the compiler already inserts these checks for regular division. + /// However, since , unchecked divisions are + /// lowered to `BinOp::Div`. Prefer adding duplicated checks for now. + fn check_div_overflow( + &mut self, + dividend: &Operand<'tcx>, + divisor: &Operand<'tcx>, + is_remainder: bool, + loc: Location, + ) -> Stmt { + let divisor_expr = self.codegen_operand(divisor); + let msg = if is_remainder { + "attempt to calculate the remainder with a divisor of zero" + } else { + "attempt to divide by zero" + }; + let div_by_zero_check = self.codegen_assert_assume( + divisor_expr.clone().is_zero().not(), + PropertyClass::ArithmeticOverflow, + msg, + loc, + ); + if self.operand_ty(dividend).is_signed() { + let dividend_expr = self.codegen_operand(dividend); + let overflow_msg = if is_remainder { + "attempt to calculate the remainder with overflow" + } else { + "attempt to divide with overflow" + }; + let overflow_expr = dividend_expr + .clone() + .eq(dividend_expr.typ().min_int_expr(self.symbol_table.machine_model())) + .and(divisor_expr.clone().eq(Expr::int_constant(-1, divisor_expr.typ().clone()))); + let overflow_check = self.codegen_assert_assume( + overflow_expr.not(), + PropertyClass::ArithmeticOverflow, + overflow_msg, + loc, + ); + Stmt::block(vec![overflow_check, div_by_zero_check], loc) + } else { + div_by_zero_check + } + } + /// Create an initializer for a generator struct. fn codegen_rvalue_generator( &mut self, diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 18f510dc7a56..fbabe7e112cd 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -149,7 +149,7 @@ impl<'tcx> GotocCtx<'tcx> { "unreachable code", loc, ), - TerminatorKind::Drop { place, target, unwind: _ } => { + TerminatorKind::Drop { place, target, unwind: _, replace: _ } => { self.codegen_drop(place, target, loc) } TerminatorKind::Call { func, args, destination, target, .. } => { @@ -161,12 +161,12 @@ impl<'tcx> GotocCtx<'tcx> { if *expected { r } else { Expr::not(r) } }; - let msg = if let AssertKind::BoundsCheck { .. } = msg { + let msg = if let AssertKind::BoundsCheck { .. } = &**msg { // For bounds check the following panic message is generated at runtime: // "index out of bounds: the length is {len} but the index is {index}", // but CBMC only accepts static messages so we don't add values to the message. "index out of bounds: the length is less than or equal to the given index" - } else if let AssertKind::MisalignedPointerDereference { .. } = msg { + } else if let AssertKind::MisalignedPointerDereference { .. } = &**msg { // Misaligned pointer dereference check messages is also a runtime messages. // Generate a generic one here. "misaligned pointer dereference: address must be a multiple of its type's alignment" diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 955edb615bd6..69da5f1c7ad1 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -303,7 +303,7 @@ impl<'tcx> GotocCtx<'tcx> { var: ty::BoundVar::from_usize(bound_vars.len() - 1), kind: ty::BoundRegionKind::BrEnv, }; - let env_region = self.tcx.mk_re_late_bound(ty::INNERMOST, br); + let env_region = ty::Region::new_late_bound(self.tcx, ty::INNERMOST, br); let env_ty = self.tcx.closure_env_ty(def_id, substs, env_region).unwrap(); let sig = sig.skip_binder(); @@ -345,7 +345,7 @@ impl<'tcx> GotocCtx<'tcx> { kind: ty::BoundRegionKind::BrEnv, }; let env_region = ty::ReLateBound(ty::INNERMOST, br); - let env_ty = self.tcx.mk_mut_ref(self.tcx.mk_region_from_kind(env_region), ty); + let env_ty = self.tcx.mk_mut_ref(ty::Region::new_from_kind(self.tcx, env_region), ty); let pin_did = self.tcx.require_lang_item(LangItem::Pin, None); let pin_adt_ref = self.tcx.adt_def(pin_did); @@ -429,7 +429,7 @@ impl<'tcx> GotocCtx<'tcx> { current_fn.instance().subst_mir_and_normalize_erasing_regions( self.tcx, ty::ParamEnv::reveal_all(), - value, + ty::EarlyBinder::bind(value), ) } else { // TODO: confirm with rust team there is no way to monomorphize @@ -665,8 +665,8 @@ impl<'tcx> GotocCtx<'tcx> { } _ => { // This hash is documented to be the same no matter the crate context - let id_u64 = self.tcx.type_id_hash(t).as_u64(); - format!("_{id_u64}").intern() + let id = self.tcx.type_id_hash(t).as_u128(); + format!("_{id}").intern() } } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 985cbe1efc47..a89e5035f2a2 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -27,7 +27,7 @@ use rustc_codegen_ssa::back::archive::{ use rustc_codegen_ssa::back::metadata::create_wrapper_file; use rustc_codegen_ssa::traits::CodegenBackend; use rustc_codegen_ssa::{CodegenResults, CrateInfo}; -use rustc_data_structures::fx::FxHashMap; +use rustc_data_structures::fx::{FxHashMap, FxIndexMap}; use rustc_data_structures::temp_dir::MaybeTempDir; use rustc_errors::{ErrorGuaranteed, DEFAULT_LOCALE_RESOURCE}; use rustc_hir::def_id::LOCAL_CRATE; @@ -36,8 +36,8 @@ use rustc_metadata::fs::{emit_wrapper_file, METADATA_FILENAME}; use rustc_metadata::EncodedMetadata; use rustc_middle::dep_graph::{WorkProduct, WorkProductId}; use rustc_middle::mir::mono::MonoItem; -use rustc_middle::ty::query::Providers; -use rustc_middle::ty::{self, TyCtxt}; +use rustc_middle::query::{ExternProviders, Providers}; +use rustc_middle::ty::TyCtxt; use rustc_session::config::{CrateType, OutputFilenames, OutputType}; use rustc_session::cstore::MetadataLoaderDyn; use rustc_session::output::out_filename; @@ -192,7 +192,7 @@ impl CodegenBackend for GotocCodegenBackend { provide::provide(providers, &self.queries.lock().unwrap()); } - fn provide_extern(&self, providers: &mut ty::query::ExternProviders) { + fn provide_extern(&self, providers: &mut ExternProviders) { provide::provide_extern(providers); } @@ -317,10 +317,12 @@ impl CodegenBackend for GotocCodegenBackend { ongoing_codegen: Box, _sess: &Session, _filenames: &OutputFilenames, - ) -> Result<(CodegenResults, FxHashMap), ErrorGuaranteed> { - Ok(*ongoing_codegen - .downcast::<(CodegenResults, FxHashMap)>() - .unwrap()) + ) -> Result<(CodegenResults, FxIndexMap), ErrorGuaranteed> { + match ongoing_codegen.downcast::<(CodegenResults, FxIndexMap)>() + { + Ok(val) => Ok(*val), + Err(val) => panic!("unexpected error: {:?}", val.type_id()), + } } /// Emit output files during the link stage if it was requested. @@ -345,12 +347,13 @@ impl CodegenBackend for GotocCodegenBackend { ) -> Result<(), ErrorGuaranteed> { let requested_crate_types = sess.crate_types(); for crate_type in requested_crate_types { - let out_path = out_filename( + let out_fname = out_filename( sess, *crate_type, outputs, codegen_results.crate_info.local_crate_name, ); + let out_path = out_fname.as_path(); debug!(?crate_type, ?out_path, "link"); if *crate_type == CrateType::Rlib { // Emit the `rlib` that contains just one file: `.rmeta` @@ -396,7 +399,7 @@ fn check_target(session: &Session) { `x86_64-apple-*` or `arm64-apple-*`, but it is {}", &session.target.llvm_target ); - session.err(&err_msg); + session.err(err_msg); } session.abort_if_errors(); @@ -412,7 +415,7 @@ fn check_options(session: &Session) { let err_msg = format!( "Kani requires the target architecture option `min_global_align` to be 1, but it is {align}." ); - session.err(&err_msg); + session.err(err_msg); } _ => (), } @@ -441,7 +444,7 @@ fn codegen_results( rustc_metadata: EncodedMetadata, machine: &MachineModel, ) -> Box { - let work_products = FxHashMap::::default(); + let work_products = FxIndexMap::::default(); Box::new(( CodegenResults { modules: vec![], @@ -482,7 +485,7 @@ fn symbol_table_to_gotoc(tcx: &TyCtxt, base_path: &Path) -> PathBuf { "Failed to generate goto model:\n\tsymtab2gb failed on file {}.", input_filename.display() ); - tcx.sess.err(&err_msg); + tcx.sess.err(err_msg); tcx.sess.abort_if_errors(); }; output_filename @@ -591,7 +594,7 @@ impl<'tcx> GotoCodegenResults<'tcx> { msg += "\nVerification will fail if one or more of these constructs is reachable."; msg += "\nSee https://model-checking.github.io/kani/rust-feature-support.html for more \ details."; - tcx.sess.warn(&msg); + tcx.sess.warn(msg); } if !self.concurrent_constructs.is_empty() { @@ -602,7 +605,7 @@ impl<'tcx> GotoCodegenResults<'tcx> { for (construct, locations) in self.concurrent_constructs.iter() { writeln!(&mut msg, " - {construct} ({})", locations.len()).unwrap(); } - tcx.sess.warn(&msg); + tcx.sess.warn(msg); } // Print some compilation stats. 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 836444a78165..dd43c96f27ea 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -377,13 +377,13 @@ impl<'tcx> FnAbiOfHelpers<'tcx> for GotocCtx<'tcx> { FnAbiRequest::OfFnPtr { sig, extra_args } => { span_bug!( span, - "Error: {err}\n while running `fn_abi_of_fn_ptr. ({sig}, {extra_args:?})`", + "Error: {err:?}\n while running `fn_abi_of_fn_ptr. ({sig}, {extra_args:?})`", ); } FnAbiRequest::OfInstance { instance, extra_args } => { span_bug!( span, - "Error: {err}\n while running `fn_abi_of_instance. ({instance}, {extra_args:?})`", + "Error: {err:?}\n while running `fn_abi_of_instance. ({instance}, {extra_args:?})`", ); } } diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 24726e0f9655..6ee5136e12e5 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -58,8 +58,7 @@ pub(super) fn check_attributes(tcx: TyCtxt, def_id: DefId) { format!( "the `{}` attribute also requires the `#[kani::proof]` attribute", kind.as_ref() - ) - .as_str(), + ), ); } match kind { @@ -147,7 +146,7 @@ pub fn extract_harness_attributes(tcx: TyCtxt, def_id: DefId) -> HarnessAttribut /// /// TODO: Improve error message by printing the span of the harness instead of the definition. pub fn check_unstable_features(tcx: TyCtxt, enabled_features: &[String], def_id: DefId) { - if !matches!(tcx.type_of(def_id).0.kind(), TyKind::FnDef(..)) { + if !matches!(tcx.type_of(def_id).skip_binder().kind(), TyKind::FnDef(..)) { // skip closures due to an issue with rustc. // https://github.com/model-checking/kani/pull/2406#issuecomment-1534333862 return; @@ -195,7 +194,7 @@ fn expect_single<'a>( if attributes.len() > 1 { tcx.sess.span_err( attr.span, - &format!("only one '#[kani::{}]' attribute is allowed per harness", kind.as_ref()), + format!("only one '#[kani::{}]' attribute is allowed per harness", kind.as_ref()), ); } attr diff --git a/kani-compiler/src/kani_middle/coercion.rs b/kani-compiler/src/kani_middle/coercion.rs index 3c87a8173b3f..42f3cfb0a702 100644 --- a/kani-compiler/src/kani_middle/coercion.rs +++ b/kani-compiler/src/kani_middle/coercion.rs @@ -16,8 +16,8 @@ use rustc_hir::lang_items::LangItem; use rustc_middle::traits::{ImplSource, ImplSourceUserDefinedData}; use rustc_middle::ty::adjustment::CustomCoerceUnsized; -use rustc_middle::ty::TypeAndMut; use rustc_middle::ty::{self, ParamEnv, Ty, TyCtxt}; +use rustc_middle::ty::{TraitRef, TypeAndMut}; use rustc_span::symbol::Symbol; use tracing::trace; @@ -213,9 +213,11 @@ fn custom_coerce_unsize_info<'tcx>( ) -> CustomCoerceUnsized { let def_id = tcx.require_lang_item(LangItem::CoerceUnsized, None); - let trait_ref = ty::Binder::dummy( - tcx.mk_trait_ref(def_id, tcx.mk_substs_trait(source_ty, [target_ty.into()])), - ); + let trait_ref = ty::Binder::dummy(TraitRef::new( + tcx, + def_id, + tcx.mk_substs_trait(source_ty, [target_ty.into()]), + )); match tcx.codegen_select_candidate((ParamEnv::reveal_all(), trait_ref)) { Ok(ImplSource::UserDefined(ImplSourceUserDefinedData { impl_def_id, .. })) => { diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index fc60c0cc1a14..ba235db26805 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -51,7 +51,7 @@ pub fn check_crate_items(tcx: TyCtxt, ignore_asm: bool) { `--enable-unstable --ignore-global-asm` to suppress this error \ (**Verification results may be impacted**).", ); - tcx.sess.err(&error_msg); + tcx.sess.err(error_msg); } else { tcx.sess.warn(format!( "Ignoring global ASM in crate {krate}. Verification results may be impacted.", @@ -192,13 +192,13 @@ impl<'tcx> FnAbiOfHelpers<'tcx> for CompilerHelpers<'tcx> { FnAbiRequest::OfFnPtr { sig, extra_args } => { span_bug!( span, - "Error: {err}\n while running `fn_abi_of_fn_ptr. ({sig}, {extra_args:?})`", + "Error: {err:?}\n while running `fn_abi_of_fn_ptr. ({sig}, {extra_args:?})`", ); } FnAbiRequest::OfInstance { instance, extra_args } => { span_bug!( span, - "Error: {err}\n while running `fn_abi_of_instance. ({instance}, {extra_args:?})`", + "Error: {err:?}\n while running `fn_abi_of_instance. ({instance}, {extra_args:?})`", ); } } diff --git a/kani-compiler/src/kani_middle/provide.rs b/kani-compiler/src/kani_middle/provide.rs index a3a0a37f6a2e..bdca51f43129 100644 --- a/kani-compiler/src/kani_middle/provide.rs +++ b/kani-compiler/src/kani_middle/provide.rs @@ -6,13 +6,13 @@ use crate::kani_middle::reachability::{collect_reachable_items, filter_crate_items}; use crate::kani_middle::stubbing; -use crate::kani_middle::ty::query::query_provided::collect_and_partition_mono_items; use crate::kani_queries::QueryDb; use rustc_hir::def_id::{DefId, LocalDefId}; use rustc_interface; use rustc_middle::{ mir::Body, - ty::{query::ExternProviders, query::Providers, TyCtxt}, + query::{queries, ExternProviders, Providers}, + ty::TyCtxt, }; /// Sets up rustc's query mechanism to apply Kani's custom queries to code from @@ -65,7 +65,10 @@ fn run_kani_mir_passes<'tcx>( /// This is an issue when compiling a library, since the crate metadata is /// generated (using this query) before code generation begins (which is /// when we normally run the reachability analysis). -fn collect_and_partition_mono_items(tcx: TyCtxt, key: ()) -> collect_and_partition_mono_items { +fn collect_and_partition_mono_items( + tcx: TyCtxt, + key: (), +) -> queries::collect_and_partition_mono_items::ProvidedValue { let entry_fn = tcx.entry_fn(()).map(|(id, _)| id); let local_reachable = filter_crate_items(tcx, |_, def_id| { tcx.is_reachable_non_generic(def_id) || entry_fn == Some(def_id) diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 4d32a09f7d28..a3110426dc57 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -30,8 +30,8 @@ use rustc_middle::mir::{ use rustc_middle::span_bug; use rustc_middle::ty::adjustment::PointerCast; use rustc_middle::ty::{ - Closure, ClosureKind, ConstKind, Instance, InstanceDef, ParamEnv, Ty, TyCtxt, TyKind, - TypeFoldable, VtblEntry, + Closure, ClosureKind, ConstKind, EarlyBinder, Instance, InstanceDef, ParamEnv, Ty, TyCtxt, + TyKind, TypeFoldable, VtblEntry, }; use crate::kani_middle::coercion; @@ -243,7 +243,7 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> { self.instance.subst_mir_and_normalize_erasing_regions( self.tcx, ParamEnv::reveal_all(), - value, + EarlyBinder::bind(value), ) } @@ -483,7 +483,7 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> { let receiver_ty = tcx.subst_and_normalize_erasing_regions( substs, ParamEnv::reveal_all(), - generic_ty, + EarlyBinder::bind(generic_ty), ); let sep = callee.rfind("::").unwrap(); let trait_ = &callee[..sep]; diff --git a/kani-compiler/src/session.rs b/kani-compiler/src/session.rs index 3900aba5e82f..6061554200dc 100644 --- a/kani-compiler/src/session.rs +++ b/kani-compiler/src/session.rs @@ -9,11 +9,11 @@ use rustc_errors::{ emitter::Emitter, emitter::HumanReadableErrorType, fallback_fluent_bundle, json::JsonEmitter, ColorConfig, Diagnostic, TerminalUrl, }; +use std::io::IsTerminal; use std::panic; use std::str::FromStr; use std::sync::LazyLock; use tracing_subscriber::{filter::Directive, layer::SubscriberExt, EnvFilter, Registry}; -use tracing_tree::HierarchicalLayer; /// Environment variable used to control this session log tracing. const LOG_ENV_VAR: &str = "KANI_LOG"; @@ -107,16 +107,13 @@ fn json_logs(filter: EnvFilter) { /// Configure global logger to use a hierarchical view. fn hier_logs(args: &ArgMatches, filter: EnvFilter) { - let use_colors = atty::is(atty::Stream::Stdout) || args.get_flag(parser::COLOR_OUTPUT); + let use_colors = std::io::stdout().is_terminal() || args.get_flag(parser::COLOR_OUTPUT); let subscriber = Registry::default().with(filter); let subscriber = subscriber.with( - HierarchicalLayer::default() + tracing_subscriber::fmt::layer() .with_writer(std::io::stderr) - .with_indent_lines(true) .with_ansi(use_colors) - .with_targets(true) - .with_verbose_exit(true) - .with_indent_amount(4), + .with_target(true), ); tracing::subscriber::set_global_default(subscriber).unwrap(); } diff --git a/kani-dependencies b/kani-dependencies index 0c2264b0f9b2..498182678d6f 100644 --- a/kani-dependencies +++ b/kani-dependencies @@ -1,4 +1,4 @@ -CBMC_VERSION="5.86.0" +CBMC_VERSION="5.87.0" # If you update this version number, remember to bump it in `src/setup.rs` too CBMC_VIEWER_VERSION="3.8" KISSAT_VERSION="3.0.0" diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index 18d666830854..a4385206f83f 100644 --- a/kani-driver/Cargo.toml +++ b/kani-driver/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-driver" -version = "0.31.0" +version = "0.32.0" edition = "2021" description = "Build a project with Kani and run all proof harnesses" license = "MIT OR Apache-2.0" @@ -15,7 +15,6 @@ publish = false kani_metadata = { path = "../kani_metadata" } cargo_metadata = "0.15.0" anyhow = "1" -atty = "0.2.14" console = "0.15.1" once_cell = "1.13.0" serde = { version = "1", features = ["derive"] } @@ -32,7 +31,6 @@ strum = {version = "0.24.0"} strum_macros = {version = "0.24.0"} tracing = {version = "0.1", features = ["max_level_trace", "release_max_level_debug"]} tracing-subscriber = {version = "0.3.8", features = ["env-filter", "json", "fmt"]} -tracing-tree = "0.2.2" rand = "0.8" which = "4.4.0" diff --git a/kani-driver/src/args/common.rs b/kani-driver/src/args/common.rs index b8434c76e7b8..746482c6985e 100644 --- a/kani-driver/src/args/common.rs +++ b/kani-driver/src/args/common.rs @@ -42,6 +42,8 @@ pub enum UnstableFeatures { CFfi, /// Enable concrete playback flow. ConcretePlayback, + /// Enable Kani's unstable async library. + AsyncLib, } impl ValidateArgs for CommonArgs { diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index 30dac09eddaa..82186e96a44e 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -5,7 +5,7 @@ use crate::args::VerificationArgs; use crate::call_single_file::to_rustc_arg; use crate::project::Artifact; use crate::session::KaniSession; -use crate::util; +use crate::{session, util}; use anyhow::{bail, Context, Result}; use cargo_metadata::diagnostic::{Diagnostic, DiagnosticLevel}; use cargo_metadata::{Message, Metadata, MetadataCommand, Package, Target}; @@ -14,6 +14,7 @@ use std::ffi::{OsStr, OsString}; use std::fmt::{self, Display}; use std::fs::{self, File}; use std::io::BufReader; +use std::io::IsTerminal; use std::path::PathBuf; use std::process::Command; use tracing::{debug, trace}; @@ -78,8 +79,7 @@ impl KaniSession { cargo_args.push(format!("--features={}", features.join(",")).into()); } - cargo_args.push("--target".into()); - cargo_args.push(build_target.into()); + cargo_args.append(&mut cargo_config_args()); cargo_args.push("--target-dir".into()); cargo_args.push(target_dir.into()); @@ -110,7 +110,8 @@ impl KaniSession { for package in packages { for verification_target in package_targets(&self.args, package) { let mut cmd = Command::new("cargo"); - cmd.args(&cargo_args) + cmd.arg(session::toolchain_shorthand()) + .args(&cargo_args) .args(vec!["-p", &package.name]) .args(&verification_target.to_args()) .args(&pkg_args) @@ -180,7 +181,7 @@ impl KaniSession { /// Run cargo and collect any error found. /// We also collect the metadata file generated during compilation if any. fn run_cargo(&self, cargo_cmd: Command, target: &Target) -> Result> { - let support_color = atty::is(atty::Stream::Stdout); + let support_color = std::io::stdout().is_terminal(); let mut artifact = None; if let Some(mut cargo_process) = self.run_piped(cargo_cmd)? { let reader = BufReader::new(cargo_process.stdout.take().unwrap()); @@ -251,6 +252,19 @@ impl KaniSession { } } +pub fn cargo_config_args() -> Vec { + [ + "--target", + env!("TARGET"), + // Propagate `--cfg=kani` to build scripts. + "-Zhost-config", + "-Ztarget-applies-to-host", + "--config=host.rustflags=[\"--cfg=kani\"]", + ] + .map(OsString::from) + .to_vec() +} + /// Print the compiler message following the coloring schema. fn print_msg(diagnostic: &Diagnostic, use_rendered: bool) -> Result<()> { if use_rendered { diff --git a/kani-driver/src/concrete_playback/playback.rs b/kani-driver/src/concrete_playback/playback.rs index 0a71d64fe50f..bb060cea58bd 100644 --- a/kani-driver/src/concrete_playback/playback.rs +++ b/kani-driver/src/concrete_playback/playback.rs @@ -5,6 +5,7 @@ use crate::args::common::Verbosity; use crate::args::playback_args::{CargoPlaybackArgs, KaniPlaybackArgs, MessageFormat}; +use crate::call_cargo::cargo_config_args; use crate::call_single_file::base_rustc_flags; use crate::session::{lib_playback_folder, InstallType}; use crate::{session, util}; @@ -113,8 +114,7 @@ fn cargo_test(install: &InstallType, args: CargoPlaybackArgs) -> Result<()> { } cargo_args.append(&mut args.cargo.to_cargo_args()); - cargo_args.push("--target".into()); - cargo_args.push(env!("TARGET").into()); + cargo_args.append(&mut cargo_config_args()); // These have to be the last arguments to cargo test. if !args.playback.test_args.is_empty() { @@ -124,7 +124,8 @@ fn cargo_test(install: &InstallType, args: CargoPlaybackArgs) -> Result<()> { // Arguments that will only be passed to the target package. let mut cmd = Command::new("cargo"); - cmd.args(&cargo_args) + cmd.arg(session::toolchain_shorthand()) + .args(&cargo_args) .env("RUSTC", &install.kani_compiler()?) // Use CARGO_ENCODED_RUSTFLAGS instead of RUSTFLAGS is preferred. See // https://doc.rust-lang.org/cargo/reference/environment-variables.html diff --git a/kani-driver/src/session.rs b/kani-driver/src/session.rs index 47cbb0914eaf..d0834cae2122 100644 --- a/kani-driver/src/session.rs +++ b/kani-driver/src/session.rs @@ -5,6 +5,7 @@ use crate::args::common::Verbosity; use crate::args::VerificationArgs; use crate::util::render_command; use anyhow::{bail, Context, Result}; +use std::io::IsTerminal; use std::io::Write; use std::path::{Path, PathBuf}; use std::process::{Child, Command, ExitStatus, Stdio}; @@ -13,7 +14,6 @@ use std::time::Instant; use strum_macros::Display; use tracing::level_filters::LevelFilter; use tracing_subscriber::{layer::SubscriberExt, EnvFilter, Registry}; -use tracing_tree::HierarchicalLayer; /// Environment variable used to control this session log tracing. /// This is the same variable used to control `kani-compiler` logs. Note that you can still control @@ -291,6 +291,14 @@ pub fn base_folder() -> Result { .to_path_buf()) } +/// Return the shorthand for the toolchain used by this Kani version. +/// +/// This shorthand can be used to select the exact toolchain version that matches the one used to +/// build the current Kani version. +pub fn toolchain_shorthand() -> String { + format!("+{}", env!("RUSTUP_TOOLCHAIN")) +} + impl InstallType { pub fn new() -> Result { // Case 1: We've checked out the development repo and we're built under `target/kani` @@ -368,16 +376,13 @@ fn init_logger(args: &VerificationArgs) { }; // Use a hierarchical view for now. - let use_colors = atty::is(atty::Stream::Stdout); + let use_colors = std::io::stdout().is_terminal(); let subscriber = Registry::default().with(filter); let subscriber = subscriber.with( - HierarchicalLayer::default() + tracing_subscriber::fmt::layer() .with_writer(std::io::stderr) - .with_indent_lines(true) .with_ansi(use_colors) - .with_targets(true) - .with_verbose_exit(true) - .with_indent_amount(4), + .with_target(true), ); tracing::subscriber::set_global_default(subscriber).unwrap(); } diff --git a/kani_metadata/Cargo.toml b/kani_metadata/Cargo.toml index 1f71406bbad3..7b908e068fa5 100644 --- a/kani_metadata/Cargo.toml +++ b/kani_metadata/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_metadata" -version = "0.31.0" +version = "0.32.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/kani/Cargo.toml b/library/kani/Cargo.toml index 2dfd1e5e5291..8d44bb760367 100644 --- a/library/kani/Cargo.toml +++ b/library/kani/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani" -version = "0.31.0" +version = "0.32.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/kani/src/futures.rs b/library/kani/src/futures.rs index aea5e03d1f0b..cd3b9ad60597 100644 --- a/library/kani/src/futures.rs +++ b/library/kani/src/futures.rs @@ -15,6 +15,9 @@ use std::{ /// Whereas a clever executor like `block_on` in `futures` or `tokio` would interact with the OS scheduler /// to be woken up when a resource becomes available, this is not supported by Kani. /// As a consequence, this function completely ignores the waker infrastructure and just polls the given future in a busy loop. +/// +/// Note that [`spawn`] is not supported with this function. Use [`block_on_with_spawn`] if you need it. +#[crate::unstable(feature = "async-lib", issue = 2559, reason = "experimental async support")] pub fn block_on(mut fut: impl Future) -> T { let waker = unsafe { Waker::from_raw(NOOP_RAW_WAKER) }; let cx = &mut Context::from_waker(&waker); @@ -41,3 +44,189 @@ const NOOP_RAW_WAKER: RawWaker = { RawWaker::new(std::ptr::null(), &RawWakerVTable::new(clone_waker, noop, noop, noop)) }; + +/// The global executor used by [`spawn`] and [`block_on_with_spawn`] to run tasks. +static mut GLOBAL_EXECUTOR: Option = None; + +type BoxFuture = Pin + Sync + 'static>>; + +/// Indicates to the scheduler whether it can `kani::assume` that the returned task is running. +/// +/// This is useful if the task was picked nondeterministically using `kani::any()`. +/// For more information, see [`SchedulingStrategy`]. +pub enum SchedulingAssumption { + CanAssumeRunning, + CannotAssumeRunning, +} + +/// Trait that determines the possible sequence of tasks scheduling for a harness. +/// +/// If your harness spawns several tasks, Kani's scheduler has to decide in what order to poll them. +/// This order may depend on the needs of your verification goal. +/// For example, you sometimes may wish to verify all possible schedulings, i.e. a nondeterministic scheduling strategy. +/// +/// Nondeterministic scheduling strategies can be very slow to verify because they require Kani to check a large number of permutations of tasks. +/// So if you want to verify a harness that uses `spawn`, but don't care about concurrency issues, you can simply use a deterministic scheduling strategy, +/// such as [`RoundRobin`], which polls each task in turn. +/// +/// Finally, you have the option of providing your own scheduling strategy by implementing this trait. +/// This can be useful, for example, if you want to verify that things work correctly for a very specific task ordering. +pub trait SchedulingStrategy { + /// Picks the next task to be scheduled whenever the scheduler needs to pick a task to run next, and whether it can be assumed that the picked task is still running + /// + /// Tasks are numbered `0..num_tasks`. + /// For example, if pick_task(4) returns (2, CanAssumeRunning) than it picked the task with index 2 and allows Kani to `assume` that this task is still running. + /// This is useful if the task is chosen nondeterministicall (`kani::any()`) and allows the verifier to discard useless execution branches (such as polling a completed task again). + /// + /// As a rule of thumb: + /// if the scheduling strategy picks the next task nondeterministically (using `kani::any()`), return CanAssumeRunning, otherwise CannotAssumeRunning. + /// When returning `CanAssumeRunning`, the scheduler will then assume that the picked task is still running, which cuts off "useless" paths where a completed task is polled again. + /// It is even necessary to make things terminate if nondeterminism is involved: + /// if we pick the task nondeterministically, and don't have the restriction to still running tasks, we could poll the same task over and over again. + /// + /// However, for most deterministic scheduling strategies, e.g. the round robin scheduling strategy, assuming that the picked task is still running is generally not possible + /// because if that task has ended, we are saying assume(false) and the verification effectively stops (which is undesirable, of course). + /// In such cases, return `CannotAssumeRunning` instead. + fn pick_task(&mut self, num_tasks: usize) -> (usize, SchedulingAssumption); +} + +/// Keeps cycling through the tasks in a deterministic order +#[derive(Default)] +pub struct RoundRobin { + index: usize, +} + +impl SchedulingStrategy for RoundRobin { + #[inline] + fn pick_task(&mut self, num_tasks: usize) -> (usize, SchedulingAssumption) { + self.index = (self.index + 1) % num_tasks; + (self.index, SchedulingAssumption::CannotAssumeRunning) + } +} + +pub(crate) struct Scheduler { + tasks: Vec>, + num_running: usize, +} + +impl Scheduler { + /// Creates a scheduler with an empty task list + #[inline] + pub(crate) const fn new() -> Scheduler { + Scheduler { tasks: Vec::new(), num_running: 0 } + } + + /// Adds a future to the scheduler's task list, returning a JoinHandle + pub(crate) fn spawn + Sync + 'static>(&mut self, fut: F) -> JoinHandle { + let index = self.tasks.len(); + self.tasks.push(Some(Box::pin(fut))); + self.num_running += 1; + JoinHandle { index } + } + + /// Runs the scheduler with the given scheduling plan until all tasks have completed + fn run(&mut self, mut scheduling_plan: impl SchedulingStrategy) { + let waker = unsafe { Waker::from_raw(NOOP_RAW_WAKER) }; + let cx = &mut Context::from_waker(&waker); + while self.num_running > 0 { + let (index, assumption) = scheduling_plan.pick_task(self.tasks.len()); + let task = &mut self.tasks[index]; + if let Some(fut) = task.as_mut() { + match fut.as_mut().poll(cx) { + std::task::Poll::Ready(()) => { + self.num_running -= 1; + let _prev = task.take(); + } + std::task::Poll::Pending => (), + } + } else if let SchedulingAssumption::CanAssumeRunning = assumption { + crate::assume(false); // useful so that we can assume that a nondeterministically picked task is still running + } + } + } + + /// Polls the given future and the tasks it may spawn until all of them complete + fn block_on + Sync + 'static>( + &mut self, + fut: F, + scheduling_plan: impl SchedulingStrategy, + ) { + self.spawn(fut); + self.run(scheduling_plan); + } +} + +/// Result of spawning a task. +/// +/// If you `.await` a JoinHandle, this will wait for the spawned task to complete. +pub struct JoinHandle { + index: usize, +} + +impl Future for JoinHandle { + type Output = (); + + fn poll(self: Pin<&mut Self>, cx: &mut Context<'_>) -> std::task::Poll { + if unsafe { GLOBAL_EXECUTOR.as_mut().unwrap().tasks[self.index].is_some() } { + std::task::Poll::Pending + } else { + cx.waker().wake_by_ref(); // For completeness. But Kani currently ignores wakers. + std::task::Poll::Ready(()) + } + } +} + +/// Spawns a task on the current global executor (which is set by [`block_on_with_spawn`]) +/// +/// This function can only be called inside a future passed to [`block_on_with_spawn`]. +#[crate::unstable(feature = "async-lib", issue = 2559, reason = "experimental async support")] +pub fn spawn + Sync + 'static>(fut: F) -> JoinHandle { + unsafe { + GLOBAL_EXECUTOR + .as_mut() + .expect("`spawn` should only be called within `block_on_with_spawn`") + .spawn(fut) + } +} + +/// Polls the given future and the tasks it may spawn until all of them complete +/// +/// Contrary to [`block_on`], this allows `spawn`ing other futures +#[crate::unstable(feature = "async-lib", issue = 2559, reason = "experimental async support")] +pub fn block_on_with_spawn + Sync + 'static>( + fut: F, + scheduling_plan: impl SchedulingStrategy, +) { + unsafe { + assert!(GLOBAL_EXECUTOR.is_none(), "`block_on_with_spawn` should not be nested"); + GLOBAL_EXECUTOR = Some(Scheduler::new()); + GLOBAL_EXECUTOR.as_mut().unwrap().block_on(fut, scheduling_plan); + GLOBAL_EXECUTOR = None; + } +} + +/// Suspends execution of the current future, to allow the scheduler to poll another future +/// +/// Specifically, it returns a future that isn't ready until the second time it is polled. +#[crate::unstable(feature = "async-lib", issue = 2559, reason = "experimental async support")] +pub fn yield_now() -> impl Future { + struct YieldNow { + yielded: bool, + } + + impl Future for YieldNow { + type Output = (); + + fn poll(mut self: Pin<&mut Self>, cx: &mut Context<'_>) -> std::task::Poll { + if self.yielded { + cx.waker().wake_by_ref(); // For completeness. But Kani currently ignores wakers. + std::task::Poll::Ready(()) + } else { + self.yielded = true; + std::task::Poll::Pending + } + } + } + + YieldNow { yielded: false } +} diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index 71faf63feaaf..5ab09d69f9bb 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -26,8 +26,7 @@ pub use concrete_playback::concrete_playback_run; pub fn concrete_playback_run(_: Vec>, _: F) { unreachable!("Concrete playback does not work during verification") } - -pub use futures::block_on; +pub use futures::{block_on, block_on_with_spawn, spawn, yield_now, RoundRobin}; /// Creates an assumption that will be valid after this statement run. Note that the assumption /// will only be applied for paths that follow the assumption. If the assumption doesn't hold, the diff --git a/library/kani_macros/Cargo.toml b/library/kani_macros/Cargo.toml index bfcdcb64afc0..78b8fbb529da 100644 --- a/library/kani_macros/Cargo.toml +++ b/library/kani_macros/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_macros" -version = "0.31.0" +version = "0.32.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/std/Cargo.toml b/library/std/Cargo.toml index 3ed8810f0c1d..3cad55b31167 100644 --- a/library/std/Cargo.toml +++ b/library/std/Cargo.toml @@ -5,7 +5,7 @@ # Note: this package is intentionally named std to make sure the names of # standard library symbols are preserved name = "std" -version = "0.31.0" +version = "0.32.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 0015b8619839..1935a8e3142a 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-04-30" +channel = "nightly-2023-06-24" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/cargo-kani/itoa_dep/check_signed.expected b/tests/cargo-kani/itoa_dep/check_unsigned.expected similarity index 100% rename from tests/cargo-kani/itoa_dep/check_signed.expected rename to tests/cargo-kani/itoa_dep/check_unsigned.expected diff --git a/tests/cargo-kani/itoa_dep/src/main.rs b/tests/cargo-kani/itoa_dep/src/main.rs index 9bda87de7339..c2d1a165a409 100644 --- a/tests/cargo-kani/itoa_dep/src/main.rs +++ b/tests/cargo-kani/itoa_dep/src/main.rs @@ -17,10 +17,18 @@ fn check_itoa() { assert_eq!(result, &output); } +/// Note: We ignore this harness for now due to a performance regression. +/// See for more details. #[kani::proof] #[kani::unwind(10)] fn check_signed() { check_itoa::(); } +#[kani::proof] +#[kani::unwind(10)] +fn check_unsigned() { + check_itoa::(); +} + fn main() {} diff --git a/tests/cargo-ui/verbose-cmds/expected b/tests/cargo-ui/verbose-cmds/expected index a15f3ba25b6e..f883ef972cb3 100644 --- a/tests/cargo-ui/verbose-cmds/expected +++ b/tests/cargo-ui/verbose-cmds/expected @@ -1,5 +1,5 @@ CARGO_ENCODED_RUSTFLAGS= -cargo rustc +cargo +nightly Running: `goto-cc Running: `goto-instrument Checking harness dummy_harness... diff --git a/tests/expected/slice_c_str/c_str.rs b/tests/expected/slice_c_str/c_str.rs new file mode 100644 index 000000000000..9fa2feedc6ea --- /dev/null +++ b/tests/expected/slice_c_str/c_str.rs @@ -0,0 +1,22 @@ +#![feature(rustc_private)] +#![feature(c_str_literals)] + +extern crate libc; +use libc::c_char; + +#[kani::proof] +fn check_c_str() { + assert_eq!(unsafe { *empty_c_str() }, 0); + let (s, len) = non_empty_c_str(); + assert_ne!(unsafe { *s.offset(0) }, 0); + assert_eq!(unsafe { *s.offset(len as isize) }, 0); +} + +fn empty_c_str() -> *const c_char { + c"".as_ptr() as *const c_char +} + +/// Return a C string and its length (without the null character). +fn non_empty_c_str() -> (*const c_char, usize) { + (c"hi".as_ptr() as *const c_char, 2) +} diff --git a/tests/expected/slice_c_str/expected b/tests/expected/slice_c_str/expected new file mode 100644 index 000000000000..2138044e5b88 --- /dev/null +++ b/tests/expected/slice_c_str/expected @@ -0,0 +1,7 @@ +warning: Found the following unsupported constructs: +- C string literal + +Checking harness check_c_str... +Failed Checks: C string literal is not currently supported by Kani. + +VERIFICATION:- FAILED diff --git a/tests/kani/AsyncAwait/main.rs b/tests/kani/AsyncAwait/main.rs index e8821c998c16..aa1964bfc479 100644 --- a/tests/kani/AsyncAwait/main.rs +++ b/tests/kani/AsyncAwait/main.rs @@ -2,6 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // // compile-flags: --edition 2018 +// kani-flags: -Z async-lib // Tests that the language constructs `async { ... }` blocks, `async fn`, and `.await` work correctly. diff --git a/tests/kani/AsyncAwait/manual_spawn.rs b/tests/kani/AsyncAwait/manual_spawn.rs deleted file mode 100644 index 8888bc5caea1..000000000000 --- a/tests/kani/AsyncAwait/manual_spawn.rs +++ /dev/null @@ -1,203 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT -// -// compile-flags: --edition 2018 -// kani-flags: --enable-unstable --mir-linker - -//! This file tests a hand-written spawn infrastructure and executor. -//! This should be replaced with code from the Kani library as soon as the executor can get merged. -//! Tracking issue: https://github.com/model-checking/kani/issues/1685 - -use std::{ - future::Future, - pin::Pin, - sync::{ - atomic::{AtomicI64, Ordering}, - Arc, - }, - task::{Context, RawWaker, RawWakerVTable, Waker}, -}; - -/// A dummy waker, which is needed to call [`Future::poll`] -const NOOP_RAW_WAKER: RawWaker = { - #[inline] - unsafe fn clone_waker(_: *const ()) -> RawWaker { - NOOP_RAW_WAKER - } - - #[inline] - unsafe fn noop(_: *const ()) {} - - RawWaker::new(std::ptr::null(), &RawWakerVTable::new(clone_waker, noop, noop, noop)) -}; - -static mut GLOBAL_EXECUTOR: Scheduler = Scheduler::new(); -const MAX_TASKS: usize = 16; - -type BoxFuture = Pin + Sync + 'static>>; - -/// Indicates to the scheduler whether it can `assume` that the returned task is running. -/// This is useful if the task was picked nondeterministically using `any()`. -pub enum SchedulingOptimization { - CanAssumeRunning, - CannotAssumeRunning, -} - -/// Allows to parameterize how the scheduler picks the next task to poll in `spawnable_block_on` -pub trait SchedulingStrategy { - /// Picks the next task to be scheduled whenever the scheduler needs to pick a task to run next, and whether it can be assumed that the picked task is still running - /// - /// Tasks are numbered `0..num_tasks`. - /// For example, if pick_task(4) returns `(2, CanAssumeRunning)` than it picked the task with index 2 and allows Kani to `assume` that this task is still running. - /// This is useful if the task is chosen nondeterministicall (`kani::any()`) and allows the verifier to discard useless execution branches (such as polling a completed task again). - fn pick_task(&mut self, num_tasks: usize) -> (usize, SchedulingOptimization); -} - -/// Keeps cycling through the tasks in a deterministic order -#[derive(Default)] -pub struct RoundRobin { - index: usize, -} - -impl SchedulingStrategy for RoundRobin { - fn pick_task(&mut self, num_tasks: usize) -> (usize, SchedulingOptimization) { - self.index = (self.index + 1) % num_tasks; - (self.index, SchedulingOptimization::CannotAssumeRunning) - } -} - -pub struct Scheduler { - /// Using a Vec instead of an array makes the runtime increase by a factor of 200. - tasks: [Option; MAX_TASKS], - num_tasks: usize, - num_running: usize, -} - -impl Scheduler { - /// Creates a scheduler with an empty task list - pub const fn new() -> Scheduler { - const INIT: Option = None; - Scheduler { tasks: [INIT; MAX_TASKS], num_tasks: 0, num_running: 0 } - } - - /// Adds a future to the scheduler's task list, returning a JoinHandle - pub fn spawn + Sync + 'static>(&mut self, fut: F) -> JoinHandle { - let index = self.num_tasks; - self.tasks[index] = Some(Box::pin(fut)); - self.num_tasks += 1; - assert!(self.num_tasks < MAX_TASKS, "more than {} tasks", MAX_TASKS); - self.num_running += 1; - JoinHandle { index } - } - - /// Runs the scheduler with the given scheduling plan until all tasks have completed - pub fn run(&mut self, mut scheduling_plan: impl SchedulingStrategy) { - let waker = unsafe { Waker::from_raw(NOOP_RAW_WAKER) }; - let cx = &mut Context::from_waker(&waker); - while self.num_running > 0 { - let (index, can_assume_running) = scheduling_plan.pick_task(self.num_tasks); - let task = &mut self.tasks[index]; - if let Some(fut) = task.as_mut() { - match fut.as_mut().poll(cx) { - std::task::Poll::Ready(()) => { - self.num_running -= 1; - let _prev = std::mem::replace(task, None); - } - std::task::Poll::Pending => (), - } - } else if let SchedulingOptimization::CanAssumeRunning = can_assume_running { - #[cfg(kani)] - kani::assume(false); // useful so that we can assume that a nondeterministically picked task is still running - } - } - } - - /// Polls the given future and the tasks it may spawn until all of them complete. - pub fn block_on + Sync + 'static>( - &mut self, - fut: F, - scheduling_plan: impl SchedulingStrategy, - ) { - self.spawn(fut); - self.run(scheduling_plan); - } -} - -/// Result of spawning a task. -/// -/// If you `.await` a JoinHandle, this will wait for the spawned task to complete. -pub struct JoinHandle { - index: usize, -} - -impl Future for JoinHandle { - type Output = (); - - fn poll(self: Pin<&mut Self>, cx: &mut Context<'_>) -> std::task::Poll { - if unsafe { GLOBAL_EXECUTOR.tasks[self.index].is_some() } { - std::task::Poll::Pending - } else { - cx.waker().wake_by_ref(); // For completeness. But Kani currently ignores wakers. - std::task::Poll::Ready(()) - } - } -} - -#[inline] // to work around linking issue -pub fn spawn + Sync + 'static>(fut: F) -> JoinHandle { - unsafe { GLOBAL_EXECUTOR.spawn(fut) } -} - -/// Polls the given future and the tasks it may spawn until all of them complete -/// -/// Contrary to block_on, this allows `spawn`ing other futures -pub fn spawnable_block_on + Sync + 'static>( - fut: F, - scheduling_plan: impl SchedulingStrategy, -) { - unsafe { - GLOBAL_EXECUTOR.block_on(fut, scheduling_plan); - } -} - -struct YieldNow { - yielded: bool, -} - -impl Future for YieldNow { - type Output = (); - - fn poll(mut self: Pin<&mut Self>, cx: &mut Context<'_>) -> std::task::Poll { - if self.yielded { - cx.waker().wake_by_ref(); // For completeness. But Kani currently ignores wakers. - std::task::Poll::Ready(()) - } else { - self.yielded = true; - std::task::Poll::Pending - } - } -} - -/// Suspends execution of the current future, to allow the scheduler to poll another future -pub fn yield_now() -> impl Future { - YieldNow { yielded: false } -} - -#[kani::proof] -#[kani::unwind(4)] -fn arc_spawn_deterministic_test() { - let x = Arc::new(AtomicI64::new(0)); // Surprisingly, Arc verified faster than Rc - let x2 = x.clone(); - spawnable_block_on( - async move { - let x3 = x2.clone(); - spawn(async move { - x3.fetch_add(1, Ordering::Relaxed); - }); - yield_now().await; - x2.fetch_add(1, Ordering::Relaxed); - }, - RoundRobin::default(), - ); - assert_eq!(x.load(Ordering::Relaxed), 2); -} diff --git a/tests/kani/AsyncAwait/spawn.rs b/tests/kani/AsyncAwait/spawn.rs new file mode 100644 index 000000000000..3bef244ef547 --- /dev/null +++ b/tests/kani/AsyncAwait/spawn.rs @@ -0,0 +1,33 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// compile-flags: --edition 2018 +// kani-flags: -Z async-lib + +//! This file tests the executor and spawn infrastructure from the Kani library. + +use std::sync::{ + atomic::{AtomicI64, Ordering}, + Arc, +}; + +#[kani::proof] +#[kani::unwind(4)] +fn round_robin_schedule() { + let x = Arc::new(AtomicI64::new(0)); // Surprisingly, Arc verified faster than Rc + let x2 = x.clone(); + kani::block_on_with_spawn( + async move { + let x3 = x2.clone(); + kani::spawn(async move { + assert_eq!(x3.load(Ordering::Relaxed), 0); // to check the order of the round-robin + x3.fetch_add(1, Ordering::Relaxed); + }); + kani::yield_now().await; + assert_eq!(x2.load(Ordering::Relaxed), 1); // to check the order of the round-robin + x2.fetch_add(1, Ordering::Relaxed); + }, + kani::RoundRobin::default(), + ); + assert_eq!(x.load(Ordering::Relaxed), 2); +} diff --git a/tests/kani/LibC/posix_memalign.rs b/tests/kani/LibC/posix_memalign.rs new file mode 100644 index 000000000000..dc4aa5aeaae0 --- /dev/null +++ b/tests/kani/LibC/posix_memalign.rs @@ -0,0 +1,46 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +//! Check support for `posix_memalign`. + +#![feature(rustc_private)] +#![feature(allocator_api)] +extern crate libc; + +use std::alloc::{Allocator, Layout, System}; +use std::ptr; + +#[repr(C, align(32))] +struct MyStruct { + data: [u128; 10], +} + +#[kani::proof] +fn alloc_zeroed() { + let layout = Layout::new::(); + let ptr = System.allocate_zeroed(layout).unwrap(); + assert_eq!(unsafe { ptr.as_ref()[0] }, 0); +} + +// Source rust/src/libstd/sys/unix/alloc.rs +unsafe fn aligned_malloc(layout: &Layout) -> *mut u8 { + let mut out = ptr::null_mut(); + let ret = libc::posix_memalign(&mut out, layout.align(), layout.size()); + if ret != 0 { ptr::null_mut() } else { out as *mut u8 } +} + +#[kani::proof] +fn aligned_malloc_main() { + let mut layout = Layout::from_size_align(0, 1); + let _mem = unsafe { aligned_malloc(&layout.unwrap()) }; +} + +#[kani::proof] +fn posix_memalign_incorrect_alignment() { + let mut out = ptr::null_mut(); + let small_page_size = 1; + let size = 4; + assert_eq!(unsafe { libc::posix_memalign(&mut out, small_page_size, size) }, libc::EINVAL); + let incorrect_page_size = 13; + assert_eq!(unsafe { libc::posix_memalign(&mut out, incorrect_page_size, size) }, libc::EINVAL); +} diff --git a/tests/perf/format/Cargo.toml b/tests/perf/format/Cargo.toml new file mode 100644 index 000000000000..3fe392e07c04 --- /dev/null +++ b/tests/perf/format/Cargo.toml @@ -0,0 +1,11 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "format" +version = "0.1.0" +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] diff --git a/tests/perf/format/expected b/tests/perf/format/expected new file mode 100644 index 000000000000..44572d1c72bf --- /dev/null +++ b/tests/perf/format/expected @@ -0,0 +1 @@ +Complete - 2 successfully verified harnesses, 0 failures, 2 total diff --git a/tests/perf/format/src/lib.rs b/tests/perf/format/src/lib.rs new file mode 100644 index 000000000000..1986a08222ba --- /dev/null +++ b/tests/perf/format/src/lib.rs @@ -0,0 +1,20 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This test checks the performance of calling format. +//! This test captures the performance regression introduced by the toolchain upgrade in +//! See for more details. + +#[kani::proof] +fn fmt_i8() { + let num: i8 = kani::any(); + let s = format!("{num}"); + assert!(s.len() <= 4); +} + +#[kani::proof] +fn fmt_u8() { + let num: u8 = kani::any(); + let s = format!("{num}"); + assert!(s.len() <= 3); +} diff --git a/tests/script-based-pre/build-rs-conditional/Cargo.toml b/tests/script-based-pre/build-rs-conditional/Cargo.toml new file mode 100644 index 000000000000..136bae92250e --- /dev/null +++ b/tests/script-based-pre/build-rs-conditional/Cargo.toml @@ -0,0 +1,9 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +[package] +name = "build-rs-conditional" +version = "0.1.0" +edition = "2021" + +[dependencies] + diff --git a/tests/script-based-pre/build-rs-conditional/build.rs b/tests/script-based-pre/build-rs-conditional/build.rs new file mode 100644 index 000000000000..0b083ff95f02 --- /dev/null +++ b/tests/script-based-pre/build-rs-conditional/build.rs @@ -0,0 +1,11 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Verify that build scripts can check if they are running under `kani`. + +fn main() { + if cfg!(kani) { + println!("cargo:rustc-env=RUNNING_KANI=Yes"); + } else { + println!("cargo:rustc-env=RUNNING_KANI=No"); + } +} diff --git a/tests/script-based-pre/build-rs-conditional/build_rs.sh b/tests/script-based-pre/build-rs-conditional/build_rs.sh new file mode 100755 index 000000000000..f08fcf10cb79 --- /dev/null +++ b/tests/script-based-pre/build-rs-conditional/build_rs.sh @@ -0,0 +1,25 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +set +e + +TMP_DIR="/tmp/build-rs" + +rm -rf ${TMP_DIR} +cp -r . ${TMP_DIR} +pushd ${TMP_DIR} > /dev/null + + +echo "[TEST] Run verification..." +cargo kani --concrete-playback=inplace -Z concrete-playback + +echo "[TEST] Run playback..." +cargo kani playback -Z concrete-playback --lib -- check_kani + +echo "[TEST] Run test..." +cargo test --lib + +# Cleanup +popd > /dev/null +rm -r ${TMP_DIR} diff --git a/tests/script-based-pre/build-rs-conditional/config.yml b/tests/script-based-pre/build-rs-conditional/config.yml new file mode 100644 index 000000000000..e34ed0cb5689 --- /dev/null +++ b/tests/script-based-pre/build-rs-conditional/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: build_rs.sh +expected: expected diff --git a/tests/script-based-pre/build-rs-conditional/expected b/tests/script-based-pre/build-rs-conditional/expected new file mode 100644 index 000000000000..55f309077721 --- /dev/null +++ b/tests/script-based-pre/build-rs-conditional/expected @@ -0,0 +1,16 @@ +[TEST] Run verification... +Checking harness verify::check_kani... +Complete - 1 successfully verified harnesses, 0 failures, 1 total + +[TEST] Run playback... +running 1 test\ +test verify::kani_concrete_playback_check_kani_\ +\ +test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 1 filtered out + +[TEST] Run test... +running 1 test\ +test test::check_not_kani ... ok\ +\ +test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out + diff --git a/tests/script-based-pre/build-rs-conditional/src/lib.rs b/tests/script-based-pre/build-rs-conditional/src/lib.rs new file mode 100644 index 000000000000..70df880fdc8b --- /dev/null +++ b/tests/script-based-pre/build-rs-conditional/src/lib.rs @@ -0,0 +1,24 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! This tests ensures that build scripts are able to conditionally check if they are running under +//! Kani (in both verification and playback mode). + +#[cfg(kani)] +mod verify { + /// Running `cargo kani` should verify that "RUNNING_KANI" is equals to "Yes" + #[kani::proof] + fn check_kani() { + assert_eq!(env!("RUNNING_KANI"), "Yes"); + // Add a dummy cover so playback generates a test that should succeed. + kani::cover!(kani::any()); + } +} + +#[cfg(test)] +mod test { + /// Running `cargo test` should check that "RUNNING_KANI" is "No". + #[test] + fn check_not_kani() { + assert_eq!(env!("RUNNING_KANI"), "No"); + } +} diff --git a/tests/ui/Property-Class-UI/arithmetic_overflow/expected b/tests/ui/Property-Class-UI/arithmetic_overflow/expected index 67fc7dd6c0cd..9b445e995385 100644 --- a/tests/ui/Property-Class-UI/arithmetic_overflow/expected +++ b/tests/ui/Property-Class-UI/arithmetic_overflow/expected @@ -1,11 +1,11 @@ core::num::::unchecked_mul.arithmetic_overflow.1\ Status: SUCCESS -Description: "attempt to compute unchecked_mul which would overflow" +Description: "attempt to compute `unchecked_mul` which would overflow" core::num::::unchecked_add.arithmetic_overflow.1\ Status: SUCCESS -Description: "attempt to compute unchecked_add which would overflow" +Description: "attempt to compute `unchecked_add` which would overflow" core::num::::unchecked_sub.arithmetic_overflow.1\ Status: SUCCESS -Description: "attempt to compute unchecked_sub which would overflow" +Description: "attempt to compute `unchecked_sub` which would overflow" diff --git a/tests/ui/code-location/expected b/tests/ui/code-location/expected index cced065e9f1a..9af3f651fb50 100644 --- a/tests/ui/code-location/expected +++ b/tests/ui/code-location/expected @@ -1,6 +1,7 @@ module/mod.rs:10:5 in function module::not_empty main.rs:13:5 in function same_file /toolchains/ -alloc/src/vec/mod.rs:3018:81 in function as std::ops::Drop>::drop +alloc/src/vec/mod.rs: +in function as std::ops::Drop>::drop VERIFICATION:- SUCCESSFUL diff --git a/tests/ui/duplicates/dup_checks.rs b/tests/ui/duplicates/dup_checks.rs new file mode 100644 index 000000000000..a1b45d52cc05 --- /dev/null +++ b/tests/ui/duplicates/dup_checks.rs @@ -0,0 +1,19 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +//! Test that captures how Kani implements various redundant checks +//! for the same operation. This can be confusing for the user, since +//! the duplicated check will always succeed, even when the first check fails. +//! + +use std::hint::black_box; + +#[kani::proof] +fn check_division() { + black_box(kani::any::() / kani::any::()); +} + +#[kani::proof] +fn check_remainder() { + black_box(kani::any::() % kani::any::()); +} diff --git a/tests/ui/duplicates/expected b/tests/ui/duplicates/expected new file mode 100644 index 000000000000..9e6b135283d6 --- /dev/null +++ b/tests/ui/duplicates/expected @@ -0,0 +1,49 @@ +Checking harness check_remainder... + +RESULTS: +check_remainder.assertion\ +Status: FAILURE\ +Description: "attempt to calculate the remainder with a divisor of zero" + +check_remainder.assertion\ +Status: FAILURE\ +Description: "attempt to calculate the remainder with overflow" + +check_remainder.arithmetic_overflow\ +Status: SUCCESS\ +Description: "attempt to calculate the remainder with overflow" + +check_remainder.arithmetic_overflow\ +Status: SUCCESS\ +Description: "attempt to calculate the remainder with a divisor of zero" + +check_remainder.division-by-zero\ +Status: SUCCESS\ +Description: "division by zero" + +Failed Checks: attempt to calculate the remainder with a divisor of zero +Failed Checks: attempt to calculate the remainder with overflow + +Checking harness check_division... +check_division.assertion\ +Status: FAILURE\ +Description: "attempt to divide by zero" + +check_division.assertion\ +Status: FAILURE\ +Description: "attempt to divide with overflow" + +check_division.arithmetic_overflow\ +Status: SUCCESS\ +Description: "attempt to divide with overflow" + +check_division.arithmetic_overflow\ +Status: SUCCESS\ +Description: "attempt to divide by zero" + +check_division.division-by-zero\ +Status: SUCCESS\ +Description: "division by zero" + +Failed Checks: attempt to divide by zero +Failed Checks: attempt to divide with overflow diff --git a/tools/benchcomp/benchcomp/cmd_args.py b/tools/benchcomp/benchcomp/cmd_args.py index 6a8e47d42250..d8b7e735824f 100644 --- a/tools/benchcomp/benchcomp/cmd_args.py +++ b/tools/benchcomp/benchcomp/cmd_args.py @@ -138,6 +138,13 @@ def _get_args_dict(): "help": "do not make a fresh copy of the benchmark " "directories before running each variant", + }, { + "flags": ["--keep-temps"], + "action": "store_false", + "dest": "cleanup_directory", + "help": + "do not delete fresh copies of benchmark " + "directories after running each variant", }], }, "collate": { diff --git a/tools/benchcomp/benchcomp/entry/run.py b/tools/benchcomp/benchcomp/entry/run.py index d95ce8ab0d3a..a870e7e9a1b0 100644 --- a/tools/benchcomp/benchcomp/entry/run.py +++ b/tools/benchcomp/benchcomp/entry/run.py @@ -39,6 +39,7 @@ class _SingleInvocation: command_line: str directory: pathlib.Path + cleanup_directory: bool env: dict = dataclasses.field(default_factory=dict) timeout: int = None memout: int = None @@ -85,6 +86,9 @@ def __call__(self): encoding="utf-8") as handle: yaml.dump(suite, handle, default_flow_style=False) + if self.cleanup_directory and self.copy_benchmarks_dir: + shutil.rmtree(self.working_copy) + @dataclasses.dataclass class _Run: @@ -95,6 +99,7 @@ class _Run: out_dir: str out_symlink: str copy_benchmarks_dir: bool + cleanup_directory: bool result: dict = None def __call__(self): @@ -110,6 +115,7 @@ def __call__(self): suite_id, variant_id, parse, suite_yaml_out_dir=out_path, copy_benchmarks_dir=self.copy_benchmarks_dir, + cleanup_directory=self.cleanup_directory, **config) invoke() @@ -137,6 +143,6 @@ def get_default_out_prefix(): def main(args): run = _Run( args.config, args.out_prefix, args.out_dir, args.out_symlink, - args.copy_benchmarks_dir) + args.copy_benchmarks_dir, args.cleanup_directory) run() return run diff --git a/tools/build-kani/Cargo.toml b/tools/build-kani/Cargo.toml index eb4f686bc9f3..22a3d5d864e8 100644 --- a/tools/build-kani/Cargo.toml +++ b/tools/build-kani/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "build-kani" -version = "0.31.0" +version = "0.32.0" edition = "2021" description = "Builds Kani, Sysroot and release bundle." license = "MIT OR Apache-2.0"