how to generate x86 "narrowing" divide instruction

[Jay Foad]

This source code:

$ cat rand.c
#include <stdint.h>
uint32_t rand(uint32_t x) { return (uint64_t)x * 16807 % 0x7FFFFFFF; }

compiles to this optimised x86 code:

$ gcc -S -O3 -m32 -fomit-frame-pointer -o - rand.c
...
rand:
        subl    $28, %esp
        movl    $16807, %eax
        mull    32(%esp)
        movl    $2147483647, 8(%esp)
        movl    $0, 12(%esp)
        movl    %eax, (%esp)
        movl    %edx, 4(%esp)
        call    __umoddi3
        addl    $28, %esp
        ret

Why does the compiler generate a call to __umoddi3, rather than a
single 64- to 32-bit divide/remainder instruction, "div"? Is it
lacking the necessary VRP to determine that the high part of the
dividend is strictly less than the divisor?

I'm using:

$ gcc --version
gcc (Ubuntu/Linaro 4.4.4-14ubuntu5) 4.4.5

Thanks,
Jay.