Hi Andrea, I think the first part is fine when approved, but the 2nd part is problematic like Szabolcs already pointed out. We can't just change the ABI or semantics, and these builtins are critical for GLIBC performance. We would first need to change GLIBC back to using inline assembler so it will still write zeroes in the top 32 bits (since that is the current ABI).
Cheers, Wilco
