FLOATS CROSSING C: FOLLOW THE ABI.
Once explicit floats cross an extern "C" boundary, target ABI rules decide where arguments and return values travel. The 13.1 work tests mixed integer/float signatures on SysV64 and Win64 instead of assuming every parameter consumes the next general-purpose register.
00 fixture shape
extern "C" fn c_float_contract(
tag: i32,
a: f32,
b: f64,
tail: i64
) -> f64The mixed signature is intentional. It catches register-class mistakes that a float-only function can miss. The reverse direction is covered by a public DByte callback using the same C convention.
10 XMM transport
On x86_64 System V and Win64, floating-point arguments and returns use the target floating-point register class. The backend tracks XMM placement separately from integer/pointer argument state. Exact placement is ABI-owned; the contract is not “always XMM0 then XMM1 in source order.”
20 exact fixture values
The DByte side bitcasts exact u32/u64 patterns into f32/f64, calls the C fixture, and checks returned f64 bits. The callback verifies every incoming field before returning another exact pattern.
30 C ABI is not strict portable code
The strict portability validator rejects extern "C" and repr(C) with E_PORTABLE_C_ABI. Portable DBYTE code and interoperable DBYTE code overlap, but they are not the same set.
40 inspect the fixture
explicit_float_c_abi.dby is the captured DByte fixture.
extern "C" fn c_float_contract(tag: i32, a: f32, b: f64, tail: i64) -> f64
pub extern "C" fn dbyte_float_callback(tag: i32, a: f32, b: f64, tail: i64) -> f64:
if tag != (11 as i32):
return (0 as u64) as! f64
if (a as! u32) != (0x40600000 as u32):
return (0 as u64) as! f64
if (b as! u64) != (0x4011000000000000 as u64):
return (0 as u64) as! f64
if tail != (13 as i64):
return (0 as u64) as! f64
return (0x401a000000000000 as u64) as! f64
pub fn main() -> i32:
let a: f32 = (0x3fc00000 as u32) as! f32
let b: f64 = (0x4002000000000000 as u64) as! f64
let result: f64 = c_float_contract(7 as i32, a, b, 9 as i64)
if (result as! u64) != (0x4029000000000000 as u64):
return 1
return 42