x86架构下SUB指令进位标志推导错误的技术排查请求

我确定下述推导存在错误，希望有人能指出我的“证明”中的问题所在。

我正尝试证明x86指令setb在cmp指令后使用时，确实能实现无符号比较x < y。具体来看（采用ATT语法，忽略表示位数的后缀）：

# 比较两个寄存器，无符号数场景下%eax值为y，%ebx值为x
cmp %ebx, %eax

# 若%eax小于%ebx（无符号比较），将%al设为1
setb %al

结论应该是：当且仅当无符号数x < y时，%al最终值为1。需要注意的是，ATT语法中cmp指令是将%eax的内容减去%ebx的内容，并相应设置相关条件标志——其中包括我们关注的进位标志。也就是将位模式输入减法单元计算y (-^u) x（我用(-^u)表示无符号减法，用-表示对应整数的减法）。

我的问题如下：假设x < y，我们需要证明减法会产生进位输出。假设每个数为w位。我从教材（Bryant和O'Hallaron所著《CS:APP3e》）中得知无符号减法的定义：

x(-^u)y := x(+^u)((-^u) y) = x(+^u)(2^w - y) = 2^w + x - y < 2^w,

但我套用这个公式时，得出的结果似乎不会产生进位输出，因为结果能放入w位中。但显然这是错误的，我到底哪里出错了？

错误点分析 #

你的核心错误是搞反了cmp指令的操作数对应的减法方向：

• 在ATT语法里，cmp %src, %dst执行的是%dst - %src的无符号减法，对应到你的场景就是y (-^u) x，而不是你推导里写的x (-^u) y。
• 当x < y时，整数减法y - x是正的且小于2^w，但x86的进位标志CF的逻辑是：当无符号减法a (-^u) b中a < b时，CF被置1——你混淆了“减法结果是否溢出w位”和“CF标志的触发条件”。
• 回到无符号减法定义，计算y (-^u) x且x < y时，y (-^u) x = y + (2^w - x) = 2^w + (y - x)。因为y - x是正整数且小于2^w，这个加法的总和会超过w位，所以加法单元会产生进位输出，这个进位就是x86的CF标志。
• 你之前错误地用x (-^u) y推导，当x < y时，x (-^u) y = 2^w + x - y，结果确实小于2^w，不会产生进位，但这和cmp实际执行的减法方向完全相反，自然得出错误结论。

简单总结：你推导的是x减y的情况，但cmp实际做的是y减x，操作数搞反了才导致逻辑错误。

内容的提问来源于stack exchange，提问作者EE18