From 62d805747327b93f60f7d992ca30a3c918507292 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 13 May 2025 10:33:46 -0700 Subject: [PATCH 1/5] toolchain upgrade --- rust-toolchain.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 0fb26468fadc..f1eb90721eb6 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-05-06" +channel = "nightly-2025-05-07" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] From f58fb91b1338f7bed5f0f12950cb56d006d000a1 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 13 May 2025 10:34:00 -0700 Subject: [PATCH 2/5] fix coverage --- .../codegen_cprover_gotoc/codegen/function.rs | 31 ++++++++++++++++--- 1 file changed, 26 insertions(+), 5 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index dd6909483694..c7ba1b36a768 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -247,6 +247,24 @@ pub mod rustc_smir { region_from_coverage(tcx, bcb, instance) } + pub fn merge_source_region(source_regions: Vec) -> 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`. @@ -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 = 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(), - )); + let source_region = + make_source_region(source_map, &file, mapping.span).unwrap(); + source_regions.push(source_region); } } + if !source_regions.is_empty() { + return Some((merge_source_region(source_regions), filename)); + } } None } From bd53ca9926a7e5105c5e897f6a1d7517ea16985a Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 13 May 2025 10:46:17 -0700 Subject: [PATCH 3/5] fix unwarap --- .../src/codegen_cprover_gotoc/codegen/function.rs | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index c7ba1b36a768..a3ea586fcc01 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -287,9 +287,10 @@ pub mod rustc_smir { let source_map = tcx.sess.source_map(); let file = source_map.lookup_source_file(mapping.span.lo()); if bcb == coverage { - let source_region = - make_source_region(source_map, &file, mapping.span).unwrap(); - source_regions.push(source_region); + if let Some(source_region) = make_source_region(source_map, &file, mapping.span) + { + source_regions.push(source_region); + } } } if !source_regions.is_empty() { From 875c87865d064a4f72a0a5ebfce41fc0b4bb9ddd Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 13 May 2025 13:16:12 -0700 Subject: [PATCH 4/5] fix coverage --- tests/coverage/abort/expected | 2 +- tests/coverage/assert_eq/expected | 2 +- tests/coverage/break/expected | 2 +- tests/coverage/debug-assert/expected | 2 +- tests/coverage/early-return/expected | 2 +- 5 files changed, 5 insertions(+), 5 deletions(-) diff --git a/tests/coverage/abort/expected b/tests/coverage/abort/expected index 0334841a880e..ae63575af3bc 100644 --- a/tests/coverage/abort/expected +++ b/tests/coverage/abort/expected @@ -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| }\ diff --git a/tests/coverage/assert_eq/expected b/tests/coverage/assert_eq/expected index 0cc1e01fbca9..8665bb8bcbeb 100644 --- a/tests/coverage/assert_eq/expected +++ b/tests/coverage/assert_eq/expected @@ -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| | }\ diff --git a/tests/coverage/break/expected b/tests/coverage/break/expected index e1570030f6ae..25d192336b7c 100644 --- a/tests/coverage/break/expected +++ b/tests/coverage/break/expected @@ -3,7 +3,7 @@ 3| | \ 4| 1| fn find_positive(nums: &[i32]) -> Option {\ 5| 1| for &num in nums {\ - 6| | if num > 0 {\ + 6| 1| if num > 0 {\ 7| 1| return Some(num);\ 8| 1| } \ 9| | }\ diff --git a/tests/coverage/debug-assert/expected b/tests/coverage/debug-assert/expected index 82ad7c992ca3..d36fc11843d0 100644 --- a/tests/coverage/debug-assert/expected +++ b/tests/coverage/debug-assert/expected @@ -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| | }\ diff --git a/tests/coverage/early-return/expected b/tests/coverage/early-return/expected index efdd71ee91f0..4df1f1922603 100644 --- a/tests/coverage/early-return/expected +++ b/tests/coverage/early-return/expected @@ -3,7 +3,7 @@ 3| | \ 4| 1| fn find_index(nums: &[i32], target: i32) -> Option {\ 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| | }\ From c5f3cf7e1c108e5f0fa886fbad1ad950614a0712 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 13 May 2025 13:22:23 -0700 Subject: [PATCH 5/5] fix clippy --- .../src/codegen_cprover_gotoc/codegen/function.rs | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index a3ea586fcc01..10df35d34d62 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -286,11 +286,10 @@ pub mod rustc_smir { 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 { - if let Some(source_region) = make_source_region(source_map, &file, mapping.span) - { - source_regions.push(source_region); - } + 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() {