Skip to content
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
33 changes: 27 additions & 6 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
Original file line number Diff line number Diff line change
Expand Up @@ -247,6 +247,24 @@ pub mod rustc_smir {
region_from_coverage(tcx, bcb, instance)
}

pub fn merge_source_region(source_regions: Vec<SourceRegion>) -> SourceRegion {
let start_line = source_regions.iter().map(|sr| sr.start_line).min().unwrap();
let start_col = source_regions
.iter()
.filter(|sr| sr.start_line == start_line)
.map(|sr| sr.start_col)
.min()
.unwrap();
let end_line = source_regions.iter().map(|sr| sr.end_line).max().unwrap();
let end_col = source_regions
.iter()
.filter(|sr| sr.end_line == end_line)
.map(|sr| sr.end_col)
.max()
.unwrap();
SourceRegion { start_line, start_col, end_line, end_col }
}

/// Retrieves the `SourceRegion` associated with a `BasicCoverageBlock` object.
///
/// Note: This function could be in the internal `rustc` impl for `Coverage`.
Expand All @@ -258,22 +276,25 @@ pub mod rustc_smir {
// We need to pull the coverage info from the internal MIR instance.
let instance_def = rustc_smir::rustc_internal::internal(tcx, instance.def.def_id());
let body = tcx.instance_mir(rustc_middle::ty::InstanceKind::Item(instance_def));

let filename = rustc_internal::stable(body.span).get_filename();
// Some functions, like `std` ones, may not have coverage info attached
// to them because they have been compiled without coverage flags.
if let Some(cov_info) = &body.function_coverage_info {
// Iterate over the coverage mappings and match with the coverage term.
let mut source_regions: Vec<SourceRegion> = Vec::new();
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(mapping.span.lo());
if bcb == coverage {
return Some((
make_source_region(source_map, &file, mapping.span).unwrap(),
rustc_internal::stable(mapping.span).get_filename(),
));
if bcb == coverage
&& let Some(source_region) = make_source_region(source_map, &file, mapping.span)
{
source_regions.push(source_region);
}
}
if !source_regions.is_empty() {
return Some((merge_source_region(source_regions), filename));
}
}
None
}
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-05-06"
channel = "nightly-2025-05-07"
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]
2 changes: 1 addition & 1 deletion tests/coverage/abort/expected
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
8| | #[kani::proof]\
9| 1| fn main() {\
10| 1| for i in 0..4 {\
11| | if i == 1 {\
11| 1| if i == 1 {\
12| | // This comes first and it should be reachable.\
13| 1| process::abort();\
14| 1| }\
Expand Down
2 changes: 1 addition & 1 deletion tests/coverage/assert_eq/expected
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
5| 1| fn main() {\
6| 1| let x: i32 = kani::any();\
7| 1| let y = if x > 10 { 15 } else { 33 };\
8| 0| if y > 50 ```{'''\
8| 1| if y > 50 ```{'''\
9| 0| ``` assert_eq!(y, 55);'''\
10| 1| ``` }'''\
11| | }\
2 changes: 1 addition & 1 deletion tests/coverage/break/expected
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
3| | \
4| 1| fn find_positive(nums: &[i32]) -> Option<i32> {\
5| 1| for &num in nums {\
6| | if num > 0 {\
6| 1| if num > 0 {\
7| 1| return Some(num);\
8| 1| } \
9| | }\
Expand Down
2 changes: 1 addition & 1 deletion tests/coverage/debug-assert/expected
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@
9| | #[kani::proof]\
10| 1| fn main() {\
11| 1| for i in 0..4 {\
12| 0| debug_assert!(i > 0, ```"This should fail and stop the execution"''');\
12| 1| debug_assert!(i > 0, ```"This should fail and stop the execution"''');\
13| 0| ```assert!(i == 0''', ```"This should be unreachable"''');\
14| | }\
15| | }\
2 changes: 1 addition & 1 deletion tests/coverage/early-return/expected
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
3| | \
4| 1| fn find_index(nums: &[i32], target: i32) -> Option<usize> {\
5| 1| for (index, &num) in nums.iter().enumerate() {\
6| | if num == target {\
6| 1| if num == target {\
7| 1| return Some(index);\
8| 1| } \
9| | }\
Expand Down
Loading