Upgrade toolchain to 2025-02-11

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

@@ -220,7 +220,7 @@ impl GotocCtx<'_> {
 pub mod rustc_smir {
     use crate::codegen_cprover_gotoc::codegen::source_region::{SourceRegion, make_source_region};
     use crate::stable_mir::CrateDef;
-    use rustc_middle::mir::coverage::CovTerm;
+    use rustc_middle::mir::coverage::BasicCoverageBlock;
     use rustc_middle::mir::coverage::MappingKind::Code;
     use rustc_middle::ty::TyCtxt;
     use rustc_smir::rustc_internal;
@@ -236,16 +236,16 @@ pub mod rustc_smir {
         coverage_opaque: &CoverageOpaque,
         instance: Instance,
     ) -> Option<(SourceRegion, Filename)> {
-        let cov_term = parse_coverage_opaque(coverage_opaque);
-        region_from_coverage(tcx, cov_term, instance)
+        let bcb = parse_coverage_opaque(coverage_opaque);
+        region_from_coverage(tcx, bcb, instance)
     }
 
-    /// Retrieves the `SourceRegion` associated with a `CovTerm` object.
+    /// Retrieves the `SourceRegion` associated with a `BasicCoverageBlock` object.
     ///
     /// Note: This function could be in the internal `rustc` impl for `Coverage`.
     pub fn region_from_coverage(
         tcx: TyCtxt<'_>,
-        coverage: CovTerm,
+        coverage: BasicCoverageBlock,
         instance: Instance,
     ) -> Option<(SourceRegion, Filename)> {
         // We need to pull the coverage info from the internal MIR instance.
@@ -257,10 +257,10 @@ pub mod rustc_smir {
         if let Some(cov_info) = &body.function_coverage_info {
             // Iterate over the coverage mappings and match with the coverage term.
             for mapping in &cov_info.mappings {
-                let Code(term) = mapping.kind else { unreachable!() };
+                let Code { bcb } = mapping.kind else { unreachable!() };
                 let source_map = tcx.sess.source_map();
                 let file = source_map.lookup_source_file(cov_info.body_span.lo());
-                if term == coverage {
+                if bcb == coverage {
                     return Some((
                         make_source_region(source_map, cov_info, &file, mapping.span).unwrap(),
                         rustc_internal::stable(cov_info.body_span).get_filename(),
@@ -271,25 +271,17 @@ pub mod rustc_smir {
         None
     }
 
-    /// Parse a `CoverageOpaque` item and return the corresponding `CovTerm`:
-    /// <https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/coverage/enum.CovTerm.html>
-    ///
-    /// At present, a `CovTerm` can be one of the following:
-    ///  - `CounterIncrement(<num>)`: A physical counter.
-    ///  - `ExpressionUsed(<num>)`: An expression-based counter.
-    ///  - `Zero`: A counter with a constant zero value.
-    fn parse_coverage_opaque(coverage_opaque: &Opaque) -> CovTerm {
+    /// Parse a `CoverageOpaque` item and return the corresponding `BasicCoverageBlock`:
+    fn parse_coverage_opaque(coverage_opaque: &Opaque) -> BasicCoverageBlock {
         let coverage_str = coverage_opaque.to_string();
-        if let Some(rest) = coverage_str.strip_prefix("CounterIncrement(") {
-            let (num_str, _rest) = rest.split_once(')').unwrap();
-            let num = num_str.parse::<u32>().unwrap();
-            CovTerm::Counter(num.into())
-        } else if let Some(rest) = coverage_str.strip_prefix("ExpressionUsed(") {
+        if let Some(rest) = coverage_str.strip_prefix("VirtualCounter(bcb") {
             let (num_str, _rest) = rest.split_once(')').unwrap();
             let num = num_str.parse::<u32>().unwrap();
-            CovTerm::Expression(num.into())
+            BasicCoverageBlock::from_u32(num)
         } else {
-            CovTerm::Zero
+            // When the coverage statement is injected into mir_body, it always has the form CoverageKind::VirtualCounter { bcb }
+            // https://github.com/rust-lang/rust/pull/136053/files#diff-c99ec9a281dce4a381fa7e11cf2d04f55dba5573d1d14389d47929fe0a154d24R209-R212
+            unreachable!();
         }
     }
 }

kani-driver/src/call_cbmc.rs

@@ -501,7 +501,7 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option<CoverageR
         static COUNTER_RE: OnceLock<Regex> = OnceLock::new();
         COUNTER_RE.get_or_init(|| {
             Regex::new(
-                r#"^(?<kind>CounterIncrement|ExpressionUsed)\((?<counter_num>[0-9]+)\) \$(?<func_name>[^\$]+)\$ - (?<span>.+)"#,
+                r#"^(?<kind>VirtualCounter\(bcb)(?<counter_num>[0-9]+)\) \$(?<func_name>[^\$]+)\$ - (?<span>.+)"#,
             )
             .unwrap()
         })
@@ -511,20 +511,14 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option<CoverageR
 
     for prop in cov_properties {
         let mut prop_processed = false;
-
         if let Some(captures) = counter_re.captures(&prop.description) {
-            let kind = &captures["kind"];
             let counter_num = &captures["counter_num"];
             let function = demangle(&captures["func_name"]).to_string();
             let status = prop.status;
             let span = captures["span"].to_string();
 
             let counter_id = counter_num.parse().unwrap();
-            let term = match kind {
-                "CounterIncrement" => CoverageTerm::Counter(counter_id),
-                "ExpressionUsed" => CoverageTerm::Expression(counter_id),
-                _ => unreachable!("counter kind could not be recognized: {:?}", kind),
-            };
+            let term = CoverageTerm::Counter(counter_id);
             let region = CoverageRegion::from_str(span);
 
             let cov_check = CoverageCheck::new(function, term, region, status);

kani-driver/src/coverage/cov_results.rs

@@ -64,7 +64,6 @@ impl CoverageCheck {
 #[derive(Debug, Clone, Serialize, Deserialize)]
 pub enum CoverageTerm {
     Counter(u32),
-    Expression(u32),
 }
 
 #[derive(Debug, Clone, Eq, PartialEq, PartialOrd, Ord, Serialize, Deserialize)]

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2025-02-10"
+channel = "nightly-2025-02-11"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]