Invalid pushad behaviour - pushad

[mfaerevaag]

Description

When executing pushad, the value of EBX is pushed and immediately overwritten by the original value of ESP. In result only 7 registers of the expected 8, EAX, ECX, EDX, EBX, original ESP, EBP,ESI, and EDI, are pushed.

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

Affected instructions:

0x60
0x6460
0x6760

Reproduction guide

Instruction:

00000000  60                pushad

Input:

binsec disasm -decode 60

Observed output:

       ⎧ 0: temp32 := esp₍₃₂₎
       ⎪ 1: esp := (esp₍₃₂₎ - 4₍₃₂₎)
       ⎪ 2: @[(esp₍₃₂₎ - 4₍₃₂₎)]₄ := eax₍₃₂₎
       ⎪ 3: esp := (esp₍₃₂₎ - 4₍₃₂₎)
       ⎪ 4: @[(esp₍₃₂₎ - 4₍₃₂₎)]₄ := ecx₍₃₂₎
       ⎪ 5: esp := (esp₍₃₂₎ - 4₍₃₂₎)
       ⎪ 6: @[(esp₍₃₂₎ - 4₍₃₂₎)]₄ := edx₍₃₂₎
       ⎪ 7: esp := (esp₍₃₂₎ - 4₍₃₂₎)
       ⎪ 8: @[(esp₍₃₂₎ - 4₍₃₂₎)]₄ := ebx₍₃₂₎
pushal ⎨ 9: @[(esp₍₃₂₎ - 4₍₃₂₎)]₄ := temp32₍₃₂₎
       ⎪10: esp := (esp₍₃₂₎ - 4₍₃₂₎)
       ⎪11: esp := (esp₍₃₂₎ - 4₍₃₂₎)
       ⎪12: @[(esp₍₃₂₎ - 4₍₃₂₎)]₄ := ebp₍₃₂₎
       ⎪13: esp := (esp₍₃₂₎ - 4₍₃₂₎)
       ⎪14: @[(esp₍₃₂₎ - 4₍₃₂₎)]₄ := esi₍₃₂₎
       ⎪15: esp := (esp₍₃₂₎ - 4₍₃₂₎)
       ⎪16: @[(esp₍₃₂₎ - 4₍₃₂₎)]₄ := edi₍₃₂₎
       ⎩17: goto ({0x00000001; 32}, 0)

Expected output:
Correctly push all 8 general purpose registers to the stack.

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