Skip to content

Commit 691f81e

Browse files
authored
Upgrade Toolchain to 8/29 (#3468)
Upgrade toolchain to 8/29. Culprit upstream changes: rust-lang/rust#129686 Resolves #3466 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
1 parent e28f3db commit 691f81e

File tree

4 files changed

+13
-13
lines changed

4 files changed

+13
-13
lines changed

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@
2121
use crate::codegen_cprover_gotoc::GotocCtx;
2222
use cbmc::goto_program::{Expr, Location, Stmt, Type};
2323
use cbmc::InternedString;
24-
use rustc_middle::mir::coverage::CodeRegion;
24+
use rustc_middle::mir::coverage::SourceRegion;
2525
use stable_mir::mir::{Place, ProjectionElem};
2626
use stable_mir::ty::{Span as SpanStable, TypeAndMut};
2727
use strum_macros::{AsRefStr, EnumString};
@@ -153,14 +153,14 @@ impl<'tcx> GotocCtx<'tcx> {
153153
&self,
154154
counter_data: &str,
155155
span: SpanStable,
156-
code_region: CodeRegion,
156+
source_region: SourceRegion,
157157
) -> Stmt {
158158
let loc = self.codegen_caller_span_stable(span);
159159
// Should use Stmt::cover, but currently this doesn't work with CBMC
160160
// unless it is run with '--cover cover' (see
161161
// https://github.com/diffblue/cbmc/issues/6613). So for now use
162162
// `assert(false)`.
163-
let msg = format!("{counter_data} - {code_region:?}");
163+
let msg = format!("{counter_data} - {source_region:?}");
164164
self.codegen_assert(Expr::bool_false(), PropertyClass::CodeCoverage, &msg, loc)
165165
}
166166

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

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -219,34 +219,34 @@ impl<'tcx> GotocCtx<'tcx> {
219219

220220
pub mod rustc_smir {
221221
use crate::stable_mir::CrateDef;
222-
use rustc_middle::mir::coverage::CodeRegion;
223222
use rustc_middle::mir::coverage::CovTerm;
224223
use rustc_middle::mir::coverage::MappingKind::Code;
224+
use rustc_middle::mir::coverage::SourceRegion;
225225
use rustc_middle::ty::TyCtxt;
226226
use stable_mir::mir::mono::Instance;
227227
use stable_mir::Opaque;
228228

229229
type CoverageOpaque = stable_mir::Opaque;
230230

231-
/// Retrieves the `CodeRegion` associated with the data in a
231+
/// Retrieves the `SourceRegion` associated with the data in a
232232
/// `CoverageOpaque` object.
233233
pub fn region_from_coverage_opaque(
234234
tcx: TyCtxt,
235235
coverage_opaque: &CoverageOpaque,
236236
instance: Instance,
237-
) -> Option<CodeRegion> {
237+
) -> Option<SourceRegion> {
238238
let cov_term = parse_coverage_opaque(coverage_opaque);
239239
region_from_coverage(tcx, cov_term, instance)
240240
}
241241

242-
/// Retrieves the `CodeRegion` associated with a `CovTerm` object.
242+
/// Retrieves the `SourceRegion` associated with a `CovTerm` object.
243243
///
244244
/// Note: This function could be in the internal `rustc` impl for `Coverage`.
245245
pub fn region_from_coverage(
246246
tcx: TyCtxt<'_>,
247247
coverage: CovTerm,
248248
instance: Instance,
249-
) -> Option<CodeRegion> {
249+
) -> Option<SourceRegion> {
250250
// We need to pull the coverage info from the internal MIR instance.
251251
let instance_def = rustc_smir::rustc_internal::internal(tcx, instance.def.def_id());
252252
let body = tcx.instance_mir(rustc_middle::ty::InstanceKind::Item(instance_def));
@@ -258,7 +258,7 @@ pub mod rustc_smir {
258258
for mapping in &cov_info.mappings {
259259
let Code(term) = mapping.kind else { unreachable!() };
260260
if term == coverage {
261-
return Some(mapping.code_region.clone());
261+
return Some(mapping.source_region.clone());
262262
}
263263
}
264264
}

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -163,11 +163,11 @@ impl<'tcx> GotocCtx<'tcx> {
163163
let function_name = self.current_fn().readable_name();
164164
let instance = self.current_fn().instance_stable();
165165
let counter_data = format!("{coverage_opaque:?} ${function_name}$");
166-
let maybe_code_region =
166+
let maybe_source_region =
167167
region_from_coverage_opaque(self.tcx, &coverage_opaque, instance);
168-
if let Some(code_region) = maybe_code_region {
168+
if let Some(source_region) = maybe_source_region {
169169
let coverage_stmt =
170-
self.codegen_coverage(&counter_data, stmt.span, code_region);
170+
self.codegen_coverage(&counter_data, stmt.span, source_region);
171171
// TODO: Avoid single-statement blocks when conversion of
172172
// standalone statements to the irep format is fixed.
173173
// More details in <https://github.com/model-checking/kani/issues/3012>

rust-toolchain.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,5 @@
22
# SPDX-License-Identifier: Apache-2.0 OR MIT
33

44
[toolchain]
5-
channel = "nightly-2024-08-28"
5+
channel = "nightly-2024-08-29"
66
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

0 commit comments

Comments
 (0)