assembly - x86-64 から浮動小数点数を出力するには、%rbp を保存する必要があるようです

Question

Ubuntu で gcc 4.6.1 を使用して、C ライブラリにリンクされた単純なアセンブリ言語プログラムを作成し、整数を出力しようとすると、正常に動作します。

        .global main
        .text
main:
        mov     $format, %rdi
        mov     $5, %rsi
        mov     $0, %rax
        call    printf
        ret
format:
        .asciz  "%10d\n"

期待どおり、これは 5 を出力します。

しかし、小さな変更を加えて、浮動小数点値を出力しようとすると、次のようになります。

        .global main
        .text
main:
        mov     $format, %rdi
        movsd   x, %xmm0
        mov     $1, %rax
        call    printf
        ret
format:
        .asciz  "%10.4f\n"
x:
        .double 15.5

このプログラムは、何も出力せずにフォールトします。ただ悲しいセグメンテーション違反。

しかし、これを押してポップすることで修正できます%rbp。

        .global main
        .text
main:
        push    %rbp
        mov     $format, %rdi
        movsd   x, %xmm0
        mov     $1, %rax
        call    printf
        pop     %rbp
        ret
format:
        .asciz  "%10.4f\n"
x:
        .double 15.5

これで動作し、15.5000 が出力されます。

私の質問は、なぜプッシュとポップ%rbpでアプリケーションが機能するようになったのですか? ABI によると、呼び出し先が保持する必要%rbpがあるレジスタの 1 つであるため、混乱させることはできません。実際、整数のみが に渡された最初のプログラムで機能しました。では、問題は別の場所にあるのでしょうか?printfprintfprintf