From 5252ccad0c3ee81531084fa18d704c22aceba28a Mon Sep 17 00:00:00 2001 From: fpoli Date: Sat, 15 Jul 2023 07:03:33 +0000 Subject: [PATCH 1/3] Update dependencies (rustc nightly-2023-07-15, viper v-2023-07-05-0730) --- Cargo.lock | 199 +++++++++--------- analysis/src/bin/analysis-driver.rs | 9 +- analysis/src/bin/gen-accessibility-driver.rs | 10 +- analysis/tests/test_analysis.rs | 2 +- jni-gen/src/generators/module.rs | 2 +- .../vir/optimizations/folding/expressions.rs | 2 +- .../src/vir/optimizations/methods/purifier.rs | 8 +- prusti-common/src/vir/to_viper.rs | 12 +- .../prusti-contracts-proc-macros/Cargo.toml | 4 +- prusti-contracts/prusti-contracts/Cargo.toml | 4 +- prusti-contracts/prusti-specs/Cargo.toml | 2 +- prusti-contracts/prusti-specs/src/lib.rs | 18 +- .../prusti-specs/src/parse_closure_macro.rs | 8 +- .../src/specifications/preparser.rs | 3 +- prusti-contracts/prusti-std/Cargo.toml | 4 +- prusti-interface/src/environment/body.rs | 25 ++- .../src/environment/borrowck/facts.rs | 15 +- .../collect_prusti_spec_visitor.rs | 6 +- .../mir_utils/split_aggregate_assignment.rs | 4 +- prusti-interface/src/environment/mod.rs | 4 +- .../src/environment/polonius_info.rs | 2 +- prusti-interface/src/environment/procedure.rs | 6 +- prusti-interface/src/environment/query.rs | 33 ++- prusti-interface/src/prusti_error.rs | 6 +- prusti-interface/src/specs/external.rs | 8 +- prusti-smt-solver/src/solver.rs | 2 + .../counterexample_translation.rs | 4 +- .../counterexample_translation_refactored.rs | 6 +- prusti-viper/src/encoder/encoder.rs | 2 +- prusti-viper/src/encoder/foldunfold/mod.rs | 2 +- prusti-viper/src/encoder/foldunfold/state.rs | 2 +- .../src/encoder/high/generics/interface.rs | 6 +- .../high/procedures/inference/state/places.rs | 2 +- .../core_proof/builtin_methods/interface.rs | 2 +- .../transformations/inline_functions.rs | 2 +- .../transformations/remove_predicates.rs | 2 +- .../src/encoder/mir/contracts/borrows.rs | 4 +- .../src/encoder/mir/contracts/contracts.rs | 14 +- .../src/encoder/mir/contracts/interface.rs | 20 +- .../src/encoder/mir/generics/interface.rs | 8 +- .../encoder/builtin_function_encoder.rs | 4 +- .../encoder/elaborate_drops/mir_dataflow.rs | 157 ++++---------- .../encoder/elaborate_drops/mir_transform.rs | 33 +-- .../mir/procedures/encoder/initialisation.rs | 20 +- .../src/encoder/mir/procedures/encoder/mod.rs | 17 +- .../mir/procedures/encoder/termination.rs | 6 +- .../mir/pure/interpreter/interpreter_high.rs | 21 +- .../mir/pure/interpreter/interpreter_poly.rs | 5 +- .../mir/pure/pure_functions/encoder_high.rs | 12 +- .../mir/pure/pure_functions/encoder_poly.rs | 10 +- .../mir/pure/pure_functions/interface.rs | 32 +-- .../mir/pure/specifications/encoder_high.rs | 8 +- .../mir/pure/specifications/encoder_poly.rs | 8 +- .../mir/pure/specifications/interface.rs | 26 +-- .../encoder/mir/pure/specifications/utils.rs | 12 +- .../encoder/mir/specifications/constraints.rs | 10 +- .../encoder/mir/specifications/interface.rs | 38 ++-- .../src/encoder/mir/types/const_parameters.rs | 16 +- prusti-viper/src/encoder/mir/types/encoder.rs | 16 +- .../src/encoder/mir/types/interface.rs | 14 +- .../src/encoder/mir/types/lifetimes.rs | 18 +- .../encoder/mir_encoder/downcast_detector.rs | 9 +- prusti-viper/src/encoder/mir_encoder/mod.rs | 12 +- prusti-viper/src/encoder/procedure_encoder.rs | 30 +-- .../src/encoder/stub_function_encoder.rs | 8 +- prusti-viper/src/lib.rs | 6 +- prusti-viper/src/utils/mod.rs | 1 + prusti-viper/src/utils/type_visitor.rs | 22 +- prusti/src/callbacks.rs | 3 +- prusti/src/driver.rs | 11 +- rust-toolchain | 2 +- viper-toolchain | 2 +- vir/src/legacy/ast/common.rs | 19 +- vir/src/legacy/ast/function.rs | 7 +- vir/src/lib.rs | 1 + 75 files changed, 510 insertions(+), 580 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 0a813e09cd2..dd0c0cbfdc3 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -119,9 +119,9 @@ dependencies = [ [[package]] name = "anyhow" -version = "1.0.71" +version = "1.0.72" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9c7d0618f0e0b7e8ff11427422b64564d5fb0be1940354bfe2e0529b18a9d9b8" +checksum = "3b13c32d80ecc7ab747b80c3784bce54ee8a7a0cc4fbda9bf4cda2cf6fe90854" [[package]] name = "async-attributes" @@ -153,7 +153,7 @@ dependencies = [ "async-lock", "async-task", "concurrent-queue", - "fastrand", + "fastrand 1.9.0", "futures-lite", "slab", ] @@ -256,13 +256,13 @@ checksum = "ecc7ab41815b3c653ccd2978ec3255c81349336702dfdf62ee6f7069b12a3aae" [[package]] name = "async-trait" -version = "0.1.71" +version = "0.1.72" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a564d521dd56509c4c47480d00b80ee55f7e385ae48db5744c67ad50c92d2ebf" +checksum = "cc6dde6e4ed435a4c1ee4e73592f5ba9da2151af10076cc04858746af9352d09" dependencies = [ "proc-macro2", "quote", - "syn 2.0.25", + "syn 2.0.27", ] [[package]] @@ -388,7 +388,7 @@ dependencies = [ "async-lock", "async-task", "atomic-waker", - "fastrand", + "fastrand 1.9.0", "futures-lite", "log", ] @@ -499,9 +499,9 @@ dependencies = [ [[package]] name = "clap" -version = "4.3.11" +version = "4.3.17" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1640e5cc7fb47dbb8338fd471b105e7ed6c3cb2aeb00c2e067127ffd3764a05d" +checksum = "5b0827b011f6f8ab38590295339817b0d26f344aa4932c3ced71b45b0c54b4a9" dependencies = [ "clap_builder", "clap_derive", @@ -510,9 +510,9 @@ dependencies = [ [[package]] name = "clap_builder" -version = "4.3.11" +version = "4.3.17" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "98c59138d527eeaf9b53f35a77fcc1fad9d883116070c63d5de1c7dc7b00c72b" +checksum = "9441b403be87be858db6a23edb493e7f694761acdc3343d5a0fcaafd304cbc9e" dependencies = [ "anstream", "anstyle", @@ -522,14 +522,14 @@ dependencies = [ [[package]] name = "clap_derive" -version = "4.3.2" +version = "4.3.12" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b8cd2b2a819ad6eec39e8f1d6b53001af1e5469f8c177579cdaeb313115b825f" +checksum = "54a9bb5758fc5dfe728d1019941681eccaf0cf8a4189b692a0ee2f2ecf90a050" dependencies = [ "heck", "proc-macro2", "quote", - "syn 2.0.25", + "syn 2.0.27", ] [[package]] @@ -617,9 +617,9 @@ dependencies = [ [[package]] name = "const-oid" -version = "0.9.3" +version = "0.9.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6340df57935414636969091153f35f68d9f00bbc8fb4a9c6054706c213e6c6bc" +checksum = "795bc6e66a8e340f075fcf6227e417a2dc976b92b91f3cdc778bb858778b6747" [[package]] name = "content_inspector" @@ -918,9 +918,9 @@ checksum = "56ce8c6da7551ec6c462cbaf3bfbc75131ebbfa1c944aeaa9dab51ca1c5f0c3b" [[package]] name = "ecdsa" -version = "0.16.7" +version = "0.16.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0997c976637b606099b9985693efa3581e84e41f5c11ba5255f88711058ad428" +checksum = "a4b1e0c257a9e9f25f90ff76d7a68360ed497ee519c8e428d1825ef0000799d4" dependencies = [ "der", "digest", @@ -990,9 +990,9 @@ dependencies = [ [[package]] name = "equivalent" -version = "1.0.0" +version = "1.0.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "88bffebc5d80432c9b140ee17875ff173a8ab62faad5b257da912bd2f6c1c0a1" +checksum = "5443807d6dff69373d433ab9ef5378ad8df50ca6298caf15de6e52e24aaf54d5" [[package]] name = "errno" @@ -1062,6 +1062,12 @@ dependencies = [ "instant", ] +[[package]] +name = "fastrand" +version = "2.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6999dc1837253364c2ebb0704ba97994bd874e8f195d665c50b7548f6ea92764" + [[package]] name = "ff" version = "0.13.0" @@ -1195,7 +1201,7 @@ version = "1.13.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "49a9d51ce47660b1e808d3c990b4709f2f415d928835a17dfd16991515c46bce" dependencies = [ - "fastrand", + "fastrand 1.9.0", "futures-core", "futures-io", "memchr", @@ -1212,7 +1218,7 @@ checksum = "89ca545a94061b6365f2c7355b4b32bd20df3ff95f02da9329b34ccc3bd6ee72" dependencies = [ "proc-macro2", "quote", - "syn 2.0.25", + "syn 2.0.27", ] [[package]] @@ -1605,7 +1611,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "cb0889898416213fab133e1d33a0e5858a48177452750691bde3666d0fdbaf8b" dependencies = [ "hermit-abi 0.3.2", - "rustix 0.38.3", + "rustix 0.38.4", "windows-sys 0.48.0", ] @@ -1629,9 +1635,9 @@ dependencies = [ [[package]] name = "itoa" -version = "1.0.8" +version = "1.0.9" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "62b02a5381cc465bd3041d84623d0fa3b66738b52b8e2fc3bab8ad63ab032f4a" +checksum = "af150ab688ff2122fcef229be89cb50dd66af9e01a4ff320cc137eecc9bacc38" [[package]] name = "jni" @@ -1976,9 +1982,9 @@ dependencies = [ [[package]] name = "num-traits" -version = "0.2.15" +version = "0.2.16" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "578ede34cf02f8924ab9447f50c28075b4d3e5b269972345e7e0372b38c6cdcd" +checksum = "f30b0abd723be7e2ffca1272140fac1a2f084c77ec3e123c192b66af1ee9e6c2" dependencies = [ "autocfg", ] @@ -2031,7 +2037,7 @@ checksum = "a948666b637a0f465e8564c73e89d4dde00d72d4d473cc972f390fc3dcee7d9c" dependencies = [ "proc-macro2", "quote", - "syn 2.0.25", + "syn 2.0.27", ] [[package]] @@ -2141,9 +2147,9 @@ checksum = "9b2a4787296e9989611394c33f193f676704af1686e70b8f8033ab5ba9a35a94" [[package]] name = "pest" -version = "2.7.0" +version = "2.7.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f73935e4d55e2abf7f130186537b19e7a4abc886a0252380b59248af473a3fc9" +checksum = "0d2d1d55045829d65aad9d389139882ad623b33b904e7c9f1b10c5b8927298e5" dependencies = [ "thiserror", "ucd-trie", @@ -2151,9 +2157,9 @@ dependencies = [ [[package]] name = "pest_derive" -version = "2.7.0" +version = "2.7.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "aef623c9bbfa0eedf5a0efba11a5ee83209c326653ca31ff019bec3a95bfff2b" +checksum = "5f94bca7e7a599d89dea5dfa309e217e7906c3c007fb9c3299c40b10d6a315d3" dependencies = [ "pest", "pest_generator", @@ -2161,22 +2167,22 @@ dependencies = [ [[package]] name = "pest_generator" -version = "2.7.0" +version = "2.7.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b3e8cba4ec22bada7fc55ffe51e2deb6a0e0db2d0b7ab0b103acc80d2510c190" +checksum = "99d490fe7e8556575ff6911e45567ab95e71617f43781e5c05490dc8d75c965c" dependencies = [ "pest", "pest_meta", "proc-macro2", "quote", - "syn 2.0.25", + "syn 2.0.27", ] [[package]] name = "pest_meta" -version = "2.7.0" +version = "2.7.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a01f71cb40bd8bb94232df14b946909e14660e33fc05db3e50ae2a82d7ea0ca0" +checksum = "2674c66ebb4b4d9036012091b537aae5878970d6999f81a265034d85b136b341" dependencies = [ "once_cell", "pest", @@ -2200,7 +2206,7 @@ checksum = "ec2e072ecce94ec471b13398d5402c188e76ac03cf74dd1a975161b23a3f6d9c" dependencies = [ "proc-macro2", "quote", - "syn 2.0.25", + "syn 2.0.27", ] [[package]] @@ -2273,9 +2279,9 @@ dependencies = [ [[package]] name = "proc-macro2" -version = "1.0.64" +version = "1.0.66" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "78803b62cbf1f46fde80d7c0e803111524b9877184cfe7c3033659490ac7a7da" +checksum = "18fb31db3f9bddb2ea821cde30a9f70117e3f119938b5ee630b7403aa6e2ead9" dependencies = [ "unicode-ident", ] @@ -2458,9 +2464,9 @@ dependencies = [ [[package]] name = "quote" -version = "1.0.29" +version = "1.0.31" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "573015e8ab27661678357f27dc26460738fd2b6c86e46f386fde94cb5d913105" +checksum = "5fe8a65d69dd0808184ebb5f836ab526bb259db23c657efa38711b1072ee47f0" dependencies = [ "proc-macro2", ] @@ -2554,8 +2560,8 @@ checksum = "b2eae68fc220f7cf2532e4494aded17545fce192d59cd996e0fe7887f4ceb575" dependencies = [ "aho-corasick", "memchr", - "regex-automata 0.3.2", - "regex-syntax 0.7.3", + "regex-automata 0.3.3", + "regex-syntax 0.7.4", ] [[package]] @@ -2569,13 +2575,13 @@ dependencies = [ [[package]] name = "regex-automata" -version = "0.3.2" +version = "0.3.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "83d3daa6976cffb758ec878f108ba0e062a45b2d6ca3a2cca965338855476caf" +checksum = "39354c10dd07468c2e73926b23bb9c2caca74c5501e38a35da70406f1d923310" dependencies = [ "aho-corasick", "memchr", - "regex-syntax 0.7.3", + "regex-syntax 0.7.4", ] [[package]] @@ -2586,9 +2592,9 @@ checksum = "f162c6dd7b008981e4d40210aca20b4bd0f9b60ca9271061b07f78537722f2e1" [[package]] name = "regex-syntax" -version = "0.7.3" +version = "0.7.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2ab07dc67230e4a4718e70fd5c20055a4334b121f1f9db8fe63ef39ce9b8c846" +checksum = "e5ea92a5b6195c6ef2a0295ea818b312502c6fc94dde986c5553242e18fd4ce2" [[package]] name = "remove_dir_all" @@ -2737,9 +2743,9 @@ dependencies = [ [[package]] name = "rustix" -version = "0.38.3" +version = "0.38.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ac5ffa1efe7548069688cd7028f32591853cd7b5b756d41bcffd2353e4fc75b4" +checksum = "0a962918ea88d644592894bc6dc55acc6c0956488adcebbfb6e273506b7fd6e5" dependencies = [ "bitflags 2.3.3", "errno", @@ -2750,9 +2756,9 @@ dependencies = [ [[package]] name = "rustls" -version = "0.21.3" +version = "0.21.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b19faa85ecb5197342b54f987b142fb3e30d0c90da40f80ef4fa9a726e6676ed" +checksum = "79ea77c539259495ce8ca47f53e66ae0330a8819f67e23ac96ca02f50e7b7d36" dependencies = [ "log", "ring", @@ -2791,9 +2797,9 @@ dependencies = [ [[package]] name = "rustversion" -version = "1.0.13" +version = "1.0.14" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "dc31bd9b61a32c31f9650d18add92aa83a49ba979c143eefd27fe7177b05bd5f" +checksum = "7ffc183a10b4478d04cbbbfc96d0873219d962dd5accaff2ffbd4ceb7df837f4" [[package]] name = "rustwide" @@ -2830,9 +2836,9 @@ dependencies = [ [[package]] name = "ryu" -version = "1.0.14" +version = "1.0.15" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fe232bdf6be8c8de797b22184ee71118d63780ea42ac85b61d1baa6d3b782ae9" +checksum = "1ad4cc8da4ef723ed60bced201181d83791ad433213d8c24efffda1eec85d741" [[package]] name = "same-file" @@ -2860,9 +2866,9 @@ checksum = "e1cf6437eb19a8f4a6cc0f7dca544973b0b78843adbfeb3683d1a94a0024a294" [[package]] name = "scopeguard" -version = "1.1.0" +version = "1.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d29ab0c6d3fc0ee92fe66e2d99f700eab17a8d57d1c1d3b748380fb20baa78cd" +checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49" [[package]] name = "sct" @@ -2876,9 +2882,9 @@ dependencies = [ [[package]] name = "sec1" -version = "0.7.2" +version = "0.7.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f0aec48e813d6b90b15f0b8948af3c63483992dee44c03e9930b3eebdabe046e" +checksum = "d3e97a565f76233a6003f9f5c54be1d9c5bdfa3eccfb189469f11ec4901c47dc" dependencies = [ "base16ct", "der", @@ -2913,35 +2919,35 @@ dependencies = [ [[package]] name = "semver" -version = "1.0.17" +version = "1.0.18" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bebd363326d05ec3e2f532ab7660680f3b02130d780c299bca73469d521bc0ed" +checksum = "b0293b4b29daaf487284529cc2f5675b8e57c61f70167ba415a463651fd6a918" [[package]] name = "serde" -version = "1.0.171" +version = "1.0.174" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "30e27d1e4fd7659406c492fd6cfaf2066ba8773de45ca75e855590f856dc34a9" +checksum = "3b88756493a5bd5e5395d53baa70b194b05764ab85b59e43e4b8f4e1192fa9b1" dependencies = [ "serde_derive", ] [[package]] name = "serde_derive" -version = "1.0.171" +version = "1.0.174" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "389894603bd18c46fa56231694f8d827779c0951a667087194cf9de94ed24682" +checksum = "6e5c3a298c7f978e53536f95a63bdc4c4a64550582f31a0359a9afda6aede62e" dependencies = [ "proc-macro2", "quote", - "syn 2.0.25", + "syn 2.0.27", ] [[package]] name = "serde_json" -version = "1.0.100" +version = "1.0.103" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0f1e14e89be7aa4c4b78bdbdc9eb5bf8517829a600ae8eaa39a6e1d960b5185c" +checksum = "d03b412469450d4404fe8499a268edd7f8b79fecb074b0d812ad64ca21f4031b" dependencies = [ "itoa", "ryu", @@ -3008,9 +3014,9 @@ checksum = "45bb67a18fa91266cc7807181f62f9178a6873bfad7dc788c42e6430db40184f" [[package]] name = "signal-hook" -version = "0.3.15" +version = "0.3.17" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "732768f1176d21d09e076c23a93123d40bba92d50c4058da34d45c8de8e682b9" +checksum = "8621587d4798caf8eb44879d42e56b9a93ea5dcd315a6487c357130095b62801" dependencies = [ "libc", "signal-hook-registry", @@ -3154,9 +3160,9 @@ dependencies = [ [[package]] name = "syn" -version = "2.0.25" +version = "2.0.27" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "15e3fc8c0c74267e2df136e5e5fb656a464158aa57624053375eb9c8c6e25ae2" +checksum = "b60f673f44a8255b9c8c657daf66a596d435f2da81a555b06dc644d080ba45e0" dependencies = [ "proc-macro2", "quote", @@ -3190,9 +3196,9 @@ dependencies = [ [[package]] name = "tar" -version = "0.4.38" +version = "0.4.39" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4b55807c0344e1e6c04d7c965f5289c39a8d94ae23ed5c0b57aabac549f871c6" +checksum = "ec96d2ffad078296368d46ff1cb309be1c23c513b4ab0e22a45de0185275ac96" dependencies = [ "filetime", "libc", @@ -3201,15 +3207,14 @@ dependencies = [ [[package]] name = "tempfile" -version = "3.6.0" +version = "3.7.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "31c0432476357e58790aaa47a8efb0c5138f137343f3b5f23bd36a27e3b0a6d6" +checksum = "5486094ee78b2e5038a6382ed7645bc084dc2ec433426ca4c3cb61e2007b8998" dependencies = [ - "autocfg", "cfg-if", - "fastrand", + "fastrand 2.0.0", "redox_syscall 0.3.5", - "rustix 0.37.23", + "rustix 0.38.4", "windows-sys 0.48.0", ] @@ -3266,22 +3271,22 @@ dependencies = [ [[package]] name = "thiserror" -version = "1.0.43" +version = "1.0.44" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a35fc5b8971143ca348fa6df4f024d4d55264f3468c71ad1c2f365b0a4d58c42" +checksum = "611040a08a0439f8248d1990b111c95baa9c704c805fa1f62104b39655fd7f90" dependencies = [ "thiserror-impl", ] [[package]] name = "thiserror-impl" -version = "1.0.43" +version = "1.0.44" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "463fe12d7993d3b327787537ce8dd4dfa058de32fc2b195ef3cde03dc4771e8f" +checksum = "090198534930841fab3a5d1bb637cde49e339654e606195f8d9c76eeb081dc96" dependencies = [ "proc-macro2", "quote", - "syn 2.0.25", + "syn 2.0.27", ] [[package]] @@ -3433,9 +3438,9 @@ dependencies = [ [[package]] name = "toml_edit" -version = "0.19.12" +version = "0.19.14" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c500344a19072298cd05a7224b3c0c629348b78692bf48466c5238656e315a78" +checksum = "f8123f27e969974a3dfba720fdb560be359f57b44302d280ba72e76a74480e8a" dependencies = [ "indexmap 2.0.0", "serde", @@ -3479,7 +3484,7 @@ checksum = "5f4f31f56159e98206da9efd823404b79b6ef3143b4a7ab76e67b1751b25a4ab" dependencies = [ "proc-macro2", "quote", - "syn 2.0.25", + "syn 2.0.27", ] [[package]] @@ -3586,9 +3591,9 @@ checksum = "92888ba5573ff080736b3648696b70cafad7d250551175acbaa4e0385b3e1460" [[package]] name = "unicode-ident" -version = "1.0.10" +version = "1.0.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "22049a19f4a68748a168c0fc439f9516686aa045927ff767eca0a85101fb6e73" +checksum = "301abaae475aa91687eb82514b328ab47a211a533026cb25fc3e519b86adfc3c" [[package]] name = "unicode-normalization" @@ -3658,9 +3663,9 @@ checksum = "711b9620af191e0cdc7468a8d14e709c3dcdb115b36f838e601583af800a370a" [[package]] name = "uuid" -version = "1.4.0" +version = "1.4.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d023da39d1fde5a8a3fe1f3e01ca9632ada0a63e9797de55a879d6e2236277be" +checksum = "79daa5ed5740825c40b389c5e50312b9c86df53fccd33f281df655642b43869d" dependencies = [ "getrandom", ] @@ -3847,7 +3852,7 @@ dependencies = [ "once_cell", "proc-macro2", "quote", - "syn 2.0.25", + "syn 2.0.27", "wasm-bindgen-shared", ] @@ -3881,7 +3886,7 @@ checksum = "54681b18a46765f095758388f2d0cf16eb8d4169b639ab575a8f5693af210c7b" dependencies = [ "proc-macro2", "quote", - "syn 2.0.25", + "syn 2.0.27", "wasm-bindgen-backend", "wasm-bindgen-shared", ] @@ -4168,9 +4173,9 @@ checksum = "1a515f5799fe4961cb532f983ce2b23082366b898e52ffbce459c86f67c8378a" [[package]] name = "winnow" -version = "0.4.9" +version = "0.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "81a2094c43cc94775293eaa0e499fbc30048a6d824ac82c0351a8c0bf9112529" +checksum = "81fac9742fd1ad1bd9643b991319f72dd031016d44b77039a26977eb667141e7" dependencies = [ "memchr", ] diff --git a/analysis/src/bin/analysis-driver.rs b/analysis/src/bin/analysis-driver.rs index e6bfba65d4f..51d8f083669 100644 --- a/analysis/src/bin/analysis-driver.rs +++ b/analysis/src/bin/analysis-driver.rs @@ -16,6 +16,7 @@ use prusti_rustc_interface::{ borrowck::consumers::{self, BodyWithBorrowckFacts}, data_structures::fx::FxHashMap, driver::Compilation, + errors, hir::def_id::{DefId, LocalDefId}, interface::{interface, Config, Queries}, middle::{ @@ -23,7 +24,7 @@ use prusti_rustc_interface::{ ty, }, polonius_engine::{Algorithm, Output}, - session::{Attribute, Session}, + session::{self, Attribute, EarlyErrorHandler, Session}, }; use std::{cell::RefCell, rc::Rc}; @@ -146,6 +147,7 @@ impl prusti_rustc_interface::driver::Callbacks for OurCompilerCalls { fn after_analysis<'tcx>( &mut self, + _error_handler: &EarlyErrorHandler, compiler: &interface::Compiler, queries: &'tcx Queries<'tcx>, ) -> Compilation { @@ -288,7 +290,10 @@ impl prusti_rustc_interface::driver::Callbacks for OurCompilerCalls { /// --analysis=ReachingDefsState or --analysis=DefinitelyInitializedAnalysis fn main() { env_logger::init(); - prusti_rustc_interface::driver::init_rustc_env_logger(); + let error_handler = EarlyErrorHandler::new(session::config::ErrorOutputType::HumanReadable( + errors::emitter::HumanReadableErrorType::Default(errors::emitter::ColorConfig::Auto), + )); + prusti_rustc_interface::driver::init_rustc_env_logger(&error_handler); let mut compiler_args = Vec::new(); let mut callback_args = Vec::new(); for arg in std::env::args() { diff --git a/analysis/src/bin/gen-accessibility-driver.rs b/analysis/src/bin/gen-accessibility-driver.rs index 5c6d1c36cfb..6d0b18486d9 100644 --- a/analysis/src/bin/gen-accessibility-driver.rs +++ b/analysis/src/bin/gen-accessibility-driver.rs @@ -9,7 +9,7 @@ use prusti_rustc_interface::{ borrowck::consumers::{self, BodyWithBorrowckFacts}, data_structures::fx::FxHashMap, driver::Compilation, - hir, + errors, hir, hir::def_id::LocalDefId, interface::{interface, Config, Queries}, middle::{ @@ -17,7 +17,7 @@ use prusti_rustc_interface::{ ty, }, polonius_engine::{Algorithm, Output}, - session::Session, + session::{self, EarlyErrorHandler, Session}, span::FileName, }; use std::{cell::RefCell, path::PathBuf, rc::Rc}; @@ -99,6 +99,7 @@ impl prusti_rustc_interface::driver::Callbacks for OurCompilerCalls { fn after_analysis<'tcx>( &mut self, + _error_handler: &EarlyErrorHandler, compiler: &interface::Compiler, queries: &'tcx Queries<'tcx>, ) -> Compilation { @@ -212,7 +213,10 @@ impl prusti_rustc_interface::driver::Callbacks for OurCompilerCalls { /// Run an analysis by calling like it rustc fn main() { env_logger::init(); - prusti_rustc_interface::driver::init_rustc_env_logger(); + let error_handler = EarlyErrorHandler::new(session::config::ErrorOutputType::HumanReadable( + errors::emitter::HumanReadableErrorType::Default(errors::emitter::ColorConfig::Auto), + )); + prusti_rustc_interface::driver::init_rustc_env_logger(&error_handler); let mut compiler_args = Vec::new(); let mut callback_args = Vec::new(); for arg in std::env::args() { diff --git a/analysis/tests/test_analysis.rs b/analysis/tests/test_analysis.rs index c436321cde6..fe5284bf05e 100644 --- a/analysis/tests/test_analysis.rs +++ b/analysis/tests/test_analysis.rs @@ -13,7 +13,7 @@ fn run_tests(mode: &str, path: &str, custom_args: Vec) { let mut flags = Vec::new(); flags.push("--edition 2018".to_owned()); flags.push(format!("--sysroot {}", find_sysroot())); - flags.extend(custom_args.into_iter()); + flags.extend(custom_args); config.target_rustcflags = Some(flags.join(" ")); config.mode = mode.parse().expect("Invalid mode"); config.rustc_path = find_compiled_executable("analysis-driver"); diff --git a/jni-gen/src/generators/module.rs b/jni-gen/src/generators/module.rs index 7cd436e64cb..eaa500c8ae8 100644 --- a/jni-gen/src/generators/module.rs +++ b/jni-gen/src/generators/module.rs @@ -41,7 +41,7 @@ pub fn generate_module(class_names: Vec<&ClassName>) -> String { }) .unwrap_or_else(|| "// No modules".to_string()); - vec![ + [ "//! Automatically generated code\n".to_string(), "#![allow(non_snake_case)]\n".to_string(), "pub mod builtins;\n".to_string(), diff --git a/prusti-common/src/vir/optimizations/folding/expressions.rs b/prusti-common/src/vir/optimizations/folding/expressions.rs index 40dd44d3cfd..a180d706ac5 100644 --- a/prusti-common/src/vir/optimizations/folding/expressions.rs +++ b/prusti-common/src/vir/optimizations/folding/expressions.rs @@ -163,7 +163,7 @@ fn check_requirements_conflict( conflict_set.insert(base1); } else if base1 == base2 && !place1.has_prefix(place2) && !place2.has_prefix(place1) { // Check if we have different variants. - for (part1, part2) in components1.into_iter().zip(components2.into_iter()) { + for (part1, part2) in components1.into_iter().zip(components2) { match (part1, part2) { ( ast::PlaceComponent::Variant(ast::Field { name: name1, .. }, _), diff --git a/prusti-common/src/vir/optimizations/methods/purifier.rs b/prusti-common/src/vir/optimizations/methods/purifier.rs index 98910126d9e..f465e7c54bf 100644 --- a/prusti-common/src/vir/optimizations/methods/purifier.rs +++ b/prusti-common/src/vir/optimizations/methods/purifier.rs @@ -274,7 +274,13 @@ impl VarPurifier { } } fn get_replacement(&self, expr: &ast::Expr) -> ast::Expr { - let ast::Expr::Local(ast::Local {variable: var, position: pos}) = expr else { unreachable!() }; + let ast::Expr::Local(ast::Local { + variable: var, + position: pos, + }) = expr + else { + unreachable!() + }; let replacement = self .replacements .get(var) diff --git a/prusti-common/src/vir/to_viper.rs b/prusti-common/src/vir/to_viper.rs index 8f0beac6ea9..568d04489ad 100644 --- a/prusti-common/src/vir/to_viper.rs +++ b/prusti-common/src/vir/to_viper.rs @@ -316,7 +316,9 @@ impl<'v> ToViper<'v, viper::Stmt<'v>> for Stmt { ) } Stmt::ApplyMagicWand(ref wand, ref pos) => { - let Expr::MagicWand(_, _, Some(borrow), _) = wand else { unreachable!() }; + let Expr::MagicWand(_, _, Some(borrow), _) = wand else { + unreachable!() + }; let borrow: usize = borrow_id(*borrow); let borrow: Expr = borrow.into(); let inhale = ast.inhale( @@ -618,7 +620,9 @@ impl<'v> ToViper<'v, viper::Expr<'v>> for Expr { ContainerOpKind::SeqLen => ast.seq_length(left.to_viper(context, ast)), }, Expr::Seq(ty, elems, _pos) => { - let Type::Seq(box elem_ty) = ty else { unreachable!() }; + let Type::Seq(box elem_ty) = ty else { + unreachable!() + }; let viper_elem_ty = elem_ty.to_viper(context, ast); if elems.is_empty() { ast.empty_seq(viper_elem_ty) @@ -631,7 +635,9 @@ impl<'v> ToViper<'v, viper::Expr<'v>> for Expr { } } Expr::Map(ty, elems, _pos) => { - let Type::Map(box key_ty, box val_ty) = ty else { unreachable!() }; + let Type::Map(box key_ty, box val_ty) = ty else { + unreachable!() + }; let viper_key_ty = key_ty.to_viper(context, ast); let viper_val_ty = val_ty.to_viper(context, ast); if elems.is_empty() { diff --git a/prusti-contracts/prusti-contracts-proc-macros/Cargo.toml b/prusti-contracts/prusti-contracts-proc-macros/Cargo.toml index 06f0ba29fa1..c6c0cb59e49 100644 --- a/prusti-contracts/prusti-contracts-proc-macros/Cargo.toml +++ b/prusti-contracts/prusti-contracts-proc-macros/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "prusti-contracts-proc-macros" -version = "0.1.9" +version = "0.1.10" authors = ["Prusti Devs "] edition = "2021" license = "MPL-2.0" @@ -15,7 +15,7 @@ categories = ["development-tools", "development-tools::testing"] proc-macro = true [dependencies] -prusti-specs = { path = "../prusti-specs", version = "0.1.9", optional = true } +prusti-specs = { path = "../prusti-specs", version = "0.1.10", optional = true } proc-macro2 = { version = "1.0", optional = true } [features] diff --git a/prusti-contracts/prusti-contracts/Cargo.toml b/prusti-contracts/prusti-contracts/Cargo.toml index fe3b13abb19..6a8e9368096 100644 --- a/prusti-contracts/prusti-contracts/Cargo.toml +++ b/prusti-contracts/prusti-contracts/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "prusti-contracts" -version = "0.1.9" +version = "0.1.10" authors = ["Prusti Devs "] edition = "2021" license = "MPL-2.0" @@ -12,7 +12,7 @@ keywords = ["prusti", "contracts", "verification", "formal", "specifications"] categories = ["development-tools", "development-tools::testing"] [dependencies] -prusti-contracts-proc-macros = { path = "../prusti-contracts-proc-macros", version = "0.1.9" } +prusti-contracts-proc-macros = { path = "../prusti-contracts-proc-macros", version = "0.1.10" } [dev-dependencies] trybuild = "1.0" diff --git a/prusti-contracts/prusti-specs/Cargo.toml b/prusti-contracts/prusti-specs/Cargo.toml index 4c4aded9a47..d9a70fb5c2a 100644 --- a/prusti-contracts/prusti-specs/Cargo.toml +++ b/prusti-contracts/prusti-specs/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "prusti-specs" -version = "0.1.9" +version = "0.1.10" authors = ["Prusti Devs "] edition = "2021" license = "MPL-2.0" diff --git a/prusti-contracts/prusti-specs/src/lib.rs b/prusti-contracts/prusti-specs/src/lib.rs index 965c92790c0..aa784c1267a 100644 --- a/prusti-contracts/prusti-specs/src/lib.rs +++ b/prusti-contracts/prusti-specs/src/lib.rs @@ -1,5 +1,5 @@ #![deny(unused_must_use)] -#![feature(drain_filter)] +#![feature(extract_if)] #![feature(box_patterns)] #![feature(proc_macro_span)] #![feature(if_let_guard)] @@ -78,7 +78,9 @@ fn extract_prusti_attributes( // tokens identical to the ones passed by the native procedural // macro call. let mut iter = attr.tokens.into_iter(); - let TokenTree::Group(group) = iter.next().unwrap() else { unreachable!() }; + let TokenTree::Group(group) = iter.next().unwrap() else { + unreachable!() + }; assert!(iter.next().is_none(), "Unexpected shape of an attribute."); group.stream() } @@ -597,10 +599,14 @@ pub fn refine_trait_spec(_attr: TokenStream, tokens: TokenStream) -> TokenStream let parsed_predicate = handle_result!(predicate::parse_predicate_in_impl(makro.mac.tokens.clone())); - let ParsedPredicate::Impl(predicate) = parsed_predicate else { unreachable!() }; + let ParsedPredicate::Impl(predicate) = parsed_predicate else { + unreachable!() + }; // Patch spec function: Rewrite self with _self: - let syn::Item::Fn(spec_function) = predicate.spec_function else { unreachable!() }; + let syn::Item::Fn(spec_function) = predicate.spec_function else { + unreachable!() + }; generated_spec_items.push(spec_function); // Add patched predicate function to new items @@ -883,7 +889,9 @@ fn extract_prusti_attributes_for_types( // tokens identical to the ones passed by the native procedural // macro call. let mut iter = attr.tokens.into_iter(); - let TokenTree::Group(group) = iter.next().unwrap() else { unreachable!() }; + let TokenTree::Group(group) = iter.next().unwrap() else { + unreachable!() + }; group.stream() } }; diff --git a/prusti-contracts/prusti-specs/src/parse_closure_macro.rs b/prusti-contracts/prusti-specs/src/parse_closure_macro.rs index 34d0a12d1b0..9d3fee07c42 100644 --- a/prusti-contracts/prusti-specs/src/parse_closure_macro.rs +++ b/prusti-contracts/prusti-specs/src/parse_closure_macro.rs @@ -16,16 +16,16 @@ impl Parse for ClosureWithSpec { // collect and remove any specification attributes // leave other attributes intact - attrs.drain_filter(|attr| { + attrs.retain(|attr| { if let Some(id) = attr.path.get_ident() { match id.to_string().as_ref() { "requires" => pres.push(syn::parse2(attr.tokens.clone())), "ensures" => posts.push(syn::parse2(attr.tokens.clone())), - _ => return false, + _ => return true, } - true - } else { false + } else { + true } }); cl.attrs = attrs; diff --git a/prusti-contracts/prusti-specs/src/specifications/preparser.rs b/prusti-contracts/prusti-specs/src/specifications/preparser.rs index 790e516fabc..6d64ad4eef9 100644 --- a/prusti-contracts/prusti-specs/src/specifications/preparser.rs +++ b/prusti-contracts/prusti-specs/src/specifications/preparser.rs @@ -221,8 +221,7 @@ impl PrustiTokenStream { PrustiToken::BinOp(span, PrustiBinaryOp::Rust(op)) => Ok(op.to_tokens(span)), _ => err(token.span(), "unexpected Prusti syntax"), }) - .collect::, _>>()? - .into_iter(), + .collect::, _>>()?, )) } diff --git a/prusti-contracts/prusti-std/Cargo.toml b/prusti-contracts/prusti-std/Cargo.toml index ab17a78b49c..ba0d0e43992 100644 --- a/prusti-contracts/prusti-std/Cargo.toml +++ b/prusti-contracts/prusti-std/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "prusti-std" -version = "0.1.9" +version = "0.1.10" authors = ["Prusti Devs "] edition = "2021" license = "MPL-2.0" @@ -12,7 +12,7 @@ keywords = ["prusti", "contracts", "verification", "formal", "specifications"] categories = ["development-tools", "development-tools::testing"] [dependencies] -prusti-contracts = { path = "../prusti-contracts", version = "0.1.9" } +prusti-contracts = { path = "../prusti-contracts", version = "0.1.10" } # Forward "prusti" flag [features] diff --git a/prusti-interface/src/environment/body.rs b/prusti-interface/src/environment/body.rs index 009ae794eaa..90c7229d2d3 100644 --- a/prusti-interface/src/environment/body.rs +++ b/prusti-interface/src/environment/body.rs @@ -2,11 +2,12 @@ use prusti_rustc_interface::{ macros::{TyDecodable, TyEncodable}, middle::{ mir, - ty::{self, subst::SubstsRef, TyCtxt}, + ty::{self, TyCtxt}, }, span::def_id::{DefId, LocalDefId}, }; use rustc_hash::FxHashMap; +use rustc_middle::ty::GenericArgsRef; use std::{cell::RefCell, collections::hash_map::Entry, rc::Rc}; use crate::environment::{borrowck::facts::BorrowckFacts, mir_storage}; @@ -80,7 +81,7 @@ impl<'tcx> PreLoadedBodies<'tcx> { /// - we are encoding an impure function, where the method is encoded only once /// and calls are performed indirectly via contract exhale/inhale; or /// - when the caller is unknown, e.g. to check a pure function definition. -type MonomorphKey<'tcx> = (DefId, SubstsRef<'tcx>, Option); +type MonomorphKey<'tcx> = (DefId, GenericArgsRef<'tcx>, Option); /// Store for all the `mir::Body` which we've taken out of the compiler /// or imported from external crates, all of which are indexed by DefId @@ -151,7 +152,7 @@ impl<'tcx> EnvBody<'tcx> { fn get_monomorphised( &self, def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, caller_def_id: Option, ) -> Option> { self.monomorphised_bodies @@ -162,7 +163,7 @@ impl<'tcx> EnvBody<'tcx> { fn set_monomorphised( &self, def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, caller_def_id: Option, body: MirBody<'tcx>, ) -> MirBody<'tcx> { @@ -179,7 +180,7 @@ impl<'tcx> EnvBody<'tcx> { ty::EarlyBinder::bind(body.0), ) } else { - ty::EarlyBinder::bind(body.0).subst(self.tcx, substs) + ty::EarlyBinder::bind(body.0).instantiate(self.tcx, substs) }; v.insert(MirBody(monomorphised)).clone() } else { @@ -201,7 +202,11 @@ impl<'tcx> EnvBody<'tcx> { /// with the given type substitutions. /// /// FIXME: This function is called only in pure contexts??? - pub fn get_impure_fn_body(&self, def_id: LocalDefId, substs: SubstsRef<'tcx>) -> MirBody<'tcx> { + pub fn get_impure_fn_body( + &self, + def_id: LocalDefId, + substs: GenericArgsRef<'tcx>, + ) -> MirBody<'tcx> { if let Some(body) = self.get_monomorphised(def_id.to_def_id(), substs, None) { return body; } @@ -231,7 +236,7 @@ impl<'tcx> EnvBody<'tcx> { pub fn get_closure_body( &self, def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, caller_def_id: DefId, ) -> MirBody<'tcx> { if let Some(body) = self.get_monomorphised(def_id, substs, Some(caller_def_id)) { @@ -246,7 +251,7 @@ impl<'tcx> EnvBody<'tcx> { pub fn get_pure_fn_body( &self, def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, caller_def_id: DefId, ) -> MirBody<'tcx> { if let Some(body) = self.get_monomorphised(def_id, substs, Some(caller_def_id)) { @@ -261,7 +266,7 @@ impl<'tcx> EnvBody<'tcx> { pub fn get_expression_body( &self, def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, caller_def_id: DefId, ) -> MirBody<'tcx> { if let Some(body) = self.get_monomorphised(def_id, substs, Some(caller_def_id)) { @@ -279,7 +284,7 @@ impl<'tcx> EnvBody<'tcx> { pub fn get_spec_body( &self, def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, caller_def_id: DefId, ) -> MirBody<'tcx> { if let Some(body) = self.get_monomorphised(def_id, substs, Some(caller_def_id)) { diff --git a/prusti-interface/src/environment/borrowck/facts.rs b/prusti-interface/src/environment/borrowck/facts.rs index 5e93a9d3be3..557c4a4fd7d 100644 --- a/prusti-interface/src/environment/borrowck/facts.rs +++ b/prusti-interface/src/environment/borrowck/facts.rs @@ -51,19 +51,18 @@ pub enum PointType { impl std::cmp::PartialOrd for PointType { fn partial_cmp(&self, other: &PointType) -> Option { - let res = match (self, other) { - (PointType::Start, PointType::Start) => std::cmp::Ordering::Equal, - (PointType::Start, PointType::Mid) => std::cmp::Ordering::Less, - (PointType::Mid, PointType::Start) => std::cmp::Ordering::Greater, - (PointType::Mid, PointType::Mid) => std::cmp::Ordering::Equal, - }; - Some(res) + Some(self.cmp(other)) } } impl std::cmp::Ord for PointType { fn cmp(&self, other: &PointType) -> std::cmp::Ordering { - self.partial_cmp(other).unwrap() + match (self, other) { + (PointType::Start, PointType::Start) => std::cmp::Ordering::Equal, + (PointType::Start, PointType::Mid) => std::cmp::Ordering::Less, + (PointType::Mid, PointType::Start) => std::cmp::Ordering::Greater, + (PointType::Mid, PointType::Mid) => std::cmp::Ordering::Equal, + } } } diff --git a/prusti-interface/src/environment/collect_prusti_spec_visitor.rs b/prusti-interface/src/environment/collect_prusti_spec_visitor.rs index fc581d2a170..8b52dbc51eb 100644 --- a/prusti-interface/src/environment/collect_prusti_spec_visitor.rs +++ b/prusti-interface/src/environment/collect_prusti_spec_visitor.rs @@ -73,10 +73,8 @@ impl<'tcx> Visitor<'tcx> for CollectPrustiSpecVisitor<'tcx> { ) { let def_id = self.env_query.as_local_def_id(item.hir_id()).to_def_id(); let adt_def = self.env_query.tcx().adt_def(def_id); - let ty = self - .env_query - .tcx() - .mk_adt(adt_def, self.env_query.identity_substs(def_id)); + let tcx = self.env_query.tcx(); + let ty = ty::Ty::new_adt(tcx, adt_def, self.env_query.identity_substs(def_id)); self.types.push(ty); } } diff --git a/prusti-interface/src/environment/mir_utils/split_aggregate_assignment.rs b/prusti-interface/src/environment/mir_utils/split_aggregate_assignment.rs index 5a4c8ef8050..723a5f9a737 100644 --- a/prusti-interface/src/environment/mir_utils/split_aggregate_assignment.rs +++ b/prusti-interface/src/environment/mir_utils/split_aggregate_assignment.rs @@ -50,7 +50,7 @@ impl<'tcx> SplitAggregateAssignment<'tcx> for mir::Statement<'tcx> { let items_ty = mir.local_decls[local].ty.tuple_items().unwrap(); operands .into_iter() - .zip(items_ty.into_iter()) + .zip(items_ty) .enumerate() .map(|(i, (rhs, ty))| { let field = FieldIdx::from_usize(i); @@ -63,7 +63,7 @@ impl<'tcx> SplitAggregateAssignment<'tcx> for mir::Statement<'tcx> { mir::Rvalue::Use(_) | mir::Rvalue::Ref(_, _, _) => vec![(lhs, rhs)], // slice creation is ok mir::Rvalue::Cast( - mir::CastKind::Pointer(ty::adjustment::PointerCast::Unsize), + mir::CastKind::PointerCoercion(ty::adjustment::PointerCoercion::Unsize), _, cast_ty, ) if cast_ty.is_slice_ref() => vec![(lhs, rhs)], diff --git a/prusti-interface/src/environment/mod.rs b/prusti-interface/src/environment/mod.rs index 368779a83b8..8d7bc98d374 100644 --- a/prusti-interface/src/environment/mod.rs +++ b/prusti-interface/src/environment/mod.rs @@ -7,6 +7,7 @@ //! This module defines the interface provided to a verifier. use prusti_rustc_interface::middle::ty::{self, TyCtxt}; +use rustc_middle::ty::GenericArgsRef; pub mod body; pub mod borrowck; @@ -45,7 +46,6 @@ use self::{ collect_prusti_spec_visitor::CollectPrustiSpecVisitor, }; use crate::data::ProcedureDefId; -use rustc_middle::ty::SubstsRef; /// Facade to the Rust compiler. pub struct Environment<'tcx> { @@ -139,7 +139,7 @@ impl<'tcx> Environment<'tcx> { &self, caller_def_id: ProcedureDefId, called_def_id: ProcedureDefId, - call_substs: SubstsRef<'tcx>, + call_substs: GenericArgsRef<'tcx>, ) -> bool { if called_def_id == caller_def_id { true diff --git a/prusti-interface/src/environment/polonius_info.rs b/prusti-interface/src/environment/polonius_info.rs index c5647f30728..85229132b90 100644 --- a/prusti-interface/src/environment/polonius_info.rs +++ b/prusti-interface/src/environment/polonius_info.rs @@ -587,7 +587,7 @@ fn get_borrowed_places<'a, 'tcx: 'a>( // slice creation involves an unsize pointer cast like &[i32; 3] -> &[i32] &mir::Rvalue::Cast( - mir::CastKind::Pointer(ty::adjustment::PointerCast::Unsize), + mir::CastKind::PointerCoercion(ty::adjustment::PointerCoercion::Unsize), ref operand, ref cast_ty, ) if cast_ty.is_slice_ref() => { diff --git a/prusti-interface/src/environment/procedure.rs b/prusti-interface/src/environment/procedure.rs index 41923263e09..ee81c1d93d9 100644 --- a/prusti-interface/src/environment/procedure.rs +++ b/prusti-interface/src/environment/procedure.rs @@ -247,7 +247,7 @@ pub fn get_loop_invariant<'tcx>( bb_data: &BasicBlockData<'tcx>, ) -> Option<( ProcedureDefId, - prusti_rustc_interface::middle::ty::subst::SubstsRef<'tcx>, + prusti_rustc_interface::middle::ty::GenericArgsRef<'tcx>, )> { for stmt in &bb_data.statements { if let StatementKind::Assign(box ( @@ -354,8 +354,8 @@ fn get_nonspec_basic_blocks( for (bb, _) in bb_graph.iter() { if is_marked_specification_block(env_query, &mir[*bb]) { spec_basic_blocks.insert(*bb); - spec_basic_blocks.extend(blocks_definitely_leading_to(&bb_graph, *bb).into_iter()); - spec_basic_blocks.extend(blocks_dominated_by(mir, *bb).into_iter()); + spec_basic_blocks.extend(blocks_definitely_leading_to(&bb_graph, *bb)); + spec_basic_blocks.extend(blocks_dominated_by(mir, *bb)); } } debug!("spec basic blocks: {spec_basic_blocks:#?}"); diff --git a/prusti-interface/src/environment/query.rs b/prusti-interface/src/environment/query.rs index 32370da15a0..61dc6126e6f 100644 --- a/prusti-interface/src/environment/query.rs +++ b/prusti-interface/src/environment/query.rs @@ -8,8 +8,7 @@ use prusti_rustc_interface::{ middle::{ hir::map::Map, ty::{ - self, subst::SubstsRef, Binder, BoundConstness, ImplPolarity, ParamEnv, TraitPredicate, - TyCtxt, + self, BoundConstness, GenericArgsRef, ImplPolarity, ParamEnv, TraitPredicate, TyCtxt, }, }, span::{ @@ -148,7 +147,7 @@ impl<'tcx> EnvQuery<'tcx> { pub fn is_unsafe_function(self, def_id: impl IntoParam) -> bool { self.tcx .fn_sig(def_id.into_param()) - .subst_identity() + .instantiate_identity() .unsafety() == prusti_rustc_interface::hir::Unsafety::Unsafe } @@ -157,7 +156,7 @@ impl<'tcx> EnvQuery<'tcx> { pub fn get_fn_sig( self, def_id: impl IntoParam, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> ty::PolyFnSig<'tcx> { let def_id = def_id.into_param(); let sig = if self.tcx.is_closure(def_id) { @@ -165,14 +164,14 @@ impl<'tcx> EnvQuery<'tcx> { } else { self.tcx.fn_sig(def_id) }; - sig.subst(self.tcx, substs) + sig.instantiate(self.tcx, substs) } /// Computes the signature of the function with subst applied and associated types resolved. pub fn get_fn_sig_resolved( self, def_id: impl IntoParam, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, caller_def_id: impl IntoParam, ) -> ty::PolyFnSig<'tcx> { let def_id = def_id.into_param(); @@ -206,8 +205,8 @@ impl<'tcx> EnvQuery<'tcx> { pub fn find_trait_method_substs( self, impl_method_def_id: impl IntoParam, // what are we calling? - impl_method_substs: SubstsRef<'tcx>, // what are the substs on the call? - ) -> Option<(ProcedureDefId, SubstsRef<'tcx>)> { + impl_method_substs: GenericArgsRef<'tcx>, // what are the substs on the call? + ) -> Option<(ProcedureDefId, GenericArgsRef<'tcx>)> { let impl_method_def_id = impl_method_def_id.into_param(); let impl_def_id = self.tcx.impl_of_method(impl_method_def_id)?; let trait_ref = self.tcx.impl_trait_ref(impl_def_id)?.skip_binder(); @@ -255,9 +254,9 @@ impl<'tcx> EnvQuery<'tcx> { // more precisely. We can do this directly with `impl_method_substs` // because they contain the substs for the `impl` block as a prefix. let call_trait_substs = - ty::EarlyBinder::bind(trait_ref.substs).subst(self.tcx, impl_method_substs); + ty::EarlyBinder::bind(trait_ref.args).instantiate(self.tcx, impl_method_substs); let impl_substs = self.identity_substs(impl_def_id); - let trait_method_substs = self.tcx.mk_substs_from_iter( + let trait_method_substs = self.tcx.mk_args_from_iter( call_trait_substs .iter() .chain(impl_method_substs.iter().skip(impl_substs.len())), @@ -276,7 +275,7 @@ impl<'tcx> EnvQuery<'tcx> { pub fn find_impl_of_trait_method_call( self, proc_def_id: impl IntoParam + Debug, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> Option { // TODO(tymap): remove this method? let proc_def_id = proc_def_id.into_param(); @@ -290,11 +289,11 @@ impl<'tcx> EnvQuery<'tcx> { ObligationCause::dummy(), // TODO(tymap): don't use reveal_all ParamEnv::reveal_all(), - Binder::dummy(TraitPredicate { + TraitPredicate { trait_ref, constness: BoundConstness::NotConst, polarity: ImplPolarity::Positive, - }), + }, ); let result = sc.select(&obligation); match result { @@ -328,8 +327,8 @@ impl<'tcx> EnvQuery<'tcx> { self, caller_def_id: impl IntoParam, // where are we calling from? called_def_id: impl IntoParam, // what are we calling? - call_substs: SubstsRef<'tcx>, - ) -> (ProcedureDefId, SubstsRef<'tcx>) { + call_substs: GenericArgsRef<'tcx>, + ) -> (ProcedureDefId, GenericArgsRef<'tcx>) { let called_def_id = called_def_id.into_param(); (|| { @@ -346,7 +345,7 @@ impl<'tcx> EnvQuery<'tcx> { // if no trait resolution occurred, we can keep the non-erased substs call_substs } else { - instance.substs + instance.args }; Some((resolved_def_id, resolved_substs)) @@ -415,7 +414,7 @@ impl<'tcx> EnvQuery<'tcx> { /// Return the default substitutions for a particular item, i.e. where each /// generic maps to itself. - pub fn identity_substs(self, def_id: impl IntoParam) -> SubstsRef<'tcx> { + pub fn identity_substs(self, def_id: impl IntoParam) -> GenericArgsRef<'tcx> { ty::List::identity_for_item(self.tcx, def_id.into_param()) } diff --git a/prusti-interface/src/prusti_error.rs b/prusti-interface/src/prusti_error.rs index bb0cc96f96c..308a991aeac 100644 --- a/prusti-interface/src/prusti_error.rs +++ b/prusti-interface/src/prusti_error.rs @@ -44,15 +44,13 @@ pub enum PrustiErrorKind { impl PartialOrd for PrustiError { fn partial_cmp(&self, other: &Self) -> Option { - self.span - .primary_span() - .partial_cmp(&other.span.primary_span()) + Some(self.cmp(other)) } } impl Ord for PrustiError { fn cmp(&self, other: &Self) -> std::cmp::Ordering { - self.partial_cmp(other).unwrap() + self.span.primary_span().cmp(&other.span.primary_span()) } } diff --git a/prusti-interface/src/specs/external.rs b/prusti-interface/src/specs/external.rs index dc42ed6aeaf..7568ed85692 100644 --- a/prusti-interface/src/specs/external.rs +++ b/prusti-interface/src/specs/external.rs @@ -12,7 +12,7 @@ use crate::{ environment::{EnvDiagnostic, EnvName, EnvQuery, Environment}, PrustiError, }; -use prusti_rustc_interface::{data_structures::fx::FxHashMap, middle::ty::subst::SubstsRef}; +use prusti_rustc_interface::{data_structures::fx::FxHashMap, middle::ty::GenericArgsRef}; use prusti_specs::ExternSpecKind; use std::cmp::{Eq, PartialEq}; @@ -60,7 +60,7 @@ impl ExternSpecDeclaration { /// Constructs [ExternSpecDeclaration] from a method call with the given substitutions. fn from_method_call<'tcx>( def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, env_query: EnvQuery<'tcx>, ) -> Self { let is_impl_method = env_query.is_trait_method_impl(def_id); @@ -295,7 +295,7 @@ impl<'tcx> ExternSpecResolver<'tcx> { /// accomplished by a nested match rather than a full visitor? struct ExternSpecVisitor<'tcx> { env_query: EnvQuery<'tcx>, - spec_found: Option<(DefId, SubstsRef<'tcx>, Span)>, + spec_found: Option<(DefId, GenericArgsRef<'tcx>, Span)>, } impl<'tcx> Visitor<'tcx> for ExternSpecVisitor<'tcx> { @@ -313,7 +313,7 @@ impl<'tcx> Visitor<'tcx> for ExternSpecVisitor<'tcx> { if let prusti_rustc_interface::hir::ExprKind::Call(callee_expr, _arguments) = ex.kind { if let prusti_rustc_interface::hir::ExprKind::Path(ref qself) = callee_expr.kind { let tyck_res = self.env_query.tcx().typeck(callee_expr.hir_id.owner.def_id); - let substs = tyck_res.node_substs(callee_expr.hir_id); + let substs = tyck_res.node_args(callee_expr.hir_id); let res = tyck_res.qpath_res(qself, callee_expr.hir_id); if let prusti_rustc_interface::hir::def::Res::Def(_, def_id) = res { self.spec_found = Some((def_id, substs, ex.span)); diff --git a/prusti-smt-solver/src/solver.rs b/prusti-smt-solver/src/solver.rs index c2fec55b980..b346a9f2bdf 100644 --- a/prusti-smt-solver/src/solver.rs +++ b/prusti-smt-solver/src/solver.rs @@ -1,3 +1,5 @@ +#![allow(clippy::needless_pass_by_ref_mut)] // see https://github.com/rust-lang/rust-clippy/issues/11179 + use crate::subprocess::{communicate, get_version, pass_error}; use async_std::process::{Command, Stdio}; use context::Context; diff --git a/prusti-viper/src/encoder/counterexamples/counterexample_translation.rs b/prusti-viper/src/encoder/counterexamples/counterexample_translation.rs index c211eecedd5..66fff62fcf0 100644 --- a/prusti-viper/src/encoder/counterexamples/counterexample_translation.rs +++ b/prusti-viper/src/encoder/counterexamples/counterexample_translation.rs @@ -419,7 +419,7 @@ impl<'ce, 'tcx> CounterexampleTranslator<'ce, 'tcx> { variant: &ty::VariantDef, sil_entry: Option<&ModelEntry>, vir_name: String, - subst: ty::subst::SubstsRef<'tcx>, + subst: ty::GenericArgsRef<'tcx>, silicon_ce_entries: &FxHashMap, ) -> Vec<(String, Entry)> { let mut field_entries = vec![]; @@ -716,7 +716,7 @@ impl<'ce, 'tcx> CounterexampleTranslator<'ce, 'tcx> { variant: &ty::VariantDef, snapshot_var: Option<&ModelEntry>, encoded_typ: String, - subst: ty::subst::SubstsRef<'tcx>, + subst: ty::GenericArgsRef<'tcx>, ) -> Vec<(String, Entry)> { match snapshot_var { Some(ModelEntry::DomainValue(domain, _)) => { diff --git a/prusti-viper/src/encoder/counterexamples/counterexample_translation_refactored.rs b/prusti-viper/src/encoder/counterexamples/counterexample_translation_refactored.rs index 994c89dd651..105d3a3a7b8 100644 --- a/prusti-viper/src/encoder/counterexamples/counterexample_translation_refactored.rs +++ b/prusti-viper/src/encoder/counterexamples/counterexample_translation_refactored.rs @@ -196,7 +196,7 @@ impl<'ce, 'tcx, 'v> CounterexampleTranslator<'ce, 'tcx, 'v> { .map(|fn_proc_id| { self.tcx .fn_sig(fn_proc_id) - .subst_identity() + .instantiate_identity() .skip_binder() .output() }); @@ -635,7 +635,7 @@ impl<'ce, 'tcx, 'v> CounterexampleTranslator<'ce, 'tcx, 'v> { &self, variant: &ty::VariantDef, model_entry: Option<&ModelEntry>, - subst: ty::subst::SubstsRef<'tcx>, + subst: ty::GenericArgsRef<'tcx>, model: bool, //if false, ignore models ) -> Vec<(String, Entry)> { match model_entry { @@ -725,7 +725,7 @@ impl<'ce, 'tcx, 'v> CounterexampleTranslator<'ce, 'tcx, 'v> { .get(&sil_to_model_fn_name) { let sil_model = sil_to_model_fn.get_function_value(&sil_ref_fn_param); - let model_typ = self.tcx.type_of(model_id).subst_identity(); + let model_typ = self.tcx.type_of(model_id).instantiate_identity(); let entry = self.translate_snapshot_entry(sil_model.as_ref(), Some(model_typ), false); return entry; diff --git a/prusti-viper/src/encoder/encoder.rs b/prusti-viper/src/encoder/encoder.rs index b63a3f95700..2628ab74609 100644 --- a/prusti-viper/src/encoder/encoder.rs +++ b/prusti-viper/src/encoder/encoder.rs @@ -325,7 +325,7 @@ impl<'v, 'tcx> Encoder<'v, 'tcx> { const_value.try_to_scalar() } ty::ConstKind::Unevaluated(ct) => { - let mir_ct = mir::UnevaluatedConst::new(ct.def, ct.substs); + let mir_ct = mir::UnevaluatedConst::new(ct.def, ct.args); self.uneval_eval_intlike(mir_ct) }, _ => error_unsupported!("unsupported const kind: {:?}", value), diff --git a/prusti-viper/src/encoder/foldunfold/mod.rs b/prusti-viper/src/encoder/foldunfold/mod.rs index e80b23f9ec3..ed33736504a 100644 --- a/prusti-viper/src/encoder/foldunfold/mod.rs +++ b/prusti-viper/src/encoder/foldunfold/mod.rs @@ -608,7 +608,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> vir::CfgReplacer, ActionVec> for FoldUnf .collect(); let mut perms = acc_permissions; - perms.extend(pred_permissions.into_iter()); + perms.extend(pred_permissions); trace!( "required permissions: {{\n{}\n}}", perms diff --git a/prusti-viper/src/encoder/foldunfold/state.rs b/prusti-viper/src/encoder/foldunfold/state.rs index 628005d5879..31450bc642a 100644 --- a/prusti-viper/src/encoder/foldunfold/state.rs +++ b/prusti-viper/src/encoder/foldunfold/state.rs @@ -172,7 +172,7 @@ impl State { where F: Fn(vir::Expr) -> vir::Expr, { - for coll in vec![&mut self.acc, &mut self.pred] { + for coll in [&mut self.acc, &mut self.pred] { let new_values = coll .clone() .into_iter() diff --git a/prusti-viper/src/encoder/high/generics/interface.rs b/prusti-viper/src/encoder/high/generics/interface.rs index 5adfaea6d3f..5a743eac272 100644 --- a/prusti-viper/src/encoder/high/generics/interface.rs +++ b/prusti-viper/src/encoder/high/generics/interface.rs @@ -2,7 +2,7 @@ use crate::encoder::{ errors::EncodingResult, high::lower::IntoPolymorphic, mir::generics::MirGenericsEncoderInterface, }; -use prusti_rustc_interface::{hir::def_id::DefId, middle::ty::subst::SubstsRef}; +use prusti_rustc_interface::{hir::def_id::DefId, middle::ty::GenericArgsRef}; use vir_crate::polymorphic as vir_poly; pub(crate) trait HighGenericsEncoderInterface<'tcx> { @@ -10,7 +10,7 @@ pub(crate) trait HighGenericsEncoderInterface<'tcx> { fn encode_generic_arguments( &self, def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> EncodingResult>; } @@ -22,7 +22,7 @@ impl<'v, 'tcx: 'v> HighGenericsEncoderInterface<'tcx> for super::super::super::E fn encode_generic_arguments( &self, def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> EncodingResult> { let type_arguments = self.encode_generic_arguments_high(def_id, substs)?; Ok(type_arguments.lower(self)) diff --git a/prusti-viper/src/encoder/high/procedures/inference/state/places.rs b/prusti-viper/src/encoder/high/procedures/inference/state/places.rs index a2a0c30e64f..d01d96c14b2 100644 --- a/prusti-viper/src/encoder/high/procedures/inference/state/places.rs +++ b/prusti-viper/src/encoder/high/procedures/inference/state/places.rs @@ -60,7 +60,7 @@ impl Places { F: 'a + FnMut(&vir_typed::Expression) -> bool, { self.places - .drain_filter(move |_, place| pred(place)) + .extract_if(move |_, place| pred(place)) .map(|(_, place)| place) } } diff --git a/prusti-viper/src/encoder/middle/core_proof/builtin_methods/interface.rs b/prusti-viper/src/encoder/middle/core_proof/builtin_methods/interface.rs index 30f6a32d4d0..9828f510e12 100644 --- a/prusti-viper/src/encoder/middle/core_proof/builtin_methods/interface.rs +++ b/prusti-viper/src/encoder/middle/core_proof/builtin_methods/interface.rs @@ -2050,7 +2050,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> BuiltinMethodsInterface for Lowerer<'p, 'v, 'tcx> { } _ => unimplemented!("{type_decl:?}"), } - if has_body {} + let method = builder.build(); self.declare_method(method)?; } diff --git a/prusti-viper/src/encoder/middle/core_proof/transformations/inline_functions.rs b/prusti-viper/src/encoder/middle/core_proof/transformations/inline_functions.rs index f7878f44769..c89e1fcd606 100644 --- a/prusti-viper/src/encoder/middle/core_proof/transformations/inline_functions.rs +++ b/prusti-viper/src/encoder/middle/core_proof/transformations/inline_functions.rs @@ -8,7 +8,7 @@ use vir_low::expression::visitors::ExpressionFolder; pub(crate) fn inline_caller_for(program: &mut vir_low::Program) { let caller_for_functions = program .functions - .drain_filter(|function| function.kind == vir_low::FunctionKind::CallerFor) + .extract_if(|function| function.kind == vir_low::FunctionKind::CallerFor) .map(|function| (function.name.clone(), function)) .collect(); for procedure in &mut program.procedures { diff --git a/prusti-viper/src/encoder/middle/core_proof/transformations/remove_predicates.rs b/prusti-viper/src/encoder/middle/core_proof/transformations/remove_predicates.rs index b53badeb770..ac13aa1ba7b 100644 --- a/prusti-viper/src/encoder/middle/core_proof/transformations/remove_predicates.rs +++ b/prusti-viper/src/encoder/middle/core_proof/transformations/remove_predicates.rs @@ -37,7 +37,7 @@ fn from_methods( removed_functions: &FxHashSet, ) -> FxHashSet { let removed_methods = methods - .drain_filter(|method| match method.kind { + .extract_if(|method| match method.kind { vir_low::MethodKind::LowMemoryOperation => true, vir_low::MethodKind::MirOperation | vir_low::MethodKind::Havoc => false, }) diff --git a/prusti-viper/src/encoder/mir/contracts/borrows.rs b/prusti-viper/src/encoder/mir/contracts/borrows.rs index fd045187a65..8bea77c393c 100644 --- a/prusti-viper/src/encoder/mir/contracts/borrows.rs +++ b/prusti-viper/src/encoder/mir/contracts/borrows.rs @@ -158,7 +158,7 @@ impl<'tcx> TypeVisitor<'tcx> for BorrowInfoCollectingVisitor<'tcx> { adt: ty::AdtDef<'tcx>, idx: prusti_rustc_interface::target::abi::VariantIdx, variant: &ty::VariantDef, - substs: ty::subst::SubstsRef<'tcx>, + substs: ty::GenericArgsRef<'tcx>, ) -> Result<(), Self::Error> { let old_path = self.current_path.take().unwrap(); self.current_path = Some(self.tcx.mk_place_downcast(old_path, adt, idx)); @@ -172,7 +172,7 @@ impl<'tcx> TypeVisitor<'tcx> for BorrowInfoCollectingVisitor<'tcx> { &mut self, index: usize, field: &ty::FieldDef, - substs: ty::subst::SubstsRef<'tcx>, + substs: ty::GenericArgsRef<'tcx>, ) -> Result<(), Self::Error> { let old_path = self.current_path.take().unwrap(); let ty = field.ty(self.tcx(), substs); diff --git a/prusti-viper/src/encoder/mir/contracts/contracts.rs b/prusti-viper/src/encoder/mir/contracts/contracts.rs index 55477369c19..58992cefe9b 100644 --- a/prusti-viper/src/encoder/mir/contracts/contracts.rs +++ b/prusti-viper/src/encoder/mir/contracts/contracts.rs @@ -6,7 +6,7 @@ use prusti_rustc_interface::{ def_id::{DefId, LocalDefId}, Mutability, }, - middle::{mir, ty::subst::SubstsRef}, + middle::{mir, ty::GenericArgsRef}, }; use rustc_hash::FxHashMap; use std::fmt; @@ -47,8 +47,8 @@ impl ProcedureContractGeneric { pub fn functional_precondition<'a, 'tcx>( &'a self, env: &'a Environment<'tcx>, - substs: SubstsRef<'tcx>, - ) -> Vec<(DefId, SubstsRef<'tcx>)> { + substs: GenericArgsRef<'tcx>, + ) -> Vec<(DefId, GenericArgsRef<'tcx>)> { match &self.specification.pres { typed::SpecificationItem::Empty => vec![], typed::SpecificationItem::Inherent(pres) @@ -80,8 +80,8 @@ impl ProcedureContractGeneric { pub fn functional_postcondition<'a, 'tcx>( &'a self, env: &'a Environment<'tcx>, - substs: SubstsRef<'tcx>, - ) -> Vec<(DefId, SubstsRef<'tcx>)> { + substs: GenericArgsRef<'tcx>, + ) -> Vec<(DefId, GenericArgsRef<'tcx>)> { match &self.specification.posts { typed::SpecificationItem::Empty => vec![], typed::SpecificationItem::Inherent(posts) @@ -108,8 +108,8 @@ impl ProcedureContractGeneric { pub fn functional_termination_measure<'a, 'tcx>( &'a self, env: &'a Environment<'tcx>, - substs: SubstsRef<'tcx>, - ) -> Option<(LocalDefId, SubstsRef<'tcx>)> { + substs: GenericArgsRef<'tcx>, + ) -> Option<(LocalDefId, GenericArgsRef<'tcx>)> { match self.specification.terminates { typed::SpecificationItem::Empty => None, typed::SpecificationItem::Inherent(t) | typed::SpecificationItem::Refined(_, t) => { diff --git a/prusti-viper/src/encoder/mir/contracts/interface.rs b/prusti-viper/src/encoder/mir/contracts/interface.rs index 2c5a42df99b..3d1437a5d90 100644 --- a/prusti-viper/src/encoder/mir/contracts/interface.rs +++ b/prusti-viper/src/encoder/mir/contracts/interface.rs @@ -14,7 +14,7 @@ use prusti_rustc_interface::{ hir::{def_id::DefId, Mutability}, middle::{ mir, ty, - ty::{subst::SubstsRef, FnSig}, + ty::{FnSig, GenericArgsRef}, }, }; use rustc_hash::FxHashMap; @@ -26,14 +26,14 @@ pub(crate) trait ContractsEncoderInterface<'tcx> { fn get_mir_procedure_contract_for_def( &self, proc_def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> EncodingResult>; fn get_mir_procedure_contract_for_call( &self, caller_def_id: DefId, called_def_id: DefId, - call_substs: SubstsRef<'tcx>, + call_substs: GenericArgsRef<'tcx>, ) -> EncodingResult>; /// Get a contract for a procedure's definition site, using the @@ -42,7 +42,7 @@ pub(crate) trait ContractsEncoderInterface<'tcx> { fn get_procedure_contract_for_def( &self, proc_def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> EncodingResult>; /// Get a contract for a call to a procedure, with particular argument and @@ -53,7 +53,7 @@ pub(crate) trait ContractsEncoderInterface<'tcx> { called_def_id: DefId, args: &[places::Local], target: places::Local, - call_substs: SubstsRef<'tcx>, + call_substs: GenericArgsRef<'tcx>, ) -> EncodingResult>; } @@ -66,7 +66,7 @@ impl<'v, 'tcx: 'v> ContractsEncoderInterface<'tcx> for super::super::super::Enco fn get_mir_procedure_contract_for_def( &self, proc_def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> EncodingResult> { self.contracts_encoder_state .encoded_contracts @@ -85,7 +85,7 @@ impl<'v, 'tcx: 'v> ContractsEncoderInterface<'tcx> for super::super::super::Enco &self, caller_def_id: DefId, called_def_id: DefId, - call_substs: SubstsRef<'tcx>, + call_substs: GenericArgsRef<'tcx>, ) -> EncodingResult> { let (called_def_id, call_substs) = self.env() @@ -102,7 +102,7 @@ impl<'v, 'tcx: 'v> ContractsEncoderInterface<'tcx> for super::super::super::Enco fn get_procedure_contract_for_def( &self, proc_def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> EncodingResult> { self.get_mir_procedure_contract_for_def(proc_def_id, substs) .as_ref() @@ -117,7 +117,7 @@ impl<'v, 'tcx: 'v> ContractsEncoderInterface<'tcx> for super::super::super::Enco called_def_id: DefId, args: &[places::Local], target: places::Local, - call_substs: SubstsRef<'tcx>, + call_substs: GenericArgsRef<'tcx>, ) -> EncodingResult> { let (called_def_id, call_substs) = self.env() @@ -136,7 +136,7 @@ fn get_procedure_contract<'p, 'v: 'p, 'tcx: 'v>( encoder: &'p Encoder<'v, 'tcx>, specification: typed::ProcedureSpecification, proc_def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> EncodingResult> { let env = encoder.env(); let args_ty: Vec<(mir::Local, ty::Ty<'tcx>)>; diff --git a/prusti-viper/src/encoder/mir/generics/interface.rs b/prusti-viper/src/encoder/mir/generics/interface.rs index c8006f40014..85d3c35c1ba 100644 --- a/prusti-viper/src/encoder/mir/generics/interface.rs +++ b/prusti-viper/src/encoder/mir/generics/interface.rs @@ -2,7 +2,7 @@ use crate::encoder::{errors::EncodingResult, mir::types::MirTypeEncoderInterface use prusti_rustc_interface::{ hir::def_id::DefId, - middle::ty::{self, subst::SubstsRef}, + middle::ty::{self, GenericArgsRef}, span::symbol::Symbol, }; use vir_crate::high::{self as vir_high}; @@ -20,7 +20,7 @@ pub(crate) trait MirGenericsEncoderInterface<'tcx> { fn encode_generic_arguments_high( &self, def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> EncodingResult>; fn encode_param(&self, name: Symbol, index: u32) -> vir_high::ty::TypeVar; } @@ -46,14 +46,14 @@ impl<'v, 'tcx: 'v> MirGenericsEncoderInterface<'tcx> for super::super::super::En fn encode_generic_arguments_high( &self, def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> EncodingResult> { assert_eq!(substs.len(), self.env().query.identity_substs(def_id).len()); Ok(substs .iter() // TODO(tymap): ignoring const params and lifetimes for now .filter_map(|generic| match generic.unpack() { - ty::subst::GenericArgKind::Type(ty) => Some(ty), + ty::GenericArgKind::Type(ty) => Some(ty), _ => None, }) .map(|ty| self.encode_type_high(ty)) diff --git a/prusti-viper/src/encoder/mir/procedures/encoder/builtin_function_encoder.rs b/prusti-viper/src/encoder/mir/procedures/encoder/builtin_function_encoder.rs index 998c7f9aa1d..858df2aa8dd 100644 --- a/prusti-viper/src/encoder/mir/procedures/encoder/builtin_function_encoder.rs +++ b/prusti-viper/src/encoder/mir/procedures/encoder/builtin_function_encoder.rs @@ -8,7 +8,7 @@ pub(super) trait BuiltinFuncAppEncoder<'p, 'v, 'tcx> { location: mir::Location, span: Span, called_def_id: DefId, - call_substs: SubstsRef<'tcx>, + call_substs: GenericArgsRef<'tcx>, args: &[mir::Operand<'tcx>], destination: mir::Place<'tcx>, target: &Option, @@ -24,7 +24,7 @@ impl<'p, 'v, 'tcx> BuiltinFuncAppEncoder<'p, 'v, 'tcx> for super::ProcedureEncod location: mir::Location, span: Span, called_def_id: DefId, - call_substs: SubstsRef<'tcx>, + call_substs: GenericArgsRef<'tcx>, args: &[mir::Operand<'tcx>], destination: mir::Place<'tcx>, target: &Option, diff --git a/prusti-viper/src/encoder/mir/procedures/encoder/elaborate_drops/mir_dataflow.rs b/prusti-viper/src/encoder/mir/procedures/encoder/elaborate_drops/mir_dataflow.rs index 025d2ca4682..62f98a01fd8 100644 --- a/prusti-viper/src/encoder/mir/procedures/encoder/elaborate_drops/mir_dataflow.rs +++ b/prusti-viper/src/encoder/mir/procedures/encoder/elaborate_drops/mir_dataflow.rs @@ -22,7 +22,7 @@ use prusti_rustc_interface::{ middle::{ mir::*, traits::Reveal, - ty::{self, subst::SubstsRef, util::IntTypeExt, Ty, TyCtxt}, + ty::{self, util::IntTypeExt, GenericArgsRef, Ty, TyCtxt}, }, }; use std::{fmt, iter}; @@ -238,7 +238,7 @@ where base_place: Place<'tcx>, variant_path: D::Path, variant: &'tcx ty::VariantDef, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> Vec<(Place<'tcx>, Option)> { variant .fields @@ -398,37 +398,11 @@ where } #[instrument(level = "debug", ret)] - fn open_drop_for_box(&mut self, adt: ty::AdtDef<'tcx>, substs: SubstsRef<'tcx>) -> BasicBlock { - // drop glue is sent straight to codegen - // box cannot be directly dereferenced - let unique_ty = adt.non_enum_variant().fields[FieldIdx::new(0)].ty(self.tcx(), substs); - let unique_variant = unique_ty.ty_adt_def().unwrap().non_enum_variant(); - let nonnull_ty = unique_variant.fields[FieldIdx::from_u32(0)].ty(self.tcx(), substs); - let ptr_ty = self.tcx().mk_imm_ptr(substs[0].expect_ty()); - - let unique_place = self - .tcx() - .mk_place_field(self.place, FieldIdx::new(0), unique_ty); - let nonnull_place = self - .tcx() - .mk_place_field(unique_place, FieldIdx::new(0), nonnull_ty); - let ptr_place = self - .tcx() - .mk_place_field(nonnull_place, FieldIdx::new(0), ptr_ty); - let interior = self.tcx().mk_place_deref(ptr_place); - - let interior_path = self.elaborator.deref_subpath(self.path); - - let succ = self.box_free_block(adt, substs, self.succ, self.unwind); - let unwind_succ = self - .unwind - .map(|unwind| self.box_free_block(adt, substs, unwind, Unwind::InCleanup)); - - self.drop_subpath(interior, interior_path, succ, unwind_succ) - } - - #[instrument(level = "debug", ret)] - fn open_drop_for_adt(&mut self, adt: ty::AdtDef<'tcx>, substs: SubstsRef<'tcx>) -> BasicBlock { + fn open_drop_for_adt( + &mut self, + adt: ty::AdtDef<'tcx>, + substs: GenericArgsRef<'tcx>, + ) -> BasicBlock { if adt.variants().is_empty() { return self.elaborator.patch().new_block(BasicBlockData { statements: vec![], @@ -458,7 +432,7 @@ where fn open_drop_for_adt_contents( &mut self, adt: ty::AdtDef<'tcx>, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> (BasicBlock, Unwind) { let (succ, unwind) = self.drop_ladder_bottom(); if !adt.is_enum() { @@ -477,7 +451,7 @@ where fn open_drop_for_multivariant( &mut self, adt: ty::AdtDef<'tcx>, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, succ: BasicBlock, unwind: Unwind, ) -> (BasicBlock, Unwind) { @@ -621,7 +595,8 @@ where let drop_fn = tcx.associated_item_def_ids(drop_trait)[0]; let ty = self.place_ty(self.place); - let ref_ty = tcx.mk_ref( + let ref_ty = Ty::new_ref( + tcx, tcx.lifetimes.re_erased, ty::TypeAndMut { ty, @@ -629,7 +604,7 @@ where }, ); let ref_place = self.new_temp(ref_ty); - let unit_temp = Place::from(self.new_temp(tcx.mk_unit())); + let unit_temp = Place::from(self.new_temp(Ty::new_unit(tcx))); let result = BasicBlockData { statements: vec![self.assign( @@ -637,7 +612,7 @@ where Rvalue::Ref( tcx.lifetimes.re_erased, BorrowKind::Mut { - allow_two_phase_borrow: false, + kind: MutBorrowKind::Default, }, self.place, ), @@ -654,14 +629,24 @@ where destination: unit_temp, target: Some(succ), unwind: unwind.into_action(), - from_hir_call: true, + call_source: CallSource::Misc, fn_span: self.source_info.span, }, source_info: self.source_info, }), is_cleanup: unwind.is_cleanup(), }; - self.elaborator.patch().new_block(result) + + let destructor_block = self.elaborator.patch().new_block(result); + + let block_start = Location { + block: destructor_block, + statement_index: 0, + }; + self.elaborator + .clear_drop_flag(block_start, self.path, DropFlagMode::Shallow); + + self.drop_flag_test_block(destructor_block, succ, unwind) } /// Create a loop that drops an array: @@ -687,10 +672,13 @@ where let move_ = Operand::Move; let tcx = self.tcx(); - let ptr_ty = tcx.mk_ptr(ty::TypeAndMut { - ty: ety, - mutbl: hir::Mutability::Mut, - }); + let ptr_ty = Ty::new_ptr( + tcx, + ty::TypeAndMut { + ty: ety, + mutbl: hir::Mutability::Mut, + }, + ); let ptr = Place::from(self.new_temp(ptr_ty)); let can_go = Place::from(self.new_temp(tcx.types.bool)); let one = self.constant_usize(1); @@ -854,8 +842,8 @@ where fn open_drop(&mut self) -> BasicBlock { let ty = self.place_ty(self.place); match ty.kind() { - ty::Closure(_, substs) => { - let tys: Vec<_> = substs.as_closure().upvar_tys().collect(); + ty::Closure(_, args) => { + let tys: Vec<_> = args.as_closure().upvar_tys().collect(); self.open_drop_for_tuple(&tys) } // Note that `elaborate_drops` only drops the upvars of a generator, @@ -864,18 +852,12 @@ where // This should only happen for the self argument on the resume function. // It effectively only contains upvars until the generator transformation runs. // See librustc_body/transform/generator.rs for more details. - ty::Generator(_, substs, _) => { - let tys: Vec<_> = substs.as_generator().upvar_tys().collect(); + ty::Generator(_, args, _) => { + let tys: Vec<_> = args.as_generator().upvar_tys().collect(); self.open_drop_for_tuple(&tys) } ty::Tuple(fields) => self.open_drop_for_tuple(fields), - ty::Adt(def, substs) => { - if def.is_box() { - self.open_drop_for_box(*def, substs) - } else { - self.open_drop_for_adt(*def, substs) - } - } + ty::Adt(def, args) => self.open_drop_for_adt(*def, args), ty::Dynamic(..) => self.complete_drop(self.succ, self.unwind), ty::Array(ety, size) => { let size = size.try_eval_target_usize(self.tcx(), self.elaborator.param_env()); @@ -883,7 +865,7 @@ where } ty::Slice(ety) => self.drop_loop_pair(*ety), - _ => unreachable!("open drop from non-ADT `{:?}`", ty), + _ => panic!("open drop from non-ADT `{:?}`", ty), } } @@ -927,69 +909,6 @@ where blk } - /// Creates a block that frees the backing memory of a `Box` if its drop is required (either - /// statically or by checking its drop flag). - /// - /// The contained value will not be dropped. - fn box_free_block( - &mut self, - adt: ty::AdtDef<'tcx>, - substs: SubstsRef<'tcx>, - target: BasicBlock, - unwind: Unwind, - ) -> BasicBlock { - let block = self.unelaborated_free_block(adt, substs, target, unwind); - self.drop_flag_test_block(block, target, unwind) - } - - /// Creates a block that frees the backing memory of a `Box` (without dropping the contained - /// value). - fn unelaborated_free_block( - &mut self, - adt: ty::AdtDef<'tcx>, - substs: SubstsRef<'tcx>, - target: BasicBlock, - unwind: Unwind, - ) -> BasicBlock { - let tcx = self.tcx(); - let unit_temp = Place::from(self.new_temp(tcx.mk_unit())); - let free_func = tcx.require_lang_item(LangItem::BoxFree, Some(self.source_info.span)); - let args = adt - .variant(FIRST_VARIANT) - .fields - .iter() - .enumerate() - .map(|(i, f)| { - let field = FieldIdx::new(i); - let field_ty = f.ty(tcx, substs); - Operand::Move(tcx.mk_place_field(self.place, field, field_ty)) - }) - .collect(); - - let call = TerminatorKind::Call { - func: Operand::function_handle(tcx, free_func, substs, self.source_info.span), - args, - destination: unit_temp, - target: Some(target), - unwind: if unwind.is_cleanup() { - UnwindAction::Terminate - } else { - UnwindAction::Continue - }, - from_hir_call: false, - fn_span: self.source_info.span, - }; // FIXME(#43234) - let free_block = self.new_block(unwind, call); - - let block_start = Location { - block: free_block, - statement_index: 0, - }; - self.elaborator - .clear_drop_flag(block_start, self.path, DropFlagMode::Shallow); - free_block - } - fn drop_block(&mut self, target: BasicBlock, unwind: Unwind) -> BasicBlock { let block = TerminatorKind::Drop { place: self.place, diff --git a/prusti-viper/src/encoder/mir/procedures/encoder/elaborate_drops/mir_transform.rs b/prusti-viper/src/encoder/mir/procedures/encoder/elaborate_drops/mir_transform.rs index 35f81bf40a7..f5d8fef6a4b 100644 --- a/prusti-viper/src/encoder/mir/procedures/encoder/elaborate_drops/mir_transform.rs +++ b/prusti-viper/src/encoder/mir/procedures/encoder/elaborate_drops/mir_transform.rs @@ -19,9 +19,8 @@ use prusti_rustc_interface::{ elaborate_drops::{DropFlagMode, DropFlagState, DropStyle, Unwind}, impls::{MaybeInitializedPlaces, MaybeUninitializedPlaces}, move_paths::{LookupResult, MoveData, MovePathIndex}, - on_all_children_bits, on_all_drop_children_bits, on_lookup_result_bits, - un_derefer::UnDerefer, - Analysis, MoveDataParamEnv, ResultsCursor, + on_all_children_bits, on_all_drop_children_bits, on_lookup_result_bits, Analysis, + MoveDataParamEnv, ResultsCursor, }, index::{bit_set::BitSet, IndexVec}, middle::{ @@ -66,26 +65,22 @@ pub(in super::super) fn run_pass<'tcx>(tcx: TyCtxt<'tcx>, body: &mut Body<'tcx>) let def_id = body.source.def_id(); let param_env = tcx.param_env_reveal_all_normalized(def_id); - let (side_table, move_data) = match MoveData::gather_moves(body, tcx, param_env) { + let move_data = match MoveData::gather_moves(body, tcx, param_env) { Ok(move_data) => move_data, Err((move_data, _)) => { tcx.sess.delay_span_bug( body.span, "No `move_errors` should be allowed in MIR borrowck", ); - (Default::default(), move_data) + move_data } }; - let un_derefer = UnDerefer { - tcx, - derefer_sidetable: side_table, - }; let elaborate_patch = { let env = MoveDataParamEnv { move_data, param_env, }; - remove_dead_unwinds(tcx, body, &env, &un_derefer); + remove_dead_unwinds(tcx, body, &env); let inits = MaybeInitializedPlaces::new(tcx, body, &env) .into_engine(tcx, body) @@ -110,7 +105,6 @@ pub(in super::super) fn run_pass<'tcx>(tcx: TyCtxt<'tcx>, body: &mut Body<'tcx>) init_data: InitializationData { inits, uninits }, drop_flags, patch: MirPatch::new(body), - un_derefer, reachable, } .elaborate() @@ -124,7 +118,6 @@ pub(in super::super) fn remove_dead_unwinds<'tcx>( tcx: TyCtxt<'tcx>, body: &mut Body<'tcx>, env: &MoveDataParamEnv<'tcx>, - und: &UnDerefer<'tcx>, ) { debug!("remove_dead_unwinds({:?})", body.span); // We only need to do this pass once, because unwind edges can only @@ -138,10 +131,10 @@ pub(in super::super) fn remove_dead_unwinds<'tcx>( for (bb, bb_data) in body.basic_blocks.iter_enumerated() { let place = match bb_data.terminator().kind { TerminatorKind::Drop { - ref place, + place, unwind: UnwindAction::Cleanup(_), .. - } => und.derefer(place.as_ref(), body).unwrap_or(*place), + } => place, _ => continue, }; @@ -335,7 +328,6 @@ struct ElaborateDropsCtxt<'a, 'tcx> { init_data: InitializationData<'a, 'tcx>, drop_flags: IndexVec>, patch: MirPatch<'tcx>, - un_derefer: UnDerefer<'tcx>, reachable: BitSet, } @@ -381,10 +373,7 @@ impl<'b, 'tcx> ElaborateDropsCtxt<'b, 'tcx> { } let terminator = data.terminator(); let place = match terminator.kind { - TerminatorKind::Drop { ref place, .. } => self - .un_derefer - .derefer(place.as_ref(), self.body) - .unwrap_or(*place), + TerminatorKind::Drop { ref place, .. } => place, _ => continue, }; @@ -448,15 +437,11 @@ impl<'b, 'tcx> ElaborateDropsCtxt<'b, 'tcx> { match terminator.kind { TerminatorKind::Drop { - mut place, + place, target, unwind, replace, } => { - if let Some(new_place) = self.un_derefer.derefer(place.as_ref(), self.body) { - place = new_place; - } - self.init_data.seek_before(loc); match self.move_data().rev_lookup.find(place.as_ref()) { LookupResult::Exact(path) => { diff --git a/prusti-viper/src/encoder/mir/procedures/encoder/initialisation.rs b/prusti-viper/src/encoder/mir/procedures/encoder/initialisation.rs index fc6ab05ee65..351a190f746 100644 --- a/prusti-viper/src/encoder/mir/procedures/encoder/initialisation.rs +++ b/prusti-viper/src/encoder/mir/procedures/encoder/initialisation.rs @@ -2,7 +2,6 @@ use prusti_rustc_interface::{ dataflow::{ impls::{MaybeInitializedPlaces, MaybeUninitializedPlaces}, move_paths::MoveData, - un_derefer::UnDerefer, Analysis, MoveDataParamEnv, ResultsCursor, }, middle::{mir, ty::TyCtxt}, @@ -18,9 +17,8 @@ impl<'mir, 'tcx> InitializationData<'mir, 'tcx> { tcx: TyCtxt<'tcx>, body: &'mir mut mir::Body<'tcx>, env: &'mir MoveDataParamEnv<'tcx>, - un_derefer: &'mir UnDerefer<'tcx>, ) -> Self { - super::elaborate_drops::mir_transform::remove_dead_unwinds(tcx, body, env, un_derefer); + super::elaborate_drops::mir_transform::remove_dead_unwinds(tcx, body, env); let inits = MaybeInitializedPlaces::new(tcx, body, env) .into_engine(tcx, body) @@ -46,26 +44,22 @@ impl<'mir, 'tcx> InitializationData<'mir, 'tcx> { pub(super) fn create_move_data_param_env_and_un_derefer<'tcx>( tcx: TyCtxt<'tcx>, body: &mir::Body<'tcx>, -) -> (MoveDataParamEnv<'tcx>, UnDerefer<'tcx>) { +) -> MoveDataParamEnv<'tcx> { let def_id = body.source.def_id(); let param_env = tcx.param_env_reveal_all_normalized(def_id); - let (side_table, move_data) = match MoveData::gather_moves(body, tcx, param_env) { + let move_data = match MoveData::gather_moves(body, tcx, param_env) { Ok(move_data) => move_data, Err((move_data, _)) => { tcx.sess.delay_span_bug( body.span, "No `move_errors` should be allowed in MIR borrowck", ); - (Default::default(), move_data) + move_data } }; - let un_derefer = UnDerefer { - tcx, - derefer_sidetable: side_table, - }; - let env = MoveDataParamEnv { + + MoveDataParamEnv { move_data, param_env, - }; - (env, un_derefer) + } } diff --git a/prusti-viper/src/encoder/mir/procedures/encoder/mod.rs b/prusti-viper/src/encoder/mir/procedures/encoder/mod.rs index 7e0dced682b..7311ba860ac 100644 --- a/prusti-viper/src/encoder/mir/procedures/encoder/mod.rs +++ b/prusti-viper/src/encoder/mir/procedures/encoder/mod.rs @@ -38,7 +38,7 @@ use prusti_rustc_interface::{ data_structures::graph::WithStartNode, hir::def_id::DefId, index::IndexSlice, - middle::{mir, ty, ty::subst::SubstsRef}, + middle::{mir, ty, ty::GenericArgsRef}, span::Span, }; use rustc_hash::FxHashSet; @@ -77,11 +77,10 @@ pub(super) fn encode_procedure<'v, 'tcx: 'v>( let tcx = encoder.env().tcx(); let (mir, lifetimes) = self::elaborate_drops::elaborate_drops(encoder, def_id, &procedure)?; let mir = &mir; // Mark body as immutable. - let (env, un_derefer) = - self::initialisation::create_move_data_param_env_and_un_derefer(tcx, mir); + let env = self::initialisation::create_move_data_param_env_and_un_derefer(tcx, mir); // TODO: the clone is required so that we can remove dead unwinds let mut no_dead_unwinds = mir.clone(); - let init_data = InitializationData::new(tcx, &mut no_dead_unwinds, &env, &un_derefer); + let init_data = InitializationData::new(tcx, &mut no_dead_unwinds, &env); let locals_without_explicit_allocation: BTreeSet<_> = mir.vars_and_temps_iter().collect(); let specification_blocks = SpecificationBlocks::build(encoder.env().query, mir, &procedure, true); @@ -319,7 +318,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { fn encode_precondition_expressions( &mut self, procedure_contract: &ProcedureContractMirDef<'tcx>, - call_substs: SubstsRef<'tcx>, + call_substs: GenericArgsRef<'tcx>, arguments: &[vir_high::Expression], ) -> SpannedEncodingResult> { let mut preconditions = Vec::new(); @@ -342,7 +341,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { fn encode_postcondition_expressions( &mut self, procedure_contract: &ProcedureContractMirDef<'tcx>, - call_substs: SubstsRef<'tcx>, + call_substs: GenericArgsRef<'tcx>, arguments: Vec, result: &vir_high::Expression, precondition_label: &str, @@ -1232,7 +1231,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { target, unwind, fn_span, - from_hir_call: _, + call_source: _, } => { self.encode_terminator_call( block_builder, @@ -1486,7 +1485,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { location: mir::Location, span: Span, called_def_id: DefId, - call_substs: SubstsRef<'tcx>, + call_substs: GenericArgsRef<'tcx>, args: &[mir::Operand<'tcx>], destination: mir::Place<'tcx>, target: &Option, @@ -2093,7 +2092,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { target: _, unwind: _, fn_span: _, - from_hir_call: _, + call_source: _, } => { if let ty::TyKind::FnDef(def_id, _substs) = literal.ty().kind() { let full_called_function_name = diff --git a/prusti-viper/src/encoder/mir/procedures/encoder/termination.rs b/prusti-viper/src/encoder/mir/procedures/encoder/termination.rs index 06376864ac8..7c335915291 100644 --- a/prusti-viper/src/encoder/mir/procedures/encoder/termination.rs +++ b/prusti-viper/src/encoder/mir/procedures/encoder/termination.rs @@ -8,7 +8,7 @@ use crate::encoder::{ }, }; use prusti_rustc_interface::{ - middle::{mir::BasicBlock, ty::subst::SubstsRef}, + middle::{mir::BasicBlock, ty::GenericArgsRef}, span::Span, }; use vir_crate::{ @@ -34,7 +34,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> super::ProcedureEncoder<'p, 'v, 'tcx> { &mut self, procedure_contract: &ProcedureContractMirDef<'tcx>, span: Span, - call_substs: SubstsRef<'tcx>, + call_substs: GenericArgsRef<'tcx>, arguments: &[vir_high::Expression], ) -> SpannedEncodingResult { assert!(self.encoder.terminates(self.def_id, None)); @@ -115,7 +115,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> super::ProcedureEncoder<'p, 'v, 'tcx> { block_builder: &mut BasicBlockBuilder, span: Span, procedure_contract: &ProcedureContractMirDef<'tcx>, - call_substs: SubstsRef<'tcx>, + call_substs: GenericArgsRef<'tcx>, arguments: &[vir_high::Expression], ) -> SpannedEncodingResult<()> { let called_fun = procedure_contract.def_id; diff --git a/prusti-viper/src/encoder/mir/pure/interpreter/interpreter_high.rs b/prusti-viper/src/encoder/mir/pure/interpreter/interpreter_high.rs index afa6f24bbd9..02ab43c1143 100644 --- a/prusti-viper/src/encoder/mir/pure/interpreter/interpreter_high.rs +++ b/prusti-viper/src/encoder/mir/pure/interpreter/interpreter_high.rs @@ -34,7 +34,7 @@ use prusti_rustc_interface::{ abi::FieldIdx, hir::def_id::DefId, index::IndexSlice, - middle::{mir, ty, ty::subst::SubstsRef}, + middle::{mir, ty, ty::GenericArgsRef}, span::Span, }; use rustc_hash::FxHashMap; @@ -58,7 +58,7 @@ pub(in super::super) struct ExpressionBackwardInterpreter<'p, 'v: 'p, 'tcx: 'v> pure_encoding_context: PureEncodingContext, /// DefId of the caller. Used for error reporting. caller_def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, } /// This encoding works backward, so there is the risk of generating expressions whose length @@ -73,7 +73,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ExpressionBackwardInterpreter<'p, 'v, 'tcx> { def_id: DefId, pure_encoding_context: PureEncodingContext, caller_def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> Self { Self { encoder, @@ -249,10 +249,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ExpressionBackwardInterpreter<'p, 'v, 'tcx> { state.substitute_value(&encoded_lhs, expr); } &mir::Rvalue::Ref(_, kind, place) => { - if !matches!( - kind, - mir::BorrowKind::Unique | mir::BorrowKind::Mut { .. } | mir::BorrowKind::Shared - ) { + if !matches!(kind, mir::BorrowKind::Mut { .. } | mir::BorrowKind::Shared) { return Err(SpannedEncodingError::unsupported( format!("unsupported kind of reference: {kind:?}"), span, @@ -287,7 +284,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ExpressionBackwardInterpreter<'p, 'v, 'tcx> { state.substitute_value(&encoded_lhs, encoded_rhs); } mir::Rvalue::Cast( - mir::CastKind::Pointer(ty::adjustment::PointerCast::Unsize), + mir::CastKind::PointerCoercion(ty::adjustment::PointerCoercion::Unsize), operand, cast_ty, ) => { @@ -447,8 +444,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ExpressionBackwardInterpreter<'p, 'v, 'tcx> { // compose substitutions // TODO(tymap): do we need this? - let substs = - ty::EarlyBinder::bind(*call_substs).subst(self.encoder.env().tcx(), self.substs); + let substs = ty::EarlyBinder::bind(*call_substs) + .instantiate(self.encoder.env().tcx(), self.substs); let state = if let Some(target_block) = target { let encoded_lhs = self.encode_place(destination).with_span(span)?; @@ -537,7 +534,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ExpressionBackwardInterpreter<'p, 'v, 'tcx> { args: &[prusti_rustc_interface::middle::mir::Operand<'tcx>], encoded_args: &[vir_high::Expression], span: Span, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult> { let lifetimes = self.encoder.get_lifetimes_from_substs(substs)?; use vir_high::{expression::BuiltinFunc::*, ty::*}; @@ -807,7 +804,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ExpressionBackwardInterpreter<'p, 'v, 'tcx> { def_id: DefId, args: Vec, span: Span, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult { let (function_name, return_type) = self .encoder diff --git a/prusti-viper/src/encoder/mir/pure/interpreter/interpreter_poly.rs b/prusti-viper/src/encoder/mir/pure/interpreter/interpreter_poly.rs index b63d3400dda..ca25e6a4c57 100644 --- a/prusti-viper/src/encoder/mir/pure/interpreter/interpreter_poly.rs +++ b/prusti-viper/src/encoder/mir/pure/interpreter/interpreter_poly.rs @@ -1160,8 +1160,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> BackwardMirInterpreter<'tcx> } } - &mir::Rvalue::Ref(_, mir::BorrowKind::Unique, place) - | &mir::Rvalue::Ref(_, mir::BorrowKind::Mut { .. }, place) + &mir::Rvalue::Ref(_, mir::BorrowKind::Mut { .. }, place) | &mir::Rvalue::Ref(_, mir::BorrowKind::Shared, place) => { let (encoded_place, _, _) = self.encode_place(place).with_span(span)?; // TODO: Instead of generating an `AddrOf(..)` expression, here we could @@ -1211,7 +1210,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> BackwardMirInterpreter<'tcx> } } - mir::Rvalue::Cast(mir::CastKind::Pointer(ty::adjustment::PointerCast::Unsize), ref operand, lhs_ref_ty) => { + mir::Rvalue::Cast(mir::CastKind::PointerCoercion(ty::adjustment::PointerCoercion::Unsize), ref operand, lhs_ref_ty) => { let rhs_ref_ty = self.mir_encoder.get_operand_ty(operand); if lhs_ref_ty.is_slice_ref() && rhs_ref_ty.is_array_ref() { let lhs_ty = lhs_ref_ty.peel_refs(); diff --git a/prusti-viper/src/encoder/mir/pure/pure_functions/encoder_high.rs b/prusti-viper/src/encoder/mir/pure/pure_functions/encoder_high.rs index 44060d88e92..adff5e1ee10 100644 --- a/prusti-viper/src/encoder/mir/pure/pure_functions/encoder_high.rs +++ b/prusti-viper/src/encoder/mir/pure/pure_functions/encoder_high.rs @@ -20,7 +20,7 @@ use log::debug; use prusti_common::vir_high_local; use prusti_rustc_interface::{ hir::def_id::DefId, - middle::{mir, ty, ty::subst::SubstsRef}, + middle::{mir, ty, ty::GenericArgsRef}, span::Span, }; use vir_crate::{ @@ -32,7 +32,7 @@ pub(super) fn encode_function_decl<'p, 'v: 'p, 'tcx: 'v>( encoder: &'p Encoder<'v, 'tcx>, proc_def_id: DefId, parent_def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult { let pure_encoder = PureEncoder::new( encoder, @@ -86,7 +86,7 @@ pub(super) fn encode_pure_expression<'p, 'v: 'p, 'tcx: 'v>( proc_def_id: DefId, pure_encoding_context: PureEncodingContext, parent_def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult { let mir = encoder .env() @@ -125,7 +125,7 @@ pub(super) fn encode_function_call_info<'p, 'v: 'p, 'tcx: 'v>( encoder: &'p Encoder<'v, 'tcx>, proc_def_id: DefId, parent_def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult { let encoder = PureEncoder::new( encoder, @@ -150,7 +150,7 @@ pub(super) struct PureEncoder<'p, 'v: 'p, 'tcx: 'v> { pure_encoding_context: PureEncodingContext, parent_def_id: DefId, /// Type substitutions applied to the MIR (if any) and the signature. - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, /// Span of the function declaration. span: Span, /// Signature of the function to be encoded. @@ -170,7 +170,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureEncoder<'p, 'v, 'tcx> { proc_def_id: DefId, pure_encoding_context: PureEncodingContext, parent_def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> Self { // should hold for extern specs as well (otherwise there would have // been an error reported earlier) diff --git a/prusti-viper/src/encoder/mir/pure/pure_functions/encoder_poly.rs b/prusti-viper/src/encoder/mir/pure/pure_functions/encoder_poly.rs index fc413de09a1..0a8a003da2e 100644 --- a/prusti-viper/src/encoder/mir/pure/pure_functions/encoder_poly.rs +++ b/prusti-viper/src/encoder/mir/pure/pure_functions/encoder_poly.rs @@ -27,7 +27,7 @@ use prusti_common::{config, vir::optimizations::functions::Simplifier, vir_local use prusti_rustc_interface::{ hir, hir::def_id::DefId, - middle::{mir, ty, ty::subst::SubstsRef}, + middle::{mir, ty, ty::GenericArgsRef}, span::Span, }; @@ -46,7 +46,7 @@ pub(super) struct PureFunctionEncoder<'p, 'v: 'p, 'tcx: 'v> { pure_encoding_context: PureEncodingContext, parent_def_id: DefId, /// Type substitutions applied to the MIR (if any) and the signature. - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, /// Span of the function declaration. span: Span, /// Signature of the function to be encoded. @@ -62,7 +62,7 @@ pub(super) fn encode_body<'p, 'v: 'p, 'tcx: 'v>( proc_def_id: DefId, pure_encoding_context: PureEncodingContext, parent_def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult { let mir = encoder .env() @@ -83,7 +83,7 @@ pub(super) fn encode_promoted<'p, 'v: 'p, 'tcx: 'v>( proc_def_id: DefId, promoted_id: mir::Promoted, parent_def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult { let tcx = encoder.env().tcx(); let promoted_bodies = tcx.promoted_mir(proc_def_id); @@ -148,7 +148,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> { proc_def_id: DefId, pure_encoding_context: PureEncodingContext, parent_def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> Self { // should hold for extern specs as well (otherwise there would have // been an error reported earlier) diff --git a/prusti-viper/src/encoder/mir/pure/pure_functions/interface.rs b/prusti-viper/src/encoder/mir/pure/pure_functions/interface.rs index 3da23a5ded1..49e44c76b25 100644 --- a/prusti-viper/src/encoder/mir/pure/pure_functions/interface.rs +++ b/prusti-viper/src/encoder/mir/pure/pure_functions/interface.rs @@ -10,7 +10,7 @@ use crate::encoder::{ use log::{debug, trace}; use prusti_common::config; use prusti_interface::data::ProcedureDefId; -use prusti_rustc_interface::middle::{mir, ty, ty::subst::SubstsRef}; +use prusti_rustc_interface::middle::{mir, ty, ty::GenericArgsRef}; use rustc_hash::{FxHashMap, FxHashSet}; use prusti_interface::specs::typed::ProcedureSpecificationKind; @@ -24,14 +24,14 @@ use vir_crate::{common::identifier::WithIdentifier, high as vir_high, polymorphi /// being called from callers (with different parameter environments). Each /// variant of a pure function will be encoded as a separate Viper function. /// Lifetimes/regions are erased. -type Key<'tcx> = (ProcedureDefId, SubstsRef<'tcx>, ty::PolyFnSig<'tcx>); +type Key<'tcx> = (ProcedureDefId, GenericArgsRef<'tcx>, ty::PolyFnSig<'tcx>); /// Compute the key for the given call. fn compute_key<'v, 'tcx: 'v>( encoder: &crate::encoder::encoder::Encoder<'v, 'tcx>, proc_def_id: ProcedureDefId, caller_def_id: ProcedureDefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult> { let tcx = encoder.env().tcx(); Ok(( @@ -119,7 +119,7 @@ pub(crate) struct PureFunctionEncoderState<'v, 'tcx: 'v> { pub(crate) struct FunctionDescription<'tcx> { proc_def_id: ProcedureDefId, parent_def_id: ProcedureDefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, } pub(crate) trait PureFunctionEncoderInterface<'v, 'tcx> { @@ -132,7 +132,7 @@ pub(crate) trait PureFunctionEncoderInterface<'v, 'tcx> { &self, proc_def_id: ProcedureDefId, parent_def_id: ProcedureDefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult; /// Encode the body of the given procedure as a pure expression. @@ -140,7 +140,7 @@ pub(crate) trait PureFunctionEncoderInterface<'v, 'tcx> { &self, proc_def_id: ProcedureDefId, parent_def_id: ProcedureDefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult; /// Encode the pure function definition. @@ -148,7 +148,7 @@ pub(crate) trait PureFunctionEncoderInterface<'v, 'tcx> { &self, proc_def_id: ProcedureDefId, parent_def_id: ProcedureDefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult<()>; /// Ensure that the function with the specified identifier is encoded. @@ -166,7 +166,7 @@ pub(crate) trait PureFunctionEncoderInterface<'v, 'tcx> { &self, proc_def_id: ProcedureDefId, parent_def_id: ProcedureDefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult<(String, vir_poly::Type)>; /// Encode the use (call) of a pure function, returning the name of the @@ -178,7 +178,7 @@ pub(crate) trait PureFunctionEncoderInterface<'v, 'tcx> { &self, proc_def_id: ProcedureDefId, parent_def_id: ProcedureDefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult<(String, vir_high::Type)>; /// Get the encoded function declaration. @@ -213,7 +213,7 @@ impl<'v, 'tcx: 'v> PureFunctionEncoderInterface<'v, 'tcx> &self, proc_def_id: ProcedureDefId, parent_def_id: ProcedureDefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult { let key = compute_key(self, proc_def_id, parent_def_id, substs)?; if !self @@ -248,12 +248,12 @@ impl<'v, 'tcx: 'v> PureFunctionEncoderInterface<'v, 'tcx> &self, mir::UnevaluatedConst { def, - substs, + args, promoted, }: mir::UnevaluatedConst<'tcx>, ) -> SpannedEncodingResult { let promoted_id = promoted.expect("unevaluated const should have a promoted ID"); - super::encoder_poly::encode_promoted(self, def, promoted_id, def, substs) + super::encoder_poly::encode_promoted(self, def, promoted_id, def, args) } // FIXME: This should be refactored to depend on encode_pure_expression_high @@ -262,7 +262,7 @@ impl<'v, 'tcx: 'v> PureFunctionEncoderInterface<'v, 'tcx> &self, proc_def_id: ProcedureDefId, parent_def_id: ProcedureDefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult { let key = compute_key(self, proc_def_id, parent_def_id, substs)?; if !self @@ -296,7 +296,7 @@ impl<'v, 'tcx: 'v> PureFunctionEncoderInterface<'v, 'tcx> &self, proc_def_id: ProcedureDefId, parent_def_id: ProcedureDefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult<()> { assert!( self.is_pure(proc_def_id, Some(substs)), @@ -440,7 +440,7 @@ impl<'v, 'tcx: 'v> PureFunctionEncoderInterface<'v, 'tcx> &self, proc_def_id: ProcedureDefId, parent_def_id: ProcedureDefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult<(String, vir_poly::Type)> { assert!( self.is_pure(proc_def_id, Some(substs)), @@ -499,7 +499,7 @@ impl<'v, 'tcx: 'v> PureFunctionEncoderInterface<'v, 'tcx> &self, proc_def_id: ProcedureDefId, parent_def_id: ProcedureDefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult<(String, vir_high::Type)> { assert!( self.is_pure(proc_def_id, Some(substs)), diff --git a/prusti-viper/src/encoder/mir/pure/specifications/encoder_high.rs b/prusti-viper/src/encoder/mir/pure/specifications/encoder_high.rs index d250405e775..71409b307ac 100644 --- a/prusti-viper/src/encoder/mir/pure/specifications/encoder_high.rs +++ b/prusti-viper/src/encoder/mir/pure/specifications/encoder_high.rs @@ -17,7 +17,7 @@ use crate::encoder::{ use prusti_common::config; use prusti_rustc_interface::{ hir::def_id::DefId, - middle::{ty, ty::subst::SubstsRef}, + middle::{ty, ty::GenericArgsRef}, span::Span, }; use vir_crate::{ @@ -39,7 +39,7 @@ pub(super) fn inline_closure_high<'tcx>( cl_expr: vir_high::Expression, args: Vec, parent_def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult { let mir = encoder .env() @@ -73,7 +73,7 @@ pub(super) fn inline_spec_item_high<'tcx>( target_return: Option<&vir_high::Expression>, targets_are_values: bool, parent_def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult { let mir = encoder .env() @@ -120,7 +120,7 @@ pub(super) fn encode_quantifier_high<'tcx>( encoded_args: Vec, is_exists: bool, parent_def_id: DefId, - substs: ty::subst::SubstsRef<'tcx>, + substs: ty::GenericArgsRef<'tcx>, ) -> SpannedEncodingResult { // Quantifiers are encoded as: // forall( diff --git a/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs b/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs index 2a1cafea9ac..67f838df495 100644 --- a/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs +++ b/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs @@ -22,7 +22,7 @@ use prusti_common::config; use prusti_rustc_interface::{ errors::MultiSpan, hir::def_id::DefId, - middle::{ty, ty::subst::SubstsRef}, + middle::{ty, ty::GenericArgsRef}, span::Span, }; use rustc_hash::FxHashSet; @@ -37,7 +37,7 @@ pub(super) fn inline_closure<'tcx>( cl_expr: vir_crate::polymorphic::Expr, args: Vec, parent_def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult { let mir = encoder .env() @@ -78,7 +78,7 @@ pub(super) fn inline_spec_item<'tcx>( target_return: Option<&vir_crate::polymorphic::Expr>, targets_are_values: bool, parent_def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult { // each non-lifetime parameter should be matched with a subst assert_eq!( @@ -139,7 +139,7 @@ pub(super) fn encode_quantifier<'tcx>( encoded_args: Vec, is_exists: bool, parent_def_id: DefId, - substs: ty::subst::SubstsRef<'tcx>, + substs: ty::GenericArgsRef<'tcx>, ) -> SpannedEncodingResult { // Quantifiers are encoded as: // forall( diff --git a/prusti-viper/src/encoder/mir/pure/specifications/interface.rs b/prusti-viper/src/encoder/mir/pure/specifications/interface.rs index ff05151e2dd..f927a37cf12 100644 --- a/prusti-viper/src/encoder/mir/pure/specifications/interface.rs +++ b/prusti-viper/src/encoder/mir/pure/specifications/interface.rs @@ -29,7 +29,7 @@ use crate::encoder::{ }; use prusti_rustc_interface::{ hir::def_id::DefId, - middle::{mir, ty::subst::SubstsRef}, + middle::{mir, ty::GenericArgsRef}, span::Span, }; use vir_crate::{ @@ -44,7 +44,7 @@ pub(crate) trait SpecificationEncoderInterface<'tcx> { span: Span, encoded_args: Vec, parent_def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult; #[allow(clippy::too_many_arguments)] @@ -55,7 +55,7 @@ pub(crate) trait SpecificationEncoderInterface<'tcx> { target_args: &[vir_high::Expression], target_return: Option<&vir_high::Expression>, parent_def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult; fn encode_loop_spec_high( @@ -63,7 +63,7 @@ pub(crate) trait SpecificationEncoderInterface<'tcx> { mir: &mir::Body<'tcx>, // body of the method containing the loop invariant_block: mir::BasicBlock, // in which the invariant is defined parent_def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult; fn encode_prusti_operation( @@ -72,7 +72,7 @@ pub(crate) trait SpecificationEncoderInterface<'tcx> { span: Span, encoded_args: Vec, parent_def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult; #[allow(clippy::too_many_arguments)] @@ -84,7 +84,7 @@ pub(crate) trait SpecificationEncoderInterface<'tcx> { target_return: Option<&vir_poly::Expr>, targets_are_values: bool, parent_def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult; fn encode_invariant( @@ -92,7 +92,7 @@ pub(crate) trait SpecificationEncoderInterface<'tcx> { mir: &mir::Body<'tcx>, // body of the method containing the loop invariant_block: mir::BasicBlock, // in which the invariant is defined parent_def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult; } @@ -103,7 +103,7 @@ impl<'v, 'tcx: 'v> SpecificationEncoderInterface<'tcx> for crate::encoder::Encod span: Span, encoded_args: Vec, parent_def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult { match fn_name { "prusti_contracts::forall" | "prusti_contracts::exists" => encode_quantifier_high( @@ -125,7 +125,7 @@ impl<'v, 'tcx: 'v> SpecificationEncoderInterface<'tcx> for crate::encoder::Encod target_args: &[vir_high::Expression], target_return: Option<&vir_high::Expression>, parent_def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult { let encoded_assertion = inline_spec_item_high( self, @@ -147,7 +147,7 @@ impl<'v, 'tcx: 'v> SpecificationEncoderInterface<'tcx> for crate::encoder::Encod mir: &mir::Body<'tcx>, // body of the method containing the loop invariant_block: mir::BasicBlock, // in which the invariant is defined parent_def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult { // identify previous block: there should only be one let predecessors = &mir.basic_blocks.predecessors()[invariant_block]; @@ -239,7 +239,7 @@ impl<'v, 'tcx: 'v> SpecificationEncoderInterface<'tcx> for crate::encoder::Encod span: Span, encoded_args: Vec, parent_def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult { match fn_name { "prusti_contracts::forall" | "prusti_contracts::exists" => encode_quantifier( @@ -267,7 +267,7 @@ impl<'v, 'tcx: 'v> SpecificationEncoderInterface<'tcx> for crate::encoder::Encod target_return: Option<&vir_poly::Expr>, targets_are_values: bool, parent_def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult { let mut encoded_assertion = inline_spec_item( self, @@ -302,7 +302,7 @@ impl<'v, 'tcx: 'v> SpecificationEncoderInterface<'tcx> for crate::encoder::Encod mir: &mir::Body<'tcx>, // body of the method containing the loop invariant_block: mir::BasicBlock, // in which the invariant is defined parent_def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult { // identify closure aggregate assign (the invariant body) let closure_assigns = mir.basic_blocks[invariant_block] diff --git a/prusti-viper/src/encoder/mir/pure/specifications/utils.rs b/prusti-viper/src/encoder/mir/pure/specifications/utils.rs index 84ecb1f6f02..db9dcd473c2 100644 --- a/prusti-viper/src/encoder/mir/pure/specifications/utils.rs +++ b/prusti-viper/src/encoder/mir/pure/specifications/utils.rs @@ -7,7 +7,7 @@ use prusti_interface::environment::EnvQuery; use prusti_rustc_interface::{ hir::def_id::DefId, - middle::ty::{subst::SubstsRef, Ty, TyKind}, + middle::ty::{GenericArgsRef, Ty, TyKind}, span::Span, }; @@ -15,11 +15,11 @@ pub(super) fn extract_closure_from_ty<'tcx>( env_query: EnvQuery<'tcx>, ty: Ty<'tcx>, ) -> ( - DefId, // closure definition - SubstsRef<'tcx>, // closure substitutions - Span, // definition span - Vec>, // input types - Vec>, // upvar types + DefId, // closure definition + GenericArgsRef<'tcx>, // closure substitutions + Span, // definition span + Vec>, // input types + Vec>, // upvar types ) { match ty.kind() { TyKind::Closure(def_id, substs) => { diff --git a/prusti-viper/src/encoder/mir/specifications/constraints.rs b/prusti-viper/src/encoder/mir/specifications/constraints.rs index 0cffadea6a8..882d895cc53 100644 --- a/prusti-viper/src/encoder/mir/specifications/constraints.rs +++ b/prusti-viper/src/encoder/mir/specifications/constraints.rs @@ -8,7 +8,7 @@ use prusti_interface::{ use prusti_rustc_interface::{ errors::MultiSpan, hir::def_id::DefId, - middle::{ty, ty::subst::SubstsRef}, + middle::{ty, ty::GenericArgsRef}, span::Span, }; @@ -110,7 +110,7 @@ impl<'spec, 'env: 'spec, 'tcx: 'env> ConstraintResolver<'spec, 'env, 'tcx> #[derive(Debug)] struct ConstraintSolvingContext<'tcx> { proc_def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, caller_proc_def_id: Option, } @@ -170,7 +170,7 @@ mod trait_bounds { env.query.resolve_assoc_types(predicate, param_env_lookup); env.query - .evaluate_predicate(normalized_predicate, param_env_lookup) + .evaluate_predicate(normalized_predicate.as_predicate(), param_env_lookup) }) } @@ -186,7 +186,7 @@ mod trait_bounds { .find_trait_method_substs(context.proc_def_id, context.substs); let param_env = if let Some((_, trait_substs)) = maybe_trait_method { trace!("Applying trait substs {:?}", trait_substs); - ty::EarlyBinder::bind(param_env).subst(env.tcx(), trait_substs) + ty::EarlyBinder::bind(param_env).instantiate(env.tcx(), trait_substs) } else { param_env }; @@ -200,7 +200,7 @@ mod trait_bounds { param_env } else { trace!("Applying call substs {:?}", context.substs); - ty::EarlyBinder::bind(param_env).subst(env.tcx(), context.substs) + ty::EarlyBinder::bind(param_env).instantiate(env.tcx(), context.substs) } } diff --git a/prusti-viper/src/encoder/mir/specifications/interface.rs b/prusti-viper/src/encoder/mir/specifications/interface.rs index 73a829e7e60..fbbeb6b1d56 100644 --- a/prusti-viper/src/encoder/mir/specifications/interface.rs +++ b/prusti-viper/src/encoder/mir/specifications/interface.rs @@ -6,7 +6,7 @@ use prusti_interface::{ }, utils::has_spec_only_attr, }; -use prusti_rustc_interface::{hir::def_id::DefId, middle::ty::subst::SubstsRef, span::Span}; +use prusti_rustc_interface::{hir::def_id::DefId, middle::ty::GenericArgsRef, span::Span}; use std::{cell::RefCell, hash::Hash}; pub(crate) struct SpecificationsState<'tcx> { @@ -25,16 +25,16 @@ impl<'tcx> SpecificationsState<'tcx> { pub(super) struct FunctionCallEncodingQuery<'tcx> { pub called_def_id: DefId, pub caller_def_id: DefId, - pub call_substs: SubstsRef<'tcx>, + pub call_substs: GenericArgsRef<'tcx>, } #[derive(Copy, Clone, Debug, PartialEq, Eq, Hash)] pub(super) enum SpecQuery<'tcx> { - FunctionDefEncoding(DefId, SubstsRef<'tcx>), + FunctionDefEncoding(DefId, GenericArgsRef<'tcx>), FunctionCallEncoding(FunctionCallEncodingQuery<'tcx>), /// For determining the [ProcedureSpecificationKind] of a procedure, e.g. /// for a check whether the function is pure or impure - GetProcKind(DefId, SubstsRef<'tcx>), + GetProcKind(DefId, GenericArgsRef<'tcx>), FetchSpan(DefId), } @@ -51,7 +51,7 @@ impl<'tcx> SpecQuery<'tcx> { } } - pub fn adapt_to(&self, new_def_id: DefId, new_substs: SubstsRef<'tcx>) -> Self { + pub fn adapt_to(&self, new_def_id: DefId, new_substs: GenericArgsRef<'tcx>) -> Self { use SpecQuery::*; match self { FunctionDefEncoding(_, _) => FunctionDefEncoding(new_def_id, new_substs), @@ -70,19 +70,19 @@ impl<'tcx> SpecQuery<'tcx> { pub(crate) trait SpecificationsInterface<'tcx> { // TODO abstract-predicates: Maybe this should be deleted (and ProcedureSpecificationKind::is_pure) - fn is_pure(&self, def_id: DefId, substs: Option>) -> bool; + fn is_pure(&self, def_id: DefId, substs: Option>) -> bool; fn get_proc_kind( &self, def_id: DefId, - substs: Option>, + substs: Option>, ) -> ProcedureSpecificationKind; - fn is_trusted(&self, def_id: DefId, substs: Option>) -> bool; + fn is_trusted(&self, def_id: DefId, substs: Option>) -> bool; - fn get_predicate_body(&self, def_id: DefId, substs: SubstsRef<'tcx>) -> Option; + fn get_predicate_body(&self, def_id: DefId, substs: GenericArgsRef<'tcx>) -> Option; - fn terminates(&self, def_id: DefId, substs: Option>) -> bool; + fn terminates(&self, def_id: DefId, substs: Option>) -> bool; /// Get the loop invariant attached to a function with a /// `prusti::loop_body_invariant_spec` attribute. @@ -110,7 +110,7 @@ pub(crate) trait SpecificationsInterface<'tcx> { fn get_procedure_specs( &self, def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> Option; /// Get the specifications attached to a function for a function call. @@ -118,7 +118,7 @@ pub(crate) trait SpecificationsInterface<'tcx> { &self, called_def_id: DefId, caller_def_id: DefId, - call_substs: SubstsRef<'tcx>, + call_substs: GenericArgsRef<'tcx>, ) -> Option; /// Is the closure specified with the `def_id` spec only? @@ -131,7 +131,7 @@ pub(crate) trait SpecificationsInterface<'tcx> { impl<'v, 'tcx: 'v> SpecificationsInterface<'tcx> for super::super::super::Encoder<'v, 'tcx> { #[tracing::instrument(level = "trace", skip(self), ret)] - fn is_pure(&self, def_id: DefId, substs: Option>) -> bool { + fn is_pure(&self, def_id: DefId, substs: Option>) -> bool { let kind = self.get_proc_kind(def_id, substs); let mut pure = matches!( kind, @@ -152,7 +152,7 @@ impl<'v, 'tcx: 'v> SpecificationsInterface<'tcx> for super::super::super::Encode fn get_proc_kind( &self, def_id: DefId, - substs: Option>, + substs: Option>, ) -> ProcedureSpecificationKind { let substs = substs.unwrap_or_else(|| self.env().query.identity_substs(def_id)); let query = SpecQuery::GetProcKind(def_id, substs); @@ -166,7 +166,7 @@ impl<'v, 'tcx: 'v> SpecificationsInterface<'tcx> for super::super::super::Encode } #[tracing::instrument(level = "trace", skip(self), ret)] - fn is_trusted(&self, def_id: DefId, substs: Option>) -> bool { + fn is_trusted(&self, def_id: DefId, substs: Option>) -> bool { let substs = substs.unwrap_or_else(|| self.env().query.identity_substs(def_id)); let query = SpecQuery::GetProcKind(def_id, substs); self.specifications_state @@ -178,7 +178,7 @@ impl<'v, 'tcx: 'v> SpecificationsInterface<'tcx> for super::super::super::Encode } #[tracing::instrument(level = "trace", skip(self), ret)] - fn get_predicate_body(&self, def_id: DefId, substs: SubstsRef<'tcx>) -> Option { + fn get_predicate_body(&self, def_id: DefId, substs: GenericArgsRef<'tcx>) -> Option { let query = SpecQuery::FunctionDefEncoding(def_id, substs); let mut specs = self.specifications_state.specs.borrow_mut(); specs @@ -189,7 +189,7 @@ impl<'v, 'tcx: 'v> SpecificationsInterface<'tcx> for super::super::super::Encode } #[tracing::instrument(level = "trace", skip(self), ret)] - fn terminates(&self, def_id: DefId, substs: Option>) -> bool { + fn terminates(&self, def_id: DefId, substs: Option>) -> bool { let substs = substs.unwrap_or_else(|| self.env().query.identity_substs(def_id)); let query = SpecQuery::GetProcKind(def_id, substs); self.specifications_state @@ -264,7 +264,7 @@ impl<'v, 'tcx: 'v> SpecificationsInterface<'tcx> for super::super::super::Encode fn get_procedure_specs( &self, def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> Option { let query = SpecQuery::FunctionDefEncoding(def_id, substs); let mut specs = self.specifications_state.specs.borrow_mut(); @@ -276,7 +276,7 @@ impl<'v, 'tcx: 'v> SpecificationsInterface<'tcx> for super::super::super::Encode &self, called_def_id: DefId, caller_def_id: DefId, - call_substs: SubstsRef<'tcx>, + call_substs: GenericArgsRef<'tcx>, ) -> Option { let query = SpecQuery::FunctionCallEncoding(FunctionCallEncodingQuery { called_def_id, diff --git a/prusti-viper/src/encoder/mir/types/const_parameters.rs b/prusti-viper/src/encoder/mir/types/const_parameters.rs index e472c9132a8..3fa4827918b 100644 --- a/prusti-viper/src/encoder/mir/types/const_parameters.rs +++ b/prusti-viper/src/encoder/mir/types/const_parameters.rs @@ -1,16 +1,16 @@ //! Helper functions for working with const parameters. use crate::encoder::errors::{SpannedEncodingError, SpannedEncodingResult}; -use prusti_rustc_interface::middle::{ty, ty::SubstsRef}; +use prusti_rustc_interface::middle::{ty, ty::GenericArgsRef}; use vir_crate::high as vir_high; pub(super) fn extract_const_parameters_from_substs<'tcx>( type_encoder: &impl super::MirTypeEncoderInterface<'tcx>, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, const_parameters: &mut Vec, ) -> SpannedEncodingResult<()> { for kind in substs.iter() { - if let ty::subst::GenericArgKind::Type(arg_ty) = kind.unpack() { + if let ty::GenericArgKind::Type(arg_ty) = kind.unpack() { extract_const_parameters_from_type(type_encoder, arg_ty, const_parameters)?; } } @@ -44,11 +44,11 @@ pub(super) fn extract_const_parameters_from_type<'tcx>( | ty::TyKind::Error(_) | ty::TyKind::Never | ty::TyKind::Dynamic(..) => {} - ty::TyKind::Adt(_, substs) - | ty::TyKind::Closure(_, substs) - | ty::TyKind::Alias(_, ty::AliasTy { substs, .. }) - | ty::TyKind::FnDef(_, substs) => { - extract_const_parameters_from_substs(type_encoder, substs, const_parameters)? + ty::TyKind::Adt(_, args) + | ty::TyKind::Closure(_, args) + | ty::TyKind::Alias(_, ty::AliasTy { args, .. }) + | ty::TyKind::FnDef(_, args) => { + extract_const_parameters_from_substs(type_encoder, args, const_parameters)? } ty::TyKind::Ref(_, ty, _) => { extract_const_parameters_from_type(type_encoder, *ty, const_parameters)? diff --git a/prusti-viper/src/encoder/mir/types/encoder.rs b/prusti-viper/src/encoder/mir/types/encoder.rs index c6df1436f6f..97c2e9710fa 100644 --- a/prusti-viper/src/encoder/mir/types/encoder.rs +++ b/prusti-viper/src/encoder/mir/types/encoder.rs @@ -37,7 +37,7 @@ impl<'p, 'v, 'r: 'v, 'tcx: 'v> TypeEncoder<'p, 'v, 'tcx> { fn encode_substs( &self, - substs: prusti_rustc_interface::middle::ty::subst::SubstsRef<'tcx>, + substs: prusti_rustc_interface::middle::ty::GenericArgsRef<'tcx>, ) -> Vec { encode_substs(self.encoder, substs) } @@ -235,10 +235,10 @@ impl<'p, 'v, 'r: 'v, 'tcx: 'v> TypeEncoder<'p, 'v, 'tcx> { vir::Type::TypeVar(self.encoder.encode_param(param_ty.name, param_ty.index)) } - ty::TyKind::Alias(ty::AliasKind::Projection, ty::AliasTy { def_id, substs, .. }) => { + ty::TyKind::Alias(ty::AliasKind::Projection, ty::AliasTy { def_id, args, .. }) => { vir::Type::projection( self.encoder.encode_item_name(*def_id), - self.encode_substs(substs), + self.encode_substs(args), lifetimes, ) } @@ -443,7 +443,7 @@ impl<'p, 'v, 'r: 'v, 'tcx: 'v> TypeEncoder<'p, 'v, 'tcx> { upper_bound: None, }), "prusti_contracts::Ghost" => { - if let ty::subst::GenericArgKind::Type(ty) = substs[0].unpack() { + if let ty::GenericArgKind::Type(ty) = substs[0].unpack() { Self::new(self.encoder, ty).encode_type_def_high()? } else { unreachable!("no type parameter given for Ghost") @@ -651,12 +651,12 @@ impl<'p, 'v, 'r: 'v, 'tcx: 'v> TypeEncoder<'p, 'v, 'tcx> { fn encode_substs<'v, 'tcx: 'v>( encoder: &Encoder<'v, 'tcx>, - substs: prusti_rustc_interface::middle::ty::subst::SubstsRef<'tcx>, + substs: prusti_rustc_interface::middle::ty::GenericArgsRef<'tcx>, ) -> Vec { substs .iter() .filter_map(|kind| { - if let ty::subst::GenericArgKind::Type(ty) = kind.unpack() { + if let ty::GenericArgKind::Type(ty) = kind.unpack() { encoder.encode_type_high(ty).ok() } else { None @@ -696,7 +696,7 @@ fn encode_trusted_name<'v, 'tcx: 'v>(encoder: &Encoder<'v, 'tcx>, did: DefId) -> fn encode_variant<'v, 'tcx: 'v>( encoder: &Encoder<'v, 'tcx>, name: String, - substs: ty::subst::SubstsRef<'tcx>, + substs: ty::GenericArgsRef<'tcx>, variant: &ty::VariantDef, ) -> SpannedEncodingResult { let tcx = encoder.env().tcx(); @@ -724,7 +724,7 @@ fn encode_variant<'v, 'tcx: 'v>( pub(super) fn encode_adt_def<'v, 'tcx>( encoder: &Encoder<'v, 'tcx>, adt_def: ty::AdtDef<'tcx>, - substs: ty::subst::SubstsRef<'tcx>, + substs: ty::GenericArgsRef<'tcx>, variant_index: Option, ) -> SpannedEncodingResult { let lifetimes = encoder.get_lifetimes_from_substs(substs)?; diff --git a/prusti-viper/src/encoder/mir/types/interface.rs b/prusti-viper/src/encoder/mir/types/interface.rs index 28ca979996a..72a4f2cbacf 100644 --- a/prusti-viper/src/encoder/mir/types/interface.rs +++ b/prusti-viper/src/encoder/mir/types/interface.rs @@ -2,7 +2,7 @@ use super::TypeEncoder; use crate::encoder::{ errors::{EncodingError, EncodingResult, SpannedEncodingError, SpannedEncodingResult}, high::types::HighTypeEncoderInterface, - mir::types::interface::ty::SubstsRef, + mir::types::interface::ty::GenericArgsRef, }; use prusti_rustc_interface::{ abi::FieldIdx, @@ -45,11 +45,11 @@ pub(crate) trait MirTypeEncoderInterface<'tcx> { ) -> SpannedEncodingResult>; fn get_lifetimes_from_substs( &self, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult>; fn get_const_parameters_from_substs( &self, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult>; fn get_const_parameters_from_types( &self, @@ -89,7 +89,7 @@ pub(crate) trait MirTypeEncoderInterface<'tcx> { fn encode_adt_def( &self, adt_def: ty::AdtDef<'tcx>, - substs: ty::subst::SubstsRef<'tcx>, + substs: ty::GenericArgsRef<'tcx>, variant_index: Option, ) -> SpannedEncodingResult; fn encode_type_bounds_high( @@ -185,7 +185,7 @@ impl<'v, 'tcx: 'v> MirTypeEncoderInterface<'tcx> for super::super::super::Encode } fn get_lifetimes_from_substs( &self, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult> { let mut lifetimes = Vec::new(); super::lifetimes::extract_lifetimes_from_substs(self, substs, &mut lifetimes)?; @@ -201,7 +201,7 @@ impl<'v, 'tcx: 'v> MirTypeEncoderInterface<'tcx> for super::super::super::Encode } fn get_const_parameters_from_substs( &self, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult> { let mut const_parameters = Vec::new(); super::const_parameters::extract_const_parameters_from_substs( @@ -432,7 +432,7 @@ impl<'v, 'tcx: 'v> MirTypeEncoderInterface<'tcx> for super::super::super::Encode fn encode_adt_def( &self, adt_def: ty::AdtDef<'tcx>, - substs: ty::subst::SubstsRef<'tcx>, + substs: ty::GenericArgsRef<'tcx>, variant_index: Option, ) -> SpannedEncodingResult { super::encoder::encode_adt_def(self, adt_def, substs, variant_index) diff --git a/prusti-viper/src/encoder/mir/types/lifetimes.rs b/prusti-viper/src/encoder/mir/types/lifetimes.rs index f53b1762fa3..c3b176c8288 100644 --- a/prusti-viper/src/encoder/mir/types/lifetimes.rs +++ b/prusti-viper/src/encoder/mir/types/lifetimes.rs @@ -2,23 +2,23 @@ use crate::encoder::errors::{SpannedEncodingError, SpannedEncodingResult}; use prusti_interface::environment::debug_utils::to_text::ToText; -use prusti_rustc_interface::middle::{ty, ty::SubstsRef}; +use prusti_rustc_interface::middle::{ty, ty::GenericArgsRef}; use vir_crate::high as vir_high; pub(super) fn extract_lifetimes_from_substs<'tcx>( type_encoder: &impl super::MirTypeEncoderInterface<'tcx>, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, lifetimes: &mut Vec, ) -> SpannedEncodingResult<()> { for kind in substs.iter() { - if let ty::subst::GenericArgKind::Lifetime(region) = kind.unpack() { + if let ty::GenericArgKind::Lifetime(region) = kind.unpack() { lifetimes.push(vir_high::ty::LifetimeConst { name: region.to_text(), }); } } for kind in substs.iter() { - if let ty::subst::GenericArgKind::Type(arg_ty) = kind.unpack() { + if let ty::GenericArgKind::Type(arg_ty) = kind.unpack() { extract_lifetimes_from_type(type_encoder, arg_ty, lifetimes)?; } } @@ -51,11 +51,11 @@ pub(super) fn extract_lifetimes_from_type<'tcx>( | ty::TyKind::Str | ty::TyKind::Error(_) | ty::TyKind::Never => {} - ty::TyKind::Adt(_, substs) - | ty::TyKind::Closure(_, substs) - | ty::TyKind::Alias(_, ty::AliasTy { substs, .. }) - | ty::TyKind::FnDef(_, substs) => { - extract_lifetimes_from_substs(type_encoder, substs, lifetimes)? + ty::TyKind::Adt(_, args) + | ty::TyKind::Closure(_, args) + | ty::TyKind::Alias(_, ty::AliasTy { args, .. }) + | ty::TyKind::FnDef(_, args) => { + extract_lifetimes_from_substs(type_encoder, args, lifetimes)? } ty::TyKind::Array(ty, _) | ty::TyKind::Slice(ty) => { extract_lifetimes_from_type(type_encoder, *ty, lifetimes)? diff --git a/prusti-viper/src/encoder/mir_encoder/downcast_detector.rs b/prusti-viper/src/encoder/mir_encoder/downcast_detector.rs index c5a6f1942da..9dd5a21d92f 100644 --- a/prusti-viper/src/encoder/mir_encoder/downcast_detector.rs +++ b/prusti-viper/src/encoder/mir_encoder/downcast_detector.rs @@ -23,21 +23,20 @@ struct DownCastCollector<'tcx> { impl<'tcx> Visitor<'tcx> for DownCastCollector<'tcx> { fn visit_projection_elem( &mut self, - local: mir::Local, - proj_base: &[mir::PlaceElem<'tcx>], + place_ref: mir::PlaceRef<'tcx>, elem: mir::PlaceElem<'tcx>, context: mir::visit::PlaceContext, location: mir::Location, ) { - self.super_projection_elem(local, proj_base, elem, context, location); + self.super_projection_elem(place_ref, elem, context, location); if let mir::PlaceElem::Downcast(_, variant) = elem { self.downcasts.insert( ( // FIXME: Store `PlaceRef`, once `visit_projection_elem` will provide that. MirPlace { - local, - projection: proj_base.to_owned(), + local: place_ref.local, + projection: place_ref.projection.to_owned(), }, variant, ) diff --git a/prusti-viper/src/encoder/mir_encoder/mod.rs b/prusti-viper/src/encoder/mir_encoder/mod.rs index a8bdfbc6c52..3304c97ea9a 100644 --- a/prusti-viper/src/encoder/mir_encoder/mod.rs +++ b/prusti-viper/src/encoder/mir_encoder/mod.rs @@ -500,11 +500,11 @@ impl<'p, 'v: 'p, 'tcx: 'v> MirEncoder<'p, 'v, 'tcx> { mir::BinOp::Ge => vir::Expr::ge_cmp(left, right), mir::BinOp::Lt => vir::Expr::lt_cmp(left, right), mir::BinOp::Le => vir::Expr::le_cmp(left, right), - mir::BinOp::Add => vir::Expr::add(left, right), - mir::BinOp::Sub => vir::Expr::sub(left, right), + mir::BinOp::AddUnchecked | mir::BinOp::Add => vir::Expr::add(left, right), + mir::BinOp::SubUnchecked | mir::BinOp::Sub => vir::Expr::sub(left, right), mir::BinOp::Rem => vir::Expr::rem(left, right), mir::BinOp::Div => vir::Expr::div(left, right), - mir::BinOp::Mul => vir::Expr::mul(left, right), + mir::BinOp::MulUnchecked | mir::BinOp::Mul => vir::Expr::mul(left, right), mir::BinOp::BitAnd if is_bool => vir::Expr::and(left, right), mir::BinOp::BitOr if is_bool => vir::Expr::or(left, right), mir::BinOp::BitXor if is_bool => vir::Expr::xor(left, right), @@ -526,11 +526,11 @@ impl<'p, 'v: 'p, 'tcx: 'v> MirEncoder<'p, 'v, 'tcx> { mir::BinOp::BitAnd => vir::Expr::bin_op(vir::BinaryOpKind::BitAnd, left, right), mir::BinOp::BitOr => vir::Expr::bin_op(vir::BinaryOpKind::BitOr, left, right), mir::BinOp::BitXor => vir::Expr::bin_op(vir::BinaryOpKind::BitXor, left, right), - mir::BinOp::Shl => vir::Expr::bin_op(vir::BinaryOpKind::Shl, left, right), + mir::BinOp::ShlUnchecked | mir::BinOp::Shl => vir::Expr::bin_op(vir::BinaryOpKind::Shl, left, right), // https://doc.rust-lang.org/reference/expressions/operator-expr.html#arithmetic-and-logical-binary-operators // Arithmetic right shift on signed integer types, logical right shift on unsigned integer types. - mir::BinOp::Shr if is_signed => vir::Expr::bin_op(vir::BinaryOpKind::AShr, left, right), - mir::BinOp::Shr => vir::Expr::bin_op(vir::BinaryOpKind::LShr, left, right), + mir::BinOp::ShrUnchecked | mir::BinOp::Shr if is_signed => vir::Expr::bin_op(vir::BinaryOpKind::AShr, left, right), + mir::BinOp::ShrUnchecked | mir::BinOp::Shr => vir::Expr::bin_op(vir::BinaryOpKind::LShr, left, right), mir::BinOp::Offset => { error_unsupported!("operation '{:?}' is not supported", op); } diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs index 433c1dedc2b..00e3d94408b 100644 --- a/prusti-viper/src/encoder/procedure_encoder.rs +++ b/prusti-viper/src/encoder/procedure_encoder.rs @@ -56,7 +56,7 @@ use prusti_rustc_interface::index::IndexSlice; use prusti_rustc_interface::middle::mir::Mutability; use prusti_rustc_interface::middle::mir; use prusti_rustc_interface::middle::mir::{TerminatorKind}; -use prusti_rustc_interface::middle::ty::{self, subst::SubstsRef}; +use prusti_rustc_interface::middle::ty::{self, GenericArgsRef}; use prusti_rustc_interface::target::abi::{FieldIdx, Integer}; use rustc_hash::{FxHashMap, FxHashSet}; use prusti_rustc_interface::span::Span; @@ -133,7 +133,7 @@ pub struct ProcedureEncoder<'p, 'v: 'p, 'tcx: 'v> { cached_loop_invariant_block: FxHashMap, /// Type substitutions inside this procedure. Most likely identity for the /// given proc_def_id. - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, } impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { @@ -1609,7 +1609,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { location, )? } - mir::Rvalue::Cast(mir::CastKind::Pointer(ty::adjustment::PointerCast::Unsize), ref operand, cast_ty) => { + mir::Rvalue::Cast(mir::CastKind::PointerCoercion(ty::adjustment::PointerCoercion::Unsize), ref operand, cast_ty) => { let rhs_ty = self.mir_encoder.get_operand_ty(operand); if rhs_ty.is_array_ref() && cast_ty.is_slice_ref() { trace!("slice: operand={:?}, ty={:?}", operand, cast_ty); @@ -1626,7 +1626,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { )); } } - mir::Rvalue::Cast(mir::CastKind::Pointer(_), _, _) | + mir::Rvalue::Cast(mir::CastKind::PointerCoercion(_), _, _) | mir::Rvalue::Cast(mir::CastKind::DynStar, _, _) => { return Err(SpannedEncodingError::unsupported( "raw pointers are not supported", span @@ -1664,7 +1664,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { /// Generate an unsupported encoding error for unhandled borrow kinds. fn unsupported_borrow_kind(kind: mir::BorrowKind) -> EncodingError { match kind { - mir::BorrowKind::Unique => { + mir::BorrowKind::Mut { .. } => { EncodingError::unsupported( "unsuported creation of unique borrows (implicitly created in closure bindings)", ) @@ -1773,7 +1773,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { (expiring, Some(restored), false, stmts) } - mir::Rvalue::Cast(mir::CastKind::Pointer(ty::adjustment::PointerCast::Unsize), ref operand, ty) => { + mir::Rvalue::Cast(mir::CastKind::PointerCoercion(ty::adjustment::PointerCoercion::Unsize), ref operand, ty) => { trace!("cast: operand={:?}, ty={:?}", operand, ty); let place = match *operand { mir::Operand::Move(place) => place, @@ -1867,7 +1867,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { &mir::Rvalue::Use(mir::Operand::Copy(_)) => false, &mir::Rvalue::Ref(_, mir::BorrowKind::Mut { .. }, _) | &mir::Rvalue::Use(mir::Operand::Move(_)) => true, - &mir::Rvalue::Cast(mir::CastKind::Pointer(ty::adjustment::PointerCast::Unsize), _, _ty) => false, + &mir::Rvalue::Cast(mir::CastKind::PointerCoercion(ty::adjustment::PointerCoercion::Unsize), _, _ty) => false, &mir::Rvalue::Use(mir::Operand::Constant(_)) => false, x => unreachable!("{:?}", x), }, @@ -3069,7 +3069,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { destination: mir::Place<'tcx>, target: Option, bin_op: vir::BinaryOpKind, - substs: ty::subst::SubstsRef<'tcx>, + substs: ty::GenericArgsRef<'tcx>, ) -> SpannedEncodingResult> { let arg_ty = self.mir_encoder.get_operand_ty(&args[0]); @@ -3168,7 +3168,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { destination: mir::Place<'tcx>, target: Option, called_def_id: ProcedureDefId, - mut substs: ty::subst::SubstsRef<'tcx>, + mut substs: ty::GenericArgsRef<'tcx>, ) -> SpannedEncodingResult> { let full_func_proc_name = &self .encoder @@ -3232,7 +3232,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { // TODO: weird fix for closure call substitutions, we need to // prepend the identity substs of the containing method ... - substs = self.encoder.env().tcx().mk_substs_from_iter(self.substs.iter().chain(substs)); + substs = self.encoder.env().tcx().mk_args_from_iter(self.substs.iter().chain(substs)); } else { for (arg, encoded_operand) in mir_args.iter().zip(encoded_operands.iter_mut()) { let arg_ty = self.mir_encoder.get_operand_ty(arg); @@ -3556,7 +3556,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { destination: mir::Place<'tcx>, target: Option, called_def_id: ProcedureDefId, - call_substs: SubstsRef<'tcx>, + call_substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult> { let (function_name, return_type) = self.encoder.encode_pure_function_use(called_def_id, self.proc_def_id, call_substs) .with_span(call_site_span)?; @@ -3596,7 +3596,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { arg_exprs: Vec, return_type: Type, called_def_id: ProcedureDefId, - call_substs: SubstsRef<'tcx>, + call_substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult> { let formal_args: Vec = args .iter() @@ -3835,7 +3835,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { fn encode_precondition_expr( &self, contract: &ProcedureContract<'tcx>, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, override_spans: FxHashMap // spans for fake locals ) -> SpannedEncodingResult<( vir::Expr, @@ -4147,7 +4147,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { contract: &ProcedureContract<'tcx>, pre_label: &str, post_label: &str, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> EncodingResult> { let span = if let Some(loc) = location { self.mir.source_info(loc).span @@ -4350,7 +4350,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { _diverging: bool, loan: Option, function_end: bool, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> SpannedEncodingResult<( vir::Expr, // Returned permissions from types. Option, // Permission of the return value. diff --git a/prusti-viper/src/encoder/stub_function_encoder.rs b/prusti-viper/src/encoder/stub_function_encoder.rs index 5c544f3f97b..2de09523a37 100644 --- a/prusti-viper/src/encoder/stub_function_encoder.rs +++ b/prusti-viper/src/encoder/stub_function_encoder.rs @@ -10,12 +10,10 @@ use crate::encoder::Encoder; use crate::encoder::snapshot::interface::SnapshotEncoderInterface; use vir_crate::polymorphic as vir; use prusti_rustc_interface::hir::def_id::DefId; -use prusti_rustc_interface::middle::ty::subst::SubstsRef; +use prusti_rustc_interface::middle::ty::GenericArgsRef; use prusti_rustc_interface::middle::mir; use log::debug; - use crate::encoder::errors::WithSpan; - use crate::encoder::errors::SpannedEncodingResult; pub struct StubFunctionEncoder<'p, 'v: 'p, 'tcx: 'v> { @@ -23,7 +21,7 @@ pub struct StubFunctionEncoder<'p, 'v: 'p, 'tcx: 'v> { mir: &'p mir::Body<'tcx>, mir_encoder: MirEncoder<'p, 'v, 'tcx>, proc_def_id: DefId, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, } impl<'p, 'v: 'p, 'tcx: 'v> StubFunctionEncoder<'p, 'v, 'tcx> { @@ -32,7 +30,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> StubFunctionEncoder<'p, 'v, 'tcx> { encoder: &'p Encoder<'v, 'tcx>, proc_def_id: DefId, mir: &'p mir::Body<'tcx>, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> Self { StubFunctionEncoder { encoder, diff --git a/prusti-viper/src/lib.rs b/prusti-viper/src/lib.rs index 77d9f8a80c3..86876199b0c 100644 --- a/prusti-viper/src/lib.rs +++ b/prusti-viper/src/lib.rs @@ -8,9 +8,9 @@ #![feature(box_patterns)] #![feature(try_blocks)] #![feature(never_type)] -#![feature(btree_drain_filter)] +#![feature(btree_extract_if)] #![feature(decl_macro)] -#![feature(drain_filter)] +#![feature(extract_if)] #![feature(let_chains)] #![feature(type_changing_struct_update)] @@ -22,6 +22,8 @@ // We may want to remove this in the future. #![allow(clippy::needless_lifetimes)] +#![allow(clippy::needless_pass_by_ref_mut)] // see https://github.com/rust-lang/rust-clippy/issues/11179 + pub mod encoder; mod utils; pub mod verifier; diff --git a/prusti-viper/src/utils/mod.rs b/prusti-viper/src/utils/mod.rs index 16afb3574f3..5789127116a 100644 --- a/prusti-viper/src/utils/mod.rs +++ b/prusti-viper/src/utils/mod.rs @@ -36,6 +36,7 @@ pub fn ty_to_string(typ: &ty::TyKind) -> String { &ty::TyKind::Alias(ty::AliasKind::Projection, _) => "projection", &ty::TyKind::Alias(ty::AliasKind::Opaque, _) => "opaque type", &ty::TyKind::Alias(ty::AliasKind::Inherent, _) => "inherent alias type", + &ty::TyKind::Alias(ty::AliasKind::Weak, _) => "weak alias type", &ty::TyKind::Param(_) => "type parameter", &ty::TyKind::Bound(_, _) => "bound type variable", &ty::TyKind::Placeholder(_) => "placeholder type", diff --git a/prusti-viper/src/utils/type_visitor.rs b/prusti-viper/src/utils/type_visitor.rs index e1239d98a37..e5983ce21af 100644 --- a/prusti-viper/src/utils/type_visitor.rs +++ b/prusti-viper/src/utils/type_visitor.rs @@ -7,7 +7,7 @@ use prusti_rustc_interface::hir::Mutability; use prusti_rustc_interface::middle::ty::{ AdtDef, FieldDef, List, ParamTy, Region, AliasKind, AliasTy, Ty, TyCtxt, - TypeFlags, TyKind, IntTy, UintTy, FloatTy, VariantDef, subst::SubstsRef, Const + TypeFlags, TyKind, IntTy, UintTy, FloatTy, VariantDef, GenericArgsRef, Const }; use prusti_rustc_interface::hir::def_id::DefId; @@ -126,7 +126,7 @@ pub trait TypeVisitor<'tcx>: Sized { fn visit_adt( &mut self, adt_def: AdtDef<'tcx>, - substs: SubstsRef<'tcx> + substs: GenericArgsRef<'tcx> ) -> Result<(), Self::Error> { walk_adt(self, adt_def, substs) } @@ -137,7 +137,7 @@ pub trait TypeVisitor<'tcx>: Sized { adt: AdtDef<'tcx>, idx: prusti_rustc_interface::target::abi::VariantIdx, variant: &VariantDef, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> Result<(), Self::Error> { walk_adt_variant(self, variant, substs) } @@ -147,7 +147,7 @@ pub trait TypeVisitor<'tcx>: Sized { &mut self, index: usize, field: &FieldDef, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> Result<(), Self::Error> { walk_field(self, field, substs) } @@ -193,7 +193,7 @@ pub trait TypeVisitor<'tcx>: Sized { fn visit_closure( &mut self, def_id: DefId, - substs: SubstsRef<'tcx> + substs: GenericArgsRef<'tcx> ) -> Result<(), Self::Error> { walk_closure(self, def_id, substs) } @@ -202,7 +202,7 @@ pub trait TypeVisitor<'tcx>: Sized { fn visit_fndef( &mut self, def_id: DefId, - substs: SubstsRef<'tcx> + substs: GenericArgsRef<'tcx> ) -> Result<(), Self::Error> { walk_fndef(self, def_id, substs) } @@ -220,7 +220,7 @@ pub trait TypeVisitor<'tcx>: Sized { pub fn walk_adt<'tcx, E, V: TypeVisitor<'tcx, Error = E>>( visitor: &mut V, adt_def: AdtDef<'tcx>, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> Result<(), E> { for (idx, variant) in adt_def.variants().iter_enumerated() { visitor.visit_adt_variant(adt_def, idx, variant, substs)?; @@ -231,7 +231,7 @@ pub fn walk_adt<'tcx, E, V: TypeVisitor<'tcx, Error = E>>( pub fn walk_adt_variant<'a, 'tcx, E, V: TypeVisitor<'tcx, Error = E>>( visitor: &mut V, variant: &VariantDef, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> Result<(), E> { for (index, field) in variant.fields.iter().enumerate() { visitor.visit_field(index, field, substs)?; @@ -242,7 +242,7 @@ pub fn walk_adt_variant<'a, 'tcx, E, V: TypeVisitor<'tcx, Error = E>>( pub fn walk_field<'a, 'tcx, E, V: TypeVisitor<'tcx, Error = E>>( visitor: &mut V, field: &FieldDef, - substs: SubstsRef<'tcx>, + substs: GenericArgsRef<'tcx>, ) -> Result<(), E> { let ty = field.ty(visitor.tcx(), substs); visitor.visit_ty(ty) @@ -286,7 +286,7 @@ pub fn walk_raw_ptr<'tcx, E, V: TypeVisitor<'tcx, Error = E>>( pub fn walk_closure<'tcx, E, V: TypeVisitor<'tcx, Error = E>>( visitor: &mut V, _def_id: DefId, - substs: SubstsRef<'tcx> + substs: GenericArgsRef<'tcx> ) -> Result<(), E> { let cl_substs = substs.as_closure(); // TODO: when are there bound typevars? can type visitor deal with generics? @@ -303,7 +303,7 @@ pub fn walk_closure<'tcx, E, V: TypeVisitor<'tcx, Error = E>>( pub fn walk_fndef<'tcx, E, V: TypeVisitor<'tcx, Error = E>>( visitor: &mut V, _def_id: DefId, - substs: SubstsRef<'tcx> + substs: GenericArgsRef<'tcx> ) -> Result<(), E> { for ty in substs.types() { visitor.visit_ty(ty)?; diff --git a/prusti/src/callbacks.rs b/prusti/src/callbacks.rs index b622a8b1ad0..bacfd39bc3e 100644 --- a/prusti/src/callbacks.rs +++ b/prusti/src/callbacks.rs @@ -16,7 +16,7 @@ use prusti_rustc_interface::{ query::{ExternProviders, Providers}, ty::TyCtxt, }, - session::Session, + session::{EarlyErrorHandler, Session}, }; #[derive(Default)] @@ -134,6 +134,7 @@ impl prusti_rustc_interface::driver::Callbacks for PrustiCompilerCalls { #[tracing::instrument(level = "debug", skip_all)] fn after_analysis<'tcx>( &mut self, + _error_handler: &EarlyErrorHandler, compiler: &Compiler, queries: &'tcx Queries<'tcx>, ) -> Compilation { diff --git a/prusti/src/driver.rs b/prusti/src/driver.rs index 9e70d900848..5674dd9cf9d 100644 --- a/prusti/src/driver.rs +++ b/prusti/src/driver.rs @@ -18,7 +18,11 @@ use callbacks::PrustiCompilerCalls; use lazy_static::lazy_static; use log::info; use prusti_common::{config, report::user, Stopwatch}; -use prusti_rustc_interface::interface::interface::try_print_query_stack; +use prusti_rustc_interface::{ + errors, + interface::interface::try_print_query_stack, + session::{self, EarlyErrorHandler}, +}; use std::{env, panic}; use tracing_chrome::{ChromeLayerBuilder, FlushGuard}; use tracing_subscriber::{filter::EnvFilter, prelude::*}; @@ -130,7 +134,10 @@ fn init_loggers() -> Option { None }; - prusti_rustc_interface::driver::init_rustc_env_logger(); + let error_handler = EarlyErrorHandler::new(session::config::ErrorOutputType::HumanReadable( + errors::emitter::HumanReadableErrorType::Default(errors::emitter::ColorConfig::Auto), + )); + prusti_rustc_interface::driver::init_rustc_env_logger(&error_handler); guard } diff --git a/rust-toolchain b/rust-toolchain index 4d24b8445a3..bcba639b7a0 100644 --- a/rust-toolchain +++ b/rust-toolchain @@ -1,4 +1,4 @@ [toolchain] -channel = "nightly-2023-06-15" +channel = "nightly-2023-07-20" components = [ "rustc-dev", "llvm-tools-preview", "rust-std", "rustfmt", "clippy" ] profile = "minimal" diff --git a/viper-toolchain b/viper-toolchain index 99decd43dbe..4121e0f6dd9 100644 --- a/viper-toolchain +++ b/viper-toolchain @@ -1 +1 @@ -v-2023-05-17-0733 +v-2023-07-05-0730 diff --git a/vir/src/legacy/ast/common.rs b/vir/src/legacy/ast/common.rs index 31126dbcd08..af82cc68898 100644 --- a/vir/src/legacy/ast/common.rs +++ b/vir/src/legacy/ast/common.rs @@ -111,21 +111,20 @@ impl fmt::Display for PermAmount { impl PartialOrd for PermAmount { fn partial_cmp(&self, other: &PermAmount) -> Option { - match (self, other) { - (PermAmount::Read, PermAmount::Write) => Some(Ordering::Less), - (PermAmount::Read, PermAmount::Read) | (PermAmount::Write, PermAmount::Write) => { - Some(Ordering::Equal) - } - (PermAmount::Write, PermAmount::Read) => Some(Ordering::Greater), - _ => None, - } + Some(self.cmp(other)) } } impl Ord for PermAmount { fn cmp(&self, other: &PermAmount) -> Ordering { - self.partial_cmp(other) - .unwrap_or_else(|| panic!("Undefined comparison between {self:?} and {other:?}")) + match (self, other) { + (PermAmount::Read, PermAmount::Write) => Ordering::Less, + (PermAmount::Read, PermAmount::Read) | (PermAmount::Write, PermAmount::Write) => { + Ordering::Equal + } + (PermAmount::Write, PermAmount::Read) => Ordering::Greater, + _ => panic!("Undefined comparison between {:?} and {:?}", self, other), + } } } diff --git a/vir/src/legacy/ast/function.rs b/vir/src/legacy/ast/function.rs index 092c28bde4f..424a79c9895 100644 --- a/vir/src/legacy/ast/function.rs +++ b/vir/src/legacy/ast/function.rs @@ -47,12 +47,7 @@ impl fmt::Display for Function { impl Function { pub fn inline_body(&self, args: Vec) -> Expr { - let subst: FxHashMap = self - .formal_args - .iter() - .cloned() - .zip(args.into_iter()) - .collect(); + let subst: FxHashMap = self.formal_args.iter().cloned().zip(args).collect(); // TODO: this does not handle let expressions, quantifiers, and so on self.body.clone().unwrap().fold_expr(|orig_expr| { if let Expr::Local(ref local, ref _pos) = orig_expr { diff --git a/vir/src/lib.rs b/vir/src/lib.rs index d7caf3f60a9..413bda3f859 100644 --- a/vir/src/lib.rs +++ b/vir/src/lib.rs @@ -7,6 +7,7 @@ #![deny(unused_variables)] #![deny(unused_doc_comments)] #![warn(clippy::disallowed_types)] +#![allow(clippy::needless_pass_by_ref_mut)] // see https://github.com/rust-lang/rust-clippy/issues/11179 // If only it wasn't generated automatically // so that one could do `clippy --fix`... From 5de4c4e8ca032ef262259b1f9d6dc3b12bebcc5e Mon Sep 17 00:00:00 2001 From: Vytautas Astrauskas Date: Thu, 27 Jul 2023 23:01:48 +0200 Subject: [PATCH 2/3] Fix clippy warnings. --- vir/defs/polymorphic/ast/common.rs | 1 + vir/defs/polymorphic/ast/function.rs | 7 +------ 2 files changed, 2 insertions(+), 6 deletions(-) diff --git a/vir/defs/polymorphic/ast/common.rs b/vir/defs/polymorphic/ast/common.rs index 911b101909a..71abe8eeabb 100644 --- a/vir/defs/polymorphic/ast/common.rs +++ b/vir/defs/polymorphic/ast/common.rs @@ -95,6 +95,7 @@ impl fmt::Display for PermAmount { } } +#[allow(clippy::incorrect_partial_ord_impl_on_ord_type)] impl PartialOrd for PermAmount { fn partial_cmp(&self, other: &PermAmount) -> Option { match (self, other) { diff --git a/vir/defs/polymorphic/ast/function.rs b/vir/defs/polymorphic/ast/function.rs index 91f44d5e3c1..00183c53e23 100644 --- a/vir/defs/polymorphic/ast/function.rs +++ b/vir/defs/polymorphic/ast/function.rs @@ -60,12 +60,7 @@ impl fmt::Display for Function { impl Function { pub fn inline_body(&self, args: Vec) -> Expr { - let subst: FxHashMap = self - .formal_args - .iter() - .cloned() - .zip(args.into_iter()) - .collect(); + let subst: FxHashMap = self.formal_args.iter().cloned().zip(args).collect(); // TODO: this does not handle let expressions, quantifiers, and so on self.body.clone().unwrap().fold_expr(|orig_expr| { if let Expr::Local(Local { ref variable, .. }) = orig_expr { From 7e79b1de0bf6d7fb8f84771fccd2bb0deb3f0b44 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Aurel=20B=C3=ADl=C3=BD?= Date: Thu, 3 Aug 2023 01:36:06 +0200 Subject: [PATCH 3/3] fix UI test, ignore unique borrows unsupported test --- Cargo.lock | 2 +- prusti-tests/tests/verify/fail/unsupported/unique_borrow.rs | 2 ++ .../ui/counterexamples/pure-function-2.stderr | 2 +- prusti-viper/src/encoder/procedure_encoder.rs | 5 ----- viper-toolchain | 2 +- 5 files changed, 5 insertions(+), 8 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index dd0c0cbfdc3..ea72e201ea6 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2395,7 +2395,7 @@ dependencies = [ [[package]] name = "prusti-specs" -version = "0.1.9" +version = "0.1.10" dependencies = [ "itertools 0.11.0", "proc-macro2", diff --git a/prusti-tests/tests/verify/fail/unsupported/unique_borrow.rs b/prusti-tests/tests/verify/fail/unsupported/unique_borrow.rs index 2420d03e6b1..817c3b1b093 100644 --- a/prusti-tests/tests/verify/fail/unsupported/unique_borrow.rs +++ b/prusti-tests/tests/verify/fail/unsupported/unique_borrow.rs @@ -1,3 +1,5 @@ +//ignore-test "unique borrows" no longer exist in MIR, detecting this is more difficult + // Copyright 2016 lazy-static.rs Developers // // Licensed under the Apache License, Version 2.0, $DIR/pure-function-2.rs:29:13 | 29 | let z = y.get_a(); - | ^^^^^^^^^ + | ^ note: counterexample for "z" value: 5 --> $DIR/pure-function-2.rs:29:13 diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs index 00e3d94408b..0607f26a122 100644 --- a/prusti-viper/src/encoder/procedure_encoder.rs +++ b/prusti-viper/src/encoder/procedure_encoder.rs @@ -1664,11 +1664,6 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { /// Generate an unsupported encoding error for unhandled borrow kinds. fn unsupported_borrow_kind(kind: mir::BorrowKind) -> EncodingError { match kind { - mir::BorrowKind::Mut { .. } => { - EncodingError::unsupported( - "unsuported creation of unique borrows (implicitly created in closure bindings)", - ) - } mir::BorrowKind::Shallow => { EncodingError::unsupported( "unsupported creation of shallow borrows (implicitly created when lowering matches)", diff --git a/viper-toolchain b/viper-toolchain index 4121e0f6dd9..99decd43dbe 100644 --- a/viper-toolchain +++ b/viper-toolchain @@ -1 +1 @@ -v-2023-07-05-0730 +v-2023-05-17-0733