printf %x flag shall not sign extend

[qhuo]

The in kernel printf function (kernel/printf.c) appears to have a bug with the %x flag. It treats the argument as a signed number, and sign extends to 64 bit before printing.

So if I do printf("%x", 0xd00dfeed"), I got ffffffffd00dfeed, wheras the correct output should be d00dfeed.

I think we need a fix like this: qhuo@fdfe28f