410 lines
15 KiB
Plaintext
410 lines
15 KiB
Plaintext
import t, c
|
|
from stdint import *
|
|
import string
|
|
import viperlib
|
|
import memhub
|
|
from linkedlist import GSListNode, GSList
|
|
from .__function import Function, BasicBlock, Line, Param
|
|
from .__module import LLVMModule
|
|
|
|
|
|
# ============================================================
|
|
# SSA verifier
|
|
#
|
|
# Isomorphic to llvmlite **name for name and semantically identical**: it verifies the **structured internal model + intermediate instruction
|
|
# text** (the %N definitions/uses produced by the builders, block termination, phi placement),
|
|
# independent of the rendered MLIR text -- MLIR validity is the responsibility of mlir-opt/mlir-translate.
|
|
#
|
|
# Checks:
|
|
# 1. Block termination: every basic block must end with a terminator (ret/br/switch/unreachable)
|
|
# 2. SSA uniqueness: every %name may be defined only once
|
|
# 3. Undefined references: every %name use must have a matching definition
|
|
# 4. Phi placement: a phi instruction may appear only at the head of a block (before any non-phi instruction)
|
|
# ============================================================
|
|
|
|
# Error codes
|
|
define VERIFY_OK = 0
|
|
define VERIFY_ERR_NO_TERMINATOR = 1
|
|
define VERIFY_ERR_DUPLICATE_DEF = 2
|
|
define VERIFY_ERR_UNDEFINED_USE = 3
|
|
define VERIFY_ERR_PHI_NOT_FIRST = 4
|
|
|
|
|
|
# ============================================================
|
|
# NameEntry: defined SSA name entry (linked-list node)
|
|
#
|
|
# NOTE: must carry novirtual (see the Line comment in __function.vp).
|
|
# ============================================================
|
|
novirtual class NameEntry(GSListNode[NameEntry]):
|
|
Name: str # SSA name (e.g. "%0"/"%result")
|
|
|
|
|
|
# ============================================================
|
|
# VerifyResult: verification result
|
|
# ============================================================
|
|
class VerifyResult:
|
|
ErrorCount: int # total error count
|
|
WarningCount: int # total warning count
|
|
ErrorCode: int # first error code
|
|
ErrorBuf: str # error message buffer
|
|
ErrorBufSize: sizet # buffer size
|
|
|
|
|
|
# ============================================================
|
|
# Helper functions
|
|
# ============================================================
|
|
def _new_verify_result(pool: memhub.MemBuddy*,
|
|
buf_size: sizet) -> VerifyResult*:
|
|
"""Create a VerifyResult object"""
|
|
ptr: VerifyResult* = pool.alloc(VerifyResult.__sizeof__())
|
|
if ptr is None: return None
|
|
string.memset(ptr, 0, VerifyResult.__sizeof__())
|
|
ptr.ErrorCount = 0
|
|
ptr.WarningCount = 0
|
|
ptr.ErrorCode = VERIFY_OK
|
|
buf: str = pool.alloc(buf_size)
|
|
if buf is not None:
|
|
buf[0] = '\0'
|
|
ptr.ErrorBuf = buf
|
|
ptr.ErrorBufSize = buf_size
|
|
return ptr
|
|
|
|
|
|
def _report_error(result: VerifyResult*, code: int, msg: str):
|
|
"""Record one error"""
|
|
if result is None: return
|
|
result.ErrorCount += 1
|
|
if result.ErrorCode == VERIFY_OK:
|
|
result.ErrorCode = code
|
|
if result.ErrorBuf is not None and msg is not None:
|
|
_append_cstr(result.ErrorBuf, result.ErrorBufSize, msg)
|
|
_append_cstr(result.ErrorBuf, result.ErrorBufSize, "\n")
|
|
|
|
|
|
# _append_cstr write-position cache: O(1) append into the same buffer, avoiding
|
|
# O(n^2) strlen(dst) rescans; falls back to strlen on buffer switch or reset.
|
|
_g_last_dst: uint64 = 0
|
|
_g_last_pos: sizet = 0
|
|
|
|
def _append_cstr(dst: str, dst_size: sizet, src: str):
|
|
"""Append src to the end of dst"""
|
|
global _g_last_dst, _g_last_pos
|
|
if dst is None or src is None: return
|
|
dlen: sizet = 0
|
|
if _g_last_dst == uint64(dst):
|
|
dlen = _g_last_pos
|
|
# Buffer reset (caller reuses same address after buf[0]=0) -> restart from head
|
|
if dlen > 0 and dst[0] == '\0':
|
|
dlen = 0
|
|
# Cache-consistency check (same as __module/__function): a stale cached pos would append
|
|
# past the first NUL and hide content; fall back to strlen on failure, hot path stays O(1).
|
|
if dlen == 0:
|
|
if dst[0] != '\0':
|
|
dlen = string.strlen(dst)
|
|
elif dst[dlen] != '\0' or dst[dlen - 1] == '\0':
|
|
dlen = string.strlen(dst)
|
|
else:
|
|
dlen = string.strlen(dst)
|
|
_g_last_dst = uint64(dst)
|
|
# Unsigned-underflow guard: if dlen exceeds the buffer size (corrupted/dangling buffer),
|
|
# return; otherwise remain = dst_size - dlen underflows and writes out of bounds.
|
|
if dlen >= dst_size:
|
|
return
|
|
slen: sizet = string.strlen(src)
|
|
remain: sizet = dst_size - dlen
|
|
if remain <= 0: return
|
|
i: sizet = 0
|
|
while i < slen and i + 1 < remain:
|
|
dst[dlen + i] = src[i]
|
|
i += 1
|
|
dst[dlen + i] = '\0'
|
|
_g_last_pos = dlen + i
|
|
|
|
|
|
# ============================================================
|
|
# SSA name-table operations
|
|
# ============================================================
|
|
def _new_name_table(pool: memhub.MemBuddy*) -> GSList[NameEntry]*:
|
|
"""Create an empty name table"""
|
|
gsl: GSList[NameEntry]* = pool.alloc(24) # GSList: Head+Tail+Count
|
|
if gsl is None: return None
|
|
string.memset(gsl, 0, 24)
|
|
return gsl
|
|
|
|
|
|
# NameEntry hardcoded size: Next(8) + Name(8) = 16 bytes
|
|
define NENTRY_SIZE = 16
|
|
|
|
def _name_table_add(table: GSList[NameEntry]*,
|
|
pool: memhub.MemBuddy*,
|
|
name: str) -> int:
|
|
"""Add a name to the table. Returns 1=duplicate, 0=added"""
|
|
if table is None or name is None: return 0
|
|
# Check for duplicates
|
|
cur: NameEntry* = table.Head
|
|
while cur is not None:
|
|
if string.strcmp(cur.Name, name) == 0:
|
|
return 1
|
|
cur = cur.Next
|
|
# Add new entry
|
|
entry: NameEntry* = pool.alloc(NENTRY_SIZE)
|
|
if entry is None: return 0
|
|
string.memset(entry, 0, NENTRY_SIZE)
|
|
entry.Name = name
|
|
table.append(entry)
|
|
return 0
|
|
|
|
|
|
def _name_table_contains(table: GSList[NameEntry]*,
|
|
name: str) -> int:
|
|
"""Return 1 if name is in the table, else 0"""
|
|
if table is None or name is None: return 0
|
|
cur: NameEntry* = table.Head
|
|
while cur is not None:
|
|
if string.strcmp(cur.Name, name) == 0:
|
|
return 1
|
|
cur = cur.Next
|
|
return 0
|
|
|
|
|
|
# ============================================================
|
|
# Text analysis helpers
|
|
# ============================================================
|
|
def _is_char_name(ch: char) -> int:
|
|
"""Return 1 if ch is a SSA name char [a-zA-Z0-9._]"""
|
|
if ch >= 'a' and ch <= 'z': return 1
|
|
if ch >= 'A' and ch <= 'Z': return 1
|
|
if ch >= '0' and ch <= '9': return 1
|
|
if ch == '.' or ch == '_': return 1
|
|
return 0
|
|
|
|
|
|
def _extract_def_name(pool: memhub.MemBuddy*,
|
|
text: str) -> str:
|
|
"""Extract the defined SSA name from "%<name> = <instruction>".
|
|
Returns an allocated NUL-terminated name (e.g. "%0"), or None if not a definition line.
|
|
"""
|
|
if text is None: return None
|
|
if text[0] != '%': return None
|
|
# Scan for the " = " pattern
|
|
i: int = 1
|
|
while text[i] != '\0':
|
|
if text[i] == ' ' and text[i + 1] == '=' and text[i + 2] == ' ':
|
|
# Found " = " at position i
|
|
name_len: int = int(i)
|
|
name: str = pool.alloc(name_len + 1)
|
|
if name is None: return None
|
|
for j in range(int(name_len)):
|
|
name[j] = text[j]
|
|
name[name_len] = '\0'
|
|
return name
|
|
i += 1
|
|
return None
|
|
|
|
|
|
def _is_terminator(text: str) -> int:
|
|
"""Return 1 if text is a terminator instruction"""
|
|
if text is None: return 0
|
|
if string.strncmp(text, "ret", 3) == 0: return 1
|
|
if string.strncmp(text, "br ", 3) == 0: return 1
|
|
if string.strncmp(text, "switch ", 7) == 0: return 1
|
|
if string.strncmp(text, "unreachable", 11) == 0: return 1
|
|
if string.strncmp(text, "indirectbr ", 11) == 0: return 1
|
|
if string.strncmp(text, "resume ", 7) == 0: return 1
|
|
return 0
|
|
|
|
|
|
def _is_phi(text: str) -> int:
|
|
"""Return 1 if text is a phi instruction"""
|
|
if text is None: return 0
|
|
if string.strstr(text, " = phi ") is not None: return 1
|
|
return 0
|
|
|
|
|
|
def _check_uses_in_line(table: GSList[NameEntry]*,
|
|
text: str,
|
|
def_name: str) -> int:
|
|
"""Check that all SSA name uses in the line are defined.
|
|
Skips def_name; returns the number of undefined uses.
|
|
"""
|
|
if text is None: return 0
|
|
i: int = 0
|
|
undef_count: int = 0
|
|
while text[i] != '\0':
|
|
if text[i] == '%':
|
|
# Extract name
|
|
name_start: int = int(i)
|
|
i += 1
|
|
while text[i] != '\0' and _is_char_name(text[i]) == 1:
|
|
i += 1
|
|
name_len: int = int(i - name_start)
|
|
if name_len > 1:
|
|
# Build no temp string (no stack alloc); compare char by char.
|
|
if _name_matches_at(text, name_start, name_len, table) == 0:
|
|
# Check whether this is def_name (the definition site itself)
|
|
if def_name is not None:
|
|
if _str_matches_at(text, name_start, name_len, def_name) == 0:
|
|
undef_count += 1
|
|
else:
|
|
undef_count += 1
|
|
else:
|
|
i += 1
|
|
return undef_count
|
|
|
|
|
|
def _name_matches_at(text: str, start: int, length: int,
|
|
table: GSList[NameEntry]*) -> int:
|
|
"""Return 1 if text[start:start+length] matches an entry in the name table, else 0."""
|
|
if table is None: return 0
|
|
cur: NameEntry* = table.Head
|
|
while cur is not None:
|
|
if cur.Name is not None:
|
|
if _str_matches_at(text, start, length, cur.Name) == 1:
|
|
return 1
|
|
cur = cur.Next
|
|
return 0
|
|
|
|
|
|
def _str_matches_at(text: str, start: int, length: int,
|
|
target: str) -> int:
|
|
"""Return 1 if text[start:start+length] equals target, else 0."""
|
|
if text is None or target is None: return 0
|
|
# Check target length
|
|
target_len: sizet = string.strlen(target)
|
|
if target_len != length: return 0
|
|
for i in range(int(length)):
|
|
if text[start + i] != target[i]: return 0
|
|
return 1
|
|
|
|
|
|
# ============================================================
|
|
# Main verification functions
|
|
# ============================================================
|
|
def verify_function(pool: memhub.MemBuddy*,
|
|
func: Function*,
|
|
result: VerifyResult*) -> int:
|
|
"""Verify a function's SSA correctness; result must be created via
|
|
_new_verify_result. Returns the error count (0 = pass).
|
|
"""
|
|
if func is None or result is None: return 1
|
|
|
|
# Create name table
|
|
name_table: GSList[NameEntry]* = _new_name_table(pool)
|
|
if name_table is None: return 1
|
|
|
|
# 1. Add function params to the name table (params are defined)
|
|
params: GSList[Param]* = func.Params
|
|
param: Param* = None
|
|
if params is not None:
|
|
param = params.Head
|
|
while param is not None:
|
|
if param.Name is not None:
|
|
_name_table_add(name_table, pool, param.Name)
|
|
param = param.Next
|
|
|
|
# 1b. Add block names to the table (block labels like %then are valid br/phi targets)
|
|
blocks: GSList[BasicBlock]* = func.Blocks
|
|
blk_iter: BasicBlock* = None
|
|
if blocks is not None:
|
|
blk_iter = blocks.Head
|
|
while blk_iter is not None:
|
|
if blk_iter.Name is not None:
|
|
blk_name_len: sizet = string.strlen(blk_iter.Name)
|
|
blk_ref: str = pool.alloc(blk_name_len + 2)
|
|
if blk_ref is not None:
|
|
# Build the "%<name>" string
|
|
blk_ref[0] = '%'
|
|
for k in range(int(blk_name_len)):
|
|
blk_ref[k + 1] = blk_iter.Name[k]
|
|
blk_ref[blk_name_len + 1] = '\0'
|
|
_name_table_add(name_table, pool, blk_ref)
|
|
blk_iter = blk_iter.Next
|
|
|
|
# 2. Walk all blocks
|
|
blk: BasicBlock* = None
|
|
if blocks is not None:
|
|
blk = blocks.Head
|
|
while blk is not None:
|
|
# Check terminator
|
|
if blk.IsTerminated == 0:
|
|
# Also check whether the last line is a terminator
|
|
has_term: int = 0
|
|
line_check: Line* = None
|
|
if blk.Lines is not None:
|
|
lines_check: GSList[Line]* = blk.Lines
|
|
line_check = lines_check.Head
|
|
while line_check is not None:
|
|
if line_check.Buf is not None:
|
|
if _is_terminator(line_check.Buf) == 1:
|
|
has_term = 1
|
|
line_check = line_check.Next
|
|
if has_term == 0:
|
|
blk_name: str = "<unnamed>"
|
|
if blk.Name is not None:
|
|
blk_name = blk.Name
|
|
err_buf: str = pool.alloc(128)
|
|
if err_buf is not None:
|
|
viperlib.snprintf(err_buf, 128, "ERROR: block '%s' missing terminator", blk_name)
|
|
_report_error(result, VERIFY_ERR_NO_TERMINATOR, err_buf)
|
|
|
|
# Walk instruction lines in the block
|
|
seen_non_phi: int = 0
|
|
line: Line* = None
|
|
if blk.Lines is not None:
|
|
lines: GSList[Line]* = blk.Lines
|
|
line = lines.Head
|
|
while line is not None:
|
|
if line.Buf is not None:
|
|
text: str = line.Buf
|
|
|
|
# Check phi position
|
|
if _is_phi(text) == 1:
|
|
if seen_non_phi == 1:
|
|
phi_err: str = pool.alloc(128)
|
|
if phi_err is not None:
|
|
viperlib.snprintf(phi_err, 128, "ERROR: phi not at block start")
|
|
_report_error(result, VERIFY_ERR_PHI_NOT_FIRST, phi_err)
|
|
else:
|
|
# Mark a non-empty non-phi line as seen-non-phi
|
|
if string.strlen(text) > 0:
|
|
seen_non_phi = 1
|
|
|
|
# Extract defined name
|
|
def_name: str = _extract_def_name(pool, text)
|
|
if def_name is not None:
|
|
# Check for duplicate definition
|
|
dup: int = _name_table_add(name_table, pool, def_name)
|
|
if dup == 1:
|
|
dup_err: str = pool.alloc(128)
|
|
if dup_err is not None:
|
|
viperlib.snprintf(dup_err, 128, "ERROR: duplicate definition '%s'", def_name)
|
|
_report_error(result, VERIFY_ERR_DUPLICATE_DEF, dup_err)
|
|
|
|
# Check undefined uses
|
|
undef: int = _check_uses_in_line(name_table, text, def_name)
|
|
if undef > 0:
|
|
use_err: str = pool.alloc(128)
|
|
if use_err is not None:
|
|
viperlib.snprintf(use_err, 128, "ERROR: %d undefined use(s) in: %s", undef, text)
|
|
_report_error(result, VERIFY_ERR_UNDEFINED_USE, use_err)
|
|
|
|
line = line.Next
|
|
|
|
blk = blk.Next
|
|
|
|
return result.ErrorCount
|
|
|
|
|
|
def verify_module(pool: memhub.MemBuddy*, mod: LLVMModule*, result: VerifyResult*) -> int:
|
|
"""Verify SSA correctness of all functions in the module.
|
|
Returns the total error count.
|
|
"""
|
|
if mod is None or result is None: return 1
|
|
func: Function* = mod.FuncHead
|
|
while func is not None:
|
|
if func.IsDeclared == 0:
|
|
# Verify only definitions with a body; skip declarations
|
|
verify_function(pool, func, result)
|
|
func = func.Next
|
|
return result.ErrorCount
|