SELFOUR-1491: verification updates

- renamed an architecture label so that it begins with ARM.
- changed setIRQTrigger so that it takes a boolean value instead of an int.
- Arch_decodeIRQControlInvocation converts the second argument (trigger)
to a boolean immediately.

SELFOUR-1491: add seL4_IRQCOntrol_GetTrigger

Add a new invocation which allows an irq handler capability to be
obtained with a specific trigger method (edge or level). Obtaining
this capability modifies the GIC state.

SMP: Introduce ENABLE_SMP_SUPPORT

- Make it more readable and less confusing compared to the 'CONFIG_MAX_NUM_NODES > 1' check

ARM/IRQ: add a function to initialise local IRQ controller for CPUs

Similar to initIRQController(), cpu_initLocalIRQController() has to
be implemented for each platform. For those that are gonna support
SMP, it should be implemented proprely (if required), otherwise
it can be stubbed for single core implementations.

Replace Arch_handleInterrupt with Arch_finaliseInterrupt

x86: Handle pending interrupt before scheduling thread in handleSyscall

In handleSyscall the current thread may be preempted to handle a pending interrupt.
With kernel mode interrupts in x86 this handling was delayed until we were about
to switch back to user mode. This change unifies the handling with ARM, where the
interrupt is handled prior to calling the thread scheduler.

SMP: guard arch_pause() with #ifdef for verification purposes

[STYLE_FIX]

SMP: move lock.h to architecture-independent include/smp

s/__sync_lock_test_and_set/__atomic_exchange_n in lock.h

Remove many MODIFIES annotations.

These are redundant for any function which the C-to-Isabelle parser
actually analyses, which is now the vast majority of functions.

Fix arm builds broken in 44ed6adb6

SELFOUR-519: remove duplicated constants

* rename physBaseMapping to BASE_OFFSET
* because physBaseMapping was only used explicity in a few places
* move duplicated arm definions up a level
- PPTR_TOP
- PADDR_TOP
- BASE_OFFSET

Refactor duplicated code in hardware.h

One copy to rule them all.

arm-hyp/tk1: fix bugs found during testing

Rearranging headers for aarch32 to 32/mode/*

unsigned int -> word_t

Rename uint32_t -> word_t in any relevant places

arm: Rearrange context switching code to make fastpath and regular code not duplicate functionality

ARM: Add config options for exporting PMU and ARM generic timer physical count registers to PL0

DONT_TRANSLATE more inline asm functions.

The c-parser can now parse these functions, but it does it by
discarding the inline ASM block, creating a misleading and likely
malformed function body. It is better to not translate these
with a DONT_TRANSLATE comment.

This change has been made for the current verification platform
only, and should probably be extended to any other verification
targets as necessary.

Recommit of arm_hyp branch on release snapshot

arm: Add work around for errata on some Cortex-A15 boards and move errata checking to C code

Release snapshot