diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 5a5ad45f17e3..67066d447e19 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -103,13 +103,6 @@ jobs: with: os: ubuntu-24.04 - # Patch Charon so that it compiles. This is temporary until we're able to - # upgrade the pinned commit which requires fixing - # https://github.com/AeneasVerif/charon/issues/806 and updating the - # mir-to-ullbc code - - name: Patch Charon - run: cd charon && git apply ../scripts/charon-patch.diff - - name: Build Kani with Charon run: cargo build-dev -- --features cprover --features llbc diff --git a/Cargo.lock b/Cargo.lock index 93c66a88de52..e6775698de59 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -35,11 +35,12 @@ dependencies = [ [[package]] name = "annotate-snippets" -version = "0.11.5" +version = "0.12.16" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "710e8eae58854cdc1790fcb56cca04d712a17be849eeb81da2a724bf4bae2bc4" +checksum = "f211a51805bc641f3ad5b7664c77d2547af685cc33b4cd8d31964027a46f13f1" dependencies = [ "anstyle", + "memchr", "unicode-width", ] @@ -103,7 +104,7 @@ version = "1.1.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "40c48f72fd53cd289104fc64099abca73db4166ad86ea0b4341abe65af83dadc" dependencies = [ - "windows-sys 0.61.2", + "windows-sys", ] [[package]] @@ -114,7 +115,7 @@ checksum = "291e6a250ff86cd4a820112fb8898808a366d8f9f58ce16d1f538353ad55747d" dependencies = [ "anstyle", "once_cell_polyfill", - "windows-sys 0.61.2", + "windows-sys", ] [[package]] @@ -132,12 +133,6 @@ dependencies = [ "object", ] -[[package]] -name = "arrayvec" -version = "0.7.8" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d3fb67a6e08acf24fdeccbac2cb6ac4305825bd1f117462e0e6f2f193345ad56" - [[package]] name = "assert_cmd" version = "2.2.2" @@ -153,6 +148,15 @@ dependencies = [ "wait-timeout", ] +[[package]] +name = "atomic-polyfill" +version = "1.0.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8cf2bce30dfe09ef0bfaef228b9d414faaf7e563035494d7fe092dba54b300f4" +dependencies = [ + "critical-section", +] + [[package]] name = "autocfg" version = "1.5.1" @@ -189,15 +193,6 @@ dependencies = [ "objc2", ] -[[package]] -name = "brownstone" -version = "3.0.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c5839ee4f953e811bfdcf223f509cb2c6a3e1447959b0bff459405575bc17f22" -dependencies = [ - "arrayvec", -] - [[package]] name = "bstr" version = "1.13.1" @@ -225,6 +220,12 @@ version = "3.20.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "72f5acc6cb2ba439de613abc23857ec3d78374d8ed5ac84e9d11336e87da8649" +[[package]] +name = "byteorder" +version = "1.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1fd0f2584146f6f2ef48085050886acf353beff7305ebd1ae69500e27c67f64b" + [[package]] name = "bytes" version = "1.12.1" @@ -288,17 +289,21 @@ checksum = "f079e83a288787bcd14a6aea84cee5c87a67c5a3e660c30f557a3d24761b3527" [[package]] name = "charon" -version = "0.1.91" +version = "0.1.273" dependencies = [ "annotate-snippets", "anstream 0.6.21", "anyhow", "assert_cmd", + "bitflags 2.13.2", "clap", - "colored", "convert_case", "derive_generic_visitor", + "either", "env_logger", + "extension-traits", + "hashbrown 0.15.5", + "hax-adt-into", "index_vec", "indexmap", "indoc", @@ -307,22 +312,25 @@ dependencies = [ "log", "macros", "nom", - "nom-supreme", - "num-bigint", - "num-rational", - "petgraph 0.6.5", + "paste", + "petgraph", + "postcard", + "rustc-hash", "rustc_version", "serde", - "serde-map-to-array", "serde_json", "serde_stacker", + "serde_state_perfect_derive", + "smallvec", "stacker", - "strip-ansi-escapes", + "syn 1.0.109", "take_mut", + "tempfile", "toml 0.8.23", "tracing", "tracing-subscriber", "tracing-tree 0.4.0", + "ustr", "which 7.0.3", ] @@ -378,20 +386,19 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "1c133bc6a41be0d194c306b5506d15e6feeea7b1d6604bd3f8310dfb2ca96486" [[package]] -name = "colorchoice" -version = "1.0.5" +name = "cobs" +version = "0.3.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1d07550c9036bf2ae0c684c4297d503f838287c83c53686d05370d0e139ae570" +checksum = "0fa961b519f0b462e3a3b4a34b64d119eeaca1d59af726fe450bbba07a9fc0a1" +dependencies = [ + "thiserror 2.0.21", +] [[package]] -name = "colored" -version = "2.2.0" +name = "colorchoice" +version = "1.0.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "117725a109d387c937a1533ce01b450cbde6b88abceea8473c4d7a85853cda3c" -dependencies = [ - "lazy_static", - "windows-sys 0.59.0", -] +checksum = "1d07550c9036bf2ae0c684c4297d503f838287c83c53686d05370d0e139ae570" [[package]] name = "comfy-table" @@ -438,7 +445,7 @@ dependencies = [ "encode_unicode", "libc", "unicode-width", - "windows-sys 0.61.2", + "windows-sys", ] [[package]] @@ -487,6 +494,12 @@ dependencies = [ "libc", ] +[[package]] +name = "critical-section" +version = "1.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "790eea4361631c5e7d22598ecd5723ff611904e3344ce8720784c93e3d83d40b" + [[package]] name = "crossbeam-deque" version = "0.8.8" @@ -640,18 +653,19 @@ checksum = "7cd812cc2bc1d69d4764bd80df88b4317eaef9e773c75226407d9bc0876b211c" [[package]] name = "derive_generic_visitor" -version = "0.1.3" +version = "1.1.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8f97cf6da50801d6ce913a011f0588883b9ef894603adc3cb40ebe1eb1ac43e5" +checksum = "972dd93b5dba0d648ee42fabc3c9756b1e5732e0fe514193c0e3008013305b7e" dependencies = [ "derive_generic_visitor_macros", + "itertools 0.14.0", ] [[package]] name = "derive_generic_visitor_macros" -version = "0.1.1" +version = "1.1.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "885f5274163b5b1720591c0c24b34350a0b05e4774351f9fb3d13c192d8c995b" +checksum = "079c2738859003286c4940c2f7bd50f2f6f7f7688ad53cf8e6acda2dd0a918f2" dependencies = [ "convert_case", "darling", @@ -703,6 +717,18 @@ version = "1.18.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "252afb9ae5eaa683babdc6a068b3f5726eb19e05070c731f9b2a23a7c3e8ed34" +[[package]] +name = "embedded-io" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ef1a6892d9eef45c8fa6b9e0086428a2cca8491aca8f787c534a3d6d0bcb3ced" + +[[package]] +name = "embedded-io" +version = "0.6.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "edd0f118536f44f5ccd48bcb8b111bdc3de888b58c74639dfb034a357d0f206d" + [[package]] name = "encode_unicode" version = "1.0.0" @@ -751,7 +777,36 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "39cab71617ae0d63f51a36d69f866391735b51691dbda63cf6f96d042b63efeb" dependencies = [ "libc", - "windows-sys 0.61.2", + "windows-sys", +] + +[[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", + "quote", + "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]] @@ -766,12 +821,6 @@ version = "0.1.14" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "aedcfb3409746eddb02b9e19ebda1c3394f759a152e48ee875a0844d1b955484" -[[package]] -name = "fixedbitset" -version = "0.4.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0ce7134b9999ecaf8bcd65542e436736ef32ddca1b3e06094cb6ec5755203b80" - [[package]] name = "fixedbitset" version = "0.5.7" @@ -875,7 +924,16 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "27b92c49194cd4f20bad0d9875503c951993f4249c0cfd210a49ed39ef072a0c" dependencies = [ "ahash", - "petgraph 0.8.3", + "petgraph", +] + +[[package]] +name = "hash32" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b0c35f58762feb77d74ebe43bdbc3210f09be9fe6742234d573bacc26ed92b67" +dependencies = [ + "byteorder", ] [[package]] @@ -902,6 +960,31 @@ version = "0.17.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ed5909b6e89a2db4456e54cd5f673791d7eca6732202bbf2a9cc504fe2f9b84a" +[[package]] +name = "hax-adt-into" +version = "0.3.5" +dependencies = [ + "itertools 0.13.0", + "proc-macro2", + "quote", + "syn 1.0.109", + "tracing", +] + +[[package]] +name = "heapless" +version = "0.7.17" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cdc6457c0eb62c71aac4bc17216026d8410337c4126773b9c5daba343f17964f" +dependencies = [ + "atomic-polyfill", + "hash32", + "rustc_version", + "serde", + "spin", + "stable_deref_trait", +] + [[package]] name = "heck" version = "0.5.0" @@ -914,7 +997,7 @@ version = "0.5.12" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "cc627f471c528ff0c4a49e1d5e60450c8f6461dd6d10ba9dcd3a61d3dff7728d" dependencies = [ - "windows-sys 0.61.2", + "windows-sys", ] [[package]] @@ -947,12 +1030,6 @@ version = "1.0.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b9e0384b61958566e926dc50660321d12159025e767c18e043daf26b70104c39" -[[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" @@ -1011,6 +1088,15 @@ dependencies = [ "either", ] +[[package]] +name = "itertools" +version = "0.14.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2b192c782037fadd9cfa75548310488aabdbf3d2da73885b31bd0abd03351285" +dependencies = [ + "either", +] + [[package]] name = "itertools" version = "0.15.0" @@ -1063,12 +1149,6 @@ dependencies = [ "syn 2.0.119", ] -[[package]] -name = "joinery" -version = "2.1.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "72167d68f5fce3b8655487b8038691a3c9984ee769590f93f2a631f4ad64e4f5" - [[package]] name = "js-sys" version = "0.3.106" @@ -1253,7 +1333,7 @@ version = "0.1.0" dependencies = [ "proc-macro2", "quote", - "syn 2.0.119", + "syn 1.0.109", ] [[package]] @@ -1291,7 +1371,7 @@ checksum = "4b18443e9c262bfe8fa82f51666e2642c53393f7e5c27b3e1aeab922cff5b9d8" dependencies = [ "libc", "wasi", - "windows-sys 0.61.2", + "windows-sys", ] [[package]] @@ -1316,26 +1396,13 @@ dependencies = [ "minimal-lexical", ] -[[package]] -name = "nom-supreme" -version = "0.8.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2bd3ae6c901f1959588759ff51c95d24b491ecb9ff91aa9c2ef4acc5b1dcab27" -dependencies = [ - "brownstone", - "indent_write", - "joinery", - "memchr", - "nom", -] - [[package]] name = "nu-ansi-term" version = "0.50.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "7957b9740744892f114936ab4a57b3f487491bbeafaf8083688b16841a4240e5" dependencies = [ - "windows-sys 0.61.2", + "windows-sys", ] [[package]] @@ -1617,7 +1684,7 @@ dependencies = [ "objc2", "objc2-foundation", "objc2-ui-kit", - "windows-sys 0.61.2", + "windows-sys", ] [[package]] @@ -1644,20 +1711,16 @@ dependencies = [ ] [[package]] -name = "pathdiff" -version = "0.2.3" +name = "paste" +version = "1.0.15" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "df94ce210e5bc13cb6651479fa48d14f601d9858cfe0467f43ae157023b938d3" +checksum = "57c0d7b74b563b49d38dae00a0c37d4d6de9b432382b2892f0574ddcae73fd0a" [[package]] -name = "petgraph" -version = "0.6.5" +name = "pathdiff" +version = "0.2.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b4c5cc86750666a3ed20bdaf5ca2a0344f9c67674cae0515bec2da16fbaa47db" -dependencies = [ - "fixedbitset 0.4.2", - "indexmap", -] +checksum = "df94ce210e5bc13cb6651479fa48d14f601d9858cfe0467f43ae157023b938d3" [[package]] name = "petgraph" @@ -1665,7 +1728,7 @@ version = "0.8.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "8701b58ea97060d5e5b155d383a69952a60943f0e6dfe30b04c287beb0b27455" dependencies = [ - "fixedbitset 0.5.7", + "fixedbitset", "hashbrown 0.15.5", "indexmap", "serde", @@ -1692,6 +1755,19 @@ dependencies = [ "portable-atomic", ] +[[package]] +name = "postcard" +version = "1.1.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6764c3b5dd454e283a30e6dfe78e9b31096d9e32036b5d1eaac7a6119ccb9a24" +dependencies = [ + "cobs", + "embedded-io 0.4.0", + "embedded-io 0.6.1", + "heapless", + "serde", +] + [[package]] name = "powerfmt" version = "0.2.0" @@ -1866,7 +1942,7 @@ dependencies = [ "errno", "libc", "linux-raw-sys", - "windows-sys 0.61.2", + "windows-sys", ] [[package]] @@ -1896,7 +1972,7 @@ version = "0.0.0" dependencies = [ "csv", "graph-cycles", - "petgraph 0.8.3", + "petgraph", "serde", "strum", "strum_macros", @@ -1928,15 +2004,6 @@ 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_core" version = "1.0.229" @@ -2000,6 +2067,27 @@ dependencies = [ "stacker", ] +[[package]] +name = "serde_state_perfect_derive" +version = "1.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "fee99988af71dac4de7dd0882da328b8089e1b0bf10c4bb68792ec7581fb0375" +dependencies = [ + "serde", + "serde_state_perfect_derive_derive", +] + +[[package]] +name = "serde_state_perfect_derive_derive" +version = "1.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d80d31bfa32e1e337cb392a33c11b6548c0cc888ab1054ce6661aa45f07d28fa" +dependencies = [ + "proc-macro2", + "quote", + "syn 2.0.119", +] + [[package]] name = "serde_test" version = "1.0.177" @@ -2080,6 +2168,21 @@ version = "1.16.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "f9395f0f0eee849a9b707b2f06bb92a6a422090e2123bb2ef8e87a0e61892a8e" +[[package]] +name = "spin" +version = "0.9.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3763264f6b73151db08c50ff20d7d8a0b8796e021cdea7ceedad07b80155fa0e" +dependencies = [ + "lock_api", +] + +[[package]] +name = "stable_deref_trait" +version = "1.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6ce2be8dc25455e1f91df71bfa12ad37d7af1092ae736f3a6cd0e37bc7810596" + [[package]] name = "stacker" version = "0.1.25" @@ -2090,7 +2193,7 @@ dependencies = [ "cfg-if", "libc", "psm", - "windows-sys 0.61.2", + "windows-sys", ] [[package]] @@ -2116,15 +2219,6 @@ dependencies = [ "serde", ] -[[package]] -name = "strip-ansi-escapes" -version = "0.2.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2a8f8038e7e7969abb3f1b7c2a811225e9296da208539e0f79c5251d6cac0025" -dependencies = [ - "vte", -] - [[package]] name = "strsim" version = "0.11.1" @@ -2149,6 +2243,17 @@ dependencies = [ "syn 2.0.119", ] +[[package]] +name = "syn" +version = "1.0.109" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + [[package]] name = "syn" version = "2.0.119" @@ -2187,7 +2292,7 @@ dependencies = [ "getrandom 0.4.3", "once_cell", "rustix", - "windows-sys 0.61.2", + "windows-sys", ] [[package]] @@ -2297,7 +2402,7 @@ dependencies = [ "mio", "pin-project-lite", "signal-hook-registry", - "windows-sys 0.61.2", + "windows-sys", ] [[package]] @@ -2544,6 +2649,19 @@ version = "0.2.11" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "673aac59facbab8a9007c7f6108d11f63b603f7cabff99fabf650fea5c32b861" +[[package]] +name = "ustr" +version = "1.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "18b19e258aa08450f93369cf56dd78063586adf19e92a75b338a800f799a0208" +dependencies = [ + "ahash", + "byteorder", + "lazy_static", + "parking_lot", + "serde", +] + [[package]] name = "utf8parse" version = "0.2.2" @@ -2562,15 +2680,6 @@ version = "0.9.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a" -[[package]] -name = "vte" -version = "0.14.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "231fdcd7ef3037e8330d8e17e61011a2c244126acc0a982f4040ac3f9f0bc077" -dependencies = [ - "memchr", -] - [[package]] name = "wait-timeout" version = "0.2.1" @@ -2703,7 +2812,7 @@ version = "0.1.11" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "c2a7b1c03c876122aa43f3020e6c3c3ee5c05081c9a00739faf7503aeba10d22" dependencies = [ - "windows-sys 0.61.2", + "windows-sys", ] [[package]] @@ -2771,15 +2880,6 @@ dependencies = [ "windows-link", ] -[[package]] -name = "windows-sys" -version = "0.59.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1e38bc4d79ed67fd075bcc251a1c39b32a1776bbe92e5bef1f0bf1f8c531853b" -dependencies = [ - "windows-targets", -] - [[package]] name = "windows-sys" version = "0.61.2" @@ -2789,70 +2889,6 @@ dependencies = [ "windows-link", ] -[[package]] -name = "windows-targets" -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_i686_gnullvm", - "windows_i686_msvc", - "windows_x86_64_gnu", - "windows_x86_64_gnullvm", - "windows_x86_64_msvc", -] - -[[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.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "09ec2a7bb152e2252b53fa7803150007879548bc709c039df7627cabbd05d469" - -[[package]] -name = "windows_i686_gnu" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8e9b5ad5ab802e97eb8e295ac6720e509ee4c243f69d781394014ebfe8bbfa0b" - -[[package]] -name = "windows_i686_gnullvm" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0eee52d38c090b3caa76c563b86c3a4bd71ef1a819287c19d586d7334ae8ed66" - -[[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.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "147a5c80aabfbf0c7d901cb5895d1de30ef2907eb21fbbab29ca94c5b08b1a78" - -[[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.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec" - [[package]] name = "winnow" version = "0.7.15" diff --git a/Cargo.toml b/Cargo.toml index 4217df4b42b4..4433a0575996 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -85,12 +85,3 @@ exclude = [ [workspace.lints.clippy] too_long_first_doc_paragraph = "allow" - -# The pinned Charon sources request `annotate-snippets` from its upstream git -# repository (an unreleased 0.11.5 at the time; since published). Kani forbids -# git dependencies (`deny.toml`: sources.unknown-git = "deny"), so redirect the -# git source to the crates.io release. This only affects dependency resolution: -# the charon-patch.diff applied in the llbc CI job additionally adapts Charon's -# error-rendering code, which was written against the pre-release git API. -[patch."https://github.com/rust-lang/annotate-snippets-rs"] -annotate-snippets = "0.11.5" diff --git a/charon b/charon index b250680abd40..962e40b0d732 160000 --- a/charon +++ b/charon @@ -1 +1 @@ -Subproject commit b250680abd40ff1aaa07081d0497dc2755ed112e +Subproject commit 962e40b0d732e7d011520f08ef1e8c540ec75131 diff --git a/deny.toml b/deny.toml index 3969607c9308..ab296ec67055 100644 --- a/deny.toml +++ b/deny.toml @@ -8,6 +8,13 @@ db-path = "~/.cargo/advisory-db" db-urls = ["https://github.com/rustsec/advisory-db"] yanked = "deny" +ignore = [ + # Unmaintained (not vulnerable) crates that only the LLBC backend pulls in, through charon: + # `paste` directly, `atomic-polyfill` via postcard -> heapless. The LLBC backend is behind the + # `llbc` feature and not part of Kani releases. + { id = "RUSTSEC-2024-0436", reason = "paste is unmaintained; only reached via charon" }, + { id = "RUSTSEC-2023-0089", reason = "atomic-polyfill is unmaintained; only reached via charon" }, +] # This section is considered when running `cargo deny check licenses` # More documentation for the licenses section can be found here: @@ -25,10 +32,7 @@ confidence-threshold = 0.8 exceptions = [ { name = "foldhash", allow=["Zlib"] }, # Transitive dependencies via charon (LLBC backend) - { name = "brownstone", allow=["MPL-2.0"] }, - { name = "colored", allow=["MPL-2.0"] }, - { name = "indent_write", allow=["MPL-2.0"] }, - { name = "nom-supreme", allow=["MPL-2.0"] }, + { name = "ustr", allow=["BSD-2-Clause-Patent"] }, ] [licenses.private] diff --git a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs index 44e1c5fd3b61..136c4efbdbaa 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs @@ -4,7 +4,9 @@ //! 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::codegen_aeneas_llbc::mir_to_ullbc::{ + Context, prepare_translated_crate, record_item_names, +}; use crate::kani_middle::attributes::KaniAttributes; use crate::kani_middle::check_reachable_items; use crate::kani_middle::codegen_units::{CodegenUnit, CodegenUnits}; @@ -12,12 +14,10 @@ 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::QUERY_DB; -use charon_lib::ast::{AnyTransId, TranslatedCrate, meta::ItemOpacity::*, meta::Span}; -use charon_lib::errors::{ErrorCtx, Level}; -use charon_lib::name_matcher::NamePattern; -use charon_lib::options::{MirLevel, TranslateOptions}; -use charon_lib::transform::TransformCtx; -use charon_lib::transform::ctx::TransformPass; +use charon_lib::ast::{ItemId, TranslatedCrate}; +use charon_lib::errors::ErrorCtx; +use charon_lib::options::{CliOpts, Preset, SerializationFormat, TranslateOptions}; +use charon_lib::transform::{TransformCtx, run_transformation_passes}; use kani_metadata::ArtifactType; use kani_metadata::{AssignsContract, CompilerArtifactStub}; use rustc_codegen_ssa::back::archive::{ @@ -46,7 +46,7 @@ use std::any::Any; use std::fs::File; use std::path::Path; use std::time::Instant; -use tracing::{debug, info, trace}; +use tracing::{debug, info}; #[derive(Clone)] pub struct LlbcCodegenBackend {} @@ -105,7 +105,7 @@ impl LlbcCodegenBackend { // Create a Charon transformation context that will be populated with translation results let mut ccx = create_charon_transformation_context(tcx); - let mut id_map: FxHashMap = FxHashMap::default(); + let mut id_map: FxHashMap = FxHashMap::default(); // Translate all the items for item in &items { @@ -127,46 +127,20 @@ impl LlbcCodegenBackend { } } - 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::transform::reorder_decls::Transform {}; - reordered_decls.transform_ctx(&mut ccx); - - // - // ================= - // **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.run(&mut ccx) - } + record_item_names(&mut ccx.translated); - // # Go from ULLBC to LLBC (Low-Level Borrow Calculus) by reconstructing - // the control flow. - // Run the micro-passes that clean up bodies. - for pass in charon_lib::transform::LLBC_PASSES.iter() { - pass.run(&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); - } + // Everything after translation is Charon's own pipeline, run exactly as `charon` runs it, + // so that the LLBC we emit is what Aeneas expects and a Charon bump does not require + // re-deriving its pass list here. + run_transformation_passes(&charon_cli_options(queries.args().print_llbc), &mut ccx); + // Charon has already printed each error, including those of its type check. Stop here + // rather than emit LLBC that Charon considers ill-formed. // TODO: display an error report about the external dependencies, if necessary - if ccx.errors.borrow().error_count > 0 { - todo!() + let error_count = ccx.errors.borrow().error_count; + if error_count > 0 { + tcx.dcx() + .fatal(format!("Charon reported {error_count} error(s) while translating to LLBC")); } let crate_data: charon_lib::export::CrateData = charon_lib::export::CrateData::new(ccx); @@ -178,7 +152,7 @@ impl LlbcCodegenBackend { 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) { + if let Err(()) = crate_data.serialize_to_file(&pb, SerializationFormat::Json) { tcx.sess.dcx().err("Failed to write LLBC file"); } } @@ -397,65 +371,21 @@ where ret } -fn get_translate_options(tcx: &TranslatedCrate, error_ctx: &mut ErrorCtx) -> TranslateOptions { - let mut parse_pattern = |s: &str| match NamePattern::parse(s) { - Ok(p) => Ok(p), - Err(e) => { - let msg = format!("failed to parse pattern `{s}` ({e})"); - Err(error_ctx.span_err(&TranslatedCrate::default(), Span::dummy(), &msg, Level::Error)) - } - }; - let options = tcx.options.clone(); - let item_opacities = { - let mut opacities = vec![]; - - // This is how to treat items that don't match any other pattern. - if options.extract_opaque_bodies { - opacities.push(("_".to_string(), Transparent)); - } else { - opacities.push(("_".to_string(), Foreign)); - } - - // We always include the items from the crate. - opacities.push(("crate".to_owned(), Transparent)); - - for pat in options.include.iter() { - opacities.push((pat.to_string(), Transparent)); - } - for pat in options.opaque.iter() { - opacities.push((pat.to_string(), Opaque)); - } - for pat in options.exclude.iter() { - opacities.push((pat.to_string(), Invisible)); - } - - // We always hide this trait. - opacities.push(("core::alloc::Allocator".to_string(), Invisible)); - opacities - .push(("alloc::alloc::{{impl core::alloc::Allocator for _}}".to_string(), Invisible)); - - opacities - .into_iter() - .filter_map(|(s, opacity)| parse_pattern(&s).ok().map(|pat| (pat, opacity))) - .collect() - }; - TranslateOptions { - mir_level: MirLevel::Built, - translate_all_methods: false, - monomorphize: false, - no_ops_to_function_calls: false, - hide_marker_traits: true, - no_merge_goto_chains: false, - item_opacities, - print_built_llbc: true, - remove_associated_types: Vec::new(), - } +/// The Charon options Kani runs with: Charon's `aeneas` preset, which is the configuration Aeneas +/// consumes -- including which items are opaque and which traits are hidden (`Allocator` and the +/// marker traits), so Kani does not keep a copy of that policy. `print_llbc` makes the final pass +/// pipeline print the LLBC, as `charon --print-llbc` does; the expected tests rely on it. +fn charon_cli_options(print_llbc: bool) -> CliOpts { + let mut options = CliOpts { preset: Some(Preset::Aeneas), print_llbc, ..CliOpts::default() }; + options.apply_preset(); + options } fn create_charon_transformation_context(tcx: TyCtxt) -> TransformCtx { let crate_name = tcx.crate_name(LOCAL_CRATE).as_str().into(); - let translated = TranslatedCrate { crate_name, ..TranslatedCrate::default() }; - let mut errors = ErrorCtx::new(true, false); - let options = get_translate_options(&translated, &mut errors); + let mut translated = TranslatedCrate { crate_name, ..TranslatedCrate::default() }; + prepare_translated_crate(tcx, &mut translated); + let mut errors = ErrorCtx::new(); + let options = TranslateOptions::new(&mut errors, &charon_cli_options(false)); TransformCtx { options, translated, errors: std::cell::RefCell::new(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 index d0e8e1dee03c..a944d227362e 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs @@ -6,51 +6,55 @@ //! This module contains a context for translating stable MIR into Charon's //! unstructured low-level borrow calculus (ULLBC) -use charon_lib::ast::krate::TypeDeclId as CharonTypeDeclId; use charon_lib::ast::meta::{ - AttrInfo as CharonAttrInfo, Loc as CharonLoc, RawSpan as CharonRawSpan, + AttrInfo as CharonAttrInfo, Loc as CharonLoc, SpanData as CharonRawSpan, }; use charon_lib::ast::types::{Ty as CharonTy, TyKind as CharonTyKind}; use charon_lib::ast::{ - AbortKind as CharonAbortKind, AggregateKind as CharonAggregateKind, - AnyTransId as CharonAnyTransId, Assert as CharonAssert, BinOp as CharonBinOp, - Body as CharonBody, BorrowKind as CharonBorrowKind, BuiltinTy as CharonBuiltinTy, - Call as CharonCall, CastKind as CharonCastKind, ConstGeneric as CharonConstGeneric, - ConstGenericVar as CharonConstGenericVar, ConstGenericVarId as CharonConstGenericVarId, - ConstantExpr as CharonConstantExpr, DeBruijnId as CharonDeBruijnId, - DeBruijnVar as CharonDeBruijnVar, Disambiguator as CharonDisambiguator, - ExistentialPredicate as CharonExistentialPredicate, Field as CharonField, - FieldId as CharonFieldId, FieldProjKind as CharonFieldProjKind, File as CharonFile, - FileId as CharonFileId, FileName as CharonFileName, FnOperand as CharonFnOperand, - FnPtr as CharonFnPtr, FunDecl as CharonFunDecl, FunDeclId as CharonFunDeclId, - FunId as CharonFunId, FunIdOrTraitMethodRef as CharonFunIdOrTraitMethodRef, - FunSig as CharonFunSig, GenericArgs as CharonGenericArgs, GenericParams as CharonGenericParams, - GenericsSource as CharonGenericsSource, GlobalDeclId as CharonGlobalDeclId, - GlobalDeclRef as CharonGlobalDeclRef, IntegerTy as CharonIntegerTy, ItemKind as CharonItemKind, - ItemMeta as CharonItemMeta, ItemOpacity as CharonItemOpacity, Literal as CharonLiteral, - LiteralTy as CharonLiteralTy, Locals as CharonLocals, Name as CharonName, - Opaque as CharonOpaque, Operand as CharonOperand, PathElem as CharonPathElem, - Place as CharonPlace, PolyTraitDeclRef as CharonPolyTraitDeclRef, - PredicateOrigin as CharonPredicateOrigin, ProjectionElem as CharonProjectionElem, - RawConstantExpr as CharonRawConstantExpr, RefKind as CharonRefKind, Region as CharonRegion, - RegionBinder as CharonRegionBinder, RegionId as CharonRegionId, RegionVar as CharonRegionVar, - Rvalue as CharonRvalue, ScalarValue as CharonScalarValue, Span as CharonSpan, - TraitClause as CharonTraitClause, TraitClauseId as CharonTraitClauseId, - TraitDecl as CharonTraitDecl, TraitDeclId as CharonTraitDeclId, - TraitDeclRef as CharonTraitDeclRef, TraitImplId as CharonTraitImplId, - TraitRef as CharonTraitRef, TraitRefKind as CharonTraitRefKind, - TranslatedCrate as CharonTranslatedCrate, TypeDecl as CharonTypeDecl, - TypeDeclKind as CharonTypeDeclKind, TypeId as CharonTypeId, TypeVar as CharonTypeVar, - TypeVarId as CharonTypeVarId, UnOp as CharonUnOp, Var as CharonVar, VarId as CharonVarId, - Variant as CharonVariant, VariantId as CharonVariantId, + Abi as CharonAbi, AbortKind as CharonAbortKind, AggregateKind as CharonAggregateKind, + Assert as CharonAssert, BinOp as CharonBinOp, Body as CharonBody, + BorrowKind as CharonBorrowKind, BuiltinAdt as CharonBuiltinAdt, + BuiltinAssertKind as CharonBuiltinAssertKind, BuiltinImplData as CharonBuiltinImplData, + BuiltinPathElem as CharonBuiltinPathElem, Call as CharonCall, CastKind as CharonCastKind, + ConstGenericParam as CharonConstGenericVar, ConstGenericVarId as CharonConstGenericVarId, + ConstantExpr as CharonConstantExpr, ConstantExprKind as CharonRawConstantExpr, + DeBruijnId as CharonDeBruijnId, DeBruijnVar as CharonDeBruijnVar, + Disambiguator as CharonDisambiguator, DropKind as CharonDropKind, Field as CharonField, + FieldId as CharonFieldId, File as CharonFile, FileId as CharonFileId, + FileName as CharonFileName, FloatTy as CharonFloatTy, FnOperand as CharonFnOperand, + FnPtr as CharonFnPtr, FnPtrKind as CharonFunIdOrTraitMethodRef, FunDecl as CharonFunDecl, + FunDeclId as CharonFunDeclId, FunSig as CharonFunSig, FunSource as CharonFunSource, + GenericArgs as CharonGenericArgs, GenericParams as CharonGenericParams, + GlobalDeclId as CharonGlobalDeclId, GlobalDeclRef as CharonGlobalDeclRef, IntTy as CharonIntTy, + IntegerTy as CharonIntegerTy, IntegerValue as CharonScalarValue, ItemId as CharonAnyTransId, + ItemMeta as CharonItemMeta, ItemOpacity as CharonItemOpacity, + LifetimeMutability as CharonLifetimeMutability, Local as CharonVar, LocalId as CharonVarId, + Locals as CharonLocals, Name as CharonName, Operand as CharonOperand, + OverflowMode as CharonOverflowMode, PathElem as CharonPathElem, Place as CharonPlace, + PolyTraitDeclRef as CharonPolyTraitDeclRef, PredicateOrigin as CharonPredicateOrigin, + ProjectionElem as CharonProjectionElem, PtrMetadata as CharonPtrMetadata, + RefKind as CharonRefKind, Region as CharonRegion, RegionBinder as CharonRegionBinder, + RegionId as CharonRegionId, RegionParam as CharonRegionVar, Rvalue as CharonRvalue, + ScalarTy as CharonLiteralTy, Span as CharonSpan, SwitchData as CharonSwitchData, + SwitchScrutinee as CharonSwitchScrutinee, TargetInfo as CharonTargetInfo, + TraitClauseId as CharonTraitClauseId, TraitDecl as CharonTraitDecl, + TraitDeclId as CharonTraitDeclId, TraitDeclRef as CharonTraitDeclRef, + TraitDeclSource as CharonTraitDeclSource, TraitImplId as CharonTraitImplId, + TraitParam as CharonTraitClause, TraitRef as CharonTraitRef, + TraitRefKind as CharonTraitRefKind, TranslatedCrate as CharonTranslatedCrate, + TypeDecl as CharonTypeDecl, TypeDeclId as CharonTypeDeclId, TypeDeclKind as CharonTypeDeclKind, + TypeDeclRef as CharonTypeDeclRef, TypeParam as CharonTypeVar, TypeSource as CharonTypeSource, + TypeVarId as CharonTypeVarId, UIntTy as CharonUIntTy, UnOp as CharonUnOp, + Variance as CharonVariance, Variant as CharonVariant, VariantId as CharonVariantId, + WithRetag as CharonWithRetag, }; use charon_lib::errors::{Error as CharonError, ErrorCtx as CharonErrorCtx, Level as CharonLevel}; -use charon_lib::ids::Vector as CharonVector; +use charon_lib::ids::IndexVec as CharonVector; use charon_lib::ullbc_ast::{ BlockData as CharonBlockData, BlockId as CharonBlockId, BodyContents as CharonBodyContents, - ExprBody as CharonExprBody, RawStatement as CharonRawStatement, - RawTerminator as CharonRawTerminator, Statement as CharonStatement, - SwitchTargets as CharonSwitchTargets, Terminator as CharonTerminator, + BranchId as CharonBranchId, ExprBody as CharonExprBody, Statement as CharonStatement, + StatementKind as CharonRawStatement, Terminator as CharonTerminator, + TerminatorKind as CharonRawTerminator, }; use charon_lib::{error_assert, raise_error, register_error}; use core::panic; @@ -59,15 +63,16 @@ use rustc_data_structures::fx::FxHashMap; use rustc_middle::ty::{TyCtxt, TypingEnv}; use rustc_public::mir::mono::{Instance, InstanceDef}; use rustc_public::mir::{ - AggregateKind, BasicBlock, BinOp, Body, BorrowKind, CastKind, ConstOperand, Local, Mutability, - Operand, Place, ProjectionElem, Rvalue, Statement, StatementKind, SwitchTargets, Terminator, - TerminatorKind, UnOp, VarDebugInfoContents, + AggregateKind, AssertMessage, BasicBlock, BinOp, Body, BorrowKind, CastKind, ConstOperand, + Local, Mutability, Operand, Place, ProjectionElem, Rvalue, Statement, StatementKind, + SwitchTargets, Terminator, TerminatorKind, UnOp, VarDebugInfoContents, }; use rustc_public::rustc_internal; use rustc_public::ty::{ - AdtDef, AdtKind, Allocation, ConstantKind, FnDef, GenericArgKind, GenericArgs, - GenericParamDefKind, IntTy, MirConst, Region, RegionKind, RigidTy, Span, TraitDecl, TraitDef, - Ty, TyConst, TyConstKind, TyKind, UintTy, VariantIdx, + AdtDef, AdtKind, Allocation, BoundRegionKind, BoundVariableKind, ConstantKind, FieldDef, FnDef, + GenericArgKind, GenericArgs, GenericParamDefKind, IntTy, MirConst, PolyFnSig, Region, + RegionKind, RigidTy, Span, TraitDecl, TraitDef, Ty, TyConst, TyConstKind, TyKind, UintTy, + VariantIdx, }; use rustc_public::{CrateDef, CrateDefType, DefId}; use rustc_public_bridge::IndexedVal; @@ -89,6 +94,25 @@ pub struct Context<'a, 'tcx> { /// Block ID of the synthetic block that aborts. It is the target of every call's unwind edge /// (Kani does not model unwinding) and of the return edge of calls that never return. abort_block: CharonBlockId, + /// How Charon numbers the generic parameters of the item whose declaration is being + /// translated (see [`ItemGenerics`]); `None` outside of declarations. + item_generics: Option, + /// The number of binders (`for<..>` of function-pointer types) entered since the item's + /// own binder, i.e. the De Bruijn index of the item's generic parameters. + binder_depth: usize, +} + +/// How Charon numbers the generic parameters of a type or function declaration: per kind +/// (regions, types, const generics), parent generics first, and a function's late-bound regions +/// after its early-bound ones. rustc instead numbers early-bound parameters across all kinds. +#[derive(Clone, Default)] +struct ItemGenerics { + /// rustc's parameter index -> position among the parameters of the same kind. + positions: FxHashMap, + /// The number of early-bound region parameters. + early_regions: usize, + /// Whether the item is a function, whose signature binds late-bound regions. + binds_late_regions: bool, } impl<'a, 'tcx> Context<'a, 'tcx> { @@ -112,13 +136,81 @@ impl<'a, 'tcx> Context<'a, 'tcx> { } let file_to_id: HashMap = HashMap::new(); let abort_block = CharonBlockId::from_usize(0); - Self { tcx, instance, translated, id_map, errors, local_names, file_to_id, abort_block } + Self { + tcx, + instance, + translated, + id_map, + errors, + local_names, + file_to_id, + abort_block, + item_generics: None, + binder_depth: 0, + } } fn tcx(&self) -> TyCtxt<'tcx> { self.tcx } + /// Charon's numbering of the generic parameters of `def_id` (see [`ItemGenerics`]). + fn item_generics(&self, def_id: DefId, binds_late_regions: bool) -> ItemGenerics { + let mut chain = Vec::new(); + let mut next = Some(rustc_internal::internal(self.tcx, def_id)); + while let Some(def_id) = next { + let generics = self.tcx.generics_of(def_id); + chain.push(generics); + next = generics.parent; + } + let mut positions = FxHashMap::default(); + let (mut regions, mut types, mut consts) = (0, 0, 0); + for param in chain.iter().rev().flat_map(|generics| generics.own_params.iter()) { + let counter = match param.kind { + rustc_middle::ty::GenericParamDefKind::Lifetime => &mut regions, + rustc_middle::ty::GenericParamDefKind::Type { .. } => &mut types, + rustc_middle::ty::GenericParamDefKind::Const { .. } => &mut consts, + }; + positions.insert(param.index, *counter); + *counter += 1; + } + ItemGenerics { positions, early_regions: regions, binds_late_regions } + } + + /// Run `f` with the generic parameters of `def_id` in scope, as for translating its + /// declaration. Declarations nest (a field's type may need its own declaration), so the + /// enclosing scope is restored afterwards. + fn with_item_generics( + &mut self, + def_id: DefId, + binds_late_regions: bool, + f: impl FnOnce(&mut Self) -> T, + ) -> T { + let generics = self.item_generics(def_id, binds_late_regions); + let outer_generics = self.item_generics.replace(generics); + let outer_depth = std::mem::replace(&mut self.binder_depth, 0); + let result = f(self); + self.item_generics = outer_generics; + self.binder_depth = outer_depth; + result + } + + /// The signature of `fndef` as declared, with its early-bound regions as parameters. + /// `FnDef::fn_sig` erases those, which would lose e.g. the `'a` in + /// `fn f<'a, T: 'a>(x: &'a T)`. + fn declared_fn_sig(&self, fndef: FnDef) -> PolyFnSig { + let def_id = rustc_internal::internal(self.tcx, fndef.def_id()); + rustc_internal::stable(self.tcx.fn_sig(def_id).instantiate_identity().skip_normalization()) + } + + /// Charon's position of the early-bound parameter with rustc index `index`. + fn param_position(&self, index: u32) -> usize { + self.item_generics + .as_ref() + .and_then(|generics| generics.positions.get(&index).copied()) + .unwrap_or(index as usize) + } + fn span_err(&mut self, span: CharonSpan, msg: &str, level: CharonLevel) -> CharonError { self.errors.span_err(self.translated, span, msg, level) } @@ -129,24 +221,18 @@ impl<'a, 'tcx> Context<'a, 'tcx> { match self.translated.trait_decls.get(trait_decl_id) { None => { let trait_decl = TraitDef::declaration(&trait_def); - let consts = Vec::new(); - let const_defaults = IndexMap::new(); - let types = Vec::new(); - let type_clauses = Vec::new(); - let type_defaults = IndexMap::new(); - let methods = Vec::new(); - let parent_clauses = CharonVector::new(); + // As before, Kani declares the trait with its generics only: no implied + // clauses, associated items or methods. let c_traitdecl = CharonTraitDecl { def_id: trait_decl_id, item_meta: self.translate_item_meta_from_defid(trait_def_id), + src: CharonTraitDeclSource::Normal, generics: self.generic_params_from_traitdecl(trait_decl), - parent_clauses, - type_clauses, - consts, - const_defaults, - types, - type_defaults, - methods, + implied_clauses: CharonVector::new(), + consts: Default::default(), + types: Default::default(), + methods: Default::default(), + vtable: None, }; self.translated.trait_decls.set_slot(trait_decl_id, c_traitdecl); trait_decl_id @@ -180,20 +266,16 @@ impl<'a, 'tcx> Context<'a, 'tcx> { continue; }; let c_traitdecl_id = self.translate_traitdecl(trait_def); - let c_genarg = self - .translate_generic_args_without_trait(trait_ref.args().clone(), trait_def.def_id()); + let c_genarg = self.translate_generic_args_without_trait(trait_ref.args().clone()); let c_polytrait = CharonPolyTraitDeclRef { regions: CharonVector::new(), skip_binder: CharonTraitDeclRef { - trait_id: c_traitdecl_id, + id: c_traitdecl_id, generics: Box::new(c_genarg.clone()), }, }; let debr = CharonDeBruijnVar::free(CharonTraitClauseId::from_usize(i)); - let c_traitref = CharonTraitRef { - kind: CharonTraitRefKind::Clause(debr), - trait_decl_ref: c_polytrait, - }; + let c_traitref = CharonTraitRef::new(CharonTraitRefKind::Clause(debr), c_polytrait); c_trait_refs.push(c_traitref); c_spans.push(self.translate_span(rustc_internal::stable(span))); } @@ -222,12 +304,11 @@ impl<'a, 'tcx> Context<'a, 'tcx> { continue; }; let c_traitdecl_id = self.translate_traitdecl(trait_def); - let c_genarg = self - .translate_generic_args_without_trait(trait_ref.args().clone(), trait_def.def_id()); + let c_genarg = self.translate_generic_args_without_trait(trait_ref.args().clone()); let c_polytrait = CharonPolyTraitDeclRef { regions: CharonVector::new(), skip_binder: CharonTraitDeclRef { - trait_id: c_traitdecl_id, + id: c_traitdecl_id, generics: Box::new(c_genarg), }, }; @@ -261,7 +342,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { } }; let funcname = item_meta.name.clone(); - let signature = self.translate_function_signature(self.instance); + let (generics, signature) = self.translate_function_signature(self.instance); //We temporarily don't translate the body of built-in function //because at the current step, we want to extend the amount of syntaxes //and test each syntax we extended (in tests/expected/llbc). @@ -269,22 +350,21 @@ impl<'a, 'tcx> Context<'a, 'tcx> { //translation of the tests fail because of not-yet-implemented syntaxes //Example: tests/expected/llbc/option test fails because of the function std::ptr::drop_in_place let body = if is_builtin { - Err(CharonOpaque) + CharonBody::Opaque } else { - let bodyid = match self.translate_function_body(self.instance) { + match self.translate_function_body(self.instance) { Ok(body) => body, Err(_) => { return Err(()); } - }; - Ok(bodyid) + } }; let fun_decl = CharonFunDecl { def_id: fid, item_meta, - signature, - kind: CharonItemKind::Regular, - is_global_initializer: None, + generics, + signature: Box::new(signature), + src: CharonFunSource::Normal, body, }; if self.translated.fun_decls.get(fid).is_none() { @@ -303,7 +383,6 @@ impl<'a, 'tcx> Context<'a, 'tcx> { debug!("***Not found fun_decl_id!"); let tid = CharonAnyTransId::Fun(self.translated.fun_decls.reserve_slot()); self.id_map.insert(def_id, tid); - self.translated.all_ids.insert(tid); tid } }; @@ -319,7 +398,6 @@ impl<'a, 'tcx> Context<'a, 'tcx> { debug!("***Not found type_decl_id!"); let tid = CharonAnyTransId::Type(self.translated.type_decls.reserve_slot()); self.id_map.insert(def_id, tid); - self.translated.all_ids.insert(tid); tid } }; @@ -335,7 +413,6 @@ impl<'a, 'tcx> Context<'a, 'tcx> { debug!("***Not found trait_decl_id!"); let tid = CharonAnyTransId::TraitDecl(self.translated.trait_decls.reserve_slot()); self.id_map.insert(def_id, tid); - self.translated.all_ids.insert(tid); tid } }; @@ -351,7 +428,6 @@ impl<'a, 'tcx> Context<'a, 'tcx> { debug!("***Not found trait_impl_id!"); let tid = CharonAnyTransId::TraitImpl(self.translated.trait_impls.reserve_slot()); self.id_map.insert(def_id, tid); - self.translated.all_ids.insert(tid); tid } }; @@ -367,7 +443,6 @@ impl<'a, 'tcx> Context<'a, 'tcx> { debug!("***Not found global_decl_id!"); let tid = CharonAnyTransId::Global(self.translated.global_decls.reserve_slot()); self.id_map.insert(def_id, tid); - self.translated.all_ids.insert(tid); tid } }; @@ -376,22 +451,24 @@ impl<'a, 'tcx> Context<'a, 'tcx> { } // similar to register_type_decl_id, but not adding new def_id, used for cases where the def_id has been registered, or in functions that take immut &self - fn get_type_decl_id(&self, def_id: DefId) -> CharonTypeDeclId { - debug!("register_type_decl_id: {:?}", def_id); - let tid = *self.id_map.get(&def_id).unwrap(); - debug!("register_type_decl_id: {:?}", self.id_map); - tid.try_into().unwrap() - } - //This function is implemented according to how Charon encodes discriminants fn get_discriminant(&mut self, discr_val: u128, ty: Ty) -> CharonScalarValue { let ty = self.translate_ty(ty); - let int_ty = *ty.kind().as_literal().unwrap().as_integer().unwrap(); + let int_ty = *ty.kind().as_scalar().unwrap().as_integer().unwrap(); CharonScalarValue::from_bits(int_ty, discr_val) } //Get the GenericParams for Trait Decl, which is neccessary in Trait Decl translation fn generic_params_from_traitdecl(&mut self, traitdecl: TraitDecl) -> CharonGenericParams { + self.with_item_generics(traitdecl.def_id.def_id(), false, |this| { + this.generic_params_from_traitdecl_in_scope(traitdecl) + }) + } + + fn generic_params_from_traitdecl_in_scope( + &mut self, + traitdecl: TraitDecl, + ) -> CharonGenericParams { let genvec = traitdecl.generics_of().params; let mut c_regions: CharonVector = CharonVector::new(); let mut c_types: CharonVector = CharonVector::new(); @@ -399,39 +476,40 @@ impl<'a, 'tcx> Context<'a, 'tcx> { CharonVector::new(); for gendef in genvec.iter() { let genkind = gendef.kind.clone(); - let index = gendef.index as usize; + let index = self.param_position(gendef.index); let name = gendef.name.clone(); match genkind { GenericParamDefKind::Lifetime => { let c_region = CharonRegionVar { index: CharonRegionId::from_usize(index), name: Some(name), + variance: CharonVariance::Unknown, + mutability: CharonLifetimeMutability::Unknown, }; c_regions.push(c_region); } GenericParamDefKind::Type { has_default: _, synthetic: _ } => { - let c_region = - CharonTypeVar { index: CharonTypeVarId::from_usize(index), name }; + let c_region = CharonTypeVar { + index: CharonTypeVarId::from_usize(index), + name, + variance: CharonVariance::Unknown, + }; c_types.push(c_region); } GenericParamDefKind::Const { has_default: _ } => { let def_id_internal = rustc_internal::internal(self.tcx, gendef.def_id.0); let pc_internal = rustc_middle::ty::ParamConst { - index: index as u32, + index: gendef.index, name: rustc_span::Symbol::intern(&name.clone()), }; let paramenv = TypingEnv::post_analysis(self.tcx, def_id_internal).param_env; let ty_internal = pc_internal.find_const_ty_from_env(paramenv); let ty_stable = rustc_internal::stable(ty_internal); let trans_ty = self.translate_ty(ty_stable); - let lit_ty = match trans_ty.kind() { - CharonTyKind::Literal(lit) => *lit, - _ => panic!("generic_params_from_fndef: not a literal type"), - }; let c_constgeneric = CharonConstGenericVar { index: CharonConstGenericVarId::from_usize(index), name, - ty: lit_ty, + ty: trans_ty, }; c_const_generics.push(c_constgeneric); } @@ -449,7 +527,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { } //Get the GenericParams for Func Decl, which is neccessary in Func Decl translation - fn generic_params_from_fndef(&mut self, fndef: FnDef, input: Vec) -> CharonGenericParams { + fn generic_params_from_fndef(&mut self, fndef: FnDef, sig: &PolyFnSig) -> CharonGenericParams { let genvec = match fndef.ty().kind() { TyKind::RigidTy(RigidTy::FnDef(_, genarg)) => genarg.0, _ => panic!("generic_params_from_fndef: not an FnDef"), @@ -464,8 +542,10 @@ impl<'a, 'tcx> Context<'a, 'tcx> { GenericArgKind::Lifetime(region) => match region.kind { RegionKind::ReEarlyParam(epr) => { let c_region = CharonRegionVar { - index: CharonRegionId::from_usize(epr.index as usize), + index: CharonRegionId::from_usize(self.param_position(epr.index)), name: Some(epr.name), + variance: CharonVariance::Unknown, + mutability: CharonLifetimeMutability::Unknown, }; c_regions.push(c_region); } @@ -474,8 +554,9 @@ impl<'a, 'tcx> Context<'a, 'tcx> { GenericArgKind::Type(ty) => match ty.kind() { TyKind::Param(paramty) => { let c_typevar = CharonTypeVar { - index: CharonTypeVarId::from_usize(paramty.index as usize), + index: CharonTypeVarId::from_usize(self.param_position(paramty.index)), name: paramty.name, + variance: CharonVariance::Unknown, }; c_types.push(c_typevar); } @@ -492,14 +573,12 @@ impl<'a, 'tcx> Context<'a, 'tcx> { let ty_internal = pc_internal.find_const_ty_from_env(paramenv); let ty_stable = rustc_internal::stable(ty_internal); let trans_ty = self.translate_ty(ty_stable); - let lit_ty = match trans_ty.kind() { - CharonTyKind::Literal(lit) => *lit, - _ => panic!("generic_params_from_fndef: not a literal type"), - }; let c_constgeneric = CharonConstGenericVar { - index: CharonConstGenericVarId::from_usize(paramtc.index as usize), + index: CharonConstGenericVarId::from_usize( + self.param_position(paramtc.index), + ), name: paramtc.name.clone(), - ty: lit_ty, + ty: trans_ty, }; c_const_generics.push(c_constgeneric); } @@ -507,15 +586,15 @@ impl<'a, 'tcx> Context<'a, 'tcx> { }, } } - for inpty in input.iter() { - if let TyKind::RigidTy(RigidTy::Ref(r, _, _)) = inpty.kind() { - if let RegionKind::ReBound(_, br) = r.kind { - let id = br.var as usize; - let c_region = - CharonRegionVar { index: CharonRegionId::from_usize(id), name: None }; - c_regions.push(c_region); - } - } + // The signature's late-bound regions, numbered after the early-bound ones, as Charon + // does. They are all in the binder, wherever in the signature they occur. + for name in late_bound_regions(sig) { + c_regions.push_with(|index| CharonRegionVar { + index, + name, + variance: CharonVariance::Unknown, + mutability: CharonLifetimeMutability::Unknown, + }); } let trait_clauses = self.get_traitclauses_from_defid(fndef.def_id()); CharonGenericParams { @@ -545,8 +624,10 @@ impl<'a, 'tcx> Context<'a, 'tcx> { GenericArgKind::Lifetime(region) => match region.kind { RegionKind::ReEarlyParam(epr) => { let c_region = CharonRegionVar { - index: CharonRegionId::from_usize(epr.index as usize), + index: CharonRegionId::from_usize(self.param_position(epr.index)), name: Some(epr.name), + variance: CharonVariance::Unknown, + mutability: CharonLifetimeMutability::Unknown, }; c_regions.push(c_region); } @@ -555,8 +636,9 @@ impl<'a, 'tcx> Context<'a, 'tcx> { GenericArgKind::Type(ty) => match ty.kind() { TyKind::Param(paramty) => { let c_typevar = CharonTypeVar { - index: CharonTypeVarId::from_usize(paramty.index as usize), + index: CharonTypeVarId::from_usize(self.param_position(paramty.index)), name: paramty.name, + variance: CharonVariance::Unknown, }; c_types.push(c_typevar); } @@ -574,14 +656,12 @@ impl<'a, 'tcx> Context<'a, 'tcx> { let ty_internal = pc_internal.find_const_ty_from_env(paramenv); let ty_stable = rustc_internal::stable(ty_internal); let trans_ty = self.translate_ty(ty_stable); - let lit_ty = match trans_ty.kind() { - CharonTyKind::Literal(lit) => *lit, - _ => panic!("generic_params_from_adtdef: not a literal type"), - }; let c_constgeneric = CharonConstGenericVar { - index: CharonConstGenericVarId::from_usize(paramtc.index as usize), + index: CharonConstGenericVarId::from_usize( + self.param_position(paramtc.index), + ), name: paramtc.name.clone(), - ty: lit_ty, + ty: trans_ty, }; c_const_generics.push(c_constgeneric); } @@ -602,12 +682,18 @@ impl<'a, 'tcx> Context<'a, 'tcx> { } fn translate_adtdef(&mut self, adt_def: AdtDef) -> CharonTypeDecl { - let c_genparam = self.generic_params_from_adtdef(adt_def); + self.with_item_generics(adt_def.def_id(), false, |this| { + this.translate_adtdef_in_scope(adt_def) + }) + } + + fn translate_adtdef_in_scope(&mut self, adt_def: AdtDef) -> CharonTypeDecl { + let def_id = adt_def.def_id(); + let c_typedeclid = self.register_type_decl_id(def_id); + let generics = self.generic_params_from_adtdef(adt_def); let item_meta = self.translate_item_meta_adt(adt_def).unwrap(); - match adt_def.kind() { + let kind = match adt_def.kind() { AdtKind::Enum => { - let def_id = adt_def.def_id(); - let c_typedeclid = self.register_type_decl_id(def_id); let mut c_variants: CharonVector = CharonVector::new(); for (var_idx, var_def) in adt_def.variants_iter().enumerate() { @@ -615,26 +701,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { // so the enumeration index is the variant's `VariantIdx`. // `VariantDef::idx` is no longer publicly accessible. let variant_idx = VariantIdx::to_val(var_idx); - let mut c_fields: CharonVector = - CharonVector::new(); - for field_def in var_def.fields() { - let c_field_ty = self.translate_ty(field_def.ty()); - let c_field_name = Some(field_def.name); - let c_span = self.translate_span(adt_def.span()); - let c_field = CharonField { - span: c_span, - attr_info: CharonAttrInfo { - attributes: Vec::new(), - inline: None, - rename: None, - public: true, - }, - name: c_field_name, - ty: c_field_ty, - }; - c_fields.push(c_field); - } - let var_name = var_def.name(); + let fields = self.translate_fields(adt_def, var_def.fields()); let span = self.translate_span(adt_def.span()); let adtdef_internal = rustc_internal::internal(self.tcx, adt_def); @@ -645,63 +712,112 @@ impl<'a, 'tcx> Context<'a, 'tcx> { let discr_ty = rustc_internal::stable(discr.ty); let c_discr = self.get_discriminant(discr_val, discr_ty); - let c_variant = CharonVariant { + let c_varidx = c_variants.push_with(|id| CharonVariant { + id, span, - attr_info: CharonAttrInfo { - attributes: Vec::new(), - inline: None, - rename: None, - public: true, - }, - name: var_name, - fields: c_fields, + attr_info: default_attr_info(), + name: var_def.name(), + fields, discriminant: c_discr, - }; - let c_varidx = c_variants.push(c_variant); + }); assert_eq!(c_varidx.index(), var_idx); } - let typedecl = CharonTypeDecl { - def_id: c_typedeclid, - generics: c_genparam, - kind: CharonTypeDeclKind::Enum(c_variants), - item_meta, - }; - self.translated.type_decls.set_slot(c_typedeclid, typedecl.clone()); - typedecl + CharonTypeDeclKind::Enum(c_variants) } AdtKind::Struct => { - let def_id = adt_def.def_id(); - let c_typedeclid = self.register_type_decl_id(def_id); - let mut c_fields: CharonVector = CharonVector::new(); let only_variant = *adt_def.variants().first().unwrap(); - let fields = only_variant.fields(); - for field_def in fields { - let c_field_ty = self.translate_ty(field_def.ty()); - let c_field_name = Some(field_def.name); - let c_span = self.translate_span(adt_def.span()); - let c_field = CharonField { - span: c_span, - attr_info: CharonAttrInfo { - attributes: Vec::new(), - inline: None, - rename: None, - public: true, - }, - name: c_field_name, - ty: c_field_ty, - }; - c_fields.push(c_field); - } - let typedecl = CharonTypeDecl { - def_id: c_typedeclid, - generics: c_genparam, - kind: CharonTypeDeclKind::Struct(c_fields), - item_meta, - }; - self.translated.type_decls.set_slot(c_typedeclid, typedecl.clone()); - typedecl + CharonTypeDeclKind::Struct(self.translate_fields(adt_def, only_variant.fields())) } _ => todo!(), + }; + let typedecl = CharonTypeDecl { + def_id: c_typedeclid, + item_meta, + generics, + src: CharonTypeSource::Normal, + kind, + layout: Default::default(), + // Kani only translates sized ADTs. + ptr_metadata: CharonPtrMetadata::None, + }; + self.translated.type_decls.set_slot(c_typedeclid, typedecl.clone()); + typedecl + } + + fn translate_fields( + &mut self, + adt_def: AdtDef, + fields: Vec, + ) -> CharonVector { + let mut c_fields: CharonVector = CharonVector::new(); + for field_def in fields { + let ty = self.translate_ty(field_def.ty()); + let span = self.translate_span(adt_def.span()); + // Tuple-struct and tuple-variant fields are named by their position, which Charon + // spells `_0`, `_1`, ... + let is_positional = field_def.name.chars().all(|c| c.is_ascii_digit()); + let name = if is_positional { format!("_{}", field_def.name) } else { field_def.name }; + c_fields.push(CharonField { + span, + attr_info: default_attr_info(), + name, + is_positional, + ty, + }); + } + c_fields + } + + /// The type declaration of `str`. Charon declares it as the builtin struct `str { _0: [u8] }` + /// (upstream synthesizes the same item), rather than as a builtin type without a declaration. + fn str_type_decl_ref(&mut self) -> CharonTypeDeclRef { + // One declaration per crate: look for it, since a `Context` only lives for one function. + let existing = self + .translated + .type_decls + .iter() + .find(|decl| matches!(decl.src, CharonTypeSource::Builtin(CharonBuiltinAdt::Str))) + .map(|decl| decl.def_id); + let id = match existing { + Some(id) => id, + None => { + let id = self.translated.type_decls.reserve_slot(); + let span = CharonSpan::dummy(); + let name = CharonName { + name: vec![CharonPathElem::Builtin( + CharonBuiltinPathElem::Str, + CharonDisambiguator::ZERO, + )], + }; + let u8_ty = CharonTy::new(CharonTyKind::Scalar(CharonLiteralTy::Integer( + CharonIntegerTy::Unsigned(CharonUIntTy::U8), + ))); + let mut fields = CharonVector::new(); + fields.push(CharonField { + span, + attr_info: default_attr_info(), + name: "_0".to_owned(), + is_positional: true, + // No `Sized` proof, as in `translate_rigid_ty`. + ty: CharonTy::mk_slice(u8_ty, None), + }); + let decl = CharonTypeDecl { + def_id: id, + item_meta: item_meta(span, name), + generics: CharonGenericParams::empty(), + src: CharonTypeSource::Builtin(CharonBuiltinAdt::Str), + kind: CharonTypeDeclKind::Struct(fields), + layout: Default::default(), + ptr_metadata: CharonPtrMetadata::Length, + }; + self.translated.type_decls.set_slot(id, decl); + id + } + }; + CharonTypeDeclRef { + id, + generics: Box::new(CharonGenericArgs::empty()), + builtin: Some(CharonBuiltinAdt::Str), } } @@ -712,78 +828,20 @@ impl<'a, 'tcx> Context<'a, 'tcx> { ) -> Result { let span = self.translate_instance_span(instance); let name = self.def_to_name(instance.def)?; - // TODO: populate the source text - let source_text = None; - // TODO: populate the attribute info - let attr_info = - CharonAttrInfo { 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 = CharonItemOpacity::Transparent; - - Ok(CharonItemMeta { - span, - source_text, - attr_info, - name, - is_local, - opacity, - lang_item: None, - }) + Ok(item_meta(span, name)) } fn translate_item_meta_from_defid(&mut self, defid: DefId) -> CharonItemMeta { let def_id = rustc_internal::internal(self.tcx(), defid); let span = self.translate_span(rustc_internal::stable(self.tcx.def_span(def_id))); let name = self.defid_to_name(defid).unwrap(); - // TODO: populate the source text - let source_text = None; - // TODO: populate the attribute info - let attr_info = - CharonAttrInfo { 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 = CharonItemOpacity::Transparent; - - CharonItemMeta { span, source_text, attr_info, name, is_local, opacity, lang_item: None } + item_meta(span, name) } fn translate_item_meta_adt(&mut self, adt: AdtDef) -> Result { let span = self.translate_span(adt.span()); let name = self.adtdef_to_name(adt)?; - // TODO: populate the source text - let source_text = None; - // TODO: populate the attribute info - let attr_info = - CharonAttrInfo { 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 = CharonItemOpacity::Transparent; - - Ok(CharonItemMeta { - span, - source_text, - attr_info, - name, - is_local, - opacity, - lang_item: None, - }) + Ok(item_meta(span, name)) } fn is_builtin_fun(&mut self, func_def: InstanceDef) -> bool { @@ -987,8 +1045,13 @@ impl<'a, 'tcx> Context<'a, 'tcx> { let file_id = match self.file_to_id.get(&filename) { Some(file_id) => *file_id, None => { - let file = CharonFile { name: filename.clone(), contents: None }; - let file_id = self.translated.files.push(file); + let crate_name = self.translated.crate_name.clone(); + let file_id = self.translated.files.push_with(|id| CharonFile { + id, + name: filename.clone(), + crate_name, + contents: None, + }); self.file_to_id.insert(filename, file_id); file_id } @@ -996,42 +1059,53 @@ impl<'a, 'tcx> Context<'a, 'tcx> { let lineinfo = span.get_lines(); let rspan = CharonRawSpan { file_id, - beg: CharonLoc { line: lineinfo.start_line, col: lineinfo.start_col }, - end: CharonLoc { line: lineinfo.end_line, col: lineinfo.end_col }, + beg: CharonLoc { line: loc(lineinfo.start_line), col: loc(lineinfo.start_col) }, + end: CharonLoc { line: loc(lineinfo.end_line), col: loc(lineinfo.end_col) }, }; // TODO: populate `generated_from_span` info - CharonSpan { span: rspan, generated_from_span: None } + CharonSpan::new(rspan, None) } - fn translate_function_signature(&mut self, instance: Instance) -> CharonFunSig { + /// The generics and the signature of `instance`: Charon keeps the generics on the `FunDecl`. + fn translate_function_signature( + &mut self, + instance: Instance, + ) -> (CharonGenericParams, CharonFunSig) { let fndef = match instance.ty().kind() { TyKind::RigidTy(RigidTy::FnDef(fndef, _)) => fndef, _ => panic!("Expected a function type"), }; - let value = fndef.fn_sig().value; - let inputs = value.inputs().to_vec(); - let c_genparam = self.generic_params_from_fndef(fndef, inputs.clone()); - let c_inputs: Vec = inputs.iter().map(|ty| self.translate_ty(*ty)).collect(); - let c_output = self.translate_ty(value.output()); - // TODO: populate the rest of the information (`is_unsafe`, `is_closure`, etc.) - CharonFunSig { + let sig = self.declared_fn_sig(fndef); + let value = sig.value.clone(); + let (c_genparam, c_inputs, c_output) = + self.with_item_generics(fndef.def_id(), true, |this| { + let c_genparam = this.generic_params_from_fndef(fndef, &sig); + let c_inputs: Vec = + value.inputs().iter().map(|ty| this.translate_ty(*ty)).collect(); + let c_output = this.translate_ty(value.output()); + (c_genparam, c_inputs, c_output) + }); + // TODO: populate the rest of the information (`is_unsafe`, `abi`, etc.) + let sig = CharonFunSig { is_unsafe: false, - is_closure: false, - closure_info: None, - generics: c_genparam, + abi: CharonAbi::Rust, + is_variadic: false, inputs: c_inputs, output: c_output, - } + }; + (c_genparam, sig) } - fn translate_function_body(&mut self, instance: Instance) -> Result { + fn translate_function_body(&mut self, instance: Instance) -> Result { let fndef = match instance.ty().kind() { TyKind::RigidTy(RigidTy::FnDef(fndef, _)) => fndef, _ => panic!("Expected a function type"), }; + // This is the generic body, so its types refer to the function's generic parameters. let mir_body = fndef.body().unwrap(); - let body = self.translate_body(mir_body); + let body = + self.with_item_generics(fndef.def_id(), true, |this| this.translate_body(mir_body)); Ok(body) } @@ -1052,25 +1126,25 @@ impl<'a, 'tcx> Context<'a, 'tcx> { // Add the synthetic block that aborts (Kani does not model unwinding). let abort_block = CharonBlockData { statements: Vec::new(), - terminator: CharonTerminator { - span: span.clone(), - content: CharonRawTerminator::Abort(CharonAbortKind::UndefinedBehavior), - comments_before: Vec::new(), - }, + terminator: CharonTerminator::new( + span, + CharonRawTerminator::Abort(CharonAbortKind::UndefinedBehavior), + ), }; body.push(abort_block); - assert_eq!(self.abort_block.index(), body.elem_count() - 1); + assert_eq!(self.abort_block.index(), body.len() - 1); - let body_expr = CharonExprBody { span, locals, body, comments: Vec::new() }; + // TODO: Kani does not bind any region in bodies. + let body_expr = + CharonExprBody { span, bound_body_regions: 0, locals, body, comments: Vec::new() }; CharonBody::Unstructured(body_expr) } fn translate_generic_args(&mut self, ga: GenericArgs, defid: DefId) -> CharonGenericArgs { - let target = CharonGenericsSource::Item(*self.id_map.get(&defid).unwrap()); let genvec = ga.0; let mut c_regions: CharonVector = CharonVector::new(); let mut c_types: CharonVector = CharonVector::new(); - let mut c_const_generics: CharonVector = + let mut c_const_generics: CharonVector = CharonVector::new(); for genkind in genvec.iter() { let gk = genkind.clone(); @@ -1084,7 +1158,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { c_types.push(c_ty); } GenericArgKind::Const(tc) => { - let c_const_generic = self.tyconst_to_constgeneric(tc); + let c_const_generic = self.tyconst_to_constgeneric(tc, None); c_const_generics.push(c_const_generic); } } @@ -1096,7 +1170,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { let traitgenarg = trait_ref.trait_decl_ref.skip_binder.generics.clone(); let t_regions: CharonVector = CharonVector::new(); let mut t_types: CharonVector = CharonVector::new(); - let t_const_generics: CharonVector = + let t_const_generics: CharonVector = CharonVector::new(); for tyvar in traitgenarg.types.iter() { match tyvar.kind() { @@ -1116,24 +1190,26 @@ impl<'a, 'tcx> Context<'a, 'tcx> { types: t_types, const_generics: t_const_generics, trait_refs: trait_ref.trait_decl_ref.skip_binder.generics.trait_refs.clone(), - target: target.clone(), }; - let traitdecl_id = trait_ref.trait_decl_ref.skip_binder.trait_id; + let traitdecl_id = trait_ref.trait_decl_ref.skip_binder.id; let subs_traitdeclref = CharonPolyTraitDeclRef { regions: trait_ref.trait_decl_ref.regions.clone(), skip_binder: CharonTraitDeclRef { - trait_id: traitdecl_id, + id: traitdecl_id, generics: Box::new(generics.clone()), }, }; - let subs_traitref = CharonTraitRef { - kind: CharonTraitRefKind::BuiltinOrAuto { - trait_decl_ref: subs_traitdeclref.clone(), + // TODO: this proof is a placeholder, as it was before Charon changed the + // representation: Kani does not resolve which impl proves the clause. + let subs_traitref = CharonTraitRef::new( + CharonTraitRefKind::BuiltinOrAuto { + builtin_data: CharonBuiltinImplData::Auto, parent_trait_refs: CharonVector::new(), - types: Vec::new(), + types: Default::default(), + vtable: None, }, - trait_decl_ref: subs_traitdeclref, - }; + subs_traitdeclref, + ); trait_refs.push(subs_traitref); } CharonGenericArgs { @@ -1141,20 +1217,14 @@ impl<'a, 'tcx> Context<'a, 'tcx> { types: c_types, const_generics: c_const_generics, trait_refs, - target, } } - fn translate_generic_args_without_trait( - &mut self, - ga: GenericArgs, - defid: DefId, - ) -> CharonGenericArgs { - let target = CharonGenericsSource::Item(*self.id_map.get(&defid).unwrap()); + fn translate_generic_args_without_trait(&mut self, ga: GenericArgs) -> CharonGenericArgs { let genvec = ga.0; let mut c_regions: CharonVector = CharonVector::new(); let mut c_types: CharonVector = CharonVector::new(); - let mut c_const_generics: CharonVector = + let mut c_const_generics: CharonVector = CharonVector::new(); for genkind in genvec.iter() { let gk = genkind.clone(); @@ -1168,7 +1238,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { c_types.push(c_ty); } GenericArgKind::Const(tc) => { - let c_const_generic = self.tyconst_to_constgeneric(tc); + let c_const_generic = self.tyconst_to_constgeneric(tc, None); c_const_generics.push(c_const_generic); } } @@ -1178,7 +1248,6 @@ impl<'a, 'tcx> Context<'a, 'tcx> { types: c_types, const_generics: c_const_generics, trait_refs: CharonVector::new(), - target, } } @@ -1187,8 +1256,8 @@ impl<'a, 'tcx> Context<'a, 'tcx> { TyKind::RigidTy(rigid_ty) => self.translate_rigid_ty(rigid_ty), TyKind::Param(paramty) => { let debr = CharonDeBruijnVar::Bound( - CharonDeBruijnId::new(0), - CharonTypeVarId::from_usize(paramty.index as usize), + CharonDeBruijnId::new(self.binder_depth), + CharonTypeVarId::from_usize(self.param_position(paramty.index)), ); CharonTy::new(CharonTyKind::TypeVar(debr)) } @@ -1196,58 +1265,52 @@ impl<'a, 'tcx> Context<'a, 'tcx> { } } - fn tyconst_to_constgeneric(&self, tyconst: TyConst) -> CharonConstGeneric { + /// A type-level constant (an array length or a const generic argument). Charon merged its + /// separate const-generic representation into `ConstantExpr`. + fn tyconst_to_constgeneric( + &mut self, + tyconst: TyConst, + param_ty: Option, + ) -> CharonConstantExpr { match tyconst.kind() { TyConstKind::Value(ty, alloc) => { - let c_raw_constexpr = self.translate_allocation(alloc, *ty); - translate_constant_expr_to_const_generic(c_raw_constexpr).unwrap() + let kind = self.translate_allocation(alloc, *ty); + CharonConstantExpr::new(kind, self.translate_ty(*ty)) } TyConstKind::Param(paramc) => { let debr = CharonDeBruijnVar::Bound( - CharonDeBruijnId::new(0), - CharonConstGenericVarId::from_usize(paramc.index as usize), + CharonDeBruijnId::new(self.binder_depth), + CharonConstGenericVarId::from_usize(self.param_position(paramc.index)), ); - CharonConstGeneric::Var(debr) + // Neither `TyConst` nor `ParamConst` carries the parameter's type. + let ty = param_ty.unwrap_or_else(|| todo!("const generic parameter {paramc:?}")); + CharonConstantExpr::new(CharonRawConstantExpr::Var(debr), ty) } _ => todo!(), } } + /// Translate a type, following Charon's own translation (`translate_ty`): arrays and slices + /// carry no `Sized` proof (the `aeneas` preset hides marker traits), tuples are the builtin + /// tuple ADT (the preset does not generate tuple structs), and `Box` is tagged as builtin. fn translate_rigid_ty(&mut self, rigid_ty: RigidTy) -> CharonTy { debug!("translate_rigid_ty: {rigid_ty:?}"); match rigid_ty { - RigidTy::Bool => CharonTy::new(CharonTyKind::Literal(CharonLiteralTy::Bool)), - RigidTy::Char => CharonTy::new(CharonTyKind::Literal(CharonLiteralTy::Char)), + RigidTy::Bool => CharonTy::new(CharonTyKind::Scalar(CharonLiteralTy::Bool)), + RigidTy::Char => CharonTy::new(CharonTyKind::Scalar(CharonLiteralTy::Char)), RigidTy::Int(it) => { - CharonTy::new(CharonTyKind::Literal(CharonLiteralTy::Integer(translate_int_ty(it)))) + CharonTy::new(CharonTyKind::Scalar(CharonLiteralTy::Integer(translate_int_ty(it)))) } - RigidTy::Uint(uit) => CharonTy::new(CharonTyKind::Literal(CharonLiteralTy::Integer( + RigidTy::Uint(uit) => CharonTy::new(CharonTyKind::Scalar(CharonLiteralTy::Integer( translate_uint_ty(uit), ))), RigidTy::Never => CharonTy::new(CharonTyKind::Never), - RigidTy::Str => CharonTy::new(CharonTyKind::Adt( - CharonTypeId::Builtin(CharonBuiltinTy::Str), - // TODO: find out whether any of the information below should be - // populated for strings - CharonGenericArgs::empty(CharonGenericsSource::Builtin), - )), + RigidTy::Str => CharonTy::new(CharonTyKind::Adt(self.str_type_decl_ref())), RigidTy::Array(ty, tyconst) => { let c_ty = self.translate_ty(ty); - let c_const_generic = self.tyconst_to_constgeneric(tyconst); - let mut c_types = CharonVector::new(); - let mut c_const_generics = CharonVector::new(); - c_types.push(c_ty); - c_const_generics.push(c_const_generic); - CharonTy::new(CharonTyKind::Adt( - CharonTypeId::Builtin(CharonBuiltinTy::Array), - CharonGenericArgs { - regions: CharonVector::new(), - types: c_types, - const_generics: c_const_generics, - trait_refs: CharonVector::new(), - target: CharonGenericsSource::Builtin, - }, - )) + // An array length is always a `usize`. + let len = self.tyconst_to_constgeneric(tyconst, Some(CharonTy::mk_usize())); + CharonTy::mk_array(c_ty, len, None) } RigidTy::Ref(region, ty, mutability) => CharonTy::new(CharonTyKind::Ref( self.translate_region(region), @@ -1259,20 +1322,24 @@ impl<'a, 'tcx> Context<'a, 'tcx> { )), 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 = CharonGenericArgs::new_for_builtin(types); - CharonTy::new(CharonTyKind::Adt(CharonTypeId::Tuple, generic_args)) + CharonTy::new(CharonTyKind::Adt(CharonTypeDeclRef { + id: CharonTypeDeclId::UNIT, + generics: Box::new(CharonGenericArgs::new_types(types)), + builtin: Some(CharonBuiltinAdt::Tuple), + })) } - 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()); + RigidTy::FnDef(def_id, args) => { + let fn_ptr = CharonFnPtr { + kind: Box::new(CharonFunIdOrTraitMethodRef::Fun( + self.register_fun_decl_id(def_id.def_id()), + )), + generics: Box::new(self.translate_generic_args(args, def_id.def_id())), + }; // TODO: populate regions? - let rb = CharonRegionBinder { + CharonTy::new(CharonTyKind::FnDef(CharonRegionBinder { regions: CharonVector::new(), - skip_binder: (inputs, output), - }; - CharonTy::new(CharonTyKind::Arrow(rb)) + skip_binder: fn_ptr, + })) } RigidTy::Adt(adt_def, genarg) => { let def_id = adt_def.def_id(); @@ -1281,17 +1348,18 @@ impl<'a, 'tcx> Context<'a, 'tcx> { self.translate_adtdef(adt_def); } let c_generic_args = self.translate_generic_args(genarg, adt_def.def_id()); - CharonTy::new(CharonTyKind::Adt(CharonTypeId::Adt(c_typedeclid), c_generic_args)) - } - RigidTy::Slice(ty) => { - let c_ty = self.translate_ty(ty); - let mut c_types = CharonVector::new(); - c_types.push(c_ty); - CharonTy::new(CharonTyKind::Adt( - CharonTypeId::Builtin(CharonBuiltinTy::Slice), - CharonGenericArgs::new_for_builtin(c_types), - )) + let internal = rustc_internal::internal(self.tcx, def_id); + let builtin = self + .tcx + .is_lang_item(internal, rustc_hir::attrs::lang_items::LangItem::OwnedBox) + .then_some(CharonBuiltinAdt::Box); + CharonTy::new(CharonTyKind::Adt(CharonTypeDeclRef { + id: c_typedeclid, + generics: Box::new(c_generic_args), + builtin, + })) } + RigidTy::Slice(ty) => CharonTy::mk_slice(self.translate_ty(ty), None), RigidTy::RawPtr(ty, mutability) => { let c_ty = self.translate_ty(ty); CharonTy::new(CharonTyKind::RawPtr( @@ -1303,19 +1371,33 @@ impl<'a, 'tcx> Context<'a, 'tcx> { )) } RigidTy::FnPtr(polyfunsig) => { + let mut regions = CharonVector::new(); + for name in late_bound_regions(&polyfunsig) { + regions.push_with(|index| CharonRegionVar { + index, + name, + variance: CharonVariance::Unknown, + mutability: CharonLifetimeMutability::Unknown, + }); + } let value = polyfunsig.value; - let inputs = value.inputs().to_vec(); - let c_inputs: Vec = - inputs.iter().map(|ty| self.translate_ty(*ty)).collect(); - let c_output = self.translate_ty(value.output()); - let rb = CharonRegionBinder { - regions: CharonVector::new(), - skip_binder: (c_inputs, c_output), + self.binder_depth += 1; + let inputs = value.inputs().iter().map(|ty| self.translate_ty(*ty)).collect(); + let output = self.translate_ty(value.output()); + self.binder_depth -= 1; + let sig = CharonFunSig { + is_unsafe: value.safety == rustc_public::mir::Safety::Unsafe, + abi: CharonAbi::Rust, + is_variadic: value.c_variadic, + inputs, + output, }; - CharonTy::new(CharonTyKind::Arrow(rb)) + CharonTy::new(CharonTyKind::FnPtr(CharonRegionBinder { regions, skip_binder: sig })) } + // Kani never translated trait objects: this used to be a placeholder predicate, and + // Charon now requires the real one. RigidTy::Dynamic(_, _) => { - CharonTy::new(CharonTyKind::DynTrait(CharonExistentialPredicate)) + CharonTy::new(CharonTyKind::Error("trait objects are not supported".to_owned())) } _ => todo!("Not yet implemented RigidTy: {:?}", rigid_ty), } @@ -1329,8 +1411,9 @@ impl<'a, 'tcx> Context<'a, 'tcx> { let mut locals = CharonVector::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| CharonVar { index, name: name.cloned(), ty }); + let name = self.local_names.get(&local).cloned(); + let span = self.translate_span(local_decl.span); + locals.push_with(|index| CharonVar { index, name, span, ty, drop_flag_for: None }); }); locals } @@ -1364,11 +1447,10 @@ impl<'a, 'tcx> Context<'a, 'tcx> { StatementKind::Nop => None, _ => todo!(), }; - if let Some(content) = content { + content.map(|content| { let span = self.translate_span(stmt.source_info.span); - return Some(CharonStatement { span, content, comments_before: Vec::new() }); - }; - None + CharonStatement::new(span, content) + }) } fn translate_terminator( @@ -1384,13 +1466,30 @@ impl<'a, 'tcx> Context<'a, 'tcx> { TerminatorKind::Unreachable => { (None, CharonRawTerminator::Abort(CharonAbortKind::UndefinedBehavior)) } - TerminatorKind::Drop { place, target, .. } => ( - Some(CharonRawStatement::Drop(self.translate_place(&place))), - CharonRawTerminator::Goto { target: CharonBlockId::from_usize(*target) }, - ), + TerminatorKind::Drop { place, target, .. } => { + // Charon now carries the drop glue to run. Upstream reaches it through a trait + // proof for its synthetic `Destruct::drop_glue` method, which Kani does not model. + // `resolve_drop_in_place` gives the glue for `T` directly: an instance of the + // `core::ptr::drop_glue` lang item (which `drop_in_place::` merely wraps), and + // Kani already collects it. + let place_ty = place.ty(self.instance.body().unwrap().locals()).unwrap(); + let drop_glue = Instance::resolve_drop_in_place(place_ty); + let fn_ptr = self.translate_fn_ptr(drop_glue); + ( + None, + CharonRawTerminator::Drop { + // Kani translates optimized MIR, where drops are precise. + kind: CharonDropKind::Precise, + place: self.translate_place(place), + fn_ptr, + target: CharonBlockId::from_usize(*target), + on_unwind: self.abort_block, + }, + ) + } TerminatorKind::SwitchInt { discr, targets } => { - let (discr, targets) = self.translate_switch_targets(discr, targets); - (None, CharonRawTerminator::Switch { discr, targets }) + let (data, branches) = self.translate_switch_targets(discr, targets); + (None, CharonRawTerminator::Switch { data, branches }) } TerminatorKind::Call { func, args, destination, target, .. } => { debug!("translate_call: {func:?} {args:?} {destination:?} {target:?}"); @@ -1398,15 +1497,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { let fn_ptr = match fn_ty.kind() { TyKind::RigidTy(RigidTy::FnDef(def, genarg)) => { let instance = Instance::resolve(def, &genarg).unwrap(); - let def_id = instance.def.def_id(); - let fid = self.register_fun_decl_id(def_id); - let genarg_resolve = match instance.ty().kind() { - TyKind::RigidTy(RigidTy::FnDef(_, ga)) => ga, - _ => panic!("Expected a function type"), - }; - let funcid = CharonFunIdOrTraitMethodRef::Fun(CharonFunId::Regular(fid)); - let generics = self.translate_generic_args(genarg_resolve, def_id); - CharonFnPtr { func: Box::new(funcid), generics: Box::new(generics) } + self.translate_fn_ptr(instance) } TyKind::RigidTy(RigidTy::FnPtr(..)) => todo!(), x => unreachable!( @@ -1436,26 +1527,85 @@ impl<'a, 'tcx> Context<'a, 'tcx> { }, ) } - TerminatorKind::Assert { cond, expected, msg: _, target, .. } => ( - Some(CharonRawStatement::Assert(CharonAssert { - cond: self.translate_operand(cond), - expected: *expected, - on_failure: CharonAbortKind::Panic(None), - })), - CharonRawTerminator::Goto { target: CharonBlockId::from_usize(*target) }, + // As in Charon's own translation, an `Assert` terminator whose `check_kind` records + // which check it is: `reconstruct_fallible_operations` needs it to fold an overflow, + // bounds or division check into the operation it guards. + TerminatorKind::Assert { cond, expected, msg, target, .. } => ( + None, + CharonRawTerminator::Assert { + assert: CharonAssert { + cond: self.translate_operand(cond), + expected: *expected, + check_kind: Some(self.translate_assert_kind(msg)), + }, + target: CharonBlockId::from_usize(*target), + on_unwind: self.abort_block, + }, ), _ => todo!(), }; ( - statement.map(|statement| CharonStatement { - span, - content: statement, - comments_before: Vec::new(), - }), - CharonTerminator { span, content: terminator, comments_before: Vec::new() }, + statement.map(|statement| CharonStatement::new(span, statement)), + CharonTerminator::new(span, terminator), ) } + /// A pointer to the function `instance`. + fn translate_fn_ptr(&mut self, instance: Instance) -> CharonFnPtr { + let def_id = instance.def.def_id(); + let fid = self.register_fun_decl_id(def_id); + let genarg_resolve = match instance.ty().kind() { + TyKind::RigidTy(RigidTy::FnDef(_, ga)) => ga, + _ => panic!("Expected a function type"), + }; + let mut generics = self.translate_generic_args(genarg_resolve, def_id); + // The callee's declaration also binds its signature's late-bound regions + // (`generic_params_from_fndef`), which the instance's arguments do not carry. Pass them as + // erased, as Charon's own translation does; Charon's type check rejects the call otherwise. + let sig = match instance.ty().kind() { + TyKind::RigidTy(RigidTy::FnDef(fndef, _)) => fndef.fn_sig(), + _ => panic!("Expected a function type"), + }; + for _ in late_bound_regions(&sig) { + generics.regions.push(CharonRegion::Erased); + } + CharonFnPtr::new(CharonFunIdOrTraitMethodRef::Fun(fid), generics) + } + + /// The check an `Assert` performs, as Charon's own translation (`translate_assert_kind`) + /// records it. + fn translate_assert_kind(&mut self, msg: &AssertMessage) -> CharonBuiltinAssertKind { + use CharonBuiltinAssertKind as K; + match msg { + AssertMessage::BoundsCheck { len, index } => K::BoundsCheck { + len: self.translate_operand(len), + index: self.translate_operand(index), + }, + AssertMessage::Overflow(bin_op, lhs, rhs) => K::Overflow( + translate_bin_op(*bin_op), + self.translate_operand(lhs), + self.translate_operand(rhs), + ), + AssertMessage::OverflowNeg(op) => K::OverflowNeg(self.translate_operand(op)), + AssertMessage::DivisionByZero(op) => K::DivisionByZero(self.translate_operand(op)), + AssertMessage::RemainderByZero(op) => K::RemainderByZero(self.translate_operand(op)), + AssertMessage::MisalignedPointerDereference { required, found } => { + K::MisalignedPointerDereference { + required: self.translate_operand(required), + found: self.translate_operand(found), + } + } + AssertMessage::NullPointerDereference => K::NullPointerDereference, + AssertMessage::NullReferenceConstructed => K::NullReferenceCreated, + AssertMessage::InvalidEnumConstruction(op) => { + K::InvalidEnumConstruction(self.translate_operand(op)) + } + AssertMessage::ResumedAfterReturn(_) => K::ResumedAfterReturn, + AssertMessage::ResumedAfterPanic(_) => K::ResumedAfterPanic, + AssertMessage::ResumedAfterDrop(_) => K::ResumedAfterDrop, + } + } + fn translate_place(&mut self, place: &Place) -> CharonPlace { let projection = self.translate_projection(place, &place.projection); let local = place.local; @@ -1478,14 +1628,24 @@ impl<'a, 'tcx> Context<'a, 'tcx> { fn translate_rvalue(&mut self, rvalue: &Rvalue) -> CharonRvalue { trace!("translate_rvalue: {rvalue:?}"); match rvalue { - Rvalue::Use(operand, _) => CharonRvalue::Use(self.translate_operand(operand)), + Rvalue::Use(operand, retag) => CharonRvalue::Use( + self.translate_operand(operand), + match retag { + rustc_public::mir::WithRetag::Yes => CharonWithRetag::Yes, + rustc_public::mir::WithRetag::No => CharonWithRetag::No, + }, + ), Rvalue::Repeat(_operand, _) => todo!(), - Rvalue::Ref(_region, kind, place) => { - CharonRvalue::Ref(self.translate_place(&place), translate_borrow_kind(kind)) - } + Rvalue::Ref(_region, kind, place) => CharonRvalue::Ref { + place: self.translate_place(place), + kind: translate_borrow_kind(kind), + // Filled in by Charon's `insert_ptr_metadata` pass, as for Charon's own + // translation. + ptr_metadata: missing_ptr_metadata(), + }, Rvalue::AddressOf(_, _) => todo!(), Rvalue::Len(place) => CharonRvalue::Len( - self.translate_place(&place), + self.translate_place(place), self.translate_ty(rvalue.ty(self.instance.body().unwrap().locals()).unwrap()), None, ), @@ -1507,13 +1667,9 @@ impl<'a, 'tcx> Context<'a, 'tcx> { CharonRvalue::UnaryOp(translate_un_op(*op), self.translate_operand(operand)) } Rvalue::Discriminant(place) => { - let c_place = self.translate_place(place); - let ty = self.place_ty(place); - let c_ty = self.translate_ty(ty); + let c_ty = self.translate_ty(self.place_ty(place)); match c_ty.kind() { - CharonTyKind::Adt(CharonTypeId::Adt(c_typedeclid), _) => { - CharonRvalue::Discriminant(c_place, *c_typedeclid) - } + CharonTyKind::Adt(_) => CharonRvalue::Discriminant(self.translate_place(place)), _ => todo!("Not yet implemented:{:?}", c_ty.kind()), } } @@ -1521,62 +1677,41 @@ impl<'a, 'tcx> Context<'a, 'tcx> { Rvalue::Aggregate(agg_kind, operands) => { let c_operands = (*operands).iter().map(|operand| self.translate_operand(operand)).collect(); - let akind = agg_kind.clone(); - match akind { - AggregateKind::Adt(adt_def, variant_id, genarg, _user_anot, field_id) => { - let adt_kind = adt_def.kind(); - match adt_kind { - AdtKind::Enum => { - let def_id = adt_def.def_id(); - let c_typedeclid: CharonTypeDeclId = self.get_type_decl_id(def_id); - let c_type_id = CharonTypeId::Adt(c_typedeclid); - let c_variant_id = - Some(CharonVariantId::from_usize(variant_id.to_index())); - let c_field_id = field_id.map(CharonFieldId::from_usize); - let c_generic_args = - self.translate_generic_args(genarg, adt_def.def_id()); - let c_agg_kind = CharonAggregateKind::Adt( - c_type_id, - c_variant_id, - c_field_id, - Box::new(c_generic_args), - ); - CharonRvalue::Aggregate(c_agg_kind, c_operands) - } - AdtKind::Struct => { - let def_id = adt_def.def_id(); - let c_typedeclid: CharonTypeDeclId = self.get_type_decl_id(def_id); - let c_type_id = CharonTypeId::Adt(c_typedeclid); - let c_variant_id = None; - let c_field_id = None; - let c_generic_args = - self.translate_generic_args(genarg, adt_def.def_id()); - let c_agg_kind = CharonAggregateKind::Adt( - c_type_id, - c_variant_id, - c_field_id, - Box::new(c_generic_args), - ); - CharonRvalue::Aggregate(c_agg_kind, c_operands) - } + // The type the aggregate builds, as `translate_ty` translates it: for ADTs and + // tuples this is the `TypeDeclRef` the aggregate names. + let agg_ty = + self.translate_ty(rvalue.ty(self.instance.body().unwrap().locals()).unwrap()); + match agg_kind.clone() { + AggregateKind::Adt(adt_def, variant_id, _genarg, _user_anot, field_id) => { + let (c_variant_id, c_field_id) = match adt_def.kind() { + AdtKind::Enum => ( + Some(CharonVariantId::from_usize(variant_id.to_index())), + field_id.map(CharonFieldId::from_usize), + ), + AdtKind::Struct => (None, None), _ => todo!(), - } + }; + let tref = agg_ty.as_adt().unwrap().clone(); + CharonRvalue::Aggregate( + CharonAggregateKind::Adt(tref, c_variant_id, c_field_id), + c_operands, + ) + } + AggregateKind::Tuple => { + let tref = agg_ty.as_adt().unwrap().clone(); + CharonRvalue::Aggregate( + CharonAggregateKind::Adt(tref, None, None), + c_operands, + ) } - AggregateKind::Tuple => CharonRvalue::Aggregate( - CharonAggregateKind::Adt( - CharonTypeId::Tuple, - None, - None, - Box::new(CharonGenericArgs::empty(CharonGenericsSource::Builtin)), - ), - c_operands, - ), AggregateKind::Array(ty) => { let c_ty = self.translate_ty(ty); - let cg = CharonConstGeneric::Value(CharonLiteral::Scalar( - CharonScalarValue::Usize(c_operands.len() as u64), - )); - CharonRvalue::Aggregate(CharonAggregateKind::Array(c_ty, cg), c_operands) + let len = CharonConstantExpr::mk_usize(c_operands.len() as u128); + // No `Sized` proof, as in `translate_rigid_ty`. + CharonRvalue::Aggregate( + CharonAggregateKind::Array(c_ty, len, None), + c_operands, + ) } _ => todo!(), } @@ -1591,9 +1726,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { fn translate_operand(&mut self, operand: &Operand) -> CharonOperand { trace!("translate_operand: {operand:?}"); match operand { - Operand::Constant(constant) => { - CharonOperand::Const(Box::new(self.translate_constant(constant))) - } + 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)), // `Operand::RuntimeChecks` (rust-lang/rust#148766) is not yet modeled by the @@ -1605,7 +1738,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { fn translate_constant(&mut self, constant: &ConstOperand) -> CharonConstantExpr { trace!("translate_constant: {constant:?}"); let value = self.translate_constant_value(&constant.const_); - CharonConstantExpr { value, ty: self.translate_ty(constant.ty()) } + CharonConstantExpr::new(value, self.translate_ty(constant.ty())) } fn translate_constant_value(&mut self, constant: &MirConst) -> CharonRawConstantExpr { @@ -1630,23 +1763,26 @@ impl<'a, 'tcx> Context<'a, 'tcx> { fn translate_allocation(&self, alloc: &Allocation, ty: Ty) -> CharonRawConstantExpr { match ty.kind() { TyKind::RigidTy(RigidTy::Int(it)) => { - // `as u128` keeps the two's-complement bits, which `scalar_value` truncates. + // `as u128` keeps the two's-complement bits, which `from_bits` sign-extends. let bits = alloc.read_int().unwrap() as u128; - let scalar_value = scalar_value(translate_int_ty(it), bits); - CharonRawConstantExpr::Literal(CharonLiteral::Scalar(scalar_value)) + CharonRawConstantExpr::Integer(CharonScalarValue::from_bits( + translate_int_ty(it), + bits, + )) } TyKind::RigidTy(RigidTy::Uint(uit)) => { let bits = alloc.read_uint().unwrap(); - let scalar_value = scalar_value(translate_uint_ty(uit), bits); - CharonRawConstantExpr::Literal(CharonLiteral::Scalar(scalar_value)) + CharonRawConstantExpr::Integer(CharonScalarValue::from_bits( + translate_uint_ty(uit), + bits, + )) } TyKind::RigidTy(RigidTy::Bool) => { - let value = alloc.read_bool().unwrap(); - CharonRawConstantExpr::Literal(CharonLiteral::Bool(value)) + CharonRawConstantExpr::Bool(alloc.read_bool().unwrap()) } TyKind::RigidTy(RigidTy::Char) => { let value = char::from_u32(alloc.read_uint().unwrap() as u32); - CharonRawConstantExpr::Literal(CharonLiteral::Char(value.unwrap())) + CharonRawConstantExpr::Char(value.unwrap()) } _ => todo!("Not yet implement {:?}, {:?}", ty, alloc), } @@ -1656,38 +1792,44 @@ impl<'a, 'tcx> Context<'a, 'tcx> { todo!() } + /// Translate a `SwitchInt`, following Charon's own `translate_switch_targets`: one branch per + /// distinct target block, each case value built with `ConstantExprKind::from_bits`, and the + /// `otherwise` target as the fallback. fn translate_switch_targets( &mut self, discr: &Operand, targets: &SwitchTargets, - ) -> (CharonOperand, CharonSwitchTargets) { + ) -> (CharonSwitchData, CharonVector) { 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( - CharonBlockId::from_usize(then_bb), - CharonBlockId::from_usize(else_bb), - ) - } else { - let CharonTyKind::Literal(CharonLiteralTy::Integer(int_ty)) = charon_ty.kind() else { - panic!("Expected integer type for switch discriminant"); - }; - let branches = targets - .branches() - .map(|(value, bb)| (scalar_value(*int_ty, value), CharonBlockId::from_usize(bb))) - .collect(); - let otherwise = CharonBlockId::from_usize(targets.otherwise()); - CharonSwitchTargets::SwitchInt(*int_ty, branches, otherwise) + let switch_ty = self.translate_ty(ty); + let switch_scalar_ty = *switch_ty.kind().as_scalar().unwrap(); + let mut branch_targets: CharonVector = CharonVector::new(); + let mut target_to_branch: IndexMap = IndexMap::new(); + let mut branch_of = |target: usize| { + let target = CharonBlockId::from_usize(target); + *target_to_branch.entry(target).or_insert_with(|| branch_targets.push(target)) + }; + + // Keep Charon's true-then-false traversal order for boolean switches. + let bool_fallback = + (switch_scalar_ty == CharonLiteralTy::Bool).then(|| branch_of(targets.otherwise())); + let branches = targets + .branches() + .map(|(bits, target)| { + let kind = CharonRawConstantExpr::from_bits(&switch_scalar_ty, bits) + .unwrap_or_else(|| panic!("Can't match on type {switch_ty:?}")); + (CharonConstantExpr::new(kind, switch_ty.clone()), branch_of(target)) + }) + .collect(); + let fallback = bool_fallback.unwrap_or_else(|| branch_of(targets.otherwise())); + let data = CharonSwitchData { + scrutinee: CharonSwitchScrutinee::Value(discr), + branches, + fallback: Some(fallback), }; - (discr, switch_targets) + (data, branch_targets) } fn translate_projection( @@ -1710,38 +1852,25 @@ impl<'a, 'tcx> Context<'a, 'tcx> { ProjectionElem::Field(fid, ty) => { let c_fieldid = CharonFieldId::from_usize(*fid); let c_variantid = CharonVariantId::from_usize(current_var); - match current_ty.kind() { - CharonTyKind::Adt(CharonTypeId::Adt(tdid), _) => { - let adttype = self.translated.type_decls.get(*tdid).unwrap(); - match adttype.kind { - CharonTypeDeclKind::Struct(_) => { - let c_fprj = CharonFieldProjKind::Adt(*tdid, None); - current_ty = self.translate_ty(*ty); - c_provec.push(( - CharonProjectionElem::Field(c_fprj, c_fieldid), - current_ty.clone(), - )); - } - CharonTypeDeclKind::Enum(_) => { - let c_fprj = CharonFieldProjKind::Adt(*tdid, Some(c_variantid)); - current_ty = self.translate_ty(*ty); - c_provec.push(( - CharonProjectionElem::Field(c_fprj, c_fieldid), - current_ty.clone(), - )); - } - _ => (), + // As in Charon's own translation: struct and tuple fields are projected + // without a variant, enum fields with the variant `Downcast` selected. + let variant = match current_ty.kind() { + CharonTyKind::Adt(tref) if tref.builtin.is_some() => Some(None), + CharonTyKind::Adt(tref) => { + match self.translated.type_decls.get(tref.id).map(|d| &d.kind) { + Some(CharonTypeDeclKind::Struct(_)) => Some(None), + Some(CharonTypeDeclKind::Enum(_)) => Some(Some(c_variantid)), + _ => None, } } - CharonTyKind::Adt(CharonTypeId::Tuple, genargs) => { - let c_fprj = CharonFieldProjKind::Tuple(genargs.types.elem_count()); - current_ty = self.translate_ty(*ty); - c_provec.push(( - CharonProjectionElem::Field(c_fprj, c_fieldid), - current_ty.clone(), - )); - } - _ => (), + _ => None, + }; + if let Some(variant) = variant { + current_ty = self.translate_ty(*ty); + c_provec.push(( + CharonProjectionElem::Field(variant, c_fieldid), + current_ty.clone(), + )); } } ProjectionElem::Downcast(varid) => { @@ -1773,15 +1902,26 @@ impl<'a, 'tcx> Context<'a, 'tcx> { RegionKind::ReErased => CharonRegion::Erased, RegionKind::ReEarlyParam(epr) => { let debr = CharonDeBruijnVar::bound( - CharonDeBruijnId { index: 0_usize }, - CharonRegionId::from_usize(epr.index as usize), + CharonDeBruijnId { index: self.binder_depth }, + CharonRegionId::from_usize(self.param_position(epr.index)), ); CharonRegion::Var(debr) } RegionKind::ReBound(var, boundregion) => { + // A region bound by the function's own signature is one of the function's + // generics, numbered after its early-bound regions; any other binder is a + // function-pointer type's, whose regions are numbered from zero. + let offset = match &self.item_generics { + Some(generics) + if generics.binds_late_regions && var as usize == self.binder_depth => + { + generics.early_regions + } + _ => 0, + }; let debr = CharonDeBruijnVar::bound( CharonDeBruijnId { index: var as usize }, - CharonRegionId::from_usize(boundregion.var as usize), + CharonRegionId::from_usize(offset + boundregion.var as usize), ); CharonRegion::Var(debr) } @@ -1792,79 +1932,229 @@ impl<'a, 'tcx> Context<'a, 'tcx> { } } -fn translate_int_ty(int_ty: IntTy) -> CharonIntegerTy { - match int_ty { - IntTy::I8 => CharonIntegerTy::I8, - IntTy::I16 => CharonIntegerTy::I16, - IntTy::I32 => CharonIntegerTy::I32, - IntTy::I64 => CharonIntegerTy::I64, - IntTy::I128 => CharonIntegerTy::I128, - // TODO: assumes 64-bit platform - IntTy::Isize => CharonIntegerTy::Isize, +/// Set up a translated crate the way Charon's own driver does before translating any item: +/// record the target, and claim the first type declaration id for the unit type. +/// +/// `TypeDeclId::UNIT` is where every tuple type points when tuple structs are not generated (the +/// `aeneas` preset), so it must be the declaration of `()`; otherwise every tuple would silently +/// name whichever ADT happened to be registered first. +pub fn prepare_translated_crate(tcx: TyCtxt, translated: &mut CharonTranslatedCrate) { + let unit_id = translated.type_decls.reserve_slot(); + assert_eq!(unit_id, CharonTypeDeclId::UNIT, "the unit type must come first"); + let name = CharonName { + name: vec![CharonPathElem::Builtin( + CharonBuiltinPathElem::Tuple(0), + CharonDisambiguator::ZERO, + )], + }; + translated.type_decls.set_slot( + unit_id, + CharonTypeDecl { + def_id: unit_id, + item_meta: item_meta(CharonSpan::dummy(), name), + generics: CharonGenericParams::empty(), + src: CharonTypeSource::Builtin(CharonBuiltinAdt::Tuple), + // What Charon declares for `()` when it does not generate tuple structs. + kind: CharonTypeDeclKind::Opaque, + layout: Default::default(), + ptr_metadata: CharonPtrMetadata::None, + }, + ); + + // As in Charon's `register_target_info`. + let target_data = &tcx.data_layout; + let mut primitive_alignments = charon_lib::ast::SeqHashMap::new(); + primitive_alignments.insert(CharonLiteralTy::Bool, target_data.i8_align.bytes()); + let int = |ty| CharonLiteralTy::Integer(ty); + for (ty, alignment) in [ + (CharonIntegerTy::Signed(CharonIntTy::I8), target_data.i8_align.bytes()), + (CharonIntegerTy::Signed(CharonIntTy::I16), target_data.i16_align.bytes()), + (CharonIntegerTy::Signed(CharonIntTy::I32), target_data.i32_align.bytes()), + (CharonIntegerTy::Signed(CharonIntTy::I64), target_data.i64_align.bytes()), + (CharonIntegerTy::Signed(CharonIntTy::I128), target_data.i128_align.bytes()), + (CharonIntegerTy::Signed(CharonIntTy::Isize), target_data.pointer_align().bytes()), + (CharonIntegerTy::Unsigned(CharonUIntTy::U8), target_data.i8_align.bytes()), + (CharonIntegerTy::Unsigned(CharonUIntTy::U16), target_data.i16_align.bytes()), + (CharonIntegerTy::Unsigned(CharonUIntTy::U32), target_data.i32_align.bytes()), + (CharonIntegerTy::Unsigned(CharonUIntTy::U64), target_data.i64_align.bytes()), + (CharonIntegerTy::Unsigned(CharonUIntTy::U128), target_data.i128_align.bytes()), + (CharonIntegerTy::Unsigned(CharonUIntTy::Usize), target_data.pointer_align().bytes()), + ] { + primitive_alignments.insert(int(ty), alignment); + } + for (ty, alignment) in [ + (CharonFloatTy::F16, target_data.f16_align.bytes()), + (CharonFloatTy::F32, target_data.f32_align.bytes()), + (CharonFloatTy::F64, target_data.f64_align.bytes()), + (CharonFloatTy::F128, target_data.f128_align.bytes()), + ] { + primitive_alignments.insert(CharonLiteralTy::Float(ty), alignment); } + // Not guaranteed by the reference, but by rustc's implementation (as Charon notes). + primitive_alignments.insert(CharonLiteralTy::Char, target_data.i32_align.bytes()); + let c_enum_smallest_repr_ty = match target_data.c_enum_min_size { + rustc_abi::Integer::I8 => CharonIntTy::I8, + rustc_abi::Integer::I16 => CharonIntTy::I16, + rustc_abi::Integer::I32 => CharonIntTy::I32, + rustc_abi::Integer::I64 => CharonIntTy::I64, + rustc_abi::Integer::I128 => CharonIntTy::I128, + }; + let info = CharonTargetInfo { + target_pointer_size: target_data.pointer_size().bytes(), + is_little_endian: matches!(target_data.endian, rustc_abi::Endian::Little), + c_enum_smallest_repr_ty, + primitive_alignments, + }; + translated.target_information.insert(tcx.sess.opts.target_triple.tuple().to_owned(), info); } -fn translate_uint_ty(uint_ty: UintTy) -> CharonIntegerTy { - match uint_ty { - UintTy::U8 => CharonIntegerTy::U8, - UintTy::U16 => CharonIntegerTy::U16, - UintTy::U32 => CharonIntegerTy::U32, - UintTy::U64 => CharonIntegerTy::U64, - UintTy::U128 => CharonIntegerTy::U128, - // TODO: assumes 64-bit platform - UintTy::Usize => CharonIntegerTy::Usize, - } +/// Record every declaration's name in `item_names`, which Charon's passes and printer read and +/// which Charon's own driver fills in as it registers items. +pub fn record_item_names(translated: &mut CharonTranslatedCrate) { + let mut names = Vec::new(); + names.extend( + translated + .type_decls + .iter() + .map(|d| (CharonAnyTransId::Type(d.def_id), d.item_meta.name.clone())), + ); + names.extend( + translated + .fun_decls + .iter() + .map(|d| (CharonAnyTransId::Fun(d.def_id), d.item_meta.name.clone())), + ); + names.extend( + translated + .global_decls + .iter() + .map(|d| (CharonAnyTransId::Global(d.def_id), d.item_meta.name.clone())), + ); + names.extend( + translated + .trait_decls + .iter() + .map(|d| (CharonAnyTransId::TraitDecl(d.def_id), d.item_meta.name.clone())), + ); + names.extend( + translated + .trait_impls + .iter() + .map(|d| (CharonAnyTransId::TraitImpl(d.def_id), d.item_meta.name.clone())), + ); + translated.item_names.extend(names); +} + +/// The placeholder metadata of a borrow, which Charon's `insert_ptr_metadata` pass replaces. This +/// is the same placeholder as Charon's own translation emits. +fn missing_ptr_metadata() -> CharonOperand { + CharonOperand::Const(CharonConstantExpr::new( + CharonRawConstantExpr::Opaque("Missing metadata".to_string()), + CharonTy::mk_unit(), + )) +} + +/// The regions bound by a function signature's binder, in order, with their names if any. They +/// are its late-bound regions, wherever in the signature they occur, each listed once. +fn late_bound_regions(sig: &PolyFnSig) -> Vec> { + sig.bound_vars + .iter() + .map(|var| match var { + // Charon leaves elided (`'_`) regions unnamed, too. + BoundVariableKind::Region(BoundRegionKind::BrNamed(_, name)) if name == "'_" => None, + BoundVariableKind::Region(BoundRegionKind::BrNamed(_, name)) => Some(name.clone()), + BoundVariableKind::Region(BoundRegionKind::BrAnon | BoundRegionKind::BrEnv) => None, + // Only `#![feature(non_lifetime_binders)]` binds anything else here. + BoundVariableKind::Ty(_) | BoundVariableKind::Const => { + todo!("non-region bound variable {var:?}") + } + }) + .collect() } -/// The Charon integer value of type `int_ty` whose two's-complement bits are the low bits of -/// `bits`. MIR hands out both switch values and constant integers as such bit patterns. -fn scalar_value(int_ty: CharonIntegerTy, bits: u128) -> CharonScalarValue { - match int_ty { - CharonIntegerTy::I8 => CharonScalarValue::I8(bits as i8), - CharonIntegerTy::I16 => CharonScalarValue::I16(bits as i16), - CharonIntegerTy::I32 => CharonScalarValue::I32(bits as i32), - CharonIntegerTy::I64 => CharonScalarValue::I64(bits as i64), - CharonIntegerTy::I128 => CharonScalarValue::I128(bits as i128), - // TODO: assumes 64-bit platform, as `translate_int_ty` does. - CharonIntegerTy::Isize => CharonScalarValue::Isize(bits as i64), - CharonIntegerTy::U8 => CharonScalarValue::U8(bits as u8), - CharonIntegerTy::U16 => CharonScalarValue::U16(bits as u16), - CharonIntegerTy::U32 => CharonScalarValue::U32(bits as u32), - CharonIntegerTy::U64 => CharonScalarValue::U64(bits as u64), - CharonIntegerTy::U128 => CharonScalarValue::U128(bits), - CharonIntegerTy::Usize => CharonScalarValue::Usize(bits as u64), +fn loc(n: usize) -> u32 { + u32::try_from(n).expect("source location out of range") +} + +/// The meta information Kani gives every item it translates. +fn item_meta(span: CharonSpan, name: CharonName) -> CharonItemMeta { + CharonItemMeta { + name, + span, + // TODO: populate the source text + source_text: None, + attr_info: default_attr_info(), + // 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 + is_local: true, + // For now, assume all items are transparent + opacity: CharonItemOpacity::Transparent, + lang_item: None, + diagnostic_item: None, + has_errors: false, } } +// TODO: populate the attribute info +fn default_attr_info() -> CharonAttrInfo { + CharonAttrInfo { attributes: Vec::new(), inline: None, rename: None, public: true } +} + +fn translate_int_ty(int_ty: IntTy) -> CharonIntegerTy { + CharonIntegerTy::Signed(match int_ty { + IntTy::I8 => CharonIntTy::I8, + IntTy::I16 => CharonIntTy::I16, + IntTy::I32 => CharonIntTy::I32, + IntTy::I64 => CharonIntTy::I64, + IntTy::I128 => CharonIntTy::I128, + IntTy::Isize => CharonIntTy::Isize, + }) +} + +fn translate_uint_ty(uint_ty: UintTy) -> CharonIntegerTy { + CharonIntegerTy::Unsigned(match uint_ty { + UintTy::U8 => CharonUIntTy::U8, + UintTy::U16 => CharonUIntTy::U16, + UintTy::U32 => CharonUIntTy::U32, + UintTy::U64 => CharonUIntTy::U64, + UintTy::U128 => CharonUIntTy::U128, + UintTy::Usize => CharonUIntTy::Usize, + }) +} + /// The operator of a MIR `CheckedBinaryOp`, which yields `(result, overflowed)`. Charon folds it with -/// the overflow `Assert` that follows into a panicking operator (`remove_dynamic_checks`). +/// the overflow `Assert` that follows into a panicking operator. fn translate_checked_bin_op(bin_op: BinOp) -> CharonBinOp { match bin_op { - BinOp::Add => CharonBinOp::CheckedAdd, - BinOp::Sub => CharonBinOp::CheckedSub, - BinOp::Mul => CharonBinOp::CheckedMul, + BinOp::Add => CharonBinOp::AddChecked, + BinOp::Sub => CharonBinOp::SubChecked, + BinOp::Mul => CharonBinOp::MulChecked, _ => translate_bin_op(bin_op), } } -/// The operator of a plain MIR `BinaryOp`. MIR's `Add`/`Sub`/`Mul` wrap on overflow -- checked -/// arithmetic is a separate `CheckedBinaryOp` -- so they must not become Charon's `Checked*` -/// operators, which produce a `(result, overflowed)` pair. +/// The operator of a plain MIR `BinaryOp`, mapped as Charon's own translation does +/// (`translate_binaryop_kind`): MIR's `Add`/`Sub`/`Mul`/shifts wrap, their `*Unchecked` forms and +/// `Div`/`Rem` are undefined behavior on overflow (MIR guards them with an explicit `Assert`). fn translate_bin_op(bin_op: BinOp) -> CharonBinOp { + use CharonOverflowMode::{UB, Wrap}; match bin_op { - BinOp::AddUnchecked => CharonBinOp::Add, - BinOp::Add => CharonBinOp::WrappingAdd, - BinOp::SubUnchecked => CharonBinOp::Sub, - BinOp::Sub => CharonBinOp::WrappingSub, - BinOp::MulUnchecked => CharonBinOp::Mul, - BinOp::Mul => CharonBinOp::WrappingMul, - BinOp::Div => CharonBinOp::Div, - BinOp::Rem => CharonBinOp::Rem, + BinOp::Add => CharonBinOp::Add(Wrap), + BinOp::AddUnchecked => CharonBinOp::Add(UB), + BinOp::Sub => CharonBinOp::Sub(Wrap), + BinOp::SubUnchecked => CharonBinOp::Sub(UB), + BinOp::Mul => CharonBinOp::Mul(Wrap), + BinOp::MulUnchecked => CharonBinOp::Mul(UB), + BinOp::Div => CharonBinOp::Div(UB), + BinOp::Rem => CharonBinOp::Rem(UB), 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::Shl => CharonBinOp::Shl(Wrap), + BinOp::ShlUnchecked => CharonBinOp::Shl(UB), + BinOp::Shr => CharonBinOp::Shr(Wrap), + BinOp::ShrUnchecked => CharonBinOp::Shr(UB), BinOp::Eq => CharonBinOp::Eq, BinOp::Lt => CharonBinOp::Lt, BinOp::Le => CharonBinOp::Le, @@ -1879,7 +2169,8 @@ fn translate_bin_op(bin_op: BinOp) -> CharonBinOp { fn translate_un_op(un_op: UnOp) -> CharonUnOp { match un_op { UnOp::Not => CharonUnOp::Not, - UnOp::Neg => CharonUnOp::Neg, + // As in Charon's own translation; MIR guards overflow with an explicit `Assert`. + UnOp::Neg => CharonUnOp::Neg(CharonOverflowMode::Wrap), UnOp::PtrMetadata => todo!(), } } @@ -1891,13 +2182,3 @@ fn translate_borrow_kind(kind: &BorrowKind) -> CharonBorrowKind { BorrowKind::Fake(_kind) => todo!(), } } - -fn translate_constant_expr_to_const_generic( - value: CharonRawConstantExpr, -) -> Result { - match value { - CharonRawConstantExpr::Literal(v) => Ok(CharonConstGeneric::Value(v)), - CharonRawConstantExpr::Var(v) => Ok(CharonConstGeneric::Var(v)), - _ => todo!(), - } -} diff --git a/scripts/charon-patch.diff b/scripts/charon-patch.diff deleted file mode 100644 index 83ba6d828463..000000000000 --- a/scripts/charon-patch.diff +++ /dev/null @@ -1,359 +0,0 @@ -diff --git a/charon/Cargo.toml b/charon/Cargo.toml -index 15fbfe00..ba534a33 100644 ---- a/charon/Cargo.toml -+++ b/charon/Cargo.toml -@@ -5,7 +5,7 @@ authors = [ - "Son Ho ", - "Guillaume Boisseau ", - ] --edition = "2021" -+edition = "2024" - license = "Apache-2.0" - - [lib] -@@ -40,7 +40,7 @@ path = "tests/cargo.rs" - harness = false - - [dependencies] --annotate-snippets = { git = "https://github.com/rust-lang/annotate-snippets-rs", version = "0.11.5" } -+annotate-snippets = "0.11.4" - anstream = "0.6.18" - anyhow = "1.0.81" - assert_cmd = "2.0" -diff --git a/charon/src/errors.rs b/charon/src/errors.rs -index 800e8768..4bf3e6a6 100644 ---- a/charon/src/errors.rs -+++ b/charon/src/errors.rs -@@ -13,11 +13,11 @@ use std::collections::{HashMap, HashSet}; - macro_rules! register_error { - ($ctx:expr, crate($krate:expr), $span: expr, $($fmt:tt)*) => {{ - let msg = format!($($fmt)*); -- $ctx.span_err($krate, $span, &msg, $crate::errors::Level::WARNING) -+ $ctx.span_err($krate, $span, &msg, $crate::errors::Level::Warning) - }}; - ($ctx:expr, $span: expr, $($fmt:tt)*) => {{ - let msg = format!($($fmt)*); -- $ctx.span_err($span, &msg, $crate::errors::Level::WARNING) -+ $ctx.span_err($span, &msg, $crate::errors::Level::Warning) - }}; - } - pub use register_error; -@@ -78,37 +78,45 @@ pub struct Error { - impl Error { - pub(crate) fn render(&self, krate: &TranslatedCrate, level: Level) -> String { - use annotate_snippets::*; -- let span = self.span.span; -+ let msg_indent = format!("{level:?}: ").len(); -+ // If the message is multiline, indent the other lines to match the first line. -+ let mut msg = self -+ .msg -+ .replace('\n', &format!("\n{}", str::repeat(" ", msg_indent))); - -- let mut group = Group::new(); -+ let span = self.span.span; - let origin; -- if let Some(file) = krate.files.get(span.file_id) { -- origin = format!("{}", file.name); -+ let message = if let Some(file) = krate.files.get(span.file_id) { - if let Some(source) = &file.contents { -+ origin = format!("{}", file.name); - let snippet = Snippet::source(source) - .origin(&origin) - .fold(true) -- .annotation(AnnotationKind::Primary.span(span.to_byte_range(source))); -- group = group.element(snippet); -+ .annotation(level.span(span.to_byte_range(source))); -+ level.title(&msg).snippet(snippet) - } else { - // Show just the file and line/col. -- let origin = Origin::new(&origin) -- .line(span.beg.line) -- .char_column(span.beg.col + 1) -- .primary(true); -- group = group.element(origin); -+ msg = format!( -+ "{msg}\n --> {}:{}:{}", -+ file.name, -+ span.beg.line, -+ span.beg.col + 1 -+ ); -+ level.title(&msg) - } -- } -- let message = level.header(&self.msg).group(group); -+ } else { -+ level.title(&msg) -+ }; - -- Renderer::styled().render(message).to_string() -+ let out = Renderer::styled().render(message).to_string(); -+ out - } - } - - /// Display an error without a specific location. - pub fn display_unspanned_error(level: Level, msg: &str) { - use annotate_snippets::*; -- let message = level.header(msg); -+ let message = level.title(msg); - let message = Renderer::styled().render(message).to_string(); - anstream::eprintln!("{message}\n"); - } -@@ -232,8 +240,8 @@ impl ErrorCtx { - msg: &str, - level: Level, - ) -> Error { -- let level = if level == Level::WARNING && self.error_on_warnings { -- Level::ERROR -+ let level = if level == Level::Warning && self.error_on_warnings { -+ Level::Error - } else { - level - }; -@@ -311,7 +319,7 @@ impl ErrorCtx { - // Sort by file id to avoid output instability. - by_file.sort_by_key(|(file_id, ..)| *file_id); - -- let level = Level::NOTE; -+ let level = Level::Note; - let snippets = by_file.iter().map(|(_, origin, source, spans)| { - Snippet::source(source) - .origin(&origin) -@@ -319,7 +327,7 @@ impl ErrorCtx { - .annotations( - spans - .iter() -- .map(|span| AnnotationKind::Context.span(span.span.to_byte_range(source))), -+ .map(|span| level.span(span.span.to_byte_range(source))), - ) - }); - -@@ -328,7 +336,7 @@ impl ErrorCtx { - which is (transitively) used at the following location(s):", - krate.into_fmt().format_object(id) - ); -- let message = level.header(&msg).group(Group::new().elements(snippets)); -+ let message = level.title(&msg).snippets(snippets); - let out = Renderer::styled().render(message).to_string(); - anstream::eprintln!("{}", out); - } -diff --git a/charon/src/ids/vector.rs b/charon/src/ids/vector.rs -index 3cb58353..0d5f88f9 100644 ---- a/charon/src/ids/vector.rs -+++ b/charon/src/ids/vector.rs -@@ -261,7 +261,7 @@ where - self.iter_indexed().map(|(id, _)| id) - } - -- pub fn all_indices(&self) -> impl Iterator { -+ pub fn all_indices(&self) -> impl Iterator + use { - self.vector.indices() - } - -diff --git a/charon/src/lib.rs b/charon/src/lib.rs -index 62b33782..8eb0728e 100644 ---- a/charon/src/lib.rs -+++ b/charon/src/lib.rs -@@ -14,7 +14,6 @@ - // For rustdoc: prevents overflows - #![recursion_limit = "256"] - #![feature(assert_matches)] --#![feature(box_patterns)] - #![feature(deref_pure_trait)] - #![feature(if_let_guard)] - #![feature(impl_trait_in_assoc_type)] -diff --git a/charon/src/options.rs b/charon/src/options.rs -index 5f2960d1..99008474 100644 ---- a/charon/src/options.rs -+++ b/charon/src/options.rs -@@ -290,55 +290,55 @@ impl CliOpts { - - if self.input_file.is_some() { - display_unspanned_error( -- Level::WARNING, -+ Level::Warning, - "`--input` is deprecated, use `charon rustc [charon options] -- [rustc options] ` instead", - ) - } - if self.no_cargo { - display_unspanned_error( -- Level::WARNING, -+ Level::Warning, - "`--no-cargo` is deprecated, use `charon rustc [charon options] -- [rustc options] ` instead", - ) - } - if self.read_llbc.is_some() { - display_unspanned_error( -- Level::WARNING, -+ Level::Warning, - "`--read_llbc` is deprecated, use `charon pretty-print ` instead", - ) - } - if self.use_polonius { - display_unspanned_error( -- Level::WARNING, -+ Level::Warning, - "`--polonius` is deprecated, use `--rustc-arg=-Zpolonius` instead", - ) - } - if self.mir_optimized { - display_unspanned_error( -- Level::WARNING, -+ Level::Warning, - "`--mir_optimized` is deprecated, use `--mir optimized` instead", - ) - } - if self.mir_promoted { - display_unspanned_error( -- Level::WARNING, -+ Level::Warning, - "`--mir_promoted` is deprecated, use `--mir promoted` instead", - ) - } - if self.lib { - display_unspanned_error( -- Level::WARNING, -+ Level::Warning, - "`--lib` is deprecated, use `charon cargo -- --lib` instead", - ) - } - if self.bin.is_some() { - display_unspanned_error( -- Level::WARNING, -+ Level::Warning, - "`--bin` is deprecated, use `charon cargo -- --bin ` instead", - ) - } - if self.dest_dir.is_some() { - display_unspanned_error( -- Level::WARNING, -+ Level::Warning, - "`--dest` is deprecated, use `--dest-file` instead", - ) - } -diff --git a/charon/src/pretty/fmt_with_ctx.rs b/charon/src/pretty/fmt_with_ctx.rs -index 6730e159..f01fbd07 100644 ---- a/charon/src/pretty/fmt_with_ctx.rs -+++ b/charon/src/pretty/fmt_with_ctx.rs -@@ -1025,14 +1025,17 @@ impl FmtWithCtx for ullbc::Statement { - place.fmt_with_ctx(ctx), - variant_id - ), -- RawStatement::CopyNonOverlapping(box CopyNonOverlapping { src, dst, count }) => write!( -- &mut out, -- "{}copy_nonoverlapping({}, {}, {})", -- tab, -- src.fmt_with_ctx(ctx), -- dst.fmt_with_ctx(ctx), -- count.fmt_with_ctx(ctx), -- ), -+ RawStatement::CopyNonOverlapping(copy) => { -+ let CopyNonOverlapping { src, dst, count } = &**copy; -+ write!( -+ &mut out, -+ "{}copy_nonoverlapping({}, {}, {})", -+ tab, -+ src.fmt_with_ctx(ctx), -+ dst.fmt_with_ctx(ctx), -+ count.fmt_with_ctx(ctx), -+ ) -+ } - RawStatement::StorageLive(var_id) => { - write!( - &mut out, -@@ -1088,14 +1091,17 @@ impl FmtWithCtx for llbc::Statement { - place.fmt_with_ctx(ctx), - variant_id - ), -- RawStatement::CopyNonOverlapping(box CopyNonOverlapping { src, dst, count }) => write!( -- &mut out, -- "{}copy_nonoverlapping({}, {}, {})", -- tab, -- src.fmt_with_ctx(ctx), -- dst.fmt_with_ctx(ctx), -- count.fmt_with_ctx(ctx), -- ), -+ RawStatement::CopyNonOverlapping(copy) => { -+ let CopyNonOverlapping { src, dst, count } = &**copy; -+ write!( -+ &mut out, -+ "{}copy_nonoverlapping({}, {}, {})", -+ tab, -+ src.fmt_with_ctx(ctx), -+ dst.fmt_with_ctx(ctx), -+ count.fmt_with_ctx(ctx), -+ ) -+ } - RawStatement::StorageLive(var_id) => { - write!( - &mut out, -diff --git a/charon/src/transform/check_generics.rs b/charon/src/transform/check_generics.rs -index cf4dad41..180adf08 100644 ---- a/charon/src/transform/check_generics.rs -+++ b/charon/src/transform/check_generics.rs -@@ -42,7 +42,7 @@ impl CheckGenericsVisitor<'_> { - .join("\n "), - ); - // This is a fatal error: the output llbc is inconsistent and should not be used. -- self.ctx.span_err(self.span, &msg, Level::ERROR); -+ self.ctx.span_err(self.span, &msg, Level::Error); - } - - /// For pretty error printing. This can print values that we encounter because we track binders -diff --git a/charon/src/transform/expand_associated_types.rs b/charon/src/transform/expand_associated_types.rs -index c6140aa0..781c109a 100644 ---- a/charon/src/transform/expand_associated_types.rs -+++ b/charon/src/transform/expand_associated_types.rs -@@ -794,7 +794,7 @@ impl<'a> ComputeItemModifications<'a> { - &'b mut self, - clause: &TraitClause, - clause_to_path: fn(TraitClauseId) -> TraitRefPath, -- ) -> impl Iterator + use<'b> { -+ ) -> impl Iterator + use<'a, 'b> { - let trait_id = clause.trait_.skip_binder.trait_id; - let clause_path = clause_to_path(clause.clause_id); - self.compute_extra_params_for_trait(trait_id) -@@ -806,7 +806,7 @@ impl<'a> ComputeItemModifications<'a> { - fn compute_implied_constraints_for_predicate<'b>( - &'b mut self, - pred: &'b TraitDeclRef, -- ) -> impl Iterator + use<'b> { -+ ) -> impl Iterator + use<'a, 'b> { - let _ = self.compute_extra_params_for_trait(pred.trait_id); - self.trait_modifications[pred.trait_id] - .as_processed() -diff --git a/charon/src/transform/inline_local_panic_functions.rs b/charon/src/transform/inline_local_panic_functions.rs -index a0327689..31cb929d 100644 ---- a/charon/src/transform/inline_local_panic_functions.rs -+++ b/charon/src/transform/inline_local_panic_functions.rs -@@ -50,15 +50,12 @@ impl UllbcPass for Transform { - if let RawTerminator::Call { - call: - Call { -- func: -- FnOperand::Regular(FnPtr { -- func: box FunIdOrTraitMethodRef::Fun(FunId::Regular(fun_id)), -- .. -- }), -+ func: FnOperand::Regular(FnPtr { func, .. }), - .. - }, - .. - } = &block.terminator.content -+ && let FunIdOrTraitMethodRef::Fun(FunId::Regular(fun_id)) = &**func - && panic_fns.contains(fun_id) - { - block.terminator.content = panic_terminator.clone(); -diff --git a/charon/src/transform/simplify_constants.rs b/charon/src/transform/simplify_constants.rs -index 3664f51b..1c535677 100644 ---- a/charon/src/transform/simplify_constants.rs -+++ b/charon/src/transform/simplify_constants.rs -@@ -11,7 +11,7 @@ - //! handle the globals like function calls. - - use itertools::Itertools; --use std::assert_matches::assert_matches; -+use std::assert_matches; - - use crate::transform::TransformCtx; - use crate::ullbc_ast::*; diff --git a/tests/llbc/arith_checked/expected b/tests/llbc/arith_checked/expected index 882578b9dc66..257f3558cab7 100644 --- a/tests/llbc/arith_checked/expected +++ b/tests/llbc/arith_checked/expected @@ -1,38 +1,78 @@ -pub fn test::add(@1: u8, @2: u8) -> u8\ +// Full name: test::sub\ +pub fn sub(a: i16, b: i16) -> i16\ {\ - let @0: u8; // return\ - let a@1: u8; // arg #1\ - let b@2: u8; // arg #2\ - let @3: (u8, bool); // anonymous local\ + let _0: i16; // return\ + let a: i16; // arg #1\ + let b: i16; // arg #2\ + let _3: i16; // anonymous local\ \ - nop\ - nop\ - @0 := copy (a@1) + copy (b@2)\ + storage_live(_0)\ + storage_live(_3)\ + _3 = copy a panic.- copy b\ + _0 = move _3\ + storage_dead(_3)\ + storage_dead(b)\ + storage_dead(a)\ return\ } -pub fn test::mul(@1: u32, @2: u32) -> u32\ +// Full name: test::add\ +pub fn add(a: u8, b: u8) -> u8\ {\ - let @0: u32; // return\ - let a@1: u32; // arg #1\ - let b@2: u32; // arg #2\ - let @3: (u32, bool); // anonymous local\ + let _0: u8; // return\ + let a: u8; // arg #1\ + let b: u8; // arg #2\ + let _3: u8; // anonymous local\ \ - nop\ - nop\ - @0 := copy (a@1) * copy (b@2)\ + storage_live(_0)\ + storage_live(_3)\ + _3 = copy a panic.+ copy b\ + _0 = move _3\ + storage_dead(_3)\ + storage_dead(b)\ + storage_dead(a)\ return\ } -pub fn test::sub(@1: i16, @2: i16) -> i16\ +// Full name: test::mul\ +pub fn mul(a: u32, b: u32) -> u32\ {\ - let @0: i16; // return\ - let a@1: i16; // arg #1\ - let b@2: i16; // arg #2\ - let @3: (i16, bool); // anonymous local\ + let _0: u32; // return\ + let a: u32; // arg #1\ + let b: u32; // arg #2\ + let _3: u32; // anonymous local\ \ - nop\ - nop\ - @0 := copy (a@1) - copy (b@2)\ + storage_live(_0)\ + storage_live(_3)\ + _3 = copy a panic.* copy b\ + _0 = move _3\ + storage_dead(_3)\ + storage_dead(b)\ + storage_dead(a)\ + return\ +} + +// Full name: test::main\ +pub fn main()\ +{\ + let _0: (); // return\ + let _1: u8; // anonymous local\ + let _2: i16; // anonymous local\ + let _3: u32; // anonymous local\ +\ + storage_live(_0)\ + storage_live(_1)\ + storage_live(_2)\ + storage_live(_3)\ + _0 = ()\ + _1 = add(const 1u8, const 2u8)\ + ↳⚡ undefined_behavior\ + storage_dead(_1)\ + _2 = sub(const 5i16, const 2i16)\ + ↳⚡ undefined_behavior\ + storage_dead(_2)\ + _3 = mul(const 3u32, const 4u32)\ + ↳⚡ undefined_behavior\ + storage_dead(_3)\ return\ } diff --git a/tests/llbc/arith_unchecked/expected b/tests/llbc/arith_unchecked/expected index e23d7147cde9..687f9584899d 100644 --- a/tests/llbc/arith_unchecked/expected +++ b/tests/llbc/arith_unchecked/expected @@ -1,29 +1,66 @@ -pub fn test::add(@1: u8, @2: u8) -> u8\ +// Full name: test::sub\ +pub fn sub(a: i16, b: i16) -> i16\ {\ - let @0: u8; // return\ - let a@1: u8; // arg #1\ - let b@2: u8; // arg #2\ + let _0: i16; // return\ + let a: i16; // arg #1\ + let b: i16; // arg #2\ \ - @0 := copy (a@1) + copy (b@2)\ + storage_live(_0)\ + _0 = copy a ub.- copy b\ + storage_dead(b)\ + storage_dead(a)\ return\ } -pub fn test::mul(@1: u32, @2: u32) -> u32\ +// Full name: test::add\ +pub fn add(a: u8, b: u8) -> u8\ {\ - let @0: u32; // return\ - let a@1: u32; // arg #1\ - let b@2: u32; // arg #2\ + let _0: u8; // return\ + let a: u8; // arg #1\ + let b: u8; // arg #2\ \ - @0 := copy (a@1) * copy (b@2)\ + storage_live(_0)\ + _0 = copy a ub.+ copy b\ + storage_dead(b)\ + storage_dead(a)\ return\ } -pub fn test::sub(@1: i16, @2: i16) -> i16\ +// Full name: test::mul\ +pub fn mul(a: u32, b: u32) -> u32\ {\ - let @0: i16; // return\ - let a@1: i16; // arg #1\ - let b@2: i16; // arg #2\ + let _0: u32; // return\ + let a: u32; // arg #1\ + let b: u32; // arg #2\ \ - @0 := copy (a@1) - copy (b@2)\ + storage_live(_0)\ + _0 = copy a ub.* copy b\ + storage_dead(b)\ + storage_dead(a)\ + return\ +} + +// Full name: test::main\ +pub fn main()\ +{\ + let _0: (); // return\ + let _1: u8; // anonymous local\ + let _2: i16; // anonymous local\ + let _3: u32; // anonymous local\ +\ + storage_live(_0)\ + storage_live(_1)\ + storage_live(_2)\ + storage_live(_3)\ + _0 = ()\ + _1 = add(const 1u8, const 2u8)\ + ↳⚡ undefined_behavior\ + storage_dead(_1)\ + _2 = sub(const 5i16, const 2i16)\ + ↳⚡ undefined_behavior\ + storage_dead(_2)\ + _3 = mul(const 3u32, const 4u32)\ + ↳⚡ undefined_behavior\ + storage_dead(_3)\ return\ } diff --git a/tests/llbc/arith_wrapping/expected b/tests/llbc/arith_wrapping/expected index ce7d085abb9b..25fc0c5e395f 100644 --- a/tests/llbc/arith_wrapping/expected +++ b/tests/llbc/arith_wrapping/expected @@ -1,29 +1,66 @@ -pub fn test::add(@1: u8, @2: u8) -> u8\ +// Full name: test::sub\ +pub fn sub(a: i16, b: i16) -> i16\ {\ - let @0: u8; // return\ - let a@1: u8; // arg #1\ - let b@2: u8; // arg #2\ + let _0: i16; // return\ + let a: i16; // arg #1\ + let b: i16; // arg #2\ \ - @0 := copy (a@1) wrapping.+ copy (b@2)\ + storage_live(_0)\ + _0 = copy a wrap.- copy b\ + storage_dead(b)\ + storage_dead(a)\ return\ } -pub fn test::mul(@1: u32, @2: u32) -> u32\ +// Full name: test::add\ +pub fn add(a: u8, b: u8) -> u8\ {\ - let @0: u32; // return\ - let a@1: u32; // arg #1\ - let b@2: u32; // arg #2\ + let _0: u8; // return\ + let a: u8; // arg #1\ + let b: u8; // arg #2\ \ - @0 := copy (a@1) wrapping.* copy (b@2)\ + storage_live(_0)\ + _0 = copy a wrap.+ copy b\ + storage_dead(b)\ + storage_dead(a)\ return\ } -pub fn test::sub(@1: i16, @2: i16) -> i16\ +// Full name: test::mul\ +pub fn mul(a: u32, b: u32) -> u32\ {\ - let @0: i16; // return\ - let a@1: i16; // arg #1\ - let b@2: i16; // arg #2\ + let _0: u32; // return\ + let a: u32; // arg #1\ + let b: u32; // arg #2\ \ - @0 := copy (a@1) wrapping.- copy (b@2)\ + storage_live(_0)\ + _0 = copy a wrap.* copy b\ + storage_dead(b)\ + storage_dead(a)\ + return\ +} + +// Full name: test::main\ +pub fn main()\ +{\ + let _0: (); // return\ + let _1: u8; // anonymous local\ + let _2: i16; // anonymous local\ + let _3: u32; // anonymous local\ +\ + storage_live(_0)\ + storage_live(_1)\ + storage_live(_2)\ + storage_live(_3)\ + _0 = ()\ + _1 = add(const 200u8, const 100u8)\ + ↳⚡ undefined_behavior\ + storage_dead(_1)\ + _2 = sub(const -1i16, const 2i16)\ + ↳⚡ undefined_behavior\ + storage_dead(_2)\ + _3 = mul(const 3u32, const 4u32)\ + ↳⚡ undefined_behavior\ + storage_dead(_3)\ return\ } diff --git a/tests/llbc/arith_wrapping/test.rs b/tests/llbc/arith_wrapping/test.rs index 8ccb8f829516..ca1c9e0ab23e 100644 --- a/tests/llbc/arith_wrapping/test.rs +++ b/tests/llbc/arith_wrapping/test.rs @@ -3,9 +3,9 @@ // kani-flags: -Zlean --print-llbc //! This test checks that Kani's LLBC backend handles wrapping arithmetic. A plain MIR -//! `Add`/`Sub`/`Mul` wraps on overflow, so it must become Charon's `wrapping.` operators rather -//! than `checked.`, which produce a `(result, overflowed)` pair and made the LLBC type-incorrect: -//! `u8 := a checked.+ b`. +//! `Add`/`Sub`/`Mul` wraps on overflow, so it must become Charon's wrapping operators rather than +//! its checked ones, which produce a `(result, overflowed)` pair and once made the LLBC +//! type-incorrect: `u8 := a checked.+ b`. #![feature(core_intrinsics)] #![allow(internal_features)] diff --git a/tests/llbc/basic0/expected b/tests/llbc/basic0/expected index 45d073737f3b..410f26394fbb 100644 --- a/tests/llbc/basic0/expected +++ b/tests/llbc/basic0/expected @@ -1,8 +1,26 @@ -fn test::is_zero(@1: i32) -> bool\ +// Full name: test::is_zero\ +pub fn is_zero(i: i32) -> bool\ {\ - let @0: bool; // return\ - let i@1: i32; // arg #1\ + let _0: bool; // return\ + let i: i32; // arg #1\ +\ + storage_live(_0)\ + _0 = copy i == const 0i32\ + storage_dead(i)\ + return\ +} - @0 := copy (i@1) == const (0 : i32)\ +// Full name: test::main\ +pub fn main()\ +{\ + let _0: (); // return\ + let _1: bool; // anonymous local\ +\ + storage_live(_0)\ + storage_live(_1)\ + _0 = ()\ + _1 = is_zero(const 0i32)\ + ↳⚡ undefined_behavior\ + storage_dead(_1)\ return\ } diff --git a/tests/llbc/basic1/expected b/tests/llbc/basic1/expected index 233940af9752..447615627524 100644 --- a/tests/llbc/basic1/expected +++ b/tests/llbc/basic1/expected @@ -1,15 +1,38 @@ -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 +// Full name: test::select\ +pub fn select(s: bool, x: i32, y: i32) -> i32\ +{\ + let _0: i32; // return\ + let s: bool; // arg #1\ + let x: i32; // arg #2\ + let y: i32; // arg #3\ +\ + storage_live(_0)\ + if copy s {\ + } else {\ + _0 = copy y\ + storage_dead(y)\ + storage_dead(x)\ + storage_dead(s)\ + return\ + }\ + _0 = copy x\ + storage_dead(y)\ + storage_dead(x)\ + storage_dead(s)\ + return\ +} - if copy (s@1) { - @0 := copy (x@2) - } - else { - @0 := copy (y@3) - } - return +// Full name: test::main\ +pub fn main()\ +{\ + let _0: (); // return\ + let _1: i32; // anonymous local\ +\ + storage_live(_0)\ + storage_live(_1)\ + _0 = ()\ + _1 = select(const true, const 3i32, const 7i32)\ + ↳⚡ undefined_behavior\ + storage_dead(_1)\ + return\ } diff --git a/tests/llbc/bool_char/expected b/tests/llbc/bool_char/expected index 5104e759f5e6..6b2c2f4c1010 100644 --- a/tests/llbc/bool_char/expected +++ b/tests/llbc/bool_char/expected @@ -1,16 +1,41 @@ -pub fn test::always() -> bool\ +// Full name: test::is_a\ +pub fn is_a(c: char) -> bool\ {\ - let @0: bool; // return\ + let _0: bool; // return\ + let c: char; // arg #1\ \ - @0 := const (true)\ + storage_live(_0)\ + _0 = copy c == const 'a'\ + storage_dead(c)\ return\ } -pub fn test::is_a(@1: char) -> bool\ +// Full name: test::always\ +pub fn always() -> bool\ {\ - let @0: bool; // return\ - let c@1: char; // arg #1\ + let _0: bool; // return\ \ - @0 := copy (c@1) == const (a)\ + storage_live(_0)\ + _0 = const true\ + return\ +} + +// Full name: test::main\ +pub fn main()\ +{\ + let _0: (); // return\ + let _1: bool; // anonymous local\ + let _2: bool; // anonymous local\ +\ + storage_live(_0)\ + storage_live(_1)\ + storage_live(_2)\ + _0 = ()\ + _1 = is_a(const 'b')\ + ↳⚡ undefined_behavior\ + storage_dead(_1)\ + _2 = always()\ + ↳⚡ undefined_behavior\ + storage_dead(_2)\ return\ } diff --git a/tests/llbc/div_rem/expected b/tests/llbc/div_rem/expected index 36d8b3c6577c..730501b98e12 100644 --- a/tests/llbc/div_rem/expected +++ b/tests/llbc/div_rem/expected @@ -1,32 +1,47 @@ -pub fn test::div(@1: u32, @2: u32) -> u32\ +// Full name: test::rem\ +pub fn rem(a: i32, b: i32) -> i32\ {\ - let @0: u32; // return\ - let a@1: u32; // arg #1\ - let b@2: u32; // arg #2\ - let @3: bool; // anonymous local\ + let _0: i32; // return\ + let a: i32; // arg #1\ + let b: i32; // arg #2\ \ - nop\ - nop\ - @0 := copy (a@1) / copy (b@2)\ + storage_live(_0)\ + _0 = copy a panic.% copy b\ + storage_dead(b)\ + storage_dead(a)\ return\ } -pub fn test::rem(@1: i32, @2: i32) -> i32\ +// Full name: test::div\ +pub fn div(a: u32, b: u32) -> u32\ {\ - let @0: i32; // return\ - let a@1: i32; // arg #1\ - let b@2: i32; // arg #2\ - let @3: bool; // anonymous local\ - let @4: bool; // anonymous local\ - let @5: bool; // anonymous local\ - let @6: bool; // anonymous local\ + let _0: u32; // return\ + let a: u32; // arg #1\ + let b: u32; // arg #2\ \ - nop\ - nop\ - nop\ - nop\ - nop\ - nop\ - @0 := copy (a@1) % copy (b@2)\ + storage_live(_0)\ + _0 = copy a panic./ copy b\ + storage_dead(b)\ + storage_dead(a)\ + return\ +} + +// Full name: test::main\ +pub fn main()\ +{\ + let _0: (); // return\ + let _1: u32; // anonymous local\ + let _2: i32; // anonymous local\ +\ + storage_live(_0)\ + storage_live(_1)\ + storage_live(_2)\ + _0 = ()\ + _1 = div(const 7u32, const 2u32)\ + ↳⚡ undefined_behavior\ + storage_dead(_1)\ + _2 = rem(const 7i32, const 2i32)\ + ↳⚡ undefined_behavior\ + storage_dead(_2)\ return\ } diff --git a/tests/llbc/diverging_call/expected b/tests/llbc/diverging_call/expected index b71705a6a14f..cee6873f0989 100644 --- a/tests/llbc/diverging_call/expected +++ b/tests/llbc/diverging_call/expected @@ -1,4 +1,23 @@ -pub fn test::diverge() -> !\ +// Full name: test::diverge\ +pub fn diverge() -> !\ {\ - let @0: !; // return -pub fn test::main() + let _0: !; // return\ +\ + storage_live(_0)\ + loop {\ + continue 0\ + }\ +} + +// Full name: test::main\ +pub fn main()\ +{\ + let _0: (); // return\ + let _1: !; // anonymous local\ +\ + storage_live(_0)\ + storage_live(_1)\ + _0 = ()\ + _1 = diverge()\ + ↳⚡ undefined_behavior\ +} diff --git a/tests/llbc/enum/expected b/tests/llbc/enum/expected index 62d41c0f4f34..fb7caf53aece 100644 --- a/tests/llbc/enum/expected +++ b/tests/llbc/enum/expected @@ -1,26 +1,49 @@ -pub enum test::MyEnum =\ -| A(0: i32)\ -| B() +// Full name: test::MyEnum\ +pub enum MyEnum {\ + A { _0: i32 },\ + B,\ +} -pub fn test::enum_match(@1: @Adt0) -> i32\ +// Full name: test::enum_match\ +pub fn enum_match(e: MyEnum) -> i32\ {\ - let @0: i32; // return\ - let e@1: @Adt0; // arg #1\ - let @2: isize; // anonymous local\ - let i@3: i32; // local\ + let _0: i32; // return\ + let e: MyEnum; // arg #1\ + let i: i32; // local\ \ - nop\ - match e@1 {\ - test::MyEnum::A => {\ - nop\ + storage_live(_0)\ + storage_live(i)\ + match e {\ + MyEnum::A => {\ },\ - test::MyEnum::B => {\ - @0 := const (0 : i32)\ + MyEnum::B => {\ + _0 = const 0i32\ + storage_dead(e)\ return\ },\ }\ - i@3 := copy ((e@1 as variant @0).0)\ - @0 := copy (i@3)\ - storage_dead(i@3)\ + i = copy (e as variant MyEnum::A)._0\ + _0 = copy i\ + storage_dead(i)\ + storage_dead(e)\ + return\ +} + +// Full name: test::main\ +pub fn main()\ +{\ + let _0: (); // return\ + let e: MyEnum; // local\ + let i: i32; // local\ +\ + storage_live(_0)\ + storage_live(e)\ + storage_live(i)\ + _0 = ()\ + e = MyEnum::A { _0: const 1i32 }\ + i = enum_match(copy e)\ + ↳⚡ undefined_behavior\ + storage_dead(i)\ + storage_dead(e)\ return\ } diff --git a/tests/llbc/generic/expected b/tests/llbc/generic/expected index 75e0d7fa3baa..a174247aed13 100644 --- a/tests/llbc/generic/expected +++ b/tests/llbc/generic/expected @@ -1,44 +1,85 @@ -pub enum core::option::Option =\ -| None()\ -| Some(0: T) +// Full name: core::option::Option\ +pub enum Option {\ + None,\ + Some { _0: T },\ +} -pub fn test::add_opt(@1: @Adt0, @2: @Adt0) -> @Adt0\ +// Full name: test::add_opt\ +pub fn add_opt(x: Option, y: Option) -> Option\ {\ - let @0: @Adt0; // return\ - let x@1: @Adt0; // arg #1\ - let y@2: @Adt0; // arg #2\ - let @3: isize; // anonymous local\ - let u@4: i32; // local\ - let @5: isize; // anonymous local\ - let v@6: i32; // local\ - let @7: i32; // anonymous local\ - let @8: (i32, bool); // anonymous local\ + let _0: Option; // return\ + let x: Option; // arg #1\ + let y: Option; // arg #2\ + let u: i32; // local\ + let v: i32; // local\ + let _5: i32; // anonymous local\ + let _6: i32; // anonymous local\ \ - nop\ - match x@1 {\ - core::option::Option::Some => {\ - u@4 := copy ((x@1 as variant @1).0)\ - nop\ - match y@2 {\ - core::option::Option::Some => {\ - v@6 := copy ((y@2 as variant @1).0)\ - nop\ - nop\ - @7 := copy (u@4) + copy (v@6)\ - @0 := core::option::Option::Some { 0: move (@7) }\ - storage_dead(@7)\ + storage_live(_0)\ + storage_live(u)\ + storage_live(v)\ + storage_live(_5)\ + storage_live(_6)\ + match x {\ + Option::Some => {\ + u = copy (x as variant Option::Some)._0\ + match y {\ + Option::Some => {\ + v = copy (y as variant Option::Some)._0\ + _6 = copy u panic.+ copy v\ + _5 = move _6\ + _0 = Option::Some { _0: move _5 }\ + storage_dead(_5)\ + storage_dead(_6)\ + storage_dead(v)\ + storage_dead(u)\ + storage_dead(y)\ + storage_dead(x)\ return\ },\ - core::option::Option::None => {\ - @0 := core::option::Option::None { }\ + Option::None => {\ + _0 = Option::None { }\ + storage_dead(_6)\ + storage_dead(v)\ + storage_dead(u)\ + storage_dead(y)\ + storage_dead(x)\ return\ },\ }\ },\ - core::option::Option::None => {\ - @0 := core::option::Option::None { }\ + Option::None => {\ + _0 = Option::None { }\ + storage_dead(_6)\ + storage_dead(v)\ + storage_dead(u)\ + storage_dead(y)\ + storage_dead(x)\ return\ },\ }\ undefined_behavior\ } + +// Full name: test::main\ +pub fn main()\ +{\ + let _0: (); // return\ + let e: Option; // local\ + let _2: Option; // anonymous local\ + let _3: Option; // anonymous local\ +\ + storage_live(_0)\ + storage_live(e)\ + storage_live(_2)\ + storage_live(_3)\ + _0 = ()\ + _2 = Option::Some { _0: const 1i32 }\ + _3 = Option::Some { _0: const 2i32 }\ + e = add_opt(move _2, move _3)\ + ↳⚡ undefined_behavior\ + storage_dead(_3)\ + storage_dead(_2)\ + storage_dead(e)\ + return\ +} diff --git a/tests/llbc/inherent_core/expected b/tests/llbc/inherent_core/expected index abe032d9151b..84fed9697c5f 100644 --- a/tests/llbc/inherent_core/expected +++ b/tests/llbc/inherent_core/expected @@ -1,11 +1,33 @@ -pub fn core::num::wrapping_addu8(@1: u8, @2: u8) -> u8 +// Full name: core::num::wrapping_addu8\ +pub fn wrapping_addu8(_1: u8, _2: u8) -> u8\ += -pub fn test::wrap(@1: u8, @2: u8) -> u8\ +// Full name: test::wrap\ +pub fn wrap(a: u8, b: u8) -> u8\ {\ - let @0: u8; // return\ - let a@1: u8; // arg #1\ - let b@2: u8; // arg #2\ + let _0: u8; // return\ + let a: u8; // arg #1\ + let b: u8; // arg #2\ \ - @0 := @Fun\ + storage_live(_0)\ + _0 = wrapping_addu8(copy a, copy b)\ + ↳⚡ undefined_behavior\ + storage_dead(b)\ + storage_dead(a)\ + return\ +} + +// Full name: test::main\ +pub fn main()\ +{\ + let _0: (); // return\ + let _1: u8; // anonymous local\ +\ + storage_live(_0)\ + storage_live(_1)\ + _0 = ()\ + _1 = wrap(const 200u8, const 100u8)\ + ↳⚡ undefined_behavior\ + storage_dead(_1)\ return\ } diff --git a/tests/llbc/inherent_local/expected b/tests/llbc/inherent_local/expected index a1c972b2ac7d..57c97bf10cf5 100644 --- a/tests/llbc/inherent_local/expected +++ b/tests/llbc/inherent_local/expected @@ -1,8 +1,39 @@ -pub fn test::getCounter<'_0>(@1: &'_0 (@Adt0)) -> u32\ +// Full name: test::Counter\ +pub struct Counter {\ + n: u32,\ +} + +// Full name: test::getCounter\ +pub fn getCounter<'_0>(self: &'_0 Counter) -> u32\ +{\ + let _0: u32; // return\ + let self: &'_ Counter; // arg #1\ +\ + storage_live(_0)\ + _0 = copy (*self).n\ + storage_dead(self)\ + return\ +} + +// Full name: test::main\ +pub fn main()\ {\ - let @0: u32; // return\ - let self@1: &'_ (@Adt0); // arg #1\ + let _0: (); // return\ + let c: Counter; // local\ + let _2: u32; // anonymous local\ + let _3: &'_ Counter; // anonymous local\ \ - @0 := copy ((*(self@1)).n)\ + storage_live(_0)\ + storage_live(c)\ + storage_live(_2)\ + storage_live(_3)\ + _0 = ()\ + c = Counter { n: const 1u32 }\ + _3 = &c\ + _2 = getCounter<'_>(move _3)\ + ↳⚡ undefined_behavior\ + storage_dead(_3)\ + storage_dead(_2)\ + storage_dead(c)\ return\ } diff --git a/tests/llbc/int_literals/expected b/tests/llbc/int_literals/expected index 14c624b30b0e..076fc30afbf0 100644 --- a/tests/llbc/int_literals/expected +++ b/tests/llbc/int_literals/expected @@ -1,15 +1,39 @@ -pub fn test::signed() -> (i8, i16, i32, i64, i128, isize)\ +// Full name: test::unsigned\ +pub fn unsigned() -> (u8, u16, u32, u64, u128, usize)\ {\ - let @0: (i8, i16, i32, i64, i128, isize); // return\ + let _0: (u8, u16, u32, u64, u128, usize); // return\ \ - @0 := (const (-1 : i8), const (-2 : i16), const (-3 : i32), const (-4 : i64), const (-5 : i128), const (-6 : isize))\ + storage_live(_0)\ + _0 = (const 1u8, const 2u16, const 3u32, const 4u64, const 5u128, const 6usize)\ return\ } -pub fn test::unsigned() -> (u8, u16, u32, u64, u128, usize)\ +// Full name: test::signed\ +pub fn signed() -> (i8, i16, i32, i64, i128, isize)\ {\ - let @0: (u8, u16, u32, u64, u128, usize); // return\ + let _0: (i8, i16, i32, i64, i128, isize); // return\ \ - @0 := (const (1 : u8), const (2 : u16), const (3 : u32), const (4 : u64), const (5 : u128), const (6 : usize))\ + storage_live(_0)\ + _0 = (const -1i8, const -2i16, const -3i32, const -4i64, const -5i128, const -6isize)\ + return\ +} + +// Full name: test::main\ +pub fn main()\ +{\ + let _0: (); // return\ + let _1: (i8, i16, i32, i64, i128, isize); // anonymous local\ + let _2: (u8, u16, u32, u64, u128, usize); // anonymous local\ +\ + storage_live(_0)\ + storage_live(_1)\ + storage_live(_2)\ + _0 = ()\ + _1 = signed()\ + ↳⚡ undefined_behavior\ + storage_dead(_1)\ + _2 = unsigned()\ + ↳⚡ undefined_behavior\ + storage_dead(_2)\ return\ } diff --git a/tests/llbc/option/expected b/tests/llbc/option/expected index 7dea7051bd70..92bb7720ec3c 100644 --- a/tests/llbc/option/expected +++ b/tests/llbc/option/expected @@ -1,38 +1,66 @@ -pub enum core::option::Option =\ -| None()\ -| Some(0: T) +// Full name: core::option::Option\ +pub enum Option {\ + None,\ + Some { _0: T },\ +} -pub fn core::ptr::drop_glue<'_0, T>(@1: &'_0 mut (T)) +// Full name: core::ptr::drop_glue\ +pub fn drop_glue<'_0, T>(_1: &'_0 mut T)\ +where\ + TypeOutlives0: T: '_0,\ += -pub fn test::both_none(@1: @Adt0, @2: @Adt0) -> bool\ +// Full name: test::both_none\ +pub fn both_none(a: Option, b: Option) -> bool\ {\ - let @0: bool; // return\ - let a@1: @Adt0; // arg #1\ - let b@2: @Adt0; // arg #2\ - let @3: isize; // anonymous local\ - let @4: isize; // anonymous local\ + let _0: bool; // return\ + let a: Option; // arg #1\ + let b: Option; // arg #2\ \ - nop\ - match a@1 {\ - core::option::Option::None => {\ - nop\ - match b@2 {\ - core::option::Option::None => {\ - @0 := const (true)\ - nop\ + storage_live(_0)\ + match a {\ + Option::None => {\ + match b {\ + Option::None => {\ + _0 = const true\ },\ - core::option::Option::Some => {\ - @0 := const (false)\ - nop\ + Option::Some => {\ + _0 = const false\ },\ }\ },\ - core::option::Option::Some => {\ - @0 := const (false)\ - nop\ + Option::Some => {\ + _0 = const false\ },\ }\ - drop b@2\ - drop a@1\ + drop[drop_glue<'_, Option>] b\ + ↳⚡ undefined_behavior\ + drop[drop_glue<'_, Option>] a\ + ↳⚡ undefined_behavior\ + storage_dead(b)\ + storage_dead(a)\ + return\ +} + +// Full name: test::main\ +pub fn main()\ +{\ + let _0: (); // return\ + let a: Option; // local\ + let b: Option; // local\ + let i: bool; // local\ +\ + storage_live(_0)\ + storage_live(a)\ + storage_live(b)\ + storage_live(i)\ + _0 = ()\ + a = Option::Some { _0: const 1u32 }\ + b = Option::Some { _0: const 2i32 }\ + i = both_none(copy a, copy b)\ + ↳⚡ undefined_behavior\ + storage_dead(i)\ + storage_dead(b)\ + storage_dead(a)\ return\ } diff --git a/tests/llbc/projection/expected b/tests/llbc/projection/expected index 9d2836cdde33..1a287301e7c0 100644 --- a/tests/llbc/projection/expected +++ b/tests/llbc/projection/expected @@ -1,78 +1,141 @@ -pub enum test::MyEnum =\ -| A(0: @Adt\ -| B(0: (i32, i32)) +// Full name: test::MyStruct\ +pub struct MyStruct {\ + a: i32,\ + b: i32,\ +} -pub enum test::MyEnum0 =\ -| A(0: @Adt\ -| B() +// Full name: test::MyEnum0\ +pub enum MyEnum0 {\ + A { _0: MyStruct, _1: i32 },\ + B,\ +} -pub fn test::enum_match(@1: @Adt\ +// Full name: test::MyEnum\ +pub enum MyEnum {\ + A { _0: MyStruct, _1: MyEnum0 },\ + B { _0: (i32, i32) },\ +} + +// Full name: test::enum_match\ +pub fn enum_match(e: MyEnum) -> i32\ {\ - let @0: i32; // return\ - let e@1: @Adt\ - let @2: isize; // anonymous local\ - let s@3: @Adt\ - let e0@4: @Adt\ - let @5: isize; // anonymous local\ - let s1@6: @Adt\ - let b@7: i32; // local\ - let @8: i32; // anonymous local\ - let @9: (i32, bool); // anonymous local\ - let @10: i32; // anonymous local\ - let @11: i32; // anonymous local\ - let @12: (i32, bool); // anonymous local\ - let a@13: i32; // local\ - let b@14: i32; // local\ - let @15: (i32, bool); // anonymous local\ + let _0: i32; // return\ + let e: MyEnum; // arg #1\ + let s: MyStruct; // local\ + let e0: MyEnum0; // local\ + let s1: MyStruct; // local\ + let b_5: i32; // local\ + let _6: i32; // anonymous local\ + let _7: i32; // anonymous local\ + let _8: i32; // anonymous local\ + let _9: i32; // anonymous local\ + let _10: i32; // anonymous local\ + let a: i32; // local\ + let b_12: i32; // local\ + let _13: i32; // anonymous local\ \ - nop\ - match e@1 {\ - test::MyEnum::A => {\ - s@3 := move ((e@1 as variant @0).0)\ - e0@4 := move ((e@1 as variant @0).1)\ - nop\ - match e0@4 {\ - test::MyEnum0::A => {\ - s1@6 := move ((e0@4 as variant @0).0)\ - b@7 := copy ((e0@4 as variant @0).1)\ - @8 := copy ((s1@6).a)\ - nop\ - nop\ - @0 := copy (@8) + copy (b@7)\ - storage_dead(@8)\ - storage_dead(s1@6)\ - storage_dead(e0@4)\ - storage_dead(s@3)\ + storage_live(_0)\ + storage_live(s)\ + storage_live(e0)\ + storage_live(s1)\ + storage_live(b_5)\ + storage_live(_6)\ + storage_live(_7)\ + storage_live(_8)\ + storage_live(_9)\ + storage_live(_10)\ + storage_live(a)\ + storage_live(b_12)\ + storage_live(_13)\ + match e {\ + MyEnum::A => {\ + s = move (e as variant MyEnum::A)._0\ + e0 = move (e as variant MyEnum::A)._1\ + match e0 {\ + MyEnum0::A => {\ + s1 = move (e0 as variant MyEnum0::A)._0\ + b_5 = copy (e0 as variant MyEnum0::A)._1\ + _6 = copy s1.a\ + _7 = copy _6 panic.+ copy b_5\ + _0 = move _7\ + storage_dead(_6)\ + storage_dead(s1)\ + storage_dead(e0)\ + storage_dead(s)\ + storage_dead(_13)\ + storage_dead(b_12)\ + storage_dead(a)\ + storage_dead(_10)\ + storage_dead(_7)\ + storage_dead(b_5)\ + storage_dead(e)\ return\ },\ - test::MyEnum0::B => {\ - @10 := copy ((s@3).a)\ - @11 := copy ((s@3).b)\ - nop\ - nop\ - @0 := copy (@10) + copy (@11)\ - storage_dead(@11)\ - storage_dead(@10)\ - storage_dead(e0@4)\ - storage_dead(s@3)\ + MyEnum0::B => {\ + _8 = copy s.a\ + _9 = copy s.b\ + _10 = copy _8 panic.+ copy _9\ + _0 = move _10\ + storage_dead(_9)\ + storage_dead(_8)\ + storage_dead(e0)\ + storage_dead(s)\ + storage_dead(_13)\ + storage_dead(b_12)\ + storage_dead(a)\ + storage_dead(_10)\ + storage_dead(_7)\ + storage_dead(b_5)\ + storage_dead(e)\ return\ },\ }\ },\ - test::MyEnum::B => {\ - a@13 := copy (((e@1 as variant @1).0).0)\ - b@14 := copy (((e@1 as variant @1).0).1)\ - nop\ - nop\ - @0 := copy (a@13) + copy (b@14)\ + MyEnum::B => {\ + a = copy (e as variant MyEnum::B)._0.0\ + b_12 = copy (e as variant MyEnum::B)._0.1\ + _13 = copy a panic.+ copy b_12\ + _0 = move _13\ + storage_dead(_13)\ + storage_dead(b_12)\ + storage_dead(a)\ + storage_dead(_10)\ + storage_dead(_7)\ + storage_dead(b_5)\ + storage_dead(e)\ return\ },\ }\ undefined_behavior\ } -pub struct test::MyStruct =\ +// Full name: test::main\ +pub fn main()\ {\ - a: i32,\ - b: i32,\ + let _0: (); // return\ + let s: MyStruct; // local\ + let s0: MyStruct; // local\ + let e: MyEnum; // local\ + let _4: MyEnum0; // anonymous local\ + let i: i32; // local\ +\ + storage_live(_0)\ + storage_live(s)\ + storage_live(s0)\ + storage_live(e)\ + storage_live(_4)\ + storage_live(i)\ + _0 = ()\ + s = MyStruct { a: const 1i32, b: const 2i32 }\ + s0 = MyStruct { a: const 1i32, b: const 2i32 }\ + _4 = MyEnum0::A { _0: copy s0, _1: const 1i32 }\ + e = MyEnum::A { _0: copy s, _1: move _4 }\ + storage_dead(_4)\ + i = enum_match(copy e)\ + ↳⚡ undefined_behavior\ + storage_dead(i)\ + storage_dead(e)\ + storage_dead(s0)\ + storage_dead(s)\ + return\ } diff --git a/tests/llbc/regions/expected b/tests/llbc/regions/expected new file mode 100644 index 000000000000..320fade27327 --- /dev/null +++ b/tests/llbc/regions/expected @@ -0,0 +1,20 @@ +// Full name: test::deref2\ +pub fn deref2<'_0, '_1>(x: &'_0 &'_1 u32) -> u32 + +// Full name: test::early\ +pub fn early<'a, T>(x: &'a T) -> &'a T + +// Full name: test::getHolder<'a>\ +pub fn getHolder<'a><'a, '_1>(self: &'_1 Holder<'a>) -> u32 + +// Full name: test::get\ +pub fn get<'_0>(x: Option<&'_0 u32>) -> u32 + +// Full name: test::pick\ +pub fn pick<'a>(x: &'a u32, y: &'a u32, c: bool) -> &'a u32 + +// Full name: test::read\ +pub fn read<'_0>(h: Holder<'_0>) -> u32 + +// Full name: test::take\ +pub fn take<'_0>(g: Option(&'_0_1 u32) -> &'_0_1 u32>, x: &'_0 u8) -> u8 diff --git a/tests/llbc/regions/test.rs b/tests/llbc/regions/test.rs new file mode 100644 index 000000000000..42a018394095 --- /dev/null +++ b/tests/llbc/regions/test.rs @@ -0,0 +1,70 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zlean --print-llbc + +//! This test checks that Kani's LLBC backend declares the regions of function signatures the way +//! Charon's type check expects: every late-bound region, wherever it occurs in the signature and +//! only once; late-bound regions numbered after early-bound ones; generic parameters numbered per +//! kind; and the regions bound by function-pointer types. Each of these used to make Charon +//! reject the translation. + +struct Holder<'a> { + r: &'a u32, +} + +impl<'a> Holder<'a> { + // `'a` is early-bound (from the impl), the region of `&self` late-bound. + fn get(&self) -> u32 { + *self.r + } +} + +// A late-bound region nested in an ADT. +fn get(x: Option<&u32>) -> u32 { + match x { + Some(v) => *v, + None => 0, + } +} + +// Two late-bound regions, one nested in the other. +fn deref2(x: &&u32) -> u32 { + **x +} + +// A late-bound region as an ADT's region argument. +fn read(h: Holder<'_>) -> u32 { + *h.r +} + +// One late-bound region used three times. +fn pick<'a>(x: &'a u32, y: &'a u32, c: bool) -> &'a u32 { + if c { x } else { y } +} + +// An early-bound region (because of `T: 'a`) before a type parameter. +fn early<'a, T: 'a>(x: &'a T) -> &'a T { + x +} + +// A function-pointer type binding its own region. +fn take(g: Option &u32>, x: &u8) -> u8 { + let _ = g; + *x +} + +#[kani::proof] +fn main() { + let a = 1u32; + let b = 2u32; + let r = &a; + let h = Holder { r: &a }; + let _ = h.get(); + let _ = get(Some(&a)); + let _ = deref2(&r); + let _ = read(Holder { r: &b }); + let _ = *pick(&a, &b, true); + let _ = *early(&a); + let c = 3u8; + let _ = take(None, &c); +} diff --git a/tests/llbc/shifts/expected b/tests/llbc/shifts/expected index 6701d652fab3..272fa3a31164 100644 --- a/tests/llbc/shifts/expected +++ b/tests/llbc/shifts/expected @@ -1,25 +1,47 @@ -pub fn test::shl(@1: u32, @2: u32) -> u32\ +// Full name: test::shl\ +pub fn shl(a: u32, b: u32) -> u32\ {\ - let @0: u32; // return\ - let a@1: u32; // arg #1\ - let b@2: u32; // arg #2\ - let @3: bool; // anonymous local\ + let _0: u32; // return\ + let a: u32; // arg #1\ + let b: u32; // arg #2\ \ - nop\ - nop\ - @0 := copy (a@1) << copy (b@2)\ + storage_live(_0)\ + _0 = copy a panic.<< copy b\ + storage_dead(b)\ + storage_dead(a)\ return\ } -pub fn test::shr(@1: i64, @2: u32) -> i64\ +// Full name: test::shr\ +pub fn shr(a: i64, b: u32) -> i64\ {\ - let @0: i64; // return\ - let a@1: i64; // arg #1\ - let b@2: u32; // arg #2\ - let @3: bool; // anonymous local\ + let _0: i64; // return\ + let a: i64; // arg #1\ + let b: u32; // arg #2\ \ - nop\ - nop\ - @0 := copy (a@1) >> copy (b@2)\ + storage_live(_0)\ + _0 = copy a panic.>> copy b\ + storage_dead(b)\ + storage_dead(a)\ + return\ +} + +// Full name: test::main\ +pub fn main()\ +{\ + let _0: (); // return\ + let _1: u32; // anonymous local\ + let _2: i64; // anonymous local\ +\ + storage_live(_0)\ + storage_live(_1)\ + storage_live(_2)\ + _0 = ()\ + _1 = shl(const 1u32, const 3u32)\ + ↳⚡ undefined_behavior\ + storage_dead(_1)\ + _2 = shr(const -8i64, const 1u32)\ + ↳⚡ undefined_behavior\ + storage_dead(_2)\ return\ } diff --git a/tests/llbc/struct/expected b/tests/llbc/struct/expected index f5e66a86f257..40d23123c508 100644 --- a/tests/llbc/struct/expected +++ b/tests/llbc/struct/expected @@ -1,14 +1,36 @@ -pub fn test::struct_project(@1: @Adt0) -> i32\ +// Full name: test::MyStruct\ +pub struct MyStruct {\ + a: i32,\ + b: bool,\ +} + +// Full name: test::struct_project\ +pub fn struct_project(s: MyStruct) -> i32\ {\ - let @0: i32; // return\ - let s@1: @Adt0; // arg #1\ + let _0: i32; // return\ + let s: MyStruct; // arg #1\ \ - @0 := copy ((s@1).a)\ + storage_live(_0)\ + _0 = copy s.a\ + storage_dead(s)\ return\ } -pub struct test::MyStruct =\ +// Full name: test::main\ +pub fn main()\ {\ - a: i32,\ - b: bool,\ + let _0: (); // return\ + let s: MyStruct; // local\ + let a: i32; // local\ +\ + storage_live(_0)\ + storage_live(s)\ + storage_live(a)\ + _0 = ()\ + s = MyStruct { a: const 1i32, b: const true }\ + a = struct_project(copy s)\ + ↳⚡ undefined_behavior\ + storage_dead(a)\ + storage_dead(s)\ + return\ } diff --git a/tests/llbc/switch_int/expected b/tests/llbc/switch_int/expected index 3f2b4506548c..27591712f8e3 100644 --- a/tests/llbc/switch_int/expected +++ b/tests/llbc/switch_int/expected @@ -1,21 +1,40 @@ -pub fn test::classify(@1: u8) -> u8\ +// Full name: test::classify\ +pub fn classify(x: u8) -> u8\ {\ - let @0: u8; // return\ - let x@1: u8; // arg #1\ + let _0: u8; // return\ + let x: u8; // arg #1\ \ - switch copy (x@1) {\ - 0 : u8 => {\ - nop\ + storage_live(_0)\ + switch copy x {\ + 0u8 => {\ },\ - 1 : u8 | 2 : u8 => {\ - @0 := const (20 : u8)\ + 1u8 | 2u8 => {\ + _0 = const 20u8\ + storage_dead(x)\ return\ },\ _ => {\ - @0 := const (30 : u8)\ + _0 = const 30u8\ + storage_dead(x)\ return\ },\ }\ - @0 := const (10 : u8)\ + _0 = const 10u8\ + storage_dead(x)\ + return\ +} + +// Full name: test::main\ +pub fn main()\ +{\ + let _0: (); // return\ + let _1: u8; // anonymous local\ +\ + storage_live(_0)\ + storage_live(_1)\ + _0 = ()\ + _1 = classify(const 1u8)\ + ↳⚡ undefined_behavior\ + storage_dead(_1)\ return\ } diff --git a/tests/llbc/traitimpl/expected b/tests/llbc/traitimpl/expected index 498618bb1739..4ebedc78c096 100644 --- a/tests/llbc/traitimpl/expected +++ b/tests/llbc/traitimpl/expected @@ -1,27 +1,69 @@ -pub fn test::get_valA<'_0>(@1: &'_0 (@Adt\ -{\ - let @0: i32; // return\ - let self@1: &'_ (@Adt\ -\ - @0 := copy ((*(self@1)).val)\ - return\ +// Full name: test::B\ +pub struct B {\ + index: i32,\ } -pub fn test::get_valB<'_0>(@1: &'_0 (@Adt\ +// Full name: test::get_valB\ +pub fn get_valB<'_0>(self: &'_0 B) -> i32\ {\ - let @0: i32; // return\ - let self@1: &'_ (@Adt\ + let _0: i32; // return\ + let self: &'_ B; // arg #1\ \ - @0 := copy ((*(self@1)).index)\ + storage_live(_0)\ + _0 = copy (*self).index\ + storage_dead(self)\ return\ } -pub struct test::A =\ -{\ +// Full name: test::A\ +pub struct A {\ val: i32,\ } -pub struct test::B =\ +// Full name: test::get_valA\ +pub fn get_valA<'_0>(self: &'_0 A) -> i32\ {\ - index: i32,\ + let _0: i32; // return\ + let self: &'_ A; // arg #1\ +\ + storage_live(_0)\ + _0 = copy (*self).val\ + storage_dead(self)\ + return\ +} + +// Full name: test::main\ +pub fn main()\ +{\ + let _0: (); // return\ + let e: A; // local\ + let k: B; // local\ + let i: i32; // local\ + let _4: &'_ A; // anonymous local\ + let j: i32; // local\ + let _6: &'_ B; // anonymous local\ +\ + storage_live(_0)\ + storage_live(e)\ + storage_live(k)\ + storage_live(i)\ + storage_live(_4)\ + storage_live(j)\ + storage_live(_6)\ + _0 = ()\ + e = A { val: const 3i32 }\ + k = B { index: const 3i32 }\ + _4 = &e\ + i = get_valA<'_>(move _4)\ + ↳⚡ undefined_behavior\ + storage_dead(_4)\ + _6 = &k\ + j = get_valB<'_>(move _6)\ + ↳⚡ undefined_behavior\ + storage_dead(_6)\ + storage_dead(j)\ + storage_dead(i)\ + storage_dead(k)\ + storage_dead(e)\ + return\ } diff --git a/tests/llbc/tuple/expected b/tests/llbc/tuple/expected index b62479aee00f..0c15d03deae2 100644 --- a/tests/llbc/tuple/expected +++ b/tests/llbc/tuple/expected @@ -1,17 +1,42 @@ -pub fn test::tuple_add(@1: (i32, i32)) -> i32\ +// Full name: test::tuple_add\ +pub fn tuple_add(t: (i32, i32)) -> i32\ {\ - let @0: i32; // return\ - let t@1: (i32, i32); // arg #1\ - let @2: i32; // anonymous local\ - let @3: i32; // anonymous local\ - let @4: (i32, bool); // anonymous local\ + let _0: i32; // return\ + let t: (i32, i32); // arg #1\ + let _2: i32; // anonymous local\ + let _3: i32; // anonymous local\ + let _4: i32; // anonymous local\ \ - @2 := copy ((t@1).0)\ - @3 := copy ((t@1).1)\ - nop\ - nop\ - @0 := copy (@2) + copy (@3)\ - storage_dead(@3)\ - storage_dead(@2)\ + storage_live(_0)\ + storage_live(_2)\ + storage_live(_3)\ + storage_live(_4)\ + _2 = copy t.0\ + _3 = copy t.1\ + _4 = copy _2 panic.+ copy _3\ + _0 = move _4\ + storage_dead(_3)\ + storage_dead(_2)\ + storage_dead(_4)\ + storage_dead(t)\ + return\ +} + +// Full name: test::main\ +pub fn main()\ +{\ + let _0: (); // return\ + let s: i32; // local\ + let _2: (i32, i32); // anonymous local\ +\ + storage_live(_0)\ + storage_live(s)\ + storage_live(_2)\ + _0 = ()\ + _2 = (const 1i32, const 2i32)\ + s = tuple_add(move _2)\ + ↳⚡ undefined_behavior\ + storage_dead(_2)\ + storage_dead(s)\ return\ } diff --git a/tests/llbc/unops/expected b/tests/llbc/unops/expected index 9e048a4f41d7..4eaa37256daf 100644 --- a/tests/llbc/unops/expected +++ b/tests/llbc/unops/expected @@ -1,29 +1,60 @@ -pub fn test::lnot(@1: bool) -> bool\ +// Full name: test::not\ +pub fn not(a: u8) -> u8\ {\ - let @0: bool; // return\ - let a@1: bool; // arg #1\ + let _0: u8; // return\ + let a: u8; // arg #1\ \ - @0 := ~(copy (a@1))\ + storage_live(_0)\ + _0 = ~(copy a)\ + storage_dead(a)\ return\ } -pub fn test::neg(@1: i32) -> i32\ +// Full name: test::neg\ +pub fn neg(a: i32) -> i32\ {\ - let @0: i32; // return\ - let a@1: i32; // arg #1\ - let @2: bool; // anonymous local\ + let _0: i32; // return\ + let a: i32; // arg #1\ \ - nop\ - nop\ - @0 := -(copy (a@1))\ + storage_live(_0)\ + _0 = panic.-(copy a)\ + storage_dead(a)\ return\ } -pub fn test::not(@1: u8) -> u8\ +// Full name: test::lnot\ +pub fn lnot(a: bool) -> bool\ {\ - let @0: u8; // return\ - let a@1: u8; // arg #1\ + let _0: bool; // return\ + let a: bool; // arg #1\ \ - @0 := ~(copy (a@1))\ + storage_live(_0)\ + _0 = ~(copy a)\ + storage_dead(a)\ + return\ +} + +// Full name: test::main\ +pub fn main()\ +{\ + let _0: (); // return\ + let _1: i32; // anonymous local\ + let _2: u8; // anonymous local\ + let _3: bool; // anonymous local\ +\ + storage_live(_0)\ + storage_live(_1)\ + storage_live(_2)\ + storage_live(_3)\ + _0 = ()\ + _1 = neg(const 3i32)\ + ↳⚡ undefined_behavior\ + storage_dead(_1)\ + _2 = not(const 1u8)\ + ↳⚡ undefined_behavior\ + storage_dead(_2)\ + _3 = lnot(const true)\ + ↳⚡ undefined_behavior\ + storage_dead(_3)\ return\ }