Confusion of source and destination operands - xadd

[mfaerevaag]

Description

Instruction xadd occasionally confuses source and destination operand, by writing to the wrong one. The sum of the operands should be written to the destination operand, i.e. the first one, but instead writes to source operand.

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

Affected instructions:

0x0fc100    # xadd

NOTE: All combinations of prefixes and operands are omitted.

Reproduction guide

Instruction:

00000000  0FC100            xadd [eax],eax

Input:

bap-mc "0fc100" --show-bil --arch=X86

Observed output:

{
  v1 := (low:32[EAX]) + (mem32[pad:32[low:32[EAX]], el]:u32)
  mem32 := mem32 with [pad:32[low:32[EAX]], el]:u32 <- low:32[EAX]
  EAX := v1
  CF := (low:32[EAX]) < v1
  OF := ((high:1[v1]) = (high:1[mem32[pad:32[low:32[EAX]], el]:u32])) & ((high:1[v1]) ^ (high:1[low:32[EAX]]))
  AF := 0x10:32 = (0x10:32 & (((low:32[EAX]) ^ v1) ^ (mem32[pad:32[low:32[EAX]], el]:u32)))
  PF := ~(low:1[let v2 = ((low:32[EAX]) >> 0x4:32) ^ (low:32[EAX]) in
    let v2 = (v2 >> 0x2:32) ^ v2 in
    (v2 >> 0x1:32) ^ v2])
  SF := high:1[low:32[EAX]]
  ZF := 0x0:32 = (low:32[EAX])
}

Expected output:
Instead of writing v1 to EAX, it should be written to the memory of EAX.

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"

BAP:

# bap-mc --version
1.0.0
# bap --version
1.2.0