diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs index 4fce3f7494b6..84b20a623541 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs @@ -156,13 +156,14 @@ impl GotocCtx<'_> { counter_data: &str, span: SpanStable, source_region: SourceRegion, + file_name: &str, ) -> Stmt { let loc = self.codegen_caller_span_stable(span); // Should use Stmt::cover, but currently this doesn't work with CBMC // unless it is run with '--cover cover' (see // https://github.com/diffblue/cbmc/issues/6613). So for now use // `assert(false)`. - let msg = format!("{counter_data} - {source_region:?}"); + let msg = format!("{counter_data} - {file_name}:{source_region:?}"); self.codegen_assert(Expr::bool_false(), PropertyClass::CodeCoverage, &msg, loc) } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index 3b92dcdae876..ed5c5c593b20 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -223,8 +223,9 @@ pub mod rustc_smir { use rustc_middle::mir::coverage::MappingKind::Code; use rustc_middle::mir::coverage::SourceRegion; use rustc_middle::ty::TyCtxt; - use stable_mir::Opaque; + use rustc_smir::rustc_internal; use stable_mir::mir::mono::Instance; + use stable_mir::{Filename, Opaque}; type CoverageOpaque = stable_mir::Opaque; @@ -234,7 +235,7 @@ pub mod rustc_smir { tcx: TyCtxt, coverage_opaque: &CoverageOpaque, instance: Instance, - ) -> Option { + ) -> Option<(SourceRegion, Filename)> { let cov_term = parse_coverage_opaque(coverage_opaque); region_from_coverage(tcx, cov_term, instance) } @@ -246,7 +247,7 @@ pub mod rustc_smir { tcx: TyCtxt<'_>, coverage: CovTerm, instance: Instance, - ) -> Option { + ) -> Option<(SourceRegion, Filename)> { // 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)); @@ -258,7 +259,10 @@ pub mod rustc_smir { for mapping in &cov_info.mappings { let Code(term) = mapping.kind else { unreachable!() }; if term == coverage { - return Some(mapping.source_region.clone()); + return Some(( + mapping.source_region.clone(), + rustc_internal::stable(cov_info.body_span).get_filename(), + )); } } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index ab02d54b2559..8171c5ffdda3 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -165,9 +165,9 @@ impl GotocCtx<'_> { let counter_data = format!("{coverage_opaque:?} ${function_name}$"); let maybe_source_region = region_from_coverage_opaque(self.tcx, &coverage_opaque, instance); - if let Some(source_region) = maybe_source_region { + if let Some((source_region, file_name)) = maybe_source_region { let coverage_stmt = - self.codegen_coverage(&counter_data, stmt.span, source_region); + self.codegen_coverage(&counter_data, stmt.span, source_region, &file_name); // TODO: Avoid single-statement blocks when conversion of // standalone statements to the irep format is fixed. // More details in diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 16b1d374e0b9..03cddbfea649 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2024-11-09" +channel = "nightly-2024-11-11" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/coverage/assert/expected b/tests/coverage/assert/expected index c2f3ffbe733e..17dbcb42c205 100644 --- a/tests/coverage/assert/expected +++ b/tests/coverage/assert/expected @@ -10,7 +10,7 @@ 10| 1| if x < 3 ```{'''\ 11| 0| ``` // unreachable'''\ 12| 0| ``` assert!(x == 2);'''\ - 13| 0| ``` }'''``` '''\ + 13| 0| ``` ```}''''''\ 14| 1| } else {\ 15| 1| // passes\ 16| 1| assert!(x <= 5);\ diff --git a/tests/coverage/known_issues/assert_uncovered_end/expected b/tests/coverage/known_issues/assert_uncovered_end/expected index 2f6fca5e4aae..170217d73b31 100644 --- a/tests/coverage/known_issues/assert_uncovered_end/expected +++ b/tests/coverage/known_issues/assert_uncovered_end/expected @@ -10,5 +10,5 @@ 10| 1| let x: u32 = kani::any_where(|val| *val == 5);\ 11| 1| if x > 3 {\ 12| 1| assert!(x > 4);\ - 13| 1| }``` '''\ + 13| 1| ```}'''\ 14| | }\