diff --git a/Cargo.lock b/Cargo.lock index 677931f67b3..27bcf1aaa9b 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -4,9 +4,9 @@ version = 3 [[package]] name = "addr2line" -version = "0.20.0" +version = "0.21.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f4fa78e18c64fce05e902adecd7a5eed15a5e0a3439f7b0e169f0252214865e3" +checksum = "8a30b2e23b9e17a9f90641c7ab1549cd9b44f296d3ccbf309d2863cfe398a0cb" dependencies = [ "gimli", ] @@ -30,9 +30,9 @@ dependencies = [ [[package]] name = "aho-corasick" -version = "1.0.4" +version = "1.0.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6748e8def348ed4d14996fa801f4122cd763fff530258cdc03f64b25f89d3a5a" +checksum = "0c378d78423fdad8089616f827526ee33c19f2fddbd5de1629152c9593ba4783" dependencies = [ "memchr", ] @@ -70,24 +70,23 @@ dependencies = [ [[package]] name = "anstream" -version = "0.3.2" +version = "0.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0ca84f3628370c59db74ee214b3263d58f9aadd9b4fe7e711fd87dc452b7f163" +checksum = "b1f58811cfac344940f1a400b6e6231ce35171f614f26439e80f8c1465c5cc0c" dependencies = [ "anstyle", "anstyle-parse", "anstyle-query", "anstyle-wincon", "colorchoice", - "is-terminal", "utf8parse", ] [[package]] name = "anstyle" -version = "1.0.1" +version = "1.0.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3a30da5c5f2d5e72842e00bcb57657162cdabef0931f40e2deb9b4140440cecd" +checksum = "15c4c2c83f81532e5845a733998b6971faca23490340a418e9b72a3ec9de12ea" [[package]] name = "anstyle-parse" @@ -109,9 +108,9 @@ dependencies = [ [[package]] name = "anstyle-wincon" -version = "1.0.2" +version = "2.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c677ab05e09154296dd37acecd46420c17b9713e8366facafa8fc0885167cf4c" +checksum = "58f54d10c6dfa51283a066ceab3ec1ab78d13fae00aa49243a45e4571fb79dfd" dependencies = [ "anstyle", "windows-sys 0.48.0", @@ -262,7 +261,7 @@ checksum = "bc00ceb34980c03614e35a3a4e218276a0a824e911d07651cd0d858a51e8c0f0" dependencies = [ "proc-macro2", "quote", - "syn 2.0.29", + "syn 2.0.31", ] [[package]] @@ -294,9 +293,9 @@ checksum = "d468802bab17cbc0cc575e9b053f41e72aa36bfa6b7f55e3529ffa43161b97fa" [[package]] name = "backtrace" -version = "0.3.68" +version = "0.3.69" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4319208da049c43661739c5fade2ba182f09d1dc2299b32298d3a31692b17e12" +checksum = "2089b7e3f35b9dd2d0ed921ead4f6d318c27680d4a5bd167b3ee120edb105837" dependencies = [ "addr2line", "cc", @@ -321,9 +320,9 @@ checksum = "9e1b586273c5702936fe7b7d6896644d8be71e6314cfe09d3167c95f712589e8" [[package]] name = "base64" -version = "0.21.2" +version = "0.21.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "604178f6c5c21f02dc555784810edfb88d34ac2c73b2eae109655649ee73ce3d" +checksum = "414dcefbc63d77c526a76b3afcf6fbb9b5e2791c19c3aa2297733208750c6e53" [[package]] name = "base64ct" @@ -477,32 +476,31 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" [[package]] name = "chrono" -version = "0.4.26" +version = "0.4.28" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ec837a71355b28f6556dbd569b37b3f363091c0bd4b2e735674521b4c5fd9bc5" +checksum = "95ed24df0632f708f5f6d8082675bef2596f7084dee3dd55f632290bf35bfe0f" dependencies = [ "android-tzdata", "iana-time-zone", "num-traits", - "winapi", + "windows-targets 0.48.5", ] [[package]] name = "clap" -version = "4.3.23" +version = "4.4.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "03aef18ddf7d879c15ce20f04826ef8418101c7e528014c3eeea13321047dca3" +checksum = "6a13b88d2c62ff462f88e4a121f17a82c1af05693a2f192b5c38d14de73c19f6" dependencies = [ "clap_builder", "clap_derive", - "once_cell", ] [[package]] name = "clap_builder" -version = "4.3.23" +version = "4.4.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f8ce6fffb678c9b80a70b6b6de0aad31df727623a70fd9a842c30cd573e2fa98" +checksum = "2bb9faaa7c2ef94b2743a21f5a29e6f0010dff4caa69ac8e9d6cf8b6fa74da08" dependencies = [ "anstream", "anstyle", @@ -512,21 +510,21 @@ dependencies = [ [[package]] name = "clap_derive" -version = "4.3.12" +version = "4.4.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "54a9bb5758fc5dfe728d1019941681eccaf0cf8a4189b692a0ee2f2ecf90a050" +checksum = "0862016ff20d69b84ef8247369fabf5c008a7417002411897d40ee1f4532b873" dependencies = [ "heck", "proc-macro2", "quote", - "syn 2.0.29", + "syn 2.0.31", ] [[package]] name = "clap_lex" -version = "0.5.0" +version = "0.5.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2da6da31387c7e4ef160ffab6d5e7f00c42626fe39aea70a7b0f1773f7dd6c1b" +checksum = "cd7cc57abe963c6d3b9d8be5b06ba7c8957a930305ca90304f24ef040aa6f961" [[package]] name = "color-backtrace" @@ -766,11 +764,11 @@ checksum = "f3b7eb4404b8195a9abb6356f4ac07d8ba267045c8d6d220ac4dc992e6cc75df" [[package]] name = "ctrlc" -version = "3.4.0" +version = "3.4.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2a011bbe2c35ce9c1f143b7af6f94f29a167beb4cd1d29e6740ce836f723120e" +checksum = "82e95fbd621905b854affdc67943b043a0fbb6ed7385fd5a25650d19a8a6cfdf" dependencies = [ - "nix 0.26.2", + "nix 0.27.1", "windows-sys 0.48.0", ] @@ -963,9 +961,9 @@ dependencies = [ [[package]] name = "encoding_rs" -version = "0.8.32" +version = "0.8.33" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "071a31f4ee85403370b58aca746f01041ede6f0da2730960ad001edc2b71b394" +checksum = "7268b386296a025e474d5140678f75d6de9493ae55a5d709eeb9dd08149945e1" dependencies = [ "cfg-if", ] @@ -991,9 +989,9 @@ checksum = "5443807d6dff69373d433ab9ef5378ad8df50ca6298caf15de6e52e24aaf54d5" [[package]] name = "errno" -version = "0.3.2" +version = "0.3.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6b30f669a7961ef1631673d2766cc92f52d64f7ef354d4fe0ddfd30ed52f0f4f" +checksum = "136526188508e25c6fef639d7927dfb3e0e3084488bf202267829cf7fc23dbdd" dependencies = [ "errno-dragonfly", "libc", @@ -1213,7 +1211,7 @@ checksum = "89ca545a94061b6365f2c7355b4b32bd20df3ff95f02da9329b34ccc3bd6ee72" dependencies = [ "proc-macro2", "quote", - "syn 2.0.29", + "syn 2.0.31", ] [[package]] @@ -1281,9 +1279,9 @@ dependencies = [ [[package]] name = "gimli" -version = "0.27.3" +version = "0.28.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b6c80984affa11d98d1b88b66ac8853f143217b399d3c74116778ff8fdb4ed2e" +checksum = "6fb8d784f27acf97159b40fc4db5ecd8aa23b9ad5ef69cdd136d3bc80665f0c0" [[package]] name = "git2" @@ -1331,9 +1329,9 @@ dependencies = [ [[package]] name = "h2" -version = "0.3.20" +version = "0.3.21" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "97ec8491ebaf99c8eaa73058b045fe58073cd6be7f596ac993ced0b0a0c01049" +checksum = "91fc23aa11be92976ef4729127f1a74adf36d8436f7816b185d18df956790833" dependencies = [ "bytes", "fnv", @@ -1365,12 +1363,11 @@ checksum = "2c6201b9ff9fd90a5a3bac2e56a830d0caa509576f0e503818ee82c181b3437a" [[package]] name = "headers" -version = "0.3.8" +version = "0.3.9" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f3e372db8e5c0d213e0cd0b9be18be2aca3d44cf2fe30a9d46a65581cd454584" +checksum = "06683b93020a07e3dbcf5f8c0f6d40080d725bea7936fc01ad345c01b97dc270" dependencies = [ - "base64 0.13.1", - "bitflags 1.3.2", + "base64 0.21.3", "bytes", "headers-core", "http", @@ -1597,7 +1594,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "cb0889898416213fab133e1d33a0e5858a48177452750691bde3666d0fdbaf8b" dependencies = [ "hermit-abi", - "rustix 0.38.8", + "rustix 0.38.11", "windows-sys 0.48.0", ] @@ -1785,9 +1782,9 @@ dependencies = [ [[package]] name = "memchr" -version = "2.5.0" +version = "2.6.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2dffe52ecf27772e601905b7522cb4ef790d2cc203488bbd0e2fe85fcb74566d" +checksum = "8f232d6ef707e1956a43342693d2a31e72989554d58299d7a88738cc95b0d35c" [[package]] name = "memoffset" @@ -1928,16 +1925,26 @@ dependencies = [ [[package]] name = "nix" -version = "0.26.2" +version = "0.26.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bfdda3d196821d6af13126e40375cdf7da646a96114af134d5f417a9a1dc8e1a" +checksum = "598beaf3cc6fdd9a5dfb1630c2800c7acd31df7aaf0f565796fba2b53ca1af1b" dependencies = [ "bitflags 1.3.2", "cfg-if", "libc", "memoffset 0.7.1", "pin-utils", - "static_assertions", +] + +[[package]] +name = "nix" +version = "0.27.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2eb04e9c688eff1c89d72b407f168cf79bb9e867a9d3323ed6c01519eb9cc053" +dependencies = [ + "bitflags 2.4.0", + "cfg-if", + "libc", ] [[package]] @@ -1987,9 +1994,9 @@ dependencies = [ [[package]] name = "object" -version = "0.31.1" +version = "0.32.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8bda667d9f2b5051b8833f59f3bf748b28ef54f850f4fcb389a252aa383866d1" +checksum = "9cf5f9dd3933bd50a9e1f149ec995f39ae2c496d31fd772c1fd45ebc27e902b0" dependencies = [ "memchr", ] @@ -2002,11 +2009,11 @@ checksum = "dd8b5dd2ae5ed71462c540258bedcb51965123ad7e7ccf4b9a8cafaa4a63576d" [[package]] name = "openssl" -version = "0.10.56" +version = "0.10.57" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "729b745ad4a5575dd06a3e1af1414bd330ee561c01b3899eb584baeaa8def17e" +checksum = "bac25ee399abb46215765b1cb35bc0212377e58a061560d8b29b024fd0430e7c" dependencies = [ - "bitflags 1.3.2", + "bitflags 2.4.0", "cfg-if", "foreign-types", "libc", @@ -2023,7 +2030,7 @@ checksum = "a948666b637a0f465e8564c73e89d4dde00d72d4d473cc972f390fc3dcee7d9c" dependencies = [ "proc-macro2", "quote", - "syn 2.0.29", + "syn 2.0.31", ] [[package]] @@ -2034,9 +2041,9 @@ checksum = "ff011a302c396a5197692431fc1948019154afc178baf7d8e37367442a4601cf" [[package]] name = "openssl-sys" -version = "0.9.91" +version = "0.9.92" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "866b5f16f90776b9bb8dc1e1802ac6f0513de3a7a7465867bfbc563dc737faac" +checksum = "db7e971c2c2bba161b2d2fdf37080177eff520b3bc044787c7f1f5f9e78d869b" dependencies = [ "cc", "libc", @@ -2133,19 +2140,20 @@ checksum = "9b2a4787296e9989611394c33f193f676704af1686e70b8f8033ab5ba9a35a94" [[package]] name = "pest" -version = "2.7.2" +version = "2.7.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1acb4a4365a13f749a93f1a094a7805e5cfa0955373a9de860d962eaa3a5fe5a" +checksum = "d7a4d085fd991ac8d5b05a147b437791b4260b76326baf0fc60cf7c9c27ecd33" dependencies = [ + "memchr", "thiserror", "ucd-trie", ] [[package]] name = "pest_derive" -version = "2.7.2" +version = "2.7.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "666d00490d4ac815001da55838c500eafb0320019bbaa44444137c48b443a853" +checksum = "a2bee7be22ce7918f641a33f08e3f43388c7656772244e2bbb2477f44cc9021a" dependencies = [ "pest", "pest_generator", @@ -2153,22 +2161,22 @@ dependencies = [ [[package]] name = "pest_generator" -version = "2.7.2" +version = "2.7.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "68ca01446f50dbda87c1786af8770d535423fa8a53aec03b8f4e3d7eb10e0929" +checksum = "d1511785c5e98d79a05e8a6bc34b4ac2168a0e3e92161862030ad84daa223141" dependencies = [ "pest", "pest_meta", "proc-macro2", "quote", - "syn 2.0.29", + "syn 2.0.31", ] [[package]] name = "pest_meta" -version = "2.7.2" +version = "2.7.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "56af0a30af74d0445c0bf6d9d051c979b516a1a5af790d251daee76005420a48" +checksum = "b42f0394d3123e33353ca5e1e89092e533d2cc490389f2bd6131c43c634ebc5f" dependencies = [ "once_cell", "pest", @@ -2192,14 +2200,14 @@ checksum = "4359fd9c9171ec6e8c62926d6faaf553a8dc3f64e1507e76da7911b4f6a04405" dependencies = [ "proc-macro2", "quote", - "syn 2.0.29", + "syn 2.0.31", ] [[package]] name = "pin-project-lite" -version = "0.2.12" +version = "0.2.13" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "12cc1b0bf1727a77a54b6654e7b5f1af8604923edc8b81885f8ec92f9e3f0a05" +checksum = "8afb450f006bf6385ca15ef45d71d2288452bc3683ce2e2cacc0d18e4be60b58" [[package]] name = "pin-utils" @@ -2414,7 +2422,7 @@ dependencies = [ "itertools 0.11.0", "lazy_static", "log", - "nix 0.26.2", + "nix 0.26.4", "rustc-hash", "serde", "toml 0.7.6", @@ -2540,14 +2548,14 @@ dependencies = [ [[package]] name = "regex" -version = "1.9.3" +version = "1.9.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "81bc1d4caf89fac26a70747fe603c130093b53c773888797a6329091246d651a" +checksum = "697061221ea1b4a94a624f67d0ae2bfe4e22b8a17b6a192afb11046542cc8c47" dependencies = [ "aho-corasick", "memchr", - "regex-automata 0.3.6", - "regex-syntax 0.7.4", + "regex-automata 0.3.8", + "regex-syntax 0.7.5", ] [[package]] @@ -2561,13 +2569,13 @@ dependencies = [ [[package]] name = "regex-automata" -version = "0.3.6" +version = "0.3.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fed1ceff11a1dddaee50c9dc8e4938bd106e9d89ae372f192311e7da498e3b69" +checksum = "c2f401f4955220693b56f8ec66ee9c78abffd8d1c4f23dc41a23839eb88f0795" dependencies = [ "aho-corasick", "memchr", - "regex-syntax 0.7.4", + "regex-syntax 0.7.5", ] [[package]] @@ -2578,9 +2586,9 @@ checksum = "f162c6dd7b008981e4d40210aca20b4bd0f9b60ca9271061b07f78537722f2e1" [[package]] name = "regex-syntax" -version = "0.7.4" +version = "0.7.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e5ea92a5b6195c6ef2a0295ea818b312502c6fc94dde986c5553242e18fd4ce2" +checksum = "dbb5fb1acd8a1a18b3dd5be62d25485eb770e05afb408a9627d14d451bae12da" [[package]] name = "remove_dir_all" @@ -2597,11 +2605,11 @@ dependencies = [ [[package]] name = "reqwest" -version = "0.11.18" +version = "0.11.20" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "cde824a14b7c14f85caff81225f411faacc04a2013f41670f41443742b1c1c55" +checksum = "3e9ad3fe7488d7e34558a2033d45a0c90b72d97b4f80705666fea71472e2e6a1" dependencies = [ - "base64 0.21.2", + "base64 0.21.3", "bytes", "encoding_rs", "futures-core", @@ -2630,7 +2638,7 @@ dependencies = [ "wasm-bindgen", "wasm-bindgen-futures", "web-sys", - "webpki-roots 0.22.6", + "webpki-roots 0.25.2", "winreg", ] @@ -2729,9 +2737,9 @@ dependencies = [ [[package]] name = "rustix" -version = "0.38.8" +version = "0.38.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "19ed4fa021d81c8392ce04db050a3da9a60299050b7ae1cf482d862b54a7218f" +checksum = "c0c3dde1fc030af041adc40e79c0e7fbcf431dd24870053d187d7c66e4b87453" dependencies = [ "bitflags 2.4.0", "errno", @@ -2742,13 +2750,13 @@ dependencies = [ [[package]] name = "rustls" -version = "0.21.6" +version = "0.21.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1d1feddffcfcc0b33f5c6ce9a29e341e4cd59c3f78e7ee45f4a40c038b1d6cbb" +checksum = "cd8d6c9f025a446bc4d18ad9632e69aec8f287aa84499ee335599fabd20c3fd8" dependencies = [ "log", "ring", - "rustls-webpki 0.101.3", + "rustls-webpki 0.101.4", "sct", ] @@ -2758,14 +2766,14 @@ version = "1.0.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "2d3987094b1d07b653b7dfdc3f70ce9a1da9c51ac18c1b06b662e4f9a0e9f4b2" dependencies = [ - "base64 0.21.2", + "base64 0.21.3", ] [[package]] name = "rustls-webpki" -version = "0.100.1" +version = "0.100.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d6207cd5ed3d8dca7816f8f3725513a34609c0c765bf652b8c3cb4cfd87db46b" +checksum = "e98ff011474fa39949b7e5c0428f9b4937eda7da7848bbb947786b7be0b27dab" dependencies = [ "ring", "untrusted", @@ -2773,9 +2781,9 @@ dependencies = [ [[package]] name = "rustls-webpki" -version = "0.101.3" +version = "0.101.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "261e9e0888cba427c3316e6322805653c9425240b6fd96cee7cb671ab70ab8d0" +checksum = "7d93931baf2d282fff8d3a532bbfd7653f734643161b87e3e01e59a04439bf0d" dependencies = [ "ring", "untrusted", @@ -2911,22 +2919,22 @@ checksum = "b0293b4b29daaf487284529cc2f5675b8e57c61f70167ba415a463651fd6a918" [[package]] name = "serde" -version = "1.0.185" +version = "1.0.188" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "be9b6f69f1dfd54c3b568ffa45c310d6973a5e5148fd40cf515acaf38cf5bc31" +checksum = "cf9e0fcba69a370eed61bcf2b728575f726b50b55cba78064753d708ddc7549e" dependencies = [ "serde_derive", ] [[package]] name = "serde_derive" -version = "1.0.185" +version = "1.0.188" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "dc59dfdcbad1437773485e0367fea4b090a2e0a16d9ffc46af47764536a298ec" +checksum = "4eca7ac642d82aa35b60049a6eccb4be6be75e599bd2e9adb5f875a737654af2" dependencies = [ "proc-macro2", "quote", - "syn 2.0.29", + "syn 2.0.31", ] [[package]] @@ -3035,9 +3043,9 @@ checksum = "420acb44afdae038210c99e69aae24109f32f15500aa708e81d46c9f29d55fcf" [[package]] name = "slab" -version = "0.4.8" +version = "0.4.9" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6528351c9bc8ab22353f9d776db39a20288e8d6c37ef8cfe3317cf875eecfc2d" +checksum = "8f92a496fb766b417c996b9c5e57daf2f7ad3b0bebe1ccfca4856390e3d3bb67" dependencies = [ "autocfg", ] @@ -3058,9 +3066,9 @@ dependencies = [ [[package]] name = "snapbox" -version = "0.4.11" +version = "0.4.12" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f6bccd62078347f89a914e3004d94582e13824d4e3d8a816317862884c423835" +checksum = "ad90eb3a2e3a8031d636d45bd4832751aefd58a291b553f7305a2bacae21aff3" dependencies = [ "anstream", "anstyle", @@ -3076,9 +3084,9 @@ dependencies = [ [[package]] name = "snapbox-macros" -version = "0.3.4" +version = "0.3.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "eaaf09df9f0eeae82be96290918520214530e738a7fe5a351b0f24cf77c0ca31" +checksum = "95f4ffd811b87da98d0e48285134b7847954bd76e843bb794a893b47ca3ee325" dependencies = [ "anstream", ] @@ -3125,12 +3133,6 @@ dependencies = [ "der", ] -[[package]] -name = "static_assertions" -version = "1.1.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a2eb9349b6444b326872e140eb1cf5e7c522154d69e7a0ffb0fb81c06b37543f" - [[package]] name = "strsim" version = "0.10.0" @@ -3156,9 +3158,9 @@ dependencies = [ [[package]] name = "syn" -version = "2.0.29" +version = "2.0.31" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c324c494eba9d92503e6f1ef2e6df781e78f6a7705a0202d9801b198807d518a" +checksum = "718fa2415bcb8d8bd775917a1bf12a7931b6dfa890753378538118181e0cb398" dependencies = [ "proc-macro2", "quote", @@ -3210,7 +3212,7 @@ dependencies = [ "cfg-if", "fastrand 2.0.0", "redox_syscall 0.3.5", - "rustix 0.38.8", + "rustix 0.38.11", "windows-sys 0.48.0", ] @@ -3267,22 +3269,22 @@ dependencies = [ [[package]] name = "thiserror" -version = "1.0.47" +version = "1.0.48" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "97a802ec30afc17eee47b2855fc72e0c4cd62be9b4efe6591edde0ec5bd68d8f" +checksum = "9d6d7a740b8a666a7e828dd00da9c0dc290dff53154ea77ac109281de90589b7" dependencies = [ "thiserror-impl", ] [[package]] name = "thiserror-impl" -version = "1.0.47" +version = "1.0.48" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6bb623b56e39ab7dcd4b1b98bb6c8f8d907ed255b18de254088016b27a8ee19b" +checksum = "49922ecae66cc8a249b77e68d1d0623c1b2c514f0060c27cdc68bd62a1219d35" dependencies = [ "proc-macro2", "quote", - "syn 2.0.29", + "syn 2.0.31", ] [[package]] @@ -3297,9 +3299,9 @@ dependencies = [ [[package]] name = "time" -version = "0.3.25" +version = "0.3.28" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b0fdd63d58b18d663fbdf70e049f00a22c8e42be082203be7f26589213cd75ea" +checksum = "17f6bb557fd245c28e6411aa56b6403c689ad95061f50e4be16c274e70a17e48" dependencies = [ "deranged", "itoa", @@ -3316,9 +3318,9 @@ checksum = "7300fbefb4dadc1af235a9cef3737cea692a9d97e1b9cbcd4ebdae6f8868e6fb" [[package]] name = "time-macros" -version = "0.2.11" +version = "0.2.14" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "eb71511c991639bb078fd5bf97757e03914361c48100d52878b8e52b46fb92cd" +checksum = "1a942f44339478ef67935ab2bbaec2fb0322496cf3cbe84b261e06ac3814c572" dependencies = [ "time-core", ] @@ -3480,7 +3482,7 @@ checksum = "5f4f31f56159e98206da9efd823404b79b6ef3143b4a7ab76e67b1751b25a4ab" dependencies = [ "proc-macro2", "quote", - "syn 2.0.29", + "syn 2.0.31", ] [[package]] @@ -3572,9 +3574,9 @@ checksum = "ed646292ffc8188ef8ea4d1e0e0150fb15a5c2e12ad9b8fc191ae7a8a7f3c4b9" [[package]] name = "unicase" -version = "2.6.0" +version = "2.7.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "50f37be617794602aabbeee0be4f259dc1778fabe05e2d67ee8f79326d5cb4f6" +checksum = "f7d2d4dafb69621809a81864c9c1b864479e1235c0dd4e199924b9742439ed89" dependencies = [ "version_check", ] @@ -3624,21 +3626,21 @@ version = "2.7.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0b11c96ac7ee530603dcdf68ed1557050f374ce55a5a07193ebf8cbc9f8927e9" dependencies = [ - "base64 0.21.2", + "base64 0.21.3", "flate2", "log", "once_cell", "rustls", - "rustls-webpki 0.100.1", + "rustls-webpki 0.100.2", "url", "webpki-roots 0.23.1", ] [[package]] name = "url" -version = "2.4.0" +version = "2.4.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "50bff7831e19200a85b17131d085c25d7811bc4e186efdaf54bbd132994a88cb" +checksum = "143b538f18257fac9cad154828a57c6bf5157e1aa604d4816b5995bf6de87ae5" dependencies = [ "form_urlencoded", "idna", @@ -3848,7 +3850,7 @@ dependencies = [ "once_cell", "proc-macro2", "quote", - "syn 2.0.29", + "syn 2.0.31", "wasm-bindgen-shared", ] @@ -3882,7 +3884,7 @@ checksum = "54681b18a46765f095758388f2d0cf16eb8d4169b639ab575a8f5693af210c7b" dependencies = [ "proc-macro2", "quote", - "syn 2.0.29", + "syn 2.0.31", "wasm-bindgen-backend", "wasm-bindgen-shared", ] @@ -3903,33 +3905,20 @@ dependencies = [ "wasm-bindgen", ] -[[package]] -name = "webpki" -version = "0.22.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f095d78192e208183081cc07bc5515ef55216397af48b873e5edcd72637fa1bd" -dependencies = [ - "ring", - "untrusted", -] - [[package]] name = "webpki-roots" -version = "0.22.6" +version = "0.23.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b6c71e40d7d2c34a5106301fb632274ca37242cd0c9d3e64dbece371a40a2d87" +checksum = "b03058f88386e5ff5310d9111d53f48b17d732b401aeb83a8d5190f2ac459338" dependencies = [ - "webpki", + "rustls-webpki 0.100.2", ] [[package]] name = "webpki-roots" -version = "0.23.1" +version = "0.25.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b03058f88386e5ff5310d9111d53f48b17d732b401aeb83a8d5190f2ac459338" -dependencies = [ - "rustls-webpki 0.100.1", -] +checksum = "14247bb57be4f377dfb94c72830b8ce8fc6beac03cf4bf7b9732eadd414123fc" [[package]] name = "wildmatch" @@ -4169,20 +4158,21 @@ checksum = "ed94fce61571a4006852b7389a063ab983c02eb1bb37b47f8272ce92d06d9538" [[package]] name = "winnow" -version = "0.5.14" +version = "0.5.15" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d09770118a7eb1ccaf4a594a221334119a44a814fcb0d31c5b85e83e97227a97" +checksum = "7c2e3184b9c4e92ad5167ca73039d0c42476302ab603e2fec4487511f38ccefc" dependencies = [ "memchr", ] [[package]] name = "winreg" -version = "0.10.1" +version = "0.50.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "80d0f4e272c85def139476380b12f9ac60926689dd2e01d4923222f40580869d" +checksum = "524e57b2c537c0f9b1e69f1965311ec12182b4122e45035b1508cd24d2adadb1" dependencies = [ - "winapi", + "cfg-if", + "windows-sys 0.48.0", ] [[package]] diff --git a/docs/user-guide/src/SUMMARY.md b/docs/user-guide/src/SUMMARY.md index 10edf7c0b80..a8f6239eab8 100644 --- a/docs/user-guide/src/SUMMARY.md +++ b/docs/user-guide/src/SUMMARY.md @@ -17,6 +17,7 @@ - [Final Code](tour/final.md) - [Loop Invariants](tour/loop_invariants.md) - [Counterexamples](tour/counterexamples.md) + - [`prusti-std` and External Specifications](tour/extern_specs.md) - [Verification Features](verify/summary.md) - [Absence of panics](verify/panic.md) - [Overflow checks](verify/overflow.md) diff --git a/docs/user-guide/src/tour/extern_specs.md b/docs/user-guide/src/tour/extern_specs.md new file mode 100644 index 00000000000..1c0dfa80ef7 --- /dev/null +++ b/docs/user-guide/src/tour/extern_specs.md @@ -0,0 +1,42 @@ +# `prusti-std` and External Specifications + +In the previous chapters, the code we verified included calls to functions provided by the standard library, such as `std::mem::replace`. Prusti verifies code in a *function modular* fashion, so it only considers the specification of a function in order to verify a call to it. By default, external functions are assumed to have the contract `#[requires(true)]`, `#[ensures(true)]`, i.e. it is always possible to call the function, but it does not guarantee anything. + +`prusti-std` is a crate that is part of the Prusti project. It provides specifications for some standard library methods. It does not provide specifications for *all* standard library methods, but the aim is to provide a high coverage of calls, based on data found in real Rust code, evaluated on the top crates of `crates.io`. + +The documentation of `prusti-std` provides an overview of the specified methods, as well as informal descriptions of the contracts. + +## Creating new external specifications + +When the specification for an external method is not provided (for example, because it is not in `prusti-std`), it is likely that verification of code using that method will fail. To provide the contract for an external method, an [*external specification*](../verify/external.md) should be declared. + +For the sake of example, assume the `std::mem::replace` method was *not* specified in `prusti-std`. We could provide an external specification for it like so: + +```rust,ignore +#[extern_spec(std::mem)] +#[ensures(snap(dest) === src)] +#[ensures(result === old(snap(dest)))] +fn replace(dest: &mut T, src: T) -> T; +``` + +Let's break this snippet down step by step: +- First, we write the Prusti annotation `#[extern_spec]` to denote that we are writing an external specification. This requires `prusti_contracts::*` to be imported first. +- Next, we need to declare where the original function is located. In this case it is the module `std::mem`, so we put its path in the parameter: `#[extern_spec(std::mem)]` +- After a quick search for *\"rust std mem replace\"* we can find the [documentation for std::mem::replace](https://doc.rust-lang.org/std/mem/fn.replace.html). Here we can get the function signature: `pub fn replace(dest: &mut T, src: T) -> T`. We then write down the signature in the inner module, followed by a `;`. The visibility modifier is omitted for external specifications. +- Since there are no preconditions to `replace`, we can use the (implicit) default `#[requires(true)]`. +- For writing the postcondition, we use four pieces of Prusti syntax: + - [`===`](../syntax.md#snapshot-equality) is called **snapshot equality** or **logical equality**. Is means that the left and right operands are structurally equal. `===` does not require the type of the compared elements to implement [PartialEq](https://doc.rust-lang.org/std/cmp/trait.PartialEq.html), which would be required if we used the standard equality operator `==`. + - The [`snap()`](../syntax.md#snap-function) function takes a snapshot of a reference. It has a similar functionality to the [`clone()`](https://doc.rust-lang.org/std/clone/trait.Clone.html) method, but does not require the type of the reference it is called on to implement the `Clone` trait. `snap` should only be used in specifications, since it ignores the borrow checker. + - Lastly, we have the [`old()` function](../syntax.md#old-expressions), which denotes that we want to refer to the state of `snap(dest)` from before the function was called. + - The identifier [`result`](../syntax.md#result-variable) is used to refer to the return parameter of the function. +- The postcondition consists of two parts, which can either be written in one condition with `&&`, or in multiple `#[ensures(...)]` annotations like in the example above. + - The first condition `snap(dest) === src` means: *After the function returns, the location referenced by `dest` is structurally equal to the parameter `src`.* + - The second part of the postcondition is `result === old(snap(dest))`. This means: *The `result` returned by the function is structurally equal to the the element that was referenced by `dest` **before** the function was called.* + +Since `result` is structurally equal to `dest` from before the function call, Prusti knows that the pure function `len()` called on `result` returns the same value as it would have for `dest`. + +An important thing to note here is that Prusti does ***not*** check if `replace` actually does what the external specification says it does. `#[extern_spec]` implicitly implies the `#[trusted]` annotation, which means that any postconditions are just accepted and used by Prusti. + +### Future + +There is currently new functionality planned for Prusti-assistant, which should enable the user to automatically generate the `extern_spec` declaration for a given call. diff --git a/docs/user-guide/src/tour/option.md b/docs/user-guide/src/tour/option.md index 77281396469..b22e46eca18 100644 --- a/docs/user-guide/src/tour/option.md +++ b/docs/user-guide/src/tour/option.md @@ -10,12 +10,6 @@ Just like in the "Learning Rust With Entirely Too Many Linked Lists" tutorial, w type Link = Option>; ``` -In order to use the `Option::take` function, we also have to implement the `extern_spec` for it. As you can see, it is quite similar to the `extern_spec` for `mem::replace`, since `take` does the same as `replace(&mut self, None)`: - -```rust,noplaypen -{{#rustdoc_include ../../../../prusti-tests/tests/verify/pass/user-guide/option.rs:option_take_extern_spec}} -``` - Changing the `Link` type requires some adjustments of the code and specifications. With the new type alias for `Link`, we cannot have an `impl Link` block anymore, so our `lookup` and `len` functions on `Link` are now normal, free-standing functions: ```rust,noplaypen @@ -31,6 +25,9 @@ Due to current limitations of Prusti, we cannot replace our `link_len` and `link ``` Since Prusti doesn't fully support closures yet, we also cannot do the rewrite to use the `Option::map` function: + + + ```rust,noplaypen {{#rustdoc_include ../../../../prusti-tests/tests/verify/pass/user-guide/option.rs:try_pop_rewrite}} ``` @@ -41,4 +38,4 @@ If you want to see the full code after all the changes, expand the following cod ```rust,noplaypen // Expand to see full code up to this chapter {{#rustdoc_include ../../../../prusti-tests/tests/verify/pass/user-guide/option.rs:nothing}} -``` \ No newline at end of file +``` diff --git a/docs/user-guide/src/tour/pop.md b/docs/user-guide/src/tour/pop.md index e5c494684c6..58182a1288d 100644 --- a/docs/user-guide/src/tour/pop.md +++ b/docs/user-guide/src/tour/pop.md @@ -45,18 +45,6 @@ Since we will need to check if a list is empty, we can implement a `#[pure]` fun {{#rustdoc_include ../../../../prusti-tests/tests/verify/fail/user-guide/pop.rs:is_empty}} ``` -### Writing the external specifications for `Option` - -Since we use `Option::unwrap`, we will need an external specification for it. While we're at it, let's also write the `#[extern_spec]` for `Option::is_some` and `Option::is_none`: - -```rust,noplaypen -{{#rustdoc_include ../../../../prusti-tests/tests/verify/pass/user-guide/pop.rs:extern_spec}} -``` - -The syntax for writing external specifications for functions associated with `Option` is slightly different to that of `std::mem::replace`, which was a standalone function. - -Note: In the future, you should just be able to import these external specifications using the [`prusti-std` crate](https://crates.io/crates/prusti-std). It should be available after [this PR](https://github.com/viperproject/prusti-dev/pull/1249) is merged. Until then, you can find the work in progress specifications in the PR (e.g., for [`Option::unwrap`](https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49)). - ## Implementing the specification ### Writing the precondition diff --git a/docs/user-guide/src/tour/push.md b/docs/user-guide/src/tour/push.md index 250a5cb7c25..20114500e4d 100644 --- a/docs/user-guide/src/tour/push.md +++ b/docs/user-guide/src/tour/push.md @@ -44,79 +44,20 @@ pure method `len` introduced in the [previous chapter](new.md): ```rust,noplaypen {{#rustdoc_include ../../../../prusti-tests/tests/verify/pass/user-guide/push_property_1.rs:property_1}} +// Prusti: Verifies ``` -Even though the above implementation of `push` is correct, attempting to verify it with Prusti still yields a verification error: - -```plain -[Prusti: verification error] postcondition might not hold. -``` - -This error may look surprising at first: -We create a new list node that stores the the original list in its next field. -Why is Prusti unable to realize that the length of the resulting list -is one plus the length of the original list? - -The explanation is that Prusti performs *function modular* verification, -that is, it only uses a function's specification (instead of also consulting the -function's implementation) whenever it encounters a function call. -The only exception are *pure* functions, such as `len`, where Prusti also takes the -function body into account. - - - -### Adding external specifications to library code - -In our case, the function `std::mem::replace` is neither marked as `pure` nor does it -come with a specification. Hence, Prusti assumes that it is memory safe and nothing else. -That is, Prusti uses `true` as both pre- and postcondition of `replace`, -which is too weak to prove the specification of `push`. According to its specification, -`replace` could arbitrarily change the original list and thus also its length. -Hence, we cannot conclude that the length the list returned by -`replace(&mut self.head, Link::Empty)` coincides with the length of the original -list. - -We can remedy this issue by strengthening the specification of `replace`. -In this tutorial, we will assume that the standard library is correct, that is, we -do not attempt to verify specifications for functions in external crates, -like `replace`. To this end, we have to add the specification to the function. -This can be done with another piece of Prusti syntax, the [extern_spec](../verify/external.md): - -```rust,noplaypen -{{#rustdoc_include ../../../../prusti-tests/tests/verify/pass/user-guide/push_property_1.rs:extern_spec}} -``` - -Let's break this snippet down step by step: -- First, we write the Prusti annotation `#[extern_spec]` to denote that we are writing an external specification. This requires `prusti_contracts::*` to be imported first. -- Next, we need to declare where the original function is located. In this case it is the module `std::mem`, so we put its path in the parameter: `#[extern_spec(std::mem)]` -- After a quick search for *\"rust std mem replace\"* we can find the [documentation for std::mem::replace](https://doc.rust-lang.org/std/mem/fn.replace.html). Here we can get the function signature: `pub fn replace(dest: &mut T, src: T) -> T`. We then write down the signature in the inner module, followed by a `;`. -- Since there are no preconditions to `replace`, we can use the (implicit) default `#[requires(true)]`. -- For writing the postcondition, we use four pieces of Prusti syntax: - - [`===`](../syntax.md#snapshot-equality) is called **snapshot equality** or **logical equality**. Is means that the left and right operands are structurally equal. `===` does not require the type of the compared elements to implement [PartialEq](https://doc.rust-lang.org/std/cmp/trait.PartialEq.html), which would be required if we used the standard equality operator `==`. - - The [`snap()`](../syntax.md#snap-function) function takes a snapshot of a reference. It has a similar functionality to the [`clone()`](https://doc.rust-lang.org/std/clone/trait.Clone.html) method, but does not require the type of the reference it is called on to implement the `Clone` trait. `snap` should only be used in specifications, since it ignores the borrow checker. - - Lastly, we have the [`old()` function](../syntax.md#old-expressions), which denotes that we want to refer to the state of `snap(dest)` from before the function was called. - - The identifier [`result`](../syntax.md#result-variable) is used to refer to the return parameter of the function. -- The postcondition consists of two parts, which can either be written in one condition with `&&`, or in multiple `#[ensures(...)]` annotations like in the example above. - - The first condition `snap(dest) === src` means: *After the function returns, the location referenced by `dest` is structurally equal to the parameter `src`* - - The second part of the postcondition is `result === old(snap(dest))`. This means: *The `result` returned by the function is structurally equal to the the element that was referenced by `dest` **before** the function was called.* - -Since `result` is structurally equal to `dest` from before the function call, Prusti knows that the pure function `len()` called on `result` returns the same value as it would have for `dest`. - - -An important thing to note here is that Prusti does ***not*** check if `replace` actually does what the external specification says it does. `#[extern_spec]` implicitly implies the `#[trusted]` annotation, which means that any postconditions are just accepted and used by Prusti. - -### Future +With this, the first of the three properties of `push` is verified, but we still have two more to prove. -There is currently new functionality planned for Prusti-assistant, which should enable the user to automatically generate parts of the `extern_spec` syntax. +## Note about external specifications -There is also work being done for providing external specifications for the Rust standard library. Depending on when you are reading this, the `std::mem::replace` function might be annotated already, in that case this `extern_spec` may not be needed anymore. -You can track the progress and find some already completed specifications [in this Pull Request](https://github.com/viperproject/prusti-dev/pull/1249). +Prusti verifies the above implementation of `push`, but this might come as a surprise: the implementation calls the standard library method `std::mem::replace`. How does Prusti know what this method does? Prusti performs *function modular* verification, so calls to other methods only use that method's specifications, and never its implementation (which may not even be available, or may use unsupported features). -Specifications for the standard library should eventually be available in the [prusti-std crate](https://crates.io/crates/prusti-std). Any specifications in this crate will be available by adding it to your project's dependencies. +The answer is that the `prusti-std` crate provides specifications for *some* of the most common standard library methods, including `std::mem::replace`. In situations where `prusti-std` does not (yet) provide a suitable specification for a method used in the code, an *external specification* must be declared. Creating external specifications is discussed in the [`prusti-std` and External Specifications](extern_specs.md) chapter of this guide. ## Trusted functions -As mentioned above, `extern_specs` are implicitly `#[trusted]` by Prusti. +External specifications, like the one for `std::mem::replace` provided by `prusti-std`, are implicitly `#[trusted]` by Prusti. Trusted functions can be used for verifying projects containing external code that does not have Prusti annotations, or projects using Rust features that are not yet supported by Prusti. An example is printing a string slice (not supported yet): ```rust,noplaypen @@ -156,17 +97,6 @@ This one is even worse, it will enable anything to be verified: fn wrong() {} ``` -### Checking the `extern_spec` - -Let's get back to our code. After adding the external specification for `std::mem::replace`, we can finally verify the first property of our `push` function: - -```rust,noplaypen -{{#rustdoc_include ../../../../prusti-tests/tests/verify/pass/user-guide/push_property_1.rs:property_1}} -// Prusti: Verifies -``` - -With this, the first of the three properties of `push` is verified, but we still have two more to prove. - ## Second property Recall the second property of our specification: @@ -203,9 +133,6 @@ We don't need to add the condition `0 <= index`, since `index` has the type `usi After these changes, Prusti can successfully verify the code, so the first two properties of `push` are correct. - - - ## Third property The third and final property we will verify for `push` is that the original list diff --git a/docs/user-guide/src/tour/setup.md b/docs/user-guide/src/tour/setup.md index ea0e2171e91..74d9fd4d426 100644 --- a/docs/user-guide/src/tour/setup.md +++ b/docs/user-guide/src/tour/setup.md @@ -18,10 +18,10 @@ cargo add prusti-contracts For older versions of Rust, you can manually add the dependency in your Cargo.toml file: ```toml [dependencies] -prusti-contracts = "0.1.6" +prusti-contracts = "0.1" ``` -To use prusti-contracts in a Rust code file, just add the following line: +To use `prusti-contracts` in a Rust code file, just add the following line: ```rust,ignore use prusti_contracts::*; ``` @@ -37,9 +37,9 @@ check_overflows = false -## Standard library annotations +## Standard library specifications -Annotations for functions and types in the Rust standard library will be available in the [`prusti-std` crate](https://crates.io/crates/prusti-std) after [this PR](https://github.com/viperproject/prusti-dev/pull/1249) is merged. +Specifications for functions and types in the Rust standard library are provided in the [`prusti-std` crate](https://crates.io/crates/prusti-std). Adding this crate works the same as for the `prusti-contracts` crate: ```sh @@ -48,6 +48,11 @@ cargo add prusti-std or: ```toml [dependencies] -prusti-std = "0.1.6" +prusti-std = "0.1" +``` + +To make the specifications available when using `cargo prusti`, the following line also needs to be added to the crate: + +```rust,ignore +use prusti_std; ``` -You do not need to import anything to use the annotations in this crate in a file. diff --git a/docs/user-guide/src/tour/summary.md b/docs/user-guide/src/tour/summary.md index 2f3c4bd7534..3eb78053031 100644 --- a/docs/user-guide/src/tour/summary.md +++ b/docs/user-guide/src/tour/summary.md @@ -49,3 +49,4 @@ are as follows: 11. [Final Code](final.md): Final code for the verified linked list 12. [Loop Invariants](loop_invariants.md): Verifying code containing loops by writing loop invariants 13. [Counterexamples](counterexamples.md): Getting counterexamples for failing assertions +14. [`prusti-std` and External Specifications](extern_specs.md): Specifications for the Rust standard library, specifying external methods diff --git a/prusti-contracts/prusti-contracts-proc-macros/Cargo.toml b/prusti-contracts/prusti-contracts-proc-macros/Cargo.toml index 29ec7cf3746..bed0a26fb3a 100644 --- a/prusti-contracts/prusti-contracts-proc-macros/Cargo.toml +++ b/prusti-contracts/prusti-contracts-proc-macros/Cargo.toml @@ -16,7 +16,7 @@ proc-macro = true [dependencies] prusti-specs = { path = "../prusti-specs", version = "0.2.0", optional = true } -proc-macro2 = { version = "1.0", optional = true } +proc-macro2 = { version = "1.0.60", optional = true } [features] # Are we being compiled by Prusti and should include dependency on diff --git a/prusti-contracts/prusti-contracts/src/core_spec.rs b/prusti-contracts/prusti-contracts/src/core_spec.rs deleted file mode 100644 index 61fa73e42b8..00000000000 --- a/prusti-contracts/prusti-contracts/src/core_spec.rs +++ /dev/null @@ -1,18 +0,0 @@ -use crate::*; - -#[extern_spec] -impl ::core::result::Result { - #[pure] - #[ensures(result == matches!(self, Ok(_)))] - fn is_ok(&self) -> bool; - - #[pure] - #[ensures(result == matches!(self, Err(_)))] - fn is_err(&self) -> bool; -} - -#[extern_spec] -impl ::core::result::Result { - #[requires(matches!(self, Ok(_)))] - fn unwrap(self) -> T; -} diff --git a/prusti-contracts/prusti-contracts/src/core_spec/clone.rs b/prusti-contracts/prusti-contracts/src/core_spec/clone.rs new file mode 100644 index 00000000000..c8cb089e499 --- /dev/null +++ b/prusti-contracts/prusti-contracts/src/core_spec/clone.rs @@ -0,0 +1,12 @@ +use crate::*; + +#[extern_spec] +trait Clone { + #[refine_spec(where Self: SnapshotEqualClone, [ + ensures(result === self), + ])] + fn clone(&self) -> Self; +} + +/// Specifies that `Clone::clone`, if implemented, preserves snapshot equality (`===`). +pub auto trait SnapshotEqualClone {} diff --git a/prusti-contracts/prusti-contracts/src/core_spec/convert.rs b/prusti-contracts/prusti-contracts/src/core_spec/convert.rs new file mode 100644 index 00000000000..b55e81856dc --- /dev/null +++ b/prusti-contracts/prusti-contracts/src/core_spec/convert.rs @@ -0,0 +1,77 @@ +use crate::*; + +/// Specifies that `From::from`, if implemented, is a pure method, allowing its usage in specs. +/// This enables specifying the blanket impl of `Into` as calling `From::from`. +/// +/// Does not apply to types that do not implement `Copy`, since pure methods can only involve `Copy` types. +pub auto trait PureFrom {} + +#[extern_spec] +trait From { + #[refine_spec(where Self: Copy + PureFrom, T: Copy, [pure])] + fn from(other: T) -> Self; +} + +#[extern_spec] +impl Into for T +where + U: From, +{ + // When From is pure, we can use it to specify the behavior of Into + #[refine_spec(where U: Copy + PureFrom, T: Copy, [ + pure, + ensures(result === U::from(self)) + ])] + // FUTURE(where_equality): we can specify the behavior of Into for identity conversions even if impure, but for that we need equality constraints + // #[refine_spec(where T = U, [ensures(result === self)])] + fn into(self) -> U; +} + +// identity conversion +#[extern_spec] +impl From for T { + #[ensures(result === other)] + #[refine_spec(where T: Copy, [pure])] + fn from(other: T) -> Self; +} + +// numeric conversions + +// specifies From for lossless numeric conversions using as casts +macro_rules! specify_numeric_from { + ($from:ty => $($to:ty)*) => ($( + #[extern_spec] + impl From<$from> for $to { + #[pure] + #[ensures(result == num as Self)] + fn from(num: $from) -> Self; + } + )*) +} + +specify_numeric_from!(bool => u8 i8 u16 i16 u32 i32 u64 i64 usize isize); + +specify_numeric_from!(u8 => u16 i16 u32 i32 u64 i64 usize); +specify_numeric_from!(u16 => u32 i32 u64 i64); +specify_numeric_from!(u32 => u64 i64); +specify_numeric_from!(i8 => i16 i32 i64 isize); +specify_numeric_from!(i16 => i32 i64); +specify_numeric_from!(i32 => i64); +// size is not guaranteed to be at least 32 or at most 64 bits, so not valid for many conversions one might expect + +// int-to-float conversions are exact when the int type has at most as many bits as the float's mantissa +specify_numeric_from!(u8 => f32 f64); +specify_numeric_from!(u16 => f32 f64); +specify_numeric_from!(u32 => f64); +specify_numeric_from!(i8 => f32 f64); +specify_numeric_from!(i16 => f32 f64); +specify_numeric_from!(i32 => f64); + +specify_numeric_from!(f32 => f64); + +#[cfg(version("1.26"))] +specify_numeric_from!(i16 => isize); +#[cfg(version("1.26"))] +specify_numeric_from!(u16 => usize); +#[cfg(version("1.26"))] +specify_numeric_from!(u8 => isize); diff --git a/prusti-contracts/prusti-contracts/src/core_spec/default.rs b/prusti-contracts/prusti-contracts/src/core_spec/default.rs new file mode 100644 index 00000000000..f5dc47ca1ac --- /dev/null +++ b/prusti-contracts/prusti-contracts/src/core_spec/default.rs @@ -0,0 +1,83 @@ +use crate::*; + +#[extern_spec] +trait Default { + #[refine_spec(where Self: Copy + PureDefault, [pure])] + fn default() -> Self; +} + +/// Specifies that `Default::default`, if implemented, is a pure method, allowing its usage in specs. +/// +/// Does not apply to types that do not implement `Copy`, since pure methods can only involve `Copy` types. +pub auto trait PureDefault {} + +// analogous to https://github.com/rust-lang/rust/blob/872631d0f0fadffe3220ab1bd9c8f1f2342341e2/library/core/src/default.rs#L190-L202 +macro_rules! default_spec { + ($t:ty, $v:expr) => { + #[extern_spec] + impl Default for $t { + #[pure] + #[ensures(snapshot_equality(result, $v))] + fn default() -> Self; + } + }; +} + +default_spec! { (), () } +default_spec! { bool, false } +default_spec! { char, '\x00' } + +default_spec! { usize, 0 } +default_spec! { u8, 0 } +default_spec! { u16, 0 } +default_spec! { u32, 0 } +default_spec! { u64, 0 } +default_spec! { u128, 0 } + +default_spec! { isize, 0 } +default_spec! { i8, 0 } +default_spec! { i16, 0 } +default_spec! { i32, 0 } +default_spec! { i64, 0 } +default_spec! { i128, 0 } + +default_spec! { f32, 0.0f32 } +default_spec! { f64, 0.0f64 } + +// specify behavior for tuples (have to rely on PureDefault) + +// recursive like https://github.com/rust-lang/rust/blob/a5fa99eed20a46a88c0c85eed6552a94b6656634/library/core/src/tuple.rs#L10 +macro_rules! specify_tuple_default { + (impl $( $T:ident )*) => { + #[extern_spec] + impl<$($T,)*> Default for ($($T,)*) where + $($T: Default,)* + { + #[refine_spec(where + $($T: Copy + PureDefault,)* + [ + pure, + ensures(snapshot_equality(&result, &($($T::default(),)*))), + ])] + fn default() -> Self; + } + }; + (impls $T:ident $( $U:ident )+) => { + specify_tuple_default!(impl $T $($U)+); + specify_tuple_default!(impls $($U)+); + }; + (impls $T:ident) => { + specify_tuple_default!(impl $T); + }; +} + +specify_tuple_default!(impls E D C B A Z Y X W V U T); + +// more specific types + +#[extern_spec] +impl Default for Option { + #[refine_spec(where Self: Copy, [pure])] + #[ensures(result.is_none())] + fn default() -> Self; +} diff --git a/prusti-contracts/prusti-contracts/src/core_spec/mem.rs b/prusti-contracts/prusti-contracts/src/core_spec/mem.rs new file mode 100644 index 00000000000..c14919f14b8 --- /dev/null +++ b/prusti-contracts/prusti-contracts/src/core_spec/mem.rs @@ -0,0 +1,92 @@ +use crate::*; + +#[extern_spec(core)] +mod mem { + #[pure] + #[refine_spec(where T: KnownSize, [ensures(result == T::size())])] + fn size_of() -> usize; + + #[pure] + #[refine_spec(where T: KnownSize, [ensures(result == T::align())])] + fn align_of() -> usize; + + #[ensures(*x === old(snap(y)) && *y === old(snap(x)))] + fn swap(x: &mut T, y: &mut T); + + #[ensures(snap(dest) === src)] + #[ensures(result === old(snap(dest)))] + fn replace(dest: &mut T, src: T) -> T; +} + +pub trait KnownSize { + #[pure] + fn size() -> usize; + + #[pure] + fn align() -> usize; +} + +macro_rules! known_size_spec { + ($t:ty, $size:expr, $align:expr) => { + #[refine_trait_spec] + impl KnownSize for $t { + #[pure] + fn size() -> usize { + $size + } + + #[pure] + fn align() -> usize { + $align + } + } + }; + ($t:ty, $size:expr) => { + known_size_spec!($t, $size, $size); + }; +} + +known_size_spec!(bool, 1); + +known_size_spec!(i8, 1); +known_size_spec!(i16, 2); +known_size_spec!(i32, 4); +known_size_spec!(i64, 8); +known_size_spec!(i128, 16); + +known_size_spec!(u8, 1); +known_size_spec!(u16, 2); +known_size_spec!(u32, 4); +known_size_spec!(u64, 8); +known_size_spec!(u128, 16); + +known_size_spec!(f32, 4); +known_size_spec!(f64, 8); + +#[cfg(target_pointer_width = "16")] +known_size_spec!(usize, 2); +#[cfg(target_pointer_width = "16")] +known_size_spec!(isize, 2); + +#[cfg(target_pointer_width = "32")] +known_size_spec!(usize, 4); +#[cfg(target_pointer_width = "32")] +known_size_spec!(isize, 4); + +#[cfg(target_pointer_width = "64")] +known_size_spec!(usize, 8); +#[cfg(target_pointer_width = "64")] +known_size_spec!(isize, 8); + +#[refine_trait_spec] +impl KnownSize for [T; N] { + #[pure] + fn size() -> usize { + T::size() * N + } + + #[pure] + fn align() -> usize { + T::align() + } +} diff --git a/prusti-contracts/prusti-contracts/src/core_spec/mod.rs b/prusti-contracts/prusti-contracts/src/core_spec/mod.rs new file mode 100644 index 00000000000..7b3cc744b9f --- /dev/null +++ b/prusti-contracts/prusti-contracts/src/core_spec/mod.rs @@ -0,0 +1,16 @@ +pub mod clone; +pub mod convert; +pub mod default; +pub mod mem; +pub mod ops; +pub mod option; +pub mod result; +pub mod slice; + +// NOTE: specs marked with FUTURE are not fully expressible yet (in a clean way). +// They are due to be revised later as features are added. + +pub use clone::SnapshotEqualClone; +pub use convert::PureFrom; +pub use default::PureDefault; +pub use mem::KnownSize; diff --git a/prusti-contracts/prusti-contracts/src/core_spec/ops/index.rs b/prusti-contracts/prusti-contracts/src/core_spec/ops/index.rs new file mode 100644 index 00000000000..faa16470593 --- /dev/null +++ b/prusti-contracts/prusti-contracts/src/core_spec/ops/index.rs @@ -0,0 +1,14 @@ +#[allow(unused_imports)] +use crate::*; + +#[allow(unused_imports)] +use core::ops::Index; + +// FUTURE(#1221): This spec is currently not usable due to issue #1221. +/* +#[extern_spec] +trait Index { + #[pure] + fn index(&self, idx: Idx) -> &Self::Output; +} +*/ diff --git a/prusti-contracts/prusti-contracts/src/core_spec/ops/mod.rs b/prusti-contracts/prusti-contracts/src/core_spec/ops/mod.rs new file mode 100644 index 00000000000..01daeaeacf8 --- /dev/null +++ b/prusti-contracts/prusti-contracts/src/core_spec/ops/mod.rs @@ -0,0 +1,3 @@ +pub mod index; +pub mod ref_forwarding; +pub mod r#try; diff --git a/prusti-contracts/prusti-contracts/src/core_spec/ops/ref_forwarding.rs b/prusti-contracts/prusti-contracts/src/core_spec/ops/ref_forwarding.rs new file mode 100644 index 00000000000..93ef0fe2c2f --- /dev/null +++ b/prusti-contracts/prusti-contracts/src/core_spec/ops/ref_forwarding.rs @@ -0,0 +1,65 @@ +use crate::*; + +#[allow(unused_imports)] +use core::ops::*; + +macro_rules! specify_ref_op { + (impl $trait:tt fn $name:ident as $op:tt for $($t:ty)*) => ($( + #[extern_spec] + impl $trait<$t> for &$t { + #[pure] + #[ensures(result == *self $op other)] + fn $name(self, other: $t) -> $t; + } + + #[extern_spec] + impl $trait<&$t> for $t { + #[pure] + #[ensures(result == self $op *other)] + fn $name(self, other: &$t) -> $t; + } + + #[extern_spec] + impl $trait<&$t> for &$t { + #[pure] + #[ensures(result == *self $op *other)] + fn $name(self, other: &$t) -> $t; + } + )*) +} + +specify_ref_op! { impl Add fn add as + for usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128 f32 f64 } +specify_ref_op! { impl Sub fn sub as - for usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128 f32 f64 } +specify_ref_op! { impl Mul fn mul as * for usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128 f32 f64 } +specify_ref_op! { impl Div fn div as / for usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128 f32 f64 } +specify_ref_op! { impl Rem fn rem as % for usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128 f32 f64 } + +// FUTURE(bitvectors): bitwise operations on non-boolean types are experimental (`encode_bitvectors` to enable). could specify: usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128 +specify_ref_op! { impl BitAnd fn bitand as & for bool } +specify_ref_op! { impl BitOr fn bitor as | for bool } +specify_ref_op! { impl BitXor fn bitxor as ^ for bool } + +// FUTURE(bitvectors): left/right shifts. these will need special care since LHS and RHS may have different types + +macro_rules! specify_ref_op_assign { + (impl $trait:tt fn $name:ident as $op:tt for $($t:ty)*) => ($( + #[extern_spec] + impl $trait<&$t> for $t { + #[ensures(*self == old(*self) $op *other)] + fn $name(&mut self, other: &$t); + } + )*) +} + +specify_ref_op_assign! { impl AddAssign fn add_assign as + for usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128 f32 f64 } +specify_ref_op_assign! { impl SubAssign fn sub_assign as - for usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128 f32 f64 } +specify_ref_op_assign! { impl MulAssign fn mul_assign as * for usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128 f32 f64 } +specify_ref_op_assign! { impl DivAssign fn div_assign as / for usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128 f32 f64 } +specify_ref_op_assign! { impl RemAssign fn rem_assign as % for usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128 f32 f64 } + +// FUTURE(bitvectors): bitwise operations on non-boolean types are experimental (`encode_bitvectors` to enable). could specify: usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128 +specify_ref_op_assign! { impl BitAndAssign fn bitand_assign as & for bool } +specify_ref_op_assign! { impl BitOrAssign fn bitor_assign as | for bool } +specify_ref_op_assign! { impl BitXorAssign fn bitxor_assign as ^ for bool } + +// FUTURE(bitvectors): left/right shifts. these will need special care since LHS and RHS may have different types diff --git a/prusti-contracts/prusti-contracts/src/core_spec/ops/try.rs b/prusti-contracts/prusti-contracts/src/core_spec/ops/try.rs new file mode 100644 index 00000000000..b72e2b3cd35 --- /dev/null +++ b/prusti-contracts/prusti-contracts/src/core_spec/ops/try.rs @@ -0,0 +1,34 @@ +use crate::*; + +#[allow(unused_imports)] +use core::convert::Infallible; +#[allow(unused_imports)] +use core::ops::*; + +#[extern_spec] +impl Try for Result { + #[ensures(result === Ok(output))] + fn from_output(output: T) -> Self; + + #[ensures(match old(self) { + Ok(output) => result === ControlFlow::Continue(output), + Err(error) => result === ControlFlow::Break(Err(error)), + })] + fn branch(self) -> ControlFlow, T>; +} + +#[extern_spec] +impl Try for Option { + #[ensures(result === Some(output))] + fn from_output(output: T) -> Self; + + #[ensures(match old(self) { + Some(output) => result === ControlFlow::Continue(output), + //None => result === ControlFlow::Break(None), + None => match result { + ControlFlow::Break(residual) => residual.is_none(), + _ => false, + }, + })] + fn branch(self) -> ControlFlow, T>; +} diff --git a/prusti-contracts/prusti-contracts/src/core_spec/option.rs b/prusti-contracts/prusti-contracts/src/core_spec/option.rs new file mode 100644 index 00000000000..35b247142fa --- /dev/null +++ b/prusti-contracts/prusti-contracts/src/core_spec/option.rs @@ -0,0 +1,229 @@ +use crate::*; + +#[allow(unused_imports)] +use core::ops::{Deref, DerefMut}; +#[allow(unused_imports)] +use core::option::*; +#[allow(unused_imports)] +use core::pin::Pin; + +// NOTE: these are all non-nightly methods without trait bounds as of 2022-09 + +// FUTURE(unsupported_constants): reference None as a constant where it makes sense, rather than .is_none() +#[extern_spec] +impl Option { + #[pure] + #[ensures(result == matches!(self, Some(_)))] + fn is_some(&self) -> bool; + + #[pure] + #[ensures(result == matches!(self, None))] + fn is_none(&self) -> bool; + + #[ensures(result.is_some() == self.is_some())] + // FUTURE(refs): ensure identity matches + //#[ensures(match self { + // Some(v) => *result.unwrap() == v, + // None => result.is_none(), + //})] + fn as_ref(&self) -> Option<&T>; + + #[ensures(result.is_some() == self.is_some())] + // FUTURE(refs): ensure identity matches + fn as_mut(&mut self) -> Option<&mut T>; + + #[ensures(result.is_some() == self.is_some())] + // FUTURE(refs): ensure identity matches + fn as_pin_ref(self: Pin<&Option>) -> Option>; + + #[ensures(result.is_some() == self.is_some())] + // FUTURE(refs): ensure identity matches + fn as_pin_mut(self: Pin<&mut Option>) -> Option>; + + #[requires(self.is_some())] + #[ensures(old(self) === Some(result))] + fn expect(self, msg: &str) -> T; + + #[requires(self.is_some())] + #[ensures(old(self) === Some(result))] + fn unwrap(self) -> T; + + #[ensures(match old(self) { + Some(v) => result === v, + None => result === default, + })] + fn unwrap_or(self, default: T) -> T; + + #[ensures(match old(self) { + Some(v) => result === v, + None => true, + })] + // FUTURE(calls): describe that the function is called if none + fn unwrap_or_else(self, f: F) -> T + where + F: FnOnce() -> T; + + #[ensures(old(self.is_none()) || old(self) === Some(result))] + #[refine_spec(where T: Copy + super::default::PureDefault, [ + ensures(result === match old(self) { + Some(v) => v, + None => Default::default(), + }) + ])] + // FUTURE(calls): describe as call to Default::default rather than PureDefault + fn unwrap_or_default(self) -> T + where + T: Default; + + #[requires(self.is_some())] + #[ensures(old(self) === Some(result))] + unsafe fn unwrap_unchecked(self) -> T; + + #[ensures(result.is_some() == old(self.is_some()))] + // FUTURE(calls): describe that and how the function is called if some, and that its result is returned + fn map(self, f: F) -> Option + where + F: FnOnce(T) -> U; + + #[ensures(old(self.is_none()) ==> result === default)] + // FUTURE(calls): describe that and how the function is called if some, and that its result is returned + fn map_or(self, default: U, f: F) -> U + where + F: FnOnce(T) -> U; + + // FUTURE(calls): describe all function calls involved here and how they affect the result + fn map_or_else(self, default: D, f: F) -> U + where + D: FnOnce() -> U, + F: FnOnce(T) -> U; + + #[ensures(result === match old(self) { + Some(v) => Ok(v), + None => Err(err), + })] + fn ok_or(self, err: E) -> Result; + + #[ensures(match old(self) { + Some(v) => result === Ok(v), + None => result.is_err(), + })] + // FUTURE(calls): describe call to error function if none, and that its result is returned + fn ok_or_else(self, err: F) -> Result + where + F: FnOnce() -> E; + + #[ensures(self.is_some() == result.is_some())] + // FUTURE(refs): describe using PureDeref or call description if available + // FUTURE(calls): describe as call to Deref::deref if some + fn as_deref(&self) -> Option<&::Target> + where + T: Deref; + + #[ensures(self.is_some() == result.is_some())] + // FUTURE(calls): describe as call to DerefMut::deref_mut if some + fn as_deref_mut(&mut self) -> Option<&mut ::Target> + where + T: DerefMut; + + // FUTURE(iterators): describe what the iterator will yield + fn iter(&self) -> Iter<'_, T>; + + // FUTURE(iterators): describe what the iterator will yield + fn iter_mut(&mut self) -> IterMut<'_, T>; + + #[ensures(match old(self) { + Some(_) => result === old(optb), + None => result.is_none(), + })] + fn and(self, optb: Option) -> Option; + + #[ensures(old(self.is_none()) ==> result.is_none())] + // FUTURE(calls): describe call to function if some, and that its result is returned + fn and_then(self, f: F) -> Option + where + F: FnOnce(T) -> Option; + + #[ensures(match old(self) { + Some(v) => result.is_none() || result === Some(v), + None => result.is_none(), + })] + // FUTURE(calls): describe call to function if some, and how it affects result + fn filter

(self, predicate: P) -> Option + where + P: FnOnce(&T) -> bool; + + #[ensures(result === match old(self) { + Some(v) => Some(v), + None => old(optb), + })] + fn or(self, optb: Option) -> Option; + + #[ensures(old(self.is_some()) ==> result.is_some())] + // FUTURE(calls): describe call to function if none, and that its result is returned + fn or_else(self, f: F) -> Option + where + F: FnOnce() -> Option; + + #[ensures(result === match (old(self), old(optb)) { + (Some(v0), None) => Some(v0), + (None, Some(v0)) => Some(v0), + _ => None, + })] + fn xor(self, optb: Option) -> Option; + + #[ensures(*result === value)] + #[after_expiry(snap(self) === Some(before_expiry(snap(result))))] + fn insert(&mut self, value: T) -> &mut T; + + #[ensures(match old(self) { + Some(v) => *result === v, + None => *result === value, + })] + #[after_expiry(snap(self) === Some(before_expiry(snap(result))))] + fn get_or_insert(&mut self, value: T) -> &mut T; + + #[ensures(match old(self) { + Some(v) => *result === v, + None => true, + })] + #[after_expiry(snap(self) === Some(before_expiry(snap(result))))] + // FUTURE(calls): describe call to function if none, and that its result is returned and placed in the option + fn get_or_insert_with(&mut self, f: F) -> &mut T + where + F: FnOnce() -> T; + + #[ensures(result === old(snap(self)))] + #[ensures(self.is_none())] + fn take(&mut self) -> Option; + + #[ensures(result === old(snap(self)))] + #[ensures(*self === Some(value))] + fn replace(&mut self, value: T) -> Option; + + #[ensures(match (old(self), old(other)) { + (Some(v0), Some(v1)) => result === Some((v0, v1)), + _ => result.is_none(), + })] + fn zip(self, other: Option) -> Option<(T, U)>; + + // TODO: specific methods depending on trait bounds +} + +#[extern_spec] +impl Option> { + #[ensures(match old(self) { + Some(Some(x)) => result === Some(x), + _ => result.is_none(), + })] + pub fn flatten(self) -> Option; +} + +#[extern_spec] +impl Option> { + #[ensures(match old(self) { + Some(Ok(x)) => result === Ok(Some(x)), + Some(Err(e)) => result === Err(e), + None => matches!(result, Ok(None)), + })] + pub fn transpose(self) -> Result, E>; +} diff --git a/prusti-contracts/prusti-contracts/src/core_spec/result.rs b/prusti-contracts/prusti-contracts/src/core_spec/result.rs new file mode 100644 index 00000000000..5b42c89abc5 --- /dev/null +++ b/prusti-contracts/prusti-contracts/src/core_spec/result.rs @@ -0,0 +1,190 @@ +use crate::*; + +#[allow(unused_imports)] +use core::fmt::Debug; +#[allow(unused_imports)] +use core::ops::{Deref, DerefMut}; +#[allow(unused_imports)] +use core::result::*; + +#[extern_spec] +impl Result { + #[pure] + #[ensures(result == matches!(self, Ok(_)))] + fn is_ok(&self) -> bool; + + #[pure] + #[ensures(result == matches!(self, Err(_)))] + fn is_err(&self) -> bool; + + #[ensures(result === match old(self) { + Ok(v) => Some(v), + Err(_) => None, + })] + fn ok(self) -> Option; + + #[ensures(result === match old(self) { + Ok(_) => None, + Err(e) => Some(e), + })] + fn err(self) -> Option; + + #[ensures(result.is_ok() == self.is_ok())] + // FUTURE(refs): ensure identity matches + fn as_ref(&self) -> Result<&T, &E>; + + #[ensures(result.is_ok() == old(self.is_ok()))] + // FUTURE(refs): ensure identity matches & result affects original + fn as_mut(&mut self) -> Result<&mut T, &mut E>; + + #[ensures(result.is_ok() == old(self.is_ok()))] + // FUTURE(calls): describe that and how the function is called if ok, and that its result is returned + fn map(self, op: F) -> Result + where + F: FnOnce(T) -> U; + + #[ensures(old(self.is_err()) ==> result === default)] + // FUTURE(calls): describe that and how the function is called if ok, and that its result is returned + fn map_or(self, default: U, op: F) -> U + where + F: FnOnce(T) -> U; + + // FUTURE(calls): describe all function calls involved here and how they affect the result + fn map_or_else(self, default: D, f: F) -> U + where + D: FnOnce(E) -> U, + F: FnOnce(T) -> U; + + #[ensures(match old(self) { + Ok(v) => result === Ok(v), + Err(_) => result.is_err(), + })] + // FUTURE(calls): describe that and how the function is called if err, and that its result is returned + fn map_err(self, op: O) -> Result + where + O: FnOnce(E) -> F; + + #[ensures(match self { + Ok(v) => result.is_ok(), + Err(e) => result === Err(e), + })] + // FUTURE(calls): describe as call to Deref::deref if some + // FUTURE(refs): describe transformation of ok value and error not changing + fn as_deref(&self) -> Result<&::Target, &E> + where + T: Deref; + + #[ensures(result.is_ok() == old(self.is_ok()))] + // FUTURE(calls): describe as call to Deref::deref if some + // FUTURE(refs): describe transformation of ok value and error not changing + fn as_deref_mut(&mut self) -> Result<&mut ::Target, &mut E> + where + T: DerefMut; + + // FUTURE(iterators): describe what the iterator will yield + fn iter(&self) -> Iter<'_, T>; + + // FUTURE(iterators): describe what the iterator will yield + fn iter_mut(&mut self) -> IterMut<'_, T>; + + #[requires(self.is_ok())] + #[ensures(old(self) === Ok(result))] + fn expect(self, msg: &str) -> T + where + E: Debug; + + #[requires(self.is_ok())] + #[ensures(old(self) === Ok(result))] + fn unwrap(self) -> T + where + E: Debug; + + #[ensures(old(self.is_err()) || old(self) === Ok(result))] + #[refine_spec(where T: Copy + super::default::PureDefault, [ + ensures(result === match old(self) { + Ok(v) => v, + Err(_) => T::default(), + }) + ])] + // FUTURE(calls): describe as call to Default::default if err + fn unwrap_or_default(self) -> T + where + T: Default; + + #[requires(self.is_err())] + #[ensures(old(self) === Err(result))] + fn expect_err(self, msg: &str) -> E + where + T: Debug; + + #[requires(self.is_err())] + #[ensures(old(self) === Err(result))] + fn unwrap_err(self) -> E + where + T: Debug; + + #[ensures(result === match old(self) { + Ok(v) => old(res), + Err(e) => Err(e), + })] + fn and(self, res: Result) -> Result; + + #[ensures(match old(self) { + Ok(v) => true, + Err(e) => result === Err(e), + })] + // FUTURE(calls): describe call to function if ok, and that its result is returned + fn and_then(self, f: F) -> Result + where + F: FnOnce(T) -> Result; + + #[ensures(result === match old(self) { + Ok(v) => Ok(v), + Err(_) => old(res), + })] + fn or(self, res: Result) -> Result; + + #[ensures(match old(self) { + Ok(v) => result === Ok(v), + Err(_) => true, + })] + // FUTURE(calls): describe call to function if err, and that its result is returned + fn or_else(self, op: O) -> Result + where + O: FnOnce(E) -> Result; + + #[ensures(result === match old(self) { + Ok(v) => v, + Err(_) => default, + })] + fn unwrap_or(self, default: T) -> T; + + #[ensures(match old(self) { + Ok(v) => result === v, + Err(_) => true, + })] + // FUTURE(calls): describe that the function is called if err + fn unwrap_or_else(self, op: F) -> T + where + F: FnOnce(E) -> T; + + #[requires(self.is_ok())] + #[ensures(old(self) === Ok(result))] + unsafe fn unwrap_unchecked(self) -> T; + + #[requires(self.is_err())] + #[ensures(old(self) === Err(result))] + unsafe fn unwrap_err_unchecked(self) -> E; + + // TODO: specific methods depending on trait bounds +} + +#[extern_spec] +impl Result, E> { + #[ensures(match old(self) { + Ok(Some(x)) => result === Some(Ok(x)), + Ok(None) => result.is_none(), + Err(e) => result === Some(Err(e)), + })] + pub fn transpose(self) -> Option>; +} diff --git a/prusti-contracts/prusti-contracts/src/core_spec/slice.rs b/prusti-contracts/prusti-contracts/src/core_spec/slice.rs new file mode 100644 index 00000000000..9e13193bc97 --- /dev/null +++ b/prusti-contracts/prusti-contracts/src/core_spec/slice.rs @@ -0,0 +1,54 @@ +use crate::*; + +#[allow(unused_imports)] +use core::{ops::Index, slice::SliceIndex}; + +#[extern_spec] +impl [T] { + #[pure] + #[ensures(result == (self.len() == 0))] + fn is_empty(&self) -> bool; + + #[pure] + fn len(&self) -> usize; + + #[ensures(match result { + Some(x) => *x === self[0], + None => self.len() == 0, + })] + // FUTURE(refs): make statements about the returned reference + fn first(&self) -> Option<&T>; + + #[ensures(match result { + Some(x) => *x === self[0], + None => self.len() == 0, + })] + // FUTURE(refs): make statements about the returned reference + fn first_mut(&mut self) -> Option<&mut T>; + + #[ensures(match result { + Some(x) => *x === self[self.len() - 1], + None => self.len() == 0, + })] + // FUTURE(refs): make statements about the returned reference + fn last(&self) -> Option<&T>; + + #[ensures(match result { + Some(x) => *x === self[self.len() - 1], + None => self.len() == 0, + })] + // FUTURE(refs): make statements about the returned reference + fn last_mut(&mut self) -> Option<&mut T>; +} + +// FUTURE(#1221): This spec is currently not usable due to issue #1221. +/* +#[extern_spec] +impl Index for [T] +where + I: SliceIndex<[T]>, +{ + #[pure] + fn index(&self, index: I) -> &I::Output; +} +*/ diff --git a/prusti-contracts/prusti-contracts/src/lib.rs b/prusti-contracts/prusti-contracts/src/lib.rs index 28ab1bce27d..90668c09b0e 100644 --- a/prusti-contracts/prusti-contracts/src/lib.rs +++ b/prusti-contracts/prusti-contracts/src/lib.rs @@ -1,4 +1,11 @@ #![no_std] +#![feature(auto_traits)] +#![feature(negative_impls)] +#![feature(try_trait_v2)] +#![feature(cfg_version)] + +// this is present even when compiling outside prusti to enable (negatively) implementing traits used for better specs +pub mod core_spec; /// A macro for writing a precondition on a function. pub use prusti_contracts_proc_macros::requires; @@ -121,9 +128,6 @@ mod private { } } -#[cfg(feature = "prusti")] -pub mod core_spec; - #[cfg(feature = "prusti")] mod private { use core::{marker::PhantomData, ops::*}; diff --git a/prusti-contracts/prusti-std/Cargo.toml b/prusti-contracts/prusti-std/Cargo.toml index acb0cbd637e..c1c2dde3a20 100644 --- a/prusti-contracts/prusti-std/Cargo.toml +++ b/prusti-contracts/prusti-std/Cargo.toml @@ -14,6 +14,9 @@ categories = ["development-tools", "development-tools::testing"] [dependencies] prusti-contracts = { path = "../prusti-contracts", version = "0.2.0" } -# Forward "prusti" flag [features] +default = ["alloc", "std"] +alloc = [] +std = [] +# Forward "prusti" flag prusti = ["prusti-contracts/prusti"] diff --git a/prusti-contracts/prusti-std/src/alloc_spec/mod.rs b/prusti-contracts/prusti-std/src/alloc_spec/mod.rs new file mode 100644 index 00000000000..88b18b9c830 --- /dev/null +++ b/prusti-contracts/prusti-std/src/alloc_spec/mod.rs @@ -0,0 +1,5 @@ +// These specs can't be built-in like the core specs since some no_std crates may not even have an allocator. +// Instead, prusti-std supports no_std through a feature. + +pub mod string; +pub mod vec; diff --git a/prusti-contracts/prusti-std/src/alloc_spec/string.rs b/prusti-contracts/prusti-std/src/alloc_spec/string.rs new file mode 100644 index 00000000000..9318eeceba2 --- /dev/null +++ b/prusti-contracts/prusti-std/src/alloc_spec/string.rs @@ -0,0 +1,82 @@ +use prusti_contracts::*; + +use alloc::string::{String, ToString}; + +// FUTURE(#1221): String should forward its specs to as_str where possible, to avoid writing each spec twice. +// That doesn't currently work though, due to issue #1221 +#[extern_spec] +impl String { + #[ensures(result.is_empty())] + fn new() -> Self; + + #[pure] + #[ensures(result == (self.len() == 0))] + //#[ensures(result == self.as_str().is_empty()))] + fn is_empty(&self) -> bool; + + #[pure] + #[ensures(result.len() == self.len())] + fn as_str(&self) -> &str; + + #[pure] + //#[ensures(result == self.as_str().len())] + fn len(&self) -> usize; + + #[ensures(self.len() == 0)] + fn clear(&mut self); + + #[ensures(self.len() == old(self.len()) + 1)] + //#[ensures(self[self.len() - 1] === ch)] + //#[ensures(forall(|i: usize| i < old(self.len()) ==> self[i] === old(self[i])))] + fn push(&mut self, ch: char); +} + +#[extern_spec] +impl str { + // TODO: this should be a prusti intrinsic, like it is for slices. + #[pure] + fn len(&self) -> usize; + + #[pure] + #[ensures(result == (self.len() == 0))] + fn is_empty(&self) -> bool; +} + +// FUTURE(#1221): these specs make their methods crash due to issue #1221, so they are disabled for now. +/* +#[extern_spec] +impl Deref for String { + #[ensures(result === self.as_str()] + fn deref(&self) -> &str; +} + +#[extern_spec] +impl ToOwned for str { + #[ensures(result.as_str() === self)] + fn to_owned(&self) -> String; +} + +#[extern_spec] +impl ToString for str { + #[ensures(result.as_str() === self)] + fn to_string(&self) -> String; +} + +#[extern_spec] +impl From<&str> for String { + #[ensures(result.as_str() === other)] + fn from(other: &str) -> Self; +} +*/ + +#[extern_spec] +impl ToString for String { + #[ensures(result === self)] + fn to_string(&self) -> String; +} + +#[extern_spec] +impl Default for String { + #[ensures(result.is_empty())] + fn default() -> Self; +} diff --git a/prusti-contracts/prusti-std/src/alloc_spec/vec.rs b/prusti-contracts/prusti-std/src/alloc_spec/vec.rs new file mode 100644 index 00000000000..e635967bc31 --- /dev/null +++ b/prusti-contracts/prusti-std/src/alloc_spec/vec.rs @@ -0,0 +1,58 @@ +use prusti_contracts::*; + +use alloc::{alloc::Allocator, vec::Vec}; + +#[extern_spec] +impl Vec { + #[ensures(result.is_empty())] + fn new() -> Self; + + // capacity is not relevant to functional behavior + #[ensures(result.is_empty())] + fn with_capacity(capacity: usize) -> Self; +} + +// FUTURE(#1221): Vec should forward its specs to as_slice where possible, to avoid writing each spec twice. +// That doesn't currently work though, due to issue #1221 +#[extern_spec] +impl Vec { + #[pure] + #[ensures(result == (self.len() == 0))] + //#[ensures(result == self.as_slice().is_empty())] + fn is_empty(&self) -> bool; + + #[pure] + //#[ensures(result == self.as_slice().len())] + fn len(&self) -> usize; + + #[pure] + #[ensures(result.len() == self.len())] + fn as_slice(&self) -> &[T]; + + #[ensures(self.is_empty())] + fn clear(&mut self); + + #[ensures(self.len() == old(self.len()) + 1)] + //#[ensures(self[self.len() - 1] === value)] + //#[ensures(forall(|i: usize| i < old(self.len()) ==> &self[i] === old(&self[i])))] + fn push(&mut self, value: T); +} + +// FUTURE(#1221): We'd like to specify the behavior of Index for Vec, but issue #1221 is currently blocking that. Once it's fixed, Prusti can be amended to rely on these specs instead of rejecting the index operation because Vec doesn't have hardcoded support. +/* +use core::{ops::Index, slice::SliceIndex}; + +#[extern_spec] +impl> Index for Vec { + #[pure] + #[ensures(*result === self.as_slice()[index])] + fn index(&self, index: I) -> &Self::Output; +} +*/ + +#[extern_spec] +impl Default for Vec { + #[refine_spec(where Self: Copy, [pure])] + #[ensures(result.is_empty())] + fn default() -> Self; +} diff --git a/prusti-contracts/prusti-std/src/lib.rs b/prusti-contracts/prusti-std/src/lib.rs index 5b317c1fc8d..a67c1354035 100644 --- a/prusti-contracts/prusti-std/src/lib.rs +++ b/prusti-contracts/prusti-std/src/lib.rs @@ -1,14 +1,16 @@ -use prusti_contracts::*; +#![feature(allocator_api)] // to specify Vec +#![no_std] // disable std by default -#[extern_spec] -impl ::std::collections::hash_map::HashMap -where - K: Eq + ::core::hash::Hash, - S: ::std::hash::BuildHasher, -{ - #[pure] - pub fn contains_key(&self, k: &Q) -> bool - where - K: ::core::borrow::Borrow, - Q: ::core::hash::Hash + Eq; -} +// link to std if the feature is set +#[cfg(feature = "std")] +extern crate std; + +// Even alloc can be disabled for consistency with std, and in preparation for future specs for other, possibly no_std, crates. +#[cfg(feature = "alloc")] +extern crate alloc; + +// modules have a `_spec` suffix to avoid name conflicts with their crates. +#[cfg(feature = "alloc")] +pub mod alloc_spec; +#[cfg(feature = "std")] +pub mod std_spec; diff --git a/prusti-contracts/prusti-std/src/std_spec/collections.rs b/prusti-contracts/prusti-std/src/std_spec/collections.rs new file mode 100644 index 00000000000..da953ef5449 --- /dev/null +++ b/prusti-contracts/prusti-std/src/std_spec/collections.rs @@ -0,0 +1,21 @@ +use prusti_contracts::*; + +#[extern_spec] +impl std::collections::hash_map::HashMap +where + K: Eq + ::core::hash::Hash, + S: ::std::hash::BuildHasher, +{ + #[pure] + #[ensures(result.is_some() == self.contains_key(k))] + pub fn get(&self, k: &Q) -> Option<&V> + where + K: core::borrow::Borrow + std::cmp::Eq + std::hash::Hash, + Q: core::hash::Hash + Eq; + + #[pure] + fn contains_key(&self, k: &Q) -> bool + where + K: core::borrow::Borrow + Eq + std::hash::Hash, + Q: core::hash::Hash + Eq; +} diff --git a/prusti-contracts/prusti-std/src/std_spec/mod.rs b/prusti-contracts/prusti-std/src/std_spec/mod.rs new file mode 100644 index 00000000000..2e4fe9b79c2 --- /dev/null +++ b/prusti-contracts/prusti-std/src/std_spec/mod.rs @@ -0,0 +1 @@ +pub mod collections; diff --git a/prusti-tests/tests/compiletest.rs b/prusti-tests/tests/compiletest.rs index c1dafc5a37b..bfdb693d54e 100644 --- a/prusti-tests/tests/compiletest.rs +++ b/prusti-tests/tests/compiletest.rs @@ -197,6 +197,11 @@ fn test_runner(_tests: &[&()]) { run_verification_overflow("verify_overflow", &filter); save_verification_cache(); + // Test the functionality of built-in specs. + println!("[std]"); + run_verification_no_overflow("std", &filter); + save_verification_cache(); + // Test the verifier with test cases that only partially verify due to known open issues. // The purpose of these tests is two-fold: 1. these tests help prevent potential further // regressions, because the tests also test code paths not covered by other tests; and diff --git a/prusti-tests/tests/std/fail/clone.rs b/prusti-tests/tests/std/fail/clone.rs new file mode 100644 index 00000000000..50e8e9665ca --- /dev/null +++ b/prusti-tests/tests/std/fail/clone.rs @@ -0,0 +1,46 @@ +#![feature(negative_impls)] +//~^ ERROR: postcondition might not hold +// the above error is currently reported with an incorrect span due to issue #1310. +// it should be down on line 38 at the actual implementation. + +use prusti_contracts::*; + +fn main() {} + +#[derive(Clone)] +struct Foo { + x: i32, +} + +impl !core_spec::SnapshotEqualClone for Foo {} + +fn foo() { + let foo = Foo { x: 1 }; + assert!(foo.clone().x == 1); //~ ERROR: the asserted expression might not hold +} + +#[derive(Clone)] +struct FooHolder { + foo: Foo, +} + +fn foo_holder() { + let foo = Foo { x: 1 }; + let holder = FooHolder { foo }; + assert!(holder.clone().foo.x == 1); //~ ERROR: the asserted expression might not hold +} + +struct Bar { + x: i32, +} + +impl Clone for Bar { + fn clone(&self) -> Self { + Self { x: self.x + 1 } + } +} + +fn bar() { + let bar = Bar { x: 2 }; + assert!(bar.clone().x == 2); +} diff --git a/prusti-tests/tests/std/fail/convert.rs b/prusti-tests/tests/std/fail/convert.rs new file mode 100644 index 00000000000..21a932f527e --- /dev/null +++ b/prusti-tests/tests/std/fail/convert.rs @@ -0,0 +1,43 @@ +#![feature(negative_impls)] + +use prusti_contracts::*; + +fn main() {} + +fn numeric_conversions_1() { + let small: u8 = 41; + let x = 42; + assert!(i32::from(small) == x); //~ ERROR the asserted expression might not hold +} + +fn numeric_conversions_2() { + let small: u8 = 41; + let x = 42; + let converted: i32 = small.into(); + assert!(converted == x); //~ ERROR the asserted expression might not hold +} + +fn impure_conversion() { + let x = 42; + let converted = ImpureFrom::from(x); + assert!(converted.x == 1); + // because our from implementation is not pure, it can't be used to express the behavior of into: + let converted: ImpureFrom = x.into(); + assert!(converted.x == 1); //~ ERROR the asserted expression might not hold +} + +#[derive(Clone, Copy)] +struct ImpureFrom { + x: i32, +} + +impl !core_spec::PureFrom for ImpureFrom {} + +#[refine_trait_spec] +impl From for ImpureFrom { + #[ensures(result.x == 1)] + #[trusted] + fn from(x: i32) -> Self { + Self { x } + } +} diff --git a/prusti-tests/tests/std/fail/default.rs b/prusti-tests/tests/std/fail/default.rs new file mode 100644 index 00000000000..7d6b5196e1b --- /dev/null +++ b/prusti-tests/tests/std/fail/default.rs @@ -0,0 +1,25 @@ +use prusti_contracts::*; +use prusti_std; + +fn main() {} + +fn element0() { + let default: (Special, i32) = Default::default(); + assert!(default.0.value == 0); //~ ERROR: the asserted expression might not +} + +fn element1() { + let default: (Special, i32) = Default::default(); + assert!(default.1 == 0); //~ ERROR: the asserted expression might not hold +} + +fn special_value() { + let default: Special = Default::default(); + assert!(default.value == 0); //~ ERROR: the asserted expression might not hold +} + +// not Copy => Default not pure +#[derive(Default)] +struct Special { + value: i32, +} diff --git a/prusti-tests/tests/std/pass/clone.rs b/prusti-tests/tests/std/pass/clone.rs new file mode 100644 index 00000000000..9e16efda40f --- /dev/null +++ b/prusti-tests/tests/std/pass/clone.rs @@ -0,0 +1,23 @@ +use prusti_contracts::*; + +fn main() { + let foo = Foo { x: 1 }; + let bar = Bar { x: 2 }; + assert!(foo.clone().x == 1); + assert!(bar.clone().x == 2); +} + +#[derive(Clone)] +struct Foo { + x: i32, +} + +struct Bar { + x: i32, +} + +impl Clone for Bar { + fn clone(&self) -> Self { + Self { x: self.x } + } +} diff --git a/prusti-tests/tests/std/pass/convert.rs b/prusti-tests/tests/std/pass/convert.rs new file mode 100644 index 00000000000..6c12fcacbfa --- /dev/null +++ b/prusti-tests/tests/std/pass/convert.rs @@ -0,0 +1,57 @@ +#![feature(negative_impls)] + +use prusti_contracts::*; + +fn main() {} + +fn numeric_conversions() { + let small: u8 = 42; + let x = 42; + assert!(i32::from(small) == x); + let converted: i32 = small.into(); + assert!(converted == x); +} + +fn self_conversion() { + let foo = Foo { x: 42 }; + let converted: Foo = foo.into(); + assert!(converted.x == foo.x); +} + +#[derive(Clone, Copy)] +struct Foo { + x: i32, +} + +fn impure_conversion() { + let x = 42; + let converted = ImpureFrom::from(x); + assert!(converted.x == 1); +} + +#[derive(Clone, Copy)] +struct ImpureFrom { + x: i32, +} + +impl !core_spec::PureFrom for ImpureFrom {} + +#[refine_trait_spec] +impl From for ImpureFrom { + #[ensures(result.x == 1)] + #[trusted] + fn from(x: i32) -> Self { + Self { x } + } +} + +// can't currently specify blanket Into impl for impure types +fn impure_self_conversion() { + let unique = Unique { x: 1 }; + let converted = Unique::from(unique); + assert!(converted.x == 1); +} + +struct Unique { + x: i32, +} diff --git a/prusti-tests/tests/std/pass/default.rs b/prusti-tests/tests/std/pass/default.rs new file mode 100644 index 00000000000..c4ee58cc84c --- /dev/null +++ b/prusti-tests/tests/std/pass/default.rs @@ -0,0 +1,26 @@ +use prusti_contracts::*; +use prusti_std; + +fn main() { + let default: bool = Default::default(); + assert!(!default); + + let default: (i32, u64) = Default::default(); + assert!(default.0 == 0); + assert!(default.1 == 0); + + let default: Option = Default::default(); + assert!(default.is_none()); + + let default: Vec = Default::default(); + assert!(default.is_empty()); + + let default = String::default(); + assert!(default.is_empty()); +} + +// not Copy => Default not pure +#[derive(Default)] +struct Special { + value: i32, +} diff --git a/prusti-tests/tests/std/pass/mem.rs b/prusti-tests/tests/std/pass/mem.rs new file mode 100644 index 00000000000..a3dabdfd56d --- /dev/null +++ b/prusti-tests/tests/std/pass/mem.rs @@ -0,0 +1,27 @@ +use prusti_contracts::*; + +use core::mem::{align_of, size_of}; + +fn main() { + assert!(size_of::<[i32; 3]>() == 12); + assert!(align_of::<[i32; 3]>() == 4); + assert!(size_of::() == 8); + assert!(align_of::() == 4); +} + +struct Foo { + a: i32, + b: i32, +} + +impl core_spec::KnownSize for Foo { + #[pure] + fn size() -> usize { + 8 + } + + #[pure] + fn align() -> usize { + 4 + } +} diff --git a/prusti-tests/tests/std/pass/ops_ref_forwarding.rs b/prusti-tests/tests/std/pass/ops_ref_forwarding.rs new file mode 100644 index 00000000000..c86430c22e7 --- /dev/null +++ b/prusti-tests/tests/std/pass/ops_ref_forwarding.rs @@ -0,0 +1,46 @@ +use prusti_contracts::*; + +fn main() { + let x = 5; + let y = 4; + assert!(x + y == 9); + prusti_assert!(x + &y == 9); + assert!(x + &y == 9); + prusti_assert!(&x + y == 9); + assert!(&x + y == 9); + prusti_assert!(&x + &y == 9); + assert!(&x + &y == 9); + + assert!(x - y == 1); + prusti_assert!(x - &y == 1); + assert!(x - &y == 1); + prusti_assert!(&x - y == 1); + assert!(&x - y == 1); + prusti_assert!(&x - &y == 1); + assert!(&x - &y == 1); + + prusti_assert!(&x - &y + &y == x); + assert!(&x - &y + &y == x); +} + +fn mutation() { + let mut x = 5; + let y = 4; + x += &y; + assert!(x == 9); + x += y; + assert!(x == 13); +} + +fn bools() { + let t = true; + let f = false; + + assert!(t | f == true); + prusti_assert!(t | &f == true); + assert!(t | &f == true); + prusti_assert!(&t & f == false); + assert!(&t & f == false); + prusti_assert!(&t & &f == false); + assert!(&t & &f == false); +} diff --git a/prusti-tests/tests/std/pass/option.rs b/prusti-tests/tests/std/pass/option.rs new file mode 100644 index 00000000000..1e272c18002 --- /dev/null +++ b/prusti-tests/tests/std/pass/option.rs @@ -0,0 +1,179 @@ +#![feature(unboxed_closures)] +#![feature(fn_traits)] + +use prusti_contracts::*; + +fn main() {} + +// split into many functions to avoid exponential branching complexity + +fn test_1() { + let some = Some(42); + let none = Option::::None; + + assert!(some.is_some()); + assert!(!some.is_none()); + assert!(!none.is_some()); + assert!(none.is_none()); + + assert!(some.as_ref().is_some()); + //let x = some.as_ref().unwrap(); + //assert!(*x == 42); + //assert!(*some.as_ref().unwrap() == 42); + assert!(none.as_ref().is_none()); + + assert!(some.unwrap() == 42); + assert!(some.expect("test") == 42); + assert!(some.unwrap_or(69) == 42); + assert!(none.unwrap_or(69) == 69); + assert!(some.unwrap_or_else(|| 69) == 42); + let _ = none.unwrap_or_else(|| 69); + assert!(some.unwrap_or_default() == 42); + assert!(none.unwrap_or_default() == 0); + unsafe { + assert!(some.unwrap_unchecked() == 42); + } +} + +fn test_2() { + let some = Some(42); + let none = Option::::None; + + assert!(some.map(|x| x + 1).is_some()); + let _ = some.map_or(69, |x| x + 1); + assert!(none.map_or(69, |x| x + 1) == 69); + let _ = some.map_or_else(|| 42, |x| x + 1); + + let ok: Result = Ok(42); + let err: Result = Err(false); + assert!(some.ok_or(false) == ok); + assert!(none.ok_or(false) == err); + assert!(some.ok_or_else(|| true) == ok); + assert!(none.ok_or_else(|| true).is_err()); +} + +fn test_3() { + let some = Some(42); + let none = Option::::None; + + assert!(some.and(some).unwrap() == 42); + assert!(some.and(none).is_none()); + assert!(none.and(some).is_none()); + assert!(none.and(none).is_none()); + + let _ = some.and_then(|v| Some(v)); + let _ = some.and_then(|_| Option::::None); + assert!(none.and_then(|v| Some(v)).is_none()); + assert!(none.and_then(|_| Option::::None).is_none()); +} + +fn test_4() { + let some = Some(42); + let none = Option::::None; + + // manual predicate + + struct Equals42; + + impl FnOnce<(&i32,)> for Equals42 { + type Output = bool; + #[trusted] + extern "rust-call" fn call_once(self, arg: (&i32,)) -> bool { + *arg.0 == 42 + } + } + + let filtered = some.filter(Equals42); + assert!(match filtered { + Some(v) => v == 42, + None => true, // can't yet prove that Equals42 succeeds + }); + assert!(none.filter(Equals42) == none); +} + +fn test_5() { + let some = Some(42); + let some_2 = Some(2); + let none = Option::::None; + + assert!(some.or(some_2) == some); + assert!(none.or(some_2) == some_2); + assert!(some.or(none) == some); + assert!(none.or(none) == none); + + assert!(some.xor(some) == none); + assert!(none.xor(some) == some); + assert!(some.xor(none) == some); + assert!(none.xor(none) == none); +} + +fn test_6() { + let some = Some(42); + let none = Option::::None; + + let mut opt = none; + let val = opt.insert(1); + assert!(*val == 1); + *val = 42; + assert!(opt == some); + + let mut opt = some; + assert!(*opt.get_or_insert(0) == 42); + assert!(opt == some); + let mut opt = none; + let val = opt.get_or_insert(0); + assert!(*val == 0); + *val += 1; + assert!(opt.unwrap() == 1); + + let mut opt = some; + assert!(*opt.get_or_insert_with(|| 0) == 42); + assert!(opt == some); + + let mut opt = none; + *opt.get_or_insert_with(|| 0) = 42; + assert!(opt == some); + + let mut opt = some; + assert!(opt.take() == some); + assert!(opt == none); + assert!(opt.take() == none); + assert!(opt == none); + + let mut opt = none; + assert!(opt.replace(42) == none); + assert!(opt == some); + assert!(opt.replace(1) == some); + assert!(opt.unwrap() == 1); + + let pair = (42, 42); + assert!(some.zip(some).unwrap() == pair); + assert!(some.zip(none).is_none()); + assert!(none.zip(some).is_none()); + assert!(none.zip(none).is_none()); +} + +fn test_flatten() { + let x: Option> = Some(Some(6)); + assert!(x.flatten().unwrap() == 6); + + let x: Option> = Some(None); + assert!(x.flatten().is_none()); + + let x: Option> = None; + assert!(x.flatten().is_none()); + + let x: Option>> = Some(Some(Some(6))); + assert!(x.flatten().unwrap().unwrap() == 6); + assert!(x.flatten().flatten().unwrap() == 6); +} + +fn test_transpose() { + #[derive(Debug, Eq, PartialEq)] + struct SomeErr; + + let x: Result, SomeErr> = Ok(Some(5)); + let y: Option> = Some(Ok(5)); + let y = y.transpose(); + prusti_assert!(x === y); +} diff --git a/prusti-tests/tests/std/pass/result.rs b/prusti-tests/tests/std/pass/result.rs new file mode 100644 index 00000000000..07092d24334 --- /dev/null +++ b/prusti-tests/tests/std/pass/result.rs @@ -0,0 +1,103 @@ +use prusti_contracts::*; + +fn main() {} + +// split into many functions to avoid exponential branching complexity + +fn test_1() { + let ok = Result::::Ok(42); + let err = Result::::Err("test".to_string()); + + assert!(ok.is_ok()); + assert!(!ok.is_err()); + assert!(!err.is_ok()); + assert!(err.is_err()); + + let some = Some(42); + let none = Option::::None; + assert!(ok.clone().ok() == some); + assert!(err.clone().ok() == none); + + assert!(ok.as_ref().is_ok()); + assert!(err.as_ref().is_err()); +} + +fn test_2() { + let ok = Result::::Ok(42); + let err = Result::::Err(false); + + assert!(ok.map(|x| x + 1).is_ok()); + let _ = ok.map_or(69, |x| x + 1); + assert!(err.map_or(69, |x| x + 1) == 69); + let _ = ok.map_or_else(|_| 42, |x| x + 1); + assert!(ok.map_err(|x| !x) == ok); + assert!(err.map_err(|x| !x).is_err()); +} + +fn test_3() { + let ok = Result::::Ok(42); + let err = Result::::Err(false); + + assert!(ok.expect("test") == 42); + assert!(ok.unwrap() == 42); + assert!(ok.unwrap_or_default() == 42); + //assert!(err.unwrap_or_default() == 0); + assert!(err.expect_err("test") == false); + assert!(err.unwrap_err() == false); +} + +fn test_4() { + let ok = Result::::Ok(42); + let ok2 = Result::::Ok(5); + let err = Result::::Err(false); + let err2 = Result::::Err(true); + + assert!(ok.and(err2) == err2); + assert!(ok.and(ok2) == ok2); + assert!(err.and(ok2) == err); + assert!(err.and(err2) == err); + + let _ = ok.and_then(|v| Result::::Ok(v + 1)); + let _ = ok.and_then(|_| Result::::Err(true)); + assert!(err.and_then(|v| Result::::Ok(v + 1)) == err); + assert!(err.and_then(|_| Result::::Err(true)) == err); + + assert!(ok.or(err2) == ok); + assert!(ok.or(ok2) == ok); + assert!(err.or(ok2) == ok2); + assert!(err.or(err2) == err2); + + assert!(ok.or_else(|_| Result::::Ok(42)) == ok); + assert!(ok.or_else(|e| Result::::Err(e)) == ok); + let _ = err.or_else(|_| Result::::Ok(42)); + let _ = err.or_else(|e| Result::::Err(e)); +} + +fn test_5() { + let ok = Result::::Ok(42); + let err = Result::::Err(false); + + assert!(ok.unwrap_or(69) == 42); + assert!(err.unwrap_or(69) == 69); + + let _ = ok.unwrap_or_else(|_| 42); + let _ = err.unwrap_or_else(|_| 42); + + assert!(ok.unwrap_or_default() == 42); + assert!(err.unwrap_or_default() == 0); + + unsafe { + assert!(ok.unwrap_unchecked() == 42); + assert!(err.unwrap_err_unchecked() == false); + } +} + +fn test_transpose() { + #[derive(Debug, Eq, PartialEq)] + struct SomeErr; + + let x: Result, SomeErr> = Ok(Some(5)); + let y: Option> = Some(Ok(5)); + let x = x.transpose(); + prusti_assert!(x === y); +} diff --git a/prusti-tests/tests/std/pass/vec.rs b/prusti-tests/tests/std/pass/vec.rs new file mode 100644 index 00000000000..4f32aa8e003 --- /dev/null +++ b/prusti-tests/tests/std/pass/vec.rs @@ -0,0 +1,24 @@ +use prusti_contracts::*; +use prusti_std; + +fn main() { + let mut v = Vec::new(); + assert!(v.is_empty()); + assert!(v.len() == 0); + + v.push(10); + assert!(!v.is_empty()); + assert!(v.len() == 1); + // issue #1221: + //let slice = v.as_slice(); + //assert!(slice[0] == 10); + + v.push(20); + assert!(v.len() == 2); + //let slice = v.as_slice(); + //assert!(slice[0] == 10); + //assert!(slice[1] == 10); + + v.clear(); + assert!(v.is_empty()); +} diff --git a/prusti-tests/tests/verify/fail/user-guide/peek_mut_pledges.rs b/prusti-tests/tests/verify/fail/user-guide/peek_mut_pledges.rs index 4302e9cd5b5..c92daa57cb7 100644 --- a/prusti-tests/tests/verify/fail/user-guide/peek_mut_pledges.rs +++ b/prusti-tests/tests/verify/fail/user-guide/peek_mut_pledges.rs @@ -17,32 +17,6 @@ struct Node { next: Link, } -#[extern_spec(std::mem)] -#[ensures(snap(dest) === src)] -#[ensures(result === old(snap(dest)))] -fn replace(dest: &mut T, src: T) -> T; - -// Specs for std::option::Option::unwrap(self) (and others) can be found here (work in progress): -// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49 - -#[extern_spec] -impl std::option::Option { - #[requires(self.is_some())] - #[ensures(old(self) === Some(result))] - pub fn unwrap(self) -> T; - - #[pure] - #[ensures(result == matches!(self, None))] - pub const fn is_none(&self) -> bool; - - #[pure] - #[ensures(result == matches!(self, Some(_)))] - pub const fn is_some(&self) -> bool; - - #[ensures(result === old(snap(self)))] - #[ensures(self.is_none())] - pub fn take(&mut self) -> Option; -} //// ANCHOR: peek_mut_code impl List { //// ANCHOR_END: peek_mut_code diff --git a/prusti-tests/tests/verify/fail/user-guide/pop.rs b/prusti-tests/tests/verify/fail/user-guide/pop.rs index 95c2eec5369..b7426c55ecc 100644 --- a/prusti-tests/tests/verify/fail/user-guide/pop.rs +++ b/prusti-tests/tests/verify/fail/user-guide/pop.rs @@ -29,7 +29,7 @@ impl List { pub fn len(&self) -> usize { self.head.len() } - + //// ANCHOR: is_empty #[pure] fn is_empty(&self) -> bool { @@ -50,7 +50,7 @@ impl List { self.head.lookup(index) } - #[ensures(self.len() == old(self.len()) + 1)] //~ ERROR postcondition might not hold + #[ensures(self.len() == old(self.len()) + 1)] #[ensures(self.lookup(0) == elem)] #[ensures(forall(|i: usize| (i < old(self.len())) ==> old(self.lookup(i)) == self.lookup(i + 1)))] @@ -73,13 +73,13 @@ impl List { }, } } - + //// ANCHOR_END: initial //// ANCHOR: pop_precondition #[requires(!self.is_empty())] //// ANCHOR: initial pub fn pop(&mut self) -> i32 { - self.try_pop().unwrap() + self.try_pop().unwrap() //~ ERROR precondition might not hold } //// ANCHOR: is_empty } @@ -99,10 +99,10 @@ impl Link { node.next.lookup(index - 1) } }, - Link::Empty => unreachable!(), + Link::Empty => unreachable!(), } } - + #[pure] fn len(&self) -> usize { match self { diff --git a/prusti-tests/tests/verify/fail/user-guide/push_property_2_missing_bounds.rs b/prusti-tests/tests/verify/fail/user-guide/push_property_2_missing_bounds.rs index fbbeec1a421..15bb4a4bfd0 100644 --- a/prusti-tests/tests/verify/fail/user-guide/push_property_2_missing_bounds.rs +++ b/prusti-tests/tests/verify/fail/user-guide/push_property_2_missing_bounds.rs @@ -18,11 +18,6 @@ struct Node { next: Link, } -#[extern_spec(std::mem)] -#[ensures(snap(dest) === src)] -#[ensures(result === old(snap(dest)))] -fn replace(dest: &mut T, src: T) -> T; - //// ANCHOR: lookup impl List { #[pure] diff --git a/prusti-tests/tests/verify/pass/crates/ansi-term-external-call.rs b/prusti-tests/tests/verify/pass/crates/ansi-term-external-call.rs index 99fc5219402..88127288a19 100644 --- a/prusti-tests/tests/verify/pass/crates/ansi-term-external-call.rs +++ b/prusti-tests/tests/verify/pass/crates/ansi-term-external-call.rs @@ -100,6 +100,7 @@ impl Default for Style { /// assert_eq!(false, Style::default().is_bold); /// assert_eq!("txt", Style::default().paint("txt").to_string()); /// ``` + #[pure] fn default() -> Style { Style { is_bold: false, diff --git a/prusti-tests/tests/verify/pass/user-guide/assert_on_expiry.rs b/prusti-tests/tests/verify/pass/user-guide/assert_on_expiry.rs index 1d01faef70b..6ba6a46639d 100644 --- a/prusti-tests/tests/verify/pass/user-guide/assert_on_expiry.rs +++ b/prusti-tests/tests/verify/pass/user-guide/assert_on_expiry.rs @@ -17,32 +17,6 @@ struct Node { next: Link, } -#[extern_spec(std::mem)] -#[ensures(snap(dest) === src)] -#[ensures(result === old(snap(dest)))] -fn replace(dest: &mut T, src: T) -> T; - -// Specs for std::option::Option::unwrap(self) (and others) can be found here (work in progress): -// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49 - -#[extern_spec] -impl std::option::Option { - #[requires(self.is_some())] - #[ensures(old(self) === Some(result))] - pub fn unwrap(self) -> T; - - #[pure] - #[ensures(result == matches!(self, None))] - pub const fn is_none(&self) -> bool; - - #[pure] - #[ensures(result == matches!(self, Some(_)))] - pub const fn is_some(&self) -> bool; - - #[ensures(result === old(snap(self)))] - #[ensures(self.is_none())] - pub fn take(&mut self) -> Option; -} //// ANCHOR: pledge impl List { //// ANCHOR_END: pledge diff --git a/prusti-tests/tests/verify/pass/user-guide/generic.rs b/prusti-tests/tests/verify/pass/user-guide/generic.rs index 8f25ba1da4e..0cf6d00cb93 100644 --- a/prusti-tests/tests/verify/pass/user-guide/generic.rs +++ b/prusti-tests/tests/verify/pass/user-guide/generic.rs @@ -20,32 +20,6 @@ struct Node { } //// ANCHOR_END: generic_types -#[extern_spec(std::mem)] -#[ensures(snap(dest) === src)] -#[ensures(result === old(snap(dest)))] -fn replace(dest: &mut T, src: T) -> T; - -// Specs for std::option::Option::unwrap(self) (and others) can be found here (work in progress): -// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49 - -#[extern_spec] -impl std::option::Option { - #[requires(self.is_some())] - #[ensures(old(self) === Some(result))] - pub fn unwrap(self) -> T; - - #[pure] - #[ensures(result == matches!(self, None))] - pub const fn is_none(&self) -> bool; - - #[pure] - #[ensures(result == matches!(self, Some(_)))] - pub const fn is_some(&self) -> bool; - - #[ensures(result === old(snap(self)))] - #[ensures(self.is_none())] - pub fn take(&mut self) -> Option; -} //// ANCHOR: generic_types //// ANCHOR: lookup_reference @@ -142,8 +116,8 @@ impl List { } } //// ANCHOR_END: lookup_reference - //// ANCHOR_END: generic_types + #[pure] #[requires(index < link_len(link))] //// ANCHOR: lookup_reference @@ -171,13 +145,11 @@ fn link_len(link: &Link) -> usize { } } -//// ANCHOR: generic_types //// ANCHOR: lookup_reference #[cfg(prusti)] mod prusti_tests { use super::*; - //// ANCHOR_END: generic_types fn _test_list(){ // ... //// ANCHOR_END: lookup_reference @@ -208,5 +180,4 @@ mod prusti_tests { //// ANCHOR: lookup_reference } } -//// ANCHOR_END: generic_types //// ANCHOR_END: lookup_reference \ No newline at end of file diff --git a/prusti-tests/tests/verify/pass/user-guide/option.rs b/prusti-tests/tests/verify/pass/user-guide/option.rs index 48d75f37026..b2e8c4fb3cb 100644 --- a/prusti-tests/tests/verify/pass/user-guide/option.rs +++ b/prusti-tests/tests/verify/pass/user-guide/option.rs @@ -17,39 +17,6 @@ struct Node { next: Link, } -//// ANCHOR: option_take_extern_spec -#[extern_spec(std::mem)] -#[ensures(snap(dest) === src)] -#[ensures(result === old(snap(dest)))] -fn replace(dest: &mut T, src: T) -> T; - -//// ANCHOR_END: option_take_extern_spec -// Specs for std::option::Option::unwrap(self) (and others) can be found here (work in progress): -// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49 - -//// ANCHOR: option_take_extern_spec -#[extern_spec] -impl std::option::Option { - //// ANCHOR_END: option_take_extern_spec - #[requires(self.is_some())] - #[ensures(old(self) === Some(result))] - pub fn unwrap(self) -> T; - - #[pure] - #[ensures(result == matches!(self, None))] - pub const fn is_none(&self) -> bool; - - #[pure] - #[ensures(result == matches!(self, Some(_)))] - pub const fn is_some(&self) -> bool; - - //// ANCHOR: option_take_extern_spec - #[ensures(result === old(snap(self)))] - #[ensures(self.is_none())] - pub fn take(&mut self) -> Option; -} -//// ANCHOR_END: option_take_extern_spec - //// ANCHOR: try_pop_rewrite //// ANCHOR: rewrite_link_impl impl List { @@ -121,7 +88,7 @@ impl List { } } - // // This will likely work in the future, but doesn't currently (even if you provide an `extern_spec` for `Option::map`): + // // This will likely work in the future, but doesn't currently: // // Currently you get this error: // // [Prusti: unsupported feature] unsupported creation of unique borrows (implicitly created in closure bindings) // pub fn try_pop(&mut self) -> Option { diff --git a/prusti-tests/tests/verify/pass/user-guide/peek.rs b/prusti-tests/tests/verify/pass/user-guide/peek.rs index a964451fe4e..8cee81dcbfe 100644 --- a/prusti-tests/tests/verify/pass/user-guide/peek.rs +++ b/prusti-tests/tests/verify/pass/user-guide/peek.rs @@ -17,33 +17,6 @@ struct Node { next: Link, } -#[extern_spec(std::mem)] -#[ensures(snap(dest) === src)] -#[ensures(result === old(snap(dest)))] -fn replace(dest: &mut T, src: T) -> T; - -// Specs for std::option::Option::unwrap(self) (and others) can be found here (work in progress): -// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49 - -#[extern_spec] -impl std::option::Option { - #[requires(self.is_some())] - #[ensures(old(self) === Some(result))] - pub fn unwrap(self) -> T; - - #[pure] - #[ensures(result == matches!(self, None))] - pub const fn is_none(&self) -> bool; - - #[pure] - #[ensures(result == matches!(self, Some(_)))] - pub const fn is_some(&self) -> bool; - - #[ensures(result === old(snap(self)))] - #[ensures(self.is_none())] - pub fn take(&mut self) -> Option; -} - //// ANCHOR: implementation impl List { //// ANCHOR_END: implementation diff --git a/prusti-tests/tests/verify/pass/user-guide/peek_mut_pledges.rs b/prusti-tests/tests/verify/pass/user-guide/peek_mut_pledges.rs index e083b676514..19d99b3cbc1 100644 --- a/prusti-tests/tests/verify/pass/user-guide/peek_mut_pledges.rs +++ b/prusti-tests/tests/verify/pass/user-guide/peek_mut_pledges.rs @@ -17,32 +17,6 @@ struct Node { next: Link, } -#[extern_spec(std::mem)] -#[ensures(snap(dest) === src)] -#[ensures(result === old(snap(dest)))] -fn replace(dest: &mut T, src: T) -> T; - -// Specs for std::option::Option::unwrap(self) (and others) can be found here (work in progress): -// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49 - -#[extern_spec] -impl std::option::Option { - #[requires(self.is_some())] - #[ensures(old(self) === Some(result))] - pub fn unwrap(self) -> T; - - #[pure] - #[ensures(result == matches!(self, None))] - pub const fn is_none(&self) -> bool; - - #[pure] - #[ensures(result == matches!(self, Some(_)))] - pub const fn is_some(&self) -> bool; - - #[ensures(result === old(snap(self)))] - #[ensures(self.is_none())] - pub fn take(&mut self) -> Option; -} //// ANCHOR: pledge impl List { //// ANCHOR_END: pledge diff --git a/prusti-tests/tests/verify/pass/user-guide/pop.rs b/prusti-tests/tests/verify/pass/user-guide/pop.rs index b2026b18b3f..f40290d4d85 100644 --- a/prusti-tests/tests/verify/pass/user-guide/pop.rs +++ b/prusti-tests/tests/verify/pass/user-guide/pop.rs @@ -20,31 +20,6 @@ struct Node { next: Link, } -//// ANCHOR: extern_spec -#[extern_spec(std::mem)] -#[ensures(snap(dest) === src)] -#[ensures(result === old(snap(dest)))] -fn replace(dest: &mut T, src: T) -> T; - -// Specs for std::option::Option::unwrap(self) (and others) can be found here (work in progress): -// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49 - -#[extern_spec] -impl std::option::Option { - #[requires(self.is_some())] - #[ensures(old(self) === Some(result))] - pub fn unwrap(self) -> T; - - #[pure] - #[ensures(result == matches!(self, None))] - pub const fn is_none(&self) -> bool; - - #[pure] - #[ensures(result == matches!(self, Some(_)))] - pub const fn is_some(&self) -> bool; -} -//// ANCHOR_END: extern_spec - //// ANCHOR: two_state_predicate //// ANCHOR: predicate_use //// ANCHOR: try_pop_empty diff --git a/prusti-tests/tests/verify/pass/user-guide/push_final_code.rs b/prusti-tests/tests/verify/pass/user-guide/push_final_code.rs index 30f3e9efaaf..72601b7420f 100644 --- a/prusti-tests/tests/verify/pass/user-guide/push_final_code.rs +++ b/prusti-tests/tests/verify/pass/user-guide/push_final_code.rs @@ -20,11 +20,6 @@ struct Node { next: Link, } -#[extern_spec(std::mem)] -#[ensures(snap(dest) === src)] -#[ensures(result === old(snap(dest)))] -fn replace(dest: &mut T, src: T) -> T; - //// ANCHOR: shifted_back impl List { //// ANCHOR_END: shifted_back diff --git a/prusti-tests/tests/verify/pass/user-guide/push_property_1.rs b/prusti-tests/tests/verify/pass/user-guide/push_property_1.rs index 4eb11dd92cb..f0be7f169a1 100644 --- a/prusti-tests/tests/verify/pass/user-guide/push_property_1.rs +++ b/prusti-tests/tests/verify/pass/user-guide/push_property_1.rs @@ -18,13 +18,6 @@ struct Node { next: Link, } -//// ANCHOR: extern_spec -#[extern_spec(std::mem)] -#[ensures(snap(dest) === src)] -#[ensures(result === old(snap(dest)))] -fn replace(dest: &mut T, src: T) -> T; -//// ANCHOR_END: extern_spec - //// ANCHOR: property_1 impl List { #[ensures(self.len() == old(self.len()) + 1)] // 1. Property diff --git a/prusti-tests/tests/verify/pass/user-guide/push_property_2_with_bounds.rs b/prusti-tests/tests/verify/pass/user-guide/push_property_2_with_bounds.rs index 47c9baeae60..fc54e6663ef 100644 --- a/prusti-tests/tests/verify/pass/user-guide/push_property_2_with_bounds.rs +++ b/prusti-tests/tests/verify/pass/user-guide/push_property_2_with_bounds.rs @@ -18,11 +18,6 @@ struct Node { next: Link, } -#[extern_spec(std::mem)] -#[ensures(snap(dest) === src)] -#[ensures(result === old(snap(dest)))] -fn replace(dest: &mut T, src: T) -> T; - //// ANCHOR: bounds impl List { #[pure] diff --git a/prusti-tests/tests/verify/pass/user-guide/testing_initial_code.rs b/prusti-tests/tests/verify/pass/user-guide/testing_initial_code.rs index 4e2d1de1b7a..94f6e7dff16 100644 --- a/prusti-tests/tests/verify/pass/user-guide/testing_initial_code.rs +++ b/prusti-tests/tests/verify/pass/user-guide/testing_initial_code.rs @@ -18,29 +18,6 @@ struct Node { next: Link, } -#[extern_spec(std::mem)] -#[ensures(snap(dest) === src)] -#[ensures(result === old(snap(dest)))] -fn replace(dest: &mut T, src: T) -> T; - -// Specs for std::option::Option::unwrap(self) (and others) can be found here (work in progress): -// https://github.com/viperproject/prusti-dev/pull/1249/files#diff-bccda07f8a48357687e26408251041072c7470c188092fb58439de39974bdab5R47-R49 - -#[extern_spec] -impl std::option::Option { - #[requires(self.is_some())] - #[ensures(old(self) === Some(result))] - pub fn unwrap(self) -> T; - - #[pure] - #[ensures(result == matches!(self, None))] - pub const fn is_none(&self) -> bool; - - #[pure] - #[ensures(result == matches!(self, Some(_)))] - pub const fn is_some(&self) -> bool; -} - impl List { #[pure] pub fn len(&self) -> usize { diff --git a/prusti-tests/tests/verify_overflow/fail/core_proof/loops.rs b/prusti-tests/tests/verify_overflow/fail/core_proof/loops.rs index 8cd19f53d21..00365dce4f8 100644 --- a/prusti-tests/tests/verify_overflow/fail/core_proof/loops.rs +++ b/prusti-tests/tests/verify_overflow/fail/core_proof/loops.rs @@ -107,6 +107,7 @@ fn next3() -> Result, E> { Ok(None) } +/* fn test11() -> Result { while let Some(n) = next3()? { } Err(E) @@ -121,21 +122,21 @@ fn test12() -> Result { fn test13() -> Result { while let Some(n) = next3()? { - assert!(false); //~ ERROR: the asserted expression might not hold + assert!(false); ERROR: the asserted expression might not hold } Err(E) } fn test14() -> Result { while let Some(n) = next3()? { } - assert!(false); //~ ERROR: the asserted expression might not hold + assert!(false); ERROR: the asserted expression might not hold Err(E) } fn test15() -> Result { while let Some(n) = next3()? { body_invariant!(true); - assert!(false); //~ ERROR: the asserted expression might not hold + assert!(false); ERROR: the asserted expression might not hold } Err(E) } @@ -144,7 +145,7 @@ fn test16() -> Result { while let Some(n) = next3()? { body_invariant!(true); } - assert!(false); //~ ERROR: the asserted expression might not hold + assert!(false); ERROR: the asserted expression might not hold Err(E) } @@ -167,6 +168,7 @@ fn test18() -> Result { } Err(E) } +*/ fn next4() -> u32 { 4 diff --git a/prusti-tests/tests/verify_overflow/pass/binary_search.rs b/prusti-tests/tests/verify_overflow/pass/binary_search.rs index b1db1525339..02af81e0962 100644 --- a/prusti-tests/tests/verify_overflow/pass/binary_search.rs +++ b/prusti-tests/tests/verify_overflow/pass/binary_search.rs @@ -1,16 +1,5 @@ use prusti_contracts::*; -#[extern_spec] -impl std::option::Option { - #[pure] - #[ensures(matches!(*self, Some(_)) == result)] - pub fn is_some(&self) -> bool; - - #[pure] - #[ensures(self.is_some() == !result)] - pub fn is_none(&self) -> bool; -} - // cloned unwrap #[trusted] #[pure] @@ -19,7 +8,9 @@ impl std::option::Option { Some(value) => *value == result, None => unreachable!(), })] -fn option_peek(opt: &Option) -> usize { unimplemented!() } +fn option_peek(opt: &Option) -> usize { + unimplemented!() +} fn main() {} diff --git a/prusti-tests/tests/verify_overflow/pass/copy/erase-regions.rs b/prusti-tests/tests/verify_overflow/pass/copy/erase-regions.rs index 3c5d4759246..69fe24797bf 100644 --- a/prusti-tests/tests/verify_overflow/pass/copy/erase-regions.rs +++ b/prusti-tests/tests/verify_overflow/pass/copy/erase-regions.rs @@ -6,12 +6,8 @@ struct Iter<'a, #[generic] T: Copy> { position: usize, } -type SliceTy = [T]; #[extern_spec] -impl SliceTy { - #[pure] - fn len(&self) -> usize; - +impl [T] { #[ensures( result.model().position == 0 )] fn iter(&self) -> std::slice::Iter<'_, T>; } @@ -20,6 +16,4 @@ fn verify_slice_iter(slice: &[i32]) { let iter = slice.iter(); } -fn main() { - -} \ No newline at end of file +fn main() {} diff --git a/prusti-tests/tests/verify_overflow/pass/extern-spec/linked-list.rs b/prusti-tests/tests/verify_overflow/pass/extern-spec/linked-list.rs index d502713c4cd..d681199acf1 100644 --- a/prusti-tests/tests/verify_overflow/pass/extern-spec/linked-list.rs +++ b/prusti-tests/tests/verify_overflow/pass/extern-spec/linked-list.rs @@ -3,24 +3,6 @@ use prusti_contracts::*; use std::collections::LinkedList; -use std::option::Option; - -#[extern_spec] -impl std::option::Option { - #[pure] - #[ensures(matches!(*self, Some(_)) == result)] - pub fn is_some(&self) -> bool; - - #[pure] - #[ensures(self.is_some() == !result)] - pub fn is_none(&self) -> bool; - - #[requires(self.is_some())] - pub fn unwrap(self) -> T; - - #[requires(self.is_some())] - pub fn expect(self, msg: &str) -> T; -} /// Ghost method for LinkedList used to access an index in the LinkedList #[trusted] @@ -37,7 +19,9 @@ fn get(list: &LinkedList, index #[extern_spec] impl LinkedList - where T: Copy + PartialEq { +where + T: Copy + PartialEq, +{ #[ensures(result.is_empty())] pub fn new() -> LinkedList; diff --git a/prusti-tests/tests/verify_overflow/pass/extern-spec/map.rs b/prusti-tests/tests/verify_overflow/pass/extern-spec/map.rs index 9cf4cc00adf..2ec5fa8ce0c 100644 --- a/prusti-tests/tests/verify_overflow/pass/extern-spec/map.rs +++ b/prusti-tests/tests/verify_overflow/pass/extern-spec/map.rs @@ -1,16 +1,14 @@ use prusti_contracts::*; #[extern_spec] -impl std::option::Option { - #[pure] - pub fn is_some(&self) -> bool; -} - -#[extern_spec] -impl std::collections::HashMap { +impl ::std::collections::hash_map::HashMap +where + K: Eq + ::core::hash::Hash, + S: ::std::hash::BuildHasher, +{ #[pure] #[ensures(result.is_some() == self.contains_key(k))] - pub fn get<'a, Q: ?Sized>(&'a self, k: &Q) -> Option<&'a V> + pub fn get(&self, k: &Q) -> Option<&V> where K: core::borrow::Borrow + std::cmp::Eq + std::hash::Hash, Q: core::hash::Hash + Eq; @@ -18,7 +16,7 @@ impl std::collections::HashMap { #[pure] fn contains_key(&self, k: &Q) -> bool where - K: core::borrow::Borrow + std::cmp::Eq + std::hash::Hash, + K: core::borrow::Borrow + Eq + std::hash::Hash, Q: core::hash::Hash + Eq; } @@ -28,5 +26,4 @@ fn go(key: u32, m: &std::collections::HashMap) { assert!(result.is_some()) } -fn main(){ -} +fn main() {} diff --git a/prusti-tests/tests/verify_overflow/pass/extern-spec/map_unchanged.rs b/prusti-tests/tests/verify_overflow/pass/extern-spec/map_unchanged.rs index 936f49dbf63..2ec5fa8ce0c 100644 --- a/prusti-tests/tests/verify_overflow/pass/extern-spec/map_unchanged.rs +++ b/prusti-tests/tests/verify_overflow/pass/extern-spec/map_unchanged.rs @@ -1,13 +1,11 @@ use prusti_contracts::*; #[extern_spec] -impl std::option::Option { - #[pure] - pub fn is_some(&self) -> bool; -} - -#[extern_spec] -impl std::collections::HashMap { +impl ::std::collections::hash_map::HashMap +where + K: Eq + ::core::hash::Hash, + S: ::std::hash::BuildHasher, +{ #[pure] #[ensures(result.is_some() == self.contains_key(k))] pub fn get(&self, k: &Q) -> Option<&V> @@ -18,7 +16,7 @@ impl std::collections::HashMap { #[pure] fn contains_key(&self, k: &Q) -> bool where - K: core::borrow::Borrow + std::cmp::Eq + std::hash::Hash, + K: core::borrow::Borrow + Eq + std::hash::Hash, Q: core::hash::Hash + Eq; } @@ -28,5 +26,4 @@ fn go(key: u32, m: &std::collections::HashMap) { assert!(result.is_some()) } -fn main(){ -} +fn main() {} diff --git a/prusti-tests/tests/verify_overflow/pass/extern-spec/option.rs b/prusti-tests/tests/verify_overflow/pass/extern-spec/option.rs index 73d6f556f48..760110b54ec 100644 --- a/prusti-tests/tests/verify_overflow/pass/extern-spec/option.rs +++ b/prusti-tests/tests/verify_overflow/pass/extern-spec/option.rs @@ -1,31 +1,5 @@ use prusti_contracts::*; -#[extern_spec] -impl std::option::Option { - #[pure] - #[ensures(matches!(*self, Some(_)) == result)] - pub fn is_some(&self) -> bool; - - #[pure] - #[ensures(self.is_some() == !result)] - pub fn is_none(&self) -> bool; - - #[requires(self.is_some())] - pub fn unwrap(self) -> T; - - pub fn unwrap_or(self, default: T) -> T; - - pub fn unwrap_or_else(self, f: F) -> T - where F: FnOnce() -> T; - - #[requires(self.is_some())] - pub fn expect(self, msg: &str) -> T; - - pub fn as_ref(&self) -> Option<&T>; - - pub fn as_mut(&mut self) -> Option<&mut T>; -} - fn main() { let mut x = Some(3); assert!(x.is_some()); diff --git a/prusti-tests/tests/verify_overflow/pass/extern-spec/set.rs b/prusti-tests/tests/verify_overflow/pass/extern-spec/set.rs index 06344a1b133..1f080b9ae3e 100644 --- a/prusti-tests/tests/verify_overflow/pass/extern-spec/set.rs +++ b/prusti-tests/tests/verify_overflow/pass/extern-spec/set.rs @@ -1,24 +1,12 @@ use prusti_contracts::*; -use std::collections::HashSet; -use std::borrow::Borrow; -use std::hash::{BuildHasher, Hash}; -use std::cmp::Eq; -use std::option::Option; - -#[extern_spec] -impl Option { - #[pure] - #[ensures(matches!(*self, Some(_)) == result)] - pub fn is_some(&self) -> bool; - - #[pure] - #[ensures(result != self.is_some())] - pub fn is_none(&self) -> bool; - - #[requires(self.is_some())] - pub fn unwrap(self) -> T; -} +use std::{ + borrow::Borrow, + cmp::Eq, + collections::HashSet, + hash::{BuildHasher, Hash}, + option::Option, +}; #[extern_spec] impl HashSet { @@ -47,9 +35,9 @@ where { #[pure] pub fn contains(&self, value: &Q) -> bool - where - T: std::borrow::Borrow, - Q: std::hash::Hash + std::cmp::Eq; + where + T: std::borrow::Borrow, + Q: std::hash::Hash + std::cmp::Eq; #[ensures(self.len() == old(self.len()) + 1)] pub fn insert(&mut self, value: T) -> bool; diff --git a/prusti-tests/tests/verify_overflow/pass/extern-spec/swap.rs b/prusti-tests/tests/verify_overflow/pass/extern-spec/swap.rs index 95098299184..ccc71005e47 100644 --- a/prusti-tests/tests/verify_overflow/pass/extern-spec/swap.rs +++ b/prusti-tests/tests/verify_overflow/pass/extern-spec/swap.rs @@ -4,14 +4,6 @@ use prusti_contracts::*; -#[extern_spec] -mod std { - mod mem { - #[ensures(*a == old(*b) && *b == old(*a))] - pub fn swap(a: &mut T, b: &mut T); - } -} - fn main() { let mut x = 5; let mut y = 42; diff --git a/prusti-tests/tests/verify_overflow/pass/extern-spec/vec-3.rs b/prusti-tests/tests/verify_overflow/pass/extern-spec/vec-3.rs index 42963b298b8..c8a29fcca05 100644 --- a/prusti-tests/tests/verify_overflow/pass/extern-spec/vec-3.rs +++ b/prusti-tests/tests/verify_overflow/pass/extern-spec/vec-3.rs @@ -1,28 +1,12 @@ #![feature(allocator_api)] use prusti_contracts::*; -use std::vec::Vec; -use std::option::Option; - -#[extern_spec] -impl Option { - #[pure] - #[ensures(matches!(*self, Some(_)) == result)] - pub fn is_some(&self) -> bool; - - #[pure] - #[ensures(self.is_some() ==> !result)] - #[ensures(!self.is_some() ==> result)] - pub fn is_none(&self) -> bool; - - #[requires(self.is_some())] - pub fn unwrap(self) -> T; -} +use std::{option::Option, vec::Vec}; #[extern_spec] impl Vec { #[ensures(result.len() == 0)] - fn new() -> Vec::; + fn new() -> Vec; } #[extern_spec] diff --git a/prusti-tests/tests/verify_overflow/pass/trait-contracts-refinement/refine-non-local-type-with-generics.rs b/prusti-tests/tests/verify_overflow/pass/trait-contracts-refinement/refine-non-local-type-with-generics.rs index a182a62242d..22ba19eea21 100644 --- a/prusti-tests/tests/verify_overflow/pass/trait-contracts-refinement/refine-non-local-type-with-generics.rs +++ b/prusti-tests/tests/verify_overflow/pass/trait-contracts-refinement/refine-non-local-type-with-generics.rs @@ -1,17 +1,5 @@ use prusti_contracts::*; -#[extern_spec] -impl std::option::Option { - #[pure] - #[ensures(matches!(*self, Some(_)) == result)] - pub fn is_some(&self) -> bool; - - #[pure] - #[ensures(self.is_some() == ! result)] - #[ensures(matches!(*self, None) == result)] - pub fn is_none(&self) -> bool; -} - trait OptionPeeker { #[pure] #[requires(false)] @@ -33,4 +21,4 @@ impl OptionPeeker for Option { fn main() { let o = Some(5); assert!(o.peek() == 5); -} \ No newline at end of file +} diff --git a/prusti-viper/src/encoder/mir/specifications/constraints.rs b/prusti-viper/src/encoder/mir/specifications/constraints.rs index 882d895cc53..e12376535d4 100644 --- a/prusti-viper/src/encoder/mir/specifications/constraints.rs +++ b/prusti-viper/src/encoder/mir/specifications/constraints.rs @@ -186,7 +186,11 @@ 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).instantiate(env.tcx(), trait_substs) + let combined = trait_substs + .iter() + .chain(context.substs.iter()) + .collect::>(); + ty::EarlyBinder::bind(param_env).instantiate(env.tcx(), &combined) } else { param_env }; diff --git a/x.py b/x.py index 8dc7ed8c063..9549ab20b84 100755 --- a/x.py +++ b/x.py @@ -238,8 +238,10 @@ def fmt_check_all(): def check_smir(): """Check that `extern crate` is used only in `prusti_rustc_interface` (TODO: `prusti_interface` is also ignored for now).""" + # also ignore prusti-contracts because the prusti-std needs std but is no_std to make it conditional (https://doc.rust-lang.org/edition-guide/rust-2018/path-changes.html) + blacklist = set(['prusti-rustc-interface', 'prusti-interface', 'prusti-contracts']) for folder in os.listdir('.'): - if folder == 'prusti-rustc-interface' or folder == 'prusti-interface': + if folder in blacklist: continue if os.path.exists(os.path.join(folder, 'Cargo.toml')): completed = subprocess.run(