function::usrdev2kerndev(3stap) on Linux

The text f0163b8a99d2, as Debian 8 (Jessie) shipped it.

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