x86_64 ABI question

[John Fine <johnsfine at verizon dot net>]

When an unsigned int is passed or returned in a 64-bit register, does 
either the C or C++ ABI specify that the top half of the register 
contain zero?

I am using the Intel 10.0 compiler set for ABI compatibility with GCC 
3.4.6 on Linux.

I have looked at a lot of disassemblies of the generated code.  A few 
times, I have seen the code

mov %eax,%eax

immediately before a function returns an unsigned int, under conditions 
where the low 32 bits of %rax contained the unsigned int to be returned 
and the upper bits were garbage.  That instruction clears the upper bits 
as would be required if the ABI does specify the upper bits contain zero.

I have also seen cases where a function uses %rdi in an address 
expression, when %edi has just been passed in as an unsigned int.  That 
would only be correct if the ABI specifies the top half is zeroed.  If 
incorrect, it would still almost always work, because the top half would 
be cleared for free by almost all code sequences that put an unsigned 
int into a 64 bit register.

But I have also seen cases where, under the same conditions, the 
compiler has generated
mov %edi,%edi
directly before the use of %rdi, even though %edi was just passed in as 
an unsigned int.  I can't tell whether the compiler is just being 
stupid, or whether the ABI doesn't allow it to assume the top half is 
clear, or whether the extra instruction is for some other purpose 
entirely (to affect some obscure aspect of instruction pipelining and/or 
16-byte alignment of the instruction stream).

If the ABI rules were well designed, then they must specify those high 
order bits are zeroed.  In typical code the cases where extra work is 
needed to obey that rule are much rarer than the cases where work could 
be avoided by relying on that rule.

I found AMD's X86_64 ABI document and it specifies that the high 63 bits 
are zeroed when a bool is passed in a 64-bit register, but is says 
nothing about that for other types that might be passed in 64-bit 
registers.  I can't figure out what document gives this sort of 
information for X86_64, GCC, C++