Rework checker to not require DefAlloc by tracking all vregs on each alloc.

The symbolic checker currently works by tracking a single symbolic vreg
label for each "alloc" (physical register or stack slot). On definition
of a vreg into an alloc, the label is updated to the new vreg's name.

This worked quite well when the regalloc was simpler, but in the
presence of redundant move elimination, it started to become apparent
that the analysis has a shortcoming: when multiple vregs have the same
value, and the regalloc has deduced this, it can make use of an alloc
that is labeled with one vreg but use it as another vreg and the checker
will not validate the use.

In other words, the regalloc became smart enough to avoid emitting
unnecessary moves, but the checker was relying on those moves to know
the most up-to-date symbolic name for a value in a physical location. In
a sense, a register or stackslot can contain *both* vreg1 and vreg2, and
the regalloc can use it as either.

The stopgap measure of emitting more DefAllocs as part of the redundant
move elimination never quite sat right with me. It works, but it's
asking too much of the regalloc to prove why its moves are correct. We
should rely less on the regalloc and on complex
built-just-for-the-checker plumbing; we should instead improve the
checker so that it can prove on its own that the result is correct.

This PR modifies the checker so that its basic abstraction for an
alloc's value is a *set* of virtual register labels, rather than just
one. The transfer function is a little more complex, but manageable: a
move keeps the old label(s) and adds a new one; redefining a vreg into
one alloc needs to remove that vreg label from all other alloc's sets.

This completely removes the need for metadata from the regalloc (!); all
we need is the original program (pre-alloc, with vregs), the set of
allocations, and the set of inserted moves, and we can validate the
result. This should mean that we trust our checker-validated allocation
results more, and should result in less complexity and maintenance going
forward if we improve the allocator further.

src/checker.rs

@@ -3,7 +3,7 @@
  * regalloc.rs project
  * (https://github.com/bytecodealliance/regalloc.rs). regalloc.rs is
  * also licensed under Apache-2.0 with the LLVM exception, as the rest
- * of regalloc2's non-Ion-derived code is.
+ * of regalloc2 is.
  */
 
 //! Checker: verifies that spills/reloads/moves retain equivalent
@@ -17,55 +17,73 @@
 //! conceptually generates a symbolic value "Vn" when storing to (or
 //! modifying) a virtual register.
 //!
+//! A symbolic value is logically a *set of virtual registers*,
+//! representing all virtual registers equal to the value in the given
+//! storage slot at a given program point. This representation (as
+//! opposed to tracking just one virtual register) is necessary
+//! because the regalloc may implement moves in the source program
+//! (via move instructions or blockparam assignments on edges) in
+//! "intelligent" ways, taking advantage of values that are already in
+//! the right place, so we need to know *all* names for a value.
+//!
 //! These symbolic values are precise but partial: in other words, if
 //! a physical register is described as containing a virtual register
 //! at a program point, it must actually contain the value of this
-//! register (modulo any analysis bugs); but it may resolve to
+//! register (modulo any analysis bugs); but it may describe fewer
-//! `Conflicts` even in cases where one *could* statically prove that
+//! virtual registers even in cases where one *could* statically prove
-//! it contains a certain register, because the analysis is not
+//! that it contains a certain register, because the analysis is not
 //! perfectly path-sensitive or value-sensitive. However, all
 //! assignments *produced by our register allocator* should be
-//! analyzed fully precisely.
+//! analyzed fully precisely. (This last point is important and bears
+//! repeating: we only need to verify the programs that we produce,
+//! not arbitrary programs.)
 //!
 //! Operand constraints (fixed register, register, any) are also checked
 //! at each operand.
 //!
-//! The dataflow analysis state at each program point is:
+//! ## Formal Definition
 //!
-//!   - map of: Allocation -> lattice value  (top > Vn symbols (unordered) > bottom)
+//! The analysis lattice is:
+//!
+//!                      Top (V)
+//!                         |
+//!                        𝒫(V)   // the Powerset of the set of virtual regs
+//!                         |
+//!                 Bottom ( ∅ )     // the empty set
+//!
+//! and the lattice ordering relation is the subset relation: S ≤ U
+//! iff S ⊆ U. The lattice meet-function is intersection.
+//!
+//! The dataflow analysis state at each program point (each point
+//! before or after an instruction) is:
+//!
+//!   - map of: Allocation -> lattice value
 //!
 //! And the transfer functions for instructions are (where `A` is the
-//! above map from allocated physical registers to symbolic values):
+//! above map from allocated physical registers to lattice values):
 //!
 //!   - `Edit::Move` inserted by RA:       [ alloc_d := alloc_s ]
 //!
-//!       A[alloc_d] := A[alloc_s]
+//!       A' = A[alloc_d → A[alloc_s]]
-//!
-//!   - phi-node          [ V_i := phi block_j:V_j, block_k:V_k, ... ]
-//!     with allocations  [ A_i := phi block_j:A_j, block_k:A_k, ... ]
-//!     (N.B.: phi-nodes are not semantically present in the final
-//!      machine code, but we include their allocations so that this
-//!      checker can work)
-//!
-//!       A[A_i] := meet(A[A_j], A[A_k], ...)
 //!
 //!   - statement in pre-regalloc function [ V_i := op V_j, V_k, ... ]
 //!     with allocated form                [ A_i := op A_j, A_k, ... ]
 //!
-//!       A[A_i] := `V_i`
+//!       A' = { A_k → A[A_k] \ { V_i } for k ≠ i } ∪
+//!            { A_i -> { V_i } }
 //!
 //!     In other words, a statement, even after allocation, generates
 //!     a symbol that corresponds to its original virtual-register
-//!     def.
+//!     def. Simultaneously, that same virtual register symbol is removed
+//!     from all other allocs: they no longer carry the current value.
 //!
-//!     (N.B.: moves in pre-regalloc function fall into this last case
+//!   - Parallel moves or blockparam-assignments in original program
-//!     -- they are "just another operation" and generate a new
+//!                                       [ V_d1 := V_s1, V_d2 := V_s2, ... ]
-//!     symbol)
 //!
-//! At control-flow join points, the symbols meet using a very simple
+//!       A' = { A_k → subst(A[A_k]) for all k }
-//! lattice meet-function: two different symbols in the same
+//!            where subst(S) removes symbols for overwritten virtual
-//! allocation meet to "conflicted"; otherwise, the symbol meets with
+//!            registers (V_d1 .. V_dn) and then adds V_di whenever
-//! itself to produce itself (reflexivity).
+//!            V_si appeared prior to the removals.
 //!
 //! To check correctness, we first find the dataflow fixpoint with the
 //! above lattice and transfer/meet functions. Then, at each op, we
@@ -80,8 +98,9 @@ use crate::{
     Allocation, AllocationKind, Block, Edit, Function, Inst, InstOrEdit, InstPosition, Operand,
     OperandConstraint, OperandKind, OperandPos, Output, PReg, RegClass, VReg,
 };
-
+use fxhash::{FxHashMap, FxHashSet};
-use std::collections::{HashMap, HashSet, VecDeque};
+use smallvec::{smallvec, SmallVec};
+use std::collections::VecDeque;
 use std::default::Default;
 use std::hash::Hash;
 use std::result::Result;
@@ -109,11 +128,11 @@ pub enum CheckerError {
         op: Operand,
         alloc: Allocation,
     },
-    IncorrectValueInAllocation {
+    IncorrectValuesInAllocation {
         inst: Inst,
         op: Operand,
         alloc: Allocation,
-        actual: VReg,
+        actual: FxHashSet<VReg>,
     },
     ConstraintViolated {
         inst: Inst,
@@ -145,55 +164,78 @@ pub enum CheckerError {
         inst: Inst,
         alloc: Allocation,
     },
-    NonRefValueInStackmap {
+    NonRefValuesInStackmap {
         inst: Inst,
         alloc: Allocation,
-        vreg: VReg,
+        vregs: FxHashSet<VReg>,
     },
 }
 
 /// Abstract state for an allocation.
 ///
-/// Forms a lattice with \top (`Unknown`), \bot (`Conflicted`), and a
+/// Equivalent to a set of virtual register names, with the
-/// number of mutually unordered value-points in between, one per real
+/// universe-set as top and empty set as bottom lattice element. The
-/// or virtual register. Any two different registers meet to \bot.
+/// meet-function is thus set intersection.
-#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+#[derive(Clone, Debug, PartialEq, Eq)]
-enum CheckerValue {
+struct CheckerValue {
-    /// "top" value: this storage slot has no known value.
+    /// This value is the "universe set".
-    Unknown,
+    universe: bool,
-    /// "bottom" value: this storage slot has a conflicted value.
+    /// The VRegs that this value is equal to.
-    Conflicted,
+    vregs: FxHashSet<VReg>,
-    /// Reg: this storage slot has a value that originated as a def
-    /// into the given virtual register.
-    ///
-    /// The boolean flag indicates whether the value is
-    /// reference-typed.
-    Reg(VReg, bool),
 }
 
 impl Default for CheckerValue {
     fn default() -> CheckerValue {
-        CheckerValue::Unknown
+        CheckerValue {
+            universe: true,
+            vregs: FxHashSet::default(),
+        }
     }
 }
 
 impl CheckerValue {
-    /// Meet function of the abstract-interpretation value lattice.
+    /// Meet function of the abstract-interpretation value
-    fn meet(&self, other: &CheckerValue) -> CheckerValue {
+    /// lattice. Returns a boolean value indicating whether `self` was
-        match (self, other) {
+    /// changed.
-            (&CheckerValue::Unknown, _) => *other,
+    fn meet_with(&mut self, other: &CheckerValue) -> bool {
-            (_, &CheckerValue::Unknown) => *self,
+        if self.universe {
-            (&CheckerValue::Conflicted, _) => *self,
+            *self = other.clone();
-            (_, &CheckerValue::Conflicted) => *other,
+            true
-            (&CheckerValue::Reg(r1, ref1), &CheckerValue::Reg(r2, ref2))
+        } else if other.universe {
-                if r1 == r2 && ref1 == ref2 =>
+            false
-            {
+        } else {
-                CheckerValue::Reg(r1, ref1)
+            let mut remove_keys: SmallVec<[VReg; 4]> = smallvec![];
+            for vreg in &self.vregs {
+                if !other.vregs.contains(vreg) {
+                    // Not present in other; this is intersection, so
+                    // remove.
+                    remove_keys.push(vreg.clone());
                 }
-            _ => {
-                trace!("{:?} and {:?} meet to Conflicted", self, other);
-                CheckerValue::Conflicted
             }
+
+            for key in &remove_keys {
+                self.vregs.remove(key);
+            }
+
+            !remove_keys.is_empty()
+        }
+    }
+
+    fn from_reg(reg: VReg) -> CheckerValue {
+        CheckerValue {
+            universe: false,
+            vregs: std::iter::once(reg).collect(),
+        }
+    }
+
+    fn remove_vreg(&mut self, reg: VReg) {
+        self.vregs.remove(&reg);
+    }
+
+    fn empty() -> CheckerValue {
+        CheckerValue {
+            universe: false,
+            vregs: FxHashSet::default(),
         }
     }
 }
@@ -201,39 +243,60 @@ impl CheckerValue {
 /// State that steps through program points as we scan over the instruction stream.
 #[derive(Clone, Debug, PartialEq, Eq)]
 struct CheckerState {
-    allocations: HashMap<Allocation, CheckerValue>,
+    top: bool,
+    allocations: FxHashMap<Allocation, CheckerValue>,
 }
 
 impl Default for CheckerState {
     fn default() -> CheckerState {
         CheckerState {
-            allocations: HashMap::new(),
+            top: true,
+            allocations: FxHashMap::default(),
         }
     }
 }
 
 impl std::fmt::Display for CheckerValue {
     fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
-        match self {
+        if self.universe {
-            CheckerValue::Unknown => write!(f, "?"),
+            write!(f, "top")
-            CheckerValue::Conflicted => write!(f, "!"),
+        } else {
-            CheckerValue::Reg(r, false) => write!(f, "{}", r),
+            write!(f, "{{ ")?;
-            CheckerValue::Reg(r, true) => write!(f, "{}/ref", r),
+            for vreg in &self.vregs {
+                write!(f, "{} ", vreg)?;
+            }
+            write!(f, "}}")?;
+            Ok(())
         }
     }
 }
 
+/// Meet function for analysis value: meet individual values at
+/// matching allocations, and intersect keys (remove key-value pairs
+/// only on one side). Returns boolean flag indicating whether `into`
+/// changed.
 fn merge_map<K: Copy + Clone + PartialEq + Eq + Hash>(
-    into: &mut HashMap<K, CheckerValue>,
+    into: &mut FxHashMap<K, CheckerValue>,
-    from: &HashMap<K, CheckerValue>,
+    from: &FxHashMap<K, CheckerValue>,
-) {
+) -> bool {
-    for (k, v) in from {
+    let mut changed = false;
-        let into_v = into.entry(*k).or_insert(Default::default());
+    let mut remove_keys: SmallVec<[K; 4]> = smallvec![];
-        let merged = into_v.meet(v);
+    for (k, into_v) in into.iter_mut() {
-        *into_v = merged;
+        if let Some(from_v) = from.get(k) {
+            changed |= into_v.meet_with(from_v);
+        } else {
+            remove_keys.push(k.clone());
         }
     }
 
+    for remove_key in &remove_keys {
+        into.remove(remove_key);
+    }
+    changed |= !remove_keys.is_empty();
+
+    changed
+}
+
 impl CheckerState {
     /// Create a new checker state.
     fn new() -> CheckerState {
@@ -241,8 +304,16 @@ impl CheckerState {
     }
 
     /// Merge this checker state with another at a CFG join-point.
-    fn meet_with(&mut self, other: &CheckerState) {
+    fn meet_with(&mut self, other: &CheckerState) -> bool {
-        merge_map(&mut self.allocations, &other.allocations);
+        if self.top {
+            *self = other.clone();
+            !self.top
+        } else if other.top {
+            false
+        } else {
+            self.top = false;
+            merge_map(&mut self.allocations, &other.allocations)
+        }
     }
 
     fn check_val(
@@ -250,30 +321,25 @@ impl CheckerState {
         inst: Inst,
         op: Operand,
         alloc: Allocation,
-        val: CheckerValue,
+        val: &CheckerValue,
         allocs: &[Allocation],
     ) -> Result<(), CheckerError> {
         if alloc == Allocation::none() {
             return Err(CheckerError::MissingAllocation { inst, op });
         }
 
-        match val {
+        if val.universe {
-            CheckerValue::Unknown => {
             return Err(CheckerError::UnknownValueInAllocation { inst, op, alloc });
         }
-            CheckerValue::Conflicted => {
+
-                return Err(CheckerError::ConflictedValueInAllocation { inst, op, alloc });
+        if !val.vregs.contains(&op.vreg()) {
-            }
+            return Err(CheckerError::IncorrectValuesInAllocation {
-            CheckerValue::Reg(r, _) if r != op.vreg() => {
-                return Err(CheckerError::IncorrectValueInAllocation {
                 inst,
                 op,
                 alloc,
-                    actual: r,
+                actual: val.vregs.clone(),
             });
         }
-            _ => {}
-        }
 
         self.check_constraint(inst, op, alloc, allocs)?;
 
@@ -283,7 +349,13 @@ impl CheckerState {
     /// Check an instruction against this state. This must be called
     /// twice: once with `InstPosition::Before`, and once with
     /// `InstPosition::After` (after updating state with defs).
-    fn check(&self, pos: InstPosition, checkinst: &CheckerInst) -> Result<(), CheckerError> {
+    fn check<'a, F: Function>(
+        &self,
+        pos: InstPosition,
+        checkinst: &CheckerInst,
+        checker: &Checker<'a, F>,
+    ) -> Result<(), CheckerError> {
+        let default_val = Default::default();
         match checkinst {
             &CheckerInst::Op {
                 inst,
@@ -317,11 +389,7 @@ impl CheckerState {
                         continue;
                     }
 
-                    let val = self
+                    let val = self.allocations.get(alloc).unwrap_or(&default_val);
-                        .allocations
-                        .get(alloc)
-                        .cloned()
-                        .unwrap_or(Default::default());
                     trace!(
                         "checker: checkinst {:?}: op {:?}, alloc {:?}, checker value {:?}",
                         checkinst,
@@ -334,11 +402,7 @@ impl CheckerState {
             }
             &CheckerInst::Safepoint { inst, ref allocs } => {
                 for &alloc in allocs {
-                    let val = self
+                    let val = self.allocations.get(&alloc).unwrap_or(&default_val);
-                        .allocations
-                        .get(&alloc)
-                        .cloned()
-                        .unwrap_or(Default::default());
                     trace!(
                         "checker: checkinst {:?}: safepoint slot {}, checker value {:?}",
                         checkinst,
@@ -346,32 +410,35 @@ impl CheckerState {
                         val
                     );
 
-                    match val {
+                    let reffy = val
-                        CheckerValue::Unknown => {}
+                        .vregs
-                        CheckerValue::Conflicted => {
+                        .iter()
-                            return Err(CheckerError::ConflictedValueInStackmap { inst, alloc });
+                        .any(|vreg| checker.reftyped_vregs.contains(vreg));
-                        }
+                    if !reffy {
-                        CheckerValue::Reg(vreg, false) => {
+                        return Err(CheckerError::NonRefValuesInStackmap {
-                            return Err(CheckerError::NonRefValueInStackmap { inst, alloc, vreg });
+                            inst,
-                        }
+                            alloc,
-                        CheckerValue::Reg(_, true) => {}
+                            vregs: val.vregs.clone(),
+                        });
                     }
                 }
             }
-            _ => {}
+            &CheckerInst::ParallelMove { .. } | &CheckerInst::Move { .. } => {
+                // This doesn't need verification; we just update
+                // according to the move semantics in the step
+                // function below.
+            }
         }
         Ok(())
     }
 
     /// Update according to instruction.
     fn update<'a, F: Function>(&mut self, checkinst: &CheckerInst, checker: &Checker<'a, F>) {
+        self.top = false;
+        let default_val = Default::default();
         match checkinst {
             &CheckerInst::Move { into, from } => {
-                let val = self
+                let val = self.allocations.get(&from).unwrap_or(&default_val).clone();
-                    .allocations
-                    .get(&from)
-                    .cloned()
-                    .unwrap_or(Default::default());
                 trace!(
                     "checker: checkinst {:?} updating: move {:?} -> {:?} val {:?}",
                     checkinst,
@@ -381,35 +448,83 @@ impl CheckerState {
                 );
                 self.allocations.insert(into, val);
             }
+            &CheckerInst::ParallelMove { ref into, ref from } => {
+                // First, build map of actions for each vreg in an
+                // alloc. If an alloc has a reg V_i before a parallel
+                // move, then for each use of V_i as a source (V_i ->
+                // V_j), we might add a new V_j wherever V_i appears;
+                // and if V_i is used as a dest (at most once), then
+                // it must be removed first from allocs' vreg sets.
+                let mut additions: FxHashMap<VReg, SmallVec<[VReg; 2]>> = FxHashMap::default();
+                let mut deletions: FxHashSet<VReg> = FxHashSet::default();
+
+                for (&dest, &src) in into.iter().zip(from.iter()) {
+                    deletions.insert(dest);
+                    additions
+                        .entry(src)
+                        .or_insert_with(|| smallvec![])
+                        .push(dest);
+                }
+
+                // Now process each allocation's set of vreg labels,
+                // first deleting those labels that were updated by
+                // this parallel move, then adding back labels
+                // redefined by the move.
+                for value in self.allocations.values_mut() {
+                    if value.universe {
+                        continue;
+                    }
+                    let mut insertions: SmallVec<[VReg; 2]> = smallvec![];
+                    for &vreg in &value.vregs {
+                        if let Some(additions) = additions.get(&vreg) {
+                            insertions.extend(additions.iter().cloned());
+                        }
+                    }
+                    for &d in &deletions {
+                        value.vregs.remove(&d);
+                    }
+                    value.vregs.extend(insertions);
+                }
+            }
             &CheckerInst::Op {
                 ref operands,
                 ref allocs,
                 ref clobbers,
                 ..
             } => {
+                // For each def, (i) update alloc to reflect defined
+                // vreg (and only that vreg), and (ii) update all
+                // other allocs in the checker state by removing this
+                // vreg, if defined (other defs are now stale).
                 for (op, alloc) in operands.iter().zip(allocs.iter()) {
                     if op.kind() != OperandKind::Def {
                         continue;
                     }
-                    let reftyped = checker.reftyped_vregs.contains(&op.vreg());
                     self.allocations
-                        .insert(*alloc, CheckerValue::Reg(op.vreg(), reftyped));
+                        .insert(*alloc, CheckerValue::from_reg(op.vreg()));
+                    for (other_alloc, other_value) in &mut self.allocations {
+                        if *alloc != *other_alloc {
+                            other_value.remove_vreg(op.vreg());
+                        }
+                    }
                 }
                 for clobber in clobbers {
                     self.allocations.remove(&Allocation::reg(*clobber));
                 }
             }
-            &CheckerInst::DefAlloc { alloc, vreg } => {
-                let reftyped = checker.reftyped_vregs.contains(&vreg);
-                self.allocations
-                    .insert(alloc, CheckerValue::Reg(vreg, reftyped));
-            }
             &CheckerInst::Safepoint { ref allocs, .. } => {
                 for (alloc, value) in &mut self.allocations {
-                    if let CheckerValue::Reg(_, true) = *value {
+                    if alloc.is_reg() {
-                        if !allocs.contains(&alloc) {
+                        continue;
-                            *value = CheckerValue::Conflicted;
                     }
+                    if !allocs.contains(&alloc) {
+                        // Remove all reftyped vregs as labels.
+                        let new_vregs = value
+                            .vregs
+                            .difference(&checker.reftyped_vregs)
+                            .cloned()
+                            .collect();
+                        value.vregs = new_vregs;
                     }
                 }
             }
@@ -475,6 +590,12 @@ pub(crate) enum CheckerInst {
     /// spillslots).
     Move { into: Allocation, from: Allocation },
 
+    /// A parallel move in the original program. Simultaneously moves
+    /// from all source vregs to all corresponding dest vregs,
+    /// permitting overlap in the src and dest sets and doing all
+    /// reads before any writes.
+    ParallelMove { into: Vec<VReg>, from: Vec<VReg> },
+
     /// A regular instruction with fixed use and def slots. Contains
     /// both the original operands (as given to the regalloc) and the
     /// allocation results.
@@ -485,11 +606,6 @@ pub(crate) enum CheckerInst {
         clobbers: Vec<PReg>,
     },
 
-    /// Define an allocation's contents. Like BlockParams but for one
-    /// allocation. Used sometimes when moves are elided but ownership
-    /// of a value is logically transferred to a new vreg.
-    DefAlloc { alloc: Allocation, vreg: VReg },
-
     /// A safepoint, with the given Allocations specified as containing
     /// reftyped values. All other reftyped values become invalid.
     Safepoint { inst: Inst, allocs: Vec<Allocation> },
@@ -498,9 +614,10 @@ pub(crate) enum CheckerInst {
 #[derive(Debug)]
 pub struct Checker<'a, F: Function> {
     f: &'a F,
-    bb_in: HashMap<Block, CheckerState>,
+    bb_in: FxHashMap<Block, CheckerState>,
-    bb_insts: HashMap<Block, Vec<CheckerInst>>,
+    bb_insts: FxHashMap<Block, Vec<CheckerInst>>,
-    reftyped_vregs: HashSet<VReg>,
+    edge_insts: FxHashMap<(Block, Block), Vec<CheckerInst>>,
+    reftyped_vregs: FxHashSet<VReg>,
 }
 
 impl<'a, F: Function> Checker<'a, F> {
@@ -509,14 +626,18 @@ impl<'a, F: Function> Checker<'a, F> {
     /// methods to add abstract instructions to each BB before
     /// invoking `run()` to check for errors.
     pub fn new(f: &'a F) -> Checker<'a, F> {
-        let mut bb_in = HashMap::new();
+        let mut bb_in = FxHashMap::default();
-        let mut bb_insts = HashMap::new();
+        let mut bb_insts = FxHashMap::default();
-        let mut reftyped_vregs = HashSet::new();
+        let mut edge_insts = FxHashMap::default();
+        let mut reftyped_vregs = FxHashSet::default();
 
         for block in 0..f.num_blocks() {
             let block = Block::new(block);
             bb_in.insert(block, Default::default());
             bb_insts.insert(block, vec![]);
+            for &succ in f.block_succs(block) {
+                edge_insts.insert((block, succ), vec![]);
+            }
         }
 
         for &vreg in f.reftype_vregs() {
@@ -527,6 +648,7 @@ impl<'a, F: Function> Checker<'a, F> {
             f,
             bb_in,
             bb_insts,
+            edge_insts,
             reftyped_vregs,
         }
     }
@@ -536,7 +658,7 @@ impl<'a, F: Function> Checker<'a, F> {
     pub fn prepare(&mut self, out: &Output) {
         trace!("checker: out = {:?}", out);
         // Preprocess safepoint stack-maps into per-inst vecs.
-        let mut safepoint_slots: HashMap<Inst, Vec<Allocation>> = HashMap::new();
+        let mut safepoint_slots: FxHashMap<Inst, Vec<Allocation>> = FxHashMap::default();
         for &(progpoint, slot) in &out.safepoint_slots {
             safepoint_slots
                 .entry(progpoint.inst())
@@ -565,7 +687,7 @@ impl<'a, F: Function> Checker<'a, F> {
         &mut self,
         block: Block,
         inst: Inst,
-        safepoint_slots: &mut HashMap<Inst, Vec<Allocation>>,
+        safepoint_slots: &mut FxHashMap<Inst, Vec<Allocation>>,
         out: &Output,
     ) {
         // If this is a safepoint, then check the spillslots at this point.
@@ -576,10 +698,9 @@ impl<'a, F: Function> Checker<'a, F> {
             self.bb_insts.get_mut(&block).unwrap().push(checkinst);
         }
 
-        // Skip if this is a branch: the blockparams do not
+        // Skip normal checks if this is a branch: the blockparams do
-        // exist in post-regalloc code, and the edge-moves
+        // not exist in post-regalloc code, and the edge-moves have to
-        // have to be inserted before the branch rather than
+        // be inserted before the branch rather than after.
-        // after.
         if !self.f.is_branch(inst) {
             // Instruction itself.
             let operands: Vec<_> = self.f.inst_operands(inst).iter().cloned().collect();
@@ -594,6 +715,23 @@ impl<'a, F: Function> Checker<'a, F> {
             trace!("checker: adding inst {:?}", checkinst);
             self.bb_insts.get_mut(&block).unwrap().push(checkinst);
         }
+        // Instead, if this is a branch, emit a ParallelMove on each
+        // outgoing edge as necessary to handle blockparams.
+        else {
+            for (i, &succ) in self.f.block_succs(block).iter().enumerate() {
+                let args = self.f.branch_blockparams(block, inst, i);
+                let params = self.f.block_params(succ);
+                assert_eq!(args.len(), params.len());
+                if args.len() > 0 {
+                    self.edge_insts.get_mut(&(block, succ)).unwrap().push(
+                        CheckerInst::ParallelMove {
+                            into: params.iter().cloned().collect(),
+                            from: args.iter().cloned().collect(),
+                        },
+                    );
+                }
+            }
+        }
     }
 
     fn handle_edit(&mut self, block: Block, edit: &Edit) {
@@ -605,19 +743,14 @@ impl<'a, F: Function> Checker<'a, F> {
                     .unwrap()
                     .push(CheckerInst::Move { into: to, from });
             }
-            &Edit::DefAlloc { alloc, vreg } => {
+            _ => {}
-                self.bb_insts
-                    .get_mut(&block)
-                    .unwrap()
-                    .push(CheckerInst::DefAlloc { alloc, vreg });
-            }
         }
     }
 
     /// Perform the dataflow analysis to compute checker state at each BB entry.
     fn analyze(&mut self) {
         let mut queue = VecDeque::new();
-        let mut queue_set = HashSet::new();
+        let mut queue_set = FxHashSet::default();
         for block in 0..self.f.num_blocks() {
             let block = Block::new(block);
             queue.push_back(block);
@@ -635,10 +768,29 @@ impl<'a, F: Function> Checker<'a, F> {
             }
 
             for &succ in self.f.block_succs(block) {
-                let cur_succ_in = self.bb_in.get(&succ).unwrap();
                 let mut new_state = state.clone();
+                for edge_inst in self.edge_insts.get(&(block, succ)).unwrap() {
+                    new_state.update(edge_inst, self);
+                    trace!(
+                        "analyze: succ {:?}: inst {:?} -> state {:?}",
+                        succ,
+                        edge_inst,
+                        new_state
+                    );
+                }
+
+                let cur_succ_in = self.bb_in.get(&succ).unwrap();
+                trace!(
+                    "meeting state {:?} for block {} with state {:?} for block {}",
+                    new_state,
+                    block.index(),
+                    cur_succ_in,
+                    succ.index()
+                );
                 new_state.meet_with(cur_succ_in);
                 let changed = &new_state != cur_succ_in;
+                trace!(" -> {:?}, changed {}", new_state, changed);
+
                 if changed {
                     trace!(
                         "analyze: block {} state changed from {:?} to {:?}; pushing onto queue",
@@ -664,12 +816,12 @@ impl<'a, F: Function> Checker<'a, F> {
         for (block, input) in &self.bb_in {
             let mut state = input.clone();
             for inst in self.bb_insts.get(block).unwrap() {
-                if let Err(e) = state.check(InstPosition::Before, inst) {
+                if let Err(e) = state.check(InstPosition::Before, inst, self) {
                     trace!("Checker error: {:?}", e);
                     errors.push(e);
                 }
                 state.update(inst, self);
-                if let Err(e) = state.check(InstPosition::After, inst) {
+                if let Err(e) = state.check(InstPosition::After, inst, self) {
                     trace!("Checker error: {:?}", e);
                     errors.push(e);
                 }
@@ -725,9 +877,6 @@ impl<'a, F: Function> Checker<'a, F> {
                     &CheckerInst::Move { from, into } => {
                         trace!("    {} -> {}", from, into);
                     }
-                    &CheckerInst::DefAlloc { alloc, vreg } => {
-                        trace!("    defalloc: {}:{}", vreg, alloc);
-                    }
                     &CheckerInst::Safepoint { ref allocs, .. } => {
                         let mut slotargs = vec![];
                         for &slot in allocs {
@@ -735,10 +884,28 @@ impl<'a, F: Function> Checker<'a, F> {
                         }
                         trace!("    safepoint: {}", slotargs.join(", "));
                     }
+                    &CheckerInst::ParallelMove { .. } => {
+                        panic!("unexpected parallel_move in body (non-edge)")
+                    }
                 }
                 state.update(inst, &self);
                 print_state(&state);
             }
+
+            for &succ in self.f.block_succs(bb) {
+                trace!("  succ {:?}:", succ);
+                let mut state = state.clone();
+                for edge_inst in self.edge_insts.get(&(bb, succ)).unwrap() {
+                    match edge_inst {
+                        &CheckerInst::ParallelMove { ref from, ref into } => {
+                            trace!("    parallel_move {:?} -> {:?}", from, into);
+                        }
+                        _ => panic!("unexpected edge_inst: not a parallel move"),
+                    }
+                    state.update(edge_inst, &self);
+                    print_state(&state);
+                }
+            }
         }
 
         result