diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index aa120dafb790..74af1c0be544 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -68,17 +68,23 @@ jobs: df -h # This is required before checkout because the container does not - # have Git installed, so cannot run checkout action. The checkout - # action requires Git >=2.18, so use the Git maintainers' PPA. + # have Git installed, so cannot run checkout action. + # The checkout action requires Git >=2.18 and python 3.7, so use the Git maintainers' PPA. + # and the "deadsnakes" PPA, as the default version of python on ubuntu 22.04 is Python 3.10 - name: Install system dependencies run: | apt-get update apt-get install -y software-properties-common apt-utils add-apt-repository ppa:git-core/ppa + add-apt-repository ppa:deadsnakes/ppa apt-get update apt-get install -y \ build-essential bash-completion curl lsb-release sudo g++ gcc flex \ - bison make patch git + bison make patch git python3.7 python3.7-dev python3.7-distutils + update-alternatives --install /usr/bin/python3 python3 /usr/bin/python3.7 1 + curl -s https://bootstrap.pypa.io/get-pip.py -o get-pip.py + python3 get-pip.py --force-reinstall + rm get-pip.py - name: Checkout Kani uses: actions/checkout@v3 diff --git a/CHANGELOG.md b/CHANGELOG.md index d93685e865be..dd24e2c19b08 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -8,8 +8,19 @@ This file was introduced starting Kani 0.23.0, so it only contains changes from ### Breaking Changes +* Set minimum python to 3.7 in docker container and release action by @remi-delmas-3000 in https://github.com/model-checking/kani/pull/2879 * Delete `any_slice` which has been deprecated since Kani 0.38.0. by @zhassan-aws in https://github.com/model-checking/kani/pull/2860 +### What's Changed + +* Make `cover` const by @jswrenn in https://github.com/model-checking/kani/pull/2867 +* Change `expect()` from taking formatted strings to use `unwrap_or_else()` by @matthiaskrgr in https://github.com/model-checking/kani/pull/2865 +* Fix setup for `aarch64-unknown-linux-gnu` platform by @adpaco-aws in https://github.com/model-checking/kani/pull/2864 +* Do not override `std` library during playback by @celinval in https://github.com/model-checking/kani/pull/2852 +* Rust toolchain upgraded to `nightly-2023-11-11` by @zhassan-aws + +**Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.40.0...kani-0.41.0 + ## [0.40.0] ### What's Changed @@ -65,7 +76,7 @@ https://github.com/model-checking/kani/compare/kani-0.38.0...kani-0.39.0 * Fix expected value for `pref_align_of` under aarch64/macos by @remi-delmas-3000 in https://github.com/model-checking/kani/pull/2782 * Bump CBMC version to 5.92.0 by @zhassan-aws in https://github.com/model-checking/kani/pull/2771 * Upgrade to Kissat 3.1.1 by @zhassan-aws in https://github.com/model-checking/kani/pull/2756 -* Rust toolchain upgraded to `nightly-2023-09-19` by @remi-delmas-3000 @tautschnig +* Rust toolchain upgraded to `nightly-2023-09-19` by @remi-delmas-3000 @tautschnig **Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.36.0...kani-0.37.0 diff --git a/Cargo.lock b/Cargo.lock index fc70bbf7808a..70173c6c8b67 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -119,7 +119,7 @@ dependencies = [ [[package]] name = "build-kani" -version = "0.40.0" +version = "0.41.0" dependencies = [ "anyhow", "cargo_metadata", @@ -167,9 +167,9 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" [[package]] name = "clap" -version = "4.4.7" +version = "4.4.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ac495e00dcec98c83465d5ad66c5c4fabd652fd6686e7c6269b117e729a6f17b" +checksum = "2275f18819641850fa26c89acc84d465c1bf91ce57bc2748b28c420473352f64" dependencies = [ "clap_builder", "clap_derive", @@ -177,9 +177,9 @@ dependencies = [ [[package]] name = "clap_builder" -version = "4.4.7" +version = "4.4.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c77ed9a32a62e6ca27175d00d29d05ca32e396ea1eb5fb01d8256b669cec7663" +checksum = "07cdf1b148b25c1e1f7a42225e30a0d99a615cd4637eae7365548dd4529b95bc" dependencies = [ "anstream", "anstyle", @@ -196,7 +196,7 @@ dependencies = [ "heck", "proc-macro2", "quote", - "syn 2.0.38", + "syn 2.0.39", ] [[package]] @@ -255,7 +255,7 @@ dependencies = [ [[package]] name = "cprover_bindings" -version = "0.40.0" +version = "0.41.0" dependencies = [ "lazy_static", "linear-map", @@ -343,9 +343,9 @@ checksum = "5443807d6dff69373d433ab9ef5378ad8df50ca6298caf15de6e52e24aaf54d5" [[package]] name = "errno" -version = "0.3.5" +version = "0.3.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ac3e13f66a2f95e32a39eaa81f6b95d42878ca0e1db0c7543723dfe12557e860" +checksum = "f258a7194e7f7c2a7837a8913aeab7fd8c383457034fa20ce4dd3dcb813e8eb8" dependencies = [ "libc", "windows-sys 0.48.0", @@ -368,9 +368,9 @@ dependencies = [ [[package]] name = "getrandom" -version = "0.2.10" +version = "0.2.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "be4136b2a15dd319360be1c07d9933517ccf0be8f16bf62a3bee4f0d618df427" +checksum = "fe9006bed769170c11f845cf00c7c1e9092aeb3f268e007c3e760ac68008070f" dependencies = [ "cfg-if", "libc", @@ -415,9 +415,9 @@ dependencies = [ [[package]] name = "indexmap" -version = "2.0.2" +version = "2.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8adf3ddd720272c6ea8bf59463c04e0f93d0bbf7c5439b691bca2987e0270897" +checksum = "d530e1a18b1cb4c484e6e34556a0d948706958449fca0cab753d649f2bce3d1f" dependencies = [ "equivalent", "hashbrown 0.14.2", @@ -440,14 +440,14 @@ checksum = "af150ab688ff2122fcef229be89cb50dd66af9e01a4ff320cc137eecc9bacc38" [[package]] name = "kani" -version = "0.40.0" +version = "0.41.0" dependencies = [ "kani_macros", ] [[package]] name = "kani-compiler" -version = "0.40.0" +version = "0.41.0" dependencies = [ "clap", "cprover_bindings", @@ -468,7 +468,7 @@ dependencies = [ [[package]] name = "kani-driver" -version = "0.40.0" +version = "0.41.0" dependencies = [ "anyhow", "cargo_metadata", @@ -496,7 +496,7 @@ dependencies = [ [[package]] name = "kani-verifier" -version = "0.40.0" +version = "0.41.0" dependencies = [ "anyhow", "home", @@ -505,17 +505,17 @@ dependencies = [ [[package]] name = "kani_macros" -version = "0.40.0" +version = "0.41.0" dependencies = [ "proc-macro-error", "proc-macro2", "quote", - "syn 2.0.38", + "syn 2.0.39", ] [[package]] name = "kani_metadata" -version = "0.40.0" +version = "0.41.0" dependencies = [ "clap", "cprover_bindings", @@ -532,9 +532,9 @@ checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646" [[package]] name = "libc" -version = "0.2.149" +version = "0.2.150" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a08173bc88b7955d1b3145aa561539096c421ac8debde8cbc3612ec635fee29b" +checksum = "89d92a4743f9a61002fae18374ed11e7973f530cb3a3255fb354818118b2203c" [[package]] name = "linear-map" @@ -548,9 +548,9 @@ dependencies = [ [[package]] name = "linux-raw-sys" -version = "0.4.10" +version = "0.4.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "da2479e8c062e40bf0066ffa0bc823de0a9368974af99c9f6df941d2c231e03f" +checksum = "969488b55f8ac402214f3f5fd243ebb7206cf82de60d3172994707a4bcc2b829" [[package]] name = "lock_api" @@ -918,9 +918,9 @@ dependencies = [ [[package]] name = "rustix" -version = "0.38.21" +version = "0.38.24" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2b426b0506e5d50a7d8dafcf2e81471400deb602392c7dd110815afb4eaf02a3" +checksum = "9ad981d6c340a49cdc40a1028d9c6084ec7e9fa33fcb839cab656a267071e234" dependencies = [ "bitflags 2.4.1", "errno", @@ -967,22 +967,22 @@ dependencies = [ [[package]] name = "serde" -version = "1.0.190" +version = "1.0.192" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "91d3c334ca1ee894a2c6f6ad698fe8c435b76d504b13d436f0685d648d6d96f7" +checksum = "bca2a08484b285dcb282d0f67b26cadc0df8b19f8c12502c13d966bf9482f001" dependencies = [ "serde_derive", ] [[package]] name = "serde_derive" -version = "1.0.190" +version = "1.0.192" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "67c5609f394e5c2bd7fc51efda478004ea80ef42fee983d5c67a65e34f32c0e3" +checksum = "d6c7207fbec9faa48073f3e3074cbe553af6ea512d7c21ba46e434e70ea9fbc1" dependencies = [ "proc-macro2", "quote", - "syn 2.0.38", + "syn 2.0.39", ] [[package]] @@ -1044,13 +1044,13 @@ checksum = "24188a676b6ae68c3b2cb3a01be17fbf7240ce009799bb56d5b1409051e78fde" [[package]] name = "smallvec" -version = "1.11.1" +version = "1.11.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "942b4a808e05215192e39f4ab80813e599068285906cc91aa64f923db842bd5a" +checksum = "4dccd0940a2dcdf68d092b8cbab7dc0ad8fa938bf95787e1b916b0e3d0e8e970" [[package]] name = "std" -version = "0.40.0" +version = "0.41.0" dependencies = [ "kani", ] @@ -1088,7 +1088,7 @@ dependencies = [ "proc-macro2", "quote", "rustversion", - "syn 2.0.38", + "syn 2.0.39", ] [[package]] @@ -1103,9 +1103,9 @@ dependencies = [ [[package]] name = "syn" -version = "2.0.38" +version = "2.0.39" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e96b79aaa137db8f61e26363a0c9b47d8b4ec75da28b7d1d614c2303e232408b" +checksum = "23e78b90f2fcf45d3e842032ce32e3f2d1545ba6636271dcbf24fa306d87be7a" dependencies = [ "proc-macro2", "quote", @@ -1142,7 +1142,7 @@ checksum = "266b2e40bc00e5a6c09c3584011e08b06f123c00362c92b975ba9843aaaa14b8" dependencies = [ "proc-macro2", "quote", - "syn 2.0.38", + "syn 2.0.39", ] [[package]] @@ -1157,9 +1157,9 @@ dependencies = [ [[package]] name = "toml" -version = "0.8.6" +version = "0.8.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8ff9e3abce27ee2c9a37f9ad37238c1bdd4e789c84ba37df76aa4d528f5072cc" +checksum = "a1a195ec8c9da26928f773888e0742ca3ca1040c6cd859c919c9f59c1954ab35" dependencies = [ "serde", "serde_spanned", @@ -1178,9 +1178,9 @@ dependencies = [ [[package]] name = "toml_edit" -version = "0.20.7" +version = "0.21.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "70f427fce4d84c72b5b732388bf4a9f4531b53f74e2887e3ecb2481f68f66d81" +checksum = "d34d383cd00a163b4a5b85053df514d45bc330f6de7737edfe0a93311d1eaa03" dependencies = [ "indexmap", "serde", @@ -1208,7 +1208,7 @@ checksum = "34704c8d6ebcbc939824180af020566b01a7c01f80641264eba0999f6c2b6be7" dependencies = [ "proc-macro2", "quote", - "syn 2.0.38", + "syn 2.0.39", ] [[package]] @@ -1223,9 +1223,9 @@ dependencies = [ [[package]] name = "tracing-log" -version = "0.1.4" +version = "0.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f751112709b4e791d8ce53e32c4ed2d353565a795ce84da2285393f41557bdf2" +checksum = "ee855f1f400bd0e5c02d150ae5de3840039a3f54b025156404e34c23c03f47c3" dependencies = [ "log", "once_cell", @@ -1244,9 +1244,9 @@ dependencies = [ [[package]] name = "tracing-subscriber" -version = "0.3.17" +version = "0.3.18" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "30a651bc37f915e81f087d86e62a18eec5f79550c7faff886f7090b4ea757c77" +checksum = "ad0f048c97dbd9faa9b7df56362b8ebcaa52adb06b498c050d2f4e32f90a7a8b" dependencies = [ "matchers", "nu-ansi-term", @@ -1511,9 +1511,9 @@ checksum = "ed94fce61571a4006852b7389a063ab983c02eb1bb37b47f8272ce92d06d9538" [[package]] name = "winnow" -version = "0.5.18" +version = "0.5.19" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "176b6138793677221d420fd2f0aeeced263f197688b36484660da767bca2fa32" +checksum = "829846f3e3db426d4cee4510841b71a8e58aa2a76b1132579487ae430ccd9c7b" dependencies = [ "memchr", ] diff --git a/Cargo.toml b/Cargo.toml index 75d146eacb48..cfcefdb8b2ee 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-verifier" -version = "0.40.0" +version = "0.41.0" edition = "2021" description = "A bit-precise model checker for Rust." readme = "README.md" diff --git a/cprover_bindings/Cargo.toml b/cprover_bindings/Cargo.toml index 6acd112c34d2..53b97fe989c0 100644 --- a/cprover_bindings/Cargo.toml +++ b/cprover_bindings/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "cprover_bindings" -version = "0.40.0" +version = "0.41.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/docs/src/install-guide.md b/docs/src/install-guide.md index 7f5bd0a7f232..776209987ba1 100644 --- a/docs/src/install-guide.md +++ b/docs/src/install-guide.md @@ -14,7 +14,7 @@ GitHub CI workflows, see [GitHub CI Action](./install-github-ci.md). The following must already be installed: -* **Python version 3.6 or newer** and the package installer `pip`. +* **Python version 3.7 or newer** and the package installer `pip`. * Rust 1.58 or newer installed via `rustup`. * `ctags` is required for Kani's `--visualize` option to work correctly. [Universal ctags](https://ctags.io/) is recommended. diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index c673fb7d9288..912976218e83 100644 --- a/kani-compiler/Cargo.toml +++ b/kani-compiler/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-compiler" -version = "0.40.0" +version = "0.41.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/kani-compiler/src/kani_middle/analysis.rs b/kani-compiler/src/kani_middle/analysis.rs index e5cced950e01..5a26fa071a19 100644 --- a/kani-compiler/src/kani_middle/analysis.rs +++ b/kani-compiler/src/kani_middle/analysis.rs @@ -7,10 +7,13 @@ //! This module will perform all the analyses requested. Callers are responsible for selecting //! when the cost of these analyses are worth it. -use rustc_middle::mir::mono::MonoItem; -use rustc_middle::mir::visit::Visitor as MirVisitor; -use rustc_middle::mir::{Location, Rvalue, Statement, StatementKind, Terminator, TerminatorKind}; +use rustc_middle::mir::mono::MonoItem as InternalMonoItem; use rustc_middle::ty::TyCtxt; +use rustc_smir::rustc_internal; +use stable_mir::mir::mono::MonoItem; +use stable_mir::mir::{ + visit::Location, MirVisitor, Rvalue, Statement, StatementKind, Terminator, TerminatorKind, +}; use std::collections::HashMap; use std::fmt::Display; @@ -20,29 +23,30 @@ use std::fmt::Display; /// - Number of items per type (Function / Constant / Shims) /// - Number of instructions per type. /// - Total number of MIR instructions. -pub fn print_stats<'tcx>(tcx: TyCtxt<'tcx>, items: &[MonoItem<'tcx>]) { - let item_types = items.iter().collect::(); - let visitor = items - .iter() - .filter_map(|&mono| { - if let MonoItem::Fn(instance) = mono { - Some(tcx.instance_mir(instance.def)) - } else { - None - } - }) - .fold(StatsVisitor::default(), |mut visitor, body| { - visitor.visit_body(body); - visitor - }); - eprintln!("====== Reachability Analysis Result ======="); - eprintln!("Total # items: {}", item_types.total()); - eprintln!("Total # statements: {}", visitor.stmts.total()); - eprintln!("Total # expressions: {}", visitor.exprs.total()); - eprintln!("\nReachable Items:\n{item_types}"); - eprintln!("Statements:\n{}", visitor.stmts); - eprintln!("Expressions:\n{}", visitor.exprs); - eprintln!("-------------------------------------------") +pub fn print_stats<'tcx>(tcx: TyCtxt<'tcx>, items: &[InternalMonoItem<'tcx>]) { + rustc_internal::run(tcx, || { + let items: Vec = items.iter().map(rustc_internal::stable).collect(); + let item_types = items.iter().collect::(); + let visitor = items + .iter() + .filter_map( + |mono| { + if let MonoItem::Fn(instance) = mono { Some(instance) } else { None } + }, + ) + .fold(StatsVisitor::default(), |mut visitor, body| { + visitor.visit_body(&body.body()); + visitor + }); + eprintln!("====== Reachability Analysis Result ======="); + eprintln!("Total # items: {}", item_types.total()); + eprintln!("Total # statements: {}", visitor.stmts.total()); + eprintln!("Total # expressions: {}", visitor.exprs.total()); + eprintln!("\nReachable Items:\n{item_types}"); + eprintln!("Statements:\n{}", visitor.stmts); + eprintln!("Expressions:\n{}", visitor.exprs); + eprintln!("-------------------------------------------") + }); } #[derive(Default)] @@ -54,20 +58,20 @@ struct StatsVisitor { exprs: Counter, } -impl<'tcx> MirVisitor<'tcx> for StatsVisitor { - fn visit_statement(&mut self, statement: &Statement<'tcx>, location: Location) { +impl MirVisitor for StatsVisitor { + fn visit_statement(&mut self, statement: &Statement, location: Location) { self.stmts.add(statement); // Also visit the type of expression. self.super_statement(statement, location); } - fn visit_terminator(&mut self, terminator: &Terminator<'tcx>, _location: Location) { + fn visit_terminator(&mut self, terminator: &Terminator, _location: Location) { self.stmts.add(terminator); // Stop here since we don't care today about the information inside the terminator. // self.super_terminator(terminator, location); } - fn visit_rvalue(&mut self, rvalue: &Rvalue<'tcx>, _location: Location) { + fn visit_rvalue(&mut self, rvalue: &Rvalue, _location: Location) { self.exprs.add(rvalue); // Stop here since we don't care today about the information inside the rvalue. // self.super_rvalue(rvalue, location); @@ -115,8 +119,8 @@ impl> FromIterator for Counter { #[derive(Debug, Eq, Hash, PartialEq)] struct Key(pub &'static str); -impl<'tcx> From<&MonoItem<'tcx>> for Key { - fn from(value: &MonoItem) -> Self { +impl From<&MonoItem> for Key { + fn from(value: &stable_mir::mir::mono::MonoItem) -> Self { match value { MonoItem::Fn(_) => Key("function"), MonoItem::GlobalAsm(_) => Key("global assembly"), @@ -125,18 +129,18 @@ impl<'tcx> From<&MonoItem<'tcx>> for Key { } } -impl<'tcx> From<&Statement<'tcx>> for Key { - fn from(value: &Statement<'tcx>) -> Self { +impl From<&Statement> for Key { + fn from(value: &Statement) -> Self { match value.kind { - StatementKind::Assign(_) => Key("Assign"), + StatementKind::Assign(..) => Key("Assign"), StatementKind::Deinit(_) => Key("Deinit"), StatementKind::Intrinsic(_) => Key("Intrinsic"), StatementKind::SetDiscriminant { .. } => Key("SetDiscriminant"), // For now, we don't care about the ones below. - StatementKind::AscribeUserType(_, _) + StatementKind::AscribeUserType { .. } | StatementKind::Coverage(_) | StatementKind::ConstEvalCounter - | StatementKind::FakeRead(_) + | StatementKind::FakeRead(..) | StatementKind::Nop | StatementKind::PlaceMention(_) | StatementKind::Retag(_, _) @@ -146,29 +150,26 @@ impl<'tcx> From<&Statement<'tcx>> for Key { } } -impl<'tcx> From<&Terminator<'tcx>> for Key { - fn from(value: &Terminator<'tcx>) -> Self { +impl From<&Terminator> for Key { + fn from(value: &Terminator) -> Self { match value.kind { + TerminatorKind::Abort => Key("Abort"), TerminatorKind::Assert { .. } => Key("Assert"), TerminatorKind::Call { .. } => Key("Call"), TerminatorKind::Drop { .. } => Key("Drop"), TerminatorKind::CoroutineDrop => Key("CoroutineDrop"), TerminatorKind::Goto { .. } => Key("Goto"), - TerminatorKind::FalseEdge { .. } => Key("FalseEdge"), - TerminatorKind::FalseUnwind { .. } => Key("FalseUnwind"), TerminatorKind::InlineAsm { .. } => Key("InlineAsm"), - TerminatorKind::UnwindResume => Key("UnwindResume"), + TerminatorKind::Resume { .. } => Key("Resume"), TerminatorKind::Return => Key("Return"), TerminatorKind::SwitchInt { .. } => Key("SwitchInt"), - TerminatorKind::UnwindTerminate(_) => Key("UnwindTerminate"), TerminatorKind::Unreachable => Key("Unreachable"), - TerminatorKind::Yield { .. } => Key("Yield"), } } } -impl<'tcx> From<&Rvalue<'tcx>> for Key { - fn from(value: &Rvalue<'tcx>) -> Self { +impl From<&Rvalue> for Key { + fn from(value: &Rvalue) -> Self { match value { Rvalue::Use(_) => Key("Use"), Rvalue::Repeat(_, _) => Key("Repeat"), @@ -177,8 +178,8 @@ impl<'tcx> From<&Rvalue<'tcx>> for Key { Rvalue::AddressOf(_, _) => Key("AddressOf"), Rvalue::Len(_) => Key("Len"), Rvalue::Cast(_, _, _) => Key("Cast"), - Rvalue::BinaryOp(_, _) => Key("BinaryOp"), - Rvalue::CheckedBinaryOp(_, _) => Key("CheckedBinaryOp"), + Rvalue::BinaryOp(..) => Key("BinaryOp"), + Rvalue::CheckedBinaryOp(..) => Key("CheckedBinaryOp"), Rvalue::NullaryOp(_, _) => Key("NullaryOp"), Rvalue::UnaryOp(_, _) => Key("UnaryOp"), Rvalue::Discriminant(_) => Key("Discriminant"), diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs index 0199642f9a60..4316d188c02d 100644 --- a/kani-compiler/src/main.rs +++ b/kani-compiler/src/main.rs @@ -26,8 +26,10 @@ extern crate rustc_interface; extern crate rustc_metadata; extern crate rustc_middle; extern crate rustc_session; +extern crate rustc_smir; extern crate rustc_span; extern crate rustc_target; +extern crate stable_mir; // We can't add this directly as a dependency because we need the version to match rustc extern crate tempfile; diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index 9b6f9de8644a..136c36cf63f2 100644 --- a/kani-driver/Cargo.toml +++ b/kani-driver/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-driver" -version = "0.40.0" +version = "0.41.0" edition = "2021" description = "Build a project with Kani and run all proof harnesses" license = "MIT OR Apache-2.0" diff --git a/kani_metadata/Cargo.toml b/kani_metadata/Cargo.toml index fb0c303f98e2..604f0214dea9 100644 --- a/kani_metadata/Cargo.toml +++ b/kani_metadata/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_metadata" -version = "0.40.0" +version = "0.41.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/kani/Cargo.toml b/library/kani/Cargo.toml index bd2fd77338b5..b61dcd7a0564 100644 --- a/library/kani/Cargo.toml +++ b/library/kani/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani" -version = "0.40.0" +version = "0.41.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 dec7bf1f1232..3c1f90b7d3cf 100644 --- a/library/kani_macros/Cargo.toml +++ b/library/kani_macros/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_macros" -version = "0.40.0" +version = "0.41.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/std/Cargo.toml b/library/std/Cargo.toml index 2370ea83a58c..83a8e4adb894 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.40.0" +version = "0.41.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/scripts/ci/Dockerfile.bundle-test-ubuntu-18-04 b/scripts/ci/Dockerfile.bundle-test-ubuntu-18-04 index a4cc79c80f07..d3ddfd20fdbf 100644 --- a/scripts/ci/Dockerfile.bundle-test-ubuntu-18-04 +++ b/scripts/ci/Dockerfile.bundle-test-ubuntu-18-04 @@ -10,9 +10,19 @@ FROM ubuntu:18.04 ENV DEBIAN_FRONTEND=noninteractive \ DEBCONF_NONINTERACTIVE_SEEN=true + RUN apt-get update && \ - apt-get install -y python3 python3-pip curl ctags && \ - curl -sSf https://sh.rustup.rs | sh -s -- -y + apt-get install --no-install-recommends -y build-essential software-properties-common && \ + add-apt-repository -y ppa:deadsnakes/ppa && \ + apt install --no-install-recommends -y python3.7 python3.7-dev python3.7-distutils curl ctags + +RUN update-alternatives --install /usr/bin/python3 python3 /usr/bin/python3.7 1 + +RUN curl -s https://bootstrap.pypa.io/get-pip.py -o get-pip.py && \ + python3 get-pip.py --force-reinstall && \ + rm get-pip.py + +RUN curl -sSf https://sh.rustup.rs | sh -s -- -y ENV PATH="/root/.cargo/bin:${PATH}" WORKDIR /tmp/kani diff --git a/scripts/setup/ubuntu/install_cbmc.sh b/scripts/setup/ubuntu/install_cbmc.sh index 9aefab019110..f37aafcd6327 100755 --- a/scripts/setup/ubuntu/install_cbmc.sh +++ b/scripts/setup/ubuntu/install_cbmc.sh @@ -15,7 +15,7 @@ fi UBUNTU_VERSION=$(lsb_release -rs) MAJOR=${UBUNTU_VERSION%.*} -if [[ "${MAJOR}" -gt "18" ]] +if [[ "${MAJOR}" -gt "18" ]] && [[ $(dpkg --print-architecture) = "amd64" ]] then FILE="ubuntu-${UBUNTU_VERSION}-cbmc-${CBMC_VERSION}-Linux.deb" URL="https://github.com/diffblue/cbmc/releases/download/cbmc-${CBMC_VERSION}/$FILE" @@ -29,7 +29,7 @@ then exit 0 fi -# Binaries are no longer released for 18.04, so build from source +# There are no binaries for 18.04 or for non-x86_64, so build from source WORK_DIR=$(mktemp -d) git clone \ @@ -44,7 +44,8 @@ git submodule update --init cmake -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical" make -C build -j$(nproc) -sudo make -C build install +cpack -G DEB --config build/CPackConfig.cmake +sudo dpkg -i ./cbmc-*.deb popd rm -rf "${WORK_DIR}" diff --git a/src/os_hacks.rs b/src/os_hacks.rs index cf39c39be82d..ca064a662901 100644 --- a/src/os_hacks.rs +++ b/src/os_hacks.rs @@ -5,7 +5,6 @@ //! "flow" of code in setup.rs, this module contains all functions that implement os-specific //! workarounds. -use std::ffi::OsString; use std::path::Path; use std::process::Command; @@ -14,74 +13,6 @@ use os_info::Info; use crate::cmd::AutoRun; -pub fn should_apply_ubuntu_18_04_python_hack(os: &os_info::Info) -> Result { - if os.os_type() != os_info::Type::Ubuntu { - return Ok(false); - } - // Check both versions: https://github.com/stanislav-tkach/os_info/issues/318 - if *os.version() != os_info::Version::Semantic(18, 4, 0) - && *os.version() != os_info::Version::Custom("18.04".into()) - { - return Ok(false); - } - // It's not enough to check that we're on Ubuntu 18.04 because the user may have - // manually updated to a newer version of Python instead of using what the OS ships. - // So check if it looks like the OS-shipped version as best we can. - let cmd = Command::new("python3").args(["-m", "pip", "--version"]).output()?; - let output = std::str::from_utf8(&cmd.stdout)?; - // The problem version looks like: - // 'pip 9.0.1 from /usr/lib/python3/dist-packages (python 3.6)' - // So we'll test for version 9. - Ok(pip_major_version(output)? == 9) -} - -/// Unit testable parsing function for extracting pip version numbers, from strings that look like: -/// 'pip 9.0.1 from /usr/lib/python3/dist-packages (python 3.6)' -fn pip_major_version(output: &str) -> Result { - // We don't want dependencies so parse with stdlib string functions as best we can. - let mut words = output.split_whitespace(); - let _pip = words.next().context("No pip output")?; - let version = words.next().context("No pip version")?; - - let mut versions = version.split('.'); - let major = versions.next().context("No pip major version")?; - - Ok(major.parse()?) -} - -/// See [`crate::setup::setup_python_deps`] -pub fn setup_python_deps_on_ubuntu_18_04(pyroot: &Path, pkg_versions: &[&str]) -> Result<()> { - println!("Applying a workaround for 18.04..."); - // https://github.com/pypa/pip/issues/3826 - // Ubuntu 18.04 has a patched-to-be-broken version of pip that just straight-up makes `--target` not work. - // Worse still, there is no apparent way to replicate the correct behavior cleanly. - - // This is a really awful hack to simulate getting the same result. I can find no other solution. - // Example failed approach: `--system --target pyroot` fails to create a `pyroot/bin` with binaries. - - // Step 1: use `--system --prefix pyroot`. This disables the broken behavior, and creates `bin` but... - Command::new("python3") - .args(["-m", "pip", "install", "--system", "--prefix"]) - .arg(pyroot) - .args(pkg_versions) - .run()?; - - // Step 2: move `pyroot/lib/python3.6/site-packages/*` up to `pyroot` - // This seems to successfully replicate the behavior of `--target` - // "mv" is not idempotent however so we need to do "cp -r" then delete - let mut cp_cmd = OsString::new(); - cp_cmd.push("cp -r "); - cp_cmd.push(pyroot.as_os_str()); - cp_cmd.push("/lib/python*/site-packages/* "); - cp_cmd.push(pyroot.as_os_str()); - Command::new("bash").arg("-c").arg(cp_cmd).run()?; - - // `lib` is the directory `--prefix` creates that `--target` does not. - std::fs::remove_dir_all(pyroot.join("lib"))?; - - Ok(()) -} - /// This is the final step of setup, where we look for OSes that require additional setup steps /// beyond the usual ones that we have done already. pub fn setup_os_hacks(kani_dir: &Path, os: &Info) -> Result<()> { @@ -159,25 +90,3 @@ fn setup_nixos_patchelf(kani_dir: &Path) -> Result<()> { Ok(()) } - -#[cfg(test)] -mod tests { - use super::*; - - #[test] - fn check_pip_major_version() -> Result<()> { - // These read a lot better formatted on one line, so shorten them: - use pip_major_version as p; - // 18.04 example: (with extra newline to test whitespace handling) - assert_eq!(p("pip 9.0.1 from /usr/lib/python3/dist-packages (python 3.6)\n")?, 9); - // a mac - assert_eq!(p("pip 21.1.1 from /usr/local/python3.9/site-packages/pip (python 3.9)")?, 21); - // 20.04 - assert_eq!(p("pip 20.0.2 from /usr/lib/python3/dist-packages/pip (python 3.8)")?, 20); - // How mangled can we get and still "work"? - assert_eq!(p("pip 1")?, 1); - assert_eq!(p("p 1")?, 1); - assert_eq!(p("\n\n p 1 p")?, 1); - Ok(()) - } -} diff --git a/src/setup.rs b/src/setup.rs index 747d3435108a..ffdcf340e336 100644 --- a/src/setup.rs +++ b/src/setup.rs @@ -83,7 +83,7 @@ pub fn setup(use_local_bundle: Option) -> Result<()> { setup_rust_toolchain(&kani_dir)?; - setup_python_deps(&kani_dir, &os)?; + setup_python_deps(&kani_dir)?; os_hacks::setup_os_hacks(&kani_dir, &os)?; @@ -152,18 +152,13 @@ fn setup_rust_toolchain(kani_dir: &Path) -> Result { } /// Install into the pyroot the python dependencies we need -fn setup_python_deps(kani_dir: &Path, os: &os_info::Info) -> Result<()> { +fn setup_python_deps(kani_dir: &Path) -> Result<()> { println!("[4/5] Installing Kani python dependencies..."); let pyroot = kani_dir.join("pyroot"); // TODO: this is a repetition of versions from kani/kani-dependencies let pkg_versions = &["cbmc-viewer==3.8"]; - if os_hacks::should_apply_ubuntu_18_04_python_hack(os)? { - os_hacks::setup_python_deps_on_ubuntu_18_04(&pyroot, pkg_versions)?; - return Ok(()); - } - Command::new("python3") .args(["-m", "pip", "install", "--target"]) .arg(&pyroot) diff --git a/tools/build-kani/Cargo.toml b/tools/build-kani/Cargo.toml index 0bb15a53abf9..f64a3075f8a3 100644 --- a/tools/build-kani/Cargo.toml +++ b/tools/build-kani/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "build-kani" -version = "0.40.0" +version = "0.41.0" edition = "2021" description = "Builds Kani, Sysroot and release bundle." license = "MIT OR Apache-2.0"