+/// See [`State`].
+#[derive(PartialEq, Eq, Debug)]
+enum StateData<V> {
+ Reachable(IndexVec<ValueIndex, V>),
+ Unreachable,
+}
+
+impl<V: Clone> Clone for StateData<V> {
+ fn clone(&self) -> Self {
+ match self {
+ Self::Reachable(x) => Self::Reachable(x.clone()),
+ Self::Unreachable => Self::Unreachable,
+ }
+ }
+
+ fn clone_from(&mut self, source: &Self) {
+ match (&mut *self, source) {
+ (Self::Reachable(x), Self::Reachable(y)) => {
+ // We go through `raw` here, because `IndexVec` currently has a naive `clone_from`.
+ x.raw.clone_from(&y.raw);
+ }
+ _ => *self = source.clone(),
+ }
+ }
+}
+
+/// The dataflow state for an instance of [`ValueAnalysis`].
+///
+/// Every instance specifies a lattice that represents the possible values of a single tracked
+/// place. If we call this lattice `V` and set set of tracked places `P`, then a [`State`] is an
+/// element of `{unreachable} ∪ (P -> V)`. This again forms a lattice, where the bottom element is
+/// `unreachable` and the top element is the mapping `p ↦ ⊤`. Note that the mapping `p ↦ ⊥` is not
+/// the bottom element (because joining an unreachable and any other reachable state yields a
+/// reachable state). All operations on unreachable states are ignored.
+///
+/// Flooding means assigning a value (by default `⊤`) to all tracked projections of a given place.
+#[derive(PartialEq, Eq, Debug)]
+pub struct State<V>(StateData<V>);
+
+impl<V: Clone> Clone for State<V> {
+ fn clone(&self) -> Self {
+ Self(self.0.clone())
+ }
+
+ fn clone_from(&mut self, source: &Self) {
+ self.0.clone_from(&source.0);
+ }
+}
+
+impl<V: Clone + HasTop + HasBottom> State<V> {
+ pub fn is_reachable(&self) -> bool {
+ matches!(&self.0, StateData::Reachable(_))
+ }