diff --git a/CHANGELOG.md b/CHANGELOG.md index 3835d15177dd..2f2805277846 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,6 +4,52 @@ This file contains notable changes (e.g. breaking changes, major changes, etc.) This file was introduced starting Kani 0.23.0, so it only contains changes from version 0.23.0 onwards. +## [0.57.0] + +### Major Changes +* `kani-cov`: A coverage tool for Kani by @adpaco-aws in https://github.com/model-checking/kani/pull/3121 +* Add a timeout option by @zhassan-aws in https://github.com/model-checking/kani/pull/3649 +* Loop Contracts Annotation for While-Loop by @qinheping in https://github.com/model-checking/kani/pull/3151 +* Harness output individual files by @Alexander-Aghili in https://github.com/model-checking/kani/pull/3360 +* Enable support for Ubuntu 24.04 by @tautschnig in https://github.com/model-checking/kani/pull/3758 + +### Breaking Changes +* Make `kani::check` private by @celinval in https://github.com/model-checking/kani/pull/3614 +* Remove symtab json support by @celinval in https://github.com/model-checking/kani/pull/3695 +* Remove CBMC viewer and visualize option by @zhassan-aws in https://github.com/model-checking/kani/pull/3699 +* Dropping support for Ubuntu 18.04 / AL2. by @thanhnguyen-aws in https://github.com/model-checking/kani/pull/3744 + +### What's Changed +* Remove the overflow checks for wrapping_offset by @zhassan-aws in https://github.com/model-checking/kani/pull/3589 +* Support fully-qualified --package arguments by @celinval in https://github.com/model-checking/kani/pull/3593 +* Implement proper function pointer handling for validity checks by @celinval in https://github.com/model-checking/kani/pull/3606 +* Add fn that checks pointers point to same allocation by @celinval in https://github.com/model-checking/kani/pull/3583 +* [Lean back-end] Preserve variable names by @zhassan-aws in https://github.com/model-checking/kani/pull/3560 +* Emit an error when proof_for_contract function is not found by @zhassan-aws in https://github.com/model-checking/kani/pull/3609 +* [Lean back-end] Rename user-facing options from Aeneas to Lean by @zhassan-aws in https://github.com/model-checking/kani/pull/3630 +* Fix ICE due to mishandling of Aggregate rvalue for raw pointers to trait objects by @carolynzech in https://github.com/model-checking/kani/pull/3636 +* Fix loop contracts transformation when loops in branching by @qinheping in https://github.com/model-checking/kani/pull/3640 +* Move any_slice_from_array to kani_core by @qinheping in https://github.com/model-checking/kani/pull/3646 +* Implement `Arbitrary` for `Range*` by @c410-f3r in https://github.com/model-checking/kani/pull/3666 +* Add support for float_to_int_unchecked by @zhassan-aws in https://github.com/model-checking/kani/pull/3660 +* Change `same_allocation` to accept wide pointers by @celinval in https://github.com/model-checking/kani/pull/3684 +* Derive `Arbitrary` for enums with a single variant by @AlgebraicWolf in https://github.com/model-checking/kani/pull/3692 +* Apply loop contracts only if there exists some usage by @qinheping in https://github.com/model-checking/kani/pull/3694 +* Add support for f16 and f128 in float_to_int_unchecked intrinsic by @zhassan-aws in https://github.com/model-checking/kani/pull/3701 +* Fix codegen for rvalue aggregate raw pointer to an adt with slice tail by @carolynzech in https://github.com/model-checking/kani/pull/3644 +* Improve Kani handling of function markers by @celinval in https://github.com/model-checking/kani/pull/3718 +* Enable contracts for const generic functions by @qinheping in https://github.com/model-checking/kani/pull/3726 +* List Subcommand Improvements by @carolynzech in https://github.com/model-checking/kani/pull/3729 +* [Lean back-end] add support for enum, struct, tuple in llbc backend by @thanhnguyen-aws in https://github.com/model-checking/kani/pull/3721 +* Fix issues with how we compute DST size by @celinval in https://github.com/model-checking/kani/pull/3687 +* Fix size and alignment computation for intrinsics by @celinval in https://github.com/model-checking/kani/pull/3734 +* Add a Kani function that checks if the range of a float is valid for conversion to int by @zhassan-aws in https://github.com/model-checking/kani/pull/3742 +* Add out of bounds check for `offset` intrinsics by @celinval in https://github.com/model-checking/kani/pull/3755 +* Automatic upgrade of CBMC from 6.3.1 to 6.4.1 +* Rust toolchain upgraded to nightly-2024-12-15 by @zhassan-aws @carolynzech @qinheping @celinval @tautschnig + +**Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.56.0...kani-0.57.0 + ## [0.56.0] ### Major/Breaking Changes diff --git a/Cargo.lock b/Cargo.lock index 7931066348b7..45a46da09280 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -39,6 +39,16 @@ dependencies = [ "memchr", ] +[[package]] +name = "annotate-snippets" +version = "0.11.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "710e8eae58854cdc1790fcb56cca04d712a17be849eeb81da2a724bf4bae2bc4" +dependencies = [ + "anstyle", + "unicode-width 0.2.0", +] + [[package]] name = "anstream" version = "0.6.18" @@ -90,15 +100,9 @@ dependencies = [ [[package]] name = "anyhow" -version = "1.0.94" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c1fd03a028ef38ba2276dce7e33fcd6369c158a1bca17946c4b1b701891c1ff7" - -[[package]] -name = "arrayvec" -version = "0.5.2" +version = "1.0.95" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "23b62fc65de8e4e7f52534fb52b0f3ed04746ae267519eef2a83941e8085068b" +checksum = "34ac096ce696dc2fcabef30516bb13c0a68a11d30131d3df6f04711467681b04" [[package]] name = "arrayvec" @@ -140,7 +144,7 @@ dependencies = [ "miniz_oxide", "object", "rustc-demangle", - "windows-targets 0.52.6", + "windows-targets", ] [[package]] @@ -155,14 +159,14 @@ version = "3.0.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "c5839ee4f953e811bfdcf223f509cb2c6a3e1447959b0bff459405575bc17f22" dependencies = [ - "arrayvec 0.7.6", + "arrayvec", ] [[package]] name = "bstr" -version = "1.11.0" +version = "1.11.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1a68f1f47cdf0ec8ee4b941b2eee2a80cb796db73118c0dd09ac63fbe405be22" +checksum = "531a9155a481e2ee699d4f98f43c0ca4ff8ee1bfd55c31e9e98fb29d2b176fe0" dependencies = [ "memchr", "regex-automata 0.4.9", @@ -171,7 +175,7 @@ dependencies = [ [[package]] name = "build-kani" -version = "0.56.0" +version = "0.57.0" dependencies = [ "anyhow", "cargo_metadata", @@ -211,23 +215,23 @@ dependencies = [ [[package]] name = "cargo_metadata" -version = "0.18.1" +version = "0.19.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2d886547e41f740c616ae73108f6eb70afe6d940c7bc697cb30f13daec073037" +checksum = "8769706aad5d996120af43197bf46ef6ad0fda35216b4505f926a365a232d924" dependencies = [ "camino", "cargo-platform", "semver", "serde", "serde_json", - "thiserror", + "thiserror 2.0.9", ] [[package]] name = "cc" -version = "1.2.3" +version = "1.2.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "27f657647bcff5394bf56c7317665bbf790a137a50eaaa5c6bfbb9e27a518f2d" +checksum = "a012a0df96dd6d06ba9a1b29d6402d1a5d77c6befd2566afdc26e10603dc93d7" dependencies = [ "shlex", ] @@ -240,28 +244,27 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" [[package]] name = "charon" -version = "0.1.45" +version = "0.1.58" dependencies = [ + "annotate-snippets", + "anstream", "anyhow", "assert_cmd", "clap", "colored", - "convert_case 0.6.0", - "derive-visitor", + "convert_case", + "derive_generic_visitor", "env_logger", "hashlink", "index_vec", "indoc", - "itertools 0.13.0", + "itertools", "lazy_static", "log", "macros", "nom", "nom-supreme", "petgraph", - "pretty", - "regex", - "rustc_apfloat", "rustc_version", "serde", "serde-map-to-array", @@ -307,7 +310,7 @@ dependencies = [ "heck", "proc-macro2", "quote", - "syn 2.0.90", + "syn", ] [[package]] @@ -324,12 +327,12 @@ checksum = "5b63caa9aa9397e2d9480a9b13673856c78d8ac123288526c37d7839f2a86990" [[package]] name = "colored" -version = "2.1.0" +version = "2.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "cbf2150cce219b664a8a70df7a1f933836724b503f8a413af9365b4dcc4d90b8" +checksum = "117725a109d387c937a1533ce01b450cbde6b88abceea8473c4d7a85853cda3c" dependencies = [ "lazy_static", - "windows-sys 0.48.0", + "windows-sys 0.59.0", ] [[package]] @@ -372,23 +375,17 @@ dependencies = [ [[package]] name = "console" -version = "0.15.8" +version = "0.15.10" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0e1f83fc076bd6dd27517eacdf25fef6c4dfe5f1d7448bafaaf3a26f13b5e4eb" +checksum = "ea3c6ecd8059b57859df5c69830340ed3c41d30e3da0c1cbed90a96ac853041b" dependencies = [ "encode_unicode", - "lazy_static", "libc", - "unicode-width 0.1.14", - "windows-sys 0.52.0", + "once_cell", + "unicode-width 0.2.0", + "windows-sys 0.59.0", ] -[[package]] -name = "convert_case" -version = "0.4.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6245d59a3e82a7fc217c5828a6692dbc6dfb63a0c8c90495621f7b9d79704a0e" - [[package]] name = "convert_case" version = "0.6.0" @@ -400,7 +397,7 @@ dependencies = [ [[package]] name = "cprover_bindings" -version = "0.56.0" +version = "0.57.0" dependencies = [ "lazy_static", "linear-map", @@ -415,9 +412,9 @@ dependencies = [ [[package]] name = "crossbeam-deque" -version = "0.8.5" +version = "0.8.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "613f8cc01fe9cf1a3eb3d7f488fd2fa8388403e97039e2f73692932e291a770d" +checksum = "9dd111b7b7f7d55b72c0a6ae361660ee5853c9af73f70c3c2ef6858b950e2e51" dependencies = [ "crossbeam-epoch", "crossbeam-utils", @@ -434,9 +431,9 @@ dependencies = [ [[package]] name = "crossbeam-utils" -version = "0.8.20" +version = "0.8.21" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "22ec99545bb0ed0ea7bb9b8e1e9122ea386ff8a48c0922e43f36d45ab09e0e80" +checksum = "d0a5c400df2834b80a4c3327b3aad3a4c4cd4de0629063962b03235697506a28" [[package]] name = "crossterm" @@ -481,6 +478,41 @@ dependencies = [ "memchr", ] +[[package]] +name = "darling" +version = "0.20.10" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6f63b86c8a8826a49b8c21f08a2d07338eec8d900540f8630dc76284be802989" +dependencies = [ + "darling_core", + "darling_macro", +] + +[[package]] +name = "darling_core" +version = "0.20.10" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "95133861a8032aaea082871032f5815eb9e98cef03fa916ab4500513994df9e5" +dependencies = [ + "fnv", + "ident_case", + "proc-macro2", + "quote", + "strsim", + "syn", +] + +[[package]] +name = "darling_macro" +version = "0.20.10" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d336a2a514f6ccccaa3e09b02d41d35330c07ddf03a62165fcec10bb561c7806" +dependencies = [ + "darling_core", + "quote", + "syn", +] + [[package]] name = "deranged" version = "0.3.11" @@ -491,25 +523,26 @@ dependencies = [ ] [[package]] -name = "derive-visitor" -version = "0.4.0" +name = "derive_generic_visitor" +version = "0.1.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d47165df83b9707cbada3216607a5d66125b6a66906de0bc1216c0669767ca9e" +checksum = "b3e1c241e4f464b614bd7650f1a7c4c0e20e5ef21564d6b916b4c51fd76f7688" dependencies = [ - "derive-visitor-macros", + "derive_generic_visitor_macros", ] [[package]] -name = "derive-visitor-macros" -version = "0.4.0" +name = "derive_generic_visitor_macros" +version = "0.1.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "427b39a85fecafea16b1a5f3f50437151022e35eb4fe038107f08adbf7f8def6" +checksum = "885f5274163b5b1720591c0c24b34350a0b05e4774351f9fb3d13c192d8c995b" dependencies = [ - "convert_case 0.4.0", - "itertools 0.10.5", + "convert_case", + "darling", + "itertools", "proc-macro2", "quote", - "syn 1.0.109", + "syn", ] [[package]] @@ -532,25 +565,31 @@ checksum = "60b1af1c220855b6ceac025d3f6ecdd2b7c4894bfe9cd9bda4fbb4bc7c0d4cf0" [[package]] name = "encode_unicode" -version = "0.3.6" +version = "1.0.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a357d28ed41a50f9c765dbfe56cbc04a64e53e5fc58ba79fbc34c10ef3df831f" +checksum = "34aa73646ffb006b8f5147f3dc182bd4bcb190227ce861fc4a4844bf8e3cb2c0" [[package]] name = "env_filter" -version = "0.1.2" +version = "0.1.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4f2c92ceda6ceec50f43169f9ee8424fe2db276791afde7b2cd8bc084cb376ab" +checksum = "186e05a59d4c50738528153b83b0b0194d3a29507dfec16eccd4b342903397d0" dependencies = [ "log", "regex", ] +[[package]] +name = "env_home" +version = "0.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c7f84e12ccf0a7ddc17a6c41c93326024c42920d7ee630d04950e6926645c0fe" + [[package]] name = "env_logger" -version = "0.11.5" +version = "0.11.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e13fa619b91fb2381732789fc5de83b45675e882f66623b7d8cb4f643017018d" +checksum = "dcaee3d8e3cfc3fd92428d477bc97fc29ec8716d180c0d74c643bb26166660e0" dependencies = [ "anstream", "anstyle", @@ -587,6 +626,18 @@ version = "0.4.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0ce7134b9999ecaf8bcd65542e436736ef32ddca1b3e06094cb6ec5755203b80" +[[package]] +name = "fnv" +version = "1.0.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3f9eec918d3f24069decb9af1554cad7c880e2da24a9afd88aca000531ab82c1" + +[[package]] +name = "foldhash" +version = "0.1.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a0d2fde1f7b3d48b8395d5f2de76c18a528bd6a9cdde438df747bfcba3e05d6f" + [[package]] name = "getopts" version = "0.2.21" @@ -615,9 +666,9 @@ checksum = "07e28edb80900c19c28f1072f2e8aeca7fa06b23cd4169cefe1af5aa3260783f" [[package]] name = "glob" -version = "0.3.1" +version = "0.3.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d2fabcfbdc87f4758337ca535fb41a6d701b65693ce38287d856d1674551ec9b" +checksum = "a8d1add55171497b4705a648c6b583acafb01d58050a51727785f0b2c8e0a2b2" [[package]] name = "graph-cycles" @@ -627,7 +678,7 @@ checksum = "3a6ad932c6dd3cfaf16b66754a42f87bbeefd591530c4b6a8334270a7df3e853" dependencies = [ "ahash", "petgraph", - "thiserror", + "thiserror 1.0.69", ] [[package]] @@ -644,6 +695,9 @@ name = "hashbrown" version = "0.15.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "bf151400ff0baff5465007dd2f3e717f3fe502074ca563069ce3a6629d07b289" +dependencies = [ + "foldhash", +] [[package]] name = "hashlink" @@ -663,11 +717,11 @@ checksum = "2304e00983f87ffb38b55b444b5e3b60a884b5d30c0fca7d82fe33449bbe55ea" [[package]] name = "home" -version = "0.5.9" +version = "0.5.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e3d1354bf6b7235cb4a0576c2619fd4ed18183f689b12b006a0ee7329eeff9a5" +checksum = "589533453244b0995c858700322199b2becb13b627df2851f64a2775d024abcf" dependencies = [ - "windows-sys 0.52.0", + "windows-sys 0.59.0", ] [[package]] @@ -676,6 +730,12 @@ version = "2.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9a3a5bfb195931eeb336b2a7b4d761daec841b97f947d34394601737a7bba5e4" +[[package]] +name = "ident_case" +version = "1.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b9e0384b61958566e926dc50660321d12159025e767c18e043daf26b70104c39" + [[package]] name = "indent_write" version = "2.2.0" @@ -713,15 +773,6 @@ version = "1.70.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "7943c866cc5cd64cbc25b2e01621d07fa8eb2a1a23160ee81ce38704e97b8ecf" -[[package]] -name = "itertools" -version = "0.10.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b0fd2260e829bddf4cb6ea802289de2f86d6a7a690192fbe91b3f46e0f2c8473" -dependencies = [ - "either", -] - [[package]] name = "itertools" version = "0.13.0" @@ -745,7 +796,7 @@ checksum = "72167d68f5fce3b8655487b8038691a3c9984ee769590f93f2a631f4ad64e4f5" [[package]] name = "kani" -version = "0.56.0" +version = "0.57.0" dependencies = [ "kani_core", "kani_macros", @@ -753,13 +804,13 @@ dependencies = [ [[package]] name = "kani-compiler" -version = "0.56.0" +version = "0.57.0" dependencies = [ "charon", "clap", "cprover_bindings", "home", - "itertools 0.13.0", + "itertools", "kani_metadata", "lazy_static", "num", @@ -770,7 +821,7 @@ dependencies = [ "shell-words", "strum", "strum_macros", - "syn 2.0.90", + "syn", "tracing", "tracing-subscriber", "tracing-tree 0.4.0 (registry+https://github.com/rust-lang/crates.io-index)", @@ -792,7 +843,7 @@ dependencies = [ [[package]] name = "kani-driver" -version = "0.56.0" +version = "0.57.0" dependencies = [ "anyhow", "cargo_metadata", @@ -824,7 +875,7 @@ dependencies = [ [[package]] name = "kani-verifier" -version = "0.56.0" +version = "0.57.0" dependencies = [ "anyhow", "home", @@ -833,24 +884,24 @@ dependencies = [ [[package]] name = "kani_core" -version = "0.56.0" +version = "0.57.0" dependencies = [ "kani_macros", ] [[package]] name = "kani_macros" -version = "0.56.0" +version = "0.57.0" dependencies = [ "proc-macro-error2", "proc-macro2", "quote", - "syn 2.0.90", + "syn", ] [[package]] name = "kani_metadata" -version = "0.56.0" +version = "0.57.0" dependencies = [ "clap", "cprover_bindings", @@ -867,9 +918,9 @@ checksum = "bbd2bcb4c963f2ddae06a2efc7e9f3591312473c50c6685e1f298068316e66fe" [[package]] name = "libc" -version = "0.2.167" +version = "0.2.169" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "09d6582e104315a817dff97f75133544b2e094ee22447d2acf4a74e189ba06fc" +checksum = "b5aba8db14291edd000dfcc4d620c7ebfb122c613afb886ca8803fa4e128a20a" [[package]] name = "linear-map" @@ -909,7 +960,7 @@ version = "0.1.0" dependencies = [ "proc-macro2", "quote", - "syn 2.0.90", + "syn", ] [[package]] @@ -929,9 +980,9 @@ checksum = "78ca9ab1a0babb1e7d5695e3530886289c18cf2f87ec19a575a0abdce112e3a3" [[package]] name = "memuse" -version = "0.2.1" +version = "0.2.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2145869435ace5ea6ea3d35f59be559317ec9a0d04e1812d5f185a87b6d36f1a" +checksum = "3d97bbf43eb4f088f8ca469930cde17fa036207c9a5e02ccc5107c4e8b17c964" [[package]] name = "minimal-lexical" @@ -941,9 +992,9 @@ checksum = "68354c5c6bd36d73ff3feceb05efa59b6acb7626617f4962be322a825e61f79a" [[package]] name = "miniz_oxide" -version = "0.8.0" +version = "0.8.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e2d80299ef12ff69b16a84bb182e3b9df68b5a91574d3d4fa6e41b65deec4df1" +checksum = "4ffbe83022cedc1d264172192511ae958937694cd57ce297164951b8b3568394" dependencies = [ "adler2", ] @@ -1091,9 +1142,9 @@ dependencies = [ [[package]] name = "object" -version = "0.36.5" +version = "0.36.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "aedf0a2d09c573ed1d8d85b30c119153926a2b36dce0ab28322c09a117a4683e" +checksum = "62948e14d923ea95ea2c7c86c71013138b66525b86bdc08d2dcc262bdb497b87" dependencies = [ "memchr", ] @@ -1106,9 +1157,9 @@ checksum = "1261fe7e33c73b354eab43b1273a57c8f967d0391e80353e51f764ac02cf6775" [[package]] name = "os_info" -version = "3.9.0" +version = "3.9.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e5ca711d8b83edbb00b44d504503cd247c9c0bd8b0fa2694f2a1a3d8165379ce" +checksum = "6e6520c8cc998c5741ee68ec1dc369fc47e5f0ea5320018ecf2a1ccd6328f48b" dependencies = [ "log", "windows-sys 0.52.0", @@ -1140,7 +1191,7 @@ dependencies = [ "libc", "redox_syscall", "smallvec", - "windows-targets 0.52.6", + "windows-targets", ] [[package]] @@ -1182,9 +1233,9 @@ dependencies = [ [[package]] name = "predicates" -version = "3.1.2" +version = "3.1.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7e9086cc7640c29a356d1a29fd134380bee9d8f79a17410aa76e7ad295f42c97" +checksum = "a5d19ee57562043d37e82899fade9a22ebab7be9cef5026b07fda9cdd4293573" dependencies = [ "anstyle", "difflib", @@ -1193,31 +1244,20 @@ dependencies = [ [[package]] name = "predicates-core" -version = "1.0.8" +version = "1.0.9" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ae8177bee8e75d6846599c6b9ff679ed51e882816914eec639944d7c9aa11931" +checksum = "727e462b119fe9c93fd0eb1429a5f7647394014cf3c04ab2c0350eeb09095ffa" [[package]] name = "predicates-tree" -version = "1.0.11" +version = "1.0.12" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "41b740d195ed3166cd147c8047ec98db0e22ec019eb8eeb76d343b795304fb13" +checksum = "72dd2d6d381dfb73a193c7fca536518d7caee39fc8503f74e7dc0be0531b425c" dependencies = [ "predicates-core", "termtree", ] -[[package]] -name = "pretty" -version = "0.12.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b55c4d17d994b637e2f4daf6e5dc5d660d209d5642377d675d7a1c3ab69fa579" -dependencies = [ - "arrayvec 0.5.2", - "typed-arena", - "unicode-width 0.1.14", -] - [[package]] name = "proc-macro-error-attr2" version = "2.0.0" @@ -1237,7 +1277,7 @@ dependencies = [ "proc-macro-error-attr2", "proc-macro2", "quote", - "syn 2.0.90", + "syn", ] [[package]] @@ -1260,9 +1300,9 @@ dependencies = [ [[package]] name = "quote" -version = "1.0.37" +version = "1.0.38" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b5b9d34b8991d19d98081b46eacdd8eb58c6f2b201139f7c5f643cc155a633af" +checksum = "0e4dccaaaf89514f546c693ddc140f729f958c247918a13380cccc6078391acc" dependencies = [ "proc-macro2", ] @@ -1319,9 +1359,9 @@ dependencies = [ [[package]] name = "redox_syscall" -version = "0.5.7" +version = "0.5.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9b6dfecf2c74bce2466cabf93f6664d6998a69eb21e39f4207930065b27b771f" +checksum = "03a862b389f93e68874fbf580b9de08dd02facb9a788ebadaf4a3fd33cf58834" dependencies = [ "bitflags", ] @@ -1376,16 +1416,6 @@ version = "0.1.24" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "719b953e2095829ee67db738b3bfa9fa368c94900df327b3f07fe6e794d2fe1f" -[[package]] -name = "rustc_apfloat" -version = "0.2.2+llvm-462a31f5a5ab" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "121e2195ff969977a4e2b5c9965ea867fce7e4cb5aee5b09dee698a7932d574f" -dependencies = [ - "bitflags", - "smallvec", -] - [[package]] name = "rustc_version" version = "0.4.1" @@ -1410,9 +1440,9 @@ dependencies = [ [[package]] name = "rustversion" -version = "1.0.18" +version = "1.0.19" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0e819f2bc632f285be6d7cd36e25940d45b2391dd6d9b939e79de557f7014248" +checksum = "f7c45b9784283f1b2e7fb61b42047c2fd678ef0960d4f6f1eba131594cc369d4" [[package]] name = "ryu" @@ -1449,18 +1479,18 @@ checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49" [[package]] name = "semver" -version = "1.0.23" +version = "1.0.24" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "61697e0a1c7e512e84a621326239844a24d8207b4669b41bc18b32ea5cbf988b" +checksum = "3cb6eb87a131f756572d7fb904f6e7b68633f09cca868c5df1c4b8d1a694bbba" dependencies = [ "serde", ] [[package]] name = "serde" -version = "1.0.215" +version = "1.0.217" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6513c1ad0b11a9376da888e3e0baa0077f1aed55c17f50e7b2397136129fb88f" +checksum = "02fc4265df13d6fa1d00ecff087228cc0a2b5f3c0e87e258d8b94a156e984c70" dependencies = [ "serde_derive", ] @@ -1476,20 +1506,20 @@ dependencies = [ [[package]] name = "serde_derive" -version = "1.0.215" +version = "1.0.217" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ad1e866f866923f252f05c889987993144fb74e722403468a4ebd70c3cd756c0" +checksum = "5a9bf7cf98d04a2b28aead066b7496853d4779c9cc183c440dbac457641e19a0" dependencies = [ "proc-macro2", "quote", - "syn 2.0.90", + "syn", ] [[package]] name = "serde_json" -version = "1.0.133" +version = "1.0.134" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c7fceb2473b9166b2294ef05efcb65a3db80803f0b03ef86a5fc88a2b85ee377" +checksum = "d00f4175c42ee48b15416f6193a959ba3a0d67fc699a0db9ad12df9f83991c7d" dependencies = [ "indexmap", "itoa", @@ -1590,19 +1620,24 @@ dependencies = [ [[package]] name = "std" -version = "0.56.0" +version = "0.57.0" dependencies = [ "kani", ] +[[package]] +name = "streaming-iterator" +version = "0.1.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2b2231b7c3057d5e4ad0156fb3dc807d900806020c5ffa3ee6ff2c8c76fb8520" + [[package]] name = "string-interner" -version = "0.17.0" +version = "0.18.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1c6a0d765f5807e98a091107bae0a56ea3799f66a5de47b2c84c94a39c09974e" +checksum = "1a3275464d7a9f2d4cac57c89c2ef96a8524dba2864c8d6f82e3980baf136f9b" dependencies = [ - "cfg-if", - "hashbrown 0.14.5", + "hashbrown 0.15.2", "serde", ] @@ -1628,25 +1663,14 @@ dependencies = [ "proc-macro2", "quote", "rustversion", - "syn 2.0.90", -] - -[[package]] -name = "syn" -version = "1.0.109" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237" -dependencies = [ - "proc-macro2", - "quote", - "unicode-ident", + "syn", ] [[package]] name = "syn" -version = "2.0.90" +version = "2.0.95" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "919d3b74a5dd0ccd15aeb8f93e7006bd9e14c295087c9896a110f490752bcf31" +checksum = "46f71c0377baf4ef1cc3e3402ded576dccc315800fbc62dfc7fe04b009773b4a" dependencies = [ "proc-macro2", "quote", @@ -1661,12 +1685,13 @@ checksum = "f764005d11ee5f36500a149ace24e00e3da98b0158b3e2d53a7495660d3f4d60" [[package]] name = "tempfile" -version = "3.14.0" +version = "3.15.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "28cce251fcbc87fac86a866eeb0d6c2d536fc16d06f184bb61aeae11aa4cee0c" +checksum = "9a8a559c81686f576e8cd0290cd2a24a2a9ad80c98b3478856500fcbd7acd704" dependencies = [ "cfg-if", "fastrand", + "getrandom", "once_cell", "rustix", "windows-sys 0.59.0", @@ -1674,9 +1699,9 @@ dependencies = [ [[package]] name = "termtree" -version = "0.4.1" +version = "0.5.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3369f5ac52d5eb6ab48c6b4ffdc8efbcad6b89c765749064ba298f2c68a16a76" +checksum = "8f50febec83f5ee1df3015341d8bd429f2d1cc62bcba7ea2076759d315084683" [[package]] name = "thiserror" @@ -1684,7 +1709,16 @@ version = "1.0.69" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b6aaf5339b578ea85b50e080feb250a3e8ae8cfcdff9a461c9ec2904bc923f52" dependencies = [ - "thiserror-impl", + "thiserror-impl 1.0.69", +] + +[[package]] +name = "thiserror" +version = "2.0.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f072643fd0190df67a8bab670c20ef5d8737177d6ac6b2e9a236cb096206b2cc" +dependencies = [ + "thiserror-impl 2.0.9", ] [[package]] @@ -1695,7 +1729,18 @@ checksum = "4fee6c4efc90059e10f81e6d42c60a18f76588c3d74cb83a0b242a2b6c7504c1" dependencies = [ "proc-macro2", "quote", - "syn 2.0.90", + "syn", +] + +[[package]] +name = "thiserror-impl" +version = "2.0.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7b50fa271071aae2e6ee85f842e2e28ba8cd2c5fb67f11fcb1fd70b276f9e7d4" +dependencies = [ + "proc-macro2", + "quote", + "syn", ] [[package]] @@ -1747,7 +1792,7 @@ version = "0.1.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "8450ade61b78735ed7811cc14639462723d87a6cd748a41e7bfde554ac5033dd" dependencies = [ - "thiserror", + "thiserror 1.0.69", ] [[package]] @@ -1818,7 +1863,7 @@ checksum = "395ae124c09f9e6918a2310af6038fba074bcf474ac352496d5910dd59a2226d" dependencies = [ "proc-macro2", "quote", - "syn 2.0.90", + "syn", ] [[package]] @@ -1900,38 +1945,33 @@ dependencies = [ [[package]] name = "tree-sitter" -version = "0.23.2" +version = "0.24.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0203df02a3b6dd63575cc1d6e609edc2181c9a11867a271b25cfd2abff3ec5ca" +checksum = "5f2434c86ba59ed15af56039cc5bf1acf8ba76ce301e32ef08827388ef285ec5" dependencies = [ "cc", "regex", "regex-syntax 0.8.5", + "streaming-iterator", "tree-sitter-language", ] [[package]] name = "tree-sitter-language" -version = "0.1.2" +version = "0.1.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e8ddffe35a0e5eeeadf13ff7350af564c6e73993a24db62caee1822b185c2600" +checksum = "c199356c799a8945965bb5f2c55b2ad9d9aa7c4b4f6e587fe9dea0bc715e5f9c" [[package]] name = "tree-sitter-rust" -version = "0.21.2" +version = "0.23.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "277690f420bf90741dea984f3da038ace46c4fe6047cba57a66822226cde1c93" +checksum = "a4d64d449ca63e683c562c7743946a646671ca23947b9c925c0cfbe65051a4af" dependencies = [ "cc", - "tree-sitter", + "tree-sitter-language", ] -[[package]] -name = "typed-arena" -version = "2.0.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6af6ae20167a9ece4bcb41af5b80f8a1f1df981f6391189ce00fd257af04126a" - [[package]] name = "unicode-ident" version = "1.0.14" @@ -2007,12 +2047,12 @@ checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423" [[package]] name = "which" -version = "6.0.3" +version = "7.0.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b4ee928febd44d98f2f459a4a79bd4d928591333a494a10a868418ac1b39cf1f" +checksum = "fb4a9e33648339dc1642b0e36e21b3385e6148e289226f657c809dee59df5028" dependencies = [ "either", - "home", + "env_home", "rustix", "winsafe", ] @@ -2048,22 +2088,13 @@ version = "0.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f" -[[package]] -name = "windows-sys" -version = "0.48.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "677d2418bec65e3338edb076e806bc1ec15693c5d0104683f2efe857f61056a9" -dependencies = [ - "windows-targets 0.48.5", -] - [[package]] name = "windows-sys" version = "0.52.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "282be5f36a8ce781fad8c8ae18fa3f9beff57ec1b52cb3de0789201425d9a33d" dependencies = [ - "windows-targets 0.52.6", + "windows-targets", ] [[package]] @@ -2072,22 +2103,7 @@ version = "0.59.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "1e38bc4d79ed67fd075bcc251a1c39b32a1776bbe92e5bef1f0bf1f8c531853b" dependencies = [ - "windows-targets 0.52.6", -] - -[[package]] -name = "windows-targets" -version = "0.48.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9a2fa6e2155d7247be68c096456083145c183cbbbc2764150dda45a87197940c" -dependencies = [ - "windows_aarch64_gnullvm 0.48.5", - "windows_aarch64_msvc 0.48.5", - "windows_i686_gnu 0.48.5", - "windows_i686_msvc 0.48.5", - "windows_x86_64_gnu 0.48.5", - "windows_x86_64_gnullvm 0.48.5", - "windows_x86_64_msvc 0.48.5", + "windows-targets", ] [[package]] @@ -2096,46 +2112,28 @@ version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9b724f72796e036ab90c1021d4780d4d3d648aca59e491e6b98e725b84e99973" dependencies = [ - "windows_aarch64_gnullvm 0.52.6", - "windows_aarch64_msvc 0.52.6", - "windows_i686_gnu 0.52.6", + "windows_aarch64_gnullvm", + "windows_aarch64_msvc", + "windows_i686_gnu", "windows_i686_gnullvm", - "windows_i686_msvc 0.52.6", - "windows_x86_64_gnu 0.52.6", - "windows_x86_64_gnullvm 0.52.6", - "windows_x86_64_msvc 0.52.6", + "windows_i686_msvc", + "windows_x86_64_gnu", + "windows_x86_64_gnullvm", + "windows_x86_64_msvc", ] -[[package]] -name = "windows_aarch64_gnullvm" -version = "0.48.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2b38e32f0abccf9987a4e3079dfb67dcd799fb61361e53e2882c3cbaf0d905d8" - [[package]] name = "windows_aarch64_gnullvm" version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "32a4622180e7a0ec044bb555404c800bc9fd9ec262ec147edd5989ccd0c02cd3" -[[package]] -name = "windows_aarch64_msvc" -version = "0.48.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "dc35310971f3b2dbbf3f0690a219f40e2d9afcf64f9ab7cc1be722937c26b4bc" - [[package]] name = "windows_aarch64_msvc" version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "09ec2a7bb152e2252b53fa7803150007879548bc709c039df7627cabbd05d469" -[[package]] -name = "windows_i686_gnu" -version = "0.48.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a75915e7def60c94dcef72200b9a8e58e5091744960da64ec734a6c6e9b3743e" - [[package]] name = "windows_i686_gnu" version = "0.52.6" @@ -2148,48 +2146,24 @@ version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0eee52d38c090b3caa76c563b86c3a4bd71ef1a819287c19d586d7334ae8ed66" -[[package]] -name = "windows_i686_msvc" -version = "0.48.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8f55c233f70c4b27f66c523580f78f1004e8b5a8b659e05a4eb49d4166cca406" - [[package]] name = "windows_i686_msvc" version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "240948bc05c5e7c6dabba28bf89d89ffce3e303022809e73deaefe4f6ec56c66" -[[package]] -name = "windows_x86_64_gnu" -version = "0.48.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "53d40abd2583d23e4718fddf1ebec84dbff8381c07cae67ff7768bbf19c6718e" - [[package]] name = "windows_x86_64_gnu" version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "147a5c80aabfbf0c7d901cb5895d1de30ef2907eb21fbbab29ca94c5b08b1a78" -[[package]] -name = "windows_x86_64_gnullvm" -version = "0.48.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0b7b52767868a23d5bab768e390dc5f5c55825b6d30b86c844ff2dc7414044cc" - [[package]] name = "windows_x86_64_gnullvm" version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "24d5b23dc417412679681396f2b49f3de8c1473deb516bd34410872eff51ed0d" -[[package]] -name = "windows_x86_64_msvc" -version = "0.48.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ed94fce61571a4006852b7389a063ab983c02eb1bb37b47f8272ce92d06d9538" - [[package]] name = "windows_x86_64_msvc" version = "0.52.6" @@ -2198,9 +2172,9 @@ checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec" [[package]] name = "winnow" -version = "0.6.20" +version = "0.6.22" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "36c1fec1a2bb5866f07c25f68c26e565c4c200aebb96d7e55710c19d3e8ac49b" +checksum = "39281189af81c07ec09db316b302a3e67bf9bd7cbf6c820b50e35fee9c2fa980" dependencies = [ "memchr", ] @@ -2229,5 +2203,5 @@ checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e" dependencies = [ "proc-macro2", "quote", - "syn 2.0.90", + "syn", ] diff --git a/Cargo.toml b/Cargo.toml index 3c61638025e5..f6236785e038 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-verifier" -version = "0.56.0" +version = "0.57.0" edition = "2021" description = "A bit-precise model checker for Rust." readme = "README.md" diff --git a/charon b/charon index 454078ebdb4a..adc0a855aa14 160000 --- a/charon +++ b/charon @@ -1 +1 @@ -Subproject commit 454078ebdb4a607e2b21dc115e1ca99b516e436f +Subproject commit adc0a855aa1428d68e4270edef0d52131cef06ab diff --git a/cprover_bindings/Cargo.toml b/cprover_bindings/Cargo.toml index e26f23d5c081..b8f0210f9c72 100644 --- a/cprover_bindings/Cargo.toml +++ b/cprover_bindings/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "cprover_bindings" -version = "0.56.0" +version = "0.57.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false @@ -17,7 +17,7 @@ lazy_static = "1.4.0" num = "0.4.0" num-traits = "0.2" serde = {version = "1", features = ["derive"]} -string-interner = "0.17.0" +string-interner = "0.18" tracing = "0.1" linear-map = {version = "1.2", features = ["serde_impl"]} diff --git a/cprover_bindings/src/irep/goto_binary_serde.rs b/cprover_bindings/src/irep/goto_binary_serde.rs index c1b901ddd5c8..15cc0afa8902 100644 --- a/cprover_bindings/src/irep/goto_binary_serde.rs +++ b/cprover_bindings/src/irep/goto_binary_serde.rs @@ -936,9 +936,9 @@ where } } -//////////////////////////////////////// -//// Dynamic memory usage computation -//////////////////////////////////////// +// ================================== +// Dynamic memory usage computation +// ================================== #[cfg(test)] mod sharing_stats { @@ -1032,7 +1032,7 @@ mod sharing_stats { } } - impl<'a, W> DynamicUsage for GotoBinarySerializer<'a, W> + impl DynamicUsage for GotoBinarySerializer<'_, W> where W: Write, { @@ -1127,9 +1127,9 @@ mod sharing_stats { max_count = *count; max_id = Some(id); }; - nof_unique = nof_unique + 1; + nof_unique += 1; let incr = (*count as f64 - avg_count) / (nof_unique as f64); - avg_count = avg_count + incr; + avg_count += incr; } SharingStats { _nof_unique: nof_unique, @@ -1156,7 +1156,7 @@ mod sharing_stats { } impl GotoBinarySharingStats { - fn from_serializer<'a, W: Write>(s: &GotoBinarySerializer<'a, W>) -> Self { + fn from_serializer(s: &GotoBinarySerializer<'_, W>) -> Self { GotoBinarySharingStats { _allocated_bytes: s.dynamic_usage(), _string_stats: SharingStats::new(&s.string_count), @@ -1173,7 +1173,7 @@ mod sharing_stats { } } - impl<'a, W> GotoBinarySerializer<'a, W> + impl GotoBinarySerializer<'_, W> where W: Write, { @@ -1277,13 +1277,13 @@ mod tests { let mut writer = BufWriter::new(&mut vec); let mut serializer = GotoBinarySerializer::new(&mut writer); - for u in std::u8::MIN..std::u8::MAX { + for u in u8::MIN..u8::MAX { serializer.write_u8(u); } } // read back from byte stream - for u in std::u8::MIN..std::u8::MAX { + for u in u8::MIN..u8::MAX { assert_eq!(vec[u as usize], u); } } @@ -1352,7 +1352,7 @@ mod tests { let foo = String::from("foo").intern(); let bar = String::from("bar").intern(); let baz = String::from("baz").intern(); - let strings = vec![foo, bar, foo, bar, foo, baz, baz, bar, foo]; + let strings = [foo, bar, foo, bar, foo, baz, baz, bar, foo]; let mut vec: Vec = Vec::new(); diff --git a/cprover_bindings/src/utils.rs b/cprover_bindings/src/utils.rs index 4a323277ec9e..e161fb886a22 100644 --- a/cprover_bindings/src/utils.rs +++ b/cprover_bindings/src/utils.rs @@ -106,6 +106,7 @@ mod tests { use num::BigInt; #[test] + #[allow(clippy::bool_assert_comparison)] fn test_fits_in_bits() { assert_eq!(BigInt::from(10).fits_in_bits(3, false), false); assert_eq!(BigInt::from(10).fits_in_bits(4, false), true); diff --git a/deny.toml b/deny.toml index 0347d4ac177a..f0b9049ffc03 100644 --- a/deny.toml +++ b/deny.toml @@ -16,14 +16,13 @@ yanked = "deny" allow = [ "MIT", "Apache-2.0", - "MPL-2.0", ] confidence-threshold = 0.8 # All these exceptions should probably appear in: tools/build-kani/license-notes.txt exceptions = [ { name = "unicode-ident", allow=["Unicode-3.0"] }, - { name = "rustc_apfloat", allow=["Apache-2.0 WITH LLVM-exception"] }, + { name = "foldhash", allow=["Zlib"] }, ] [licenses.private] @@ -43,4 +42,3 @@ wildcards = "allow" unknown-registry = "deny" unknown-git = "deny" allow-registry = ["https://github.com/rust-lang/crates.io-index"] -allow-git = ["https://github.com/Nadrieril/tracing-tree"] diff --git a/docs/src/build-from-source.md b/docs/src/build-from-source.md index e0982bf2899b..bfe5d9057d8d 100644 --- a/docs/src/build-from-source.md +++ b/docs/src/build-from-source.md @@ -12,7 +12,7 @@ In general, the following dependencies are required to build Kani from source. 1. Cargo installed via [rustup](https://rustup.rs/) 2. [CBMC](https://github.com/diffblue/cbmc) (latest release) -3. [Kissat](https://github.com/arminbiere/kissat) (Release 3.1.1) +3. [Kissat](https://github.com/arminbiere/kissat) (Release 4.0.1) Kani has been tested in [Ubuntu](#install-dependencies-on-ubuntu) and [macOS](##install-dependencies-on-macos) platforms. diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index 9f084da7b962..50ae4e0a58d6 100644 --- a/kani-compiler/Cargo.toml +++ b/kani-compiler/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-compiler" -version = "0.56.0" +version = "0.57.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs index 5a5f02969b01..ddc6f6264d1e 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs @@ -38,7 +38,6 @@ use rustc_smir::rustc_internal; use stable_mir::mir::mono::{Instance, MonoItem}; use stable_mir::{CrateDef, DefId}; use std::any::Any; -use std::collections::{HashMap, HashSet}; use std::fs::File; use std::path::Path; use std::sync::{Arc, Mutex}; @@ -394,16 +393,6 @@ fn create_charon_transformation_context(tcx: TyCtxt) -> TransformCtx { }; let crate_name = tcx.crate_name(LOCAL_CRATE).as_str().into(); let translated = TranslatedCrate { crate_name, ..TranslatedCrate::default() }; - let errors = ErrorCtx { - continue_on_failure: true, - error_on_warnings: false, - dcx: &(), - external_decls_with_errors: HashSet::new(), - ignored_failed_decls: HashSet::new(), - external_dep_sources: HashMap::new(), - def_id: None, - def_id_is_local: true, - error_count: 0, - }; + let errors = ErrorCtx::new(true, false); TransformCtx { options, translated, errors } } diff --git a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs index 24cb007be0b8..1664867b087d 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs @@ -6,12 +6,11 @@ //! This module contains a context for translating stable MIR into Charon's //! unstructured low-level borrow calculus (ULLBC) +use charon_lib::ast::krate::TypeDeclId as CharonTypeDeclId; use charon_lib::ast::meta::{ AttrInfo as CharonAttrInfo, Loc as CharonLoc, RawSpan as CharonRawSpan, }; -use charon_lib::ast::types::{ - Ty as CharonTy, TyKind as CharonTyKind, TypeDeclId as CharonTypeDeclId, -}; +use charon_lib::ast::types::{Ty as CharonTy, TyKind as CharonTyKind}; use charon_lib::ast::{ AbortKind as CharonAbortKind, AggregateKind as CharonAggregateKind, AnyTransId as CharonAnyTransId, Assert as CharonAssert, BinOp as CharonBinOp, @@ -19,21 +18,23 @@ use charon_lib::ast::{ BuiltinTy as CharonBuiltinTy, Call as CharonCall, CastKind as CharonCastKind, ConstGeneric as CharonConstGeneric, ConstGenericVar as CharonConstGenericVar, ConstGenericVarId as CharonConstGenericVarId, ConstantExpr as CharonConstantExpr, - Disambiguator as CharonDisambiguator, Field as CharonField, FieldId as CharonFieldId, - FieldProjKind as CharonFieldProjKind, FileName as CharonFileName, FnOperand as CharonFnOperand, + DeBruijnVar as CharonDeBruijnVar, Disambiguator as CharonDisambiguator, Field as CharonField, + FieldId as CharonFieldId, FieldProjKind as CharonFieldProjKind, File as CharonFile, + FileId as CharonFileId, FileName as CharonFileName, FnOperand as CharonFnOperand, FnPtr as CharonFnPtr, FunDecl as CharonFunDecl, FunDeclId as CharonFunDeclId, FunId as CharonFunId, FunIdOrTraitMethodRef as CharonFunIdOrTraitMethodRef, FunSig as CharonFunSig, GenericArgs as CharonGenericArgs, GenericParams as CharonGenericParams, IntegerTy as CharonIntegerTy, ItemKind as CharonItemKind, ItemMeta as CharonItemMeta, ItemOpacity as CharonItemOpacity, Literal as CharonLiteral, LiteralTy as CharonLiteralTy, - Name as CharonName, Opaque as CharonOpaque, Operand as CharonOperand, + Locals, Name as CharonName, Opaque as CharonOpaque, Operand as CharonOperand, PathElem as CharonPathElem, Place as CharonPlace, ProjectionElem as CharonProjectionElem, RawConstantExpr as CharonRawConstantExpr, RefKind as CharonRefKind, Region as CharonRegion, - RegionId as CharonRegionId, RegionVar as CharonRegionVar, Rvalue as CharonRvalue, - ScalarValue as CharonScalarValue, Span as CharonSpan, TranslatedCrate as CharonTranslatedCrate, - TypeDecl as CharonTypeDecl, TypeDeclKind as CharonTypeDeclKind, TypeId as CharonTypeId, - TypeVar as CharonTypeVar, TypeVarId as CharonTypeVarId, UnOp as CharonUnOp, Var as CharonVar, - VarId as CharonVarId, Variant as CharonVariant, VariantId as CharonVariantId, + RegionBinder as CharonRegionBinder, RegionId as CharonRegionId, RegionVar as CharonRegionVar, + Rvalue as CharonRvalue, ScalarValue as CharonScalarValue, Span as CharonSpan, + TranslatedCrate as CharonTranslatedCrate, TypeDecl as CharonTypeDecl, + TypeDeclKind as CharonTypeDeclKind, TypeId as CharonTypeId, TypeVar as CharonTypeVar, + TypeVarId as CharonTypeVarId, UnOp as CharonUnOp, Var as CharonVar, VarId as CharonVarId, + Variant as CharonVariant, VariantId as CharonVariantId, }; use charon_lib::errors::{Error as CharonError, ErrorCtx as CharonErrorCtx}; use charon_lib::ids::Vector as CharonVector; @@ -60,6 +61,7 @@ use stable_mir::ty::{ MirConst, Region, RegionKind, RigidTy, Span, Ty, TyConst, TyConstKind, TyKind, UintTy, }; use stable_mir::{CrateDef, DefId}; +use std::collections::HashMap; use std::path::PathBuf; use tracing::{debug, trace}; @@ -70,8 +72,9 @@ pub struct Context<'a, 'tcx> { instance: Instance, translated: &'a mut CharonTranslatedCrate, id_map: &'a mut FxHashMap, - errors: &'a mut CharonErrorCtx<'tcx>, + errors: &'a mut CharonErrorCtx, local_names: FxHashMap, + file_to_id: HashMap, } impl<'a, 'tcx> Context<'a, 'tcx> { @@ -82,7 +85,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { instance: Instance, translated: &'a mut CharonTranslatedCrate, id_map: &'a mut FxHashMap, - errors: &'a mut CharonErrorCtx<'tcx>, + errors: &'a mut CharonErrorCtx, ) -> Self { let mut local_names = FxHashMap::default(); // populate names of locals @@ -93,8 +96,8 @@ impl<'a, 'tcx> Context<'a, 'tcx> { } } } - - Self { tcx, instance, translated, id_map, errors, local_names } + let file_to_id: HashMap = HashMap::new(); + Self { tcx, instance, translated, id_map, errors, local_names, file_to_id } } fn tcx(&self) -> TyCtxt<'tcx> { @@ -102,7 +105,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { } fn span_err(&mut self, span: CharonSpan, msg: &str) { - self.errors.span_err(span, msg); + self.errors.span_err(self.translated, span, msg); } fn continue_on_failure(&self) -> bool { @@ -136,6 +139,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { item_meta, signature, kind: CharonItemKind::Regular, + is_global_initializer: None, body: Ok(body), }; @@ -645,11 +649,12 @@ impl<'a, 'tcx> Context<'a, 'tcx> { /// Compute the span information for MIR span fn translate_span(&mut self, span: Span) -> CharonSpan { let filename = CharonFileName::Local(PathBuf::from(span.get_filename())); - let file_id = match self.translated.file_to_id.get(&filename) { + let file_id = match self.file_to_id.get(&filename) { Some(file_id) => *file_id, None => { - let file_id = self.translated.id_to_file.push(filename.clone()); - self.translated.file_to_id.insert(filename, file_id); + let file = CharonFile { name: filename.clone(), contents: None }; + let file_id = self.translated.files.push(file); + self.file_to_id.insert(filename, file_id); file_id } }; @@ -699,7 +704,6 @@ impl<'a, 'tcx> Context<'a, 'tcx> { is_closure: false, closure_info: None, generics: CharonGenericParams::default(), - parent_params_info: None, inputs: args, output: ret_type, } @@ -717,11 +721,12 @@ impl<'a, 'tcx> Context<'a, 'tcx> { fn translate_body(&mut self, mir_body: Body) -> CharonBody { let span = self.translate_span(mir_body.span); let arg_count = self.instance.fn_abi().unwrap().args.len(); - let locals = self.translate_body_locals(&mir_body); + let vars = self.translate_body_locals(&mir_body); + let locals = Locals { vars, arg_count }; let body: CharonBodyContents = mir_body.blocks.iter().map(|bb| self.translate_block(bb)).collect(); - let body_expr = CharonExprBody { span, arg_count, locals, body, comments: Vec::new() }; + let body_expr = CharonExprBody { span, locals, body, comments: Vec::new() }; CharonBody::Unstructured(body_expr) } @@ -764,9 +769,11 @@ impl<'a, 'tcx> Context<'a, 'tcx> { fn translate_ty(&mut self, ty: Ty) -> CharonTy { match ty.kind() { TyKind::RigidTy(rigid_ty) => self.translate_rigid_ty(rigid_ty), - TyKind::Param(paramty) => CharonTy::new(CharonTyKind::TypeVar( - CharonTypeVarId::from_usize(paramty.index as usize), - )), + TyKind::Param(paramty) => { + let debr = + CharonDeBruijnVar::free(CharonTypeVarId::from_usize(paramty.index as usize)); + CharonTy::new(CharonTyKind::TypeVar(debr)) + } x => todo!("Not yet implemented translation for TyKind: {:?}", x), } } @@ -778,7 +785,10 @@ impl<'a, 'tcx> Context<'a, 'tcx> { translate_constant_expr_to_const_generic(c_raw_constexpr).unwrap() } TyConstKind::Param(paramc) => { - CharonConstGeneric::Var(CharonConstGenericVarId::from_usize(paramc.index as usize)) + let debr = CharonDeBruijnVar::free(CharonConstGenericVarId::from_usize( + paramc.index as usize, + )); + CharonConstGeneric::Var(debr) } _ => todo!(), } @@ -843,15 +853,16 @@ impl<'a, 'tcx> Context<'a, 'tcx> { }; CharonTy::new(CharonTyKind::Adt(CharonTypeId::Tuple, generic_args)) } - RigidTy::FnDef(def_id, args) => { - if !args.0.is_empty() { - unimplemented!("generic args are not yet handled"); - } + RigidTy::FnDef(def_id, _args) => { let sig = def_id.fn_sig().value; let inputs = sig.inputs().iter().map(|ty| self.translate_ty(*ty)).collect(); let output = self.translate_ty(sig.output()); // TODO: populate regions? - CharonTy::new(CharonTyKind::Arrow(CharonVector::new(), inputs, output)) + let rb = CharonRegionBinder { + regions: CharonVector::new(), + skip_binder: (inputs, output), + }; + CharonTy::new(CharonTyKind::Arrow(rb)) } RigidTy::Adt(adt_def, genarg) => { let def_id = adt_def.def_id(); @@ -1004,10 +1015,10 @@ impl<'a, 'tcx> Context<'a, 'tcx> { } fn translate_place(&mut self, place: &Place) -> CharonPlace { - let projection = self.translate_projection(place, &place.projection); + let (_projection, ty) = self.translate_projection(place, &place.projection); let local = place.local; let var_id = CharonVarId::from_usize(local); - CharonPlace { var_id, projection } + CharonPlace::new(var_id, ty) } fn place_ty(&self, place: &Place) -> Ty { @@ -1251,7 +1262,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { &mut self, place: &Place, projection: &[ProjectionElem], - ) -> Vec { + ) -> (Vec, CharonTy) { let c_place_ty = self.translate_ty(self.place_ty(place)); let mut c_provec = Vec::new(); let mut current_ty = c_place_ty.clone(); @@ -1291,27 +1302,29 @@ impl<'a, 'tcx> Context<'a, 'tcx> { current_var = varid.to_index(); } ProjectionElem::Index(local) => { - let c_operand = - CharonOperand::Copy(CharonPlace::new(CharonVarId::from_usize(*local))); + let c_operand = CharonOperand::Copy(CharonPlace::new( + CharonVarId::from_usize(*local), + current_ty.clone(), + )); c_provec.push(CharonProjectionElem::Index { - offset: c_operand, + offset: Box::new(c_operand), from_end: false, - ty: current_ty.clone(), }); } _ => continue, } } - c_provec + (c_provec, current_ty) } fn translate_region(&self, region: Region) -> CharonRegion { match region.kind { RegionKind::ReStatic => CharonRegion::Static, RegionKind::ReErased => CharonRegion::Erased, - RegionKind::ReEarlyParam(_) => CharonRegion::Unknown, - RegionKind::ReBound(_, _) | RegionKind::RePlaceholder(_) => { + RegionKind::ReEarlyParam(_) + | RegionKind::ReBound(_, _) + | RegionKind::RePlaceholder(_) => { todo!("Not yet implemented RegionKind: {:?}", region.kind) } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 3dccbea5837f..b6189c070538 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -283,6 +283,16 @@ impl GotocCtx<'_> { .member("direct_fields", &self.symbol_table) .member(field_name, &self.symbol_table)) } + TyKind::RigidTy(RigidTy::CoroutineClosure(def, args)) => { + let typ = Ty::new_coroutine_closure(def, args); + let goto_typ = self.codegen_ty_stable(typ); + Err(UnimplementedData::new( + "Coroutine closures", + "https://github.com/model-checking/kani/issues/3783", + goto_typ, + *parent_expr.location(), + )) + } TyKind::RigidTy(RigidTy::Str) | TyKind::RigidTy(RigidTy::Array(_, _)) | TyKind::RigidTy(RigidTy::Slice(_)) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 68c174ae2119..d13597794d19 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -729,6 +729,15 @@ impl GotocCtx<'_> { } } AggregateKind::Coroutine(_, _, _) => self.codegen_rvalue_coroutine(&operands, res_ty), + AggregateKind::CoroutineClosure(_, _) => { + let ty = self.codegen_ty_stable(res_ty); + self.codegen_unimplemented_expr( + "CoroutineClosure", + ty, + loc, + "https://github.com/model-checking/kani/issues/3783", + ) + } } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs index 00160a0db1a0..549fbcf3447d 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs @@ -6,7 +6,7 @@ use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::goto_program::Location; use lazy_static::lazy_static; -use rustc_ast::Attribute; +use rustc_hir::Attribute; use rustc_smir::rustc_internal; use rustc_span::Span; use stable_mir::ty::Span as SpanStable; diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 903baf8eaced..748eb42e7655 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -590,6 +590,9 @@ impl<'tcx> GotocCtx<'tcx> { } ty::Closure(_, subst) => self.codegen_ty_closure(ty, subst), ty::Coroutine(..) => self.codegen_ty_coroutine(ty), + ty::CoroutineClosure(..) => unimplemented!( + "Kani does not yet support coroutine closures. Please post your example at https://github.com/model-checking/kani/issues/3783" + ), ty::Never => self.ensure_struct(NEVER_TYPE_EMPTY_STRUCT_NAME, "!", |_, _| vec![]), ty::Tuple(ts) => { if ts.is_empty() { @@ -619,11 +622,7 @@ impl<'tcx> GotocCtx<'tcx> { ty::Bound(_, _) | ty::Param(_) => unreachable!("monomorphization bug"), // type checking remnants which shouldn't be reachable - ty::CoroutineWitness(_, _) - | ty::CoroutineClosure(_, _) - | ty::Infer(_) - | ty::Placeholder(_) - | ty::Error(_) => { + ty::CoroutineWitness(_, _) | ty::Infer(_) | ty::Placeholder(_) | ty::Error(_) => { unreachable!("remnants of type checking") } } @@ -879,7 +878,7 @@ impl<'tcx> GotocCtx<'tcx> { /// Generates a struct for a variant of the coroutine. /// - /// The field `discriminant_field` should be `Some(idx)` when generating the variant for the direct (top-[evel) fields of the coroutine. + /// The field `discriminant_field` should be `Some(idx)` when generating the variant for the direct (top-level) fields of the coroutine. /// Then the field with the index `idx` will be treated as the discriminant and will be given a special name to work with the rest of the code. /// The field `discriminant_field` should be `None` when generating an actual variant of the coroutine because those don't contain the discriminant as a field. fn codegen_coroutine_variant_struct( diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 017266717de7..83893da0707d 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -6,11 +6,9 @@ use std::collections::{BTreeMap, HashSet}; use kani_metadata::{CbmcSolver, HarnessAttributes, HarnessKind, Stub}; use quote::ToTokens; -use rustc_ast::{ - AttrArgs, AttrArgsEq, AttrKind, Attribute, ExprKind, LitKind, MetaItem, MetaItemKind, attr, -}; +use rustc_ast::{LitKind, MetaItem, MetaItemKind, attr}; use rustc_errors::ErrorGuaranteed; -use rustc_hir::{def::DefKind, def_id::DefId}; +use rustc_hir::{AttrArgs, AttrKind, Attribute, def::DefKind, def_id::DefId}; use rustc_middle::ty::{Instance, TyCtxt, TyKind}; use rustc_session::Session; use rustc_smir::rustc_internal; @@ -673,31 +671,12 @@ fn expect_key_string_value( attr: &Attribute, ) -> Result { let span = attr.span; - let AttrArgs::Eq { eq_span: _, value } = &attr.get_normal_item().args else { + let AttrArgs::Eq { expr, .. } = &attr.get_normal_item().args else { return Err(sess .dcx() .span_err(span, "Expected attribute of the form #[attr = \"value\"]")); }; - let maybe_str = match value { - AttrArgsEq::Ast(expr) => { - if let ExprKind::Lit(tok) = expr.kind { - match LitKind::from_token_lit(tok) { - Ok(l) => l.str(), - Err(err) => { - return Err(sess.dcx().span_err( - span, - format!("Invalid string literal on right hand side of `=` {err:?}"), - )); - } - } - } else { - return Err(sess - .dcx() - .span_err(span, "Expected literal string as right hand side of `=`")); - } - } - AttrArgsEq::Hir(lit) => lit.kind.str(), - }; + let maybe_str = expr.kind.str(); if let Some(str) = maybe_str { Ok(str) } else { @@ -841,7 +820,7 @@ fn parse_stubs(tcx: TyCtxt, harness: DefId, attributes: &[&Attribute]) -> Vec Option { /// Extracts a vector with the path arguments of an attribute. /// /// Emits an error if it couldn't convert any of the arguments and return an empty vector. -fn parse_paths(attr: &Attribute) -> Result, syn::Error> { - let syn_attr = syn_attr(attr); +fn parse_paths(tcx: TyCtxt, attr: &Attribute) -> Result, syn::Error> { + let syn_attr = syn_attr(tcx, attr); let parser = Punctuated::::parse_terminated; let paths = syn_attr.parse_args_with(parser)?; Ok(paths.into_iter().collect()) @@ -990,11 +969,11 @@ fn parse_str_value(attr: &Attribute) -> Option { fn attr_kind(tcx: TyCtxt, attr: &Attribute) -> Option { match &attr.kind { AttrKind::Normal(normal) => { - let segments = &normal.item.path.segments; - if (!segments.is_empty()) && segments[0].ident.as_str() == "kanitool" { + let segments = &normal.path.segments; + if (!segments.is_empty()) && segments[0].as_str() == "kanitool" { let ident_str = segments[1..] .iter() - .map(|segment| segment.ident.as_str()) + .map(|segment| segment.as_str()) .intersperse("::") .collect::(); KaniAttributeKind::try_from(ident_str.as_str()) @@ -1014,8 +993,8 @@ fn attr_kind(tcx: TyCtxt, attr: &Attribute) -> Option { /// Parse an attribute using `syn`. /// /// This provides a user-friendly interface to manipulate than the internal compiler AST. -fn syn_attr(attr: &Attribute) -> syn::Attribute { - let attr_str = rustc_ast_pretty::pprust::attribute_to_string(attr); +fn syn_attr(tcx: TyCtxt, attr: &Attribute) -> syn::Attribute { + let attr_str = rustc_hir_pretty::attribute_to_string(&tcx, attr); let parser = syn::Attribute::parse_outer; parser.parse_str(&attr_str).unwrap().pop().unwrap() } diff --git a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs index 369296db6ed4..345a27309b50 100644 --- a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs +++ b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs @@ -136,7 +136,7 @@ impl<'tcx> Analysis<'tcx> for PointsToAnalysis<'_, 'tcx> { /// Update current dataflow state based on the information we can infer from the given /// statement. - fn apply_statement_effect( + fn apply_primary_statement_effect( &mut self, state: &mut Self::Domain, statement: &Statement<'tcx>, @@ -184,7 +184,7 @@ impl<'tcx> Analysis<'tcx> for PointsToAnalysis<'_, 'tcx> { } } - fn apply_terminator_effect<'mir>( + fn apply_primary_terminator_effect<'mir>( &mut self, state: &mut Self::Domain, terminator: &'mir Terminator<'tcx>, diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs index 8a9e3ac094d5..0a1fc16dcc07 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs @@ -393,6 +393,7 @@ fn data_bytes_for_ty( | RigidTy::FnPtr(_) | RigidTy::Closure(_, _) | RigidTy::Coroutine(_, _, _) + | RigidTy::CoroutineClosure(_, _) | RigidTy::CoroutineWitness(_, _) | RigidTy::Foreign(_) | RigidTy::Dynamic(_, _, _) => Err(LayoutComputationError::UnsupportedType(ty)), diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs index 5d66d00cf094..2276906aae81 100644 --- a/kani-compiler/src/kani_middle/transform/check_values.rs +++ b/kani-compiler/src/kani_middle/transform/check_values.rs @@ -640,6 +640,7 @@ impl MirVisitor for CheckValueVisitor<'_, '_> { AggregateKind::Array(_) | AggregateKind::Closure(_, _) | AggregateKind::Coroutine(_, _, _) + | AggregateKind::CoroutineClosure(_, _) | AggregateKind::RawPtr(_, _) | AggregateKind::Tuple => {} }, @@ -981,6 +982,7 @@ pub fn ty_validity_per_offset( | RigidTy::FnPtr(_) | RigidTy::Closure(_, _) | RigidTy::Coroutine(_, _, _) + | RigidTy::CoroutineClosure(_, _) | RigidTy::CoroutineWitness(_, _) | RigidTy::Foreign(_) | RigidTy::Dynamic(_, _, _) => Err(format!("Unsupported {ty:?}")), diff --git a/kani-compiler/src/kani_middle/transform/internal_mir.rs b/kani-compiler/src/kani_middle/transform/internal_mir.rs index d29a5e688d2c..4f1095cce06e 100644 --- a/kani-compiler/src/kani_middle/transform/internal_mir.rs +++ b/kani-compiler/src/kani_middle/transform/internal_mir.rs @@ -56,6 +56,12 @@ impl RustcInternalMir for AggregateKind { internal(tcx, generic_args), ) } + AggregateKind::CoroutineClosure(coroutine_def, generic_args) => { + rustc_middle::mir::AggregateKind::CoroutineClosure( + internal(tcx, coroutine_def.0), + internal(tcx, generic_args), + ) + } AggregateKind::RawPtr(ty, mutability) => rustc_middle::mir::AggregateKind::RawPtr( internal(tcx, ty), internal(tcx, mutability), diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs index 65f1a22852b7..6f108595dbfc 100644 --- a/kani-compiler/src/main.rs +++ b/kani-compiler/src/main.rs @@ -25,6 +25,7 @@ extern crate rustc_data_structures; extern crate rustc_driver; extern crate rustc_errors; extern crate rustc_hir; +extern crate rustc_hir_pretty; extern crate rustc_index; extern crate rustc_interface; extern crate rustc_metadata; diff --git a/kani-dependencies b/kani-dependencies index 004e9a0a9811..ed8e32faca90 100644 --- a/kani-dependencies +++ b/kani-dependencies @@ -2,4 +2,4 @@ CBMC_MAJOR="6" CBMC_MINOR="4" CBMC_VERSION="6.4.1" -KISSAT_VERSION="3.1.1" +KISSAT_VERSION="4.0.1" diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index 1025b4b201e2..123801e81a0a 100644 --- a/kani-driver/Cargo.toml +++ b/kani-driver/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-driver" -version = "0.56.0" +version = "0.57.0" edition = "2021" description = "Build a project with Kani and run all proof harnesses" license = "MIT OR Apache-2.0" @@ -13,7 +13,7 @@ publish = false [dependencies] kani_metadata = { path = "../kani_metadata" } -cargo_metadata = "0.18.0" +cargo_metadata = "0.19" anyhow = "1" console = "0.15.1" once_cell = "1.19.0" @@ -35,7 +35,7 @@ tempfile = "3" tracing = {version = "0.1", features = ["max_level_trace", "release_max_level_debug"]} tracing-subscriber = {version = "0.3.8", features = ["env-filter", "json", "fmt"]} rand = "0.8" -which = "6" +which = "7" time = {version = "0.3.36", features = ["formatting"]} tokio = { version = "1.40.0", features = ["io-util", "process", "rt", "time"] } diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 66ff247ddc82..9b2408d484e2 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -257,8 +257,11 @@ pub struct VerificationArgs { // consumes everything pub cbmc_args: Vec, - /// Number of parallel jobs, defaults to 1 - #[arg(short, long, hide = true, requires("enable_unstable"))] + /// Number of threads to spawn to verify harnesses in parallel. + /// Omit the flag entirely to run sequentially (i.e. one thread). + /// Pass -j to run with the thread pool's default number of threads. + /// Pass -j to specify N threads. + #[arg(short, long, hide_short_help = true, requires("enable_unstable"))] pub jobs: Option>, /// Enable extra pointer checks such as invalid pointers in relation operations and pointer diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index cec8226e5f8e..f26a8e0aa4e8 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -9,7 +9,8 @@ use crate::util; use anyhow::{Context, Result, bail}; use cargo_metadata::diagnostic::{Diagnostic, DiagnosticLevel}; use cargo_metadata::{ - Artifact as RustcArtifact, Message, Metadata, MetadataCommand, Package, PackageId, Target, + Artifact as RustcArtifact, CrateType, Message, Metadata, MetadataCommand, Package, PackageId, + Target, TargetKind, }; use kani_metadata::{ArtifactType, CompilerArtifactStub}; use std::collections::HashMap; @@ -22,16 +23,6 @@ use std::path::{Path, PathBuf}; use std::process::Command; use tracing::{debug, trace}; -//---- Crate types identifier used by cargo. -const CRATE_TYPE_BIN: &str = "bin"; -const CRATE_TYPE_CDYLIB: &str = "cdylib"; -const CRATE_TYPE_DYLIB: &str = "dylib"; -const CRATE_TYPE_LIB: &str = "lib"; -const CRATE_TYPE_PROC_MACRO: &str = "proc-macro"; -const CRATE_TYPE_RLIB: &str = "rlib"; -const CRATE_TYPE_STATICLIB: &str = "staticlib"; -const CRATE_TYPE_TEST: &str = "test"; - /// The outputs of kani-compiler being invoked via cargo on a project. pub struct CargoOutputs { /// The directory where compiler outputs should be directed. @@ -123,8 +114,8 @@ crate-type = ["lib"] .run_build(cmd)? .into_iter() .filter_map(|artifact| { - if artifact.target.crate_types.contains(&CRATE_TYPE_LIB.to_string()) - || artifact.target.crate_types.contains(&CRATE_TYPE_RLIB.to_string()) + if artifact.target.crate_types.contains(&CrateType::Lib) + || artifact.target.crate_types.contains(&CrateType::RLib) { map_kani_artifact(artifact) } else { @@ -576,26 +567,29 @@ fn package_targets(args: &VerificationArgs, package: &Package) -> Vec { + match kind { + TargetKind::Bin => { if args.target.include_bin(&target.name) { // Binary targets. verification_targets.push(VerificationTarget::Bin(target.clone())); } } - CRATE_TYPE_LIB | CRATE_TYPE_RLIB | CRATE_TYPE_CDYLIB | CRATE_TYPE_DYLIB - | CRATE_TYPE_STATICLIB => { + TargetKind::Lib + | TargetKind::RLib + | TargetKind::CDyLib + | TargetKind::DyLib + | TargetKind::StaticLib => { if args.target.include_lib() { supported_lib = true; } } - CRATE_TYPE_PROC_MACRO => { + TargetKind::ProcMacro => { if args.target.include_lib() { unsupported_lib = true; ignored_unsupported.push(target.name.as_str()); } } - CRATE_TYPE_TEST => { + TargetKind::Test => { // Test target. if args.target.include_tests() { if args.tests { diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index ee14992cba78..b78e1dc9d80b 100644 --- a/kani-driver/src/harness_runner.rs +++ b/kani-driver/src/harness_runner.rs @@ -103,14 +103,23 @@ impl<'pr> HarnessRunner<'_, 'pr> { } impl KaniSession { - fn process_output(&self, result: &VerificationResult, harness: &HarnessMetadata) { + fn process_output( + &self, + result: &VerificationResult, + harness: &HarnessMetadata, + thread_index: usize, + ) { if self.should_print_output() { if self.args.output_into_files { - self.write_output_to_file(result, harness); + self.write_output_to_file(result, harness, thread_index); } let output = result.render(&self.args.output_format, harness.attributes.should_panic); - println!("{}", output); + if rayon::current_num_threads() > 1 { + println!("Thread {thread_index}: {output}"); + } else { + println!("{output}"); + } } } @@ -118,7 +127,12 @@ impl KaniSession { !self.args.common_args.quiet && self.args.output_format != OutputFormat::Old } - fn write_output_to_file(&self, result: &VerificationResult, harness: &HarnessMetadata) { + fn write_output_to_file( + &self, + result: &VerificationResult, + harness: &HarnessMetadata, + thread_index: usize, + ) { let target_dir = self.result_output_dir().unwrap(); let file_name = target_dir.join(harness.pretty_name.clone()); let path = Path::new(&file_name); @@ -126,7 +140,11 @@ impl KaniSession { std::fs::create_dir_all(prefix).unwrap(); let mut file = File::create(&file_name).unwrap(); - let file_output = result.render(&OutputFormat::Regular, harness.attributes.should_panic); + let mut file_output = + result.render(&OutputFormat::Regular, harness.attributes.should_panic); + if rayon::current_num_threads() > 1 { + file_output = format!("Thread {thread_index}:\n{file_output}"); + } if let Err(e) = writeln!(file, "{}", file_output) { eprintln!( @@ -148,13 +166,18 @@ impl KaniSession { binary: &Path, harness: &HarnessMetadata, ) -> Result { + let thread_index = rayon::current_thread_index().unwrap_or_default(); if !self.args.common_args.quiet { - println!("Checking harness {}...", harness.pretty_name); + if rayon::current_num_threads() > 1 { + println!("Thread {thread_index}: Checking harness {}...", harness.pretty_name); + } else { + println!("Checking harness {}...", harness.pretty_name); + } } let mut result = self.with_timer(|| self.run_cbmc(binary, harness), "run_cbmc")?; - self.process_output(&result, harness); + self.process_output(&result, harness, thread_index); self.gen_and_add_concrete_playback(harness, &mut result)?; Ok(result) } diff --git a/kani_metadata/Cargo.toml b/kani_metadata/Cargo.toml index 2a0a03401c40..840990adca7a 100644 --- a/kani_metadata/Cargo.toml +++ b/kani_metadata/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_metadata" -version = "0.56.0" +version = "0.57.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/kani_metadata/src/artifact.rs b/kani_metadata/src/artifact.rs index 12f8f9a49566..dbb41a213bc8 100644 --- a/kani_metadata/src/artifact.rs +++ b/kani_metadata/src/artifact.rs @@ -99,7 +99,7 @@ mod test { #[test] fn test_convert_ok() { - let path = PathBuf::from("/tmp/my_file.rs").with_extension(&SymTabGoto); + let path = PathBuf::from("/tmp/my_file.rs").with_extension(SymTabGoto); let goto = convert_type(&path, SymTabGoto, Goto); assert_eq!(goto.as_os_str(), "/tmp/my_file.out"); @@ -109,7 +109,7 @@ mod test { #[test] fn test_set_extension_ok() { - let path = PathBuf::from("/tmp/my_file.rs").with_extension(&SymTabGoto); + let path = PathBuf::from("/tmp/my_file.rs").with_extension(SymTabGoto); assert_eq!(path.as_os_str(), "/tmp/my_file.symtab.out"); } } diff --git a/library/kani/Cargo.toml b/library/kani/Cargo.toml index 3ad1b286ebe6..a8c697e3d19f 100644 --- a/library/kani/Cargo.toml +++ b/library/kani/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani" -version = "0.56.0" +version = "0.57.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/kani/src/models/mod.rs b/library/kani/src/models/mod.rs index 2081ddf639df..af5ac336e09e 100644 --- a/library/kani/src/models/mod.rs +++ b/library/kani/src/models/mod.rs @@ -191,7 +191,7 @@ mod test { u64: From, { assert_eq!( - unsafe { u64::from(kani_intrinsic::simd_bitmask::<_, M, E, LANES>(mask.clone())) }, + unsafe { u64::from(kani_intrinsic::simd_bitmask::<_, M, E, LANES>(mask)) }, mask.to_bitmask() ); } @@ -220,8 +220,7 @@ mod test { let bitmask = mask.to_bitmask(); assert_eq!(bitmask, 0b1010); - let kani_mask = - unsafe { u64::from(kani_intrinsic::simd_bitmask::<_, u8, u32, 4>(mask.clone())) }; + let kani_mask = unsafe { u64::from(kani_intrinsic::simd_bitmask::<_, u8, u32, 4>(mask)) }; assert_eq!(kani_mask, bitmask); } } diff --git a/library/kani_core/Cargo.toml b/library/kani_core/Cargo.toml index df55e6278282..c214c64c0f02 100644 --- a/library/kani_core/Cargo.toml +++ b/library/kani_core/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_core" -version = "0.56.0" +version = "0.57.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/kani_macros/Cargo.toml b/library/kani_macros/Cargo.toml index a7876176adb2..13f20b96b6c7 100644 --- a/library/kani_macros/Cargo.toml +++ b/library/kani_macros/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_macros" -version = "0.56.0" +version = "0.57.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/std/Cargo.toml b/library/std/Cargo.toml index e1e353704723..08c033407fb4 100644 --- a/library/std/Cargo.toml +++ b/library/std/Cargo.toml @@ -5,7 +5,7 @@ # Note: this package is intentionally named std to make sure the names of # standard library symbols are preserved name = "std" -version = "0.56.0" +version = "0.57.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/rust-toolchain.toml b/rust-toolchain.toml index f7fb65c37ec5..75152d6384f4 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2024-12-13" +channel = "nightly-2024-12-19" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] diff --git a/scripts/ci/Dockerfile.bundle-release-20-04 b/scripts/ci/Dockerfile.bundle-release-20-04 index 7a8b7f21b74b..963aa952d6df 100644 --- a/scripts/ci/Dockerfile.bundle-release-20-04 +++ b/scripts/ci/Dockerfile.bundle-release-20-04 @@ -17,7 +17,7 @@ COPY ./target/package/kani-verifier-*[^e] ./kani-verifier # directory. Rustup is purged for space. RUN apt-get update && \ - apt-get install -y curl && \ + apt-get install -y curl build-essential && \ curl -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain none && \ (cd kani-verifier/; cargo) && \ rustup default $(rustup toolchain list | awk '{ print $1 }') && \ diff --git a/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04 b/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04 index 44084606f98d..f81af91f6f52 100644 --- a/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04 +++ b/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04 @@ -7,7 +7,7 @@ FROM ubuntu:20.04 ENV DEBIAN_FRONTEND=noninteractive \ DEBCONF_NONINTERACTIVE_SEEN=true RUN apt-get update && \ - apt-get install -y curl && \ + apt-get install -y curl build-essential && \ curl -sSf https://sh.rustup.rs | sh -s -- -y ENV PATH="/root/.cargo/bin:${PATH}" diff --git a/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04-alt b/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04-alt index ebba8e3a178b..35bc522b651f 100644 --- a/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04-alt +++ b/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04-alt @@ -9,7 +9,7 @@ ENV DEBIAN_FRONTEND=noninteractive \ DEBCONF_NONINTERACTIVE_SEEN=true \ KANI_HOME="/tmp" RUN apt-get update && \ - apt-get install -y curl && \ + apt-get install -y curl build-essential && \ curl -sSf https://sh.rustup.rs | sh -s -- -y ENV PATH="/root/.cargo/bin:${PATH}" diff --git a/scripts/ci/Dockerfile.bundle-test-ubuntu-22-04 b/scripts/ci/Dockerfile.bundle-test-ubuntu-22-04 index f53c11cf7fcb..f7dd23e1233d 100644 --- a/scripts/ci/Dockerfile.bundle-test-ubuntu-22-04 +++ b/scripts/ci/Dockerfile.bundle-test-ubuntu-22-04 @@ -7,7 +7,7 @@ FROM ubuntu:22.04 ENV DEBIAN_FRONTEND=noninteractive \ DEBCONF_NONINTERACTIVE_SEEN=true RUN apt-get update && \ - apt-get install -y curl && \ + apt-get install -y curl build-essential && \ curl -sSf https://sh.rustup.rs | sh -s -- -y ENV PATH="/root/.cargo/bin:${PATH}" diff --git a/scripts/ci/Dockerfile.bundle-test-ubuntu-24-04 b/scripts/ci/Dockerfile.bundle-test-ubuntu-24-04 index db4e8b88640d..1b85fd2e0b58 100644 --- a/scripts/ci/Dockerfile.bundle-test-ubuntu-24-04 +++ b/scripts/ci/Dockerfile.bundle-test-ubuntu-24-04 @@ -7,7 +7,7 @@ FROM ubuntu:24.04 ENV DEBIAN_FRONTEND=noninteractive \ DEBCONF_NONINTERACTIVE_SEEN=true RUN apt-get update && \ - apt-get install -y curl && \ + apt-get install -y curl build-essential && \ curl -sSf https://sh.rustup.rs | sh -s -- -y ENV PATH="/root/.cargo/bin:${PATH}" diff --git a/tests/expected/uninit/delayed-ub/expected b/tests/expected/uninit/delayed-ub/expected index dc0411bdba9c..b7c139c2d101 100644 --- a/tests/expected/uninit/delayed-ub/expected +++ b/tests/expected/uninit/delayed-ub/expected @@ -1,44 +1,44 @@ -delayed_ub_trigger_copy.assertion.1\ +delayed_ub_trigger_copy.assertion.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"\ -delayed_ub_slices.assertion.4\ +delayed_ub_slices.assertion.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `[u128; 4]`" -delayed_ub_structs.assertion.2\ +delayed_ub_structs.assertion.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `U`" -delayed_ub_double_copy.assertion.1\ +delayed_ub_double_copy.assertion.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"\ -delayed_ub_copy.assertion.1\ +delayed_ub_copy.assertion.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" -delayed_ub_closure_capture_laundered.assertion.2\ +delayed_ub_closure_capture_laundered.assertion.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" -delayed_ub_closure_laundered.assertion.2\ +delayed_ub_closure_laundered.assertion.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" -delayed_ub_laundered.assertion.2\ +delayed_ub_laundered.assertion.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" -delayed_ub_static.assertion.4\ +delayed_ub_static.assertion.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" -delayed_ub_transmute.assertion.2\ +delayed_ub_transmute.assertion.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" -delayed_ub.assertion.2\ +delayed_ub.assertion.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" diff --git a/tests/perf/s2n-quic b/tests/perf/s2n-quic index e4a236578bcb..ac52a4805a62 160000 --- a/tests/perf/s2n-quic +++ b/tests/perf/s2n-quic @@ -1 +1 @@ -Subproject commit e4a236578bcb36109d238753307c970d6c997666 +Subproject commit ac52a4805a62ca4c7c9d1c17e86ba41c2afd308f diff --git a/tools/build-kani/Cargo.toml b/tools/build-kani/Cargo.toml index 25e022e70d3f..ff5b3a406db1 100644 --- a/tools/build-kani/Cargo.toml +++ b/tools/build-kani/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "build-kani" -version = "0.56.0" +version = "0.57.0" edition = "2021" description = "Builds Kani, Sysroot and release bundle." license = "MIT OR Apache-2.0" @@ -11,6 +11,6 @@ publish = false [dependencies] anyhow = "1" -cargo_metadata = "0.18.0" +cargo_metadata = "0.19" clap = { version = "4.4.11", features=["derive"] } -which = "6" +which = "7" diff --git a/tools/build-kani/src/sysroot.rs b/tools/build-kani/src/sysroot.rs index 29d481e4b9dd..139dce794f13 100644 --- a/tools/build-kani/src/sysroot.rs +++ b/tools/build-kani/src/sysroot.rs @@ -13,7 +13,7 @@ use crate::{AutoRun, cp}; use anyhow::{Result, bail, format_err}; -use cargo_metadata::{Artifact, Message}; +use cargo_metadata::{Artifact, Message, TargetKind}; use std::ffi::OsStr; use std::fs; use std::io::BufReader; @@ -194,9 +194,13 @@ fn copy_artifacts(artifacts: &[Artifact], sysroot_lib: &Path, copy_std: bool) -> /// Check if an artifact is a rust library that can be used by rustc on further crates compilations. /// This inspects the kind of targets that this artifact originates from. fn is_rust_lib(artifact: &Artifact) -> bool { - artifact.target.kind.iter().any(|kind| match kind.as_str() { - "lib" | "rlib" | "proc-macro" => true, - "bin" | "dylib" | "cdylib" | "staticlib" | "custom-build" => false, + artifact.target.kind.iter().any(|kind| match kind { + TargetKind::Lib | TargetKind::RLib | TargetKind::ProcMacro => true, + TargetKind::Bin + | TargetKind::DyLib + | TargetKind::CDyLib + | TargetKind::StaticLib + | TargetKind::CustomBuild => false, _ => unreachable!("Unknown crate type {kind}"), }) } diff --git a/tools/kani-cov/Cargo.toml b/tools/kani-cov/Cargo.toml index 4b9f14cc3ca9..a2764791dcf1 100644 --- a/tools/kani-cov/Cargo.toml +++ b/tools/kani-cov/Cargo.toml @@ -17,5 +17,5 @@ console = "0.15.8" serde = "1.0.197" serde_derive = "1.0.197" serde_json = "1.0.115" -tree-sitter = "0.23.0" -tree-sitter-rust = "0.21.2" +tree-sitter = "0.24" +tree-sitter-rust = "0.23" diff --git a/tools/kani-cov/src/coverage.rs b/tools/kani-cov/src/coverage.rs index 96a3dfdb7353..0898010ea2d0 100644 --- a/tools/kani-cov/src/coverage.rs +++ b/tools/kani-cov/src/coverage.rs @@ -154,7 +154,7 @@ pub struct FunctionInfo { pub fn function_info_from_file(filepath: &PathBuf) -> Vec { let source_code = fs::read_to_string(filepath).expect("could not read source file"); let mut parser = Parser::new(); - parser.set_language(&tree_sitter_rust::language()).expect("Error loading Rust grammar"); + parser.set_language(&tree_sitter_rust::LANGUAGE.into()).expect("Error loading Rust grammar"); let tree = parser.parse(&source_code, None).expect("Failed to parse file");