From b1f1f5286e360f8619084db97b66e22aca3fba89 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Sun, 26 Jan 2025 16:00:19 -0500 Subject: [PATCH 1/4] Toolchain upgrade to nightly-2025-01-26 Signed-off-by: Felipe R. Monteiro --- rust-toolchain.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 9ae762092eb2..6799f7fbc422 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2025-01-24" +channel = "nightly-2025-01-26" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] From d2aaa616c1b517e822fe2e83ddfbd0304e149f4e Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Sun, 26 Jan 2025 16:54:41 -0500 Subject: [PATCH 2/4] Remove RunCompiler Signed-off-by: Felipe R. Monteiro --- kani-compiler/src/kani_compiler.rs | 15 ++++++++------- kani-compiler/src/main.rs | 5 ++--- kani-compiler/src/session.rs | 2 +- 3 files changed, 11 insertions(+), 11 deletions(-) diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index 253a9b88a52c..e4bfba3113b0 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/kani-compiler/src/kani_compiler.rs @@ -3,7 +3,7 @@ //! This module defines all compiler extensions that form the Kani compiler. //! -//! The [KaniCompiler] can be used across multiple rustc driver runs ([RunCompiler::run()]), +//! The [KaniCompiler] can be used across multiple rustc driver runs ([`rustc_driver::run_compiler`]), //! which is used to implement stubs. //! //! In the first run, [KaniCompiler::config] will implement the compiler configuration and it will @@ -25,7 +25,7 @@ use crate::kani_queries::QueryDb; use crate::session::init_session; use clap::Parser; use rustc_codegen_ssa::traits::CodegenBackend; -use rustc_driver::{Callbacks, Compilation, RunCompiler}; +use rustc_driver::{Callbacks, Compilation, run_compiler}; use rustc_interface::Config; use rustc_middle::ty::TyCtxt; use rustc_session::config::ErrorOutputType; @@ -34,7 +34,7 @@ use std::sync::{Arc, Mutex}; use tracing::debug; /// Run the Kani flavour of the compiler. -/// This may require multiple runs of the rustc driver ([RunCompiler::run]). +/// This may require multiple runs of the rustc driver ([`rustc_driver::run_compiler`]). pub fn run(args: Vec) { let mut kani_compiler = KaniCompiler::new(); kani_compiler.run(args); @@ -96,10 +96,7 @@ impl KaniCompiler { /// actually invoke the rust compiler multiple times. pub fn run(&mut self, args: Vec) { debug!(?args, "run_compilation_session"); - let queries = self.queries.clone(); - let mut compiler = RunCompiler::new(&args, self); - compiler.set_make_codegen_backend(Some(Box::new(move |_cfg| backend(queries)))); - compiler.run(); + run_compiler(&args, self); } } @@ -108,6 +105,10 @@ impl Callbacks for KaniCompiler { /// Configure the [KaniCompiler] `self` object during the [CompilationStage::Init]. fn config(&mut self, config: &mut Config) { let mut args = vec!["kani-compiler".to_string()]; + config.make_codegen_backend = Some(Box::new({ + let queries = self.queries.clone(); + move |_cfg| backend(queries) + })); args.extend(config.opts.cg.llvm_args.iter().cloned()); let args = Arguments::parse_from(args); init_session(&args, matches!(config.opts.error_format, ErrorOutputType::Json { .. })); diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs index 65424f6d46bf..c8a56d3ef062 100644 --- a/kani-compiler/src/main.rs +++ b/kani-compiler/src/main.rs @@ -50,7 +50,7 @@ mod kani_middle; mod kani_queries; mod session; -use rustc_driver::{RunCompiler, TimePassesCallbacks}; +use rustc_driver::{TimePassesCallbacks, run_compiler}; use std::env; /// Main function. Configure arguments and run the compiler. @@ -63,8 +63,7 @@ fn main() { kani_compiler::run(rustc_args); } else { let mut callbacks = TimePassesCallbacks::default(); - let compiler = RunCompiler::new(&rustc_args, &mut callbacks); - compiler.run(); + run_compiler(&rustc_args, &mut callbacks); } } diff --git a/kani-compiler/src/session.rs b/kani-compiler/src/session.rs index f448afb801cc..5b4990790a10 100644 --- a/kani-compiler/src/session.rs +++ b/kani-compiler/src/session.rs @@ -57,7 +57,7 @@ static JSON_PANIC_HOOK: LazyLock) + Sync + let mut emitter = JsonEmitter::new( Box::new(io::BufWriter::new(io::stderr())), #[allow(clippy::arc_with_non_send_sync)] - Lrc::new(SourceMap::new(FilePathMapping::empty())), + Some(Lrc::new(SourceMap::new(FilePathMapping::empty()))), fallback_bundle, false, HumanReadableErrorType::Default, From fc2c865404779a2046577cb33efe9a73760a99ae Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Mon, 27 Jan 2025 14:34:39 -0500 Subject: [PATCH 3/4] Toolchain upgrade to nightly-2025-01-27 Signed-off-by: Felipe R. Monteiro --- rust-toolchain.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 6799f7fbc422..fa14c8c40293 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2025-01-26" +channel = "nightly-2025-01-27" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] From 1477ddb74eac7c88a0d23cd0f2dbd2d2ecf9dbd5 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Tue, 28 Jan 2025 12:35:16 -0500 Subject: [PATCH 4/4] Toolchain upgrade to nightly-2025-01-28 Signed-off-by: Felipe R. Monteiro --- rust-toolchain.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index fa14c8c40293..3741e551a5b8 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2025-01-27" +channel = "nightly-2025-01-28" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]