Invalid OF calculation - xadd, sbb

[mfaerevaag]

Description

Invalid calculation of the carry flag, OF, when executing xadd instruction.

Reference:
Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2C 5-580

Affected instructions:

0x0fc1c0   # xadd
0x1800     # sbb
0x1a00

NOTE: All combinations of prefixes and operands are omitted.

Reproduction guide

Instruction:

00000000  1800              sbb [eax],al

Input:

binsec disasm -decode 1800

Observed output:

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

Expected output:
The RHS of first clause of OF should be (eax₍₃₂₎{0,7} + (extu CF₍₁₎ 8)){7}.

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