Skip to content

Commit 47a7c22

Browse files
authored
Upgrade toolchain to nightly-2024-11-11 (#3710)
Changes required due to - rust-lang/rust#132675 (coverage: Restrict empty-span expansion to only cover { and }) 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 80d4451 commit 47a7c22

File tree

6 files changed

+15
-10
lines changed

6 files changed

+15
-10
lines changed

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

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -156,13 +156,14 @@ impl GotocCtx<'_> {
156156
counter_data: &str,
157157
span: SpanStable,
158158
source_region: SourceRegion,
159+
file_name: &str,
159160
) -> Stmt {
160161
let loc = self.codegen_caller_span_stable(span);
161162
// Should use Stmt::cover, but currently this doesn't work with CBMC
162163
// unless it is run with '--cover cover' (see
163164
// https://github.com/diffblue/cbmc/issues/6613). So for now use
164165
// `assert(false)`.
165-
let msg = format!("{counter_data} - {source_region:?}");
166+
let msg = format!("{counter_data} - {file_name}:{source_region:?}");
166167
self.codegen_assert(Expr::bool_false(), PropertyClass::CodeCoverage, &msg, loc)
167168
}
168169

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

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -223,8 +223,9 @@ pub mod rustc_smir {
223223
use rustc_middle::mir::coverage::MappingKind::Code;
224224
use rustc_middle::mir::coverage::SourceRegion;
225225
use rustc_middle::ty::TyCtxt;
226-
use stable_mir::Opaque;
226+
use rustc_smir::rustc_internal;
227227
use stable_mir::mir::mono::Instance;
228+
use stable_mir::{Filename, Opaque};
228229

229230
type CoverageOpaque = stable_mir::Opaque;
230231

@@ -234,7 +235,7 @@ pub mod rustc_smir {
234235
tcx: TyCtxt,
235236
coverage_opaque: &CoverageOpaque,
236237
instance: Instance,
237-
) -> Option<SourceRegion> {
238+
) -> Option<(SourceRegion, Filename)> {
238239
let cov_term = parse_coverage_opaque(coverage_opaque);
239240
region_from_coverage(tcx, cov_term, instance)
240241
}
@@ -246,7 +247,7 @@ pub mod rustc_smir {
246247
tcx: TyCtxt<'_>,
247248
coverage: CovTerm,
248249
instance: Instance,
249-
) -> Option<SourceRegion> {
250+
) -> Option<(SourceRegion, Filename)> {
250251
// We need to pull the coverage info from the internal MIR instance.
251252
let instance_def = rustc_smir::rustc_internal::internal(tcx, instance.def.def_id());
252253
let body = tcx.instance_mir(rustc_middle::ty::InstanceKind::Item(instance_def));
@@ -258,7 +259,10 @@ pub mod rustc_smir {
258259
for mapping in &cov_info.mappings {
259260
let Code(term) = mapping.kind else { unreachable!() };
260261
if term == coverage {
261-
return Some(mapping.source_region.clone());
262+
return Some((
263+
mapping.source_region.clone(),
264+
rustc_internal::stable(cov_info.body_span).get_filename(),
265+
));
262266
}
263267
}
264268
}

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -165,9 +165,9 @@ impl GotocCtx<'_> {
165165
let counter_data = format!("{coverage_opaque:?} ${function_name}$");
166166
let maybe_source_region =
167167
region_from_coverage_opaque(self.tcx, &coverage_opaque, instance);
168-
if let Some(source_region) = maybe_source_region {
168+
if let Some((source_region, file_name)) = maybe_source_region {
169169
let coverage_stmt =
170-
self.codegen_coverage(&counter_data, stmt.span, source_region);
170+
self.codegen_coverage(&counter_data, stmt.span, source_region, &file_name);
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-11-09"
5+
channel = "nightly-2024-11-11"
66
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

tests/coverage/assert/expected

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@
1010
10| 1| if x < 3 ```{'''\
1111
11| 0| ``` // unreachable'''\
1212
12| 0| ``` assert!(x == 2);'''\
13-
13| 0| ``` }'''``` '''\
13+
13| 0| ``` ```}''''''\
1414
14| 1| } else {\
1515
15| 1| // passes\
1616
16| 1| assert!(x <= 5);\

tests/coverage/known_issues/assert_uncovered_end/expected

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,5 +10,5 @@
1010
10| 1| let x: u32 = kani::any_where(|val| *val == 5);\
1111
11| 1| if x > 3 {\
1212
12| 1| assert!(x > 4);\
13-
13| 1| }``` '''\
13+
13| 1| ```}'''\
1414
14| | }\

0 commit comments

Comments
 (0)