Skip to content

Commit e232f16

Browse files
Toolchain upgrade to nightly-2025-05-07 (#4070)
This PR upgrades the toolchain to nightly-2025-05-07. Some wrong coverage expected tests are fixed. Relevant uptream PR: rust-lang/rust@77a7ae4e9f coverage: Handle hole spans without dividing spans into buckets rust-lang/rust@4d5a1acebf coverage: Only merge adjacent coverage spans General idea: The spans of BasicCoverageBlock are not merged automatically , so we have to do that from Kani side. Resolves #4063 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
1 parent db238e6 commit e232f16

File tree

7 files changed

+33
-12
lines changed

7 files changed

+33
-12
lines changed

kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs

Lines changed: 27 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -258,6 +258,24 @@ pub mod rustc_smir {
258258
region_from_coverage(tcx, bcb, instance)
259259
}
260260

261+
pub fn merge_source_region(source_regions: Vec<SourceRegion>) -> SourceRegion {
262+
let start_line = source_regions.iter().map(|sr| sr.start_line).min().unwrap();
263+
let start_col = source_regions
264+
.iter()
265+
.filter(|sr| sr.start_line == start_line)
266+
.map(|sr| sr.start_col)
267+
.min()
268+
.unwrap();
269+
let end_line = source_regions.iter().map(|sr| sr.end_line).max().unwrap();
270+
let end_col = source_regions
271+
.iter()
272+
.filter(|sr| sr.end_line == end_line)
273+
.map(|sr| sr.end_col)
274+
.max()
275+
.unwrap();
276+
SourceRegion { start_line, start_col, end_line, end_col }
277+
}
278+
261279
/// Retrieves the `SourceRegion` associated with a `BasicCoverageBlock` object.
262280
///
263281
/// Note: This function could be in the internal `rustc` impl for `Coverage`.
@@ -269,22 +287,25 @@ pub mod rustc_smir {
269287
// We need to pull the coverage info from the internal MIR instance.
270288
let instance_def = rustc_smir::rustc_internal::internal(tcx, instance.def.def_id());
271289
let body = tcx.instance_mir(rustc_middle::ty::InstanceKind::Item(instance_def));
272-
290+
let filename = rustc_internal::stable(body.span).get_filename();
273291
// Some functions, like `std` ones, may not have coverage info attached
274292
// to them because they have been compiled without coverage flags.
275293
if let Some(cov_info) = &body.function_coverage_info {
276294
// Iterate over the coverage mappings and match with the coverage term.
295+
let mut source_regions: Vec<SourceRegion> = Vec::new();
277296
for mapping in &cov_info.mappings {
278297
let Code { bcb } = mapping.kind else { unreachable!() };
279298
let source_map = tcx.sess.source_map();
280299
let file = source_map.lookup_source_file(mapping.span.lo());
281-
if bcb == coverage {
282-
return Some((
283-
make_source_region(source_map, &file, mapping.span).unwrap(),
284-
rustc_internal::stable(mapping.span).get_filename(),
285-
));
300+
if bcb == coverage
301+
&& let Some(source_region) = make_source_region(source_map, &file, mapping.span)
302+
{
303+
source_regions.push(source_region);
286304
}
287305
}
306+
if !source_regions.is_empty() {
307+
return Some((merge_source_region(source_regions), filename));
308+
}
288309
}
289310
None
290311
}

rust-toolchain.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,5 @@
22
# SPDX-License-Identifier: Apache-2.0 OR MIT
33

44
[toolchain]
5-
channel = "nightly-2025-05-06"
5+
channel = "nightly-2025-05-07"
66
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

tests/coverage/abort/expected

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@
88
8| | #[kani::proof]\
99
9| 1| fn main() {\
1010
10| 1| for i in 0..4 {\
11-
11| | if i == 1 {\
11+
11| 1| if i == 1 {\
1212
12| | // This comes first and it should be reachable.\
1313
13| 1| process::abort();\
1414
14| 1| }\

tests/coverage/assert_eq/expected

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55
5| 1| fn main() {\
66
6| 1| let x: i32 = kani::any();\
77
7| 1| let y = if x > 10 { 15 } else { 33 };\
8-
8| 0| if y > 50 ```{'''\
8+
8| 1| if y > 50 ```{'''\
99
9| 0| ``` assert_eq!(y, 55);'''\
1010
10| 1| ``` }'''\
1111
11| | }\

tests/coverage/break/expected

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
3| | \
44
4| 1| fn find_positive(nums: &[i32]) -> Option<i32> {\
55
5| 1| for &num in nums {\
6-
6| | if num > 0 {\
6+
6| 1| if num > 0 {\
77
7| 1| return Some(num);\
88
8| 1| } \
99
9| | }\

tests/coverage/debug-assert/expected

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@
99
9| | #[kani::proof]\
1010
10| 1| fn main() {\
1111
11| 1| for i in 0..4 {\
12-
12| 0| debug_assert!(i > 0, ```"This should fail and stop the execution"''');\
12+
12| 1| debug_assert!(i > 0, ```"This should fail and stop the execution"''');\
1313
13| 0| ```assert!(i == 0''', ```"This should be unreachable"''');\
1414
14| | }\
1515
15| | }\

tests/coverage/early-return/expected

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
3| | \
44
4| 1| fn find_index(nums: &[i32], target: i32) -> Option<usize> {\
55
5| 1| for (index, &num) in nums.iter().enumerate() {\
6-
6| | if num == target {\
6+
6| 1| if num == target {\
77
7| 1| return Some(index);\
88
8| 1| } \
99
9| | }\

0 commit comments

Comments
 (0)