Upgrade toolchain to nightly-2024-11-11

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)
     }
 

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

@@ -218,11 +218,14 @@ impl GotocCtx<'_> {
 }
 
 pub mod rustc_smir {
+    use crate::rustc_session::RemapFileNameExt;
     use crate::stable_mir::CrateDef;
     use rustc_middle::mir::coverage::CovTerm;
     use rustc_middle::mir::coverage::MappingKind::Code;
     use rustc_middle::mir::coverage::SourceRegion;
     use rustc_middle::ty::TyCtxt;
+    use rustc_session::config::RemapPathScopeComponents;
+    use rustc_span::{Span, Symbol};
     use stable_mir::Opaque;
     use stable_mir::mir::mono::Instance;
 
@@ -234,7 +237,7 @@ pub mod rustc_smir {
         tcx: TyCtxt,
         coverage_opaque: &CoverageOpaque,
         instance: Instance,
-    ) -> Option<SourceRegion> {
+    ) -> Option<(SourceRegion, Symbol)> {
         let cov_term = parse_coverage_opaque(coverage_opaque);
         region_from_coverage(tcx, cov_term, instance)
     }
@@ -246,7 +249,7 @@ pub mod rustc_smir {
         tcx: TyCtxt<'_>,
         coverage: CovTerm,
         instance: Instance,
-    ) -> Option<SourceRegion> {
+    ) -> Option<(SourceRegion, Symbol)> {
         // 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 +261,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(),
+                        span_file_name(tcx, cov_info.body_span),
+                    ));
                 }
             }
         }
@@ -286,4 +292,11 @@ pub mod rustc_smir {
             CovTerm::Zero
         }
     }
+
+    pub fn span_file_name(tcx: TyCtxt<'_>, span: Span) -> Symbol {
+        let source_file = tcx.sess.source_map().lookup_source_file(span.lo());
+        let name =
+            source_file.name.for_scope(tcx.sess, RemapPathScopeComponents::MACRO).to_string_lossy();
+        Symbol::intern(&name)
+    }
 }

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

@@ -165,9 +165,10 @@ 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_symbol)) = maybe_source_region {
+                    let file_name = format!("{file_symbol}");
                     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 <https://github.com/model-checking/kani/issues/3012>

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"]

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);\

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|     | }\