Skip to content

Commit 7c9b710

Browse files
tautschnigtautschnig
authored
Update toolchain to 2024-09-26 (#3549)
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.
1 parent 61aca4c commit 7c9b710

File tree

9 files changed

+94
-90
lines changed

9 files changed

+94
-90
lines changed

‎cprover_bindings/src/goto_program/expr.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ use std::collections::BTreeMap;
1515
use std::fmt::Debug;
1616

1717
///////////////////////////////////////////////////////////////////////////////////////////////
18-
/// Datatypes
18+
// Datatypes
1919
///////////////////////////////////////////////////////////////////////////////////////////////
2020

2121
/// 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 {
292292
}
293293

294294
///////////////////////////////////////////////////////////////////////////////////////////////
295-
/// Implementations
295+
// Implementations
296296
///////////////////////////////////////////////////////////////////////////////////////////////
297297

298298
/// Getters

‎cprover_bindings/src/goto_program/stmt.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ use crate::{InternString, InternedString};
66
use std::fmt::Debug;
77

88
///////////////////////////////////////////////////////////////////////////////////////////////
9-
/// Datatypes
9+
// Datatypes
1010
///////////////////////////////////////////////////////////////////////////////////////////////
1111

1212
/// An `Stmt` represents a statement type: i.e. a computation that does not return a value.
@@ -118,7 +118,7 @@ pub struct SwitchCase {
118118
}
119119

120120
///////////////////////////////////////////////////////////////////////////////////////////////
121-
/// Implementations
121+
// Implementations
122122
///////////////////////////////////////////////////////////////////////////////////////////////
123123

124124
/// Getters

‎cprover_bindings/src/goto_program/symbol.rs

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -20,8 +20,6 @@ pub struct Symbol {
2020
/// Contracts to be enforced (only supported for functions)
2121
pub contract: Option<Box<FunctionContract>>,
2222

23-
/// Optional debugging information
24-
2523
/// Local name `x`
2624
pub base_name: Option<InternedString>,
2725
/// Fully qualifier name `foo::bar::x`

‎cprover_bindings/src/goto_program/typ.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ use std::collections::BTreeMap;
1010
use std::fmt::Debug;
1111

1212
///////////////////////////////////////////////////////////////////////////////////////////////
13-
/// Datatypes
13+
// Datatypes
1414
///////////////////////////////////////////////////////////////////////////////////////////////
1515

1616
/// Represents the different types that can be used in a goto-program.
@@ -112,7 +112,7 @@ pub struct Parameter {
112112
}
113113

114114
///////////////////////////////////////////////////////////////////////////////////////////////
115-
/// Implementations
115+
// Implementations
116116
///////////////////////////////////////////////////////////////////////////////////////////////
117117

118118
/// Getters

‎cprover_bindings/src/irep/goto_binary_serde.rs

Lines changed: 76 additions & 76 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,82 @@
11
// Copyright Kani Contributors
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33
//! GOTO binary serializer.
4+
//!
5+
//! # Design overview
6+
//!
7+
//! When saving a [SymbolTable] to a binary file, the [Irep] describing each
8+
//! symbol's type, value and source location are structurally hashed and
9+
//! uniquely numbered so that structurally identical [Irep] only get written
10+
//! in full to the file the first time they are encountered and that ulterior
11+
//! occurrences are referenced by their unique number instead.
12+
//! The key concept at play is that of a numbering, ie a function that assigns
13+
//! numbers to values of a given type.
14+
//!
15+
//! The [IrepNumbering] struct offers high-level methods to number
16+
//! [InternedString], [IrepId] and [Irep] values:
17+
//! - [InternedString] objects get mapped to [NumberedString] objects based on
18+
//! the characters they contain.
19+
//! - [IrepId] objects get mapped to [NumberedString] objects based on the
20+
//! characters of their string representation, in the same number space
21+
//! as [InternedString].
22+
//! - [Irep] objects get mapped to [NumberedIrep] based on:
23+
//! + the unique numbers assigned to their [Irep::id] attribute,
24+
//! + the unique numbers of [Irep] found in their [Irep::sub] attribute,
25+
//! + the pairs of unique numbers assigned to the ([IrepId],[Irep]) pairs
26+
//! found in their [Ipre::named_sub] attribute.
27+
//!
28+
//! In order to assign the same number to structurally identical [Irep] objects,
29+
//! [IrepNumbering] essentially implements a cache where each [NumberedIrep] is
30+
//! keyed under an [IrepKey] that describes its internal structure.
31+
//!
32+
//! An [IrepKey] is simply the vector of unique numbers describing the
33+
//! `id`, `sub` and `named_sub` attributes of a [Irep].
34+
//!
35+
//! A [NumberedIrep] is conceptually a pair made of the [IrepKey] itself and the
36+
//! unique number assigned to that key.
37+
//!
38+
//! The cache implemented by [IrepNumbering] is bidirectional. It lets you
39+
//! compute the [NumberedIrep] of an [Irep], and lets you fetch a numbered
40+
//! [NumberedIrep] from its unique number.
41+
//!
42+
//! In practice:
43+
//! - the forward directon from [IrepKey] to unique numbers is implemented using a `HashMap<IrepKey,usize>`
44+
//! - the inverse direction from unique numbers to [NumberedIrep] is implemented usign a `Vec<NumberedIrep>`
45+
//! called the `index` that stores [NumberedIrep] under their unique number.
46+
//!
47+
//! Earlier we said that an [NumberedIrep] is conceptually a pair formed of
48+
//! an [IrepKey] and its unique number. It is represented using only
49+
//! a pair formed of a `usize` representing the unique number, and a `usize`
50+
//! representing the index at which the key can be found inside a single vector
51+
//! of type `Vec<usize>` called `keys` where all [IrepKey] are concatenated when
52+
//! they first get numbered. The inverse map of keys is represented this way
53+
//! because the Rust hash map that implements the forward cache owns
54+
//! its keys which would make it difficult to store keys references in inverse
55+
//! cache, which would introduce circular dependencies and require `Rc` and
56+
//! liftetimes annotations everywhere.
57+
//!
58+
//! Numberig an [Irep] consists in recursively traversing it and numbering its
59+
//! contents in a bottom-up fashion, then assembling its [IrepKey] and querying
60+
//! the cache to either return an existing [NumberedIrep] or creating a new one
61+
//! (in case that key has never been seen before).
62+
//!
63+
//! The [GotoBinarySerializer] internally uses a [IrepNumbering] and a cache
64+
//! of [NumberedIrep] and [NumberedString] it has already written to file.
65+
//!
66+
//! When given an [InternedString], [IrepId] or [Irep] to serialize,
67+
//! the [GotoBinarySerializer] first numbers that object using its internal
68+
//! [IrepNumbering] instance. Then it looks up that unique number in its cache
69+
//! of already written objects. If the object was seen before, only the unique
70+
//! number of that object is written to file. If the object was never seen
71+
//! before, then the unique number of that object is written to file, followed
72+
//! by the objects describing its contents (themselves only being written fully
73+
//! if they have never been seen before, or only referenced if they have been
74+
//! seen before, etc.)
75+
//!
76+
//! The [GotoBinaryDeserializer] also uses an [IrepNumbering] and a cache
77+
//! of [NumberedIrep] and [NumberedString] it has already read from file.
78+
//! Dually to the serializer, it will only attempt to decode the contents of an
79+
//! object from the byte stream on the first occurrence.
480
581
use crate::irep::{Irep, IrepId, Symbol, SymbolTable};
682
use crate::{InternString, InternedString};
@@ -40,82 +116,6 @@ pub fn read_goto_binary_file(filename: &Path) -> io::Result<()> {
40116
deserializer.read_file()
41117
}
42118

43-
/// # Design overview
44-
///
45-
/// When saving a [SymbolTable] to a binary file, the [Irep] describing each
46-
/// symbol's type, value and source location are structurally hashed and
47-
/// uniquely numbered so that structurally identical [Irep] only get written
48-
/// in full to the file the first time they are encountered and that ulterior
49-
/// occurrences are referenced by their unique number instead.
50-
/// The key concept at play is that of a numbering, ie a function that assigns
51-
/// numbers to values of a given type.
52-
///
53-
/// The [IrepNumbering] struct offers high-level methods to number
54-
/// [InternedString], [IrepId] and [Irep] values:
55-
/// - [InternedString] objects get mapped to [NumberedString] objects based on
56-
/// the characters they contain.
57-
/// - [IrepId] objects get mapped to [NumberedString] objects based on the
58-
/// characters of their string representation, in the same number space
59-
/// as [InternedString].
60-
/// - [Irep] objects get mapped to [NumberedIrep] based on:
61-
/// + the unique numbers assigned to their [Irep::id] attribute,
62-
/// + the unique numbers of [Irep] found in their [Irep::sub] attribute,
63-
/// + the pairs of unique numbers assigned to the ([IrepId],[Irep]) pairs
64-
/// found in their [Ipre::named_sub] attribute.
65-
///
66-
/// In order to assign the same number to structurally identical [Irep] objects,
67-
/// [IrepNumbering] essentially implements a cache where each [NumberedIrep] is
68-
/// keyed under an [IrepKey] that describes its internal structure.
69-
///
70-
/// An [IrepKey] is simply the vector of unique numbers describing the
71-
/// `id`, `sub` and `named_sub` attributes of a [Irep].
72-
///
73-
/// A [NumberedIrep] is conceptually a pair made of the [IrepKey] itself and the
74-
/// unique number assigned to that key.
75-
///
76-
/// The cache implemented by [IrepNumbering] is bidirectional. It lets you
77-
/// compute the [NumberedIrep] of an [Irep], and lets you fetch a numbered
78-
/// [NumberedIrep] from its unique number.
79-
///
80-
/// In practice:
81-
/// - the forward directon from [IrepKey] to unique numbers is implemented using a `HashMap<IrepKey,usize>`
82-
/// - the inverse direction from unique numbers to [NumberedIrep] is implemented usign a `Vec<NumberedIrep>`
83-
/// called the `index` that stores [NumberedIrep] under their unique number.
84-
///
85-
/// Earlier we said that an [NumberedIrep] is conceptually a pair formed of
86-
/// an [IrepKey] and its unique number. It is represented using only
87-
/// a pair formed of a `usize` representing the unique number, and a `usize`
88-
/// representing the index at which the key can be found inside a single vector
89-
/// of type `Vec<usize>` called `keys` where all [IrepKey] are concatenated when
90-
/// they first get numbered. The inverse map of keys is represented this way
91-
/// because the Rust hash map that implements the forward cache owns
92-
/// its keys which would make it difficult to store keys references in inverse
93-
/// cache, which would introduce circular dependencies and require `Rc` and
94-
/// liftetimes annotations everywhere.
95-
///
96-
/// Numberig an [Irep] consists in recursively traversing it and numbering its
97-
/// contents in a bottom-up fashion, then assembling its [IrepKey] and querying
98-
/// the cache to either return an existing [NumberedIrep] or creating a new one
99-
/// (in case that key has never been seen before).
100-
///
101-
/// The [GotoBinarySerializer] internally uses a [IrepNumbering] and a cache
102-
/// of [NumberedIrep] and [NumberedString] it has already written to file.
103-
///
104-
/// When given an [InternedString], [IrepId] or [Irep] to serialize,
105-
/// the [GotoBinarySerializer] first numbers that object using its internal
106-
/// [IrepNumbering] instance. Then it looks up that unique number in its cache
107-
/// of already written objects. If the object was seen before, only the unique
108-
/// number of that object is written to file. If the object was never seen
109-
/// before, then the unique number of that object is written to file, followed
110-
/// by the objects describing its contents (themselves only being written fully
111-
/// if they have never been seen before, or only referenced if they have been
112-
/// seen before, etc.)
113-
///
114-
/// The [GotoBinaryDeserializer] also uses an [IrepNumbering] and a cache
115-
/// of [NumberedIrep] and [NumberedString] it has already read from file.
116-
/// Dually to the serializer, it will only attempt to decode the contents of an
117-
/// object from the byte stream on the first occurrence.
118-
119119
/// A numbered [InternedString]. The number is guaranteed to be in [0,N].
120120
/// Had to introduce this indirection because [InternedString] does not let you
121121
/// access its unique id, so we have to build one ourselves.

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

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -249,7 +249,6 @@ impl<'tcx> GotocCtx<'tcx> {
249249
/// Ensures that a struct with name `struct_name` appears in the symbol table.
250250
/// If it doesn't, inserts it using `f`.
251251
/// Returns: a struct-tag referencing the inserted struct.
252-
253252
pub fn ensure_struct<
254253
T: Into<InternedString>,
255254
U: Into<InternedString>,

‎kani-compiler/src/kani_middle/resolve.rs

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -544,7 +544,6 @@ fn resolve_in_type_def<'tcx>(
544544
|| ResolveError::MissingItem { tcx, base: type_id, unresolved: name.to_string() };
545545
// Try the inherent `impl` blocks (i.e., non-trait `impl`s).
546546
tcx.inherent_impls(type_id)
547-
.map_err(|_| missing_item_err())?
548547
.iter()
549548
.flat_map(|impl_id| tcx.associated_item_def_ids(impl_id))
550549
.cloned()
@@ -588,7 +587,7 @@ where
588587
let simple_ty =
589588
fast_reject::simplify_type(tcx, internal_ty, TreatParams::InstantiateWithInfer)
590589
.unwrap();
591-
let impls = tcx.incoherent_impls(simple_ty).unwrap();
590+
let impls = tcx.incoherent_impls(simple_ty);
592591
// Find the primitive impl.
593592
let item = impls
594593
.iter()

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

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@
77
//! other maintainers wanted to keep the conversions minimal. For more information, see
88
//! https://github.com/rust-lang/rust/pull/127782
99
10+
use rustc_middle::mir::CoercionSource;
1011
use rustc_middle::ty::{self as rustc_ty, TyCtxt};
1112
use rustc_smir::rustc_internal::internal;
1213
use stable_mir::mir::{
@@ -125,10 +126,17 @@ impl RustcInternalMir for CastKind {
125126
CastKind::PointerWithExposedProvenance => {
126127
rustc_middle::mir::CastKind::PointerWithExposedProvenance
127128
}
129+
// smir doesn't yet have CoercionSource information, so we just choose "Implicit"
128130
CastKind::PointerCoercion(ptr_coercion) => {
129-
rustc_middle::mir::CastKind::PointerCoercion(ptr_coercion.internal_mir(tcx))
131+
rustc_middle::mir::CastKind::PointerCoercion(
132+
ptr_coercion.internal_mir(tcx),
133+
CoercionSource::Implicit,
134+
)
130135
}
131-
CastKind::DynStar => rustc_middle::mir::CastKind::DynStar,
136+
CastKind::DynStar => rustc_middle::mir::CastKind::PointerCoercion(
137+
rustc_ty::adjustment::PointerCoercion::DynStar,
138+
CoercionSource::Implicit,
139+
),
132140
CastKind::IntToInt => rustc_middle::mir::CastKind::IntToInt,
133141
CastKind::FloatToInt => rustc_middle::mir::CastKind::FloatToInt,
134142
CastKind::FloatToFloat => rustc_middle::mir::CastKind::FloatToFloat,

‎rust-toolchain.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,5 @@
22
# SPDX-License-Identifier: Apache-2.0 OR MIT
33

44
[toolchain]
5-
channel = "nightly-2024-09-25"
5+
channel = "nightly-2024-09-26"
66
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

0 commit comments

Comments
 (0)