Invalid CF calculation - `sbb`

[mfaerevaag]

Description

Invalid calculation of the carry flag, CF, when executing sbb instructions with the opcodes below.

Reference: Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2B 4-587

Affected instructions:

0x1900    # sbb
0x1B00
0x1CFF

NOTE: All combinations of prefixes and operands are omitted.

Reproduction guide

Instruction:

00000000  1900              sbb [eax],eax

Input:

binsec disasm -decode 1900

Observed output:

               ⎧ 0: res32 := (@[eax₍₃₂₎]₄ - (eax₍₃₂₎ + (extu CF₍₁₎ 32)))
               ⎪ 1: OF := ((@[eax₍₃₂₎]₄{31} ≠ (@[eax₍₃₂₎]₄ + (extu CF₍₁₎ 32)){31}) && (@[eax₍₃₂₎]₄{31} ≠ res32₍₃₂₎{31}))
               ⎪ 2: SF := (res32₍₃₂₎ <𝒔 0₍₃₂₎)
               ⎪ 3: ZF := (res32₍₃₂₎ = 0₍₃₂₎)
sbb [eax], eax ⎨ 4: AF := (@[eax₍₃₂₎]₄{0,7} <𝒖 (eax₍₃₂₎{0,7} + (extu AF₍₁₎ 8)))
               ⎪ 5: PF := ¬(((((((res32₍₃₂₎{0} ⨁ res32₍₃₂₎{1}) ⨁ res32₍₃₂₎{2}) ⨁ res32₍₃₂₎{3}) ⨁ res32₍₃₂₎{4}) ⨁ res32₍₃₂₎{5}) ⨁ res32₍₃₂₎{6}) ⨁ res32₍₃₂₎{7})
               ⎪ 6: CF := (@[eax₍₃₂₎]₄ <𝒖 (eax₍₃₂₎ + (extu CF₍₁₎ 32)))
               ⎪ 7: @[eax₍₃₂₎]₄ := res32₍₃₂₎
               ⎩ 8: goto ({0x00000002; 32}, 0)

Expected output: It cannot detect the overflow situation correctly when the destination operand is negative.

System Info

OS:

# uname -a
Linux ubuntu 4.10.0-28-generic #32-Ubuntu SMP Fri Jun 30 05:32:18 UTC 2017 x86_64 x86_64 x86_64 GNU/Linux
# cat /etc/lsb-release
DISTRIB_ID=Ubuntu
DISTRIB_RELEASE=17.04
DISTRIB_CODENAME=zesty
DISTRIB_DESCRIPTION="Ubuntu 17.04"

BINSEC: 20170301 0.1