camkes: Add const expression attributes

Unfortunately C language does not allow constant values to be used as
literals (e.g. when declaring an array), so we need to introduce a
mechanism for converting CAmkES attributes to literals.

`CAMKES_CONST_ATTR` literal has been introduced for that purpose.

Signed-off-by: Slawomir Kwasniak <slawomir.kwasniak@hensoldt-cyber.de>

camkes: Add support for connector header files

A connector can now define template header files that will be included
by camkes.h. This is intended to allow connectors to have public and
private symbols without requiring duplicate definitions.

templates: seL4DTBHardware uses new query format

Updated the seL4DTBHardware template to match the new query
format.

templates: Add WEAK tag to IRQ 'handle' function

With the introduction of the new IRQ interface, the old handle and
acknowledge function pairs can be substituted for the interface.
However, to maintain backwards compatibility, we still allow the old
functions to exist.

templates: Create seL4DTBHardware buffer declares

The buffers created by the seL4DTBHardware connector were not exposed
before, and one had to use 'extern void * foo' to access the buffers.
This commit now declares and exposes those buffers in the component
header file.

camkes: Remove template header mechanism

This was never fully implemented as there was no way for custom
templates to declare templates that weren't C source files.
Given that the only use case can be moved into the main component header
file and still be valid, this mechanism is being removed.

templates: Add interrupt ack and handle prototypes

This is done to distinguish between normal notification interfaces and
hardware-based interrupt notification interfaces. However, the new
prototypes only apply to the seL4DTBHardware connector.

Move component init interfaces to libsel4camkes

These functions are constant and will always be defined by all components and so there is need
for them to be templated. Removing them specifically from the component header also removes the
implication that they should be called by component code when they are intended for internal use
by CAmkES only.

Finally putting these definitions in a library allows them to be used by other library code in
the future, as libraries cannot include per component templates.

Define component_control_main

component_control_main is intended to be the entry point for a component control thread
in potentially different environments. Currently, as there is only one assumed environment,
this just acts as a minor refactor, but once environment support is added this can be
moved to a different template.

Extract control thread init into helpers

Takes the interface thread synchronization logic of the control thread and puts it into
two helper functions. This provides a much cleaner view of what is happening in the control
thread and opens up the possibility for different control logic that reuses these helpers.

Fix AST traversal for enumerating connections

This previously must have assumed that the component's parent was the
assembly composition. However with hierarchical components this isn't
true and this instead gets connections from the top composition passed
in.

Use pragma once instead of header guard based on outfile

Having the 'outfile' be an option templates can query is being removed, as a result
we cannot use it to construct a header guard. Using #pragma once removes the need to
worry about generating a unique header name of any kind, and makes the component
header match other headers that already use #pragma once

Added "hardware_cached" attribute to hardware dataports

Setting the <instance>.<interface>_hardware_cached to the boolean True
enables caching for that region of memory. Setting it to False
disables caching. The default value is False.

Frames backing hardware dataports are allocated by a template

Previously they were allocated in the collapse_shared_frames filter.
Moving their allocation to the template is necessary to support
components being able to flush hardware dataport frames from the cpu
cache. This is necessary because the cap addresses of the frames must be
included in the hardware dataport template. In the
collapse_shared_frames filter, the frames backing hardware dataports are
located by searching the cspace of the component connected to the
dataport.

Fix licenses

CAMKES-584: Add Struct type to camkes

Struct type represents a collection of attributes. Attributes are set by
providing a dictionary of fields and values

CAMKES-584: Add array support for Attributes

This makes it possible to define an attribute as a list of a type.
Assigning values to an attribute can be achieved by using the
`[3,4,5,6]` syntax.

Dataports using seL4SharedData are not volatile

This removes the `volatile` from definition/declarations of shared
variables implementing dataports connected with the seL4SharedData
connector. Dataports now use release/acquire semantics. For a dataport
interface "foo", there are functions `foo_release` and `foo_acquire`
available that prevent memory access re-ordering.

Instantiate and include connector header templates

Added binary_semaphore primitive

s/unsigned int/unsigned; Why use 12 characters when 8 will do?

This commit cherry-picks 6f50d5e0ebf0d97665edc77a23c5f280d9dd8e6d from
ssh://github.inside.nicta.com.au/mfernandez/project.

Optimise a comparison in the per-component header.

This commit cherry-picks b1a52d29b103741401614be12ac046fc8121e5d5 from
ssh://github.inside.nicta.com.au/mfernandez/project.

Tag some glue functions to avoid the user ignoring their return value.

This commit cherry-picks fdcf8f86b52d7b43de086329a4d3f681c78c2823 from
ssh://github.inside.nicta.com.au/mfernandez/project.

Mark RPC interface prototypes as NONNULL_ALL.

This commit cherry-picks 8c32a4562be80cccea3e40e299c606930dea00aa from
ssh://github.inside.nicta.com.au/mfernandez/project.

Expose {interface_name}_get_sender_id for n to 1 seL4RPCCall

Renamed from {interface_name}_get_badge and wasn't previously exposed
This was needed so that the provides app can tell who it is receiving
the request from if required

ARM: Add functionailty for flushing a hardware dataport from the cache

Components connected to hardware dataports can call a function to flush
part or all of the dataport from the cpu cache
(using seL4_ARM_Page_CleanInvalidate_Data). Only relevant when using
cached hardware dataports.

Refactored parser init commit.

Fix: Only check whether 'uses' interfaces are optional, not 'provides'.

It is not valid for a 'provides' interface to be optional. Nevertheless we
checked whether it was when generating the component header. This silently went
through and behaved as expected because we are running in a non-strict mode
[0]. In future we should switch to a strict mode to catch typos like this.

[0]: http://jinja.pocoo.org/docs/dev/api/#undefined-types

Remove support for arrays as return types.

This commit effectively backs out part of
20f4072ac25eeb707f4e17c4a26501d4b59308ee. The motivation for removing support
for this is that array return types are not representable in the upcoming
refactored AST. Note that there is currently no grammar for describing an array
return type anyway, so no end users are relying on this support. The only way
to use an array return type was to programmatically construct a method with one
and I am not currently aware of any uses of this.

Templates: Use explicit comparison when testing against `None`.

This is slightly clearer and safer.

Use void function prototypes where possible for additional type checking.

Closes JIRA CAMKES-371

Abbreviate regex in a template.

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.

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

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.

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.

Merge DMA support from 'development'.

This commit contains the changes to implement support for DMA as well as some
auxiliary changes to how we implement dataports. Specifically, DMA pools can
now be created as described in the docs and allocated from. Memory allocated
from this pool can be reverse looked up to get its physical address(es).

A linker script is introduced in this commit, which is actually part of the (to
come) support for large frames. DMA pools, stacks, IPC buffers and dataports
all end up in specific custom sections. The dataport change that comes as part
of this commit is that we now define dataports in the connection templates (as
opposed to just declaring them there and then defining them in the component
template). This is a little cleaner, though it doesn't remove all dataport code
from the component template.

As of this commit, the dataport declaration the user sees is only tagged as
weak if they have used the 'maybe' keyword. If this is the case, they are
expected to check at runtime whether the dataport is connected or not.

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

Add trywait to semaphore.

Release snapshot