From 7b39417c5d447c83fc4fd5be77d8d7ec76d4867b Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Fri, 21 Jul 2023 01:28:58 -0500 Subject: [PATCH 1/6] Automatic toolchain upgrade to nightly-2023-06-25 (#2603) Update Rust toolchain from nightly-2023-06-24 to nightly-2023-06-25 without any other source changes. Co-authored-by: celinval --- rust-toolchain.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 1935a8e3142a..98b700fbda14 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2023-06-24" +channel = "nightly-2023-06-25" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] From a27905f2e275ea7fb929d7567c2c62d7fefd02d7 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Fri, 21 Jul 2023 19:46:48 -0500 Subject: [PATCH 2/6] Bump CBMC version to 5.88.0 (#2614) --- kani-dependencies | 2 +- scripts/kani-regression.sh | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/kani-dependencies b/kani-dependencies index 498182678d6f..ec9b5f8c8919 100644 --- a/kani-dependencies +++ b/kani-dependencies @@ -1,4 +1,4 @@ -CBMC_VERSION="5.87.0" +CBMC_VERSION="5.88.0" # If you update this version number, remember to bump it in `src/setup.rs` too CBMC_VIEWER_VERSION="3.8" KISSAT_VERSION="3.0.0" diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh index 6710937004b8..fd04b579deb3 100755 --- a/scripts/kani-regression.sh +++ b/scripts/kani-regression.sh @@ -19,7 +19,7 @@ KANI_DIR=$SCRIPT_DIR/.. export KANI_FAIL_ON_UNEXPECTED_DESCRIPTION="true" # Required dependencies -check-cbmc-version.py --major 5 --minor 86 +check-cbmc-version.py --major 5 --minor 88 check-cbmc-viewer-version.py --major 3 --minor 8 check_kissat_version.sh From 18e657a281313cdfd010bc71f4ce3c34aa9e8be2 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Sun, 23 Jul 2023 07:34:39 -0500 Subject: [PATCH 3/6] Upgrade Rust toolchain to nightly-2023-07-01 (#2616) --- kani-compiler/src/kani_compiler.rs | 2 ++ kani-compiler/src/session.rs | 5 ++++- rust-toolchain.toml | 2 +- 3 files changed, 7 insertions(+), 2 deletions(-) diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index cdb17b8cd0ac..2a5e4c188578 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/kani-compiler/src/kani_compiler.rs @@ -33,6 +33,7 @@ use rustc_hir::definitions::DefPathHash; use rustc_interface::Config; use rustc_middle::ty::TyCtxt; use rustc_session::config::{ErrorOutputType, OutputType}; +use rustc_session::EarlyErrorHandler; use rustc_span::ErrorGuaranteed; use std::collections::{BTreeMap, HashMap}; use std::fs::File; @@ -370,6 +371,7 @@ impl Callbacks for KaniCompiler { /// During the initialization state, we collect the crate harnesses and prepare for codegen. fn after_analysis<'tcx>( &mut self, + _handler: &EarlyErrorHandler, _compiler: &rustc_interface::interface::Compiler, rustc_queries: &'tcx rustc_interface::Queries<'tcx>, ) -> Compilation { diff --git a/kani-compiler/src/session.rs b/kani-compiler/src/session.rs index 6061554200dc..c19501c4a62e 100644 --- a/kani-compiler/src/session.rs +++ b/kani-compiler/src/session.rs @@ -9,6 +9,8 @@ use rustc_errors::{ emitter::Emitter, emitter::HumanReadableErrorType, fallback_fluent_bundle, json::JsonEmitter, ColorConfig, Diagnostic, TerminalUrl, }; +use rustc_session::config::ErrorOutputType; +use rustc_session::EarlyErrorHandler; use std::io::IsTerminal; use std::panic; use std::str::FromStr; @@ -71,7 +73,8 @@ pub fn init_session(args: &ArgMatches, json_hook: bool) { // Initialize the rustc logger using value from RUSTC_LOG. We keep the log control separate // because we cannot control the RUSTC log format unless if we match the exact tracing // version used by RUSTC. - rustc_driver::init_rustc_env_logger(); + let handler = EarlyErrorHandler::new(ErrorOutputType::default()); + rustc_driver::init_rustc_env_logger(&handler); // Install Kani panic hook. if json_hook { diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 98b700fbda14..f672b2397f5a 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2023-06-25" +channel = "nightly-2023-07-01" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] From dfe1e95fee1282a88c0c80df06d4342c1d478c39 Mon Sep 17 00:00:00 2001 From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Date: Tue, 25 Jul 2023 10:25:34 -0700 Subject: [PATCH 4/6] Bump CBMC version (#2623) --- kani-dependencies | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-dependencies b/kani-dependencies index ec9b5f8c8919..e84748cef527 100644 --- a/kani-dependencies +++ b/kani-dependencies @@ -1,4 +1,4 @@ -CBMC_VERSION="5.88.0" +CBMC_VERSION="5.88.1" # If you update this version number, remember to bump it in `src/setup.rs` too CBMC_VIEWER_VERSION="3.8" KISSAT_VERSION="3.0.0" From 5bc61f5b72c5b13a89c4f79a8d8b68ed8d06db7b Mon Sep 17 00:00:00 2001 From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Date: Tue, 25 Jul 2023 12:01:52 -0700 Subject: [PATCH 5/6] Bump dependencies (#2624) --- Cargo.lock | 152 ++++++++++++++++++++--------------------- kani-driver/Cargo.toml | 2 +- 2 files changed, 77 insertions(+), 77 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 0847cd2f318a..9e6ef0d642dc 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -83,9 +83,9 @@ dependencies = [ [[package]] name = "anyhow" -version = "1.0.71" +version = "1.0.72" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9c7d0618f0e0b7e8ff11427422b64564d5fb0be1940354bfe2e0529b18a9d9b8" +checksum = "3b13c32d80ecc7ab747b80c3784bce54ee8a7a0cc4fbda9bf4cda2cf6fe90854" [[package]] name = "autocfg" @@ -130,18 +130,18 @@ dependencies = [ [[package]] name = "camino" -version = "1.1.4" +version = "1.1.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c530edf18f37068ac2d977409ed5cd50d53d73bc653c7647b48eb78976ac9ae2" +checksum = "c59e92b5a388f549b863a7bea62612c09f24c8393560709a54558a9abdfb3b9c" dependencies = [ "serde", ] [[package]] name = "cargo-platform" -version = "0.1.2" +version = "0.1.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "cbdb825da8a5df079a43676dbe042702f1707b1109f713a01420fbb4cc71fa27" +checksum = "2cfa25e60aea747ec7e1124f238816749faa93759c6ff5b31f1ccdda137f4479" dependencies = [ "serde", ] @@ -174,9 +174,9 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" [[package]] name = "clap" -version = "4.3.11" +version = "4.3.19" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1640e5cc7fb47dbb8338fd471b105e7ed6c3cb2aeb00c2e067127ffd3764a05d" +checksum = "5fd304a20bff958a57f04c4e96a2e7594cc4490a0e809cbd48bb6437edaa452d" dependencies = [ "clap_builder", "clap_derive", @@ -185,9 +185,9 @@ dependencies = [ [[package]] name = "clap_builder" -version = "4.3.11" +version = "4.3.19" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "98c59138d527eeaf9b53f35a77fcc1fad9d883116070c63d5de1c7dc7b00c72b" +checksum = "01c6a3f08f1fe5662a35cfe393aec09c4df95f60ee93b7556505260f75eee9e1" dependencies = [ "anstream", "anstyle", @@ -198,14 +198,14 @@ dependencies = [ [[package]] name = "clap_derive" -version = "4.3.2" +version = "4.3.12" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b8cd2b2a819ad6eec39e8f1d6b53001af1e5469f8c177579cdaeb313115b825f" +checksum = "54a9bb5758fc5dfe728d1019941681eccaf0cf8a4189b692a0ee2f2ecf90a050" dependencies = [ "heck", "proc-macro2", "quote", - "syn 2.0.25", + "syn 2.0.27", ] [[package]] @@ -222,9 +222,9 @@ checksum = "acbf1af155f9b9ef647e42cdc158db4b64a1b61f743629225fde6f3e0be2a7c7" [[package]] name = "comfy-table" -version = "6.2.0" +version = "7.0.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7e959d788268e3bf9d35ace83e81b124190378e4c91c9067524675e33394b8ba" +checksum = "9ab77dbd8adecaf3f0db40581631b995f312a8a5ae3aa9993188bb8f23d83a5b" dependencies = [ "crossterm", "strum", @@ -347,9 +347,9 @@ dependencies = [ [[package]] name = "either" -version = "1.8.1" +version = "1.9.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7fcaabb2fef8c910e7f4c7ce9f67a1283a1715879a7c230ca9d6d1ae31f16d91" +checksum = "a26ae43d7bcc3b814de94796a5e736d4029efb0ee900c12e2d54c993ad1a1e07" [[package]] name = "encode_unicode" @@ -359,9 +359,9 @@ checksum = "a357d28ed41a50f9c765dbfe56cbc04a64e53e5fc58ba79fbc34c10ef3df831f" [[package]] name = "equivalent" -version = "1.0.0" +version = "1.0.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "88bffebc5d80432c9b140ee17875ff173a8ab62faad5b257da912bd2f6c1c0a1" +checksum = "5443807d6dff69373d433ab9ef5378ad8df50ca6298caf15de6e52e24aaf54d5" [[package]] name = "errno" @@ -478,9 +478,9 @@ dependencies = [ [[package]] name = "itoa" -version = "1.0.8" +version = "1.0.9" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "62b02a5381cc465bd3041d84623d0fa3b66738b52b8e2fc3bab8ad63ab032f4a" +checksum = "af150ab688ff2122fcef229be89cb50dd66af9e01a4ff320cc137eecc9bacc38" [[package]] name = "kani" @@ -553,7 +553,7 @@ dependencies = [ "proc-macro-error", "proc-macro2", "quote", - "syn 2.0.25", + "syn 2.0.27", ] [[package]] @@ -664,9 +664,9 @@ dependencies = [ [[package]] name = "num" -version = "0.4.0" +version = "0.4.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "43db66d1170d347f9a065114077f7dccb00c1b9478c89384490a3425279a4606" +checksum = "b05180d69e3da0e530ba2a1dae5110317e49e3b7f3d41be227dc5f92e49ee7af" dependencies = [ "num-bigint", "num-complex", @@ -731,9 +731,9 @@ dependencies = [ [[package]] name = "num-traits" -version = "0.2.15" +version = "0.2.16" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "578ede34cf02f8924ab9447f50c28075b4d3e5b269972345e7e0372b38c6cdcd" +checksum = "f30b0abd723be7e2ffca1272140fac1a2f084c77ec3e123c192b66af1ee9e6c2" dependencies = [ "autocfg", ] @@ -837,9 +837,9 @@ dependencies = [ [[package]] name = "proc-macro2" -version = "1.0.64" +version = "1.0.66" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "78803b62cbf1f46fde80d7c0e803111524b9877184cfe7c3033659490ac7a7da" +checksum = "18fb31db3f9bddb2ea821cde30a9f70117e3f119938b5ee630b7403aa6e2ead9" dependencies = [ "unicode-ident", ] @@ -857,9 +857,9 @@ dependencies = [ [[package]] name = "quote" -version = "1.0.29" +version = "1.0.32" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "573015e8ab27661678357f27dc26460738fd2b6c86e46f386fde94cb5d913105" +checksum = "50f3b39ccfb720540debaa0164757101c08ecb8d326b15358ce76a62c7e85965" dependencies = [ "proc-macro2", ] @@ -933,8 +933,8 @@ checksum = "b2eae68fc220f7cf2532e4494aded17545fce192d59cd996e0fe7887f4ceb575" dependencies = [ "aho-corasick", "memchr", - "regex-automata 0.3.2", - "regex-syntax 0.7.3", + "regex-automata 0.3.3", + "regex-syntax 0.7.4", ] [[package]] @@ -948,13 +948,13 @@ dependencies = [ [[package]] name = "regex-automata" -version = "0.3.2" +version = "0.3.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "83d3daa6976cffb758ec878f108ba0e062a45b2d6ca3a2cca965338855476caf" +checksum = "39354c10dd07468c2e73926b23bb9c2caca74c5501e38a35da70406f1d923310" dependencies = [ "aho-corasick", "memchr", - "regex-syntax 0.7.3", + "regex-syntax 0.7.4", ] [[package]] @@ -965,9 +965,9 @@ checksum = "f162c6dd7b008981e4d40210aca20b4bd0f9b60ca9271061b07f78537722f2e1" [[package]] name = "regex-syntax" -version = "0.7.3" +version = "0.7.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2ab07dc67230e4a4718e70fd5c20055a4334b121f1f9db8fe63ef39ce9b8c846" +checksum = "e5ea92a5b6195c6ef2a0295ea818b312502c6fc94dde986c5553242e18fd4ce2" [[package]] name = "rustc-demangle" @@ -984,9 +984,9 @@ dependencies = [ [[package]] name = "rustix" -version = "0.38.3" +version = "0.38.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ac5ffa1efe7548069688cd7028f32591853cd7b5b756d41bcffd2353e4fc75b4" +checksum = "0a962918ea88d644592894bc6dc55acc6c0956488adcebbfb6e273506b7fd6e5" dependencies = [ "bitflags 2.3.3", "errno", @@ -997,15 +997,15 @@ dependencies = [ [[package]] name = "rustversion" -version = "1.0.13" +version = "1.0.14" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "dc31bd9b61a32c31f9650d18add92aa83a49ba979c143eefd27fe7177b05bd5f" +checksum = "7ffc183a10b4478d04cbbbfc96d0873219d962dd5accaff2ffbd4ceb7df837f4" [[package]] name = "ryu" -version = "1.0.14" +version = "1.0.15" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fe232bdf6be8c8de797b22184ee71118d63780ea42ac85b61d1baa6d3b782ae9" +checksum = "1ad4cc8da4ef723ed60bced201181d83791ad433213d8c24efffda1eec85d741" [[package]] name = "same-file" @@ -1018,44 +1018,44 @@ dependencies = [ [[package]] name = "scopeguard" -version = "1.1.0" +version = "1.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d29ab0c6d3fc0ee92fe66e2d99f700eab17a8d57d1c1d3b748380fb20baa78cd" +checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49" [[package]] name = "semver" -version = "1.0.17" +version = "1.0.18" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bebd363326d05ec3e2f532ab7660680f3b02130d780c299bca73469d521bc0ed" +checksum = "b0293b4b29daaf487284529cc2f5675b8e57c61f70167ba415a463651fd6a918" dependencies = [ "serde", ] [[package]] name = "serde" -version = "1.0.171" +version = "1.0.175" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "30e27d1e4fd7659406c492fd6cfaf2066ba8773de45ca75e855590f856dc34a9" +checksum = "5d25439cd7397d044e2748a6fe2432b5e85db703d6d097bd014b3c0ad1ebff0b" dependencies = [ "serde_derive", ] [[package]] name = "serde_derive" -version = "1.0.171" +version = "1.0.175" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "389894603bd18c46fa56231694f8d827779c0951a667087194cf9de94ed24682" +checksum = "b23f7ade6f110613c0d63858ddb8b94c1041f550eab58a16b371bdf2c9c80ab4" dependencies = [ "proc-macro2", "quote", - "syn 2.0.25", + "syn 2.0.27", ] [[package]] name = "serde_json" -version = "1.0.100" +version = "1.0.103" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0f1e14e89be7aa4c4b78bdbdc9eb5bf8517829a600ae8eaa39a6e1d960b5185c" +checksum = "d03b412469450d4404fe8499a268edd7f8b79fecb074b0d812ad64ca21f4031b" dependencies = [ "itoa", "ryu", @@ -1073,18 +1073,18 @@ dependencies = [ [[package]] name = "serde_test" -version = "1.0.171" +version = "1.0.175" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b6480a2f4e1449ec9757ea143362ad5cea79bc7f1cb7711c06e1c5d03b6b5a3a" +checksum = "29baf0f77ca9ad9c6ed46e1b408b5e0f30b5184bcd66884e7f6d36bd7a65a8a4" dependencies = [ "serde", ] [[package]] name = "serde_yaml" -version = "0.9.22" +version = "0.9.25" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "452e67b9c20c37fa79df53201dc03839651086ed9bbe92b3ca585ca9fdaa7d85" +checksum = "1a49e178e4452f45cb61d0cd8cebc1b0fafd3e41929e996cef79aa3aca91f574" dependencies = [ "indexmap", "itoa", @@ -1110,9 +1110,9 @@ checksum = "24188a676b6ae68c3b2cb3a01be17fbf7240ce009799bb56d5b1409051e78fde" [[package]] name = "signal-hook" -version = "0.3.15" +version = "0.3.17" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "732768f1176d21d09e076c23a93123d40bba92d50c4058da34d45c8de8e682b9" +checksum = "8621587d4798caf8eb44879d42e56b9a93ea5dcd315a6487c357130095b62801" dependencies = [ "libc", "signal-hook-registry", @@ -1200,9 +1200,9 @@ dependencies = [ [[package]] name = "syn" -version = "2.0.25" +version = "2.0.27" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "15e3fc8c0c74267e2df136e5e5fb656a464158aa57624053375eb9c8c6e25ae2" +checksum = "b60f673f44a8255b9c8c657daf66a596d435f2da81a555b06dc644d080ba45e0" dependencies = [ "proc-macro2", "quote", @@ -1211,22 +1211,22 @@ dependencies = [ [[package]] name = "thiserror" -version = "1.0.43" +version = "1.0.44" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a35fc5b8971143ca348fa6df4f024d4d55264f3468c71ad1c2f365b0a4d58c42" +checksum = "611040a08a0439f8248d1990b111c95baa9c704c805fa1f62104b39655fd7f90" dependencies = [ "thiserror-impl", ] [[package]] name = "thiserror-impl" -version = "1.0.43" +version = "1.0.44" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "463fe12d7993d3b327787537ce8dd4dfa058de32fc2b195ef3cde03dc4771e8f" +checksum = "090198534930841fab3a5d1bb637cde49e339654e606195f8d9c76eeb081dc96" dependencies = [ "proc-macro2", "quote", - "syn 2.0.25", + "syn 2.0.27", ] [[package]] @@ -1262,9 +1262,9 @@ dependencies = [ [[package]] name = "toml_edit" -version = "0.19.12" +version = "0.19.14" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c500344a19072298cd05a7224b3c0c629348b78692bf48466c5238656e315a78" +checksum = "f8123f27e969974a3dfba720fdb560be359f57b44302d280ba72e76a74480e8a" dependencies = [ "indexmap", "serde", @@ -1293,7 +1293,7 @@ checksum = "5f4f31f56159e98206da9efd823404b79b6ef3143b4a7ab76e67b1751b25a4ab" dependencies = [ "proc-macro2", "quote", - "syn 2.0.25", + "syn 2.0.27", ] [[package]] @@ -1360,9 +1360,9 @@ dependencies = [ [[package]] name = "unicode-ident" -version = "1.0.10" +version = "1.0.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "22049a19f4a68748a168c0fc439f9516686aa045927ff767eca0a85101fb6e73" +checksum = "301abaae475aa91687eb82514b328ab47a211a533026cb25fc3e519b86adfc3c" [[package]] name = "unicode-width" @@ -1372,9 +1372,9 @@ checksum = "c0edd1e5b14653f783770bce4a4dabb4a5108a5370a5f5d8cfe8710c361f6c8b" [[package]] name = "unsafe-libyaml" -version = "0.2.8" +version = "0.2.9" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1865806a559042e51ab5414598446a5871b561d21b6764f2eabb0dd481d880a6" +checksum = "f28467d3e1d3c6586d8f25fa243f544f5800fec42d97032474e17222c2b75cfa" [[package]] name = "utf8parse" @@ -1595,9 +1595,9 @@ checksum = "1a515f5799fe4961cb532f983ce2b23082366b898e52ffbce459c86f67c8378a" [[package]] name = "winnow" -version = "0.4.9" +version = "0.5.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "81a2094c43cc94775293eaa0e499fbc30048a6d824ac82c0351a8c0bf9112529" +checksum = "25b5872fa2e10bd067ae946f927e726d7d603eaeb6e02fa6a350e0722d2b8c11" dependencies = [ "memchr", ] diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index a4385206f83f..19f31d2a4287 100644 --- a/kani-driver/Cargo.toml +++ b/kani-driver/Cargo.toml @@ -26,7 +26,7 @@ regex = "1.6" rustc-demangle = "0.1.21" pathdiff = "0.2.1" rayon = "1.5.3" -comfy-table = "6.0.0" +comfy-table = "7.0.1" strum = {version = "0.24.0"} strum_macros = {version = "0.24.0"} tracing = {version = "0.1", features = ["max_level_trace", "release_max_level_debug"]} From 319d859bf2fc32e6025b9844538615f612b9788e Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Tue, 25 Jul 2023 15:43:56 -0400 Subject: [PATCH 6/6] Adds support for sysconf (#2557) Signed-off-by: Felipe R. Monteiro --- cprover_bindings/src/goto_program/builtin.rs | 5 ++++ cprover_bindings/src/goto_program/typ.rs | 24 +++++++++++++++++-- cprover_bindings/src/irep/to_irep.rs | 5 ++++ .../src/codegen_cprover_gotoc/codegen/typ.rs | 1 + tests/kani/LibC/sysconf.rs | 12 ++++++++++ 5 files changed, 45 insertions(+), 2 deletions(-) create mode 100644 tests/kani/LibC/sysconf.rs diff --git a/cprover_bindings/src/goto_program/builtin.rs b/cprover_bindings/src/goto_program/builtin.rs index 258691b9ade4..95c38d7e0f8a 100644 --- a/cprover_bindings/src/goto_program/builtin.rs +++ b/cprover_bindings/src/goto_program/builtin.rs @@ -61,6 +61,7 @@ pub enum BuiltinFn { Sinf, Sqrt, Sqrtf, + Sysconf, Trunc, Truncf, Unlink, @@ -124,6 +125,7 @@ impl ToString for BuiltinFn { Sinf => "sinf", Sqrt => "sqrt", Sqrtf => "sqrtf", + Sysconf => "sysconf", Trunc => "trunc", Truncf => "truncf", Unlink => "unlink", @@ -188,6 +190,7 @@ impl BuiltinFn { Sinf => vec![Type::float()], Sqrt => vec![Type::double()], Sqrtf => vec![Type::float()], + Sysconf => vec![Type::c_int()], Trunc => vec![Type::double()], Truncf => vec![Type::float()], Unlink => vec![Type::c_char().to_pointer()], @@ -251,6 +254,7 @@ impl BuiltinFn { Sinf => Type::float(), Sqrt => Type::double(), Sqrtf => Type::float(), + Sysconf => Type::c_long_int(), Trunc => Type::double(), Truncf => Type::float(), Unlink => Type::c_int(), @@ -314,6 +318,7 @@ impl BuiltinFn { Sinf, Sqrt, Sqrtf, + Sysconf, Trunc, Truncf, Unlink, diff --git a/cprover_bindings/src/goto_program/typ.rs b/cprover_bindings/src/goto_program/typ.rs index a038b8dee779..9d1649b99cd1 100644 --- a/cprover_bindings/src/goto_program/typ.rs +++ b/cprover_bindings/src/goto_program/typ.rs @@ -27,7 +27,7 @@ pub enum Type { Bool, /// `typ x : width`. e.g. `unsigned int x: 3`. CBitField { typ: Box, width: u64 }, - /// Machine dependent integers: `bool`, `char`, `int`, `size_t`, etc. + /// Machine dependent integers: `bool`, `char`, `int`, `long int`, `size_t`, etc. CInteger(CIntType), /// `return_type x(parameters)` Code { parameters: Vec, return_type: Box }, @@ -83,6 +83,8 @@ pub enum CIntType { Char, /// `int` Int, + /// `long int` + LongInt, /// `size_t` SizeT, /// `ssize_t` @@ -232,6 +234,7 @@ impl CIntType { CIntType::Bool => st.machine_model().bool_width, CIntType::Char => st.machine_model().char_width, CIntType::Int => st.machine_model().int_width, + CIntType::LongInt => st.machine_model().long_int_width, CIntType::SizeT => st.machine_model().pointer_width, CIntType::SSizeT => st.machine_model().pointer_width, } @@ -287,6 +290,7 @@ impl Type { CInteger(CIntType::Bool) => Some(mm.bool_width), CInteger(CIntType::Char) => Some(mm.char_width), CInteger(CIntType::Int) => Some(mm.int_width), + CInteger(CIntType::LongInt) => Some(mm.long_int_width), Signedbv { width } | Unsignedbv { width } => Some(*width), _ => None, } @@ -450,6 +454,14 @@ impl Type { } } + pub fn is_long_int(&self) -> bool { + let concrete = self.unwrap_typedef(); + match concrete { + Type::CInteger(CIntType::LongInt) => true, + _ => false, + } + } + pub fn is_c_size_t(&self) -> bool { let concrete = self.unwrap_typedef(); match concrete { @@ -637,7 +649,10 @@ impl Type { pub fn is_signed(&self, mm: &MachineModel) -> bool { let concrete = self.unwrap_typedef(); match concrete { - CInteger(CIntType::Int) | CInteger(CIntType::SSizeT) | Signedbv { .. } => true, + CInteger(CIntType::Int) + | CInteger(CIntType::LongInt) + | CInteger(CIntType::SSizeT) + | Signedbv { .. } => true, CInteger(CIntType::Char) => !mm.char_is_unsigned, _ => false, } @@ -963,6 +978,10 @@ impl Type { CInteger(CIntType::Int) } + pub fn c_long_int() -> Self { + CInteger(CIntType::LongInt) + } + pub fn c_size_t() -> Self { CInteger(CIntType::SizeT) } @@ -1471,6 +1490,7 @@ mod type_tests { assert_eq!(type_def.is_empty(), src_type.is_empty()); assert_eq!(type_def.is_double(), src_type.is_double()); assert_eq!(type_def.is_bool(), src_type.is_bool()); + assert_eq!(type_def.is_long_int(), src_type.is_long_int()); assert_eq!(type_def.is_array(), src_type.is_array()); assert_eq!(type_def.is_array_like(), src_type.is_array_like()); assert_eq!(type_def.is_union(), src_type.is_union()); diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs index 70810e403c54..904221a0a85a 100644 --- a/cprover_bindings/src/irep/to_irep.rs +++ b/cprover_bindings/src/irep/to_irep.rs @@ -589,6 +589,11 @@ impl ToIrep for Type { sub: vec![], named_sub: linear_map![(IrepId::Width, Irep::just_int_id(mm.int_width),)], }, + Type::CInteger(CIntType::LongInt) => Irep { + id: IrepId::Signedbv, + sub: vec![], + named_sub: linear_map![(IrepId::Width, Irep::just_int_id(mm.long_int_width),)], + }, Type::CInteger(CIntType::SizeT) => Irep { id: IrepId::Unsignedbv, sub: vec![], diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 69da5f1c7ad1..881dec1765f9 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -157,6 +157,7 @@ impl<'tcx> GotocCtx<'tcx> { cbmc::goto_program::CIntType::Bool => "bool", cbmc::goto_program::CIntType::Char => "char", cbmc::goto_program::CIntType::Int => "int", + cbmc::goto_program::CIntType::LongInt => "long int", cbmc::goto_program::CIntType::SizeT => "size_t", cbmc::goto_program::CIntType::SSizeT => "ssize_t", }; diff --git a/tests/kani/LibC/sysconf.rs b/tests/kani/LibC/sysconf.rs new file mode 100644 index 000000000000..5a17dfde34eb --- /dev/null +++ b/tests/kani/LibC/sysconf.rs @@ -0,0 +1,12 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +//! Check support for `sysconf`. + +#![feature(rustc_private)] +extern crate libc; + +#[kani::proof] +fn main() { + let page_size = unsafe { libc::sysconf(libc::_SC_PAGESIZE) } as usize; +}