Invalid CF calculation - `xadd`

Description

Invalid calculation of the carry flag, CF, when executing xadd instruction with the 0xc0 as operand and prefixed as below.

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

Affected instructions:

0xc1
0x64660fc1c0
0x6466670fc1c0
0x660fc1c0
0x66670fc1c0
0xf20fc1c0
0xf2640fc1c0
0xf264660fc1c0
0xf26466670fc1c0
0xf264670fc1c0
0xf2660fc1c0
0xf266670fc1c0
0xf2670fc1c0
0xf30fc1c0
0xf3640fc1c0
0xf364660fc1c0
0xf36466670fc1c0
0xf364670fc1c0
0xf3660fc1c0
0xf366670fc1c0
0xf3670fc1c0

Reproduction guide

Instruction:

00000000  64660FC1C0        fs xadd ax,ax

Input:

bap-mc "64660fc1c0" --show-bil --arch=X86

Observed output:

{
  v1 := (low:16[low:32[EAX]]) + (low:16[low:32[EAX]])
  EAX := (extract: 31:16[EAX]).(low:16[low:32[EAX]])
  EAX := (extract: 31:16[EAX]).v1
  CF := (low:16[low:32[EAX]]) < v1
  OF := ((high:1[v1]) = (high:1[low:16[low:32[EAX]]])) & ((high:1[v1]) ^ (high:1[low:16[low:32[EAX]]]))
  AF := 0x10:16 = (0x10:16 & (((low:16[low:32[EAX]]) ^ v1) ^ (low:16[low:32[EAX]])))
  PF := ~(low:1[let v2 = ((low:16[low:32[EAX]]) >> 0x4:16) ^ (low:16[low:32[EAX]]) in
    let v2 = (v2 >> 0x2:16) ^ v2 in
    (v2 >> 0x1:16) ^ v2])
  SF := high:1[low:16[low:32[EAX]]]
  ZF := 0x0:16 = (low:16[low:32[EAX]])
}

Expected output: With this implementation, CF is only set to zero.

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

Let me elaborate a little bit on this issue. First of all the prefix here doesn't really matter, the issue is observed even without it;

 bap-mc "660fc1c0" --show-bil --arch=X86 --show-insn=asm
xaddw %ax, %ax
{
  v1 := low:16[EAX] + low:16[EAX]
  EAX := extract:31:16[EAX].low:16[EAX]
  EAX := extract:31:16[EAX].v1
  CF := low:16[EAX] < v1
  OF := high:1[v1] = high:1[low:16[EAX]] & (high:1[v1] ^ high:1[low:16[EAX]])
  AF := 0x10 = (0x10 & (low:16[EAX] ^ v1 ^ low:16[EAX]))
  PF := ~low:1[let v2 = low:16[EAX] >> 4 ^ low:16[EAX] in
    let v2 = v2 >> 2 ^ v2 in
    v2 >> 1 ^ v2]
  SF := high:1[low:16[EAX]]
  ZF := 0 = low:16[EAX]
}

Indeed, in CF := low:16[EAX] < v1 the left hand side of the comparison low:16[EAX] will be always equal to the right hand side, since it was assigned in the previous statement. So it will be always false.

SoftSec-KAIST / MeanDiff