Toolchain update 06-01-2025

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 | |

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};

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,11 @@ 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).unwrap(),
                         rustc_internal::stable(cov_info.body_span).get_filename(),
                     ));
                 }

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

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;

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() {

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

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<Span> {
+    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<SourceRegion> {
+    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<SourceRegion> {
+    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,
+    })
+}

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

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

@@ -625,6 +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"
+            ),
         }
     }
 
@@ -1032,6 +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"
+            ),
         }
     }
 
@@ -1191,12 +1197,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

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
             }

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()
             }

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();

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();

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),

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;

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"]

tests/expected/uninit/intrinsics/expected

@@ -6,11 +6,11 @@ std::ptr::write::<std::mem::MaybeUninit<u8>>.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::<u8>.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

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);
     }
 }