Skip to content

Commit

Permalink
Update toolchain to 2024-09-26 (#3549)
Browse files Browse the repository at this point in the history
Changes required due to:
- rust-lang/rust#130234 improve compile errors
for invalid ptr-to-ptr casts with trait objects
- rust-lang/rust@cfb8419900 Separate collection of crate-local inherent
impls from error reporting
- rust-lang/rust@40fca8f7a8 Bump Clippy version -> 0.1.83

Resolves: #3548

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
tautschnig authored Sep 27, 2024
1 parent 61aca4c commit 7c9b710
Show file tree
Hide file tree
Showing 9 changed files with 94 additions and 90 deletions.
4 changes: 2 additions & 2 deletions cprover_bindings/src/goto_program/expr.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -292,7 +292,7 @@ pub fn arithmetic_overflow_result_type(operand_type: Type) -> Type {
}

///////////////////////////////////////////////////////////////////////////////////////////////
/// Implementations
// Implementations
///////////////////////////////////////////////////////////////////////////////////////////////

/// Getters
Expand Down
4 changes: 2 additions & 2 deletions cprover_bindings/src/goto_program/stmt.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -118,7 +118,7 @@ pub struct SwitchCase {
}

///////////////////////////////////////////////////////////////////////////////////////////////
/// Implementations
// Implementations
///////////////////////////////////////////////////////////////////////////////////////////////

/// Getters
Expand Down
2 changes: 0 additions & 2 deletions cprover_bindings/src/goto_program/symbol.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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`
Expand Down
4 changes: 2 additions & 2 deletions cprover_bindings/src/goto_program/typ.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -112,7 +112,7 @@ pub struct Parameter {
}

///////////////////////////////////////////////////////////////////////////////////////////////
/// Implementations
// Implementations
///////////////////////////////////////////////////////////////////////////////////////////////

/// Getters
Expand Down
152 changes: 76 additions & 76 deletions cprover_bindings/src/irep/goto_binary_serde.rs
Original file line number Diff line number Diff line change
@@ -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};
Expand Down Expand Up @@ -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.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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>,
Expand Down
3 changes: 1 addition & 2 deletions kani-compiler/src/kani_middle/resolve.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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()
Expand Down Expand Up @@ -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()
Expand Down
12 changes: 10 additions & 2 deletions kani-compiler/src/kani_middle/transform/internal_mir.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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::{
Expand Down Expand Up @@ -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,
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-09-25"
channel = "nightly-2024-09-26"
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

0 comments on commit 7c9b710

Please sign in to comment.