trivial: clean up code for C parser

Remove unused cases and add break in switch statements.
Add conditions to sel4arch.xml.
Change guard in capdl printing to correct TK1_SMMU.
Set KernelArmSMMU default to off.
Add types to aarch32 syscall_stub_gen.py.

Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>

SMMU: binding stream ID to context banks

Providing system calls that binds context banks to stream IDs.
Once the stream ID is bound, the transaction using that SID is
enabled.

Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>

SMMU: assigning vspace to context banks

Supporting user-level applications to assign vsapce root to context
banks through system calls. This commit also configures the context
bank according to stage 1 or stage 2 requirement.

Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>

SMMU: system calls for creating SID and CB caps

Providing system calls on stream ID control cap and context bank
control cap for creating stream ID and context bank caps.

Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>

aarch32: Move tpidruro from vcpu to tcb context

This register is visible to software executing at PL0 but not writeable.
Storing it in the VCPU context required custom save/restore handling as
it had to be explicitly handled when switching from a VCPU thread to a
non-VCPU thread so that it didn't become a channel. It is possible to
now update this register via seL4_TCB_WriteRegisters for software
executing at PL0.

This also fixes a bug where if a vcpu-thread is switched for a
non-vcpu-thread and then switched to a different vcpu-thread the
original vcpu-thread's copy of this register will get set to 0.

Signed-off-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>

Enabled IPC debug features under new config

Introduced a new config flag to enable
userError format strings to be written to the IPC buffer.
Another config bool has been introduced to toggle
printing the error out and this can also be set at runtime.

Signed-off-by: Saer Debel <saer.debel@data61.csiro.au>

Fix python warning in syscall stub generator

The "is" keyword compares addresses. "==" compares values.

Convert license tags to SPDX identifiers

This commit also converts our own copyright headers to directly use
SPDX, but leaves all other copyright header intact, only adding the
SPDX ident. As far as possible this commit also merges multiple
Data61 copyright statements/headers into one for consistency.

aarch64: Move tpidrro_el0 from vcpu to tcb context

This register is visible to software executing at EL0 but not writeable.
Storing it in the VCPU context required custom save/restore handling as
it had to be explicitly handled when switching from a VCPU thread to a
non-VCPU thread so that it didn't become a channel. It is possible to
now update this register via seL4_TCB_WriteRegisters for software
executing at EL0.

This also fixes a potential bug where if a vcpu-thread is switched for a
non-vcpu-thread and then switched to a different vcpu-thread the
original vcpu-thread's copy of this register will get set to 0.

mcs: scheduling context donation over ipc

After this commit, threads blocked on an endpoint can recieve a
scheduling context from the thread that wakes the blocked thread.

mcs: Add a scheduling context object

This is the first part of the seL4 MCS. This commit:

* adds a scheduling context object. Threads without scheduling
context objects cannot be scheduled.
* replaces tcbTimeSlice with the scheduling context object
* adds seL4_SchedControl caps for each core
* adds seL4_SchedControl_Configure which allows users to configure
amount of ticks a scheduling context has, and set a core for the
scheduling context.
* adds seL4_SchedContext_Bind, Unbind and UnbindObject, which allows
a tcb to be bound to a scheduling context.

python2 --> python3

Update all scripts and build system to call python3, given python2's
upcoming doom. Use sys.maxsize instead of sys.maxint in one script
(maxint does not exist in python3).

aarch64: abstract vspace in libsel4

Depending on the physical address range the top level translation table
may be a page upper directory or a page global directory. Rename in
libsel4 the invocations on top level structures to be on an
seL4_ARM_VSpace rather than an seL4_ARM_PageGlobalDirectory.

RFC-3: Update user context for ARM with thread IDs

Switched appropriate naming conventions.
Was using the aarch64, have switched to aarch64 names.

TIPDRURW -> tpidr_el0
TPIDRURO -> tpidrro_el0
TPIDRPRW -> tpidr_el1

Switch TLS register on aarch32 from TPIDURO (tpidrro_el0) to tpidr_ro so
that it can be written to from user-land.

Thread ID registers tpidr_el0 have been added to the user context for
aarch32 and aarch64.

Only the thread ID that is writeable from EL0 is saved in the TCB and
saved/restored on context switch.

Thread IDs that are only changed within a VM (the read-only thread ID
for exception level 0 and the thread ID for exception level 1) are
stored in the VCPU and saved and stored as part of VM enable/disable.

Thread IDs that are only changed with VMs have been separated out into
hypervisor code.

RFC-3: Update context for x86 to use FS and GS.

TLS_BASE virtual register is replaced with FS_BASE and GS_BASE virtual
registers.

The FS_BASE and GS_BASE virtual registers are moved to the end of the
context so they need not be considered in the kernel exit and entry
implementation.

Removed tracking of ES, DS, FS, and GS segment selectors on kernel entry
and exit.

ES and DS are clobbered on kernel entry with the RPL 3 selector for a
DPL 3 linear data segment.

FS is clobbered on exit with the RPL 3 selector for the DPL 3 segment
with FS_BASE as the base. This is done on exit to reload the value from
the GDT.

GS is clobbered on exit with the RPL 3 selector for the DPL 3 segment
with GS_BASE as the base. This is done on exit to reload the value from
the GDT.

Kernel entry and exit code is refactored, simplified, and improved in
light of the above changes.

x64: update verified config to use fsgsbase instr

The verification platform for x64 relies on the fsgsbase instruction.

style: run autopep8 on python files

riscv: add remaining registers to user context.

The registers a7, s2-11, and t3-6 were missing from seL4_UserContext.
We also add these to frameRegisters and gpRegisters, which are used
to implement the TCB invocations for reading and writing these
registers.

Zero-length arrays aren't valid expressions or types in ISO C, so
to keep the c parser happy we need to either remove gpRegisters or
provide some contents for it.

In the past, frameRegisters and gpRegisters distinguished between
those registers preserved across a syscall and those that weren't.
TCB_CopyRegisters allows the caller to choose which set to copy.

Since we preserve all non-return registers, this distinction isn't
relevant anymore and there's no easy way to justify the members of
frameRegisters and gpRegisters.

We arbitrarily choose to put the 'last' register t6 in gpRegisters,
for consistency with the register list in registerset.h and with the
order that registers are restored.

manual: group generated API methods by object type

This change generates doxygen groups for each object type, which allows us to create sections in
output documents for each object. This has the advantage that we can later label those sections and
link to them from the main document. Additionally, it improves nagivation of the API docs.

x86: Introduce IO port control caps

Changes the way IO ports work such that instead of 'minting' IO port caps down into new
IO port caps with smaller ranges new IO port ranges must be allocated centrally from
an IO port control cap. This mechanism acts in a very similar fashion as IRQ handler/control
capabilities and ensures that allocated IO ports do not overlap. Disallowing overlapping
IO ports is necessary to ensure the CDT remains valid as capabilities are deleted.

[SELFOUR-1156] RISC-V Port

Experimental release that supports both RV32 and RV64

libsel4/armv8: Add seL4_ARM_VCPU for aarch64

SELFOUR-1016: Require auth cap to set prio/mcp

This fixes confused deputy problem when setting priorities/mcps.

libsel4: Remove bitfield type unifying Guard and Badge construction

Using the bitfield generator to treat guards and badges as a union type can be convenient,
but it requires reserving a bit in the data for the bitfield run time type information.
This type information is not needed by the kernel as it knows implicitly whether the passed
data is a badge or a guard based on the kind of cap being operated on. However, with the
type information present we cannot pass a word sized piece of data to the kernel.

The solution here is to go back to using a plain seL4_Word as the type for invocations
that want a capdata and let the user either construct a badge as a plain word, or use
the seL4_CNode_CapData bitfield for constructing a guard, although they have to manually extract
the word representation out of it.

libsel4: Return seL4_Error in invocation stubs

Some stubs return structs, which will not change, however instead of
long for those that don't return structs they now return a seL4_Error.

tools: fix licenses

libsel4: fix licenses

- some were incorrectly marked GPL (libsel4 is BSD)
- update NICTA --> DATA61 etc
- fix tags D61 --> DATA61
- update year to 2017

manual: Better inference of method manual labels

Manual labels for methods are inferred unless specified in the api
description. This change extends this inference to prevent slashes
appearing in method labels. It also refactors the logic for label
inference to be more readable.

manual: Improve handling of return type docs

If no documentation is provided for the return value of a function, the
documentation generator will attempt to infer the documentation based on
the return type.

manual: Undocumented return defaults to error enum

manual: Tweak manual label inference

manual: Add label_prefix to method names

Replace division with int division in py scripts

Import reduce from functools in python scripts

Parens around print args in python scripts

aarch64: Add aarch64 libsel4 implementation

manual: Removed default cap description

SELFOUR-675: x64: Increase message registers from 2 to 4

manual: Obj inv stub gen generates doxy comments

This modifies the object invocations stub generator to generate doxygen
comments based on documentation in the xml files it parses.

JIRA: SELFOUR-606

SELFOUR-567: use seL4_CapRights_t from libsel4

This change

* changes seL4_CapRights from the kernel to be seL4_CapRights_t in
libsel4
* deprecates the duplicated seL4_CapRights in libsel4, which is
now the bitfield generated type seL4_CapRights_t.
* fixes all usages in kernel and libsel4

Impact: for verification, this will require the type to change name
from cap_rights to seL4_CapRights_t.
This is a breaking libsel4 API change, although most code uses
seL4_AllRights or similar constants, which will not break
at a source level as these constants have been updated.

Retain in-register error descriptions when not using IPC buffer

- Fixes "lost" error descriptions when using *WithMRs system call
variants [1].
- Only stores real registers to IPC buffer if there's an error.
- If there's an error in a struct-returning function, return
early without setting any struct members.
- Passes the sabre/qemu test suite... with and without --buffer!

[1] https://sel4.systems/pipermail/devel/2016-October/001079.html

libsel4: Move vt-x definitions into common x86

SELFOUR-287: 32-bit vt-x implementation

This is an implementation of vt-x for x86 kernels running in
ia32 mode.

Let x86_64 CallWithMRs

* `syscall_stub_gen.py` now works on x86_64 without passing `--buffer`

update #ifdef to #if in auto generated files

x64/libsel4: Add x64 libsel4 implementation

SELFOUR-276: Add MCP field to threads.

Where MCP = Maximum Controlled Priority

This commit adds:

* seL4_TCB_SetMCPriority

and changes the arguments to

* seL4_TCB_Configure

As of this commit, a thread cannot create or set a threads
priority (including itself) above its mcp. Previously the kernel
did this check against a threads priority, which prevented a thread
from setting it's own priority down and then up again.

fix "syscall_stub_gen.py --word-size" invocation

Fixes #29

tools: Further support for conditional invocation labels

Condition invocation labels where added in commit 73837c8aceabdb1a986bcc2e179f55bf9ee0de3a
This commit guards usage of conditionally generated labels during generation
of the syscall stubs.

Minor fixes for other ARM platforms

Correct merge of master

arm/tk1: a checkpoint for SMMU implementation

SELFOUR-404: fix bug related to double words

They would get shifted by the size of the type rather than the
size of the word. This wasn't detected initially as the master
branch of the kernel does not have any double word types in the API.

SELFOUR-404: Remove hardcoded constants in stub generator.

`syscall_stub_gen` has hardcoded constants for word size, this patch removes
that constraint and makes the word size an argument to the program instead.
The word size can either be passed either as command line arugmemt (-w option)
or a path to the build configuration file can be given(-c option) and the
generator will use the value of `CONFIG_WORD_SIZE` instead.
The `Makefile` in `libsel4` calls the generator with the configuration file as
an option.

Ideally, the architecture should be determined from the configration file, but
since we don't have unit tests for the generator, I will make one change at a
time.

This commit also includes a few changes to make it Python 2.7 compliant.

x86/libsel4: Rename ia32->x86

Rename all functions, constants and types in libsel4 that are in the
general x86 architecture to have an X86 name instead of an IA32 name.
As libsel4 and the kernel share names this requires changing those
in the kernel as well.

All the original IA32 names can still be used for the moment, but are
marked as deprecated.

libsel4: Change syscall_stub_gen to cast constants to the correct word size

Modify Kconfig and Makefile for aach32 as sel4_arch
libsel4: updates to include aarch32 as sel4_arch

Fixes for recent merge with master branch

libsel4: Allow WORD_SIZE_BITS to be changed in the syscall stub generator

libsel4: Generate libsel4 definitions from the current ARCH as well as the SEL4_ARCH

libsel4: Generate non inlined syscall invocations

For performing verification on libsel4 the syscall invocations need
to not be inlined. This provides a (somewhat hacky) way of doing that.

libsel4/tools: Fix: Remove incorrect usage message.

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

Correctly generate a 64-bit type in unmarshalling code in syscall_stub_gen

This was introduced in changeset e653f8f65a916c1babe38a13d1f29e5dfb67390d
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

Streamline libsel4 and remove its libc dependencies.

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

x86: Make x86 the name of the architecture instead of IA32

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

libsel4: Support multiple struct types for the generated syscall stubs

libsel4: Fix trivial comment typos.

syscall stub generator: change CapDataType into a generic BitFieldType for using bitfield generated types in generated invocations

Use usr/bin/env for all python bangpaths to enable virtualenv use.

Very useful with python3 as the default platform.

Recommit of arm_hyp branch on release snapshot

Release snapshot