function::usrdev2kerndev(3stap) on Linux

The text 03aceecd7e6b, as Debian 11 (Bullseye) shipped it.

Converts a user-space device number into the format used in the kernel