IR 验证器 (Verifier)¶
可扩展的验证系统，通过可插拔属性验证器和诊断报告来验证 PyPTO 中间表示 (IR) 的正确性，并与 Pass 系统集成。
概述¶
| 组件 | 描述 |
|---|---|
| PropertyVerifier (C++) | 验证规则的基类 |
| PropertyVerifierRegistry (C++) | IRProperty → PropertyVerifier 工厂的单例映射，提供验证/报告 API |
| Diagnostic | 结构化的错误/警告报告，包含严重级别、位置和消息 |
| VerificationError | 验证失败时抛出的异常 |
关键特性¶
- 可插拔规则系统：可通过自定义验证规则进行扩展
- 基于属性的验证：选择性属性集——精确验证所需内容
- 结构性属性 (Structural Properties)：TypeChecked、BreakContinueValid、NoRedundantBlocks、UseAfterDef、OutParamNotShadowed、NoNestedInCore、InOutUseValid、PipelineLoopValid、ArrayNotEscaped 和 ManualDepsOnSubmitOnly 由
VerificationInstrument在每个 Pass 执行前后验证；在流水线启动时，PassPipeline仅验证与GetVerifiedProperties()共有的轻量子集 - 双重验证模式：收集诊断信息或在首个错误时抛出异常
- Pass 集成：可作为优化流水线中的 Pass 使用
- 全面的诊断信息：收集所有问题及源码位置
架构¶
结构性属性 vs 流水线属性¶
| 类别 | 示例 | 行为 |
|---|---|---|
| 结构性 | TypeChecked, BreakContinueValid, NoRedundantBlocks, UseAfterDef, OutParamNotShadowed, NoNestedInCore, InOutUseValid, PipelineLoopValid, ArrayNotEscaped, ManualDepsOnSubmitOnly | 始终为真。由 VerificationInstrument 在每个 Pass 执行前后验证；与 GetVerifiedProperties() 共有的子集还会在流水线启动时验证。不在 PassProperties 中声明。 |
| 流水线 | SSAForm, NoNestedCalls, HasMemRefs, ... | 由 Pass 产生/失效。按 Pass 声明的契约验证。 |
GetStructuralProperties() 返回 {TypeChecked, BreakContinueValid, NoRedundantBlocks, UseAfterDef, OutParamNotShadowed, NoNestedInCore, InOutUseValid, PipelineLoopValid, ArrayNotEscaped, ManualDepsOnSubmitOnly}。这些由 VerificationInstrument 在每个 Pass 执行前后验证。在流水线启动时，PassPipeline::Run() 仅额外验证与 GetVerifiedProperties() 共有的轻量子集（GetStructuralProperties().Intersection(GetVerifiedProperties())）——因此例如 ArrayNotEscaped 会在每个 Pass 前后验证，但不会在流水线启动时验证。由于没有 Pass 在 required/produced/invalidated 中声明它们，VerificationInstrument 将它们与 Pass 声明的属性合并，确保没有 Pass 破坏这些基本不变量。
验证规则系统¶
验证器使用插件架构，每个 PropertyVerifier 子类是一个独立的规则：
- 规则按注册顺序在所有函数上运行
- 每个规则独立运行——一个规则的失败不影响其他规则
- 规则接收
ProgramPtr，并在内部决定是遍历函数还是检查程序级属性 - 可以通过
IRPropertySet选择性地包含规则
诊断系统¶
| 字段 | 类型 | 用途 |
|---|---|---|
severity |
DiagnosticSeverity |
错误或警告 |
rule_name |
string |
检测到问题的规则 |
error_code |
int |
数字错误标识符 |
message |
string |
人类可读的描述 |
span |
Span |
源码位置信息 |
与 Pass 系统的集成¶
- 自动属性验证：
PassPipeline使用PropertyVerifierRegistry在每个 Pass 执行后检查产生的属性（由PassContext中的VerificationLevel控制）。与GetVerifiedProperties()共有的轻量结构性属性子集在流水线启动时检查。详见 Pass 管理器。 VerificationInstrument：一个PassInstrument，通过PassContext验证属性。在每个 Pass 执行前，检查 Pass 声明的required属性。在每个 Pass 执行后，检查 Pass 声明的produced属性加上所有结构性属性——确保没有 Pass 破坏基本的 IR 不变量。
run_verifier() 工具函数创建一个独立的 Pass，用于自定义流水线中的临时使用，但它不是默认优化策略的一部分。
内置规则¶
| 规则名称 | IRProperty | 用途 |
|---|---|---|
| SSAVerify | SSAForm | 无多重赋值、无名称遮蔽、无缺失 yield、作用域违规、基数检查 |
| TypeCheck | TypeChecked | 类型种类/数据类型/形状/大小一致性 |
| NoNestedCall | NoNestedCalls | 参数、条件、范围中无嵌套调用表达式 |
| BreakContinueCheck | BreakContinueValid | break/continue 仅在顺序/while 循环中 |
| UseAfterDefCheck | UseAfterDef | 每个 Var 使用均由定义支配（参数、AssignStmt、循环变量、iter_arg、return_var） |
| NormalizedStmtStructure | NormalizedStmtStructure | 展平嵌套 SeqStmts 并解包单子节点 SeqStmts |
| NoRedundantBlocks | NoRedundantBlocks | 无单子节点或嵌套的 SeqStmts |
| SplitIncoreOrch | SplitIncoreOrch | Opaque 函数中不残留 InCoreScopeStmt 节点 |
| IncoreTileOps | IncoreTileOps | InCore 函数使用 tile 操作（无张量级操作残留） |
| HasMemRefs | HasMemRefs | 所有 TileType 变量已初始化 MemRef |
| AllocatedMemoryAddr | AllocatedMemoryAddr | 所有 MemRef 在缓冲区限制内具有有效地址 |
| OutParamNotShadowed | OutParamNotShadowed | Out/InOut 参数未被张量创建操作重新赋值 |
| NoNestedInCore | NoNestedInCore | 无嵌套 InCore 作用域（InCoreScopeStmt 内含 InCoreScopeStmt） |
| InOutUseValid | InOutUseValid | 作为 InOut/Out 传入用户函数调用的变量，在调用之后不得再被读取（RFC #1026）。Group 类型函数体目前跳过，待后续完善。 |
| PipelineLoopValid | PipelineLoopValid | 每个 ForStmt 上的双向不变量：kind_ == ForKind::Pipeline ⇔ 含有 pipeline_stages 属性。任一方向失败即表示 pipeline 循环格式错误。 |
| ArrayNotEscaped | ArrayNotEscaped | ArrayType 不得作为任何函数参数或返回类型出现（会通过 TupleType 递归检查）。ArrayType 是归属于所在函数的片上标量寄存器堆 / C 栈存储——让它跨越函数边界会泄漏栈指针，因此只能在函数体内创建并就地使用。 |
| ManualDepsOnSubmitOnly | ManualDepsOnSubmitOnly | 任何普通跨函数 Call（GlobalVar callee）都不得携带 attrs["manual_dep_edges"]——手动依赖边只存在于类型化的 Submit::deps_ 字段中。Op call（system.task_dummy）作为 codegen fanin 契约保留该 attr，属于豁免。 |
| OrchestrationReferencesResolved | OrchestrationReferencesResolved | FunctionType::Orchestration 函数体内每一个非 builtin Call 必须对应到 Program 中存在的 Function。取代 codegen 端原本在生成时抛错的 ValidateOrchestrationReferences 遍历。 |
| AssignTypeSymmetry | AssignTypeSymmetry | 每个 AssignStmt(var, value) 满足 structural_equal(var.type, value.type)。覆盖 dtype、shape 以及 tile_view/tensor_view；此外比较 TileType 的 memory_space（TensorType 没有 memory_space）和 DistributedTensorType 的 window_buffer；元组赋值逐元素递归比较。不包含 memref_——structural_equal 将其视为绑定在 Var 上的内存分配细节，由 HasMemRefs / AllocatedMemoryAddr 负责。用于捕获只修改赋值一侧类型的 Pass（例如 #1262 的 TileType memory_space、#1278 的 tile_view）。已在 PropertyVerifierRegistry 注册，但尚未加入 GetStructuralProperties()——可通过 PropertyVerifierRegistry::verify 或将该属性加入 VerificationInstrument 按需运行。 |
| AivSplitValid | AivSplitValid | 针对一等公民 SplitAivScopeStmt 区域的结构性检查，以该节点本身为准（因此嵌套 / 多模式函数会逐区域检查）。(a) 数据并行区域内不得有 cube 计算——每个 AIV lane 只持有半块 tile，matmul 无法被向量切分。(b) 不得有在切分轴上折叠的向量归约（tile.row_* / tile.col_* / tile.sum / tile.max / tile.min）——它会产生每 lane 的部分结果（错误编译）。(c) aiv_shard / aic_gather 必须出现在区域内部（tile.* 与面向作者的 tensor.* 两种形式皆然），且不得出现在任务并行的 mode=NONE 区域中——该模式没有可切分的轴。(d) 边界内存契约：tile.aiv_shard 为 Acc → Vec，tile.aic_gather 为 Vec → Mat。这两个算子本身就是跨核传输，因此操作数必须位于生产侧 lane、结果必须位于消费侧 lane；内存尚未解析前会跳过检查，故同一检查在整个窗口内都安全。由 OutlineIncoreScopes 产生，随后由 ConvertTensorToTileOps 与 InferTileMemorySpace 失效并重新产生，最后由 LowerAutoVectorSplit 失效（后者擦除区域节点）。PassPipeline 只验证产生的属性（passes.cpp），因此正是这两次重新产生才为检查 (d) 提供了真正生效的验证点——在 OutlineIncoreScopes 处边界仍是不带内存空间的 tensor.* 形式，(d) 必然是空转的。被检查的算子都是带非空 op_ 的普通 Call；Submit 会被正确跳过。修复方式：(a) 将 cube 算子移出区域；(b) 在非切分轴上归约，或先用 tile.aic_gather 汇聚回完整 tile；(c) 数据并行折半请使用 UP_DOWN / LEFT_RIGHT；(d) 只对 cube 产出的值做 shard——向量产出的值（pl.load / pl.full）本就位于 AIV lane，应去掉 pl.aiv_shard，交由隐式 affinity 门控的切分来折半。 |
| HardSyncallOccupancy | HardSyncallOccupancyValid | 硬（FFTS）形式的 system.syncall 会等待其 core_type 的每一个物理核到达 barrier，因此外层 SPMD 启动必须同时满足两个独立保证：(1) 满占用——恰好填满这些核（N != required 即报错，覆盖部分占用与超占用）；(2) sync_start=True——所有 block 同时驻留，因为非 sync_start 启动可能分波次派发 block，即便满占用也会使 barrier 死锁。任一缺失都会在设备上死锁（AICore 超时 507018）并使设备残留需复位。由 ExpandMixedKernel 产生（该 Pass 解析出每个被启动 kernel 的 FunctionType——检查所依赖的前提）并列入 GetVerifiedProperties()，故 PassPipeline 在该 Pass 之后立即自动验证一次。覆盖所有块数可被识别的 SPMD 启动点：FunctionType::Spmd 函数（作用域式 pl.spmd）、带 core_num 属性的 FunctionType::Group 函数（pl.cluster() 内嵌 pl.spmd）、以及带 core_num 的 Submit（pl.spmd_submit）。启动宽度分两类：编译期字面量（对照 SoC 物理核数校验），或启动形状查询——pl.system.available_cluster_count() / pl.system.available_aiv_count()，可直接传入或经其绑定的 Var 传入。查询在设备上解析为本次运行自身的几何，因而天然满占用，无需再比数量；它同时是可移植写法：字面量即便与本 SoC 静态核数相符，只要运行时设备报告的可用核数不同就是错的——可用核更多时块数不足，更少时块数超额（后者会被 runtime 直接拒绝）。用错核类型的查询（纯 AIV 启动却用 cluster 数、混合启动却用 AIV 数）会被拒绝。按启动点及其直接被调：独立 AIV kernel + aiv_only → required = GetCoreCount(VECTOR)；独立 AIC kernel + aic_only → required = GetCoreCount(CUBE)；独立 AIV/AIC kernel 若用了不匹配的 core_type（含默认的 mix）直接报错——单核类型启动下另一种核零参与，barrier 永远无法完成；Group（混合 kernel）→ 任意 barrier core_type 的 required = GetCoreCount(CUBE) 个 core-group（每 group 一个 AIC，填满全部 group 即填满全部核），检查其 AIC/AIV 子 kernel 中的硬 syncall（复制的 mix 只报一次）。当后端未配置、core_num 既非字面量也非启动形状查询、或没有 SPMD 启动点启动该 kernel（占用率是启动期属性）时跳过。修复方式：用匹配的 core_type 满占用启动并设置 sync_start=True（推荐直接用对应的启动形状查询来定尺寸），或对部分占用改用 pl.system.syncall(mode="soft", ...)（GM 轮询）。 |
SSAVerify¶
错误类型 (ssa::ErrorType)：
| 错误码 | 名称 | 描述 |
|---|---|---|
| 1 | MULTIPLE_ASSIGNMENT |
变量在同一作用域中被多次赋值 |
| 2 | NAME_SHADOWING |
变量名遮蔽了外层作用域的变量 |
| 3 | MISSING_YIELD |
ForStmt 或 IfStmt 缺少必需的 YieldStmt |
| 4 | ITER_ARGS_RETURN_VARS_MISMATCH |
ForStmt/WhileStmt 中 iter_args 数量 != return_vars 数量 |
| 5 | YIELD_COUNT_MISMATCH |
YieldStmt 值数量 != iter_args/return_vars 数量 |
| 6 | SCOPE_VIOLATION |
变量在其定义作用域之外被使用 |
| 7 | MISPLACED_YIELD |
YieldStmt 出现在作用域中尾部以外的位置 |
TypeCheck¶
错误类型 (typecheck::ErrorType)：
| 错误码 | 名称 | 描述 |
|---|---|---|
| 101 | TYPE_KIND_MISMATCH |
类型种类不匹配（如 ScalarType 与 TensorType） |
| 102 | DTYPE_MISMATCH |
数据类型不匹配（如 INT64 与 FLOAT32） |
| 103 | SHAPE_DIMENSION_MISMATCH |
形状维度数不匹配 |
| 104 | SHAPE_VALUE_MISMATCH |
形状维度值不匹配 |
| 105 | SIZE_MISMATCH |
控制流分支中向量大小不匹配 |
| 106 | IF_CONDITION_MUST_BE_SCALAR |
IfStmt/WhileStmt 条件必须是 ScalarType |
| 107 | FOR_RANGE_MUST_BE_SCALAR |
ForStmt 范围必须是 ScalarType |
| 108 | CONDITION_MUST_BE_BOOL |
IfStmt/WhileStmt 条件 dtype 必须是 BOOL |
| 109 | TENSOR_PADDING_MISMATCH |
Tensor 填充元数据不匹配 |
| 110 | DISTRIBUTED_WINDOW_IDENTITY_MISMATCH |
DistributedTensor 引用了不同的窗口缓冲区 |
| 111 | TILE_VIEW_MISMATCH |
有效 TileView 元数据不匹配 |
NoNestedCall¶
| 名称 | 描述 |
|---|---|
CALL_IN_CALL_ARGS |
调用表达式嵌套在另一个调用的参数中 |
CALL_IN_IF_CONDITION |
调用表达式在 if 语句条件中 |
CALL_IN_FOR_RANGE |
调用表达式在 for 循环范围中 |
CALL_IN_BINARY_EXPR |
调用表达式在二元表达式中 |
CALL_IN_UNARY_EXPR |
调用表达式在一元表达式中 |
UseAfterDefCheck¶
错误类型 (use_after_def::ErrorType)：
| 错误码 | 名称 | 描述 |
|---|---|---|
| 401 | USE_BEFORE_DEF |
变量在当前作用域中任何定义之前被引用 |
作用域规则：
- 函数参数在整个函数体内可见
AssignStmt：LHS 变量在 RHS 求值后进入作用域ForStmt：loop_var和iter_args仅在循环体内可见；return_vars在循环结束后进入外层作用域WhileStmt：iter_args在条件和循环体内可见；return_vars在循环结束后进入外层作用域IfStmt：- SSA/phi 形式（存在
return_vars）：then/else 分支内新定义的局部变量不传播到外层作用域，只有return_vars在 if 结束后进入外层作用域 - 泄漏模式（无
return_vars）：then/else 分支内定义的变量可能泄漏到外层作用域；该形式通常由 Python 解析器在无yield的情况下生成，后续由ConvertToSSA/SSAVerify负责将其转换并检查合法性
PropertyVerifierRegistry¶
头文件：include/pypto/ir/verifier/property_verifier_registry.h
将 IRProperty 值映射到 PropertyVerifier 工厂的单例注册表。由 PassPipeline 用于在 Pass 执行前/后自动验证属性。
| 方法 | 描述 |
|---|---|
GetInstance() |
获取单例实例 |
Register(prop, factory) |
为属性注册验证器工厂 |
GetVerifier(prop) |
创建验证器实例（若未注册则返回 nullptr） |
HasVerifier(prop) |
检查是否已注册验证器 |
VerifyProperties(properties, program) |
验证一组属性，返回诊断信息 |
VerifyOrThrow(properties, program) |
验证并在出错时抛出 VerificationError |
GenerateReport(diagnostics) |
静态方法——将诊断信息格式化为可读报告 |
C++ API 参考¶
PropertyVerifier 接口¶
| 方法 | 签名 | 描述 |
|---|---|---|
GetName() |
std::string GetName() const |
返回唯一的规则标识符 |
Verify() |
void Verify(const ProgramPtr&, std::vector<Diagnostic>&) |
检查程序并追加诊断信息 |
结构性属性和默认属性¶
| 函数 | 返回值 | 描述 |
|---|---|---|
GetStructuralProperties() |
{TypeChecked, BreakContinueValid, NoRedundantBlocks, UseAfterDef, OutParamNotShadowed, NoNestedInCore, InOutUseValid, PipelineLoopValid, ArrayNotEscaped, ManualDepsOnSubmitOnly} |
由 VerificationInstrument 在每个 Pass 执行前后验证的不变量（与 GetVerifiedProperties() 共有的子集还会在流水线启动时验证） |
GetDefaultVerifyProperties() |
{SSAForm, TypeChecked, NoNestedCalls, BreakContinueValid, NoRedundantBlocks, UseAfterDef, OutParamNotShadowed, NoNestedInCore, TileTypeCoherence, ArrayNotEscaped} |
run_verifier() 的默认属性集 |
GetVerifiedProperties() |
{SSAForm, TypeChecked, MixedKernelExpanded, AllocatedMemoryAddr, BreakContinueValid, NoRedundantBlocks, InOutUseValid, CallDirectionsResolved, ManualDepsOnSubmitOnly, ReturnParamsExplicit, AivSplitValid, HardSyncallOccupancyValid} |
PassPipeline 自动验证的轻量级属性集 |
RunVerifier Pass 工厂¶
创建一个 Pass，使用 PropertyVerifierRegistry 验证指定的属性。
Python API 参考¶
模块：pypto.pypto_core.passes
PropertyVerifierRegistry¶
| 方法 | 参数 | 返回值 | 描述 |
|---|---|---|---|
verify(properties, program) |
IRPropertySet, Program |
list[Diagnostic] |
收集诊断信息 |
verify_or_throw(properties, program) |
IRPropertySet, Program |
None |
出错时抛出异常 |
generate_report(diagnostics) |
list[Diagnostic] |
str |
格式化诊断信息 |
辅助函数¶
| 函数 | 返回值 | 描述 |
|---|---|---|
get_default_verify_properties() |
IRPropertySet |
run_verifier() 的默认属性集 |
get_structural_properties() |
IRPropertySet |
结构性不变量属性 |
run_verifier 函数¶
| 参数 | 类型 | 默认值 | 描述 |
|---|---|---|---|
properties |
IRPropertySet \| None |
None |
要验证的属性（None → 默认属性集） |
| 返回值 | Pass |
- | 验证器 Pass 对象 |
使用示例¶
基本验证¶
from pypto.pypto_core import passes
# Verify default properties
props = passes.get_default_verify_properties()
diagnostics = passes.PropertyVerifierRegistry.verify(props, program)
if diagnostics:
report = passes.PropertyVerifierRegistry.generate_report(diagnostics)
print(report)
选择性验证¶
# Verify only specific properties
props = passes.IRPropertySet()
props.insert(passes.IRProperty.SSAForm)
props.insert(passes.IRProperty.TypeChecked)
diagnostics = passes.PropertyVerifierRegistry.verify(props, program)
禁用检查¶
# Start from default set and remove what you don't want
props = passes.get_default_verify_properties()
props.remove(passes.IRProperty.SSAForm)
diagnostics = passes.PropertyVerifierRegistry.verify(props, program)
使用异常处理错误¶
props = passes.get_default_verify_properties()
try:
passes.PropertyVerifierRegistry.verify_or_throw(props, program)
print("Program is valid")
except Exception as e:
print(f"Verification failed: {e}")
在自定义流水线中使用¶
# Create verifier pass (defaults to get_default_verify_properties())
verify_pass = passes.run_verifier()
result = verify_pass(program)
# Or with custom properties
props = passes.get_default_verify_properties()
props.remove(passes.IRProperty.SSAForm)
verify_pass = passes.run_verifier(properties=props)
result = verify_pass(program)
添加自定义规则¶
实现步骤¶
- 继承
PropertyVerifier，实现GetName()和Verify() - 创建返回
PropertyVerifierPtr的工厂函数 - 在构造函数中向
PropertyVerifierRegistry注册 - 添加 Python 绑定和类型存根（可选）
准则¶
- 使用
IRVisitor系统地遍历 IR 节点 - 保持规则聚焦——一个规则检查一类问题
- 避免副作用——仅读取 IR 并写入诊断信息
- 创建描述性诊断信息，包含严重级别、规则名称、错误码、消息和 span
相关组件¶
- Pass 系统（
00-pass_manager.md）：验证器作为 Pass 集成，PropertyVerifierRegistry 由 PassPipeline 使用 - IR 构建器（
../ir/06-builder.md）：构造验证器验证的 IR - 类型系统（
../ir/02-types.md）：TypeCheck 规则根据类型系统进行验证 - 错误处理（
../02-error-handling.md）：异常体系、断言宏（CHECK、INTERNAL_CHECK_SPAN）以及Diagnostic/VerificationError定义
测试¶
测试覆盖在 tests/ut/ir/transforms/test_verifier.py 中：有效/无效程序验证、基于属性的选择、异常与诊断模式、Pass 集成、诊断字段访问、报告生成、结构性/默认属性集。
UseAfterDef 专项覆盖在 tests/ut/ir/transforms/test_verify_use_after_def.py 中：有效程序（参数、链式赋值、for 循环体、循环后 return_var）、无效程序（先用后定义、循环变量越界、分支定义不可见于外层）、错误码/规则名验证、结构性属性成员验证。