From cbd1e83c7dfb17288769cb0c8ef3dd3ad0650d58 Mon Sep 17 00:00:00 2001 From: Felipe Monteiro Date: Sun, 27 Sep 2026 18:32:22 +0000 Subject: [PATCH 1/9] Move the Charon pin to nightly-2026.09.26 and drop the patch machinery Charon at `nightly-2026.09.26` (67da6d3b, 2,176 commits past our pin) builds on our toolchain without any patch, so `scripts/charon-patch.diff`, the CI step that applied it, and the workspace `[patch]` that redirected Charon's `annotate-snippets` git dependency all go. That dependency is now a crates.io release. Charon picked up a new git dependency, `serde_state` (Nadrieril's fork, not the unrelated crates.io crate of that name), which `cargo deny` rejects; allow it next to `tracing-tree`. AeneasVerif/charon#1486 asks whether it can be published. The LLBC backend does not compile against this Charon yet; the following commits port it. --- .github/workflows/kani.yml | 7 - Cargo.lock | 428 ++++++++++++++++++++----------------- Cargo.toml | 9 - charon | 2 +- deny.toml | 7 +- scripts/charon-patch.diff | 359 ------------------------------- 6 files changed, 238 insertions(+), 574 deletions(-) delete mode 100644 scripts/charon-patch.diff 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..883c8b0ea538 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", + "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,25 @@ dependencies = [ "stacker", ] +[[package]] +name = "serde_state" +version = "1.0.0" +source = "git+https://github.com/Nadrieril/serde_state?branch=main#78055e2f2be94b27c58027854d151d87a75957cc" +dependencies = [ + "serde", + "serde_state_derive", +] + +[[package]] +name = "serde_state_derive" +version = "1.0.0" +source = "git+https://github.com/Nadrieril/serde_state?branch=main#78055e2f2be94b27c58027854d151d87a75957cc" +dependencies = [ + "proc-macro2", + "quote", + "syn 2.0.119", +] + [[package]] name = "serde_test" version = "1.0.177" @@ -2080,6 +2166,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 +2191,7 @@ dependencies = [ "cfg-if", "libc", "psm", - "windows-sys 0.61.2", + "windows-sys", ] [[package]] @@ -2116,15 +2217,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 +2241,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 +2290,7 @@ dependencies = [ "getrandom 0.4.3", "once_cell", "rustix", - "windows-sys 0.61.2", + "windows-sys", ] [[package]] @@ -2297,7 +2400,7 @@ dependencies = [ "mio", "pin-project-lite", "signal-hook-registry", - "windows-sys 0.61.2", + "windows-sys", ] [[package]] @@ -2544,6 +2647,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 +2678,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 +2810,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 +2878,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 +2887,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..67da6d3b8f31 160000 --- a/charon +++ b/charon @@ -1 +1 @@ -Subproject commit b250680abd40ff1aaa07081d0497dc2755ed112e +Subproject commit 67da6d3b8f31dfb0d003aee1596040f9efd7d27f diff --git a/deny.toml b/deny.toml index 3969607c9308..c91a868479c4 100644 --- a/deny.toml +++ b/deny.toml @@ -48,4 +48,9 @@ wildcards = "allow" unknown-registry = "deny" unknown-git = "deny" allow-registry = ["https://github.com/rust-lang/crates.io-index"] -allow-git = ["https://github.com/Nadrieril/tracing-tree"] +# Charon's git dependencies. `serde_state` has no crates.io release (the crate of that name there is +# an unrelated one); see https://github.com/AeneasVerif/charon/issues/1486. +allow-git = [ + "https://github.com/Nadrieril/serde_state", + "https://github.com/Nadrieril/tracing-tree", +] 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::*; From d950a8bc670aef7046d6e1fd147e4c6441a4b1b2 Mon Sep 17 00:00:00 2001 From: Felipe Monteiro Date: Sun, 27 Sep 2026 18:34:12 +0000 Subject: [PATCH 2/9] LLBC: configure and run Charon the way `charon --preset aeneas` does Kani kept its own copies of Charon's option defaults and of its list of transformation passes, and each Charon release changed both underneath it -- this Charon no longer has `ULLBC_PASSES`/`LLBC_PASSES`, a top-level `reorder_decls`, or most of the `TranslateOptions` fields we set. Charon now exposes the pieces its own driver uses. Build `CliOpts` with the `aeneas` preset (the configuration Aeneas consumes), derive `TranslateOptions` from it with `TranslateOptions::new`, and after Kani's own MIR-to-ULLBC translation run `run_transformation_passes`. That covers the opacity policy we hand-built -- `_` foreign, `crate` transparent, `Allocator` and its impls hidden -- and the LLBC printing the expected tests use, so all of it goes. The MIR level is no longer set: only Charon's own MIR fetcher reads it, and Kani translates the MIR it has already transformed. --- .../codegen_aeneas_llbc/compiler_interface.rs | 121 ++++-------------- 1 file changed, 23 insertions(+), 98 deletions(-) diff --git a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs index 44e1c5fd3b61..b05a33f9dc5d 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs @@ -12,12 +12,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::{ @@ -105,7 +103,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,42 +125,10 @@ 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) - } - - // # 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); // TODO: display an error report about the external dependencies, if necessary if ccx.errors.borrow().error_count > 0 { @@ -178,7 +144,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 +363,24 @@ 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() +/// 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() }; - 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(), - } + 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 errors = ErrorCtx::new(); + let options = TranslateOptions::new(&mut errors, &charon_cli_options(false)); TransformCtx { options, translated, errors: std::cell::RefCell::new(errors) } } From 45f9d71cae33f05de4a26138a8d38aad713934a7 Mon Sep 17 00:00:00 2001 From: Felipe Monteiro Date: Sun, 27 Sep 2026 18:36:14 +0000 Subject: [PATCH 3/9] cargo deny: update the exceptions for Charon's new dependency set The four MPL-2.0 exceptions (brownstone, colored, indent_write, nom-supreme) were for Charon dependencies that are gone; `ustr` (BSD-2-Clause-Patent) is new. Two new dependencies carry unmaintained-crate advisories: `paste` (RUSTSEC-2024-0436), used by Charon directly, and `atomic-polyfill` (RUSTSEC-2023-0089), via postcard -> heapless. Neither is a vulnerability, and both are only reached through the LLBC backend, which sits behind the `llbc` feature and is not part of Kani releases, so ignore them with that reason. `cargo deny --all-features --workspace check` passes. --- deny.toml | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/deny.toml b/deny.toml index c91a868479c4..c07647814c5d 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] From 5563d50f77a570e9405a245326e46c07e5a6e925 Mon Sep 17 00:00:00 2001 From: Felipe Monteiro Date: Sun, 27 Sep 2026 19:17:19 +0000 Subject: [PATCH 4/9] LLBC: port the MIR-to-ULLBC translation to the current Charon AST Charon's AST was reorganised between our old pin and nightly-2026.09.26, and some of it was redesigned rather than renamed. The renames are mechanical; for every redesigned construct, this follows what Charon's own MIR translator (`bin/charon-driver/translate`) emits, since that is what the passes and Aeneas expect: - Arithmetic carries an overflow mode: MIR `Add`/`Sub`/`Mul`/shifts are `Wrap`, their `*Unchecked` forms and `Div`/`Rem` are `UB`, and `CheckedBinaryOp` is `AddChecked`/... (upstream's `translate_binaryop_kind`). - `Assert` is a terminator whose `check_kind` records the check. Kani dropped the MIR assert message; it is translated now, because `reconstruct_fallible_operations` only folds an overflow, bounds or division check into the operation it guards when it knows which check it is. - Constants are `ConstantExpr::new(kind, ty)`, with `Literal` and `ConstGeneric` merged into `ConstantExprKind`; integer values come from `IntegerValue::from_bits` instead of a hand-written table. - Switches are `SwitchData` plus a branch table, built as upstream does. - Builtin types are type declarations: tuples point at `TypeDeclId::UNIT`, `str` is the builtin `struct str { _0: [u8] }`, `Box` is tagged builtin. - Drops are terminators naming their drop glue. Upstream reaches it through a proof for its synthetic `Destruct::drop_glue`; Kani points at `drop_in_place::`, which is that glue. - `TraitDecl` is built around associated items, `TraitRef` is hash-consed, and `FunDecl` holds the generics that used to be on the signature. Three things Charon's own driver sets up and Kani now does too: - `TypeDeclId::UNIT` must be the declaration of `()`. Every tuple points there, so without reserving it first, tuples silently named whichever ADT was registered first. - The target information, which `compute_layout_guarantees` requires. - `item_names`, which the printer and `compute_short_names` read; LLBC is now printed with item names instead of `@Adt0`/`@Fun1`. Charon now type-checks the translation, and it caught a mismatch that the old pin never checked: a function binds a region for each late-bound region of its reference inputs, but calls passed none. Calls now pass them as erased, as upstream does, from the same helper the declaration uses. Trait-clause proofs stay placeholders (`BuiltinOrAuto`), as they were, and trait objects become an explicit `TyKind::Error` instead of a placeholder predicate the new AST no longer has; neither is reachable from the tests. --- .../codegen_aeneas_llbc/compiler_interface.rs | 17 +- .../codegen_aeneas_llbc/mir_to_ullbc/mod.rs | 1280 +++++++++-------- 2 files changed, 724 insertions(+), 573 deletions(-) diff --git a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs index b05a33f9dc5d..c739bbd5a276 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}; @@ -44,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 {} @@ -125,6 +127,8 @@ impl LlbcCodegenBackend { } } + record_item_names(&mut ccx.translated); + // 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. @@ -368,18 +372,15 @@ where /// 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() - }; + 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 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..4326478e9fcd 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,13 +63,13 @@ 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, + AdtDef, AdtKind, Allocation, ConstantKind, FieldDef, FnDef, GenericArgKind, GenericArgs, GenericParamDefKind, IntTy, MirConst, Region, RegionKind, RigidTy, Span, TraitDecl, TraitDef, Ty, TyConst, TyConstKind, TyKind, UintTy, VariantIdx, }; @@ -129,24 +133,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 @@ -185,15 +183,12 @@ impl<'a, 'tcx> Context<'a, 'tcx> { 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))); } @@ -227,7 +222,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { 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 +256,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 +264,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 +297,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 +312,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 +327,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 +342,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 +357,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,17 +365,10 @@ 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) } @@ -406,12 +388,17 @@ impl<'a, 'tcx> Context<'a, 'tcx> { 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: _ } => { @@ -424,14 +411,10 @@ 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(index), name, - ty: lit_ty, + ty: trans_ty, }; c_const_generics.push(c_constgeneric); } @@ -466,6 +449,8 @@ impl<'a, 'tcx> Context<'a, 'tcx> { let c_region = CharonRegionVar { index: CharonRegionId::from_usize(epr.index as usize), name: Some(epr.name), + variance: CharonVariance::Unknown, + mutability: CharonLifetimeMutability::Unknown, }; c_regions.push(c_region); } @@ -476,6 +461,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { let c_typevar = CharonTypeVar { index: CharonTypeVarId::from_usize(paramty.index as usize), name: paramty.name, + variance: CharonVariance::Unknown, }; c_types.push(c_typevar); } @@ -492,14 +478,10 @@ 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), name: paramtc.name.clone(), - ty: lit_ty, + ty: trans_ty, }; c_const_generics.push(c_constgeneric); } @@ -507,15 +489,13 @@ 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); - } - } + for id in late_bound_input_regions(&input) { + c_regions.push(CharonRegionVar { + index: CharonRegionId::from_usize(id), + name: None, + variance: CharonVariance::Unknown, + mutability: CharonLifetimeMutability::Unknown, + }); } let trait_clauses = self.get_traitclauses_from_defid(fndef.def_id()); CharonGenericParams { @@ -547,6 +527,8 @@ impl<'a, 'tcx> Context<'a, 'tcx> { let c_region = CharonRegionVar { index: CharonRegionId::from_usize(epr.index as usize), name: Some(epr.name), + variance: CharonVariance::Unknown, + mutability: CharonLifetimeMutability::Unknown, }; c_regions.push(c_region); } @@ -557,6 +539,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { let c_typevar = CharonTypeVar { index: CharonTypeVarId::from_usize(paramty.index as usize), name: paramty.name, + variance: CharonVariance::Unknown, }; c_types.push(c_typevar); } @@ -574,14 +557,10 @@ 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), name: paramtc.name.clone(), - ty: lit_ty, + ty: trans_ty, }; c_const_generics.push(c_constgeneric); } @@ -602,12 +581,12 @@ 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); + 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 +594,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 +605,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 +721,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 +938,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,15 +952,19 @@ 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"), @@ -1014,18 +974,18 @@ impl<'a, 'tcx> Context<'a, 'tcx> { 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 { + // 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"), @@ -1052,25 +1012,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 +1044,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 +1056,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 +1076,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,7 +1103,6 @@ impl<'a, 'tcx> Context<'a, 'tcx> { types: c_types, const_generics: c_const_generics, trait_refs, - target, } } @@ -1150,11 +1111,11 @@ impl<'a, 'tcx> Context<'a, 'tcx> { ga: GenericArgs, defid: DefId, ) -> CharonGenericArgs { - let target = CharonGenericsSource::Item(*self.id_map.get(&defid).unwrap()); + let _ = defid; 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 +1129,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 +1139,6 @@ impl<'a, 'tcx> Context<'a, 'tcx> { types: c_types, const_generics: c_const_generics, trait_refs: CharonVector::new(), - target, } } @@ -1196,58 +1156,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), ); - 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 +1213,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 +1239,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( @@ -1304,18 +1263,25 @@ impl<'a, 'tcx> Context<'a, 'tcx> { } RigidTy::FnPtr(polyfunsig) => { 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), + let inputs = value.inputs().iter().map(|ty| self.translate_ty(*ty)).collect(); + let output = self.translate_ty(value.output()); + 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)) + // TODO: populate regions? + CharonTy::new(CharonTyKind::FnPtr(CharonRegionBinder { + regions: CharonVector::new(), + 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 +1295,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 +1331,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 +1350,28 @@ 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; + // the glue for `T` is exactly `drop_in_place::`, which Kani already collects. + 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 +1379,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 +1409,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 a region for each late-bound region of its inputs + // (`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 inputs = match instance.ty().kind() { + TyKind::RigidTy(RigidTy::FnDef(fndef, _)) => fndef.fn_sig().value.inputs().to_vec(), + _ => panic!("Expected a function type"), + }; + for _ in late_bound_input_regions(&inputs) { + 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 +1510,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 +1549,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 +1559,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 +1608,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 +1620,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 +1645,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 +1674,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 +1734,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) => { @@ -1792,79 +1803,227 @@ 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 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), +/// 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 late-bound regions a function declaration binds for its inputs: one per top-level +/// reference argument. `generic_params_from_fndef` declares them and call sites must supply them, +/// so both use this. +fn late_bound_input_regions(inputs: &[Ty]) -> Vec { + inputs + .iter() + .filter_map(|ty| match ty.kind() { + TyKind::RigidTy(RigidTy::Ref(r, _, _)) => match r.kind { + RegionKind::ReBound(_, br) => Some(br.var as usize), + _ => None, + }, + _ => None, + }) + .collect() +} + +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 +2038,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 +2051,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!(), - } -} From e88ea4eed005b13fe5456386b6d00315189e0bc9 Mon Sep 17 00:00:00 2001 From: Felipe Monteiro Date: Sun, 27 Sep 2026 19:17:19 +0000 Subject: [PATCH 5/9] LLBC: refresh the expected output for the current Charon MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Every expected file changed, and I reviewed each against its old version for meaning rather than format. What changed: - Formatting: `_0 = copy i == const 0i32` for `@0 := copy (i@1) == const (0 : i32)`, `storage_live`, and a `↳⚡` line for each call's unwind edge (Kani's existing abort block, now printed). - Items are printed by name (`is_zero(..)`, `(i32, i32)`, `Option`) rather than by id, now that `item_names` is filled in. Since ids no longer appear, `main` is included again; `diverging_call`'s real check is the call in `main`. The `()` declaration is left out, as it is the same in every test. - Arithmetic spells its overflow mode: wrapping `wrap.+`, checked `panic.+` (was `+`, "fails on overflow"), and `/`, `%`, shifts and negation `panic.`, all as before. `unchecked_*` is now `ub.+` where it was `+`: its overflow is undefined behavior, which the old AST could not express. - Drops name their glue: `drop[drop_glue<'_, Option>] b`, with the types matching the values dropped. Nothing else changed meaning: literal values (negative ones at every width), switch arms, enum and tuple projections, trait impl and inherent method names are the same. --- tests/llbc/arith_checked/expected | 88 +++++++++---- tests/llbc/arith_unchecked/expected | 67 +++++++--- tests/llbc/arith_wrapping/expected | 67 +++++++--- tests/llbc/arith_wrapping/test.rs | 6 +- tests/llbc/basic0/expected | 26 +++- tests/llbc/basic1/expected | 49 ++++++-- tests/llbc/bool_char/expected | 39 ++++-- tests/llbc/div_rem/expected | 61 ++++++---- tests/llbc/diverging_call/expected | 25 +++- tests/llbc/enum/expected | 57 ++++++--- tests/llbc/generic/expected | 101 ++++++++++----- tests/llbc/inherent_core/expected | 34 +++++- tests/llbc/inherent_local/expected | 39 +++++- tests/llbc/int_literals/expected | 36 +++++- tests/llbc/option/expected | 80 ++++++++---- tests/llbc/projection/expected | 183 +++++++++++++++++++--------- tests/llbc/shifts/expected | 54 +++++--- tests/llbc/struct/expected | 36 ++++-- tests/llbc/switch_int/expected | 39 ++++-- tests/llbc/traitimpl/expected | 72 ++++++++--- tests/llbc/tuple/expected | 51 ++++++-- tests/llbc/unops/expected | 61 +++++++--- 22 files changed, 939 insertions(+), 332 deletions(-) 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/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\ } From f5c3d5139408af99f968448eaddd48c37f49e0ca Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 29 Sep 2026 14:54:54 +0000 Subject: [PATCH 6/9] LLBC: declare generic parameters and regions the way Charon numbers them With Charon's type check now running on the translation, several common signatures made it reject Kani's output ("Found incorrect region var" / "Found incorrect type var") and the compiler then hit a `todo!()`: - `fn get(x: Option<&u32>)`, `fn deref2(x: &&u32)`, `fn read(h: Holder<'_>)`: only top-level `&T` inputs contributed late-bound regions, so a region nested in an ADT or another reference was undeclared. `fn pick<'a>(x: &'a u32, y: &'a u32)` declared `'a` twice, once per input. - `fn f<'a, T: 'a>(x: &'a T)`, `fn rd<'a, T>(x: R<'a, T>)`, methods of an `impl<'a>`: parameters were numbered with rustc's index, which counts all kinds together (and parent generics first), while Charon numbers each kind from zero. Late-bound regions also reused the ids of early-bound ones. - `FnDef::fn_sig` erases early-bound regions, so `f` above printed `x: &'_ T`. - Function-pointer types declared no regions for their own binder. Now, as in Charon's translation: - the late-bound regions are the signature binder's bound variables (all of them, each once, wherever they occur), numbered after the early-bound regions; - every generic parameter gets its position among parameters of the same kind, computed per item from `generics_of`, including parents; an `ItemGenerics` scope is active while translating a type, trait or function declaration (and a function's generic body, which mentions its parameters); - the declaration's signature comes from `tcx.fn_sig(..).instantiate_identity()`; - function-pointer types bind their regions, and item parameters inside them are referenced one binder further out. Elided regions (`'_`) stay unnamed, as Charon leaves them. `tests/llbc/regions` covers each case; it fails without this change. The llbc suite passes (22/22), and fmt and both CI clippy invocations are clean. `cargo clippy --features llbc` still reports the three pre-existing lints that #4886 fixes. Co-authored-by: Kiro --- .../codegen_aeneas_llbc/mir_to_ullbc/mod.rs | 236 ++++++++++++++---- tests/llbc/regions/expected | 20 ++ tests/llbc/regions/test.rs | 70 ++++++ 3 files changed, 276 insertions(+), 50 deletions(-) create mode 100644 tests/llbc/regions/expected create mode 100644 tests/llbc/regions/test.rs 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 4326478e9fcd..6f6a735a5fda 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 @@ -69,9 +69,10 @@ use rustc_public::mir::{ }; use rustc_public::rustc_internal; use rustc_public::ty::{ - AdtDef, AdtKind, Allocation, ConstantKind, FieldDef, 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; @@ -93,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> { @@ -116,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) } @@ -374,6 +462,15 @@ impl<'a, 'tcx> Context<'a, 'tcx> { //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(); @@ -381,7 +478,7 @@ 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 => { @@ -404,7 +501,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { 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; @@ -432,7 +529,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"), @@ -447,7 +544,7 @@ 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, @@ -459,7 +556,7 @@ 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, }; @@ -479,7 +576,9 @@ impl<'a, 'tcx> Context<'a, 'tcx> { let ty_stable = rustc_internal::stable(ty_internal); let trans_ty = self.translate_ty(ty_stable); 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: trans_ty, }; @@ -489,10 +588,12 @@ impl<'a, 'tcx> Context<'a, 'tcx> { }, } } - for id in late_bound_input_regions(&input) { - c_regions.push(CharonRegionVar { - index: CharonRegionId::from_usize(id), - name: None, + // 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, }); @@ -525,7 +626,7 @@ 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, @@ -537,7 +638,7 @@ 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, }; @@ -558,7 +659,9 @@ impl<'a, 'tcx> Context<'a, 'tcx> { let ty_stable = rustc_internal::stable(ty_internal); let trans_ty = self.translate_ty(ty_stable); 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: trans_ty, }; @@ -581,6 +684,12 @@ impl<'a, 'tcx> Context<'a, 'tcx> { } fn translate_adtdef(&mut self, adt_def: AdtDef) -> CharonTypeDecl { + 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); @@ -969,11 +1078,16 @@ impl<'a, 'tcx> Context<'a, 'tcx> { 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()); + 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, @@ -990,8 +1104,10 @@ impl<'a, 'tcx> Context<'a, 'tcx> { 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) } @@ -1147,8 +1263,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)) } @@ -1170,8 +1286,8 @@ impl<'a, 'tcx> Context<'a, 'tcx> { } 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)), ); // Neither `TyConst` nor `ParamConst` carries the parameter's type. let ty = param_ty.unwrap_or_else(|| todo!("const generic parameter {paramc:?}")); @@ -1262,9 +1378,20 @@ 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; + 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, @@ -1272,11 +1399,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { inputs, output, }; - // TODO: populate regions? - CharonTy::new(CharonTyKind::FnPtr(CharonRegionBinder { - regions: CharonVector::new(), - skip_binder: sig, - })) + 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. @@ -1441,14 +1564,14 @@ impl<'a, 'tcx> Context<'a, 'tcx> { _ => panic!("Expected a function type"), }; let mut generics = self.translate_generic_args(genarg_resolve, def_id); - // The callee's declaration also binds a region for each late-bound region of its inputs + // 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 inputs = match instance.ty().kind() { - TyKind::RigidTy(RigidTy::FnDef(fndef, _)) => fndef.fn_sig().value.inputs().to_vec(), + let sig = match instance.ty().kind() { + TyKind::RigidTy(RigidTy::FnDef(fndef, _)) => fndef.fn_sig(), _ => panic!("Expected a function type"), }; - for _ in late_bound_input_regions(&inputs) { + for _ in late_bound_regions(&sig) { generics.regions.push(CharonRegion::Erased); } CharonFnPtr::new(CharonFunIdOrTraitMethodRef::Fun(fid), generics) @@ -1784,15 +1907,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) } @@ -1925,18 +2059,20 @@ fn missing_ptr_metadata() -> CharonOperand { )) } -/// The late-bound regions a function declaration binds for its inputs: one per top-level -/// reference argument. `generic_params_from_fndef` declares them and call sites must supply them, -/// so both use this. -fn late_bound_input_regions(inputs: &[Ty]) -> Vec { - inputs +/// 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() - .filter_map(|ty| match ty.kind() { - TyKind::RigidTy(RigidTy::Ref(r, _, _)) => match r.kind { - RegionKind::ReBound(_, br) => Some(br.var as usize), - _ => None, - }, - _ => None, + .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() } 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); +} From 817c2aa1fe3ec7bc4bc2d5e4f90283ba5cde56e3 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 29 Sep 2026 14:55:09 +0000 Subject: [PATCH 7/9] LLBC: stop with an error instead of a `todo!()` when Charon reports errors Charon's pass pipeline type-checks the translation, so its error count is no longer zero in practice: on an input it rejects, Kani printed Charon's errors, then panicked with "not yet implemented" and reported an internal compiler error. Emit a fatal error that says Charon reported errors instead; Charon has already printed each of them, and no LLBC file is written. Checked by temporarily undoing the region declarations of the previous commit: `fn get(x: Option<&u32>)` now ends with "error: Charon reported 2 error(s) while translating to LLBC" and no `.llbc` file, instead of a panic. Co-authored-by: Kiro --- .../src/codegen_aeneas_llbc/compiler_interface.rs | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs index c739bbd5a276..136c4efbdbaa 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs @@ -134,9 +134,13 @@ impl LlbcCodegenBackend { // 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); From 3a07dcfc0130c476920c0f780484950bb9070f2d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 29 Sep 2026 14:55:10 +0000 Subject: [PATCH 8/9] LLBC: name the drop glue correctly and drop an unused parameter The comment on the `Drop` terminator said the glue for `T` is `drop_in_place::`, but `Instance::resolve_drop_in_place` resolves to the `core::ptr::drop_glue` lang item (which `drop_in_place` wraps), and that is what the LLBC prints. `translate_generic_args_without_trait` took a `DefId` that it discarded; remove it. No change to the emitted LLBC. Co-authored-by: Kiro --- .../codegen_aeneas_llbc/mir_to_ullbc/mod.rs | 19 +++++++------------ 1 file changed, 7 insertions(+), 12 deletions(-) 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 6f6a735a5fda..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 @@ -266,8 +266,7 @@ 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 { @@ -305,8 +304,7 @@ 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 { @@ -1222,12 +1220,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { } } - fn translate_generic_args_without_trait( - &mut self, - ga: GenericArgs, - defid: DefId, - ) -> CharonGenericArgs { - let _ = defid; + 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(); @@ -1475,8 +1468,10 @@ impl<'a, 'tcx> Context<'a, 'tcx> { } 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; - // the glue for `T` is exactly `drop_in_place::`, which Kani already collects. + // 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); From c00ab4007dcb4bf5643e9b7ca1a8c5d86bc2c09c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 29 Sep 2026 14:57:40 +0000 Subject: [PATCH 9/9] Move the Charon pin to nightly-2026.09.29 and drop the `serde_state` git source Charon's nightly-2026.09.29 tag (962e40b0) differs from nightly-2026.09.26 only in depending on the published `serde_state_perfect_derive` 1.0.0 (MIT OR Apache-2.0) instead of the `serde_state` git fork (AeneasVerif/charon#1486, #1487). With no git source left besides `tracing-tree`, `deny.toml`'s `allow-git` is back to what main has. `cargo update -p charon` changes only the two `serde_state` entries in Cargo.lock. The llbc suite passes (22/22); `cargo deny check licenses sources bans` is ok. Co-authored-by: Kiro --- Cargo.lock | 14 ++++++++------ charon | 2 +- deny.toml | 7 +------ 3 files changed, 10 insertions(+), 13 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 883c8b0ea538..e6775698de59 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -320,7 +320,7 @@ dependencies = [ "serde", "serde_json", "serde_stacker", - "serde_state", + "serde_state_perfect_derive", "smallvec", "stacker", "syn 1.0.109", @@ -2068,18 +2068,20 @@ dependencies = [ ] [[package]] -name = "serde_state" +name = "serde_state_perfect_derive" version = "1.0.0" -source = "git+https://github.com/Nadrieril/serde_state?branch=main#78055e2f2be94b27c58027854d151d87a75957cc" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "fee99988af71dac4de7dd0882da328b8089e1b0bf10c4bb68792ec7581fb0375" dependencies = [ "serde", - "serde_state_derive", + "serde_state_perfect_derive_derive", ] [[package]] -name = "serde_state_derive" +name = "serde_state_perfect_derive_derive" version = "1.0.0" -source = "git+https://github.com/Nadrieril/serde_state?branch=main#78055e2f2be94b27c58027854d151d87a75957cc" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d80d31bfa32e1e337cb392a33c11b6548c0cc888ab1054ce6661aa45f07d28fa" dependencies = [ "proc-macro2", "quote", diff --git a/charon b/charon index 67da6d3b8f31..962e40b0d732 160000 --- a/charon +++ b/charon @@ -1 +1 @@ -Subproject commit 67da6d3b8f31dfb0d003aee1596040f9efd7d27f +Subproject commit 962e40b0d732e7d011520f08ef1e8c540ec75131 diff --git a/deny.toml b/deny.toml index c07647814c5d..ab296ec67055 100644 --- a/deny.toml +++ b/deny.toml @@ -52,9 +52,4 @@ wildcards = "allow" unknown-registry = "deny" unknown-git = "deny" allow-registry = ["https://github.com/rust-lang/crates.io-index"] -# Charon's git dependencies. `serde_state` has no crates.io release (the crate of that name there is -# an unrelated one); see https://github.com/AeneasVerif/charon/issues/1486. -allow-git = [ - "https://github.com/Nadrieril/serde_state", - "https://github.com/Nadrieril/tracing-tree", -] +allow-git = ["https://github.com/Nadrieril/tracing-tree"]