Skip to content

Commit 5aad1a9

Browse files
authored
Upgrade toolchain to 08/28 (#3454)
Upgrades toolchain to 08/28 Culprit upstream changes: 1. rust-lang/rust#128812 2. rust-lang/rust#128703 3. rust-lang/rust#127679 4. rust-lang/rust-clippy#12993 5. rust-lang/cargo#14370 6. rust-lang/rust#128806 Resolves #3429 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
1 parent 8c17849 commit 5aad1a9

File tree

17 files changed

+46
-13
lines changed

17 files changed

+46
-13
lines changed

Cargo.toml

+3
Original file line numberDiff line numberDiff line change
@@ -71,3 +71,6 @@ exclude = [
7171
"tests/script-based-pre/build-cache-dirty/target/new_dep",
7272
"tests/script-based-pre/verify_std_cmd/tmp_dir/target/kani_verify_std",
7373
]
74+
75+
[workspace.lints.clippy]
76+
too_long_first_doc_paragraph = "allow"

cprover_bindings/Cargo.toml

+3
Original file line numberDiff line numberDiff line change
@@ -24,3 +24,6 @@ linear-map = {version = "1.2", features = ["serde_impl"]}
2424
[dev-dependencies]
2525
serde_test = "1"
2626
memuse = "0.2.1"
27+
28+
[lints]
29+
workspace = true

kani-compiler/Cargo.toml

+3
Original file line numberDiff line numberDiff line change
@@ -35,3 +35,6 @@ write_json_symtab = []
3535
[package.metadata.rust-analyzer]
3636
# This package uses rustc crates.
3737
rustc_private=true
38+
39+
[lints]
40+
workspace = true

kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs

+5-2
Original file line numberDiff line numberDiff line change
@@ -579,7 +579,10 @@ impl<'tcx> GotocCtx<'tcx> {
579579
.unwrap();
580580
self.codegen_fndef_type(instance)
581581
}
582-
ty::FnPtr(sig) => self.codegen_function_sig(*sig).to_pointer(),
582+
ty::FnPtr(sig_tys, hdr) => {
583+
let sig = sig_tys.with(*hdr);
584+
self.codegen_function_sig(sig).to_pointer()
585+
}
583586
ty::Closure(_, subst) => self.codegen_ty_closure(ty, subst),
584587
ty::Coroutine(..) => self.codegen_ty_coroutine(ty),
585588
ty::Never => self.ensure_struct(NEVER_TYPE_EMPTY_STRUCT_NAME, "!", |_, _| vec![]),
@@ -1014,7 +1017,7 @@ impl<'tcx> GotocCtx<'tcx> {
10141017

10151018
// These types were blocking stdlib. Doing the default thing to unblock.
10161019
// https://github.com/model-checking/kani/issues/214
1017-
ty::FnPtr(_) => self.codegen_ty(pointee_type).to_pointer(),
1020+
ty::FnPtr(_, _) => self.codegen_ty(pointee_type).to_pointer(),
10181021

10191022
// These types have no regression tests for them.
10201023
// For soundness, hold off on generating them till we have test-cases.

kani-compiler/src/kani_middle/coercion.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -99,7 +99,7 @@ pub fn extract_unsize_casting<'tcx>(
9999
coerce_info.dst_ty
100100
));
101101
// Find the tail of the coercion that determines the type of metadata to be stored.
102-
let (src_base_ty, dst_base_ty) = tcx.struct_lockstep_tails_erasing_lifetimes(
102+
let (src_base_ty, dst_base_ty) = tcx.struct_lockstep_tails_for_codegen(
103103
src_pointee_ty,
104104
dst_pointee_ty,
105105
ParamEnv::reveal_all(),

kani-compiler/src/kani_middle/points_to/points_to_analysis.rs

+2-2
Original file line numberDiff line numberDiff line change
@@ -53,7 +53,7 @@ struct PointsToAnalysis<'a, 'tcx> {
5353
tcx: TyCtxt<'tcx>,
5454
/// This will be used in the future to resolve function pointer and vtable calls. Currently, we
5555
/// can resolve call graph edges just by looking at the terminators and erroring if we can't
56-
/// resolve the callee.
56+
/// resolve the callee.
5757
call_graph: &'a CallGraph,
5858
/// This graph should contain a subset of the points-to graph reachable from function arguments.
5959
/// For the entry function it will be empty (as it supposedly does not have any parameters).
@@ -521,7 +521,7 @@ impl<'a, 'tcx> PointsToAnalysis<'a, 'tcx> {
521521
| Rvalue::ShallowInitBox(operand, _)
522522
| Rvalue::Cast(_, operand, _)
523523
| Rvalue::Repeat(operand, ..) => self.successors_for_operand(state, operand),
524-
Rvalue::Ref(_, _, ref_place) | Rvalue::AddressOf(_, ref_place) => {
524+
Rvalue::Ref(_, _, ref_place) | Rvalue::RawPtr(_, ref_place) => {
525525
// Here, a reference to a place is created, which leaves the place
526526
// unchanged.
527527
state.resolve_place(ref_place, self.instance)

kani-compiler/src/kani_middle/transform/internal_mir.rs

+3-4
Original file line numberDiff line numberDiff line change
@@ -210,10 +210,9 @@ impl RustcInternalMir for Rvalue {
210210

211211
fn internal_mir<'tcx>(&self, tcx: TyCtxt<'tcx>) -> Self::T<'tcx> {
212212
match self {
213-
Rvalue::AddressOf(mutability, place) => rustc_middle::mir::Rvalue::AddressOf(
214-
internal(tcx, mutability),
215-
internal(tcx, place),
216-
),
213+
Rvalue::AddressOf(mutability, place) => {
214+
rustc_middle::mir::Rvalue::RawPtr(internal(tcx, mutability), internal(tcx, place))
215+
}
217216
Rvalue::Aggregate(aggregate_kind, operands) => rustc_middle::mir::Rvalue::Aggregate(
218217
Box::new(aggregate_kind.internal_mir(tcx)),
219218
rustc_index::IndexVec::from_raw(

kani-compiler/src/session.rs

+2-1
Original file line numberDiff line numberDiff line change
@@ -61,7 +61,8 @@ static JSON_PANIC_HOOK: LazyLock<Box<dyn Fn(&panic::PanicHookInfo<'_>) + Sync +
6161
Lrc::new(SourceMap::new(FilePathMapping::empty())),
6262
fallback_bundle,
6363
false,
64-
HumanReadableErrorType::Default(ColorConfig::Never),
64+
HumanReadableErrorType::Default,
65+
ColorConfig::Never,
6566
);
6667
let diagnostic = DiagInner::new(rustc_errors::Level::Bug, msg);
6768
emitter.emit_diagnostic(diagnostic);

kani-driver/src/call_cargo.rs

+6-1
Original file line numberDiff line numberDiff line change
@@ -73,6 +73,11 @@ impl KaniSession {
7373
cargo_args.push("-v".into());
7474
}
7575

76+
// We need this suffix push because of https://github.com/rust-lang/cargo/pull/14370
77+
// which removes the library suffix from the build-std command
78+
let mut full_path = std_path.to_path_buf();
79+
full_path.push("library");
80+
7681
// Since we are verifying the standard library, we set the reachability to all crates.
7782
let mut cmd = setup_cargo_command()?;
7883
cmd.args(&cargo_args)
@@ -82,7 +87,7 @@ impl KaniSession {
8287
// https://doc.rust-lang.org/cargo/reference/environment-variables.html
8388
.env("CARGO_ENCODED_RUSTFLAGS", rustc_args.join(OsStr::new("\x1f")))
8489
.env("CARGO_TERM_PROGRESS_WHEN", "never")
85-
.env("__CARGO_TESTS_ONLY_SRC_ROOT", std_path.as_os_str());
90+
.env("__CARGO_TESTS_ONLY_SRC_ROOT", full_path.as_os_str());
8691

8792
Ok(self
8893
.run_build(cmd)?

kani_metadata/Cargo.toml

+3
Original file line numberDiff line numberDiff line change
@@ -16,3 +16,6 @@ cbmc = { path = "../cprover_bindings", package = "cprover_bindings" }
1616
strum = "0.26"
1717
strum_macros = "0.26"
1818
clap = { version = "4.4.11", features = ["derive"] }
19+
20+
[lints]
21+
workspace = true

library/kani/Cargo.toml

+3
Original file line numberDiff line numberDiff line change
@@ -15,3 +15,6 @@ kani_core = { path = "../kani_core" }
1515
[features]
1616
concrete_playback = []
1717
no_core=["kani_macros/no_core"]
18+
19+
[lints]
20+
workspace = true

library/kani_core/Cargo.toml

+3
Original file line numberDiff line numberDiff line change
@@ -14,3 +14,6 @@ kani_macros = { path = "../kani_macros"}
1414

1515
[features]
1616
no_core=["kani_macros/no_core"]
17+
18+
[lints]
19+
workspace = true

library/kani_macros/Cargo.toml

+3
Original file line numberDiff line numberDiff line change
@@ -23,3 +23,6 @@ rustc_private = true
2323

2424
[features]
2525
no_core = []
26+
27+
[lints]
28+
workspace = true

library/kani_macros/src/lib.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,6 @@
88
// So we have to enable this on the commandline (see kani-rustc) with:
99
// RUSTFLAGS="-Zcrate-attr=feature(register_tool) -Zcrate-attr=register_tool(kanitool)"
1010
#![feature(proc_macro_diagnostic)]
11-
1211
mod derive;
1312

1413
// proc_macro::quote is nightly-only, so we'll cobble things together instead
@@ -65,6 +64,7 @@ pub fn recursion(attr: TokenStream, item: TokenStream) -> TokenStream {
6564
/// Set Loop unwind limit for proof harnesses
6665
/// The attribute `#[kani::unwind(arg)]` can only be called alongside `#[kani::proof]`.
6766
/// arg - Takes in a integer value (u32) that represents the unwind value for the harness.
67+
#[allow(clippy::too_long_first_doc_paragraph)]
6868
#[proc_macro_attribute]
6969
pub fn unwind(attr: TokenStream, item: TokenStream) -> TokenStream {
7070
attr_impl::unwind(attr, item)

rust-toolchain.toml

+1-1
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,5 @@
22
# SPDX-License-Identifier: Apache-2.0 OR MIT
33

44
[toolchain]
5-
channel = "nightly-2024-08-07"
5+
channel = "nightly-2024-08-28"
66
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

tools/compiletest/Cargo.toml

+3
Original file line numberDiff line numberDiff line change
@@ -30,3 +30,6 @@ wait-timeout = "0.2.0"
3030

3131
[target.'cfg(unix)'.dependencies]
3232
libc = "0.2"
33+
34+
[lints]
35+
workspace = true

tools/scanner/src/bin/scan.rs

+1
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@
1414
//! together with the name of the analysis.
1515
//!
1616
//! Look at each analysis documentation to see which files an analysis produces.
17+
#![feature(rustc_private)]
1718

1819
use scanner::run_all;
1920
use std::process::ExitCode;

0 commit comments

Comments
 (0)