Header PHI creates a dst ValueId, but later instructions might accidentally overwrite it:
```rust
// Header block
%10 = phi [%5, entry], [%20, latch] // PHI dst
...
%10 = binop %8 + %9 // ❌ Overwrites PHI dst!
```
This violates SSA invariant (single assignment) and causes undefined behavior.
#### Detection Algorithm
```rust
fn verify_no_phi_dst_overwrite(
func: &MirFunction,
header_block: BasicBlockId,
loop_info: &LoopHeaderPhiInfo,
) {
let block_data = &func.blocks[&header_block];
// 1. Collect all PHI dsts
let phi_dsts: HashSet<ValueId> = loop_info.carrier_phis.values()
.map(|entry| entry.phi_dst)
.collect();
if phi_dsts.is_empty() {
return; // No PHIs to verify
}
// 2. Check instructions after PHI definitions
let mut after_phis = false;
for instr in &block_data.instructions {
match instr {
MirInstruction::Phi { dst, .. } => {
// PHI instructions come first
if !after_phis {
continue;
}
}
_ => {
after_phis = true;
// Check if this instruction writes to a PHI dst
if let Some(dst) = instr.dst() {
if phi_dsts.contains(&dst) {
panic!(
"[JoinIRVerifier] PHI dst {:?} is overwritten by {:?} in header block {}",
dst, instr, header_block
);
}
}
}
}
}
}
```
#### Integration Point
Add to `verify_joinir_contracts()`:
```rust
#[cfg(debug_assertions)]
fn verify_joinir_contracts(...) {
verify_loop_header_phis(...);
verify_no_phi_dst_overwrite(func, header_block, loop_info); // ← NEW
verify_exit_line(...);
}
```
### 3.2 Task 204-3: PHI Inputs Defined Verification
#### Problem
PHI instructions reference incoming values from predecessor blocks. These values must be defined before the PHI:
```rust
// Entry block
%5 = const 0
jump header
// Header block
%10 = phi [%5, entry], [%99, latch] // ❌ %99 undefined if latch not executed!
```
#### Detection Algorithm
```rust
fn verify_phi_inputs_defined(
func: &MirFunction,
header_block: BasicBlockId,
) {
let block_data = &func.blocks[&header_block];
for instr in &block_data.instructions {
if let MirInstruction::Phi { inputs, .. } = instr {
for (value_id, pred_block) in inputs {
// Check if value_id is defined before this PHI
// Options:
// 1. Conservative: Check if value_id exists in any reachable block
// 2. Optimistic: Assume all pred_blocks are reachable (current approach)
// 3. Full DFA: Track defined values through CFG (future enhancement)
// Phase 204: Conservative check - value_id should not be "obviously undefined"
// (e.g., ValueId > reasonable threshold, or in PHI reserved region but not a PHI dst)
// For now, we rely on existing SSA construction to handle this.
// This is a placeholder for future enhancement.
}
}
}
}
```
**Note**: Full PHI input verification requires data-flow analysis. Phase 204 focuses on simpler checks first. This can be enhanced in Phase 205+ if needed.
### 3.3 Task 204-4: JoinValueSpace Region Verification
#### Problem
Phase 201 introduced JoinValueSpace with region separation:
- PHI Reserved: 0-99
- Param Region: 100-999
- Local Region: 1000+
We need to verify these contracts are maintained during JoinIR lowering.
#### Detection Algorithm
```rust
fn verify_value_id_regions(
boundary: &JoinInlineBoundary,
loop_info: &LoopHeaderPhiInfo,
join_value_space: &JoinValueSpace,
) {
// 1. Verify Param region usage
for (host_id, join_id) in boundary.host_inputs.iter().zip(&boundary.join_inputs) {
let region = join_value_space.region_of(*join_id);
if region != Region::Param {
panic!(
"[JoinIRVerifier] Boundary input {:?} is in {:?} region, expected Param",
join_id, region
);
}
}
// 2. Verify PHI dst region (should be in PHI Reserved or Param)
for (carrier_name, entry) in &loop_info.carrier_phis {
let region = join_value_space.region_of(entry.phi_dst);
// PHI dst can be in Param region (assigned from frontend) or Local region
// This is OK since PHI dst comes from host side
// Just verify it's not in obviously wrong range
if entry.phi_dst.0 > 100000 {
panic!(
"[JoinIRVerifier] Carrier '{}' PHI dst {:?} has suspiciously large ID",
carrier_name, entry.phi_dst
);
}
}
// 3. Run JoinValueSpace's own verification
if let Err(e) = join_value_space.verify_no_overlap() {
`JoinValueSpace` is created in pattern lowerers (e.g., `pattern2_with_break.rs`), but verification runs in `merge/mod.rs`. We need to pass `JoinValueSpace` through the pipeline:
**Option A**: Add `JoinValueSpace` to `JoinInlineBoundary` (metadata field)
**Option B**: Add `JoinValueSpace` to `LoopHeaderPhiInfo` (already has carrier info)
**Option C**: Create new `JoinIRVerificationContext` struct
**Recommendation**: **Option B** (add to `LoopHeaderPhiInfo`) since it's already passed to verification functions.
```rust
// In src/mir/join_ir/lowering/loop_header_phi_builder.rs
