diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs index aa687c11cb2e..0ebeeef7a023 100644 --- a/cprover_bindings/src/goto_program/expr.rs +++ b/cprover_bindings/src/goto_program/expr.rs @@ -1687,11 +1687,6 @@ impl Expr { Stmt::assign(self, rhs, loc) } - /// Shorthand to build a `Deinit(self)` statement. See `StmtBody::Deinit` - pub fn deinit(self, loc: Location) -> Stmt { - Stmt::deinit(self, loc) - } - /// `if (self) { t } else { e }` or `if (self) { t }` pub fn if_then_else(self, t: Stmt, e: Option, loc: Location) -> Stmt { Stmt::if_then_else(self, t, e, loc) diff --git a/cprover_bindings/src/goto_program/stmt.rs b/cprover_bindings/src/goto_program/stmt.rs index 972088fe822f..46973cf0b0fd 100644 --- a/cprover_bindings/src/goto_program/stmt.rs +++ b/cprover_bindings/src/goto_program/stmt.rs @@ -64,8 +64,6 @@ pub enum StmtBody { lhs: Expr, // SymbolExpr value: Option, }, - /// Marks the target place as uninitialized. - Deinit(Expr), /// `e;` Expression(Expr), // `for (init; cond; update) {body}` @@ -252,11 +250,6 @@ impl Stmt { stmt!(Decl { lhs, value }, loc) } - /// `Deinit(place)`, see `StmtBody::Deinit`. - pub fn deinit(place: Expr, loc: Location) -> Self { - stmt!(Deinit(place), loc) - } - /// `e;` pub fn code_expression(e: Expr, loc: Location) -> Self { stmt!(Expression(e), loc) diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs index 85918ac56633..688e7f64e874 100644 --- a/cprover_bindings/src/irep/to_irep.rs +++ b/cprover_bindings/src/irep/to_irep.rs @@ -541,13 +541,6 @@ impl ToIrep for StmtBody { code_irep(IrepId::Decl, vec![lhs.to_irep(mm)]) } } - StmtBody::Deinit(place) => { - // CBMC doesn't yet have a notion of poison (https://github.com/diffblue/cbmc/issues/7014) - // So we translate identically to `nondet` here, but add a comment noting we wish it were poison - // potentially for other backends to pick up and treat specially. - code_irep(IrepId::Assign, vec![place.to_irep(mm), place.typ().nondet().to_irep(mm)]) - .with_comment("deinit") - } StmtBody::Expression(e) => code_irep(IrepId::Expression, vec![e.to_irep(mm)]), StmtBody::For { init, cond, update, body } => code_irep( IrepId::For, diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index b79c96359d43..b38f30e58cce 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -129,7 +129,6 @@ impl GotocCtx<'_, '_> { .assign(self.codegen_rvalue_stable(rhs, location), location) } } - StatementKind::Deinit(place) => self.codegen_deinit(place, location), StatementKind::SetDiscriminant { place, variant_index } => { let dest_ty = self.place_ty_stable(place); let dest_expr = unwrap_or_return_codegen_unimplemented_stmt!( @@ -444,27 +443,6 @@ impl GotocCtx<'_, '_> { } } - /// From rustc doc: "This writes `uninit` bytes to the entire place." - /// Our model of GotoC has a similar statement, which is later lowered - /// to assigning a Nondet in CBMC, with a comment specifying that it - /// corresponds to a Deinit. - fn codegen_deinit(&mut self, place: &Place, loc: Location) -> Stmt { - let dst_mir_ty = self.place_ty_stable(place); - let dst_type = self.codegen_ty_stable(dst_mir_ty); - let layout = self.layout_of_stable(dst_mir_ty); - if layout.is_zst() || dst_type.sizeof_in_bits(&self.symbol_table) == 0 { - // We ignore assignment for all zero size types - Stmt::skip(loc) - } else { - unwrap_or_return_codegen_unimplemented_stmt!( - self, - self.codegen_place_stable(place, loc) - ) - .goto_expr - .deinit(loc) - } - } - /// A special case handler to codegen `return ();` fn codegen_ret_unit(&mut self, loc: Location) -> Stmt { let is_file_local = false; diff --git a/kani-compiler/src/kani_middle/analysis.rs b/kani-compiler/src/kani_middle/analysis.rs index a2f3007c007f..1720e043344e 100644 --- a/kani-compiler/src/kani_middle/analysis.rs +++ b/kani-compiler/src/kani_middle/analysis.rs @@ -123,7 +123,6 @@ impl From<&Statement> for Key { fn from(value: &Statement) -> Self { match value.kind { StatementKind::Assign(..) => Key("Assign"), - StatementKind::Deinit(_) => Key("Deinit"), StatementKind::Intrinsic(_) => Key("Intrinsic"), StatementKind::SetDiscriminant { .. } => Key("SetDiscriminant"), // For now, we don't care about the ones below. diff --git a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs index 47eed40f19c4..267c8ff105c0 100644 --- a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs +++ b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs @@ -171,7 +171,6 @@ impl<'tcx> Analysis<'tcx> for PointsToAnalysis<'_, 'tcx> { } StatementKind::FakeRead(..) | StatementKind::SetDiscriminant { .. } - | StatementKind::Deinit(..) | StatementKind::StorageLive(..) | StatementKind::StorageDead(..) | StatementKind::Retag(..) diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index fc8be9e671a2..277f49f8ed14 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -569,7 +569,6 @@ pub trait MutMirVisitor { }, StatementKind::FakeRead(_, _) | StatementKind::SetDiscriminant { .. } - | StatementKind::Deinit(_) | StatementKind::StorageLive(_) | StatementKind::StorageDead(_) | StatementKind::Retag(_, _) diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs index db5da16fcaae..b8edc1f85e36 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs @@ -220,14 +220,6 @@ impl MirVisitor for CheckUninitVisitor { } } } - StatementKind::Deinit(place) => { - self.super_statement(stmt, location); - self.push_target(MemoryInitOp::Set { - operand: Operand::Copy(place.clone()), - value: false, - position: InsertPosition::After, - }); - } StatementKind::FakeRead(_, _) | StatementKind::SetDiscriminant { .. } | StatementKind::StorageLive(_) diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs index d0c6b2e6abf7..6334648fdd09 100644 --- a/kani-compiler/src/kani_middle/transform/check_values.rs +++ b/kani-compiler/src/kani_middle/transform/check_values.rs @@ -411,7 +411,6 @@ impl MirVisitor for CheckValueVisitor<'_, '_> { } StatementKind::FakeRead(_, _) | StatementKind::SetDiscriminant { .. } - | StatementKind::Deinit(_) | StatementKind::StorageLive(_) | StatementKind::StorageDead(_) | StatementKind::Retag(_, _) diff --git a/kani-compiler/src/kani_middle/transform/internal_mir.rs b/kani-compiler/src/kani_middle/transform/internal_mir.rs index 7c76f91f87bc..4db9d4cca4c3 100644 --- a/kani-compiler/src/kani_middle/transform/internal_mir.rs +++ b/kani-compiler/src/kani_middle/transform/internal_mir.rs @@ -381,9 +381,6 @@ impl RustcInternalMir for StatementKind { variant_index: internal(tcx, variant_index), } } - StatementKind::Deinit(place) => { - rustc_middle::mir::StatementKind::Deinit(internal(tcx, place).into()) - } StatementKind::StorageLive(local) => rustc_middle::mir::StatementKind::StorageLive( rustc_middle::mir::Local::from_usize(*local), ), diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 2f040813b84d..5489956d51e4 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2025-10-11" +channel = "nightly-2025-10-12" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]