Invalid stack operation - `push`, `pop`

[mfaerevaag]

Description

When pushing segment registers, as SS, CS, DS, ES, FS and GS, the stack pointer is incremented by four bytes, although the segment registers are only two bytes of size. According to the Intel manual, "The operand size (16, 32, or 64 bits) determines the amount by which the stack pointer is decremented (2, 4 or 8)."

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

Affected instructions:

0x06    # push
0x0e
0x0fa0
0x0fa8
0x16
0x1e
0x07    # pop
0x0fa1
0x0fa9
0x17
0x1f

Reproduction guide

Instruction:

00000000  06                push es

Input:

pyvex.IRSB("\x06", 0x8048000, archinfo.ArchX86())

Observed output:

IRSB {
   t0:Ity_I16 t1:Ity_I32 t2:Ity_I32 t3:Ity_I32 t4:Ity_I32

   00 | ------ IMark(0x0, 1, 0) ------
   01 | t0 = GET:I16(es)
   02 | t3 = GET:I32(esp)
   03 | t2 = Sub32(t3,0x00000004)
   04 | PUT(esp) = t2
   05 | STle(t2) = t0
   NEXT: PUT(eip) = 0x00000001; Ijk_Boring
}

Expected output: Subtract only two bytes from ESP:

IRSB {
   t0:Ity_I16 t1:Ity_I32 t2:Ity_I32 t3:Ity_I32 t4:Ity_I32

   00 | ------ IMark(0x0, 1, 0) ------
   01 | t0 = GET:I16(es)
   02 | t3 = GET:I32(esp)
   03 | t2 = Sub32(t3,0x00000002)    <-----
   04 | PUT(esp) = t2
   05 | STle(t2) = t0
   NEXT: PUT(eip) = 0x00000001; Ijk_Boring
}

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"

PyVEX:

#  pip freeze | grep pyvex
pyvex==6.7.4.12