pub mod verify;

//! RIL type verifier.

//!

//! Walks each function's blocks and checks pointer-provenance rules:

//!

//! 1. Every register is assigned a type (W8/W16/W32/W64/Ptr) based on

//!    its defining instruction.

//! 2. Load/Store/Blit base registers must have type Ptr.

//! 3. WordToPtr is flagged as a provenance violation.

//! 4. BinOp::Add with Ptr type requires exactly one Ptr operand.

//! 5. Copy(DataSym)/Copy(FnAddr) produces Ptr; Copy(Imm) produces W64.

//! 6. Reserve always produces Ptr.

use std::fmt;

use std::io;

use std::lang::alloc;

/// Maximum SSA registers per function (must match regalloc).

const MAX_REGS: u32 = 8192;

/// A verification error found in an IL function.

pub record VerifyError {

    /// Name of the function containing the error.

    fnName: *[u8],

    /// Block index where the error occurred.

    blockIdx: u32,

    /// Instruction index within the block.

    instrIdx: u32,

    /// Description of the error.

    message: *[u8],

}

/// Result of verifying a program.

pub record VerifyResult {

    /// Errors found during verification.

    errors: *mut [VerifyError],

    /// Number of WordToPtr instructions found (provenance escapes).

    wtpCount: u32,

}

/// Verify pointer-type safety of an IL program.

///

/// Returns a list of errors. An empty list means the program passes

/// all checks. WordToPtr instructions are counted but not treated as

/// errors (they are legal in unsafe code).

pub fn verifyProgram(program: *super::Program, arena: *mut alloc::Arena) -> VerifyResult {

    let a = alloc::arenaAllocator(arena);

    let mut errors: *mut [VerifyError] = &mut [];

    let mut wtpCount: u32 = 0;

    for func in program.fns {

        if func.isExtern {

            continue;

        }

        verifyFn(func, &mut errors, &mut wtpCount, a);

    }

    return VerifyResult { errors, wtpCount };

}

/// Inferred type of an SSA register: either a word width or pointer.

union RegType {

    /// Not yet defined.

    Undef,

    /// Word type (W8, W16, W32, W64).

    Word(super::Type),

    /// Pointer type.

    Ptr,

}

/// Check if a register type is Ptr.

fn isPtr(t: RegType) -> bool {

    if let case RegType::Ptr = t { return true; }

    return false;

}

/// Infer the type of a Val without looking at the register map.

/// Returns nil for Reg values (caller must look up the map).

fn valType(val: super::Val) -> ?RegType {

    match val {

        case super::Val::Imm(_) => return RegType::Word(super::Type::W64),

        case super::Val::DataSym(_),

             super::Val::FnAddr(_) => return RegType::Ptr,

        case super::Val::Undef => return RegType::Word(super::Type::W64),

        case super::Val::Reg(_) => return nil,

    }

}

/// Look up the type of a Val, consulting the register map for Reg values.

fn resolveValType(val: super::Val, regs: *[RegType]) -> RegType {

    if let vt = valType(val) {

        return vt;

    }

    let case super::Val::Reg(r) = val else return RegType::Word(super::Type::W64);

    if r.n < regs.len {

        return regs[r.n];

    }

    return RegType::Undef;

}

/// Verify a single function.

fn verifyFn(

    func: *super::Fn,

    errors: *mut *mut [VerifyError],

    wtpCount: *mut u32,

    a: alloc::Allocator,

) {

    // Type map: regId -> RegType.

    let mut regTypes: [RegType; MAX_REGS] = undefined;

    for i in 0..MAX_REGS {

        regTypes[i] = RegType::Undef;

    }

    // Type function parameters.

    for param in func.params {

        if param.value.n < MAX_REGS {

            if let case super::Type::Ptr = param.type {

                regTypes[param.value.n] = RegType::Ptr;

            } else {

                regTypes[param.value.n] = RegType::Word(param.type);

            }

        }

    }

    // Walk blocks.

    for block, blockIdx in func.blocks {

        // Type block parameters.

        for param in block.params {

            if param.value.n < MAX_REGS {

                if let case super::Type::Ptr = param.type {

                    regTypes[param.value.n] = RegType::Ptr;

                } else {

                    regTypes[param.value.n] = RegType::Word(param.type);

                }

            }

        }

        // Check each instruction.

        for instr, instrIdx in block.instrs {

            verifyInstr(

                func, blockIdx as u32, instrIdx as u32,

                instr, &mut regTypes[..], errors, wtpCount, a,

            );

        }

    }

}

/// Verify a single instruction: assign dst type and check operands.

fn verifyInstr(

    func: *super::Fn,

    blockIdx: u32,

    instrIdx: u32,

    instr: super::Instr,

    regs: *mut [RegType],

    errors: *mut *mut [VerifyError],

    wtpCount: *mut u32,

    a: alloc::Allocator,

) {

    match instr {

        case super::Instr::Reserve { dst, .. } => {

            // Reserve always produces a pointer.

            setReg(regs, dst, RegType::Ptr);

        }

        case super::Instr::Load { typ, dst, src, .. } => {

            // Base must be Ptr.

            checkPtrBase(func, blockIdx, instrIdx, regs, src, errors, a, "load base");

            // Result type depends on the load type.

            if let case super::Type::Ptr = typ {

                setReg(regs, dst, RegType::Ptr);

            } else {

                setReg(regs, dst, RegType::Word(typ));

            }

        }

        case super::Instr::Sload { typ, dst, src, .. } => {

            checkPtrBase(func, blockIdx, instrIdx, regs, src, errors, a, "sload base");

            if let case super::Type::Ptr = typ {

                setReg(regs, dst, RegType::Ptr);

            } else {

                setReg(regs, dst, RegType::Word(typ));

            }

        }

        case super::Instr::Store { dst, .. } => {

            checkPtrBase(func, blockIdx, instrIdx, regs, dst, errors, a, "store base");

        }

        case super::Instr::Blit { dst, src, .. } => {

            checkPtrBase(func, blockIdx, instrIdx, regs, dst, errors, a, "blit dst");

            checkPtrBase(func, blockIdx, instrIdx, regs, src, errors, a, "blit src");

        }

        case super::Instr::Copy { dst, val } => {

            // Type depends on the value being copied.

            let vt = resolveValType(val, regs);

            setReg(regs, dst, vt);

        }

        case super::Instr::BinOp { op, typ, dst, a: va, b: vb } => {

            if let case super::Type::Ptr = typ {

                // Pointer arithmetic: result is Ptr.

                // Check that exactly one operand is Ptr.

                let aIsPtr = isPtr(resolveValType(va, regs));

                let bIsPtr = isPtr(resolveValType(vb, regs));

                if let case super::BinOp::Add = op {

                    if not (aIsPtr or bIsPtr) {

                        emitError(func, blockIdx, instrIdx, errors, a,

                            "ptr add: neither operand is Ptr");

                    }

                }

                setReg(regs, dst, RegType::Ptr);

            } else {

                setReg(regs, dst, RegType::Word(typ));

            }

        }

        case super::Instr::UnOp { typ, dst, .. } => {

            setReg(regs, dst, RegType::Word(typ));

        }

        case super::Instr::Zext { dst, .. } => {

            setReg(regs, dst, RegType::Word(super::Type::W64));

        }

        case super::Instr::Sext { dst, .. } => {

            setReg(regs, dst, RegType::Word(super::Type::W64));

        }

        case super::Instr::PtrToWord { dst, .. } => {

            setReg(regs, dst, RegType::Word(super::Type::W64));

        }

        case super::Instr::WordToPtr { dst, .. } => {

            // Count provenance escapes.

            *wtpCount += 1;

            setReg(regs, dst, RegType::Ptr);

        }

        case super::Instr::Call { retTy, dst, .. } => {

            if let d = dst {

                if let case super::Type::Ptr = retTy {

                    setReg(regs, d, RegType::Ptr);

                } else {

                    setReg(regs, d, RegType::Word(retTy));

                }

            }

        }

        case super::Instr::Ecall { dst, .. } => {

            // Ecall returns a word value.

            setReg(regs, dst, RegType::Word(super::Type::W64));

        }

        case super::Instr::Ret { .. },

             super::Instr::Jmp { .. },

             super::Instr::Br { .. },

             super::Instr::Switch { .. },

             super::Instr::Unreachable,

             super::Instr::Ebreak => {}

    }

}

/// Set a register's type in the map.

fn setReg(regs: *mut [RegType], reg: super::Reg, typ: RegType) {

    if reg.n < regs.len {

        regs[reg.n] = typ;

    }

}

/// Check that a register used as a memory base has type Ptr.

fn checkPtrBase(

    func: *super::Fn,

    blockIdx: u32,

    instrIdx: u32,

    regs: *[RegType],

    reg: super::Reg,

    errors: *mut *mut [VerifyError],

    a: alloc::Allocator,

    context: *[u8],

) {

    if reg.n >= regs.len {

        return;

    }

    if not isPtr(regs[reg.n]) {

        emitError(func, blockIdx, instrIdx, errors, a, context);

    }

}

/// Record a verification error.

fn emitError(

    func: *super::Fn,

    blockIdx: u32,

    instrIdx: u32,

    errors: *mut *mut [VerifyError],

    a: alloc::Allocator,

    message: *[u8],

) {

    errors.append(VerifyError {

        fnName: func.name,

        blockIdx,

        instrIdx,

        message,

    }, a);

}

/// Print verification results to stderr.

pub fn printResult(result: *VerifyResult) {

    if result.errors.len == 0 and result.wtpCount == 0 {

        io::printError("verify: ok\n");

        return;

    }

    let mut buf: [u8; 10] = undefined;

    if result.wtpCount > 0 {

        io::printError("verify: ");

        io::printError(fmt::formatU32(result.wtpCount, &mut buf[..]));

        io::printError(" WordToPtr instruction(s) found\n");

    }

    for err in result.errors {

        io::printError("verify: ");

        io::printError(err.fnName);

        io::printError(" block ");

        io::printError(fmt::formatU32(err.blockIdx, &mut buf[..]));

        io::printError(" instr ");

        io::printError(fmt::formatU32(err.instrIdx, &mut buf[..]));

        io::printError(": ");

        io::printError(err.message);

        io::printError("\n");

    }

}

lib/std/lang/il/verify.rad