From df9924ed1bf000c01b8364e84bccc0de2595904b Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Mon, 6 Jan 2025 17:56:48 -0500 Subject: [PATCH 01/10] Update toolchain to 2025-01-06 --- rust-toolchain.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 75152d6384f4..0ff66e1bc6b7 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-12-19" +channel = "nightly-2025-01-06" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] From 1c8fd4b2d00445b497b721fd8839ce8112e3cb4e Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Mon, 6 Jan 2025 18:03:37 -0500 Subject: [PATCH 02/10] Implement `SourceRegion` locally in Kani The original SourceRegion was moved to the llvm backend and made private by https://github.com/rust-lang/rust/pull/134497. We implement our own local version of it to maintain our handling of SourceRegion for coverage properties. --- .../codegen_cprover_gotoc/codegen/assert.rs | 2 +- .../codegen_cprover_gotoc/codegen/function.rs | 7 +- .../src/codegen_cprover_gotoc/codegen/mod.rs | 1 + .../codegen/source_region.rs | 135 ++++++++++++++++++ kani-compiler/src/main.rs | 1 + 5 files changed, 143 insertions(+), 3 deletions(-) create mode 100644 kani-compiler/src/codegen_cprover_gotoc/codegen/source_region.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs index f1971f2f158e..2392a801809f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs @@ -18,10 +18,10 @@ //! 7. `codegen_sanity` : `assert` but not normally displayed as failure would be a Kani bug //! +use super::source_region::SourceRegion; use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::InternedString; use cbmc::goto_program::{Expr, Location, Stmt, Type}; -use rustc_middle::mir::coverage::SourceRegion; use stable_mir::mir::{Place, ProjectionElem}; use stable_mir::ty::{Span as SpanStable, Ty}; use strum_macros::{AsRefStr, EnumString}; diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index ed5c5c593b20..95476dc8c574 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -218,10 +218,10 @@ impl GotocCtx<'_> { } pub mod rustc_smir { + use crate::codegen_cprover_gotoc::codegen::source_region::{SourceRegion, make_source_region}; use crate::stable_mir::CrateDef; 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 rustc_smir::rustc_internal; use stable_mir::mir::mono::Instance; @@ -258,9 +258,12 @@ pub mod rustc_smir { // Iterate over the coverage mappings and match with the coverage term. for mapping in &cov_info.mappings { let Code(term) = mapping.kind else { unreachable!() }; + let source_map = tcx.sess.source_map(); + let file = source_map.lookup_source_file(cov_info.body_span.lo()); if term == coverage { return Some(( - mapping.source_region.clone(), + make_source_region(source_map, cov_info, &file, mapping.span.clone()) + .unwrap(), rustc_internal::stable(cov_info.body_span).get_filename(), )); } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/mod.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/mod.rs index 238bdb27b069..f176cbbb88d2 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/mod.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/mod.rs @@ -12,6 +12,7 @@ mod intrinsic; mod operand; mod place; mod rvalue; +mod source_region; mod span; mod statement; mod static_var; diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/source_region.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/source_region.rs new file mode 100644 index 000000000000..aa327372321f --- /dev/null +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/source_region.rs @@ -0,0 +1,135 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This file contains our own local version of +//! the `Span` to `CoverageRegion` conversion defined in +//! https://github.com/rust-lang/rust/tree/master/compiler/rustc_codegen_llvm/src/coverageinfo/mapgen/spans.rs + +use rustc_middle::mir::coverage::FunctionCoverageInfo; +use rustc_span::Span; +use rustc_span::source_map::SourceMap; +use rustc_span::{BytePos, SourceFile}; +use std::fmt::{self, Debug, Formatter}; +use tracing::debug; + +#[derive(Clone, Hash, PartialEq, Eq, PartialOrd, Ord)] +pub struct SourceRegion { + pub start_line: u32, + pub start_col: u32, + pub end_line: u32, + pub end_col: u32, +} + +impl Debug for SourceRegion { + fn fmt(&self, fmt: &mut Formatter<'_>) -> fmt::Result { + let &Self { start_line, start_col, end_line, end_col } = self; + write!(fmt, "{start_line}:{start_col} - {end_line}:{end_col}") + } +} + +fn ensure_non_empty_span( + source_map: &SourceMap, + fn_cov_info: &FunctionCoverageInfo, + span: Span, +) -> Option { + if !span.is_empty() { + return Some(span); + } + let lo = span.lo(); + let hi = span.hi(); + // The span is empty, so try to expand it to cover an adjacent '{' or '}', + // but only within the bounds of the body span. + let try_next = hi < fn_cov_info.body_span.hi(); + let try_prev = fn_cov_info.body_span.lo() < lo; + if !(try_next || try_prev) { + return None; + } + source_map + .span_to_source(span, |src, start, end| try { + // Adjusting span endpoints by `BytePos(1)` is normally a bug, + // but in this case we have specifically checked that the character + // we're skipping over is one of two specific ASCII characters, so + // adjusting by exactly 1 byte is correct. + if try_next && src.as_bytes()[end] == b'{' { + Some(span.with_hi(hi + BytePos(1))) + } else if try_prev && src.as_bytes()[start - 1] == b'}' { + Some(span.with_lo(lo - BytePos(1))) + } else { + None + } + }) + .ok()? +} + +/// If `llvm-cov` sees a source region that is improperly ordered (end < start), +/// it will immediately exit with a fatal error. To prevent that from happening, +/// discard regions that are improperly ordered, or might be interpreted in a +/// way that makes them improperly ordered. +fn check_source_region(source_region: SourceRegion) -> Option { + let SourceRegion { start_line, start_col, end_line, end_col } = source_region; + // Line/column coordinates are supposed to be 1-based. If we ever emit + // coordinates of 0, `llvm-cov` might misinterpret them. + let all_nonzero = [start_line, start_col, end_line, end_col].into_iter().all(|x| x != 0); + // Coverage mappings use the high bit of `end_col` to indicate that a + // region is actually a "gap" region, so make sure it's unset. + let end_col_has_high_bit_unset = (end_col & (1 << 31)) == 0; + // If a region is improperly ordered (end < start), `llvm-cov` will exit + // with a fatal error, which is inconvenient for users and hard to debug. + let is_ordered = (start_line, start_col) <= (end_line, end_col); + if all_nonzero && end_col_has_high_bit_unset && is_ordered { + Some(source_region) + } else { + debug!( + ?source_region, + ?all_nonzero, + ?end_col_has_high_bit_unset, + ?is_ordered, + "Skipping source region that would be misinterpreted or rejected by LLVM" + ); + // If this happens in a debug build, ICE to make it easier to notice. + debug_assert!(false, "Improper source region: {source_region:?}"); + None + } +} + +/// Converts the span into its start line and column, and end line and column. +/// +/// Line numbers and column numbers are 1-based. Unlike most column numbers emitted by +/// the compiler, these column numbers are denoted in **bytes**, because that's what +/// LLVM's `llvm-cov` tool expects to see in coverage maps. +/// +/// Returns `None` if the conversion failed for some reason. This shouldn't happen, +/// but it's hard to rule out entirely (especially in the presence of complex macros +/// or other expansions), and if it does happen then skipping a span or function is +/// better than an ICE or `llvm-cov` failure that the user might have no way to avoid. +pub(crate) fn make_source_region( + source_map: &SourceMap, + fn_cov_info: &FunctionCoverageInfo, + file: &SourceFile, + span: Span, +) -> Option { + let span = ensure_non_empty_span(source_map, fn_cov_info, span)?; + let lo = span.lo(); + let hi = span.hi(); + // Column numbers need to be in bytes, so we can't use the more convenient + // `SourceMap` methods for looking up file coordinates. + let line_and_byte_column = |pos: BytePos| -> Option<(usize, usize)> { + let rpos = file.relative_position(pos); + let line_index = file.lookup_line(rpos)?; + let line_start = file.lines()[line_index]; + // Line numbers and column numbers are 1-based, so add 1 to each. + Some((line_index + 1, ((rpos - line_start).0 as usize) + 1)) + }; + let (mut start_line, start_col) = line_and_byte_column(lo)?; + let (mut end_line, end_col) = line_and_byte_column(hi)?; + // Apply an offset so that code in doctests has correct line numbers. + // FIXME(#79417): Currently we have no way to offset doctest _columns_. + start_line = source_map.doctest_offset_line(&file.name, start_line); + end_line = source_map.doctest_offset_line(&file.name, end_line); + check_source_region(SourceRegion { + start_line: start_line as u32, + start_col: start_col as u32, + end_line: end_line as u32, + end_col: end_col as u32, + }) +} diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs index 6f108595dbfc..02709797cf3a 100644 --- a/kani-compiler/src/main.rs +++ b/kani-compiler/src/main.rs @@ -17,6 +17,7 @@ #![feature(f16)] #![feature(non_exhaustive_omitted_patterns_lint)] #![feature(float_next_up_down)] +#![feature(try_blocks)] extern crate rustc_abi; extern crate rustc_ast; extern crate rustc_ast_pretty; From feca7ab9ba62be11b3a0b6ef7976a2acbb596e39 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Mon, 6 Jan 2025 18:10:30 -0500 Subject: [PATCH 03/10] Propagate upstream representation change for enums with no variants Propagated from https://github.com/rust-lang/rust/pull/133702. Empty enums now have `Variants::Empty` as variants instead of `Variants::Single{ index: None }`. --- kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs | 2 +- .../src/codegen_cprover_gotoc/codegen/rvalue.rs | 4 ++++ .../src/codegen_cprover_gotoc/codegen/statement.rs | 2 +- kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs | 9 +++++++-- .../src/kani_middle/transform/check_uninit/ty_layout.rs | 1 + kani-compiler/src/kani_middle/transform/check_values.rs | 1 + 6 files changed, 15 insertions(+), 4 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index b6189c070538..8cabd10c87ad 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -611,7 +611,7 @@ impl GotocCtx<'_> { }; let layout = self.layout_of(rustc_internal::internal(self.tcx, ty)); let expr = match &layout.variants { - Variants::Single { .. } => before.goto_expr, + Variants::Empty | Variants::Single { .. } => before.goto_expr, Variants::Multiple { tag_encoding, .. } => match tag_encoding { TagEncoding::Direct => { let cases = if ty_kind.is_coroutine() { diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index d13597794d19..f4ca557afbdb 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -554,6 +554,9 @@ impl GotocCtx<'_> { let variant_expr = variant_proj.goto_expr.clone(); let layout = self.layout_of_stable(res_ty); let fields = match &layout.variants { + Variants::Empty => { + unreachable!("Aggregate expression for uninhabited enum with no variants") + } Variants::Single { index } => { if *index != rustc_internal::internal(self.tcx, variant_index) { // This may occur if all variants except for the one pointed by @@ -960,6 +963,7 @@ impl GotocCtx<'_> { pub fn codegen_get_discriminant(&mut self, e: Expr, ty: Ty, res_ty: Ty) -> Expr { let layout = self.layout_of_stable(ty); match &layout.variants { + Variants::Empty => unreachable!("Discriminant for uninhabited enum with no variants"), Variants::Single { index } => { let discr_val = layout .ty diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 12a61c45b558..90635a71f2e8 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -305,7 +305,7 @@ impl GotocCtx<'_> { let variant_index_internal = rustc_internal::internal(self.tcx, variant_index); let layout = self.layout_of(dest_ty_internal); match &layout.variants { - Variants::Single { .. } => Stmt::skip(location), + Variants::Empty | Variants::Single { .. } => Stmt::skip(location), Variants::Multiple { tag, tag_encoding, .. } => match tag_encoding { TagEncoding::Direct => { let discr = dest_ty_internal diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 748eb42e7655..88960d40d2ba 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -1191,12 +1191,17 @@ impl<'tcx> GotocCtx<'tcx> { let layout = self.layout_of(ty); // variants appearing in mir code match &layout.variants { + Variants::Empty => { + // an empty enum with no variants (its value cannot be instantiated) + self.ensure_struct(self.ty_mangled_name(ty), pretty_name, |_, _| vec![]) + } Variants::Single { index } => { self.ensure_struct(self.ty_mangled_name(ty), pretty_name, |gcx, _| { match source_variants.get(*index) { None => { - // an empty enum with no variants (its value cannot be instantiated) - vec![] + unreachable!( + "Enum with no variants must be represented as Variants::Empty" + ); } Some(variant) => { // a single enum is pretty much like a struct diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs index 0a1fc16dcc07..73dce8c2e898 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs @@ -217,6 +217,7 @@ fn data_bytes_for_ty( // Support basic enumeration forms let ty_variants = def.variants(); match layout.variants { + VariantsShape::Empty => Ok(vec![]), VariantsShape::Single { index } => { // Only one variant is reachable. This behaves like a struct. let fields = ty_variants[index.to_index()].fields(); diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs index 2276906aae81..4f5f0530f4cc 100644 --- a/kani-compiler/src/kani_middle/transform/check_values.rs +++ b/kani-compiler/src/kani_middle/transform/check_values.rs @@ -879,6 +879,7 @@ pub fn ty_validity_per_offset( // Support basic enumeration forms let ty_variants = def.variants(); match layout.variants { + VariantsShape::Empty => Ok(vec![]), VariantsShape::Single { index } => { // Only one variant is reachable. This behaves like a struct. let fields = ty_variants[index.to_index()].fields(); From 75ce5d6a21b2d2bd1953e71ca847f14e3ebfe04e Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Mon, 6 Jan 2025 18:15:10 -0500 Subject: [PATCH 04/10] Add UnsafeBinder variant (WIP in rustc). Rustc has started implementing `UnsafeBinder`: - https://github.com/rust-lang/rust/pull/134625 - https://github.com/rust-lang/rust/issues/130516 Only the enums variants have been added for now, semantics is TBD. --- kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 88960d40d2ba..35bb3b914dff 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -625,6 +625,8 @@ impl<'tcx> GotocCtx<'tcx> { ty::CoroutineWitness(_, _) | ty::Infer(_) | ty::Placeholder(_) | ty::Error(_) => { unreachable!("remnants of type checking") } + // TODO cf. https://github.com/rust-lang/rust/issues/130516 + ty::UnsafeBinder(_) => todo!(), } } @@ -1032,6 +1034,8 @@ impl<'tcx> GotocCtx<'tcx> { ty::Infer(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()), ty::Param(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()), ty::Placeholder(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()), + // TODO cf. https://github.com/rust-lang/rust/issues/130516 + ty::UnsafeBinder(_) => todo!(), } } From 8159275512ce2032b4f1eaf25ebc2c8f2d382d75 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Mon, 6 Jan 2025 18:17:28 -0500 Subject: [PATCH 05/10] Propagate removal of `RValue::Len(place)` in MIR. Propagated form https://github.com/rust-lang/rust/pull/134330. `RValue::Len(place)` is still present in StableMIR, so we translate it back to MIR as `PtrMetadata(Copy(place))`. --- .../src/kani_middle/points_to/points_to_analysis.rs | 2 +- kani-compiler/src/kani_middle/transform/internal_mir.rs | 5 ++++- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs index 345a27309b50..834b3e4026c4 100644 --- a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs +++ b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs @@ -575,7 +575,7 @@ impl<'tcx> PointsToAnalysis<'_, 'tcx> { // The same story from BinOp applies here, too. Need to track those things. self.successors_for_operand(state, operand) } - Rvalue::Len(..) | Rvalue::NullaryOp(..) | Rvalue::Discriminant(..) => { + Rvalue::NullaryOp(..) | Rvalue::Discriminant(..) => { // All of those should yield a constant. HashSet::new() } diff --git a/kani-compiler/src/kani_middle/transform/internal_mir.rs b/kani-compiler/src/kani_middle/transform/internal_mir.rs index 4f1095cce06e..fd499db7c3c6 100644 --- a/kani-compiler/src/kani_middle/transform/internal_mir.rs +++ b/kani-compiler/src/kani_middle/transform/internal_mir.rs @@ -251,7 +251,10 @@ impl RustcInternalMir for Rvalue { Rvalue::Discriminant(place) => { rustc_middle::mir::Rvalue::Discriminant(internal(tcx, place)) } - Rvalue::Len(place) => rustc_middle::mir::Rvalue::Len(internal(tcx, place)), + Rvalue::Len(place) => rustc_middle::mir::Rvalue::UnaryOp( + rustc_middle::mir::UnOp::PtrMetadata, + rustc_middle::mir::Operand::Copy(internal(tcx, place)), + ), Rvalue::Ref(region, borrow_kind, place) => rustc_middle::mir::Rvalue::Ref( internal(tcx, region), borrow_kind.internal_mir(tcx), From 49745b8cb32922f08354233edd0427a575c5374b Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Tue, 7 Jan 2025 11:12:08 -0500 Subject: [PATCH 06/10] Rename `typed_swap` to `typed_swap_nonoverlapping`. Propagated from https://github.com/rust-lang/rust/pull/134757. --- docs/src/rust-feature-support/intrinsics.md | 2 +- .../src/codegen_cprover_gotoc/codegen/intrinsic.rs | 2 +- kani-compiler/src/intrinsics.rs | 2 +- tests/expected/uninit/intrinsics/expected | 8 ++++---- tests/expected/uninit/intrinsics/intrinsics.rs | 8 ++++---- .../{typed_swap.rs => typed_swap_nonoverlapping.rs} | 8 ++++---- 6 files changed, 15 insertions(+), 15 deletions(-) rename tests/kani/Intrinsics/{typed_swap.rs => typed_swap_nonoverlapping.rs} (73%) diff --git a/docs/src/rust-feature-support/intrinsics.md b/docs/src/rust-feature-support/intrinsics.md index a9e2740836e5..9f3495da0adc 100644 --- a/docs/src/rust-feature-support/intrinsics.md +++ b/docs/src/rust-feature-support/intrinsics.md @@ -220,7 +220,7 @@ truncf64 | Yes | | try | No | [#267](https://github.com/model-checking/kani/issues/267) | type_id | Yes | | type_name | Yes | | -typed_swap | Yes | | +typed_swap_nonoverlapping | Yes | | unaligned_volatile_load | No | See [Notes - Concurrency](#concurrency) | unaligned_volatile_store | No | See [Notes - Concurrency](#concurrency) | unchecked_add | Yes | | diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 654a7f2b6861..e1436cd8ccc0 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -1864,7 +1864,7 @@ impl GotocCtx<'_> { } /// Swaps the memory contents pointed to by arguments `x` and `y`, respectively, which is - /// required for the `typed_swap` intrinsic. + /// required for the `typed_swap_nonoverlapping` intrinsic. /// /// The standard library API requires that `x` and `y` are readable and writable as their /// (common) type (which auto-generated checks for dereferencing will take care of), and the diff --git a/kani-compiler/src/intrinsics.rs b/kani-compiler/src/intrinsics.rs index 0121975b11a2..f58a40bf8cb6 100644 --- a/kani-compiler/src/intrinsics.rs +++ b/kani-compiler/src/intrinsics.rs @@ -389,7 +389,7 @@ impl Intrinsic { assert_sig_matches!(sig, => RigidTy::Ref(_, _, Mutability::Not)); Self::TypeName } - "typed_swap" => { + "typed_swap_nonoverlapping" => { assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), RigidTy::RawPtr(_, Mutability::Mut) => RigidTy::Tuple(_)); Self::TypedSwap } diff --git a/tests/expected/uninit/intrinsics/expected b/tests/expected/uninit/intrinsics/expected index b5555785e8af..b40fe6714ba8 100644 --- a/tests/expected/uninit/intrinsics/expected +++ b/tests/expected/uninit/intrinsics/expected @@ -6,11 +6,11 @@ std::ptr::write::>.assertion.1\ - Status: FAILURE\ - Description: "Interaction between raw pointers and unions is not yet supported."\ -check_typed_swap.assertion.1\ +check_typed_swap_nonoverlapping.assertion.1\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*mut u8`" -check_typed_swap.assertion.2\ +check_typed_swap_nonoverlapping.assertion.2\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*mut u8`" @@ -35,8 +35,8 @@ std::ptr::read::.assertion.2\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u8`" Summary: -Verification failed for - check_typed_swap_safe -Verification failed for - check_typed_swap +Verification failed for - check_typed_swap_nonoverlapping_safe +Verification failed for - check_typed_swap_nonoverlapping Verification failed for - check_volatile_load Verification failed for - check_compare_bytes Verification failed for - check_copy_read diff --git a/tests/expected/uninit/intrinsics/intrinsics.rs b/tests/expected/uninit/intrinsics/intrinsics.rs index 33d5e72b1da9..76f0fff67357 100644 --- a/tests/expected/uninit/intrinsics/intrinsics.rs +++ b/tests/expected/uninit/intrinsics/intrinsics.rs @@ -131,23 +131,23 @@ fn check_volatile_store_and_load_safe() { } #[kani::proof] -fn check_typed_swap() { +fn check_typed_swap_nonoverlapping() { unsafe { let layout = Layout::from_size_align(16, 8).unwrap(); let left: *mut u8 = alloc(layout); let right: *mut u8 = alloc(layout); // ~ERROR: Accessing `left` and `right` here, both of which are uninitialized. - typed_swap(left, right); + typed_swap_nonoverlapping(left, right); } } #[kani::proof] -fn check_typed_swap_safe() { +fn check_typed_swap_nonoverlapping_safe() { unsafe { let layout = Layout::from_size_align(16, 8).unwrap(); let left: *mut u8 = alloc_zeroed(layout); let right: *mut u8 = alloc_zeroed(layout); // Both `left` and `right` are initialized here. - typed_swap(left, right); + typed_swap_nonoverlapping(left, right); } } diff --git a/tests/kani/Intrinsics/typed_swap.rs b/tests/kani/Intrinsics/typed_swap_nonoverlapping.rs similarity index 73% rename from tests/kani/Intrinsics/typed_swap.rs rename to tests/kani/Intrinsics/typed_swap_nonoverlapping.rs index 996784b5181d..8177c1f6f357 100644 --- a/tests/kani/Intrinsics/typed_swap.rs +++ b/tests/kani/Intrinsics/typed_swap_nonoverlapping.rs @@ -1,20 +1,20 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// Check that `typed_swap` yields the expected results. -// https://doc.rust-lang.org/nightly/std/intrinsics/fn.typed_swap.html +// Check that `typed_swap_nonoverlapping` yields the expected results. +// https://doc.rust-lang.org/nightly/std/intrinsics/fn.typed_swap_nonoverlapping.html #![feature(core_intrinsics)] #![allow(internal_features)] #[kani::proof] -fn test_typed_swap_u32() { +fn test_typed_swap_nonoverlapping_u32() { let mut a: u32 = kani::any(); let a_before = a; let mut b: u32 = kani::any(); let b_before = b; unsafe { - std::intrinsics::typed_swap(&mut a, &mut b); + std::intrinsics::typed_swap_nonoverlapping(&mut a, &mut b); } assert!(b == a_before); assert!(a == b_before); From 30fec9e8405ce67692c7d1444f1e00af63424722 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Tue, 7 Jan 2025 11:12:25 -0500 Subject: [PATCH 07/10] Clippy fixes. --- kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs | 2 +- tools/compiletest/src/main.rs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index 95476dc8c574..0f2e30bd7a6e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -262,7 +262,7 @@ pub mod rustc_smir { let file = source_map.lookup_source_file(cov_info.body_span.lo()); if term == coverage { return Some(( - make_source_region(source_map, cov_info, &file, mapping.span.clone()) + make_source_region(source_map, cov_info, &file, mapping.span) .unwrap(), rustc_internal::stable(cov_info.body_span).get_filename(), )); diff --git a/tools/compiletest/src/main.rs b/tools/compiletest/src/main.rs index 9027e30121f8..8a77fd87cf90 100644 --- a/tools/compiletest/src/main.rs +++ b/tools/compiletest/src/main.rs @@ -149,7 +149,7 @@ pub fn parse_config(args: Vec) -> Config { let timeout = matches.opt_str("timeout").map(|val| { Duration::from_secs( u64::from_str(&val) - .expect("Unexpected timeout format. Expected a positive number but found {val}"), + .expect(&format!("Unexpected timeout format. Expected a positive number but found {val}")), ) }); From cc4abe6d87077b79b7a52244bdf48d1a6dd8021b Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Tue, 7 Jan 2025 11:46:13 -0500 Subject: [PATCH 08/10] Clippy fixes. --- .../src/codegen_cprover_gotoc/codegen/function.rs | 3 +-- tools/compiletest/src/main.rs | 7 +++---- 2 files changed, 4 insertions(+), 6 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index 0f2e30bd7a6e..bf64f0dd2e66 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -262,8 +262,7 @@ pub mod rustc_smir { let file = source_map.lookup_source_file(cov_info.body_span.lo()); if term == coverage { return Some(( - make_source_region(source_map, cov_info, &file, mapping.span) - .unwrap(), + make_source_region(source_map, cov_info, &file, mapping.span).unwrap(), rustc_internal::stable(cov_info.body_span).get_filename(), )); } diff --git a/tools/compiletest/src/main.rs b/tools/compiletest/src/main.rs index 8a77fd87cf90..c0e599b725cf 100644 --- a/tools/compiletest/src/main.rs +++ b/tools/compiletest/src/main.rs @@ -147,10 +147,9 @@ pub fn parse_config(args: Vec) -> Config { let run_ignored = matches.opt_present("ignored"); let mode = matches.opt_str("mode").unwrap().parse().expect("invalid mode"); let timeout = matches.opt_str("timeout").map(|val| { - Duration::from_secs( - u64::from_str(&val) - .expect(&format!("Unexpected timeout format. Expected a positive number but found {val}")), - ) + Duration::from_secs(u64::from_str(&val).expect(&format!( + "Unexpected timeout format. Expected a positive number but found {val}" + ))) }); Config { From 3c437215a16b5f34df2520af3bcddd4b009b8d84 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Thu, 9 Jan 2025 12:05:02 -0500 Subject: [PATCH 09/10] Add todo message for UnsafeBinder --- kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 35bb3b914dff..12f207d79017 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -625,8 +625,7 @@ impl<'tcx> GotocCtx<'tcx> { ty::CoroutineWitness(_, _) | ty::Infer(_) | ty::Placeholder(_) | ty::Error(_) => { unreachable!("remnants of type checking") } - // TODO cf. https://github.com/rust-lang/rust/issues/130516 - ty::UnsafeBinder(_) => todo!(), + ty::UnsafeBinder(_) => todo!("Implement support for UnsafeBinder https://github.com/rust-lang/rust/issues/130516"), } } @@ -1034,8 +1033,7 @@ impl<'tcx> GotocCtx<'tcx> { ty::Infer(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()), ty::Param(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()), ty::Placeholder(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()), - // TODO cf. https://github.com/rust-lang/rust/issues/130516 - ty::UnsafeBinder(_) => todo!(), + ty::UnsafeBinder(_) => todo!("Implement support for UnsafeBinder https://github.com/rust-lang/rust/issues/130516"), } } From f9134c84332fa41031e11e5464c6c7cdab3f3b3b Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Thu, 9 Jan 2025 17:22:18 -0500 Subject: [PATCH 10/10] rustfmt fixes --- kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 12f207d79017..18c121694223 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -625,7 +625,9 @@ impl<'tcx> GotocCtx<'tcx> { ty::CoroutineWitness(_, _) | ty::Infer(_) | ty::Placeholder(_) | ty::Error(_) => { unreachable!("remnants of type checking") } - ty::UnsafeBinder(_) => todo!("Implement support for UnsafeBinder https://github.com/rust-lang/rust/issues/130516"), + ty::UnsafeBinder(_) => todo!( + "Implement support for UnsafeBinder https://github.com/rust-lang/rust/issues/130516" + ), } } @@ -1033,7 +1035,9 @@ impl<'tcx> GotocCtx<'tcx> { ty::Infer(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()), ty::Param(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()), ty::Placeholder(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()), - ty::UnsafeBinder(_) => todo!("Implement support for UnsafeBinder https://github.com/rust-lang/rust/issues/130516"), + ty::UnsafeBinder(_) => todo!( + "Implement support for UnsafeBinder https://github.com/rust-lang/rust/issues/130516" + ), } }