Skip to content

Commit

Permalink
Upgrade toolchain to nightly-2024-11-11 (#3710)
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
qinheping authored Nov 13, 2024
1 parent 80d4451 commit 47a7c22
Show file tree
Hide file tree
Showing 6 changed files with 15 additions and 10 deletions.
3 changes: 2 additions & 1 deletion kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
}

Expand Down
12 changes: 8 additions & 4 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
Original file line number Diff line number Diff line change
Expand Up @@ -223,8 +223,9 @@ pub mod rustc_smir {
use rustc_middle::mir::coverage::MappingKind::Code;
use rustc_middle::mir::coverage::SourceRegion;
use rustc_middle::ty::TyCtxt;
use stable_mir::Opaque;
use rustc_smir::rustc_internal;
use stable_mir::mir::mono::Instance;
use stable_mir::{Filename, Opaque};

type CoverageOpaque = stable_mir::Opaque;

Expand All @@ -234,7 +235,7 @@ pub mod rustc_smir {
tcx: TyCtxt,
coverage_opaque: &CoverageOpaque,
instance: Instance,
) -> Option<SourceRegion> {
) -> Option<(SourceRegion, Filename)> {
let cov_term = parse_coverage_opaque(coverage_opaque);
region_from_coverage(tcx, cov_term, instance)
}
Expand All @@ -246,7 +247,7 @@ pub mod rustc_smir {
tcx: TyCtxt<'_>,
coverage: CovTerm,
instance: Instance,
) -> Option<SourceRegion> {
) -> Option<(SourceRegion, Filename)> {
// 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));
Expand All @@ -258,7 +259,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(),
rustc_internal::stable(cov_info.body_span).get_filename(),
));
}
}
}
Expand Down
4 changes: 2 additions & 2 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
Original file line number Diff line number Diff line change
Expand Up @@ -165,9 +165,9 @@ 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_name)) = maybe_source_region {
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>
Expand Down
2 changes: 1 addition & 1 deletion rust-toolchain.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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"]
2 changes: 1 addition & 1 deletion tests/coverage/assert/expected
Original file line number Diff line number Diff line change
Expand Up @@ -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);\
Expand Down
2 changes: 1 addition & 1 deletion tests/coverage/known_issues/assert_uncovered_end/expected
Original file line number Diff line number Diff line change
Expand Up @@ -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| | }\

0 comments on commit 47a7c22

Please sign in to comment.