Invalid AF calculation - `scasb`, `scasd`, `add`, `adc`, `sbb`, `sub`, `cmp`, `inc`, `dec`

[mfaerevaag]

Description

The AF flag is being calculated in much the same way as the OF flag, but this is not the correct behaviour. Instead of taking the carry of a whole byte, it should take the 5th bit (zero indexed), as a decimal number is represented by five bits in BCD.

Reference:
scasb, scasd: Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2B 4-590
adc: Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2A 3-26
add: Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2A 3-31
sbb: Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2B 4-587
sub: Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2B 4-652
cmp: Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2A 3-153
inc: Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2A 3-451
dec: Ref. Intel 64 and IA-32 Architecture Software Developer's Manual Vol. 2A 3-285

Affected instructions:

0xae         # scasb
0xaf         # scasd
0x0000       # add
0x0100
0x0200
0x0300
0x0442
0x0542424242
0x1000       # adc
0x1100
0x1200
0x1300
0x1400
0x1500000000
0x18c0       # sbb
0x19c0
0x1ac0
0x1bc0
0x1c00
0x1d00000000
0x2800       # sub
0x2900
0x2a08
0x2b08
0x2c42
0x3800       # cmp
0x3900
0x3a00
0x3b00
0x3c42
0x3d42424242
0x40         # inc
0x41
0x42
0x43
0x44
0x45
0x46
0x47
0xfe00
0xff00
0x48         # dec
0x49
0x4a
0x4b
0x4c
0x4d
0x4e
0x4f

NOTE: All combinations of prefixes are omitted.

Reproduction guide

Instruction:

00000000  0000              add [eax],al

Input:

binsec disasm -decode 0000

Observed output:

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

Expected output:
Something like this BAP code:

  v1 := mem32[pad:32[low:32[EAX]], el]:u8
  v2 := low:8[low:32[EAX]]
  AF := 0x10:8 = (0x10:8 & (((mem32[pad:32[low:32[EAX]], el]:u8) ^ v1) ^ v2))

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