how to generate x86 "narrowing" divide instruction

[Jay Foad <jay dot foad at gmail dot com>]

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.