name: 优化正确性验证器 description: 使用形式化方法验证编译器优化的正确性 allowed-tools:
- Bash
- Read
- Write
- Edit
- Glob
- Grep metadata: specialization: 计算机科学 domain: 科学 category: 编译器优化 phase: 6
优化正确性验证器
目的
提供关于验证编译器优化语义保持性的专家指导。
能力
- 语义保持性检查
- Alive2风格验证
- 互模拟证明构建
- 反例生成
- 优化改进建议
- 未定义行为处理
使用指南
- 优化规范：定义源模式和目标模式
- 前提条件识别：识别所需前提条件
- 验证：检查语义等价性
- 反例分析：分析任何反例
- 改进：如有需要，改进优化
工具/库
- Alive2
- CompCert
- SMT求解器
- Vellvm