From 93da29161650434687f88595953f766bce4ac0d8 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 13 Nov 2025 12:57:41 +0000 Subject: [PATCH 1/2] Upgrade Rust toolchain to 2025-11-13 Relevant upstream PR: - https://github.com/rust-lang/rust/pull/148531 (rustc_target: introduce Abi, Env, Os) Resolves: #4471 --- .../codegen_aeneas_llbc/compiler_interface.rs | 10 ++++++++- .../compiler_interface.rs | 22 +++++++++++-------- rust-toolchain.toml | 2 +- 3 files changed, 23 insertions(+), 11 deletions(-) diff --git a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs index d146c5bfa97..c7fa8179a9f 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs @@ -39,6 +39,7 @@ use rustc_public::{CrateDef, DefId}; use rustc_session::Session; use rustc_session::config::{CrateType, OutputFilenames, OutputType}; use rustc_session::output::out_filename; +use rustc_target::spec::Arch; use std::any::Any; use std::fs::File; use std::path::Path; @@ -376,7 +377,14 @@ fn codegen_results(tcx: TyCtxt) -> Box { CodegenResults { modules: vec![], allocator_module: None, - crate_info: CrateInfo::new(tcx, tcx.sess.target.arch.clone().to_string()), + crate_info: CrateInfo::new( + tcx, + match tcx.sess.target.arch { + Arch::X86_64 => "x86_64".to_string(), + Arch::AArch64 => "aarch64".to_string(), + _ => format!("{:?}", tcx.sess.target.arch).to_lowercase(), + }, + ), }, work_products, )) diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 9b044e8aeea..c230e225d13 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -43,7 +43,7 @@ use rustc_session::Session; use rustc_session::config::{CrateType, OutputFilenames, OutputType}; use rustc_session::output::out_filename; use rustc_span::{Symbol, sym}; -use rustc_target::spec::{Arch, PanicStrategy}; +use rustc_target::spec::{Arch, Os, PanicStrategy}; use std::any::Any; use std::cmp::min; use std::collections::BTreeMap; @@ -302,15 +302,15 @@ impl CodegenBackend for GotocCodegenBackend { fn target_config(&self, sess: &Session) -> TargetConfig { // This code is adapted from the cranelift backend: // https://github.com/rust-lang/rust/blob/a124fb3cb7291d75872934f411d81fe298379ace/compiler/rustc_codegen_cranelift/src/lib.rs#L184 - let target_features = if sess.target.arch == Arch::X86_64 && sess.target.os != "none" { + let target_features = if sess.target.arch == Arch::X86_64 && sess.target.os != Os::None { // x86_64 mandates SSE2 support and rustc requires the x87 feature to be enabled vec![sym::sse, sym::sse2, Symbol::intern("x87")] } else if sess.target.arch == Arch::AArch64 { - match &*sess.target.os { - "none" => vec![], + match sess.target.os { + Os::None => vec![], // On macOS the aes, sha2 and sha3 features are enabled by default and ring // fails to compile on macOS when they are not present. - "macos" => vec![sym::neon, sym::aes, sym::sha2, sym::sha3], + Os::MacOS => vec![sym::neon, sym::aes, sym::sha2, sym::sha3], // AArch64 mandates Neon support _ => vec![sym::neon], } @@ -818,7 +818,11 @@ fn new_machine_model(sess: &Session) -> MachineModel { let wchar_t_width = 32; MachineModel { - architecture: architecture.to_string(), + architecture: match architecture { + Arch::X86_64 => "x86_64".to_string(), + Arch::AArch64 => "aarch64".to_string(), + _ => panic!("Unsupported architecture: {:?}", architecture), + }, alignment, bool_width, char_is_unsigned, @@ -848,8 +852,8 @@ fn new_machine_model(sess: &Session) -> MachineModel { let double_width = 64; let float_width = 32; let int_width = 32; - let long_double_width = match os.as_ref() { - "linux" => 128, + let long_double_width = match os { + Os::Linux => 128, _ => 64, }; let long_int_width = 64; @@ -859,7 +863,7 @@ fn new_machine_model(sess: &Session) -> MachineModel { // https://developer.arm.com/documentation/dui0491/i/Compiler-Command-line-Options/--signed-chars----unsigned-chars // https://www.arm.linux.org.uk/docs/faqs/signedchar.php // https://developer.apple.com/documentation/xcode/writing-arm64-code-for-apple-platforms - let wchar_t_is_unsigned = matches!(os.as_ref(), "linux"); + let wchar_t_is_unsigned = matches!(os, Os::Linux); let wchar_t_width = 32; MachineModel { diff --git a/rust-toolchain.toml b/rust-toolchain.toml index bf8fffdca8a..0791fdfc4aa 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-11-12" +channel = "nightly-2025-11-13" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] From ec4917f0c88ef010ab39bafdf8be9b6a75d2a456 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 13 Nov 2025 13:10:05 +0000 Subject: [PATCH 2/2] Fix typo --- kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index c230e225d13..c111f906e5b 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -310,7 +310,7 @@ impl CodegenBackend for GotocCodegenBackend { Os::None => vec![], // On macOS the aes, sha2 and sha3 features are enabled by default and ring // fails to compile on macOS when they are not present. - Os::MacOS => vec![sym::neon, sym::aes, sym::sha2, sym::sha3], + Os::MacOs => vec![sym::neon, sym::aes, sym::sha2, sym::sha3], // AArch64 mandates Neon support _ => vec![sym::neon], }