diff --git a/artifacts/verified-codegen-roadmap.yaml b/artifacts/verified-codegen-roadmap.yaml index b7fee10f6..0ea9b927a 100644 --- a/artifacts/verified-codegen-roadmap.yaml +++ b/artifacts/verified-codegen-roadmap.yaml @@ -88,10 +88,15 @@ artifacts: # free colour; no colour => actual spill). THE allocation decision the # single-pass allocator can't make (it hard-fails instead). Verified on real # selector output: colourable within the R0-R8 pool (k=9). Still unwired. + # - Precolouring: color_graph_precolored(graph, k, pins) pins nodes to fixed + # colours (never simplified/spilled, only constrain neighbours) — the + # mechanism for synth's reserved regs (R9/R10/R11/R12) + ABI arg pins. + # color_graph() now delegates with empty pins. Still unwired. # Remaining for VCR-RA-001: spill-code insertion (rewrite spilled values to - # stack slots + reload) -> precolouring reserved regs (R9/R11/R12/R10) -> - # ABI-exit-liveness union -> virtual-reg selector output -> oracle-gated - # wiring (the consequential step that finally removes the hard-fail). + # stack slots + reload) -> ABI-exit-liveness union -> virtual-reg selector + # output -> oracle-gated wiring (the consequential step that finally removes + # the hard-fail; it CHANGES emitted bytes so needs the full differential + # gate, unlike the unwired-by-construction analysis pieces above). - id: VCR-RA-001 type: sw-req title: SSA-based register allocator with spilling (remove the hard-fail) diff --git a/crates/synth-synthesis/src/liveness.rs b/crates/synth-synthesis/src/liveness.rs index 593d29fcc..7658f7271 100644 --- a/crates/synth-synthesis/src/liveness.rs +++ b/crates/synth-synthesis/src/liveness.rs @@ -894,12 +894,37 @@ pub enum ColorResult { /// `k == 0` with a non-empty graph is trivially uncolourable (every node /// spills). Pure function: it computes a decision, it does not mutate codegen. pub fn color_graph(g: &InterferenceGraph, k: usize) -> ColorResult { - // Working adjacency we can shrink as we simplify. - let mut adj: BTreeMap> = - g.nodes().map(|n| (n, g.neighbors(n).collect())).collect(); + color_graph_precolored(g, k, &BTreeMap::new()) +} + +/// `k`-colouring with **precoloured** nodes pinned to fixed colours — the +/// mechanism for honouring synth's reserved registers and ABI pins. Each entry +/// `(reg → colour)` in `precolored` keeps that colour and is never simplified or +/// spilled; it only *constrains* its neighbours (occupying a colour they cannot +/// reuse). Free nodes are coloured/​spilled by the same Chaitin/Briggs pass. +/// +/// To reserve physical registers (e.g. keep `R11` = memory base), pin the +/// corresponding node to its colour and treat that colour as taken for the pool; +/// to force args, pin `R0..=R3`. Precoloured colours should be in `0..k` +/// (out-of-range pins are ignored for conflict purposes rather than panicking). +/// Pure function: a decision, not a codegen mutation. +pub fn color_graph_precolored( + g: &InterferenceGraph, + k: usize, + precolored: &BTreeMap, +) -> ColorResult { + // Working adjacency over the FREE (non-precoloured) nodes only; precoloured + // nodes are fixed, so they never enter the simplify worklist — but they + // remain in every free node's neighbourhood (via `g.neighbors`) so they + // still constrain colouring. + let mut adj: BTreeMap> = g + .nodes() + .filter(|n| !precolored.contains_key(n)) + .map(|n| (n, g.neighbors(n).collect())) + .collect(); let mut stack: Vec = Vec::with_capacity(adj.len()); - // SIMPLIFY / SPILL: push every node, preferring low-degree (< k) nodes; + // SIMPLIFY / SPILL: push every free node, preferring low-degree (< k) nodes; // when none qualify, optimistically push the highest-degree node. while !adj.is_empty() { let pick = adj @@ -925,8 +950,10 @@ pub fn color_graph(g: &InterferenceGraph, k: usize) -> ColorResult { } // SELECT: pop in reverse, assign the lowest free colour using the ORIGINAL - // neighbourhood. A node with no free colour in 0..k is an actual spill. - let mut colour: BTreeMap = BTreeMap::new(); + // neighbourhood. Seeded with the precoloured pins, so a free node avoids + // both its precoloured and its already-selected neighbours. A node with no + // free colour in 0..k is an actual spill. + let mut colour: BTreeMap = precolored.clone(); let mut spilled: BTreeSet = BTreeSet::new(); while let Some(n) = stack.pop() { let mut used = vec![false; k]; @@ -1755,4 +1782,51 @@ mod tests { g.node(Reg::R0); assert!(matches!(color_graph(&g, 0), ColorResult::Spilled(_))); } + + #[test] + fn precolored_node_keeps_its_colour_and_constrains_neighbours() { + // Triangle R0—R1—R2; pin R0 to colour 2. With k=3, R1/R2 must avoid 2 + // (and each other), so they take {0,1}. + let g = clique(&[Reg::R0, Reg::R1, Reg::R2]); + let pre = BTreeMap::from([(Reg::R0, 2usize)]); + match color_graph_precolored(&g, 3, &pre) { + ColorResult::Colored(c) => { + assert_eq!(c[&Reg::R0], 2, "precoloured node keeps its colour"); + assert_ne!(c[&Reg::R1], 2); + assert_ne!(c[&Reg::R2], 2); + assert_ne!(c[&Reg::R1], c[&Reg::R2]); + } + ColorResult::Spilled(s) => panic!("3-colourable with the pin, got {s:?}"), + } + } + + #[test] + fn precoloring_can_force_a_spill_by_exhausting_colours() { + // R2 interferes with R0 and R1; pin R0=0, R1=1. With only k=2 colours + // both are taken in R2's neighbourhood → R2 must spill, even though the + // bare graph (a path) is 2-colourable without the pins. + let mut g = InterferenceGraph::default(); + g.add_edge(Reg::R2, Reg::R0); + g.add_edge(Reg::R2, Reg::R1); + let pre = BTreeMap::from([(Reg::R0, 0usize), (Reg::R1, 1usize)]); + match color_graph_precolored(&g, 2, &pre) { + ColorResult::Spilled(s) => assert!(s.contains(&Reg::R2)), + ColorResult::Colored(c) => panic!("R2 has no free colour, got {c:?}"), + } + // One more colour resolves it: R2 takes colour 2. + match color_graph_precolored(&g, 3, &pre) { + ColorResult::Colored(c) => assert_eq!(c[&Reg::R2], 2), + ColorResult::Spilled(s) => panic!("k=3 leaves a free colour, got {s:?}"), + } + } + + #[test] + fn color_graph_delegates_to_empty_precoloring() { + // The plain entry point must agree with the precoloured one given no pins. + let g = clique(&[Reg::R0, Reg::R1, Reg::R2, Reg::R3]); + assert_eq!( + color_graph(&g, 4), + color_graph_precolored(&g, 4, &BTreeMap::new()) + ); + } }