Invalid OF calculation - `sub`

[mfaerevaag]

Description

Incorrectly calculates overflow flag OF.

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

Affected instructions:

0x28c0
0x29c0
0x2ac0
0x2bc0

NOTE: All combinations of prefixes are omitted.

Reproduction guide

Instruction:

00000000  28C0              sub al,al

Input:

bap-mc "28c0" --show-bil --arch=X86

Observed output:

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

Expected output: OF should be cleared whenever the given two operands are identical.

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

[ivg]

So, what I'm seeing here is that OF is cleared. The expression is just not simplified. In BAP 1.3 we have much better printer (that doesn't print unnecessary parenthesis), as well as better expression simplifier, e.g.,

 echo '\x28\xc0' | bap-mc --arch=x86 --show-bil --show-insn=asm
subb %al, %al
{
  v1 := low:8[EAX]
  EAX := extract:31:8[EAX].0
  CF := v1 < low:8[EAX]
  OF := high:1[v1 ^ low:8[EAX]]
  AF := 0x10 = (0x10 & (low:8[EAX] ^ v1 ^ low:8[EAX]))
  PF := ~low:1[let v2 = low:8[EAX] >> 4 ^ low:8[EAX] in
    let v2 = v2 >> 2 ^ v2 in
    v2 >> 1 ^ v2]
  SF := high:1[low:8[EAX]]
  ZF := 0 = low:8[EAX]
}

You may see that high:1[v1 ^ low:8[EAX]] is zero since v1 is equal to low:8[EAX] and xor of two equal values is 0, this the high bit of 0 is also a zero.

[soomin-kim]

Also in this case, like Issue #3, every statement should be executed sequentially so at the point of OF calculation, the lower 8 bit of EAX register is 0, not same as v1. So if al contains a negative 8-bit width integer, OF should be 1 in BIL's semantics.