Преобразование из uint64_t в двойное

Question

Для STM32F7, который включает инструкции для двойных чисел с плавающей запятой, я хочу преобразовать uint64_t в double,

Чтобы проверить это, я использовал следующий код:

volatile static uint64_t m_testU64 = 45uLL * 0xFFFFFFFFuLL;
volatile static double m_testD;

#ifndef DO_NOT_USE_UL2D
    m_testD = (double)m_testU64;
#else
    double t = (double)(uint32_t)(m_testU64 >> 32u);
    t *= 4294967296.0;
    t += (double)(uint32_t)(m_testU64 & 0xFFFFFFFFu);
    m_testD = t;
#endif

По умолчанию (если DO_NOT_USE_UL2D не определено) компилятор (gcc или clang) вызывает функцию: __aeabi_ul2d() что-то сложное в количестве выполненных инструкций. Смотрите код сборки здесь: https://github.com/gcc-mirror/gcc/blob/master/libgcc/config/arm/ieee754-df.S#L537

Для моего конкретного примера требуется 20 инструкций без ввода в большинство веток

И если DO_NOT_USE_UL2D определено, компилятор генерирует следующий код сборки:

movw    r0, #1728       ; 0x6c0
vldr    d2, [pc, #112]  ; 0x303fa0
movt    r0, #8192       ; 0x2000
vldr    s0, [r0, #4]
ldr     r1, [r0, #0]
vcvt.f64.u32    d0, s0
vldr    s2, [r0]
vcvt.f64.u32    d1, s2
ldr     r1, [r0, #4]
vfma.f64        d1, d0, d2
vstr    d1, [r0, #8]

Код проще, и это всего 10 инструкций.

Так что здесь вопросы (если DO_NOT_USE_UL2D определено):

• Мой код (в C) правильный?
• Мой код медленнее, чем __aeabi_ul2d() функция (не очень важно, но немного любопытно)?

Я должен сделать это, так как мне не разрешено использовать функцию из libgcc (есть очень веские причины для этого...)

Имейте в виду, что основная цель этого вопроса не в производительности, мне действительно интересно узнать о реализации в libgcc, и я действительно хочу знать, если что-то не так в моем коде.