From e84fccd26a0c77b8c5d4248ee90aec0ffcb71696 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 1 Apr 2025 16:55:54 -0700 Subject: [PATCH 1/2] Upgrade toolchain to 2025-03-19 --- .../codegen/foreign_function.rs | 30 ++++++++++++------- kani-compiler/src/kani_middle/resolve.rs | 6 ++-- rust-toolchain.toml | 2 +- 3 files changed, 24 insertions(+), 14 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs index 169f2022a6e7..45670332a22f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs @@ -49,25 +49,35 @@ impl GotocCtx<'_> { /// handled later. pub fn codegen_foreign_fn(&mut self, instance: Instance) -> &Symbol { debug!(?instance, "codegen_foreign_function"); - let fn_name = instance.mangled_name().intern(); + let trimmed_fn_name = instance.trimmed_name().intern(); + let mangled_fn_name = instance.mangled_name().intern(); let loc = self.codegen_span_stable(instance.def.span()); - if self.symbol_table.contains(fn_name) { - // Symbol has been added (either a built-in CBMC function or a Rust allocation function). - self.symbol_table.lookup(fn_name).unwrap() - } else if RUST_ALLOC_FNS.contains(&fn_name) - || (self.is_cffi_enabled() && instance.fn_abi().unwrap().conv == CallConvention::C) - { + if self.symbol_table.contains(mangled_fn_name) { + // Symbol has been added (a built-in CBMC function) + self.symbol_table.lookup(mangled_fn_name).unwrap() + } else if self.symbol_table.contains(trimmed_fn_name) { + // Symbol has been added (a Rust allocation function) + self.symbol_table.lookup(trimmed_fn_name).unwrap() + } else if RUST_ALLOC_FNS.contains(&trimmed_fn_name) { // Add a Rust alloc lib function as is declared by core. + // We use the trimmed name to ensure that it matches the function names in kani_lib.c + self.ensure(trimmed_fn_name, |gcx, _| { + let typ = gcx.codegen_ffi_type(instance); + Symbol::function(trimmed_fn_name, typ, None, instance.name(), loc) + .with_is_extern(true) + }) + } else if self.is_cffi_enabled() && instance.fn_abi().unwrap().conv == CallConvention::C { // When C-FFI feature is enabled, we just trust the rust declaration. // TODO: Add proper casting and clashing definitions check. // https://github.com/model-checking/kani/issues/1350 // https://github.com/model-checking/kani/issues/2426 - self.ensure(fn_name, |gcx, _| { + self.ensure(mangled_fn_name, |gcx, _| { let typ = gcx.codegen_ffi_type(instance); - Symbol::function(fn_name, typ, None, instance.name(), loc).with_is_extern(true) + Symbol::function(mangled_fn_name, typ, None, instance.name(), loc) + .with_is_extern(true) }) } else { - let shim_name = format!("{fn_name}_ffi_shim"); + let shim_name = format!("{mangled_fn_name}_ffi_shim"); trace!(?shim_name, "codegen_foreign_function"); self.ensure(&shim_name, |gcx, _| { // Generate a shim with an unsupported C-FFI error message. diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs index accb4807f00e..ea51e80fbf81 100644 --- a/kani-compiler/src/kani_middle/resolve.rs +++ b/kani-compiler/src/kani_middle/resolve.rs @@ -432,10 +432,10 @@ fn resolve_relative(tcx: TyCtxt, current_module: LocalModDefId, name: &str) -> R let mut glob_imports = vec![]; let result = tcx.hir_module_free_items(current_module).find_map(|item_id| { let item = tcx.hir_item(item_id); - if item.ident.as_str() == name { + if item.kind.ident().is_some_and(|ident| ident.as_str() == name) { match item.kind { - ItemKind::Use(use_path, UseKind::Single) => use_path.res[0].opt_def_id(), - ItemKind::ExternCrate(orig_name) => resolve_external( + ItemKind::Use(use_path, UseKind::Single(_)) => use_path.res[0].opt_def_id(), + ItemKind::ExternCrate(orig_name, _) => resolve_external( tcx, orig_name.as_ref().map(|sym| sym.as_str()).unwrap_or(name), ), diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 8bfb24bdc697..082c4ff14e2d 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-03-18" +channel = "nightly-2025-03-19" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] From bbec2848eb19cafad834d161731dc9695243901c Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 1 Apr 2025 14:02:32 -0700 Subject: [PATCH 2/2] Upgrade toolchain to 2025-04-01 --- .../codegen_cprover_gotoc/codegen/function.rs | 6 ++-- .../codegen/source_region.rs | 29 +++++-------------- rust-toolchain.toml | 2 +- 3 files changed, 12 insertions(+), 25 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index 7def214fc5a8..dd6909483694 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -266,11 +266,11 @@ pub mod rustc_smir { for mapping in &cov_info.mappings { let Code { bcb } = mapping.kind else { unreachable!() }; let source_map = tcx.sess.source_map(); - let file = source_map.lookup_source_file(cov_info.body_span.lo()); + let file = source_map.lookup_source_file(mapping.span.lo()); if bcb == coverage { return Some(( - make_source_region(source_map, cov_info, &file, mapping.span).unwrap(), - rustc_internal::stable(cov_info.body_span).get_filename(), + make_source_region(source_map, &file, mapping.span).unwrap(), + rustc_internal::stable(mapping.span).get_filename(), )); } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/source_region.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/source_region.rs index aa327372321f..19cb2a7aeb01 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/source_region.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/source_region.rs @@ -5,7 +5,6 @@ //! the `Span` to `CoverageRegion` conversion defined in //! https://github.com/rust-lang/rust/tree/master/compiler/rustc_codegen_llvm/src/coverageinfo/mapgen/spans.rs -use rustc_middle::mir::coverage::FunctionCoverageInfo; use rustc_span::Span; use rustc_span::source_map::SourceMap; use rustc_span::{BytePos, SourceFile}; @@ -27,33 +26,22 @@ impl Debug for SourceRegion { } } -fn ensure_non_empty_span( - source_map: &SourceMap, - fn_cov_info: &FunctionCoverageInfo, - span: Span, -) -> Option { +fn ensure_non_empty_span(source_map: &SourceMap, span: Span) -> Option { if !span.is_empty() { return Some(span); } - let lo = span.lo(); - let hi = span.hi(); - // The span is empty, so try to expand it to cover an adjacent '{' or '}', - // but only within the bounds of the body span. - let try_next = hi < fn_cov_info.body_span.hi(); - let try_prev = fn_cov_info.body_span.lo() < lo; - if !(try_next || try_prev) { - return None; - } + + // The span is empty, so try to enlarge it to cover an adjacent '{' or '}'. source_map .span_to_source(span, |src, start, end| try { // Adjusting span endpoints by `BytePos(1)` is normally a bug, // but in this case we have specifically checked that the character // we're skipping over is one of two specific ASCII characters, so // adjusting by exactly 1 byte is correct. - if try_next && src.as_bytes()[end] == b'{' { - Some(span.with_hi(hi + BytePos(1))) - } else if try_prev && src.as_bytes()[start - 1] == b'}' { - Some(span.with_lo(lo - BytePos(1))) + if src.as_bytes().get(end).copied() == Some(b'{') { + Some(span.with_hi(span.hi() + BytePos(1))) + } else if start > 0 && src.as_bytes()[start - 1] == b'}' { + Some(span.with_lo(span.lo() - BytePos(1))) } else { None } @@ -104,11 +92,10 @@ fn check_source_region(source_region: SourceRegion) -> Option { /// better than an ICE or `llvm-cov` failure that the user might have no way to avoid. pub(crate) fn make_source_region( source_map: &SourceMap, - fn_cov_info: &FunctionCoverageInfo, file: &SourceFile, span: Span, ) -> Option { - let span = ensure_non_empty_span(source_map, fn_cov_info, span)?; + let span = ensure_non_empty_span(source_map, span)?; let lo = span.lo(); let hi = span.hi(); // Column numbers need to be in bytes, so we can't use the more convenient diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 082c4ff14e2d..61dc66fe9fc0 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-03-19" +channel = "nightly-2025-04-01" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]