CSSA verifier.

During register allocation, the code must be kept in conventional SSA
form. Add a verifier that checks this property.

lib/cretonne/src/regalloc/context.rs

@@ -17,7 +17,7 @@ use regalloc::spilling::Spilling;
 use regalloc::virtregs::VirtRegs;
 use result::CtonResult;
 use topo_order::TopoOrder;
-use verifier::{verify_context, verify_liveness};
+use verifier::{verify_context, verify_liveness, verify_cssa};
 
 /// Persistent memory allocations for register allocation.
 pub struct Context {
@@ -85,6 +85,7 @@ impl Context {
         if isa.flags().enable_verifier() {
             verify_context(func, cfg, domtree, Some(isa))?;
             verify_liveness(isa, func, cfg, &self.liveness)?;
+            verify_cssa(func, cfg, domtree, &self.liveness, &self.virtregs)?;
         }
 
 
@@ -101,6 +102,7 @@ impl Context {
         if isa.flags().enable_verifier() {
             verify_context(func, cfg, domtree, Some(isa))?;
             verify_liveness(isa, func, cfg, &self.liveness)?;
+            verify_cssa(func, cfg, domtree, &self.liveness, &self.virtregs)?;
         }
 
         // Pass: Reload.
@@ -115,6 +117,7 @@ impl Context {
         if isa.flags().enable_verifier() {
             verify_context(func, cfg, domtree, Some(isa))?;
             verify_liveness(isa, func, cfg, &self.liveness)?;
+            verify_cssa(func, cfg, domtree, &self.liveness, &self.virtregs)?;
         }
 
         // Pass: Coloring.
@@ -124,6 +127,7 @@ impl Context {
         if isa.flags().enable_verifier() {
             verify_context(func, cfg, domtree, Some(isa))?;
             verify_liveness(isa, func, cfg, &self.liveness)?;
+            verify_cssa(func, cfg, domtree, &self.liveness, &self.virtregs)?;
         }
         Ok(())
     }

lib/cretonne/src/regalloc/mod.rs

@@ -7,6 +7,7 @@ pub mod liveness;
 pub mod allocatable_set;
 pub mod live_value_tracker;
 pub mod coloring;
+pub mod virtregs;
 
 mod affinity;
 mod coalescing;
@@ -16,7 +17,6 @@ mod pressure;
 mod reload;
 mod solver;
 mod spilling;
-mod virtregs;
 
 pub use self::allocatable_set::AllocatableSet;
 pub use self::context::Context;

lib/cretonne/src/regalloc/virtregs.rs

@@ -12,11 +12,12 @@
 //! memory-to-memory copies when a spilled value is passed as an EBB argument.
 
 use entity_list::{EntityList, ListPool};
-use entity_map::{EntityMap, PrimaryEntityData};
+use entity_map::{EntityMap, PrimaryEntityData, Keys};
 use ir::Value;
 use packed_option::PackedOption;
 use ref_slice::ref_slice;
 
+/// A virtual register reference.
 #[derive(Copy, Clone, PartialEq, Eq, Hash, Debug, PartialOrd, Ord)]
 pub struct VirtReg(u32);
 entity_impl!(VirtReg, "vreg");
@@ -71,6 +72,11 @@ impl VirtRegs {
         self.vregs[vreg].as_slice(&self.pool)
     }
 
+    /// Get an iterator over all virtual registers.
+    pub fn all_virtregs(&self) -> Keys<VirtReg> {
+        self.vregs.keys()
+    }
+
     /// Get the congruence class of `value`.
     ///
     /// If `value` belongs to a virtual register, the congruence class is the values of the virtual

lib/cretonne/src/verifier/cssa.rs

@@ -0,0 +1,122 @@
+//! Verify conventional SSA form.
+
+use dominator_tree::DominatorTree;
+use flowgraph::ControlFlowGraph;
+use ir::Function;
+use regalloc::liveness::Liveness;
+use regalloc::virtregs::VirtRegs;
+use std::cmp::Ordering;
+use verifier::Result;
+
+/// Verify conventional SSA form for `func`.
+///
+/// Conventional SSA form is represented in Cretonne with the help of virtual registers:
+///
+/// - Two values are said to be *PHI-related* if one is an EBB argument and the other is passed as
+///   a branch argument in a location that matches the first value.
+/// - PHI-related values must belong to the same virtual register.
+/// - Two values in the same virtual register must not have overlapping live ranges.
+///
+/// Additionally, we verify this property of virtual registers:
+///
+/// - The values in a virtual register are ordered according to the dominator tree's `rpo_cmp()`.
+///
+/// We don't verify that virtual registers are minimal. Minimal CSSA is not required.
+pub fn verify_cssa(func: &Function,
+                   cfg: &ControlFlowGraph,
+                   domtree: &DominatorTree,
+                   liveness: &Liveness,
+                   virtregs: &VirtRegs)
+                   -> Result {
+    let verifier = CssaVerifier {
+        func,
+        cfg,
+        domtree,
+        virtregs,
+        liveness,
+    };
+    verifier.check_virtregs()?;
+    verifier.check_cssa()?;
+    Ok(())
+}
+
+struct CssaVerifier<'a> {
+    func: &'a Function,
+    cfg: &'a ControlFlowGraph,
+    domtree: &'a DominatorTree,
+    virtregs: &'a VirtRegs,
+    liveness: &'a Liveness,
+}
+
+impl<'a> CssaVerifier<'a> {
+    fn check_virtregs(&self) -> Result {
+        for vreg in self.virtregs.all_virtregs() {
+            let values = self.virtregs.values(vreg);
+
+            for (idx, &val) in values.iter().enumerate() {
+                if !self.func.dfg.value_is_valid(val) {
+                    return err!(val, "Invalid value in {}", vreg);
+                }
+                if !self.func.dfg.value_is_attached(val) {
+                    return err!(val, "Detached value in {}", vreg);
+                }
+                if self.liveness.get(val).is_none() {
+                    return err!(val, "Value in {} has no live range", vreg);
+                };
+
+                // Check RPO ordering with the previous values in the virtual register.
+                let def = self.func.dfg.value_def(val).into();
+                let def_ebb = self.func.layout.pp_ebb(def);
+                for &prev_val in &values[0..idx] {
+                    let prev_def = self.func.dfg.value_def(prev_val);
+
+                    // Enforce RPO of defs in the virtual register.
+                    match self.domtree.rpo_cmp(prev_def, def, &self.func.layout) {
+                        Ordering::Less => {}
+                        Ordering::Equal => {
+                            return err!(val, "Value in {} has same def as {}", vreg, prev_val);
+                        }
+                        Ordering::Greater => {
+                            return err!(val,
+                                        "Value in {} in wrong order relative to {}",
+                                        vreg,
+                                        prev_val);
+                        }
+                    }
+
+                    // Knowing that values are in RPO order, we can check for interference this
+                    // way.
+                    if self.liveness[prev_val].overlaps_def(def, def_ebb, &self.func.layout) {
+                        return err!(val, "Value def in {} interferes with {}", vreg, prev_val);
+                    }
+                }
+            }
+        }
+
+        Ok(())
+    }
+
+    fn check_cssa(&self) -> Result {
+        for ebb in self.func.layout.ebbs() {
+            let ebb_args = self.func.dfg.ebb_args(ebb);
+            for &(_, pred) in self.cfg.get_predecessors(ebb) {
+                let pred_args = self.func.dfg.inst_variable_args(pred);
+                // This should have been caught by an earlier verifier pass.
+                assert_eq!(ebb_args.len(),
+                           pred_args.len(),
+                           "Wrong arguments on branch.");
+
+                for (&ebb_arg, &pred_arg) in ebb_args.iter().zip(pred_args) {
+                    if !self.virtregs.same_class(ebb_arg, pred_arg) {
+                        return err!(pred,
+                                    "{} and {} must be in the same virtual register",
+                                    ebb_arg,
+                                    pred_arg);
+                    }
+                }
+            }
+        }
+
+        Ok(())
+    }
+}

lib/cretonne/src/verifier/mod.rs

@@ -65,6 +65,7 @@ use std::result;
 use std::collections::BTreeSet;
 
 pub use self::liveness::verify_liveness;
+pub use self::cssa::verify_cssa;
 
 // Create an `Err` variant of `Result<X>` from a location and `format!` arguments.
 macro_rules! err {
@@ -83,6 +84,7 @@ macro_rules! err {
     };
 }
 
+mod cssa;
 mod liveness;
 
 /// A verifier error.