x86-symbolic: Stack alignment

[langston-barrett]

On the subject of the stack under the x86_64 SysV ABI, the OSDev wiki says:

The stack is 16-byte aligned just before the call instruction is called.

We should ensure that the functions introduced in #433 properly establish this precondition.

[langston-barrett]

The "System V Application Binary Interface x86-64 Architecture Processor Supplement Draft Version 0.99.6" section 3.2.2 "The Stack Frame" is a bit more specific on what the above means:

The end of the input argument area shall be aligned on a 16 [...] byte boundary. In other words, the value (%rsp + 8) is always a multiple of 16 when control is transferred to the function entry point.

Note that the standard function prelude involves push %rbp, after which %rsp will be 16-byte aligned again (though this prelude is left out with -fomit-frame-pointer).

In 3.2.3 "Parameter Passing", it further says:

The size of each argument gets rounded up to eightbytes [sic]. Therefore the stack will always be eightbyte aligned.

[sauclovian-g]

Er... I thought -fomit-frame-pointer was the default on x86_64 (not that this is really relevant)

[langston-barrett]

Er... I thought -fomit-frame-pointer was the default on x86_64 (not that this is really relevant)

Yeah, I think you're right! I added that comment because I saw it while I was reading about this, and found it helpful for understanding why it can often be unnecessary for the compiler to insert padding before calls.

[sauclovian-g]

True enough...