Skip to content

Commit

Permalink
Update toolchain to 1/29
Browse files Browse the repository at this point in the history
- RValue::RawRef changes, c.f. rust-lang/rust#135748 and rust-lang/rust#136590
  • Loading branch information
carolynzech committed Feb 9, 2025
1 parent 94ed3f7 commit 1c0db81
Show file tree
Hide file tree
Showing 4 changed files with 26 additions and 13 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@
use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceInstruction};
use stable_mir::{
mir::{FieldIdx, Mutability, Operand, Place, Rvalue, Statement, StatementKind},
mir::{FieldIdx, Mutability, Operand, Place, RawPtrKind, Rvalue, Statement, StatementKind},
ty::{RigidTy, Ty},
};
use strum_macros::AsRefStr;
Expand Down Expand Up @@ -123,7 +123,7 @@ impl MemoryInitOp {
Operand::Copy(place) | Operand::Move(place) => place,
Operand::Constant(_) => unreachable!(),
};
let rvalue = Rvalue::AddressOf(Mutability::Not, place.clone());
let rvalue = Rvalue::AddressOf(RawPtrKind::Const, place.clone());
rvalue.ty(body.locals()).unwrap()
}
MemoryInitOp::Unsupported { .. } | MemoryInitOp::TriviallyUnsafe { .. } => {
Expand All @@ -147,7 +147,7 @@ impl MemoryInitOp {
MemoryInitOp::AssignUnion { lvalue, .. } => {
// It does not matter which operand to return for layout generation, since both of
// them have the same pointee type.
let address_of = Rvalue::AddressOf(Mutability::Not, lvalue.clone());
let address_of = Rvalue::AddressOf(RawPtrKind::Const, lvalue.clone());
address_of.ty(body.locals()).unwrap()
}
}
Expand Down Expand Up @@ -271,7 +271,7 @@ fn mk_ref(
Operand::Copy(place) | Operand::Move(place) => place,
Operand::Constant(_) => unreachable!(),
};
let rvalue = Rvalue::AddressOf(Mutability::Not, place.clone());
let rvalue = Rvalue::AddressOf(RawPtrKind::Const, place.clone());
let ret_ty = rvalue.ty(body.locals()).unwrap();
let result = body.new_local(ret_ty, span, Mutability::Not);
let stmt = Statement { kind: StatementKind::Assign(Place::from(result), rvalue), span };
Expand Down
6 changes: 3 additions & 3 deletions kani-compiler/src/kani_middle/transform/check_values.rs
Original file line number Diff line number Diff line change
Expand Up @@ -28,8 +28,8 @@ use stable_mir::mir::mono::Instance;
use stable_mir::mir::visit::{Location, PlaceContext, PlaceRef};
use stable_mir::mir::{
AggregateKind, BasicBlockIdx, BinOp, Body, CastKind, ConstOperand, FieldIdx, Local, LocalDecl,
MirVisitor, Mutability, NonDivergingIntrinsic, Operand, Place, ProjectionElem, Rvalue,
Statement, StatementKind, Terminator, TerminatorKind,
MirVisitor, Mutability, NonDivergingIntrinsic, Operand, Place, ProjectionElem, RawPtrKind,
Rvalue, Statement, StatementKind, Terminator, TerminatorKind,
};
use stable_mir::target::{MachineInfo, MachineSize};
use stable_mir::ty::{AdtKind, IndexedVal, MirConst, RigidTy, Span, Ty, TyKind, UintTy};
Expand Down Expand Up @@ -86,7 +86,7 @@ impl ValidValuePass {
match operation {
SourceOp::BytesValidity { ranges, target_ty, rvalue } => {
let value = body.insert_assignment(rvalue, &mut source, InsertPosition::Before);
let rvalue_ptr = Rvalue::AddressOf(Mutability::Not, Place::from(value));
let rvalue_ptr = Rvalue::AddressOf(RawPtrKind::Const, Place::from(value));
for range in ranges {
let result = build_limits(body, &range, rvalue_ptr.clone(), &mut source);
let msg =
Expand Down
23 changes: 18 additions & 5 deletions kani-compiler/src/kani_middle/transform/internal_mir.rs
Original file line number Diff line number Diff line change
Expand Up @@ -13,8 +13,8 @@ use rustc_smir::rustc_internal::internal;
use stable_mir::mir::{
AggregateKind, AssertMessage, Body, BorrowKind, CastKind, ConstOperand, CopyNonOverlapping,
CoroutineDesugaring, CoroutineKind, CoroutineSource, FakeBorrowKind, FakeReadCause, LocalDecl,
MutBorrowKind, NonDivergingIntrinsic, NullOp, Operand, PointerCoercion, RetagKind, Rvalue,
Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind, UnwindAction,
MutBorrowKind, NonDivergingIntrinsic, NullOp, Operand, PointerCoercion, RawPtrKind, RetagKind,
Rvalue, Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind, UnwindAction,
UserTypeProjection, Variance,
};

Expand Down Expand Up @@ -224,9 +224,10 @@ impl RustcInternalMir for Rvalue {

fn internal_mir<'tcx>(&self, tcx: TyCtxt<'tcx>) -> Self::T<'tcx> {
match self {
Rvalue::AddressOf(mutability, place) => {
rustc_middle::mir::Rvalue::RawPtr(internal(tcx, mutability), internal(tcx, place))
}
Rvalue::AddressOf(raw_ptr_kind, place) => rustc_middle::mir::Rvalue::RawPtr(
raw_ptr_kind.internal_mir(tcx),
internal(tcx, place),
),
Rvalue::Aggregate(aggregate_kind, operands) => rustc_middle::mir::Rvalue::Aggregate(
Box::new(aggregate_kind.internal_mir(tcx)),
rustc_index::IndexVec::from_raw(
Expand Down Expand Up @@ -282,6 +283,18 @@ impl RustcInternalMir for Rvalue {
}
}

impl RustcInternalMir for RawPtrKind {
type T<'tcx> = rustc_middle::mir::RawPtrKind;

fn internal_mir<'tcx>(&self, _tcx: TyCtxt<'tcx>) -> Self::T<'tcx> {
match self {
RawPtrKind::Mut => rustc_middle::mir::RawPtrKind::Mut,
RawPtrKind::Const => rustc_middle::mir::RawPtrKind::Const,
RawPtrKind::FakeForPtrMetadata => rustc_middle::mir::RawPtrKind::FakeForPtrMetadata,
}
}
}

impl RustcInternalMir for FakeReadCause {
type T<'tcx> = rustc_middle::mir::FakeReadCause;

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-2025-01-28"
channel = "nightly-2025-01-29"
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

0 comments on commit 1c0db81

Please sign in to comment.