Invalid order of calculation - cmpxchg

[mfaerevaag]

Description

When executing cmpxchg, the semantics for comparison is accumulator minus destination operand, but they are switched.

Reference:
Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2A 3-181

Affected instructions:

0x0fb100    #cmpxchg

Reproduction guide

Instruction:

00000000  0FB100            cmpxchg [eax],eax

Input:

binsec disasm -decode 0fb100

Observed output:

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

Expected output:
Correct order of operands during calculation.

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