xIntroduce RELEASE_PRINTF, which allows a renamed printf (release_printf) to be used in a release build of the kernel - userful for debugging tests that only fail on a release build of the kernel

fix syscall stub gen to shift by the size of the type not the type itself when outputting double word values

This was introduced in changeset e653f8f6
where hard coded size types were replaced with an indirection. This corrects
a case where a 'uint64_t' was replaced with a '%s', but there is no corresponding
'TYPES[64]' in the argument list, resulting in too few arguments when processing
the string

Restrict CONFIG_NUM_PRIORITIES to the range of 1-256 as there are assumptions on a priority fitting into a single byte

Once again, we know in the abstract invariants that these must be
async endpoint caps or null caps, but this is only knowable in
haskell by asserting it.

Need to be careful about operations that are ambiguous in Haskell
but well-defined in the resulting Isabelle import.

We can't prove that the caller cap must be a reply cap or that
the frames mapped in an arbitrary address space are backed by caps
without appealing to the abstract invariants, which means yet more
assertions in haskell and work in the abstract/haskell refinement.

It's true that the interrupt node must contain async endpoint
caps, but we never proved the relevant invariant, and it doesn't
change much.

There are now separate libs for benchmark, assert, printf, putchar
start/stop:

      libs/libsel4benchmark
      libs/libsel4assert
      libs/libsel4printf
      libs/libsel4putchar
      libs/libsel4startstop

The primary changes are introducing sel4/sel4.h and removing std* types
plus porting assert and IO code from the kernel to libsel4assert,
libsel4printf, libsel4putchar.

This means the code within libsel4 and the newlibs do not overload any
typical libc entities. Instead the libraries use types like
seL4_Uint32 ... instead of uint32_t. And printf is now seL4_Printf and
assert is seL4_Assert ....

Finally, the only file modified that effects kernel code is
kernel/tools/bitfield_gen.py. It needed to be modified as it generates
files for both kernel and user space. And for user space the generated code
(types_gen.h) needed to use the new types and asserts. The changes should
not change what is generated for the kernel and I did a comparison of
kernel_final.{c|s} before and after my change and the only differences
were time stamps.

Bug: #15 Streamline kernel/libsel4 and remove its libc dependencies

Fix: In exynos timer driver, declaring comparator_value variable at top of initTimer to comply with C90.

When initializing the exynos mct, set the initial value of the 64-bit comparator to the sum of the the 64-bit counter and TIMER_TICKS.

bitfield: Allow for controlling how many bits of a word are actually used, and whether the rest of the bits are signed extended or not

This change purely changes the ordering of C symbols, as well as
adding some extra checking

This option is not necessary at compile-time as it is subsumed by the
compiler's #defines, but it is useful for code generators such as CAmkES to
know, at generation-time, the native word size of the platform they are
generating code for. Existing mechanisms either hard code a 32-bit platform or
use a set of fragile heuristics to work out the word size. Note that this
option is set automatically and not visible from menuconfig.

IA32 is 32bit version of the x86 architecture. Whilst only IA32
is supported, much of the code is generic x86. Using a generic
x86 architecture will aid in future 64bit support

Use explicit struct packing instead of using compiler asserts
to check that packing happened as expected

The ACPI standard says these fields are 32bits, not the size
of a machine word or pointer

Using an unsigned long instead of forcing to 32bits allows this code
to be reused in a 64-bit context

This is a paranoia commit as most compilers will not
pad members of a struct if they are all the same size,
but this commit ensures it.