Skip to content

Commit

Permalink
Upgrade Toolchain to 8/29 (#3468)
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
carolynzech authored Aug 29, 2024
1 parent e28f3db commit 691f81e
Show file tree
Hide file tree
Showing 4 changed files with 13 additions and 13 deletions.
6 changes: 3 additions & 3 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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};
Expand Down Expand Up @@ -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)
}

Expand Down
12 changes: 6 additions & 6 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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<CodeRegion> {
) -> Option<SourceRegion> {
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<CodeRegion> {
) -> Option<SourceRegion> {
// 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 +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());
}
}
}
Expand Down
6 changes: 3 additions & 3 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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 <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-08-28"
channel = "nightly-2024-08-29"
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

0 comments on commit 691f81e

Please sign in to comment.