diff --git a/src/checker.rs b/src/checker.rs index 323c66b..82915e7 100644 --- a/src/checker.rs +++ b/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 -//! `Conflicts` even in cases where one *could* statically prove that -//! it contains a certain register, because the analysis is not +//! register (modulo any analysis bugs); but it may describe fewer +//! virtual registers even in cases where one *could* statically prove +//! 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] -//! -//! - 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], ...) +//! A' = A[alloc_d → A[alloc_s]] //! //! - 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 -//! -- they are "just another operation" and generate a new -//! symbol) +//! - Parallel moves or blockparam-assignments in original program +//! [ V_d1 := V_s1, V_d2 := V_s2, ... ] //! -//! At control-flow join points, the symbols meet using a very simple -//! lattice meet-function: two different symbols in the same -//! allocation meet to "conflicted"; otherwise, the symbol meets with -//! itself to produce itself (reflexivity). +//! A' = { A_k → subst(A[A_k]) for all k } +//! where subst(S) removes symbols for overwritten virtual +//! registers (V_d1 .. V_dn) and then adds V_di whenever +//! 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 std::collections::{HashMap, HashSet, VecDeque}; +use fxhash::{FxHashMap, FxHashSet}; +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, }, ConstraintViolated { inst: Inst, @@ -145,55 +164,78 @@ pub enum CheckerError { inst: Inst, alloc: Allocation, }, - NonRefValueInStackmap { + NonRefValuesInStackmap { inst: Inst, alloc: Allocation, - vreg: VReg, + vregs: FxHashSet, }, } /// Abstract state for an allocation. /// -/// Forms a lattice with \top (`Unknown`), \bot (`Conflicted`), and a -/// number of mutually unordered value-points in between, one per real -/// or virtual register. Any two different registers meet to \bot. -#[derive(Clone, Copy, Debug, PartialEq, Eq)] -enum CheckerValue { - /// "top" value: this storage slot has no known value. - Unknown, - /// "bottom" value: this storage slot has a conflicted value. - Conflicted, - /// 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), +/// Equivalent to a set of virtual register names, with the +/// universe-set as top and empty set as bottom lattice element. The +/// meet-function is thus set intersection. +#[derive(Clone, Debug, PartialEq, Eq)] +struct CheckerValue { + /// This value is the "universe set". + universe: bool, + /// The VRegs that this value is equal to. + vregs: FxHashSet, } 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. - fn meet(&self, other: &CheckerValue) -> CheckerValue { - match (self, other) { - (&CheckerValue::Unknown, _) => *other, - (_, &CheckerValue::Unknown) => *self, - (&CheckerValue::Conflicted, _) => *self, - (_, &CheckerValue::Conflicted) => *other, - (&CheckerValue::Reg(r1, ref1), &CheckerValue::Reg(r2, ref2)) - if r1 == r2 && ref1 == ref2 => - { - CheckerValue::Reg(r1, ref1) + /// Meet function of the abstract-interpretation value + /// lattice. Returns a boolean value indicating whether `self` was + /// changed. + fn meet_with(&mut self, other: &CheckerValue) -> bool { + if self.universe { + *self = other.clone(); + true + } else if other.universe { + false + } else { + 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(®); + } + + fn empty() -> CheckerValue { + CheckerValue { + universe: false, + vregs: FxHashSet::default(), } } } @@ -201,37 +243,58 @@ impl CheckerValue { /// State that steps through program points as we scan over the instruction stream. #[derive(Clone, Debug, PartialEq, Eq)] struct CheckerState { - allocations: HashMap, + top: bool, + allocations: FxHashMap, } 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 { - CheckerValue::Unknown => write!(f, "?"), - CheckerValue::Conflicted => write!(f, "!"), - CheckerValue::Reg(r, false) => write!(f, "{}", r), - CheckerValue::Reg(r, true) => write!(f, "{}/ref", r), + if self.universe { + write!(f, "top") + } else { + write!(f, "{{ ")?; + 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( - into: &mut HashMap, - from: &HashMap, -) { - for (k, v) in from { - let into_v = into.entry(*k).or_insert(Default::default()); - let merged = into_v.meet(v); - *into_v = merged; + into: &mut FxHashMap, + from: &FxHashMap, +) -> bool { + let mut changed = false; + let mut remove_keys: SmallVec<[K; 4]> = smallvec![]; + for (k, into_v) in into.iter_mut() { + 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 { @@ -241,8 +304,16 @@ impl CheckerState { } /// Merge this checker state with another at a CFG join-point. - fn meet_with(&mut self, other: &CheckerState) { - merge_map(&mut self.allocations, &other.allocations); + fn meet_with(&mut self, other: &CheckerState) -> bool { + 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,29 +321,24 @@ 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 { - CheckerValue::Unknown => { - return Err(CheckerError::UnknownValueInAllocation { inst, op, alloc }); - } - CheckerValue::Conflicted => { - return Err(CheckerError::ConflictedValueInAllocation { inst, op, alloc }); - } - CheckerValue::Reg(r, _) if r != op.vreg() => { - return Err(CheckerError::IncorrectValueInAllocation { - inst, - op, - alloc, - actual: r, - }); - } - _ => {} + if val.universe { + return Err(CheckerError::UnknownValueInAllocation { inst, op, alloc }); + } + + if !val.vregs.contains(&op.vreg()) { + return Err(CheckerError::IncorrectValuesInAllocation { + inst, + op, + alloc, + 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 - .allocations - .get(alloc) - .cloned() - .unwrap_or(Default::default()); + let val = self.allocations.get(alloc).unwrap_or(&default_val); 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 - .allocations - .get(&alloc) - .cloned() - .unwrap_or(Default::default()); + let val = self.allocations.get(&alloc).unwrap_or(&default_val); trace!( "checker: checkinst {:?}: safepoint slot {}, checker value {:?}", checkinst, @@ -346,32 +410,35 @@ impl CheckerState { val ); - match val { - CheckerValue::Unknown => {} - CheckerValue::Conflicted => { - return Err(CheckerError::ConflictedValueInStackmap { inst, alloc }); - } - CheckerValue::Reg(vreg, false) => { - return Err(CheckerError::NonRefValueInStackmap { inst, alloc, vreg }); - } - CheckerValue::Reg(_, true) => {} + let reffy = val + .vregs + .iter() + .any(|vreg| checker.reftyped_vregs.contains(vreg)); + if !reffy { + return Err(CheckerError::NonRefValuesInStackmap { + inst, + alloc, + 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 - .allocations - .get(&from) - .cloned() - .unwrap_or(Default::default()); + let val = self.allocations.get(&from).unwrap_or(&default_val).clone(); 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> = FxHashMap::default(); + let mut deletions: FxHashSet = 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 !allocs.contains(&alloc) { - *value = CheckerValue::Conflicted; - } + if alloc.is_reg() { + continue; + } + 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, from: Vec }, + /// 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, }, - /// 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 }, @@ -498,9 +614,10 @@ pub(crate) enum CheckerInst { #[derive(Debug)] pub struct Checker<'a, F: Function> { f: &'a F, - bb_in: HashMap, - bb_insts: HashMap>, - reftyped_vregs: HashSet, + bb_in: FxHashMap, + bb_insts: FxHashMap>, + edge_insts: FxHashMap<(Block, Block), Vec>, + reftyped_vregs: FxHashSet, } 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_insts = HashMap::new(); - let mut reftyped_vregs = HashSet::new(); + let mut bb_in = FxHashMap::default(); + let mut bb_insts = FxHashMap::default(); + 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> = HashMap::new(); + let mut safepoint_slots: FxHashMap> = 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>, + safepoint_slots: &mut FxHashMap>, 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 - // exist in post-regalloc code, and the edge-moves - // have to be inserted before the branch rather than - // after. + // Skip normal checks if this is a branch: the blockparams do + // not exist in post-regalloc code, and the edge-moves have to + // be inserted before the branch rather than 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