diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs index 4ee81d0c7d3e..72ccb95cf97b 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs @@ -21,7 +21,7 @@ use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::goto_program::{Expr, Location, Stmt, Type}; use cbmc::InternedString; -use rustc_middle::mir::coverage::CodeRegion; +use rustc_middle::mir::coverage::SourceRegion; use stable_mir::mir::{Place, ProjectionElem}; use stable_mir::ty::{Span as SpanStable, TypeAndMut}; use strum_macros::{AsRefStr, EnumString}; @@ -153,14 +153,14 @@ impl<'tcx> GotocCtx<'tcx> { &self, counter_data: &str, span: SpanStable, - code_region: CodeRegion, + source_region: SourceRegion, ) -> 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} - {code_region:?}"); + let msg = format!("{counter_data} - {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 0793e0c4688f..34f8363f4948 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -219,34 +219,34 @@ impl<'tcx> GotocCtx<'tcx> { pub mod rustc_smir { use crate::stable_mir::CrateDef; - use rustc_middle::mir::coverage::CodeRegion; 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 stable_mir::mir::mono::Instance; use stable_mir::Opaque; type CoverageOpaque = stable_mir::Opaque; - /// Retrieves the `CodeRegion` associated with the data in a + /// Retrieves the `SourceRegion` associated with the data in a /// `CoverageOpaque` object. pub fn region_from_coverage_opaque( tcx: TyCtxt, coverage_opaque: &CoverageOpaque, instance: Instance, - ) -> Option { + ) -> Option { let cov_term = parse_coverage_opaque(coverage_opaque); region_from_coverage(tcx, cov_term, instance) } - /// Retrieves the `CodeRegion` associated with a `CovTerm` object. + /// Retrieves the `SourceRegion` associated with a `CovTerm` object. /// /// Note: This function could be in the internal `rustc` impl for `Coverage`. pub fn region_from_coverage( tcx: TyCtxt<'_>, coverage: CovTerm, instance: Instance, - ) -> Option { + ) -> Option { // 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 +258,7 @@ pub mod rustc_smir { for mapping in &cov_info.mappings { let Code(term) = mapping.kind else { unreachable!() }; if term == coverage { - return Some(mapping.code_region.clone()); + return Some(mapping.source_region.clone()); } } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 81407c4dc704..ed0178511126 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -163,11 +163,11 @@ impl<'tcx> GotocCtx<'tcx> { let function_name = self.current_fn().readable_name(); let instance = self.current_fn().instance_stable(); let counter_data = format!("{coverage_opaque:?} ${function_name}$"); - let maybe_code_region = + let maybe_source_region = region_from_coverage_opaque(self.tcx, &coverage_opaque, instance); - if let Some(code_region) = maybe_code_region { + if let Some(source_region) = maybe_source_region { let coverage_stmt = - self.codegen_coverage(&counter_data, stmt.span, code_region); + self.codegen_coverage(&counter_data, stmt.span, source_region); // 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 3421b9b3adc9..1494baafeb51 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-08-28" +channel = "nightly-2024-08-29" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]