本文详解如何用 Z3 正确建模基于 3-bit 分块运算的虚拟机程序逆向问题，指出混合 Int 与 BitVec 导致求解卡死的根本原因，并提供高效、可收敛的位向量建模方案及完整可运行示例。
本文详解如何用 z3 正确建模基于 3-bit 分块运算的虚拟机程序逆向问题，指出混合 `int` 与 `bitvec` 导致求解卡死的根本原因，并提供高效、可收敛的位向量建模方案及完整可运行示例。
在 Advent of Code 2024 Day 17 这类虚拟机逆向题中，程序按 3-bit（即八进制位）逐段解析输入整数 a，每轮执行异或、整除、位移等操作并生成一位输出。目标是：给定输出序列（如 [2, 2, 3]），反推出任一合法输入 a。初学者常尝试用 Z3 的 Int 类型直接翻译 Python 逻辑，却遭遇 s.check() 长时间无响应或返回 unknown——这并非 Z3 能力不足，而是建模方式触发了底层求解器的性能瓶颈。
核心问题在于：混用 Int 与 BitVec 会引入非线性整数约束（如 `2 b中指数为变量）**。SMT 求解器对非线性整数算术（NIA）缺乏完备决策过程，相关算法复杂度高、启发式依赖强，极易陷入搜索僵局。原代码中频繁调用Int2BV/BV2Int、用IntVal(2) ** s2` 计算动态幂次，正是典型“雷区”。
✅ 正确做法是统一使用固定宽度位向量（BitVec）建模，显式限定变量范围（如 32 位），并将所有运算映射到位级语义：
-
% 8→bvand(b, 0b111)或直接b % 8（Z3BitVec支持） -
2 ** b→ 左移1 （<code>BitVec原生支持，无非线性） - 整除
/→ 使用UDiv语义（无符号除法，符合//行为）
以下是优化后的完整可运行代码：
from z3 import *
# 给定目标输出（例如由已知输入 123 生成）
output = [2, 2, 3]
s = Solver()
# 统一使用 32 位位向量，避免类型混用
a, b, c = BitVecs('a b c', 32)
s.add(a > 0) # 输入为正整数
# 模拟原始程序的 while 循环（手动展开）
for x in output:
# b = a % 8
b = a % 8
# b = b ^ 6
b = b ^ 6
# denominator = 2 ** b → 等价于 1 0:
b = a_val % 8
b ^= 6
denominator = 1 <p>运行后将快速输出 <code>sat</code> 及一个有效解（如 <code>a = 115</code>）。值得注意的是，由于程序存在多解性（如 <code>program(115)</code> 和 <code>program(123)</code> 均输出 <code>[2, 2, 3]</code>），Z3 返回任意满足条件的解即为成功——这恰恰体现了 SMT 求解器在逆向工程中的实用价值：无需遍历全部可能，即可高效定位可行输入。</p><p>? <strong>关键总结</strong>：</p>
-
禁用类型混用：勿在同一流程中交叉使用
Int和BitVec，尤其避免**、sqrt等非线性运算； -
显式位宽：对嵌入式/VM 类问题，优先假设变量为固定宽度（如 32 位），用
BitVec(n, width)建模； -
算符语义对齐：用
UDiv替代/（防符号歧义），用1 替代 <code>2**b（保持线性）； - 循环需手动展开：Z3 不支持动态循环，需根据输出长度确定迭代次数。
掌握这一建模范式后，Z3 将成为你破解虚拟机、协议逆向、密码学约束等场景的高效利器。
