Propagate removal of RValue::Len(place) in MIR.

Propagated form rust-lang/rust#134330. `RValue::Len(place)` is still present in StableMIR, so we translate it back to MIR as `PtrMetadata(Copy(place))`.
model-checking · Jan 6, 2025 · 05e6550 · 05e6550
1 parent de97904
commit 05e6550
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 2 deletions.
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
@@ -575,7 +575,7 @@ impl<'tcx> PointsToAnalysis<'_, 'tcx> {
                 // The same story from BinOp applies here, too. Need to track those things.
                 self.successors_for_operand(state, operand)
             }
-            Rvalue::Len(..) | Rvalue::NullaryOp(..) | Rvalue::Discriminant(..) => {
+            Rvalue::NullaryOp(..) | Rvalue::Discriminant(..) => {
                 // All of those should yield a constant.
                 HashSet::new()
             }

diff --git a/kani-compiler/src/kani_middle/transform/internal_mir.rs b/kani-compiler/src/kani_middle/transform/internal_mir.rs
@@ -251,7 +251,10 @@ impl RustcInternalMir for Rvalue {
             Rvalue::Discriminant(place) => {
                 rustc_middle::mir::Rvalue::Discriminant(internal(tcx, place))
             }
-            Rvalue::Len(place) => rustc_middle::mir::Rvalue::Len(internal(tcx, place)),
+            Rvalue::Len(place) => rustc_middle::mir::Rvalue::UnaryOp(
+                rustc_middle::mir::UnOp::PtrMetadata,
+                rustc_middle::mir::Operand::Copy(internal(tcx, place)),
+            ),
             Rvalue::Ref(region, borrow_kind, place) => rustc_middle::mir::Rvalue::Ref(
                 internal(tcx, region),
                 borrow_kind.internal_mir(tcx),