Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions artifacts/verified-codegen-roadmap.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -70,6 +70,15 @@ artifacts:
# Track A — codegen core (sequential within: allocator first, then selector)
# ---------------------------------------------------------------------------

# PROGRESS (substrate, side-by-side / unwired):
# - reg_effect + per-segment dead-store/redundant-const analysis
# (synth-synthesis/src/liveness.rs)
# - CFG-aware liveness: cfg_liveness() builds the label-form basic-block CFG
# and solves per-block live-in/live-out via the backward dataflow fixpoint
# (the interference-graph substrate). Pure analysis, zero codegen callers,
# so every frozen fixture stays bit-identical by construction. Leaf-only,
# label-form scope; declines (None) on calls/offset/computed branches.
# Remaining for VCR-RA-001: interference graph -> colouring -> spill/reload.
- id: VCR-RA-001
type: sw-req
title: SSA-based register allocator with spilling (remove the hard-fail)
Expand Down
23 changes: 23 additions & 0 deletions crates/synth-synthesis/src/instruction_selector.rs
Original file line number Diff line number Diff line change
Expand Up @@ -14814,6 +14814,29 @@ mod tests {
let (out, removed) = liveness::eliminate_dead_stores(&instrs);
assert_eq!(removed, report.dead_defs.len());
assert_eq!(out.len(), instrs.len() - removed);

// CFG-aware liveness on the same real output must either decline
// (out-of-scope construct) or return a *structurally sound* graph:
// blocks tile [0, len) gaplessly, every successor index is in range,
// and the per-block live-set vectors line up with the block count.
if let Some(cfg) = liveness::cfg_liveness(&instrs) {
assert_eq!(cfg.live_in.len(), cfg.blocks.len());
assert_eq!(cfg.live_out.len(), cfg.blocks.len());
let mut expected_start = 0usize;
for b in &cfg.blocks {
assert_eq!(b.start, expected_start, "blocks must tile without gaps");
assert!(b.end > b.start, "blocks are non-empty");
for &s in &b.succ {
assert!(s < cfg.blocks.len(), "successor index in range");
}
expected_start = b.end;
}
assert_eq!(
expected_start,
instrs.len(),
"blocks cover the whole stream"
);
}
}

#[test]
Expand Down
Loading
Loading