diff --git a/Cargo.toml b/Cargo.toml index f2301983fcb4..149b8d2c93c8 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -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" diff --git a/cprover_bindings/Cargo.toml b/cprover_bindings/Cargo.toml index c53ffb207fcf..b0e3c578bbcf 100644 --- a/cprover_bindings/Cargo.toml +++ b/cprover_bindings/Cargo.toml @@ -24,3 +24,6 @@ linear-map = {version = "1.2", features = ["serde_impl"]} [dev-dependencies] serde_test = "1" memuse = "0.2.1" + +[lints] +workspace = true diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index fcb33b8074e4..fc06c393f3eb 100644 --- a/kani-compiler/Cargo.toml +++ b/kani-compiler/Cargo.toml @@ -35,3 +35,6 @@ write_json_symtab = [] [package.metadata.rust-analyzer] # This package uses rustc crates. rustc_private=true + +[lints] +workspace = true diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 9baa3c59f4c2..016bf0d3a261 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -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![]), @@ -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. diff --git a/kani-compiler/src/kani_middle/coercion.rs b/kani-compiler/src/kani_middle/coercion.rs index 822f32631e0c..38760fca300d 100644 --- a/kani-compiler/src/kani_middle/coercion.rs +++ b/kani-compiler/src/kani_middle/coercion.rs @@ -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(), diff --git a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs index eff7dd1fc486..68343ccaad37 100644 --- a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs +++ b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs @@ -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). @@ -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) diff --git a/kani-compiler/src/kani_middle/transform/internal_mir.rs b/kani-compiler/src/kani_middle/transform/internal_mir.rs index 0dcf7d47c13a..ba23fbf2dddf 100644 --- a/kani-compiler/src/kani_middle/transform/internal_mir.rs +++ b/kani-compiler/src/kani_middle/transform/internal_mir.rs @@ -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( diff --git a/kani-compiler/src/session.rs b/kani-compiler/src/session.rs index ecc084e0cc85..f5dd78ff86b0 100644 --- a/kani-compiler/src/session.rs +++ b/kani-compiler/src/session.rs @@ -61,7 +61,8 @@ static JSON_PANIC_HOOK: LazyLock) + 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); diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index e69062a0cd4f..ef289cead4c2 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -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) @@ -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)? diff --git a/kani_metadata/Cargo.toml b/kani_metadata/Cargo.toml index de91900d6d9c..efa28288d148 100644 --- a/kani_metadata/Cargo.toml +++ b/kani_metadata/Cargo.toml @@ -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 diff --git a/library/kani/Cargo.toml b/library/kani/Cargo.toml index 7d7ced8ee0b7..a3692f95e3f5 100644 --- a/library/kani/Cargo.toml +++ b/library/kani/Cargo.toml @@ -15,3 +15,6 @@ kani_core = { path = "../kani_core" } [features] concrete_playback = [] no_core=["kani_macros/no_core"] + +[lints] +workspace = true diff --git a/library/kani_core/Cargo.toml b/library/kani_core/Cargo.toml index 8928992c3f16..9df828e77c5a 100644 --- a/library/kani_core/Cargo.toml +++ b/library/kani_core/Cargo.toml @@ -14,3 +14,6 @@ kani_macros = { path = "../kani_macros"} [features] no_core=["kani_macros/no_core"] + +[lints] +workspace = true diff --git a/library/kani_macros/Cargo.toml b/library/kani_macros/Cargo.toml index 475e2978df91..574960e5fc0a 100644 --- a/library/kani_macros/Cargo.toml +++ b/library/kani_macros/Cargo.toml @@ -23,3 +23,6 @@ rustc_private = true [features] no_core = [] + +[lints] +workspace = true diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 6fe0979f08bc..63ed990a4840 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -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 @@ -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) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index e3b6229d73c6..3421b9b3adc9 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -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"] diff --git a/tools/compiletest/Cargo.toml b/tools/compiletest/Cargo.toml index 78a90d9aae38..967bc1715525 100644 --- a/tools/compiletest/Cargo.toml +++ b/tools/compiletest/Cargo.toml @@ -30,3 +30,6 @@ wait-timeout = "0.2.0" [target.'cfg(unix)'.dependencies] libc = "0.2" + +[lints] +workspace = true diff --git a/tools/scanner/src/bin/scan.rs b/tools/scanner/src/bin/scan.rs index 92b5319ec780..197b34d23422 100644 --- a/tools/scanner/src/bin/scan.rs +++ b/tools/scanner/src/bin/scan.rs @@ -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;