function::usrdev2kerndev(3stap) on Linux

The text ed23b4d5eb8b, as Debian 10 (Buster) shipped it.

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