usb_cdc: avoid pulling in extra float-uint64 routines

[dhalbert]

A couple of conversions from float to uint64_t in usb_cdc brought in a bunch of floating-point library routines that were otherwise not needed, adding a couple of kB to the build. Use a special-purpose conversion routine instead.

Another alternative would be to limit the conversion to uint32_t, but then I have to check for the timeouts being too large, so this is probably less code.

This is the inverse of a routine I wrote a long time ago to compactly convert a uint64_t to a float.

I did write a small test program to confirm the calculation was correct (it's meant to run on a 64-bit host, not on the chip).

#include <stdint.h>
#include <stdio.h>

uint64_t float_to_uint64(float f) {
    // 4294967296 = 2^32
    const uint32_t upper_half = (uint32_t) (f /  4294967296.0f);
    const uint32_t lower_half = (uint32_t) f;
    return (((uint64_t) upper_half) << 32) + lower_half;
}

int main(void) {
    float f = 1.0f;
    while(1) {
        printf("%g: float_to_uint64: %lu, (uint64_t): %lu\n",
               (double) f, float_to_uint64(f), (uint64_t) f);
        f *= 1.5f;
        if (f > 4294967296.0f * (1L << 32)) {
            break;
        }
    }
}

[jepler]

I didn't actually test or check binary sizes. However, I did use cbmc to "prove" that your code is equivalent to the standard cast. This should include any possible floating-point value (though this is done via theorem prover, not exhaustive testing):

#include <assert.h>
#include <stdint.h>

uint64_t float_to_uint64_danh(float f) {
    // 4294967296 = 2^32
    const uint32_t upper_half = (uint32_t) (f /  4294967296.0f);
    const uint32_t lower_half = (uint32_t) f;
    return (((uint64_t) upper_half) << 32) + lower_half;
}

uint64_t float_to_uint64_cast(float f) {
    return (uint64_t)f;
}

int main() {
    float f = nondet_float();
    uint64_t a = float_to_uint64_danh(f);
    uint64_t b = float_to_uint64_cast(f);
    assert(a == b);
}

$ cbmc float_to_uint64.c  --trace --beautify
CBMC version 5.10 (cbmc-5.10) 64-bit x86_64 linux
...
Runtime decision procedure: 0.0413051s

** Results:
[main.assertion.1] assertion a == b: SUCCESS

** 0 of 1 failed (1 iteration)
VERIFICATION SUCCESSFUL

[dhalbert]

I had no idea this tool existed - thanks for the "proof"!