Skip to content

Commit

Permalink
Upgrade toolchain to 08/28 (#3454)
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
jaisnan committed Aug 28, 2024
1 parent 8c17849 commit 5aad1a9
Show file tree
Hide file tree
Showing 17 changed files with 46 additions and 13 deletions.
3 changes: 3 additions & 0 deletions Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -71,3 +71,6 @@ exclude = [
"tests/script-based-pre/build-cache-dirty/target/new_dep",
"tests/script-based-pre/verify_std_cmd/tmp_dir/target/kani_verify_std",
]

[workspace.lints.clippy]
too_long_first_doc_paragraph = "allow"
3 changes: 3 additions & 0 deletions cprover_bindings/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -24,3 +24,6 @@ linear-map = {version = "1.2", features = ["serde_impl"]}
[dev-dependencies]
serde_test = "1"
memuse = "0.2.1"

[lints]
workspace = true
3 changes: 3 additions & 0 deletions kani-compiler/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -35,3 +35,6 @@ write_json_symtab = []
[package.metadata.rust-analyzer]
# This package uses rustc crates.
rustc_private=true

[lints]
workspace = true
7 changes: 5 additions & 2 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
Original file line number Diff line number Diff line change
Expand Up @@ -579,7 +579,10 @@ impl<'tcx> GotocCtx<'tcx> {
.unwrap();
self.codegen_fndef_type(instance)
}
ty::FnPtr(sig) => self.codegen_function_sig(*sig).to_pointer(),
ty::FnPtr(sig_tys, hdr) => {
let sig = sig_tys.with(*hdr);
self.codegen_function_sig(sig).to_pointer()
}
ty::Closure(_, subst) => self.codegen_ty_closure(ty, subst),
ty::Coroutine(..) => self.codegen_ty_coroutine(ty),
ty::Never => self.ensure_struct(NEVER_TYPE_EMPTY_STRUCT_NAME, "!", |_, _| vec![]),
Expand Down Expand Up @@ -1014,7 +1017,7 @@ impl<'tcx> GotocCtx<'tcx> {

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

// These types have no regression tests for them.
// For soundness, hold off on generating them till we have test-cases.
Expand Down
2 changes: 1 addition & 1 deletion kani-compiler/src/kani_middle/coercion.rs
Original file line number Diff line number Diff line change
Expand Up @@ -99,7 +99,7 @@ pub fn extract_unsize_casting<'tcx>(
coerce_info.dst_ty
));
// Find the tail of the coercion that determines the type of metadata to be stored.
let (src_base_ty, dst_base_ty) = tcx.struct_lockstep_tails_erasing_lifetimes(
let (src_base_ty, dst_base_ty) = tcx.struct_lockstep_tails_for_codegen(
src_pointee_ty,
dst_pointee_ty,
ParamEnv::reveal_all(),
Expand Down
4 changes: 2 additions & 2 deletions kani-compiler/src/kani_middle/points_to/points_to_analysis.rs
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,7 @@ struct PointsToAnalysis<'a, 'tcx> {
tcx: TyCtxt<'tcx>,
/// This will be used in the future to resolve function pointer and vtable calls. Currently, we
/// can resolve call graph edges just by looking at the terminators and erroring if we can't
/// resolve the callee.
/// resolve the callee.
call_graph: &'a CallGraph,
/// This graph should contain a subset of the points-to graph reachable from function arguments.
/// For the entry function it will be empty (as it supposedly does not have any parameters).
Expand Down Expand Up @@ -521,7 +521,7 @@ impl<'a, 'tcx> PointsToAnalysis<'a, 'tcx> {
| Rvalue::ShallowInitBox(operand, _)
| Rvalue::Cast(_, operand, _)
| Rvalue::Repeat(operand, ..) => self.successors_for_operand(state, operand),
Rvalue::Ref(_, _, ref_place) | Rvalue::AddressOf(_, ref_place) => {
Rvalue::Ref(_, _, ref_place) | Rvalue::RawPtr(_, ref_place) => {
// Here, a reference to a place is created, which leaves the place
// unchanged.
state.resolve_place(ref_place, self.instance)
Expand Down
7 changes: 3 additions & 4 deletions kani-compiler/src/kani_middle/transform/internal_mir.rs
Original file line number Diff line number Diff line change
Expand Up @@ -210,10 +210,9 @@ impl RustcInternalMir for Rvalue {

fn internal_mir<'tcx>(&self, tcx: TyCtxt<'tcx>) -> Self::T<'tcx> {
match self {
Rvalue::AddressOf(mutability, place) => rustc_middle::mir::Rvalue::AddressOf(
internal(tcx, mutability),
internal(tcx, place),
),
Rvalue::AddressOf(mutability, place) => {
rustc_middle::mir::Rvalue::RawPtr(internal(tcx, mutability), internal(tcx, place))
}
Rvalue::Aggregate(aggregate_kind, operands) => rustc_middle::mir::Rvalue::Aggregate(
Box::new(aggregate_kind.internal_mir(tcx)),
rustc_index::IndexVec::from_raw(
Expand Down
3 changes: 2 additions & 1 deletion kani-compiler/src/session.rs
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,8 @@ static JSON_PANIC_HOOK: LazyLock<Box<dyn Fn(&panic::PanicHookInfo<'_>) + Sync +
Lrc::new(SourceMap::new(FilePathMapping::empty())),
fallback_bundle,
false,
HumanReadableErrorType::Default(ColorConfig::Never),
HumanReadableErrorType::Default,
ColorConfig::Never,
);
let diagnostic = DiagInner::new(rustc_errors::Level::Bug, msg);
emitter.emit_diagnostic(diagnostic);
Expand Down
7 changes: 6 additions & 1 deletion kani-driver/src/call_cargo.rs
Original file line number Diff line number Diff line change
Expand Up @@ -73,6 +73,11 @@ impl KaniSession {
cargo_args.push("-v".into());
}

// We need this suffix push because of https://github.com/rust-lang/cargo/pull/14370
// which removes the library suffix from the build-std command
let mut full_path = std_path.to_path_buf();
full_path.push("library");

// Since we are verifying the standard library, we set the reachability to all crates.
let mut cmd = setup_cargo_command()?;
cmd.args(&cargo_args)
Expand All @@ -82,7 +87,7 @@ impl KaniSession {
// https://doc.rust-lang.org/cargo/reference/environment-variables.html
.env("CARGO_ENCODED_RUSTFLAGS", rustc_args.join(OsStr::new("\x1f")))
.env("CARGO_TERM_PROGRESS_WHEN", "never")
.env("__CARGO_TESTS_ONLY_SRC_ROOT", std_path.as_os_str());
.env("__CARGO_TESTS_ONLY_SRC_ROOT", full_path.as_os_str());

Ok(self
.run_build(cmd)?
Expand Down
3 changes: 3 additions & 0 deletions kani_metadata/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -16,3 +16,6 @@ cbmc = { path = "../cprover_bindings", package = "cprover_bindings" }
strum = "0.26"
strum_macros = "0.26"
clap = { version = "4.4.11", features = ["derive"] }

[lints]
workspace = true
3 changes: 3 additions & 0 deletions library/kani/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -15,3 +15,6 @@ kani_core = { path = "../kani_core" }
[features]
concrete_playback = []
no_core=["kani_macros/no_core"]

[lints]
workspace = true
3 changes: 3 additions & 0 deletions library/kani_core/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -14,3 +14,6 @@ kani_macros = { path = "../kani_macros"}

[features]
no_core=["kani_macros/no_core"]

[lints]
workspace = true
3 changes: 3 additions & 0 deletions library/kani_macros/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -23,3 +23,6 @@ rustc_private = true

[features]
no_core = []

[lints]
workspace = true
2 changes: 1 addition & 1 deletion library/kani_macros/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,6 @@
// So we have to enable this on the commandline (see kani-rustc) with:
// RUSTFLAGS="-Zcrate-attr=feature(register_tool) -Zcrate-attr=register_tool(kanitool)"
#![feature(proc_macro_diagnostic)]

mod derive;

// proc_macro::quote is nightly-only, so we'll cobble things together instead
Expand Down Expand Up @@ -65,6 +64,7 @@ pub fn recursion(attr: TokenStream, item: TokenStream) -> TokenStream {
/// Set Loop unwind limit for proof harnesses
/// The attribute `#[kani::unwind(arg)]` can only be called alongside `#[kani::proof]`.
/// arg - Takes in a integer value (u32) that represents the unwind value for the harness.
#[allow(clippy::too_long_first_doc_paragraph)]
#[proc_macro_attribute]
pub fn unwind(attr: TokenStream, item: TokenStream) -> TokenStream {
attr_impl::unwind(attr, item)
Expand Down
2 changes: 1 addition & 1 deletion rust-toolchain.toml
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-08-07"
channel = "nightly-2024-08-28"
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]
3 changes: 3 additions & 0 deletions tools/compiletest/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -30,3 +30,6 @@ wait-timeout = "0.2.0"

[target.'cfg(unix)'.dependencies]
libc = "0.2"

[lints]
workspace = true
1 change: 1 addition & 0 deletions tools/scanner/src/bin/scan.rs
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@
//! together with the name of the analysis.
//!
//! Look at each analysis documentation to see which files an analysis produces.
#![feature(rustc_private)]

use scanner::run_all;
use std::process::ExitCode;
Expand Down

0 comments on commit 5aad1a9

Please sign in to comment.