printf '0x%x', -0xaaaaaaaa >> 32;