Update toolchain to 2024-09-26

cprover_bindings/src/goto_program/expr.rs

@@ -15,7 +15,7 @@ use std::collections::BTreeMap;
 use std::fmt::Debug;
 
 ///////////////////////////////////////////////////////////////////////////////////////////////
-/// Datatypes
+// Datatypes
 ///////////////////////////////////////////////////////////////////////////////////////////////
 
 /// An `Expr` represents an expression type: i.e. a computation that returns a value.
@@ -292,7 +292,7 @@ pub fn arithmetic_overflow_result_type(operand_type: Type) -> Type {
 }
 
 ///////////////////////////////////////////////////////////////////////////////////////////////
-/// Implementations
+// Implementations
 ///////////////////////////////////////////////////////////////////////////////////////////////
 
 /// Getters

cprover_bindings/src/goto_program/stmt.rs

@@ -6,7 +6,7 @@ use crate::{InternString, InternedString};
 use std::fmt::Debug;
 
 ///////////////////////////////////////////////////////////////////////////////////////////////
-/// Datatypes
+// Datatypes
 ///////////////////////////////////////////////////////////////////////////////////////////////
 
 /// An `Stmt` represents a statement type: i.e. a computation that does not return a value.
@@ -118,7 +118,7 @@ pub struct SwitchCase {
 }
 
 ///////////////////////////////////////////////////////////////////////////////////////////////
-/// Implementations
+// Implementations
 ///////////////////////////////////////////////////////////////////////////////////////////////
 
 /// Getters

cprover_bindings/src/goto_program/symbol.rs

@@ -20,8 +20,6 @@ pub struct Symbol {
     /// Contracts to be enforced (only supported for functions)
     pub contract: Option<Box<FunctionContract>>,
 
-    /// Optional debugging information
-
     /// Local name `x`
     pub base_name: Option<InternedString>,
     /// Fully qualifier name `foo::bar::x`

cprover_bindings/src/goto_program/typ.rs

@@ -10,7 +10,7 @@ use std::collections::BTreeMap;
 use std::fmt::Debug;
 
 ///////////////////////////////////////////////////////////////////////////////////////////////
-/// Datatypes
+// Datatypes
 ///////////////////////////////////////////////////////////////////////////////////////////////
 
 /// Represents the different types that can be used in a goto-program.
@@ -112,7 +112,7 @@ pub struct Parameter {
 }
 
 ///////////////////////////////////////////////////////////////////////////////////////////////
-/// Implementations
+// Implementations
 ///////////////////////////////////////////////////////////////////////////////////////////////
 
 /// Getters

cprover_bindings/src/irep/goto_binary_serde.rs

@@ -1,6 +1,82 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //! GOTO binary serializer.
+//!
+//! # Design overview
+//!
+//! When saving a [SymbolTable] to a binary file, the [Irep] describing each
+//! symbol's type, value and source location are structurally hashed and
+//! uniquely numbered so that structurally identical [Irep] only get written
+//! in full to the file the first time they are encountered and that ulterior
+//! occurrences are referenced by their unique number instead.
+//! The key concept at play is that of a numbering, ie a function that assigns
+//! numbers to values of a given type.
+//!
+//! The [IrepNumbering] struct offers high-level methods to number
+//! [InternedString], [IrepId] and [Irep] values:
+//! - [InternedString] objects get mapped to [NumberedString] objects based on
+//!   the characters they contain.
+//! - [IrepId] objects get mapped to [NumberedString] objects based on the
+//!   characters of their string representation, in the same number space
+//!   as [InternedString].
+//! - [Irep] objects get mapped to [NumberedIrep] based on:
+//!     + the unique numbers assigned to their [Irep::id] attribute,
+//!     + the unique numbers of [Irep] found in their [Irep::sub] attribute,
+//!     + the pairs of unique numbers assigned to the ([IrepId],[Irep]) pairs
+//!       found in their [Ipre::named_sub] attribute.
+//!
+//! In order to assign the same number to structurally identical [Irep] objects,
+//! [IrepNumbering] essentially implements a cache where each [NumberedIrep] is
+//! keyed under an [IrepKey] that describes its internal structure.
+//!
+//! An [IrepKey] is simply the vector of unique numbers describing the
+//! `id`, `sub` and `named_sub` attributes of a [Irep].
+//!
+//! A [NumberedIrep] is conceptually a pair made of the [IrepKey] itself and the
+//! unique number assigned to that key.
+//!
+//! The cache implemented by [IrepNumbering] is bidirectional. It lets you
+//! compute the [NumberedIrep] of an [Irep], and lets you fetch a numbered
+//! [NumberedIrep] from its unique number.
+//!
+//! In practice:
+//! - the forward directon from [IrepKey] to unique numbers is implemented using a `HashMap<IrepKey,usize>`
+//! - the inverse direction from unique numbers to [NumberedIrep] is implemented usign a `Vec<NumberedIrep>`
+//!   called the `index` that stores [NumberedIrep] under their unique number.
+//!
+//! Earlier we said that an [NumberedIrep] is conceptually a pair formed of
+//! an [IrepKey] and its unique number. It is represented using only
+//! a pair formed of a `usize` representing the unique number, and a `usize`
+//! representing the index at which the key can be found inside a single vector
+//! of type `Vec<usize>` called `keys` where all [IrepKey] are concatenated when
+//! they first get numbered. The inverse map of keys is represented this way
+//! because the Rust hash map that implements the forward cache owns
+//! its keys which would make it difficult to store keys references in inverse
+//! cache, which would introduce circular dependencies and require `Rc` and
+//! liftetimes annotations everywhere.
+//!
+//! Numberig an [Irep] consists in recursively traversing it and numbering its
+//! contents in a bottom-up fashion, then assembling its [IrepKey] and querying
+//! the cache to either return an existing [NumberedIrep] or creating a new one
+//! (in case that key has never been seen before).
+//!
+//! The [GotoBinarySerializer] internally uses a [IrepNumbering] and a cache
+//! of [NumberedIrep] and [NumberedString] it has already written to file.
+//!
+//! When given an [InternedString], [IrepId] or [Irep] to serialize,
+//! the [GotoBinarySerializer] first numbers that object using its internal
+//! [IrepNumbering] instance. Then it looks up that unique number in its cache
+//! of already written objects. If the object was seen before, only the unique
+//! number of that object is written to file. If the object was never seen
+//! before, then the unique number of that object is written to file, followed
+//! by the objects describing its contents (themselves only being written fully
+//! if they have never been seen before, or only referenced if they have been
+//! seen before, etc.)
+//!
+//! The [GotoBinaryDeserializer] also uses an [IrepNumbering] and a cache
+//! of [NumberedIrep] and [NumberedString] it has already read from file.
+//! Dually to the serializer, it will only attempt to decode the contents of an
+//! object from the byte stream on the first occurrence.
 
 use crate::irep::{Irep, IrepId, Symbol, SymbolTable};
 use crate::{InternString, InternedString};
@@ -40,82 +116,6 @@ pub fn read_goto_binary_file(filename: &Path) -> io::Result<()> {
     deserializer.read_file()
 }
 
-/// # Design overview
-///
-/// When saving a [SymbolTable] to a binary file, the [Irep] describing each
-/// symbol's type, value and source location are structurally hashed and
-/// uniquely numbered so that structurally identical [Irep] only get written
-/// in full to the file the first time they are encountered and that ulterior
-/// occurrences are referenced by their unique number instead.
-/// The key concept at play is that of a numbering, ie a function that assigns
-/// numbers to values of a given type.
-///
-/// The [IrepNumbering] struct offers high-level methods to number
-/// [InternedString], [IrepId] and [Irep] values:
-/// - [InternedString] objects get mapped to [NumberedString] objects based on
-///   the characters they contain.
-/// - [IrepId] objects get mapped to [NumberedString] objects based on the
-///   characters of their string representation, in the same number space
-///   as [InternedString].
-/// - [Irep] objects get mapped to [NumberedIrep] based on:
-///     + the unique numbers assigned to their [Irep::id] attribute,
-///     + the unique numbers of [Irep] found in their [Irep::sub] attribute,
-///     + the pairs of unique numbers assigned to the ([IrepId],[Irep]) pairs
-///       found in their [Ipre::named_sub] attribute.
-///
-/// In order to assign the same number to structurally identical [Irep] objects,
-/// [IrepNumbering] essentially implements a cache where each [NumberedIrep] is
-/// keyed under an [IrepKey] that describes its internal structure.
-///
-/// An [IrepKey] is simply the vector of unique numbers describing the
-/// `id`, `sub` and `named_sub` attributes of a [Irep].
-///
-/// A [NumberedIrep] is conceptually a pair made of the [IrepKey] itself and the
-/// unique number assigned to that key.
-///
-/// The cache implemented by [IrepNumbering] is bidirectional. It lets you
-/// compute the [NumberedIrep] of an [Irep], and lets you fetch a numbered
-/// [NumberedIrep] from its unique number.
-///
-/// In practice:
-/// - the forward directon from [IrepKey] to unique numbers is implemented using a `HashMap<IrepKey,usize>`
-/// - the inverse direction from unique numbers to [NumberedIrep] is implemented usign a `Vec<NumberedIrep>`
-///   called the `index` that stores [NumberedIrep] under their unique number.
-///
-/// Earlier we said that an [NumberedIrep] is conceptually a pair formed of
-/// an [IrepKey] and its unique number. It is represented using only
-/// a pair formed of a `usize` representing the unique number, and a `usize`
-/// representing the index at which the key can be found inside a single vector
-/// of type `Vec<usize>` called `keys` where all [IrepKey] are concatenated when
-/// they first get numbered. The inverse map of keys is represented this way
-/// because the Rust hash map that implements the forward cache owns
-/// its keys which would make it difficult to store keys references in inverse
-/// cache, which would introduce circular dependencies and require `Rc` and
-/// liftetimes annotations everywhere.
-///
-/// Numberig an [Irep] consists in recursively traversing it and numbering its
-/// contents in a bottom-up fashion, then assembling its [IrepKey] and querying
-/// the cache to either return an existing [NumberedIrep] or creating a new one
-/// (in case that key has never been seen before).
-///
-/// The [GotoBinarySerializer] internally uses a [IrepNumbering] and a cache
-/// of [NumberedIrep] and [NumberedString] it has already written to file.
-///
-/// When given an [InternedString], [IrepId] or [Irep] to serialize,
-/// the [GotoBinarySerializer] first numbers that object using its internal
-/// [IrepNumbering] instance. Then it looks up that unique number in its cache
-/// of already written objects. If the object was seen before, only the unique
-/// number of that object is written to file. If the object was never seen
-/// before, then the unique number of that object is written to file, followed
-/// by the objects describing its contents (themselves only being written fully
-/// if they have never been seen before, or only referenced if they have been
-/// seen before, etc.)
-///
-/// The [GotoBinaryDeserializer] also uses an [IrepNumbering] and a cache
-/// of [NumberedIrep] and [NumberedString] it has already read from file.
-/// Dually to the serializer, it will only attempt to decode the contents of an
-/// object from the byte stream on the first occurrence.
-
 /// A numbered [InternedString]. The number is guaranteed to be in [0,N].
 /// Had to introduce this indirection because [InternedString] does not let you
 /// access its unique id, so we have to build one ourselves.

kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs

@@ -249,7 +249,6 @@ impl<'tcx> GotocCtx<'tcx> {
     /// Ensures that a struct with name `struct_name` appears in the symbol table.
     /// If it doesn't, inserts it using `f`.
     /// Returns: a struct-tag referencing the inserted struct.
-
     pub fn ensure_struct<
         T: Into<InternedString>,
         U: Into<InternedString>,

kani-compiler/src/kani_middle/resolve.rs

@@ -544,7 +544,6 @@ fn resolve_in_type_def<'tcx>(
         || ResolveError::MissingItem { tcx, base: type_id, unresolved: name.to_string() };
     // Try the inherent `impl` blocks (i.e., non-trait `impl`s).
     tcx.inherent_impls(type_id)
-        .map_err(|_| missing_item_err())?
         .iter()
         .flat_map(|impl_id| tcx.associated_item_def_ids(impl_id))
         .cloned()
@@ -588,7 +587,7 @@ where
         let simple_ty =
             fast_reject::simplify_type(tcx, internal_ty, TreatParams::InstantiateWithInfer)
                 .unwrap();
-        let impls = tcx.incoherent_impls(simple_ty).unwrap();
+        let impls = tcx.incoherent_impls(simple_ty);
         // Find the primitive impl.
         let item = impls
             .iter()

kani-compiler/src/kani_middle/transform/internal_mir.rs

@@ -7,6 +7,7 @@
 //! other maintainers wanted to keep the conversions minimal. For more information, see
 //! https://github.com/rust-lang/rust/pull/127782
 
+use rustc_middle::mir::CoercionSource;
 use rustc_middle::ty::{self as rustc_ty, TyCtxt};
 use rustc_smir::rustc_internal::internal;
 use stable_mir::mir::{
@@ -125,10 +126,17 @@ impl RustcInternalMir for CastKind {
             CastKind::PointerWithExposedProvenance => {
                 rustc_middle::mir::CastKind::PointerWithExposedProvenance
             }
+            // smir doesn't yet have CoercionSource information, so we just choose "Implicit"
             CastKind::PointerCoercion(ptr_coercion) => {
-                rustc_middle::mir::CastKind::PointerCoercion(ptr_coercion.internal_mir(tcx))
+                rustc_middle::mir::CastKind::PointerCoercion(
+                    ptr_coercion.internal_mir(tcx),
+                    CoercionSource::Implicit,
+                )
             }
-            CastKind::DynStar => rustc_middle::mir::CastKind::DynStar,
+            CastKind::DynStar => rustc_middle::mir::CastKind::PointerCoercion(
+                rustc_ty::adjustment::PointerCoercion::DynStar,
+                CoercionSource::Implicit,
+            ),
             CastKind::IntToInt => rustc_middle::mir::CastKind::IntToInt,
             CastKind::FloatToInt => rustc_middle::mir::CastKind::FloatToInt,
             CastKind::FloatToFloat => rustc_middle::mir::CastKind::FloatToFloat,

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2024-09-25"
+channel = "nightly-2024-09-26"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]