From 69840fb198704f1be118d00be0dec0659fc2e86b Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Fri, 13 Sep 2024 17:06:40 -0700 Subject: [PATCH] Add an LLBC backend --- .gitignore | 3 + Cargo.lock | 794 ++++++++++++++---- deny.toml | 5 +- kani-compiler/Cargo.toml | 4 +- kani-compiler/src/args.rs | 20 +- .../codegen_aeneas_llbc/compiler_interface.rs | 418 +++++++++ .../codegen_aeneas_llbc/mir_to_ullbc/mod.rs | 770 +++++++++++++++++ kani-compiler/src/codegen_aeneas_llbc/mod.rs | 6 + kani-compiler/src/kani_compiler.rs | 51 +- kani-compiler/src/main.rs | 2 + kani-driver/src/call_cargo.rs | 3 + kani-driver/src/call_single_file.rs | 17 +- kani_metadata/src/unstable.rs | 2 + scripts/codegen-firecracker.sh | 2 +- scripts/std-lib-regression.sh | 2 +- tests/expected/llbc/basic0/expected | 8 + tests/expected/llbc/basic0/test.rs | 15 + 17 files changed, 1960 insertions(+), 162 deletions(-) create mode 100644 kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs create mode 100644 kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs create mode 100644 kani-compiler/src/codegen_aeneas_llbc/mod.rs create mode 100644 tests/expected/llbc/basic0/expected create mode 100644 tests/expected/llbc/basic0/test.rs 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/Cargo.lock b/Cargo.lock index 63f86490e284..17782d98d568 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -26,9 +26,9 @@ dependencies = [ [[package]] name = "anstream" -version = "0.6.15" +version = "0.6.14" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "64e15c1ab1f89faffbf04a634d5e1962e9074f2741eef6d97f3c4e322426d526" +checksum = "418c75fa768af9c03be99d17643f93f79bbba589895012a80e3452a19ddda15b" dependencies = [ "anstyle", "anstyle-parse", @@ -41,33 +41,33 @@ dependencies = [ [[package]] name = "anstyle" -version = "1.0.8" +version = "1.0.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1bec1de6f59aedf83baf9ff929c98f2ad654b97c9510f4e70cf6f661d49fd5b1" +checksum = "038dfcf04a5feb68e9c60b21c9625a54c2c0616e79b72b0fd87075a056ae1d1b" [[package]] name = "anstyle-parse" -version = "0.2.5" +version = "0.2.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "eb47de1e80c2b463c735db5b217a0ddc39d612e7ac9e2e96a5aed1f57616c1cb" +checksum = "c03a11a9034d92058ceb6ee011ce58af4a9bf61491aa7e1e59ecd24bd40d22d4" dependencies = [ "utf8parse", ] [[package]] name = "anstyle-query" -version = "1.1.1" +version = "1.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6d36fc52c7f6c869915e99412912f22093507da8d9e942ceaf66fe4b7c14422a" +checksum = "ad186efb764318d35165f1758e7dcef3b10628e26d41a44bc5550652e6804391" dependencies = [ "windows-sys 0.52.0", ] [[package]] name = "anstyle-wincon" -version = "3.0.4" +version = "3.0.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5bf74e1b6e971609db8ca7a9ce79fd5768ab6ae46441c572e46cf596f59e57f8" +checksum = "61a38449feb7068f52bb06c12759005cf459ee52bb4adc1d5a7c4322d716fb19" dependencies = [ "anstyle", "windows-sys 0.52.0", @@ -75,9 +75,36 @@ dependencies = [ [[package]] name = "anyhow" -version = "1.0.89" +version = "1.0.86" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "86fdf8605db99b54d3cd748a44c6d04df638eb5dafb219b135d0149bd0db01f6" +checksum = "b3d1d046238990b9cf5bcde22a3fb3584ee5cf65fb2765f454ed428c7a0063da" + +[[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.15" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bc65048dd435533bb1baf2ed9956b9a278fbfdcf90301b39ee117f06c0199d37" +dependencies = [ + "anstyle", + "bstr", + "doc-comment", + "predicates", + "predicates-core", + "predicates-tree", + "wait-timeout", +] [[package]] name = "autocfg" @@ -87,9 +114,38 @@ checksum = "0c4b4d0bd25bd0b74681c0ad21497610ce1b7c91b1022cd21c80c6fbdd9476b0" [[package]] name = "bitflags" -version = "2.6.0" +version = "2.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cf4b9d6a944f767f8e5e0db018570623c85f3d925ac718db4e06d0187adb21c1" + +[[package]] +name = "bitmaps" +version = "2.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b048fb63fd8b5923fc5aa7b340d8e156aec7ec02f0c78fa8a6ddc2613f6f71de" +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.7", + "serde", +] [[package]] name = "build-kani" @@ -101,17 +157,11 @@ dependencies = [ "which", ] -[[package]] -name = "byteorder" -version = "1.5.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1fd0f2584146f6f2ef48085050886acf353beff7305ebd1ae69500e27c67f64b" - [[package]] name = "camino" -version = "1.1.9" +version = "1.1.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8b96ec4966b5813e2c0507c1f86115c8c5abaadc3980879c3424042a02fd1ad3" +checksum = "e0ec6b951b160caa93cc0c7b209e5a3bff7aae9062213451ac99493cd844c239" dependencies = [ "serde", ] @@ -139,17 +189,63 @@ dependencies = [ "thiserror", ] +[[package]] +name = "cc" +version = "1.0.101" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ac367972e516d45567c7eafc73d24e1c193dcf200a8d94e9db7b3d38b349572d" + [[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" +source = "git+https://github.com/AeneasVerif/charon?rev=cdc1dcde447a50cbc20336c79b21b42ac977b7fd#cdc1dcde447a50cbc20336c79b21b42ac977b7fd" +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.17" +version = "4.5.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3e5a21b8495e732f1b3c364c9949b201ca7bae518c502c80256c96ad79eaf6ac" +checksum = "5db83dced34638ad474f39f250d7fea9598bdd239eaced1bdf45d597da0f433f" dependencies = [ "clap_builder", "clap_derive", @@ -157,9 +253,9 @@ dependencies = [ [[package]] name = "clap_builder" -version = "4.5.17" +version = "4.5.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8cf2dd12af7a047ad9d6da2b6b249759a22a7abc0f474c1dae1777afa4b21a73" +checksum = "f7e204572485eb3fbf28f871612191521df159bc3e15a9f5064c66dba3a8c05f" dependencies = [ "anstream", "anstyle", @@ -169,27 +265,37 @@ dependencies = [ [[package]] name = "clap_derive" -version = "4.5.13" +version = "4.5.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "501d359d5f3dcaf6ecdeee48833ae73ec6e42723a1e52419c79abf9507eec0a0" +checksum = "c780290ccf4fb26629baa7a1081e68ced113f1d3ec302fa5948f1c381ebf06c6" dependencies = [ "heck", "proc-macro2", "quote", - "syn", + "syn 2.0.77", ] [[package]] name = "clap_lex" -version = "0.7.2" +version = "0.7.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1462739cb27611015575c0c11df5df7601141071f07518d56fcc1be504cbec97" +checksum = "4b82cf0babdbd58558212896d1a4272303a57bdb245c2bf1147185fb45640e70" [[package]] name = "colorchoice" -version = "1.0.2" +version = "1.0.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d3fd119d74b830634cea2a0f58bbd0d54540518a14397557951e79340abc28c0" +checksum = "0b6a852b24ab71dffc585bcb46eaf7959d175cb865a7152e35b348d1b2960422" + +[[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 = "comfy-table" @@ -233,6 +339,21 @@ 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" @@ -325,11 +446,56 @@ 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" +version = "1.12.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "60b1af1c220855b6ceac025d3f6ecdd2b7c4894bfe9cd9bda4fbb4bc7c0d4cf0" +checksum = "3dca9240753cf90908d7e4aac30f630662b02aebaa1b58a3cadabdb23385b58b" [[package]] name = "encode_unicode" @@ -337,6 +503,29 @@ version = "0.3.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "a357d28ed41a50f9c765dbfe56cbc04a64e53e5fc58ba79fbc34c10ef3df831f" +[[package]] +name = "env_filter" +version = "0.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a009aa4810eb158359dda09d0c87378e4bbb89b5a801f016885a4707ba24f7ea" +dependencies = [ + "log", + "regex", +] + +[[package]] +name = "env_logger" +version = "0.11.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "38b35839ba51819680ba087cd351788c9a3c476841207e0b8cee0b04722343b9" +dependencies = [ + "anstream", + "anstyle", + "env_filter", + "humantime", + "log", +] + [[package]] name = "equivalent" version = "1.0.1" @@ -355,9 +544,9 @@ dependencies = [ [[package]] name = "fastrand" -version = "2.1.1" +version = "2.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e8c02a5121d4ea3eb16a80748c74f5549a5665e4c21333c6098f283870fbdea6" +checksum = "9fc0510504f03c51ada170672ac806f1f105a88aa97a5281117e1ddc3368e51a" [[package]] name = "fixedbitset" @@ -411,6 +600,16 @@ dependencies = [ "ahash", ] +[[package]] +name = "hashlink" +version = "0.9.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6ba4ff7128dee98c7dc9794b6a411377e1404dba1c97deb8d1a55297bd25d8af" +dependencies = [ + "hashbrown", + "serde", +] + [[package]] name = "heck" version = "0.5.0" @@ -426,21 +625,71 @@ 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.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "74086667896a940438f2118212f313abba4aff3831fef6f4b17d02add5c8bb60" +dependencies = [ + "serde", +] + [[package]] name = "indexmap" -version = "2.5.0" +version = "2.2.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "68b900aa2f7301e21c36462b170ee99994de34dff39a4a6a528e80e7376d07e5" +checksum = "168fb715dda47215e360912c096649d23d58bf392ac62f73919e831745e40f26" dependencies = [ "equivalent", "hashbrown", ] +[[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" +version = "1.70.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f8478577c03552c21db0e2724ffb8986a5ce7af88107e6be5d2ee6e158c12800" + +[[package]] +name = "itertools" +version = "0.10.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7943c866cc5cd64cbc25b2e01621d07fa8eb2a1a23160ee81ce38704e97b8ecf" +checksum = "b0fd2260e829bddf4cb6ea802289de2f86d6a7a690192fbe91b3f46e0f2c8473" +dependencies = [ + "either", +] [[package]] name = "itertools" @@ -457,6 +706,12 @@ 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" @@ -469,10 +724,11 @@ dependencies = [ name = "kani-compiler" version = "0.55.0" dependencies = [ + "charon", "clap", "cprover_bindings", "home", - "itertools", + "itertools 0.13.0", "kani_metadata", "lazy_static", "num", @@ -483,10 +739,10 @@ dependencies = [ "shell-words", "strum", "strum_macros", - "syn", + "syn 2.0.77", "tracing", "tracing-subscriber", - "tracing-tree", + "tracing-tree 0.4.0", ] [[package]] @@ -541,7 +797,7 @@ dependencies = [ "proc-macro-error2", "proc-macro2", "quote", - "syn", + "syn 2.0.77", ] [[package]] @@ -563,9 +819,9 @@ checksum = "bbd2bcb4c963f2ddae06a2efc7e9f3591312473c50c6685e1f298068316e66fe" [[package]] name = "libc" -version = "0.2.158" +version = "0.2.155" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d8adc4bb1803a324070e64a98ae98f38934d91957a99cfb3a43dcbc01bc56439" +checksum = "97b3888a4aecf77e811145cadf6eef5901f4782c53886191b2f693f24761847c" [[package]] name = "linear-map" @@ -595,9 +851,19 @@ dependencies = [ [[package]] name = "log" -version = "0.4.22" +version = "0.4.21" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a7a70ba024b9dc04c27ea2f0c0548feb474ec5c54bba33a7f72f873a39d07b24" +checksum = "90ed8c1e510134f979dbc4f070f87d4313098b704861a105fe34231c70a3901c" + +[[package]] +name = "macros" +version = "0.1.0" +source = "git+https://github.com/AeneasVerif/charon?rev=cdc1dcde447a50cbc20336c79b21b42ac977b7fd#cdc1dcde447a50cbc20336c79b21b42ac977b7fd" +dependencies = [ + "proc-macro2", + "quote", + "syn 2.0.77", +] [[package]] name = "matchers" @@ -620,6 +886,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" @@ -632,11 +927,11 @@ dependencies = [ [[package]] name = "nu-ansi-term" -version = "0.50.1" +version = "0.50.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d4a28e057d01f97e61255210fcff094d74ed0466038633e95017f5beb68e4399" +checksum = "dd2800e1520bdc966782168a627aa5d1ad92e33b984bf7c7615d31280c83ff14" dependencies = [ - "windows-sys 0.52.0", + "windows-sys 0.48.0", ] [[package]] @@ -655,9 +950,9 @@ dependencies = [ [[package]] name = "num-bigint" -version = "0.4.6" +version = "0.4.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a5e44f723f1133c9deac646763579fdb3ac745e418f2a7af9cd0c431da1f20b9" +checksum = "c165a9ab64cf766f73521c0dd2cfdff64f488b8f0b3e621face3462d3db536d7" dependencies = [ "num-integer", "num-traits", @@ -760,7 +1055,7 @@ dependencies = [ "libc", "redox_syscall", "smallvec", - "windows-targets", + "windows-targets 0.52.5", ] [[package]] @@ -793,11 +1088,46 @@ checksum = "439ee305def115ba05938db6eb1644ff94165c5ab5e9420d1c1bcedbba909391" [[package]] name = "ppv-lite86" -version = "0.2.20" +version = "0.2.17" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "77957b295656769bb8ad2b6a6b09d897d94f05c41b069aede1fcdaa675eaea04" +checksum = "5b40af805b3121feab8a3c29f04d8ad262fa8e0561883e7653e024ae4479e6de" + +[[package]] +name = "predicates" +version = "3.1.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7e9086cc7640c29a356d1a29fd134380bee9d8f79a17410aa76e7ad295f42c97" dependencies = [ - "zerocopy", + "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]] @@ -819,7 +1149,7 @@ dependencies = [ "proc-macro-error-attr2", "proc-macro2", "quote", - "syn", + "syn 2.0.77", ] [[package]] @@ -831,11 +1161,20 @@ dependencies = [ "unicode-ident", ] +[[package]] +name = "psm" +version = "0.1.21" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5787f7cda34e3033a72192c018bc5883100330f362ef279a8cbccfce8bb4e874" +dependencies = [ + "cc", +] + [[package]] name = "quote" -version = "1.0.37" +version = "1.0.36" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b5b9d34b8991d19d98081b46eacdd8eb58c6f2b201139f7c5f643cc155a633af" +checksum = "0fa76aaf39101c457836aec0ce2316dbdc3ab723cdda1c6bd4e6ad4208acaca7" dependencies = [ "proc-macro2", ] @@ -870,6 +1209,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" @@ -892,18 +1240,18 @@ dependencies = [ [[package]] name = "redox_syscall" -version = "0.5.4" +version = "0.5.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0884ad60e090bf1345b93da0a5de8923c93884cd03f40dfcfddd3b4bee661853" +checksum = "c82cf8cff14456045f55ec4241383baeff27af886adb72ffb2162f99911de0fd" dependencies = [ "bitflags", ] [[package]] name = "regex" -version = "1.10.6" +version = "1.10.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4219d74c6b67a3654a9fbebc4b419e22126d13d2f3c4a07ee0cb61ff79a79619" +checksum = "b91213439dad192326a0d7c6ee3955910425f441d7038e0d6933b0aec5c4517f" dependencies = [ "aho-corasick", "memchr", @@ -949,11 +1297,20 @@ version = "0.1.24" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "719b953e2095829ee67db738b3bfa9fa368c94900df327b3f07fe6e794d2fe1f" +[[package]] +name = "rustc_version" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bfa0f585226d2e68097d4f95d113b15b83a82e819ab25717ec0590d9584ef366" +dependencies = [ + "semver", +] + [[package]] name = "rustix" -version = "0.38.37" +version = "0.38.34" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8acb788b847c24f28525660c4d7758620a7210875711f79e7f663cc152726811" +checksum = "70dc5ec042f7a43c4a73241207cecc9873a06d45debb38b329f8541d85c2730f" dependencies = [ "bitflags", "errno", @@ -1012,50 +1369,68 @@ dependencies = [ [[package]] name = "serde" -version = "1.0.210" +version = "1.0.203" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c8e3592472072e6e22e0a54d5904d9febf8508f65fb8552499a1abc7d1078c3a" +checksum = "7253ab4de971e72fb7be983802300c30b5a7f0c2e56fab8abfc6a214307c0094" 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" +version = "1.0.203" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "243902eda00fad750862fc144cea25caca5e20d615af0a81bee94ca738f1df1f" +checksum = "500cbc0ebeb6f46627f50f3f5811ccf6bf00643be300b4c3eabc0ef55dc5b5ba" dependencies = [ "proc-macro2", "quote", - "syn", + "syn 2.0.77", ] [[package]] name = "serde_json" -version = "1.0.128" +version = "1.0.117" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6ff5456707a1de34e7e37f2a6fd3d3f808c318259cbd01ab6377795054b483d8" +checksum = "455182ea6142b14f93f4bc5320a2b31c1f266b66a4a5c858b013302a5d8cbfc3" dependencies = [ "itoa", - "memchr", "ryu", "serde", ] [[package]] name = "serde_spanned" -version = "0.6.7" +version = "0.6.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "79e674e01f999af37c49f70a6ede167a8a60b2503e56c5599532a65baa5969a0" +dependencies = [ + "serde", +] + +[[package]] +name = "serde_stacker" +version = "0.1.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "eb5b1b31579f3811bf615c144393417496f152e12ac8b7663bf664f4a815306d" +checksum = "babfccff5773ff80657f0ecf553c7c516bdc2eb16389c0918b36b73e7015276e" dependencies = [ "serde", + "stacker", ] [[package]] name = "serde_test" -version = "1.0.177" +version = "1.0.176" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7f901ee573cab6b3060453d2d5f0bae4e6d628c23c0a962ff9b5f1d7c8d4f1ed" +checksum = "5a2f49ace1498612d14f7e0b8245519584db8299541dfe31a06374a828d620ab" dependencies = [ "serde", ] @@ -1088,12 +1463,35 @@ version = "1.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "24188a676b6ae68c3b2cb3a01be17fbf7240ce009799bb56d5b1409051e78fde" +[[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.15" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c886bd4480155fd3ef527d45e9ac8dd7118a898a46530b7b94c3e21866259fce" +dependencies = [ + "cc", + "cfg-if", + "libc", + "psm", + "winapi", +] + [[package]] name = "std" version = "0.55.0" @@ -1134,7 +1532,18 @@ dependencies = [ "proc-macro2", "quote", "rustversion", - "syn", + "syn 2.0.77", +] + +[[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]] @@ -1148,37 +1557,48 @@ 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.12.0" +version = "3.10.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "04cbcdd0c794ebb0d4cf35e88edd2f7d2c4c3e9a5a6dab322839b321c6a87a64" +checksum = "85b77fafb263dd9d05cbeac119526425676db3784113aa9295c88498cbf8bff1" dependencies = [ "cfg-if", "fastrand", - "once_cell", "rustix", - "windows-sys 0.59.0", + "windows-sys 0.52.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.63" +version = "1.0.61" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c0342370b38b6a11b6cc11d6a805569958d54cfa061a29969c3b5ce2ea405724" +checksum = "c546c80d6be4bc6a00c0f01730c08df82eaa7a7a61f11d656526506112cc1709" dependencies = [ "thiserror-impl", ] [[package]] name = "thiserror-impl" -version = "1.0.63" +version = "1.0.61" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a4558b58466b9ad7ca0f102865eccc95938dca1a74a856f2b57b6629050da261" +checksum = "46c3384250002a6d5af4d114f2845d37b57521033f30d5c3f46c4d70e1197533" dependencies = [ "proc-macro2", "quote", - "syn", + "syn 2.0.77", ] [[package]] @@ -1224,9 +1644,9 @@ dependencies = [ [[package]] name = "toml" -version = "0.8.19" +version = "0.8.14" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a1ed1f98e3fdc28d6d910e6737ae6ab1a93bf1985935a1193e68f93eeb68d24e" +checksum = "6f49eb2ab21d2f26bd6db7bf383edc527a7ebaee412d17af4d40fdccd442f335" dependencies = [ "serde", "serde_spanned", @@ -1236,18 +1656,18 @@ dependencies = [ [[package]] name = "toml_datetime" -version = "0.6.8" +version = "0.6.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0dd7358ecb8fc2f8d014bf86f6f638ce72ba252a2c3a2572f2a795f1d23efb41" +checksum = "4badfd56924ae69bcc9039335b2e017639ce3f9b001c393c1b2d1ef846ce2cbf" dependencies = [ "serde", ] [[package]] name = "toml_edit" -version = "0.22.20" +version = "0.22.14" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "583c44c02ad26b0c3f3066fe629275e50627026c51ac2e595cca4c230ce1ce1d" +checksum = "f21c7aaf97f1bd9ca9d4f9e73b0a6c74bd5afef56f2bc931943a6e1c37e04e38" dependencies = [ "indexmap", "serde", @@ -1275,7 +1695,7 @@ checksum = "34704c8d6ebcbc939824180af020566b01a7c01f80641264eba0999f6c2b6be7" dependencies = [ "proc-macro2", "quote", - "syn", + "syn 2.0.77", ] [[package]] @@ -1331,23 +1751,53 @@ 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.0", + "tracing-core", + "tracing-log", + "tracing-subscriber", +] + [[package]] name = "tracing-tree" version = "0.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "f459ca79f1b0d5f71c54ddfde6debfc59c8b6eeb46808ae492077f739dc7b49c" dependencies = [ - "nu-ansi-term 0.50.1", + "nu-ansi-term 0.50.0", "tracing-core", "tracing-log", "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" +version = "1.0.12" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e91b56cd4cadaeb79bbf1a5645f6b4f8dc5bde8834ad5894a8db35fda9efa1fe" +checksum = "3354b9ac3fae1ff6755cb6db53683adb661634f67557942dea4facebec0fee4b" + +[[package]] +name = "unicode-segmentation" +version = "1.11.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d4c87d22b6e3f4a18d4d40ef354e97c90fcb14dd91d7dc0aa9d8a1172ebf7202" [[package]] name = "unicode-width" @@ -1375,9 +1825,9 @@ checksum = "830b7e5d4d90034032940e4ace0d9a9a057e7a45cd94e6c007832e39edb82f6d" [[package]] name = "version_check" -version = "0.9.5" +version = "0.9.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a" +checksum = "49874b5167b65d7193b8aba1567f5c7d93d001cafc34600cee003eda787e483f" [[package]] name = "wait-timeout" @@ -1406,9 +1856,9 @@ checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423" [[package]] name = "which" -version = "6.0.3" +version = "6.0.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b4ee928febd44d98f2f459a4a79bd4d928591333a494a10a868418ac1b39cf1f" +checksum = "8211e4f58a2b2805adfbefbc07bab82958fc91e3836339b1ab7ae32465dce0d7" dependencies = [ "either", "home", @@ -1434,11 +1884,11 @@ checksum = "ac3b87c63620426dd9b991e5ce0329eff545bccbbb34f3be09ff6fb6ab51b7b6" [[package]] name = "winapi-util" -version = "0.1.9" +version = "0.1.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "cf221c93e13a30d793f7645a0e7762c55d169dbb0a49671918a2319d289b10bb" +checksum = "4d4cc384e1e73b93bafa6fb4f1df8c41695c8a91cf9c4c64358067d15a7b6c6b" dependencies = [ - "windows-sys 0.59.0", + "windows-sys 0.52.0", ] [[package]] @@ -1447,93 +1897,150 @@ 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.5", ] [[package]] -name = "windows-sys" -version = "0.59.0" +name = "windows-targets" +version = "0.48.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1e38bc4d79ed67fd075bcc251a1c39b32a1776bbe92e5bef1f0bf1f8c531853b" +checksum = "9a2fa6e2155d7247be68c096456083145c183cbbbc2764150dda45a87197940c" dependencies = [ - "windows-targets", + "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]] name = "windows-targets" -version = "0.52.6" +version = "0.52.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9b724f72796e036ab90c1021d4780d4d3d648aca59e491e6b98e725b84e99973" +checksum = "6f0713a46559409d202e70e28227288446bf7841d3211583a4b53e3f6d96e7eb" dependencies = [ - "windows_aarch64_gnullvm", - "windows_aarch64_msvc", - "windows_i686_gnu", + "windows_aarch64_gnullvm 0.52.5", + "windows_aarch64_msvc 0.52.5", + "windows_i686_gnu 0.52.5", "windows_i686_gnullvm", - "windows_i686_msvc", - "windows_x86_64_gnu", - "windows_x86_64_gnullvm", - "windows_x86_64_msvc", + "windows_i686_msvc 0.52.5", + "windows_x86_64_gnu 0.52.5", + "windows_x86_64_gnullvm 0.52.5", + "windows_x86_64_msvc 0.52.5", ] [[package]] name = "windows_aarch64_gnullvm" -version = "0.52.6" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2b38e32f0abccf9987a4e3079dfb67dcd799fb61361e53e2882c3cbaf0d905d8" + +[[package]] +name = "windows_aarch64_gnullvm" +version = "0.52.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7088eed71e8b8dda258ecc8bac5fb1153c5cffaf2578fc8ff5d61e23578d3263" + +[[package]] +name = "windows_aarch64_msvc" +version = "0.48.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "32a4622180e7a0ec044bb555404c800bc9fd9ec262ec147edd5989ccd0c02cd3" +checksum = "dc35310971f3b2dbbf3f0690a219f40e2d9afcf64f9ab7cc1be722937c26b4bc" [[package]] name = "windows_aarch64_msvc" -version = "0.52.6" +version = "0.52.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "09ec2a7bb152e2252b53fa7803150007879548bc709c039df7627cabbd05d469" +checksum = "9985fd1504e250c615ca5f281c3f7a6da76213ebd5ccc9561496568a2752afb6" [[package]] name = "windows_i686_gnu" -version = "0.52.6" +version = "0.48.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8e9b5ad5ab802e97eb8e295ac6720e509ee4c243f69d781394014ebfe8bbfa0b" +checksum = "a75915e7def60c94dcef72200b9a8e58e5091744960da64ec734a6c6e9b3743e" + +[[package]] +name = "windows_i686_gnu" +version = "0.52.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "88ba073cf16d5372720ec942a8ccbf61626074c6d4dd2e745299726ce8b89670" [[package]] name = "windows_i686_gnullvm" -version = "0.52.6" +version = "0.52.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "87f4261229030a858f36b459e748ae97545d6f1ec60e5e0d6a3d32e0dc232ee9" + +[[package]] +name = "windows_i686_msvc" +version = "0.48.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0eee52d38c090b3caa76c563b86c3a4bd71ef1a819287c19d586d7334ae8ed66" +checksum = "8f55c233f70c4b27f66c523580f78f1004e8b5a8b659e05a4eb49d4166cca406" [[package]] name = "windows_i686_msvc" -version = "0.52.6" +version = "0.52.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "db3c2bf3d13d5b658be73463284eaf12830ac9a26a90c717b7f771dfe97487bf" + +[[package]] +name = "windows_x86_64_gnu" +version = "0.48.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "240948bc05c5e7c6dabba28bf89d89ffce3e303022809e73deaefe4f6ec56c66" +checksum = "53d40abd2583d23e4718fddf1ebec84dbff8381c07cae67ff7768bbf19c6718e" [[package]] name = "windows_x86_64_gnu" -version = "0.52.6" +version = "0.52.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4e4246f76bdeff09eb48875a0fd3e2af6aada79d409d33011886d3e1581517d9" + +[[package]] +name = "windows_x86_64_gnullvm" +version = "0.48.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "147a5c80aabfbf0c7d901cb5895d1de30ef2907eb21fbbab29ca94c5b08b1a78" +checksum = "0b7b52767868a23d5bab768e390dc5f5c55825b6d30b86c844ff2dc7414044cc" [[package]] name = "windows_x86_64_gnullvm" -version = "0.52.6" +version = "0.52.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "852298e482cd67c356ddd9570386e2862b5673c85bd5f88df9ab6802b334c596" + +[[package]] +name = "windows_x86_64_msvc" +version = "0.48.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "24d5b23dc417412679681396f2b49f3de8c1473deb516bd34410872eff51ed0d" +checksum = "ed94fce61571a4006852b7389a063ab983c02eb1bb37b47f8272ce92d06d9538" [[package]] name = "windows_x86_64_msvc" -version = "0.52.6" +version = "0.52.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec" +checksum = "bec47e5bfd1bff0eeaf6d8b485cc1074891a197ab4225d504cb7a1ab88b02bf0" [[package]] name = "winnow" -version = "0.6.18" +version = "0.6.13" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "68a9bda4691f099d435ad181000724da8e5899daa10713c2d432552b9ccd3a6f" +checksum = "59b5e5f6c299a3c7890b876a2a587f3115162487e704907d9b6cd29473052ba1" dependencies = [ "memchr", ] @@ -1546,21 +2053,20 @@ checksum = "d135d17ab770252ad95e9a872d365cf3090e3be864a34ab46f48555993efc904" [[package]] name = "zerocopy" -version = "0.7.35" +version = "0.7.34" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1b9b4fd18abc82b8136838da5d50bae7bdea537c574d8dc1a34ed098d6c166f0" +checksum = "ae87e3fcd617500e5d106f0380cf7b77f3c6092aae37191433159dda23cfb087" dependencies = [ - "byteorder", "zerocopy-derive", ] [[package]] name = "zerocopy-derive" -version = "0.7.35" +version = "0.7.34" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e" +checksum = "15e934569e47891f7d9411f1a451d947a60e000ab3bd24fbb970f000387d1b3b" dependencies = [ "proc-macro2", "quote", - "syn", + "syn 2.0.77", ] diff --git a/deny.toml b/deny.toml index 733f91e12f36..9cfc0df87d90 100644 --- a/deny.toml +++ b/deny.toml @@ -21,6 +21,7 @@ ignore = [ allow = [ "MIT", "Apache-2.0", + "MPL-2.0", ] confidence-threshold = 0.8 @@ -46,4 +47,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/AeneasVerif/charon", +] diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index 9ca8d10f5275..fa1f60105010 100644 --- a/kani-compiler/Cargo.toml +++ b/kani-compiler/Cargo.toml @@ -10,6 +10,7 @@ publish = false [dependencies] cbmc = { path = "../cprover_bindings", package = "cprover_bindings", optional = true } +charon = { git = "https://github.com/AeneasVerif/charon", optional = true, default-features = false, rev = "cdc1dcde447a50cbc20336c79b21b42ac977b7fd" } 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..0ed762d651c1 100644 --- a/kani-compiler/src/args.rs +++ b/kani-compiler/src/args.rs @@ -4,6 +4,20 @@ use strum_macros::{AsRefStr, EnumString, VariantNames}; use tracing_subscriber::filter::Directive; +#[derive(Debug, Default, Clone, Copy, AsRefStr, EnumString, VariantNames, PartialEq, Eq)] +#[strum(serialize_all = "snake_case")] +pub enum BackendOption { + /// Aeneas (LLBC) backend + Aeneas, + + /// CProver (Goto) backend + CProver, + + /// Backend option was not explicitly set + #[default] + None, +} + #[derive(Debug, Default, Clone, Copy, AsRefStr, EnumString, VariantNames, PartialEq, Eq)] #[strum(serialize_all = "snake_case")] pub enum ReachabilityType { @@ -69,11 +83,9 @@ 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, + #[clap(long = "backend", default_value = "none")] + pub backend: BackendOption, } #[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..12c1bff8307e --- /dev/null +++ b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs @@ -0,0 +1,418 @@ +// 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::ctx::TransformOptions; +use charon_lib::transform::TransformCtx; +use kani_metadata::ArtifactType; +use kani_metadata::{AssignsContract, CompilerArtifactStub}; +use rustc_codegen_ssa::back::archive::{ArArchiveBuilder, ArchiveBuilder, DEFAULT_OBJECT_READER}; +use rustc_codegen_ssa::back::metadata::create_wrapper_file; +use rustc_codegen_ssa::traits::CodegenBackend; +use rustc_codegen_ssa::{CodegenResults, CrateInfo}; +use rustc_data_structures::fx::FxIndexMap; +use rustc_data_structures::temp_dir::MaybeTempDir; +use rustc_errors::{ErrorGuaranteed, DEFAULT_LOCALE_RESOURCE}; +use rustc_hir::def_id::{DefId as InternalDefId, LOCAL_CRATE}; +use rustc_metadata::creader::MetadataLoaderDyn; +use rustc_metadata::fs::{emit_wrapper_file, METADATA_FILENAME}; +use rustc_metadata::EncodedMetadata; +use rustc_middle::dep_graph::{WorkProduct, WorkProductId}; +use rustc_middle::ty::TyCtxt; +use rustc_middle::util::Providers; +use rustc_session::config::{CrateType, OutputFilenames, OutputType}; +use rustc_session::output::out_filename; +use rustc_session::Session; +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 tempfile::Builder as TempFileBuilder; +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 + } + } + + info!("# 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); + + info!("# 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) + } + + println!("# Final LLBC before serialization:\n\n{}\n", ccx); + + // Display an error report about the external dependencies, if necessary + ccx.errors.report_external_deps_errors(); + + trace!("Done"); + + 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()); + trace!("Target file: {:?}", pb); + 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 metadata_loader(&self) -> Box { + Box::new(rustc_codegen_ssa::back::metadata::DefaultMetadataLoader) + } + + 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` + let mut builder = Box::new(ArArchiveBuilder::new(sess, &DEFAULT_OBJECT_READER)); + let tmp_dir = TempFileBuilder::new().prefix("kani").tempdir().unwrap(); + let path = MaybeTempDir::new(tmp_dir, sess.opts.cg.save_temps); + let (metadata, _metadata_position) = create_wrapper_file( + sess, + ".rmeta".to_string(), + codegen_results.metadata.raw_data(), + ); + let metadata = emit_wrapper_file(sess, &metadata, &path, METADATA_FILENAME); + builder.add_file(&metadata); + builder.build(&out_path); + } 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(()) + } +} + +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..cec934ab1522 --- /dev/null +++ b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs @@ -0,0 +1,770 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This module contains a context for translating stable MIR into ULLBC + +use core::panic; +use std::path::PathBuf; + +use charon_lib::ast::meta::{AttrInfo, Loc, RawSpan}; +use charon_lib::ast::types::Ty as CharonTy; +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::{make_locals_generator, AbortKind, Body as CharonBody, Var, VarId}; +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, 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, RigidTy, Span, Ty, TyKind, UintTy, +}; + +use stable_mir::{CrateDef, DefId}; +use tracing::{debug, trace}; + +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> { + 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() + } + + 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(()) + } + + 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. + pub(crate) fn translate_item_meta_from_rid( + &mut self, + instance: Instance, + ) -> Result { + let span = self.translate_span_from_rid(instance); + let name = self.def_id_to_name(instance.def.def_id())?; + let source_text = None; + let attr_info = + AttrInfo { attributes: Vec::new(), inline: None, rename: None, public: true }; + let is_local = true; //def_id.is_local(); + + 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 + pub 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 a Rust definition identified by its id. + pub(crate) fn translate_span_from_rid(&mut self, instance: Instance) -> CharonSpan { + self.translate_span(instance.def.span()) + } + + /// Compute the span information for MIR span + pub(crate) 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 + CharonSpan { span: rspan, generated_from_span: None } + } + + pub(crate) 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(move |(idx, arg_abi)| { + arg_abi.mode != PassMode::Ignore + && !(requires_caller_location && idx + 1 == num_args) + }) + .filter_map(|(i, arg_abi)| { + let ty = arg_abi.ty; + debug!(?i, ?arg_abi, "fn_typ"); + if arg_abi.mode == PassMode::Ignore { + // We ignore zero-sized parameters. + // See https://github.com/model-checking/kani/issues/274 for more details. + None + } else { + Some(self.translate_ty(ty)) + } + }) + .collect(); + + debug!(?args, ?fn_abi, "function_type"); + let ret_type = self.translate_ty(fn_abi.ret.ty); + + FunSig { + is_unsafe: false, + is_closure: false, + closure_info: None, + generics: GenericParams::default(), + parent_params_info: None, + inputs: args, + output: ret_type, + } + } + + pub(crate) 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) + } + + pub(crate) 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) + } + + pub 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()) + } + + pub fn translate_ty(&self, ty: Ty) -> CharonTy { + match ty.kind() { + TyKind::RigidTy(rigid_ty) => self.translate_rigid_ty(rigid_ty), + _ => todo!(), + } + } + + pub 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), + GenericArgs { + regions: Vector::new(), + types: Vector::new(), + const_generics: Vector::new(), + trait_refs: Vector::new(), + }, + ), + RigidTy::Ref(_region, ty, mutability) => CharonTy::Ref( + Region::Static, + 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(); + 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) => { + 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()); + 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 ret_local = mir_body.ret_local(); + { + let mut add_variable = make_locals_generator(&mut locals); + //let ret_ty = self.translate_ty_stable(ret_local.ty); + //add_variable(ret_ty); + mir_body.local_decls().for_each(|(_, local)| { + add_variable(self.translate_ty(local.ty)); + }); + } + locals + } + + pub 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 } + } + + pub 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 + } + + pub 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)), + 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 } + } + + pub 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 } + } + + pub 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!(), + } + } + + pub 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)), + } + } + + pub 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()) } + } + + pub 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!(), + } + } + + pub 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!(), + } + } + + pub fn translate_cast(&self, _kind: CastKind, _operand: &Operand, _ty: Ty) -> CharonCastKind { + todo!() + } + + pub 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_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, + } +} + +pub 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..2f8541c63e29 --- /dev/null +++ b/kani-compiler/src/codegen_aeneas_llbc/mod.rs @@ -0,0 +1,6 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +mod compiler_interface; +mod mir_to_ullbc; + +pub use compiler_interface::LlbcCodegenBackend; diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index 58c22f940352..77a3301deca0 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,53 @@ 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"))] + //rustc_session::early_error( + // ErrorOutputType::default(), + // "`--backend aeneas` requires enabling the `aeneas` feature", + //); + panic!("`--backend aeneas` requires enabling the `aeneas` feature"); +} + +/// 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"))] + //rustc_session::early_error( + // ErrorOutputType::default(), + // "`--backend cprover` requires enabling the `cprover` feature", + //); + panic!("`--backend cprover` requires enabling the `cprover` feature") +} + +#[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 { + BackendOption::None => { + // priority list of backends + if cfg!(feature = "cprover") { + cprover_backend(queries) + } else if cfg!(feature = "aeneas") { + aeneas_backend(queries) + } else { + unreachable!(); + } + } + BackendOption::Aeneas => aeneas_backend(queries), + 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/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index ef289cead4c2..6fcfa5fb9b2b 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -164,6 +164,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 868d1adce636..92d439c9e014 100644 --- a/kani-driver/src/call_single_file.rs +++ b/kani-driver/src/call_single_file.rs @@ -53,6 +53,11 @@ 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()); + } else { + kani_args.push("--backend=c_prover".into()); + } let lib_path = lib_folder().unwrap(); let mut rustc_args = self.kani_rustc_flags(LibConfig::new(lib_path)); @@ -95,6 +100,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()]; @@ -144,10 +157,6 @@ impl KaniSession { flags.extend(self.args.common_args.unstable_features.as_arguments().map(str::to_string)); - // 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 } diff --git a/kani_metadata/src/unstable.rs b/kani_metadata/src/unstable.rs index 11df998c820f..abab48304914 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/scripts/codegen-firecracker.sh b/scripts/codegen-firecracker.sh index 3ac7dfa6585d..c6be47542c03 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=c_prover" "-Cllvm-args=--ignore-global-asm" "-Cllvm-args=--reachability=pub_fns" "--sysroot=${KANI_DIR}/target/kani" diff --git a/scripts/std-lib-regression.sh b/scripts/std-lib-regression.sh index a7881f1dc19a..a1474945ee41 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=c_prover" "-Cllvm-args=--ignore-global-asm" "-Cllvm-args=--reachability=pub_fns" "-Cllvm-args=--build-std" 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..15fa50d98c3f --- /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 + +//! 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); +}