使用 Z3 验证汇编代码

本文展示了如何利用 Z3 SMT 求解器来验证汇编级别的代码优化。作者以 Ruby ZJIT 中修复 fixnum 除法溢出 bug 的 PR 为例，通过 Z3 证明了一个无分支条件测试（使用 xor、or 和 test 指令）与原始 C 语言中的显式条件检查等价。文章详细介绍了如何通过否定条件让 Z3 搜索反例来验证等价性，这是一种将 SMT 求解器用作"证明引擎"的标准技巧。