diff --git a/.github/workflows/deny.yml b/.github/workflows/deny.yml index 7ce00cabd2f9..a5db349f8abc 100644 --- a/.github/workflows/deny.yml +++ b/.github/workflows/deny.yml @@ -18,6 +18,8 @@ jobs: runs-on: ubuntu-latest steps: - uses: actions/checkout@v4 + with: + submodules: recursive - uses: EmbarkStudios/cargo-deny-action@v2 with: arguments: --all-features --workspace diff --git a/.github/workflows/format-check.yml b/.github/workflows/format-check.yml index cc13306a4eaf..81253f1a9790 100644 --- a/.github/workflows/format-check.yml +++ b/.github/workflows/format-check.yml @@ -47,7 +47,7 @@ jobs: - name: 'Run Clippy' run: | - cargo clippy --all -- -D warnings + cargo clippy --workspace --exclude charon --exclude macros --no-deps -- -D warnings - name: 'Print Clippy Statistics' run: | diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index a565c9cd4cbe..d8cb0fc2bb2d 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -98,6 +98,8 @@ jobs: steps: - name: Checkout Kani uses: actions/checkout@v4 + with: + submodules: recursive - name: Install book dependencies run: ./scripts/setup/ubuntu/install_doc_deps.sh diff --git a/.gitignore b/.gitignore index a2defc0df119..db10863e2b0f 100644 --- a/.gitignore +++ b/.gitignore @@ -77,6 +77,9 @@ package-lock.json ## Rustdoc GUI tests tests/rustdoc-gui/src/**.lock +## Charon/Aeneas LLBC files +*.llbc + # Before adding new lines, see the comment at the top. /.ninja_deps /.ninja_log diff --git a/.gitmodules b/.gitmodules index b02c263a898e..c7e25f120c95 100644 --- a/.gitmodules +++ b/.gitmodules @@ -5,3 +5,6 @@ path = tests/perf/s2n-quic url = https://github.com/aws/s2n-quic branch = main +[submodule "charon"] + path = charon + url = https://github.com/AeneasVerif/charon diff --git a/CHANGELOG.md b/CHANGELOG.md index e35af4c8fa24..23d740f534a9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,6 +4,27 @@ 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.56.0] + +### Breaking Changes + +* Remove obsolete linker options (`--mir-linker` and `--legacy-linker`) by @zhassan-aws in https://github.com/model-checking/kani/pull/3559 +* Deprecate `kani::check` by @celinval in https://github.com/model-checking/kani/pull/3557 + +### What's Changed + +* Enable stubbing and function contracts for primitive types by @celinval in https://github.com/model-checking/kani/pull/3496 +* Instrument validity checks for pointer to reference casts for slices and str's by @zhassan-aws in https://github.com/model-checking/kani/pull/3513 +* Fail compilation if `proof_for_contract` is added to generic function by @carolynzech in https://github.com/model-checking/kani/pull/3522 +* Fix storing coverage data in cargo projects by @adpaco-aws in https://github.com/model-checking/kani/pull/3527 +* Add experimental API to generate arbitrary pointers by @celinval in https://github.com/model-checking/kani/pull/3538 +* Running `verify-std` no longer changes Cargo files by @celinval in https://github.com/model-checking/kani/pull/3577 +* Add an LLBC backend by @zhassan-aws in https://github.com/model-checking/kani/pull/3514 +* Rust toolchain upgraded to nightly-2024-10-03 by @qinheping @tautschnig @celinval +* CBMC upgraded to 6.3.1 by @tautschnig in https://github.com/model-checking/kani/pull/3537 + +**Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.55.0...kani-0.56.0 + ## [0.55.0] ### Major/Breaking Changes diff --git a/Cargo.lock b/Cargo.lock index 42abe00cb6dc..580cdf70946a 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -79,6 +79,34 @@ version = "1.0.89" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "86fdf8605db99b54d3cd748a44c6d04df638eb5dafb219b135d0149bd0db01f6" +[[package]] +name = "arrayvec" +version = "0.5.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "23b62fc65de8e4e7f52534fb52b0f3ed04746ae267519eef2a83941e8085068b" + +[[package]] +name = "arrayvec" +version = "0.7.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7c02d123df017efcdfbd739ef81735b36c5ba83ec3c59c80a9d7ecc718f92e50" + +[[package]] +name = "assert_cmd" +version = "2.0.16" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "dc1835b7f27878de8525dc71410b5a31cdcc5f230aed5ba5df968e09c201b23d" +dependencies = [ + "anstyle", + "bstr", + "doc-comment", + "libc", + "predicates", + "predicates-core", + "predicates-tree", + "wait-timeout", +] + [[package]] name = "autocfg" version = "1.4.0" @@ -91,9 +119,38 @@ version = "2.6.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b048fb63fd8b5923fc5aa7b340d8e156aec7ec02f0c78fa8a6ddc2613f6f71de" +[[package]] +name = "bitmaps" +version = "2.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "031043d04099746d8db04daf1fa424b2bc8bd69d92b25962dcde24da39ab64a2" +dependencies = [ + "typenum", +] + +[[package]] +name = "brownstone" +version = "3.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c5839ee4f953e811bfdcf223f509cb2c6a3e1447959b0bff459405575bc17f22" +dependencies = [ + "arrayvec 0.7.6", +] + +[[package]] +name = "bstr" +version = "1.10.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "40723b8fb387abc38f4f4a37c09073622e41dd12327033091ef8950659e6dc0c" +dependencies = [ + "memchr", + "regex-automata 0.4.8", + "serde", +] + [[package]] name = "build-kani" -version = "0.55.0" +version = "0.56.0" dependencies = [ "anyhow", "cargo_metadata", @@ -139,17 +196,65 @@ dependencies = [ "thiserror", ] +[[package]] +name = "cc" +version = "1.1.28" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2e80e3b6a3ab07840e1cae9b0666a63970dc28e8ed5ffbcdacbfc760c281bfc1" +dependencies = [ + "shlex", +] + [[package]] name = "cfg-if" version = "1.0.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" +[[package]] +name = "charon" +version = "0.1.36" +dependencies = [ + "anyhow", + "assert_cmd", + "clap", + "colored", + "convert_case 0.6.0", + "derivative", + "derive-visitor", + "env_logger", + "hashlink", + "im", + "index_vec", + "indoc", + "itertools 0.13.0", + "lazy_static", + "log", + "macros", + "nom", + "nom-supreme", + "petgraph", + "pretty", + "regex", + "rustc_version", + "serde", + "serde-map-to-array", + "serde_json", + "serde_stacker", + "stacker", + "take_mut", + "toml", + "tracing", + "tracing-subscriber", + "tracing-tree 0.3.1", + "which", +] + [[package]] name = "clap" -version = "4.5.18" +version = "4.5.19" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b0956a43b323ac1afaffc053ed5c4b7c1f1800bacd1683c353aabbb752515dd3" +checksum = "7be5744db7978a28d9df86a214130d106a89ce49644cbc4e3f0c22c3fba30615" dependencies = [ "clap_builder", "clap_derive", @@ -157,9 +262,9 @@ dependencies = [ [[package]] name = "clap_builder" -version = "4.5.18" +version = "4.5.19" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4d72166dd41634086d5803a47eb71ae740e61d84709c36f3c34110173db3961b" +checksum = "a5fbc17d3ef8278f55b282b2a2e75ae6f6c7d4bb70ed3d0382375104bfafdb4b" dependencies = [ "anstream", "anstyle", @@ -176,7 +281,7 @@ dependencies = [ "heck", "proc-macro2", "quote", - "syn", + "syn 2.0.79", ] [[package]] @@ -191,6 +296,16 @@ version = "1.0.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d3fd119d74b830634cea2a0f58bbd0d54540518a14397557951e79340abc28c0" +[[package]] +name = "colored" +version = "2.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cbf2150cce219b664a8a70df7a1f933836724b503f8a413af9365b4dcc4d90b8" +dependencies = [ + "lazy_static", + "windows-sys 0.48.0", +] + [[package]] name = "colour" version = "2.1.0" @@ -242,9 +357,24 @@ dependencies = [ "windows-sys 0.52.0", ] +[[package]] +name = "convert_case" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6245d59a3e82a7fc217c5828a6692dbc6dfb63a0c8c90495621f7b9d79704a0e" + +[[package]] +name = "convert_case" +version = "0.6.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ec182b0ca2f35d8fc196cf3404988fd8b8c739a4d270ff118a398feb0cbec1ca" +dependencies = [ + "unicode-segmentation", +] + [[package]] name = "cprover_bindings" -version = "0.55.0" +version = "0.56.0" dependencies = [ "lazy_static", "linear-map", @@ -334,6 +464,51 @@ dependencies = [ "powerfmt", ] +[[package]] +name = "derivative" +version = "2.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "fcc3dd5e9e9c0b295d6e1e4d811fb6f157d5ffd784b8d202fc62eac8035a770b" +dependencies = [ + "proc-macro2", + "quote", + "syn 1.0.109", +] + +[[package]] +name = "derive-visitor" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d47165df83b9707cbada3216607a5d66125b6a66906de0bc1216c0669767ca9e" +dependencies = [ + "derive-visitor-macros", +] + +[[package]] +name = "derive-visitor-macros" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "427b39a85fecafea16b1a5f3f50437151022e35eb4fe038107f08adbf7f8def6" +dependencies = [ + "convert_case 0.4.0", + "itertools 0.10.5", + "proc-macro2", + "quote", + "syn 1.0.109", +] + +[[package]] +name = "difflib" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6184e33543162437515c2e2b48714794e37845ec9851711914eec9d308f6ebe8" + +[[package]] +name = "doc-comment" +version = "0.3.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "fea41bba32d969b513997752735605054bc0dfa92b4c56bf1189f2e174be7a10" + [[package]] name = "either" version = "1.13.0" @@ -346,6 +521,29 @@ version = "0.3.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "a357d28ed41a50f9c765dbfe56cbc04a64e53e5fc58ba79fbc34c10ef3df831f" +[[package]] +name = "env_filter" +version = "0.1.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4f2c92ceda6ceec50f43169f9ee8424fe2db276791afde7b2cd8bc084cb376ab" +dependencies = [ + "log", + "regex", +] + +[[package]] +name = "env_logger" +version = "0.11.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e13fa619b91fb2381732789fc5de83b45675e882f66623b7d8cb4f643017018d" +dependencies = [ + "anstream", + "anstyle", + "env_filter", + "humantime", + "log", +] + [[package]] name = "equivalent" version = "1.0.1" @@ -420,6 +618,22 @@ dependencies = [ "ahash", ] +[[package]] +name = "hashbrown" +version = "0.15.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1e087f84d4f86bf4b218b927129862374b72199ae7d8657835f1e89000eea4fb" + +[[package]] +name = "hashlink" +version = "0.9.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6ba4ff7128dee98c7dc9794b6a411377e1404dba1c97deb8d1a55297bd25d8af" +dependencies = [ + "hashbrown 0.14.5", + "serde", +] + [[package]] name = "heck" version = "0.5.0" @@ -435,22 +649,72 @@ dependencies = [ "windows-sys 0.52.0", ] +[[package]] +name = "humantime" +version = "2.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9a3a5bfb195931eeb336b2a7b4d761daec841b97f947d34394601737a7bba5e4" + +[[package]] +name = "im" +version = "15.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d0acd33ff0285af998aaf9b57342af478078f53492322fafc47450e09397e0e9" +dependencies = [ + "bitmaps", + "rand_core", + "rand_xoshiro", + "sized-chunks", + "typenum", + "version_check", +] + +[[package]] +name = "indent_write" +version = "2.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0cfe9645a18782869361d9c8732246be7b410ad4e919d3609ebabdac00ba12c3" + +[[package]] +name = "index_vec" +version = "0.1.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "44faf5bb8861a9c72e20d3fb0fdbd59233e43056e2b80475ab0aacdc2e781355" +dependencies = [ + "serde", +] + [[package]] name = "indexmap" -version = "2.5.0" +version = "2.6.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "68b900aa2f7301e21c36462b170ee99994de34dff39a4a6a528e80e7376d07e5" +checksum = "707907fe3c25f5424cce2cb7e1cbcafee6bdbe735ca90ef77c29e84591e5b9da" dependencies = [ "equivalent", - "hashbrown", + "hashbrown 0.15.0", ] +[[package]] +name = "indoc" +version = "2.0.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b248f5224d1d606005e02c97f5aa4e88eeb230488bcc03bc9ca4d7991399f2b5" + [[package]] name = "is_terminal_polyfill" version = "1.70.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "7943c866cc5cd64cbc25b2e01621d07fa8eb2a1a23160ee81ce38704e97b8ecf" +[[package]] +name = "itertools" +version = "0.10.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b0fd2260e829bddf4cb6ea802289de2f86d6a7a690192fbe91b3f46e0f2c8473" +dependencies = [ + "either", +] + [[package]] name = "itertools" version = "0.13.0" @@ -466,9 +730,15 @@ version = "1.0.11" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "49f1f14873335454500d59611f1cf4a4b0f786f9ac11f4312a78e4cf2566695b" +[[package]] +name = "joinery" +version = "2.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "72167d68f5fce3b8655487b8038691a3c9984ee769590f93f2a631f4ad64e4f5" + [[package]] name = "kani" -version = "0.55.0" +version = "0.56.0" dependencies = [ "kani_core", "kani_macros", @@ -476,12 +746,13 @@ dependencies = [ [[package]] name = "kani-compiler" -version = "0.55.0" +version = "0.56.0" dependencies = [ + "charon", "clap", "cprover_bindings", "home", - "itertools", + "itertools 0.13.0", "kani_metadata", "lazy_static", "num", @@ -492,15 +763,15 @@ dependencies = [ "shell-words", "strum", "strum_macros", - "syn", + "syn 2.0.79", "tracing", "tracing-subscriber", - "tracing-tree", + "tracing-tree 0.4.0", ] [[package]] name = "kani-driver" -version = "0.55.0" +version = "0.56.0" dependencies = [ "anyhow", "cargo_metadata", @@ -530,7 +801,7 @@ dependencies = [ [[package]] name = "kani-verifier" -version = "0.55.0" +version = "0.56.0" dependencies = [ "anyhow", "home", @@ -539,24 +810,24 @@ dependencies = [ [[package]] name = "kani_core" -version = "0.55.0" +version = "0.56.0" dependencies = [ "kani_macros", ] [[package]] name = "kani_macros" -version = "0.55.0" +version = "0.56.0" dependencies = [ "proc-macro-error2", "proc-macro2", "quote", - "syn", + "syn 2.0.79", ] [[package]] name = "kani_metadata" -version = "0.55.0" +version = "0.56.0" dependencies = [ "clap", "cprover_bindings", @@ -609,6 +880,15 @@ version = "0.4.22" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "a7a70ba024b9dc04c27ea2f0c0548feb474ec5c54bba33a7f72f873a39d07b24" +[[package]] +name = "macros" +version = "0.1.0" +dependencies = [ + "proc-macro2", + "quote", + "syn 2.0.79", +] + [[package]] name = "matchers" version = "0.1.0" @@ -630,6 +910,35 @@ version = "0.2.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "2145869435ace5ea6ea3d35f59be559317ec9a0d04e1812d5f185a87b6d36f1a" +[[package]] +name = "minimal-lexical" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "68354c5c6bd36d73ff3feceb05efa59b6acb7626617f4962be322a825e61f79a" + +[[package]] +name = "nom" +version = "7.1.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d273983c5a657a70a3e8f2a01329822f3b8c8172b73826411a55751e404a0a4a" +dependencies = [ + "memchr", + "minimal-lexical", +] + +[[package]] +name = "nom-supreme" +version = "0.8.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2bd3ae6c901f1959588759ff51c95d24b491ecb9ff91aa9c2ef4acc5b1dcab27" +dependencies = [ + "brownstone", + "indent_write", + "joinery", + "memchr", + "nom", +] + [[package]] name = "nu-ansi-term" version = "0.46.0" @@ -730,12 +1039,9 @@ dependencies = [ [[package]] name = "once_cell" -version = "1.20.1" +version = "1.20.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "82881c4be219ab5faaf2ad5e5e5ecdff8c66bd7402ca3160975c93b24961afd1" -dependencies = [ - "portable-atomic", -] +checksum = "1261fe7e33c73b354eab43b1273a57c8f967d0391e80353e51f764ac02cf6775" [[package]] name = "os_info" @@ -773,7 +1079,7 @@ dependencies = [ "libc", "redox_syscall", "smallvec", - "windows-targets", + "windows-targets 0.52.6", ] [[package]] @@ -798,12 +1104,6 @@ version = "0.2.14" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "bda66fc9667c18cb2758a2ac84d1167245054bcf85d5d1aaa6923f45801bdd02" -[[package]] -name = "portable-atomic" -version = "1.9.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "cc9c68a3f6da06753e9335d63e27f6b9754dd1920d941135b7ea8224f141adb2" - [[package]] name = "powerfmt" version = "0.2.0" @@ -819,6 +1119,44 @@ dependencies = [ "zerocopy", ] +[[package]] +name = "predicates" +version = "3.1.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7e9086cc7640c29a356d1a29fd134380bee9d8f79a17410aa76e7ad295f42c97" +dependencies = [ + "anstyle", + "difflib", + "predicates-core", +] + +[[package]] +name = "predicates-core" +version = "1.0.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ae8177bee8e75d6846599c6b9ff679ed51e882816914eec639944d7c9aa11931" + +[[package]] +name = "predicates-tree" +version = "1.0.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "41b740d195ed3166cd147c8047ec98db0e22ec019eb8eeb76d343b795304fb13" +dependencies = [ + "predicates-core", + "termtree", +] + +[[package]] +name = "pretty" +version = "0.12.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b55c4d17d994b637e2f4daf6e5dc5d660d209d5642377d675d7a1c3ab69fa579" +dependencies = [ + "arrayvec 0.5.2", + "typed-arena", + "unicode-width", +] + [[package]] name = "proc-macro-error-attr2" version = "2.0.0" @@ -838,7 +1176,7 @@ dependencies = [ "proc-macro-error-attr2", "proc-macro2", "quote", - "syn", + "syn 2.0.79", ] [[package]] @@ -850,6 +1188,15 @@ dependencies = [ "unicode-ident", ] +[[package]] +name = "psm" +version = "0.1.23" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "aa37f80ca58604976033fae9515a8a2989fc13797d953f7c04fb8fa36a11f205" +dependencies = [ + "cc", +] + [[package]] name = "quote" version = "1.0.37" @@ -889,6 +1236,15 @@ dependencies = [ "getrandom", ] +[[package]] +name = "rand_xoshiro" +version = "0.6.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6f97cdb2a36ed4183de61b2f824cc45c9f1037f28afe0a322e9fff4c108b5aaa" +dependencies = [ + "rand_core", +] + [[package]] name = "rayon" version = "1.10.0" @@ -911,9 +1267,9 @@ dependencies = [ [[package]] name = "redox_syscall" -version = "0.5.6" +version = "0.5.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "355ae415ccd3a04315d3f8246e86d67689ea74d88d915576e1589a351062a13b" +checksum = "9b6dfecf2c74bce2466cabf93f6664d6998a69eb21e39f4207930065b27b771f" dependencies = [ "bitflags", ] @@ -968,6 +1324,15 @@ version = "0.1.24" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "719b953e2095829ee67db738b3bfa9fa368c94900df327b3f07fe6e794d2fe1f" +[[package]] +name = "rustc_version" +version = "0.4.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cfcb3a22ef46e85b45de6ee7e79d063319ebb6594faafcf1c225ea92ab6e9b92" +dependencies = [ + "semver", +] + [[package]] name = "rustix" version = "0.38.37" @@ -1038,6 +1403,15 @@ dependencies = [ "serde_derive", ] +[[package]] +name = "serde-map-to-array" +version = "1.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c14b52efc56c711e0dbae3f26e0cc233f5dac336c1bf0b07e1b7dc2dca3b2cc7" +dependencies = [ + "serde", +] + [[package]] name = "serde_derive" version = "1.0.210" @@ -1046,7 +1420,7 @@ checksum = "243902eda00fad750862fc144cea25caca5e20d615af0a81bee94ca738f1df1f" dependencies = [ "proc-macro2", "quote", - "syn", + "syn 2.0.79", ] [[package]] @@ -1071,6 +1445,16 @@ dependencies = [ "serde", ] +[[package]] +name = "serde_stacker" +version = "0.1.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "babfccff5773ff80657f0ecf553c7c516bdc2eb16389c0918b36b73e7015276e" +dependencies = [ + "serde", + "stacker", +] + [[package]] name = "serde_test" version = "1.0.177" @@ -1108,15 +1492,44 @@ version = "1.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "24188a676b6ae68c3b2cb3a01be17fbf7240ce009799bb56d5b1409051e78fde" +[[package]] +name = "shlex" +version = "1.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0fda2ff0d084019ba4d7c6f371c95d8fd75ce3524c3cb8fb653a3023f6323e64" + +[[package]] +name = "sized-chunks" +version = "0.6.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "16d69225bde7a69b235da73377861095455d298f2b970996eec25ddbb42b3d1e" +dependencies = [ + "bitmaps", + "typenum", +] + [[package]] name = "smallvec" version = "1.13.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "3c5e1a9a646d36c3599cd173a41282daf47c44583ad367b8e6837255952e5c67" +[[package]] +name = "stacker" +version = "0.1.17" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "799c883d55abdb5e98af1a7b3f23b9b6de8ecada0ecac058672d7635eb48ca7b" +dependencies = [ + "cc", + "cfg-if", + "libc", + "psm", + "windows-sys 0.59.0", +] + [[package]] name = "std" -version = "0.55.0" +version = "0.56.0" dependencies = [ "kani", ] @@ -1128,7 +1541,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "1c6a0d765f5807e98a091107bae0a56ea3799f66a5de47b2c84c94a39c09974e" dependencies = [ "cfg-if", - "hashbrown", + "hashbrown 0.14.5", "serde", ] @@ -1154,7 +1567,18 @@ dependencies = [ "proc-macro2", "quote", "rustversion", - "syn", + "syn 2.0.79", +] + +[[package]] +name = "syn" +version = "1.0.109" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", ] [[package]] @@ -1168,6 +1592,12 @@ dependencies = [ "unicode-ident", ] +[[package]] +name = "take_mut" +version = "0.2.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f764005d11ee5f36500a149ace24e00e3da98b0158b3e2d53a7495660d3f4d60" + [[package]] name = "tempfile" version = "3.13.0" @@ -1181,6 +1611,12 @@ dependencies = [ "windows-sys 0.59.0", ] +[[package]] +name = "termtree" +version = "0.4.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3369f5ac52d5eb6ab48c6b4ffdc8efbcad6b89c765749064ba298f2c68a16a76" + [[package]] name = "thiserror" version = "1.0.64" @@ -1198,7 +1634,7 @@ checksum = "08904e7672f5eb876eaaf87e0ce17857500934f4981c4a0ab2b4aa98baac7fc3" dependencies = [ "proc-macro2", "quote", - "syn", + "syn 2.0.79", ] [[package]] @@ -1295,7 +1731,7 @@ checksum = "34704c8d6ebcbc939824180af020566b01a7c01f80641264eba0999f6c2b6be7" dependencies = [ "proc-macro2", "quote", - "syn", + "syn 2.0.79", ] [[package]] @@ -1351,6 +1787,18 @@ dependencies = [ "tracing-serde", ] +[[package]] +name = "tracing-tree" +version = "0.3.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b56c62d2c80033cb36fae448730a2f2ef99410fe3ecbffc916681a32f6807dbe" +dependencies = [ + "nu-ansi-term 0.50.1", + "tracing-core", + "tracing-log", + "tracing-subscriber", +] + [[package]] name = "tracing-tree" version = "0.4.0" @@ -1363,12 +1811,30 @@ dependencies = [ "tracing-subscriber", ] +[[package]] +name = "typed-arena" +version = "2.0.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6af6ae20167a9ece4bcb41af5b80f8a1f1df981f6391189ce00fd257af04126a" + +[[package]] +name = "typenum" +version = "1.17.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "42ff0bf0c66b8238c6f3b578df37d0b7848e55df8577b3f74f92a69acceeb825" + [[package]] name = "unicode-ident" version = "1.0.13" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "e91b56cd4cadaeb79bbf1a5645f6b4f8dc5bde8834ad5894a8db35fda9efa1fe" +[[package]] +name = "unicode-segmentation" +version = "1.12.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f6ccf251212114b54433ec949fd6a7841275f9ada20dddd2f29e9ceea4501493" + [[package]] name = "unicode-width" version = "0.1.14" @@ -1467,13 +1933,22 @@ version = "0.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f" +[[package]] +name = "windows-sys" +version = "0.48.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "677d2418bec65e3338edb076e806bc1ec15693c5d0104683f2efe857f61056a9" +dependencies = [ + "windows-targets 0.48.5", +] + [[package]] name = "windows-sys" version = "0.52.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "282be5f36a8ce781fad8c8ae18fa3f9beff57ec1b52cb3de0789201425d9a33d" dependencies = [ - "windows-targets", + "windows-targets 0.52.6", ] [[package]] @@ -1482,7 +1957,22 @@ version = "0.59.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "1e38bc4d79ed67fd075bcc251a1c39b32a1776bbe92e5bef1f0bf1f8c531853b" dependencies = [ - "windows-targets", + "windows-targets 0.52.6", +] + +[[package]] +name = "windows-targets" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9a2fa6e2155d7247be68c096456083145c183cbbbc2764150dda45a87197940c" +dependencies = [ + "windows_aarch64_gnullvm 0.48.5", + "windows_aarch64_msvc 0.48.5", + "windows_i686_gnu 0.48.5", + "windows_i686_msvc 0.48.5", + "windows_x86_64_gnu 0.48.5", + "windows_x86_64_gnullvm 0.48.5", + "windows_x86_64_msvc 0.48.5", ] [[package]] @@ -1491,28 +1981,46 @@ version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9b724f72796e036ab90c1021d4780d4d3d648aca59e491e6b98e725b84e99973" dependencies = [ - "windows_aarch64_gnullvm", - "windows_aarch64_msvc", - "windows_i686_gnu", + "windows_aarch64_gnullvm 0.52.6", + "windows_aarch64_msvc 0.52.6", + "windows_i686_gnu 0.52.6", "windows_i686_gnullvm", - "windows_i686_msvc", - "windows_x86_64_gnu", - "windows_x86_64_gnullvm", - "windows_x86_64_msvc", + "windows_i686_msvc 0.52.6", + "windows_x86_64_gnu 0.52.6", + "windows_x86_64_gnullvm 0.52.6", + "windows_x86_64_msvc 0.52.6", ] +[[package]] +name = "windows_aarch64_gnullvm" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2b38e32f0abccf9987a4e3079dfb67dcd799fb61361e53e2882c3cbaf0d905d8" + [[package]] name = "windows_aarch64_gnullvm" version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "32a4622180e7a0ec044bb555404c800bc9fd9ec262ec147edd5989ccd0c02cd3" +[[package]] +name = "windows_aarch64_msvc" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "dc35310971f3b2dbbf3f0690a219f40e2d9afcf64f9ab7cc1be722937c26b4bc" + [[package]] name = "windows_aarch64_msvc" version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "09ec2a7bb152e2252b53fa7803150007879548bc709c039df7627cabbd05d469" +[[package]] +name = "windows_i686_gnu" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a75915e7def60c94dcef72200b9a8e58e5091744960da64ec734a6c6e9b3743e" + [[package]] name = "windows_i686_gnu" version = "0.52.6" @@ -1525,24 +2033,48 @@ version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0eee52d38c090b3caa76c563b86c3a4bd71ef1a819287c19d586d7334ae8ed66" +[[package]] +name = "windows_i686_msvc" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8f55c233f70c4b27f66c523580f78f1004e8b5a8b659e05a4eb49d4166cca406" + [[package]] name = "windows_i686_msvc" version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "240948bc05c5e7c6dabba28bf89d89ffce3e303022809e73deaefe4f6ec56c66" +[[package]] +name = "windows_x86_64_gnu" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "53d40abd2583d23e4718fddf1ebec84dbff8381c07cae67ff7768bbf19c6718e" + [[package]] name = "windows_x86_64_gnu" version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "147a5c80aabfbf0c7d901cb5895d1de30ef2907eb21fbbab29ca94c5b08b1a78" +[[package]] +name = "windows_x86_64_gnullvm" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0b7b52767868a23d5bab768e390dc5f5c55825b6d30b86c844ff2dc7414044cc" + [[package]] name = "windows_x86_64_gnullvm" version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "24d5b23dc417412679681396f2b49f3de8c1473deb516bd34410872eff51ed0d" +[[package]] +name = "windows_x86_64_msvc" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ed94fce61571a4006852b7389a063ab983c02eb1bb37b47f8272ce92d06d9538" + [[package]] name = "windows_x86_64_msvc" version = "0.52.6" @@ -1582,5 +2114,5 @@ checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e" dependencies = [ "proc-macro2", "quote", - "syn", + "syn 2.0.79", ] diff --git a/Cargo.toml b/Cargo.toml index ee9848b578dc..42c6f2c722b6 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-verifier" -version = "0.55.0" +version = "0.56.0" edition = "2021" description = "A bit-precise model checker for Rust." readme = "README.md" @@ -56,6 +56,7 @@ default-members = [ exclude = [ "build", + "charon", "target", # dependency tests have their own workspace "tests/kani-dependency-test/dependency3", diff --git a/charon b/charon new file mode 160000 index 000000000000..cdc1dcde447a --- /dev/null +++ b/charon @@ -0,0 +1 @@ +Subproject commit cdc1dcde447a50cbc20336c79b21b42ac977b7fd diff --git a/cprover_bindings/Cargo.toml b/cprover_bindings/Cargo.toml index 008c81aef2ad..e26f23d5c081 100644 --- a/cprover_bindings/Cargo.toml +++ b/cprover_bindings/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "cprover_bindings" -version = "0.55.0" +version = "0.56.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/deny.toml b/deny.toml index 733f91e12f36..e44b234f4ca8 100644 --- a/deny.toml +++ b/deny.toml @@ -11,7 +11,10 @@ yanked = "deny" # A list of advisory IDs to ignore. Note that ignored advisories will still # output a note when they are encountered. ignore = [ - #"RUSTSEC-0000-0000", + # This is for a crate that is used by Charon + "RUSTSEC-2021-0139", + # This is for a crate that is used by Charon + "RUSTSEC-2020-0095", ] # This section is considered when running `cargo deny check licenses` @@ -21,6 +24,7 @@ ignore = [ allow = [ "MIT", "Apache-2.0", + "MPL-2.0", ] confidence-threshold = 0.8 @@ -46,4 +50,6 @@ wildcards = "allow" unknown-registry = "deny" unknown-git = "deny" allow-registry = ["https://github.com/rust-lang/crates.io-index"] -allow-git = [] +allow-git = [ + "https://github.com/hacspec/hax", +] diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index 9ca8d10f5275..7b17e6073bb3 100644 --- a/kani-compiler/Cargo.toml +++ b/kani-compiler/Cargo.toml @@ -3,13 +3,14 @@ [package] name = "kani-compiler" -version = "0.55.0" +version = "0.56.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false [dependencies] cbmc = { path = "../cprover_bindings", package = "cprover_bindings", optional = true } +charon = { path = "../charon/charon", optional = true, default-features = false } clap = { version = "4.4.11", features = ["derive", "cargo"] } home = "0.5" itertools = "0.13" @@ -30,7 +31,8 @@ tracing-tree = "0.4.0" # Future proofing: enable backend dependencies using feature. [features] -default = ['cprover'] +default = ['aeneas', 'cprover'] +aeneas = ['charon'] cprover = ['cbmc', 'num', 'serde'] write_json_symtab = [] diff --git a/kani-compiler/src/args.rs b/kani-compiler/src/args.rs index 3fa74b0e5aba..b5b799321cf3 100644 --- a/kani-compiler/src/args.rs +++ b/kani-compiler/src/args.rs @@ -1,9 +1,23 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -use strum_macros::{AsRefStr, EnumString, VariantNames}; +use strum_macros::{AsRefStr, Display, EnumString, VariantNames}; use tracing_subscriber::filter::Directive; +#[derive(Debug, Default, Display, Clone, Copy, AsRefStr, EnumString, VariantNames, PartialEq, Eq)] +#[strum(serialize_all = "snake_case")] +pub enum BackendOption { + /// Aeneas (LLBC) backend + #[cfg(feature = "aeneas")] + Aeneas, + + /// CProver (Goto) backend + #[cfg(feature = "cprover")] + #[strum(serialize = "cprover")] + #[default] + CProver, +} + #[derive(Debug, Default, Clone, Copy, AsRefStr, EnumString, VariantNames, PartialEq, Eq)] #[strum(serialize_all = "snake_case")] pub enum ReachabilityType { @@ -69,11 +83,13 @@ pub struct Arguments { /// Pass the kani version to the compiler to ensure cache coherence. check_version: Option, #[clap(long)] - /// A legacy flag that is now ignored. - goto_c: bool, - /// Enable specific checks. - #[clap(long)] pub ub_check: Vec, + /// Option name used to select which backend to use. + #[clap(long = "backend", default_value_t = BackendOption::CProver)] + pub backend: BackendOption, + /// Print the final LLBC file to stdout. This requires `-Zaeneas`. + #[clap(long)] + pub print_llbc: bool, } #[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 new file mode 100644 index 000000000000..f9922f237bd5 --- /dev/null +++ b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs @@ -0,0 +1,411 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This file contains the code necessary to interface with the compiler backend + +use crate::args::ReachabilityType; +use crate::codegen_aeneas_llbc::mir_to_ullbc::Context; +use crate::kani_middle::attributes::KaniAttributes; +use crate::kani_middle::check_reachable_items; +use crate::kani_middle::codegen_units::{CodegenUnit, CodegenUnits}; +use crate::kani_middle::provide; +use crate::kani_middle::reachability::{collect_reachable_items, filter_crate_items}; +use crate::kani_middle::transform::{BodyTransformation, GlobalPasses}; +use crate::kani_queries::QueryDb; +use charon_lib::ast::TranslatedCrate; +use charon_lib::errors::ErrorCtx; +use charon_lib::transform::TransformCtx; +use charon_lib::transform::ctx::TransformOptions; +use kani_metadata::ArtifactType; +use kani_metadata::{AssignsContract, CompilerArtifactStub}; +use rustc_codegen_ssa::back::archive::{ + ArArchiveBuilder, ArchiveBuilder, ArchiveBuilderBuilder, DEFAULT_OBJECT_READER, +}; +use rustc_codegen_ssa::back::link::link_binary; +use rustc_codegen_ssa::traits::CodegenBackend; +use rustc_codegen_ssa::{CodegenResults, CrateInfo}; +use rustc_data_structures::fx::FxIndexMap; +use rustc_errors::{DEFAULT_LOCALE_RESOURCE, ErrorGuaranteed}; +use rustc_hir::def_id::{DefId as InternalDefId, LOCAL_CRATE}; +use rustc_metadata::EncodedMetadata; +use rustc_middle::dep_graph::{WorkProduct, WorkProductId}; +use rustc_middle::ty::TyCtxt; +use rustc_middle::util::Providers; +use rustc_session::Session; +use rustc_session::config::{CrateType, OutputFilenames, OutputType}; +use rustc_session::output::out_filename; +use rustc_smir::rustc_internal; +use stable_mir::mir::mono::{Instance, MonoItem}; +use stable_mir::{CrateDef, DefId}; +use std::any::Any; +use std::collections::{HashMap, HashSet}; +use std::fs::File; +use std::path::Path; +use std::sync::{Arc, Mutex}; +use std::time::Instant; +use tracing::{debug, info, trace}; + +#[derive(Clone)] +pub struct LlbcCodegenBackend { + /// The query is shared with `KaniCompiler` and it is initialized as part of `rustc` + /// initialization, which may happen after this object is created. + /// Since we don't have any guarantees on when the compiler creates the Backend object, neither + /// in which thread it will be used, we prefer to explicitly synchronize any query access. + queries: Arc>, +} + +impl LlbcCodegenBackend { + pub fn new(queries: Arc>) -> Self { + LlbcCodegenBackend { queries } + } + + /// Generate code that is reachable from the given starting points. + /// + /// Invariant: iff `check_contract.is_some()` then `return.2.is_some()` + fn codegen_items( + &self, + tcx: TyCtxt, + starting_items: &[MonoItem], + llbc_file: &Path, + _check_contract: Option, + mut transformer: BodyTransformation, + ) -> (Vec, Option) { + let (items, call_graph) = with_timer( + || collect_reachable_items(tcx, &mut transformer, starting_items), + "codegen reachability analysis", + ); + + // Retrieve all instances from the currently codegened items. + let instances = items + .iter() + .filter_map(|item| match item { + MonoItem::Fn(instance) => Some(*instance), + MonoItem::Static(static_def) => { + let instance: Instance = (*static_def).into(); + instance.has_body().then_some(instance) + } + MonoItem::GlobalAsm(_) => None, + }) + .collect(); + + // Apply all transformation passes, including global passes. + let mut global_passes = GlobalPasses::new(&self.queries.lock().unwrap(), tcx); + global_passes.run_global_passes( + &mut transformer, + tcx, + starting_items, + instances, + call_graph, + ); + + let queries = self.queries.lock().unwrap().clone(); + check_reachable_items(tcx, &queries, &items); + + // Follow rustc naming convention (cx is abbrev for context). + // https://rustc-dev-guide.rust-lang.org/conventions.html#naming-conventions + + // Create a Charon transformation context that will be populated with translation results + let mut ccx = create_charon_transformation_context(tcx); + + // Translate all the items + for item in &items { + match item { + MonoItem::Fn(instance) => { + let mut fcx = + Context::new(tcx, *instance, &mut ccx.translated, &mut ccx.errors); + let _ = fcx.translate(); + } + MonoItem::Static(_def) => todo!(), + MonoItem::GlobalAsm(_) => {} // We have already warned above + } + } + + trace!("# ULLBC after translation from MIR:\n\n{}\n", ccx); + + // # Reorder the graph of dependencies and compute the strictly + // connex components to: + // - compute the order in which to extract the definitions + // - find the recursive definitions + // - group the mutually recursive definitions + let reordered_decls = charon_lib::reorder_decls::compute_reordered_decls(&ccx); + ccx.translated.ordered_decls = Some(reordered_decls); + + // + // ================= + // **Micro-passes**: + // ================= + // At this point, the bulk of the translation is done. From now onwards, + // we simply apply some micro-passes to make the code cleaner, before + // serializing the result. + + // Run the micro-passes that clean up bodies. + for pass in charon_lib::transform::ULLBC_PASSES.iter() { + pass.transform_ctx(&mut ccx) + } + + // # Go from ULLBC to LLBC (Low-Level Borrow Calculus) by reconstructing + // the control flow. + charon_lib::ullbc_to_llbc::translate_functions(&mut ccx); + + trace!("# LLBC resulting from control-flow reconstruction:\n\n{}\n", ccx); + + // Run the micro-passes that clean up bodies. + for pass in charon_lib::transform::LLBC_PASSES.iter() { + pass.transform_ctx(&mut ccx) + } + + // Print the LLBC if requested. This is useful for expected tests. + if queries.args().print_llbc { + println!("# Final LLBC before serialization:\n\n{}\n", ccx); + } else { + debug!("# Final LLBC before serialization:\n\n{}\n", ccx); + } + + // Display an error report about the external dependencies, if necessary + ccx.errors.report_external_deps_errors(); + + let crate_data: charon_lib::export::CrateData = charon_lib::export::CrateData::new(&ccx); + + // No output should be generated if user selected no_codegen. + if !tcx.sess.opts.unstable_opts.no_codegen && tcx.sess.opts.output_types.should_codegen() { + // # Final step: generate the files. + // `crate_data` is set by our callbacks when there is no fatal error. + let mut pb = llbc_file.to_path_buf(); + pb.set_extension("llbc"); + println!("Writing LLBC file to {}", pb.display()); + if let Err(()) = crate_data.serialize_to_file(&pb) { + tcx.sess.dcx().err("Failed to write LLBC file"); + } + } + + (items, None) + } +} + +impl CodegenBackend for LlbcCodegenBackend { + fn provide(&self, providers: &mut Providers) { + provide::provide(providers, &self.queries.lock().unwrap()); + } + + fn print_version(&self) { + println!("Kani-llbc version: {}", env!("CARGO_PKG_VERSION")); + } + + fn locale_resource(&self) -> &'static str { + // We don't currently support multiple languages. + DEFAULT_LOCALE_RESOURCE + } + + fn codegen_crate( + &self, + tcx: TyCtxt, + rustc_metadata: EncodedMetadata, + _need_metadata_module: bool, + ) -> Box { + let ret_val = rustc_internal::run(tcx, || { + // Queries shouldn't change today once codegen starts. + let queries = self.queries.lock().unwrap().clone(); + + // Codegen all items that need to be processed according to the selected reachability mode: + // + // - Harnesses: Generate one model per local harnesses (marked with `kani::proof` attribute). + // - Tests: Generate one model per test harnesses. + // - PubFns: Generate code for all reachable logic starting from the local public functions. + // - None: Don't generate code. This is used to compile dependencies. + let base_filepath = tcx.output_filenames(()).path(OutputType::Object); + let base_filename = base_filepath.as_path(); + let reachability = queries.args().reachability_analysis; + match reachability { + ReachabilityType::Harnesses => { + let mut units = CodegenUnits::new(&queries, tcx); + let modifies_instances = vec![]; + // Cross-crate collecting of all items that are reachable from the crate harnesses. + for unit in units.iter() { + // We reset the body cache for now because each codegen unit has different + // configurations that affect how we transform the instance body. + let mut transformer = BodyTransformation::new(&queries, tcx, &unit); + for harness in &unit.harnesses { + let model_path = units.harness_model_path(*harness).unwrap(); + let contract_metadata = + contract_metadata_for_harness(tcx, harness.def.def_id()).unwrap(); + let (_items, contract_info) = self.codegen_items( + tcx, + &[MonoItem::Fn(*harness)], + model_path, + contract_metadata, + transformer, + ); + transformer = BodyTransformation::new(&queries, tcx, &unit); + if let Some(_assigns_contract) = contract_info { + //self.queries.lock().unwrap().register_assigns_contract( + // canonical_mangled_name(harness).intern(), + // assigns_contract, + //); + } + } + } + units.store_modifies(&modifies_instances); + units.write_metadata(&queries, tcx); + } + ReachabilityType::Tests => todo!(), + ReachabilityType::None => {} + ReachabilityType::PubFns => { + let unit = CodegenUnit::default(); + let transformer = BodyTransformation::new(&queries, tcx, &unit); + let main_instance = + stable_mir::entry_fn().map(|main_fn| Instance::try_from(main_fn).unwrap()); + let local_reachable = filter_crate_items(tcx, |_, instance| { + let def_id = rustc_internal::internal(tcx, instance.def.def_id()); + Some(instance) == main_instance || tcx.is_reachable_non_generic(def_id) + }) + .into_iter() + .map(MonoItem::Fn) + .collect::>(); + let model_path = base_filename.with_extension(ArtifactType::SymTabGoto); + let (_items, contract_info) = self.codegen_items( + tcx, + &local_reachable, + &model_path, + Default::default(), + transformer, + ); + assert!(contract_info.is_none()); + } + } + + if reachability != ReachabilityType::None && reachability != ReachabilityType::Harnesses + { + // 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 + // reachability is None, even because there is nothing to record. + } + codegen_results(tcx, rustc_metadata) + }); + ret_val.unwrap() + } + + fn join_codegen( + &self, + ongoing_codegen: Box, + _sess: &Session, + _filenames: &OutputFilenames, + ) -> (CodegenResults, FxIndexMap) { + match ongoing_codegen.downcast::<(CodegenResults, FxIndexMap)>() + { + Ok(val) => *val, + Err(val) => panic!("unexpected error: {:?}", (*val).type_id()), + } + } + + /// Emit output files during the link stage if it was requested. + /// + /// We need to emit `rlib` files normally if requested. Cargo expects these in some + /// circumstances and sends them to subsequent builds with `-L`. + /// + /// We CAN NOT invoke the native linker, because that will fail. We don't have real objects. + /// What determines whether the native linker is invoked or not is the set of `crate_types`. + /// Types such as `bin`, `cdylib`, `dylib` will trigger the native linker. + /// + /// Thus, we manually build the rlib file including only the `rmeta` file. + /// + /// For cases where no metadata file was requested, we stub the file requested by writing the + /// path of the `kani-metadata.json` file so `kani-driver` can safely find the latest metadata. + /// See for more details. + fn link( + &self, + sess: &Session, + codegen_results: CodegenResults, + outputs: &OutputFilenames, + ) -> Result<(), ErrorGuaranteed> { + let requested_crate_types = &codegen_results.crate_info.crate_types; + for crate_type in requested_crate_types { + let out_fname = out_filename( + sess, + *crate_type, + outputs, + codegen_results.crate_info.local_crate_name, + ); + let out_path = out_fname.as_path(); + debug!(?crate_type, ?out_path, "link"); + if *crate_type == CrateType::Rlib { + // Emit the `rlib` that contains just one file: `.rmeta` + link_binary(sess, &ArArchiveBuilderBuilder, &codegen_results, outputs)? + } else { + // Write the location of the kani metadata file in the requested compiler output file. + let base_filepath = outputs.path(OutputType::Object); + let base_filename = base_filepath.as_path(); + let content_stub = CompilerArtifactStub { + metadata_path: base_filename.with_extension(ArtifactType::Metadata), + }; + let out_file = File::create(out_path).unwrap(); + serde_json::to_writer(out_file, &content_stub).unwrap(); + } + } + Ok(()) + } +} + +struct ArArchiveBuilderBuilder; +impl ArchiveBuilderBuilder for ArArchiveBuilderBuilder { + fn new_archive_builder<'a>(&self, sess: &'a Session) -> Box { + Box::new(ArArchiveBuilder::new(sess, &DEFAULT_OBJECT_READER)) + } +} + +fn contract_metadata_for_harness( + tcx: TyCtxt, + def_id: DefId, +) -> Result, ErrorGuaranteed> { + let attrs = KaniAttributes::for_def_id(tcx, def_id); + Ok(attrs.interpret_for_contract_attribute().map(|(_, id, _)| id)) +} + +/// Return a struct that contains information about the codegen results as expected by `rustc`. +fn codegen_results(tcx: TyCtxt, rustc_metadata: EncodedMetadata) -> Box { + let work_products = FxIndexMap::::default(); + Box::new(( + CodegenResults { + modules: vec![], + allocator_module: None, + metadata_module: None, + metadata: rustc_metadata, + crate_info: CrateInfo::new(tcx, tcx.sess.target.arch.clone().to_string()), + }, + work_products, + )) +} + +/// Execute the provided function and measure the clock time it took for its execution. +/// Log the time with the given description. +pub fn with_timer(func: F, description: &str) -> T +where + F: FnOnce() -> T, +{ + let start = Instant::now(); + let ret = func(); + let elapsed = start.elapsed(); + info!("Finished {description} in {}s", elapsed.as_secs_f32()); + ret +} + +fn create_charon_transformation_context(tcx: TyCtxt) -> TransformCtx { + let options = TransformOptions { + no_code_duplication: false, + hide_marker_traits: false, + item_opacities: Vec::new(), + }; + let crate_name = tcx.crate_name(LOCAL_CRATE).as_str().into(); + let translated = TranslatedCrate { crate_name, ..TranslatedCrate::default() }; + let errors = ErrorCtx { + continue_on_failure: true, + errors_as_warnings: false, + dcx: tcx.dcx(), + decls_with_errors: HashSet::new(), + ignored_failed_decls: HashSet::new(), + dep_sources: HashMap::new(), + def_id: None, + error_count: 0, + }; + TransformCtx { options, translated, errors } +} diff --git a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs new file mode 100644 index 000000000000..62462915480e --- /dev/null +++ b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs @@ -0,0 +1,802 @@ +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Modifications Copyright Kani Contributors +// See GitHub history for details. + +//! This module contains a context for translating stable MIR into Charon's +//! unstructured low-level borrow calculus (ULLBC) + +use core::panic; +use std::path::PathBuf; + +use charon_lib::ast::CastKind as CharonCastKind; +use charon_lib::ast::Place as CharonPlace; +use charon_lib::ast::ProjectionElem as CharonProjectionElem; +use charon_lib::ast::Rvalue as CharonRvalue; +use charon_lib::ast::Span as CharonSpan; +use charon_lib::ast::meta::{AttrInfo, Loc, RawSpan}; +use charon_lib::ast::types::Ty as CharonTy; +use charon_lib::ast::{AbortKind, Body as CharonBody, Var, VarId, make_locals_generator}; +use charon_lib::ast::{ + AnyTransId, Assert, BodyId, BuiltinTy, Disambiguator, FileName, FunDecl, FunSig, GenericArgs, + GenericParams, IntegerTy, ItemKind, ItemMeta, ItemOpacity, Literal, LiteralTy, Name, Opaque, + PathElem, RawConstantExpr, RefKind, Region as CharonRegion, ScalarValue, TranslatedCrate, + TypeId, +}; +use charon_lib::ast::{ + BinOp as CharonBinOp, Call, FnOperand, FnPtr, FunDeclId, FunId, FunIdOrTraitMethodRef, + VariantId, +}; +use charon_lib::ast::{ + BorrowKind as CharonBorrowKind, ConstantExpr, Operand as CharonOperand, UnOp, +}; +use charon_lib::common::Error; +use charon_lib::errors::ErrorCtx; +use charon_lib::ids::Vector; +use charon_lib::ullbc_ast::{ + BlockData, BlockId, BodyContents, ExprBody, RawStatement, RawTerminator, + Statement as CharonStatement, SwitchTargets as CharonSwitchTargets, + Terminator as CharonTerminator, +}; +use charon_lib::{error_assert, error_or_panic}; +use rustc_errors::MultiSpan; +use rustc_middle::ty::TyCtxt; +use rustc_smir::rustc_internal; +use rustc_span::def_id::DefId as InternalDefId; +use stable_mir::abi::PassMode; +use stable_mir::mir::mono::Instance; +use stable_mir::mir::{ + BasicBlock, BinOp, Body, BorrowKind, CastKind, ConstOperand, Mutability, Operand, Place, + ProjectionElem, Rvalue, Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind, +}; +use stable_mir::ty::{ + Allocation, ConstantKind, IndexedVal, IntTy, MirConst, Region, RegionKind, RigidTy, Span, Ty, + TyKind, UintTy, +}; + +use stable_mir::{CrateDef, DefId}; +use tracing::{debug, trace}; + +/// A context for translating a single MIR function to ULLBC. +/// The results of the translation are stored in the `translated` field. +pub struct Context<'a, 'tcx> { + tcx: TyCtxt<'tcx>, + instance: Instance, + translated: &'a mut TranslatedCrate, + errors: &'a mut ErrorCtx<'tcx>, +} + +impl<'a, 'tcx> Context<'a, 'tcx> { + /// Create a new context for translating the function `instance`, populating + /// the results of the translation in `translated` + pub fn new( + tcx: TyCtxt<'tcx>, + instance: Instance, + translated: &'a mut TranslatedCrate, + errors: &'a mut ErrorCtx<'tcx>, + ) -> Self { + Self { tcx, instance, translated, errors } + } + + fn tcx(&self) -> TyCtxt<'tcx> { + self.tcx + } + + fn span_err>(&mut self, span: S, msg: &str) { + self.errors.span_err(span, msg); + } + + fn continue_on_failure(&self) -> bool { + self.errors.continue_on_failure() + } + + /// Perform the translation + pub fn translate(&mut self) -> Result<(), ()> { + // Charon's `id_map` is in terms of internal `DefId` + let def_id = rustc_internal::internal(self.tcx(), self.instance.def.def_id()); + + // TODO: might want to populate `errors.dep_sources` to help with + // debugging + + let fid = self.register_fun_decl_id(def_id); + + let item_meta = match self.translate_item_meta_from_rid(self.instance) { + Ok(item_meta) => item_meta, + Err(_) => { + return Err(()); + } + }; + + let signature = self.translate_function_signature(); + let body = match self.translate_function_body() { + Ok(body) => body, + Err(_) => { + return Err(()); + } + }; + + let fun_decl = FunDecl { + def_id: fid, + rust_id: def_id, + item_meta, + signature, + kind: ItemKind::Regular, + body: Ok(body), + }; + + self.translated.fun_decls.set_slot(fid, fun_decl); + + Ok(()) + } + + /// Get or create a `FunDeclId` for the given function + fn register_fun_decl_id(&mut self, def_id: InternalDefId) -> FunDeclId { + let tid = match self.translated.id_map.get(&def_id) { + Some(tid) => *tid, + None => { + let tid = AnyTransId::Fun(self.translated.fun_decls.reserve_slot()); + self.translated.id_map.insert(def_id, tid); + self.translated.reverse_id_map.insert(tid, def_id); + self.translated.all_ids.insert(tid); + tid + } + }; + *tid.as_fun() + } + + /// Compute the meta information for a Rust item identified by its id. + fn translate_item_meta_from_rid(&mut self, instance: Instance) -> Result { + let span = self.translate_instance_span(instance); + let name = self.def_id_to_name(instance.def.def_id())?; + // TODO: populate the source text + let source_text = None; + // TODO: populate the attribute info + let attr_info = + AttrInfo { attributes: Vec::new(), inline: None, rename: None, public: true }; + + // Aeneas only translates items that are local to the top-level crate + // Since we want all reachable items (including those in external + // crates) to be translated, always set `is_local` to true + let is_local = true; + + // For now, assume all items are transparent + let opacity = ItemOpacity::Transparent; + + Ok(ItemMeta { span, source_text, attr_info, name, is_local, opacity }) + } + + /// Retrieve an item name from a [DefId]. + /// This function is adapted from Charon: + /// https://github.com/AeneasVerif/charon/blob/53530427db2941ce784201e64086766504bc5642/charon/src/bin/charon-driver/translate/translate_ctx.rs#L344 + fn def_id_to_name(&mut self, def_id: DefId) -> Result { + trace!("{:?}", def_id); + let def_id = rustc_internal::internal(self.tcx(), def_id); + let tcx = self.tcx(); + let span = tcx.def_span(def_id); + + // We have to be a bit careful when retrieving names from def ids. For instance, + // due to reexports, [`TyCtxt::def_path_str`](TyCtxt::def_path_str) might give + // different names depending on the def id on which it is called, even though + // those def ids might actually identify the same definition. + // For instance: `std::boxed::Box` and `alloc::boxed::Box` are actually + // the same (the first one is a reexport). + // This is why we implement a custom function to retrieve the original name + // (though this makes us lose aliases - we may want to investigate this + // issue in the future). + + // We lookup the path associated to an id, and convert it to a name. + // Paths very precisely identify where an item is. There are important + // subcases, like the items in an `Impl` block: + // ``` + // impl List { + // fn new() ... + // } + // ``` + // + // One issue here is that "List" *doesn't appear* in the path, which would + // look like the following: + // + // `TypeNS("Crate") :: Impl :: ValueNs("new")` + // ^^^ + // This is where "List" should be + // + // For this reason, whenever we find an `Impl` path element, we actually + // lookup the type of the sub-path, from which we can derive a name. + // + // Besides, as there may be several "impl" blocks for one type, each impl + // block is identified by a unique number (rustc calls this a + // "disambiguator"), which we grab. + // + // Example: + // ======== + // For instance, if we write the following code in crate `test` and module + // `bla`: + // ``` + // impl Foo { + // fn foo() { ... } + // } + // + // impl Foo { + // fn bar() { ... } + // } + // ``` + // + // The names we will generate for `foo` and `bar` are: + // `[Ident("test"), Ident("bla"), Ident("Foo"), Disambiguator(0), Ident("foo")]` + // `[Ident("test"), Ident("bla"), Ident("Foo"), Disambiguator(1), Ident("bar")]` + let mut found_crate_name = false; + let mut name: Vec = Vec::new(); + + let def_path = tcx.def_path(def_id); + let crate_name = tcx.crate_name(def_path.krate).to_string(); + + let parents: Vec<_> = { + let mut parents = vec![def_id]; + let mut cur_id = def_id; + while let Some(parent) = tcx.opt_parent(cur_id) { + parents.push(parent); + cur_id = parent; + } + parents.into_iter().rev().collect() + }; + + // Rk.: below we try to be as tight as possible with regards to sanity + // checks, to make sure we understand what happens with def paths, and + // fail whenever we get something which is even slightly outside what + // we expect. + for cur_id in parents { + let data = tcx.def_key(cur_id).disambiguated_data; + // Match over the key data + let disambiguator = Disambiguator::new(data.disambiguator as usize); + use rustc_hir::definitions::DefPathData; + match &data.data { + DefPathData::TypeNs(symbol) => { + error_assert!(self, span, data.disambiguator == 0); // Sanity check + name.push(PathElem::Ident(symbol.to_string(), disambiguator)); + } + DefPathData::ValueNs(symbol) => { + // I think `disambiguator != 0` only with names introduced by macros (though + // not sure). + name.push(PathElem::Ident(symbol.to_string(), disambiguator)); + } + DefPathData::CrateRoot => { + // Sanity check + error_assert!(self, span, data.disambiguator == 0); + + // This should be the beginning of the path + error_assert!(self, span, name.is_empty()); + found_crate_name = true; + name.push(PathElem::Ident(crate_name.clone(), disambiguator)); + } + DefPathData::Impl => todo!(), + DefPathData::OpaqueTy => { + // TODO: do nothing for now + } + DefPathData::MacroNs(symbol) => { + error_assert!(self, span, data.disambiguator == 0); // Sanity check + + // There may be namespace collisions between, say, function + // names and macros (not sure). However, this isn't much + // of an issue here, because for now we don't expose macros + // in the AST, and only use macro names in [register], for + // instance to filter opaque modules. + name.push(PathElem::Ident(symbol.to_string(), disambiguator)); + } + DefPathData::Closure => { + // TODO: this is not very satisfactory, but on the other hand + // we should be able to extract closures in local let-bindings + // (i.e., we shouldn't have to introduce top-level let-bindings). + name.push(PathElem::Ident("closure".to_string(), disambiguator)) + } + DefPathData::ForeignMod => { + // Do nothing, functions in `extern` blocks are in the same namespace as the + // block. + } + _ => { + error_or_panic!(self, span, format!("Unexpected DefPathData: {:?}", data)); + } + } + } + + // We always add the crate name + if !found_crate_name { + name.push(PathElem::Ident(crate_name, Disambiguator::new(0))); + } + + trace!("{:?}", name); + Ok(Name { name }) + } + + /// Compute the span information for the given instance + fn translate_instance_span(&mut self, instance: Instance) -> CharonSpan { + self.translate_span(instance.def.span()) + } + + /// Compute the span information for MIR span + fn translate_span(&mut self, span: Span) -> CharonSpan { + let filename = FileName::Local(PathBuf::from(span.get_filename())); + let file_id = match self.translated.file_to_id.get(&filename) { + Some(file_id) => *file_id, + None => { + let file_id = self.translated.id_to_file.push(filename.clone()); + self.translated.file_to_id.insert(filename, file_id); + file_id + } + }; + let lineinfo = span.get_lines(); + let rspan = RawSpan { + file_id, + beg: Loc { line: lineinfo.start_line, col: lineinfo.start_col }, + end: Loc { line: lineinfo.end_line, col: lineinfo.end_col }, + rust_span_data: rustc_internal::internal(self.tcx(), span).data(), + }; + + // TODO: populate `generated_from_span` info + CharonSpan { span: rspan, generated_from_span: None } + } + + fn translate_function_signature(&mut self) -> FunSig { + let instance = self.instance; + let fn_abi = instance.fn_abi().unwrap(); + let requires_caller_location = self.requires_caller_location(instance); + let num_args = fn_abi.args.len(); + let args = fn_abi + .args + .iter() + .enumerate() + .filter_map(|(idx, arg_abi)| { + // We ignore zero-sized parameters. + // See https://github.com/model-checking/kani/issues/274 for more details. + // We also ingore the last parameter if the function requires + // caller location. + if arg_abi.mode == PassMode::Ignore + || (requires_caller_location && idx + 1 == num_args) + { + None + } else { + let ty = arg_abi.ty; + debug!(?idx, ?arg_abi, "fn_typ"); + Some(self.translate_ty(ty)) + } + }) + .collect(); + + debug!(?args, ?fn_abi, "function_type"); + let ret_type = self.translate_ty(fn_abi.ret.ty); + + // TODO: populate the rest of the information (`is_unsafe`, `is_closure`, etc.) + FunSig { + is_unsafe: false, + is_closure: false, + closure_info: None, + generics: GenericParams::default(), + parent_params_info: None, + inputs: args, + output: ret_type, + } + } + + fn translate_function_body(&mut self) -> Result { + let instance = self.instance; + let mir_body = instance.body().unwrap(); + let body_id = self.translated.bodies.reserve_slot(); + let body = self.translate_body(mir_body); + self.translated.bodies.set_slot(body_id, body); + Ok(body_id) + } + + fn translate_body(&mut self, mir_body: Body) -> CharonBody { + let span = self.translate_span(mir_body.span); + let arg_count = self.instance.fn_abi().unwrap().args.len(); + let locals = self.translate_body_locals(&mir_body); + let body: BodyContents = + mir_body.blocks.iter().map(|bb| self.translate_block(bb)).collect(); + + let body_expr = ExprBody { span, arg_count, locals, body }; + CharonBody::Unstructured(body_expr) + } + + fn requires_caller_location(&self, instance: Instance) -> bool { + let instance_internal = rustc_internal::internal(self.tcx(), instance); + instance_internal.def.requires_caller_location(self.tcx()) + } + + fn translate_ty(&self, ty: Ty) -> CharonTy { + match ty.kind() { + TyKind::RigidTy(rigid_ty) => self.translate_rigid_ty(rigid_ty), + _ => todo!(), + } + } + + fn translate_rigid_ty(&self, rigid_ty: RigidTy) -> CharonTy { + debug!("translate_rigid_ty: {rigid_ty:?}"); + match rigid_ty { + RigidTy::Bool => CharonTy::Literal(LiteralTy::Bool), + RigidTy::Char => CharonTy::Literal(LiteralTy::Char), + RigidTy::Int(it) => CharonTy::Literal(LiteralTy::Integer(translate_int_ty(it))), + RigidTy::Uint(uit) => CharonTy::Literal(LiteralTy::Integer(translate_uint_ty(uit))), + RigidTy::Never => CharonTy::Never, + RigidTy::Str => CharonTy::Adt( + TypeId::Builtin(BuiltinTy::Str), + // TODO: find out whether any of the information below should be + // populated for strings + GenericArgs { + regions: Vector::new(), + types: Vector::new(), + const_generics: Vector::new(), + trait_refs: Vector::new(), + }, + ), + RigidTy::Ref(region, ty, mutability) => CharonTy::Ref( + self.translate_region(region), + Box::new(self.translate_ty(ty)), + match mutability { + Mutability::Mut => RefKind::Mut, + Mutability::Not => RefKind::Shared, + }, + ), + RigidTy::Tuple(ty) => { + let types = ty.iter().map(|ty| self.translate_ty(*ty)).collect(); + // TODO: find out if any of the information below is needed + let generic_args = GenericArgs { + regions: Vector::new(), + types, + const_generics: Vector::new(), + trait_refs: Vector::new(), + }; + CharonTy::Adt(TypeId::Tuple, generic_args) + } + RigidTy::FnDef(def_id, args) => { + if !args.0.is_empty() { + unimplemented!("generic args are not yet handled"); + } + let sig = def_id.fn_sig().value; + let inputs = sig.inputs().iter().map(|ty| self.translate_ty(*ty)).collect(); + let output = self.translate_ty(sig.output()); + // TODO: populate regions? + CharonTy::Arrow(Vector::new(), inputs, Box::new(output)) + } + _ => todo!(), + } + } + + fn translate_body_locals(&mut self, mir_body: &Body) -> Vector { + // Charon expects the locals in the following order: + // - the local used for the return value (index 0) + // - the input arguments + // - the remaining locals, used for the intermediate computations + let mut locals = Vector::new(); + { + let mut add_variable = make_locals_generator(&mut locals); + mir_body.local_decls().for_each(|(_, local)| { + add_variable(self.translate_ty(local.ty)); + }); + } + locals + } + + fn translate_block(&mut self, bb: &BasicBlock) -> BlockData { + let statements = + bb.statements.iter().filter_map(|stmt| self.translate_statement(stmt)).collect(); + let terminator = self.translate_terminator(&bb.terminator); + BlockData { statements, terminator } + } + + fn translate_statement(&mut self, stmt: &Statement) -> Option { + let content = match &stmt.kind { + StatementKind::Assign(place, rhs) => Some(RawStatement::Assign( + self.translate_place(&place), + self.translate_rvalue(&rhs), + )), + StatementKind::SetDiscriminant { place, variant_index } => { + Some(RawStatement::SetDiscriminant( + self.translate_place(&place), + VariantId::from_usize(variant_index.to_index()), + )) + } + StatementKind::StorageLive(_) => None, + StatementKind::StorageDead(local) => { + Some(RawStatement::StorageDead(VarId::from_usize(*local))) + } + StatementKind::Nop => None, + _ => todo!(), + }; + if let Some(content) = content { + let span = self.translate_span(stmt.span); + return Some(CharonStatement { span, content }); + }; + None + } + + fn translate_terminator(&mut self, terminator: &Terminator) -> CharonTerminator { + let span = self.translate_span(terminator.span); + let content = match &terminator.kind { + TerminatorKind::Return => RawTerminator::Return, + TerminatorKind::Goto { target } => { + RawTerminator::Goto { target: BlockId::from_usize(*target) } + } + TerminatorKind::Unreachable => RawTerminator::Abort(AbortKind::UndefinedBehavior), + TerminatorKind::Drop { place, target, .. } => RawTerminator::Drop { + place: self.translate_place(&place), + target: BlockId::from_usize(*target), + }, + TerminatorKind::SwitchInt { discr, targets } => { + let (discr, targets) = self.translate_switch_targets(discr, targets); + RawTerminator::Switch { discr, targets } + } + TerminatorKind::Call { func, args, destination, target, .. } => { + debug!("translate_call: {func:?} {args:?} {destination:?} {target:?}"); + let fn_ty = func.ty(self.instance.body().unwrap().locals()).unwrap(); + let fn_ptr = match fn_ty.kind() { + TyKind::RigidTy(RigidTy::FnDef(def, args)) => { + let instance = Instance::resolve(def, &args).unwrap(); + let def_id = rustc_internal::internal(self.tcx(), instance.def.def_id()); + let fid = self.register_fun_decl_id(def_id); + FnPtr { + func: FunIdOrTraitMethodRef::Fun(FunId::Regular(fid)), + // TODO: populate generics? + generics: GenericArgs { + regions: Vector::new(), + types: Vector::new(), + const_generics: Vector::new(), + trait_refs: Vector::new(), + }, + } + } + TyKind::RigidTy(RigidTy::FnPtr(..)) => todo!(), + x => unreachable!( + "Function call where the function was of unexpected type: {:?}", + x + ), + }; + let func = FnOperand::Regular(fn_ptr); + let call = Call { + func, + args: args.iter().map(|arg| self.translate_operand(arg)).collect(), + dest: self.translate_place(destination), + }; + RawTerminator::Call { call, target: target.map(BlockId::from_usize) } + } + TerminatorKind::Assert { cond, expected, msg: _, target, .. } => { + RawTerminator::Assert { + assert: Assert { cond: self.translate_operand(cond), expected: *expected }, + target: BlockId::from_usize(*target), + } + } + _ => todo!(), + }; + CharonTerminator { span, content } + } + + fn translate_place(&self, place: &Place) -> CharonPlace { + let projection = self.translate_projection(&place.projection); + let local = place.local; + let var_id = VarId::from_usize(local); + CharonPlace { var_id, projection } + } + + fn translate_rvalue(&self, rvalue: &Rvalue) -> CharonRvalue { + trace!("translate_rvalue: {rvalue:?}"); + match rvalue { + Rvalue::Use(operand) => CharonRvalue::Use(self.translate_operand(operand)), + Rvalue::Repeat(_operand, _) => todo!(), + Rvalue::Ref(_region, kind, place) => { + CharonRvalue::Ref(self.translate_place(&place), translate_borrow_kind(kind)) + } + Rvalue::AddressOf(_, _) => todo!(), + Rvalue::Len(place) => CharonRvalue::Len( + self.translate_place(&place), + self.translate_ty(rvalue.ty(self.instance.body().unwrap().locals()).unwrap()), + None, + ), + Rvalue::Cast(kind, operand, ty) => CharonRvalue::UnaryOp( + UnOp::Cast(self.translate_cast(*kind, operand, *ty)), + self.translate_operand(operand), + ), + Rvalue::BinaryOp(bin_op, lhs, rhs) => CharonRvalue::BinaryOp( + translate_bin_op(*bin_op), + self.translate_operand(lhs), + self.translate_operand(rhs), + ), + Rvalue::CheckedBinaryOp(_, _, _) => todo!(), + Rvalue::UnaryOp(_, _) => todo!(), + Rvalue::Discriminant(_) => todo!(), + Rvalue::Aggregate(_, _) => todo!(), + Rvalue::ShallowInitBox(_, _) => todo!(), + Rvalue::CopyForDeref(_) => todo!(), + Rvalue::ThreadLocalRef(_) => todo!(), + _ => todo!(), + } + } + + fn translate_operand(&self, operand: &Operand) -> CharonOperand { + trace!("translate_operand: {operand:?}"); + match operand { + Operand::Constant(constant) => CharonOperand::Const(self.translate_constant(constant)), + Operand::Copy(place) => CharonOperand::Copy(self.translate_place(&place)), + Operand::Move(place) => CharonOperand::Move(self.translate_place(&place)), + } + } + + fn translate_constant(&self, constant: &ConstOperand) -> ConstantExpr { + trace!("translate_constant: {constant:?}"); + let value = self.translate_constant_value(&constant.const_); + ConstantExpr { value, ty: self.translate_ty(constant.ty()) } + } + + fn translate_constant_value(&self, constant: &MirConst) -> RawConstantExpr { + trace!("translate_constant_value: {constant:?}"); + match constant.kind() { + ConstantKind::Allocated(alloc) => self.translate_allocation(alloc, constant.ty()), + ConstantKind::Ty(_) => todo!(), + ConstantKind::ZeroSized => todo!(), + ConstantKind::Unevaluated(_) => todo!(), + ConstantKind::Param(_) => todo!(), + } + } + + fn translate_allocation(&self, alloc: &Allocation, ty: Ty) -> RawConstantExpr { + match ty.kind() { + TyKind::RigidTy(RigidTy::Int(it)) => { + let value = alloc.read_int().unwrap(); + let scalar_value = match it { + IntTy::I8 => ScalarValue::I8(value as i8), + IntTy::I16 => ScalarValue::I16(value as i16), + IntTy::I32 => ScalarValue::I32(value as i32), + IntTy::I64 => ScalarValue::I64(value as i64), + IntTy::I128 => ScalarValue::I128(value), + IntTy::Isize => ScalarValue::Isize(value as i64), + }; + RawConstantExpr::Literal(Literal::Scalar(scalar_value)) + } + TyKind::RigidTy(RigidTy::Uint(uit)) => { + let value = alloc.read_uint().unwrap(); + let scalar_value = match uit { + UintTy::U8 => ScalarValue::U8(value as u8), + UintTy::U16 => ScalarValue::U16(value as u16), + UintTy::U32 => ScalarValue::U32(value as u32), + UintTy::U64 => ScalarValue::U64(value as u64), + UintTy::U128 => ScalarValue::U128(value), + UintTy::Usize => ScalarValue::Usize(value as u64), + }; + RawConstantExpr::Literal(Literal::Scalar(scalar_value)) + } + TyKind::RigidTy(RigidTy::Bool) => { + let value = alloc.read_bool().unwrap(); + RawConstantExpr::Literal(Literal::Bool(value)) + } + TyKind::RigidTy(RigidTy::Char) => { + let value = char::from_u32(alloc.read_uint().unwrap() as u32); + RawConstantExpr::Literal(Literal::Char(value.unwrap())) + } + _ => todo!(), + } + } + + fn translate_cast(&self, _kind: CastKind, _operand: &Operand, _ty: Ty) -> CharonCastKind { + todo!() + } + + fn translate_switch_targets( + &self, + discr: &Operand, + targets: &SwitchTargets, + ) -> (CharonOperand, CharonSwitchTargets) { + trace!("translate_switch_targets: {discr:?} {targets:?}"); + let ty = discr.ty(self.instance.body().unwrap().locals()).unwrap(); + let discr = self.translate_operand(discr); + let charon_ty = self.translate_ty(ty); + let switch_targets = if ty.kind().is_bool() { + // Charon/Aeneas expects types with a bool discriminant to be translated to an `If` + // `len` includes the `otherwise` branch + assert_eq!(targets.len(), 2); + let (value, bb) = targets.branches().last().unwrap(); + let (then_bb, else_bb) = + if value == 0 { (targets.otherwise(), bb) } else { (bb, targets.otherwise()) }; + CharonSwitchTargets::If(BlockId::from_usize(then_bb), BlockId::from_usize(else_bb)) + } else { + let CharonTy::Literal(LiteralTy::Integer(int_ty)) = charon_ty else { + panic!("Expected integer type for switch discriminant"); + }; + let branches = targets + .branches() + .map(|(value, bb)| { + let scalar_val = match int_ty { + IntegerTy::I8 => ScalarValue::I8(value as i8), + IntegerTy::I16 => ScalarValue::I16(value as i16), + IntegerTy::I32 => ScalarValue::I32(value as i32), + IntegerTy::I64 => ScalarValue::I64(value as i64), + IntegerTy::I128 => ScalarValue::I128(value as i128), + IntegerTy::Isize => ScalarValue::Isize(value as i64), + IntegerTy::U8 => ScalarValue::U8(value as u8), + IntegerTy::U16 => ScalarValue::U16(value as u16), + IntegerTy::U32 => ScalarValue::U32(value as u32), + IntegerTy::U64 => ScalarValue::U64(value as u64), + IntegerTy::U128 => ScalarValue::U128(value), + IntegerTy::Usize => ScalarValue::Usize(value as u64), + }; + (scalar_val, BlockId::from_usize(bb)) + }) + .collect(); + let otherwise = BlockId::from_usize(targets.otherwise()); + CharonSwitchTargets::SwitchInt(int_ty, branches, otherwise) + }; + (discr, switch_targets) + } + + fn translate_projection(&self, projection: &[ProjectionElem]) -> Vec { + projection.iter().map(|elem| self.translate_projection_elem(elem)).collect() + } + + fn translate_projection_elem(&self, projection_elem: &ProjectionElem) -> CharonProjectionElem { + match projection_elem { + ProjectionElem::Deref => CharonProjectionElem::Deref, + _ => todo!(), + } + } + + fn translate_region(&self, region: Region) -> CharonRegion { + match region.kind { + RegionKind::ReStatic => CharonRegion::Static, + RegionKind::ReErased => CharonRegion::Erased, + RegionKind::ReEarlyParam(_) + | RegionKind::ReBound(_, _) + | RegionKind::RePlaceholder(_) => todo!(), + } + } +} + +fn translate_int_ty(int_ty: IntTy) -> IntegerTy { + match int_ty { + IntTy::I8 => IntegerTy::I8, + IntTy::I16 => IntegerTy::I16, + IntTy::I32 => IntegerTy::I32, + IntTy::I64 => IntegerTy::I64, + IntTy::I128 => IntegerTy::I128, + // TODO: assumes 64-bit platform + IntTy::Isize => IntegerTy::I64, + } +} + +fn translate_uint_ty(uint_ty: UintTy) -> IntegerTy { + match uint_ty { + UintTy::U8 => IntegerTy::U8, + UintTy::U16 => IntegerTy::U16, + UintTy::U32 => IntegerTy::U32, + UintTy::U64 => IntegerTy::U64, + UintTy::U128 => IntegerTy::U128, + // TODO: assumes 64-bit platform + UintTy::Usize => IntegerTy::U64, + } +} + +fn translate_bin_op(bin_op: BinOp) -> CharonBinOp { + match bin_op { + BinOp::Add | BinOp::AddUnchecked => CharonBinOp::Add, + BinOp::Sub | BinOp::SubUnchecked => CharonBinOp::Sub, + BinOp::Mul | BinOp::MulUnchecked => CharonBinOp::Mul, + BinOp::Div => CharonBinOp::Div, + BinOp::Rem => CharonBinOp::Rem, + BinOp::BitXor => CharonBinOp::BitXor, + BinOp::BitAnd => CharonBinOp::BitAnd, + BinOp::BitOr => CharonBinOp::BitOr, + BinOp::Shl | BinOp::ShlUnchecked => CharonBinOp::Shl, + BinOp::Shr | BinOp::ShrUnchecked => CharonBinOp::Shr, + BinOp::Eq => CharonBinOp::Eq, + BinOp::Lt => CharonBinOp::Lt, + BinOp::Le => CharonBinOp::Le, + BinOp::Ne => CharonBinOp::Ne, + BinOp::Ge => CharonBinOp::Ge, + BinOp::Gt => CharonBinOp::Gt, + BinOp::Cmp => todo!(), + BinOp::Offset => todo!(), + } +} + +fn translate_borrow_kind(kind: &BorrowKind) -> CharonBorrowKind { + match kind { + BorrowKind::Shared => CharonBorrowKind::Shared, + BorrowKind::Mut { .. } => CharonBorrowKind::Mut, + BorrowKind::Fake(_kind) => todo!(), + } +} diff --git a/kani-compiler/src/codegen_aeneas_llbc/mod.rs b/kani-compiler/src/codegen_aeneas_llbc/mod.rs new file mode 100644 index 000000000000..085c42ea4119 --- /dev/null +++ b/kani-compiler/src/codegen_aeneas_llbc/mod.rs @@ -0,0 +1,10 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This module hosts a codegen backend that produces low-level borrow calculus +//! (LLBC), which is the format defined by Charon/Aeneas + +mod compiler_interface; +mod mir_to_ullbc; + +pub use compiler_interface::LlbcCodegenBackend; diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 250a7b79d8bc..25bc0cbe8ad1 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -402,13 +402,7 @@ impl CodegenBackend for GotocCodegenBackend { /// We need to emit `rlib` files normally if requested. Cargo expects these in some /// circumstances and sends them to subsequent builds with `-L`. /// - /// We CAN NOT invoke the native linker, because that will fail. We don't have real objects. - /// What determines whether the native linker is invoked or not is the set of `crate_types`. - /// Types such as `bin`, `cdylib`, `dylib` will trigger the native linker. - /// - /// Thus, we manually build the rlib file including only the `rmeta` file. - /// - /// For cases where no metadata file was requested, we stub the file requested by writing the + /// For other crate types, we stub the file requested by writing the /// path of the `kani-metadata.json` file so `kani-driver` can safely find the latest metadata. /// See for more details. fn link( @@ -418,6 +412,14 @@ impl CodegenBackend for GotocCodegenBackend { outputs: &OutputFilenames, ) -> Result<(), ErrorGuaranteed> { let requested_crate_types = &codegen_results.crate_info.crate_types; + // Create the rlib if one was requested. + if requested_crate_types.iter().any(|crate_type| *crate_type == CrateType::Rlib) { + link_binary(sess, &ArArchiveBuilderBuilder, &codegen_results, outputs)?; + } + + // But override all the other outputs. + // Note: Do this after `link_binary` call, since it may write to the object files + // and override the json we are creating. for crate_type in requested_crate_types { let out_fname = out_filename( sess, @@ -427,10 +429,7 @@ impl CodegenBackend for GotocCodegenBackend { ); let out_path = out_fname.as_path(); debug!(?crate_type, ?out_path, "link"); - if *crate_type == CrateType::Rlib { - // Emit the `rlib` that contains just one file: `.rmeta` - link_binary(sess, &ArArchiveBuilderBuilder, &codegen_results, outputs)? - } else { + if *crate_type != CrateType::Rlib { // Write the location of the kani metadata file in the requested compiler output file. let base_filepath = outputs.path(OutputType::Object); let base_filename = base_filepath.as_path(); diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index 58c22f940352..a6b6cf3a03af 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/kani-compiler/src/kani_compiler.rs @@ -15,7 +15,9 @@ //! in order to apply the stubs. For the subsequent runs, we add the stub configuration to //! `-C llvm-args`. -use crate::args::Arguments; +use crate::args::{Arguments, BackendOption}; +#[cfg(feature = "aeneas")] +use crate::codegen_aeneas_llbc::LlbcCodegenBackend; #[cfg(feature = "cprover")] use crate::codegen_cprover_gotoc::GotocCodegenBackend; use crate::kani_middle::check_crate_items; @@ -42,16 +44,37 @@ pub fn run(args: Vec) -> ExitCode { } } -/// Configure the cprover backend that generate goto-programs. -#[cfg(feature = "cprover")] +/// Configure the Aeneas backend that generates LLBC. +fn aeneas_backend(_queries: Arc>) -> Box { + #[cfg(feature = "aeneas")] + return Box::new(LlbcCodegenBackend::new(_queries)); + #[cfg(not(feature = "aeneas"))] + unreachable!() +} + +/// Configure the cprover backend that generates goto-programs. +fn cprover_backend(_queries: Arc>) -> Box { + #[cfg(feature = "cprover")] + return Box::new(GotocCodegenBackend::new(_queries)); + #[cfg(not(feature = "cprover"))] + unreachable!() +} + +#[cfg(any(feature = "aeneas", feature = "cprover"))] fn backend(queries: Arc>) -> Box { - Box::new(GotocCodegenBackend::new(queries)) + let backend = queries.lock().unwrap().args().backend; + match backend { + #[cfg(feature = "aeneas")] + BackendOption::Aeneas => aeneas_backend(queries), + #[cfg(feature = "cprover")] + BackendOption::CProver => cprover_backend(queries), + } } /// Fallback backend. It will trigger an error if no backend has been enabled. -#[cfg(not(feature = "cprover"))] +#[cfg(not(any(feature = "aeneas", feature = "cprover")))] fn backend(queries: Arc>) -> Box { - compile_error!("No backend is available. Only supported value today is `cprover`"); + compile_error!("No backend is available. Use `aeneas` or `cprover`."); } /// This object controls the compiler behavior. diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs index 3a7816c1b084..1ba05d990955 100644 --- a/kani-compiler/src/main.rs +++ b/kani-compiler/src/main.rs @@ -38,6 +38,8 @@ extern crate stable_mir; extern crate tempfile; mod args; +#[cfg(feature = "aeneas")] +mod codegen_aeneas_llbc; #[cfg(feature = "cprover")] mod codegen_cprover_gotoc; mod intrinsics; diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index a67dd1cea50f..67214738fa7c 100644 --- a/kani-driver/Cargo.toml +++ b/kani-driver/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-driver" -version = "0.55.0" +version = "0.56.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/mod.rs b/kani-driver/src/args/mod.rs index 1b7dac90facb..8aa758219524 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -41,6 +41,7 @@ where .unwrap() } +#[allow(dead_code)] pub fn print_obsolete(verbosity: &CommonArgs, option: &str) { if !verbosity.quiet { warning(&format!( @@ -195,14 +196,6 @@ pub struct VerificationArgs { #[arg(long, hide_short_help = true)] pub only_codegen: bool, - /// Deprecated flag. This is a no-op since we no longer support the legacy linker and - /// it will be removed in a future Kani release. - #[arg(long, hide = true, conflicts_with("mir_linker"))] - pub legacy_linker: bool, - /// Deprecated flag. This is a no-op since we no longer support any other linker. - #[arg(long, hide = true)] - pub mir_linker: bool, - /// Specify the value used for loop unwinding in CBMC #[arg(long)] pub default_unwind: Option, @@ -284,6 +277,10 @@ pub struct VerificationArgs { #[arg(long, hide_short_help = true)] pub coverage: bool, + /// Print final LLBC for Aeneas backend. This requires the `-Z aeneas` option. + #[arg(long, hide = true)] + pub print_llbc: bool, + /// Arguments to pass down to Cargo #[command(flatten)] pub cargo: CargoCommonArgs, @@ -532,14 +529,6 @@ impl ValidateArgs for VerificationArgs { } } - if self.mir_linker { - print_obsolete(&self.common_args, "--mir-linker"); - } - - if self.legacy_linker { - print_obsolete(&self.common_args, "--legacy-linker"); - } - // TODO: these conflicting flags reflect what's necessary to pass current tests unmodified. // We should consider improving the error messages slightly in a later pull request. if natives_unwind && extra_unwind { @@ -632,6 +621,23 @@ impl ValidateArgs for VerificationArgs { )); } + if self.print_llbc && !self.common_args.unstable_features.contains(UnstableFeature::Aeneas) + { + return Err(Error::raw( + ErrorKind::MissingRequiredArgument, + "The `--print-llbc` argument is unstable and requires `-Z aeneas` to be used.", + )); + } + + // TODO: error out for other CBMC-backend-specific arguments + if self.common_args.unstable_features.contains(UnstableFeature::Aeneas) + && !self.cbmc_args.is_empty() + { + return Err(Error::raw( + ErrorKind::ArgumentConflict, + "The `--cbmc-args` argument cannot be used with -Z aeneas.", + )); + } Ok(()) } } @@ -922,4 +928,12 @@ mod tests { check_invalid_args("kani input.rs --package foo".split_whitespace()); check_invalid_args("kani input.rs --exclude bar --workspace".split_whitespace()); } + + #[test] + fn check_cbmc_args_aeneas_backend() { + let args = "kani input.rs -Z aeneas --enable-unstable --cbmc-args --object-bits 10" + .split_whitespace(); + let err = StandaloneArgs::try_parse_from(args).unwrap().validate().unwrap_err(); + assert_eq!(err.kind(), ErrorKind::ArgumentConflict); + } } diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index 191b104a8c1c..b566f0ff79c7 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -46,10 +46,39 @@ pub struct CargoOutputs { impl KaniSession { /// Create a new cargo library in the given path. + /// + /// Since we cannot create a new workspace with `cargo init --lib`, we create the dummy + /// crate manually. =( See . + /// + /// Without setting up a new workspace, cargo init will modify the workspace where this is + /// running. See for details. pub fn cargo_init_lib(&self, path: &Path) -> Result<()> { - let mut cmd = setup_cargo_command()?; - cmd.args(["init", "--lib", path.to_string_lossy().as_ref()]); - self.run_terminal(cmd) + let toml_path = path.join("Cargo.toml"); + if toml_path.exists() { + bail!("Cargo.toml already exists in {}", path.display()); + } + + // Create folder for library + fs::create_dir_all(path.join("src"))?; + + // Create dummy crate and write dummy body + let lib_path = path.join("src/lib.rs"); + fs::write(&lib_path, "pub fn dummy() {}")?; + + // Create Cargo.toml + fs::write( + &toml_path, + r#"[package] +name = "dummy" +version = "0.1.0" + +[lib] +crate-type = ["lib"] + +[workspace] +"#, + )?; + Ok(()) } pub fn cargo_build_std(&self, std_path: &Path, krate_path: &Path) -> Result> { @@ -164,6 +193,9 @@ impl KaniSession { // Arguments that will only be passed to the target package. let mut pkg_args: Vec = vec![]; pkg_args.extend(["--".to_string(), self.reachability_arg()]); + if let Some(backend_arg) = self.backend_arg() { + pkg_args.push(backend_arg); + } let mut found_target = false; let packages = packages_to_verify(&self.args, &metadata)?; diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs index 63ca71d5b8d1..e33fbe874946 100644 --- a/kani-driver/src/call_single_file.rs +++ b/kani-driver/src/call_single_file.rs @@ -53,6 +53,9 @@ impl KaniSession { ) -> Result<()> { let mut kani_args = self.kani_compiler_flags(); kani_args.push(format!("--reachability={}", self.reachability_mode())); + if self.args.common_args.unstable_features.contains(UnstableFeature::Aeneas) { + kani_args.push("--backend=aeneas".into()); + } let lib_path = lib_folder().unwrap(); let mut rustc_args = self.kani_rustc_flags(LibConfig::new(lib_path)); @@ -95,6 +98,14 @@ impl KaniSession { to_rustc_arg(vec![format!("--reachability={}", self.reachability_mode())]) } + pub fn backend_arg(&self) -> Option { + if self.args.common_args.unstable_features.contains(UnstableFeature::Aeneas) { + Some(to_rustc_arg(vec!["--backend=aeneas".into()])) + } else { + None + } + } + /// These arguments are arguments passed to kani-compiler that are `kani` compiler specific. pub fn kani_compiler_flags(&self) -> Vec { let mut flags = vec![check_version()]; @@ -142,11 +153,11 @@ impl KaniSession { flags.push("--ub-check=uninit".into()); } - flags.extend(self.args.common_args.unstable_features.as_arguments().map(str::to_string)); + if self.args.print_llbc { + flags.push("--print-llbc".into()); + } - // This argument will select the Kani flavour of the compiler. It will be removed before - // rustc driver is invoked. - flags.push("--goto-c".into()); + flags.extend(self.args.common_args.unstable_features.as_arguments().map(str::to_string)); flags } diff --git a/kani_metadata/Cargo.toml b/kani_metadata/Cargo.toml index 18eadc4095ed..2a0a03401c40 100644 --- a/kani_metadata/Cargo.toml +++ b/kani_metadata/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_metadata" -version = "0.55.0" +version = "0.56.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/kani_metadata/src/unstable.rs b/kani_metadata/src/unstable.rs index db302498ef58..a602c33e0326 100644 --- a/kani_metadata/src/unstable.rs +++ b/kani_metadata/src/unstable.rs @@ -88,6 +88,8 @@ pub enum UnstableFeature { /// Automatically check that no invalid value is produced which is considered UB in Rust. /// Note that this does not include checking uninitialized value. ValidValueChecks, + /// Aeneas/LLBC + Aeneas, /// Ghost state and shadow memory APIs. GhostState, /// Automatically check that uninitialized memory is not used. diff --git a/library/kani/Cargo.toml b/library/kani/Cargo.toml index fa50783516f4..3ad1b286ebe6 100644 --- a/library/kani/Cargo.toml +++ b/library/kani/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani" -version = "0.55.0" +version = "0.56.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/kani/src/contracts.rs b/library/kani/src/contracts.rs index beddd7cc580e..2dc2bd2a4957 100644 --- a/library/kani/src/contracts.rs +++ b/library/kani/src/contracts.rs @@ -25,7 +25,7 @@ //! simple division function `my_div`: //! //! ``` -//! fn my_div(dividend: u32, divisor: u32) -> u32 { +//! fn my_div(dividend: usize, divisor: usize) -> usize { //! dividend / divisor //! } //! ``` @@ -35,8 +35,12 @@ //! allows us to declare constraints on what constitutes valid inputs to our //! function. In this case we would want to disallow a divisor that is `0`. //! -//! ```ignore +//! ``` +//! # use kani::requires; //! #[requires(divisor != 0)] +//! # fn my_div(dividend: usize, divisor: usize) -> usize { +//! # dividend / divisor +//! # } //! ``` //! //! This is called a precondition, because it is enforced before (pre-) the @@ -51,7 +55,11 @@ //! approximation of the result of division for instance could be this: //! //! ``` -//! #[ensures(|result : &u32| *result <= dividend)] +//! # use kani::ensures; +//! #[ensures(|result : &usize| *result <= dividend)] +//! # fn my_div(dividend: usize, divisor: usize) -> usize { +//! # dividend / divisor +//! # } //! ``` //! //! This is called a postcondition and it also has access to the arguments and @@ -66,9 +74,11 @@ //! order does not matter. In our example putting them together looks like this: //! //! ``` -//! #[kani::requires(divisor != 0)] -//! #[kani::ensures(|result : &u32| *result <= dividend)] -//! fn my_div(dividend: u32, divisor: u32) -> u32 { +//! use kani::{requires, ensures}; +//! +//! #[requires(divisor != 0)] +//! #[ensures(|result : &usize| *result <= dividend)] +//! fn my_div(dividend: usize, divisor: usize) -> usize { //! dividend / divisor //! } //! ``` @@ -84,9 +94,18 @@ //! function we want to check. //! //! ``` +//! # use kani::{requires, ensures}; +//! # +//! # #[requires(divisor != 0)] +//! # #[ensures(|result : &usize| *result <= dividend)] +//! # fn my_div(dividend: usize, divisor: usize) -> usize { +//! # dividend / divisor +//! # } +//! # //! #[kani::proof_for_contract(my_div)] //! fn my_div_harness() { -//! my_div(kani::any(), kani::any()) } +//! my_div(kani::any(), kani::any()); +//! } //! ``` //! //! The harness is checked like any other by running `cargo kani` and can be @@ -104,10 +123,18 @@ //! the contract will be used automatically. //! //! ``` +//! # use kani::{requires, ensures}; +//! # +//! # #[requires(divisor != 0)] +//! # #[ensures(|result : &usize| *result <= dividend)] +//! # fn my_div(dividend: usize, divisor: usize) -> usize { +//! # dividend / divisor +//! # } +//! # //! #[kani::proof] //! #[kani::stub_verified(my_div)] //! fn use_div() { -//! let v = vec![...]; +//! let v = kani::vec::any_vec::(); //! let some_idx = my_div(v.len() - 1, 3); //! v[some_idx]; //! } diff --git a/library/kani/src/invariant.rs b/library/kani/src/invariant.rs index 068cdedc277e..b1bac031b677 100644 --- a/library/kani/src/invariant.rs +++ b/library/kani/src/invariant.rs @@ -39,6 +39,14 @@ /// ``` /// You can specify its safety invariant as: /// ```rust +/// # #[derive(kani::Arbitrary)] +/// # pub struct MyDate { +/// # day: u8, +/// # month: u8, +/// # year: i64, +/// # } +/// # fn days_in_month(_: i64, _: u8) -> u8 { 31 } +/// /// impl kani::Invariant for MyDate { /// fn is_safe(&self) -> bool { /// self.month > 0 @@ -49,12 +57,33 @@ /// } /// ``` /// And use it to check that your APIs are safe: -/// ```rust +/// ```no_run +/// # use kani::Invariant; +/// # +/// # #[derive(kani::Arbitrary)] +/// # pub struct MyDate { +/// # day: u8, +/// # month: u8, +/// # year: i64, +/// # } +/// # +/// # fn days_in_month(_: i64, _: u8) -> u8 { todo!() } +/// # fn increase_date(_: &mut MyDate, _: u8) { todo!() } +/// # +/// # impl Invariant for MyDate { +/// # fn is_safe(&self) -> bool { +/// # self.month > 0 +/// # && self.month <= 12 +/// # && self.day > 0 +/// # && self.day <= days_in_month(self.year, self.month) +/// # } +/// # } +/// # /// #[kani::proof] /// fn check_increase_date() { /// let mut date: MyDate = kani::any(); /// // Increase date by one day -/// increase_date(date, 1); +/// increase_date(&mut date, 1); /// assert!(date.is_safe()); /// } /// ``` diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index 053af760067b..ce1eeb992121 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -19,6 +19,8 @@ #![feature(ptr_metadata)] #![feature(f16)] #![feature(f128)] +// Need to add this since we are deprecating `kani::check`. Remove this when we remove that API. +#![allow(deprecated)] // Allow us to use `kani::` to access crate features. extern crate self as kani; diff --git a/library/kani/src/shadow.rs b/library/kani/src/shadow.rs index a7ea57c6fd40..48ce8f0f9211 100644 --- a/library/kani/src/shadow.rs +++ b/library/kani/src/shadow.rs @@ -10,7 +10,7 @@ //! //! # Example //! -//! ``` +//! ```no_run //! use kani::shadow::ShadowMem; //! use std::alloc::{alloc, Layout}; //! diff --git a/library/kani/src/slice.rs b/library/kani/src/slice.rs index 1b13de29d589..c419a881fa55 100644 --- a/library/kani/src/slice.rs +++ b/library/kani/src/slice.rs @@ -9,7 +9,8 @@ use crate::{any, assume}; /// /// # Example: /// -/// ```rust +/// ```no_run +/// # fn foo(_: &[i32]) {} /// let arr = [1, 2, 3]; /// let slice = kani::slice::any_slice_of_array(&arr); /// foo(slice); // where foo is a function that takes a slice and verifies a property about it diff --git a/library/kani_core/Cargo.toml b/library/kani_core/Cargo.toml index 447cd0b3f298..df55e6278282 100644 --- a/library/kani_core/Cargo.toml +++ b/library/kani_core/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_core" -version = "0.55.0" +version = "0.56.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/kani_core/src/arbitrary.rs b/library/kani_core/src/arbitrary.rs index 8c6cfd335104..1dc30feca566 100644 --- a/library/kani_core/src/arbitrary.rs +++ b/library/kani_core/src/arbitrary.rs @@ -7,11 +7,16 @@ //! by an unconstrained symbolic value of their size (e.g., `u8`, `u16`, `u32`, etc.). //! //! TODO: Use this inside kani library so that we dont have to maintain two copies of the same proc macro for arbitrary. + +mod pointer; + #[macro_export] #[allow(clippy::crate_in_macro_def)] macro_rules! generate_arbitrary { ($core:path) => { use core_path::marker::{PhantomData, PhantomPinned}; + use core_path::mem::MaybeUninit; + use core_path::ptr::{self, addr_of_mut}; use $core as core_path; pub trait Arbitrary @@ -157,6 +162,15 @@ macro_rules! generate_arbitrary { } } + impl Arbitrary for MaybeUninit + where + T: Arbitrary, + { + fn any() -> Self { + if crate::kani::any() { MaybeUninit::new(T::any()) } else { MaybeUninit::uninit() } + } + } + arbitrary_tuple!(A); arbitrary_tuple!(A, B); arbitrary_tuple!(A, B, C); @@ -169,6 +183,11 @@ macro_rules! generate_arbitrary { arbitrary_tuple!(A, B, C, D, E, F, G, H, I, J); arbitrary_tuple!(A, B, C, D, E, F, G, H, I, J, K); arbitrary_tuple!(A, B, C, D, E, F, G, H, I, J, K, L); + + pub use self::arbitrary_ptr::*; + mod arbitrary_ptr { + kani_core::ptr_generator!(); + } }; } diff --git a/library/kani_core/src/arbitrary/pointer.rs b/library/kani_core/src/arbitrary/pointer.rs new file mode 100644 index 000000000000..0e987b1260c6 --- /dev/null +++ b/library/kani_core/src/arbitrary/pointer.rs @@ -0,0 +1,371 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This macro generates the logic required to generate pointers with arbitrary statuses. +#[allow(clippy::crate_in_macro_def)] +#[macro_export] +macro_rules! ptr_generator { + () => { + use core::marker::PhantomData; + use core::mem::MaybeUninit; + use core::ptr::{self, addr_of_mut}; + use crate::kani; + + /// Pointer generator that can be used to generate arbitrary pointers. + /// + /// This generator allows users to build pointers with different safety properties. + /// This is different than creating a pointer that can have any address, since it will never + /// point to a previously allocated object. + /// See [this section](crate::PointerGenerator#pointer-generator-vs-pointer-with-any-address) + /// for more details. + /// + /// The generator contains an internal buffer of a constant generic size, `BYTES`, that it + /// uses to generate `InBounds` and `OutOfBounds` pointers. + /// In those cases, the generated pointers will have the same provenance as the generator, + /// and the same lifetime. + /// The address of an `InBounds` pointer will represent all possible addresses in the range + /// of the generator's buffer address. + /// + /// For other allocation statuses, the generator will create a pointer that satisfies the + /// given condition. + /// The pointer address will **not** represent all possible addresses that satisfies the + /// given allocation status. + /// + /// For example: + /// ```no_run + /// # use kani::*; + /// # #[kani::proof] + /// # fn harness() { + /// let mut generator = PointerGenerator::<10>::new(); + /// let arbitrary = generator.any_alloc_status::(); + /// kani::assume(arbitrary.status == AllocationStatus::InBounds); + /// // Pointer may be unaligned, but it should be in-bounds, so it is safe to write to + /// unsafe { arbitrary.ptr.write_unaligned(kani::any()) } + /// # } + /// ``` + /// + /// The generator is parameterized by the number of bytes of its internal buffer. + /// See [pointer_generator] function if you would like to create a generator that fits + /// a minimum number of objects of a given type. Example: + /// + /// ```no_run + /// # use kani::*; + /// # #[allow(unused)] + /// # #[kani::proof] + /// # fn harness() { + /// // These generators have the same capacity of 6 bytes. + /// let generator1 = PointerGenerator::<6>::new(); + /// let generator2 = pointer_generator::(); + /// # } + /// ``` + /// + /// ## Buffer size + /// + /// The internal buffer is used to generate pointers, and its size determines the maximum + /// number of pointers it can generate without overlapping. + /// Larger values will impact the maximum distance between generated pointers. + /// + /// We recommend that you pick a size that is at least big enough to + /// cover the cases where all pointers produced are non-overlapping. + /// The buffer size in bytes must be big enough to fit distinct objects for each call + /// of generate pointer. + /// For example, generating two `*mut u8` and one `*mut u32` requires a buffer + /// of at least 6 bytes. + /// + /// This guarantees that your harness covers cases where all generated pointers + /// point to allocated positions that do not overlap. For example: + /// + /// ```no_run + /// # use kani::*; + /// # #[kani::proof] + /// # fn harness() { + /// let mut generator = PointerGenerator::<6>::new(); + /// let ptr1: *mut u8 = generator.any_in_bounds().ptr; + /// let ptr2: *mut u8 = generator.any_in_bounds().ptr; + /// let ptr3: *mut u32 = generator.any_in_bounds().ptr; + /// // This cover is satisfied. + /// cover!((ptr1 as usize) >= (ptr2 as usize) + size_of::() + /// && (ptr2 as usize) >= (ptr3 as usize) + size_of::()); + /// // As well as having overlapping pointers. + /// cover!((ptr1 as usize) == (ptr3 as usize)); + /// # } + /// ``` + /// + /// The first cover will be satisfied, since there exists at least one path where + /// the generator produces inbounds pointers that do not overlap. Such as this scenario: + /// + /// ```text + /// +--------+--------+--------+--------+--------+--------+ + /// | Byte 0 | Byte 1 | Byte 2 | Byte 3 | Byte 4 | Byte 5 | + /// +--------+--------+--------+--------+--------+--------+ + /// <--------------- ptr3 --------------><--ptr2-><--ptr1-> + /// ``` + /// + /// I.e., the generator buffer is large enough to fit all 3 objects without overlapping. + /// + /// In contrast, if we had used a size of 1 element, all calls to `any_in_bounds()` would + /// return elements that overlap, and the first cover would no longer be satisfied. + /// + /// Note that the generator requires a minimum number of 1 byte, otherwise the + /// `InBounds` case would never be covered. + /// Compilation will fail if you try to create a generator of size `0`. + /// + /// Additionally, the verification will fail if you try to generate a pointer for a type + /// with size greater than the buffer size. + /// + /// Use larger buffer size if you want to cover scenarios where the distance + /// between the generated pointers matters. + /// + /// The only caveats of using very large numbers are: + /// 1. The value cannot exceed the solver maximum object size (currently 2^48 by default), neither Rust's + /// maximum object size (`isize::MAX`). + /// 2. Larger sizes could impact performance as they can lead to an exponential increase in the number of possibilities of pointer placement within the buffer. + /// + /// # Pointer provenance + /// + /// The pointer returned in the `InBounds` and `OutOfBounds` case will have the same + /// provenance as the generator. + /// + /// Use the same generator if you want to handle cases where 2 or more pointers may overlap. E.g.: + /// ```no_run + /// # use kani::*; + /// # #[kani::proof] + /// # fn harness() { + /// let mut generator = pointer_generator::(); + /// let ptr1 = generator.any_in_bounds::().ptr; + /// let ptr2 = generator.any_in_bounds::().ptr; + /// // This cover is satisfied. + /// cover!(ptr1 == ptr2) + /// # } + /// ``` + /// + /// If you want to cover cases where two or more pointers may not have the same + /// provenance, you will need to instantiate multiple generators. + /// You can also apply non-determinism to cover cases where the pointers may or may not + /// have the same provenance. E.g.: + /// + /// ```no_run + /// # use kani::*; + /// # unsafe fn my_target(_ptr1: *const T, _ptr2: *const T) {} + /// # #[kani::proof] + /// # fn harness() { + /// let mut generator1 = pointer_generator::(); + /// let mut generator2 = pointer_generator::(); + /// let ptr1: *const char = generator1.any_in_bounds().ptr; + /// let ptr2: *const char = if kani::any() { + /// // Pointers will have same provenance and may overlap. + /// generator1.any_in_bounds().ptr + /// } else { + /// // Pointers will have different provenance and will not overlap. + /// generator2.any_in_bounds().ptr + /// }; + /// // Invoke the function under verification + /// unsafe { my_target(ptr1, ptr2) }; + /// # } + /// ``` + /// + /// # Pointer Generator vs Pointer with any address + /// + /// Creating a pointer using the generator is different than generating a pointer + /// with any address. + /// + /// I.e.: + /// ```no_run + /// # use kani::*; + /// # #[kani::proof] + /// # #[allow(unused)] + /// # fn harness() { + /// // This pointer represents any address, and it may point to anything in memory, + /// // allocated or not. + /// let ptr1 = kani::any::() as *const u8; + /// + /// // This pointer address will either point to unallocated memory, to a dead object + /// // or to allocated memory within the generator address space. + /// let mut generator = PointerGenerator::<5>::new(); + /// let ptr2: *const u8 = generator.any_alloc_status().ptr; + /// # } + /// ``` + /// + /// Kani cannot reason about a pointer allocation status (except for asserting its validity). + /// Thus, the generator was introduced to help writing harnesses that need to impose + /// constraints to the arbitrary pointer allocation status. + /// It also allow us to restrict the pointer provenance, excluding for example the address of + /// variables that are not available in the current context. + /// As a limitation, it will not cover the entire address space that a pointer can take. + /// + /// If your harness does not need to reason about pointer allocation, for example, verifying + /// pointer wrapping arithmetic, using a pointer with any address will allow you to cover + /// all possible scenarios. + #[derive(Debug)] + pub struct PointerGenerator { + // Internal allocation that may be used to generate valid pointers. + buf: MaybeUninit<[u8; BYTES]>, + } + + /// Enumeration with the cases currently covered by the pointer generator. + #[derive(Copy, Clone, Debug, PartialEq, Eq, kani::Arbitrary)] + pub enum AllocationStatus { + /// Dangling pointers + Dangling, + /// Pointer to dead object + DeadObject, + /// Null pointers + Null, + /// In bounds pointer (it may be unaligned) + InBounds, + /// The pointer cannot be read / written to for the given type since one or more bytes + /// would be out of bounds of the current allocation. + OutOfBounds, + } + + /// Holds information about a pointer that is generated non-deterministically. + #[derive(Debug)] + pub struct ArbitraryPointer<'a, T> { + /// The pointer that was generated. + pub ptr: *mut T, + /// The expected allocation status. + pub status: AllocationStatus, + /// Whether the pointer was generated with an initialized value or not. + pub is_initialized: bool, + /// Lifetime for this object. + phantom: PhantomData<&'a T>, + } + + impl PointerGenerator { + const BUF_LEN: usize = BYTES; + const VALID : () = assert!(BYTES > 0, "PointerGenerator requires at least one byte."); + + /// Create a new PointerGenerator. + #[kani::unstable_feature( + feature = "mem-predicates", + issue = 2690, + reason = "experimental memory predicates and manipulation feature" + )] + pub fn new() -> Self { + let _ = Self::VALID; + PointerGenerator { buf: MaybeUninit::uninit() } + } + + /// Creates a raw pointer with non-deterministic properties. + /// + /// The pointer returned is either dangling or has the same provenance of the generator. + #[kani::unstable_feature( + feature = "mem-predicates", + issue = 2690, + reason = "experimental memory predicates and manipulation feature" + )] + pub fn any_alloc_status<'a, T>(&'a mut self) -> ArbitraryPointer<'a, T> + where T: kani::Arbitrary + { + assert!(core::mem::size_of::() <= Self::BUF_LEN, + "Cannot generate in-bounds object of the requested type. Buffer is not big enough." + ); + + let status = kani::any(); + let ptr = match status { + AllocationStatus::Dangling => { + // Generate potentially unaligned pointer. + let offset = kani::any_where(|b: &usize| *b < size_of::()); + crate::ptr::NonNull::::dangling().as_ptr().wrapping_add(offset) + } + AllocationStatus::DeadObject => { + let mut obj: T = kani::any(); + &mut obj as *mut _ + } + AllocationStatus::Null => crate::ptr::null_mut::(), + AllocationStatus::InBounds => { + return self.create_in_bounds_ptr(); + } + AllocationStatus::OutOfBounds => { + // Generate potentially unaligned pointer. + let buf_ptr = addr_of_mut!(self.buf) as *mut u8; + let offset = kani::any_where(|b: &usize| *b < size_of::()); + unsafe { buf_ptr.add(Self::BUF_LEN - offset) as *mut T } + } + }; + + ArbitraryPointer { + ptr, + is_initialized: false, + status, + phantom: PhantomData, + } + } + + /// Creates a in-bounds raw pointer with non-deterministic properties. + /// + /// The pointer points to an allocated location with the same provenance of the generator. + /// The pointer may be unaligned, and the pointee may be uninitialized. + /// + /// ```no_run + /// # use kani::*; + /// # #[kani::proof] + /// # fn check_distance() { + /// let mut generator = PointerGenerator::<6>::new(); + /// let ptr1: *mut u8 = generator.any_in_bounds().ptr; + /// let ptr2: *mut u8 = generator.any_in_bounds().ptr; + /// // SAFETY: Both pointers have the same provenance. + /// let distance = unsafe { ptr1.offset_from(ptr2) }; + /// assert!(distance > -5 && distance < 5) + /// # } + /// ``` + #[kani::unstable_feature( + feature = "mem-predicates", + issue = 2690, + reason = "experimental memory predicates and manipulation feature" + )] + pub fn any_in_bounds<'a, T>(&'a mut self) -> ArbitraryPointer<'a, T> + where T: kani::Arbitrary { + assert!(core::mem::size_of::() <= Self::BUF_LEN, + "Cannot generate in-bounds object of the requested type. Buffer is not big enough." + ); + self.create_in_bounds_ptr() + } + + /// This is the inner logic to create an arbitrary pointer that is inbounds. + /// + /// Note that pointer may be unaligned. + fn create_in_bounds_ptr<'a, T>(&'a mut self) -> ArbitraryPointer<'a, T> + where T: kani::Arbitrary { + assert!(core::mem::size_of::() <= Self::BUF_LEN, + "Cannot generate in-bounds object of the requested type. Buffer is not big enough." + ); + let buf_ptr = addr_of_mut!(self.buf) as *mut u8; + let offset = kani::any_where(|b: &usize| *b <= Self::BUF_LEN - size_of::()); + let ptr = unsafe { buf_ptr.add(offset) as *mut T }; + let is_initialized = kani::any(); + if is_initialized { + unsafe { ptr.write_unaligned(kani::any()) }; + } + ArbitraryPointer { + ptr, + is_initialized, + status: AllocationStatus::InBounds, + phantom: PhantomData, + } + } + } + + kani_core::ptr_generator_fn!(); + }; +} + +#[cfg(not(feature = "no_core"))] +#[macro_export] +macro_rules! ptr_generator_fn { + () => { + /// Create a pointer generator that fits at least `N` elements of type `T`. + pub fn pointer_generator() + -> PointerGenerator<{ size_of::() * NUM_ELTS }> { + PointerGenerator::<{ size_of::() * NUM_ELTS }>::new() + } + }; +} + +/// Don't generate the pointer_generator function here since it requires generic constant +/// expression. +#[cfg(feature = "no_core")] +#[macro_export] +macro_rules! ptr_generator_fn { + () => {}; +} diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index 5df8f2228c62..839313f084c2 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -42,6 +42,7 @@ macro_rules! kani_lib { pub use kani_core::*; kani_core::kani_intrinsics!(core); kani_core::generate_arbitrary!(core); + kani_core::check_intrinsic!(); pub mod mem { kani_core::kani_mem!(core); @@ -58,6 +59,10 @@ macro_rules! kani_lib { kani_core::kani_intrinsics!(std); kani_core::generate_arbitrary!(std); + kani_core::check_intrinsic! { + msg="This API will be made private in future releases.", vis=pub + } + pub mod mem { kani_core::kani_mem!(std); } @@ -85,7 +90,7 @@ macro_rules! kani_intrinsics { /// /// The code snippet below should never panic. /// - /// ```rust + /// ```no_run /// let i : i32 = kani::any(); /// kani::assume(i > 10); /// if i < 0 { @@ -95,7 +100,7 @@ macro_rules! kani_intrinsics { /// /// The following code may panic though: /// - /// ```rust + /// ```no_run /// let i : i32 = kani::any(); /// assert!(i < 0, "This may panic and verification should fail."); /// kani::assume(i > 10); @@ -118,7 +123,7 @@ macro_rules! kani_intrinsics { /// /// # Example: /// - /// ```rust + /// ```no_run /// let x: bool = kani::any(); /// let y = !x; /// kani::assert(x || y, "ORing a boolean variable with its negation must be true") @@ -138,35 +143,15 @@ macro_rules! kani_intrinsics { assert!(cond, "{}", msg); } - /// Creates an assertion of the specified condition and message, but does not assume it afterwards. - /// - /// # Example: - /// - /// ```rust - /// let x: bool = kani::any(); - /// let y = !x; - /// kani::check(x || y, "ORing a boolean variable with its negation must be true") - /// ``` - #[cfg(not(feature = "concrete_playback"))] - #[inline(never)] - #[rustc_diagnostic_item = "KaniCheck"] - pub const fn check(cond: bool, msg: &'static str) { - let _ = cond; - let _ = msg; - } - - #[cfg(feature = "concrete_playback")] - #[inline(never)] - #[rustc_diagnostic_item = "KaniCheck"] - pub const fn check(cond: bool, msg: &'static str) { - assert!(cond, "{}", msg); - } - /// Creates a cover property with the specified condition and message. /// /// # Example: /// - /// ```rust + /// ```no_run + /// # use crate::kani; + /// # + /// # let array: [u8; 10] = kani::any(); + /// # let slice = kani::slice::any_slice_of_array(&array); /// kani::cover(slice.len() == 0, "The slice may have a length of 0"); /// ``` /// @@ -193,7 +178,11 @@ macro_rules! kani_intrinsics { /// In the snippet below, we are verifying the behavior of the function `fn_under_verification` /// under all possible `NonZeroU8` input values, i.e., all possible `u8` values except zero. /// - /// ```rust + /// ```no_run + /// # use std::num::NonZeroU8; + /// # use crate::kani; + /// # + /// # fn fn_under_verification(_: NonZeroU8) {} /// let inputA = kani::any::(); /// fn_under_verification(inputA); /// ``` @@ -231,7 +220,11 @@ macro_rules! kani_intrinsics { /// In the snippet below, we are verifying the behavior of the function `fn_under_verification` /// under all possible `u8` input values between 0 and 12. /// - /// ```rust + /// ```no_run + /// # use std::num::NonZeroU8; + /// # use crate::kani; + /// # + /// # fn fn_under_verification(_: u8) {} /// let inputA: u8 = kani::any_where(|x| *x < 12); /// fn_under_verification(inputA); /// ``` @@ -460,3 +453,48 @@ macro_rules! kani_intrinsics { } }; } + +#[macro_export] +macro_rules! check_intrinsic { + ($(msg=$msg:literal, vis=$vis:vis)?) => { + /// Creates a non-fatal property with the specified condition and message. + /// + /// This check will not impact the program control flow even when it fails. + /// + /// # Example: + /// + /// ```no_run + /// let x: bool = kani::any(); + /// let y = !x; + /// kani::check(x || y, "ORing a boolean variable with its negation must be true"); + /// kani::check(x == y, "A boolean variable is always different than its negation"); + /// kani::cover!(true, "This should still be reachable"); + /// ``` + /// + /// # Deprecated + /// + /// This function was meant to be internal only, and it was added to Kani's public interface + /// by mistake. Thus, it will be made private in future releases. + /// Instead, we recommend users to either use `assert` or `cover` to create properties they + /// would like to verify. + /// + /// See for more details. + #[cfg(not(feature = "concrete_playback"))] + #[inline(never)] + #[rustc_diagnostic_item = "KaniCheck"] + // TODO: Remove the `#![allow(deprecated)]` inside kani's crate once this is made private. + $(#[deprecated(since="0.55.0", note=$msg)])? + $($vis)? const fn check(cond: bool, msg: &'static str) { + let _ = cond; + let _ = msg; + } + + #[cfg(feature = "concrete_playback")] + #[inline(never)] + #[rustc_diagnostic_item = "KaniCheck"] + $(#[deprecated(since="0.55.0", note=$msg)])? + $($vis)? const fn check(cond: bool, msg: &'static str) { + assert!(cond, "{}", msg); + } + }; +} diff --git a/library/kani_macros/Cargo.toml b/library/kani_macros/Cargo.toml index 6930366b84fc..a7876176adb2 100644 --- a/library/kani_macros/Cargo.toml +++ b/library/kani_macros/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_macros" -version = "0.55.0" +version = "0.56.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/kani_macros/src/derive.rs b/library/kani_macros/src/derive.rs index 04b288069387..258afc36af77 100644 --- a/library/kani_macros/src/derive.rs +++ b/library/kani_macros/src/derive.rs @@ -18,10 +18,37 @@ use syn::{ parse_quote, }; +#[cfg(feature = "no_core")] +macro_rules! kani_path { + ($span:expr) => { + quote_spanned! { $span => core::kani } + }; + () => { + quote! { core::kani } + }; +} + +#[cfg(not(feature = "no_core"))] +macro_rules! kani_path { + ($span:expr) => { + quote_spanned! { $span => kani } + }; + () => { + quote! { kani } + }; +} + +/// Generate the Arbitrary implementation for the given type. +/// +/// Note that we cannot use `proc_macro_crate::crate_name()` to discover the name for `kani` crate +/// since we define it as an extern crate via `rustc` command line. +/// +/// In order to support core, we check the `no_core` feature. pub fn expand_derive_arbitrary(item: proc_macro::TokenStream) -> proc_macro::TokenStream { let trait_name = "Arbitrary"; let derive_item = parse_macro_input!(item as DeriveInput); let item_name = &derive_item.ident; + let kani_path = kani_path!(); let body = fn_any_body(&item_name, &derive_item.data); // Get the safety constraints (if any) to produce type-safe values @@ -36,11 +63,11 @@ pub fn expand_derive_arbitrary(item: proc_macro::TokenStream) -> proc_macro::Tok let field_refs = field_refs(&item_name, &derive_item.data); quote! { // The generated implementation. - impl #impl_generics kani::Arbitrary for #item_name #ty_generics #where_clause { + impl #impl_generics #kani_path::Arbitrary for #item_name #ty_generics #where_clause { fn any() -> Self { let obj = #body; #field_refs - kani::assume(#safety_conds); + #kani_path::assume(#safety_conds); obj } } @@ -48,7 +75,7 @@ pub fn expand_derive_arbitrary(item: proc_macro::TokenStream) -> proc_macro::Tok } else { quote! { // The generated implementation. - impl #impl_generics kani::Arbitrary for #item_name #ty_generics #where_clause { + impl #impl_generics #kani_path::Arbitrary for #item_name #ty_generics #where_clause { fn any() -> Self { #body } @@ -60,9 +87,10 @@ pub fn expand_derive_arbitrary(item: proc_macro::TokenStream) -> proc_macro::Tok /// Add a bound `T: Arbitrary` to every type parameter T. fn add_trait_bound_arbitrary(mut generics: Generics) -> Generics { + let kani_path = kani_path!(); generics.params.iter_mut().for_each(|param| { if let GenericParam::Type(type_param) = param { - type_param.bounds.push(parse_quote!(kani::Arbitrary)); + type_param.bounds.push(parse_quote!(#kani_path::Arbitrary)); } }); generics @@ -222,8 +250,10 @@ fn init_symbolic_item(ident: &Ident, fields: &Fields) -> TokenStream { // Expands to an expression like // Self(kani::any(), kani::any(), ..., kani::any()); let init = fields.unnamed.iter().map(|field| { - quote_spanned! {field.span()=> - kani::any() + let span = field.span(); + let kani_path = kani_path!(span); + quote_spanned! {span=> + #kani_path::any() } }); quote! { @@ -349,8 +379,9 @@ fn fn_any_enum(ident: &Ident, data: &DataEnum) -> TokenStream { } }); + let kani_path = kani_path!(); quote! { - match kani::any() { + match #kani_path::any() { #(#arms)* } } @@ -376,6 +407,7 @@ pub fn expand_derive_invariant(item: proc_macro::TokenStream) -> proc_macro::Tok let trait_name = "Invariant"; let derive_item = parse_macro_input!(item as DeriveInput); let item_name = &derive_item.ident; + let kani_path = kani_path!(); let safe_body = safe_body_with_calls(&item_name, &derive_item, trait_name); let field_refs = field_refs(&item_name, &derive_item.data); @@ -387,7 +419,7 @@ pub fn expand_derive_invariant(item: proc_macro::TokenStream) -> proc_macro::Tok let expanded = quote! { // The generated implementation. - impl #impl_generics kani::Invariant for #item_name #ty_generics #where_clause { + impl #impl_generics #kani_path::Invariant for #item_name #ty_generics #where_clause { fn is_safe(&self) -> bool { let obj = self; #field_refs @@ -463,9 +495,10 @@ fn has_field_safety_constraints_inner(_ident: &Ident, fields: &Fields) -> bool { /// Add a bound `T: Invariant` to every type parameter T. pub fn add_trait_bound_invariant(mut generics: Generics) -> Generics { + let kani_path = kani_path!(); generics.params.iter_mut().for_each(|param| { if let GenericParam::Type(type_param) = param { - type_param.bounds.push(parse_quote!(kani::Invariant)); + type_param.bounds.push(parse_quote!(#kani_path::Invariant)); } }); generics diff --git a/library/std/Cargo.toml b/library/std/Cargo.toml index 12c923e9b655..e1e353704723 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.55.0" +version = "0.56.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/rust-toolchain.toml b/rust-toolchain.toml index c0fba0261fa7..7ef640dbfdc9 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2024-10-01" +channel = "nightly-2024-10-03" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] diff --git a/rustfmt.toml b/rustfmt.toml index 44cbfe4a3dc9..f895fafbbdef 100644 --- a/rustfmt.toml +++ b/rustfmt.toml @@ -15,4 +15,5 @@ ignore = [ # For some reason, this is not working without the directory wildcard. "**/firecracker", "**/tests/perf/s2n-quic/", + "**/charon/charon/", ] diff --git a/scripts/codegen-firecracker.sh b/scripts/codegen-firecracker.sh index 3ac7dfa6585d..bffb27023412 100755 --- a/scripts/codegen-firecracker.sh +++ b/scripts/codegen-firecracker.sh @@ -42,7 +42,7 @@ RUST_FLAGS=( "--kani-compiler" "-Cpanic=abort" "-Zalways-encode-mir" - "-Cllvm-args=--goto-c" + "-Cllvm-args=--backend=cprover" "-Cllvm-args=--ignore-global-asm" "-Cllvm-args=--reachability=pub_fns" "--sysroot=${KANI_DIR}/target/kani" diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh index bd6b04d7386e..be2548235ce6 100755 --- a/scripts/kani-regression.sh +++ b/scripts/kani-regression.sh @@ -41,8 +41,8 @@ cargo test -p cprover_bindings cargo test -p kani-compiler cargo test -p kani-driver cargo test -p kani_metadata -# skip doc tests and enable assertions to fail -cargo test -p kani --lib --features concrete_playback +# Use concrete playback to enable assertions failure +cargo test -p kani --features concrete_playback # Test the actual macros, skipping doc tests and enabling extra traits for "syn" # so we can debug print AST RUSTFLAGS=--cfg=kani_sysroot cargo test -p kani_macros --features syn/extra-traits --lib diff --git a/scripts/std-lib-regression.sh b/scripts/std-lib-regression.sh index a7881f1dc19a..b010da4581f6 100755 --- a/scripts/std-lib-regression.sh +++ b/scripts/std-lib-regression.sh @@ -71,7 +71,7 @@ RUST_FLAGS=( "--kani-compiler" "-Cpanic=abort" "-Zalways-encode-mir" - "-Cllvm-args=--goto-c" + "-Cllvm-args=--backend=cprover" "-Cllvm-args=--ignore-global-asm" "-Cllvm-args=--reachability=pub_fns" "-Cllvm-args=--build-std" diff --git a/tests/cargo-kani/asm/global/Cargo.toml b/tests/cargo-kani/asm/global/Cargo.toml index 21ff904a2f99..79ffab9377c1 100644 --- a/tests/cargo-kani/asm/global/Cargo.toml +++ b/tests/cargo-kani/asm/global/Cargo.toml @@ -13,4 +13,4 @@ crate_with_global_asm = { path = "crate_with_global_asm" } [package.metadata.kani] # Issue with MIR Linker on static constant. -flags = { enable-unstable = true, ignore-global-asm = true, mir-linker = true } +flags = { enable-unstable = true, ignore-global-asm = true } diff --git a/tests/cargo-kani/mir-linker/Cargo.toml b/tests/cargo-kani/mir-linker/Cargo.toml index 39d5016a407b..f00d4c687864 100644 --- a/tests/cargo-kani/mir-linker/Cargo.toml +++ b/tests/cargo-kani/mir-linker/Cargo.toml @@ -8,6 +8,3 @@ description = "Ensures that the mir-linker works accross crates" [dependencies] semver = "1.0" - -[package.metadata.kani] -flags = { mir-linker=true, enable-unstable=true } diff --git a/tests/cargo-ui/supported-lib-types/cdylib-rlib/Cargo.toml b/tests/cargo-ui/supported-lib-types/cdylib-rlib/Cargo.toml new file mode 100644 index 000000000000..fcf91e061e57 --- /dev/null +++ b/tests/cargo-ui/supported-lib-types/cdylib-rlib/Cargo.toml @@ -0,0 +1,13 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +[package] +name = "supported-lib" +version = "0.1.0" +edition = "2021" +description = "Test that Kani correctly handle supported crate types" + +[lib] +name = "lib" +crate-type = ["cdylib", "rlib"] +path = "../src/lib.rs" + diff --git a/tests/cargo-ui/supported-lib-types/cdylib-rlib/expected b/tests/cargo-ui/supported-lib-types/cdylib-rlib/expected new file mode 100644 index 000000000000..426470e8702c --- /dev/null +++ b/tests/cargo-ui/supported-lib-types/cdylib-rlib/expected @@ -0,0 +1,2 @@ +Checking harness check_ok... +VERIFICATION:- SUCCESSFUL diff --git a/tests/cargo-ui/ws-integ-tests/Cargo.toml b/tests/cargo-ui/ws-integ-tests/Cargo.toml index b09d4c9a5f19..93c4baebe120 100644 --- a/tests/cargo-ui/ws-integ-tests/Cargo.toml +++ b/tests/cargo-ui/ws-integ-tests/Cargo.toml @@ -15,5 +15,3 @@ members = [ [workspace.metadata.kani.flags] workspace = true tests = true -enable-unstable=true -mir-linker=true diff --git a/tests/expected/arbitrary/ptrs/pointer_generator.expected b/tests/expected/arbitrary/ptrs/pointer_generator.expected new file mode 100644 index 000000000000..4627d354aebb --- /dev/null +++ b/tests/expected/arbitrary/ptrs/pointer_generator.expected @@ -0,0 +1,21 @@ +Checking harness check_arbitrary_ptr... + +Status: SUCCESS\ +Description: ""OutOfBounds"" + +Status: SUCCESS\ +Description: ""InBounds"" + +Status: SUCCESS\ +Description: ""NullPtr"" + +Status: FAILURE\ +Description: ""DeadObject"" + +Status: SATISFIED\ +Description: "Dangling" + +Status: UNREACHABLE\ +Description: ""Dangling write"" + +Verification failed for - check_arbitrary_ptr diff --git a/tests/expected/arbitrary/ptrs/pointer_generator.rs b/tests/expected/arbitrary/ptrs/pointer_generator.rs new file mode 100644 index 000000000000..214c7fad2bfa --- /dev/null +++ b/tests/expected/arbitrary/ptrs/pointer_generator.rs @@ -0,0 +1,38 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// kani-flags: -Z mem-predicates +//! Check the behavior of the new `PointerGenerator`. +extern crate kani; + +use kani::{AllocationStatus, PointerGenerator, cover}; + +/// Harness that checks that all cases are covered and the code behaves as expected. +/// +/// Note that for `DeadObject`, `Dangling`, and `OutOfBounds` the predicate will fail due to demonic non-determinism. +#[kani::proof] +fn check_arbitrary_ptr() { + let mut generator = PointerGenerator::<10>::new(); + let arbitrary = generator.any_alloc_status::(); + let ptr = arbitrary.ptr; + match arbitrary.status { + AllocationStatus::Dangling => { + cover!(true, "Dangling"); + assert!(!kani::mem::can_write_unaligned(ptr), "Dangling write"); + } + AllocationStatus::Null => { + assert!(!kani::mem::can_write_unaligned(ptr), "NullPtr"); + } + AllocationStatus::DeadObject => { + // Due to demonic non-determinism, the API will trigger an error. + assert!(!kani::mem::can_write_unaligned(ptr), "DeadObject"); + } + AllocationStatus::OutOfBounds => { + assert!(!kani::mem::can_write_unaligned(ptr), "OutOfBounds"); + } + AllocationStatus::InBounds => { + // This should always succeed + assert!(kani::mem::can_write_unaligned(ptr), "InBounds"); + } + }; +} diff --git a/tests/expected/arbitrary/ptrs/pointer_generator_error.expected b/tests/expected/arbitrary/ptrs/pointer_generator_error.expected new file mode 100644 index 000000000000..a0592c586a03 --- /dev/null +++ b/tests/expected/arbitrary/ptrs/pointer_generator_error.expected @@ -0,0 +1,9 @@ +error[E0080]: evaluation of `kani::PointerGenerator::<0>::VALID` failed\ + +the evaluated program panicked at 'PointerGenerator requires at least one byte.' + +note: the above error was encountered while instantiating `fn kani::PointerGenerator::<0>::new`\ +pointer_generator_error.rs\ +|\ +| let _generator = PointerGenerator::<0>::new();\ +| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/tests/expected/arbitrary/ptrs/pointer_generator_error.rs b/tests/expected/arbitrary/ptrs/pointer_generator_error.rs new file mode 100644 index 000000000000..30b50f3699e3 --- /dev/null +++ b/tests/expected/arbitrary/ptrs/pointer_generator_error.rs @@ -0,0 +1,12 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// kani-flags: -Z mem-predicates +//! Check misusage of pointer generator fails compilation. +extern crate kani; + +use kani::PointerGenerator; + +pub fn check_invalid_generator() { + let _generator = PointerGenerator::<0>::new(); +} diff --git a/tests/expected/arbitrary/ptrs/pointer_inbounds.expected b/tests/expected/arbitrary/ptrs/pointer_inbounds.expected new file mode 100644 index 000000000000..838829163a36 --- /dev/null +++ b/tests/expected/arbitrary/ptrs/pointer_inbounds.expected @@ -0,0 +1,39 @@ +Checking harness check_overlap... + +Status: SATISFIED\ +Description: "Same" + +Status: SATISFIED\ +Description: "Overlap" + +Status: SATISFIED\ +Description: "Greater" + +Status: SATISFIED\ +Description: "Smaller" + +Checking harness check_alignment... + +Status: SUCCESS\ +Description: ""Aligned"" + +Status: SUCCESS\ +Description: ""Unaligned"" + +Checking harness check_inbounds_initialized... + +Status: SUCCESS\ +Description: ""ValidRead"" + +Checking harness check_inbounds... + +Status: SATISFIED\ +Description: "Uninitialized" + +Status: SATISFIED\ +Description: "Initialized" + +Status: SUCCESS\ +Description: ""ValidWrite"" + +Complete - 4 successfully verified harnesses, 0 failures, 4 total. diff --git a/tests/expected/arbitrary/ptrs/pointer_inbounds.rs b/tests/expected/arbitrary/ptrs/pointer_inbounds.rs new file mode 100644 index 000000000000..36e4abeff48b --- /dev/null +++ b/tests/expected/arbitrary/ptrs/pointer_inbounds.rs @@ -0,0 +1,56 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// kani-flags: -Z mem-predicates +//! Check different cases for `PointerGenerator` for in-bounds pointers. +//! TODO: Enable initialization checks (`-Z uninit-checks`) once we add support to unions. +//! The current instrumentation does not work in the presence of MaybeUninit which we use +//! to implement PointerGenerator. +//! Kani will detect the usage of MaybeUninit and fail the verification. +extern crate kani; + +use kani::PointerGenerator; + +#[kani::proof] +fn check_inbounds() { + let mut generator = kani::pointer_generator::(); + let ptr = generator.any_in_bounds::().ptr; + kani::cover!(!kani::mem::can_read_unaligned(ptr), "Uninitialized"); + kani::cover!(kani::mem::can_read_unaligned(ptr), "Initialized"); + assert!(kani::mem::can_write_unaligned(ptr), "ValidWrite"); +} + +#[kani::proof] +fn check_inbounds_initialized() { + let mut generator = kani::pointer_generator::(); + let arbitrary = generator.any_in_bounds::(); + kani::assume(arbitrary.is_initialized); + assert!(kani::mem::can_read_unaligned(arbitrary.ptr), "ValidRead"); +} + +#[kani::proof] +fn check_alignment() { + let mut generator = kani::pointer_generator::(); + let ptr: *mut char = generator.any_in_bounds().ptr; + if ptr.is_aligned() { + assert!(kani::mem::can_write(ptr), "Aligned"); + } else { + assert!(!kani::mem::can_write(ptr), "Not aligned"); + assert!(kani::mem::can_write_unaligned(ptr), "Unaligned"); + } +} + +#[kani::proof] +fn check_overlap() { + let mut generator = kani::pointer_generator::(); + let ptr_1 = generator.any_in_bounds::().ptr; + let ptr_2 = generator.any_in_bounds::().ptr; + kani::cover!(ptr_1 == ptr_2, "Same"); + kani::cover!(ptr_1 == unsafe { ptr_2.byte_add(1) }, "Overlap"); + + let distance = unsafe { ptr_1.offset_from(ptr_2) }; + kani::cover!(distance > 0, "Greater"); + kani::cover!(distance < 0, "Smaller"); + + assert!(distance >= -4 && distance <= 4, "Expected a maximum distance of 4 elements"); +} diff --git a/tests/expected/llbc/basic0/expected b/tests/expected/llbc/basic0/expected new file mode 100644 index 000000000000..112a67a21548 --- /dev/null +++ b/tests/expected/llbc/basic0/expected @@ -0,0 +1,8 @@ +fn test::is_zero(@1: i32) -> bool\ +{\ + let @0: bool; // return\ + let @1: i32; // arg #1\ + + @0 := copy (@1) == const (0 : i32)\ + return\ +} diff --git a/tests/expected/llbc/basic0/test.rs b/tests/expected/llbc/basic0/test.rs new file mode 100644 index 000000000000..5025994ab31c --- /dev/null +++ b/tests/expected/llbc/basic0/test.rs @@ -0,0 +1,15 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zaeneas --print-llbc + +//! This test checks that Kani's LLBC backend handles basic expressions, in this +//! case an equality between a variable and a constant + +fn is_zero(i: i32) -> bool { + i == 0 +} + +#[kani::proof] +fn main() { + let _ = is_zero(0); +} diff --git a/tests/expected/llbc/basic1/expected b/tests/expected/llbc/basic1/expected new file mode 100644 index 000000000000..9cb0bef6f7c6 --- /dev/null +++ b/tests/expected/llbc/basic1/expected @@ -0,0 +1,15 @@ +fn test::select(@1: bool, @2: i32, @3: i32) -> i32 +{ + let @0: i32; // return + let @1: bool; // arg #1 + let @2: i32; // arg #2 + let @3: i32; // arg #3 + + if copy (@1) { + @0 := copy (@2) + } + else { + @0 := copy (@3) + } + return +} diff --git a/tests/expected/llbc/basic1/test.rs b/tests/expected/llbc/basic1/test.rs new file mode 100644 index 000000000000..92818fb93bfb --- /dev/null +++ b/tests/expected/llbc/basic1/test.rs @@ -0,0 +1,15 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zaeneas --print-llbc + +//! This test checks that Kani's LLBC backend handles basic expressions, in this +//! case an if condition + +fn select(s: bool, x: i32, y: i32) -> i32 { + if s { x } else { y } +} + +#[kani::proof] +fn main() { + let _ = select(true, 3, 7); +} diff --git a/tests/kani/UnsizedCoercion/basic_coercion.rs b/tests/kani/UnsizedCoercion/basic_coercion.rs index a60a76aec3be..ee8c80e87011 100644 --- a/tests/kani/UnsizedCoercion/basic_coercion.rs +++ b/tests/kani/UnsizedCoercion/basic_coercion.rs @@ -1,6 +1,5 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --mir-linker --enable-unstable //! Check the basic coercion from using built-in references and pointers. //! Tests are broken down into different crates to ensure that the reachability works for each case. diff --git a/tests/kani/UnsizedCoercion/basic_inner_coercion.rs b/tests/kani/UnsizedCoercion/basic_inner_coercion.rs index efc84b61ea1e..19d8f39fed7e 100644 --- a/tests/kani/UnsizedCoercion/basic_inner_coercion.rs +++ b/tests/kani/UnsizedCoercion/basic_inner_coercion.rs @@ -1,6 +1,5 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --mir-linker --enable-unstable //! Check the basic coercion from using built-in references and pointers. //! Tests are broken down into different crates to ensure that the reachability works for each case. diff --git a/tests/kani/UnsizedCoercion/basic_outer_coercion.rs b/tests/kani/UnsizedCoercion/basic_outer_coercion.rs index a2b5bfae3129..633dfbdaa995 100644 --- a/tests/kani/UnsizedCoercion/basic_outer_coercion.rs +++ b/tests/kani/UnsizedCoercion/basic_outer_coercion.rs @@ -1,6 +1,5 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --mir-linker --enable-unstable //! Check the basic coercion from using built-in references and pointers. //! Tests are broken down into different crates to ensure that the reachability works for each case. diff --git a/tests/kani/UnsizedCoercion/box_coercion.rs b/tests/kani/UnsizedCoercion/box_coercion.rs index e022bdef06e1..106f586f8eed 100644 --- a/tests/kani/UnsizedCoercion/box_coercion.rs +++ b/tests/kani/UnsizedCoercion/box_coercion.rs @@ -1,6 +1,5 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --mir-linker --enable-unstable //! Check the basic coercion when using boxes. //! Tests are broken down into different crates to ensure that the reachability works for each case. diff --git a/tests/kani/UnsizedCoercion/box_inner_coercion.rs b/tests/kani/UnsizedCoercion/box_inner_coercion.rs index 35f10373d5ef..4e8a8b56624c 100644 --- a/tests/kani/UnsizedCoercion/box_inner_coercion.rs +++ b/tests/kani/UnsizedCoercion/box_inner_coercion.rs @@ -1,6 +1,5 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --mir-linker --enable-unstable //! Check the basic coercion when using boxes. //! Tests are broken down into different crates to ensure that the reachability works for each case. diff --git a/tests/kani/UnsizedCoercion/box_outer_coercion.rs b/tests/kani/UnsizedCoercion/box_outer_coercion.rs index 586f54003cdf..2d91360cd576 100644 --- a/tests/kani/UnsizedCoercion/box_outer_coercion.rs +++ b/tests/kani/UnsizedCoercion/box_outer_coercion.rs @@ -1,6 +1,5 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --mir-linker --enable-unstable //! Check the basic coercion when using boxes. //! Tests are broken down into different crates to ensure that the reachability works for each case. mod defs; diff --git a/tests/kani/UnsizedCoercion/custom_outer_coercion.rs b/tests/kani/UnsizedCoercion/custom_outer_coercion.rs index 7f7d68ef6e84..6d75204223c1 100644 --- a/tests/kani/UnsizedCoercion/custom_outer_coercion.rs +++ b/tests/kani/UnsizedCoercion/custom_outer_coercion.rs @@ -1,6 +1,5 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --mir-linker --enable-unstable //! Check the basic coercion when using a custom CoerceUnsized implementation. //! Tests are broken down into different crates to ensure that the reachability works for each case. #![feature(coerce_unsized)] diff --git a/tests/kani/UnsizedCoercion/double_coercion.rs b/tests/kani/UnsizedCoercion/double_coercion.rs index 26cfb585821e..76158c811c00 100644 --- a/tests/kani/UnsizedCoercion/double_coercion.rs +++ b/tests/kani/UnsizedCoercion/double_coercion.rs @@ -1,6 +1,5 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --mir-linker --enable-unstable //! Check the basic coercion when using box of box. //! Tests are broken down into different crates to ensure that the reachability works for each case. diff --git a/tests/kani/UnsizedCoercion/rc_outer_coercion.rs b/tests/kani/UnsizedCoercion/rc_outer_coercion.rs index 2543498cca80..7a608d7d1d57 100644 --- a/tests/kani/UnsizedCoercion/rc_outer_coercion.rs +++ b/tests/kani/UnsizedCoercion/rc_outer_coercion.rs @@ -1,6 +1,5 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --mir-linker --enable-unstable //! Check the basic coercion from using reference counter. //! Tests are broken down into different crates to ensure that the reachability works for each case. mod defs; diff --git a/tests/kani/UnsizedCoercion/trait_to_trait_coercion.rs b/tests/kani/UnsizedCoercion/trait_to_trait_coercion.rs index 32875f8b8e22..b7750db487e2 100644 --- a/tests/kani/UnsizedCoercion/trait_to_trait_coercion.rs +++ b/tests/kani/UnsizedCoercion/trait_to_trait_coercion.rs @@ -1,6 +1,5 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --mir-linker --enable-unstable //! Check the basic coercion from using built-in references and pointers. //! Tests are broken down into different crates to ensure that the reachability works for each case. diff --git a/tests/perf/s2n-quic b/tests/perf/s2n-quic index 2a735a983a54..17171ece180d 160000 --- a/tests/perf/s2n-quic +++ b/tests/perf/s2n-quic @@ -1 +1 @@ -Subproject commit 2a735a983a5426b13c926d19090d32ea0a99ea36 +Subproject commit 17171ece180d6512f21dd98cdc8637e33646d994 diff --git a/tests/perf/string/src/any_str.rs b/tests/perf/string/src/any_str.rs index 3b58d56750a7..6b3f9cffbc37 100644 --- a/tests/perf/string/src/any_str.rs +++ b/tests/perf/string/src/any_str.rs @@ -1,10 +1,5 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// -// kani-flags: --enable-unstable --mir-linker -// -//! This test is to check MIR linker state of the art. -//! I.e.: Currently, this should fail with missing function definition. #[kani::proof] #[kani::unwind(4)] diff --git a/tests/script-based-pre/verify_std_cmd/verify_core.rs b/tests/script-based-pre/verify_std_cmd/verify_core.rs index 9bdabb32dde3..551345653c7b 100644 --- a/tests/script-based-pre/verify_std_cmd/verify_core.rs +++ b/tests/script-based-pre/verify_std_cmd/verify_core.rs @@ -76,4 +76,15 @@ pub mod verify { unsafe fn add_one(inout: *mut [u32]) { inout.as_mut_unchecked().iter_mut().for_each(|e| *e += 1) } + + /// Test that arbitrary pointer works as expected. + /// Disable it for uninit checks, since these checks do not support `MaybeUninit` which is used + /// by the pointer generator. + #[kani::proof] + #[cfg(not(uninit_checks))] + fn check_any_ptr() { + let mut generator = kani::PointerGenerator::<8>::new(); + let ptr = generator.any_in_bounds::().ptr; + assert!(kani::mem::can_write_unaligned(ptr)); + } } diff --git a/tests/script-based-pre/verify_std_cmd/verify_std.expected b/tests/script-based-pre/verify_std_cmd/verify_std.expected index 16705ffcfefa..3c1f474af0e7 100644 --- a/tests/script-based-pre/verify_std_cmd/verify_std.expected +++ b/tests/script-based-pre/verify_std_cmd/verify_std.expected @@ -1,3 +1,7 @@ +[TEST] Only codegen inside library folder +No kani crate inside Cargo.toml as expected + + [TEST] Run kani verify-std Checking harness verify::dummy_proof... @@ -15,10 +19,13 @@ VERIFICATION:- SUCCESSFUL Checking harness verify::check_swap_tuple... VERIFICATION:- SUCCESSFUL +Checking harness verify::check_any_ptr... +VERIFICATION:- SUCCESSFUL + Checking harness num::verify::check_non_zero... VERIFICATION:- SUCCESSFUL -Complete - 6 successfully verified harnesses, 0 failures, 6 total. +Complete - 7 successfully verified harnesses, 0 failures, 7 total. [TEST] Run kani verify-std -Z uninit-checks diff --git a/tests/script-based-pre/verify_std_cmd/verify_std.sh b/tests/script-based-pre/verify_std_cmd/verify_std.sh index f06e8a8f9921..e7276867a2a5 100755 --- a/tests/script-based-pre/verify_std_cmd/verify_std.sh +++ b/tests/script-based-pre/verify_std_cmd/verify_std.sh @@ -50,12 +50,44 @@ cp ${TMP_DIR}/library/std/src/lib.rs ${TMP_DIR}/std_lib.rs echo '#![cfg_attr(kani, feature(kani))]' > ${TMP_DIR}/library/std/src/lib.rs cat ${TMP_DIR}/std_lib.rs >> ${TMP_DIR}/library/std/src/lib.rs +# Test that the command works inside the library folder and does not change +# the existing workspace +# See https://github.com/model-checking/kani/issues/3574 +echo "[TEST] Only codegen inside library folder" +pushd "${TMP_DIR}/library" >& /dev/null +RUSTFLAGS="--cfg=uninit_checks" kani verify-std \ + -Z unstable-options \ + . \ + -Z function-contracts \ + -Z stubbing \ + -Z mem-predicates \ + --only-codegen +popd +# Grep should not find anything and exit status is 1. +grep -c kani ${TMP_DIR}/library/Cargo.toml \ + && echo "Unexpected kani crate inside Cargo.toml" \ + || echo "No kani crate inside Cargo.toml as expected" + echo "[TEST] Run kani verify-std" export RUST_BACKTRACE=1 -kani verify-std -Z unstable-options "${TMP_DIR}/library" --target-dir "${TMP_DIR}/target" -Z function-contracts -Z stubbing -Z mem-predicates +kani verify-std \ + -Z unstable-options \ + "${TMP_DIR}/library" \ + --target-dir "${TMP_DIR}/target" \ + -Z function-contracts \ + -Z stubbing \ + -Z mem-predicates +# Test that uninit-checks basic setup works on a no-core library echo "[TEST] Run kani verify-std -Z uninit-checks" -RUSTFLAGS="--cfg=uninit_checks" kani verify-std -Z unstable-options "${TMP_DIR}/library" --target-dir "${TMP_DIR}/target" -Z function-contracts -Z stubbing -Z mem-predicates -Z uninit-checks +RUSTFLAGS="--cfg=uninit_checks" kani verify-std \ + -Z unstable-options \ + "${TMP_DIR}/library" \ + --target-dir "${TMP_DIR}/target" \ + -Z function-contracts \ + -Z stubbing \ + -Z mem-predicates \ + -Z uninit-checks # Cleanup rm -r ${TMP_DIR} diff --git a/tests/slow/kani/Strings/copy_empty_string_by_intrinsic.rs b/tests/slow/kani/Strings/copy_empty_string_by_intrinsic.rs index a0c1bef7d003..596bedaa7825 100644 --- a/tests/slow/kani/Strings/copy_empty_string_by_intrinsic.rs +++ b/tests/slow/kani/Strings/copy_empty_string_by_intrinsic.rs @@ -1,7 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --enable-unstable --mir-linker //! Make sure we can handle explicit copy_nonoverlapping on empty string //! This used to trigger an issue: https://github.com/model-checking/kani/issues/241 diff --git a/tests/ui/arbitrary-ptr-doc/doc_examples.expected b/tests/ui/arbitrary-ptr-doc/doc_examples.expected new file mode 100644 index 000000000000..19c01006f313 --- /dev/null +++ b/tests/ui/arbitrary-ptr-doc/doc_examples.expected @@ -0,0 +1,24 @@ +Checking harness check_distance... +VERIFICATION:- SUCCESSFUL + +Checking harness diff_from_usize... +VERIFICATION:- SUCCESSFUL + +Checking harness usage_example... +VERIFICATION:- SUCCESSFUL + +Checking harness pointer_may_be_same... + ** 1 of 1 cover properties satisfied +VERIFICATION:- SUCCESSFUL + +Checking harness generator_large_enough... + ** 2 of 2 cover properties satisfied +VERIFICATION:- SUCCESSFUL + +Checking harness same_capacity... +VERIFICATION:- SUCCESSFUL + +Checking harness basic_inbounds... +VERIFICATION:- SUCCESSFUL + +Complete - 7 successfully verified harnesses, 0 failures, 7 total. diff --git a/tests/ui/arbitrary-ptr-doc/doc_examples.rs b/tests/ui/arbitrary-ptr-doc/doc_examples.rs new file mode 100644 index 000000000000..319863f6f6ef --- /dev/null +++ b/tests/ui/arbitrary-ptr-doc/doc_examples.rs @@ -0,0 +1,90 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// kani-flags: -Z mem-predicates + +//! These are copies of the examples we added to our documentation. +//! We currently cannot run our examples using Kani. +//! We may be able to leverage `--runtool` from rustdoc once its stabilized. See +//! . +#![allow(unused)] + +extern crate kani; + +use kani::*; +#[kani::proof] +fn basic_inbounds() { + let mut generator = PointerGenerator::<10>::new(); + let arbitrary = generator.any_alloc_status::(); + kani::assume(arbitrary.status == AllocationStatus::InBounds); + // Pointer may be unaligned, but it should be in-bounds, so it is safe to write to + unsafe { arbitrary.ptr.write_unaligned(kani::any()) } +} + +#[kani::proof] +fn same_capacity() { + // These generators have the same capacity of 6 bytes. + let generator1 = PointerGenerator::<6>::new(); + let generator2 = pointer_generator::(); +} + +#[kani::proof] +fn generator_large_enough() { + let mut generator = PointerGenerator::<6>::new(); + let ptr1: *mut u8 = generator.any_in_bounds().ptr; + let ptr2: *mut u8 = generator.any_in_bounds().ptr; + let ptr3: *mut u32 = generator.any_in_bounds().ptr; + // This cover is satisfied. + cover!( + (ptr1 as usize) >= (ptr2 as usize) + size_of::() + && (ptr2 as usize) >= (ptr3 as usize) + size_of::() + ); + // As well as having overlapping pointers. + cover!((ptr1 as usize) == (ptr3 as usize)); +} + +#[kani::proof] +fn pointer_may_be_same() { + let mut generator = pointer_generator::(); + let ptr1 = generator.any_in_bounds::().ptr; + let ptr2 = generator.any_in_bounds::().ptr; + // This cover is satisfied. + cover!(ptr1 == ptr2) +} +unsafe fn my_target(_ptr1: *const T, _ptr2: *const T) {} + +#[kani::proof] +fn usage_example() { + let mut generator1 = pointer_generator::(); + let mut generator2 = pointer_generator::(); + let ptr1: *const char = generator1.any_in_bounds().ptr; + let ptr2: *const char = if kani::any() { + // Pointers will have same provenance and may overlap. + generator1.any_in_bounds().ptr + } else { + // Pointers will have different provenance and will not overlap. + generator2.any_in_bounds().ptr + }; + // Invoke the function under verification + unsafe { my_target(ptr1, ptr2) }; +} +#[kani::proof] +fn diff_from_usize() { + // This pointer represents any address, and it may point to anything in memory, + // allocated or not. + let ptr1 = kani::any::() as *const u8; + + // This pointer address will either point to unallocated memory, to a dead object + // or to allocated memory within the generator address space. + let mut generator = PointerGenerator::<5>::new(); + let ptr2: *const u8 = generator.any_alloc_status().ptr; +} +#[kani::proof] +fn check_distance() { + let mut generator = PointerGenerator::<6>::new(); + let ptr1: *mut u8 = generator.any_in_bounds().ptr; + let ptr2: *mut u8 = generator.any_in_bounds().ptr; + // SAFETY: Both pointers have the same provenance. + let distance = unsafe { ptr1.offset_from(ptr2) }; + assert!(distance >= -5 && distance <= 5) +} diff --git a/tests/ui/check_deprecated/deprecated_warning.expected b/tests/ui/check_deprecated/deprecated_warning.expected new file mode 100644 index 000000000000..3a0760035f8b --- /dev/null +++ b/tests/ui/check_deprecated/deprecated_warning.expected @@ -0,0 +1 @@ +warning: use of deprecated function `kani::check`: This API will be made private in future releases. diff --git a/tests/ui/check_deprecated/deprecated_warning.rs b/tests/ui/check_deprecated/deprecated_warning.rs new file mode 100644 index 000000000000..f3d791256081 --- /dev/null +++ b/tests/ui/check_deprecated/deprecated_warning.rs @@ -0,0 +1,10 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// kani-flags: --only-codegen + +/// Ensure that Kani prints a deprecation warning if users invoke `kani::check`. +#[kani::proof] +fn internal_api() { + kani::check(kani::any(), "oops"); +} diff --git a/tests/ui/mir-linker/generic-harness/incorrect.rs b/tests/ui/mir-linker/generic-harness/incorrect.rs index e68eba6ec834..e52b06801517 100644 --- a/tests/ui/mir-linker/generic-harness/incorrect.rs +++ b/tests/ui/mir-linker/generic-harness/incorrect.rs @@ -1,8 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --enable-unstable --mir-linker -// //! Checks that we correctly fail if the harness is a generic function. #[kani::proof] diff --git a/tools/build-kani/Cargo.toml b/tools/build-kani/Cargo.toml index 41095f1d7c3c..25e022e70d3f 100644 --- a/tools/build-kani/Cargo.toml +++ b/tools/build-kani/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "build-kani" -version = "0.55.0" +version = "0.56.0" edition = "2021" description = "Builds Kani, Sysroot and release bundle." license = "MIT OR Apache-2.0"