diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs index dad3b06e7753..2a29985cb229 100644 --- a/cprover_bindings/src/goto_program/expr.rs +++ b/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 diff --git a/cprover_bindings/src/goto_program/stmt.rs b/cprover_bindings/src/goto_program/stmt.rs index 951e58f9a954..2afbdafc95a3 100644 --- a/cprover_bindings/src/goto_program/stmt.rs +++ b/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 diff --git a/cprover_bindings/src/goto_program/symbol.rs b/cprover_bindings/src/goto_program/symbol.rs index 457be1163a3a..5c86dd04909a 100644 --- a/cprover_bindings/src/goto_program/symbol.rs +++ b/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>, - /// Optional debugging information - /// Local name `x` pub base_name: Option, /// Fully qualifier name `foo::bar::x` diff --git a/cprover_bindings/src/goto_program/typ.rs b/cprover_bindings/src/goto_program/typ.rs index 3210dd46e43f..6e087a6b7f58 100644 --- a/cprover_bindings/src/goto_program/typ.rs +++ b/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 diff --git a/cprover_bindings/src/irep/goto_binary_serde.rs b/cprover_bindings/src/irep/goto_binary_serde.rs index bb725de638cf..1e2dc37eb589 100644 --- a/cprover_bindings/src/irep/goto_binary_serde.rs +++ b/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` +//! - the inverse direction from unique numbers to [NumberedIrep] is implemented usign a `Vec` +//! 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` 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` -/// - the inverse direction from unique numbers to [NumberedIrep] is implemented usign a `Vec` -/// 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` 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. diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs index d88506464cf7..3a47f7b9c09c 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/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, U: Into, diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs index d71f9710d404..31cf55650559 100644 --- a/kani-compiler/src/kani_middle/resolve.rs +++ b/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() diff --git a/kani-compiler/src/kani_middle/transform/internal_mir.rs b/kani-compiler/src/kani_middle/transform/internal_mir.rs index ba23fbf2dddf..d29a5e688d2c 100644 --- a/kani-compiler/src/kani_middle/transform/internal_mir.rs +++ b/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, diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 3cd835927ee1..9b6300f9fa74 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-09-25" +channel = "nightly-2024-09-26" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]