Remove trust_partner attribute from rpc connectors

This was only used for an optimization that is removed.

Remove maybe_perform_optimized_empty_call

Also remove related configuration options for this optimization
This optimisation is so narrow that it is never used.

python3: Update template to work on python3

filter returns a generator and needs to be converted to a list to take
the len.

Rewrite seL4RPCCall to use an abstract 'connector'

This is a substantial refactor that is meant to make it easier to change how different
templated connections work without having to duplicate a template and change it. In
theory the seL4RPCCall template could be instantiated with a different 'connector' to
give it different behaviours, although the mechanism to change the used connector is not
done in this change.

Whilst intended to be a semantics preserving refactor there are some minor changes. Some
code gets trivial changes of being split into multiple statements or moved into different
blocks. The largest change is some error handling is changed to be 'less helpful' due to
difficulties in getting precise information to the point where the error code now has to be
generated and having nice abstractions.

Fix licenses

Refactored parser init commit.

Refactor RPCCall template

Move most of the functionality of the RPCCall template into common
stubs that are included into the existing RPCCall template.

These common stubs can eventually be refactored and used by the other
existing RPC templates as well as other custom RPC templates

Move variable setting out of 'if' statements in RPC templates

Userspace IPC checking was broken due to variables being
assigned to in an 'if' statement, which is considered a
different scope.

Use void function prototypes where possible for additional type checking.

Closes JIRA CAMKES-371

Remove AST type `Direction`.

This AST object was not gaining us anything as you always needed to look at its
content to do anything with it. In the templates it was inducing strange code
of the form `p.direction.direction`. This commit removes the type entirely. RPC
parameter directions are now represented as bare strings.

This also relevant in movement towards JIRA CAMKES-334.

Check at compile-time that RPC parameters typedefs are not arrays.

The types of RPC parameters can be external references that are expected to be
provided as visible C typedefs at compile-time. In C it is possible for a user
to provide a typedef representing an array type. Such types have different
behaviour to scalar typedefs, in particular the way they are transformed across
function calls.

Typedef-ed arrays like this are not supported as RPC parameters, due to the
glue code's limited ability to introspect these types. This commit adds a best
effort mechanism to induce a compile-time warning if the user has made use of
such an unsupported type.

Closes JIRA CAMKES-306

Optimisation: Use new configuration dictionary interface in the templates.

Qualify input pointers as `const`.

** BREAKING CHANGE **
Functions that correspond to RPC interfaces may need `const` added to some of
their arguments.

This commit alters the prototypes for RPC interfaces to mark input pointers --
specifically 'refin' scalars, 'in' strings and 'in' arrays -- as `const`. The
purpose of this is largely a hint to user programmers, but it can potentially
enable some further compiler optimisations. An effort has been made to maintain
const-ness of pointers internally for the purposes of marshalling as well.

Note that `const` has not been applied to any parameter that manifests as a
double pointer ('in' string arrays, 'refin' strings, 'refin' arrays). The
rationale for this decision was that introducing `const` here actually makes
things *more* complicated for the user. E.g. a `char**` does not naturally
coerce to a `const char**`. The result is a series of confusing compilation
warnings and generated code that the compiler (incorrectly) believes to be
unsafe.

Closes JIRA CAMKES-358

Templates: Be more explicit about testing for None and [].

This commit replaces the idiom 'if foo' with explicit tests for None or the
empty list when that is the intention of the given code. This makes the
templates a little more readable and is necessary to avoid confusion in
relation to some upcoming commits.

Suffix TLS variables with the connection side of their host.

The purpose of this commit is to avoid naming conflicts with the TLS variables
from opposing sides of a connection and their accessors. As for the previous
commit, this is irrelevant for the implementation, but aids verification.
Again, this is expected to have no user-visible effects and no effect on the
generated binaries.

seL4RPC/seL4RPCCall: Rename internal glue code functions to avoid collisions.

This commit renames marshalling and unmarshalling functions that previously had
the same name. These functions were compiled into separate binaries, so this
was not an issue from an implementation perspective, but this caused problems
for verification, where we see both snippets of generated code as the same
translation unit. This commit is expected to have no user-visible effects and
no effect on generated binaries.

Fix some incorrect register constraints.

Support for configurable TLS.

For verification we need to avoid taking the address of local variables. In the
glue code this is difficult because multiple threads may be executing in the
glue concurrently. The current work around for this is per-thread global
variables that can have their address taken. This is added here as a
configuration option with the default remaining the existing behaviour, because
this structure has a non-trivial performance impact. In particular, GCC fails
to determine that our use of static variables does not rely on their previous
value and thus persistent stores to them can be eliminated. Experimenting with
small examples suggests that this is just not an optimisation that GCC ever
attempts. This is unsurprising as this pattern of variable usage is fairly
unusual and would be unlikely to be encountered in handwritten code.

This change should have no visible effect to unaware users.

Templates: Name per-interface error handlers statically.

This allows us to more straightforwardly blacklist these symbols -- which is
also done in this commit -- to avoid them appearing in verification input.

seL4RPC/seL4RPCCall: avoid calls to `memset` where possible.

We were using `memset` to construct a dummy return value when failing glue code
functions. This involved taking the address of a local, which is not compatible
with the verification C parser. We now return a literal when using a return
type that is a native CAmkES type. External C typedefs still require a
`memset`.

This change has no effect on binary code as GCC can - and does - freely convert
assignments and `memset`s back and forth.

Include tls.h in all RPC templates for ease of use.

Use ROUND_UP_UNSAFE in glue code instead of ROUND_UP.

ROUND_UP_UNSAFE is an alternative to ROUND_UP that evaluates its arguments more
than once and thus is sometimes unwise to call. In the context we are invoking
it, it is safe to evaluate the arguments multiple times. The motivation for
this switch is because the verification C parser cannot handle the GNU
statement expressions used in ROUND_UP.

Implement 'refin' as a new parameter direction.

This commit implements a new direction for RPC parameters, 'refin.' In
everything except the C backend, this direction is identical to 'in.' In the C
backend this generates a user function prototype that passes this parameter by
pointer instead of by value. The primary use case of this is for interfaces
involving C types that are typedefed structs. The cost of a function call
involving such types can be decreased by passing the parameter by pointer. In
generaly this should only be used as an optimisation and 'in' should remain the
default direction for input parameters.

seL4RPCCall: Only elide asm clobbers when explicitly trusting components.

This commit introduces an extra degree of safety, wherein users are required to
explicitly use an attribute to declare component instances 'trusted = "true"'
if they want to elide all clobbers in the specialised asm stub. If the partner
you are communicating with is not trusted it is not safe to elide these
clobbers as they can overflow the message length you wre expecting and cause
unexpected behaviour. To my knowledge no one had hit issues like this or were
using this specialisation in the presence of untrusted components, but this is
an added safety measure.

In future it would be possible to introduce more broader stub optimisations to
use seL4_CallWithMRs when we can detect (at generation time) that there is a
payload, but it is short enough to fit in the message registers.

Implement error handling in glue code.

This commit replaces previous assertion placeholders and other assumptions with
a flexible error handling mechanism. For details on how to use this, refer to
the accompanying documentation.

Fix some issues with usage of arrays as return types.

In particular, the size of the returned array was never actually returned to
the caller and was simply discarded. As mentioned in
20f4072ac25eeb707f4e17c4a26501d4b59308ee, these issues are all theoretical as
array return value cannot currently be specified.

Templates: Consolidate and rewrite RPC marshalling code.

This commit moves all RPC marshalling and unmarshalling code into separate
template fragments that are included by the seL4RPC and seL4RPCCall templates.
The marshalling and unmarshalling code is some of the most dense and
edge-case-ridden template code we have, so hopefully this change will make it
more readable and maintainable. Another driving factor for this change is the
upcoming introduction of universal error handling in the glue code.

This change should not have any user-visible effect beyond potential
performance improvements and perhaps fixing latent bugs. The main internal
effects of this commit are:

* String arguments are treated more uniformly. In particular, whenever glue
code needs to dynamically allocate space for a string, it references the
constant `CAMKES_STR_MAX`. Users can refer to this to see how much
information can be passed in string parameters.

* Calls to `memcpy` are emitted inline, instead of calls to
`camkes_marshal_*`. With LTO enabled, your compiler should have been able to
inline the calls to `camkes_marshal_*` previously anyway, but most users
build without LTO. This change inlines `memcpy` invocations always.

* Marshalling and unmarshalling generated as separate, static functions. These
operations were previously done inline in both seL4RPC and seL4RPCCall. The
runtime effect of separating them into individual functions should be nil as
they are static and each called precisely once, so the compiler should
happily inline them. Separating them out does prepare the way for users like
Adrian to provide their own event loop in future, though.

* Method indicies are packed in seL4RPC. The seL4RPCCall connector previously
used the smallest data type that could be used to transmit the method index,
while seL4RPC just always used an `int`. In unifying the code, both now pack
the method index.

* Interfaces with more than 2^32 methods are supported. That is, the method
index is now stored in a 64-bit type when necessary. 2^64 is the new upper
limit on the number of methods you can have in an interface. Having said
that, if you have more than 2^32 methods in an interface you should probably
consult your doctor as pain will most certainly persist.

* Arrays as return types are now supported. If you define an interface method
with a return type that is an array, your C implementation will be
prototyped (and must be implemented) with an additional leading `size_t`
output parameter for the return type's length. Note that array return types
are not currently supported during the parsing phase, so this is more
future-proofing the marshalling code than extra functionality.

* Method indicies for interfaces with 0 methods are handled. This is somewhat
irrelevant as interfaces with 0 methods are not supported during the parsing
phase, but it was a side-effect of code consistency.

* The function `stpcpy` is used pervasively for string marshalling. This is a
POSIX extension and only worth mentioning here because the calls to it will
be removed in a future change that implements bounds checking.

* Dynamically allocated memory in the glue code is freed more eagerly. Some
calls to `free` have been shifted upwards, though this should only be
observable if your heap already had a high occupancy.

Fix: Lock accesses to a userspace IPC window when in use (seL4RPCCall).

Closes JIRA CAMKES-212.

Fix: Check for reference types when specialising syscall stubs.

The code at these locations attempts to determine whether the arguments to an
RPC call can be packed into registers and hit the kernel IPC fastpath.
Unfortunately it assumed that all types of your methods were CAmkES native
types, which was not necessarily true. This commit checks whether we have any
reference types (C typedefs) in the method we're currently looking at
specialising.

Closes JIRA CAMKES-303

Change template license headers to Jinja comments.

The effect of this is that they do not appear in generated output, which was a
bit confusing previously.

Closes JIRA CAMKES-319

Conflicts:
camkes/templates/autocorres/AsynchNativeFrom.template.thy
camkes/templates/autocorres/AsynchNativeTo.template.thy
camkes/templates/autocorres/RPCSimpleFrom.template.thy
camkes/templates/autocorres/RPCSimpleTo.template.thy
camkes/templates/autocorres/SharedDataFrom.template.thy
camkes/templates/autocorres/SharedDataTo.template.thy
camkes/templates/echronos/eChronosAsynch-from.template.c
camkes/templates/echronos/eChronosAsynch-to.template.c
camkes/templates/echronos/eChronosDirectCall-from.template.c
camkes/templates/echronos/eChronosDirectCall-to.template.c
camkes/templates/linker.lds
camkes/templates/linux/component.template.c
camkes/templates/linux/component.template.h
camkes/templates/linux/linuxMQ-from.template.c
camkes/templates/linux/linuxMQ-to.template.c
camkes/templates/linux/linuxMQEmpty-from.template.c
camkes/templates/linux/linuxMQEmpty-to.template.c
camkes/templates/linux/linuxMmap-from.template.c
camkes/templates/linux/linuxMmap-to.template.c

Move Jinja macros into Python.

Jinja macros have unexpected, and often unpleasant, behaviour. A non-exhaustive
list of issues with them is:
- They are not first class Python functions so cannot be passed within the
template context to, e.g., `map`;
- They can mask and inadvertently overwrite your local variables;
- Certain types of references have unexpected expansions within the context of
a macro;
- Calling a macro within a macro is dangerous; and
- You cannot call certain Python functions from within a macro.

This commit transliterates the existing macros into Python, attempting to
preserve all current functionality. This has involved essentially inverting
their implementation such that they become C hosted within Python, rather than
Python hosted within C. The macros are now unconditionally available to all
templates (see Context.py).

This change is intended to be transparent to template authors and CAmkES users.

Conflicts:
camkes/templates/echronos/eChronosAsynch-from.template.c
camkes/templates/echronos/eChronosAsynch-to.template.c
camkes/templates/linux/component.template.h
camkes/templates/linux/linuxMQ-from.template.c
camkes/templates/linux/linuxMQ-to.template.c
camkes/templates/linux/linuxMQEmpty-from.template.c
camkes/templates/linux/linuxMQEmpty-to.template.c
camkes/templates/linux/linuxMmap-from.template.c
camkes/templates/linux/linuxMmap-to.template.c
camkes/templates/macros.jinja

Allow the endpoints used in seL4RPCCall connections to be badged on the -to side and provide a function to retrieve the badge on the -from side

Release snapshot