Skip to content

Upgrade toolchain to 2025-04-01 #3973

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Apr 2, 2025
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
6 changes: 3 additions & 3 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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(),
));
}
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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};
Expand All @@ -27,33 +26,22 @@ impl Debug for SourceRegion {
}
}

fn ensure_non_empty_span(
source_map: &SourceMap,
fn_cov_info: &FunctionCoverageInfo,
span: Span,
) -> Option<Span> {
fn ensure_non_empty_span(source_map: &SourceMap, span: Span) -> Option<Span> {
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
}
Expand Down Expand Up @@ -104,11 +92,10 @@ fn check_source_region(source_region: SourceRegion) -> Option<SourceRegion> {
/// 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<SourceRegion> {
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
Expand Down
6 changes: 3 additions & 3 deletions kani-compiler/src/kani_middle/resolve.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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),
),
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-2025-03-18"
channel = "nightly-2025-04-01"
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]
Loading