diff --git a/Cargo.lock b/Cargo.lock index f94867f0293..61726bfb7fe 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -64,9 +64,9 @@ dependencies = [ [[package]] name = "anyhow" -version = "1.0.68" +version = "1.0.69" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2cb2f989d18dd141ab8ae82f64d1a8cdd37e0840f73a406896cf5e99502fab61" +checksum = "224afbd727c3d6e4b90103ece64b8d1b67fbb1973b1046c2281eed3f3803f800" [[package]] name = "async-attributes" @@ -140,12 +140,11 @@ dependencies = [ [[package]] name = "async-lock" -version = "2.6.0" +version = "2.7.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c8101efe8695a6c17e02911402145357e718ac92d3ff88ae8419e84b1707b685" +checksum = "fa24f727524730b077666307f2734b4a1a1c57acb79193127dcc8914d5242dd7" dependencies = [ "event-listener", - "futures-lite", ] [[package]] @@ -194,6 +193,28 @@ dependencies = [ "wasm-bindgen-futures", ] +[[package]] +name = "async-stream" +version = "0.3.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ad445822218ce64be7a341abfb0b1ea43b5c23aa83902542a4542e78309d8e5e" +dependencies = [ + "async-stream-impl", + "futures-core", + "pin-project-lite", +] + +[[package]] +name = "async-stream-impl" +version = "0.3.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e4655ae1a7b0cdf149156f780c5bf3f1352bc53cbd9e0a361a7ef7b22947e965" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + [[package]] name = "async-task" version = "4.3.0" @@ -202,9 +223,9 @@ checksum = "7a40729d2133846d9ed0ea60a8b9541bccddab49cd30f0715a1da672fe9a2524" [[package]] name = "async-trait" -version = "0.1.60" +version = "0.1.66" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "677d1d8ab452a3936018a687b20e6f7cf5363d713b732b8884001317b0e48aa3" +checksum = "b84f9ebcc6c1f5b8cb160f6990096a5c127f423fcb6e1ccc46c370cbdfb75dfc" dependencies = [ "proc-macro2", "quote", @@ -213,9 +234,9 @@ dependencies = [ [[package]] name = "atomic-waker" -version = "1.0.0" +version = "1.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "065374052e7df7ee4047b1160cca5e1467a12351a40b3da123c870ba0b8eda2a" +checksum = "debc29dde2e69f9e47506b525f639ed42300fc014a3e007832592448fa8e4599" [[package]] name = "attohttpc" @@ -297,6 +318,15 @@ version = "1.3.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a" +[[package]] +name = "block-buffer" +version = "0.9.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4152116fd6e9dadb291ae18fc1ec3575ed6d84c29642d97890f4b4a3417297e4" +dependencies = [ + "generic-array", +] + [[package]] name = "block-buffer" version = "0.10.3" @@ -320,18 +350,6 @@ dependencies = [ "futures-lite", ] -[[package]] -name = "bstr" -version = "0.2.17" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ba3569f383e8f1598449f1a423e72e99569137b47740b1da11ef19af3d5c3223" -dependencies = [ - "lazy_static", - "memchr", - "regex-automata", - "serde", -] - [[package]] name = "buf_redux" version = "0.8.4" @@ -344,9 +362,9 @@ dependencies = [ [[package]] name = "bumpalo" -version = "3.11.1" +version = "3.12.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "572f695136211188308f16ad2ca5c851a712c464060ae6974944458eb83880ba" +checksum = "0d261e256854913907f67ed06efbc3338dfe6179796deefc1ff763fc1aee5535" [[package]] name = "byteorder" @@ -356,9 +374,9 @@ checksum = "14c189c53d098945499cdfa7ecc63567cf3886b3332b312a5b4585d8d3a6a610" [[package]] name = "bytes" -version = "1.3.0" +version = "1.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "dfb24e866b15a1af2a1b663f10c6b6b8f397a84aadb828f12e5b289ec23a3a3c" +checksum = "89b2fd2a0dcf38d7971e2194b6b6eebab45ae01067456a7fd93d5547a61b70be" [[package]] name = "cargo-test-macro" @@ -411,9 +429,9 @@ dependencies = [ [[package]] name = "cc" -version = "1.0.78" +version = "1.0.79" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a20104e2335ce8a659d6dd92a51a767a0c062599c73b343fd152cb401e828c3d" +checksum = "50d30906286121d95be3d479533b458f87493b30a4b5f79a607db8f5d11aa91f" dependencies = [ "jobserver", ] @@ -444,9 +462,9 @@ dependencies = [ [[package]] name = "clap" -version = "4.0.32" +version = "4.1.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a7db700bc935f9e43e88d00b0850dae18a63773cfbec6d8e070fccf7fef89a39" +checksum = "c3d7ae14b20b94cb02149ed21a86c423859cbe18dc7ed69845cace50e52b40a5" dependencies = [ "bitflags", "clap_derive", @@ -459,9 +477,9 @@ dependencies = [ [[package]] name = "clap_derive" -version = "4.0.21" +version = "4.1.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0177313f9f02afc995627906bbd8967e2be069f5261954222dac78290c2b9014" +checksum = "44bec8e5c9d09e439c4335b1af0abaab56dcf3b94999a936e1bb47b9134288f0" dependencies = [ "heck", "proc-macro-error", @@ -472,9 +490,9 @@ dependencies = [ [[package]] name = "clap_lex" -version = "0.3.0" +version = "0.3.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0d4198f73e42b4936b35b5bb248d81d2b595ecb170da0bac7655c54eedfa8da8" +checksum = "350b9cf31731f9957399229e9b2adc51eeabdfbe9d71d9a0552275fd12710d09" dependencies = [ "os_str_bytes", ] @@ -569,9 +587,9 @@ checksum = "d6417fe6fc03a8b533fd2177742eeb39a90c7233eedec7bac96d4d6b69a09449" [[package]] name = "concurrent-queue" -version = "2.0.0" +version = "2.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bd7bef69dc86e3c610e4e7aed41035e2a7ed12e72dd7530f61327a6579a4390b" +checksum = "c278839b831783b70278b14df4d45e1beb1aad306c07bb796637de9a0e323e8e" dependencies = [ "crossbeam-utils", ] @@ -646,9 +664,9 @@ dependencies = [ [[package]] name = "crossbeam-channel" -version = "0.5.6" +version = "0.5.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c2dd04ddaf88237dc3b8d8f9a3c1004b506b54b3313403944054d23c0870c521" +checksum = "cf2b3e8478797446514c91ef04bafcb59faba183e621ad488df88983cc14128c" dependencies = [ "cfg-if", "crossbeam-utils", @@ -656,9 +674,9 @@ dependencies = [ [[package]] name = "crossbeam-deque" -version = "0.8.2" +version = "0.8.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "715e8152b692bba2d374b53d4875445368fdf21a94751410af607a5ac677d1fc" +checksum = "ce6fd6f855243022dcecf8702fef0c297d4338e226845fe067f6341ad9fa0cef" dependencies = [ "cfg-if", "crossbeam-epoch", @@ -667,22 +685,22 @@ dependencies = [ [[package]] name = "crossbeam-epoch" -version = "0.9.13" +version = "0.9.14" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "01a9af1f4c2ef74bb8aa1f7e19706bc72d03598c8a570bb5de72243c7a9d9d5a" +checksum = "46bd5f3f85273295a9d14aedfb86f6aadbff6d8f5295c4a9edb08e819dcf5695" dependencies = [ "autocfg", "cfg-if", "crossbeam-utils", - "memoffset 0.7.1", + "memoffset 0.8.0", "scopeguard", ] [[package]] name = "crossbeam-utils" -version = "0.8.14" +version = "0.8.15" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4fb766fa798726286dbbb842f174001dab8abc7b627a1dd86e0b7222a95d929f" +checksum = "3c063cd8cc95f5c377ed0d4b49a4b21f632396ff690e8470c29b3359b346984b" dependencies = [ "cfg-if", ] @@ -711,13 +729,12 @@ dependencies = [ [[package]] name = "csv" -version = "1.1.6" +version = "1.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "22813a6dc45b335f9bade10bf7271dc477e81113e89eb251a0bc2a8a81c536e1" +checksum = "af91f40b7355f82b0a891f50e70399475945bb0b0da4f1700ce60761c9d3e359" dependencies = [ - "bstr", "csv-core", - "itoa 0.4.8", + "itoa", "ryu", "serde", ] @@ -743,19 +760,19 @@ dependencies = [ [[package]] name = "ctrlc" -version = "3.2.4" +version = "3.2.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1631ca6e3c59112501a9d87fd86f21591ff77acd31331e8a73f8d80a65bbdd71" +checksum = "bbcf33c2a618cbe41ee43ae6e9f2e48368cd9f9db2896f10167d8d762679f639" dependencies = [ - "nix 0.26.1", - "windows-sys 0.42.0", + "nix 0.26.2", + "windows-sys 0.45.0", ] [[package]] name = "cxx" -version = "1.0.85" +version = "1.0.92" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5add3fc1717409d029b20c5b6903fc0c0b02fa6741d820054f4a2efa5e5816fd" +checksum = "9a140f260e6f3f79013b8bfc65e7ce630c9ab4388c6a89c71e07226f49487b72" dependencies = [ "cc", "cxxbridge-flags", @@ -765,9 +782,9 @@ dependencies = [ [[package]] name = "cxx-build" -version = "1.0.85" +version = "1.0.92" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b4c87959ba14bc6fbc61df77c3fcfe180fc32b93538c4f1031dd802ccb5f2ff0" +checksum = "da6383f459341ea689374bf0a42979739dc421874f112ff26f829b8040b8e613" dependencies = [ "cc", "codespan-reporting", @@ -780,15 +797,15 @@ dependencies = [ [[package]] name = "cxxbridge-flags" -version = "1.0.85" +version = "1.0.92" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "69a3e162fde4e594ed2b07d0f83c6c67b745e7f28ce58c6df5e6b6bef99dfb59" +checksum = "90201c1a650e95ccff1c8c0bb5a343213bdd317c6e600a93075bca2eff54ec97" [[package]] name = "cxxbridge-macro" -version = "1.0.85" +version = "1.0.92" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3e7e2adeb6a0d4a282e581096b06e1791532b7d576dcde5ccd9382acf55db8e6" +checksum = "0b75aed41bb2e6367cae39e6326ef817a851db13c13e4f3263714ca3cfb8de56" dependencies = [ "proc-macro2", "quote", @@ -840,13 +857,22 @@ dependencies = [ "nu-ansi-term", ] +[[package]] +name = "digest" +version = "0.9.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d3dd60d1080a57a05ab032377049e0591415d2b31afd7028356dbf3cc6dcb066" +dependencies = [ + "generic-array", +] + [[package]] name = "digest" version = "0.10.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "8168378f4e5023e7218c89c891c0fd8ecdb5e5e4f18cb78f38cf245dd021e76f" dependencies = [ - "block-buffer", + "block-buffer 0.10.3", "crypto-common", ] @@ -885,15 +911,15 @@ checksum = "0bd4b30a6560bbd9b4620f4de34c3f14f60848e58a9b7216801afcb4c7b31c3c" [[package]] name = "either" -version = "1.8.0" +version = "1.8.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "90e5c1c8368803113bf0c9584fc495a58b86dc8a29edbf8fe877d21d9507e797" +checksum = "7fcaabb2fef8c910e7f4c7ce9f67a1283a1715879a7c230ca9d6d1ae31f16d91" [[package]] name = "encoding_rs" -version = "0.8.31" +version = "0.8.32" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9852635589dc9f9ea1b6fe9f05b50ef208c85c834a562f0c6abb1c475736ec2b" +checksum = "071a31f4ee85403370b58aca746f01041ede6f0da2730960ad001edc2b71b394" dependencies = [ "cfg-if", ] @@ -972,23 +998,23 @@ dependencies = [ [[package]] name = "fastrand" -version = "1.8.0" +version = "1.9.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a7a407cfaa3385c4ae6b23e84623d48c2798d06e3e6a1878f7f59f17b3f86499" +checksum = "e51093e27b0797c359783294ca4f0a911c270184cb10f85783b118614a1501be" dependencies = [ "instant", ] [[package]] name = "filetime" -version = "0.2.19" +version = "0.2.20" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4e884668cd0c7480504233e951174ddc3b382f7c2666e3b7310b5c4e7b0c37f9" +checksum = "8a3de6e8d11b22ff9edc6d916f890800597d60f8b2da1caf2955c274638d6412" dependencies = [ "cfg-if", "libc", "redox_syscall", - "windows-sys 0.42.0", + "windows-sys 0.45.0", ] [[package]] @@ -1044,9 +1070,9 @@ dependencies = [ [[package]] name = "futures" -version = "0.3.25" +version = "0.3.26" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "38390104763dc37a5145a53c29c63c1290b5d316d6086ec32c293f6736051bb0" +checksum = "13e2792b0ff0340399d58445b88fd9770e3489eff258a4cbc1523418f12abf84" dependencies = [ "futures-channel", "futures-core", @@ -1059,9 +1085,9 @@ dependencies = [ [[package]] name = "futures-channel" -version = "0.3.25" +version = "0.3.26" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "52ba265a92256105f45b719605a571ffe2d1f0fea3807304b522c1d778f79eed" +checksum = "2e5317663a9089767a1ec00a487df42e0ca174b61b4483213ac24448e4664df5" dependencies = [ "futures-core", "futures-sink", @@ -1069,15 +1095,15 @@ dependencies = [ [[package]] name = "futures-core" -version = "0.3.25" +version = "0.3.26" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "04909a7a7e4633ae6c4a9ab280aeb86da1236243a77b694a49eacd659a4bd3ac" +checksum = "ec90ff4d0fe1f57d600049061dc6bb68ed03c7d2fbd697274c41805dcb3f8608" [[package]] name = "futures-executor" -version = "0.3.25" +version = "0.3.26" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7acc85df6714c176ab5edf386123fafe217be88c0840ec11f199441134a074e2" +checksum = "e8de0a35a6ab97ec8869e32a2473f4b1324459e14c29275d14b10cb1fd19b50e" dependencies = [ "futures-core", "futures-task", @@ -1086,9 +1112,9 @@ dependencies = [ [[package]] name = "futures-io" -version = "0.3.25" +version = "0.3.26" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "00f5fb52a06bdcadeb54e8d3671f8888a39697dcb0b81b23b55174030427f4eb" +checksum = "bfb8371b6fb2aeb2d280374607aeabfc99d95c72edfe51692e42d3d7f0d08531" [[package]] name = "futures-lite" @@ -1107,9 +1133,9 @@ dependencies = [ [[package]] name = "futures-macro" -version = "0.3.25" +version = "0.3.26" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bdfb8ce053d86b91919aad980c220b1fb8401a9394410e1c289ed7e66b61835d" +checksum = "95a73af87da33b5acf53acfebdc339fe592ecf5357ac7c0a7734ab9d8c876a70" dependencies = [ "proc-macro2", "quote", @@ -1118,21 +1144,21 @@ dependencies = [ [[package]] name = "futures-sink" -version = "0.3.25" +version = "0.3.26" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "39c15cf1a4aa79df40f1bb462fb39676d0ad9e366c2a33b590d7c66f4f81fcf9" +checksum = "f310820bb3e8cfd46c80db4d7fb8353e15dfff853a127158425f31e0be6c8364" [[package]] name = "futures-task" -version = "0.3.25" +version = "0.3.26" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2ffb393ac5d9a6eaa9d3fdf37ae2776656b706e200c8e16b1bdb227f5198e6ea" +checksum = "dcf79a1bf610b10f42aea489289c5a2c478a786509693b80cd39c44ccd936366" [[package]] name = "futures-util" -version = "0.3.25" +version = "0.3.26" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "197676987abd2f9cadff84926f410af1c183608d36641465df73ae8211dc65d6" +checksum = "9c1d6de3acfef38d2be4b1f543f553131788603495be83da675e180c8d6b7bd1" dependencies = [ "futures-channel", "futures-core", @@ -1178,9 +1204,9 @@ dependencies = [ [[package]] name = "gimli" -version = "0.27.0" +version = "0.27.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "dec7af912d60cdbd3677c1af9352ebae6fb8394d165568a2234df0fa00f87793" +checksum = "ad0a93d233ebf96623465aad4046a8d3aa4da22d4f4beba5388838c8a434bbb4" [[package]] name = "git2" @@ -1199,15 +1225,15 @@ dependencies = [ [[package]] name = "glob" -version = "0.3.0" +version = "0.3.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9b919933a397b79c37e33b77bb2aa3dc8eb6e165ad809e58ff75bc7db2e34574" +checksum = "d2fabcfbdc87f4758337ca535fb41a6d701b65693ce38287d856d1674551ec9b" [[package]] name = "gloo-timers" -version = "0.2.5" +version = "0.2.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "98c4a8d6391675c6b2ee1a6c8d06e8e2d03605c44cec1270675985a4c2a5500b" +checksum = "9b995a66bb87bebce9a0f4a95aed01daca4872c050bfcb21653361c03bc35e5c" dependencies = [ "futures-channel", "futures-core", @@ -1217,9 +1243,9 @@ dependencies = [ [[package]] name = "h2" -version = "0.3.15" +version = "0.3.16" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5f9f29bc9dda355256b2916cf526ab02ce0aeaaaf2bad60d65ef3f12f11dd0f4" +checksum = "5be7b54589b581f624f566bf5d8eb2bab1db736c51528720b6bd36b96b55924d" dependencies = [ "bytes", "fnv", @@ -1270,9 +1296,9 @@ dependencies = [ [[package]] name = "heck" -version = "0.4.0" +version = "0.4.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2540771e65fc8cb83cd6e8a237f70c319bd5c29f78ed1084ba5d50eeac86f7f9" +checksum = "95505c38b4572b2d910cecb0281560f54b440a19336cbbcb27bf6ce6adc6f5a8" [[package]] name = "hermit-abi" @@ -1292,6 +1318,12 @@ dependencies = [ "libc", ] +[[package]] +name = "hermit-abi" +version = "0.3.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "fed44880c466736ef9a5c5b5facefb5ed0785676d0c02d612db14e54f0d84286" + [[package]] name = "hex" version = "0.3.2" @@ -1306,13 +1338,13 @@ checksum = "7f24254aa9a54b5c858eaee2f5bccdb46aaf0e486a595ed5fd8f86ba55232a70" [[package]] name = "http" -version = "0.2.8" +version = "0.2.9" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "75f43d41e26995c17e71ee126451dd3941010b0514a81a9d11f3b341debc2399" +checksum = "bd6effc99afb63425aff9b05836f029929e345a6148a14b7ecd5ab67af944482" dependencies = [ "bytes", "fnv", - "itoa 1.0.5", + "itoa", ] [[package]] @@ -1346,9 +1378,9 @@ checksum = "9a3a5bfb195931eeb336b2a7b4d761daec841b97f947d34394601737a7bba5e4" [[package]] name = "hyper" -version = "0.14.23" +version = "0.14.24" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "034711faac9d2166cb1baf1a2fb0b60b1f277f8492fd72176c17f3515e1abd3c" +checksum = "5e011372fa0b68db8350aa7a248930ecc7839bf46d8485577d69f117a75f164c" dependencies = [ "bytes", "futures-channel", @@ -1359,7 +1391,7 @@ dependencies = [ "http-body", "httparse", "httpdate", - "itoa 1.0.5", + "itoa", "pin-project-lite", "socket2", "tokio", @@ -1434,6 +1466,15 @@ dependencies = [ "hashbrown", ] +[[package]] +name = "input_buffer" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f97967975f448f1a7ddb12b0bc41069d09ed6a1c161a92687e057325db35d413" +dependencies = [ + "bytes", +] + [[package]] name = "instant" version = "0.1.12" @@ -1445,30 +1486,30 @@ dependencies = [ [[package]] name = "io-lifetimes" -version = "1.0.3" +version = "1.0.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "46112a93252b123d31a119a8d1a1ac19deac4fac6e0e8b0df58f0d4e5870e63c" +checksum = "1abeb7a0dd0f8181267ff8adc397075586500b81b28a73e8a0208b00fc170fb3" dependencies = [ "libc", - "windows-sys 0.42.0", + "windows-sys 0.45.0", ] [[package]] name = "ipnet" -version = "2.7.0" +version = "2.7.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "11b0d96e660696543b251e58030cf9787df56da39dab19ad60eae7353040917e" +checksum = "30e22bd8629359895450b59ea7a776c850561b96a3b1d31321c1949d9e6c9146" [[package]] name = "is-terminal" -version = "0.4.2" +version = "0.4.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "28dfb6c8100ccc63462345b67d1bbc3679177c75ee4bf59bf29c8b1d110b8189" +checksum = "21b6b32576413a8e69b90e952e4a026476040d81017b80445deda5f2d3921857" dependencies = [ - "hermit-abi 0.2.6", + "hermit-abi 0.3.1", "io-lifetimes", "rustix", - "windows-sys 0.42.0", + "windows-sys 0.45.0", ] [[package]] @@ -1482,15 +1523,9 @@ dependencies = [ [[package]] name = "itoa" -version = "0.4.8" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b71991ff56294aa922b450139ee08b3bfc70982c6b2c7562771375cf73542dd4" - -[[package]] -name = "itoa" -version = "1.0.5" +version = "1.0.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fad582f4b9e86b6caa621cabeb0963332d92eea04729ab12892c2533951e6440" +checksum = "453ad9f582a441959e5f0d088b02ce04cfe8d51a8eaf077f12ac6d3e94164ca6" [[package]] name = "jni" @@ -1526,28 +1561,22 @@ checksum = "8eaf4bc02d17cbdd7ff4c7438cafcdf7fb9a4613313ad11b4f8fefe7d3fa0130" [[package]] name = "jobserver" -version = "0.1.25" +version = "0.1.26" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "068b1ee6743e4d11fb9c6a1e6064b3693a1b600e7f5f5988047d98b3dc9fb90b" +checksum = "936cfd212a0155903bcbc060e316fb6cc7cbf2e1907329391ebadc1fe0ce77c2" dependencies = [ "libc", ] [[package]] name = "js-sys" -version = "0.3.60" +version = "0.3.61" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "49409df3e3bf0856b916e2ceaca09ee28e6871cf7d9ce97a692cacfdb2a25a47" +checksum = "445dde2150c55e483f3d8416706b97ec8e8237c307e5b7b4b8dd15e6af2a0730" dependencies = [ "wasm-bindgen", ] -[[package]] -name = "json" -version = "0.12.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "078e285eafdfb6c4b434e0d31e8cfcb5115b651496faca5749b88fafd4f23bfd" - [[package]] name = "json5" version = "0.4.1" @@ -1591,9 +1620,9 @@ checksum = "201de327520df007757c1f0adce6e827fe8562fbc28bfd9c15571c66ca1f5f79" [[package]] name = "libgit2-sys" -version = "0.13.4+1.4.2" +version = "0.13.5+1.4.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d0fa6563431ede25f5cc7f6d803c6afbc1c5d3ad3d4925d12c882bf2b526f5d1" +checksum = "51e5ea06c26926f1002dd553fded6cfcdc9784c1f60feeb58368b4d9b07b6dba" dependencies = [ "cc", "libc", @@ -1693,6 +1722,15 @@ dependencies = [ "autocfg", ] +[[package]] +name = "memoffset" +version = "0.8.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d61c719bcfbcf5d62b3a09efa6088de8c54bc0bfcd3ea7ae39fcc186108b8de1" +dependencies = [ + "autocfg", +] + [[package]] name = "mime" version = "0.3.16" @@ -1726,14 +1764,14 @@ dependencies = [ [[package]] name = "mio" -version = "0.8.5" +version = "0.8.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e5d732bc30207a6423068df043e3d02e0735b155ad7ce1a6f76fe2baa5b158de" +checksum = "5b9d9a46eff5b4ff64b45a9e316a6d1e0bc719ef429cbec4dc630684212bfdf9" dependencies = [ "libc", "log", "wasi", - "windows-sys 0.42.0", + "windows-sys 0.45.0", ] [[package]] @@ -1797,9 +1835,9 @@ dependencies = [ [[package]] name = "nix" -version = "0.26.1" +version = "0.26.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "46a58d1d356c6597d08cde02c2f09d785b09e28711837b1ed667dc652c08a694" +checksum = "bfdda3d196821d6af13126e40375cdf7da646a96114af134d5f417a9a1dc8e1a" dependencies = [ "bitflags", "cfg-if", @@ -1811,9 +1849,9 @@ dependencies = [ [[package]] name = "nom" -version = "7.1.2" +version = "7.1.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e5507769c4919c998e69e49c839d9dc6e693ede4cc4290d6ad8b41d4f09c548c" +checksum = "d273983c5a657a70a3e8f2a01329822f3b8c8172b73826411a55751e404a0a4a" dependencies = [ "memchr", "minimal-lexical", @@ -1866,9 +1904,9 @@ dependencies = [ [[package]] name = "object" -version = "0.30.1" +version = "0.30.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8d864c91689fdc196779b98dba0aceac6118594c2df6ee5d943eb6a8df4d107a" +checksum = "ea86265d3d3dcb6a27fc51bd29a4bf387fae9d2986b823079d4986af253eb439" dependencies = [ "memchr", ] @@ -1879,6 +1917,12 @@ version = "1.17.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b7e5500299e16ebb147ae15a00a942af264cf3688f47923b8fc2cd5858f23ad3" +[[package]] +name = "opaque-debug" +version = "0.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "624a8340c38c1b80fd549087862da4ba43e08858af025b236e509b6649fc13d5" + [[package]] name = "openssl" version = "0.10.45" @@ -1966,9 +2010,9 @@ checksum = "478c572c3d73181ff3c2539045f6eb99e5491218eae919370993b890cdbdd98e" [[package]] name = "pest" -version = "2.5.2" +version = "2.5.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0f6e86fb9e7026527a0d46bc308b841d73170ef8f443e1807f6ef88526a816d4" +checksum = "8cbd939b234e95d72bc393d51788aec68aeeb5d51e748ca08ff3aad58cb722f7" dependencies = [ "thiserror", "ucd-trie", @@ -1976,9 +2020,9 @@ dependencies = [ [[package]] name = "pest_derive" -version = "2.5.2" +version = "2.5.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "96504449aa860c8dcde14f9fba5c58dc6658688ca1fe363589d6327b8662c603" +checksum = "a81186863f3d0a27340815be8f2078dd8050b14cd71913db9fbda795e5f707d7" dependencies = [ "pest", "pest_generator", @@ -1986,9 +2030,9 @@ dependencies = [ [[package]] name = "pest_generator" -version = "2.5.2" +version = "2.5.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "798e0220d1111ae63d66cb66a5dcb3fc2d986d520b98e49e1852bfdb11d7c5e7" +checksum = "75a1ef20bf3193c15ac345acb32e26b3dc3223aff4d77ae4fc5359567683796b" dependencies = [ "pest", "pest_meta", @@ -1999,13 +2043,13 @@ dependencies = [ [[package]] name = "pest_meta" -version = "2.5.2" +version = "2.5.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "984298b75898e30a843e278a9f2452c31e349a073a0ce6fd950a12a74464e065" +checksum = "5e3b284b1f13a20dc5ebc90aff59a51b8d7137c221131b52a7260c08cbc1cc80" dependencies = [ "once_cell", "pest", - "sha1", + "sha2", ] [[package]] @@ -2101,16 +2145,16 @@ dependencies = [ [[package]] name = "proc-macro2" -version = "1.0.49" +version = "1.0.51" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "57a8eca9f9c4ffde41714334dee777596264c7825420f521abc92b5b5deb63a5" +checksum = "5d727cae5b39d21da60fa540906919ad737832fe0b1c165da3a34d6548c849d6" dependencies = [ "unicode-ident", ] [[package]] name = "prusti" -version = "0.2.1" +version = "0.3.0" dependencies = [ "chrono", "env_logger", @@ -2120,6 +2164,8 @@ dependencies = [ "prusti-interface", "prusti-rustc-interface", "prusti-viper", + "serde", + "serde_json", "tracing 0.1.0", "tracing-chrome", "tracing-subscriber", @@ -2178,7 +2224,7 @@ version = "0.1.0" dependencies = [ "ctrlc", "glob", - "nix 0.26.1", + "nix 0.26.2", "prusti-utils", ] @@ -2190,9 +2236,13 @@ version = "0.1.0" name = "prusti-server" version = "0.1.0" dependencies = [ + "async-stream", "bincode", "clap", "env_logger", + "futures", + "futures-util", + "jni", "lazy_static", "log", "num_cpus", @@ -2202,10 +2252,13 @@ dependencies = [ "reqwest", "rustc-hash", "serde", + "serde_json", "tokio", + "tokio-tungstenite 0.13.0", "tracing 0.1.0", "url", "viper", + "viper-sys", "warp", ] @@ -2253,7 +2306,7 @@ dependencies = [ "itertools", "lazy_static", "log", - "nix 0.26.1", + "nix 0.26.2", "rustc-hash", "serde", "toml", @@ -2265,9 +2318,11 @@ dependencies = [ name = "prusti-viper" version = "0.1.0" dependencies = [ + "async-stream", "backtrace", "derive_more", "diffy", + "futures-util", "itertools", "lazy_static", "log", @@ -2281,6 +2336,7 @@ dependencies = [ "rustc-hash", "serde", "serde_json", + "tokio", "tracing 0.1.0", "viper", "vir", @@ -2333,9 +2389,9 @@ dependencies = [ [[package]] name = "rayon" -version = "1.6.1" +version = "1.7.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6db3a213adf02b3bcfd2d3846bb41cb22857d131789e01df434fb7e7bc0759b7" +checksum = "1d2df5196e37bcc87abebc0053e20787d73847bb33134a69841207dd0a47f03b" dependencies = [ "either", "rayon-core", @@ -2343,9 +2399,9 @@ dependencies = [ [[package]] name = "rayon-core" -version = "1.10.2" +version = "1.11.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "356a0625f1954f730c0201cdab48611198dc6ce21f4acff55089b5a78e6e835b" +checksum = "4b8f95bd6966f5c87776639160a66bd8ab9895d9d4ab01ddba9fc60661aebe8d" dependencies = [ "crossbeam-channel", "crossbeam-deque", @@ -2375,9 +2431,9 @@ dependencies = [ [[package]] name = "regex" -version = "1.7.0" +version = "1.7.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e076559ef8e241f2ae3479e36f97bd5741c0330689e217ad51ce2c76808b868a" +checksum = "48aaa5748ba571fb95cd2c85c09f629215d3a6ece942baa100950af03a34f733" dependencies = [ "aho-corasick", "memchr", @@ -2423,11 +2479,11 @@ dependencies = [ [[package]] name = "reqwest" -version = "0.11.13" +version = "0.11.14" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "68cc60575865c7831548863cc02356512e3f1dc2f3f82cb837d7fc4cc8f3c97c" +checksum = "21eed90ec8570952d53b772ecf8f206aa1ec9a3d76b2521c56c42973f2d91ee9" dependencies = [ - "base64 0.13.1", + "base64 0.21.0", "bytes", "encoding_rs", "futures-core", @@ -2531,23 +2587,23 @@ dependencies = [ [[package]] name = "rustix" -version = "0.36.6" +version = "0.36.9" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4feacf7db682c6c329c4ede12649cd36ecab0f3be5b7d74e6a20304725db4549" +checksum = "fd5c6ff11fecd55b40746d1995a02f2eb375bf8c00d192d521ee09f42bef37bc" dependencies = [ "bitflags", "errno", "io-lifetimes", "libc", "linux-raw-sys", - "windows-sys 0.42.0", + "windows-sys 0.45.0", ] [[package]] name = "rustls" -version = "0.20.7" +version = "0.20.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "539a2bfe908f471bfa933876bd1eb6a19cf2176d375f82ef7f99530a40e48c2c" +checksum = "fff78fc74d175294f4e83b28343315ffcfb114b156f0185e9741cb5570f50e2f" dependencies = [ "log", "ring", @@ -2575,9 +2631,9 @@ dependencies = [ [[package]] name = "rustversion" -version = "1.0.11" +version = "1.0.12" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5583e89e108996506031660fe09baa5011b9dd0341b89029313006d1fb508d70" +checksum = "4f3208ce4d8448b3f3e7d168a73f5e0c43a61e32930de3bceeccedb388b6bf06" [[package]] name = "rustwide" @@ -2614,9 +2670,9 @@ dependencies = [ [[package]] name = "ryu" -version = "1.0.12" +version = "1.0.13" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7b4b9743ed687d4b4bcedf9ff5eaa7398495ae14e61cba0a295704edbc7decde" +checksum = "f91339c0467de62360649f8d3e185ca8de4224ff281f66000de5eb2a77a79041" [[package]] name = "safemem" @@ -2656,9 +2712,9 @@ checksum = "d29ab0c6d3fc0ee92fe66e2d99f700eab17a8d57d1c1d3b748380fb20baa78cd" [[package]] name = "scratch" -version = "1.0.3" +version = "1.0.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ddccb15bcce173023b3fedd9436f882a0739b8dfb45e4f6b6002bee5929f61b2" +checksum = "1792db035ce95be60c3f8853017b3999209281c24e2ba5bc8e59bf97a0c590c1" [[package]] name = "sct" @@ -2721,11 +2777,11 @@ dependencies = [ [[package]] name = "serde_json" -version = "1.0.91" +version = "1.0.94" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "877c235533714907a8c2464236f5c4b2a17262ef1bd71f38f35ea592c8da6883" +checksum = "1c533a59c9d8a93a09c6ab31f0fd5e5f4dd1b8fc9434804029839884765d04ea" dependencies = [ - "itoa 1.0.5", + "itoa", "ryu", "serde", ] @@ -2737,11 +2793,24 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d3491c14715ca2294c4d6a88f15e84739788c1d030eed8c110436aafdaa2f3fd" dependencies = [ "form_urlencoded", - "itoa 1.0.5", + "itoa", "ryu", "serde", ] +[[package]] +name = "sha-1" +version = "0.9.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "99cd6713db3cf16b6c84e06321e049a9b9f699826e16096d23bbcc44d15d51a6" +dependencies = [ + "block-buffer 0.9.0", + "cfg-if", + "cpufeatures", + "digest 0.9.0", + "opaque-debug", +] + [[package]] name = "sha-1" version = "0.10.1" @@ -2750,7 +2819,7 @@ checksum = "f5058ada175748e33390e40e872bd0fe59a19f265d0158daa551c5a88a76009c" dependencies = [ "cfg-if", "cpufeatures", - "digest", + "digest 0.10.6", ] [[package]] @@ -2761,7 +2830,18 @@ checksum = "f04293dc80c3993519f2d7f6f511707ee7094fe0c6d3406feb330cdb3540eba3" dependencies = [ "cfg-if", "cpufeatures", - "digest", + "digest 0.10.6", +] + +[[package]] +name = "sha2" +version = "0.10.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "82e6b795fe2e3b1e845bafcb27aa35405c4d47cdfc92af5fc8d3002f76cebdc0" +dependencies = [ + "cfg-if", + "cpufeatures", + "digest 0.10.6", ] [[package]] @@ -2781,9 +2861,9 @@ checksum = "45bb67a18fa91266cc7807181f62f9178a6873bfad7dc788c42e6430db40184f" [[package]] name = "signal-hook" -version = "0.3.14" +version = "0.3.15" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a253b5e89e2698464fc26b545c9edceb338e18a89effeeecfea192c3025be29d" +checksum = "732768f1176d21d09e076c23a93123d40bba92d50c4058da34d45c8de8e682b9" dependencies = [ "libc", "signal-hook-registry", @@ -2791,9 +2871,9 @@ dependencies = [ [[package]] name = "signal-hook-registry" -version = "1.4.0" +version = "1.4.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e51e73328dc4ac0c7ccbda3a494dfa03df1de2f46018127f60c693f2648455b0" +checksum = "d8229b473baa5980ac72ef434c4415e70c4b5e71b423043adb4ba059f89c99a1" dependencies = [ "libc", ] @@ -2806,9 +2886,9 @@ checksum = "420acb44afdae038210c99e69aae24109f32f15500aa708e81d46c9f29d55fcf" [[package]] name = "slab" -version = "0.4.7" +version = "0.4.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4614a76b2a8be0058caa9dbbaf66d988527d86d003c11a94fbd335d7661edcef" +checksum = "6528351c9bc8ab22353f9d776db39a20288e8d6c37ef8cfe3317cf875eecfc2d" dependencies = [ "autocfg", ] @@ -2853,9 +2933,9 @@ checksum = "c01dea7e04cbb27ef4c86e9922184608185f7cd95c1763bc30d727cda4a5e930" [[package]] name = "socket2" -version = "0.4.7" +version = "0.4.9" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "02e2d2db9033d13a1567121ddd7a095ee144db4e1ca1b1bda3419bc0da294ebd" +checksum = "64a4a911eed85daf18834cfaa86a79b7d266ff93ff5ba14005426219480ed662" dependencies = [ "libc", "winapi", @@ -2881,9 +2961,9 @@ checksum = "73473c0e59e6d5812c5dfe2a064a6444949f089e20eec9a2e5506596494e4623" [[package]] name = "syn" -version = "1.0.107" +version = "1.0.109" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1f4064b5b16e03ae50984a5a8ed5d4f8803e6bc1fd170a3cda91a1be4b18e3f5" +checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237" dependencies = [ "proc-macro2", "quote", @@ -2928,16 +3008,15 @@ dependencies = [ [[package]] name = "tempfile" -version = "3.3.0" +version = "3.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5cdb1ef4eaeeaddc8fbd371e5017057064af0911902ef36b39801f67cc6d79e4" +checksum = "af18f7ae1acd354b992402e9ec5864359d693cd8a79dcbef59f76891701c1e95" dependencies = [ "cfg-if", "fastrand", - "libc", "redox_syscall", - "remove_dir_all 0.5.3", - "winapi", + "rustix", + "windows-sys 0.42.0", ] [[package]] @@ -2953,9 +3032,9 @@ dependencies = [ [[package]] name = "termcolor" -version = "1.1.3" +version = "1.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bab24d30b911b2376f3a13cc2cd443142f0c81dda04c118693e35b3835757755" +checksum = "be55cf8942feac5c765c2c993422806843c9a9a45d4d5c407ad6dd2ea95eb9b6" dependencies = [ "winapi-util", ] @@ -2993,18 +3072,18 @@ dependencies = [ [[package]] name = "thiserror" -version = "1.0.38" +version = "1.0.39" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6a9cd18aa97d5c45c6603caea1da6628790b37f7a34b6ca89522331c5180fed0" +checksum = "a5ab016db510546d856297882807df8da66a16fb8c4101cb8b30054b0d5b2d9c" dependencies = [ "thiserror-impl", ] [[package]] name = "thiserror-impl" -version = "1.0.38" +version = "1.0.39" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1fb327af4685e4d03fa8cbcf1716380da910eeb2bb8be417e7f9fd3fb164f36f" +checksum = "5420d42e90af0c38c3290abcca25b9b3bdf379fc9f55c528f53a269d9c9a267e" dependencies = [ "proc-macro2", "quote", @@ -3032,15 +3111,15 @@ dependencies = [ [[package]] name = "tinyvec_macros" -version = "0.1.0" +version = "0.1.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "cda74da7e1a664f795bb1f8a87ec406fb89a02522cf6e50620d016add6dbbf5c" +checksum = "1f3ccbac311fea05f86f61904b462b55fb3df8837a366dfc601a0161d0532f20" [[package]] name = "tokio" -version = "1.23.0" +version = "1.26.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "eab6d665857cc6ca78d6e80303a02cea7a7851e85dfbd77cbdc09bd129f1ef46" +checksum = "03201d01c3c27a29c8a5cee5b55a93ddae1ccf6f08f65365c2c918f8c1b76f64" dependencies = [ "autocfg", "bytes", @@ -3051,7 +3130,7 @@ dependencies = [ "pin-project-lite", "signal-hook-registry", "socket2", - "windows-sys 0.42.0", + "windows-sys 0.45.0", ] [[package]] @@ -3067,15 +3146,28 @@ dependencies = [ [[package]] name = "tokio-stream" -version = "0.1.11" +version = "0.1.12" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d660770404473ccd7bc9f8b28494a811bc18542b915c0855c51e8f419d5223ce" +checksum = "8fb52b74f05dbf495a8fba459fdc331812b96aa086d9eb78101fa0d4569c3313" dependencies = [ "futures-core", "pin-project-lite", "tokio", ] +[[package]] +name = "tokio-tungstenite" +version = "0.13.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e1a5f475f1b9d077ea1017ecbc60890fda8e54942d680ca0b1d2b47cfa2d861b" +dependencies = [ + "futures-util", + "log", + "pin-project", + "tokio", + "tungstenite 0.12.0", +] + [[package]] name = "tokio-tungstenite" version = "0.17.2" @@ -3085,14 +3177,14 @@ dependencies = [ "futures-util", "log", "tokio", - "tungstenite", + "tungstenite 0.17.3", ] [[package]] name = "tokio-util" -version = "0.7.4" +version = "0.7.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0bb2e075f03b3d66d8d8785356224ba688d2906a371015e225beeb65ca92c740" +checksum = "5427d89453009325de0d8f342c9490009f76e999cb7672d77e46267448f7e6b2" dependencies = [ "bytes", "futures-core", @@ -3104,9 +3196,9 @@ dependencies = [ [[package]] name = "toml" -version = "0.5.10" +version = "0.5.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1333c76748e868a4d9d1017b5ab53171dfd095f70c712fdb4653a406547f598f" +checksum = "f4f7f0dd8d50a853a531c426359045b1998f04219d88799810762cd4ad314234" dependencies = [ "serde", ] @@ -3164,12 +3256,11 @@ dependencies = [ [[package]] name = "tracing-chrome" -version = "0.7.0" +version = "0.7.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "865016457701971958e047b9f61add5bba70d7a7b084a13c9e54f9bb4f19d3a6" +checksum = "496b3cd5447f7ff527bbbf19b071ad542a000adf297d4127078b4dfdb931f41a" dependencies = [ - "crossbeam-channel", - "json", + "serde_json", "tracing-core", "tracing-subscriber", ] @@ -3215,9 +3306,28 @@ dependencies = [ [[package]] name = "try-lock" -version = "0.2.3" +version = "0.2.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "59547bce71d9c38b83d9c0e92b6066c4253371f15005def0c30d9657f50c7642" +checksum = "3528ecfd12c466c6f163363caf2d02a71161dd5e1cc6ae7b34207ea2d42d81ed" + +[[package]] +name = "tungstenite" +version = "0.12.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8ada8297e8d70872fa9a551d93250a9f407beb9f37ef86494eb20012a2ff7c24" +dependencies = [ + "base64 0.13.1", + "byteorder", + "bytes", + "http", + "httparse", + "input_buffer", + "log", + "rand", + "sha-1 0.9.8", + "url", + "utf-8", +] [[package]] name = "tungstenite" @@ -3232,7 +3342,7 @@ dependencies = [ "httparse", "log", "rand", - "sha-1", + "sha-1 0.10.1", "thiserror", "url", "utf-8", @@ -3270,15 +3380,15 @@ dependencies = [ [[package]] name = "unicode-bidi" -version = "0.3.8" +version = "0.3.10" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "099b7128301d285f79ddd55b9a83d5e6b9e97c92e0ea0daebee7263e932de992" +checksum = "d54675592c1dbefd78cbd98db9bacd89886e1ca50692a0692baefffdeb92dd58" [[package]] name = "unicode-ident" -version = "1.0.6" +version = "1.0.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "84a22b9f218b40614adcb3f4ff08b703773ad44fa9423e4e0d346d5db86e4ebc" +checksum = "e5464a87b239f13a63a501f2701565754bae92d243d4bb7eb12f6d57d2269bf4" [[package]] name = "unicode-normalization" @@ -3309,9 +3419,9 @@ checksum = "a156c684c91ea7d62626509bce3cb4e1d9ed5c4d978f7b4352658f96a4c26b4a" [[package]] name = "ureq" -version = "2.6.1" +version = "2.6.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "733b5ad78377302af52c0dbcb2623d78fe50e4b3bf215948ff29e9ee031d8566" +checksum = "338b31dd1314f68f3aabf3ed57ab922df95ffcd902476ca7ba3c4ce7b908c46d" dependencies = [ "base64 0.13.1", "flate2", @@ -3342,9 +3452,9 @@ checksum = "09cc8ee72d2a9becf2f2febe0205bbed8fc6615b7cb429ad062dc7b7ddd036a9" [[package]] name = "uuid" -version = "1.2.2" +version = "1.3.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "422ee0de9031b5b948b97a8fc04e3aa35230001a722ddd27943e0be31564ce4c" +checksum = "1674845326ee10d37ca60470760d4288a6f80f304007d92e5c53bab78c9cfd79" dependencies = [ "getrandom", "serde", @@ -3505,7 +3615,7 @@ dependencies = [ "serde_urlencoded", "tokio", "tokio-stream", - "tokio-tungstenite", + "tokio-tungstenite 0.17.2", "tokio-util", "tower-service", "tracing 0.1.37", @@ -3519,9 +3629,9 @@ checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423" [[package]] name = "wasm-bindgen" -version = "0.2.83" +version = "0.2.84" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "eaf9f5aceeec8be17c128b2e93e031fb8a4d469bb9c4ae2d7dc1888b26887268" +checksum = "31f8dcbc21f30d9b8f2ea926ecb58f6b91192c17e9d33594b3df58b2007ca53b" dependencies = [ "cfg-if", "wasm-bindgen-macro", @@ -3529,9 +3639,9 @@ dependencies = [ [[package]] name = "wasm-bindgen-backend" -version = "0.2.83" +version = "0.2.84" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4c8ffb332579b0557b52d268b91feab8df3615f265d5270fec2a8c95b17c1142" +checksum = "95ce90fd5bcc06af55a641a86428ee4229e44e07033963a2290a8e241607ccb9" dependencies = [ "bumpalo", "log", @@ -3544,9 +3654,9 @@ dependencies = [ [[package]] name = "wasm-bindgen-futures" -version = "0.4.33" +version = "0.4.34" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "23639446165ca5a5de86ae1d8896b737ae80319560fbaa4c2887b7da6e7ebd7d" +checksum = "f219e0d211ba40266969f6dbdd90636da12f75bee4fc9d6c23d1260dadb51454" dependencies = [ "cfg-if", "js-sys", @@ -3556,9 +3666,9 @@ dependencies = [ [[package]] name = "wasm-bindgen-macro" -version = "0.2.83" +version = "0.2.84" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "052be0f94026e6cbc75cdefc9bae13fd6052cdcaf532fa6c45e7ae33a1e6c810" +checksum = "4c21f77c0bedc37fd5dc21f897894a5ca01e7bb159884559461862ae90c0b4c5" dependencies = [ "quote", "wasm-bindgen-macro-support", @@ -3566,9 +3676,9 @@ dependencies = [ [[package]] name = "wasm-bindgen-macro-support" -version = "0.2.83" +version = "0.2.84" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "07bc0c051dc5f23e307b13285f9d75df86bfdf816c5721e573dec1f9b8aa193c" +checksum = "2aff81306fcac3c7515ad4e177f521b5c9a15f2b08f4e32d823066102f35a5f6" dependencies = [ "proc-macro2", "quote", @@ -3579,15 +3689,15 @@ dependencies = [ [[package]] name = "wasm-bindgen-shared" -version = "0.2.83" +version = "0.2.84" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1c38c045535d93ec4f0b4defec448e4291638ee608530863b1e2ba115d4fff7f" +checksum = "0046fef7e28c3804e5e38bfa31ea2a0f73905319b677e57ebe37e49358989b5d" [[package]] name = "web-sys" -version = "0.3.60" +version = "0.3.61" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bcda906d8be16e728fd5adc5b729afad4e444e106ab28cd1c7256e54fa61510f" +checksum = "e33b99f4b23ba3eec1a53ac264e35a755f00e966e0065077d6027c0f575b0b97" dependencies = [ "js-sys", "wasm-bindgen", @@ -3678,19 +3788,43 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "5a3e1820f08b8513f676f7ab6c1f99ff312fb97b553d30ff4dd86f9f15728aa7" dependencies = [ "windows_aarch64_gnullvm", - "windows_aarch64_msvc 0.42.0", - "windows_i686_gnu 0.42.0", - "windows_i686_msvc 0.42.0", - "windows_x86_64_gnu 0.42.0", + "windows_aarch64_msvc 0.42.1", + "windows_i686_gnu 0.42.1", + "windows_i686_msvc 0.42.1", + "windows_x86_64_gnu 0.42.1", + "windows_x86_64_gnullvm", + "windows_x86_64_msvc 0.42.1", +] + +[[package]] +name = "windows-sys" +version = "0.45.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "75283be5efb2831d37ea142365f009c02ec203cd29a3ebecbc093d52315b66d0" +dependencies = [ + "windows-targets", +] + +[[package]] +name = "windows-targets" +version = "0.42.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8e2522491fbfcd58cc84d47aeb2958948c4b8982e9a2d8a2a35bbaed431390e7" +dependencies = [ + "windows_aarch64_gnullvm", + "windows_aarch64_msvc 0.42.1", + "windows_i686_gnu 0.42.1", + "windows_i686_msvc 0.42.1", + "windows_x86_64_gnu 0.42.1", "windows_x86_64_gnullvm", - "windows_x86_64_msvc 0.42.0", + "windows_x86_64_msvc 0.42.1", ] [[package]] name = "windows_aarch64_gnullvm" -version = "0.42.0" +version = "0.42.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "41d2aa71f6f0cbe00ae5167d90ef3cfe66527d6f613ca78ac8024c3ccab9a19e" +checksum = "8c9864e83243fdec7fc9c5444389dcbbfd258f745e7853198f365e3c4968a608" [[package]] name = "windows_aarch64_msvc" @@ -3700,9 +3834,9 @@ checksum = "9bb8c3fd39ade2d67e9874ac4f3db21f0d710bee00fe7cab16949ec184eeaa47" [[package]] name = "windows_aarch64_msvc" -version = "0.42.0" +version = "0.42.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "dd0f252f5a35cac83d6311b2e795981f5ee6e67eb1f9a7f64eb4500fbc4dcdb4" +checksum = "4c8b1b673ffc16c47a9ff48570a9d85e25d265735c503681332589af6253c6c7" [[package]] name = "windows_i686_gnu" @@ -3712,9 +3846,9 @@ checksum = "180e6ccf01daf4c426b846dfc66db1fc518f074baa793aa7d9b9aaeffad6a3b6" [[package]] name = "windows_i686_gnu" -version = "0.42.0" +version = "0.42.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fbeae19f6716841636c28d695375df17562ca208b2b7d0dc47635a50ae6c5de7" +checksum = "de3887528ad530ba7bdbb1faa8275ec7a1155a45ffa57c37993960277145d640" [[package]] name = "windows_i686_msvc" @@ -3724,9 +3858,9 @@ checksum = "e2e7917148b2812d1eeafaeb22a97e4813dfa60a3f8f78ebe204bcc88f12f024" [[package]] name = "windows_i686_msvc" -version = "0.42.0" +version = "0.42.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "84c12f65daa39dd2babe6e442988fc329d6243fdce47d7d2d155b8d874862246" +checksum = "bf4d1122317eddd6ff351aa852118a2418ad4214e6613a50e0191f7004372605" [[package]] name = "windows_x86_64_gnu" @@ -3736,15 +3870,15 @@ checksum = "4dcd171b8776c41b97521e5da127a2d86ad280114807d0b2ab1e462bc764d9e1" [[package]] name = "windows_x86_64_gnu" -version = "0.42.0" +version = "0.42.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bf7b1b21b5362cbc318f686150e5bcea75ecedc74dd157d874d754a2ca44b0ed" +checksum = "c1040f221285e17ebccbc2591ffdc2d44ee1f9186324dd3e84e99ac68d699c45" [[package]] name = "windows_x86_64_gnullvm" -version = "0.42.0" +version = "0.42.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "09d525d2ba30eeb3297665bd434a54297e4170c7f1a44cad4ef58095b4cd2028" +checksum = "628bfdf232daa22b0d64fdb62b09fcc36bb01f05a3939e20ab73aaf9470d0463" [[package]] name = "windows_x86_64_msvc" @@ -3754,9 +3888,9 @@ checksum = "c811ca4a8c853ef420abd8592ba53ddbbac90410fab6903b3e79972a631f7680" [[package]] name = "windows_x86_64_msvc" -version = "0.42.0" +version = "0.42.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f40009d85759725a34da6d89a94e63d7bdc50a862acf0dbc7c8e488f1edcb6f5" +checksum = "447660ad36a13288b1db4d4248e857b510e8c3a225c822ba4fb748c0aafecffd" [[package]] name = "winreg" diff --git a/docs/dev-guide/src/config/flags.md b/docs/dev-guide/src/config/flags.md index b3ef1913dc9..b42bb4e2249 100644 --- a/docs/dev-guide/src/config/flags.md +++ b/docs/dev-guide/src/config/flags.md @@ -55,18 +55,25 @@ | [`PRINT_DESUGARED_SPECS`](#print_desugared_specs) | `bool` | `false` | A | | [`PRINT_HASH`](#print_hash) | `bool` | `false` | A | | [`PRINT_TYPECKD_SPECS`](#print_typeckd_specs) | `bool` | `false` | A | +| [`QUERY_METHOD_SIGNATURE`](#query_method_signature) | `Option` | `None` | A | | [`QUIET`](#quiet) | `bool` | `false` | A* | +| [`REPORT_VIPER_MESSAGES`](#report_viper_messages) | `bool` | `false` | A | +| [`VERIFY_ONLY_DEFPATH`](#verify_only_defpath) | `Option` | `None` | A | | [`SERVER_ADDRESS`](#server_address) | `Option` | `None` | A | | [`SERVER_MAX_CONCURRENCY`](#server_max_concurrency) | `Option` | `None` | A | | [`SERVER_MAX_STORED_VERIFIERS`](#server_max_stored_verifiers) | `Option` | `None` | A | +| [`SHOW_IDE_INFO`](#show_ide_info) | `bool` | `false` | A | | [`SIMPLIFY_ENCODING`](#simplify_encoding) | `bool` | `true` | A | | [`SKIP_UNSUPPORTED_FEATURES`](#skip_unsupported_features) | `bool` | `false` | A | +| [`SKIP_VERIFICATION`](#skip_verification) | `bool` | `false` | A | | [`SMT_QI_BOUND_GLOBAL`](#smt_qi_bound_global) | `Option` | `None` | A | -[`SMT_QI_BOUND_GLOBAL_KIND`](#smt_qi_bound_global_kind) | `Option` | `None` | A | +| [`SMT_QI_BOUND_GLOBAL_KIND`](#smt_qi_bound_global_kind) | `Option` | `None` | A | | [`SMT_QI_BOUND_TRACE`](#smt_qi_bound_trace) | `Option` | `None` | A | | [`SMT_QI_BOUND_TRACE_KIND`](#smt_qi_bound_trace_kind) | `Option` | `None` | A | -| [`SMT_QI_IGNORE_BUILTIN`](#smt_qi_ignore_builtin) | `bool` | `true` | A | | [`SMT_QI_EAGER_THRESHOLD`](#smt_qi_eager_threshold) | `u64` | `1000` | A | +| [`SMT_QI_IGNORE_BUILTIN`](#smt_qi_ignore_builtin) | `bool` | `true` | A | +| [`SMT_QI_PROFILE`](#smt_qi_profile) | `Option` | `None` | A | +| [`SMT_QI_PROFILE_FREQ`](#smt_qi_profile_freq) | `Option` | `None` | A | | [`SMT_SOLVER_PATH`](#smt_solver_path) | `Option` | `env::var("Z3_EXE")` | A | | [`SMT_SOLVER_WRAPPER_PATH`](#smt_solver_wrapper_path) | `Option` | `None` | A | | [`SMT_UNIQUE_TRIGGERS_BOUND`](#smt_unique_triggers_bound) | `Option` | `None` | A | @@ -351,12 +358,24 @@ When enabled, prints the hash of a verification request (the hash is used for ca When enabled, prints the type-checked specifications. +## `QUERY_METHOD_SIGNATURE` + +When set to a defpath, prusti will generate a template for an external specification for this method. The result is part of the CompilerInfo and will only be emitted if the `SHOW_IDE_INFO` flag is enabled too. + ## `QUIET` When enabled, user messages are not printed. Otherwise, messages output into `stderr`. > **Note:** `cargo prusti` sets this flag with `DEFAULT_PRUSTI_QUIET=true`. +## `REPORT_VIPER_MESSAGES` + +When enabled for both server and client, certain supported Viper messages will be reported to the user. + +## `VERIFY_ONLY_DEFPATH` + +When set to the defpath of a local method, prusti will only verify the specified method. A fake error will be generated to avoid caching of a success. + ## `SERVER_ADDRESS` When set to an address and port (e.g. `"127.0.0.1:2468"`), Prusti will connect to the given server and use it for its verification backend. @@ -373,6 +392,10 @@ Maximum amount of instantiated Viper verifiers the server will keep around for r > **Note:** This does _not_ limit how many verification requests the server handles concurrently, only the size of what is essentially its verifier cache. +## `SHOW_IDE_INFO` + +When enabled, we emit various json data structures containing information about the program, its encoding, and the results of the verification. This flag intended for prusti-assistant (IDE). + ## `SIMPLIFY_ENCODING` When enabled, the encoded program is simplified before it is passed to the Viper backend. @@ -381,6 +404,10 @@ When enabled, the encoded program is simplified before it is passed to the Viper When enabled, features not supported by Prusti will be reported as warnings rather than errors. +## `SKIP_VERIFICATION` + +When enabled, verification will be skipped. Opposed to `NO_VERIFY`, this flag will cause fake errors to stop the compiler from caching the result. + ## `SMT_QI_BOUND_GLOBAL` If not `None`, checks that the number of global quantifier instantiations reported by the SMT wrapper is smaller than the specified bound. @@ -408,6 +435,13 @@ If not `None`, checks that the number of quantifier instantiations in each trace ## `SMT_QI_IGNORE_BUILTIN` When enabled, ignores the built-in quantifiers in SMT quantifier instantiation bounds checking. +## `SMT_QI_PROFILE` + +When enabled, the Z3 backend periodically (and on finish) reports the number of quantifier instantiations to Viper. + +## `SMT_QI_PROFILE_FREQ` + +Frequency of the quantifier instantiation reporting of Z3 (every X instantiations, a report is issued). ## `SMT_QI_EAGER_THRESHOLD` diff --git a/prusti-common/src/vir/program_normalization.rs b/prusti-common/src/vir/program_normalization.rs index 5420e9c3635..306cd12c04e 100644 --- a/prusti-common/src/vir/program_normalization.rs +++ b/prusti-common/src/vir/program_normalization.rs @@ -7,8 +7,9 @@ use crate::vir::{program::Program, Position}; use log::{debug, trace}; use rustc_hash::{FxHashMap, FxHashSet}; -use viper::VerificationResult; +use viper::VerificationResultKind; +#[derive(Clone)] pub enum NormalizationInfo { LegacyProgram { original_position_ids: Vec }, LowProgram, @@ -103,8 +104,8 @@ impl NormalizationInfo { } /// Denormalize a verification result. - pub fn denormalize_result(&self, result: &mut VerificationResult) { - if let VerificationResult::Failure(ref mut ver_errors) = result { + pub fn denormalize_result(&self, result: &mut VerificationResultKind) { + if let VerificationResultKind::Failure(ref mut ver_errors) = result { ver_errors.iter_mut().for_each(|ver_error| { if let Some(pos) = ver_error.pos_id.as_mut() { self.denormalize_position_string(pos); diff --git a/prusti-interface/src/environment/diagnostic.rs b/prusti-interface/src/environment/diagnostic.rs index e3e84075f9a..2dae0d01a75 100644 --- a/prusti-interface/src/environment/diagnostic.rs +++ b/prusti-interface/src/environment/diagnostic.rs @@ -78,6 +78,11 @@ impl<'tcx> EnvDiagnostic<'tcx> { diagnostic.buffer(&mut self.warn_buffer.borrow_mut()); } + /// Emits a note + pub fn span_note + Clone>(&self, sp: S, msg: &str) { + self.tcx.sess.span_note_without_error(sp, msg); + } + /// Returns true if an error has been emitted pub fn has_errors(&self) -> bool { self.tcx.sess.has_errors().is_some() diff --git a/prusti-interface/src/prusti_error.rs b/prusti-interface/src/prusti_error.rs index bb0cc96f96c..e69c2e8c8a7 100644 --- a/prusti-interface/src/prusti_error.rs +++ b/prusti-interface/src/prusti_error.rs @@ -20,7 +20,7 @@ use prusti_rustc_interface::{errors::MultiSpan, span::Span}; /// `SpannedEncodingError` and similar types to something less confusing.) #[derive(Clone, Debug, PartialEq, Eq)] pub struct PrustiError { - kind: PrustiErrorKind, + kind: PrustiDiagnosticKind, /// If `true`, it should not be reported to the user. We need this in cases /// when the same error could be reported twice. /// @@ -35,11 +35,12 @@ pub struct PrustiError { } /// Determines how a `PrustiError` is reported. #[derive(Clone, Debug, PartialEq, Eq)] -pub enum PrustiErrorKind { +pub enum PrustiDiagnosticKind { Error, Warning, /// A warning which is only shown if at least one error is emitted. WarningOnError, + Message, } impl PartialOrd for PrustiError { @@ -60,7 +61,7 @@ impl PrustiError { /// Private constructor. Use one of the following methods. fn new(message: String, span: MultiSpan) -> Self { PrustiError { - kind: PrustiErrorKind::Error, + kind: PrustiDiagnosticKind::Error, is_disabled: false, message, span: Box::new(span), @@ -114,7 +115,7 @@ impl PrustiError { pub fn warning(message: S, span: MultiSpan) -> Self { check_message(message.to_string()); let mut err = PrustiError::new(format!("[Prusti: warning] {}", message.to_string()), span); - err.kind = PrustiErrorKind::Warning; + err.kind = PrustiDiagnosticKind::Warning; err } @@ -123,7 +124,7 @@ impl PrustiError { pub fn warning_on_error(message: S, span: MultiSpan) -> Self { check_message(message.to_string()); let mut err = PrustiError::new(format!("[Prusti: warning] {}", message.to_string()), span); - err.kind = PrustiErrorKind::WarningOnError; + err.kind = PrustiDiagnosticKind::WarningOnError; err } @@ -146,13 +147,21 @@ impl PrustiError { error } + /// Report a message + pub fn message(message: S, span: MultiSpan) -> Self { + check_message(message.to_string()); + let mut msg = PrustiError::new(message.to_string(), span); + msg.kind = PrustiDiagnosticKind::Message; + msg + } + /// Set that this Prusti error should be reported as a warning to the user pub fn set_warning(&mut self) { - self.kind = PrustiErrorKind::Warning; + self.kind = PrustiDiagnosticKind::Warning; } pub fn is_error(&self) -> bool { - matches!(self.kind, PrustiErrorKind::Error) + matches!(self.kind, PrustiDiagnosticKind::Error) } // FIXME: This flag is a temporary workaround for having duplicate errors @@ -185,24 +194,26 @@ impl PrustiError { pub fn emit(self, env_diagnostic: &EnvDiagnostic) { assert!(!self.is_disabled); match self.kind { - PrustiErrorKind::Error => env_diagnostic.span_err_with_help_and_notes( - *self.span, - &self.message, - &self.help, - &self.notes, - ), - PrustiErrorKind::Warning => env_diagnostic.span_warn_with_help_and_notes( + PrustiDiagnosticKind::Error => env_diagnostic.span_err_with_help_and_notes( *self.span, &self.message, &self.help, &self.notes, ), - PrustiErrorKind::WarningOnError => env_diagnostic.span_warn_on_err_with_help_and_notes( + PrustiDiagnosticKind::Warning => env_diagnostic.span_warn_with_help_and_notes( *self.span, &self.message, &self.help, &self.notes, ), + PrustiDiagnosticKind::WarningOnError => env_diagnostic + .span_warn_on_err_with_help_and_notes( + *self.span, + &self.message, + &self.help, + &self.notes, + ), + PrustiDiagnosticKind::Message => env_diagnostic.span_note(*self.span, &self.message), }; } diff --git a/prusti-server/Cargo.toml b/prusti-server/Cargo.toml index 6fb906a0a10..6499cc0c6f4 100644 --- a/prusti-server/Cargo.toml +++ b/prusti-server/Cargo.toml @@ -19,6 +19,7 @@ doctest = false [dependencies] log = { version = "0.4", features = ["release_max_level_info"] } viper = { path = "../viper" } +viper-sys = { path = "../viper-sys" } prusti-common = { path = "../prusti-common" } prusti-utils = { path = "../prusti-utils" } tracing = { path = "../tracing" } @@ -28,11 +29,18 @@ bincode = "1.0" url = "2.2.2" num_cpus = "1.14" serde = { version = "1.0", features = ["derive"] } +serde_json = { version = "1.0" } +tokio = "1.20" +jni = { version = "0.20", features = ["invocation"] } +# the tungstenite version used by warp 0.3 +tokio-tungstenite = "0.13" +futures = "0.3.25" +futures-util = "0.3.25" +async-stream = "0.3.3" +once_cell = "1.17.0" reqwest = { version = "0.11", default-features = false, features = ["json", "rustls-tls"] } warp = "0.3" -tokio = "1.20" rustc-hash = "1.1.0" -once_cell = "1.17.1" [dev-dependencies] lazy_static = "1.4.0" diff --git a/prusti-server/src/backend.rs b/prusti-server/src/backend.rs index 5a36ad6c399..43d021ca732 100644 --- a/prusti-server/src/backend.rs +++ b/prusti-server/src/backend.rs @@ -1,19 +1,33 @@ -use crate::dump_viper_program; +use crate::{dump_viper_program, ServerMessage}; +use log::{debug, info}; use prusti_common::{ config, vir::{LoweringContext, ToViper}, Stopwatch, }; -use viper::{VerificationContext, VerificationResult}; +use std::{ + sync::{mpsc, Arc}, + thread, time, +}; +use viper::{jni_utils::JniUtils, VerificationContext, VerificationResultKind, Viper}; +use viper_sys::wrappers::{java, viper::*}; pub enum Backend<'a> { - Viper(viper::Verifier<'a>, &'a VerificationContext<'a>), + Viper( + viper::Verifier<'a>, + &'a VerificationContext<'a>, + &'a Arc, + ), } impl<'a> Backend<'a> { - pub fn verify(&mut self, program: &prusti_common::vir::program::Program) -> VerificationResult { + pub fn verify( + &mut self, + program: &prusti_common::vir::program::Program, + sender: mpsc::Sender, + ) -> VerificationResultKind { match self { - Backend::Viper(viper, context) => { + Backend::Viper(ref mut verifier, context, viper_arc) => { let mut stopwatch = Stopwatch::start("prusti-server backend", "construction of JVM objects"); @@ -33,9 +47,131 @@ impl<'a> Backend<'a> { } stopwatch.start_next("viper verification"); - viper.verify(viper_program) + if config::report_viper_messages() { + verify_and_poll_msgs(verifier, context, viper_arc, viper_program, sender) + } else { + verifier.verify(viper_program) + } }) } } } } + +fn verify_and_poll_msgs( + verifier: &mut viper::Verifier, + verification_context: &viper::VerificationContext, + viper_arc: &Arc, + viper_program: viper::Program, + sender: mpsc::Sender, +) -> VerificationResultKind { + let mut kind = VerificationResultKind::Success; + + // get the reporter global reference outside of the thread scope because it needs to + // be dropped by thread attached to the jvm. This is also why we pass it as reference + // and not per value + let env = &verification_context.env(); + let jni = JniUtils::new(env); + let verifier_wrapper = silver::verifier::Verifier::with(env); + let reporter = jni.unwrap_result(verifier_wrapper.call_reporter(*verifier.verifier_instance())); + let rep_glob_ref = env.new_global_ref(reporter).unwrap(); + + debug!("Starting viper message polling thread"); + + // start thread for polling messages + thread::scope(|scope| { + let polling_thread = scope.spawn(|| polling_function(viper_arc, &rep_glob_ref, sender)); + kind = verifier.verify(viper_program); + polling_thread.join().unwrap(); + }); + debug!("Viper message polling thread terminated"); + kind +} + +fn polling_function( + viper_arc: &Arc, + rep_glob_ref: &jni::objects::GlobalRef, + sender: mpsc::Sender, +) { + let verification_context = viper_arc.attach_current_thread(); + let env = verification_context.env(); + let jni = JniUtils::new(env); + let reporter_instance = rep_glob_ref.as_obj(); + let reporter_wrapper = silver::reporter::PollingReporter::with(env); + loop { + while reporter_wrapper + .call_hasNewMessage(reporter_instance) + .unwrap() + { + let msg = reporter_wrapper + .call_getNewMessage(reporter_instance) + .unwrap(); + debug!("Polling thread received {}", jni.class_name(msg).as_str()); + match jni.class_name(msg).as_str() { + "viper.silver.reporter.QuantifierInstantiationsMessage" => { + let msg_wrapper = silver::reporter::QuantifierInstantiationsMessage::with(env); + let q_name = + jni.get_string(jni.unwrap_result(msg_wrapper.call_quantifier(msg))); + let q_inst = jni.unwrap_result(msg_wrapper.call_instantiations(msg)); + debug!("QuantifierInstantiationsMessage: {} {}", q_name, q_inst); + // also matches the "-aux" and "_precondition" quantifiers generated + // we encoded the position id in the line and column number since this is not used by + // prusti either way + if q_name.starts_with("prog.l") { + let no_pref = q_name.strip_prefix("prog.l").unwrap(); + let stripped = no_pref + .strip_suffix("-aux") + .or(no_pref.strip_suffix("_precondition")) + .unwrap_or(no_pref); + let parsed = stripped.parse::(); + match parsed { + Ok(pos_id) => { + sender + .send(ServerMessage::QuantifierInstantiation { + q_name, + insts: u64::try_from(q_inst).unwrap(), + pos_id, + }) + .unwrap(); + } + _ => info!("Unexpected quantifier name {}", q_name), + } + } + } + "viper.silver.reporter.QuantifierChosenTriggersMessage" => { + let obj_wrapper = java::lang::Object::with(env); + let positioned_wrapper = silver::ast::Positioned::with(env); + let msg_wrapper = silver::reporter::QuantifierChosenTriggersMessage::with(env); + + let viper_quant = jni.unwrap_result(msg_wrapper.call_quantifier(msg)); + let viper_quant_str = + jni.get_string(jni.unwrap_result(obj_wrapper.call_toString(viper_quant))); + // we encoded the position id in the line and column number since this is not used by + // prusti either way + let pos = jni.unwrap_result(positioned_wrapper.call_pos(viper_quant)); + let pos_string = + jni.get_string(jni.unwrap_result(obj_wrapper.call_toString(pos))); + let pos_id_index = pos_string.rfind('.').unwrap(); + let pos_id = pos_string[pos_id_index + 1..].parse::().unwrap(); + + let viper_triggers = + jni.get_string(jni.unwrap_result(msg_wrapper.call_triggers__string(msg))); + debug!( + "QuantifierChosenTriggersMessage: {} {} {}", + viper_quant_str, viper_triggers, pos_id + ); + sender + .send(ServerMessage::QuantifierChosenTriggers { + viper_quant: viper_quant_str, + triggers: viper_triggers, + pos_id, + }) + .unwrap(); + } + "viper.silver.reporter.VerificationTerminationMessage" => return, + _ => (), + } + } + thread::sleep(time::Duration::from_millis(10)); + } +} diff --git a/prusti-server/src/client.rs b/prusti-server/src/client.rs index d1b53ea63bf..33ec57aa105 100644 --- a/prusti-server/src/client.rs +++ b/prusti-server/src/client.rs @@ -4,58 +4,76 @@ // License, v. 2.0. If a copy of the MPL was not distributed with this // file, You can obtain one at http://mozilla.org/MPL/2.0/. -use crate::VerificationRequest; +use crate::{ServerMessage, VerificationRequest}; +use futures_util::{ + sink::SinkExt, + stream::{Stream, StreamExt}, +}; use prusti_common::config; -use reqwest::Client; -use url::{ParseError, Url}; -use viper::VerificationResult; +use tokio_tungstenite::{ + connect_async, + tungstenite::{error::Error, Message}, +}; +use url::Url; -pub struct PrustiClient { - client: Client, - server_url: Url, -} +pub struct PrustiClient; impl PrustiClient { - pub fn new(server_address: S) -> Result { + pub async fn verify( + server_address: S, + request: VerificationRequest, + ) -> impl Stream { + // TODO: do proper error handling let mut address = server_address.to_string(); - if !address.starts_with("http") { - address = format!("http://{address}"); + if !address.starts_with("ws") { + address = format!("ws://{address}"); } - Ok(Self { - client: Client::new(), - server_url: Url::parse(address.as_str())?, - }) - } - pub async fn verify( - &self, - request: VerificationRequest, - ) -> reqwest::Result { + let server_url = Url::parse(address.as_str()).unwrap(); + let use_json = config::json_communication(); - let base = self.client.post( - self.server_url - .join(if use_json { "json/" } else { "bincode/" }) - .unwrap() - .join("verify/") - .unwrap(), - ); - let response = if use_json { - base.json(&request) - .send() - .await? - .error_for_status()? - .json() - .await? + + let uri = server_url + .join(if use_json { "json/" } else { "bincode/" }) + .unwrap() + .join("verify/") + .unwrap(); + let (mut socket, _) = connect_async(uri).await.unwrap(); + let msg = if use_json { + Message::text( + serde_json::to_string(&request) + .expect("error encoding verification request in json"), + ) } else { - let bytes = base - .body(bincode::serialize(&request).expect("error encoding verification request")) - .send() - .await? - .error_for_status()? - .bytes() - .await?; - bincode::deserialize(&bytes).expect("error decoding verification result") + Message::binary( + bincode::serialize(&request) + .expect("error encoding verification request as binary"), + ) + }; + socket.send(msg).await.unwrap(); + let json_map = |ws_msg| { + if let Message::Text(json) = ws_msg { + serde_json::from_str(&json).expect("error decoding verification result from json") + } else { + panic!("Invalid response from the server."); + } + }; + let bin_map = |ws_msg| { + if let Message::Binary(bytes) = ws_msg { + bincode::deserialize(&bytes).expect("error decoding verification result") + } else { + panic!("Invalid response from the server."); + } + }; + let filter_close = |msg_result: Result| async { + let msg = msg_result.unwrap(); + match msg { + Message::Close(_) => None, + _ => Some(msg), + } }; - Ok(response) + socket + .filter_map(filter_close) + .map(if use_json { json_map } else { bin_map }) } } diff --git a/prusti-server/src/lib.rs b/prusti-server/src/lib.rs index 64b7b670ffd..9597fba0792 100644 --- a/prusti-server/src/lib.rs +++ b/prusti-server/src/lib.rs @@ -9,6 +9,7 @@ mod client; mod process_verification; mod server; +mod server_message; mod verification_request; mod backend; @@ -16,6 +17,7 @@ pub use backend::*; pub use client::*; pub use process_verification::*; pub use server::*; +pub use server_message::*; pub use verification_request::*; // Futures returned by `Client` need to be executed in a compatible tokio runtime. diff --git a/prusti-server/src/process_verification.rs b/prusti-server/src/process_verification.rs index 46af5cd681f..3921cdd9185 100644 --- a/prusti-server/src/process_verification.rs +++ b/prusti-server/src/process_verification.rs @@ -4,8 +4,9 @@ // License, v. 2.0. If a copy of the MPL was not distributed with this // file, You can obtain one at http://mozilla.org/MPL/2.0/. -use crate::{Backend, VerificationRequest, ViperBackendConfig}; -use log::info; +use crate::{Backend, ServerMessage, VerificationRequest, ViperBackendConfig}; +use futures::{lock, stream::Stream}; +use log::{debug, info}; use once_cell::sync::Lazy; use prusti_common::{ config, @@ -13,17 +14,137 @@ use prusti_common::{ vir::{program_normalization::NormalizationInfo, ToViper}, Stopwatch, }; -use std::{fs::create_dir_all, path::PathBuf}; +use std::{ + fs::create_dir_all, + path::PathBuf, + sync::{self, mpsc, Arc}, + thread, +}; use viper::{ - smt_manager::SmtManager, Cache, VerificationBackend, VerificationContext, VerificationResult, + smt_manager::SmtManager, Cache, PersistentCache, VerificationBackend, VerificationContext, + VerificationResult, VerificationResultKind, Viper, }; +enum ServerRequest { + Verification(VerificationRequest), + SaveCache, +} + +struct ThreadJoin { + handle: Option>, +} + +// we join the thread after dropping the sender for the ServerRequests, so +// that the verification thread actually terminates +impl Drop for ThreadJoin { + fn drop(&mut self) { + self.handle.take().unwrap().join().unwrap(); + } +} + +pub struct VerificationRequestProcessing { + mtx_rx_servermsg: lock::Mutex>, + mtx_tx_verreq: sync::Mutex>, + // mtx_tx_verreq has to be dropped before thread_join + #[allow(dead_code)] + thread_join: ThreadJoin, +} + +impl Default for VerificationRequestProcessing { + fn default() -> Self { + Self::new() + } +} + +/// A structure that lives for all the requests and has a single thread working on all the +/// requests sequentially. +/// On reception of a verification request, we send it through a channel to the already running +/// thread. +impl VerificationRequestProcessing { + pub fn new() -> Self { + let (tx_servermsg, rx_servermsg) = mpsc::channel(); + let (tx_verreq, rx_verreq) = mpsc::channel(); + let mtx_rx_servermsg = lock::Mutex::new(rx_servermsg); + let mtx_tx_verreq = sync::Mutex::new(tx_verreq); + + let handle = thread::spawn(move || verification_thread(rx_verreq, tx_servermsg)); + Self { + mtx_rx_servermsg, + mtx_tx_verreq, + thread_join: ThreadJoin { + handle: Some(handle), + }, + } + } + + pub fn verify(&self, request: VerificationRequest) -> impl Stream + '_ { + self.mtx_tx_verreq + .lock() + .unwrap() + .send(ServerRequest::Verification(request)) + .unwrap(); + // return a stream that has as last non-None message the ServerMessage::Termination + futures::stream::unfold(false, move |done: bool| async move { + if done { + return None; + } + let msg = self.mtx_rx_servermsg.lock().await.recv().unwrap(); + let mut done = false; + if let ServerMessage::Termination(_) = msg { + done = true; + } + Some((msg, done)) + }) + } + + pub fn save_cache(&self) { + self.mtx_tx_verreq + .lock() + .unwrap() + .send(ServerRequest::SaveCache) + .unwrap(); + } +} + +fn verification_thread( + rx_verreq: mpsc::Receiver, + tx_servermsg: mpsc::Sender, +) { + debug!("Verification thread started."); + let viper = Lazy::new(|| { + Arc::new(Viper::new_with_args( + &config::viper_home(), + config::extra_jvm_args(), + )) + }); + let viper_thread = Lazy::new(|| viper.attach_current_thread()); + let mut cache = PersistentCache::load_cache(config::cache_path()); + + while let Ok(request) = rx_verreq.recv() { + match request { + ServerRequest::Verification(verification_request) => process_verification_request( + &viper, + &viper_thread, + &mut cache, + &tx_servermsg, + verification_request, + ), + ServerRequest::SaveCache => cache.save(), + } + } + debug!("Verification thread finished."); +} + #[tracing::instrument(level = "debug", skip_all, fields(program = %request.program.get_name()))] pub fn process_verification_request<'v, 't: 'v>( + viper_arc: &Lazy, impl Fn() -> Arc>, verification_context: &'v Lazy, impl Fn() -> VerificationContext<'t>>, - mut request: VerificationRequest, cache: impl Cache, -) -> viper::VerificationResult { + sender: &mpsc::Sender, + mut request: VerificationRequest, +) { + // TODO: if I'm not mistaken, this currently triggers the creation of the JVM on every request, + // so this should be changed once there are actually backends that not use a JVM let ast_utils = verification_context.new_ast_utils(); // Only for testing: Check that the normalization is reversible. @@ -78,7 +199,12 @@ pub fn process_verification_request<'v, 't: 'v>( let _ = build_or_dump_viper_program(); }); } - return viper::VerificationResult::Success; + sender + .send(ServerMessage::Termination( + VerificationResult::dummy_success(), + )) + .unwrap(); + return; } // Early return in case of cache hit @@ -94,8 +220,10 @@ pub fn process_verification_request<'v, 't: 'v>( let _ = build_or_dump_viper_program(); }); } - normalization_info.denormalize_result(&mut result); - return result; + result.cached = true; + normalization_info.denormalize_result(&mut result.kind); + sender.send(ServerMessage::Termination(result)).unwrap(); + return; } }; @@ -111,14 +239,22 @@ pub fn process_verification_request<'v, 't: 'v>( request.backend_config, ), verification_context, + Lazy::force(viper_arc), ), }; stopwatch.start_next("backend verification"); - let mut result = backend.verify(&request.program); + let mut result = VerificationResult { + item_name: request.program.get_name().to_string(), + kind: VerificationResultKind::Success, + cached: false, + time_ms: 0, + }; + result.kind = backend.verify(&request.program, sender.clone()); + result.time_ms = stopwatch.finish().as_millis(); // Don't cache Java exceptions, which might be due to misconfigured paths. - if config::enable_cache() && !matches!(result, VerificationResult::JavaException(_)) { + if config::enable_cache() && !matches!(result.kind, VerificationResultKind::JavaException(_)) { info!( "Storing new cached result {:?} for program {}", &result, @@ -127,8 +263,8 @@ pub fn process_verification_request<'v, 't: 'v>( cache.insert(hash, result.clone()); } - normalization_info.denormalize_result(&mut result); - result + normalization_info.denormalize_result(&mut result.kind); + sender.send(ServerMessage::Termination(result)).unwrap(); } pub fn dump_viper_program( diff --git a/prusti-server/src/server.rs b/prusti-server/src/server.rs index 1d13a9a01c3..87dc48714a4 100644 --- a/prusti-server/src/server.rs +++ b/prusti-server/src/server.rs @@ -4,17 +4,16 @@ // License, v. 2.0. If a copy of the MPL was not distributed with this // file, You can obtain one at http://mozilla.org/MPL/2.0/. -use crate::{process_verification_request, VerificationRequest}; +use crate::VerificationRequestProcessing; +use futures_util::{pin_mut, SinkExt, StreamExt}; use log::info; use once_cell::sync::Lazy; -use prusti_common::{config, Stopwatch}; use std::{ net::{Ipv4Addr, SocketAddr}, - sync::{mpsc, Arc, Mutex}, + sync::mpsc, thread, }; use tokio::runtime::Builder; -use viper::{PersistentCache, Viper}; use warp::Filter; #[derive(Debug)] @@ -42,61 +41,74 @@ pub fn spawn_server_thread() -> SocketAddr { receiver.recv().unwrap() } +// This VerificationRequestProcessing object is starting the verification thread (for more details +// see the file process_verification.rs). +// It has to have a static lifetime because warp websockets need their closures to have a static +// lifetime and we need to access this object in them. +static VERIFICATION_REQUEST_PROCESSING: Lazy = + Lazy::new(VerificationRequestProcessing::new); + fn listen_on_port_with_address_callback(port: u16, address_callback: F) -> ! where F: FnOnce(SocketAddr), { - let stopwatch = Stopwatch::start("prusti-server", "JVM startup"); - let viper = Arc::new(Lazy::new(|| { - Viper::new_with_args(&config::viper_home(), config::extra_jvm_args()) - })); - - stopwatch.finish(); - - let cache_data = PersistentCache::load_cache(config::cache_path()); - let cache = Arc::new(Mutex::new(cache_data)); - let build_verification_request_handler = |viper_arc: Arc>, cache| { - move |request: VerificationRequest| { - let stopwatch = Stopwatch::start("prusti-server", "attach thread to JVM"); - let viper_thread = Lazy::new(|| viper_arc.attach_current_thread()); - stopwatch.finish(); - process_verification_request(&viper_thread, request, &cache) - } - }; - let json_verify = warp::path!("json" / "verify") - .and(warp::body::json()) - .map(build_verification_request_handler( - viper.clone(), - cache.clone(), - )) - .map(|response| warp::reply::json(&response)); + .and(warp::filters::ws::ws()) + .map(|ws: warp::filters::ws::Ws| { + ws.on_upgrade(|websocket| async { + let (mut ws_send, mut ws_recv) = websocket.split(); + let req_msg = ws_recv.next().await.unwrap().unwrap(); + let verification_request = req_msg + .to_str() + .and_then(|s: &str| serde_json::from_str(s).unwrap()) + .unwrap(); + let stream = VERIFICATION_REQUEST_PROCESSING.verify(verification_request); + pin_mut!(stream); + while let Some(server_msg) = stream.next().await { + ws_send + .send(warp::filters::ws::Message::text( + serde_json::to_string(&server_msg).unwrap(), + )) + .await + .unwrap(); + } + ws_send.close().await.unwrap(); + // receive the client close to complete the handshake + ws_recv.next().await.unwrap().unwrap(); + }) + }); let bincode_verify = warp::path!("bincode" / "verify") - .and(warp::body::bytes()) - .and_then(|buf: warp::hyper::body::Bytes| async move { - bincode::deserialize(&buf).map_err(|err| { - info!("request bincode body error: {}", err); - warp::reject::custom(BincodeReject(err)) + .and(warp::filters::ws::ws()) + .map(|ws: warp::filters::ws::Ws| { + ws.on_upgrade(|websocket| async { + let (mut ws_send, mut ws_recv) = websocket.split(); + let req_msg = ws_recv.next().await.unwrap().unwrap(); + let verification_request = bincode::deserialize(req_msg.as_bytes()).unwrap(); + let stream = VERIFICATION_REQUEST_PROCESSING.verify(verification_request); + pin_mut!(stream); + while let Some(server_msg) = stream.next().await { + ws_send + .send(warp::filters::ws::Message::binary( + bincode::serialize(&server_msg).unwrap(), + )) + .await + .unwrap(); + } + ws_send.close().await.unwrap(); + // receive the client close to complete the handshake + ws_recv.next().await.unwrap().unwrap(); }) - }) - .map(build_verification_request_handler(viper, cache.clone())) - .map(|result| { - warp::http::Response::new( - bincode::serialize(&result).expect("could not encode verification result"), - ) }); - let save_cache = warp::post() .and(warp::path("save")) .and(warp::path::end()) .map(move || { - cache.lock().unwrap().save(); + VERIFICATION_REQUEST_PROCESSING.save_cache(); warp::reply::html("Saved") }); let endpoints = json_verify.or(bincode_verify).or(save_cache); - // Here we use a single thread because // 1. Viper is not thread safe yet (Silicon issue #578), and // 2. By default Silicon already uses as many cores as possible. diff --git a/prusti-server/src/server_message.rs b/prusti-server/src/server_message.rs new file mode 100644 index 00000000000..8eacbb17a04 --- /dev/null +++ b/prusti-server/src/server_message.rs @@ -0,0 +1,33 @@ +// © 2023, ETH Zurich +// +// This Source Code Form is subject to the terms of the Mozilla Public +// License, v. 2.0. If a copy of the MPL was not distributed with this +// file, You can obtain one at http://mozilla.org/MPL/2.0/. + +use viper::VerificationResult; + +#[derive(Debug, Clone, serde::Serialize, serde::Deserialize)] +/// A message from a Prusti server to a Prusti client. It may contain a result +/// of a verification or anything a server might send to a client. +pub enum ServerMessage { + /// Contains the result of a verification and signals that this verification + /// has terminated. + Termination(VerificationResult), + + /// A message created by the Viper backend with Z3 about + /// the number of instantiations of the named quantifier. + QuantifierInstantiation { + q_name: String, + insts: u64, + pos_id: u64, + }, + + /// Also created by the Viper backend. The viper_quant is the expression the + /// quantifier was translated to in silver syntax while the triggers are the + /// triggers provided or automatically derived for this quantifier. + QuantifierChosenTriggers { + viper_quant: String, + triggers: String, + pos_id: u64, + }, +} diff --git a/prusti-server/src/verification_request.rs b/prusti-server/src/verification_request.rs index 6f33840ea70..a86ceee26ad 100644 --- a/prusti-server/src/verification_request.rs +++ b/prusti-server/src/verification_request.rs @@ -53,16 +53,25 @@ impl ViperBackendConfig { "--assertTimeout".to_string(), config::assert_timeout().to_string(), "--proverConfigArgs".to_string(), - // model.partial changes the default case of functions in counterexamples - // to #unspecified - format!( - "smt.qi.eager_threshold={} model.partial={}", - config::smt_qi_eager_threshold(), - config::counterexample() - ), - "--logLevel".to_string(), - "ERROR".to_string(), ]); + // model.partial changes the default case of functions in counterexamples + // to #unspecified + let mut prover_args = format!( + "smt.qi.eager_threshold={} model.partial={}", + config::smt_qi_eager_threshold(), + config::counterexample() + ); + + if let Some(smt_qi_profile) = config::smt_qi_profile() { + prover_args = format!("{prover_args} smt.qi.profile={smt_qi_profile}"); + } + if let Some(smt_qi_profile_freq) = config::smt_qi_profile_freq() { + prover_args = + format!("{prover_args} smt.qi.profile_freq={smt_qi_profile_freq}"); + } + verifier_args.push(prover_args); + + verifier_args.extend(vec!["--logLevel".to_string(), "ERROR".to_string()]); if let Some(check_timeout) = config::check_timeout() { verifier_args.push("--checkTimeout".to_string()); diff --git a/prusti-server/tests/basic_requests.rs b/prusti-server/tests/basic_requests.rs index edb7aca6768..8a92b8adcd4 100644 --- a/prusti-server/tests/basic_requests.rs +++ b/prusti-server/tests/basic_requests.rs @@ -1,10 +1,11 @@ +use futures_util::stream::StreamExt; use lazy_static::lazy_static; use prusti_common::vir::*; use prusti_server::{ - spawn_server_thread, tokio::runtime::Builder, PrustiClient, VerificationRequest, + spawn_server_thread, tokio::runtime::Builder, PrustiClient, ServerMessage, VerificationRequest, ViperBackendConfig, }; -use viper::VerificationResult; +use viper::VerificationResultKind; lazy_static! { // only start the jvm & server once @@ -21,7 +22,7 @@ fn consistency_error() { }); match result { - VerificationResult::ConsistencyErrors(errors) => assert_eq!(errors.len(), 1), + VerificationResultKind::ConsistencyErrors(errors) => assert_eq!(errors.len(), 1), other => panic!("consistency errors not identified, instead found {other:?}"), } } @@ -31,17 +32,15 @@ fn empty_program() { let result = process_program(|_| ()); match result { - VerificationResult::Success => {} + VerificationResultKind::Success => {} other => panic!("empty program not verified successfully, instead found {other:?}"), } } -fn process_program(configure: F) -> VerificationResult +fn process_program(configure: F) -> VerificationResultKind where F: FnOnce(&mut Program), { - let client = PrustiClient::new(SERVER_ADDRESS.clone()).expect("Could not connect to server!"); - let mut program = Program { name: "dummy".to_string(), backend_types: vec![], @@ -65,6 +64,16 @@ where .enable_all() .build() .expect("failed to construct Tokio runtime") - .block_on(client.verify(request)) - .expect("Verification request failed") + .block_on(async { + PrustiClient::verify(SERVER_ADDRESS.clone(), request) + .await + .collect::>() + .await + .into_iter() + .find_map(|m| match m { + ServerMessage::Termination(res) => Some(res.kind), + _ => None, + }) + .unwrap_or_else(|| VerificationResultKind::Failure(vec![])) + }) } diff --git a/prusti-smt-solver/Cargo.toml b/prusti-smt-solver/Cargo.toml index b1ce69b796b..4793cb0a5c4 100644 --- a/prusti-smt-solver/Cargo.toml +++ b/prusti-smt-solver/Cargo.toml @@ -15,4 +15,4 @@ futures = "0.3" [dependencies.async-std] version = "1.7.0" -features = ["attributes", "unstable"] \ No newline at end of file +features = ["attributes", "unstable"] diff --git a/prusti-tests/tests/verify/ui/forall_verify.rs b/prusti-tests/tests/verify/ui/forall_verify.rs index 27bb02cc20e..42fd19e8cb3 100644 --- a/prusti-tests/tests/verify/ui/forall_verify.rs +++ b/prusti-tests/tests/verify/ui/forall_verify.rs @@ -25,9 +25,6 @@ fn test4() {} #[ensures(exists(|x: i32| identity(x) == x))] fn test5() {} -// TODO: Figure out why the error position is worse than for test3. I -// have checked the emitted Viper code (including the positions) and -// could not see any relevant differences. #[ensures(exists(|x: i32| identity(x) == x + 1))] fn test6() {} diff --git a/prusti-tests/tests/verify/ui/forall_verify.stderr b/prusti-tests/tests/verify/ui/forall_verify.stderr index 63d52476fb4..bc184727e7f 100644 --- a/prusti-tests/tests/verify/ui/forall_verify.stderr +++ b/prusti-tests/tests/verify/ui/forall_verify.stderr @@ -11,9 +11,15 @@ note: the error originates here | ^^^^^^^^^^^^^ error: [Prusti: verification error] postcondition might not hold. - --> $DIR/forall_verify.rs:32:1 + --> $DIR/forall_verify.rs:28:11 | -32 | fn test6() {} +28 | #[ensures(exists(|x: i32| identity(x) == x + 1))] + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + | +note: the error originates here + --> $DIR/forall_verify.rs:29:1 + | +29 | fn test6() {} | ^^^^^^^^^^^^^ error: aborting due to 2 previous errors diff --git a/prusti-tests/tests/verify/ui/forall_verify.stdout b/prusti-tests/tests/verify/ui/forall_verify.stdout index 29f01018e3e..db8ca2a9fe6 100644 --- a/prusti-tests/tests/verify/ui/forall_verify.stdout +++ b/prusti-tests/tests/verify/ui/forall_verify.stdout @@ -12,9 +12,6 @@ // A witness. -// TODO: Figure out why the error position is worse than for test3. I -// have checked the emitted Viper code (including the positions) and -// could not see any relevant differences. #![feature(type_ascription)] #![feature(stmt_expr_attributes)] diff --git a/prusti-utils/src/config.rs b/prusti-utils/src/config.rs index 65a6bc9e624..3b21b54e4eb 100644 --- a/prusti-utils/src/config.rs +++ b/prusti-utils/src/config.rs @@ -103,6 +103,9 @@ lazy_static::lazy_static! { settings.set_default("quiet", false).unwrap(); settings.set_default("assert_timeout", 10_000).unwrap(); settings.set_default("smt_qi_eager_threshold", 1000).unwrap(); + settings.set_default::>("smt_qi_profile", None).unwrap(); + settings.set_default::>("smt_qi_profile_freq", None).unwrap(); + settings.set_default("report_viper_messages", false).unwrap(); settings.set_default("use_more_complete_exhale", true).unwrap(); settings.set_default("skip_unsupported_features", false).unwrap(); settings.set_default("internal_errors_as_warnings", false).unwrap(); @@ -168,6 +171,13 @@ lazy_static::lazy_static! { settings.set_default::>("verify_only_basic_block_path", vec![]).unwrap(); settings.set_default::>("delete_basic_blocks", vec![]).unwrap(); + // Flags specifically for Prusti-Assistant: + settings.set_default("show_ide_info", false).unwrap(); + settings.set_default("skip_verification", false).unwrap(); + settings.set_default::>("verify_only_defpath", None).unwrap(); + settings.set_default::>("query_method_signature", None).unwrap(); + + // Get the list of all allowed flags. let mut allowed_keys = get_keys(&settings); allowed_keys.insert("server_max_stored_verifiers".to_string()); @@ -500,6 +510,22 @@ pub fn smt_qi_eager_threshold() -> u64 { read_setting("smt_qi_eager_threshold") } +/// Whether to make Z3 periodically report quantifier instantiations to Viper. +pub fn smt_qi_profile() -> Option { + read_setting("smt_qi_profile") +} + +/// The frequency for the report of quantifier instantiations of Z3 to Viper. +pub fn smt_qi_profile_freq() -> Option { + read_setting("smt_qi_profile_freq") +} + +/// Whether to report the messages produced by the viper backend (e.g. quantifier instantiations, +/// quantifier triggers) +pub fn report_viper_messages() -> bool { + read_setting("report_viper_messages") +} + /// Maximum time (in milliseconds) for the verifier to spend on checks. /// Set to None uses the verifier's default value. Maps to the verifier command-line /// argument `--checkTimeout`. @@ -1023,3 +1049,31 @@ pub fn cargo_command() -> String { pub fn enable_type_invariants() -> bool { read_setting("enable_type_invariants") } + +/// When enabled, prusti should return various Data structures that are +/// used by prusti-assistant, such as a list of method calls, +/// a list of all procedures to be verified, etc. +pub fn show_ide_info() -> bool { + read_setting("show_ide_info") +} + +/// When enabled, verification is skipped. Similar to no_verify but needed +/// because no_verify is also set automatically for dependencies, independent +/// of whether the user passed this flag. In general only required because +/// of issue #1261 +pub fn skip_verification() -> bool { + read_setting("skip_verification") +} + +/// Used for selective verification, can be passed a String containing +/// the DefPath of the method to be verified +pub fn verify_only_defpath() -> Option { + read_setting("verify_only_defpath") +} + +/// A flag that can be used to ask the compiler for the declaration / +/// signature of a method, used to automatically generate a skeleton +/// for an external specification +pub fn query_method_signature() -> Option { + read_setting("query_method_signature") +} diff --git a/prusti-viper/Cargo.toml b/prusti-viper/Cargo.toml index 8ff1f75d43a..22478865bd6 100644 --- a/prusti-viper/Cargo.toml +++ b/prusti-viper/Cargo.toml @@ -27,7 +27,10 @@ backtrace = "0.3" rustc-hash = "1.1.0" derive_more = "0.99.16" itertools = "0.10.3" +async-stream = "0.3.3" +futures-util = "0.3.25" once_cell = "1.17.1" +tokio = { version = "1.20", features = ["io-util", "net", "rt", "sync"] } [dev-dependencies] lazy_static = "1.4" diff --git a/prusti-viper/src/encoder/encoder.rs b/prusti-viper/src/encoder/encoder.rs index c576005244e..76d2f06b11d 100644 --- a/prusti-viper/src/encoder/encoder.rs +++ b/prusti-viper/src/encoder/encoder.rs @@ -63,6 +63,7 @@ use super::mir::{ use super::high::types::{HighTypeEncoderState, HighTypeEncoderInterface}; use super::counterexamples::{MirProcedureMappingInterface, MirProcedureMapping}; use super::counterexamples::DiscriminantsState; +use crate::ide::encoding_info::SpanOfCallContracts; use super::high::to_typed::types::HighToTypedTypeEncoderState; pub struct Encoder<'v, 'tcx: 'v> { @@ -104,6 +105,9 @@ pub struct Encoder<'v, 'tcx: 'v> { /// this requires special care when encoding array/slice accesses which may come with /// bound checks included in the MIR. pub(super) is_encoding_trigger: Cell, + /// When calls are being encoded, this Vec saves the spans of all items of the + /// contract so they can later be passed to prusti-assistant + pub spans_of_call_contracts: RefCell>, } pub enum EncodingTask<'tcx> { @@ -182,6 +186,7 @@ impl<'v, 'tcx> Encoder<'v, 'tcx> { specifications_state: SpecificationsState::new(def_spec), mir_procedure_mapping: Default::default(), discriminants_state: Default::default(), + spans_of_call_contracts: Default::default(), } } diff --git a/prusti-viper/src/encoder/errors/position_manager.rs b/prusti-viper/src/encoder/errors/position_manager.rs index b1575ec0e0f..997c57da97d 100644 --- a/prusti-viper/src/encoder/errors/position_manager.rs +++ b/prusti-viper/src/encoder/errors/position_manager.rs @@ -88,4 +88,8 @@ impl<'tcx> PositionManager<'tcx> pub fn get_span(&self, pos: Position) -> Option<&MultiSpan> { self.source_span.get(&pos.id()) } + + pub fn get_span_from_id(&self, pos_id: u64) -> Option<&MultiSpan> { + self.source_span.get(&pos_id) + } } diff --git a/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs b/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs index e0e7b13c189..2368165bca1 100644 --- a/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs +++ b/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs @@ -135,7 +135,7 @@ pub(super) fn inline_spec_item<'tcx>( pub(super) fn encode_quantifier<'tcx>( encoder: &Encoder<'_, 'tcx>, - _span: Span, + span: Span, encoded_args: Vec, is_exists: bool, parent_def_id: DefId, @@ -241,6 +241,8 @@ pub(super) fn encode_quantifier<'tcx>( body_substs, )?; + let pos = encoder.error_manager().register_span(parent_def_id, span); + // replace qvars with a nicer name based on quantifier depth to ensure that // quantifiers remain stable for caching let quantifier_depth = find_quantifier_depth(&encoded_body); @@ -274,17 +276,32 @@ pub(super) fn encode_quantifier<'tcx>( } else { vir_crate::polymorphic::Expr::implies(bounds.into_iter().conjoin(), encoded_body) }; + if is_exists { - Ok(vir_crate::polymorphic::Expr::exists( + Ok(vir_crate::polymorphic::Expr::exists_with_pos( fixed_qvars, encoded_trigger_sets, final_body, + // we encode the position ID in the line number because that is used to name the + // quantifiers in z3 + vir_crate::polymorphic::Position::new( + i32::try_from(pos.id()).unwrap(), + i32::try_from(pos.id()).unwrap(), + pos.id(), + ), )) } else { - Ok(vir_crate::polymorphic::Expr::forall( + Ok(vir_crate::polymorphic::Expr::forall_with_pos( fixed_qvars, encoded_trigger_sets, final_body, + // we encode the position ID in the line number because that is used to name the + // quantifiers in z3 + vir_crate::polymorphic::Position::new( + i32::try_from(pos.id()).unwrap(), + i32::try_from(pos.id()).unwrap(), + pos.id(), + ), )) } } diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs index 516870a4c19..9d8cf59f8ca 100644 --- a/prusti-viper/src/encoder/procedure_encoder.rs +++ b/prusti-viper/src/encoder/procedure_encoder.rs @@ -23,6 +23,7 @@ use crate::encoder::Encoder; use crate::encoder::snapshot::interface::SnapshotEncoderInterface; use crate::encoder::mir::procedures::encoder::specification_blocks::SpecificationBlocks; use crate::error_unsupported; +use crate::ide::encoding_info::SpanOfCallContracts; use prusti_common::{ config, utils::to_string::ToString, @@ -3378,6 +3379,16 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { substs, ).with_span(call_site_span)? }; + if config::show_ide_info() { + // store spans of items of the contracts for prusti-assistant + self.store_contract_spans( + called_def_id, + &procedure_contract, + call_site_span, + substs, + ); + } + assert_one_magic_wand(procedure_contract.borrow_infos.len()).with_span(call_site_span)?; // Store a label for the pre state @@ -3519,6 +3530,57 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { Ok(stmts) } + /// Collect all the available spans of the items of a contract + /// and store them. Purpose of this function is to later pass these + /// spans to prusti-assistant, so users can look up contracts of + /// function calls + fn store_contract_spans( + &self, + called_def_id: ProcedureDefId, + contract: &ProcedureContract<'tcx>, + call_site_span: Span, + substs: ty::subst::SubstsRef<'tcx>, + ) { + + let mut pre_post = contract.functional_precondition(self.encoder.env(), substs); + pre_post.append(&mut contract.functional_postcondition(self.encoder.env(), substs)); + let mut contracts_def_ids: Vec = pre_post.iter().map(|(ts, _)| *ts).collect(); + + if let Some(Some(purity_defid)) = contract.specification.purity.extract_with_selective_replacement() { + contracts_def_ids.push(*purity_defid); + } + if let Some(Some(term_local_defid)) = contract.specification.terminates.extract_with_selective_replacement() { + contracts_def_ids.push(term_local_defid.to_def_id()); + } + let mut result = contracts_def_ids + .iter() + .map(|id| self.encoder.env().query.get_def_span(*id)) + .collect::>(); + + // for each pledge, if it has a lefthandside, join the 2, otherwise + // just return span of the righthandside + let mut pledges: Vec = contract.pledges() + .map(|pledge| { + if let Some(lhs_defid) = pledge.lhs { + let lhs_span = self.encoder.env().query.get_def_span(lhs_defid); + let rhs_span = self.encoder.env().query.get_def_span(pledge.rhs); + lhs_span.to(rhs_span) + } else { + self.encoder.env().query.get_def_span(pledge.rhs) + } + }) + .collect(); + result.append(&mut pledges); + let tcx = self.encoder.env().tcx(); + let contract_spans = SpanOfCallContracts::new( + tcx.def_path_str(called_def_id), + call_site_span, + result, + tcx.sess.source_map(), + ); + self.encoder.spans_of_call_contracts.borrow_mut().push(contract_spans); + } + #[allow(clippy::too_many_arguments)] #[tracing::instrument(level = "debug", skip(self))] fn encode_pure_function_call( diff --git a/prusti-viper/src/ide/encoding_info.rs b/prusti-viper/src/ide/encoding_info.rs new file mode 100644 index 00000000000..e5b0e85e61a --- /dev/null +++ b/prusti-viper/src/ide/encoding_info.rs @@ -0,0 +1,48 @@ +use prusti_rustc_interface::span::{source_map::SourceMap, Span}; +use serde::Serialize; +use super::vsc_span::VscSpan; + +/// Represents the locations of specifications of a function call. +/// Generated for each encoded function call to be used by prusti-assistant. +#[derive(Serialize, Clone)] +pub struct SpanOfCallContracts { + /// the defpath of the method that is called + pub defpath: String, + /// the span where this method is called + pub call_span: VscSpan, + /// the spans of all the specifications of the called method + pub contracts_spans: Vec, +} + +impl SpanOfCallContracts { + pub fn new( + defpath: String, + call_span: Span, + contracts_spans: Vec, + source_map: &SourceMap + ) -> Self { + let call_span = VscSpan::from_span(&call_span, source_map); + let contracts_spans = contracts_spans + .iter() + .map(|sp| VscSpan::from_span(sp, source_map)) + .collect::>(); + Self { + defpath, + call_span, + contracts_spans, + } + } + +} + +#[derive(Serialize)] +pub struct EncodingInfo { + pub call_contract_spans: Vec, +} + +impl EncodingInfo { + pub fn to_json_string(self) -> String { + serde_json::to_string(&self).unwrap() + } +} + diff --git a/prusti-viper/src/ide/ide_verification_result.rs b/prusti-viper/src/ide/ide_verification_result.rs new file mode 100644 index 00000000000..378dc0a9bd4 --- /dev/null +++ b/prusti-viper/src/ide/ide_verification_result.rs @@ -0,0 +1,29 @@ +use serde::Serialize; +use viper::VerificationResult; + +/// Generated for each verification item, containing information +/// about the result of the verification. This information will be emitted +/// if the show_ide_info flag is set, and it's purpose is to be +/// consumed by prusti-assistant. +#[derive(Serialize)] +pub struct IdeVerificationResult { + /// the name / defpath of the method + item_name: String, + /// whether the verification of that method was successful + success: bool, + /// how long the verification took + time_ms: u128, + /// whether this result was cached or is fresh + cached: bool, +} + +impl From<&VerificationResult> for IdeVerificationResult { + fn from(res: &VerificationResult) -> Self { + Self { + item_name: res.item_name.clone(), + success: res.is_success(), + time_ms: res.time_ms, + cached: res.cached, + } + } +} diff --git a/prusti-viper/src/ide/mod.rs b/prusti-viper/src/ide/mod.rs new file mode 100644 index 00000000000..a5785594aba --- /dev/null +++ b/prusti-viper/src/ide/mod.rs @@ -0,0 +1,3 @@ +pub mod ide_verification_result; +pub mod encoding_info; +pub mod vsc_span; diff --git a/prusti-viper/src/ide/vsc_span.rs b/prusti-viper/src/ide/vsc_span.rs new file mode 100644 index 00000000000..e452e74bec1 --- /dev/null +++ b/prusti-viper/src/ide/vsc_span.rs @@ -0,0 +1,34 @@ +use prusti_rustc_interface::span::{source_map::SourceMap, Span}; +use serde::Serialize; + +/// a representation of spans that is more usable with VSCode. +#[derive(Serialize, Clone)] +pub struct VscSpan { + column_end: usize, + column_start: usize, + line_end: usize, + line_start: usize, + file_name: String, + is_primary: bool, +} + +impl VscSpan { + pub fn from_span(sp: &Span, sourcemap: &SourceMap) -> Self { + let span_filename = sourcemap.span_to_filename(*sp); + let diag_filename = sourcemap.filename_for_diagnostics(&span_filename); + let file_name = format!("{diag_filename}"); + + let (l1, l2) = sourcemap.is_valid_span(*sp).expect("Invalid span"); + Self { + column_start: l1.col.0, + column_end: l2.col.0, + line_start: l1.line, + line_end: l2.line, + file_name, + // the following one is not relevant here, we just want to be + // able to reuse the existing methods and the parser + // for spans in VSCode + is_primary: false, + } + } +} diff --git a/prusti-viper/src/lib.rs b/prusti-viper/src/lib.rs index f423994ada7..c260d153543 100644 --- a/prusti-viper/src/lib.rs +++ b/prusti-viper/src/lib.rs @@ -26,3 +26,4 @@ pub mod encoder; mod utils; pub mod verifier; +pub mod ide; diff --git a/prusti-viper/src/verifier.rs b/prusti-viper/src/verifier.rs index 019abb0ed40..d45051f24e6 100644 --- a/prusti-viper/src/verifier.rs +++ b/prusti-viper/src/verifier.rs @@ -4,12 +4,16 @@ // License, v. 2.0. If a copy of the MPL was not distributed with this // file, You can obtain one at http://mozilla.org/MPL/2.0/. -use crate::encoder::{ - counterexamples::{counterexample_translation, counterexample_translation_refactored}, - Encoder, +use async_stream::stream; +use crate::{ + encoder::{ + counterexamples::{counterexample_translation, counterexample_translation_refactored}, + Encoder, + }, + ide::{self, ide_verification_result::IdeVerificationResult}, }; +use futures_util::{pin_mut, Stream, StreamExt}; use ::log::{debug, error, info}; -use once_cell::sync::Lazy; use prusti_common::{ config, report::log, @@ -24,10 +28,13 @@ use prusti_interface::{ }; use prusti_rustc_interface::span::DUMMY_SP; use prusti_server::{ - process_verification_request, spawn_server_thread, tokio::runtime::Builder, PrustiClient, - VerificationRequest, ViperBackendConfig, + spawn_server_thread, PrustiClient, ServerMessage, VerificationRequest, + VerificationRequestProcessing, ViperBackendConfig, }; -use viper::{self, PersistentCache, Viper}; +use rustc_hash::FxHashMap; +use serde_json::json; +use tokio::runtime::Builder; +use viper; use vir_crate::common::check_mode::CheckMode; /// A verifier is an object for verifying a single crate, potentially @@ -74,8 +81,6 @@ impl<'v, 'tcx> Verifier<'v, 'tcx> { } self.encoder.process_encoding_queue(); - let encoding_errors_count = self.encoder.count_encoding_errors(); - let polymorphic_programs = self.encoder.get_viper_programs(); let mut programs: Vec = if config::simplify_encoding() { @@ -93,193 +98,337 @@ impl<'v, 'tcx> Verifier<'v, 'tcx> { }; programs.extend(self.encoder.get_core_proof_programs()); + if config::show_ide_info() { + self.emit_contract_spans(); + } + stopwatch.start_next("verifying Viper program"); - let verification_results = verify_programs(self.env, programs); + + let requests = self.programs_to_requests(programs); + + // runtime used either for client connecting to server sequentially + // or to sequentially verify the requests -> single thread is sufficient + // why single thread if everything is asynchronous? VerificationRequestProcessing in + // prusti-server/src/process_verification.rs only has a single thread and the underlying + // viper instance already uses as many cores as possible + let rt = Builder::new_current_thread() + .thread_name("prusti_viper_verifier_verify") + .enable_all() + .build() + .unwrap(); + + let overall_result = rt.block_on(async { + if let Some(server_address) = config::server_address() { + let verification_messages = Self::verify_requests_server(requests, server_address); + self.handle_stream(verification_messages).await + } else { + let vrp = VerificationRequestProcessing::new(); + let verification_messages = Self::verify_requests_local(requests, &vrp); + self.handle_stream(verification_messages).await + } + }); stopwatch.finish(); + overall_result + } - // Group verification results - let mut verification_errors: Vec<_> = vec![]; - let mut consistency_errors: Vec<_> = vec![]; - let mut java_exceptions: Vec<_> = vec![]; - for (method_name, result) in verification_results.into_iter() { - match result { - viper::VerificationResult::Success => {} - viper::VerificationResult::ConsistencyErrors(errors) => { - for error in errors.into_iter() { - consistency_errors.push((method_name.clone(), error)); - } - } - viper::VerificationResult::Failure(errors) => { - for error in errors.into_iter() { - verification_errors.push((method_name.clone(), error)); - } - } - viper::VerificationResult::JavaException(exception) => { - java_exceptions.push((method_name, exception)); - } + async fn handle_stream( + &self, + verification_messages: impl Stream, + ) -> VerificationResult { + let mut overall_result = VerificationResult::Success; + let encoding_errors_count = self.encoder.count_encoding_errors(); + // we want quantifier_pos_ID + program_name + q_name as identifier because there are + // different q_names for the same ID and each program reports independent results + // key: (pos_id, program_name), key to result: q_name result: num_instantiations + let mut quantifier_instantiations: FxHashMap<(u64, String), FxHashMap> = + FxHashMap::default(); + + let mut prusti_errors: Vec<_> = vec![]; + + pin_mut!(verification_messages); + + while let Some((program_name, server_msg)) = verification_messages.next().await { + match server_msg { + ServerMessage::Termination(result) => self.handle_termination_message(program_name, result, &mut prusti_errors, &mut overall_result), + ServerMessage::QuantifierInstantiation { + q_name, + insts, + pos_id, + } => self.handle_quantifier_instantiation_message(program_name, q_name, insts, pos_id, &mut quantifier_instantiations), + ServerMessage::QuantifierChosenTriggers { + viper_quant, + triggers, + pos_id, + } => self.handle_quantifier_chosen_triggers_message(program_name, viper_quant, triggers, pos_id), } } - // Convert verification results to Prusti errors - let error_manager = self.encoder.error_manager(); - let mut result = VerificationResult::Success; + // if we are in an ide, we already emit the errors asynchronously, otherwise we wait for + // all of them because we want the errors to be reported sortedly + if !config::show_ide_info() { + prusti_errors.sort(); - for (method, error) in consistency_errors.into_iter() { - PrustiError::internal( - format!("consistency error in {method}: {error}"), - DUMMY_SP.into(), - ) - .emit(&self.env.diagnostic); - result = VerificationResult::Failure; + for prusti_error in prusti_errors { + debug!("Prusti error: {:?}", prusti_error); + prusti_error.emit(&self.env.diagnostic); + } } - for (method, exception) in java_exceptions.into_iter() { - error!("Java exception: {}", exception.get_stack_trace()); - PrustiError::internal(format!("in {method}: {exception}"), DUMMY_SP.into()) - .emit(&self.env.diagnostic); - result = VerificationResult::Failure; + if encoding_errors_count != 0 { + overall_result = VerificationResult::Failure; } + overall_result + } - // Report verification errors - let mut prusti_errors: Vec<_> = vec![]; - for (method, verification_error) in verification_errors.into_iter() { - debug!("Verification error in {}: {:?}", method, verification_error); - let mut prusti_error = error_manager.translate_verification_error(&verification_error); + fn handle_termination_message( + &self, + program_name: String, + result: viper::VerificationResult, + prusti_errors: &mut Vec, + overall_result: &mut VerificationResult + ) { + debug!("Received termination message with result {result:?} in verification of {program_name}"); + if config::show_ide_info() { + PrustiError::message( + format!( + "ideVerificationResult{}", + serde_json::to_string(&IdeVerificationResult::from(&result)) + .unwrap() + ), + DUMMY_SP.into(), + ) + .emit(&self.env.diagnostic); + } + match result.kind { + // nothing to do + viper::VerificationResultKind::Success => (), + viper::VerificationResultKind::ConsistencyErrors(errors) => { + for error in errors { + PrustiError::internal( + format!("consistency error in {program_name}: {error}"), + DUMMY_SP.into(), + ) + .emit(&self.env.diagnostic); + } + *overall_result = VerificationResult::Failure; + } + viper::VerificationResultKind::Failure(errors) => { + for verification_error in errors { + debug!( + "Verification error in {}: {:?}", + program_name.clone(), + verification_error + ); + let mut prusti_error = self.encoder.error_manager() + .translate_verification_error(&verification_error); - // annotate with counterexample, if requested - if config::counterexample() { - if config::unsafe_core_proof() { - if let Some(silicon_counterexample) = &verification_error.counterexample { - if let Some(def_id) = error_manager.get_def_id(&verification_error) { - let counterexample = - counterexample_translation_refactored::backtranslate( - &self.encoder, - error_manager.position_manager(), - def_id, - silicon_counterexample, + // annotate with counterexample, if requested + if config::counterexample() { + if config::unsafe_core_proof() { + if let Some(silicon_counterexample) = + &verification_error.counterexample + { + let error_manager = self.encoder.error_manager(); + if let Some(def_id) = error_manager + .get_def_id(&verification_error) + { + let counterexample = counterexample_translation_refactored::backtranslate( + &self.encoder, + error_manager.position_manager(), + def_id, + silicon_counterexample, + ); + prusti_error = + counterexample.annotate_error(prusti_error); + } else { + prusti_error = prusti_error.add_note( + format!( + "the verifier produced a counterexample for {program_name}, but it could not be mapped to source code" + ), + None, + ); + } + } + } else if let Some(silicon_counterexample) = + &verification_error.counterexample + { + if let Some(def_id) = self.encoder.error_manager() + .get_def_id(&verification_error) + { + let counterexample = + counterexample_translation::backtranslate( + &self.encoder, + def_id, + silicon_counterexample, + ); + prusti_error = + counterexample.annotate_error(prusti_error); + } else { + prusti_error = prusti_error.add_note( + format!( + "the verifier produced a counterexample for {program_name}, but it could not be mapped to source code" + ), + None, ); - prusti_error = counterexample.annotate_error(prusti_error); - } else { - prusti_error = prusti_error.add_note( - format!( - "the verifier produced a counterexample for {method}, but it could not be mapped to source code" - ), - None, - ); + } } } - } else if let Some(silicon_counterexample) = &verification_error.counterexample { - if let Some(def_id) = error_manager.get_def_id(&verification_error) { - let counterexample = counterexample_translation::backtranslate( - &self.encoder, - def_id, - silicon_counterexample, - ); - prusti_error = counterexample.annotate_error(prusti_error); + + debug!("Prusti error: {:?}", prusti_error); + if prusti_error.is_disabled() { + prusti_error.cancel(); + } else if config::show_ide_info() { + prusti_error.emit(&self.env.diagnostic); } else { - prusti_error = prusti_error.add_note( - format!( - "the verifier produced a counterexample for {method}, but it could not be mapped to source code" - ), - None, - ); + prusti_errors.push(prusti_error); } } + *overall_result = VerificationResult::Failure; + } + viper::VerificationResultKind::JavaException(exception) => { + error!("Java exception: {}", exception.get_stack_trace()); + PrustiError::internal( + format!("in {program_name}: {exception}"), + DUMMY_SP.into(), + ) + .emit(&self.env.diagnostic); + *overall_result = VerificationResult::Failure; } - - prusti_errors.push(prusti_error); } - prusti_errors.sort(); + } - for prusti_error in prusti_errors { - debug!("Prusti error: {:?}", prusti_error); - if prusti_error.is_disabled() { - prusti_error.cancel(); - } else { - prusti_error.emit(&self.env.diagnostic); + fn handle_quantifier_instantiation_message( + &self, + program_name: String, + q_name: String, + insts: u64, + pos_id: u64, + quantifier_instantiations: &mut FxHashMap<(u64, String), FxHashMap> + ) { + if config::report_viper_messages() { + debug!("Received #{insts} quantifier instantiations of {q_name} for position id {pos_id} in verification of {program_name}"); + match self.encoder.error_manager().position_manager().get_span_from_id(pos_id) { + Some(span) => { + let key = (pos_id, program_name.clone()); + if !quantifier_instantiations.contains_key(&key) { + quantifier_instantiations.insert(key.clone(), FxHashMap::default()); + } + let map = quantifier_instantiations.get_mut(&key).unwrap(); + // for some reason, the aux quantifiers by the same z3 instance (same uniqueId + // in silicon) can have different amount of instantiations. + // e.g. we receive a message with 100 instantiations for a certain quantifier + // and afterwards a message with 20 instantiations for the same one. + // All verifying the same viper program and by the same z3 instance. + // Since I don't see a better way to take this into account than taking the + // maximum, that is exactly what we do here. + let old_inst = map.get(&q_name).unwrap_or(&0); + map.insert(q_name, std::cmp::max(insts, *old_inst)); + let mut n: u64 = 0; + for (q_name, insts) in map.iter() { + debug!("Key: {q_name}, Value: {insts}"); + n += *insts; + } + PrustiError::message( + format!("quantifierInstantiationsMessage{}", + json!({"instantiations": n, "method": program_name}), + ), span.clone() + ).emit(&self.env.diagnostic); + }, + None => error!("#{insts} quantifier instantiations of {q_name} for unknown position id {pos_id} in verification of {program_name}"), } - result = VerificationResult::Failure; } + } - if encoding_errors_count != 0 { - result = VerificationResult::Failure; + fn handle_quantifier_chosen_triggers_message( + &self, + program_name: String, + viper_quant: String, + triggers: String, + pos_id: u64 + ) { + if config::report_viper_messages() && pos_id != 0 { + debug!("Received quantifier triggers {triggers} for quantifier {viper_quant} for position id {pos_id} in verification of {program_name}"); + match self.encoder.error_manager().position_manager().get_span_from_id(pos_id) { + Some(span) => { + PrustiError::message( + format!("quantifierChosenTriggersMessage{}", + json!({"viper_quant": viper_quant, "triggers": triggers}), + ), span.clone() + ).emit(&self.env.diagnostic); + }, + None => error!("Invalid position id {pos_id} for viper quantifier {viper_quant} in verification of {program_name}"), + } } + } - result + /// Returns a list of (program_name, verification_requests) tuples. + fn programs_to_requests(&self, programs: Vec) -> Vec<(String, VerificationRequest)> { + let source_path = self.env.name.source_path(); + let rust_program_name = source_path + .file_name() + .unwrap() + .to_str() + .unwrap() + .to_owned(); + let verification_requests = programs.into_iter().map(|mut program| { + let program_name = program.get_name().to_string(); + let check_mode = program.get_check_mode(); + // Prepend the Rust file name to the program. + program.set_name(format!("{rust_program_name}_{program_name}")); + let backend = if check_mode == CheckMode::Specifications { + config::verify_specifications_backend() + } else { + config::viper_backend() + } + .parse() + .unwrap(); + let request = VerificationRequest { + program, + backend_config: ViperBackendConfig::new(backend), + }; + (program_name, request) + }); + verification_requests.collect() } -} -/// Verify a list of programs. -/// Returns a list of (program_name, verification_result) tuples. -fn verify_programs( - env: &Environment, - programs: Vec, -) -> Vec<(String, viper::VerificationResult)> { - let source_path = env.name.source_path(); - let rust_program_name = source_path - .file_name() - .unwrap() - .to_str() - .unwrap() - .to_owned(); - let verification_requests = programs.into_iter().map(|mut program| { - let program_name = program.get_name().to_string(); - let check_mode = program.get_check_mode(); - // Prepend the Rust file name to the program. - program.set_name(format!("{rust_program_name}_{program_name}")); - let backend = if check_mode == CheckMode::Specifications { - config::verify_specifications_backend() - } else { - config::viper_backend() - } - .parse() - .unwrap(); - let request = VerificationRequest { - program, - backend_config: ViperBackendConfig::new(backend), - }; - (program_name, request) - }); - if let Some(server_address) = config::server_address() { + fn verify_requests_server( + verification_requests: Vec<(String, VerificationRequest)>, + server_address: String, + ) -> impl Stream { let server_address = if server_address == "MOCK" { spawn_server_thread().to_string() } else { server_address }; info!("Connecting to Prusti server at {}", server_address); - let client = PrustiClient::new(&server_address).unwrap_or_else(|error| { - panic!("Could not parse server address ({server_address}) due to {error:?}") - }); - // Here we construct a Tokio runtime to block until completion of the futures returned by - // `client.verify`. However, to report verification errors as early as possible, - // `verify_programs` should return an asynchronous stream of verification results. - let runtime = Builder::new_current_thread() - .thread_name("prusti-viper") - .enable_all() - .build() - .expect("failed to construct Tokio runtime"); - verification_requests - .map(|(program_name, request)| { - let remote_result = runtime.block_on(client.verify(request)); - let result = remote_result.unwrap_or_else(|error| { - panic!("Verification request of program {program_name} failed: {error:?}") - }); - (program_name, result) - }) - .collect() - } else { - let mut stopwatch = Stopwatch::start("prusti-viper", "JVM startup"); - stopwatch.start_next("attach current thread to the JVM"); - let viper = - Lazy::new(|| Viper::new_with_args(&config::viper_home(), config::extra_jvm_args())); - let viper_thread = Lazy::new(|| viper.attach_current_thread()); - stopwatch.finish(); - let mut cache = PersistentCache::load_cache(config::cache_path()); - verification_requests - .map(|(program_name, request)| { - let result = process_verification_request(&viper_thread, request, &mut cache); - (program_name, result) - }) - .collect() + let verification_stream = stream! { + for (program_name, request) in verification_requests { + yield PrustiClient::verify(server_address.clone(), request).await.map(move |msg| (program_name.clone(), msg)); + } + }; + verification_stream.flatten() + } + + fn verify_requests_local<'a>( + verification_requests: Vec<(String, VerificationRequest)>, + vrp: &'a VerificationRequestProcessing, + ) -> impl Stream + 'a { + let verification_stream = stream! { + for (program_name, request) in verification_requests { + yield vrp.verify(request).map(move |msg| (program_name.clone(), msg)); + } + }; + verification_stream.flatten() + } + + pub fn emit_contract_spans(&self) { + let encoding_info = ide::encoding_info::EncodingInfo { + call_contract_spans: self.encoder.spans_of_call_contracts.borrow().to_vec(), + }; + PrustiError::message( + format!("encodingInfo{}", encoding_info.to_json_string()), + DUMMY_SP.into(), + ) + .emit(&self.env.diagnostic); } } diff --git a/prusti/Cargo.toml b/prusti/Cargo.toml index 678eab4a2e2..2ec7262a98c 100644 --- a/prusti/Cargo.toml +++ b/prusti/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "prusti" -version = "0.2.1" +version = "0.3.0" authors = ["Prusti Devs "] edition = "2021" @@ -18,6 +18,8 @@ prusti-common = { path = "../prusti-common" } prusti-rustc-interface = { path = "../prusti-rustc-interface" } log = { version = "0.4", features = ["release_max_level_info"] } lazy_static = "1.4.0" +serde = { version = "1.0", features = ["derive"] } +serde_json = "1.0" tracing = { path = "../tracing" } tracing-subscriber = { version = "0.3", features = ["env-filter"] } tracing-chrome = "0.7" diff --git a/prusti/src/callbacks.rs b/prusti/src/callbacks.rs index c0d0b1523ac..ddb43206df5 100644 --- a/prusti/src/callbacks.rs +++ b/prusti/src/callbacks.rs @@ -1,8 +1,13 @@ -use crate::verifier::verify; +use crate::{ + ide_helper::{compiler_info, fake_error::fake_error}, + verifier::verify, +}; use prusti_common::config; use prusti_interface::{ + data::VerificationTask, environment::{mir_storage, Environment}, specs::{self, cross_crate::CrossCrateSpecs, is_spec_fn}, + PrustiError, }; use prusti_rustc_interface::{ driver::Compilation, @@ -14,6 +19,7 @@ use prusti_rustc_interface::{ TyCtxt, }, session::Session, + span::DUMMY_SP, }; #[derive(Default)] @@ -130,8 +136,50 @@ impl prusti_rustc_interface::driver::Callbacks for PrustiCompilerCalls { } } CrossCrateSpecs::import_export_cross_crate(&mut env, &mut def_spec); - if !config::no_verify() { - verify(env, def_spec); + + // TODO: can we replace `get_annotated_procedures` with information + // that is already in `def_spec`? + let (annotated_procedures, types) = env.get_annotated_procedures_and_types(); + + if config::show_ide_info() && !config::no_verify() { + let compiler_info = + compiler_info::IdeInfo::collect(&env, &annotated_procedures, &def_spec); + let out = serde_json::to_string(&compiler_info).unwrap(); + PrustiError::message(format!("compilerInfo{out}"), DUMMY_SP.into()) + .emit(&env.diagnostic); + } + // as long as we have to throw a fake error we need to check this + let is_primary_package = std::env::var("CARGO_PRIMARY_PACKAGE").is_ok(); + + // collect and output Information used by IDE: + if !config::no_verify() && !config::skip_verification() { + if let Some(target_def_path) = config::verify_only_defpath() { + // if we do selective verification, then definitely only + // for methods of the primary package. Check needed because + // of the fake_error, otherwise verification stops early + // with local dependencies + if is_primary_package { + let procedures = annotated_procedures + .into_iter() + .filter(|x| env.name.get_unique_item_name(*x) == target_def_path) + .collect(); + let selective_task = VerificationTask { procedures, types }; + // fake_error because otherwise a verification-success + // (for a single method for example) will cause this result + // to be cached by compiler at the moment + verify(&env, def_spec, selective_task); + fake_error(&env); + } + } else { + let verification_task = VerificationTask { + procedures: annotated_procedures, + types, + }; + verify(&env, def_spec, verification_task); + } + } else if config::skip_verification() && !config::no_verify() && is_primary_package { + // add a fake error, reason explained in issue #1261 + fake_error(&env); } }); diff --git a/prusti/src/driver.rs b/prusti/src/driver.rs index d8271f23e2d..23d055ad7b3 100644 --- a/prusti/src/driver.rs +++ b/prusti/src/driver.rs @@ -13,6 +13,7 @@ mod arg_value; mod callbacks; mod verifier; +mod ide_helper; use arg_value::arg_value; use callbacks::PrustiCompilerCalls; diff --git a/prusti/src/ide_helper/call_finder.rs b/prusti/src/ide_helper/call_finder.rs new file mode 100644 index 00000000000..3f65a810951 --- /dev/null +++ b/prusti/src/ide_helper/call_finder.rs @@ -0,0 +1,124 @@ +use prusti_interface::environment::{EnvQuery, Environment}; +use prusti_rustc_interface::{ + hir::{ + def_id::DefId, + intravisit::{self, Visitor}, + Expr, ExprKind, + }, + middle::{hir::map::Map, ty::TyCtxt}, + span::Span, +}; + +/// The hir-visitor to collect all the function calls +pub struct CallSpanFinder<'tcx> { + pub env_query: EnvQuery<'tcx>, + pub tcx: TyCtxt<'tcx>, + pub called_functions: Vec<(String, DefId, Span)>, +} + +impl<'tcx> CallSpanFinder<'tcx> { + pub fn new(env: &Environment<'tcx>) -> Self { + Self { + env_query: env.query, + called_functions: Vec::new(), + tcx: env.tcx(), + } + } + + pub fn resolve_expression(&self, expr: &'tcx Expr) -> Result<(DefId, DefId), ()> { + let maybe_method_def_id = self + .tcx + .typeck(expr.hir_id.owner.def_id) + .type_dependent_def_id(expr.hir_id); + if let Some(method_def_id) = maybe_method_def_id { + let owner_def_id = expr.hir_id.owner.def_id; + let tyck_res = self.tcx.typeck(owner_def_id); + let substs = tyck_res.node_substs(expr.hir_id); + let (resolved_def_id, _subst) = + self.env_query + .resolve_method_call(owner_def_id, method_def_id, substs); + Ok((method_def_id, resolved_def_id)) + } else { + Err(()) + } + } +} + +impl<'tcx> Visitor<'tcx> for CallSpanFinder<'tcx> { + type Map = Map<'tcx>; + type NestedFilter = prusti_rustc_interface::middle::hir::nested_filter::OnlyBodies; + + fn nested_visit_map(&mut self) -> Self::Map { + self.env_query.hir() + } + fn visit_expr(&mut self, expr: &'tcx Expr) { + intravisit::walk_expr(self, expr); + match expr.kind { + ExprKind::Call(e1, _e2) => { + if let ExprKind::Path(ref qself) = e1.kind { + let tyck_res = self.tcx.typeck(e1.hir_id.owner.def_id); + let res = tyck_res.qpath_res(qself, e1.hir_id); + if let prusti_rustc_interface::hir::def::Res::Def(_, def_id) = res { + if def_id.as_local().is_none() { + let defpath = self.tcx.def_path_str(def_id); + self.called_functions.push((defpath, def_id, expr.span)); + } + } + } + } + ExprKind::MethodCall(_path, _e1, _e2, sp) => { + let resolve_res = self.resolve_expression(expr); + if let Ok((method_def_id, resolved_def_id)) = resolve_res { + let defpath_unresolved = self.tcx.def_path_str(method_def_id); + let defpath_resolved = self.tcx.def_path_str(resolved_def_id); + + if method_def_id.as_local().is_none() { + if defpath_unresolved == defpath_resolved { + self.called_functions + .push((defpath_resolved, resolved_def_id, sp)); + } else { + // in this case we want both + self.called_functions + .push((defpath_resolved, resolved_def_id, sp)); + self.called_functions + .push((defpath_unresolved, method_def_id, sp)); + } + } + } + } + ExprKind::Binary(..) | ExprKind::AssignOp(..) | ExprKind::Unary(..) => { + let resolve_res = self.resolve_expression(expr); + // this will already fail for builtin-operations + if let Ok((method_def_id, resolved_def_id)) = resolve_res { + let defpath_unresolved = self.tcx.def_path_str(method_def_id); + let defpath_resolved = self.tcx.def_path_str(resolved_def_id); + + if method_def_id.as_local().is_none() { + if defpath_unresolved == defpath_resolved { + self.called_functions.push(( + defpath_resolved, + resolved_def_id, + expr.span, + )); + } else { + // For binary operations this will be the operation + // from the standard libary and the "overriding" method + + self.called_functions.push(( + defpath_resolved, + resolved_def_id, + expr.span, + )); + self.called_functions.push(( + defpath_unresolved, + method_def_id, + expr.span, + )); + } + } + } + } + _ => {} + } + } +} diff --git a/prusti/src/ide_helper/compiler_info.rs b/prusti/src/ide_helper/compiler_info.rs new file mode 100644 index 00000000000..c3bc5bb3804 --- /dev/null +++ b/prusti/src/ide_helper/compiler_info.rs @@ -0,0 +1,115 @@ +use super::{call_finder, query_signature}; +use prusti_interface::{environment::Environment, specs::typed}; +use prusti_rustc_interface::{ + hir::def_id::DefId, + span::{source_map::SourceMap, Span}, +}; +use prusti_viper::ide::vsc_span::VscSpan; +use serde::Serialize; + +/// This struct will be passed to prusti-assistant containing information +/// about the program that is currently being verified +#[derive(Serialize)] +pub struct IdeInfo { + procedure_defs: Vec, + function_calls: Vec, + queried_source: Option, +} + +impl IdeInfo { + pub fn collect( + env: &Environment<'_>, + procedures: &Vec, + def_spec: &typed::DefSpecificationMap, + ) -> Self { + let procedure_defs = collect_procedures(env, procedures, def_spec); + let source_map = env.tcx().sess.source_map(); + let function_calls = collect_fncalls(env) + .into_iter() + .map(|(name, defid, sp)| ProcDef { + name, + defid, + span: VscSpan::from_span(&sp, source_map), + }) + .collect::>(); + + // For declaring external specifications: + let queried_source = query_signature::collect_queried_signature(env.tcx(), &function_calls); + Self { + procedure_defs, + function_calls, + queried_source, + } + } +} + +/// A struct that contains either a reference to a procedure that can be verified +/// (for selective verification) or a function call (so a user can query +/// external_spec blocks for it). The name contains the defpath. +#[derive(Serialize)] +pub struct ProcDef { + pub name: String, + #[serde(skip)] + pub defid: DefId, + pub span: VscSpan, +} + +/// collect information about the program that will be passed to IDE. +/// This should find all non-trusted functions that can be verified +fn collect_procedures( + env: &Environment<'_>, + procedures: &Vec, + def_spec: &typed::DefSpecificationMap, +) -> Vec { + let sourcemap: &SourceMap = env.tcx().sess.source_map(); + let mut procs = Vec::new(); + for defid in procedures { + let defpath = env.name.get_unique_item_name(*defid); + let span = env.query.get_def_span(defid); + let vscspan = VscSpan::from_span(&span, sourcemap); + + // Filter out the predicates and trusted methods, + // since we don't want to allow selective verification + // for them + let mut is_predicate = false; + let mut is_trusted = false; + + let proc_spec_opt = def_spec.get_proc_spec(defid); + if let Some(proc_spec) = proc_spec_opt { + let kind_spec = proc_spec + .base_spec + .kind + .extract_with_selective_replacement(); + let trusted_spec = proc_spec + .base_spec + .trusted + .extract_with_selective_replacement(); + if let Some(typed::ProcedureSpecificationKind::Predicate(..)) = kind_spec { + is_predicate = true; + } + if let Some(true) = trusted_spec { + is_trusted = true; + } + } + + if !is_trusted && !is_predicate { + procs.push(ProcDef { + name: defpath, + defid: *defid, + span: vscspan, + }); + } + } + procs +} + +/// collect all the function calls, so the extension can query external_spec +/// templates for it +fn collect_fncalls(env: &Environment<'_>) -> Vec<(String, DefId, Span)> { + let mut fnvisitor = call_finder::CallSpanFinder::new(env); + env.tcx() + .hir() + .visit_all_item_likes_in_crate(&mut fnvisitor); + + fnvisitor.called_functions +} diff --git a/prusti/src/ide_helper/fake_error.rs b/prusti/src/ide_helper/fake_error.rs new file mode 100644 index 00000000000..f059f7b4217 --- /dev/null +++ b/prusti/src/ide_helper/fake_error.rs @@ -0,0 +1,16 @@ +use prusti_interface::environment::Environment; +use prusti_rustc_interface::{errors::MultiSpan, span::DUMMY_SP}; + +/// This error will be thrown when skipping verification (which is done +/// when we just collect information for prusti-assistant), because then +/// a successful result will be cached and subsequent actual verifications succeed +/// (see issue #1261) +pub fn fake_error(env: &Environment) { + let sp = MultiSpan::from_span(DUMMY_SP); + let message = String::from("[Prusti: FakeError]"); + let help = None; + let notes = []; + + env.diagnostic + .span_err_with_help_and_notes(sp, &message, &help, ¬es); +} diff --git a/prusti/src/ide_helper/mod.rs b/prusti/src/ide_helper/mod.rs new file mode 100644 index 00000000000..b57ce271f8a --- /dev/null +++ b/prusti/src/ide_helper/mod.rs @@ -0,0 +1,4 @@ +pub mod compiler_info; +pub mod fake_error; +mod call_finder; +mod query_signature; diff --git a/prusti/src/ide_helper/query_signature.rs b/prusti/src/ide_helper/query_signature.rs new file mode 100644 index 00000000000..bd392f41025 --- /dev/null +++ b/prusti/src/ide_helper/query_signature.rs @@ -0,0 +1,426 @@ +use prusti_common::config; +use std::{collections::HashMap, fmt}; + +use super::compiler_info::ProcDef; +use prusti_rustc_interface::{ + hir::{def::DefKind, def_id::DefId}, + middle::ty::{self, Clause, DefIdTree, ImplSubject, PredicateKind, TyCtxt}, +}; + +/// Data structure used to generate an external specification template. +/// The main purpose of this struct is to strictly split the collection +/// of all this information from the displaying afterwards. +/// Allows users in prusti-assistant to query such a template for function calls. +#[derive(Debug)] +enum ExternSpecBlock { + StandaloneFn { + parent_chain: String, + function_sig: FunctionSignature, + }, + Trait { + name: String, + path: String, + generics: Vec, + bounds: HashMap>, + function_sig: FunctionSignature, + }, + Impl { + name: String, // in this case the name also includes + // the path + trait_name: Option, + generics: Vec, + bounds: HashMap>, + function_sig: FunctionSignature, + }, +} + +impl ExternSpecBlock { + fn from_defid(tcx: TyCtxt<'_>, defid: DefId) -> Option { + let def_kind = tcx.opt_def_kind(defid)?; + let signature = FunctionSignature::from_defid(tcx, defid)?; + match def_kind { + DefKind::Fn => { + let parent_chain = get_parent_chain(defid, tcx); + Some(ExternSpecBlock::StandaloneFn { + parent_chain, + function_sig: signature, + }) + } + DefKind::AssocFn => { + // this will be None for traits + match tcx.impl_of_method(defid) { + Some(impl_defid) => { + // function is part of impl block + let mut trait_name = None; + let impl_subj = tcx.impl_subject(impl_defid); + let self_ty = match impl_subj { + ImplSubject::Trait(tref) => { + trait_name = Some(format!("{}", tref.print_only_trait_name())); + tref.self_ty() + } + ImplSubject::Inherent(ty) => ty, + } + .to_string(); + let generics = generic_params(tcx, impl_defid); + let bounds = trait_bounds(tcx, impl_defid); + + Some(ExternSpecBlock::Impl { + name: self_ty, + trait_name, + generics, + bounds, + function_sig: signature, + }) + } + None => { + // function is a Trait (or something else?) + // are there other cases for AssocFns? + let parent = tcx.opt_parent(defid)?; + if tcx.is_trait(parent) { + // indeed a trait + let traitname = tcx.opt_item_name(parent)?.to_string(); + let parent_defpath = get_parent_chain(parent, tcx); + let trait_params = generic_params(tcx, parent); + let bounds = trait_bounds(tcx, parent); + + Some(ExternSpecBlock::Trait { + name: traitname, + path: parent_defpath, + generics: trait_params, + bounds, + function_sig: signature, + }) + } else { + None + } + } + } + } + _ => { + // another case to be handled? + None + } + } + } +} + +impl fmt::Display for ExternSpecBlock { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + ExternSpecBlock::Impl { + name, + trait_name, + generics, + bounds, + function_sig, + } => { + let generics_str = generic_args_str(generics, false); + let where_block = bounds_where_block(bounds); + + write!(f, "#[extern_spec]\nimpl{generics_str} ")?; + if let Some(trait_name) = trait_name { + write!(f, "{trait_name} for ")?; + } + writeln!(f, "{name}{where_block}\n{{")?; + let fn_sig = indent(&function_sig.to_string()); + write!(f, "{fn_sig}\n}}") + } + ExternSpecBlock::Trait { + name, + path, + generics, + bounds, + function_sig, + } => { + let fn_sig = indent(&function_sig.to_string()); + let generics_str = generic_args_str(generics, false); + let where_block = bounds_where_block(bounds); + // do traits specify traitbounds too? + writeln!(f, "#[extern_spec({path})]")?; + writeln!(f, "trait {name}{generics_str}{where_block}\n{{")?; + writeln!(f, "{fn_sig}\n}}") + } + ExternSpecBlock::StandaloneFn { + parent_chain, + function_sig, + } => { + writeln!(f, "#[extern_spec({parent_chain})]")?; + write!(f, "{function_sig}") + } + } + } +} + +#[derive(Debug, Clone)] +struct GenericArg { + name: String, + _default_value: Option, +} + +impl fmt::Display for GenericArg { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + write!(f, "{}", self.name) + // Trait bounds will always be in where blocks since this + // complicates things a lot otherwise. + // for now we ignore defaults since prusti doesnt accept them in + // some cases.. + // if self.default_value.is_some() { + // write!(f, "={}", self.default_value.as_ref().unwrap())?; + // } + } +} + +/// the string for the where clause. Given a list of genericArgs, this would +/// generate a string of the form: +/// ``` +/// where +/// T: bound1 + bound2, +/// S: anotherbound, +/// ``` +fn bounds_where_block(traitbounds: &HashMap>) -> String { + let bounds_vec = traitbounds + .iter() + .map(|(arg, bounds)| format!("\t{}: {}", arg, traitbounds_string(bounds))) + .collect::>(); + if !bounds_vec.is_empty() { + format!("\nwhere\n{}", bounds_vec.join(",\n")) + } else { + "".to_string() + } +} + +/// If a function or impl block has a list of generic arguments, this +/// will generate the string for it such as . +fn generic_args_str(arglist: &Vec, include_bounds: bool) -> String { + if !arglist.is_empty() { + let res = arglist + .iter() + .map(|genarg| { + if include_bounds { + genarg.to_string() + } else { + genarg.name.clone() + } + }) + .collect::>() + .join(", "); + format!("<{res}>") + } else { + "".to_string() + } +} + +/// example result: Sized + PartialEq + Eq +fn traitbounds_string(boundlist: &Vec) -> String { + if !boundlist.is_empty() { + let res = boundlist + .iter() + .map(|bound| bound.to_string()) + .collect::>() + .join(" + "); + res + } else { + "".to_string() + } +} + +#[derive(Debug, Clone)] +struct TraitBound { + name: String, + args: Vec, +} + +impl fmt::Display for TraitBound { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + write!(f, "{}", self.name)?; + if !self.args.is_empty() { + let args_str = self.args.join(", "); + write!(f, "<{args_str}>")?; + } + Ok(()) + } +} + +#[derive(Debug)] +struct FunctionSignature { + name: String, + generics: Vec, + bounds: HashMap>, + arguments: Vec<(String, String)>, // (name, type) + return_type: Option, +} + +impl FunctionSignature { + fn from_defid(tcx: TyCtxt<'_>, defid: DefId) -> Option { + let name = tcx.opt_item_name(defid)?.to_string(); + let sig = tcx.fn_sig(defid).skip_binder(); + let arg_types = sig.inputs().iter(); + let arg_names = tcx.fn_arg_names(defid); + let output = sig.output().skip_binder(); + let return_type = if output.is_unit() { + None + } else { + Some(output.to_string()) + }; + + let arguments: Vec<(String, String)> = arg_names + .iter() + .zip(arg_types) + .map(|(name, ty)| (name.to_string(), ty.skip_binder().to_string())) + .collect(); + + let generics = generic_params(tcx, defid); + let bounds = trait_bounds(tcx, defid); + Some(Self { + name, + generics, + bounds, + arguments, + return_type, + }) + } + + fn arguments_string(&self) -> String { + let args = self + .arguments + .iter() + .map(|(name, ty)| format!("{name}: {ty}")) + .collect::>() + .join(", "); + format!("({args})") + } +} + +impl fmt::Display for FunctionSignature { + // fn(args) -> output where + // bounds; + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + let generics_str = generic_args_str(&self.generics, false); + let where_block = bounds_where_block(&self.bounds); + let args_str = self.arguments_string(); + + write!(f, "fn {}{}{}", self.name, generics_str, args_str)?; + if let Some(ret_ty) = self.return_type.clone() { + write!(f, " -> {ret_ty}")?; + } + write!(f, "{where_block};") + } +} + +fn generic_params(tcx: TyCtxt<'_>, defid: DefId) -> Vec { + let generics = tcx.generics_of(defid); + let substs = ty::subst::InternalSubsts::identity_for_item(tcx, defid); + + generics + .params + .iter() + .filter_map(|param| { + let ident = param.name.to_string(); + if ident == "Self" { + None + } else { + let default_value = param + .default_value(tcx) + .map(|val| val.subst(tcx, substs).to_string()); + Some(GenericArg { + name: ident, + _default_value: default_value, + }) + } + }) + .collect() +} + +fn trait_bounds(tcx: TyCtxt<'_>, defid: DefId) -> HashMap> { + let mut traitbounds: HashMap> = HashMap::new(); + let predicates = tcx.predicates_of(defid); + + for (predicate, _) in predicates.predicates { + let kind: PredicateKind = predicate.kind().skip_binder(); + match kind { + PredicateKind::Clause(Clause::Trait(t)) => { + let bound_traitref = t.trait_ref; + let trait_name = tcx.def_path_str(bound_traitref.def_id); + let self_ty = format!("{}", bound_traitref.self_ty()); + if self_ty == "Self" { + continue; + } + let trait_args_opt = bound_traitref.substs.try_as_type_list(); + let trait_args = if let Some(typelist) = trait_args_opt { + typelist + .iter() + .skip(1) // the first one is the self type + .map(|ty| format!("{ty}")) + .collect::>() + } else { + vec![] + }; + let bound = TraitBound { + name: trait_name, + args: trait_args, + }; + // add this bound to the given type. + if let Some(bounds) = traitbounds.get_mut(&self_ty) { + bounds.push(bound); + } else { + traitbounds.insert(self_ty, vec![bound]); + } + } + PredicateKind::Clause(Clause::Projection(p)) => { + let item_id = p.projection_ty.def_id; + let self_ty = format!("{}", p.projection_ty.self_ty()); + let trait_defid: DefId = p.projection_ty.trait_def_id(tcx); + let trait_defpath = tcx.def_path_str(trait_defid); + + let item_name = tcx.item_name(item_id).to_string(); + + let projection_term = format!("{}={}", item_name, p.term); + let bounds = traitbounds.get_mut(&self_ty).unwrap(); + let mut last_bound = bounds.pop().unwrap(); + if last_bound.name == trait_defpath { + last_bound.args.push(projection_term); + } + bounds.push(last_bound); + } + _ => {} + } + } + traitbounds +} + +pub fn collect_queried_signature(tcx: TyCtxt<'_>, fncalls: &[ProcDef]) -> Option { + let def_path_str: String = config::query_method_signature()?; + let existing = fncalls + .iter() + .find(|procdef| procdef.name == def_path_str)?; + + // helpers: + let defid: DefId = existing.defid; + let extern_spec_block = ExternSpecBlock::from_defid(tcx, defid); + extern_spec_block.map(|x| x.to_string()) +} + +fn get_parent_chain(defid: DefId, tcx: TyCtxt<'_>) -> String { + // let mut parent_opt = tcx.opt_parent(defid); + // this (above) apparently doesn't work. E.g. for std::ops::Add + // it will return std::ops::arith which is problematic + let defpath_str = tcx.def_path_str(defid); + let mut defpath: Vec<&str> = defpath_str.split("::").collect(); + defpath.pop(); // drop the name itself + defpath.join("::") +} + +/// indent all lines that are not empty by one tab +fn indent(input: &String) -> String { + let mut res = String::from("\t"); + let len = input.len(); + for (i, c) in input.chars().enumerate() { + res.push(c); + if c == '\n' && i != len - 1 { + // insert a tab after every newline that is not terminating + // the string + res.push('\t'); + } + } + res +} diff --git a/prusti/src/verifier.rs b/prusti/src/verifier.rs index 74775f0d628..36427748c03 100644 --- a/prusti/src/verifier.rs +++ b/prusti/src/verifier.rs @@ -10,18 +10,15 @@ use prusti_interface::{ use prusti_viper::verifier::Verifier; #[tracing::instrument(name = "prusti::verify", level = "debug", skip(env))] -pub fn verify(env: Environment<'_>, def_spec: typed::DefSpecificationMap) { +pub fn verify<'tcx>( + env: &Environment<'tcx>, + def_spec: typed::DefSpecificationMap, + verification_task: VerificationTask<'tcx>, +) { if env.diagnostic.has_errors() { warn!("The compiler reported an error, so the program will not be verified."); } else { debug!("Prepare verification task..."); - // TODO: can we replace `get_annotated_procedures` with information - // that is already in `def_spec`? - let (annotated_procedures, types) = env.get_annotated_procedures_and_types(); - let verification_task = VerificationTask { - procedures: annotated_procedures, - types, - }; debug!("Verification task: {:?}", &verification_task); user::message(format!( @@ -50,7 +47,7 @@ pub fn verify(env: Environment<'_>, def_spec: typed::DefSpecificationMap) { debug!("Dump borrow checker info..."); env.dump_borrowck_info(&verification_task.procedures); - let mut verifier = Verifier::new(&env, def_spec); + let mut verifier = Verifier::new(env, def_spec); let verification_result = verifier.verify(&verification_task); debug!("Verifier returned {:?}", verification_result); diff --git a/viper-sys/build.rs b/viper-sys/build.rs index 98423e0b9cc..ede1655911d 100644 --- a/viper-sys/build.rs +++ b/viper-sys/build.rs @@ -90,7 +90,7 @@ fn main() { method!("wrapRefArray"), ]), java_class!("scala.math.BigInt", vec![ - constructor!(), + constructor!("(Ljava/math/BigInteger;)V"), ]), java_class!("scala.collection.mutable.ArrayBuffer", vec![ constructor!("(I)V"), @@ -143,6 +143,19 @@ fn main() { java_class!("viper.silver.reporter.NoopReporter$", vec![ object_getter!(), ]), + java_class!("viper.silver.reporter.PollingReporter", vec![ + constructor!("(Ljava/lang/String;Lviper/silver/reporter/Reporter;)V"), + method!("hasNewMessage"), + method!("getNewMessage"), + ]), + java_class!("viper.silver.reporter.QuantifierChosenTriggersMessage", vec![ + method!("quantifier"), + method!("triggers_string"), + ]), + java_class!("viper.silver.reporter.QuantifierInstantiationsMessage", vec![ + method!("quantifier"), + method!("instantiations"), + ]), java_class!("viper.silver.verifier.Verifier", vec![ method!("name"), method!("buildVersion"), @@ -150,6 +163,7 @@ fn main() { method!("start"), method!("stop"), method!("verify"), + method!("reporter"), ]), java_class!("viper.silver.ast.pretty.FastPrettyPrinter$", vec![ object_getter!(), diff --git a/viper-toolchain b/viper-toolchain index 0391f0ffe80..1f4a874cf2d 100644 --- a/viper-toolchain +++ b/viper-toolchain @@ -1 +1 @@ -v-2023-01-31-0912 +v-2023-03-02-1938 diff --git a/viper/src/ast_factory/expression.rs b/viper/src/ast_factory/expression.rs index 1c34c15f89f..eb34cecdfd6 100644 --- a/viper/src/ast_factory/expression.rs +++ b/viper/src/ast_factory/expression.rs @@ -1196,7 +1196,7 @@ impl<'a> AstFactory<'a> { variables: &[LocalVarDecl], triggers: &[Trigger], expr: Expr, - _pos: Position, // FIXME: Why??? + pos: Position, ) -> Expr<'a> { build_ast_node_with_pos!( self, @@ -1205,7 +1205,7 @@ impl<'a> AstFactory<'a> { self.jni.new_seq(&map_to_jobjects!(variables)), self.jni.new_seq(&map_to_jobjects!(triggers)), expr.to_jobject(), - self.no_position().to_jobject() + pos.to_jobject() ) } diff --git a/viper/src/lib.rs b/viper/src/lib.rs index 747f7fc1261..97d0a524634 100644 --- a/viper/src/lib.rs +++ b/viper/src/lib.rs @@ -10,11 +10,11 @@ mod ast_factory; mod ast_utils; pub mod errors; -mod jni_utils; +pub mod jni_utils; #[macro_use] pub mod utils; mod cache; -mod java_exception; +pub mod java_exception; pub mod silicon_counterexample; pub mod smt_manager; mod verification_backend; diff --git a/viper/src/verification_context.rs b/viper/src/verification_context.rs index 2537431c837..09d44ac535a 100644 --- a/viper/src/verification_context.rs +++ b/viper/src/verification_context.rs @@ -25,6 +25,10 @@ impl<'a> VerificationContext<'a> { VerificationContext { env: env_guard } } + pub fn env(&self) -> &AttachGuard<'a> { + &self.env + } + pub fn new_ast_factory(&self) -> AstFactory { AstFactory::new(&self.env) } diff --git a/viper/src/verification_result.rs b/viper/src/verification_result.rs index 4bf847217df..3d9087f971c 100644 --- a/viper/src/verification_result.rs +++ b/viper/src/verification_result.rs @@ -6,9 +6,31 @@ use crate::{silicon_counterexample::SiliconCounterexample, JavaException}; +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +pub struct VerificationResult { + pub item_name: String, + pub kind: VerificationResultKind, + pub cached: bool, + pub time_ms: u128, +} + +impl VerificationResult { + pub fn is_success(&self) -> bool { + self.kind.is_success() + } + + pub fn dummy_success() -> Self { + VerificationResult { + item_name: "".to_string(), + kind: VerificationResultKind::Success, + cached: false, + time_ms: 0, + } + } +} /// The result of a verification request on a Viper program. #[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] -pub enum VerificationResult { +pub enum VerificationResultKind { /// The program verified. Success, /// The program did not verify. @@ -19,7 +41,7 @@ pub enum VerificationResult { JavaException(JavaException), } -impl VerificationResult { +impl VerificationResultKind { pub fn is_success(&self) -> bool { matches!(self, Self::Success) } diff --git a/viper/src/verifier.rs b/viper/src/verifier.rs index 14ab105bea9..ba677c96bfa 100644 --- a/viper/src/verifier.rs +++ b/viper/src/verifier.rs @@ -11,7 +11,7 @@ use crate::{ silicon_counterexample::SiliconCounterexample, smt_manager::SmtManager, verification_backend::VerificationBackend, - verification_result::{VerificationError, VerificationResult}, + verification_result::{VerificationError, VerificationResultKind}, }; use jni::{errors::Result, objects::JObject, JNIEnv}; use log::{debug, error, info}; @@ -38,7 +38,7 @@ impl<'a> Verifier<'a> { let ast_utils = AstUtils::new(env); let verifier_wrapper = silver::verifier::Verifier::with(env); let verifier_instance = jni.unwrap_result(env.with_local_frame(16, || { - let reporter = if let Some(real_report_path) = report_path { + let pass_through_reporter = if let Some(real_report_path) = report_path { jni.unwrap_result(silver::reporter::CSVReporter::with(env).new( jni.new_string("csv_reporter"), jni.new_string(real_report_path.to_str().unwrap()), @@ -47,6 +47,11 @@ impl<'a> Verifier<'a> { jni.unwrap_result(silver::reporter::NoopReporter_object::with(env).singleton()) }; + let reporter = jni.unwrap_result( + silver::reporter::PollingReporter::with(env) + .new(jni.new_string("polling_reporter"), pass_through_reporter), + ); + let debug_info = jni.new_seq(&[]); Self::instantiate_verifier(backend, env, reporter, debug_info) })); @@ -114,7 +119,7 @@ impl<'a> Verifier<'a> { } #[tracing::instrument(name = "viper::verify", level = "debug", skip_all)] - pub fn verify(&mut self, program: Program) -> VerificationResult { + pub fn verify(&mut self, program: Program) -> VerificationResultKind { let ast_utils = self.ast_utils; ast_utils.with_local_frame(16, || { debug!( @@ -126,7 +131,7 @@ impl<'a> Verifier<'a> { let consistency_errors = match self.ast_utils.check_consistency(program) { Ok(errors) => errors, Err(java_exception) => { - return VerificationResult::JavaException(java_exception); + return VerificationResultKind::JavaException(java_exception); } }; ); @@ -136,7 +141,7 @@ impl<'a> Verifier<'a> { "The provided Viper program has {} consistency errors.", consistency_errors.len() ); - return VerificationResult::ConsistencyErrors( + return VerificationResultKind::ConsistencyErrors( consistency_errors .into_iter() .map(|e| self.jni.to_string(e)) @@ -338,13 +343,17 @@ impl<'a> Verifier<'a> { )) } - VerificationResult::Failure(errors) + VerificationResultKind::Failure(errors) } else { - VerificationResult::Success + VerificationResultKind::Success } }) } + pub fn verifier_instance(&self) -> &JObject<'a> { + &self.verifier_instance + } + #[tracing::instrument(level = "debug", skip_all)] fn call_verify(&self, program: Program) -> Result> { self.verifier_wrapper diff --git a/viper/tests/invalid_programs.rs b/viper/tests/invalid_programs.rs index 13fb3caa2ad..d2d401fe9f8 100644 --- a/viper/tests/invalid_programs.rs +++ b/viper/tests/invalid_programs.rs @@ -32,7 +32,7 @@ fn runtime_error() { assert!(matches!( verification_result, - VerificationResult::JavaException(_) + VerificationResultKind::JavaException(_) )); } @@ -99,7 +99,7 @@ where let verification_result = verifier.verify(program); match verification_result { - VerificationResult::ConsistencyErrors(_) => (), + VerificationResultKind::ConsistencyErrors(_) => (), other => panic!("consistency errors not identified, instead found {other:?}"), } } diff --git a/viper/tests/simple_programs.rs b/viper/tests/simple_programs.rs index 798f284c63a..2f491f9bdfa 100644 --- a/viper/tests/simple_programs.rs +++ b/viper/tests/simple_programs.rs @@ -56,7 +56,7 @@ fn failure_with_assert_false() { let verification_result = verifier.verify(program); - if let VerificationResult::Failure(errors) = verification_result { + if let VerificationResultKind::Failure(errors) = verification_result { assert_eq!(errors.len(), 1); assert_eq!( errors[0].full_id, @@ -204,7 +204,7 @@ fn failure_with_assign_if_and_assert() { let verification_result = verifier.verify(program); - if let VerificationResult::Failure(errors) = verification_result { + if let VerificationResultKind::Failure(errors) = verification_result { assert_eq!(errors.len(), 1); assert_eq!( errors[0].full_id, diff --git a/vir/defs/polymorphic/ast/expr.rs b/vir/defs/polymorphic/ast/expr.rs index 12e3183dfaf..1012a216621 100644 --- a/vir/defs/polymorphic/ast/expr.rs +++ b/vir/defs/polymorphic/ast/expr.rs @@ -352,6 +352,24 @@ impl Expr { }) } + pub fn forall_with_pos( + vars: Vec, + triggers: Vec, + body: Expr, + pos: Position, + ) -> Self { + assert!( + !vars.is_empty(), + "A quantifier must have at least one variable." + ); + Expr::ForAll(ForAll { + variables: vars, + triggers, + body: Box::new(body), + position: pos, + }) + } + pub fn exists(vars: Vec, triggers: Vec, body: Expr) -> Self { assert!( !vars.is_empty(), @@ -365,6 +383,24 @@ impl Expr { }) } + pub fn exists_with_pos( + vars: Vec, + triggers: Vec, + body: Expr, + pos: Position, + ) -> Self { + assert!( + !vars.is_empty(), + "A quantifier must have at least one variable." + ); + Expr::Exists(Exists { + variables: vars, + triggers, + body: Box::new(body), + position: pos, + }) + } + pub fn ite(guard: Expr, left: Expr, right: Expr) -> Self { Expr::Cond(Cond { guard: Box::new(guard),