diff --git a/CHANGELOG.md b/CHANGELOG.md index f873f2a42755..7ae95fe7f52c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,6 +4,23 @@ 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.59.0] + +### Breaking Changes +* Deprecate `--enable-unstable` and `--restrict-vtable` by @celinval in https://github.com/model-checking/kani/pull/3859 +* Do not report arithmetic overflow for floating point operations that produce +/-Inf by @rajath-mk in https://github.com/model-checking/kani/pull/3873 + +### What's Changed +* Fix validity checks for `char` by @celinval in https://github.com/model-checking/kani/pull/3853 +* Support verifying contracts/stubs for generic types with multiple inherent implementations by @carolynzech in https://github.com/model-checking/kani/pull/3829 +* Allow multiple stub_verified annotations, but check for duplicate targets by @remi-delmas-3000 in https://github.com/model-checking/kani/pull/3808 +* Fix crash if a function pointer is created but never used by @celinval in https://github.com/model-checking/kani/pull/3862 +* Fix transmute codegen when sizes are different by @celinval in https://github.com/model-checking/kani/pull/3861 +* Stub linker to avoid missing symbols errors by @celinval in https://github.com/model-checking/kani/pull/3858 +* Toolchain upgrade to nightly-2025-01-28 by @feliperodri @tautschnig + +**Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.58.0...kani-0.59.0 + ## [0.58.0] ### Major/Breaking Changes diff --git a/Cargo.lock b/Cargo.lock index 2a047b63f88b..87286ca982bf 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -24,7 +24,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "e89da841a80418a9b391ebaea17f5c112ffaaa96f621d2c285b5174da76b9011" dependencies = [ "cfg-if", - "getrandom", + "getrandom 0.2.15", "once_cell", "version_check", "zerocopy", @@ -176,7 +176,7 @@ dependencies = [ [[package]] name = "build-kani" -version = "0.58.0" +version = "0.59.0" dependencies = [ "anyhow", "cargo_metadata", @@ -192,9 +192,9 @@ checksum = "1fd0f2584146f6f2ef48085050886acf353beff7305ebd1ae69500e27c67f64b" [[package]] name = "bytes" -version = "1.9.0" +version = "1.10.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "325918d6fe32f23b19878fe4b34794ae41fc19ddbe53b10571a4874d44ffd39b" +checksum = "f61dac84819c6588b558454b194026eb1f09c293b9036ae9b159e74e73ab6cf9" [[package]] name = "camino" @@ -230,9 +230,9 @@ dependencies = [ [[package]] name = "cc" -version = "1.2.10" +version = "1.2.14" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "13208fcbb66eaeffe09b99fffbe1af420f00a7b35aa99ad683dfc1aa76145229" +checksum = "0c3d1b2e905a3a7b00a6141adb0e4c0bb941d11caf55349d863942a1cc44e3c9" dependencies = [ "shlex", ] @@ -282,9 +282,9 @@ dependencies = [ [[package]] name = "clap" -version = "4.5.27" +version = "4.5.29" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "769b0145982b4b48713e01ec42d61614425f27b7058bda7180a3a41f30104796" +checksum = "8acebd8ad879283633b343856142139f2da2317c96b05b4dd6181c61e2480184" dependencies = [ "clap_builder", "clap_derive", @@ -292,9 +292,9 @@ dependencies = [ [[package]] name = "clap_builder" -version = "4.5.27" +version = "4.5.29" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1b26884eb4b57140e4d2d93652abfa49498b938b3c9179f9fc487b0acc3edad7" +checksum = "f6ba32cbda51c7e1dfd49acc1457ba1a7dec5b64fe360e828acb13ca8dc9c2f9" dependencies = [ "anstream", "anstyle", @@ -304,9 +304,9 @@ dependencies = [ [[package]] name = "clap_derive" -version = "4.5.24" +version = "4.5.28" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "54b755194d6389280185988721fffba69495eed5ee9feeee9a599b53db80318c" +checksum = "bf4ced95c6f4a675af3da73304b9ac4ed991640c36374e4b46795c49e17cf1ed" dependencies = [ "heck", "proc-macro2", @@ -347,13 +347,12 @@ dependencies = [ [[package]] name = "comfy-table" -version = "7.1.3" +version = "7.1.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "24f165e7b643266ea80cb858aed492ad9280e3e05ce24d4a99d7d7b889b6a4d9" +checksum = "4a65ebfec4fb190b6f90e944a817d60499ee0744e582530e2c9900a22e591d9a" dependencies = [ "crossterm", - "strum", - "strum_macros", + "unicode-segmentation", "unicode-width 0.2.0", ] @@ -398,7 +397,7 @@ dependencies = [ [[package]] name = "cprover_bindings" -version = "0.58.0" +version = "0.59.0" dependencies = [ "lazy_static", "linear-map", @@ -472,9 +471,9 @@ dependencies = [ [[package]] name = "csv-core" -version = "0.1.11" +version = "0.1.12" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5efa2b3d7902f4b634a20cae3c9c4e6209dc4779feb6863329607560143efa70" +checksum = "7d02f3b0da4c6504f86e9cd789d8dbafab48c2321be74e9987593de5a894d93d" dependencies = [ "memchr", ] @@ -601,9 +600,9 @@ dependencies = [ [[package]] name = "equivalent" -version = "1.0.1" +version = "1.0.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5443807d6dff69373d433ab9ef5378ad8df50ca6298caf15de6e52e24aaf54d5" +checksum = "877a4ace8713b0bcf2a4e7eec82529c029f1d0619886d18145fea96c3ffe5c0f" [[package]] name = "errno" @@ -656,7 +655,19 @@ checksum = "c4567c8db10ae91089c99af84c68c38da3ec2f087c3f82960bcdbf3656b6f4d7" dependencies = [ "cfg-if", "libc", - "wasi", + "wasi 0.11.0+wasi-snapshot-preview1", +] + +[[package]] +name = "getrandom" +version = "0.3.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "43a49c392881ce6d5c3b8cb70f98717b7c07aabbdff06687b9030dbfbe2725f8" +dependencies = [ + "cfg-if", + "libc", + "wasi 0.13.3+wasi-0.2.2", + "windows-targets", ] [[package]] @@ -797,7 +808,7 @@ checksum = "72167d68f5fce3b8655487b8038691a3c9984ee769590f93f2a631f4ad64e4f5" [[package]] name = "kani" -version = "0.58.0" +version = "0.59.0" dependencies = [ "kani_core", "kani_macros", @@ -805,7 +816,7 @@ dependencies = [ [[package]] name = "kani-compiler" -version = "0.58.0" +version = "0.59.0" dependencies = [ "charon", "clap", @@ -844,7 +855,7 @@ dependencies = [ [[package]] name = "kani-driver" -version = "0.58.0" +version = "0.59.0" dependencies = [ "anyhow", "cargo_metadata", @@ -876,7 +887,7 @@ dependencies = [ [[package]] name = "kani-verifier" -version = "0.58.0" +version = "0.59.0" dependencies = [ "anyhow", "home", @@ -885,14 +896,14 @@ dependencies = [ [[package]] name = "kani_core" -version = "0.58.0" +version = "0.59.0" dependencies = [ "kani_macros", ] [[package]] name = "kani_macros" -version = "0.58.0" +version = "0.59.0" dependencies = [ "proc-macro-error2", "proc-macro2", @@ -902,7 +913,7 @@ dependencies = [ [[package]] name = "kani_metadata" -version = "0.58.0" +version = "0.59.0" dependencies = [ "clap", "cprover_bindings", @@ -993,9 +1004,9 @@ checksum = "68354c5c6bd36d73ff3feceb05efa59b6acb7626617f4962be322a825e61f79a" [[package]] name = "miniz_oxide" -version = "0.8.3" +version = "0.8.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b8402cab7aefae129c6977bb0ff1b8fd9a04eb5b51efc50a70bea51cda0c7924" +checksum = "b3b1c9bd4fe1f0f8b387f6eb9eb3b4a1aa26185e5750efb9140301703f62cd1b" dependencies = [ "adler2", ] @@ -1007,7 +1018,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "2886843bf800fba2e3377cff24abf6379b4c4d5c6681eaf9ea5b0d15090450bd" dependencies = [ "libc", - "wasi", + "wasi 0.11.0+wasi-snapshot-preview1", "windows-sys 0.52.0", ] @@ -1152,15 +1163,15 @@ dependencies = [ [[package]] name = "once_cell" -version = "1.20.2" +version = "1.20.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1261fe7e33c73b354eab43b1273a57c8f967d0391e80353e51f764ac02cf6775" +checksum = "945462a4b81e43c4e3ba96bd7b49d834c6f61198356aa858733bc4acf3cbe62e" [[package]] name = "os_info" -version = "3.9.2" +version = "3.10.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6e6520c8cc998c5741ee68ec1dc369fc47e5f0ea5320018ecf2a1ccd6328f48b" +checksum = "2a604e53c24761286860eba4e2c8b23a0161526476b1de520139d69cdb85a6b5" dependencies = [ "log", "windows-sys 0.52.0", @@ -1292,9 +1303,9 @@ dependencies = [ [[package]] name = "psm" -version = "0.1.24" +version = "0.1.25" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "200b9ff220857e53e184257720a14553b2f4aa02577d2ed9842d45d4b9654810" +checksum = "f58e5423e24c18cc840e1c98370b3993c6649cd1678b4d24318bcf0a083cbe88" dependencies = [ "cc", ] @@ -1335,7 +1346,7 @@ version = "0.6.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ec0be4795e2f6a28069bec0b5ff3e2ac9bafc99e6a9a7dc3547996c5c816922c" dependencies = [ - "getrandom", + "getrandom 0.2.15", ] [[package]] @@ -1447,9 +1458,9 @@ checksum = "f7c45b9784283f1b2e7fb61b42047c2fd678ef0960d4f6f1eba131594cc369d4" [[package]] name = "ryu" -version = "1.0.18" +version = "1.0.19" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f3cb5ba0dc43242ce17de99c180e96db90b235b8a9fdc9543c96d2209116bd9f" +checksum = "6ea1a2d0a644769cc99faa24c3ad26b379b786fe7c36fd3c546254801650e6dd" [[package]] name = "same-file" @@ -1518,9 +1529,9 @@ dependencies = [ [[package]] name = "serde_json" -version = "1.0.137" +version = "1.0.138" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "930cfb6e6abf99298aaad7d29abbef7a9999a9a8806a40088f55f0dcec03146b" +checksum = "d434192e7da787e94a6ea7e9670b26a036d0ca41e0b7efb2676dd32bae872949" dependencies = [ "indexmap", "itoa", @@ -1602,15 +1613,15 @@ dependencies = [ [[package]] name = "smallvec" -version = "1.13.2" +version = "1.14.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3c5e1a9a646d36c3599cd173a41282daf47c44583ad367b8e6837255952e5c67" +checksum = "7fcf8323ef1faaee30a44a340193b1ac6814fd9b7b4e88e9d4519a3e4abe1cfd" [[package]] name = "stacker" -version = "0.1.17" +version = "0.1.18" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "799c883d55abdb5e98af1a7b3f23b9b6de8ecada0ecac058672d7635eb48ca7b" +checksum = "1d08feb8f695b465baed819b03c128dc23f57a694510ab1f06c77f763975685e" dependencies = [ "cc", "cfg-if", @@ -1621,7 +1632,7 @@ dependencies = [ [[package]] name = "std" -version = "0.58.0" +version = "0.59.0" dependencies = [ "kani", ] @@ -1669,9 +1680,9 @@ dependencies = [ [[package]] name = "syn" -version = "2.0.96" +version = "2.0.98" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d5d0adab1ae378d7f53bdebc67a39f1f151407ef230f0ce2883572f5d8985c80" +checksum = "36147f1a48ae0ec2b5b3bc5b537d267457555a10dc06f3dbc8cb11ba3006d3b1" dependencies = [ "proc-macro2", "quote", @@ -1686,13 +1697,13 @@ checksum = "f764005d11ee5f36500a149ace24e00e3da98b0158b3e2d53a7495660d3f4d60" [[package]] name = "tempfile" -version = "3.15.0" +version = "3.17.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9a8a559c81686f576e8cd0290cd2a24a2a9ad80c98b3478856500fcbd7acd704" +checksum = "a40f762a77d2afa88c2d919489e390a12bdd261ed568e60cfa7e48d4e20f0d33" dependencies = [ "cfg-if", "fastrand", - "getrandom", + "getrandom 0.3.1", "once_cell", "rustix", "windows-sys 0.59.0", @@ -1813,9 +1824,9 @@ dependencies = [ [[package]] name = "toml" -version = "0.8.19" +version = "0.8.20" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a1ed1f98e3fdc28d6d910e6737ae6ab1a93bf1985935a1193e68f93eeb68d24e" +checksum = "cd87a5cdd6ffab733b2f74bc4fd7ee5fff6634124999ac278c35fc78c6120148" dependencies = [ "serde", "serde_spanned", @@ -1834,9 +1845,9 @@ dependencies = [ [[package]] name = "toml_edit" -version = "0.22.22" +version = "0.22.24" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4ae48d6208a266e853d946088ed816055e556cc6028c5e8e2b84d9fa5dd7c7f5" +checksum = "17b4795ff5edd201c7cd6dca065ae59972ce77d1b80fa0a84d94950ece7d1474" dependencies = [ "indexmap", "serde", @@ -1959,9 +1970,9 @@ dependencies = [ [[package]] name = "tree-sitter-language" -version = "0.1.3" +version = "0.1.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c199356c799a8945965bb5f2c55b2ad9d9aa7c4b4f6e587fe9dea0bc715e5f9c" +checksum = "38eee4db33814de3d004de9d8d825627ed3320d0989cce0dea30efaf5be4736c" [[package]] name = "tree-sitter-rust" @@ -1975,9 +1986,9 @@ dependencies = [ [[package]] name = "unicode-ident" -version = "1.0.15" +version = "1.0.16" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "11cd88e12b17c6494200a9c1b683a04fcac9573ed74cd1b62aeb2727c5592243" +checksum = "a210d160f08b701c8721ba1c726c11662f877ea6b7094007e1ca9a1041945034" [[package]] name = "unicode-segmentation" @@ -2023,9 +2034,9 @@ checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a" [[package]] name = "wait-timeout" -version = "0.2.0" +version = "0.2.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9f200f5b12eb75f8c1ed65abd4b2db8a6e1b138a20de009dacee265a2498f3f6" +checksum = "09ac3b126d3914f9849036f826e054cbabdc8519970b8998ddaf3b5bd3c65f11" dependencies = [ "libc", ] @@ -2046,11 +2057,20 @@ version = "0.11.0+wasi-snapshot-preview1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423" +[[package]] +name = "wasi" +version = "0.13.3+wasi-0.2.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "26816d2e1a4a36a2940b96c5296ce403917633dff8f3440e9b236ed6f6bacad2" +dependencies = [ + "wit-bindgen-rt", +] + [[package]] name = "which" -version = "7.0.1" +version = "7.0.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fb4a9e33648339dc1642b0e36e21b3385e6148e289226f657c809dee59df5028" +checksum = "2774c861e1f072b3aadc02f8ba886c26ad6321567ecc294c935434cad06f1283" dependencies = [ "either", "env_home", @@ -2173,9 +2193,9 @@ checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec" [[package]] name = "winnow" -version = "0.6.24" +version = "0.7.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c8d71a593cc5c42ad7876e2c1fda56f314f3754c084128833e64f1345ff8a03a" +checksum = "59690dea168f2198d1a3b0cac23b8063efcd11012f10ae4698f284808c8ef603" dependencies = [ "memchr", ] @@ -2186,6 +2206,15 @@ version = "0.0.19" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d135d17ab770252ad95e9a872d365cf3090e3be864a34ab46f48555993efc904" +[[package]] +name = "wit-bindgen-rt" +version = "0.33.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3268f3d866458b787f390cf61f4bbb563b922d091359f9608842999eaee3943c" +dependencies = [ + "bitflags", +] + [[package]] name = "zerocopy" version = "0.7.35" diff --git a/Cargo.toml b/Cargo.toml index a83963ad986c..4948246d5110 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-verifier" -version = "0.58.0" +version = "0.59.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 a96660df3d72..b35626e3d5f4 100644 --- a/cprover_bindings/Cargo.toml +++ b/cprover_bindings/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "cprover_bindings" -version = "0.58.0" +version = "0.59.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/docs/src/SUMMARY.md b/docs/src/SUMMARY.md index d534cf1f7f22..8cd6a1ebb7b0 100644 --- a/docs/src/SUMMARY.md +++ b/docs/src/SUMMARY.md @@ -18,9 +18,11 @@ - [Reference](./reference.md) - [Attributes](./reference/attributes.md) - [Experimental features](./reference/experimental/experimental-features.md) + - [Automatic Harness Generation](./reference/experimental/autoharness.md) - [Coverage](./reference/experimental/coverage.md) - [Stubbing](./reference/experimental/stubbing.md) - [Contracts](./reference/experimental/contracts.md) + - [Loop Contracts](./reference/experimental/loop-contracts.md) - [Concrete Playback](./reference/experimental/concrete-playback.md) - [Application](./application.md) - [Comparison with other tools](./tool-comparison.md) diff --git a/docs/src/reference/experimental/autoharness.md b/docs/src/reference/experimental/autoharness.md new file mode 100644 index 000000000000..022d6471ea0e --- /dev/null +++ b/docs/src/reference/experimental/autoharness.md @@ -0,0 +1,84 @@ +# Automatic Harness Generation + +Recall the harness for `estimate_size` that we wrote in [First Steps](../../tutorial-first-steps.md): +```rust +{{#include ../../tutorial/first-steps-v1/src/lib.rs:kani}} +``` + +This harness first declares a local variable `x` using `kani::any()`, then calls `estimate_size` with argument `x`. +Many proof harnesses follow this predictable format—to verify a function `foo`, we create arbitrary values for each of `foo`'s arguments, then call `foo` on those arguments. + +The `autoharness` subcommand leverages this observation to automatically generate and run harnesses. +Kani scans the crate for functions whose arguments all implement the `kani::Arbitrary` trait, generates harnesses for them, then runs them. +These harnesses are internal to Kani--i.e., Kani does not make any changes to your source code. + +## Usage +Run either: +``` +# cargo kani autoharness -Z unstable-options +``` +or +``` +# kani autoharness -Z unstable-options +``` + +If Kani detects that all of a function `foo`'s arguments implement `kani::Arbitrary`, it will generate and run a `#[kani::proof]` harness, which prints: + +``` +Autoharness: Checking function foo against all possible inputs... + +``` + +However, if Kani detects that `foo` has a [contract](./contracts.md), it will instead generate a `#[kani::proof_for_contract]` harness and verify the contract: +``` +Autoharness: Checking function foo's contract against all possible inputs... + +``` + +Kani generates and runs these harnesses internally—the user only sees the verification results. + +The `autoharness` subcommand has options `--include-function` and `--exclude-function` to include and exclude particular functions. +These flags look for partial matches against the fully qualified name of a function. + +For example, if a module `my_module` has many functions, but we are only interested in `my_module::foo` and `my_module::bar`, we can run: +``` +cargo run autoharness -Z unstable-options --include-function foo include-function bar +``` +To exclude `my_module` entirely, run: +``` +cargo run autoharness -Z unstable-options --exclude-function my_module +``` + +## Example +Using the `estimate_size` example from [First Steps](../../tutorial-first-steps.md) again: +```rust +{{#include ../../tutorial/first-steps-v1/src/lib.rs:code}} +``` + +We get: + +``` +# cargo kani autoharness -Z unstable-options +Autoharness: Checking function estimate_size against all possible inputs... +RESULTS: +Check 3: estimate_size.assertion.1 + - Status: FAILURE + - Description: "Oh no, a failing corner case!" +[...] + +Verification failed for - estimate_size +Complete - 0 successfully verified functions, 1 failures, 1 total. +``` + +## Request for comments +This feature is experimental and is therefore subject to change. +If you have ideas for improving the user experience of this feature, +please add them to [this GitHub issue](https://github.com/model-checking/kani/issues/3832). + +## Limitations +Kani will only generate an automatic harness for a function if it can determine that all of the function's arguments implement Arbitrary. +It does not attempt to derive/implement Arbitrary for any types, even if those types could implement Arbitrary. + +If a function contains a loop with a loop contract, Kani will detect the presence of a loop contract and verify that contract. +If, however, the loop does not have a contract, then there is currently no way to specify an unwinding bound for the function, meaning that Kani may hang as it tries to unwind the loop. +We recommend using the `--exclude-function` option to exclude any functions that have this issue (or `--harness-timeout` to bail after attempting verification for some amount of time). \ No newline at end of file diff --git a/docs/src/reference/experimental/loop-contracts.md b/docs/src/reference/experimental/loop-contracts.md new file mode 100644 index 000000000000..3cf5ecd429cc --- /dev/null +++ b/docs/src/reference/experimental/loop-contracts.md @@ -0,0 +1,154 @@ +# Loop Contracts + +Loop contract are used to specify invariants for loops for the sake of extending Kani's *bounded proofs* to *unbounded proofs*. +A [loop invariant](https://en.wikipedia.org/wiki/Loop_invariant) is an expression that holds upon entering a loop and after every execution of the loop body. +It captures something that does not change about every step of the loop. + +It is worth revisiting the discussion about [bounded proof](../../tutorial-loop-unwinding.md#bounded-proof) and +[loop unwinding](../../tutorial-loop-unwinding.md#loops-unwinding-and-bounds). In short, bounds on the number of times Kani unwinds loops also bound the size of inputs, +and hence result in a bounded proof. +Loop contracts are used to abstract out loops as non-loop blocks to avoid loop unwinding, and hence remove the bounds on the inputs. + +Consider the following example: + +``` Rust +fn simple_loop() { + let mut x: u64 = kani::any_where(|i| *i >= 1); + + while x > 1 { + x = x - 1; + } + + assert!(x == 1); +} +``` + +In this program, the loop repeatedly decrements `x` until it equals `1`. Because we haven't specified an upper bound for `x`, to verify this function, +Kani needs to unwind the loop for `u64::MAX` iterations, which is computationally expensive. Loop contracts allow us to abstract the loop behavior, significantly reducing the verification cost. + +With loop contracts, we can specify the loop’s behavior using invariants. For example: + +``` Rust +#![feature(stmt_expr_attributes)] +#![feature(proc_macro_hygiene)] + +fn simple_loop_with_loop_contracts() { + let mut x: u64 = kani::any_where(|i| *i >= 1); + + #[kani::loop_invariant(x >= 1)] + while x > 1 { + x = x - 1; + } + + assert!(x == 1); +} +``` + +Here, the loop invariant `#[kani::loop_invariant(x >= 1)]` specifies that the condition `x >= 1` must hold true at the start of each iteration before the loop guard is +checked. Once Kani verifies that the loop invariant is inductive, it will use the invariant to abstract the loop and avoid unwinding. + +Now let's run the proof with loop contracts through kani: +``` bash +kani simple_loop_with_loop_contracts.rs -Z loop-contracts +``` +The output reported by Kani on the example will be +``` +... + + +Check 10: simple_loop_with_loop_contracts.loop_invariant_base.1 + - Status: SUCCESS + - Description: "Check invariant before entry for loop simple_loop_with_loop_contracts.0" + - Location: simple_while_loop.rs:15:5 in function simple_loop_with_loop_contracts + +Check 11: simple_loop_with_loop_contracts.loop_assigns.1 + - Status: SUCCESS + - Description: "Check assigns clause inclusion for loop simple_loop_with_loop_contracts.0" + - Location: simple_while_loop.rs:15:5 in function simple_loop_with_loop_contracts + +Check 13: simple_loop_with_loop_contracts.assigns.1 + - Status: SUCCESS + - Description: "Check that x is assignable" + - Location: simple_while_loop.rs:17:9 in function simple_loop_with_loop_contracts + +Check 14: simple_loop_with_loop_contracts.loop_invariant_step.1 + - Status: SUCCESS + - Description: "Check invariant after step for loop simple_loop_with_loop_contracts.0" + - Location: simple_while_loop.rs:15:5 in function simple_loop_with_loop_contracts + +Check 15: simple_loop_with_loop_contracts.loop_invariant_step.2 + - Status: SUCCESS + - Description: "Check invariant after step for loop simple_loop_with_loop_contracts.0" + - Location: simple_while_loop.rs:15:5 in function simple_loop_with_loop_contracts + +... + +SUMMARY: + ** 0 of 99 failed + +VERIFICATION:- SUCCESSFUL +Verification Time: 0.3897019s + +Complete - 1 successfully verified harnesses, 0 failures, 1 total. +``` + + +## Loop contracts for `while` loops + +### Syntax +> +> \#\[kani::loop_invariant\( [_Expression_](https://doc.rust-lang.org/reference/expressions.html) \)\] +> +> `while` [_Expression_](https://doc.rust-lang.org/reference/expressions.html)_except struct expression_ [_BlockExpression_](https://doc.rust-lang.org/reference/expressions/block-expr.html) + + +An invariant contract `#[kani::loop_invariant(cond)]` accepts a valid Boolean expression `cond` over the variables visible at the same scope as the loop. + +### Semantics +A loop invariant contract expands to several assumptions and assertions: +1. The invariant is asserted just before the first iteration. +2. The invariant is assumed on a non-deterministic state to model a non-deterministic iteration. +3. The invariant is finally asserted again to establish its inductiveness. + +Mathematical induction is the working principle here. (1) establishes the base case for induction, and (2) & (3) establish the inductive case. +Therefore, the invariant must hold after the loop execution for any number of iterations. The invariant, together with the negation of the loop guard, +must be sufficient to establish subsequent assertions. If it is not, the abstraction is too imprecise and the user must supply a stronger invariant. + +To illustrate the key idea, we show how Kani abstracts the loop in `simple_loop_with_loop_contracts` as a non-loop block: +``` Rust +assert!(x >= 1) // check loop invariant for the base case. +x = kani::any(); +kani::assume(x >= 1); +if x > 1 { + // proof path 1: + // both loop guard and loop invariant are satisfied. + x = x - 1; + assert!(x >= 1); // check that loop invariant is inductive. + kani::assume(false) // block this proof path. +} +// proof path 2: +// loop invariant is satisfied and loop guard is violated. +assert!(x == 1); +``` +That is, we assume that we are in an arbitrary iteration after checking that the loop invariant holds for the base case. With the inductive hypothesis (`kani::assume(x >= 1);`), +we will either enter the loop (proof path 1) or leave the loop (proof path 2). We prove the two paths separately by killing path 1 with `kani::assume(false);`. +Note that all assertions after `kani::assume(false)` will be ignored as `false => p` can be deduced as `true` for any `p`. + +In proof path 1, we prove properties inside the loop and at last check that the loop invariant is inductive. + +In proof path 2, we prove properties after leaving the loop. As we leave the loop only when the loop guard is violated, the post condition of the loop can be expressed as +`!guard && inv`, which is `x <= 1 && x >= 1` in the example. The postcondition implies `x == 1`—the property we want to prove at the end of `simple_loop_with_loop_contracts`. + + +## Limitations + +Loop contracts comes with the following limitations. + +1. Only `while` loops are supported. The other three kinds of loops are not supported: [`loop` loops](https://doc.rust-lang.org/reference/expressions/loop-expr.html#infinite-loops) + , [`while let` loops](https://doc.rust-lang.org/reference/expressions/loop-expr.html#predicate-pattern-loops), and [`for` loops](https://doc.rust-lang.org/reference/expressions/loop-expr.html#iterator-loops). +2. Kani infers *loop modifies* with alias analysis. Loop modifies are those variables we assume to be arbitrary in the inductive hypothesis, and should cover all memory locations that are written to during + the execution of the loops. A proof will fail if the inferred loop modifies misses some targets written in the loops. + We observed this happens when some fields of structs are modified by some other functions called in the loops. +3. Kani doesn't check if a loop will always terminate in proofs with loop contracts. So it could be that some properties are proved successfully with Kani but actually are unreachable due to the + non-termination of some loops. +4. We don't check if loop invariants are side-effect free. A loop invariant with a side effect could lead to an unsound proof result. Make sure that the specified loop contracts are side-effect free. diff --git a/docs/src/rustc-hacks.md b/docs/src/rustc-hacks.md index a6047613288a..9ee5b522d894 100644 --- a/docs/src/rustc-hacks.md +++ b/docs/src/rustc-hacks.md @@ -52,19 +52,27 @@ Note that pretty printing for the Rust nightly toolchain (which Kani uses) is no For example, a vector may be displayed as `vec![{...}, {...}]` on nightly Rust, when it would be displayed as `vec![Some(0), None]` on stable Rust. Hopefully, this will be fixed soon. -### CLion / IntelliJ +### RustRover / CLion This is not a great solution, but it works for now (see for more details). -Edit the `Cargo.toml` of the package that you're working on and add artificial dependencies on the `rustc` packages that you would like to explore. + +Open the `Cargo.toml` of your crate (e.g.: `kani-compiler`), and do the following: + +1. Add optional dependencies on the `rustc` crates you are using. +2. Add a feature that enable those dependencies. +3. Toggle that feature using the IDE GUI. + +Here is an example: ```toml -# This configuration doesn't exist so it shouldn't affect your build. -[target.'cfg(KANI_DEV)'.dependencies] +# ** At the bottom of the dependencies section: ** # Adjust the path here to point to a local copy of the rust compiler. -# The best way is to use the rustup path. Replace with the -# proper name to your toolchain. -rustc_driver = { path = "~/.rustup/toolchains//lib/rustlib/rustc-src/rust/compiler/rustc_driver" } -rustc_interface = { path = "~/.rustup/toolchains//lib/rustlib/rustc-src/rust/compiler/rustc_interface" } +# E.g.: ~/.rustup/toolchains//lib/rustlib/rustc-src/rust/compiler +rustc_smir = { path = "/rustc_smir", optional = true } +stable_mir = { path = "/stable_mir", optional = true } + +[features] +clion = ['rustc_smir', 'stable_mir'] ``` **Don't forget to rollback the changes before you create your PR.** diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index a007742e5faa..e2636f5fcd64 100644 --- a/kani-compiler/Cargo.toml +++ b/kani-compiler/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-compiler" -version = "0.58.0" +version = "0.59.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/kani-compiler/src/args.rs b/kani-compiler/src/args.rs index 99254a08423a..e524b6e5ba2a 100644 --- a/kani-compiler/src/args.rs +++ b/kani-compiler/src/args.rs @@ -30,6 +30,9 @@ pub enum ReachabilityType { PubFns, /// Start the cross-crate reachability analysis from all *test* (i.e. `#[test]`) harnesses in the local crate. Tests, + /// Start the cross-crate reachability analysis from all functions in the local crate. + /// Currently, this mode is only used for automatic harness generation. + AllFns, } /// Command line arguments that this instance of the compiler run was called @@ -88,6 +91,12 @@ pub struct Arguments { /// Print the final LLBC file to stdout. #[clap(long)] pub print_llbc: bool, + /// If we are running the autoharness subcommand, the functions to autoharness + #[arg(long = "autoharness-include-function", num_args(1))] + pub autoharness_included_functions: Vec, + /// If we are running the autoharness subcommand, the functions to exclude from autoverification + #[arg(long = "autoharness-exclude-function", num_args(1))] + pub autoharness_excluded_functions: Vec, } #[derive(Debug, Clone, Copy, AsRefStr, EnumString, VariantNames, PartialEq, Eq)] diff --git a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs index e87bed0ea388..f577d2886e6c 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs @@ -253,7 +253,7 @@ impl CodegenBackend for LlbcCodegenBackend { units.store_modifies(&modifies_instances); units.write_metadata(&queries, tcx); } - ReachabilityType::Tests => todo!(), + ReachabilityType::Tests | ReachabilityType::AllFns => todo!(), ReachabilityType::None => {} ReachabilityType::PubFns => { let unit = CodegenUnit::default(); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index bf64f0dd2e66..15a4e6357349 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -220,7 +220,7 @@ impl GotocCtx<'_> { pub mod rustc_smir { use crate::codegen_cprover_gotoc::codegen::source_region::{SourceRegion, make_source_region}; use crate::stable_mir::CrateDef; - use rustc_middle::mir::coverage::CovTerm; + use rustc_middle::mir::coverage::BasicCoverageBlock; use rustc_middle::mir::coverage::MappingKind::Code; use rustc_middle::ty::TyCtxt; use rustc_smir::rustc_internal; @@ -236,16 +236,16 @@ pub mod rustc_smir { coverage_opaque: &CoverageOpaque, instance: Instance, ) -> Option<(SourceRegion, Filename)> { - let cov_term = parse_coverage_opaque(coverage_opaque); - region_from_coverage(tcx, cov_term, instance) + let bcb = parse_coverage_opaque(coverage_opaque); + region_from_coverage(tcx, bcb, instance) } - /// Retrieves the `SourceRegion` associated with a `CovTerm` object. + /// Retrieves the `SourceRegion` associated with a `BasicCoverageBlock` object. /// /// Note: This function could be in the internal `rustc` impl for `Coverage`. pub fn region_from_coverage( tcx: TyCtxt<'_>, - coverage: CovTerm, + coverage: BasicCoverageBlock, instance: Instance, ) -> Option<(SourceRegion, Filename)> { // We need to pull the coverage info from the internal MIR instance. @@ -257,10 +257,10 @@ pub mod rustc_smir { if let Some(cov_info) = &body.function_coverage_info { // Iterate over the coverage mappings and match with the coverage term. for mapping in &cov_info.mappings { - let Code(term) = mapping.kind else { unreachable!() }; + let Code { bcb } = mapping.kind else { unreachable!() }; let source_map = tcx.sess.source_map(); let file = source_map.lookup_source_file(cov_info.body_span.lo()); - if term == coverage { + if bcb == coverage { return Some(( make_source_region(source_map, cov_info, &file, mapping.span).unwrap(), rustc_internal::stable(cov_info.body_span).get_filename(), @@ -271,25 +271,17 @@ pub mod rustc_smir { None } - /// Parse a `CoverageOpaque` item and return the corresponding `CovTerm`: - /// - /// - /// At present, a `CovTerm` can be one of the following: - /// - `CounterIncrement()`: A physical counter. - /// - `ExpressionUsed()`: An expression-based counter. - /// - `Zero`: A counter with a constant zero value. - fn parse_coverage_opaque(coverage_opaque: &Opaque) -> CovTerm { + /// Parse a `CoverageOpaque` item and return the corresponding `BasicCoverageBlock`: + fn parse_coverage_opaque(coverage_opaque: &Opaque) -> BasicCoverageBlock { let coverage_str = coverage_opaque.to_string(); - if let Some(rest) = coverage_str.strip_prefix("CounterIncrement(") { - let (num_str, _rest) = rest.split_once(')').unwrap(); - let num = num_str.parse::().unwrap(); - CovTerm::Counter(num.into()) - } else if let Some(rest) = coverage_str.strip_prefix("ExpressionUsed(") { + if let Some(rest) = coverage_str.strip_prefix("VirtualCounter(bcb") { let (num_str, _rest) = rest.split_once(')').unwrap(); let num = num_str.parse::().unwrap(); - CovTerm::Expression(num.into()) + BasicCoverageBlock::from_u32(num) } else { - CovTerm::Zero + // When the coverage statement is injected into mir_body, it always has the form CoverageKind::VirtualCounter { bcb } + // https://github.com/rust-lang/rust/pull/136053/files#diff-c99ec9a281dce4a381fa7e11cf2d04f55dba5573d1d14389d47929fe0a154d24R209-R212 + unreachable!(); } } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 8cabd10c87ad..01796a832b78 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -12,9 +12,9 @@ use crate::codegen_cprover_gotoc::codegen::typ::std_pointee_type; use crate::codegen_cprover_gotoc::utils::{dynamic_fat_ptr, slice_fat_ptr}; use crate::unwrap_or_return_codegen_unimplemented; use cbmc::goto_program::{Expr, ExprValue, Location, Stmt, Type}; +use rustc_abi::{TagEncoding, Variants}; use rustc_middle::ty::layout::LayoutOf; use rustc_smir::rustc_internal; -use rustc_target::abi::{TagEncoding, Variants}; use stable_mir::mir::{FieldIdx, Local, Mutability, Place, ProjectionElem}; use stable_mir::ty::{RigidTy, Ty, TyKind, VariantDef, VariantIdx}; use tracing::{debug, trace, warn}; diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index b78d980a2cf4..0c2a81c3082c 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -18,9 +18,9 @@ use cbmc::goto_program::{ }; use cbmc::{InternString, InternedString, btree_string_map}; use num::bigint::BigInt; +use rustc_abi::{FieldsShape, TagEncoding, Variants}; use rustc_middle::ty::{TyCtxt, TypingEnv, VtblEntry}; use rustc_smir::rustc_internal; -use rustc_target::abi::{FieldsShape, TagEncoding, Variants}; use stable_mir::abi::{Primitive, Scalar, ValueAbi}; use stable_mir::mir::mono::Instance; use stable_mir::mir::{ @@ -667,7 +667,7 @@ impl GotocCtx<'_> { assert!(operands.len() == 2); let typ = self.codegen_ty_stable(res_ty); let layout = self.layout_of_stable(res_ty); - assert!(layout.ty.is_unsafe_ptr()); + assert!(layout.ty.is_raw_ptr()); let data = self.codegen_operand_stable(&operands[0]); match pointee_ty.kind() { TyKind::RigidTy(RigidTy::Slice(inner_ty)) => { @@ -801,8 +801,30 @@ impl GotocCtx<'_> { self.codegen_pointer_cast(k, e, *t, loc) } Rvalue::Cast(CastKind::Transmute, operand, ty) => { - let goto_typ = self.codegen_ty_stable(*ty); - self.codegen_operand_stable(operand).transmute_to(goto_typ, &self.symbol_table) + let src_ty = operand.ty(self.current_fn().locals()).unwrap(); + // Transmute requires sized types. + let src_sz = LayoutOf::new(src_ty).size_of().unwrap(); + let dst_sz = LayoutOf::new(*ty).size_of().unwrap(); + let dst_type = self.codegen_ty_stable(*ty); + if src_sz != dst_sz { + Expr::statement_expression( + vec![ + self.codegen_assert_assume_false( + PropertyClass::SafetyCheck, + &format!( + "Cannot transmute between types of different sizes. \ + Transmuting from `{src_sz}` to `{dst_sz}` bytes" + ), + loc, + ), + dst_type.nondet().as_stmt(loc), + ], + dst_type, + loc, + ) + } else { + self.codegen_operand_stable(operand).transmute_to(dst_type, &self.symbol_table) + } } Rvalue::BinaryOp(op, e1, e2) => self.codegen_rvalue_binary_op(res_ty, op, e1, e2, loc), Rvalue::CheckedBinaryOp(op, e1, e2) => { @@ -829,7 +851,7 @@ impl GotocCtx<'_> { .bytes(), Type::size_t(), ), - NullOp::UbChecks => Expr::c_false(), + NullOp::ContractChecks | NullOp::UbChecks => Expr::c_false(), } } Rvalue::ShallowInitBox(ref operand, content_ty) => { @@ -1483,8 +1505,10 @@ impl GotocCtx<'_> { |ctx, var| { // Build the vtable, using Rust's vtable_entries to determine field order let vtable_entries = if let Some(principal) = trait_type.kind().trait_principal() { - let trait_ref_binder = principal.with_self_ty(src_mir_type); - ctx.tcx.vtable_entries(rustc_internal::internal(ctx.tcx, trait_ref_binder)) + let trait_ref = + rustc_internal::internal(ctx.tcx, principal.with_self_ty(src_mir_type)); + let trait_ref = ctx.tcx.instantiate_bound_regions_with_erased(trait_ref); + ctx.tcx.vtable_entries(trait_ref) } else { TyCtxt::COMMON_VTABLE_ENTRIES }; diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 90635a71f2e8..813e07d06723 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -7,10 +7,10 @@ use crate::codegen_cprover_gotoc::codegen::function::rustc_smir::region_from_cov use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx}; use crate::unwrap_or_return_codegen_unimplemented_stmt; use cbmc::goto_program::{Expr, Location, Stmt, Type}; +use rustc_abi::{FieldsShape, Primitive, TagEncoding, Variants}; use rustc_middle::ty::layout::LayoutOf; use rustc_middle::ty::{List, TypingEnv}; use rustc_smir::rustc_internal; -use rustc_target::abi::{FieldsShape, Primitive, TagEncoding, Variants}; use stable_mir::abi::{ArgAbi, FnAbi, PassMode}; use stable_mir::mir::mono::{Instance, InstanceKind}; use stable_mir::mir::{ @@ -251,19 +251,37 @@ impl GotocCtx<'_> { if *expected { r } else { Expr::not(r) } }; - let msg = if let AssertMessage::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 AssertMessage::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" - } else { + let (msg, property_class) = match msg { + AssertMessage::BoundsCheck { .. } => { + // 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", + PropertyClass::Assertion, + ) + } + AssertMessage::MisalignedPointerDereference { .. } => { + // 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", + PropertyClass::SafetyCheck, + ) + } // For all other assert kind we can get the static message. - msg.description().unwrap() + AssertMessage::NullPointerDereference => { + (msg.description().unwrap(), PropertyClass::SafetyCheck) + } + AssertMessage::Overflow { .. } + | AssertMessage::OverflowNeg { .. } + | AssertMessage::DivisionByZero { .. } + | AssertMessage::RemainderByZero { .. } + | AssertMessage::ResumedAfterReturn { .. } + | AssertMessage::ResumedAfterPanic { .. } => { + (msg.description().unwrap(), PropertyClass::Assertion) + } }; let (msg_str, reach_stmt) = @@ -274,7 +292,7 @@ impl GotocCtx<'_> { reach_stmt, self.codegen_assert_assume( cond.cast_to(Type::bool()), - PropertyClass::Assertion, + property_class, &msg_str, loc, ), @@ -552,7 +570,7 @@ impl GotocCtx<'_> { let ty = self.operand_ty_stable(op); if ty.kind().is_bool() { Some(self.codegen_operand_stable(op).cast_to(Type::c_bool())) - } else if arg_abi.map_or(true, |abi| abi.mode != PassMode::Ignore) { + } else if arg_abi.is_none_or(|abi| abi.mode != PassMode::Ignore) { Some(self.codegen_operand_stable(op)) } else { None diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 18c121694223..a22528d55407 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -4,6 +4,10 @@ use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::goto_program::{DatatypeComponent, Expr, Location, Parameter, Symbol, SymbolTable, Type}; use cbmc::utils::aggr_tag; use cbmc::{InternString, InternedString}; +use rustc_abi::{ + BackendRepr::Vector, FieldIdx, FieldsShape, Float, Integer, LayoutData, Primitive, Size, + TagEncoding, TyAndLayout, VariantIdx, Variants, +}; use rustc_ast::ast::Mutability; use rustc_index::IndexVec; use rustc_middle::ty::GenericArgsRef; @@ -17,10 +21,6 @@ use rustc_middle::ty::{ use rustc_middle::ty::{List, TypeFoldable}; use rustc_smir::rustc_internal; use rustc_span::def_id::DefId; -use rustc_target::abi::{ - BackendRepr::Vector, FieldIdx, FieldsShape, Float, Integer, LayoutData, Primitive, Size, - TagEncoding, TyAndLayout, VariantIdx, Variants, -}; use stable_mir::abi::{ArgAbi, FnAbi, PassMode}; use stable_mir::mir::Body; use stable_mir::mir::mono::Instance as InstanceStable; @@ -371,6 +371,7 @@ impl<'tcx> GotocCtx<'tcx> { // The virtual methods on the trait ref. Some auto traits have no methods. if let Some(principal) = binder.principal() { let poly = principal.with_self_ty(self.tcx, t); + let poly = self.tcx.instantiate_bound_regions_with_erased(poly); let poly = self.tcx.erase_regions(poly); let mut flds = self .tcx diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index a0ae5ae99eff..d6f353fe995d 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -23,6 +23,7 @@ use cbmc::{InternedString, MachineModel}; use kani_metadata::artifact::convert_type; use kani_metadata::{ArtifactType, HarnessMetadata, KaniMetadata, UnsupportedFeature}; use kani_metadata::{AssignsContract, CompilerArtifactStub}; +use rustc_abi::Endian; use rustc_codegen_ssa::back::archive::{ ArArchiveBuilder, ArchiveBuilder, ArchiveBuilderBuilder, DEFAULT_OBJECT_READER, }; @@ -40,7 +41,6 @@ use rustc_session::Session; use rustc_session::config::{CrateType, OutputFilenames, OutputType}; use rustc_session::output::out_filename; use rustc_smir::rustc_internal; -use rustc_target::abi::Endian; use rustc_target::spec::PanicStrategy; use stable_mir::mir::mono::{Instance, MonoItem}; use stable_mir::{CrateDef, DefId}; @@ -264,7 +264,7 @@ impl CodegenBackend for GotocCodegenBackend { let reachability = queries.args().reachability_analysis; let mut results = GotoCodegenResults::new(tcx, reachability); match reachability { - ReachabilityType::Harnesses => { + ReachabilityType::AllFns | ReachabilityType::Harnesses => { let mut units = CodegenUnits::new(&queries, tcx); let mut modifies_instances = vec![]; let mut loop_contracts_instances = vec![]; @@ -375,7 +375,9 @@ impl CodegenBackend for GotocCodegenBackend { // Print compilation report. results.print_report(tcx); - if reachability != ReachabilityType::Harnesses { + if reachability != ReachabilityType::Harnesses + && reachability != ReachabilityType::AllFns + { // In a workspace, cargo seems to be using the same file prefix to build a crate that is // a package lib and also a dependency of another package. // To avoid overriding the metadata for its verification, we skip this step when 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 0e5e72af70b6..79410bd3373e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -26,6 +26,7 @@ use cbmc::goto_program::{ }; use cbmc::utils::aggr_tag; use cbmc::{InternedString, MachineModel}; +use rustc_abi::{HasDataLayout, TargetDataLayout}; use rustc_data_structures::fx::FxHashMap; use rustc_middle::span_bug; use rustc_middle::ty::layout::{ @@ -35,8 +36,7 @@ use rustc_middle::ty::layout::{ use rustc_middle::ty::{self, Ty, TyCtxt}; use rustc_span::Span; use rustc_span::source_map::respan; -use rustc_target::abi::call::FnAbi; -use rustc_target::abi::{HasDataLayout, TargetDataLayout}; +use rustc_target::callconv::FnAbi; use stable_mir::mir::Body; use stable_mir::mir::mono::Instance; use stable_mir::ty::Allocation; diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 73c887b3eeaf..e54a1fc4dd9e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -151,6 +151,43 @@ impl GotocHook for UnsupportedCheck { unreachable!("{UNEXPECTED_CALL}") } + fn handle( + &self, + gcx: &mut GotocCtx, + _instance: Instance, + mut fargs: Vec, + _assign_to: &Place, + target: Option, + span: Span, + ) -> Stmt { + assert_eq!(fargs.len(), 1); + let msg = fargs.pop().unwrap(); + let msg = gcx.extract_const_message(&msg).unwrap(); + let caller_loc = gcx.codegen_caller_span_stable(span); + if let Some(target) = target { + Stmt::block( + vec![ + gcx.codegen_assert_assume_false( + PropertyClass::UnsupportedConstruct, + &msg, + caller_loc, + ), + Stmt::goto(bb_label(target), caller_loc), + ], + caller_loc, + ) + } else { + gcx.codegen_assert_assume_false(PropertyClass::UnsupportedConstruct, &msg, caller_loc) + } + } +} + +struct SafetyCheck; +impl GotocHook for SafetyCheck { + fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool { + unreachable!("{UNEXPECTED_CALL}") + } + fn handle( &self, gcx: &mut GotocCtx, @@ -168,12 +205,7 @@ impl GotocHook for UnsupportedCheck { let caller_loc = gcx.codegen_caller_span_stable(span); Stmt::block( vec![ - gcx.codegen_assert_assume( - cond, - PropertyClass::UnsupportedConstruct, - &msg, - caller_loc, - ), + gcx.codegen_assert_assume(cond, PropertyClass::SafetyCheck, &msg, caller_loc), Stmt::goto(bb_label(target), caller_loc), ], caller_loc, @@ -181,8 +213,8 @@ impl GotocHook for UnsupportedCheck { } } -struct SafetyCheck; -impl GotocHook for SafetyCheck { +struct SafetyCheckNoAssume; +impl GotocHook for SafetyCheckNoAssume { fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool { unreachable!("{UNEXPECTED_CALL}") } @@ -204,7 +236,7 @@ impl GotocHook for SafetyCheck { let caller_loc = gcx.codegen_caller_span_stable(span); Stmt::block( vec![ - gcx.codegen_assert_assume(cond, PropertyClass::SafetyCheck, &msg, caller_loc), + gcx.codegen_assert(cond, PropertyClass::SafetyCheck, &msg, caller_loc), Stmt::goto(bb_label(target), caller_loc), ], caller_loc, @@ -738,6 +770,7 @@ pub fn fn_hooks() -> GotocHooks { (KaniHook::Cover, Rc::new(Cover)), (KaniHook::AnyRaw, Rc::new(Nondet)), (KaniHook::SafetyCheck, Rc::new(SafetyCheck)), + (KaniHook::SafetyCheckNoAssume, Rc::new(SafetyCheckNoAssume)), (KaniHook::IsAllocated, Rc::new(IsAllocated)), (KaniHook::PointerObject, Rc::new(PointerObject)), (KaniHook::PointerOffset, Rc::new(PointerOffset)), diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index 253a9b88a52c..e4bfba3113b0 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/kani-compiler/src/kani_compiler.rs @@ -3,7 +3,7 @@ //! This module defines all compiler extensions that form the Kani compiler. //! -//! The [KaniCompiler] can be used across multiple rustc driver runs ([RunCompiler::run()]), +//! The [KaniCompiler] can be used across multiple rustc driver runs ([`rustc_driver::run_compiler`]), //! which is used to implement stubs. //! //! In the first run, [KaniCompiler::config] will implement the compiler configuration and it will @@ -25,7 +25,7 @@ use crate::kani_queries::QueryDb; use crate::session::init_session; use clap::Parser; use rustc_codegen_ssa::traits::CodegenBackend; -use rustc_driver::{Callbacks, Compilation, RunCompiler}; +use rustc_driver::{Callbacks, Compilation, run_compiler}; use rustc_interface::Config; use rustc_middle::ty::TyCtxt; use rustc_session::config::ErrorOutputType; @@ -34,7 +34,7 @@ use std::sync::{Arc, Mutex}; use tracing::debug; /// Run the Kani flavour of the compiler. -/// This may require multiple runs of the rustc driver ([RunCompiler::run]). +/// This may require multiple runs of the rustc driver ([`rustc_driver::run_compiler`]). pub fn run(args: Vec) { let mut kani_compiler = KaniCompiler::new(); kani_compiler.run(args); @@ -96,10 +96,7 @@ impl KaniCompiler { /// actually invoke the rust compiler multiple times. pub fn run(&mut self, args: Vec) { debug!(?args, "run_compilation_session"); - let queries = self.queries.clone(); - let mut compiler = RunCompiler::new(&args, self); - compiler.set_make_codegen_backend(Some(Box::new(move |_cfg| backend(queries)))); - compiler.run(); + run_compiler(&args, self); } } @@ -108,6 +105,10 @@ impl Callbacks for KaniCompiler { /// Configure the [KaniCompiler] `self` object during the [CompilationStage::Init]. fn config(&mut self, config: &mut Config) { let mut args = vec!["kani-compiler".to_string()]; + config.make_codegen_backend = Some(Box::new({ + let queries = self.queries.clone(); + move |_cfg| backend(queries) + })); args.extend(config.opts.cg.llvm_args.iter().cloned()); let args = Arguments::parse_from(args); init_session(&args, matches!(config.opts.error_format, ErrorOutputType::Json { .. })); diff --git a/kani-compiler/src/kani_middle/analysis.rs b/kani-compiler/src/kani_middle/analysis.rs index b232db8feecb..f0828dace441 100644 --- a/kani-compiler/src/kani_middle/analysis.rs +++ b/kani-compiler/src/kani_middle/analysis.rs @@ -149,7 +149,7 @@ impl From<&Terminator> for Key { TerminatorKind::Drop { .. } => Key("Drop"), TerminatorKind::Goto { .. } => Key("Goto"), TerminatorKind::InlineAsm { .. } => Key("InlineAsm"), - TerminatorKind::Resume { .. } => Key("Resume"), + TerminatorKind::Resume => Key("Resume"), TerminatorKind::Return => Key("Return"), TerminatorKind::SwitchInt { .. } => Key("SwitchInt"), TerminatorKind::Unreachable => Key("Unreachable"), diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 6d366f432e2a..bdd6db831d6c 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -394,7 +394,7 @@ impl<'tcx> KaniAttributes<'tcx> { attrs.iter().for_each(|attr| self.check_proof_attribute(kind, attr)) } KaniAttributeKind::StubVerified => { - expect_single(self.tcx, kind, &attrs); + self.check_stub_verified(); } KaniAttributeKind::FnMarker | KaniAttributeKind::CheckedWith @@ -591,15 +591,29 @@ impl<'tcx> KaniAttributes<'tcx> { } } - fn handle_stub_verified(&self, harness: &mut HarnessAttributes) { + fn check_stub_verified(&self) { let dcx = self.tcx.dcx(); + let mut seen = HashSet::new(); for (name, def_id, span) in self.interpret_stub_verified_attribute() { + if seen.contains(&name) { + dcx.struct_span_warn( + span, + format!("Multiple occurrences of `stub_verified({})`.", name), + ) + .with_span_note( + self.tcx.def_span(def_id), + format!("Use a single `stub_verified({})` annotation.", name), + ) + .emit(); + } else { + seen.insert(name); + } if KaniAttributes::for_item(self.tcx, def_id).contract_attributes().is_none() { dcx.struct_span_err( span, format!( - "Failed to generate verified stub: Function `{}` has no contract.", - self.item_name(), + "Target function in `stub_verified({})` has no contract.", + name, ), ) .with_span_note( @@ -612,6 +626,16 @@ impl<'tcx> KaniAttributes<'tcx> { .emit(); return; } + } + } + + /// Adds the verified stub names to the `harness.verified_stubs`. + /// + /// This method must be called after `check_stub_verified`, to ensure that + /// the target names are known and have contracts, and there are no + /// duplicate target names. + fn handle_stub_verified(&self, harness: &mut HarnessAttributes) { + for (name, _, _) in self.interpret_stub_verified_attribute() { harness.verified_stubs.push(name.to_string()) } } diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 072528f9a765..1fc659ea2f80 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -8,8 +8,11 @@ //! according to their stub configuration. use crate::args::ReachabilityType; -use crate::kani_middle::attributes::is_proof_harness; -use crate::kani_middle::metadata::{gen_contracts_metadata, gen_proof_metadata}; +use crate::kani_middle::attributes::{KaniAttributes, is_proof_harness}; +use crate::kani_middle::kani_functions::{KaniIntrinsic, KaniModel}; +use crate::kani_middle::metadata::{ + gen_automatic_proof_metadata, gen_contracts_metadata, gen_proof_metadata, +}; use crate::kani_middle::reachability::filter_crate_items; use crate::kani_middle::resolve::expect_resolve_fn; use crate::kani_middle::stubbing::{check_compatibility, harness_stub_map}; @@ -20,8 +23,8 @@ use rustc_middle::ty::TyCtxt; use rustc_session::config::OutputType; use rustc_smir::rustc_internal; use stable_mir::CrateDef; -use stable_mir::mir::mono::Instance; -use stable_mir::ty::{FnDef, IndexedVal, RigidTy, TyKind}; +use stable_mir::mir::{TerminatorKind, mono::Instance}; +use stable_mir::ty::{FnDef, GenericArgKind, GenericArgs, IndexedVal, RigidTy, TyKind}; use std::collections::{BTreeMap, BTreeSet, HashMap, HashSet}; use std::fs::File; use std::io::BufWriter; @@ -57,26 +60,66 @@ pub struct CodegenUnit { impl CodegenUnits { pub fn new(queries: &QueryDb, tcx: TyCtxt) -> Self { let crate_info = CrateInfo { name: stable_mir::local_crate().name.as_str().into() }; - if queries.args().reachability_analysis == ReachabilityType::Harnesses { - let base_filepath = tcx.output_filenames(()).path(OutputType::Object); - let base_filename = base_filepath.as_path(); - let harnesses = filter_crate_items(tcx, |_, instance| is_proof_harness(tcx, instance)); - let all_harnesses = harnesses - .into_iter() - .map(|harness| { - let metadata = gen_proof_metadata(tcx, harness, &base_filename); - (harness, metadata) - }) - .collect::>(); + let base_filepath = tcx.output_filenames(()).path(OutputType::Object); + let base_filename = base_filepath.as_path(); + let args = queries.args(); + match args.reachability_analysis { + ReachabilityType::Harnesses => { + let all_harnesses = get_all_manual_harnesses(tcx, base_filename); + // Even if no_stubs is empty we still need to store rustc metadata. + let units = group_by_stubs(tcx, &all_harnesses); + validate_units(tcx, &units); + debug!(?units, "CodegenUnits::new"); + CodegenUnits { units, harness_info: all_harnesses, crate_info } + } + ReachabilityType::AllFns => { + let mut all_harnesses = get_all_manual_harnesses(tcx, base_filename); + let mut units = group_by_stubs(tcx, &all_harnesses); + validate_units(tcx, &units); - // Even if no_stubs is empty we still need to store rustc metadata. - let units = group_by_stubs(tcx, &all_harnesses); - validate_units(tcx, &units); - debug!(?units, "CodegenUnits::new"); - CodegenUnits { units, harness_info: all_harnesses, crate_info } - } else { - // Leave other reachability type handling as is for now. - CodegenUnits { units: vec![], harness_info: HashMap::default(), crate_info } + let kani_fns = queries.kani_functions(); + let kani_harness_intrinsic = + kani_fns.get(&KaniIntrinsic::AutomaticHarness.into()).unwrap(); + let kani_any_inst = kani_fns.get(&KaniModel::Any.into()).unwrap(); + + let verifiable_fns = filter_crate_items(tcx, |_, instance: Instance| -> bool { + // If the user specified functions to include or exclude, only allow instances matching those filters. + let user_included = if !args.autoharness_included_functions.is_empty() { + fn_list_contains_instance(&instance, &args.autoharness_included_functions) + } else if !args.autoharness_excluded_functions.is_empty() { + !fn_list_contains_instance(&instance, &args.autoharness_excluded_functions) + } else { + true + }; + user_included + && is_eligible_for_automatic_harness(tcx, instance, *kani_any_inst) + }); + let automatic_harnesses = get_all_automatic_harnesses( + tcx, + verifiable_fns, + *kani_harness_intrinsic, + base_filename, + ); + // We generate one contract harness per function under contract, so each harness is in its own unit, + // and these harnesses have no stubs. + units.extend( + automatic_harnesses + .keys() + .map(|harness| CodegenUnit { + harnesses: vec![*harness], + stubs: HashMap::default(), + }) + .collect::>(), + ); + all_harnesses.extend(automatic_harnesses); + // No need to validate the units again because validation only checks stubs, and we haven't added any stubs. + debug!(?units, "CodegenUnits::new"); + CodegenUnits { units, harness_info: all_harnesses, crate_info } + } + _ => { + // Leave other reachability type handling as is for now. + CodegenUnits { units: vec![], harness_info: HashMap::default(), crate_info } + } } } @@ -94,7 +137,15 @@ impl CodegenUnits { /// We flag that the harness contains usage of loop contracts. pub fn store_loop_contracts(&mut self, harnesses: &[Harness]) { for harness in harnesses { - self.harness_info.get_mut(harness).unwrap().has_loop_contracts = true; + let metadata = self.harness_info.get_mut(harness).unwrap(); + metadata.has_loop_contracts = true; + // If we're generating this harness automatically and we encounter a loop contract, + // ensure that the HarnessKind is updated to be a contract harness + // targeting the function to verify. + if metadata.is_automatically_generated { + metadata.attributes.kind = + HarnessKind::ProofForContract { target_fn: metadata.pretty_name.clone() } + } } } @@ -252,3 +303,89 @@ fn apply_transitivity(tcx: TyCtxt, harness: Harness, stubs: Stubs) -> Stubs { } new_stubs } + +/// Fetch all manual harnesses (i.e., functions provided by the user) and generate their metadata +fn get_all_manual_harnesses( + tcx: TyCtxt, + base_filename: &Path, +) -> HashMap { + let harnesses = filter_crate_items(tcx, |_, instance| is_proof_harness(tcx, instance)); + harnesses + .into_iter() + .map(|harness| { + let metadata = gen_proof_metadata(tcx, harness, &base_filename); + (harness, metadata) + }) + .collect::>() +} + +/// For each function eligible for automatic verification, +/// generate a harness Instance for it, then generate its metadata. +/// Note that the body of each harness instance is still the dummy body of `kani_harness_intrinsic`; +/// the AutomaticHarnessPass will later transform the bodies of these instances to actually verify the function. +fn get_all_automatic_harnesses( + tcx: TyCtxt, + verifiable_fns: Vec, + kani_harness_intrinsic: FnDef, + base_filename: &Path, +) -> HashMap { + verifiable_fns + .into_iter() + .map(|fn_to_verify| { + // Set the generic arguments of the harness to be the function it is verifying + // so that later, in AutomaticHarnessPass, we can retrieve the function to verify + // and generate the harness body accordingly. + let harness = Instance::resolve( + kani_harness_intrinsic, + &GenericArgs(vec![GenericArgKind::Type(fn_to_verify.ty())]), + ) + .unwrap(); + let metadata = gen_automatic_proof_metadata(tcx, &base_filename, &fn_to_verify); + (harness, metadata) + }) + .collect::>() +} + +/// Determine whether `instance` is eligible for automatic verification. +fn is_eligible_for_automatic_harness(tcx: TyCtxt, instance: Instance, any_inst: FnDef) -> bool { + // `instance` is ineligble if it is a harness or has an nonexistent/empty body + if is_proof_harness(tcx, instance) || !instance.has_body() { + return false; + } + let body = instance.body().unwrap(); + + // `instance` is ineligble if it is an associated item of a Kani trait implementation, + // or part of Kani contract instrumentation. + // FIXME -- find a less hardcoded way of checking the former condition (perhaps upstream PR to StableMIR). + if instance.name().contains("kani::Arbitrary") + || instance.name().contains("kani::Invariant") + || KaniAttributes::for_instance(tcx, instance) + .fn_marker() + .is_some_and(|m| m.as_str() == "kani_contract_mode") + { + return false; + } + + // Each non-generic argument of `instance`` must implement Arbitrary. + body.arg_locals().iter().all(|arg| { + let kani_any_body = + Instance::resolve(any_inst, &GenericArgs(vec![GenericArgKind::Type(arg.ty)])) + .unwrap() + .body() + .unwrap(); + if let TerminatorKind::Call { func, .. } = &kani_any_body.blocks[0].terminator.kind { + if let Some((def, args)) = func.ty(body.arg_locals()).unwrap().kind().fn_def() { + return Instance::resolve(def, &args).is_ok(); + } + } + false + }) +} + +/// Return whether the name of `instance` is included in `fn_list`. +/// If `exact = true`, then `instance`'s exact, fully-qualified name must be in `fn_list`; otherwise, `fn_list` +/// can have a substring of `instance`'s name. +fn fn_list_contains_instance(instance: &Instance, fn_list: &[String]) -> bool { + let pretty_name = instance.name(); + fn_list.contains(&pretty_name) || fn_list.iter().any(|fn_name| pretty_name.contains(fn_name)) +} diff --git a/kani-compiler/src/kani_middle/kani_functions.rs b/kani-compiler/src/kani_middle/kani_functions.rs index 8d1ab5ef939d..01d237bf0773 100644 --- a/kani-compiler/src/kani_middle/kani_functions.rs +++ b/kani-compiler/src/kani_middle/kani_functions.rs @@ -48,6 +48,8 @@ pub enum KaniIntrinsic { CheckedAlignOf, #[strum(serialize = "CheckedSizeOfIntrinsic")] CheckedSizeOf, + #[strum(serialize = "AutomaticHarnessIntrinsic")] + AutomaticHarness, #[strum(serialize = "IsInitializedIntrinsic")] IsInitialized, #[strum(serialize = "ValidValueIntrinsic")] @@ -146,6 +148,8 @@ pub enum KaniHook { PointerOffset, #[strum(serialize = "SafetyCheckHook")] SafetyCheck, + #[strum(serialize = "SafetyCheckNoAssumeHook")] + SafetyCheckNoAssume, #[strum(serialize = "UnsupportedCheckHook")] UnsupportedCheck, #[strum(serialize = "UntrackedDerefHook")] diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs index e3ebb20b71d9..f8de975802e1 100644 --- a/kani-compiler/src/kani_middle/metadata.rs +++ b/kani-compiler/src/kani_middle/metadata.rs @@ -39,6 +39,7 @@ pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) -> goto_file: Some(model_file), contract: Default::default(), has_loop_contracts: false, + is_automatically_generated: false, } } @@ -84,6 +85,48 @@ pub fn gen_contracts_metadata(tcx: TyCtxt) -> Vec { fn_to_data.into_values().collect() } +/// Generate metadata for automatically generated harnesses. +/// For now, we just use the data from the function we are verifying; since we only generate one automatic harness per function, +/// the metdata from that function uniquely identifies the harness. +/// In future iterations of this feature, we will likely have multiple harnesses for a single function (e.g., for generic functions), +/// in which case HarnessMetadata will need to change further to differentiate between those harnesses. +pub fn gen_automatic_proof_metadata( + tcx: TyCtxt, + base_name: &Path, + fn_to_verify: &Instance, +) -> HarnessMetadata { + let def = fn_to_verify.def; + let pretty_name = fn_to_verify.name(); + let mangled_name = fn_to_verify.mangled_name(); + + // Leave the concrete playback instrumentation for now, but this feature does not actually support concrete playback. + let loc = SourceLocation::new(fn_to_verify.body().unwrap().span); + let file_stem = format!("{}_{mangled_name}", base_name.file_stem().unwrap().to_str().unwrap()); + let model_file = base_name.with_file_name(file_stem).with_extension(ArtifactType::SymTabGoto); + + let kani_attributes = KaniAttributes::for_instance(tcx, *fn_to_verify); + let harness_kind = if kani_attributes.has_contract() { + HarnessKind::ProofForContract { target_fn: pretty_name.clone() } + } else { + HarnessKind::Proof + }; + + HarnessMetadata { + pretty_name, + mangled_name, + crate_name: def.krate().name, + original_file: loc.filename, + original_start_line: loc.start_line, + original_end_line: loc.end_line, + attributes: HarnessAttributes::new(harness_kind), + // TODO: This no longer needs to be an Option. + goto_file: Some(model_file), + contract: Default::default(), + has_loop_contracts: false, + is_automatically_generated: true, + } +} + /// Create the harness metadata for a test description. #[allow(dead_code)] pub fn gen_test_metadata( @@ -110,5 +153,6 @@ pub fn gen_test_metadata( goto_file: Some(model_file), contract: Default::default(), has_loop_contracts: false, + is_automatically_generated: false, } } diff --git a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs index c326172ba843..a89baf963e7f 100644 --- a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs +++ b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs @@ -525,7 +525,8 @@ impl<'tcx> PointsToAnalysis<'_, 'tcx> { Rvalue::Use(operand) | Rvalue::ShallowInitBox(operand, _) | Rvalue::Cast(_, operand, _) - | Rvalue::Repeat(operand, ..) => self.successors_for_operand(state, operand), + | Rvalue::Repeat(operand, ..) + | Rvalue::WrapUnsafeBinder(operand, _) => self.successors_for_operand(state, operand), Rvalue::Ref(_, _, ref_place) | Rvalue::RawPtr(_, ref_place) => { // Here, a reference to a place is created, which leaves the place // unchanged. diff --git a/kani-compiler/src/kani_middle/points_to/points_to_graph.rs b/kani-compiler/src/kani_middle/points_to/points_to_graph.rs index 0b52a84eaa59..6e473a84eecc 100644 --- a/kani-compiler/src/kani_middle/points_to/points_to_graph.rs +++ b/kani-compiler/src/kani_middle/points_to/points_to_graph.rs @@ -163,7 +163,8 @@ impl<'tcx> PointsToGraph<'tcx> { | ProjectionElem::Subslice { .. } | ProjectionElem::Downcast(..) | ProjectionElem::OpaqueCast(..) - | ProjectionElem::Subtype(..) => { + | ProjectionElem::Subtype(..) + | ProjectionElem::UnwrapUnsafeBinder(..) => { /* There operations are no-ops w.r.t aliasing since we are tracking it on per-object basis. */ } } diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index dea7cca60844..fdc81e177d1f 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -256,11 +256,11 @@ impl MonoItemsFnCollector<'_, '_> { // A trait object type can have multiple trait bounds but up to one non-auto-trait // bound. This non-auto-trait, named principal, is the only one that can have methods. // https://doc.rust-lang.org/reference/special-types-and-traits.html#auto-traits - let poly_trait_ref = principal.with_self_ty(concrete_ty); + let trait_ref = rustc_internal::internal(self.tcx, principal.with_self_ty(concrete_ty)); + let trait_ref = self.tcx.instantiate_bound_regions_with_erased(trait_ref); // Walk all methods of the trait, including those of its supertraits - let entries = - self.tcx.vtable_entries(rustc_internal::internal(self.tcx, &poly_trait_ref)); + let entries = self.tcx.vtable_entries(trait_ref); let methods = entries.iter().filter_map(|entry| match entry { VtblEntry::MetadataAlign | VtblEntry::MetadataDropInPlace @@ -458,7 +458,7 @@ impl MirVisitor for MonoItemsFnCollector<'_, '_> { // We don't support inline assembly. This shall be replaced by an unsupported // construct during codegen. } - TerminatorKind::Abort { .. } | TerminatorKind::Assert { .. } => { + TerminatorKind::Abort | TerminatorKind::Assert { .. } => { // We generate code for this without invoking any lang item. } TerminatorKind::Goto { .. } @@ -470,6 +470,22 @@ impl MirVisitor for MonoItemsFnCollector<'_, '_> { self.super_terminator(terminator, location); } + + /// Collect any function definition that may occur as a type. + /// + /// The codegen stage will require the definition to be available. + /// This is a conservative approach, since there are cases where the function is never + /// actually used, so we don't need the body. + /// + /// Another alternative would be to lazily declare functions, but it would require a bigger + /// change to codegen. + fn visit_ty(&mut self, ty: &Ty, _: Location) { + if let TyKind::RigidTy(RigidTy::FnDef(def, args)) = ty.kind() { + let instance = Instance::resolve(def, &args).unwrap(); + self.collect_instance(instance, true); + } + self.super_ty(ty); + } } fn extract_unsize_coercion(tcx: TyCtxt, orig_ty: Ty, dst_trait: Ty) -> (Ty, Ty) { diff --git a/kani-compiler/src/kani_middle/transform/automatic.rs b/kani-compiler/src/kani_middle/transform/automatic.rs new file mode 100644 index 000000000000..705a8ac26a88 --- /dev/null +++ b/kani-compiler/src/kani_middle/transform/automatic.rs @@ -0,0 +1,129 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This module transforms the body of an automatic harness to verify a function. +//! Upon entry to this module, a harness has the dummy body of the automatic_harness Kani intrinsic. +//! We obtain the function its meant to verify by inspecting its generic arguments, +//! then transform its body to be a harness for that function. + +use crate::args::ReachabilityType; +use crate::kani_middle::codegen_units::CodegenUnit; +use crate::kani_middle::kani_functions::{KaniIntrinsic, KaniModel}; +use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceInstruction}; +use crate::kani_middle::transform::{TransformPass, TransformationType}; +use crate::kani_queries::QueryDb; +use rustc_middle::ty::TyCtxt; +use stable_mir::mir::mono::Instance; +use stable_mir::mir::{Body, Operand, Place, TerminatorKind}; +use stable_mir::ty::{FnDef, GenericArgKind, GenericArgs}; +use tracing::debug; + +#[derive(Debug)] +pub struct AutomaticHarnessPass { + /// The FnDef of KaniModel::Any + kani_any: FnDef, + /// All of the automatic harness Instances that we generated in the CodegenUnits constructor + automatic_harnesses: Vec, +} + +impl AutomaticHarnessPass { + // FIXME: this is a bit clunky. + // Historically, in codegen_crate, we reset the BodyTransformation cache on a per-unit basis, + // so the BodyTransformation constructor only accepts a CodegenUnit and thus this constructor can only accept a unit. + // Later, we changed codegen to reset the cache on a per-harness basis (for uninitialized memory instrumentation). + // So BodyTransformation should really be changed to reflect that, so that this constructor can just save the one automatic harness it should transform + // and not all of the possibilities. + pub fn new(unit: &CodegenUnit, query_db: &QueryDb) -> Self { + let kani_fns = query_db.kani_functions(); + let harness_intrinsic = *kani_fns.get(&KaniIntrinsic::AutomaticHarness.into()).unwrap(); + let kani_any = *kani_fns.get(&KaniModel::Any.into()).unwrap(); + let automatic_harnesses = unit + .harnesses + .iter() + .cloned() + .filter(|harness| { + let (def, _) = harness.ty().kind().fn_def().unwrap(); + def == harness_intrinsic + }) + .collect::>(); + Self { kani_any, automatic_harnesses } + } +} + +impl TransformPass for AutomaticHarnessPass { + fn transformation_type() -> TransformationType + where + Self: Sized, + { + TransformationType::Stubbing + } + + fn is_enabled(&self, query_db: &QueryDb) -> bool + where + Self: Sized, + { + matches!(query_db.args().reachability_analysis, ReachabilityType::AllFns) + } + + fn transform(&mut self, _tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) { + debug!(function=?instance.name(), "AutomaticHarnessPass::transform"); + + if !self.automatic_harnesses.contains(&instance) { + return (false, body); + } + + // Retrieve the generic arguments of the harness, which is the type of the function it is verifying, + // and then resolve `fn_to_verify`. + let kind = instance.args().0[0].expect_ty().kind(); + let (def, args) = kind.fn_def().unwrap(); + let fn_to_verify = Instance::resolve(def, &args).unwrap(); + let fn_to_verify_body = fn_to_verify.body().unwrap(); + + let mut harness_body = MutableBody::from(body); + harness_body.clear_body(TerminatorKind::Return); + let mut source = SourceInstruction::Terminator { bb: 0 }; + + let mut arg_locals = vec![]; + + // For each argument of `fn_to_verify`, create a nondeterministic value of its type + // by generating a kani::any() call and saving the result in `arg_local`. + for local_decl in fn_to_verify_body.arg_locals().iter() { + let arg_local = harness_body.new_local( + local_decl.ty, + source.span(harness_body.blocks()), + local_decl.mutability, + ); + let kani_any_inst = Instance::resolve( + self.kani_any, + &GenericArgs(vec![GenericArgKind::Type(local_decl.ty)]), + ) + .unwrap(); + harness_body.insert_call( + &kani_any_inst, + &mut source, + InsertPosition::Before, + vec![], + Place::from(arg_local), + ); + arg_locals.push(arg_local); + } + + let func_to_verify_ret = fn_to_verify_body.ret_local(); + let ret_place = Place::from(harness_body.new_local( + func_to_verify_ret.ty, + source.span(harness_body.blocks()), + func_to_verify_ret.mutability, + )); + + // Call `fn_to_verify` on the nondeterministic arguments generated above. + harness_body.insert_call( + &fn_to_verify, + &mut source, + InsertPosition::Before, + arg_locals.iter().map(|lcl| Operand::Copy(Place::from(*lcl))).collect::>(), + ret_place, + ); + + (true, harness_body.into()) + } +} diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index f2072fb21fb1..6f7b59041d12 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -181,23 +181,31 @@ impl MutableBody { check_type: &CheckType, source: &mut SourceInstruction, position: InsertPosition, - value: Local, + value: Option, msg: &str, ) { - assert_eq!( - self.locals[value].ty, - Ty::bool_ty(), - "Expected boolean value as the assert input" - ); let new_bb = self.blocks.len(); let span = source.span(&self.blocks); - let CheckType::Assert(assert_fn) = check_type; + let msg_op = self.new_str_operand(msg, span); + let (assert_fn, args) = match check_type { + CheckType::SafetyCheck(assert_fn) | CheckType::SafetyCheckNoAssume(assert_fn) => { + assert_eq!( + self.locals[value.unwrap()].ty, + Ty::bool_ty(), + "Expected boolean value as the assert input" + ); + (assert_fn, vec![Operand::Move(Place::from(value.unwrap())), msg_op]) + } + CheckType::UnsupportedCheck(assert_fn) => { + assert!(value.is_none()); + (assert_fn, vec![msg_op]) + } + }; let assert_op = Operand::Copy(Place::from(self.new_local(assert_fn.ty(), span, Mutability::Not))); - let msg_op = self.new_str_operand(msg, span); let kind = TerminatorKind::Call { func: assert_op, - args: vec![Operand::Move(Place::from(value)), msg_op], + args, destination: Place { local: self.new_local(Ty::new_tuple(&[]), span, Mutability::Not), projection: vec![], @@ -441,30 +449,35 @@ impl MutableBody { } } -// TODO: Remove this enum, since we now only support kani's assert. #[derive(Clone, Debug)] pub enum CheckType { - /// This is used by default when the `kani` crate is available. - Assert(Instance), + SafetyCheck(Instance), + SafetyCheckNoAssume(Instance), + UnsupportedCheck(Instance), } impl CheckType { - /// This will create the type of check that is available in the current crate, attempting to - /// create a check that generates an assertion following by an assumption of the same assertion. - pub fn new_assert_assume(queries: &QueryDb) -> CheckType { - let fn_def = queries.kani_functions()[&KaniHook::Assert.into()]; - CheckType::Assert(Instance::resolve(fn_def, &GenericArgs(vec![])).unwrap()) - } - - /// This will create the type of check that is available in the current crate, attempting to - /// create a check that generates an assertion, without assuming the condition afterwards. - /// - /// If `kani` crate is available, this will return [CheckType::Assert], and the instance will - /// point to `kani::assert`. Otherwise, we will collect the `core::panic_str` method and return - /// [CheckType::Panic]. - pub fn new_assert(queries: &QueryDb) -> CheckType { - let fn_def = queries.kani_functions()[&KaniHook::Check.into()]; - CheckType::Assert(Instance::resolve(fn_def, &GenericArgs(vec![])).unwrap()) + /// This will create the type of safety check that is available in the current crate, attempting + /// to create a check that generates an assertion following by an assumption of the same + /// assertion. + pub fn new_safety_check_assert_assume(queries: &QueryDb) -> CheckType { + let fn_def = queries.kani_functions()[&KaniHook::SafetyCheck.into()]; + CheckType::SafetyCheck(Instance::resolve(fn_def, &GenericArgs(vec![])).unwrap()) + } + + /// This will create the type of safety check that is available in the current crate, attempting + /// to create a check that generates an assertion, but not following by an assumption. + pub fn new_safety_check_assert_no_assume(queries: &QueryDb) -> CheckType { + let fn_def = queries.kani_functions()[&KaniHook::SafetyCheckNoAssume.into()]; + CheckType::SafetyCheckNoAssume(Instance::resolve(fn_def, &GenericArgs(vec![])).unwrap()) + } + + /// This will create the type of operation-unsupported check that is available in the current + /// crate, attempting to create a check that generates an assertion following by an assumption + /// of the same assertion. + pub fn new_unsupported_check_assert_assume_false(queries: &QueryDb) -> CheckType { + let fn_def = queries.kani_functions()[&KaniHook::UnsupportedCheck.into()]; + CheckType::UnsupportedCheck(Instance::resolve(fn_def, &GenericArgs(vec![])).unwrap()) } } diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/mod.rs index 19d625da6c53..15d5af1dced6 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/mod.rs @@ -33,13 +33,22 @@ mod instrumentation_visitor; #[derive(Debug)] pub struct DelayedUbPass { - pub check_type: CheckType, + pub safety_check_type: CheckType, + pub unsupported_check_type: CheckType, pub mem_init_fn_cache: HashMap, } impl DelayedUbPass { - pub fn new(check_type: CheckType, queries: &QueryDb) -> Self { - Self { check_type, mem_init_fn_cache: queries.kani_functions().clone() } + pub fn new( + safety_check_type: CheckType, + unsupported_check_type: CheckType, + queries: &QueryDb, + ) -> Self { + Self { + safety_check_type, + unsupported_check_type, + mem_init_fn_cache: queries.kani_functions().clone(), + } } } @@ -122,7 +131,8 @@ impl GlobalPass for DelayedUbPass { let (instrumentation_added, body) = UninitInstrumenter::run( body, instance, - self.check_type.clone(), + self.safety_check_type.clone(), + self.unsupported_check_type.clone(), &mut self.mem_init_fn_cache, target_finder, ); diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs index 892c2086c65c..e7178e2a7eb0 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs @@ -70,7 +70,8 @@ const SKIPPED_ITEMS: &[KaniFunction] = &[ /// Instruments the code with checks for uninitialized memory, agnostic to the source of targets. pub struct UninitInstrumenter<'a> { - check_type: CheckType, + safety_check_type: CheckType, + unsupported_check_type: CheckType, /// Used to cache FnDef lookups of injected memory initialization functions. mem_init_fn_cache: &'a mut HashMap, } @@ -80,11 +81,13 @@ impl<'a> UninitInstrumenter<'a> { pub(crate) fn run( body: Body, instance: Instance, - check_type: CheckType, + safety_check_type: CheckType, + unsupported_check_type: CheckType, mem_init_fn_cache: &'a mut HashMap, target_finder: impl TargetFinder, ) -> (bool, Body) { - let mut instrumenter = Self { check_type, mem_init_fn_cache }; + let mut instrumenter = + Self { safety_check_type, unsupported_check_type, mem_init_fn_cache }; let body = MutableBody::from(body); let (changed, new_body) = instrumenter.instrument(body, instance, target_finder); (changed, new_body.into()) @@ -134,12 +137,11 @@ impl<'a> UninitInstrumenter<'a> { source: &mut SourceInstruction, operation: MemoryInitOp, ) { - if let MemoryInitOp::Unsupported { reason } | MemoryInitOp::TriviallyUnsafe { reason } = - &operation - { - // If the operation is unsupported or trivially accesses uninitialized memory, encode - // the check as `assert!(false)`. - self.inject_assert_false(body, source, operation.position(), reason); + if let MemoryInitOp::Unsupported { reason } = &operation { + self.inject_unsupported_check(body, source, operation.position(), reason); + return; + } else if let MemoryInitOp::TriviallyUnsafe { reason } = &operation { + self.inject_safety_check(body, source, operation.position(), reason); return; }; @@ -162,7 +164,7 @@ impl<'a> UninitInstrumenter<'a> { let reason = format!( "Kani currently doesn't support checking memory initialization for pointers to `{pointee_ty}. {reason}", ); - self.inject_assert_false(body, source, operation.position(), &reason); + self.inject_unsupported_check(body, source, operation.position(), &reason); return; } } @@ -284,7 +286,7 @@ impl<'a> UninitInstrumenter<'a> { } PointeeLayout::TraitObject => { let reason = "Kani does not support reasoning about memory initialization of pointers to trait objects."; - self.inject_assert_false(body, source, operation.position(), reason); + self.inject_unsupported_check(body, source, operation.position(), reason); return; } PointeeLayout::Union { .. } => { @@ -292,7 +294,7 @@ impl<'a> UninitInstrumenter<'a> { // TODO: we perhaps need to check that the union at least contains an intersection // of all layouts initialized. let reason = "Interaction between raw pointers and unions is not yet supported."; - self.inject_assert_false(body, source, operation.position(), reason); + self.inject_unsupported_check(body, source, operation.position(), reason); return; } }; @@ -309,10 +311,10 @@ impl<'a> UninitInstrumenter<'a> { _ => unreachable!(), }; body.insert_check( - &self.check_type, + &self.safety_check_type, source, operation.position(), - ret_place.local, + Some(ret_place.local), &format!( "Undefined Behavior: Reading from an uninitialized pointer of type `{operand_ty}`" ), @@ -452,7 +454,7 @@ impl<'a> UninitInstrumenter<'a> { None => { let reason = "Interaction between raw pointers and unions is not yet supported."; - self.inject_assert_false(body, source, operation.position(), reason); + self.inject_unsupported_check(body, source, operation.position(), reason); return; } }; @@ -617,7 +619,7 @@ impl<'a> UninitInstrumenter<'a> { body.insert_bb(BasicBlock { statements, terminator }, source, operation.position()); } - fn inject_assert_false( + fn inject_safety_check( &self, body: &mut MutableBody, source: &mut SourceInstruction, @@ -631,7 +633,17 @@ impl<'a> UninitInstrumenter<'a> { user_ty: None, })); let result = body.insert_assignment(rvalue, source, position); - body.insert_check(&self.check_type, source, position, result, reason); + body.insert_check(&self.safety_check_type, source, position, Some(result), reason); + } + + fn inject_unsupported_check( + &self, + body: &mut MutableBody, + source: &mut SourceInstruction, + position: InsertPosition, + reason: &str, + ) { + body.insert_check(&self.unsupported_check_type, source, position, None, reason); } } diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/mod.rs index b8a8806ec48a..3cba12bf21ee 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/mod.rs @@ -30,7 +30,8 @@ mod uninit_visitor; /// pointers. #[derive(Debug)] pub struct UninitPass { - pub check_type: CheckType, + pub safety_check_type: CheckType, + pub unsupported_check_type: CheckType, pub mem_init_fn_cache: HashMap, } @@ -66,7 +67,8 @@ impl TransformPass for UninitPass { let (instrumentation_added, body) = UninitInstrumenter::run( new_body.into(), instance, - self.check_type.clone(), + self.safety_check_type.clone(), + self.unsupported_check_type.clone(), &mut self.mem_init_fn_cache, CheckUninitVisitor::new(), ); diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/relevant_instruction.rs b/kani-compiler/src/kani_middle/transform/check_uninit/relevant_instruction.rs index 9ad23071df4a..7469508e2c70 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/relevant_instruction.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/relevant_instruction.rs @@ -6,7 +6,7 @@ use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceInstruction}; use stable_mir::{ - mir::{FieldIdx, Mutability, Operand, Place, Rvalue, Statement, StatementKind}, + mir::{FieldIdx, Mutability, Operand, Place, RawPtrKind, Rvalue, Statement, StatementKind}, ty::{RigidTy, Ty}, }; use strum_macros::AsRefStr; @@ -123,7 +123,7 @@ impl MemoryInitOp { Operand::Copy(place) | Operand::Move(place) => place, Operand::Constant(_) => unreachable!(), }; - let rvalue = Rvalue::AddressOf(Mutability::Not, place.clone()); + let rvalue = Rvalue::AddressOf(RawPtrKind::Const, place.clone()); rvalue.ty(body.locals()).unwrap() } MemoryInitOp::Unsupported { .. } | MemoryInitOp::TriviallyUnsafe { .. } => { @@ -147,7 +147,7 @@ impl MemoryInitOp { MemoryInitOp::AssignUnion { lvalue, .. } => { // It does not matter which operand to return for layout generation, since both of // them have the same pointee type. - let address_of = Rvalue::AddressOf(Mutability::Not, lvalue.clone()); + let address_of = Rvalue::AddressOf(RawPtrKind::Const, lvalue.clone()); address_of.ty(body.locals()).unwrap() } } @@ -271,7 +271,7 @@ fn mk_ref( Operand::Copy(place) | Operand::Move(place) => place, Operand::Constant(_) => unreachable!(), }; - let rvalue = Rvalue::AddressOf(Mutability::Not, place.clone()); + let rvalue = Rvalue::AddressOf(RawPtrKind::Const, place.clone()); let ret_ty = rvalue.ty(body.locals()).unwrap(); let result = body.new_local(ret_ty, span, Mutability::Not); let stmt = Statement { kind: StatementKind::Assign(Place::from(result), rvalue), span }; diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs index eba23503dacb..8689bf6c59ac 100644 --- a/kani-compiler/src/kani_middle/transform/check_values.rs +++ b/kani-compiler/src/kani_middle/transform/check_values.rs @@ -27,12 +27,12 @@ use stable_mir::abi::{FieldsShape, Scalar, TagEncoding, ValueAbi, VariantsShape, use stable_mir::mir::mono::Instance; use stable_mir::mir::visit::{Location, PlaceContext, PlaceRef}; use stable_mir::mir::{ - AggregateKind, BasicBlockIdx, BinOp, Body, CastKind, ConstOperand, FieldIdx, Local, LocalDecl, - MirVisitor, Mutability, NonDivergingIntrinsic, Operand, Place, ProjectionElem, Rvalue, + AggregateKind, BasicBlockIdx, BinOp, Body, CastKind, FieldIdx, Local, LocalDecl, MirVisitor, + Mutability, NonDivergingIntrinsic, Operand, Place, ProjectionElem, RawPtrKind, Rvalue, Statement, StatementKind, Terminator, TerminatorKind, }; use stable_mir::target::{MachineInfo, MachineSize}; -use stable_mir::ty::{AdtKind, IndexedVal, MirConst, RigidTy, Span, Ty, TyKind, UintTy}; +use stable_mir::ty::{AdtKind, IndexedVal, RigidTy, Span, Ty, TyKind, UintTy}; use std::fmt::Debug; use strum_macros::AsRefStr; use tracing::{debug, trace}; @@ -40,7 +40,8 @@ use tracing::{debug, trace}; /// Instrument the code with checks for invalid values. #[derive(Debug)] pub struct ValidValuePass { - pub check_type: CheckType, + pub safety_check_type: CheckType, + pub unsupported_check_type: CheckType, } impl TransformPass for ValidValuePass { @@ -86,16 +87,16 @@ impl ValidValuePass { match operation { SourceOp::BytesValidity { ranges, target_ty, rvalue } => { let value = body.insert_assignment(rvalue, &mut source, InsertPosition::Before); - let rvalue_ptr = Rvalue::AddressOf(Mutability::Not, Place::from(value)); + let rvalue_ptr = Rvalue::AddressOf(RawPtrKind::Const, Place::from(value)); for range in ranges { let result = build_limits(body, &range, rvalue_ptr.clone(), &mut source); let msg = format!("Undefined Behavior: Invalid value of type `{target_ty}`",); body.insert_check( - &self.check_type, + &self.safety_check_type, &mut source, InsertPosition::Before, - result, + Some(result), &msg, ); } @@ -106,10 +107,10 @@ impl ValidValuePass { let msg = format!("Undefined Behavior: Invalid value of type `{pointee_ty}`",); body.insert_check( - &self.check_type, + &self.safety_check_type, &mut source, InsertPosition::Before, - result, + Some(result), &msg, ); } @@ -130,14 +131,13 @@ impl ValidValuePass { source: &mut SourceInstruction, reason: &str, ) { - let span = source.span(body.blocks()); - let rvalue = Rvalue::Use(Operand::Constant(ConstOperand { - const_: MirConst::from_bool(false), - span, - user_ty: None, - })); - let result = body.insert_assignment(rvalue, source, InsertPosition::Before); - body.insert_check(&self.check_type, source, InsertPosition::Before, result, reason); + body.insert_check( + &self.unsupported_check_type, + source, + InsertPosition::Before, + None, + reason, + ); } } diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs index 41a41d2e73f7..df5e4209e900 100644 --- a/kani-compiler/src/kani_middle/transform/contracts.rs +++ b/kani-compiler/src/kani_middle/transform/contracts.rs @@ -1,6 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT //! This module contains code related to the MIR-to-MIR pass to enable contracts. +use crate::args::ReachabilityType; use crate::kani_middle::attributes::KaniAttributes; use crate::kani_middle::codegen_units::CodegenUnit; use crate::kani_middle::kani_functions::{KaniIntrinsic, KaniModel}; @@ -341,13 +342,34 @@ impl FunctionWithContractPass { /// verifying. pub fn new(tcx: TyCtxt, queries: &QueryDb, unit: &CodegenUnit) -> FunctionWithContractPass { if let Some(harness) = unit.harnesses.first() { - let attrs = KaniAttributes::for_instance(tcx, *harness); - let check_fn = attrs.interpret_for_contract_attribute().map(|(_, def_id, _)| def_id); - let replace_fns: HashSet<_> = attrs - .interpret_stub_verified_attribute() - .iter() - .map(|(_, def_id, _)| *def_id) - .collect(); + let (check_fn, replace_fns) = { + let harness_generic_args = harness.args().0; + // Manual harnesses have no arguments, so if there are generic arguments, + // we know this is an automatic harness + if matches!(queries.args().reachability_analysis, ReachabilityType::AllFns) + && !harness_generic_args.is_empty() + { + let kind = harness.args().0[0].expect_ty().kind(); + let (def, args) = kind.fn_def().unwrap(); + let fn_to_verify = Instance::resolve(def, &args).unwrap(); + // For automatic harnesses, the target is the function to verify, + // and stubs are empty. + ( + Some(rustc_internal::internal(tcx, fn_to_verify.def.def_id())), + HashSet::default(), + ) + } else { + let attrs = KaniAttributes::for_instance(tcx, *harness); + let check_fn = + attrs.interpret_for_contract_attribute().map(|(_, def_id, _)| def_id); + let replace_fns: HashSet<_> = attrs + .interpret_stub_verified_attribute() + .iter() + .map(|(_, def_id, _)| *def_id) + .collect(); + (check_fn, replace_fns) + } + }; let run_contract_fn = queries.kani_functions().get(&KaniModel::RunContract.into()).copied(); assert!(run_contract_fn.is_some(), "Failed to find Kani run contract function"); diff --git a/kani-compiler/src/kani_middle/transform/internal_mir.rs b/kani-compiler/src/kani_middle/transform/internal_mir.rs index fd499db7c3c6..090c74311fa4 100644 --- a/kani-compiler/src/kani_middle/transform/internal_mir.rs +++ b/kani-compiler/src/kani_middle/transform/internal_mir.rs @@ -42,7 +42,7 @@ impl RustcInternalMir for AggregateKind { internal(tcx, generic_args), maybe_user_type_annotation_index .map(rustc_middle::ty::UserTypeAnnotationIndex::from_usize), - maybe_field_idx.map(rustc_target::abi::FieldIdx::from_usize), + maybe_field_idx.map(rustc_abi::FieldIdx::from_usize), ), AggregateKind::Closure(closure_def, generic_args) => { rustc_middle::mir::AggregateKind::Closure( @@ -207,7 +207,7 @@ impl RustcInternalMir for NullOp { .map(|(variant_idx, field_idx)| { ( internal(tcx, variant_idx), - rustc_target::abi::FieldIdx::from_usize(*field_idx), + rustc_abi::FieldIdx::from_usize(*field_idx), ) }) .collect::>() @@ -215,6 +215,7 @@ impl RustcInternalMir for NullOp { ), ), NullOp::UbChecks => rustc_middle::mir::NullOp::UbChecks, + NullOp::ContractChecks => rustc_middle::mir::NullOp::ContractChecks, } } } @@ -224,8 +225,8 @@ impl RustcInternalMir for Rvalue { fn internal_mir<'tcx>(&self, tcx: TyCtxt<'tcx>) -> Self::T<'tcx> { match self { - Rvalue::AddressOf(mutability, place) => { - rustc_middle::mir::Rvalue::RawPtr(internal(tcx, mutability), internal(tcx, place)) + Rvalue::AddressOf(raw_ptr_kind, place) => { + rustc_middle::mir::Rvalue::RawPtr(internal(tcx, raw_ptr_kind), internal(tcx, place)) } Rvalue::Aggregate(aggregate_kind, operands) => rustc_middle::mir::Rvalue::Aggregate( Box::new(aggregate_kind.internal_mir(tcx)), @@ -545,6 +546,9 @@ impl RustcInternalMir for AssertMessage { found: found.internal_mir(tcx), } } + AssertMessage::NullPointerDereference => { + rustc_middle::mir::AssertMessage::NullPointerDereference + } } } } diff --git a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs index 206c0160a80d..343fc2fe0c92 100644 --- a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs @@ -39,7 +39,7 @@ use tracing::{debug, trace}; /// Generate the body for a few Kani intrinsics. #[derive(Debug)] pub struct IntrinsicGeneratorPass { - check_type: CheckType, + unsupported_check_type: CheckType, /// Used to cache FnDef lookups for models and Kani intrinsics. kani_defs: HashMap, /// Whether the user enabled uninitialized memory checks when they invoked Kani. @@ -74,8 +74,10 @@ impl TransformPass for IntrinsicGeneratorPass { KaniIntrinsic::CheckedSizeOf => (true, self.checked_size_of(body, instance)), KaniIntrinsic::IsInitialized => (true, self.is_initialized_body(body)), KaniIntrinsic::ValidValue => (true, self.valid_value_body(body)), - // This is handled in contracts pass for now. - KaniIntrinsic::WriteAny | KaniIntrinsic::AnyModifies => (false, body), + // The former two are handled in contracts pass for now, while the latter is handled in the the automatic harness pass. + KaniIntrinsic::WriteAny + | KaniIntrinsic::AnyModifies + | KaniIntrinsic::AutomaticHarness => (false, body), } } else { (false, body) @@ -84,11 +86,11 @@ impl TransformPass for IntrinsicGeneratorPass { } impl IntrinsicGeneratorPass { - pub fn new(check_type: CheckType, queries: &QueryDb) -> Self { + pub fn new(unsupported_check_type: CheckType, queries: &QueryDb) -> Self { let enable_uninit = queries.args().ub_check.contains(&ExtraChecks::Uninit); let kani_defs = queries.kani_functions().clone(); debug!(?kani_defs, ?enable_uninit, "IntrinsicGeneratorPass::new"); - IntrinsicGeneratorPass { check_type, enable_uninit, kani_defs } + IntrinsicGeneratorPass { unsupported_check_type, enable_uninit, kani_defs } } /// Generate the body for valid value. Which should be something like: @@ -149,21 +151,14 @@ impl IntrinsicGeneratorPass { } Err(msg) => { // We failed to retrieve all the valid ranges. - let rvalue = Rvalue::Use(Operand::Constant(ConstOperand { - const_: MirConst::from_bool(false), - span, - user_ty: None, - })); - let result = - new_body.insert_assignment(rvalue, &mut terminator, InsertPosition::Before); let reason = format!( "Kani currently doesn't support checking validity of `{target_ty}`. {msg}" ); new_body.insert_check( - &self.check_type, + &self.unsupported_check_type, &mut terminator, InsertPosition::Before, - result, + None, &reason, ); } @@ -312,39 +307,25 @@ impl IntrinsicGeneratorPass { ); } PointeeLayout::TraitObject => { - let rvalue = Rvalue::Use(Operand::Constant(ConstOperand { - const_: MirConst::from_bool(false), - span: source.span(new_body.blocks()), - user_ty: None, - })); - let result = - new_body.insert_assignment(rvalue, &mut source, InsertPosition::Before); let reason: &str = "Kani does not support reasoning about memory initialization of pointers to trait objects."; new_body.insert_check( - &self.check_type, + &self.unsupported_check_type, &mut source, InsertPosition::Before, - result, + None, &reason, ); } PointeeLayout::Union { .. } => { - let rvalue = Rvalue::Use(Operand::Constant(ConstOperand { - const_: MirConst::from_bool(false), - span: source.span(new_body.blocks()), - user_ty: None, - })); - let result = - new_body.insert_assignment(rvalue, &mut source, InsertPosition::Before); let reason: &str = "Kani does not yet support using initialization predicates on unions."; new_body.insert_check( - &self.check_type, + &self.unsupported_check_type, &mut source, InsertPosition::Before, - result, + None, &reason, ); } @@ -352,21 +333,14 @@ impl IntrinsicGeneratorPass { } Err(reason) => { // We failed to retrieve the type layout. - let rvalue = Rvalue::Use(Operand::Constant(ConstOperand { - const_: MirConst::from_bool(false), - span: source.span(new_body.blocks()), - user_ty: None, - })); - let result = - new_body.insert_assignment(rvalue, &mut source, InsertPosition::Before); let reason = format!( "Kani currently doesn't support checking memory initialization for pointers to `{pointee_ty}. {reason}", ); new_body.insert_check( - &self.check_type, + &self.unsupported_check_type, &mut source, InsertPosition::Before, - result, + None, &reason, ); } diff --git a/kani-compiler/src/kani_middle/transform/mod.rs b/kani-compiler/src/kani_middle/transform/mod.rs index 32caea57750e..fbe9bebf42f8 100644 --- a/kani-compiler/src/kani_middle/transform/mod.rs +++ b/kani-compiler/src/kani_middle/transform/mod.rs @@ -26,6 +26,7 @@ use crate::kani_middle::transform::kani_intrinsics::IntrinsicGeneratorPass; use crate::kani_middle::transform::loop_contracts::LoopContractPass; use crate::kani_middle::transform::stubs::{ExternFnStubPass, FnStubPass}; use crate::kani_queries::QueryDb; +use automatic::AutomaticHarnessPass; use dump_mir_pass::DumpMirPass; use rustc_middle::ty::TyCtxt; use stable_mir::mir::Body; @@ -36,6 +37,7 @@ use std::fmt::Debug; use crate::kani_middle::transform::rustc_intrinsics::RustcIntrinsicsPass; pub use internal_mir::RustcInternalMir; +mod automatic; pub(crate) mod body; mod check_uninit; mod check_values; @@ -70,14 +72,23 @@ impl BodyTransformation { inst_passes: vec![], cache: Default::default(), }; - let check_type = CheckType::new_assert_assume(queries); + let safety_check_type = CheckType::new_safety_check_assert_assume(queries); + let unsupported_check_type = CheckType::new_unsupported_check_assert_assume_false(queries); + // This has to come first, since creating harnesses affects later stubbing and contract passes. + transformer.add_pass(queries, AutomaticHarnessPass::new(unit, queries)); transformer.add_pass(queries, FnStubPass::new(&unit.stubs)); transformer.add_pass(queries, ExternFnStubPass::new(&unit.stubs)); transformer.add_pass(queries, FunctionWithContractPass::new(tcx, queries, &unit)); // This has to come after the contract pass since we want this to only replace the closure // body that is relevant for this harness. transformer.add_pass(queries, AnyModifiesPass::new(tcx, queries, &unit)); - transformer.add_pass(queries, ValidValuePass { check_type: check_type.clone() }); + transformer.add_pass( + queries, + ValidValuePass { + safety_check_type: safety_check_type.clone(), + unsupported_check_type: unsupported_check_type.clone(), + }, + ); // Putting `UninitPass` after `ValidValuePass` makes sure that the code generated by // `UninitPass` does not get unnecessarily instrumented by valid value checks. However, it // would also make sense to check that the values are initialized before checking their @@ -87,11 +98,13 @@ impl BodyTransformation { queries, UninitPass { // Since this uses demonic non-determinism under the hood, should not assume the assertion. - check_type: CheckType::new_assert(queries), + safety_check_type: CheckType::new_safety_check_assert_no_assume(queries), + unsupported_check_type: unsupported_check_type.clone(), mem_init_fn_cache: queries.kani_functions().clone(), }, ); - transformer.add_pass(queries, IntrinsicGeneratorPass::new(check_type, &queries)); + transformer + .add_pass(queries, IntrinsicGeneratorPass::new(unsupported_check_type, &queries)); transformer.add_pass(queries, LoopContractPass::new(tcx, queries, &unit)); transformer.add_pass(queries, RustcIntrinsicsPass::new(&queries)); transformer @@ -194,8 +207,14 @@ pub struct GlobalPasses { impl GlobalPasses { pub fn new(queries: &QueryDb, tcx: TyCtxt) -> Self { let mut global_passes = GlobalPasses { global_passes: vec![] }; - global_passes - .add_global_pass(queries, DelayedUbPass::new(CheckType::new_assert(queries), queries)); + global_passes.add_global_pass( + queries, + DelayedUbPass::new( + CheckType::new_safety_check_assert_assume(queries), + CheckType::new_unsupported_check_assert_assume_false(queries), + queries, + ), + ); global_passes.add_global_pass(queries, DumpMirPass::new(tcx)); global_passes } diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs index 761d9eba7a45..106ad662b3ae 100644 --- a/kani-compiler/src/main.rs +++ b/kani-compiler/src/main.rs @@ -52,7 +52,7 @@ mod kani_middle; mod kani_queries; mod session; -use rustc_driver::{RunCompiler, TimePassesCallbacks}; +use rustc_driver::{TimePassesCallbacks, run_compiler}; use std::env; /// Main function. Configure arguments and run the compiler. @@ -65,8 +65,7 @@ fn main() { kani_compiler::run(rustc_args); } else { let mut callbacks = TimePassesCallbacks::default(); - let compiler = RunCompiler::new(&rustc_args, &mut callbacks); - compiler.run(); + run_compiler(&rustc_args, &mut callbacks); } } diff --git a/kani-compiler/src/session.rs b/kani-compiler/src/session.rs index f448afb801cc..8efabb2c9517 100644 --- a/kani-compiler/src/session.rs +++ b/kani-compiler/src/session.rs @@ -4,7 +4,6 @@ //! Module used to configure a compiler session. use crate::args::Arguments; -use rustc_data_structures::sync::Lrc; use rustc_errors::{ ColorConfig, DiagInner, emitter::Emitter, emitter::HumanReadableErrorType, fallback_fluent_bundle, json::JsonEmitter, registry::Registry as ErrorRegistry, @@ -16,6 +15,7 @@ use rustc_span::source_map::SourceMap; use std::io; use std::io::IsTerminal; use std::panic; +use std::sync::Arc; use std::sync::LazyLock; use tracing_subscriber::{EnvFilter, Registry, layer::SubscriberExt}; use tracing_tree::HierarchicalLayer; @@ -57,7 +57,7 @@ static JSON_PANIC_HOOK: LazyLock) + Sync + let mut emitter = JsonEmitter::new( Box::new(io::BufWriter::new(io::stderr())), #[allow(clippy::arc_with_non_send_sync)] - Lrc::new(SourceMap::new(FilePathMapping::empty())), + Some(Arc::new(SourceMap::new(FilePathMapping::empty()))), fallback_bundle, false, HumanReadableErrorType::Default, diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index a2378c407fcc..ec39fbf67dec 100644 --- a/kani-driver/Cargo.toml +++ b/kani-driver/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-driver" -version = "0.58.0" +version = "0.59.0" edition = "2021" description = "Build a project with Kani and run all proof harnesses" license = "MIT OR Apache-2.0" diff --git a/kani-driver/src/args/autoharness_args.rs b/kani-driver/src/args/autoharness_args.rs new file mode 100644 index 000000000000..d7a69070bf41 --- /dev/null +++ b/kani-driver/src/args/autoharness_args.rs @@ -0,0 +1,136 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Implements the subcommand handling of the autoharness subcommand + +use std::path::PathBuf; + +use crate::args::{ValidateArgs, VerificationArgs}; +use clap::{Error, Parser, error::ErrorKind}; +use kani_metadata::UnstableFeature; + +#[derive(Debug, Parser)] +pub struct CommonAutoharnessArgs { + /// If specified, only autoharness functions that match this filter. This option can be provided + /// multiple times, which will verify all functions matching any of the filters. + /// Note that this filter will match against partial names, i.e., providing the name of a module will include all functions from that module. + /// Also note that if the function specified is unable to be automatically verified, this flag will have no effect. + #[arg( + long = "include-function", + num_args(1), + value_name = "FUNCTION", + conflicts_with = "exclude_function" + )] + pub include_function: Vec, + + /// If specified, only autoharness functions that do not match this filter. This option can be provided + /// multiple times, which will verify all functions that do not match any of the filters. + /// Note that this filter will match against partial names, i.e., providing the name of a module will exclude all functions from that module. + #[arg(long = "exclude-function", num_args(1), value_name = "FUNCTION")] + pub exclude_function: Vec, + // TODO: It would be nice if we could borrow --exact here from VerificationArgs to differentiate between partial/exact matches, + // like --harnesses does. Sharing arguments with VerificationArgs doesn't work with our current structure, though. +} + +/// Automatically verify functions in a crate. +#[derive(Debug, Parser)] +pub struct CargoAutoharnessArgs { + #[command(flatten)] + pub common_autoharness_args: CommonAutoharnessArgs, + + #[command(flatten)] + pub verify_opts: VerificationArgs, +} + +/// Automatically verify functions in a file. +#[derive(Debug, Parser)] +pub struct StandaloneAutoharnessArgs { + /// Rust crate's top file location. + #[arg(required = true)] + pub input: PathBuf, + + #[arg(long, hide = true)] + pub crate_name: Option, + + #[command(flatten)] + pub common_autoharness_args: CommonAutoharnessArgs, + + #[command(flatten)] + pub verify_opts: VerificationArgs, +} + +impl ValidateArgs for CargoAutoharnessArgs { + fn validate(&self) -> Result<(), Error> { + self.verify_opts.validate()?; + if !self + .verify_opts + .common_args + .unstable_features + .contains(UnstableFeature::UnstableOptions) + { + return Err(Error::raw( + ErrorKind::MissingRequiredArgument, + format!( + "The `autoharness` subcommand is unstable and requires -Z {}", + UnstableFeature::UnstableOptions + ), + )); + } + + if self + .verify_opts + .common_args + .unstable_features + .contains(UnstableFeature::ConcretePlayback) + { + return Err(Error::raw( + ErrorKind::ArgumentConflict, + "The autoharness subcommand does not support concrete playback", + )); + } + + Ok(()) + } +} + +impl ValidateArgs for StandaloneAutoharnessArgs { + fn validate(&self) -> Result<(), Error> { + self.verify_opts.validate()?; + if !self + .verify_opts + .common_args + .unstable_features + .contains(UnstableFeature::UnstableOptions) + { + return Err(Error::raw( + ErrorKind::MissingRequiredArgument, + format!( + "The `autoharness` subcommand is unstable and requires -Z {}", + UnstableFeature::UnstableOptions + ), + )); + } + if !self.input.is_file() { + return Err(Error::raw( + ErrorKind::InvalidValue, + format!( + "Invalid argument: Input invalid. `{}` is not a regular file.", + self.input.display() + ), + )); + } + + if self + .verify_opts + .common_args + .unstable_features + .contains(UnstableFeature::ConcretePlayback) + { + return Err(Error::raw( + ErrorKind::ArgumentConflict, + "The autoharness subcommand does not support concrete playback", + )); + } + + Ok(()) + } +} diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 9ba06826d200..26e9927cf67c 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -3,6 +3,7 @@ //! Module that define Kani's command line interface. This includes all subcommands. pub mod assess_args; +pub mod autoharness_args; pub mod cargo; pub mod common; pub mod list_args; @@ -145,6 +146,8 @@ pub enum StandaloneSubcommand { VerifyStd(Box), /// List contracts and harnesses. List(Box), + /// Scan the input file for functions eligible for automatic (i.e., harness-free) verification and verify them. + Autoharness(Box), } #[derive(Debug, clap::Parser)] @@ -173,6 +176,9 @@ pub enum CargoKaniSubcommand { /// List contracts and harnesses. List(Box), + + /// Scan the crate for functions eligible for automatic (i.e., harness-free) verification and verify them. + Autoharness(Box), } // Common arguments for invoking Kani for verification purpose. This gets put into KaniContext, @@ -334,6 +340,10 @@ pub struct VerificationArgs { #[arg(long)] pub harness_timeout: Option, + /// Stop the verification process as soon as one of the harnesses fails. + #[arg(long)] + pub fail_fast: bool, + /// Arguments to pass down to Cargo #[command(flatten)] pub cargo: CargoCommonArgs, @@ -483,6 +493,7 @@ impl ValidateArgs for StandaloneArgs { match &self.command { Some(StandaloneSubcommand::VerifyStd(args)) => args.validate()?, Some(StandaloneSubcommand::List(args)) => args.validate()?, + Some(StandaloneSubcommand::Autoharness(args)) => args.validate()?, // TODO: Invoke PlaybackArgs::validate() None | Some(StandaloneSubcommand::Playback(..)) => {} }; @@ -528,6 +539,7 @@ impl ValidateArgs for CargoKaniSubcommand { match self { // Assess doesn't implement validation yet. CargoKaniSubcommand::Assess(_) => Ok(()), + CargoKaniSubcommand::Autoharness(autoharness) => autoharness.validate(), CargoKaniSubcommand::Playback(playback) => playback.validate(), CargoKaniSubcommand::List(list) => list.validate(), } diff --git a/kani-driver/src/assess/mod.rs b/kani-driver/src/assess/mod.rs index ec91918ac8b5..02b3da0974f8 100644 --- a/kani-driver/src/assess/mod.rs +++ b/kani-driver/src/assess/mod.rs @@ -53,7 +53,7 @@ fn assess_project(mut session: KaniSession) -> Result { session.args.jobs = Some(None); // -j, num_cpu } - let project = project::cargo_project(&session, true)?; + let project = project::cargo_project(&mut session, true)?; let cargo_metadata = project.cargo_metadata.as_ref().expect("built with cargo"); let packages_metadata = diff --git a/kani-driver/src/autoharness/mod.rs b/kani-driver/src/autoharness/mod.rs new file mode 100644 index 000000000000..69c49580cd77 --- /dev/null +++ b/kani-driver/src/autoharness/mod.rs @@ -0,0 +1,73 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +use crate::call_cbmc::VerificationStatus; +use crate::call_single_file::to_rustc_arg; +use crate::harness_runner::HarnessResult; +use crate::session::KaniSession; +use anyhow::Result; + +impl KaniSession { + /// Enable autoharness mode. + pub fn enable_autoharness(&mut self) { + self.auto_harness = true; + } + + /// Add the compiler arguments specific to the `autoharness` subcommand. + pub fn add_auto_harness_args(&mut self, included: Vec, excluded: Vec) { + for func in included { + self.pkg_args + .push(to_rustc_arg(vec![format!("--autoharness-include-function {}", func)])); + } + for func in excluded { + self.pkg_args + .push(to_rustc_arg(vec![format!("--autoharness-exclude-function {}", func)])); + } + } + + /// Prints the results from running the `autoharness` subcommand. + pub fn print_autoharness_summary(&self, automatic: Vec<&HarnessResult<'_>>) -> Result<()> { + let (successes, failures): (Vec<_>, Vec<_>) = + automatic.into_iter().partition(|r| r.result.status == VerificationStatus::Success); + + let succeeding = successes.len(); + let failing = failures.len(); + let total = succeeding + failing; + + // TODO: it would be nice if we had access to which functions the user included/excluded here + // so that we could print a comparison for them of any of the included functions that we skipped. + println!("Autoharness Summary:"); + println!( + "Note that Kani will only generate an automatic harness for a function if it determines that each of its arguments implement the Arbitrary trait." + ); + println!( + "Examine the summary closely to determine which functions were automatically verified." + ); + + // Since autoverification skips over some functions, print the successes to make it easier to see what we verified in one place. + for success in successes { + println!("Verification succeeded for - {}", success.harness.pretty_name); + } + + for failure in failures { + println!("Verification failed for - {}", failure.harness.pretty_name); + } + + if total > 0 { + println!( + "Complete - {succeeding} successfully verified functions, {failing} failures, {total} total." + ); + } else { + println!( + "No functions were eligible for automatic verification. Functions can only be automatically verified if each of their arguments implement kani::Arbitrary." + ); + println!( + "If you specified --include-function or --exclude-function, make sure that your filters were not overly restrictive." + ); + } + + // Manual harness summary may come afterward, so separate them with a new line. + println!(); + Ok(()) + } +} diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index b28d8b089d9f..9097713a0016 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -126,7 +126,7 @@ crate-type = ["lib"] } /// Calls `cargo_build` to generate `*.symtab.json` files in `target_dir` - pub fn cargo_build(&self, keep_going: bool) -> Result { + pub fn cargo_build(&mut self, keep_going: bool) -> Result { let build_target = env!("TARGET"); // see build.rs let metadata = self.cargo_metadata(build_target)?; let target_dir = self @@ -183,13 +183,12 @@ crate-type = ["lib"] } // Arguments that will only be passed to the target package. - let mut pkg_args: Vec = vec![]; - pkg_args.extend(["--".to_string(), self.reachability_arg()]); + self.pkg_args.push(self.reachability_arg()); if let Some(backend_arg) = self.backend_arg() { - pkg_args.push(backend_arg); + self.pkg_args.push(backend_arg); } if self.args.no_assert_contracts { - pkg_args.push("--no-assert-contracts".into()); + self.pkg_args.push("--no-assert-contracts".into()); } let mut found_target = false; @@ -202,7 +201,7 @@ crate-type = ["lib"] cmd.args(&cargo_args) .args(vec!["-p", &package.id.to_string()]) .args(verification_target.to_args()) - .args(&pkg_args) + .args(&self.pkg_args) .env("RUSTC", &self.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/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 4e10cb98c650..92c82f25888d 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -233,7 +233,6 @@ impl KaniSession { args.push("--no-pointer-check".into()); } if self.args.checks.overflow_on() { - args.push("--float-overflow-check".into()); args.push("--nan-check".into()); // TODO: Implement conversion checks as an optional check. @@ -310,9 +309,9 @@ impl VerificationResult { /// /// NOTE: We actually ignore the CBMC exit status, in favor of two checks: /// 1. Examining the actual results of CBMC properties. - /// (CBMC will regularly report "failure" but that's just our cover checks.) + /// (CBMC will regularly report "failure" but that's just our cover checks.) /// 2. Positively checking for the presence of results. - /// (Do not mistake lack of results for success: report it as failure.) + /// (Do not mistake lack of results for success: report it as failure.) fn from( output: VerificationOutput, should_panic: bool, @@ -502,7 +501,7 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option = OnceLock::new(); COUNTER_RE.get_or_init(|| { Regex::new( - r#"^(?CounterIncrement|ExpressionUsed)\((?[0-9]+)\) \$(?[^\$]+)\$ - (?.+)"#, + r#"^(?VirtualCounter\(bcb)(?[0-9]+)\) \$(?[^\$]+)\$ - (?.+)"#, ) .unwrap() }) @@ -512,20 +511,14 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option CoverageTerm::Counter(counter_id), - "ExpressionUsed" => CoverageTerm::Expression(counter_id), - _ => unreachable!("counter kind could not be recognized: {:?}", kind), - }; + let term = CoverageTerm::Counter(counter_id); let region = CoverageRegion::from_str(span); let cov_check = CoverageCheck::new(function, term, region, status); diff --git a/kani-driver/src/cbmc_output_parser.rs b/kani-driver/src/cbmc_output_parser.rs index bf86ef08c217..79a2c20732b4 100644 --- a/kani-driver/src/cbmc_output_parser.rs +++ b/kani-driver/src/cbmc_output_parser.rs @@ -296,12 +296,20 @@ pub struct TraceItem { /// Struct that represents a trace value. /// /// Note: this struct can have a lot of different fields depending on the value type. -/// The fields included right now are relevant to primitive types. +/// The fields included right now are relevant to primitive types and arrays. #[derive(Clone, Debug, Deserialize)] pub struct TraceValue { pub binary: Option, pub data: Option, pub width: Option, + // Invariant: elements is Some iff binary, data, and width are None. + pub elements: Option>, +} + +/// Struct that represents an element of an array in a trace. +#[derive(Clone, Debug, Deserialize)] +pub struct TraceArrayValue { + pub value: TraceValue, } /// Enum that represents a trace data item. diff --git a/kani-driver/src/concrete_playback/test_generator.rs b/kani-driver/src/concrete_playback/test_generator.rs index 282ae42a7c37..d397c5f00dff 100644 --- a/kani-driver/src/concrete_playback/test_generator.rs +++ b/kani-driver/src/concrete_playback/test_generator.rs @@ -9,7 +9,7 @@ use crate::call_cbmc::VerificationResult; use crate::cbmc_output_parser::Property; use crate::session::KaniSession; use anyhow::{Context, Result}; -use concrete_vals_extractor::{ConcreteVal, extract_harness_values}; +use concrete_vals_extractor::{ConcreteItem, PrimitiveConcreteVal, extract_harness_values}; use kani_metadata::{HarnessKind, HarnessMetadata}; use std::collections::hash_map::DefaultHasher; use std::ffi::OsString; @@ -44,9 +44,9 @@ impl KaniSession { } else { let mut unit_tests: Vec = harness_values .iter() - .map(|(prop, concrete_vals)| { + .map(|(prop, concrete_items)| { let pretty_name = harness.get_harness_name_unqualified(); - format_unit_test(&pretty_name, &concrete_vals, gen_test_doc(harness, prop)) + format_unit_test(&pretty_name, &concrete_items, gen_test_doc(harness, prop)) }) .collect(); unit_tests.dedup_by(|a, b| a.name == b.name); @@ -278,13 +278,13 @@ fn gen_test_doc(harness: &HarnessMetadata, property: &Property) -> String { /// Generate a formatted unit test from a list of concrete values. fn format_unit_test( harness_name: &str, - concrete_vals: &[ConcreteVal], + concrete_items: &[ConcreteItem], doc_str: String, ) -> UnitTest { // Hash the concrete values along with the proof harness name. let mut hasher = DefaultHasher::new(); harness_name.hash(&mut hasher); - concrete_vals.hash(&mut hasher); + concrete_items.hash(&mut hasher); let hash = hasher.finish(); let func_name = format!("kani_concrete_playback_{harness_name}_{hash}"); @@ -295,7 +295,7 @@ fn format_unit_test( format!("{:<4}let concrete_vals: Vec> = vec![", " "), ] .into_iter(); - let formatted_concrete_vals = format_concrete_vals(concrete_vals); + let formatted_concrete_items = format_concrete_items(concrete_items); let func_after_concrete_vals = [ format!("{:<4}];", " "), format!("{:<4}kani::concrete_playback_run(concrete_vals, {harness_name});", " "), @@ -304,15 +304,33 @@ fn format_unit_test( .into_iter(); let full_func: Vec<_> = func_before_concrete_vals - .chain(formatted_concrete_vals) + .chain(formatted_concrete_items) .chain(func_after_concrete_vals) .collect(); UnitTest { code: full_func, name: func_name } } +/// Format concrete items as strings--these make up the body of the concrete test. +fn format_concrete_items(concrete_items: &[ConcreteItem]) -> impl Iterator + '_ { + // Note that ConcreteItem::Arrays are flattened, e.g., given: concrete_items = [ConcreteItem::Array(val1, val2), ConcreteItem::Primitive(val3)], + // we output the formatted strings for val1, val2, and val3, with no grouping of val1 and val2 in an outer vector. + // library::concrete_playback::any_raw_array relies on this formatting assumption. + // This is not a fundamental limitation -- we could group the byte arrays for an array in an outer vector, + // but that could cause confusion if we don't group byte arrays for other types, e.g., a struct with multiple fields. + // So, we leave it flattened for now. + // See the tracking issue for improving this output format at https://github.com/model-checking/kani/issues/1527. + concrete_items.iter().flat_map(|item| match item { + ConcreteItem::Array(vals) => format_concrete_vals(vals), + ConcreteItem::Primitive(val) => format_concrete_vals(std::slice::from_ref(val)), + }) +} + /// Format an initializer expression for a number of concrete values. -fn format_concrete_vals(concrete_vals: &[ConcreteVal]) -> impl Iterator + '_ { +/// Each byte vector has a comment above it with its interpreted value, i.e., its decimal representation. +fn format_concrete_vals( + concrete_vals: &[PrimitiveConcreteVal], +) -> impl Iterator + '_ { /* Given a number of byte vectors, format them as: // interp_concrete_val_1 @@ -362,10 +380,18 @@ struct UnitTest { /// ..., ] } /// ``` mod concrete_vals_extractor { - use crate::cbmc_output_parser::{CheckStatus, Property, TraceItem}; + use crate::cbmc_output_parser::{CheckStatus, Property, TraceItem, TraceValue}; + + #[derive(Hash)] + pub enum ConcreteItem { + Primitive(PrimitiveConcreteVal), + Array(Vec), + } + /// Represents the concrete value of a primitive type--its byte representation and the intepreted value. + /// E.g., a u16 with decimal value 65280 would be PrimitiveConcreteVal { byte_arr: vec![0, 255], interp_val: "65280" }. #[derive(Hash)] - pub struct ConcreteVal { + pub struct PrimitiveConcreteVal { pub byte_arr: Vec, pub interp_val: String, } @@ -373,7 +399,9 @@ mod concrete_vals_extractor { /// Extract a set of concrete values that trigger one assertion /// failure. Each element of the outer vector corresponds to /// inputs triggering one assertion failure or cover statement. - pub fn extract_harness_values(result_items: &[Property]) -> Vec<(&Property, Vec)> { + pub fn extract_harness_values( + result_items: &[Property], + ) -> Vec<(&Property, Vec)> { result_items .iter() .filter(|prop| { @@ -386,70 +414,109 @@ mod concrete_vals_extractor { .trace .as_ref() .expect(&format!("Missing trace for {}", property.property_name())); - let concrete_vals: Vec = + let concrete_items: Vec = trace.iter().filter_map(&extract_from_trace_item).collect(); - (property, concrete_vals) + (property, concrete_items) }) .collect() } - /// Extracts individual bytes returned by kani::any() calls. - fn extract_from_trace_item(trace_item: &TraceItem) -> Option { - if let (Some(lhs), Some(source_location), Some(value)) = - (&trace_item.lhs, &trace_item.source_location, &trace_item.value) - { - if let ( - Some(func), - Some(width_u64), - Some(bit_concrete_val), - Some(interp_concrete_val), - ) = (&source_location.function, value.width, &value.binary, &value.data) - { - if trace_item.step_type == "assignment" - && lhs.starts_with("goto_symex$$return_value") - && func.starts_with("kani::any_raw_") - { - let declared_width = width_u64 as usize; - let actual_width = bit_concrete_val.len(); - assert_eq!( - declared_width, actual_width, - "Declared width of {declared_width} doesn't equal actual width of {actual_width}" - ); - let mut next_num: Vec = Vec::new(); - - // Reverse because of endianess of CBMC trace. - for i in (0..declared_width).step_by(8).rev() { - let str_chunk = &bit_concrete_val[i..i + 8]; - let str_chunk_len = str_chunk.len(); - assert_eq!( - str_chunk_len, 8, - "Tried to read a chunk of 8 bits of actually read {str_chunk_len} bits" - ); - let next_byte = u8::from_str_radix(str_chunk, 2).expect(&format!( - "Couldn't convert the string chunk `{str_chunk}` to u8" - )); - next_num.push(next_byte); - } + /// Extracts individual bytes from a TraceValue for a primitive type + /// to produce a PrimitiveConcreteVal representing that value. + fn extract_primitive_value(value: &TraceValue) -> Option { + assert!( + value.elements.is_none(), + "Expected no array elements for primitive value, but found: {:?}", + value.elements + ); + let (Some(width_u64), Some(bit_concrete_val), Some(interp_concrete_val)) = + (value.width, &value.binary, &value.data) + else { + return None; + }; - // In ARM64 Linux, CBMC will produce a character instead of a number for - // interpreted values because the char type is unsigned in that platform. - // For example, for the value `101` it will produce `'e'` instead of `101`. - // To correct this, we check if the value starts and ends with `'`, and - // convert the character into its ASCII value in that case. - let interp_val = { - let interp_val_str = interp_concrete_val.to_string(); - if interp_val_str.starts_with('\'') && interp_val_str.ends_with('\'') { - let interp_num = interp_val_str.chars().nth(1).unwrap() as u8; - interp_num.to_string() - } else { - interp_val_str - } - }; + let declared_width = width_u64 as usize; + let actual_width = bit_concrete_val.len(); + assert_eq!( + declared_width, actual_width, + "Declared width of {declared_width} doesn't equal actual width of {actual_width}" + ); + let mut next_num: Vec = Vec::new(); + + // Reverse because of endianess of CBMC trace. + for i in (0..declared_width).step_by(8).rev() { + let str_chunk = &bit_concrete_val[i..i + 8]; + let str_chunk_len = str_chunk.len(); + assert_eq!( + str_chunk_len, 8, + "Tried to read a chunk of 8 bits of actually read {str_chunk_len} bits" + ); + let next_byte = u8::from_str_radix(str_chunk, 2) + .expect(&format!("Couldn't convert the string chunk `{str_chunk}` to u8")); + next_num.push(next_byte); + } - return Some(ConcreteVal { byte_arr: next_num, interp_val }); - } + // In ARM64 Linux, CBMC will produce a character instead of a number for + // interpreted values because the char type is unsigned in that platform. + // For example, for the value `101` it will produce `'e'` instead of `101`. + // To correct this, we check if the value starts and ends with `'`, and + // convert the character into its ASCII value in that case. + let interp_val = { + let interp_val_str = interp_concrete_val.to_string(); + if interp_val_str.starts_with('\'') && interp_val_str.ends_with('\'') { + let interp_num = interp_val_str.chars().nth(1).unwrap() as u8; + interp_num.to_string() + } else { + interp_val_str } + }; + + Some(PrimitiveConcreteVal { byte_arr: next_num, interp_val }) + } + + /// Extracts individual bytes from a TraceItem corresponding to a kani::any() call + /// and returns a ConcreteItem representing it. + fn extract_from_trace_item(trace_item: &TraceItem) -> Option { + let (Some(lhs), Some(source_location), Some(value)) = + (&trace_item.lhs, &trace_item.source_location, &trace_item.value) + else { + return None; + }; + + let Some(func) = &source_location.function else { + return None; + }; + + if !(trace_item.step_type == "assignment" + && lhs.starts_with("goto_symex$$return_value") + && func.starts_with("kani::any_raw_")) + { + return None; + } + + if let Some(array_elements) = &value.elements { + let concrete_vals = array_elements + .iter() + .map(|array_value| { + let element_val = extract_primitive_value(&array_value.value); + if let Some(val) = element_val { + val + } else { + // We expect that if we have an array, every value in the array is representable as a primitive type. + // To avoid generating a test with a malformed (i.e., too short) array, we panic instead of returning None + // if converting an element fails. + panic!("Couldn't extract concrete value from {array_value:?}"); + } + }) + .collect::>(); + return Some(ConcreteItem::Array(concrete_vals)); + // At time of writing, if the array length is <= 64, CBMC's trace will include TraceItems for each primitive value of the array, + // as well as the `elements` field with the entire array (for arrays length > 65, it just has `elements`). + // So, filter out any instance of any_raw_array to avoid generating duplicate values for the primitive values that are separate from `elements`. + } else if !func.starts_with("kani::any_raw_array") { + let concrete_val = extract_primitive_value(value); + return concrete_val.map(ConcreteItem::Primitive); } None } @@ -460,7 +527,8 @@ mod tests { use super::concrete_vals_extractor::*; use super::*; use crate::cbmc_output_parser::{ - CheckStatus, Property, PropertyId, SourceLocation, TraceData, TraceItem, TraceValue, + CheckStatus, Property, PropertyId, SourceLocation, TraceArrayValue, TraceData, TraceItem, + TraceValue, }; /// util function for unit tests taht generates the rustfmt args used for formatting specific lines inside specific files. @@ -491,7 +559,7 @@ mod tests { #[test] fn format_zero_concrete_vals() { - let concrete_vals: [ConcreteVal; 0] = []; + let concrete_vals: [PrimitiveConcreteVal; 0] = []; let actual: Vec<_> = format_concrete_vals(&concrete_vals).collect(); let expected: Vec = Vec::new(); assert_eq!(actual, expected); @@ -501,8 +569,11 @@ mod tests { #[test] fn format_two_concrete_vals() { let concrete_vals = [ - ConcreteVal { byte_arr: vec![0, 0], interp_val: "0".to_string() }, - ConcreteVal { byte_arr: vec![0, 0, 0, 0, 0, 0, 0, 0], interp_val: "0l".to_string() }, + PrimitiveConcreteVal { byte_arr: vec![0, 0], interp_val: "0".to_string() }, + PrimitiveConcreteVal { + byte_arr: vec![0, 0, 0, 0, 0, 0, 0, 0], + interp_val: "0l".to_string(), + }, ]; let actual: Vec<_> = format_concrete_vals(&concrete_vals).collect(); let expected = vec![ @@ -535,7 +606,10 @@ mod tests { fn format_unit_test_full_func() { let doc_str = "/// Test documentation"; let harness_name = "test_proof_harness"; - let concrete_vals = [ConcreteVal { byte_arr: vec![0, 0], interp_val: "0".to_string() }]; + let concrete_vals = [ConcreteItem::Primitive(PrimitiveConcreteVal { + byte_arr: vec![0, 0], + interp_val: "0".to_string(), + })]; let unit_test = format_unit_test(harness_name, &concrete_vals, doc_str.to_string()); let full_func = unit_test.code; let split_unit_test_name = split_unit_test_name(&unit_test.name); @@ -559,10 +633,10 @@ mod tests { } /// Generates a unit test and returns its hash. - fn extract_hash_from_unit_test(harness_name: &str, concrete_vals: &[ConcreteVal]) -> String { + fn extract_hash_from_unit_test(harness_name: &str, concrete_items: &[ConcreteItem]) -> String { let unit_test = format_unit_test( harness_name, - concrete_vals, + concrete_items, "/// Harness created for unit test".to_string(), ); split_unit_test_name(&unit_test.name).hash @@ -573,14 +647,41 @@ mod tests { fn check_hashes_are_unique() { let harness_name_1 = "test_proof_harness1"; let harness_name_2 = "test_proof_harness2"; - let concrete_vals_1 = [ConcreteVal { byte_arr: vec![0, 0], interp_val: "0".to_string() }]; - let concrete_vals_2 = [ConcreteVal { byte_arr: vec![1, 0], interp_val: "0".to_string() }]; - let concrete_vals_3 = [ConcreteVal { byte_arr: vec![0, 0], interp_val: "1".to_string() }]; + let concrete_items_1 = [ + ConcreteItem::Primitive(PrimitiveConcreteVal { + byte_arr: vec![0, 0], + interp_val: "0".to_string(), + }), + ConcreteItem::Array(vec![PrimitiveConcreteVal { + byte_arr: vec![0, 0], + interp_val: "0".to_string(), + }]), + ]; + let concrete_items_2 = [ConcreteItem::Primitive(PrimitiveConcreteVal { + byte_arr: vec![1, 0], + interp_val: "0".to_string(), + })]; + let concrete_items_3 = [ + ConcreteItem::Array(vec![PrimitiveConcreteVal { + byte_arr: vec![0, 0], + interp_val: "0".to_string(), + }]), + ConcreteItem::Primitive(PrimitiveConcreteVal { + byte_arr: vec![0, 0], + interp_val: "1".to_string(), + }), + ConcreteItem::Array(vec![ + PrimitiveConcreteVal { byte_arr: vec![0, 0], interp_val: "0".to_string() }, + PrimitiveConcreteVal { byte_arr: vec![1, 0], interp_val: "0".to_string() }, + PrimitiveConcreteVal { byte_arr: vec![1, 0, 255], interp_val: "0".to_string() }, + ]), + ]; - let hash_base = extract_hash_from_unit_test(harness_name_1, &concrete_vals_1); - let hash_diff_harness_name = extract_hash_from_unit_test(harness_name_2, &concrete_vals_1); - let hash_diff_concrete_byte = extract_hash_from_unit_test(harness_name_1, &concrete_vals_2); - let hash_diff_interp_val = extract_hash_from_unit_test(harness_name_1, &concrete_vals_3); + let hash_base = extract_hash_from_unit_test(harness_name_1, &concrete_items_1); + let hash_diff_harness_name = extract_hash_from_unit_test(harness_name_2, &concrete_items_1); + let hash_diff_concrete_byte = + extract_hash_from_unit_test(harness_name_1, &concrete_items_2); + let hash_diff_interp_val = extract_hash_from_unit_test(harness_name_1, &concrete_items_3); assert_ne!(hash_base, hash_diff_harness_name); assert_ne!(hash_base, hash_diff_concrete_byte); @@ -626,7 +727,7 @@ mod tests { /// Test util functions which extract the counter example values from a property. #[test] - fn check_concrete_vals_extractor() { + fn check_concrete_vals_extractor_primitive() { let processed_items = [Property { description: "".to_string(), property_id: PropertyId { @@ -655,13 +756,173 @@ mod tests { binary: Some("0000001100000001".to_string()), data: Some(TraceData::NonBool("385".to_string())), width: Some(16), + elements: None, }), }]), }]; - let (_, concrete_vals) = extract_harness_values(&processed_items).pop().unwrap(); - let concrete_val = &concrete_vals[0]; + let (_, concrete_items) = extract_harness_values(&processed_items).pop().unwrap(); + let concrete_item = &concrete_items[0]; - assert_eq!(concrete_val.byte_arr, vec![1, 3]); - assert_eq!(concrete_val.interp_val, "385"); + assert!(matches!(concrete_item, ConcreteItem::Primitive(_))); + if let ConcreteItem::Primitive(concrete_val) = concrete_item { + assert_eq!(concrete_val.byte_arr, vec![1, 3]); + assert_eq!(concrete_val.interp_val, "385"); + } + } + + /// Test util functions which extract the counter example values from a property for arrays. + #[test] + fn check_concrete_vals_extractor_array() { + let processed_items = [Property { + description: "".to_string(), + property_id: PropertyId { + fn_name: Some("".to_string()), + class: "assertion".to_string(), + id: 1, + }, + status: CheckStatus::Failure, + reach: None, + source_location: SourceLocation { + column: None, + file: None, + function: None, + line: None, + }, + trace: Some(vec![ + TraceItem { + step_type: "assignment".to_string(), + lhs: Some("goto_symex$$return_value".to_string()), + source_location: Some(SourceLocation { + column: None, + file: None, + function: Some("kani::any_raw_array::".to_string()), + line: None, + }), + value: Some(TraceValue { + binary: None, + data: None, + width: None, + elements: Some(vec![ + TraceArrayValue { + value: TraceValue { + binary: Some("11111111111111111111111111111111".to_string()), + data: Some(TraceData::NonBool("4294967295".to_string())), + width: Some(32), + elements: None, + }, + }, + TraceArrayValue { + value: TraceValue { + binary: Some("10000000000000000000000000000000".to_string()), + data: Some(TraceData::NonBool("2147483648".to_string())), + width: Some(32), + elements: None, + }, + }, + TraceArrayValue { + value: TraceValue { + binary: Some("11111111111111111111111111111111".to_string()), + data: Some(TraceData::NonBool("4294967295".to_string())), + width: Some(32), + elements: None, + }, + }, + TraceArrayValue { + value: TraceValue { + binary: Some("00000000000000000000000000000111".to_string()), + data: Some(TraceData::NonBool("7".to_string())), + width: Some(32), + elements: None, + }, + }, + ]), + }), + }, + // Since the array is of size 4, there are also TraceItems for each element of the array, which extract_harness_value should ignore. + TraceItem { + step_type: "assignment".to_string(), + lhs: Some("goto_symex$$return_value".to_string()), + source_location: Some(SourceLocation { + column: None, + file: None, + function: Some("kani::any_raw_array::".to_string()), + line: None, + }), + value: Some(TraceValue { + binary: Some("11111111111111111111111111111111".to_string()), + data: Some(TraceData::NonBool("4294967295".to_string())), + width: Some(32), + elements: None, + }), + }, + TraceItem { + step_type: "assignment".to_string(), + lhs: Some("goto_symex$$return_value".to_string()), + source_location: Some(SourceLocation { + column: None, + file: None, + function: Some("kani::any_raw_array::".to_string()), + line: None, + }), + value: Some(TraceValue { + binary: Some("10000000000000000000000000000000".to_string()), + data: Some(TraceData::NonBool("2147483648".to_string())), + width: Some(32), + elements: None, + }), + }, + TraceItem { + step_type: "assignment".to_string(), + lhs: Some("goto_symex$$return_value".to_string()), + source_location: Some(SourceLocation { + column: None, + file: None, + function: Some("kani::any_raw_array::".to_string()), + line: None, + }), + value: Some(TraceValue { + binary: Some("11111111111111111111111111111111".to_string()), + data: Some(TraceData::NonBool("4294967295".to_string())), + width: Some(32), + elements: None, + }), + }, + TraceItem { + step_type: "assignment".to_string(), + lhs: Some("goto_symex$$return_value".to_string()), + source_location: Some(SourceLocation { + column: None, + file: None, + function: Some("kani::any_raw_array::".to_string()), + line: None, + }), + value: Some(TraceValue { + binary: Some("00000000000000000000000000000111".to_string()), + data: Some(TraceData::NonBool("7".to_string())), + width: Some(32), + elements: None, + }), + }, + ]), + }]; + let (_, concrete_items) = extract_harness_values(&processed_items).pop().unwrap(); + let concrete_item = &concrete_items[0]; + + assert!(matches!(concrete_item, ConcreteItem::Array(_))); + if let ConcreteItem::Array(concrete_vals) = concrete_item { + assert_eq!(concrete_vals.len(), 4); + let first_val = &concrete_vals[0]; + assert_eq!(first_val.byte_arr, vec![255, 255, 255, 255]); + assert_eq!(first_val.interp_val, "4294967295"); + let second_val = &concrete_vals[1]; + assert_eq!(second_val.byte_arr, vec![0, 0, 0, 128]); + assert_eq!(second_val.interp_val, "2147483648"); + let third_val = &concrete_vals[2]; + assert_eq!(third_val.byte_arr, vec![255, 255, 255, 255]); + assert_eq!(third_val.interp_val, "4294967295"); + let fourth_val = &concrete_vals[3]; + assert_eq!(fourth_val.byte_arr, vec![7, 0, 0, 0]); + assert_eq!(fourth_val.interp_val, "7"); + } } } diff --git a/kani-driver/src/coverage/cov_results.rs b/kani-driver/src/coverage/cov_results.rs index 845ae7de21bb..694cb480bc4f 100644 --- a/kani-driver/src/coverage/cov_results.rs +++ b/kani-driver/src/coverage/cov_results.rs @@ -64,7 +64,6 @@ impl CoverageCheck { #[derive(Debug, Clone, Serialize, Deserialize)] pub enum CoverageTerm { Counter(u32), - Expression(u32), } #[derive(Debug, Clone, Eq, PartialEq, PartialOrd, Ord, Serialize, Deserialize)] diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index b78e1dc9d80b..56e3f4c09ed2 100644 --- a/kani-driver/src/harness_runner.rs +++ b/kani-driver/src/harness_runner.rs @@ -1,8 +1,8 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -use anyhow::{Result, bail}; -use kani_metadata::{ArtifactType, HarnessMetadata}; +use anyhow::{Error, Result, bail}; +use kani_metadata::{ArtifactType, HarnessKind, HarnessMetadata}; use rayon::prelude::*; use std::fs::File; use std::io::Write; @@ -11,7 +11,7 @@ use std::path::Path; use crate::args::OutputFormat; use crate::call_cbmc::{VerificationResult, VerificationStatus}; use crate::project::Project; -use crate::session::KaniSession; +use crate::session::{BUG_REPORT_URL, KaniSession}; use std::env::current_dir; use std::path::PathBuf; @@ -34,6 +34,20 @@ pub(crate) struct HarnessResult<'pr> { pub result: VerificationResult, } +#[derive(Debug)] +struct FailFastHarnessInfo { + pub index_to_failing_harness: usize, + pub result: VerificationResult, +} + +impl std::error::Error for FailFastHarnessInfo {} + +impl std::fmt::Display for FailFastHarnessInfo { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + write!(f, "harness failed") + } +} + impl<'pr> HarnessRunner<'_, 'pr> { /// Given a [`HarnessRunner`] (to abstract over how these harnesses were generated), this runs /// the proof-checking process for each harness in `harnesses`. @@ -55,7 +69,8 @@ impl<'pr> HarnessRunner<'_, 'pr> { let results = pool.install(|| -> Result>> { sorted_harnesses .par_iter() - .map(|harness| -> Result> { + .enumerate() + .map(|(idx, harness)| -> Result> { let goto_file = self.project.get_harness_artifact(&harness, ArtifactType::Goto).unwrap(); @@ -66,12 +81,31 @@ impl<'pr> HarnessRunner<'_, 'pr> { } let result = self.sess.check_harness(goto_file, harness)?; - Ok(HarnessResult { harness, result }) + if self.sess.args.fail_fast && result.status == VerificationStatus::Failure { + Err(Error::new(FailFastHarnessInfo { + index_to_failing_harness: idx, + result, + })) + } else { + Ok(HarnessResult { harness, result }) + } }) .collect::>>() - })?; - - Ok(results) + }); + match results { + Ok(results) => Ok(results), + Err(err) => { + if err.is::() { + let failed = err.downcast::().unwrap(); + Ok(vec![HarnessResult { + harness: sorted_harnesses[failed.index_to_failing_harness], + result: failed.result, + }]) + } else { + Err(err) + } + } + } } /// Return an error if the user is trying to verify a harness with stubs without enabling the @@ -168,11 +202,28 @@ impl KaniSession { ) -> Result { let thread_index = rayon::current_thread_index().unwrap_or_default(); if !self.args.common_args.quiet { - if rayon::current_num_threads() > 1 { - println!("Thread {thread_index}: Checking harness {}...", harness.pretty_name); + // If the harness is automatically generated, pretty_name refers to the function under verification. + let mut msg = if harness.is_automatically_generated { + if matches!(harness.attributes.kind, HarnessKind::Proof) { + format!( + "Autoharness: Checking function {} against all possible inputs...", + harness.pretty_name + ) + } else { + format!( + "Autoharness: Checking function {}'s contract against all possible inputs...", + harness.pretty_name + ) + } } else { - println!("Checking harness {}...", harness.pretty_name); + format!("Checking harness {}...", harness.pretty_name) + }; + + if rayon::current_num_threads() > 1 { + msg = format!("Thread {thread_index}: {msg}"); } + + println!("{msg}"); } let mut result = self.with_timer(|| self.run_cbmc(binary, harness), "run_cbmc")?; @@ -188,54 +239,65 @@ impl KaniSession { /// Note: Takes `self` "by ownership". This function wants to be able to drop before /// exiting with an error code, if needed. pub(crate) fn print_final_summary(self, results: &[HarnessResult<'_>]) -> Result<()> { + if self.args.common_args.quiet { + return Ok(()); + } + + let (automatic, manual): (Vec<_>, Vec<_>) = + results.iter().partition(|r| r.harness.is_automatically_generated); + + if self.auto_harness { + self.print_autoharness_summary(automatic)?; + } + let (successes, failures): (Vec<_>, Vec<_>) = - results.iter().partition(|r| r.result.status == VerificationStatus::Success); + manual.into_iter().partition(|r| r.result.status == VerificationStatus::Success); let succeeding = successes.len(); let failing = failures.len(); let total = succeeding + failing; - if self.args.concrete_playback.is_some() - && !self.args.common_args.quiet - && results.iter().all(|r| !r.result.generated_concrete_test) - { - println!( - "INFO: The concrete playback feature never generated unit tests because there were no failing harnesses." - ) + if self.args.concrete_playback.is_some() { + if failures.is_empty() { + println!( + "INFO: The concrete playback feature never generated unit tests because there were no failing harnesses." + ) + } else if failures.iter().all(|r| !r.result.generated_concrete_test) { + eprintln!( + "The concrete playback feature did not generate unit tests, but there were failing harnesses. Please file a bug report at {BUG_REPORT_URL}" + ) + } } // We currently omit a summary if there was just 1 harness - if !self.args.common_args.quiet { - if failing > 0 { - println!("Summary:"); - } - for failure in failures.iter() { - println!("Verification failed for - {}", failure.harness.pretty_name); - } + if failing > 0 { + println!("Manual Harness Summary:"); + } + for failure in failures.iter() { + println!("Verification failed for - {}", failure.harness.pretty_name); + } - if total > 0 { - println!( - "Complete - {succeeding} successfully verified harnesses, {failing} failures, {total} total." - ); - } else { - match self.args.harnesses.as_slice() { - [] => - // TODO: This could use a better message, possibly with links to Kani documentation. - // New users may encounter this and could use a pointer to how to write proof harnesses. - { - println!( - "No proof harnesses (functions with #[kani::proof]) were found to verify." - ) - } - [harness] => { - bail!("no harnesses matched the harness filter: `{harness}`") - } - harnesses => bail!( - "no harnesses matched the harness filters: `{}`", - harnesses.join("`, `") - ), - }; - } + if total > 0 { + println!( + "Complete - {succeeding} successfully verified harnesses, {failing} failures, {total} total." + ); + } else { + match self.args.harnesses.as_slice() { + [] => + // TODO: This could use a better message, possibly with links to Kani documentation. + // New users may encounter this and could use a pointer to how to write proof harnesses. + { + println!( + "No proof harnesses (functions with #[kani::proof]) were found to verify." + ) + } + [harness] => { + bail!("no harnesses matched the harness filter: `{harness}`") + } + harnesses => { + bail!("no harnesses matched the harness filters: `{}`", harnesses.join("`, `")) + } + }; } if self.args.coverage { diff --git a/kani-driver/src/list/collect_metadata.rs b/kani-driver/src/list/collect_metadata.rs index a7901e997ab1..588cab0b63af 100644 --- a/kani-driver/src/list/collect_metadata.rs +++ b/kani-driver/src/list/collect_metadata.rs @@ -78,12 +78,12 @@ fn process_metadata(metadata: Vec) -> ListMetadata { pub fn list_cargo(args: CargoListArgs, mut verify_opts: VerificationArgs) -> Result<()> { let quiet = args.common_args.quiet; verify_opts.common_args = args.common_args; - let session = KaniSession::new(verify_opts)?; + let mut session = KaniSession::new(verify_opts)?; if !quiet { print_kani_version(InvocationType::CargoKani(vec![])); } - let project = cargo_project(&session, false)?; + let project = cargo_project(&mut session, false)?; let list_metadata = process_metadata(project.metadata); output_list_results(list_metadata, args.format, quiet) diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index 07405a30a307..9b82c8467e26 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -22,6 +22,7 @@ use tracing::debug; mod args; mod args_toml; mod assess; +mod autoharness; mod call_cargo; mod call_cbmc; mod call_goto_cc; @@ -72,28 +73,37 @@ fn cargokani_main(input_args: Vec) -> Result<()> { return list_cargo(*list_args, args.verify_opts); } - let session = session::KaniSession::new(args.verify_opts)?; - - if !session.args.common_args.quiet { - print_kani_version(InvocationType::CargoKani(input_args)); - } - - match args.command { - Some(CargoKaniSubcommand::Assess(args)) => { - return assess::run_assess(session, *args); + let mut session = match args.command { + Some(CargoKaniSubcommand::Assess(assess_args)) => { + let sess = session::KaniSession::new(args.verify_opts)?; + return assess::run_assess(sess, *assess_args); + } + Some(CargoKaniSubcommand::Autoharness(args)) => { + let mut sess = session::KaniSession::new(args.verify_opts)?; + sess.enable_autoharness(); + sess.add_auto_harness_args( + args.common_autoharness_args.include_function, + args.common_autoharness_args.exclude_function, + ); + + sess } Some(CargoKaniSubcommand::Playback(args)) => { return playback_cargo(*args); } Some(CargoKaniSubcommand::List(_)) => unreachable!(), - None => {} + None => session::KaniSession::new(args.verify_opts)?, + }; + + if !session.args.common_args.quiet { + print_kani_version(InvocationType::CargoKani(input_args)); } if session.args.assess { return assess::run_assess(session, assess::AssessArgs::default()); } - let project = project::cargo_project(&session, false)?; + let project = project::cargo_project(&mut session, false)?; if session.args.only_codegen { Ok(()) } else { verify_project(project, session) } } @@ -103,6 +113,21 @@ fn standalone_main() -> Result<()> { check_is_valid(&args); let (session, project) = match args.command { + Some(StandaloneSubcommand::Autoharness(args)) => { + let mut session = KaniSession::new(args.verify_opts)?; + session.enable_autoharness(); + session.add_auto_harness_args( + args.common_autoharness_args.include_function, + args.common_autoharness_args.exclude_function, + ); + + if !session.args.common_args.quiet { + print_kani_version(InvocationType::Standalone); + } + + let project = project::standalone_project(&args.input, args.crate_name, &session)?; + (session, project) + } Some(StandaloneSubcommand::Playback(args)) => return playback_standalone(*args), Some(StandaloneSubcommand::List(list_args)) => { return list_standalone(*list_args, args.verify_opts); diff --git a/kani-driver/src/metadata.rs b/kani-driver/src/metadata.rs index 94a5393408d3..d112591c6532 100644 --- a/kani-driver/src/metadata.rs +++ b/kani-driver/src/metadata.rs @@ -176,6 +176,10 @@ fn find_proof_harnesses<'a>( debug!(?targets, "find_proof_harness"); let mut result = vec![]; for md in all_harnesses.iter() { + // --harnesses should not select automatic harnesses + if md.is_automatically_generated { + continue; + } if exact_filter { // Check for exact match only if targets.contains(&md.pretty_name) { @@ -224,6 +228,7 @@ pub mod tests { goto_file: model_file, contract: Default::default(), has_loop_contracts: false, + is_automatically_generated: false, } } diff --git a/kani-driver/src/project.rs b/kani-driver/src/project.rs index da04cc0517ba..2a1aad2c1eff 100644 --- a/kani-driver/src/project.rs +++ b/kani-driver/src/project.rs @@ -175,7 +175,7 @@ impl Artifact { /// Generate a project using `cargo`. /// Accept a boolean to build as many targets as possible. The number of failures in that case can /// be collected from the project. -pub fn cargo_project(session: &KaniSession, keep_going: bool) -> Result { +pub fn cargo_project(session: &mut KaniSession, keep_going: bool) -> Result { let outputs = session.cargo_build(keep_going)?; let outdir = outputs.outdir.canonicalize()?; // For the MIR Linker we know there is only one metadata per crate. Use that in our favor. diff --git a/kani-driver/src/session.rs b/kani-driver/src/session.rs index 187a17ae6981..6645db06e45e 100644 --- a/kani-driver/src/session.rs +++ b/kani-driver/src/session.rs @@ -17,6 +17,9 @@ use tokio::process::Command as TokioCommand; use tracing::level_filters::LevelFilter; use tracing_subscriber::{EnvFilter, Registry, layer::SubscriberExt}; +pub const BUG_REPORT_URL: &str = + "https://github.com/model-checking/kani/issues/new?labels=bug&template=bug_report.md"; + /// 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 /// the driver logs separately, by using the logger directives to select the kani-driver crate. @@ -28,6 +31,12 @@ pub struct KaniSession { /// The common command-line arguments pub args: VerificationArgs, + /// Automatically verify functions in the crate, in addition to running manual harnesses. + pub auto_harness: bool, + + /// The arguments that will be passed to the target package, i.e. kani_compiler. + pub pkg_args: Vec, + /// Include all publicly-visible symbols in the generated goto binary, not just those reachable from /// a proof harness. Useful when attempting to verify things that were not annotated with kani /// proof attributes. @@ -62,6 +71,8 @@ impl KaniSession { Ok(KaniSession { args, + auto_harness: false, + pkg_args: vec!["--".to_string()], codegen_tests: false, kani_compiler: install.kani_compiler()?, kani_lib_c: install.kani_lib_c()?, @@ -88,13 +99,20 @@ impl KaniSession { /// Determine which symbols Kani should codegen (i.e. by slicing away symbols /// that are considered unreachable.) pub fn reachability_mode(&self) -> ReachabilityMode { - if self.codegen_tests { ReachabilityMode::Tests } else { ReachabilityMode::ProofHarnesses } + if self.codegen_tests { + ReachabilityMode::Tests + } else if self.auto_harness { + ReachabilityMode::AllFns + } else { + ReachabilityMode::ProofHarnesses + } } } #[derive(Debug, Copy, Clone, Display)] #[strum(serialize_all = "snake_case")] pub enum ReachabilityMode { + AllFns, #[strum(to_string = "harnesses")] ProofHarnesses, Tests, diff --git a/kani_metadata/Cargo.toml b/kani_metadata/Cargo.toml index 35239b0242e6..b4db86ebed1e 100644 --- a/kani_metadata/Cargo.toml +++ b/kani_metadata/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_metadata" -version = "0.58.0" +version = "0.59.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/kani_metadata/src/harness.rs b/kani_metadata/src/harness.rs index 6932b15dc1a7..227fe8df09d4 100644 --- a/kani_metadata/src/harness.rs +++ b/kani_metadata/src/harness.rs @@ -38,6 +38,8 @@ pub struct HarnessMetadata { pub contract: Option, /// If the harness contains some usage of loop contracts. pub has_loop_contracts: bool, + /// If the harness was automatically generated or manually written. + pub is_automatically_generated: bool, } /// The attributes added by the user to control how a harness is executed. diff --git a/library/kani/Cargo.toml b/library/kani/Cargo.toml index ca039ebdaa39..d559be65a88f 100644 --- a/library/kani/Cargo.toml +++ b/library/kani/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani" -version = "0.58.0" +version = "0.59.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/kani/src/models/mod.rs b/library/kani/src/models/mod.rs index af5ac336e09e..3329b1d4b895 100644 --- a/library/kani/src/models/mod.rs +++ b/library/kani/src/models/mod.rs @@ -65,7 +65,7 @@ mod intrinsics { /// Logic similar to `bitmask_len` from `portable_simd`. /// pub(super) const fn mask_len(len: usize) -> usize { - (len + 7) / 8 + len.div_ceil(8) } #[cfg(target_endian = "little")] diff --git a/library/kani_core/Cargo.toml b/library/kani_core/Cargo.toml index 89d57047a77c..b474e15d7d0c 100644 --- a/library/kani_core/Cargo.toml +++ b/library/kani_core/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_core" -version = "0.58.0" +version = "0.59.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/kani_core/src/float.rs b/library/kani_core/src/float.rs index 44475af80a51..55fe71dbf24d 100644 --- a/library/kani_core/src/float.rs +++ b/library/kani_core/src/float.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -//! This module contains functions useful for float-related checks +// This module contains functions useful for float-related checks. #[allow(clippy::crate_in_macro_def)] #[macro_export] diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index 3ba2f459470e..51b243c9ad33 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -67,14 +67,64 @@ macro_rules! kani_lib { kani_core::generate_models!(); pub mod float { + //! This module contains functions useful for float-related checks kani_core::generate_float!(std); } pub mod mem { + //! This module contains functions useful for checking unsafe memory access. + //! + //! Given the following validity rules provided in the Rust documentation: + //! (accessed Feb 6th, 2024) + //! + //! 1. A null pointer is never valid, not even for accesses of size zero. + //! 2. For a pointer to be valid, it is necessary, but not always sufficient, that the pointer + //! be dereferenceable: the memory range of the given size starting at the pointer must all be + //! within the bounds of a single allocated object. Note that in Rust, every (stack-allocated) + //! variable is considered a separate allocated object. + //! ~~Even for operations of size zero, the pointer must not be pointing to deallocated memory, + //! i.e., deallocation makes pointers invalid even for zero-sized operations.~~ + //! ZST access is not OK for any pointer. + //! See: + //! 3. However, casting any non-zero integer literal to a pointer is valid for zero-sized + //! accesses, even if some memory happens to exist at that address and gets deallocated. + //! This corresponds to writing your own allocator: allocating zero-sized objects is not very + //! hard. The canonical way to obtain a pointer that is valid for zero-sized accesses is + //! `NonNull::dangling`. + //! 4. All accesses performed by functions in this module are non-atomic in the sense of atomic + //! operations used to synchronize between threads. + //! This means it is undefined behavior to perform two concurrent accesses to the same location + //! from different threads unless both accesses only read from memory. + //! Notice that this explicitly includes `read_volatile` and `write_volatile`: + //! Volatile accesses cannot be used for inter-thread synchronization. + //! 5. The result of casting a reference to a pointer is valid for as long as the underlying + //! object is live and no reference (just raw pointers) is used to access the same memory. + //! That is, reference and pointer accesses cannot be interleaved. + //! + //! Kani is able to verify #1 and #2 today. + //! + //! For #3, we are overly cautious, and Kani will only consider zero-sized pointer access safe if + //! the address matches `NonNull::<()>::dangling()`. + //! The way Kani tracks provenance is not enough to check if the address was the result of a cast + //! from a non-zero integer literal. + //! kani_core::kani_mem!(std); } mod mem_init { + //! This module provides instrumentation for tracking memory initialization of raw pointers. + //! + //! Currently, memory initialization is tracked on per-byte basis, so each byte of memory pointed to + //! by raw pointers could be either initialized or uninitialized. Padding bytes are always + //! considered uninitialized when read as data bytes. Each type has a type layout to specify which + //! bytes are considered to be data and which -- padding. This is determined at compile time and + //! statically injected into the program (see `Layout`). + //! + //! Compiler automatically inserts calls to `is_xxx_initialized` and `set_xxx_initialized` at + //! appropriate locations to get or set the initialization status of the memory pointed to. + //! + //! Note that for each harness, tracked object and tracked offset are chosen non-deterministically, + //! so calls to `is_xxx_initialized` should be only used in assertion contexts. kani_core::kani_mem_init!(std); } }; @@ -308,6 +358,18 @@ macro_rules! kani_intrinsics { assert!(cond, "Safety check failed: {msg}"); } + #[doc(hidden)] + #[allow(dead_code)] + #[kanitool::fn_marker = "SafetyCheckNoAssumeHook"] + #[inline(never)] + pub(crate) fn safety_check_no_assume(cond: bool, msg: &'static str) { + #[cfg(not(feature = "concrete_playback"))] + return kani_intrinsic(); + + #[cfg(feature = "concrete_playback")] + assert!(cond, "Safety check failed: {msg}"); + } + /// This should indicate that Kani does not support a certain operation. #[doc(hidden)] #[allow(dead_code)] @@ -384,6 +446,12 @@ macro_rules! kani_intrinsics { } } + /// Used to hold the bodies of automatically generated harnesses. + #[kanitool::fn_marker = "AutomaticHarnessIntrinsic"] + pub fn automatic_harness() { + super::kani_intrinsic() + } + /// A way to break the ownerhip rules. Only used by contracts where we can /// guarantee it is done safely. #[inline(never)] diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs index c09d67ca51ff..1ab8a5ead993 100644 --- a/library/kani_core/src/mem.rs +++ b/library/kani_core/src/mem.rs @@ -1,41 +1,9 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -//! This module contains functions useful for checking unsafe memory access. -//! -//! Given the following validity rules provided in the Rust documentation: -//! (accessed Feb 6th, 2024) -//! -//! 1. A null pointer is never valid, not even for accesses of size zero. -//! 2. For a pointer to be valid, it is necessary, but not always sufficient, that the pointer -//! be dereferenceable: the memory range of the given size starting at the pointer must all be -//! within the bounds of a single allocated object. Note that in Rust, every (stack-allocated) -//! variable is considered a separate allocated object. -//! ~~Even for operations of size zero, the pointer must not be pointing to deallocated memory, -//! i.e., deallocation makes pointers invalid even for zero-sized operations.~~ -//! ZST access is not OK for any pointer. -//! See: -//! 3. However, casting any non-zero integer literal to a pointer is valid for zero-sized -//! accesses, even if some memory happens to exist at that address and gets deallocated. -//! This corresponds to writing your own allocator: allocating zero-sized objects is not very -//! hard. The canonical way to obtain a pointer that is valid for zero-sized accesses is -//! `NonNull::dangling`. -//! 4. All accesses performed by functions in this module are non-atomic in the sense of atomic -//! operations used to synchronize between threads. -//! This means it is undefined behavior to perform two concurrent accesses to the same location -//! from different threads unless both accesses only read from memory. -//! Notice that this explicitly includes `read_volatile` and `write_volatile`: -//! Volatile accesses cannot be used for inter-thread synchronization. -//! 5. The result of casting a reference to a pointer is valid for as long as the underlying -//! object is live and no reference (just raw pointers) is used to access the same memory. -//! That is, reference and pointer accesses cannot be interleaved. -//! -//! Kani is able to verify #1 and #2 today. -//! -//! For #3, we are overly cautious, and Kani will only consider zero-sized pointer access safe if -//! the address matches `NonNull::<()>::dangling()`. -//! The way Kani tracks provenance is not enough to check if the address was the result of a cast -//! from a non-zero integer literal. -//! + +// This module contains functions useful for checking unsafe memory access. +// For full documentation, see the usage of `kani_core::kani_mem!(std);` in library/kani_core/src/lib.rs + // TODO: This module is currently tightly coupled with CBMC's memory model, and it needs some // refactoring to be used with other backends. @@ -210,10 +178,11 @@ macro_rules! kani_mem { // stubbed. // We first assert that the data_ptr let data_ptr = ptr as *const (); - super::assert( - unsafe { is_allocated(data_ptr, 0) }, - "Kani does not support reasoning about pointer to unallocated memory", - ); + if !unsafe { is_allocated(data_ptr, 0) } { + crate::kani::unsupported( + "Kani does not support reasoning about pointer to unallocated memory", + ); + } unsafe { is_allocated(data_ptr, sz) } } } @@ -280,11 +249,11 @@ macro_rules! kani_mem { pub fn same_allocation(addr1: *const (), addr2: *const ()) -> bool { let obj1 = crate::kani::mem::pointer_object(addr1); (obj1 == crate::kani::mem::pointer_object(addr2)) && { - // TODO(3571): This should be a unsupported check - crate::kani::assert( - unsafe { is_allocated(addr1, 0) || is_allocated(addr2, 0) }, - "Kani does not support reasoning about pointer to unallocated memory", - ); + if !unsafe { is_allocated(addr1, 0) || is_allocated(addr2, 0) } { + crate::kani::unsupported( + "Kani does not support reasoning about pointer to unallocated memory", + ); + } unsafe { is_allocated(addr1, 0) && is_allocated(addr2, 0) } } } diff --git a/library/kani_core/src/mem_init.rs b/library/kani_core/src/mem_init.rs index 935f14d71c5d..3fafcb1d8388 100644 --- a/library/kani_core/src/mem_init.rs +++ b/library/kani_core/src/mem_init.rs @@ -1,19 +1,8 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -//! This module provides instrumentation for tracking memory initialization of raw pointers. -//! -//! Currently, memory initialization is tracked on per-byte basis, so each byte of memory pointed to -//! by raw pointers could be either initialized or uninitialized. Padding bytes are always -//! considered uninitialized when read as data bytes. Each type has a type layout to specify which -//! bytes are considered to be data and which -- padding. This is determined at compile time and -//! statically injected into the program (see `Layout`). -//! -//! Compiler automatically inserts calls to `is_xxx_initialized` and `set_xxx_initialized` at -//! appropriate locations to get or set the initialization status of the memory pointed to. -//! -//! Note that for each harness, tracked object and tracked offset are chosen non-deterministically, -//! so calls to `is_xxx_initialized` should be only used in assertion contexts. +// This module provides instrumentation for tracking memory initialization of raw pointers. +// For full documentation, see the usage of `kani_core::kani_mem_init!(std);` in library/kani_core/src/lib.rs // Definitions in this module are not meant to be visible to the end user, only the compiler. #![allow(dead_code)] diff --git a/library/kani_core/src/models.rs b/library/kani_core/src/models.rs index f95e1acc4899..8913c399c959 100644 --- a/library/kani_core/src/models.rs +++ b/library/kani_core/src/models.rs @@ -99,29 +99,35 @@ macro_rules! generate_models { /// An offset model that checks UB. #[kanitool::fn_marker = "OffsetModel"] pub fn offset, O: ToISize>(ptr: P, offset: O) -> P { - let offset = offset.to_isize(); let t_size = core::mem::size_of::() as isize; - if offset == 0 || t_size == 0 { + if t_size == 0 { + // It's always safe to perform an offset on a ZST. + return ptr; + } + + // Note that this check must come after the t_size check, c.f. https://github.com/model-checking/kani/issues/3896 + let offset = offset.to_isize(); + if offset == 0 { // It's always safe to perform an offset of length 0. - ptr - } else { - let (byte_offset, overflow) = offset.overflowing_mul(t_size); - kani::safety_check(!overflow, "Offset in bytes overflows isize"); - let orig_ptr = ptr.to_const_ptr(); - // NOTE: For CBMC, using the pointer addition can have unexpected behavior - // when the offset is higher than the object bits since it will wrap around. - // See for more details: https://github.com/model-checking/kani/issues/1150 - // - // However, when I tried implementing this using usize operation, we got some - // unexpected failures that still require further debugging. - // let new_ptr = orig_ptr.addr().wrapping_add_signed(byte_offset) as *const T; - let new_ptr = orig_ptr.wrapping_byte_offset(byte_offset); - kani::safety_check( - kani::mem::same_allocation_internal(orig_ptr, new_ptr), - "Offset result and original pointer must point to the same allocation", - ); - P::from_const_ptr(new_ptr) + return ptr; } + + let (byte_offset, overflow) = offset.overflowing_mul(t_size); + kani::safety_check(!overflow, "Offset in bytes overflows isize"); + let orig_ptr = ptr.to_const_ptr(); + // NOTE: For CBMC, using the pointer addition can have unexpected behavior + // when the offset is higher than the object bits since it will wrap around. + // See for more details: https://github.com/model-checking/kani/issues/1150 + // + // However, when I tried implementing this using usize operation, we got some + // unexpected failures that still require further debugging. + // let new_ptr = orig_ptr.addr().wrapping_add_signed(byte_offset) as *const T; + let new_ptr = orig_ptr.wrapping_byte_offset(byte_offset); + kani::safety_check( + kani::mem::same_allocation_internal(orig_ptr, new_ptr), + "Offset result and original pointer must point to the same allocation", + ); + P::from_const_ptr(new_ptr) } pub trait Ptr { diff --git a/library/kani_macros/Cargo.toml b/library/kani_macros/Cargo.toml index 5d8ef49541cc..85e3ee2ed48c 100644 --- a/library/kani_macros/Cargo.toml +++ b/library/kani_macros/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_macros" -version = "0.58.0" +version = "0.59.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/std/Cargo.toml b/library/std/Cargo.toml index ec29489d9aec..223310d52726 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.58.0" +version = "0.59.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 345c2254017b..4e330c132444 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "1.85.1" +channel = "1.86.0" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] diff --git a/src/os_hacks.rs b/src/os_hacks.rs index 8d3a20575d7d..0a149a005934 100644 --- a/src/os_hacks.rs +++ b/src/os_hacks.rs @@ -81,8 +81,7 @@ fn setup_nixos_patchelf(kani_dir: &Path) -> Result<()> { for filename in &["kani-compiler", "kani-driver"] { patch_interp(&bin.join(filename))?; } - for filename in &["cbmc", "goto-analyzer", "goto-cc", "goto-instrument", "kissat", "symtab2gb"] - { + for filename in &["cbmc", "goto-analyzer", "goto-cc", "goto-instrument", "kissat"] { let file = bin.join(filename); patch_interp(&file)?; patch_rpath(&file)?; diff --git a/tests/expected/MemPredicates/adt_with_metadata.expected b/tests/expected/MemPredicates/adt_with_metadata.expected new file mode 100644 index 000000000000..b3d971a40e61 --- /dev/null +++ b/tests/expected/MemPredicates/adt_with_metadata.expected @@ -0,0 +1,4 @@ +Failed Checks: Kani does not support reasoning about pointer to unallocated memory + +Verification failed for - invalid_access::check_invalid_dyn_ptr +Complete - 3 successfully verified harnesses, 1 failures, 4 total. diff --git a/tests/kani/MemPredicates/adt_with_metadata.rs b/tests/expected/MemPredicates/adt_with_metadata.rs similarity index 98% rename from tests/kani/MemPredicates/adt_with_metadata.rs rename to tests/expected/MemPredicates/adt_with_metadata.rs index aa536b26279f..9ec0a3787964 100644 --- a/tests/kani/MemPredicates/adt_with_metadata.rs +++ b/tests/expected/MemPredicates/adt_with_metadata.rs @@ -42,7 +42,6 @@ mod invalid_access { use super::*; use std::ptr; #[kani::proof] - #[kani::should_panic] pub fn check_invalid_dyn_ptr() { unsafe fn new_dead_ptr(val: T) -> *const T { let local = val; diff --git a/tests/expected/MemPredicates/fat_ptr_validity.expected b/tests/expected/MemPredicates/fat_ptr_validity.expected new file mode 100644 index 000000000000..b57ca4986e60 --- /dev/null +++ b/tests/expected/MemPredicates/fat_ptr_validity.expected @@ -0,0 +1,5 @@ +Failed Checks: Kani does not support reasoning about pointer to unallocated memory + +Verification failed for - invalid_access::check_invalid_slice_ptr +Verification failed for - invalid_access::check_invalid_dyn_ptr +Complete - 4 successfully verified harnesses, 2 failures, 6 total. diff --git a/tests/kani/MemPredicates/fat_ptr_validity.rs b/tests/expected/MemPredicates/fat_ptr_validity.rs similarity index 97% rename from tests/kani/MemPredicates/fat_ptr_validity.rs rename to tests/expected/MemPredicates/fat_ptr_validity.rs index c4f037f3a646..f39392b62c5c 100644 --- a/tests/kani/MemPredicates/fat_ptr_validity.rs +++ b/tests/expected/MemPredicates/fat_ptr_validity.rs @@ -38,14 +38,12 @@ mod valid_access { mod invalid_access { use super::*; #[kani::proof] - #[kani::should_panic] pub fn check_invalid_dyn_ptr() { let raw_ptr: *const dyn PartialEq = unsafe { new_dead_ptr::(0) }; assert!(can_dereference(raw_ptr)); } #[kani::proof] - #[kani::should_panic] pub fn check_invalid_slice_ptr() { let raw_ptr: *const [char] = unsafe { new_dead_ptr::<[char; 2]>(['a', 'b']) }; assert!(can_dereference(raw_ptr)); diff --git a/tests/expected/MemPredicates/thin_ptr_validity.expected b/tests/expected/MemPredicates/thin_ptr_validity.expected new file mode 100644 index 000000000000..54245a84a491 --- /dev/null +++ b/tests/expected/MemPredicates/thin_ptr_validity.expected @@ -0,0 +1,5 @@ +Failed Checks: Kani does not support reasoning about pointer to unallocated memory + +Verification failed for - invalid_access::check_invalid_array +Verification failed for - invalid_access::check_invalid_ptr +Complete - 3 successfully verified harnesses, 2 failures, 5 total. diff --git a/tests/kani/MemPredicates/thin_ptr_validity.rs b/tests/expected/MemPredicates/thin_ptr_validity.rs similarity index 96% rename from tests/kani/MemPredicates/thin_ptr_validity.rs rename to tests/expected/MemPredicates/thin_ptr_validity.rs index 553c5beab9f8..519a07297192 100644 --- a/tests/kani/MemPredicates/thin_ptr_validity.rs +++ b/tests/expected/MemPredicates/thin_ptr_validity.rs @@ -32,14 +32,12 @@ mod valid_access { mod invalid_access { use super::*; #[kani::proof] - #[kani::should_panic] pub fn check_invalid_ptr() { let raw_ptr = unsafe { new_dead_ptr::(0) }; assert!(!can_dereference(raw_ptr)); } #[kani::proof] - #[kani::should_panic] pub fn check_invalid_array() { let raw_ptr = unsafe { new_dead_ptr::<[char; 2]>(['a', 'b']) }; assert!(can_dereference(raw_ptr)); diff --git a/tests/expected/function-contract/missing_contract_for_replace.expected b/tests/expected/function-contract/missing_contract_for_replace.expected index 29f3fa955307..198838feca03 100644 --- a/tests/expected/function-contract/missing_contract_for_replace.expected +++ b/tests/expected/function-contract/missing_contract_for_replace.expected @@ -1,4 +1,4 @@ -error: Failed to generate verified stub: Function `harness` has no contract. +error: Target function in `stub_verified(no_contract)` has no contract. | 8 | #[kani::stub_verified(no_contract)] | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/tests/expected/function-contract/multiple_replace_fail.expected b/tests/expected/function-contract/multiple_replace_fail.expected new file mode 100644 index 000000000000..5e828259fcb6 --- /dev/null +++ b/tests/expected/function-contract/multiple_replace_fail.expected @@ -0,0 +1 @@ +warning: Multiple occurrences of `stub_verified(one)`. diff --git a/tests/expected/function-contract/multiple_replace_fail.rs b/tests/expected/function-contract/multiple_replace_fail.rs new file mode 100644 index 000000000000..ecd3c099b2ab --- /dev/null +++ b/tests/expected/function-contract/multiple_replace_fail.rs @@ -0,0 +1,31 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#[kani::ensures(|result : &u32| *result == 1)] +fn one() -> u32 { + 1 +} + +#[kani::proof_for_contract(one)] +fn check_one() { + let _ = one(); +} + +#[kani::ensures(|result : &u32| *result == 1)] +fn one_too() -> u32 { + 1 +} + +#[kani::proof_for_contract(one_too)] +fn check_one_too() { + let _ = one_too(); +} + +#[kani::proof] +#[kani::stub_verified(one)] +#[kani::stub_verified(one)] +#[kani::stub_verified(one_too)] +fn main() { + assert_eq!(one(), one_too()); +} diff --git a/tests/expected/function-contract/multiple_replace_pass.expected b/tests/expected/function-contract/multiple_replace_pass.expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/expected/function-contract/multiple_replace_pass.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/multiple_replace_pass.rs b/tests/expected/function-contract/multiple_replace_pass.rs new file mode 100644 index 000000000000..bd3cb81e136a --- /dev/null +++ b/tests/expected/function-contract/multiple_replace_pass.rs @@ -0,0 +1,30 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#[kani::ensures(|result : &u32| *result == 1)] +fn one() -> u32 { + 1 +} + +#[kani::proof_for_contract(one)] +fn check_one() { + let _ = one(); +} + +#[kani::ensures(|result : &u32| *result == 1)] +fn one_too() -> u32 { + 1 +} + +#[kani::proof_for_contract(one_too)] +fn check_one_too() { + let _ = one_too(); +} + +#[kani::proof] +#[kani::stub_verified(one)] +#[kani::stub_verified(one_too)] +fn main() { + assert_eq!(one(), one_too()); +} diff --git a/tests/expected/intrinsics/transmute_diff_size.expected b/tests/expected/intrinsics/transmute_diff_size.expected new file mode 100644 index 000000000000..efc770882422 --- /dev/null +++ b/tests/expected/intrinsics/transmute_diff_size.expected @@ -0,0 +1,2 @@ +error[E0512]: cannot transmute between types of different sizes, or dependently-sized types +error: aborting due to 3 previous errors diff --git a/tests/expected/intrinsics/transmute_diff_size.rs b/tests/expected/intrinsics/transmute_diff_size.rs new file mode 100644 index 000000000000..a38c37a379d9 --- /dev/null +++ b/tests/expected/intrinsics/transmute_diff_size.rs @@ -0,0 +1,33 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Checks that compilation fails when trying to transmute with different src and target sizes. + +#![feature(core_intrinsics)] +use std::intrinsics::transmute; + +/// This should fail due to UB detection. +#[kani::proof] +pub fn transmute_diff_size() { + let a: u32 = kani::any(); + if kani::any() { + let smaller: u16 = unsafe { transmute(a) }; + std::hint::black_box(smaller); + } else { + let bigger: (u64, isize) = unsafe { transmute(a) }; + std::hint::black_box(bigger); + } +} + +/// Generic transmute wrapper. +pub unsafe fn generic_transmute(src: S) -> D { + transmute(src) +} + +/// This should also fail due to UB detection. +#[kani::proof] +pub fn transmute_wrapper_diff_size() { + let a: (u32, char) = kani::any(); + let b: u128 = unsafe { generic_transmute(a) }; + std::hint::black_box(b); +} diff --git a/tests/expected/intrinsics/transmute_unchecked_size.expected b/tests/expected/intrinsics/transmute_unchecked_size.expected new file mode 100644 index 000000000000..6ff9a1f67366 --- /dev/null +++ b/tests/expected/intrinsics/transmute_unchecked_size.expected @@ -0,0 +1,24 @@ +Checking harness transmute_wrapper_diff_size... +Status: UNREACHABLE\ +Description: ""Unreachable expected"" + +Failed Checks: Cannot transmute between types of different sizes. Transmuting from `8` to `16` bytes + +VERIFICATION:- FAILED + +Checking harness transmute_diff_size... + +Status: UNREACHABLE\ +Description: ""This should never be reached"" + +Status: UNREACHABLE\ +Description: ""Neither this one"" + +Failed Checks: Cannot transmute between types of different sizes. Transmuting from `4` to `2` bytes +Failed Checks: Cannot transmute between types of different sizes. Transmuting from `4` to `16` bytes + +VERIFICATION:- FAILED + +Verification failed for - transmute_wrapper_diff_size +Verification failed for - transmute_diff_size +0 successfully verified harnesses, 2 failures, 2 total diff --git a/tests/expected/intrinsics/transmute_unchecked_size.rs b/tests/expected/intrinsics/transmute_unchecked_size.rs new file mode 100644 index 000000000000..704448dcc6c6 --- /dev/null +++ b/tests/expected/intrinsics/transmute_unchecked_size.rs @@ -0,0 +1,44 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Checks that Kani correctly identify UB when invoking `transmute_unchecked` with different sizes. +//! See for more details. + +#![feature(core_intrinsics)] +use std::intrinsics::transmute_unchecked; + +/// Kani reachability checks are not currently applied to `unreachable` statements. +macro_rules! unreachable { + ($msg:literal) => { + assert!(false, $msg) + }; +} + +/// This should fail due to UB detection. +#[kani::proof] +pub fn transmute_diff_size() { + let a: u32 = kani::any(); + if kani::any() { + let smaller: u16 = unsafe { transmute_unchecked(a) }; + std::hint::black_box(smaller); + unreachable!("This should never be reached"); + } else { + let bigger: (u64, isize) = unsafe { transmute_unchecked(a) }; + std::hint::black_box(bigger); + unreachable!("Neither this one"); + } +} + +/// Generic transmute wrapper. +pub unsafe fn generic_transmute(src: S) -> D { + transmute_unchecked(src) +} + +/// This should also fail due to UB detection. +#[kani::proof] +pub fn transmute_wrapper_diff_size() { + let a: (u32, char) = kani::any(); + let b: u128 = unsafe { generic_transmute(a) }; + std::hint::black_box(b); + unreachable!("Unreachable expected"); +} diff --git a/tests/expected/issue-3571/issue_3571.expected b/tests/expected/issue-3571/issue_3571.expected new file mode 100644 index 000000000000..bed39a66b7af --- /dev/null +++ b/tests/expected/issue-3571/issue_3571.expected @@ -0,0 +1,9 @@ +Failed Checks: misaligned pointer dereference: address must be a multiple of its type's alignment + +Failed Checks: null pointer dereference occurred + +VERIFICATION:- FAILED (encountered failures other than panics, which were unexpected) + +Verification failed for - rust_ub_should_fail +Verification failed for - rust_ub_fails +Complete - 0 successfully verified harnesses, 2 failures, 2 total. diff --git a/tests/expected/issue-3571/issue_3571.rs b/tests/expected/issue-3571/issue_3571.rs new file mode 100644 index 000000000000..c4d55f39b4e4 --- /dev/null +++ b/tests/expected/issue-3571/issue_3571.rs @@ -0,0 +1,16 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::proof] +#[kani::should_panic] +pub fn rust_ub_fails() { + let ptr = 0 as *const u32; + let _invalid_ref = unsafe { &*ptr }; +} + +#[kani::proof] +#[kani::should_panic] +pub fn rust_ub_should_fail() { + let ptr = 10 as *const u32; + let _invalid_read = unsafe { *ptr }; +} diff --git a/tests/expected/offset-bounds-check/out_of_bounds_ub_check.expected b/tests/expected/offset-bounds-check/out_of_bounds_ub_check.expected index d8c6e135adc9..e0cb28198a18 100644 --- a/tests/expected/offset-bounds-check/out_of_bounds_ub_check.expected +++ b/tests/expected/offset-bounds-check/out_of_bounds_ub_check.expected @@ -1,4 +1,6 @@ Failed Checks: Offset result and original pointer must point to the same allocation -Verification failed for - check_ptr_oob +Failed Checks: Offset result and original pointer must point to the same allocation -Complete - 1 successfully verified harnesses, 1 failures, 2 total. +Verification failed for - test_offset_overflow +Verification failed for - check_ptr_oob +Complete - 1 successfully verified harnesses, 2 failures, 3 total. diff --git a/tests/expected/offset-bounds-check/out_of_bounds_ub_check.rs b/tests/expected/offset-bounds-check/out_of_bounds_ub_check.rs index e6b4310269a1..fd08e7a76876 100644 --- a/tests/expected/offset-bounds-check/out_of_bounds_ub_check.rs +++ b/tests/expected/offset-bounds-check/out_of_bounds_ub_check.rs @@ -2,6 +2,9 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT //! Check that Kani offset operations correctly detect out-of-bound access. +#![feature(core_intrinsics)] +use std::intrinsics::offset; + /// Verification should fail because safety violation is not a regular panic. #[kani::proof] #[kani::should_panic] @@ -24,3 +27,15 @@ fn check_ptr_end() { // Safety: Pointers point to the same allocation assert_eq!(unsafe { end_ptr.offset_from(base_ptr) }, 1); } + +#[kani::proof] +fn test_offset_overflow() { + let s: &str = "123"; + let ptr: *const u8 = s.as_ptr(); + + unsafe { + // This should fail because adding `isize::MAX` to `ptr` would overflow + // `isize` + let _d = offset(ptr, isize::MAX); + } +} diff --git a/tests/expected/offset-overflow/expected b/tests/expected/offset-overflow/expected deleted file mode 100644 index af5ea73875ca..000000000000 --- a/tests/expected/offset-overflow/expected +++ /dev/null @@ -1,4 +0,0 @@ -Failed Checks: Offset result and original pointer must point to the same allocation -Verification failed for - test_offset_overflow - -Complete - 0 successfully verified harnesses, 1 failures, 1 total. diff --git a/tests/expected/offset-overflow/main.rs b/tests/expected/offset-overflow/main.rs deleted file mode 100644 index fc9f36b9cc5d..000000000000 --- a/tests/expected/offset-overflow/main.rs +++ /dev/null @@ -1,19 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -// Checks that `offset` fails if the offset computation would -// result in an arithmetic overflow -#![feature(core_intrinsics)] -use std::intrinsics::offset; - -#[kani::proof] -fn test_offset_overflow() { - let s: &str = "123"; - let ptr: *const u8 = s.as_ptr(); - - unsafe { - // This should fail because adding `isize::MAX` to `ptr` would overflow - // `isize` - let _d = offset(ptr, isize::MAX); - } -} diff --git a/tests/expected/offset-overflows-isize/expected b/tests/expected/offset-overflows-isize/expected new file mode 100644 index 000000000000..f554e2b1804b --- /dev/null +++ b/tests/expected/offset-overflows-isize/expected @@ -0,0 +1,8 @@ +::to_isize.safety_check\ + - Status: FAILURE\ + - Description: "Offset value overflows isize" + +Failed Checks: Offset value overflows isize + +Verification failed for - test_non_zst +Complete - 1 successfully verified harnesses, 1 failures, 2 total. diff --git a/tests/expected/offset-overflows-isize/main.rs b/tests/expected/offset-overflows-isize/main.rs new file mode 100644 index 000000000000..06400c1163d7 --- /dev/null +++ b/tests/expected/offset-overflows-isize/main.rs @@ -0,0 +1,21 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Checks that `offset` does not accept a `count` greater than isize::MAX, +// except for ZSTs, c.f. https://github.com/model-checking/kani/issues/3896 + +#[kani::proof] +fn test_zst() { + let mut x = (); + let ptr: *mut () = &mut x as *mut (); + let count: usize = (isize::MAX as usize) + 1; + let _ = unsafe { ptr.add(count) }; +} + +#[kani::proof] +fn test_non_zst() { + let mut x = 7; + let ptr: *mut i32 = &mut x as *mut i32; + let count: usize = (isize::MAX as usize) + 1; + let _ = unsafe { ptr.add(count) }; +} diff --git a/tests/expected/uninit/access-padding-uninit/access-padding-enum-diverging-variants.expected b/tests/expected/uninit/access-padding-uninit/access-padding-enum-diverging-variants.expected new file mode 100644 index 000000000000..89a3572de316 --- /dev/null +++ b/tests/expected/uninit/access-padding-uninit/access-padding-enum-diverging-variants.expected @@ -0,0 +1,4 @@ +Failed Checks: Kani currently doesn't support checking memory initialization for pointers to `E1. Cannot determine layout for an Enum of type E1, as it has multiple variants that have different padding. + +Verification failed for - access_padding_unsupported +Complete - 1 successfully verified harnesses, 1 failures, 2 total. diff --git a/tests/kani/Uninit/access-padding-enum-diverging-variants.rs b/tests/expected/uninit/access-padding-uninit/access-padding-enum-diverging-variants.rs similarity index 97% rename from tests/kani/Uninit/access-padding-enum-diverging-variants.rs rename to tests/expected/uninit/access-padding-uninit/access-padding-enum-diverging-variants.rs index fae491c40622..6f41961acb13 100644 --- a/tests/kani/Uninit/access-padding-enum-diverging-variants.rs +++ b/tests/expected/uninit/access-padding-uninit/access-padding-enum-diverging-variants.rs @@ -21,7 +21,6 @@ enum E2 { } #[kani::proof] -#[kani::should_panic] fn access_padding_unsupported() { let s = E1::A(0, 0); let ptr: *const u8 = addr_of!(s) as *const u8; diff --git a/tests/expected/uninit/access-padding-uninit/access-padding-enum-multiple-variants.expected b/tests/expected/uninit/access-padding-uninit/access-padding-enum-multiple-variants.expected new file mode 100644 index 000000000000..29fa17a972f5 --- /dev/null +++ b/tests/expected/uninit/access-padding-uninit/access-padding-enum-multiple-variants.expected @@ -0,0 +1,7 @@ +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8` + +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8` + +Verification failed for - access_padding_uninit_b +Verification failed for - access_padding_uninit_a +Complete - 2 successfully verified harnesses, 2 failures, 4 total. diff --git a/tests/kani/Uninit/access-padding-enum-multiple-variants.rs b/tests/expected/uninit/access-padding-uninit/access-padding-enum-multiple-variants.rs similarity index 96% rename from tests/kani/Uninit/access-padding-enum-multiple-variants.rs rename to tests/expected/uninit/access-padding-uninit/access-padding-enum-multiple-variants.rs index dd6942252cb2..11c70dd7cd92 100644 --- a/tests/kani/Uninit/access-padding-enum-multiple-variants.rs +++ b/tests/expected/uninit/access-padding-uninit/access-padding-enum-multiple-variants.rs @@ -33,7 +33,6 @@ fn access_padding_init_b() { } #[kani::proof] -#[kani::should_panic] fn access_padding_uninit_a() { let s = E::A(0, 0); let ptr: *const u8 = addr_of!(s) as *const u8; @@ -41,7 +40,6 @@ fn access_padding_uninit_a() { } #[kani::proof] -#[kani::should_panic] fn access_padding_uninit_b() { let s = E::A(0, 0); let ptr: *const u8 = addr_of!(s) as *const u8; diff --git a/tests/expected/uninit/access-padding-uninit/access-padding-enum-single-field.expected b/tests/expected/uninit/access-padding-uninit/access-padding-enum-single-field.expected new file mode 100644 index 000000000000..caab803ad09a --- /dev/null +++ b/tests/expected/uninit/access-padding-uninit/access-padding-enum-single-field.expected @@ -0,0 +1,5 @@ +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8` +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8` + +Verification failed for - access_padding_uninit +Complete - 1 successfully verified harnesses, 1 failures, 2 total. diff --git a/tests/kani/Uninit/access-padding-enum-single-field.rs b/tests/expected/uninit/access-padding-uninit/access-padding-enum-single-field.rs similarity index 97% rename from tests/kani/Uninit/access-padding-enum-single-field.rs rename to tests/expected/uninit/access-padding-uninit/access-padding-enum-single-field.rs index 63f7f6043905..da1f2a202364 100644 --- a/tests/kani/Uninit/access-padding-enum-single-field.rs +++ b/tests/expected/uninit/access-padding-uninit/access-padding-enum-single-field.rs @@ -25,7 +25,6 @@ fn access_padding_init() { } #[kani::proof] -#[kani::should_panic] fn access_padding_uninit() { let s = E::A(0); let ptr: *const u8 = addr_of!(s) as *const u8; diff --git a/tests/expected/uninit/access-padding-uninit/access-padding-enum-single-variant.expected b/tests/expected/uninit/access-padding-uninit/access-padding-enum-single-variant.expected new file mode 100644 index 000000000000..fa661dfbe329 --- /dev/null +++ b/tests/expected/uninit/access-padding-uninit/access-padding-enum-single-variant.expected @@ -0,0 +1,4 @@ +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8` + +Verification failed for - access_padding_uninit +Complete - 1 successfully verified harnesses, 1 failures, 2 total. diff --git a/tests/kani/Uninit/access-padding-enum-single-variant.rs b/tests/expected/uninit/access-padding-uninit/access-padding-enum-single-variant.rs similarity index 97% rename from tests/kani/Uninit/access-padding-enum-single-variant.rs rename to tests/expected/uninit/access-padding-uninit/access-padding-enum-single-variant.rs index bb87d36d26c8..9946fc83cee9 100644 --- a/tests/kani/Uninit/access-padding-enum-single-variant.rs +++ b/tests/expected/uninit/access-padding-uninit/access-padding-enum-single-variant.rs @@ -24,7 +24,6 @@ fn access_padding_init() { } #[kani::proof] -#[kani::should_panic] fn access_padding_uninit() { let s = E::A(0, 0); let ptr: *const u8 = addr_of!(s) as *const u8; diff --git a/tests/expected/uninit/access-padding-uninit/expected b/tests/expected/uninit/access-padding-uninit/access-padding-uninit.expected similarity index 100% rename from tests/expected/uninit/access-padding-uninit/expected rename to tests/expected/uninit/access-padding-uninit/access-padding-uninit.expected diff --git a/tests/expected/uninit/copy/expose_padding_via_copy.expected b/tests/expected/uninit/copy/expose_padding_via_copy.expected index 83d8badc8bf5..28686a566df4 100644 --- a/tests/expected/uninit/copy/expose_padding_via_copy.expected +++ b/tests/expected/uninit/copy/expose_padding_via_copy.expected @@ -1,8 +1,8 @@ -std::ptr::read::.assertion.1\ +std::ptr::read::.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u64`"\ -std::ptr::read::.assertion.2\ +std::ptr::read::.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u64`"\ diff --git a/tests/expected/uninit/copy/expose_padding_via_copy_convoluted.expected b/tests/expected/uninit/copy/expose_padding_via_copy_convoluted.expected index cbe7ec97cb7b..b9cdd6137592 100644 --- a/tests/expected/uninit/copy/expose_padding_via_copy_convoluted.expected +++ b/tests/expected/uninit/copy/expose_padding_via_copy_convoluted.expected @@ -1,8 +1,8 @@ -std::ptr::read::.assertion.1\ +std::ptr::read::.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u64`"\ -std::ptr::read::.assertion.2\ +std::ptr::read::.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u64`"\ diff --git a/tests/expected/uninit/copy/expose_padding_via_non_byte_copy.expected b/tests/expected/uninit/copy/expose_padding_via_non_byte_copy.expected index 3fc86e45a46e..d3b1db9bd498 100644 --- a/tests/expected/uninit/copy/expose_padding_via_non_byte_copy.expected +++ b/tests/expected/uninit/copy/expose_padding_via_non_byte_copy.expected @@ -1,8 +1,8 @@ -std::ptr::read::.assertion.1\ +std::ptr::read::.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u64`"\ -std::ptr::read::.assertion.2\ +std::ptr::read::.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u64`"\ diff --git a/tests/expected/uninit/copy/read_after_copy.expected b/tests/expected/uninit/copy/read_after_copy.expected index 56a3460a1d7b..c5d133d787b9 100644 --- a/tests/expected/uninit/copy/read_after_copy.expected +++ b/tests/expected/uninit/copy/read_after_copy.expected @@ -1,8 +1,8 @@ -std::ptr::read::.assertion.1\ +std::ptr::read::.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u64`"\ -std::ptr::read::.assertion.2\ +std::ptr::read::.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u64`"\ diff --git a/tests/expected/uninit/delayed-ub/expected b/tests/expected/uninit/delayed-ub/delayed-ub.expected similarity index 73% rename from tests/expected/uninit/delayed-ub/expected rename to tests/expected/uninit/delayed-ub/delayed-ub.expected index b7c139c2d101..d998801c2ca7 100644 --- a/tests/expected/uninit/delayed-ub/expected +++ b/tests/expected/uninit/delayed-ub/delayed-ub.expected @@ -1,50 +1,45 @@ -delayed_ub_trigger_copy.assertion.\ +delayed_ub_trigger_copy.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"\ -delayed_ub_slices.assertion.\ - - Status: FAILURE\ - - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `[u128; 4]`" - -delayed_ub_structs.assertion.\ +delayed_ub_structs.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `U`" -delayed_ub_double_copy.assertion.\ +delayed_ub_double_copy.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"\ -delayed_ub_copy.assertion.\ +delayed_ub_copy.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" -delayed_ub_closure_capture_laundered.assertion.\ +delayed_ub_closure_capture_laundered.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" -delayed_ub_closure_laundered.assertion.\ +delayed_ub_closure_laundered.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" -delayed_ub_laundered.assertion.\ +delayed_ub_laundered.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" -delayed_ub_static.assertion.\ +delayed_ub_static.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" -delayed_ub_transmute.assertion.\ +delayed_ub_transmute.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" -delayed_ub.assertion.\ +delayed_ub.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" Summary: Verification failed for - delayed_ub_trigger_copy -Verification failed for - delayed_ub_slices Verification failed for - delayed_ub_structs Verification failed for - delayed_ub_double_copy Verification failed for - delayed_ub_copy @@ -54,4 +49,4 @@ Verification failed for - delayed_ub_laundered Verification failed for - delayed_ub_static Verification failed for - delayed_ub_transmute Verification failed for - delayed_ub -Complete - 0 successfully verified harnesses, 11 failures, 11 total. +Complete - 0 successfully verified harnesses, 10 failures, 10 total. diff --git a/tests/expected/uninit/delayed-ub/delayed-ub.rs b/tests/expected/uninit/delayed-ub/delayed-ub.rs index d7f258c27ba5..17b654533406 100644 --- a/tests/expected/uninit/delayed-ub/delayed-ub.rs +++ b/tests/expected/uninit/delayed-ub/delayed-ub.rs @@ -170,19 +170,6 @@ fn delayed_ub_structs() { } } -/// Delayed UB via mutable pointer write into a slice element. -#[kani::proof] -fn delayed_ub_slices() { - unsafe { - // Create an array. - let mut arr = [0u128; 4]; - // Get a pointer to a part of the array. - let ptr = &mut arr[0..2][0..1][0] as *mut _ as *mut (u8, u32); - *ptr = (4, 4); - let arr_copy = arr; // UB: This reads a padding value inside the array! - } -} - /// Delayed UB via mutable pointer copy, which should be the only delayed UB trigger in this case. #[kani::proof] fn delayed_ub_trigger_copy() { diff --git a/tests/expected/uninit/delayed-ub/slices_fixme.expected b/tests/expected/uninit/delayed-ub/slices_fixme.expected new file mode 100644 index 000000000000..902980a2bf1c --- /dev/null +++ b/tests/expected/uninit/delayed-ub/slices_fixme.expected @@ -0,0 +1,5 @@ +delayed_ub_slices.assertion.\ + - Status: FAILURE\ + - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `[u128; 4]`" + +Verification failed for - delayed_ub_slices diff --git a/tests/expected/uninit/delayed-ub/slices_fixme.rs b/tests/expected/uninit/delayed-ub/slices_fixme.rs new file mode 100644 index 000000000000..c112a4638363 --- /dev/null +++ b/tests/expected/uninit/delayed-ub/slices_fixme.rs @@ -0,0 +1,21 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z ghost-state -Z uninit-checks + +//! Checks that Kani catches instances of delayed UB for slices. +//! This test used to live inside delayed-ub, but the 2/5/2025 toolchain upgrade introduced a regression for this test. +//! Once this test is fixed, move it back into delayed-ub.rs +//! See https://github.com/model-checking/kani/issues/3881 for details. + +/// Delayed UB via mutable pointer write into a slice element. +#[kani::proof] +fn delayed_ub_slices() { + unsafe { + // Create an array. + let mut arr = [0u128; 4]; + // Get a pointer to a part of the array. + let ptr = &mut arr[0..2][0..1][0] as *mut _ as *mut (u8, u32); + *ptr = (4, 4); + let arr_copy = arr; // UB: This reads a padding value inside the array! + } +} diff --git a/tests/expected/uninit/intrinsics/expected b/tests/expected/uninit/intrinsics/expected index b40fe6714ba8..d19d694df75e 100644 --- a/tests/expected/uninit/intrinsics/expected +++ b/tests/expected/uninit/intrinsics/expected @@ -1,36 +1,32 @@ -std::ptr::write::>.assertion.1\ +std::ptr::read::>.unsupported_construct.\ - Status: FAILURE\ - Description: "Interaction between raw pointers and unions is not yet supported." -std::ptr::write::>.assertion.1\ - - Status: FAILURE\ - - Description: "Interaction between raw pointers and unions is not yet supported."\ - -check_typed_swap_nonoverlapping.assertion.1\ +check_typed_swap_nonoverlapping.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*mut u8`" -check_typed_swap_nonoverlapping.assertion.2\ +check_typed_swap_nonoverlapping.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*mut u8`" -check_volatile_load.assertion.1\ +check_volatile_load.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`" -check_compare_bytes.assertion.1\ +check_compare_bytes.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`" -check_compare_bytes.assertion.2\ +check_compare_bytes.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`" -std::ptr::read::.assertion.1\ +std::ptr::read::.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`" -std::ptr::read::.assertion.2\ +std::ptr::read::.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u8`" diff --git a/tests/expected/uninit/multiple-instrumentations.expected b/tests/expected/uninit/multiple-instrumentations.expected index 153024dc692b..82f37b22ed0d 100644 --- a/tests/expected/uninit/multiple-instrumentations.expected +++ b/tests/expected/uninit/multiple-instrumentations.expected @@ -1,16 +1,16 @@ -multiple_instrumentations_different_vars.assertion.3\ +multiple_instrumentations_different_vars.safety_check\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" -multiple_instrumentations_different_vars.assertion.4\ +multiple_instrumentations_different_vars.safety_check\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u64`" -multiple_instrumentations.assertion.2\ +multiple_instrumentations.safety_check\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" -multiple_instrumentations.assertion.3\ +multiple_instrumentations.safety_check\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" diff --git a/tests/expected/uninit/unions.expected b/tests/expected/uninit/unions.expected index ca7f777c4065..cf40fbb608df 100644 --- a/tests/expected/uninit/unions.expected +++ b/tests/expected/uninit/unions.expected @@ -1,28 +1,28 @@ -union_update_should_fail.assertion.1\ +union_update_should_fail.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u32`" -union_complex_subfields_should_fail.assertion.1\ +union_complex_subfields_should_fail.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u16`" -basic_union_should_fail.assertion.1\ +basic_union_should_fail.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u32`" -cross_function_union_should_fail::helper.assertion.1\ +cross_function_union_should_fail::helper.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u32`" -cross_function_multi_union_should_fail::helper.assertion.1\ +cross_function_multi_union_should_fail::helper.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u32`" -multi_cross_function_union_should_fail::sub_helper.assertion.1\ +multi_cross_function_union_should_fail::sub_helper.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u32`" -basic_multifield_union_should_fail.assertion.7\ +basic_multifield_union_should_fail.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" diff --git a/tests/expected/valid-value-checks/constants.expected b/tests/expected/valid-value-checks/constants.expected new file mode 100644 index 000000000000..639e193bc561 --- /dev/null +++ b/tests/expected/valid-value-checks/constants.expected @@ -0,0 +1,10 @@ +Failed Checks: Undefined Behavior: Invalid value of type `[char; 2]` + +Failed Checks: Undefined Behavior: Invalid value of type `char` + +Failed Checks: Undefined Behavior: Invalid value of type `bool` + +Verification failed for - cast_to_invalid_offset +Verification failed for - cast_to_invalid_char +Verification failed for - transmute_invalid_bool +Complete - 3 successfully verified harnesses, 3 failures, 6 total. diff --git a/tests/kani/ValidValues/constants.rs b/tests/expected/valid-value-checks/constants.rs similarity index 93% rename from tests/kani/ValidValues/constants.rs rename to tests/expected/valid-value-checks/constants.rs index 5230e6e5e6cb..aa7aba6fe079 100644 --- a/tests/kani/ValidValues/constants.rs +++ b/tests/expected/valid-value-checks/constants.rs @@ -21,19 +21,16 @@ fn cast_to_valid_offset() { } #[kani::proof] -#[kani::should_panic] fn transmute_invalid_bool() { let _b = unsafe { std::mem::transmute::(2) }; } #[kani::proof] -#[kani::should_panic] fn cast_to_invalid_char() { let _c = unsafe { *(&u32::MAX as *const u32 as *const char) }; } #[kani::proof] -#[kani::should_panic] fn cast_to_invalid_offset() { let val = [100u32, u32::MAX]; let _c = unsafe { *(&val as *const [u32; 2] as *const [char; 2]) }; diff --git a/tests/expected/valid-value-checks/custom_niche.expected b/tests/expected/valid-value-checks/custom_niche.expected new file mode 100644 index 000000000000..3d78563ef8b1 --- /dev/null +++ b/tests/expected/valid-value-checks/custom_niche.expected @@ -0,0 +1,28 @@ +Failed Checks: Undefined Behavior: Invalid value of type `Rating` + +Failed Checks: Kani currently doesn't support checking validity of `copy_nonoverlapping` for `*const Rating` + +Failed Checks: Kani currently doesn't support checking validity of `copy_nonoverlapping` for `*const Rating` + +Failed Checks: Undefined Behavior: Invalid value of type `Rating` + +Failed Checks: Undefined Behavior: Invalid value of type `Rating` + +Failed Checks: Undefined Behavior: Invalid value of type `Rating` + +Failed Checks: Undefined Behavior: Invalid value of type `Rating` + +Failed Checks: Undefined Behavior: Invalid value of type `Rating` + +Failed Checks: Undefined Behavior: Invalid value of type `Rating` + +Verification failed for - check_invalid_increment +Verification failed for - check_copy_nonoverlap_ub +Verification failed for - check_copy_nonoverlap +Verification failed for - check_invalid_transmute_copy +Verification failed for - check_invalid_transmute +Verification failed for - check_invalid_dereference +Verification failed for - check_new_with_ub_limits +Verification failed for - check_unchecked_new_ub +Verification failed for - check_new_with_ub +Complete - 2 successfully verified harnesses, 9 failures, 11 total. diff --git a/tests/kani/ValidValues/custom_niche.rs b/tests/expected/valid-value-checks/custom_niche.rs similarity index 94% rename from tests/kani/ValidValues/custom_niche.rs rename to tests/expected/valid-value-checks/custom_niche.rs index b282fec3c645..c27bc6fdc057 100644 --- a/tests/kani/ValidValues/custom_niche.rs +++ b/tests/expected/valid-value-checks/custom_niche.rs @@ -38,41 +38,35 @@ impl Rating { } #[kani::proof] -#[kani::should_panic] pub fn check_new_with_ub() { assert_eq!(Rating::new(10), None); } #[kani::proof] -#[kani::should_panic] pub fn check_unchecked_new_ub() { let val = kani::any(); assert_eq!(unsafe { Rating::new_unchecked(val).stars }, val); } #[kani::proof] -#[kani::should_panic] pub fn check_new_with_ub_limits() { let stars = kani::any_where(|s: &u8| *s == 0 || *s > 5); let _ = Rating::new(stars); } #[kani::proof] -#[kani::should_panic] pub fn check_invalid_dereference() { let any: u8 = kani::any(); let _rating: Rating = unsafe { *(&any as *const _ as *const _) }; } #[kani::proof] -#[kani::should_panic] pub fn check_invalid_transmute() { let any: u8 = kani::any(); let _rating: Rating = unsafe { mem::transmute(any) }; } #[kani::proof] -#[kani::should_panic] pub fn check_invalid_transmute_copy() { let any: u8 = kani::any(); let _rating: Rating = unsafe { mem::transmute_copy(&any) }; @@ -82,7 +76,6 @@ pub fn check_invalid_transmute_copy() { /// /// FIX-ME: This is not supported today, and we fail due to unsupported check. #[kani::proof] -#[kani::should_panic] pub fn check_copy_nonoverlap() { let stars = kani::any_where(|s: &u8| *s == 0 || *s > 5); let mut rating: Rating = kani::any(); @@ -90,7 +83,6 @@ pub fn check_copy_nonoverlap() { } #[kani::proof] -#[kani::should_panic] pub fn check_copy_nonoverlap_ub() { let any: u8 = kani::any(); let mut rating: Rating = kani::any(); @@ -98,7 +90,6 @@ pub fn check_copy_nonoverlap_ub() { } #[kani::proof] -#[kani::should_panic] pub fn check_invalid_increment() { let mut orig: Rating = kani::any(); unsafe { orig.stars += 1 }; diff --git a/tests/expected/valid-value-checks/maybe_uninit.expected b/tests/expected/valid-value-checks/maybe_uninit.expected new file mode 100644 index 000000000000..8264876dc4f7 --- /dev/null +++ b/tests/expected/valid-value-checks/maybe_uninit.expected @@ -0,0 +1,5 @@ + ** 1 of 14 failed (1 unreachable)\ +Failed Checks: Undefined Behavior: Invalid value of type `std::num::NonZero` + +Verification failed for - check_invalid_zeroed +Complete - 1 successfully verified harnesses, 1 failures, 2 total. diff --git a/tests/kani/ValidValues/maybe_uninit.rs b/tests/expected/valid-value-checks/maybe_uninit.rs similarity index 96% rename from tests/kani/ValidValues/maybe_uninit.rs rename to tests/expected/valid-value-checks/maybe_uninit.rs index 620ad8ef5ba3..926277a744dc 100644 --- a/tests/kani/ValidValues/maybe_uninit.rs +++ b/tests/expected/valid-value-checks/maybe_uninit.rs @@ -14,7 +14,6 @@ pub fn check_valid_zeroed() { } #[kani::proof] -#[kani::should_panic] pub fn check_invalid_zeroed() { let maybe = MaybeUninit::zeroed(); let _val: NonZeroI64 = unsafe { maybe.assume_init() }; diff --git a/tests/expected/valid-value-checks/non_null.expected b/tests/expected/valid-value-checks/non_null.expected new file mode 100644 index 000000000000..bc8572b879c6 --- /dev/null +++ b/tests/expected/valid-value-checks/non_null.expected @@ -0,0 +1,7 @@ +Failed Checks: Undefined Behavior: Invalid value of type `std::ptr::NonNull` + +Failed Checks: Undefined Behavior: Invalid value of type `std::ptr::NonNull` + +Verification failed for - check_invalid_value_cfg +Verification failed for - check_invalid_value +Complete - 1 successfully verified harnesses, 2 failures, 3 total. diff --git a/tests/kani/ValidValues/non_null.rs b/tests/expected/valid-value-checks/non_null.rs similarity index 94% rename from tests/kani/ValidValues/non_null.rs rename to tests/expected/valid-value-checks/non_null.rs index 4874b61bf2d0..85d1a3876785 100644 --- a/tests/kani/ValidValues/non_null.rs +++ b/tests/expected/valid-value-checks/non_null.rs @@ -7,13 +7,11 @@ use std::num::NonZeroU8; use std::ptr::{self, NonNull}; #[kani::proof] -#[kani::should_panic] pub fn check_invalid_value() { let _ = unsafe { NonNull::new_unchecked(ptr::null_mut::()) }; } #[kani::proof] -#[kani::should_panic] pub fn check_invalid_value_cfg() { let nn = unsafe { NonNull::new_unchecked(ptr::null_mut::()) }; // This should be unreachable. TODO: Make this expected test. diff --git a/tests/expected/valid-value-checks/write_bytes.expected b/tests/expected/valid-value-checks/write_bytes.expected new file mode 100644 index 000000000000..8c14a9046d8d --- /dev/null +++ b/tests/expected/valid-value-checks/write_bytes.expected @@ -0,0 +1,5 @@ + ** 1 of 11 failed (1 unreachable)\ +Failed Checks: Undefined Behavior: Invalid value of type `char` + +Verification failed for - check_invalid_write +Complete - 1 successfully verified harnesses, 1 failures, 2 total. diff --git a/tests/kani/ValidValues/write_bytes.rs b/tests/expected/valid-value-checks/write_bytes.rs similarity index 96% rename from tests/kani/ValidValues/write_bytes.rs rename to tests/expected/valid-value-checks/write_bytes.rs index e4f73b1f3479..0b0ae6f343db 100644 --- a/tests/kani/ValidValues/write_bytes.rs +++ b/tests/expected/valid-value-checks/write_bytes.rs @@ -5,7 +5,6 @@ #![feature(core_intrinsics)] #[kani::proof] -#[kani::should_panic] pub fn check_invalid_write() { let mut val = 'a'; let ptr = &mut val as *mut char; diff --git a/tests/expected/valid-value-checks/write_invalid.expected b/tests/expected/valid-value-checks/write_invalid.expected new file mode 100644 index 000000000000..ba6c5b2ba65c --- /dev/null +++ b/tests/expected/valid-value-checks/write_invalid.expected @@ -0,0 +1,13 @@ + ** 1 of 19 failed (2 unreachable)\ +Failed Checks: Kani currently doesn't support checking validity of `transmute` for `std::option::Option>` + + ** 1 of 43 failed (2 unreachable)\ +Failed Checks: Kani currently doesn't support checking validity of `transmute` for `std::option::Option>` + + ** 1 of 18 failed (1 unreachable)\ +Failed Checks: Kani currently doesn't support checking validity of `transmute` for `std::option::Option>` + +Verification failed for - read_invalid_is_ub +Verification failed for - write_valid_before_read +Verification failed for - write_invalid_bytes_no_ub_with_spurious_cex +Complete - 0 successfully verified harnesses, 3 failures, 3 total. diff --git a/tests/kani/ValidValues/write_invalid.rs b/tests/expected/valid-value-checks/write_invalid.rs similarity index 94% rename from tests/kani/ValidValues/write_invalid.rs rename to tests/expected/valid-value-checks/write_invalid.rs index 05d3705bd69a..677ffe4edf61 100644 --- a/tests/kani/ValidValues/write_invalid.rs +++ b/tests/expected/valid-value-checks/write_invalid.rs @@ -9,7 +9,6 @@ use std::num::NonZeroU8; #[kani::proof] -#[kani::should_panic] pub fn write_invalid_bytes_no_ub_with_spurious_cex() { let mut non_zero: NonZeroU8 = kani::any(); let dest = &mut non_zero as *mut _; @@ -17,7 +16,6 @@ pub fn write_invalid_bytes_no_ub_with_spurious_cex() { } #[kani::proof] -#[kani::should_panic] pub fn write_valid_before_read() { let mut non_zero: NonZeroU8 = kani::any(); let mut non_zero_2: NonZeroU8 = kani::any(); @@ -28,7 +26,6 @@ pub fn write_valid_before_read() { } #[kani::proof] -#[kani::should_panic] pub fn read_invalid_is_ub() { let mut non_zero: NonZeroU8 = kani::any(); let dest = &mut non_zero as *mut _; diff --git a/tests/expected/zst/expected b/tests/expected/zst/expected index bec891bea92c..3efe59d3445f 100644 --- a/tests/expected/zst/expected +++ b/tests/expected/zst/expected @@ -1,4 +1,4 @@ -Status: FAILURE\ -Description: "dereference failure: pointer NULL" +- Status: FAILURE\ +- Description: "null pointer dereference occurred" VERIFICATION:- FAILED diff --git a/tests/kani/CodegenMisc/missing_mut_fn.rs b/tests/kani/CodegenMisc/missing_mut_fn.rs new file mode 100644 index 000000000000..ae7bfe753bf0 --- /dev/null +++ b/tests/kani/CodegenMisc/missing_mut_fn.rs @@ -0,0 +1,27 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Ensure Kani can codegen code with a pointer to a function that is never used +//! See for more details. +fn foo(_func: &mut F) {} +fn foo_dyn(_func: &mut dyn Fn()) {} + +#[kani::proof] +fn check_foo() { + fn f() {} + + foo(&mut f); +} + +#[kani::proof] +fn check_foo_dyn() { + fn f() {} + + foo_dyn(&mut f); +} + +#[kani::proof] +fn check_foo_unused() { + fn f() {} + + let ptr = &mut f; +} diff --git a/tests/perf/s2n-quic b/tests/perf/s2n-quic index 450059379ac2..00e33714d74b 160000 --- a/tests/perf/s2n-quic +++ b/tests/perf/s2n-quic @@ -1 +1 @@ -Subproject commit 450059379ac24f9ba73c8ac940b1c6820af401ce +Subproject commit 00e33714d74b0646bc18ab65c90a45504a185828 diff --git a/tests/script-based-pre/cargo_autoharness_contracts/Cargo.toml b/tests/script-based-pre/cargo_autoharness_contracts/Cargo.toml new file mode 100644 index 000000000000..10a47f48262b --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_contracts/Cargo.toml @@ -0,0 +1,10 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "cargo_autoharness_contracts" +version = "0.1.0" +edition = "2024" + +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } diff --git a/tests/script-based-pre/cargo_autoharness_contracts/config.yml b/tests/script-based-pre/cargo_autoharness_contracts/config.yml new file mode 100644 index 000000000000..38bf8ee6c38c --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_contracts/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: contracts.sh +expected: contracts.expected diff --git a/tests/script-based-pre/cargo_autoharness_contracts/contracts.expected b/tests/script-based-pre/cargo_autoharness_contracts/contracts.expected new file mode 100644 index 000000000000..1e25913b6765 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_contracts/contracts.expected @@ -0,0 +1,28 @@ +Autoharness: Checking function should_fail::max's contract against all possible inputs... +assertion\ + - Status: FAILURE\ + - Description: "|result : &u32| *result == x" + +Autoharness: Checking function should_pass::has_loop_contract's contract against all possible inputs... +should_pass::has_loop_contract.assertion\ + - Status: SUCCESS\ + - Description: "assertion failed: x == 2" + +Autoharness: Checking function should_pass::has_recursion_gcd's contract against all possible inputs... +assertion\ + - Status: SUCCESS\ + - Description: "|result : &u8| *result != 0 && x % *result == 0 && y % *result == 0" + +Autoharness: Checking function should_pass::div's contract against all possible inputs... + +Autoharness: Checking function should_pass::unchecked_mul's contract against all possible inputs... +arithmetic_overflow\ + - Status: SUCCESS\ + - Description: "attempt to compute `unchecked_mul` which would overflow" + +Verification succeeded for - should_pass::unchecked_mul +Verification succeeded for - should_pass::has_loop_contract +Verification succeeded for - should_pass::has_recursion_gcd +Verification succeeded for - should_pass::div +Verification failed for - should_fail::max +Complete - 4 successfully verified functions, 1 failures, 5 total. diff --git a/tests/script-based-pre/cargo_autoharness_contracts/contracts.sh b/tests/script-based-pre/cargo_autoharness_contracts/contracts.sh new file mode 100755 index 000000000000..caad53eb8ac4 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_contracts/contracts.sh @@ -0,0 +1,9 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +cargo kani autoharness -Z unstable-options -Z function-contracts -Z loop-contracts +# We expect verification to fail, so the above command will produce an exit status of 1 +# However, we don't want the test to fail because of that exit status; we only want it to fail if the expected file doesn't match +# So, exit with a status code of 0 explicitly. +exit 0; diff --git a/tests/script-based-pre/cargo_autoharness_contracts/src/lib.rs b/tests/script-based-pre/cargo_autoharness_contracts/src/lib.rs new file mode 100644 index 000000000000..c9f9dd3fd1b0 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_contracts/src/lib.rs @@ -0,0 +1,56 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Test that the autoharness subcommand correctly verifies contracts, +// i.e., that it detects the presence of a contract and generates a contract +// harness instead of a standard harness. + +#![feature(stmt_expr_attributes)] +#![feature(proc_macro_hygiene)] + +mod should_pass { + #[kani::requires(divisor != 0)] + fn div(dividend: u32, divisor: u32) -> u32 { + dividend / divisor + } + + #[kani::requires(x != 0 && y != 0)] + #[kani::ensures(|result : &u8| *result != 0 && x % *result == 0 && y % *result == 0)] + #[kani::recursion] + fn has_recursion_gcd(x: u8, y: u8) -> u8 { + let mut max = x; + let mut min = y; + if min > max { + let val = max; + max = min; + min = val; + } + + let res = max % min; + if res == 0 { min } else { has_recursion_gcd(min, res) } + } + + fn has_loop_contract() { + let mut x: u8 = kani::any_where(|i| *i >= 2); + + #[kani::loop_invariant(x >= 2)] + while x > 2 { + x = x - 1; + } + + assert!(x == 2); + } + + // Test that we can autoharness functions for unsafe functions with contracts + #[kani::requires(!left.overflowing_mul(rhs).1)] + unsafe fn unchecked_mul(left: u8, rhs: u8) -> u8 { + left.unchecked_mul(rhs) + } +} + +mod should_fail { + #[kani::ensures(|result : &u32| *result == x)] + fn max(x: u32, y: u32) -> u32 { + if x > y { x } else { y } + } +} diff --git a/tests/script-based-pre/cargo_autoharness_exclude/Cargo.toml b/tests/script-based-pre/cargo_autoharness_exclude/Cargo.toml new file mode 100644 index 000000000000..cceaa1bb7651 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_exclude/Cargo.toml @@ -0,0 +1,10 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "cargo_autoharness_include" +version = "0.1.0" +edition = "2024" + +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } diff --git a/tests/script-based-pre/cargo_autoharness_exclude/config.yml b/tests/script-based-pre/cargo_autoharness_exclude/config.yml new file mode 100644 index 000000000000..d3c26a0301f4 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_exclude/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: exclude.sh +expected: exclude.expected diff --git a/tests/script-based-pre/cargo_autoharness_exclude/exclude.expected b/tests/script-based-pre/cargo_autoharness_exclude/exclude.expected new file mode 100644 index 000000000000..91d9eb4c399a --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_exclude/exclude.expected @@ -0,0 +1,4 @@ +Autoharness: Checking function include::simple against all possible inputs... +VERIFICATION:- SUCCESSFUL +Verification succeeded for - include::simple +Complete - 1 successfully verified functions, 0 failures, 1 total. \ No newline at end of file diff --git a/tests/script-based-pre/cargo_autoharness_exclude/exclude.sh b/tests/script-based-pre/cargo_autoharness_exclude/exclude.sh new file mode 100755 index 000000000000..492325dc5c81 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_exclude/exclude.sh @@ -0,0 +1,5 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +cargo kani autoharness -Z unstable-options --exclude-function exclude diff --git a/tests/script-based-pre/cargo_autoharness_exclude/src/lib.rs b/tests/script-based-pre/cargo_autoharness_exclude/src/lib.rs new file mode 100644 index 000000000000..7757239126c0 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_exclude/src/lib.rs @@ -0,0 +1,23 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Test that the automatic harness generation feature selects functions correctly +// when --exclude-function is provided. + +mod include { + fn simple(x: u8, _y: u16) -> u8 { + x + } + + // Doesn't implement Arbitrary, so still should not be included. + fn generic(x: u32, _y: T) -> u32 { + x + } +} + +// These functions are eligible for autoverification, but are excluded. +mod excluded { + fn simple(x: u8, _y: u16) -> u8 { + x + } +} diff --git a/tests/script-based-pre/cargo_autoharness_filter/Cargo.toml b/tests/script-based-pre/cargo_autoharness_filter/Cargo.toml new file mode 100644 index 000000000000..41f0d6133106 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_filter/Cargo.toml @@ -0,0 +1,10 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "cargo_autoharness_filter" +version = "0.1.0" +edition = "2024" + +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } diff --git a/tests/script-based-pre/cargo_autoharness_filter/config.yml b/tests/script-based-pre/cargo_autoharness_filter/config.yml new file mode 100644 index 000000000000..90ee1970e96c --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_filter/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: filter.sh +expected: filter.expected diff --git a/tests/script-based-pre/cargo_autoharness_filter/filter.expected b/tests/script-based-pre/cargo_autoharness_filter/filter.expected new file mode 100644 index 000000000000..9db37edf8232 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_filter/filter.expected @@ -0,0 +1,43 @@ +Autoharness: Checking function yes_harness::f_tuple against all possible inputs... +Autoharness: Checking function yes_harness::f_maybe_uninit against all possible inputs... +Autoharness: Checking function yes_harness::f_result against all possible inputs... +Autoharness: Checking function yes_harness::f_option against all possible inputs... +Autoharness: Checking function yes_harness::f_array against all possible inputs... +Autoharness: Checking function yes_harness::f_nonzero_isize against all possible inputs... +Autoharness: Checking function yes_harness::f_nonzero_i128 against all possible inputs... +Autoharness: Checking function yes_harness::f_nonzero_i64 against all possible inputs... +Autoharness: Checking function yes_harness::f_nonzero_i32 against all possible inputs... +Autoharness: Checking function yes_harness::f_nonzero_i16 against all possible inputs... +Autoharness: Checking function yes_harness::f_nonzero_i8 against all possible inputs... +Autoharness: Checking function yes_harness::f_nonzero_usize against all possible inputs... +Autoharness: Checking function yes_harness::f_nonzero_u128 against all possible inputs... +Autoharness: Checking function yes_harness::f_nonzero_u64 against all possible inputs... +Autoharness: Checking function yes_harness::f_nonzero_u32 against all possible inputs... +Autoharness: Checking function yes_harness::f_nonzero_u16 against all possible inputs... +Autoharness: Checking function yes_harness::f_nonzero_u8 against all possible inputs... +Autoharness: Checking function yes_harness::f_f128 against all possible inputs... +Autoharness: Checking function yes_harness::f_f16 against all possible inputs... +Autoharness: Checking function yes_harness::f_f64 against all possible inputs... +Autoharness: Checking function yes_harness::f_f32 against all possible inputs... +Autoharness: Checking function yes_harness::f_char against all possible inputs... +Autoharness: Checking function yes_harness::f_bool against all possible inputs... +Autoharness: Checking function yes_harness::f_isize against all possible inputs... +Autoharness: Checking function yes_harness::f_i128 against all possible inputs... +Autoharness: Checking function yes_harness::f_i64 against all possible inputs... +Autoharness: Checking function yes_harness::f_i32 against all possible inputs... +Autoharness: Checking function yes_harness::f_i16 against all possible inputs... +Autoharness: Checking function yes_harness::f_i8 against all possible inputs... +Autoharness: Checking function yes_harness::f_usize against all possible inputs... +Autoharness: Checking function yes_harness::f_u128 against all possible inputs... +Autoharness: Checking function yes_harness::f_u64 against all possible inputs... +Autoharness: Checking function yes_harness::f_u32 against all possible inputs... +Autoharness: Checking function yes_harness::f_u16 against all possible inputs... +Autoharness: Checking function yes_harness::f_u8 against all possible inputs... +Autoharness: Checking function yes_harness::f_unsupported_return_type against all possible inputs... +Autoharness: Checking function yes_harness::f_multiple_args against all possible inputs... +Autoharness: Checking function yes_harness::f_derives_arbitrary against all possible inputs... +Autoharness: Checking function yes_harness::f_manually_implements_arbitrary against all possible inputs... +Autoharness: Checking function yes_harness::f_phantom_data against all possible inputs... +Autoharness: Checking function yes_harness::f_phantom_pinned against all possible inputs... +Autoharness: Checking function yes_harness::empty_body against all possible inputs... +Complete - 42 successfully verified functions, 0 failures, 42 total. \ No newline at end of file diff --git a/tests/script-based-pre/cargo_autoharness_filter/filter.sh b/tests/script-based-pre/cargo_autoharness_filter/filter.sh new file mode 100755 index 000000000000..cec2f2e2a10b --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_filter/filter.sh @@ -0,0 +1,5 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +cargo kani autoharness -Z unstable-options diff --git a/tests/script-based-pre/cargo_autoharness_filter/src/lib.rs b/tests/script-based-pre/cargo_autoharness_filter/src/lib.rs new file mode 100644 index 000000000000..bb278c73a2e7 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_filter/src/lib.rs @@ -0,0 +1,210 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Test that the automatic harness generation feature filters functions correctly, +// i.e., that it generates harnesses for a function iff: +// - It is not itself a harness +// - All of its arguments implement Arbitrary, either trivially or through a user-provided implementation +// The bodies of these functions are purposefully left as simple as possible; +// the point is not to test the generated harnesses themselves, +// but only that we generate the harnesses in the first place. + +#![feature(f16)] +#![feature(f128)] + +extern crate kani; +use kani::Arbitrary; + +#[derive(Arbitrary)] +struct DerivesArbitrary { + x: u8, + y: u32, +} + +struct ManuallyImplementsArbitrary { + x: u8, + y: u32, +} + +impl Arbitrary for ManuallyImplementsArbitrary { + fn any() -> Self { + Self { x: kani::any(), y: kani::any() } + } +} + +struct DoesntImplementArbitrary { + x: u8, + y: u32, +} + +mod yes_harness { + use crate::{DerivesArbitrary, ManuallyImplementsArbitrary}; + use std::marker::{PhantomData, PhantomPinned}; + use std::mem::MaybeUninit; + use std::num::NonZero; + + // Kani-provided Arbitrary implementations + fn f_u8(x: u8) -> u8 { + x + } + fn f_u16(x: u16) -> u16 { + x + } + fn f_u32(x: u32) -> u32 { + x + } + fn f_u64(x: u64) -> u64 { + x + } + fn f_u128(x: u128) -> u128 { + x + } + fn f_usize(x: usize) -> usize { + x + } + fn f_i8(x: i8) -> i8 { + x + } + fn f_i16(x: i16) -> i16 { + x + } + fn f_i32(x: i32) -> i32 { + x + } + fn f_i64(x: i64) -> i64 { + x + } + fn f_i128(x: i128) -> i128 { + x + } + fn f_isize(x: isize) -> isize { + x + } + fn f_bool(x: bool) -> bool { + x + } + fn f_char(x: char) -> char { + x + } + fn f_f32(x: f32) -> f32 { + x + } + fn f_f64(x: f64) -> f64 { + x + } + fn f_f16(x: f16) -> f16 { + x + } + fn f_f128(x: f128) -> f128 { + x + } + fn f_nonzero_u8(x: NonZero) -> NonZero { + x + } + fn f_nonzero_u16(x: NonZero) -> NonZero { + x + } + fn f_nonzero_u32(x: NonZero) -> NonZero { + x + } + fn f_nonzero_u64(x: NonZero) -> NonZero { + x + } + fn f_nonzero_u128(x: NonZero) -> NonZero { + x + } + fn f_nonzero_usize(x: NonZero) -> NonZero { + x + } + fn f_nonzero_i8(x: NonZero) -> NonZero { + x + } + fn f_nonzero_i16(x: NonZero) -> NonZero { + x + } + fn f_nonzero_i32(x: NonZero) -> NonZero { + x + } + fn f_nonzero_i64(x: NonZero) -> NonZero { + x + } + fn f_nonzero_i128(x: NonZero) -> NonZero { + x + } + fn f_nonzero_isize(x: NonZero) -> NonZero { + x + } + fn f_array(x: [u8; 4]) -> [u8; 4] { + x + } + fn f_option(x: Option) -> Option { + x + } + fn f_result(x: Result) -> Result { + x + } + fn f_maybe_uninit(x: MaybeUninit) -> MaybeUninit { + x + } + fn f_tuple(x: (u8, u16, u32)) -> (u8, u16, u32) { + x + } + + // The return type doesn't implement Arbitrary, but that shouldn't matter + fn f_unsupported_return_type(x: u8) -> Vec { + vec![x] + } + + // Multiple arguments of different types, all of which implement Arbitrary + fn f_multiple_args(x: u8, y: u16, z: u32) -> (u8, u16, u32) { + (x, y, z) + } + + // User-defined types that implement Arbitrary + fn f_derives_arbitrary(x: DerivesArbitrary) -> DerivesArbitrary { + x + } + fn f_manually_implements_arbitrary( + x: ManuallyImplementsArbitrary, + ) -> ManuallyImplementsArbitrary { + x + } + + fn f_phantom_data(x: PhantomData) -> PhantomData { + x + } + + fn f_phantom_pinned(x: PhantomPinned) -> PhantomPinned { + x + } + + fn empty_body(_x: u8, _y: u16) {} +} + +mod no_harness { + use crate::{DerivesArbitrary, DoesntImplementArbitrary}; + fn unsupported_generic(x: u32, _y: T) -> u32 { + x + } + fn unsupported_ref(x: u32, _y: &i32) -> u32 { + x + } + fn unsupported_const_pointer(x: u32, _y: *const i32) -> u32 { + x + } + fn unsupported_mut_pointer(x: u32, _y: *mut i32) -> u32 { + x + } + fn unsupported_vec(x: u32, _y: Vec) -> u32 { + x + } + fn unsupported_slice(x: u32, _y: &[u8]) -> u32 { + x + } + fn doesnt_implement_arbitrary( + x: DoesntImplementArbitrary, + _y: DerivesArbitrary, + ) -> DoesntImplementArbitrary { + x + } +} diff --git a/tests/script-based-pre/cargo_autoharness_harnesses_fail/Cargo.toml b/tests/script-based-pre/cargo_autoharness_harnesses_fail/Cargo.toml new file mode 100644 index 000000000000..948b9e1666a4 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_harnesses_fail/Cargo.toml @@ -0,0 +1,10 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "cargo_autoharness_harnesses_fail" +version = "0.1.0" +edition = "2024" + +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } diff --git a/tests/script-based-pre/cargo_autoharness_harnesses_fail/config.yml b/tests/script-based-pre/cargo_autoharness_harnesses_fail/config.yml new file mode 100644 index 000000000000..f5b3400d03bf --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_harnesses_fail/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: harnesses_fail.sh +expected: harnesses_fail.expected diff --git a/tests/script-based-pre/cargo_autoharness_harnesses_fail/harnesses_fail.expected b/tests/script-based-pre/cargo_autoharness_harnesses_fail/harnesses_fail.expected new file mode 100644 index 000000000000..7ceed3cc019a --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_harnesses_fail/harnesses_fail.expected @@ -0,0 +1,57 @@ +Autoharness: Checking function panic against all possible inputs... +panic.assertion\ + - Status: FAILURE\ + - Description: "explicit panic" + +Autoharness: Checking function integer_overflow against all possible inputs... +assertion\ + - Status: FAILURE + - Description: "attempt to add with overflow" + +Autoharness: Checking function oob_unsafe_array_access against all possible inputs... +oob_unsafe_array_access.pointer_dereference\ + - Status: FAILURE\ + - Description: "dereference failure: pointer outside object bounds" + +Autoharness: Checking function oob_safe_array_access against all possible inputs... +assertion\ + - Status: FAILURE\ + - Description: "index out of bounds: the length is less than or equal to the given index" + +Autoharness: Checking function unchecked_mul against all possible inputs... +arithmetic_overflow\ + - Status: FAILURE\ + - Description: "attempt to compute `unchecked_mul` which would overflow" + +Verification failed for - panic +Verification failed for - integer_overflow +Verification failed for - oob_unsafe_array_access +Verification failed for - oob_safe_array_access +Verification failed for - unchecked_mul +Complete - 0 successfully verified functions, 5 failures, 5 total. + +Checking harness panic_harness... +panic.assertion\ + - Status: FAILURE\ + - Description: "explicit panic" + +Checking harness integer_overflow_harness... +assertion\ + - Status: FAILURE\ + - Description: "attempt to add with overflow" + +Checking harness oob_unsafe_array_access_harness... +oob_unsafe_array_access.pointer_dereference\ + - Status: FAILURE\ + +Checking harness oob_safe_array_access_harness... +assertion\ + - Status: FAILURE\ + - Description: "index out of bounds: the length is less than or equal to the given index" + +Checking harness unchecked_mul_harness... +arithmetic_overflow\ + - Status: FAILURE\ + - Description: "attempt to compute `unchecked_mul` which would overflow" + +Complete - 0 successfully verified harnesses, 5 failures, 5 total. diff --git a/tests/script-based-pre/cargo_autoharness_harnesses_fail/harnesses_fail.sh b/tests/script-based-pre/cargo_autoharness_harnesses_fail/harnesses_fail.sh new file mode 100755 index 000000000000..b34d3203311f --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_harnesses_fail/harnesses_fail.sh @@ -0,0 +1,9 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +cargo kani autoharness -Z unstable-options +# We expect verification to fail, so the above command will produce an exit status of 1 +# However, we don't want the test to fail because of that exit status; we only want it to fail if the expected file doesn't match +# So, exit with a status code of 0 explicitly. +exit 0; diff --git a/tests/script-based-pre/cargo_autoharness_harnesses_fail/src/lib.rs b/tests/script-based-pre/cargo_autoharness_harnesses_fail/src/lib.rs new file mode 100644 index 000000000000..591c6b92ee5e --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_harnesses_fail/src/lib.rs @@ -0,0 +1,68 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Test the bodies of the automatically generated harnesses: +// do they catch the same failures as manual ones? +// Note that this also indirectly tests that the automatic harness +// subcommand also runs the manual harnesses in the crate. + +fn oob_safe_array_access(idx: usize) { + let v = vec![1, 2, 3]; + v[idx]; +} + +fn oob_unsafe_array_access(i: usize) -> u32 { + let a: &[u32] = &[1, 2, 3]; + if a.len() == 0 { + return 0; + } + return unsafe { *a.as_ptr().add(i % a.len() + 1) }; +} + +fn integer_overflow(x: i32) -> i32 { + if x <= i32::MAX - 100 { + let add_num = |mut x: i32, z: i64| x += z as i32; + add_num(x, 1); + // overflow + add_num(x, 101); + } + x +} + +fn panic() { + if kani::any() { + panic!(); + } +} + +// Test that we can autoharness functions for unsafe functions +unsafe fn unchecked_mul(left: u8, rhs: u8) -> u8 { + left.unchecked_mul(rhs) +} + +#[kani::proof] +fn oob_safe_array_access_harness() { + oob_safe_array_access(kani::any()); +} + +#[kani::proof] +fn oob_unsafe_array_access_harness() { + oob_unsafe_array_access(kani::any()); +} + +#[kani::proof] +fn integer_overflow_harness() { + integer_overflow(kani::any()); +} + +#[kani::proof] +fn panic_harness() { + panic(); +} + +#[kani::proof] +fn unchecked_mul_harness() { + unsafe { + unchecked_mul(kani::any(), kani::any()); + } +} diff --git a/tests/script-based-pre/cargo_autoharness_include/Cargo.toml b/tests/script-based-pre/cargo_autoharness_include/Cargo.toml new file mode 100644 index 000000000000..cceaa1bb7651 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_include/Cargo.toml @@ -0,0 +1,10 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "cargo_autoharness_include" +version = "0.1.0" +edition = "2024" + +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } diff --git a/tests/script-based-pre/cargo_autoharness_include/config.yml b/tests/script-based-pre/cargo_autoharness_include/config.yml new file mode 100644 index 000000000000..8df48ec69865 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_include/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: include.sh +expected: include.expected diff --git a/tests/script-based-pre/cargo_autoharness_include/include.expected b/tests/script-based-pre/cargo_autoharness_include/include.expected new file mode 100644 index 000000000000..91d9eb4c399a --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_include/include.expected @@ -0,0 +1,4 @@ +Autoharness: Checking function include::simple against all possible inputs... +VERIFICATION:- SUCCESSFUL +Verification succeeded for - include::simple +Complete - 1 successfully verified functions, 0 failures, 1 total. \ No newline at end of file diff --git a/tests/script-based-pre/cargo_autoharness_include/include.sh b/tests/script-based-pre/cargo_autoharness_include/include.sh new file mode 100755 index 000000000000..1b3fcc285c88 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_include/include.sh @@ -0,0 +1,5 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +cargo kani autoharness -Z unstable-options --include-function include diff --git a/tests/script-based-pre/cargo_autoharness_include/src/lib.rs b/tests/script-based-pre/cargo_autoharness_include/src/lib.rs new file mode 100644 index 000000000000..68b30bf7afe8 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_include/src/lib.rs @@ -0,0 +1,24 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Test that the automatic harness generation feature selects functions correctly +// when --include-function is provided. + +// Each function inside this module matches the filter. +mod include { + fn simple(x: u8, _y: u16) -> u8 { + x + } + + // Doesn't implement Arbitrary, so still should not be included. + fn generic(x: u32, _y: T) -> u32 { + x + } +} + +// These functions are eligible for autoverification, but do not match the filter. +mod excluded { + fn simple(x: u8, _y: u16) -> u8 { + x + } +} diff --git a/tests/script-based-pre/cargo_autoharness_loops_fixme/Cargo.toml b/tests/script-based-pre/cargo_autoharness_loops_fixme/Cargo.toml new file mode 100644 index 000000000000..57d8cd0f0541 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_loops_fixme/Cargo.toml @@ -0,0 +1,10 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "cargo_autoharness_loops_fixme" +version = "0.1.0" +edition = "2024" + +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } diff --git a/tests/script-based-pre/cargo_autoharness_loops_fixme/config.yml b/tests/script-based-pre/cargo_autoharness_loops_fixme/config.yml new file mode 100644 index 000000000000..fefb50875c7a --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_loops_fixme/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: loops.sh +expected: loops.expected diff --git a/tests/script-based-pre/cargo_autoharness_loops_fixme/loops.expected b/tests/script-based-pre/cargo_autoharness_loops_fixme/loops.expected new file mode 100644 index 000000000000..4c43332f6db0 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_loops_fixme/loops.expected @@ -0,0 +1 @@ +It's not yet clear what the ideal output is for this test, so this expected file is just a placeholder. \ No newline at end of file diff --git a/tests/script-based-pre/cargo_autoharness_loops_fixme/loops.sh b/tests/script-based-pre/cargo_autoharness_loops_fixme/loops.sh new file mode 100755 index 000000000000..cec2f2e2a10b --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_loops_fixme/loops.sh @@ -0,0 +1,5 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +cargo kani autoharness -Z unstable-options diff --git a/tests/script-based-pre/cargo_autoharness_loops_fixme/src/lib.rs b/tests/script-based-pre/cargo_autoharness_loops_fixme/src/lib.rs new file mode 100644 index 000000000000..99ba72445b6d --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_loops_fixme/src/lib.rs @@ -0,0 +1,39 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Test that automatic harnesses terminate on functions with loops. + +// Since foo()'s arguments implement Arbitrary, we will attempt to verify it, +// and enter an infinite loop. +// Unclear what the best solution to this problem is; perhaps this is just a known limitation +// and the user needs to specify some command line flag to skip this function, +// or we can conservatively skip functions with loops that don't have loop contracts. +fn infinite_loop() { + loop {} +} + +/// Euclid's algorithm for calculating the GCD of two numbers +#[kani::requires(x != 0 && y != 0)] +#[kani::ensures(|result : &u8| *result != 0 && x % *result == 0 && y % *result == 0)] +fn gcd(mut x: u8, mut y: u8) -> u8 { + (x, y) = (if x > y { x } else { y }, if x > y { y } else { x }); + loop { + let res = x % y; + if res == 0 { + return y; + } + + x = y; + y = res; + } +} + +// Since we can specify an unwinding bound in a manual harness, +// the proof will terminate. +// Automatic harnesses, however, do not support unwinding bounds, +// so the proof does not terminate. +#[kani::proof_for_contract(gcd)] +#[kani::unwind(12)] +fn gcd_harness() { + gcd(kani::any(), kani::any()); +} diff --git a/tests/script-based-pre/playback_already_existing/original.rs b/tests/script-based-pre/playback_already_existing/original.rs index c6fb819519df..951441ff6324 100644 --- a/tests/script-based-pre/playback_already_existing/original.rs +++ b/tests/script-based-pre/playback_already_existing/original.rs @@ -25,7 +25,7 @@ mod verify { } } #[test] - fn kani_concrete_playback_try_nz_u8_17663051139329126359() { + fn kani_concrete_playback_try_nz_u8_1592364891838466833() { let concrete_vals: Vec> = vec![ // 0 vec![0], diff --git a/tests/script-based-pre/playback_array/array.rs b/tests/script-based-pre/playback_array/array.rs new file mode 100644 index 000000000000..8168b2a2da50 --- /dev/null +++ b/tests/script-based-pre/playback_array/array.rs @@ -0,0 +1,16 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Test that concrete playback generates concrete values for arrays over the length of 64 +//! and that playback can run those tests and find the index out of bounds bug, +//! c.f. https://github.com/model-checking/kani/issues/3787 + +#[cfg(kani)] +mod verify { + #[kani::proof] + fn index_array_65() { + let arr: [u16; 65] = kani::any(); + let idx: usize = kani::any(); + arr[idx]; + } +} diff --git a/tests/script-based-pre/playback_array/config.yml b/tests/script-based-pre/playback_array/config.yml new file mode 100644 index 000000000000..88b420e8a6f0 --- /dev/null +++ b/tests/script-based-pre/playback_array/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: playback_array.sh +expected: playback_array.expected diff --git a/tests/script-based-pre/playback_array/playback_array.expected b/tests/script-based-pre/playback_array/playback_array.expected new file mode 100644 index 000000000000..ef1ffa7f2f93 --- /dev/null +++ b/tests/script-based-pre/playback_array/playback_array.expected @@ -0,0 +1,9 @@ +Failed Checks: index out of bounds: the length is less than or equal to the given index + +VERIFICATION:- FAILED + +INFO: Now modifying the source code to include the concrete playback unit test: + +running 1 test + +index out of bounds: the len is 65 but the index is \ No newline at end of file diff --git a/tests/script-based-pre/playback_array/playback_array.sh b/tests/script-based-pre/playback_array/playback_array.sh new file mode 100755 index 000000000000..3cceb8da6297 --- /dev/null +++ b/tests/script-based-pre/playback_array/playback_array.sh @@ -0,0 +1,22 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +set -e +set -o pipefail +set -o nounset + +cleanup() +{ + rm ${RS_FILE} +} +trap cleanup EXIT + +RS_FILE="modified.rs" +cp array.rs ${RS_FILE} + +echo "[TEST] Generate test..." +kani ${RS_FILE} -Z concrete-playback --concrete-playback=inplace || true + +echo "[TEST] Run test..." +kani playback -Z concrete-playback ${RS_FILE} || true diff --git a/tests/ui/cbmc_checks/float-overflow/expected b/tests/ui/cbmc_checks/float-overflow/check_message.expected similarity index 100% rename from tests/ui/cbmc_checks/float-overflow/expected rename to tests/ui/cbmc_checks/float-overflow/check_message.expected diff --git a/tests/ui/cbmc_checks/float-overflow/check_message.rs b/tests/ui/cbmc_checks/float-overflow/check_message.rs index 590a2be20230..229bc373a883 100644 --- a/tests/ui/cbmc_checks/float-overflow/check_message.rs +++ b/tests/ui/cbmc_checks/float-overflow/check_message.rs @@ -1,6 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // +// kani-flags: --enable-unstable --cbmc-args --float-overflow-check // Check we don't print temporary variables as part of CBMC messages. extern crate kani; diff --git a/tests/ui/cbmc_checks/float-overflow/check_message_overflow.expected b/tests/ui/cbmc_checks/float-overflow/check_message_overflow.expected new file mode 100644 index 000000000000..880f00714b32 --- /dev/null +++ b/tests/ui/cbmc_checks/float-overflow/check_message_overflow.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL \ No newline at end of file diff --git a/tests/ui/cbmc_checks/float-overflow/check_message_overflow.rs b/tests/ui/cbmc_checks/float-overflow/check_message_overflow.rs new file mode 100644 index 000000000000..5b57e4b4377d --- /dev/null +++ b/tests/ui/cbmc_checks/float-overflow/check_message_overflow.rs @@ -0,0 +1,22 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// This test verifies that Kani does not report floating-point overflow by default +// for operations that result in +/-Infinity. +extern crate kani; + +// Use the result so rustc doesn't optimize them away. +fn dummy(result: f32) -> f32 { + result +} + +#[kani::proof] +fn main() { + let a = kani::any_where(|&x: &f32| x.is_finite()); + let b = kani::any_where(|&x: &f32| x.is_finite()); + + dummy(a + b); + dummy(a - b); + dummy(a * b); + dummy(-a); +} diff --git a/tests/ui/multiple-harnesses/stop_at_single_fail/fail_fast_test.expected b/tests/ui/multiple-harnesses/stop_at_single_fail/fail_fast_test.expected new file mode 100644 index 000000000000..4bb591a9a72d --- /dev/null +++ b/tests/ui/multiple-harnesses/stop_at_single_fail/fail_fast_test.expected @@ -0,0 +1 @@ +Complete - 0 successfully verified harnesses, 1 failures, 1 total. \ No newline at end of file diff --git a/tests/ui/multiple-harnesses/stop_at_single_fail/fail_fast_test.rs b/tests/ui/multiple-harnesses/stop_at_single_fail/fail_fast_test.rs new file mode 100644 index 000000000000..9ac9a22204b5 --- /dev/null +++ b/tests/ui/multiple-harnesses/stop_at_single_fail/fail_fast_test.rs @@ -0,0 +1,26 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --fail-fast +//! Ensure that the verification process stops as soon as one of the harnesses fails. + +mod tests { + #[kani::proof] + fn test_01_fail() { + assert!(false, "First failure"); + } + + #[kani::proof] + fn test_02_fail() { + assert!(false, "Second failure"); + } + + #[kani::proof] + fn test_03_fail() { + assert!(false, "Third failure"); + } + + #[kani::proof] + fn test_04_fail() { + assert!(false, "Fourth failure"); + } +} diff --git a/tests/ui/multiple-harnesses/stop_at_single_fail/fail_fast_test_parallel.expected b/tests/ui/multiple-harnesses/stop_at_single_fail/fail_fast_test_parallel.expected new file mode 100644 index 000000000000..4bb591a9a72d --- /dev/null +++ b/tests/ui/multiple-harnesses/stop_at_single_fail/fail_fast_test_parallel.expected @@ -0,0 +1 @@ +Complete - 0 successfully verified harnesses, 1 failures, 1 total. \ No newline at end of file diff --git a/tests/ui/multiple-harnesses/stop_at_single_fail/fail_fast_test_parallel.rs b/tests/ui/multiple-harnesses/stop_at_single_fail/fail_fast_test_parallel.rs new file mode 100644 index 000000000000..db2535777a26 --- /dev/null +++ b/tests/ui/multiple-harnesses/stop_at_single_fail/fail_fast_test_parallel.rs @@ -0,0 +1,57 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --fail-fast -Z unstable-options --jobs 4 --output-format=terse +//! Ensure that the verification process stops as soon as one of the harnesses fails. +//! This test runs on 4 parallel threads. Stops verification as soon as a harness on any of the threads fails. + +mod tests { + #[kani::proof] + fn test_01_fail() { + assert!(false, "First failure"); + } + + #[kani::proof] + fn test_02_fail() { + assert!(false, "Second failure"); + } + + #[kani::proof] + fn test_03_fail() { + assert!(false, "Third failure"); + } + + #[kani::proof] + fn test_04_fail() { + assert!(false, "Fourth failure"); + } + + #[kani::proof] + fn test_05_fail() { + assert!(false, "Fifth failure"); + } + + #[kani::proof] + fn test_06_fail() { + assert!(false, "Sixth failure"); + } + + #[kani::proof] + fn test_07_fail() { + assert!(false, "Seventh failure"); + } + + #[kani::proof] + fn test_08_fail() { + assert!(false, "Eighth failure"); + } + + #[kani::proof] + fn test_09_fail() { + assert!(false, "Ninth failure"); + } + + #[kani::proof] + fn test_10_fail() { + assert!(false, "Tenth failure"); + } +} diff --git a/tools/build-kani/Cargo.toml b/tools/build-kani/Cargo.toml index fb862e3d8507..8d837a9b0e3f 100644 --- a/tools/build-kani/Cargo.toml +++ b/tools/build-kani/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "build-kani" -version = "0.58.0" +version = "0.59.0" edition = "2021" description = "Builds Kani, Sysroot and release bundle." license = "MIT OR Apache-2.0" diff --git a/tools/build-kani/src/main.rs b/tools/build-kani/src/main.rs index c45e9a72b189..3ff017e37509 100644 --- a/tools/build-kani/src/main.rs +++ b/tools/build-kani/src/main.rs @@ -138,7 +138,6 @@ fn bundle_cbmc(dir: &Path) -> Result<()> { cp(&which::which("cbmc")?, &bin)?; cp(&which::which("goto-instrument")?, &bin)?; cp(&which::which("goto-cc")?, &bin)?; - cp(&which::which("symtab2gb")?, &bin)?; cp(&which::which("goto-analyzer")?, &bin)?; Ok(()) diff --git a/tools/kani-cov/src/report.rs b/tools/kani-cov/src/report.rs index 95eba4d252ee..398f45fd47cb 100644 --- a/tools/kani-cov/src/report.rs +++ b/tools/kani-cov/src/report.rs @@ -261,7 +261,8 @@ fn insert_escapes(str: &str, markers: Vec<(ColumnNumber, bool)>, format: &Report escaped_str.insert_str(i + offset, b); // `offset` keeps track of the bytes we've already inserted so the original // index is shifted by the appropriate amount in subsequent insertions. - offset += b.bytes().len(); + // Note that b.len() returns the length of the string in bytes, c.f. https://doc.rust-lang.org/std/string/struct.String.html#method.len + offset += b.len(); } escaped_str } diff --git a/tools/kani-cov/src/summary.rs b/tools/kani-cov/src/summary.rs index e56008daade1..f07f4a83afdb 100644 --- a/tools/kani-cov/src/summary.rs +++ b/tools/kani-cov/src/summary.rs @@ -165,9 +165,9 @@ pub fn line_coverage_results( } } } else { - line_status = std::iter::repeat(Some((0, MarkerInfo::FullLine))) - .take(end_line - start_line + 1) - .collect(); + line_status = + std::iter::repeat_n(Some((0, MarkerInfo::FullLine)), end_line - start_line + 1) + .collect(); } line_status }