Z3 用于减法的进位、溢出和下溢标志

Question

假设我有 8-BitVectors 1 (#x01) 和 -2 (#xfe)，我用 Z3_mk_bvsub 减去它们。当我计算与标志相关的数量时，我得到

nc ≡ Z3_mk_bvsub_no_overflow → true
nu ≡ Z3_mk_bvsub_no_underflow → true

我的目标是理解这些标志的含义。当我尝试将它们与 CPU 标志进行比较时会出现混淆，因为如果我要求 CPU 减去 1 - (-2)

    mov al, 1
    sub al, -2

它的标志变为CY = 1和OV = 0。

我的问题是：如何使用减法标志从 Z3 中获取 CY 和 OV？更准确地说，从 Z3 结果 nu 和 nc 中生成 CY 和 OV 的布尔表达式是什么？我最初的猜测是 OV = ¬ nu 和 CY = ¬ nc，但显然情况并非如此，至少对于进位而言。

注意：我在加法时没有这个问题，类似的方程式确实成立。

注2：进一步调查发现，在做减法的情况下，不可能从Z3 flags推导出X86/64 CY flag .还需要减去数量的符号。 OV标志虽然可以推导，加法也是如此。

Answer 1

关于这些操作要阅读的论文是https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/z3prefix.pdf

请注意，操作是“相反的”。如果没有溢出，Z3_mk_bvsub_no_overflow 将为真。下溢也类似。这种双重否定是不幸的，但这就是定义操作的方式。

这些与 CPU 的 OV/CY 标志有何关系是一个有趣的问题。我认为最好将 z3 的结果（如上文所述）视为数学语义。用 z3 的说法，当无限精确的结果位于位向量大小所覆盖的范围的右侧时，存在上溢，而当它位于左侧时，存在下溢。

但是，您的特定架构（很可能是 x86，但不一定！）可能对这些标志的生成方式有不同的规则。特别是 CPU 不关心（或知道）参数是有符号的还是无符号的。 2 的补码算法的魔力使它们能够统一处理参数，因此与 z3 执行的类型分析没有直接对应关系。这是 x86 手册中的 description：

The SUB instruction does not distinguish between signed or unsigned operands. Instead, the processor evaluates the result for both data types and sets the OF and CF flags to indicate a borrow in the signed or unsigned result, respectively. The SF flag indicates the sign of the signed result.

长话短说，您必须非常具体地说明您是否在进行 signed/unsigned 算术运算，并查看精确的 x86（或您使用的任何架构，但我认为它们必须都是相似的），看看实际的对应关系是什么。请记住，对应关系可能不准确。由于 legacy/historical 原因，x86 以其独特的方式做事，这可能与 z3 根据上述论文产生的数学结果不完全匹配。

Answer 2

减法后 x86/64 标志的表达式如下：

CY = ¬ unu ∧ (t2 < 0).
OV = ¬ (no ∨ unu) ∨ ¬ snu

哪里

unu : Z3_mk_bvsub_no_underflow [unsigned]
t2  : arg 2
no  : Z3_mk_bvsub_no_overflow
snu : Z3_mk_bvsub_no_underflow: [signed]

加法情况下：

CY = ¬ uno
OV = ¬ sno ∨ ¬ nu

哪里

uno : Z3_mk_bvadd_no_overflow [unsigned]
sno : Z3_mk_bvadd_no_overflow [signed]
nu  : Z3_mk_bvadd_no_underflow

Z3 用于减法的进位、溢出和下溢标志

Z3 Carry, Overflow and Underflow flags for subtraction

z3