| English | 中文 |
不透明谓词消除
不透明谓词是混淆器插入的、始终以相同方式求值的条件，用于添加虚假分支。
检测方法
标准方法（Z3 位向量）
使用 Z3 的位向量理论检查谓词及其否定形式的可满足性。
高级方法（整数算术）
对于涉及模运算的谓词（位向量溢出可能会掩盖结果），回退到 Z3 的整数理论进行判定。
数论模式匹配
匹配已知的数学恒真式：
x² mod 4 ∈ {0, 1}—— 恒为真x(x+1) mod 2 = 0—— 恒为真（连续整数之积必为偶数）x + (x+1) + (x+2) mod 3 = 0—— 恒为真
示例
| 谓词 | 分类 | 判定方法 |
|---|---|---|
x == x |
恒为真 (always_true) | 位向量 (bitvector) |
(x & 1) == 2 |
恒为假 (always_false) | 位向量 (bitvector) |
x*(x+1) % 2 == 0 |
恒为真 (always_true) | 整数 (integer) |
x > 5 |
动态 (dynamic) | — |