stricter test for max object size

The previous test with word_bits was sufficient on 32 bit platforms, but
64 bit platforms may set a much smaller value for seL4_MaxUntypedBits in
relation to word_bits.

avoid shift overflow for large Untyped's on 64bit platforms

Fix max object size in range error for retype on 64-bit platforms

The expression previously used was correct for current 32-bit platforms,
but not for 64-bit platforms.

trivial: use constant in seL4_UntypedRetype check

SELFOUR-444: Preemptible zeroing for retype.

Change to the order of operations and timing behaviour of
invokeUntyped_Retype. The Retype operation now zeroes the
entire range of the Untyped cap (if it is being used for
the first time) before installing any objects. This avoids
the need for long-running initialisation of large objects,
whose initial contents are always zero. The initial zeroing
phase is preemptible, and may take multiple timeslices to
complete.

Use correct seL4_MaxUntypedBits

This change uses the seL4_MaxUntypedBits constant in decodeUntypedInvocation
when checking the size of the requested allocation. This constant
is also changed to be the correct value. The verification team suspects
this check is probably unnecessary, but have also resolved not to waste more
time investigating.

[STYLE_FIX]

Fix comment in decodeUntypedInvocation to better reflect maximum object sizes after device-untyped changes

SELFOUR-632: implement cores non-architecture dependent structres

SELFOUR-421: minor changes for c-refine

SELFOUR-421 Introduce explicit device frames and untypeds

Kernel objects cannot be created from device untypeds, with the
exception of frames, which do not get zeroed and cannot be used
as an IPC buffer. Device untypeds additionally cannot be used
in the construction of ASID pools.

This then changes the API to the rootserver (i.e. bootinfo) to
send device untypeds instead of device frames. On ARM these
device untypeds are the same as the previously exported device
frame regions. On x86 PCI scanning is removed and all physical
memory addresses (that are not important for kernel integrity)
are released to the user.

In order to have bits in the frame and untyped caps on ARM the
number of software ASIDs had to be reduced from 2^18 to 2^17,
and the maximum untyped size reduced from 2^31 to 2^30

SELFOUR-433: Shift as a 32-bit value

Shifting as an unsigned long long does not work on some ARM compilers
as the kernel is not linked against libgcc

SELFOUR-433: Prevent undefined shift in userError message

SELFOUR-114: remove duplication of seL4_MessageInfo_t, adjust naming to avoid cparser mangling

unsigned int -> word_t

Fix style and unused variable warnings.

Ghost assertions about max object size.

Release snapshot