module optimize

import v3.ssa

// VerifyError is a structured SSA verification failure. Unlike verify_ssa()
// (which panics on the first problem), the structured API collects every error so
// callers can decide which are fatal.
pub struct VerifyError {
pub:
	msg       string
	func_id   int = -1
	func_name string
	block_id  int = -1
	val_id    int = -1
}

// str returns the string form for VerifyError.
pub 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}'
}

// VerifyPanicOptions controls verify panic options behavior used by optimize.
pub struct VerifyPanicOptions {
pub:
	allow_noncritical bool
}

// verify performs comprehensive validation of SSA invariants and returns every
// error found (empty slice == valid). v3 stores branch/phi/switch targets as raw
// block ids, so block operands are validated as block ids, not block values.
pub fn verify(m &ssa.Module) []VerifyError {
	mut errors := []VerifyError{}
	for fi in 0 .. m.funcs.len {
		errors << verify_function(m, m.funcs[fi])
	}
	errors << verify_use_def_chains(m)
	return errors
}

// verify_and_panic runs verification and panics on critical errors only.
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 an explicit warning policy.
// Declaration-only functions (C externs / prototypes) are always accepted.
pub fn verify_and_panic_with_options(m &ssa.Module, pass_name string, opts VerifyPanicOptions) {
	errors := verify(m)
	if errors.len == 0 {
		return
	}
	mut msg := 'SSA verification failed after ${pass_name}:\n'
	mut critical := []VerifyError{}
	mut warnings := 0
	for err in errors {
		if is_accepted_declaration_verify_error(m, err) {
			continue
		}
		if opts.allow_noncritical && is_legacy_noncritical_verify_error(err) {
			warnings++
		} else {
			critical << err
		}
	}
	for err in critical {
		msg += '  ${err.msg}\n'
	}
	if warnings > 0 {
		msg += '  (${warnings} non-critical warnings suppressed)\n'
	}
	if critical.len > 0 {
		panic(msg)
	}
}

// is_accepted_declaration_verify_error supports is_accepted_declaration_verify_error handling.
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
}

// is_legacy_noncritical_verify_error reports is_legacy_noncritical_verify_error logic in optimize.
fn is_legacy_noncritical_verify_error(err VerifyError) bool {
	// Dominance / use-def / phi mismatches are commonly transient between passes.
	if err.msg.contains('does not dominate') || err.msg.contains('uses list')
		|| err.msg.contains('phi') || err.msg.contains('block mismatch') {
		return true
	}
	// Structural-normalization artifacts emitted by the builder before the
	// optimizer cleans them up (empty/unreachable blocks, dead code that follows
	// a terminator within the same block). These are tolerated by the lenient
	// verify_ssa() and removed by remove_unreachable_blocks / DCE.
	if err.msg.contains('has no instructions') || err.msg.contains('not at end of block')
		|| err.msg.contains('multiple terminators')
		|| err.msg.contains('does not end with terminator') {
		return true
	}
	// Type-precision findings. The v3 builder does not maintain strict SSA typing
	// on every load/store/binary operand (e.g. aggregates loaded by value), and
	// the backends tolerate it, so these are advisory rather than fatal.
	return err.msg.contains('should be pointer type') || err.msg.contains('mismatched types')
		|| err.msg.contains('result type should be pointer')
}

// verify_function validates verify function state for optimize.
fn verify_function(m &ssa.Module, func ssa.Function) []VerifyError {
	mut errors := []VerifyError{}
	if func.blocks.len == 0 {
		errors << VerifyError{
			msg:     'function has no blocks'
			func_id: func.id
		}
		return errors
	}
	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
			}
			continue
		}
		errors << verify_block(m, func, blk_id)
	}
	errors << verify_dominance(m, func)
	return errors
}

// verify_block validates verify block state for optimize.
fn verify_block(m &ssa.Module, func ssa.Function, blk_id int) []VerifyError {
	mut errors := []VerifyError{}
	blk := m.blocks[blk_id]
	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
		}
	}
	if blk.instrs.len == 0 {
		errors << VerifyError{
			msg:      'block has no instructions (missing terminator)'
			func_id:  func.id
			block_id: blk_id
		}
		return errors
	}

	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 {
			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]
		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
			}
		}
		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
		}
		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
		}
		errors << verify_instruction(m, func.id, blk_id, val_id, instr)
	}
	if !seen_terminator {
		errors << VerifyError{
			msg:      'block does not end with terminator'
			func_id:  func.id
			block_id: blk_id
		}
	}
	errors << verify_cfg_consistency(m, func.id, blk_id)
	return errors
}

// verify_instruction validates verify instruction state for optimize.
fn verify_instruction(m &ssa.Module, func_id int, blk_id int, val_id int, instr ssa.Instruction) []VerifyError {
	mut errors := []VerifyError{}
	// Only value operands are validated as value ids; block ids (branch/phi/switch
	// targets) are validated by the op-specific checks below.
	for i, op_id in instr.value_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
			}
		}
	}
	match instr.op {
		.add, .sub, .mul, .sdiv, .udiv, .srem, .urem {
			errors << verify_binary_op(m, func_id, blk_id, val_id, instr)
		}
		.fadd, .fsub, .fmul, .fdiv, .frem {
			errors << verify_binary_op(m, func_id, blk_id, val_id, instr)
		}
		.shl, .lshr, .ashr, .and_, .or_, .xor {
			errors << verify_binary_op(m, func_id, blk_id, val_id, instr)
		}
		.lt, .gt, .le, .ge, .eq, .ne, .ult, .ugt, .ule, .uge {
			errors << verify_binary_op(m, func_id, blk_id, val_id, instr)
		}
		.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 {
			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
					}
				}
			}
		}
		.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 {
			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 {
			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 {
			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 {
			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
}

// verify_binary_op validates verify binary op state for optimize.
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
	}
	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
		if t0 != t1 && t0 != 0 && t1 != 0 {
			if t0 < m.type_store.types.len && t1 < m.type_store.types.len {
				k0 := m.type_store.types[t0].kind
				k1 := m.type_store.types[t1].kind
				// Allow common mixed-kind binary patterns (different widths, ptr
				// arithmetic, struct/nil comparisons, int/float coercions).
				if k0 == .int_t && k1 == .int_t {
					return errors
				}
				if k0 == .float_t && k1 == .float_t {
					return errors
				}
				if (k0 == .int_t && k1 == .float_t) || (k0 == .float_t && k1 == .int_t) {
					return errors
				}
				if (k0 == .ptr_t && k1 == .int_t) || (k0 == .int_t && k1 == .ptr_t) {
					return errors
				}
				if k0 == .ptr_t && k1 == .ptr_t {
					return errors
				}
				if (k0 == .ptr_t && k1 == .struct_t) || (k0 == .struct_t && k1 == .ptr_t) {
					return errors
				}
				if k0 == .struct_t && k1 == .struct_t {
					return errors
				}
				if (k0 == .struct_t && k1 == .int_t) || (k0 == .int_t && k1 == .struct_t) {
					return errors
				}
				errors << VerifyError{
					msg:      'binary op operands have mismatched types: ${t0} (${k0}) vs ${t1} (${k1})'
					func_id:  func_id
					block_id: blk_id
					val_id:   val_id
				}
			}
		}
	}
	return errors
}

// verify_load validates verify load state for optimize.
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 {
			if m.type_store.types[ptr_typ_id].kind != .ptr_t {
				errors << VerifyError{
					msg:      'load operand should be pointer type, got ${m.type_store.types[ptr_typ_id].kind}'
					func_id:  func_id
					block_id: blk_id
					val_id:   val_id
				}
			}
		}
	}
	return errors
}

// verify_store validates verify store state for optimize.
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 {
			if m.type_store.types[ptr_typ_id].kind != .ptr_t {
				errors << VerifyError{
					msg:      'store destination should be pointer type, got ${m.type_store.types[ptr_typ_id].kind}'
					func_id:  func_id
					block_id: blk_id
					val_id:   val_id
				}
			}
		}
	}
	return errors
}

// verify_phi validates verify phi state for optimize.
fn verify_phi(m &ssa.Module, func_id int, blk_id int, val_id int, instr ssa.Instruction) []VerifyError {
	mut errors := []VerifyError{}
	if instr.operands.len % 2 != 0 {
		errors << VerifyError{
			msg:      'phi has odd number of operands (${instr.operands.len}), expected (value, block) pairs'
			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
	}
	blk := m.blocks[blk_id]
	for i := 0; i < instr.operands.len; i += 2 {
		val_in := instr.operands[i]
		pred_blk_id := int(instr.operands[i + 1])
		if val_in < 0 || 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
			}
		}
		if pred_blk_id < 0 || pred_blk_id >= m.blocks.len {
			errors << VerifyError{
				msg:      'phi operand ${i + 1} has invalid block id ${pred_blk_id}'
				func_id:  func_id
				block_id: blk_id
				val_id:   val_id
			}
		} else if blk.preds.len > 0 && 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
			}
		}
	}
	if blk.preds.len > 0 {
		actual_pairs := instr.operands.len / 2
		if actual_pairs != blk.preds.len {
			errors << VerifyError{
				msg:      'phi has ${actual_pairs} operand pairs but block has ${blk.preds.len} predecessors'
				func_id:  func_id
				block_id: blk_id
				val_id:   val_id
			}
		}
	}
	return errors
}

// verify_branch validates verify branch state for optimize.
fn verify_branch(m &ssa.Module, func_id int, blk_id int, val_id int, instr ssa.Instruction) []VerifyError {
	mut errors := []VerifyError{}
	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
	}
	for i in [1, 2] {
		b := int(instr.operands[i])
		if b < 0 || b >= m.blocks.len {
			errors << VerifyError{
				msg:      'br operand ${i} has invalid block id ${b}'
				func_id:  func_id
				block_id: blk_id
				val_id:   val_id
			}
		}
	}
	return errors
}

// verify_jump validates verify jump state for optimize.
fn verify_jump(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:      'jmp has ${instr.operands.len} operands, expected 1 (target_blk)'
			func_id:  func_id
			block_id: blk_id
			val_id:   val_id
		}
		return errors
	}
	b := int(instr.operands[0])
	if b < 0 || b >= m.blocks.len {
		errors << VerifyError{
			msg:      'jmp operand has invalid block id ${b}'
			func_id:  func_id
			block_id: blk_id
			val_id:   val_id
		}
	}
	return errors
}

// verify_switch validates verify switch state for optimize.
fn verify_switch(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:      '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
	}
	def_blk := int(instr.operands[1])
	if def_blk < 0 || def_blk >= m.blocks.len {
		errors << VerifyError{
			msg:      'switch default has invalid block id ${def_blk}'
			func_id:  func_id
			block_id: blk_id
			val_id:   val_id
		}
	}
	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
		}
	}
	for i := 3; i < instr.operands.len; i += 2 {
		b := int(instr.operands[i])
		if b < 0 || b >= m.blocks.len {
			errors << VerifyError{
				msg:      'switch case has invalid block id ${b}'
				func_id:  func_id
				block_id: blk_id
				val_id:   val_id
			}
		}
	}
	return errors
}

// verify_cfg_consistency validates verify cfg consistency state for optimize.
fn verify_cfg_consistency(m &ssa.Module, func_id int, blk_id int) []VerifyError {
	mut errors := []VerifyError{}
	blk := m.blocks[blk_id]
	if blk.succs.len == 0 && blk.preds.len == 0 {
		return errors
	}
	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
			}
		}
	}
	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
			}
		}
	}
	return errors
}

// verify_dominance validates verify dominance state for optimize.
fn verify_dominance(m &ssa.Module, func ssa.Function) []VerifyError {
	mut errors := []VerifyError{}
	mut def_block := map[int]int{}
	for param_id in func.params {
		if func.blocks.len > 0 {
			def_block[param_id] = func.blocks[0]
		}
	}
	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
		}
	}

	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 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]
			// Phi operands legitimately come from predecessors, not dominators.
			if instr.op == .phi {
				continue
			}
			for i, op_id in instr.value_operands() {
				if op_id >= m.values.len {
					continue
				}
				op_val := m.values[op_id]
				if op_val.kind in [.basic_block, .constant, .global, .string_literal,
					.c_string_literal, .func_ref, .argument] {
					continue
				}
				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 supports dominates handling for optimize.
fn dominates(m &ssa.Module, _func ssa.Function, a int, b int) bool {
	if a == b {
		return true
	}
	mut curr := b
	for {
		if curr < 0 || curr >= m.blocks.len {
			return false
		}
		idom := m.blocks[curr].idom
		if idom < 0 {
			return false
		}
		if idom == curr {
			return a == curr
		}
		if idom == a {
			return true
		}
		curr = idom
	}
	return false
}

// verify_use_def_chains validates verify use def chains state for optimize.
fn verify_use_def_chains(m &ssa.Module) []VerifyError {
	mut errors := []VerifyError{}
	mut expected_uses := map[int]map[int]bool{}
	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.value_operands() {
					if op_id >= 0 && 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
					}
				}
			}
		}
	}
	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
				}
			}
		}
	}
	return errors
}