Fix bug in ConstantIndex unpacking

viperproject · Oct 12, 2023 · 598ec91 · 598ec91
1 parent c485102
commit 598ec91
Show file tree

Hide file tree

Showing 3 changed files with 22 additions and 61 deletions.
diff --git a/mir-state-analysis/src/free_pcs/results/repacks.rs b/mir-state-analysis/src/free_pcs/results/repacks.rs
@@ -43,7 +43,7 @@ pub enum RepackOp<'tcx> {
     /// We guarantee that the current state holds exactly the given capability for the given place.
     /// The second place is the guide, denoting e.g. the enum variant to unpack to. One can use
     /// [`Place::expand_one_level(_.0, _.1, ..)`](Place::expand_one_level) to get the set of all
-    /// places which will be obtained by unpacking.
+    /// places (except as noted in the documentation for that fn) which will be obtained by unpacking.
     ///
     /// Until rust-lang/rust#21232 lands, we guarantee that this will only have
     /// [`CapabilityKind::Exclusive`].

diff --git a/mir-state-analysis/src/utils/place.rs b/mir-state-analysis/src/utils/place.rs
@@ -49,34 +49,6 @@ use prusti_rustc_interface::middle::mir::{
 //     }
 // }
 
-fn elem_eq<'tcx>(to_cmp: (PlaceElem<'tcx>, PlaceElem<'tcx>)) -> bool {
-    use ProjectionElem::*;
-    match to_cmp {
-        (Field(left, _), Field(right, _)) => left == right,
-        (
-            ConstantIndex {
-                offset: lo,
-                min_length: lml,
-                from_end: lfe,
-            },
-            ConstantIndex {
-                offset: ro,
-                min_length: rml,
-                from_end: rfe,
-            },
-        ) => {
-            lml == rml
-                && (if lfe == rfe {
-                    lo == ro
-                } else {
-                    (lml - lo) == ro
-                })
-        }
-        (Downcast(_, left), Downcast(_, right)) => left == right,
-        (left, right) => left == right,
-    }
-}
-
 #[derive(Clone, Copy, Deref, DerefMut)]
 pub struct Place<'tcx>(PlaceRef<'tcx>);
 
@@ -127,8 +99,8 @@ impl<'tcx> Place<'tcx> {
             }
             match (left, right) {
                 (Field(..), Field(..)) => None,
-                (ConstantIndex { min_length: l, .. }, ConstantIndex { min_length: r, .. })
-                    if r == l =>
+                (ConstantIndex { min_length: l, from_end: lfe, .. }, ConstantIndex { min_length: r, from_end: rfe, .. })
+                    if r == l && lfe == rfe =>
                 {
                     None
                 }
@@ -321,6 +293,15 @@ impl Debug for Place<'_> {
     }
 }
 
+fn elem_eq<'tcx>(to_cmp: (PlaceElem<'tcx>, PlaceElem<'tcx>)) -> bool {
+    use ProjectionElem::*;
+    match to_cmp {
+        (Field(left, _), Field(right, _)) => left == right,
+        (Downcast(_, left), Downcast(_, right)) => left == right,
+        (left, right) => left == right,
+    }
+}
+
 impl PartialEq for Place<'_> {
     fn eq(&self, other: &Self) -> bool {
         self.local == other.local
@@ -340,29 +321,11 @@ impl Hash for Place<'_> {
                     discriminant(&pe).hash(state);
                     field.hash(state);
                 }
-                ProjectionElem::ConstantIndex {
-                    offset,
-                    min_length,
-                    from_end,
-                } => {
+                ProjectionElem::Downcast(_, variant) => {
                     discriminant(&pe).hash(state);
-                    let offset = if from_end {
-                        min_length - offset
-                    } else {
-                        offset
-                    };
-                    offset.hash(state);
-                    min_length.hash(state);
+                    variant.hash(state);
                 }
-                pe => {
-                    pe.hash(state);
-                }
-            }
-            if let ProjectionElem::Field(field, _) = pe {
-                discriminant(&pe).hash(state);
-                field.hash(state);
-            } else {
-                pe.hash(state);
+                _ => pe.hash(state),
             }
         }
     }

diff --git a/mir-state-analysis/src/utils/repacker.rs b/mir-state-analysis/src/utils/repacker.rs
@@ -160,7 +160,9 @@ impl<'tcx> Place<'tcx> {
 
     /// Expand `self` one level down by following the `guide_place`.
     /// Returns the new `self` and a vector containing other places that
-    /// could have resulted from the expansion.
+    /// could have resulted from the expansion. Note: this vector is always
+    /// incomplete when projecting with `Index` or `Subslice` and also when
+    /// projecting a slice type with `ConstantIndex`!
     #[tracing::instrument(level = "trace", skip(repacker), ret)]
     pub fn expand_one_level(
         self,
@@ -185,14 +187,10 @@ impl<'tcx> Place<'tcx> {
                 min_length,
                 from_end,
             } => {
-                let other_places = (0..min_length)
-                    .filter(|&i| {
-                        if from_end {
-                            i != min_length - offset
-                        } else {
-                            i != offset
-                        }
-                    })
+                let range = if from_end { 1..min_length+1 } else { 0..min_length };
+                assert!(range.contains(&offset));
+                let other_places = range
+                    .filter(|&i| i != offset)
                     .map(|i| {
                         repacker
                             .tcx