Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Upgrade Rust toolchain to nightly-2024-02-09 #3015

Merged
merged 8 commits into from
Feb 13, 2024
Merged

Upgrade Rust toolchain to nightly-2024-02-09 #3015

Show file tree
Hide file tree
Changes from 4 commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
ddf3c11
Upgrade Rust toolchain to nightly-2024-02-09
feliperodri Feb 9, 2024
f92344b
Upgrade dependencies
feliperodri Feb 9, 2024
e2cfda4
Resolve conflicts
feliperodri Feb 9, 2024
4a6b57a
Resolve extra conflicts
feliperodri Feb 9, 2024
556d58b
Resolve conflicts
feliperodri Feb 12, 2024
e4a5cfe
Revert unnecessary changes
feliperodri Feb 12, 2024
49ed854
New line
feliperodri Feb 12, 2024
fd067e5
Remove unused traits and methods from typ.rs
feliperodri Feb 13, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
82 changes: 48 additions & 34 deletions Cargo.lock
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,13 +14,14 @@ dependencies = [

[[package]]
name = "ahash"
version = "0.7.7"
version = "0.8.7"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "5a824f2aa7e75a0c98c5a504fceb80649e9c35265d44525b5f94de4771a395cd"
checksum = "77c3a9648d43b9cd48db467b3f87fdd6e146bcc88ab0180006cef2179fe11d01"
dependencies = [
"getrandom",
"cfg-if",
"once_cell",
"version_check",
"zerocopy",
]

[[package]]
Expand Down Expand Up @@ -139,9 +140,9 @@ dependencies = [

[[package]]
name = "cargo-platform"
version = "0.1.6"
version = "0.1.7"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "ceed8ef69d8518a5dda55c07425450b58a4e1946f4951eab6d7191ee86c2443d"
checksum = "694c8807f2ae16faecc43dc17d74b3eb042482789fd0eb64b39a2e04e087053f"
dependencies = [
"serde",
]
Expand All @@ -168,19 +169,19 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"

[[package]]
name = "clap"
version = "4.4.18"
version = "4.5.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "1e578d6ec4194633722ccf9544794b71b1385c3c027efe0c55db226fc880865c"
checksum = "80c21025abd42669a92efc996ef13cfb2c5c627858421ea58d5c3b331a6c134f"
dependencies = [
"clap_builder",
"clap_derive",
]

[[package]]
name = "clap_builder"
version = "4.4.18"
version = "4.5.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "4df4df40ec50c46000231c914968278b1eb05098cf8f1b3a518a95030e71d1c7"
checksum = "458bf1f341769dfcf849846f65dffdf9146daa56bcd2a47cb4e1de9915567c99"
dependencies = [
"anstream",
"anstyle",
Expand All @@ -190,9 +191,9 @@ dependencies = [

[[package]]
name = "clap_derive"
version = "4.4.7"
version = "4.5.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "cf9804afaaf59a91e75b022a30fb7229a7901f60c755489cc61c9b423b836442"
checksum = "307bc0538d5f0f83b8248db3087aa92fe504e4691294d0c96c0eabc33f47ba47"
dependencies = [
"heck",
"proc-macro2",
Expand All @@ -202,9 +203,9 @@ dependencies = [

[[package]]
name = "clap_lex"
version = "0.6.0"
version = "0.7.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "702fc72eb24e5a1e48ce58027a675bc24edd52096d5397d4aea7c6dd9eca0bd1"
checksum = "98cc8fbded0c607b7ba9dd60cd98df59af97e84d24e49c8557331cfc26d301ce"

[[package]]
name = "colorchoice"
Expand Down Expand Up @@ -378,19 +379,13 @@ checksum = "d2fabcfbdc87f4758337ca535fb41a6d701b65693ce38287d856d1674551ec9b"

[[package]]
name = "hashbrown"
version = "0.11.2"
version = "0.14.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "ab5ef0d4909ef3724cc8cce6ccc8572c5c817592e9285f5464f8e86f8bd3726e"
checksum = "290f1a1d9242c78d09ce40a5e87e7554ee637af1351968159f4952f028f75604"
dependencies = [
"ahash",
]

[[package]]
name = "hashbrown"
version = "0.14.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "290f1a1d9242c78d09ce40a5e87e7554ee637af1351968159f4952f028f75604"

[[package]]
name = "heck"
version = "0.4.1"
Expand All @@ -413,7 +408,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "824b2ae422412366ba479e8111fd301f7b5faece8149317bb81925979a53f520"
dependencies = [
"equivalent",
"hashbrown 0.14.3",
"hashbrown",
]

[[package]]
Expand Down Expand Up @@ -628,19 +623,18 @@ dependencies = [

[[package]]
name = "num-integer"
version = "0.1.45"
version = "0.1.46"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "225d3389fb3509a24c93f5c29eb6bde2586b98d9f016636dff58d7c6f7569cd9"
checksum = "7969661fd2958a5cb096e56c8e1ad0444ac2bbcd0061bd28660485a44879858f"
dependencies = [
"autocfg",
"num-traits",
]

[[package]]
name = "num-iter"
version = "0.1.43"
version = "0.1.44"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "7d03e6c028c5dc5cac6e2dec0efda81fc887605bb3d884578bb6d6bf7514e252"
checksum = "d869c01cc0c455284163fd0092f1f93835385ccab5a98a0dcc497b2f8bf055a9"
dependencies = [
"autocfg",
"num-integer",
Expand All @@ -661,9 +655,9 @@ dependencies = [

[[package]]
name = "num-traits"
version = "0.2.17"
version = "0.2.18"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "39e3200413f237f41ab11ad6d161bc7239c84dcb631773ccd7de3dfe4b5c267c"
checksum = "da0df0e5185db44f69b44f26786fe401b6c293d1907744beaa7fa62b2e5a517a"
dependencies = [
"autocfg",
]
Expand Down Expand Up @@ -1047,20 +1041,20 @@ dependencies = [

[[package]]
name = "string-interner"
version = "0.14.0"
version = "0.15.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "91e2531d8525b29b514d25e275a43581320d587b86db302b9a7e464bac579648"
checksum = "07f9fdfdd31a0ff38b59deb401be81b73913d76c9cc5b1aed4e1330a223420b9"
dependencies = [
"cfg-if",
"hashbrown 0.11.2",
"hashbrown",
"serde",
]

[[package]]
name = "strsim"
version = "0.10.0"
version = "0.11.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "73473c0e59e6d5812c5dfe2a064a6444949f089e20eec9a2e5506596494e4623"
checksum = "5ee073c9e4cd00e28217186dbe12796d692868f432bf2e97ee73bed0c56dfa01"

[[package]]
name = "strum"
Expand Down Expand Up @@ -1517,3 +1511,23 @@ checksum = "5389a154b01683d28c77f8f68f49dea75f0a4da32557a58f68ee51ebba472d29"
dependencies = [
"memchr",
]

[[package]]
name = "zerocopy"
version = "0.7.32"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "74d4d3961e53fa4c9a25a8637fc2bfaf2595b3d3ae34875568a5cf64787716be"
dependencies = [
"zerocopy-derive",
]

[[package]]
name = "zerocopy-derive"
version = "0.7.32"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "9ce1b18ccd8e73a9321186f97e46f9f04b778851177567b1975109d26a08d2a6"
dependencies = [
"proc-macro2",
"quote",
"syn 2.0.48",
]
2 changes: 1 addition & 1 deletion cprover_bindings/Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.14.0"
string-interner = "0.15.0"
tracing = "0.1"
linear-map = {version = "1.2", features = ["serde_impl"]}

Expand Down
4 changes: 3 additions & 1 deletion cprover_bindings/src/cbmc_string.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@

use lazy_static::lazy_static;
use std::sync::Mutex;
use string_interner::backend::StringBackend;
use string_interner::symbol::SymbolU32;
use string_interner::StringInterner;

Expand All @@ -24,7 +25,8 @@ pub struct InternedString(SymbolU32);

// Use a `Mutex` to make this thread safe.
lazy_static! {
static ref INTERNER: Mutex<StringInterner> = Mutex::new(StringInterner::default());
static ref INTERNER: Mutex<StringInterner<StringBackend>> =
Mutex::new(StringInterner::default());
}

impl InternedString {
Expand Down
9 changes: 8 additions & 1 deletion kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -100,6 +100,7 @@ impl TypeExt for Type {
}
}

#[allow(unused)]
fn is_unit_pointer(&self) -> bool {
match self {
Type::Pointer { typ } => typ.is_unit(),
Expand All @@ -108,6 +109,7 @@ impl TypeExt for Type {
}
}

#[allow(unused)]
feliperodri marked this conversation as resolved.
Show resolved Hide resolved
trait ExprExt {
fn unit(symbol_table: &SymbolTable) -> Self;

Expand Down Expand Up @@ -640,7 +642,11 @@ impl<'tcx> GotocCtx<'tcx> {
ty::Bound(_, _) | ty::Param(_) => unreachable!("monomorphization bug"),

// type checking remnants which shouldn't be reachable
ty::CoroutineWitness(_, _) | ty::Infer(_) | ty::Placeholder(_) | ty::Error(_) => {
ty::CoroutineWitness(_, _)
| ty::CoroutineClosure(_, _)
| ty::Infer(_)
| ty::Placeholder(_)
| ty::Error(_) => {
unreachable!("remnants of type checking")
}
}
Expand Down Expand Up @@ -1078,6 +1084,7 @@ impl<'tcx> GotocCtx<'tcx> {
ty::Bound(_, _) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
ty::Error(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
ty::CoroutineWitness(_, _) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
ty::CoroutineClosure(_, _) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
ty::Infer(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
ty::Param(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
ty::Placeholder(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
Expand Down
2 changes: 1 addition & 1 deletion kani-compiler/src/kani_middle/coercion.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -253,7 +253,7 @@ fn custom_coerce_unsize_info<'tcx>(

match tcx.codegen_select_candidate((ParamEnv::reveal_all(), trait_ref)) {
Ok(ImplSource::UserDefined(ImplSourceUserDefinedData { impl_def_id, .. })) => {
tcx.coerce_unsized_info(impl_def_id).custom_kind.unwrap()
tcx.coerce_unsized_info(impl_def_id).unwrap().custom_kind.unwrap()
}
impl_source => {
unreachable!("invalid `CoerceUnsized` impl_source: {:?}", impl_source);
Expand Down
2 changes: 1 addition & 1 deletion kani-compiler/src/session.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,7 @@ static JSON_PANIC_HOOK: LazyLock<Box<dyn Fn(&panic::PanicInfo<'_>) + Sync + Send
TerminalUrl::No,
);
let diagnostic = Diagnostic::new(rustc_errors::Level::Bug, msg);
emitter.emit_diagnostic(&diagnostic);
emitter.emit_diagnostic(diagnostic);
(*JSON_PANIC_HOOK)(info);
}));
hook
Expand Down
6 changes: 0 additions & 6 deletions kani-driver/src/args/common.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,8 +50,6 @@ pub trait Verbosity {
/// Whether we should be verbose.
/// Note that `debug() == true` must imply `verbose() == true`.
fn verbose(&self) -> bool;
/// Whether we should emit debug messages.
fn debug(&self) -> bool;
feliperodri marked this conversation as resolved.
Show resolved Hide resolved
/// Whether any verbosity was selected.
fn is_set(&self) -> bool;
}
Expand All @@ -65,10 +63,6 @@ impl Verbosity for CommonArgs {
self.verbose || self.debug
}

fn debug(&self) -> bool {
self.debug
}

fn is_set(&self) -> bool {
self.quiet || self.verbose || self.debug
}
Expand Down
1 change: 0 additions & 1 deletion kani-driver/src/main.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
#![feature(let_chains)]
#![feature(array_methods)]
use std::ffi::OsString;
use std::process::ExitCode;

Expand Down
2 changes: 1 addition & 1 deletion rust-toolchain.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,5 +2,5 @@
# SPDX-License-Identifier: Apache-2.0 OR MIT

[toolchain]
channel = "nightly-2024-01-25"
channel = "nightly-2024-02-09"
components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
4 changes: 0 additions & 4 deletions tests/ui/derive-arbitrary/non_arbitrary_param/expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1 @@
error[E0277]: the trait bound `Void: kani::Arbitrary` is not satisfied
feliperodri marked this conversation as resolved.
Show resolved Hide resolved

|\
| let _wrapper: Wrapper<Void> = kani::any();\
| ^^^^^^^^^ the trait `kani::Arbitrary` is not implemented for `Void`\
1 change: 0 additions & 1 deletion tools/bookrunner/librustdoc/lib.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,6 @@
html_playground_url = "https://play.rust-lang.org/"
)]
#![feature(rustc_private)]
#![feature(array_methods)]
#![feature(assert_matches)]
#![feature(box_patterns)]
#![feature(control_flow_enum)]
Expand Down
Loading