Daß die Funktionsweise identisch ist, kann man dann annehmen, wenn man eine genaue Umschreibung dessen hat, was push bedeuten soll.

Genau diesem Zweck dient RTL: Algebraische Umschreibungen der Maschine (bzw. ihres Instruktionssatzes) zu ermöglichen.

Auf RTL sind dann Transormationen möglch, die zB gewisse Insns bzw. Insn-Sequenzen als äquivalent betrachten.

Die Zuordnung einer asm-Instruktionssequenz zu einer Insn geschieht wie du weißt im md-File. Ob Transormationen erlaubt sind bzw. äquivalente RTXe ergeben, sieht man nicht unbedingt am md. Hier geht auch ganz viel über das h- und das c-File, zB was gültige Register-Operanden und Adressen sind, welche Pseudos auf welche Hard-Regs abgebildet werden dürfen, etc. Und ob zB ein CALL korrekt in asm umgesetzt wurde, lässt sich am RTL nicht erkennen, weil die argumente eines CALL nicht in RTL auftauchen.

Mir ist jetzt nicht ganz klar, was du mit "virtuellem Stack" meinst.

Der Maschine sind einige besondere "virtuelle" Hard-Register bekannt wie
virtual-incoming-args, virtual-stack-vars, virtual-stack-dynamic, virtual-outgoing-args, virtual-cfa, ... die für besondere Zwecke verwendet werden und irgendwann auf Hard-Register abgebildet oder eliminiert werden.

Wenn einer Funktion zB Argumente über den Stack übergeben werden, zeigt virtual-incoming-args auf das erste Argument; virtual-incoming-args wird aber für praktisch alle Maschinen auf den Frame-Pointer oder den Stack-Pointer abgebildet (und der Frame-Pointer dann auch auf den Stack-Pointer), wobei natürlich noch die richtigen Offsets drauf müssen.

Das einzige Dokument, daß dies ansazuweise zum Thema hat, ist m.W das GCC internals. Ansonsten helfen nur die GCC-Quellen.