// Copyright (c) 2026 Alexander Medvednikov. All rights reserved.
// Use of this source code is governed by an MIT license
// that can be found in the LICENSE file.

module optimize

import v2.ssa

// VerifyError represents an SSA verification failure
struct VerifyError {
    msg       string
    func_id   int
    func_name string
    block_id  int
    val_id    int
}

fn (e VerifyError) str() string {
    mut s := 'SSA verify error'
    if e.func_id >= 0 {
        s += ' in func ${e.func_id}'
        if e.func_name != '' {
            s += ' (${e.func_name})'
        }
    }
    if e.block_id >= 0 {
        s += ' block ${e.block_id}'
    }
    if e.val_id >= 0 {
        s += ' value ${e.val_id}'
    }
    return '${s}: ${e.msg}'
}

pub struct VerifyPanicOptions {
pub:
    allow_noncritical bool
}

// verify performs comprehensive validation of SSA invariants.
// Returns a list of errors found (empty if valid).
// Call this after optimization passes to catch bugs.
pub fn verify(m &ssa.Module) []VerifyError {
    mut errors := []VerifyError{}

    // 1. Verify each function
    for fi in 0 .. m.funcs.len {
        errors << verify_function(m, &m.funcs[fi])
    }

    // 2. Verify global use-def chains
    errors << verify_use_def_chains(m)

    return errors
}

// verify_and_panic runs verification and panics on critical errors.
// Historical non-critical verifier warnings remain suppressed by default.
pub fn verify_and_panic(m &ssa.Module, pass_name string) {
    verify_and_panic_with_options(m, pass_name, VerifyPanicOptions{
        allow_noncritical: true
    })
}

// verify_and_panic_with_options runs verification with explicit warning policy.
// Set allow_noncritical to false for strict verifier checkpoints.
pub fn verify_and_panic_with_options(m &ssa.Module, pass_name string, opts VerifyPanicOptions) {
    errors := verify(m)
    if errors.len > 0 {
        mut msg := 'SSA verification failed after ${pass_name}:\n'
        // Filter out accepted declarations and optionally keep legacy warnings non-fatal:
        // - Explicit prototypes with no blocks are declarations kept in the module
        // - Dominance errors are often false positives in nested control flow
        // - Use-def chain errors happen during optimization when uses aren't cleaned up
        // - Phi errors are from mem2reg and don't affect codegen
        // - Block mismatch errors happen during block merging/optimization
        mut critical_errors := []VerifyError{}
        mut warning_count := 0
        for err in errors {
            if is_accepted_declaration_verify_error(m, err) {
                continue
            }
            if opts.allow_noncritical && is_legacy_noncritical_verify_error(err) {
                warning_count++
            } else {
                critical_errors << err
            }
        }
        for err in critical_errors {
            msg += '  ${err.msg}\n'
        }
        if warning_count > 0 {
            msg += '  (${warning_count} non-critical warnings suppressed)\n'
        }
        if critical_errors.len > 0 {
            panic(msg)
        }
    }
}

fn is_accepted_declaration_verify_error(m &ssa.Module, err VerifyError) bool {
    if err.msg == 'function has no blocks' {
        if err.func_id < 0 || err.func_id >= m.funcs.len {
            return false
        }
        func := m.funcs[err.func_id]
        return func.is_c_extern || func.is_prototype
    }
    return false
}

fn is_legacy_noncritical_verify_error(err VerifyError) bool {
    return err.msg.contains('does not dominate') || err.msg.contains('uses list')
        || err.msg.contains('phi') || err.msg.contains('block mismatch')
}

fn verify_function(m &ssa.Module, func &ssa.Function) []VerifyError {
    mut errors := []VerifyError{}

    // Function must have at least one block (entry)
    if func.blocks.len == 0 {
        errors << VerifyError{
            msg:     'function has no blocks'
            func_id: func.id
        }
        return errors
    }

    // Verify each block
    for blk_id in func.blocks {
        if blk_id < 0 || blk_id >= m.blocks.len {
            errors << VerifyError{
                msg:      'invalid block id ${blk_id}'
                func_id:  func.id
                block_id: -1
            }
            continue
        }
        errors << verify_block(m, func, blk_id)
    }

    // Verify dominance (values must dominate their uses)
    errors << verify_dominance(m, func)

    return errors
}

fn verify_block(m &ssa.Module, func &ssa.Function, blk_id int) []VerifyError {
    mut errors := []VerifyError{}
    blk := m.blocks[blk_id]

    // Block must belong to this function
    if blk.parent != func.id {
        errors << VerifyError{
            msg:      'block parent mismatch: expected ${func.id}, got ${blk.parent}'
            func_id:  func.id
            block_id: blk_id
        }
    }

    // Block must have instructions
    if blk.instrs.len == 0 {
        errors << VerifyError{
            msg:      'block has no instructions (missing terminator)'
            func_id:  func.id
            block_id: blk_id
        }
        return errors
    }

    // Verify instruction structure
    mut seen_terminator := false
    mut seen_non_phi := false

    for i, val_id in blk.instrs {
        if val_id < 0 || val_id >= m.values.len {
            errors << VerifyError{
                msg:      'invalid value id ${val_id} in instruction list'
                func_id:  func.id
                block_id: blk_id
            }
            continue
        }

        val := m.values[val_id]
        if val.kind != .instruction {
            // Skip non-instruction values (shouldn't be in instrs list normally)
            continue
        }

        if val.index < 0 || val.index >= m.instrs.len {
            errors << VerifyError{
                msg:      'value ${val_id} has invalid instruction index ${val.index}'
                func_id:  func.id
                block_id: blk_id
                val_id:   val_id
            }
            continue
        }

        instr := m.instrs[val.index]

        // Instruction must belong to this block
        if instr.block != blk_id {
            errors << VerifyError{
                msg:      'instruction block mismatch: expected ${blk_id}, got ${instr.block}'
                func_id:  func.id
                block_id: blk_id
                val_id:   val_id
            }
        }

        // Phi nodes must come before all other instructions
        if instr.op == .phi {
            if seen_non_phi {
                errors << VerifyError{
                    msg:      'phi node after non-phi instruction'
                    func_id:  func.id
                    block_id: blk_id
                    val_id:   val_id
                }
            }
        } else {
            seen_non_phi = true
        }

        // Terminator must be last
        is_terminator := instr.op in [.ret, .br, .jmp, .switch_, .unreachable]
        if is_terminator {
            if seen_terminator {
                errors << VerifyError{
                    msg:       'multiple terminators in block'
                    func_id:   func.id
                    func_name: func.name
                    block_id:  blk_id
                    val_id:    val_id
                }
            }
            if i != blk.instrs.len - 1 {
                errors << VerifyError{
                    msg:       'terminator not at end of block'
                    func_id:   func.id
                    func_name: func.name
                    block_id:  blk_id
                    val_id:    val_id
                }
            }
            seen_terminator = true
        }

        // Verify instruction operands and types
        errors << verify_instruction(m, func.id, blk_id, val_id, instr)
    }

    // Block must end with a terminator
    if !seen_terminator {
        errors << VerifyError{
            msg:      'block does not end with terminator'
            func_id:  func.id
            block_id: blk_id
        }
    }

    // Verify CFG consistency (if CFG is built)
    errors << verify_cfg_consistency(m, func.id, blk_id)

    return errors
}

fn verify_instruction(m &ssa.Module, func_id int, blk_id int, val_id int, instr ssa.Instruction) []VerifyError {
    mut errors := []VerifyError{}

    // Verify all operands are valid
    for i, op_id in instr.operands {
        if op_id < 0 || op_id >= m.values.len {
            errors << VerifyError{
                msg:      'operand ${i} has invalid value id ${op_id}'
                func_id:  func_id
                block_id: blk_id
                val_id:   val_id
            }
        }
    }

    // Type-specific verification
    match instr.op {
        // Binary arithmetic - operands should have compatible types
        .add, .sub, .mul, .sdiv, .udiv, .srem, .urem {
            errors << verify_binary_op(m, func_id, blk_id, val_id, instr)
        }
        // Binary float
        .fadd, .fsub, .fmul, .fdiv, .frem {
            errors << verify_binary_op(m, func_id, blk_id, val_id, instr)
        }
        // Bitwise - operands should be integers
        .shl, .lshr, .ashr, .and_, .or_, .xor {
            errors << verify_binary_op(m, func_id, blk_id, val_id, instr)
        }
        // Comparisons - operands should have same type
        .lt, .gt, .le, .ge, .eq, .ne, .ult, .ugt, .ule, .uge {
            errors << verify_binary_op(m, func_id, blk_id, val_id, instr)
        }
        // Memory operations
        .load {
            errors << verify_load(m, func_id, blk_id, val_id, instr)
        }
        .store {
            errors << verify_store(m, func_id, blk_id, val_id, instr)
        }
        .alloca, .heap_alloc {
            // alloca/heap_alloc result should be a pointer type
            if instr.typ > 0 && instr.typ < m.type_store.types.len {
                typ := m.type_store.types[instr.typ]
                if typ.kind != .ptr_t {
                    errors << VerifyError{
                        msg:      '${instr.op} result type should be pointer, got ${typ.kind}'
                        func_id:  func_id
                        block_id: blk_id
                        val_id:   val_id
                    }
                }
            }
        }
        // Control flow
        .phi {
            errors << verify_phi(m, func_id, blk_id, val_id, instr)
        }
        .br {
            errors << verify_branch(m, func_id, blk_id, val_id, instr)
        }
        .jmp {
            errors << verify_jump(m, func_id, blk_id, val_id, instr)
        }
        .switch_ {
            errors << verify_switch(m, func_id, blk_id, val_id, instr)
        }
        .ret {
            // ret can have 0 or 1 operands
            if instr.operands.len > 1 {
                errors << VerifyError{
                    msg:      'ret has ${instr.operands.len} operands, expected 0 or 1'
                    func_id:  func_id
                    block_id: blk_id
                    val_id:   val_id
                }
            }
        }
        .call, .call_indirect, .call_sret, .go_call, .spawn_call {
            // call should have at least a target (function pointer or name)
            if instr.operands.len == 0 {
                errors << VerifyError{
                    msg:      '${instr.op} has no operands'
                    func_id:  func_id
                    block_id: blk_id
                    val_id:   val_id
                }
            }
        }
        .select {
            // select should have 3 operands: condition, true_val, false_val
            if instr.operands.len != 3 {
                errors << VerifyError{
                    msg:      'select has ${instr.operands.len} operands, expected 3'
                    func_id:  func_id
                    block_id: blk_id
                    val_id:   val_id
                }
            }
        }
        .assign {
            // assign should have 2 operands: dest, src
            if instr.operands.len != 2 {
                errors << VerifyError{
                    msg:      'assign has ${instr.operands.len} operands, expected 2'
                    func_id:  func_id
                    block_id: blk_id
                    val_id:   val_id
                }
            }
        }
        else {}
    }

    return errors
}

fn verify_binary_op(m &ssa.Module, func_id int, blk_id int, val_id int, instr ssa.Instruction) []VerifyError {
    mut errors := []VerifyError{}

    if instr.operands.len != 2 {
        errors << VerifyError{
            msg:      'binary op has ${instr.operands.len} operands, expected 2'
            func_id:  func_id
            block_id: blk_id
            val_id:   val_id
        }
        return errors
    }

    // Check operand types match (for most binary ops)
    op0 := instr.operands[0]
    op1 := instr.operands[1]

    if op0 < m.values.len && op1 < m.values.len {
        t0 := m.values[op0].typ
        t1 := m.values[op1].typ

        // Types should be compatible (same type or one is 0/void for constants)
        if t0 != t1 && t0 != 0 && t1 != 0 {
            // Check if both are integers of potentially different widths
            if t0 < m.type_store.types.len && t1 < m.type_store.types.len {
                typ0 := m.type_store.types[t0]
                typ1 := m.type_store.types[t1]
                // Allow int-to-int operations with different widths (common pattern)
                if typ0.kind == .int_t && typ1.kind == .int_t {
                    return errors
                }
                // Allow float-to-float operations with different widths (f32 vs f64)
                if typ0.kind == .float_t && typ1.kind == .float_t {
                    return errors
                }
                // Allow int-float operations (common in numeric code, needs proper cast in builder)
                if (typ0.kind == .int_t && typ1.kind == .float_t)
                    || (typ0.kind == .float_t && typ1.kind == .int_t) {
                    return errors
                }
                // Allow pointer arithmetic (ptr +/- int)
                if (typ0.kind == .ptr_t && typ1.kind == .int_t)
                    || (typ0.kind == .int_t && typ1.kind == .ptr_t) {
                    return errors
                }
                // Allow pointer comparison/subtraction (ptr - ptr)
                if typ0.kind == .ptr_t && typ1.kind == .ptr_t {
                    return errors
                }
                // Allow ptr vs struct (common in V when passing structs by value/reference)
                if (typ0.kind == .ptr_t && typ1.kind == .struct_t)
                    || (typ0.kind == .struct_t && typ1.kind == .ptr_t) {
                    return errors
                }
                // Allow struct comparisons (V allows == on structs)
                if typ0.kind == .struct_t && typ1.kind == .struct_t {
                    return errors
                }
                // Allow struct vs int (for comparisons with nil/0)
                if (typ0.kind == .struct_t && typ1.kind == .int_t)
                    || (typ0.kind == .int_t && typ1.kind == .struct_t) {
                    return errors
                }
                errors << VerifyError{
                    msg:      'binary op operands have mismatched types: ${t0} (${typ0.kind}) vs ${t1} (${typ1.kind})'
                    func_id:  func_id
                    block_id: blk_id
                    val_id:   val_id
                }
            }
        }
    }

    return errors
}

fn verify_load(m &ssa.Module, func_id int, blk_id int, val_id int, instr ssa.Instruction) []VerifyError {
    mut errors := []VerifyError{}

    if instr.operands.len != 1 {
        errors << VerifyError{
            msg:      'load has ${instr.operands.len} operands, expected 1 (pointer)'
            func_id:  func_id
            block_id: blk_id
            val_id:   val_id
        }
        return errors
    }

    ptr_id := instr.operands[0]
    if ptr_id < m.values.len {
        ptr_typ_id := m.values[ptr_id].typ
        if ptr_typ_id > 0 && ptr_typ_id < m.type_store.types.len {
            ptr_typ := m.type_store.types[ptr_typ_id]
            if ptr_typ.kind != .ptr_t {
                errors << VerifyError{
                    msg:      'load operand should be pointer type, got ${ptr_typ.kind}'
                    func_id:  func_id
                    block_id: blk_id
                    val_id:   val_id
                }
            }
        }
    }

    return errors
}

fn verify_store(m &ssa.Module, func_id int, blk_id int, val_id int, instr ssa.Instruction) []VerifyError {
    mut errors := []VerifyError{}

    if instr.operands.len != 2 {
        errors << VerifyError{
            msg:      'store has ${instr.operands.len} operands, expected 2 (value, pointer)'
            func_id:  func_id
            block_id: blk_id
            val_id:   val_id
        }
        return errors
    }

    ptr_id := instr.operands[1]
    if ptr_id < m.values.len {
        ptr_typ_id := m.values[ptr_id].typ
        if ptr_typ_id > 0 && ptr_typ_id < m.type_store.types.len {
            ptr_typ := m.type_store.types[ptr_typ_id]
            if ptr_typ.kind != .ptr_t {
                errors << VerifyError{
                    msg:      'store destination should be pointer type, got ${ptr_typ.kind}'
                    func_id:  func_id
                    block_id: blk_id
                    val_id:   val_id
                }
            }
        }
    }

    return errors
}

fn verify_phi(m &ssa.Module, func_id int, blk_id int, val_id int, instr ssa.Instruction) []VerifyError {
    mut errors := []VerifyError{}

    // Phi operands come in pairs: [val0, block0, val1, block1, ...]
    if instr.operands.len % 2 != 0 {
        errors << VerifyError{
            msg:      'phi has odd number of operands (${instr.operands.len}), expected pairs of (value, block)'
            func_id:  func_id
            block_id: blk_id
            val_id:   val_id
        }
        return errors
    }

    if instr.operands.len == 0 {
        errors << VerifyError{
            msg:      'phi has no operands'
            func_id:  func_id
            block_id: blk_id
            val_id:   val_id
        }
        return errors
    }

    // Verify each operand pair
    for i := 0; i < instr.operands.len; i += 2 {
        val_in := instr.operands[i]
        blk_val := instr.operands[i + 1]

        // Value operand should exist
        if val_in >= m.values.len {
            errors << VerifyError{
                msg:      'phi operand ${i} has invalid value id ${val_in}'
                func_id:  func_id
                block_id: blk_id
                val_id:   val_id
            }
        }

        // Block operand should be a basic_block
        if blk_val < m.values.len {
            if m.values[blk_val].kind != .basic_block {
                errors << VerifyError{
                    msg:      'phi operand ${i + 1} should be basic_block, got ${m.values[blk_val].kind}'
                    func_id:  func_id
                    block_id: blk_id
                    val_id:   val_id
                }
            }
        }

        // Check type consistency: phi operand type should match phi result type
        if val_in < m.values.len {
            op_typ := m.values[val_in].typ
            phi_typ := instr.typ
            // Allow type mismatch with void (constants may have type 0)
            if op_typ != phi_typ && op_typ != 0 && phi_typ != 0 {
                // Only warn if both are real types
                if op_typ < m.type_store.types.len && phi_typ < m.type_store.types.len {
                    op_kind := m.type_store.types[op_typ].kind
                    phi_kind := m.type_store.types[phi_typ].kind
                    // Allow int-to-int (common pattern)
                    if op_kind != .int_t || phi_kind != .int_t {
                        errors << VerifyError{
                            msg:      'phi operand ${i} type ${op_typ} does not match phi type ${phi_typ}'
                            func_id:  func_id
                            block_id: blk_id
                            val_id:   val_id
                        }
                    }
                }
            }
        }
    }

    // If CFG is built, verify phi operand count matches predecessor count
    blk := m.blocks[blk_id]
    if blk.preds.len > 0 {
        expected_pairs := blk.preds.len
        actual_pairs := instr.operands.len / 2
        if actual_pairs != expected_pairs {
            errors << VerifyError{
                msg:      'phi has ${actual_pairs} operand pairs but block has ${expected_pairs} predecessors'
                func_id:  func_id
                block_id: blk_id
                val_id:   val_id
            }
        }

        // Verify each phi block operand is actually a predecessor
        for i := 1; i < instr.operands.len; i += 2 {
            blk_val := instr.operands[i]
            if blk_val < m.values.len && m.values[blk_val].kind == .basic_block {
                pred_blk_id := m.values[blk_val].index
                if pred_blk_id !in blk.preds {
                    errors << VerifyError{
                        msg:      'phi references block ${pred_blk_id} which is not a predecessor'
                        func_id:  func_id
                        block_id: blk_id
                        val_id:   val_id
                    }
                }
            }
        }
    }

    return errors
}

fn verify_branch(m &ssa.Module, func_id int, blk_id int, val_id int, instr ssa.Instruction) []VerifyError {
    mut errors := []VerifyError{}

    // br should have 3 operands: condition, true_block, false_block
    if instr.operands.len != 3 {
        errors << VerifyError{
            msg:      'br has ${instr.operands.len} operands, expected 3 (cond, true_blk, false_blk)'
            func_id:  func_id
            block_id: blk_id
            val_id:   val_id
        }
        return errors
    }

    // Verify block operands are basic blocks
    for i in [1, 2] {
        blk_val := instr.operands[i]
        if blk_val < m.values.len {
            if m.values[blk_val].kind != .basic_block {
                errors << VerifyError{
                    msg:      'br operand ${i} should be basic_block, got ${m.values[blk_val].kind}'
                    func_id:  func_id
                    block_id: blk_id
                    val_id:   val_id
                }
            }
        }
    }

    return errors
}

fn verify_jump(m &ssa.Module, func_id int, blk_id int, val_id int, instr ssa.Instruction) []VerifyError {
    mut errors := []VerifyError{}

    // jmp should have 1 operand: target block
    if instr.operands.len != 1 {
        errors << VerifyError{
            msg:      'jmp has ${instr.operands.len} operands, expected 1 (target_blk)'
            func_id:  func_id
            block_id: blk_id
            val_id:   val_id
        }
        return errors
    }

    blk_val := instr.operands[0]
    if blk_val < m.values.len {
        if m.values[blk_val].kind != .basic_block {
            errors << VerifyError{
                msg:      'jmp operand should be basic_block, got ${m.values[blk_val].kind}'
                func_id:  func_id
                block_id: blk_id
                val_id:   val_id
            }
        }
    }

    return errors
}

fn verify_switch(m &ssa.Module, func_id int, blk_id int, val_id int, instr ssa.Instruction) []VerifyError {
    mut errors := []VerifyError{}

    // switch should have: condition, default_block, then pairs of (value, block)
    if instr.operands.len < 2 {
        errors << VerifyError{
            msg:      'switch has ${instr.operands.len} operands, expected at least 2 (cond, default)'
            func_id:  func_id
            block_id: blk_id
            val_id:   val_id
        }
        return errors
    }

    // Verify default block is a basic block
    default_blk := instr.operands[1]
    if default_blk < m.values.len {
        if m.values[default_blk].kind != .basic_block {
            errors << VerifyError{
                msg:      'switch default should be basic_block, got ${m.values[default_blk].kind}'
                func_id:  func_id
                block_id: blk_id
                val_id:   val_id
            }
        }
    }

    // Remaining operands should be pairs of (value, block)
    remaining := instr.operands.len - 2
    if remaining % 2 != 0 {
        errors << VerifyError{
            msg:      'switch has odd number of case operands (${remaining})'
            func_id:  func_id
            block_id: blk_id
            val_id:   val_id
        }
    }

    return errors
}

fn verify_cfg_consistency(m &ssa.Module, func_id int, blk_id int) []VerifyError {
    mut errors := []VerifyError{}
    blk := m.blocks[blk_id]

    // Skip if CFG not built yet
    if blk.succs.len == 0 && blk.preds.len == 0 {
        return errors
    }

    // Verify successor symmetry: if B is successor of A, then A should be predecessor of B
    for succ_id in blk.succs {
        if succ_id < 0 || succ_id >= m.blocks.len {
            errors << VerifyError{
                msg:      'invalid successor block id ${succ_id}'
                func_id:  func_id
                block_id: blk_id
            }
            continue
        }
        if blk_id !in m.blocks[succ_id].preds {
            errors << VerifyError{
                msg:      'block ${blk_id} has successor ${succ_id} but is not in its predecessors'
                func_id:  func_id
                block_id: blk_id
            }
        }
    }

    // Verify predecessor symmetry: if A is predecessor of B, then B should be successor of A
    for pred_id in blk.preds {
        if pred_id < 0 || pred_id >= m.blocks.len {
            errors << VerifyError{
                msg:      'invalid predecessor block id ${pred_id}'
                func_id:  func_id
                block_id: blk_id
            }
            continue
        }
        if blk_id !in m.blocks[pred_id].succs {
            errors << VerifyError{
                msg:      'block ${blk_id} has predecessor ${pred_id} but is not in its successors'
                func_id:  func_id
                block_id: blk_id
            }
        }
    }

    // Verify terminator matches successors
    if blk.instrs.len > 0 {
        term_val_id := blk.instrs[blk.instrs.len - 1]
        if term_val_id < m.values.len && m.values[term_val_id].kind == .instruction {
            term := m.instrs[m.values[term_val_id].index]
            mut expected_succs := []int{}

            match term.op {
                .jmp {
                    if term.operands.len >= 1 {
                        target_val := term.operands[0]
                        if target_val < m.values.len && m.values[target_val].kind == .basic_block {
                            expected_succs << m.values[target_val].index
                        }
                    }
                }
                .br {
                    if term.operands.len >= 3 {
                        true_val := term.operands[1]
                        false_val := term.operands[2]
                        if true_val < m.values.len && m.values[true_val].kind == .basic_block {
                            expected_succs << m.values[true_val].index
                        }
                        if false_val < m.values.len && m.values[false_val].kind == .basic_block {
                            if m.values[false_val].index !in expected_succs {
                                expected_succs << m.values[false_val].index
                            }
                        }
                    }
                }
                .switch_ {
                    // Default block
                    if term.operands.len >= 2 {
                        default_val := term.operands[1]
                        if default_val < m.values.len && m.values[default_val].kind == .basic_block {
                            expected_succs << m.values[default_val].index
                        }
                    }
                    // Case blocks
                    for i := 3; i < term.operands.len; i += 2 {
                        blk_val := term.operands[i]
                        if blk_val < m.values.len && m.values[blk_val].kind == .basic_block {
                            idx := m.values[blk_val].index
                            if idx !in expected_succs {
                                expected_succs << idx
                            }
                        }
                    }
                }
                .ret, .unreachable {
                    // No successors expected
                }
                else {}
            }

            // Check for missing successors
            for succ in expected_succs {
                if succ !in blk.succs {
                    errors << VerifyError{
                        msg:      'terminator targets block ${succ} but it is not in successors'
                        func_id:  func_id
                        block_id: blk_id
                    }
                }
            }
        }
    }

    return errors
}

fn verify_dominance(m &ssa.Module, func &ssa.Function) []VerifyError {
    mut errors := []VerifyError{}

    // Build map of value -> defining block
    mut def_block := map[int]int{}

    // Function parameters are defined in entry block
    for param_id in func.params {
        if func.blocks.len > 0 {
            def_block[param_id] = func.blocks[0]
        }
    }

    // Build definition map for all instructions
    for blk_id in func.blocks {
        if blk_id >= m.blocks.len {
            continue
        }
        for val_id in m.blocks[blk_id].instrs {
            def_block[val_id] = blk_id
        }
    }

    // Skip dominance check if dominators not computed
    // After compute_dominators, dom_tree is populated for the entry block (if function has multiple blocks)
    // Before computation, dom_tree is empty. For single-block functions, there's nothing to verify.
    entry_block := func.blocks[0]
    dominators_computed := func.blocks.len == 1 || m.blocks[entry_block].dom_tree.len > 0

    if !dominators_computed {
        return errors
    }

    // For each use, verify definition dominates use
    for blk_id in func.blocks {
        if blk_id >= m.blocks.len {
            continue
        }
        for val_id in m.blocks[blk_id].instrs {
            if val_id >= m.values.len || m.values[val_id].kind != .instruction {
                continue
            }
            if m.values[val_id].index >= m.instrs.len {
                continue
            }
            instr := m.instrs[m.values[val_id].index]

            // Check each operand
            for i, op_id in instr.operands {
                if op_id >= m.values.len {
                    continue
                }

                // Skip block references and constants
                op_val := m.values[op_id]
                if op_val.kind in [.basic_block, .constant, .global, .string_literal,
                    .c_string_literal] {
                    continue
                }

                // Phi nodes are special: operands come from predecessors
                if instr.op == .phi {
                    continue
                }

                // Check dominance
                if def_blk := def_block[op_id] {
                    if !dominates(m, func, def_blk, blk_id) {
                        errors << VerifyError{
                            msg:       'operand ${i} (value ${op_id}) defined in block ${def_blk} does not dominate use in block ${blk_id}'
                            func_id:   func.id
                            func_name: func.name
                            block_id:  blk_id
                            val_id:    val_id
                        }
                    }
                }
            }
        }
    }

    return errors
}

// dominates returns true if block a dominates block b
fn dominates(m &ssa.Module, func &ssa.Function, a int, b int) bool {
    if a == b {
        return true
    }

    // Walk up dominator tree from b
    mut curr := b
    for {
        if curr < 0 || curr >= m.blocks.len {
            return false
        }
        idom := m.blocks[curr].idom
        if idom < 0 {
            // Unreachable block (idom = -1)
            return false
        }
        if idom == curr {
            // Reached entry block (or invalid state)
            return a == curr
        }
        if idom == a {
            return true
        }
        if idom == 0 && curr != 0 {
            // Entry block case
            return a == 0 || a == func.blocks[0]
        }
        curr = idom
    }
    return false
}

fn verify_use_def_chains(m &ssa.Module) []VerifyError {
    mut errors := []VerifyError{}

    // Build expected uses from instruction operands
    mut expected_uses := map[int]map[int]bool{} // value -> set of users

    for fi in 0 .. m.funcs.len {
        for blk_id in m.funcs[fi].blocks {
            if blk_id >= m.blocks.len {
                continue
            }
            for val_id in m.blocks[blk_id].instrs {
                if val_id >= m.values.len || m.values[val_id].kind != .instruction {
                    continue
                }
                if m.values[val_id].index >= m.instrs.len {
                    continue
                }
                instr := m.instrs[m.values[val_id].index]

                for op_id in instr.operands {
                    if op_id < m.values.len {
                        if op_id !in expected_uses {
                            expected_uses[op_id] = map[int]bool{}
                        }
                        expected_uses[op_id][val_id] = true
                    }
                }
            }
        }
    }

    // Verify actual uses match expected
    for val_id, users in expected_uses {
        if val_id >= m.values.len {
            continue
        }
        actual := m.values[val_id].uses

        for user_id, _ in users {
            if user_id !in actual {
                errors << VerifyError{
                    msg:    'value ${val_id} is used by ${user_id} but ${user_id} is not in uses list'
                    val_id: val_id
                }
            }
        }
    }

    // Check for spurious uses (uses list contains values that don't actually use this value)
    for i, val in m.values {
        if val.kind != .instruction && val.kind != .argument {
            continue
        }
        for user_id in val.uses {
            if user_id >= m.values.len {
                errors << VerifyError{
                    msg:    'value ${i} has invalid user ${user_id} in uses list'
                    val_id: i
                }
                continue
            }
            user_val := m.values[user_id]
            if user_val.kind != .instruction {
                continue
            }
            if user_val.index >= m.instrs.len {
                continue
            }
            instr := m.instrs[user_val.index]
            if i !in instr.operands {
                errors << VerifyError{
                    msg:    'value ${i} has ${user_id} in uses list but ${user_id} does not use it'
                    val_id: i
                }
            }
        }
    }

    return errors
}