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/Cargo.lock b/Cargo.lock index acc0cc485bdb..ef7940c1d013 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2,6 +2,21 @@ # It is not intended for manual editing. version = 4 +[[package]] +name = "addr2line" +version = "0.24.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f5fb1d8e4442bd405fdfd1dacb42792696b0cf9cb15882e5d097b742a676d375" +dependencies = [ + "gimli", +] + +[[package]] +name = "adler2" +version = "2.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "512761e0bb2578dd7380c6baaa0f4ce03e84f95e960231d1dec8bf4d7d6e2627" + [[package]] name = "ahash" version = "0.8.11" @@ -24,6 +39,15 @@ dependencies = [ "memchr", ] +[[package]] +name = "ansi_term" +version = "0.12.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d52a9bb7ec0cf484c551830a7ce27bd20d67eac647e1befb56b0be4ee39a55d2" +dependencies = [ + "winapi", +] + [[package]] name = "anstream" version = "0.6.15" @@ -79,18 +103,122 @@ 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 = "assert_tokens_eq" +version = "0.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6b21f4c5ba5c8b55031306325f196df925939bcc2bd7188ce68fabd93fb4f149" +dependencies = [ + "ansi_term", + "ctor", + "difference", + "output_vt100", + "snafu", +] + [[package]] name = "autocfg" version = "1.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ace50bade8e6234aa140d9a2f552bbee1db4d353f69b8217bc503490fc1a9f26" +[[package]] +name = "backtrace" +version = "0.3.74" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8d82cb332cdfaed17ae235a638438ac4d4839913cc2af585c3c6746e8f8bee1a" +dependencies = [ + "addr2line", + "cfg-if", + "libc", + "miniz_oxide", + "object", + "rustc-demangle", + "windows-targets 0.52.6", +] + +[[package]] +name = "bincode" +version = "2.0.0-rc.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f11ea1a0346b94ef188834a65c068a03aec181c94896d481d7a0a40d85b0ce95" +dependencies = [ + "bincode_derive", + "serde", +] + +[[package]] +name = "bincode_derive" +version = "2.0.0-rc.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7e30759b3b99a1b802a7a3aa21c85c3ded5c28e1c83170d82d70f08bbf7f3e4c" +dependencies = [ + "virtue", +] + [[package]] name = "bitflags" 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" @@ -139,12 +267,66 @@ dependencies = [ "thiserror", ] +[[package]] +name = "cc" +version = "1.1.23" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3bbb537bb4a30b90362caddba8f360c0a56bc13d3a5570028e7197204cb54a17" +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", + "hax-frontend-exporter", + "ignore", + "im", + "index_vec", + "indoc", + "itertools 0.13.0", + "lazy_static", + "libtest-mimic", + "log", + "macros", + "nom", + "nom-supreme", + "petgraph", + "pretty", + "regex", + "rustc_version", + "serde", + "serde-map-to-array", + "serde_json", + "serde_stacker", + "snapbox", + "stacker", + "take_mut", + "tempfile", + "toml", + "tracing", + "tracing-subscriber", + "tracing-tree 0.3.1", + "walkdir", + "which", +] + [[package]] name = "clap" version = "4.5.18" @@ -174,9 +356,9 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "4ac6a0c7b1a9e9a5186361f67dfa1b88213572f427fb9ab038efb2bd8c582dab" dependencies = [ "heck", - "proc-macro2", - "quote", - "syn", + "proc-macro2 1.0.86", + "quote 1.0.37", + "syn 2.0.79", ] [[package]] @@ -191,6 +373,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 = "comfy-table" version = "7.1.1" @@ -233,6 +425,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" @@ -316,6 +523,16 @@ dependencies = [ "memchr", ] +[[package]] +name = "ctor" +version = "0.1.26" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6d2301688392eb071b0bf1a37be05c469d3cc4dbbd95df672fe28ab021e6a096" +dependencies = [ + "quote 1.0.37", + "syn 1.0.109", +] + [[package]] name = "deranged" version = "0.3.11" @@ -325,6 +542,63 @@ dependencies = [ "powerfmt", ] +[[package]] +name = "derivative" +version = "2.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "fcc3dd5e9e9c0b295d6e1e4d811fb6f157d5ffd784b8d202fc62eac8035a770b" +dependencies = [ + "proc-macro2 1.0.86", + "quote 1.0.37", + "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 1.0.86", + "quote 1.0.37", + "syn 1.0.109", +] + +[[package]] +name = "difference" +version = "2.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "524cbf6897b527295dff137cec09ecf3a05f4fddffd7dfcd1585403449e74198" + +[[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 = "dyn-clone" +version = "1.0.17" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0d6ef0072f8a535281e4876be788938b528e9a1d43900b82c2569af7da799125" + [[package]] name = "either" version = "1.13.0" @@ -337,6 +611,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" @@ -353,6 +650,41 @@ dependencies = [ "windows-sys 0.52.0", ] +[[package]] +name = "escape8259" +version = "0.5.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5692dd7b5a1978a5aeb0ce83b7655c58ca8efdcb79d21036ea249da95afec2c6" + +[[package]] +name = "ext-trait" +version = "1.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d772df1c1a777963712fb68e014235e80863d6a91a85c4e06ba2d16243a310e5" +dependencies = [ + "ext-trait-proc_macros", +] + +[[package]] +name = "ext-trait-proc_macros" +version = "1.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1ab7934152eaf26aa5aa9f7371408ad5af4c31357073c9e84c3b9d7f11ad639a" +dependencies = [ + "proc-macro2 1.0.86", + "quote 1.0.37", + "syn 1.0.109", +] + +[[package]] +name = "extension-traits" +version = "1.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a296e5a895621edf9fa8329c83aa1cb69a964643e36cf54d8d7a69b789089537" +dependencies = [ + "ext-trait", +] + [[package]] name = "fastrand" version = "2.1.1" @@ -385,12 +717,31 @@ dependencies = [ "wasi", ] +[[package]] +name = "gimli" +version = "0.31.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "32085ea23f3234fc7846555e85283ba4de91e21016dc0455a16286d87a292d64" + [[package]] name = "glob" version = "0.3.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d2fabcfbdc87f4758337ca535fb41a6d701b65693ce38287d856d1674551ec9b" +[[package]] +name = "globset" +version = "0.4.15" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "15f1ce686646e7f1e19bf7d5533fe443a45dbfb990e00629110797578b42fb19" +dependencies = [ + "aho-corasick", + "bstr", + "log", + "regex-automata 0.4.8", + "regex-syntax 0.8.5", +] + [[package]] name = "graph-cycles" version = "0.1.0" @@ -411,12 +762,69 @@ 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 = "hax-adt-into" +version = "0.1.0-pre.1" +source = "git+https://github.com/hacspec/hax?branch=main#39a2f0aa52a605f68caee8f88fc6c479375becf0" +dependencies = [ + "itertools 0.11.0", + "proc-macro2 1.0.86", + "quote 1.0.37", + "syn 1.0.109", +] + +[[package]] +name = "hax-frontend-exporter" +version = "0.1.0-pre.1" +source = "git+https://github.com/hacspec/hax?branch=main#39a2f0aa52a605f68caee8f88fc6c479375becf0" +dependencies = [ + "bincode", + "extension-traits", + "hax-adt-into", + "hax-frontend-exporter-options", + "itertools 0.11.0", + "lazy_static", + "paste", + "schemars", + "serde", + "serde_json", + "tracing", +] + +[[package]] +name = "hax-frontend-exporter-options" +version = "0.1.0-pre.1" +source = "git+https://github.com/hacspec/hax?branch=main#39a2f0aa52a605f68caee8f88fc6c479375becf0" +dependencies = [ + "bincode", + "hax-adt-into", + "schemars", + "serde", + "serde_json", +] + [[package]] name = "heck" version = "0.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "2304e00983f87ffb38b55b444b5e3b60a884b5d30c0fca7d82fe33449bbe55ea" +[[package]] +name = "hermit-abi" +version = "0.3.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d231dfb89cfffdbc30e7fc41579ed6066ad03abda9e567ccafae602b97ec5024" + [[package]] name = "home" version = "0.5.9" @@ -426,6 +834,57 @@ 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 = "ignore" +version = "0.4.23" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6d89fd380afde86567dfba715db065673989d6253f42b88179abd3eae47bda4b" +dependencies = [ + "crossbeam-deque", + "globset", + "log", + "memchr", + "regex-automata 0.4.8", + "same-file", + "walkdir", + "winapi-util", +] + +[[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" @@ -436,12 +895,36 @@ dependencies = [ "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" 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.11.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b1c173a5686ce8bfa551b3563d0c2170bf24ca44da99c7ca4bfdab5418c3fe57" +dependencies = [ + "either", +] + [[package]] name = "itertools" version = "0.13.0" @@ -457,6 +940,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,24 +958,25 @@ dependencies = [ name = "kani-compiler" version = "0.55.0" dependencies = [ + "charon", "clap", "cprover_bindings", "home", - "itertools", + "itertools 0.13.0", "kani_metadata", "lazy_static", "num", - "quote", + "quote 1.0.37", "regex", "serde", "serde_json", "shell-words", "strum", "strum_macros", - "syn", + "syn 2.0.79", "tracing", "tracing-subscriber", - "tracing-tree", + "tracing-tree 0.4.0", ] [[package]] @@ -539,9 +1029,9 @@ name = "kani_macros" version = "0.55.0" dependencies = [ "proc-macro-error2", - "proc-macro2", - "quote", - "syn", + "proc-macro2 1.0.86", + "quote 1.0.37", + "syn 2.0.79", ] [[package]] @@ -567,6 +1057,18 @@ version = "0.2.159" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "561d97a539a36e26a9a5fad1ea11a3039a67714694aaa379433e580854bc3dc5" +[[package]] +name = "libtest-mimic" +version = "0.7.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cc0bda45ed5b3a2904262c1bb91e526127aa70e7ef3758aba2ef93cf896b9b58" +dependencies = [ + "clap", + "escape8259", + "termcolor", + "threadpool", +] + [[package]] name = "linear-map" version = "1.2.0" @@ -599,6 +1101,16 @@ version = "0.4.22" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "a7a70ba024b9dc04c27ea2f0c0548feb474ec5c54bba33a7f72f873a39d07b24" +[[package]] +name = "macros" +version = "0.1.0" +dependencies = [ + "assert_tokens_eq", + "proc-macro2 1.0.86", + "quote 1.0.37", + "syn 2.0.79", +] + [[package]] name = "matchers" version = "0.1.0" @@ -612,13 +1124,57 @@ dependencies = [ name = "memchr" version = "2.7.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "78ca9ab1a0babb1e7d5695e3530886289c18cf2f87ec19a575a0abdce112e3a3" +checksum = "78ca9ab1a0babb1e7d5695e3530886289c18cf2f87ec19a575a0abdce112e3a3" + +[[package]] +name = "memuse" +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 = "miniz_oxide" +version = "0.8.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e2d80299ef12ff69b16a84bb182e3b9df68b5a91574d3d4fa6e41b65deec4df1" +dependencies = [ + "adler2", +] + +[[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 = "memuse" -version = "0.2.1" +name = "normalize-line-endings" +version = "0.3.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2145869435ace5ea6ea3d35f59be559317ec9a0d04e1812d5f185a87b6d36f1a" +checksum = "61807f77802ff30975e01f4f071c8ba10c022052f98b3294119f3e615d13e5be" [[package]] name = "nu-ansi-term" @@ -718,6 +1274,25 @@ dependencies = [ "autocfg", ] +[[package]] +name = "num_cpus" +version = "1.16.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4161fcb6d602d4d2081af7c3a45852d875a03dd337a6bfdd6e06407b61342a43" +dependencies = [ + "hermit-abi", + "libc", +] + +[[package]] +name = "object" +version = "0.36.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "084f1a5821ac4c651660a94a7153d27ac9d8a53736203f58b31945ded098070a" +dependencies = [ + "memchr", +] + [[package]] name = "once_cell" version = "1.20.1" @@ -737,6 +1312,15 @@ dependencies = [ "windows-sys 0.52.0", ] +[[package]] +name = "output_vt100" +version = "0.1.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "628223faebab4e3e40667ee0b2336d34a5b960ff60ea743ddfdbcf7770bcfb66" +dependencies = [ + "winapi", +] + [[package]] name = "overload" version = "0.1.1" @@ -763,9 +1347,15 @@ dependencies = [ "libc", "redox_syscall", "smallvec", - "windows-targets", + "windows-targets 0.52.6", ] +[[package]] +name = "paste" +version = "1.0.15" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "57c0d7b74b563b49d38dae00a0c37d4d6de9b432382b2892f0574ddcae73fd0a" + [[package]] name = "pathdiff" version = "0.2.1" @@ -809,14 +1399,52 @@ 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" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "96de42df36bb9bba5542fe9f1a054b8cc87e172759a1868aa05c1f3acc89dfc5" dependencies = [ - "proc-macro2", - "quote", + "proc-macro2 1.0.86", + "quote 1.0.37", ] [[package]] @@ -826,9 +1454,18 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "11ec05c52be0a07b08061f7dd003e7d7092e0472bc731b4af7bb1ef876109802" dependencies = [ "proc-macro-error-attr2", - "proc-macro2", - "quote", - "syn", + "proc-macro2 1.0.86", + "quote 1.0.37", + "syn 2.0.79", +] + +[[package]] +name = "proc-macro2" +version = "0.4.30" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cf3d2011ab5c909338f7887f4fc896d35932e29146c12c8d01da6b22a80ba759" +dependencies = [ + "unicode-xid", ] [[package]] @@ -840,13 +1477,31 @@ 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 = "0.6.13" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6ce23b6b870e8f94f81fb0a363d65d86675884b34a09043c81e5562f11c1f8e1" +dependencies = [ + "proc-macro2 0.4.30", +] + [[package]] name = "quote" version = "1.0.37" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b5b9d34b8991d19d98081b46eacdd8eb58c6f2b201139f7c5f643cc155a633af" dependencies = [ - "proc-macro2", + "proc-macro2 1.0.86", ] [[package]] @@ -879,6 +1534,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" @@ -958,6 +1622,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" @@ -1004,6 +1677,30 @@ dependencies = [ "strum_macros", ] +[[package]] +name = "schemars" +version = "0.8.21" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "09c024468a378b7e36765cd36702b7a90cc3cba11654f6685c8f233408e89e92" +dependencies = [ + "dyn-clone", + "schemars_derive", + "serde", + "serde_json", +] + +[[package]] +name = "schemars_derive" +version = "0.8.21" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b1eee588578aff73f856ab961cd2f79e36bc45d7ded33a7562adba4667aecc0e" +dependencies = [ + "proc-macro2 1.0.86", + "quote 1.0.37", + "serde_derive_internals", + "syn 2.0.79", +] + [[package]] name = "scopeguard" version = "1.2.0" @@ -1028,15 +1725,35 @@ 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" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "243902eda00fad750862fc144cea25caca5e20d615af0a81bee94ca738f1df1f" dependencies = [ - "proc-macro2", - "quote", - "syn", + "proc-macro2 1.0.86", + "quote 1.0.37", + "syn 2.0.79", +] + +[[package]] +name = "serde_derive_internals" +version = "0.29.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "18d26a20a969b9e3fdf2fc2d9f21eda6c40e2de84c9408bb5d3b05d499aae711" +dependencies = [ + "proc-macro2 1.0.86", + "quote 1.0.37", + "syn 2.0.79", ] [[package]] @@ -1060,6 +1777,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" @@ -1097,12 +1824,91 @@ 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 = "similar" +version = "2.6.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1de1d4f81173b03af4c0cbed3c898f6bff5b870e4a7f5d6f4057d62a7a4b686e" + +[[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 = "snafu" +version = "0.4.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b028158eb06caa8345bee10cccfb25fa632beccf0ef5308832b4fd4b78a7db48" +dependencies = [ + "backtrace", + "doc-comment", + "snafu-derive", +] + +[[package]] +name = "snafu-derive" +version = "0.4.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bf50aaef500c248a590e2696e8bf8c7620ca2235b9bb90a70363d82dd1abec6a" +dependencies = [ + "proc-macro2 0.4.30", + "quote 0.6.13", + "syn 0.15.44", +] + +[[package]] +name = "snapbox" +version = "0.6.17" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "840b73eb3148bc3cbc10ebe00ec9bc6d96033e658d022c4adcbf3f35596fd64a" +dependencies = [ + "anstream", + "anstyle", + "normalize-line-endings", + "similar", + "snapbox-macros", +] + +[[package]] +name = "snapbox-macros" +version = "0.3.10" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "16569f53ca23a41bb6f62e0a5084aa1661f4814a67fa33696a79073e03a664af" +dependencies = [ + "anstream", +] + +[[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" @@ -1140,10 +1946,32 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "4c6bee85a5a24955dc440386795aa378cd9cf82acd5f764469152d2270e581be" dependencies = [ "heck", - "proc-macro2", - "quote", + "proc-macro2 1.0.86", + "quote 1.0.37", "rustversion", - "syn", + "syn 2.0.79", +] + +[[package]] +name = "syn" +version = "0.15.44" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9ca4b3b69a77cbe1ffc9e198781b7acb0c7365a883670e8f1c1bc66fba79a5c5" +dependencies = [ + "proc-macro2 0.4.30", + "quote 0.6.13", + "unicode-xid", +] + +[[package]] +name = "syn" +version = "1.0.109" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237" +dependencies = [ + "proc-macro2 1.0.86", + "quote 1.0.37", + "unicode-ident", ] [[package]] @@ -1152,11 +1980,17 @@ version = "2.0.79" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "89132cd0bf050864e1d38dc3bbc07a0eb8e7530af26344d3d2bbbef83499f590" dependencies = [ - "proc-macro2", - "quote", + "proc-macro2 1.0.86", + "quote 1.0.37", "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" @@ -1170,6 +2004,21 @@ dependencies = [ "windows-sys 0.59.0", ] +[[package]] +name = "termcolor" +version = "1.4.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "06794f8f6c5c898b3275aebefa6b8a1cb24cd2c6c79397ab15774837a0bc5755" +dependencies = [ + "winapi-util", +] + +[[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" @@ -1185,9 +2034,9 @@ version = "1.0.64" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "08904e7672f5eb876eaaf87e0ce17857500934f4981c4a0ab2b4aa98baac7fc3" dependencies = [ - "proc-macro2", - "quote", - "syn", + "proc-macro2 1.0.86", + "quote 1.0.37", + "syn 2.0.79", ] [[package]] @@ -1200,6 +2049,15 @@ dependencies = [ "once_cell", ] +[[package]] +name = "threadpool" +version = "1.8.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d050e60b33d41c19108b32cea32164033a9013fe3b46cbd4457559bfbf77afaa" +dependencies = [ + "num_cpus", +] + [[package]] name = "time" version = "0.3.36" @@ -1282,9 +2140,9 @@ version = "0.1.27" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "34704c8d6ebcbc939824180af020566b01a7c01f80641264eba0999f6c2b6be7" dependencies = [ - "proc-macro2", - "quote", - "syn", + "proc-macro2 1.0.86", + "quote 1.0.37", + "syn 2.0.79", ] [[package]] @@ -1340,6 +2198,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" @@ -1352,18 +2222,42 @@ 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" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "7dd6e30e90baa6f72411720665d41d89b9a3d039dc45b8faea1ddd07f617f6af" +[[package]] +name = "unicode-xid" +version = "0.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "fc72304796d0818e357ead4e000d19c9c174ab23dc11093ac919054d20a6a7fc" + [[package]] name = "unsafe-libyaml" version = "0.2.11" @@ -1388,6 +2282,12 @@ version = "0.9.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a" +[[package]] +name = "virtue" +version = "0.0.13" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9dcc60c0624df774c82a0ef104151231d37da4962957d691c011c852b2473314" + [[package]] name = "wait-timeout" version = "0.2.0" @@ -1456,13 +2356,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]] @@ -1471,7 +2380,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]] @@ -1480,28 +2404,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" @@ -1514,24 +2456,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" @@ -1569,7 +2535,7 @@ version = "0.7.35" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e" dependencies = [ - "proc-macro2", - "quote", - "syn", + "proc-macro2 1.0.86", + "quote 1.0.37", + "syn 2.0.79", ] 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/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..0360763f9068 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 = { 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..6973e5014365 --- /dev/null +++ b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs @@ -0,0 +1,811 @@ +// 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}; +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_data_structures::fx::FxHashMap; +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::VarDebugInfoContents; +use stable_mir::mir::mono::Instance; +use stable_mir::mir::{ + BasicBlock, BinOp, Body, BorrowKind, CastKind, ConstOperand, Local, 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>, + local_names: FxHashMap, +} + +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 { + let mut local_names = FxHashMap::default(); + // populate names of locals + for info in instance.body().unwrap().var_debug_info { + if let VarDebugInfoContents::Place(p) = info.value { + if p.projection.is_empty() { + local_names.insert(p.local, info.name); + } + } + } + + Self { tcx, instance, translated, errors, local_names } + } + + 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) => { + 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(); + mir_body.local_decls().for_each(|(local, local_decl)| { + let ty = self.translate_ty(local_decl.ty); + let name = self.local_names.get(&local); + locals.push_with(|index| Var { index, name: name.cloned(), 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/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/src/args/mod.rs b/kani-driver/src/args/mod.rs index 72de44e36014..b32b2e3a52a7 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -278,6 +278,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, @@ -624,6 +628,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(()) } } @@ -914,4 +935,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..d2c0456efdb0 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 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/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/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/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/expected/llbc/basic0/expected b/tests/expected/llbc/basic0/expected new file mode 100644 index 000000000000..45d073737f3b --- /dev/null +++ b/tests/expected/llbc/basic0/expected @@ -0,0 +1,8 @@ +fn test::is_zero(@1: i32) -> bool\ +{\ + let @0: bool; // return\ + let i@1: i32; // arg #1\ + + @0 := copy (i@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..233940af9752 --- /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 s@1: bool; // arg #1 + let x@2: i32; // arg #2 + let y@3: i32; // arg #3 + + if copy (s@1) { + @0 := copy (x@2) + } + else { + @0 := copy (y@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); +}