Skip to content

Commit

Permalink
Automatic toolchain upgrade to nightly-2024-10-04 (#3570)
Browse files Browse the repository at this point in the history
Update Rust toolchain from nightly-2024-10-03 to nightly-2024-10-04
without any other source changes.

---------

Signed-off-by: Felipe R. Monteiro <[email protected]>
Co-authored-by: celinval <[email protected]>
Co-authored-by: Felipe R. Monteiro <[email protected]>
  • Loading branch information
3 people authored Oct 10, 2024
1 parent 53d9a52 commit 509710a
Show file tree
Hide file tree
Showing 34 changed files with 54 additions and 54 deletions.
4 changes: 2 additions & 2 deletions cprover_bindings/src/irep/serialize.rs
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,7 @@ impl Serialize for crate::goto_program::SymbolTable {
}
}
struct StreamingSymbols<'a>(&'a crate::goto_program::SymbolTable);
impl<'a> Serialize for StreamingSymbols<'a> {
impl Serialize for StreamingSymbols<'_> {
fn serialize<S>(&self, serializer: S) -> Result<S::Ok, S::Error>
where
S: Serializer,
Expand Down Expand Up @@ -92,7 +92,7 @@ impl<'de> serde::Deserialize<'de> for InternedString {
}
}

impl<'de> serde::de::Visitor<'de> for InternedStringVisitor {
impl serde::de::Visitor<'_> for InternedStringVisitor {
type Value = InternedString;

fn expecting(&self, formatter: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
Expand Down
2 changes: 1 addition & 1 deletion kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
Original file line number Diff line number Diff line change
Expand Up @@ -107,7 +107,7 @@ impl PropertyClass {
}
}

impl<'tcx> GotocCtx<'tcx> {
impl GotocCtx<'_> {
/// Generates a CBMC assertion. Note: Does _NOT_ assume.
pub fn codegen_assert(
&self,
Expand Down
2 changes: 1 addition & 1 deletion kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ pub fn bb_label(bb: BasicBlockIdx) -> String {
format!("bb{bb}")
}

impl<'tcx> GotocCtx<'tcx> {
impl GotocCtx<'_> {
/// Generates Goto-C for a basic block.
///
/// A MIR basic block consists of 0 or more statements followed by a terminator.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ use stable_mir::mir::mono::{Instance, MonoItem};
use stable_mir::mir::{Local, VarDebugInfoContents};
use stable_mir::ty::{FnDef, RigidTy, TyKind};

impl<'tcx> GotocCtx<'tcx> {
impl GotocCtx<'_> {
/// Given the `proof_for_contract` target `function_under_contract` and the reachable `items`,
/// find or create the `AssignsContract` that needs to be enforced and attach it to the symbol
/// for which it needs to be enforced.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ lazy_static! {
};
}

impl<'tcx> GotocCtx<'tcx> {
impl GotocCtx<'_> {
/// Generate the symbol and symbol table entry for foreign items.
///
/// CBMC built-in functions that are supported by Kani are always added to the symbol table, and
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ use std::collections::BTreeMap;
use tracing::{debug, debug_span};

/// Codegen MIR functions into gotoc
impl<'tcx> GotocCtx<'tcx> {
impl GotocCtx<'_> {
/// Declare variables according to their index.
/// - Index 0 represents the return value.
/// - Indices [1, N] represent the function parameters where N is the number of parameters.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ enum VTableInfo {
Align,
}

impl<'tcx> GotocCtx<'tcx> {
impl GotocCtx<'_> {
fn binop<F: FnOnce(Expr, Expr) -> Expr>(
&mut self,
place: &Place,
Expand Down
2 changes: 1 addition & 1 deletion kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
Original file line number Diff line number Diff line change
Expand Up @@ -224,7 +224,7 @@ impl TypeOrVariant {
}
}

impl<'tcx> GotocCtx<'tcx> {
impl GotocCtx<'_> {
/// Codegen field access for types that allow direct field projection.
///
/// I.e.: Algebraic data types, closures, and coroutines.
Expand Down
2 changes: 1 addition & 1 deletion kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ use stable_mir::ty::{ClosureKind, IntTy, RigidTy, Size, Ty, TyConst, TyKind, Uin
use std::collections::BTreeMap;
use tracing::{debug, trace, warn};

impl<'tcx> GotocCtx<'tcx> {
impl GotocCtx<'_> {
fn codegen_comparison(&mut self, op: &BinOp, e1: &Operand, e2: &Operand) -> Expr {
let left_op = self.codegen_operand_stable(e1);
let right_op = self.codegen_operand_stable(e2);
Expand Down
2 changes: 1 addition & 1 deletion kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ lazy_static! {
("pointer-primitive", "disable:pointer-primitive-check")].iter().copied().collect();
}

impl<'tcx> GotocCtx<'tcx> {
impl GotocCtx<'_> {
pub fn codegen_span(&self, sp: &Span) -> Location {
self.codegen_span_stable(rustc_internal::stable(sp))
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ use stable_mir::mir::{
use stable_mir::ty::{Abi, RigidTy, Span, Ty, TyKind, VariantIdx};
use tracing::{debug, debug_span, trace};

impl<'tcx> GotocCtx<'tcx> {
impl GotocCtx<'_> {
/// Generate Goto-C for MIR [Statement]s.
/// This does not cover all possible "statements" because MIR distinguishes between ordinary
/// statements and [Terminator]s, which can exclusively appear at the end of a basic block.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ use stable_mir::CrateDef;
use stable_mir::mir::mono::{Instance, StaticDef};
use tracing::debug;

impl<'tcx> GotocCtx<'tcx> {
impl GotocCtx<'_> {
/// Ensures a static variable is initialized.
///
/// Note that each static variable have their own location in memory. Per Rust documentation:
Expand Down
4 changes: 2 additions & 2 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
Original file line number Diff line number Diff line change
Expand Up @@ -91,7 +91,7 @@ impl TypeExt for Type {
}

/// Function signatures
impl<'tcx> GotocCtx<'tcx> {
impl GotocCtx<'_> {
/// This method prints the details of a GotoC type, for debugging purposes.
#[allow(unused)]
pub(crate) fn debug_print_type_recursively(&self, ty: &Type) -> String {
Expand Down Expand Up @@ -1615,7 +1615,7 @@ impl<'tcx> GotocCtx<'tcx> {
pub ctx: &'a GotocCtx<'tcx>,
}

impl<'tcx, 'a> Iterator for ReceiverIter<'tcx, 'a> {
impl<'tcx> Iterator for ReceiverIter<'tcx, '_> {
type Item = (String, Ty<'tcx>);

fn next(&mut self) -> Option<Self::Item> {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -84,7 +84,7 @@ impl<'tcx> CurrentFnCtx<'tcx> {
}

/// Setters
impl<'tcx> CurrentFnCtx<'tcx> {
impl CurrentFnCtx<'_> {
/// Returns the current block, replacing it with an empty vector.
pub fn extract_block(&mut self) -> Vec<Stmt> {
std::mem::take(&mut self.block)
Expand Down
6 changes: 3 additions & 3 deletions kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
Original file line number Diff line number Diff line change
Expand Up @@ -119,7 +119,7 @@ impl<'tcx> GotocCtx<'tcx> {
}

/// Generate variables
impl<'tcx> GotocCtx<'tcx> {
impl GotocCtx<'_> {
/// Declare a local variable.
/// Handles the bookkeeping of:
/// - creating the symbol
Expand Down Expand Up @@ -302,7 +302,7 @@ impl<'tcx> GotocCtx<'tcx> {
}

/// Mutators
impl<'tcx> GotocCtx<'tcx> {
impl GotocCtx<'_> {
pub fn set_current_fn(&mut self, instance: Instance, body: &Body) {
self.current_fn = Some(CurrentFnCtx::new(instance, self, body));
}
Expand Down Expand Up @@ -346,7 +346,7 @@ impl<'tcx> HasTyCtxt<'tcx> for GotocCtx<'tcx> {
}
}

impl<'tcx> HasDataLayout for GotocCtx<'tcx> {
impl HasDataLayout for GotocCtx<'_> {
fn data_layout(&self) -> &TargetDataLayout {
self.tcx.data_layout()
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -104,7 +104,7 @@ impl VtableCtx {
}
}

impl<'tcx> GotocCtx<'tcx> {
impl GotocCtx<'_> {
/// Create a label to the virtual call site
pub fn virtual_call_with_restricted_fn_ptr(
&mut self,
Expand Down
2 changes: 1 addition & 1 deletion kani-compiler/src/codegen_cprover_gotoc/utils/names.rs
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ use rustc_middle::mir::mono::CodegenUnitNameBuilder;
use rustc_middle::ty::TyCtxt;
use stable_mir::mir::Local;

impl<'tcx> GotocCtx<'tcx> {
impl GotocCtx<'_> {
/// The full crate name including versioning info
pub fn full_crate_name(&self) -> &str {
&self.full_crate_name
Expand Down
4 changes: 2 additions & 2 deletions kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ pub fn dynamic_fat_ptr(typ: Type, data: Expr, vtable: Expr, symbol_table: &Symbo
Expr::struct_expr(typ, btree_string_map![("data", data), ("vtable", vtable)], symbol_table)
}

impl<'tcx> GotocCtx<'tcx> {
impl GotocCtx<'_> {
pub fn unsupported_msg(item: &str, url: Option<&str>) -> String {
let mut s = format!("{item} is not currently supported by Kani");
if let Some(url) = url {
Expand Down Expand Up @@ -71,7 +71,7 @@ impl<'tcx> GotocCtx<'tcx> {
/// Members traverse path to get to the raw pointer of a box (b.0.pointer.pointer).
const RAW_PTR_FROM_BOX: [&str; 3] = ["0", "pointer", "pointer"];

impl<'tcx> GotocCtx<'tcx> {
impl GotocCtx<'_> {
/// Dereference a boxed type `std::boxed::Box<T>` to get a `*T`.
///
/// WARNING: This is based on a manual inspection of how boxed types are currently
Expand Down
4 changes: 2 additions & 2 deletions kani-compiler/src/kani_middle/attributes.rs
Original file line number Diff line number Diff line change
Expand Up @@ -140,7 +140,7 @@ pub struct ContractAttributes {
pub modifies_wrapper: Symbol,
}

impl<'tcx> std::fmt::Debug for KaniAttributes<'tcx> {
impl std::fmt::Debug for KaniAttributes<'_> {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
f.debug_struct("KaniAttributes")
.field("item", &self.tcx.def_path_debug_str(self.item))
Expand Down Expand Up @@ -726,7 +726,7 @@ struct UnstableAttrParseError<'a> {
attr: &'a Attribute,
}

impl<'a> UnstableAttrParseError<'a> {
impl UnstableAttrParseError<'_> {
/// Report the error in a friendly format.
fn report(&self, tcx: TyCtxt) -> ErrorGuaranteed {
tcx.dcx()
Expand Down
2 changes: 1 addition & 1 deletion kani-compiler/src/kani_middle/coercion.rs
Original file line number Diff line number Diff line change
Expand Up @@ -189,7 +189,7 @@ impl<'tcx> CoerceUnsizedIterator<'tcx> {
/// dst_ty: Ty, // *const &dyn Debug
/// }
/// ```
impl<'tcx> Iterator for CoerceUnsizedIterator<'tcx> {
impl Iterator for CoerceUnsizedIterator<'_> {
type Item = CoerceUnsizedInfo;

fn next(&mut self) -> Option<Self::Item> {
Expand Down
4 changes: 2 additions & 2 deletions kani-compiler/src/kani_middle/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -77,7 +77,7 @@ struct FindUnsafeCell<'tcx> {
tcx: TyCtxt<'tcx>,
}

impl<'tcx> TyVisitor for FindUnsafeCell<'tcx> {
impl TyVisitor for FindUnsafeCell<'_> {
type Break = ();
fn visit_ty(&mut self, ty: &Ty) -> ControlFlow<Self::Break> {
match ty.kind() {
Expand Down Expand Up @@ -171,7 +171,7 @@ impl<'tcx> HasTyCtxt<'tcx> for CompilerHelpers<'tcx> {
}
}

impl<'tcx> HasDataLayout for CompilerHelpers<'tcx> {
impl HasDataLayout for CompilerHelpers<'_> {
fn data_layout(&self) -> &TargetDataLayout {
self.tcx.data_layout()
}
Expand Down
6 changes: 3 additions & 3 deletions kani-compiler/src/kani_middle/points_to/points_to_analysis.rs
Original file line number Diff line number Diff line change
Expand Up @@ -114,7 +114,7 @@ impl<'a, 'tcx> PointsToAnalysis<'a, 'tcx> {
}
}

impl<'a, 'tcx> AnalysisDomain<'tcx> for PointsToAnalysis<'a, 'tcx> {
impl<'tcx> AnalysisDomain<'tcx> for PointsToAnalysis<'_, 'tcx> {
/// Dataflow state at each instruction.
type Domain = PointsToGraph<'tcx>;

Expand All @@ -135,7 +135,7 @@ impl<'a, 'tcx> AnalysisDomain<'tcx> for PointsToAnalysis<'a, 'tcx> {
}
}

impl<'a, 'tcx> Analysis<'tcx> for PointsToAnalysis<'a, 'tcx> {
impl<'tcx> Analysis<'tcx> for PointsToAnalysis<'_, 'tcx> {
/// Update current dataflow state based on the information we can infer from the given
/// statement.
fn apply_statement_effect(
Expand Down Expand Up @@ -366,7 +366,7 @@ fn try_resolve_instance<'tcx>(
}
}

impl<'a, 'tcx> PointsToAnalysis<'a, 'tcx> {
impl<'tcx> PointsToAnalysis<'_, 'tcx> {
/// Update the analysis state according to the operation, which is semantically equivalent to `*to = *from`.
fn apply_copy_effect(
&self,
Expand Down
6 changes: 3 additions & 3 deletions kani-compiler/src/kani_middle/points_to/points_to_graph.rs
Original file line number Diff line number Diff line change
Expand Up @@ -70,7 +70,7 @@ struct NodeData<'tcx> {
ancestors: HashSet<MemLoc<'tcx>>,
}

impl<'tcx> NodeData<'tcx> {
impl NodeData<'_> {
/// Merge two instances of NodeData together, return true if the original one was updated and
/// false otherwise.
fn merge(&mut self, other: Self) -> bool {
Expand Down Expand Up @@ -232,7 +232,7 @@ impl<'tcx> PointsToGraph<'tcx> {
/// join operation. In our case, this is a simple union of two graphs. This "lattice" is finite,
/// because in the worst case all places will alias to all places, in which case the join will be a
/// no-op.
impl<'tcx> JoinSemiLattice for PointsToGraph<'tcx> {
impl JoinSemiLattice for PointsToGraph<'_> {
fn join(&mut self, other: &Self) -> bool {
let mut updated = false;
// Check every node in the other graph.
Expand All @@ -247,4 +247,4 @@ impl<'tcx> JoinSemiLattice for PointsToGraph<'tcx> {

/// This is a requirement for the fixpoint solver, and there is no derive macro for this, so
/// implement it manually.
impl<'tcx, C> DebugWithContext<C> for PointsToGraph<'tcx> {}
impl<C> DebugWithContext<C> for PointsToGraph<'_> {}
4 changes: 2 additions & 2 deletions kani-compiler/src/kani_middle/reachability.rs
Original file line number Diff line number Diff line change
Expand Up @@ -245,7 +245,7 @@ struct MonoItemsFnCollector<'a, 'tcx> {
body: &'a Body,
}

impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> {
impl MonoItemsFnCollector<'_, '_> {
/// Collect the implementation of all trait methods and its supertrait methods for the given
/// concrete type.
fn collect_vtable_methods(&mut self, concrete_ty: Ty, trait_ty: Ty) {
Expand Down Expand Up @@ -350,7 +350,7 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> {
/// 6. Static Initialization
///
/// Remark: This code has been mostly taken from `rustc_monomorphize::collector::MirNeighborCollector`.
impl<'a, 'tcx> MirVisitor for MonoItemsFnCollector<'a, 'tcx> {
impl MirVisitor for MonoItemsFnCollector<'_, '_> {
/// Collect the following:
/// - Trait implementations when casting from concrete to dyn Trait.
/// - Functions / Closures that have their address taken.
Expand Down
4 changes: 2 additions & 2 deletions kani-compiler/src/kani_middle/resolve.rs
Original file line number Diff line number Diff line change
Expand Up @@ -184,13 +184,13 @@ pub enum ResolveError<'tcx> {
UnsupportedPath { kind: &'static str },
}

impl<'tcx> fmt::Debug for ResolveError<'tcx> {
impl fmt::Debug for ResolveError<'_> {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
std::fmt::Display::fmt(self, f)
}
}

impl<'tcx> fmt::Display for ResolveError<'tcx> {
impl fmt::Display for ResolveError<'_> {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
match self {
ResolveError::ExtraSuper => {
Expand Down
2 changes: 1 addition & 1 deletion kani-compiler/src/kani_middle/stubbing/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -183,7 +183,7 @@ impl<'tcx> StubConstChecker<'tcx> {
}
}

impl<'tcx> MirVisitor for StubConstChecker<'tcx> {
impl MirVisitor for StubConstChecker<'_> {
/// Collect constants that are represented as static variables.
fn visit_const_operand(&mut self, constant: &ConstOperand, location: Location) {
let const_ = self.monomorphize(rustc_internal::internal(self.tcx, &constant.const_));
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,7 @@ pub struct InstrumentationVisitor<'a, 'tcx> {
tcx: TyCtxt<'tcx>,
}

impl<'a, 'tcx> TargetFinder for InstrumentationVisitor<'a, 'tcx> {
impl TargetFinder for InstrumentationVisitor<'_, '_> {
fn find_all(mut self, body: &MutableBody) -> Vec<InitRelevantInstruction> {
for (bb_idx, bb) in body.blocks().iter().enumerate() {
self.current_target = InitRelevantInstruction {
Expand Down Expand Up @@ -75,7 +75,7 @@ impl<'a, 'tcx> InstrumentationVisitor<'a, 'tcx> {
}
}

impl<'a, 'tcx> MirVisitor for InstrumentationVisitor<'a, 'tcx> {
impl MirVisitor for InstrumentationVisitor<'_, '_> {
fn visit_statement(&mut self, stmt: &Statement, location: Location) {
self.super_statement(stmt, location);
// Switch to the next statement.
Expand Down
2 changes: 1 addition & 1 deletion kani-compiler/src/kani_middle/transform/check_values.rs
Original file line number Diff line number Diff line change
Expand Up @@ -325,7 +325,7 @@ impl<'a, 'b> CheckValueVisitor<'a, 'b> {
}
}

impl<'a, 'b> MirVisitor for CheckValueVisitor<'a, 'b> {
impl MirVisitor for CheckValueVisitor<'_, '_> {
fn visit_statement(&mut self, stmt: &Statement, location: Location) {
if self.skip_next {
self.skip_next = false;
Expand Down
6 changes: 3 additions & 3 deletions kani-compiler/src/kani_middle/transform/stubs.rs
Original file line number Diff line number Diff line change
Expand Up @@ -139,7 +139,7 @@ struct FnStubValidator<'a, 'tcx> {
is_valid: bool,
}

impl<'a, 'tcx> FnStubValidator<'a, 'tcx> {
impl FnStubValidator<'_, '_> {
fn validate(tcx: TyCtxt, stub: (FnDef, FnDef), new_instance: Instance) -> Option<Body> {
if validate_stub_const(tcx, new_instance) {
let body = new_instance.body().unwrap();
Expand All @@ -153,7 +153,7 @@ impl<'a, 'tcx> FnStubValidator<'a, 'tcx> {
}
}

impl<'a, 'tcx> MirVisitor for FnStubValidator<'a, 'tcx> {
impl MirVisitor for FnStubValidator<'_, '_> {
fn visit_operand(&mut self, op: &Operand, loc: Location) {
let op_ty = op.ty(self.locals).unwrap();
if let TyKind::RigidTy(RigidTy::FnDef(def, args)) = op_ty.kind() {
Expand Down Expand Up @@ -188,7 +188,7 @@ struct ExternFnStubVisitor<'a> {
stubs: &'a Stubs,
}

impl<'a> MutMirVisitor for ExternFnStubVisitor<'a> {
impl MutMirVisitor for ExternFnStubVisitor<'_> {
fn visit_terminator(&mut self, term: &mut Terminator) {
// Replace direct calls
if let TerminatorKind::Call { func, .. } = &mut term.kind {
Expand Down
Loading

0 comments on commit 509710a

Please sign in to comment.