camkes: Continue new lines in show_attribute_value

If value returned by `show_attribute_value` is going to be used in a
macro, new lines are unfortunately causing a generated code to fail the
build, thus we need to continue line with the `\` character.

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

Get IRQ trigger type through the dts node

Pass trigger type through irq_set. This fix is needed
for odroidc2's serial whose IRQ is edge triggered.

Add seL4DTBHW connector

This connector variant is similar to seL4DTBHardware, but takes a
hardware component on the From end.

global_endpoint_badges: seL4DTBHardwareThreadless

Special case interrupt allocation for seL4DTBHardwareThreadless as this
connector requires more than 1 badge value depending on how many IRQs
the hardware node has.

Fix global_endpoint_badges fencepost behavior

This function would allocate badges from 2 instead of 1.

macros.py: Add parse_dtb_node_interrupts

Move this function from a template implementation to a python
implementation.

Add global_rpc_endpoint_badges macro

This macro assigns badges for different connectors that share the
global-rpc-endpoint object for a component instance. This function could
be thought of as an iterator that returns a set of badges for each
connection. If called for every connection that an instance belongs to,
then the total set of badges returned will be distinct. This allows many
different interfaces to be multiplexed over a single endpoint object.

trivial: Correct comment in global_endpoint_badges

macros.py: Add virtqueue_get_client_id macro

This macro is used in the seL4VirtQueues connector for automatically
assigning client IDs for distinguishing different virtqueue channels
within a single component instance.

templates: Use macro for shared symbol generation

Abstracting away the size and attribute requirements of a shared symbol
prevents each template from having to manage this.

macros: Add global_endpoint_badges macro

This macro is used by the global-endpoints mechanism to assign badge
values based on a full system composition. It forces each connection end
that is signalling the same instance to have a different badge value.

Remove call to gcc for calculating type sizes

This method supported calculating type sizes for types outside of the
Camkes built-in range but isn't used and uses incorrect compiler
arguments.

macros.py: Add get_untypeds_from_range macro

From a range of memory this function computes the untypeds that would
cover the range based on alignment constraints.

trivial: Style changed files

templates: 'Fix' next_page_multiple

Previously `next_page_multiple` calculated the smallest page multiple
that can fit a dataport by multiplying by 2 everytime from a base of
4096. This was because of the dataport size `static_asserts` were
checking if the size was aligned to a power of 2. Now that this isn't
the case anymore (commit 6c191556), we 'fix' `next_page_multiple` so
that it adds increments of 4096. This also helps in saving memory by
only allocating what we need.

support component groups in cdl-refine proof

The capDL refinement specification assumes that all components have
separate integrity domains. This commit adds two changes to handle
component groups:

1. Components in a CAmkES `group` composition are automatically merged
to the label of the group.

2. For components with unstructured integrity semantics (typically
`hardware` components), we recognise a new `<foo>.integrity_label`
attribute to let the user specify another component label. See the
CAmkES apps repository for examples.

Part of VER-1109.

templates: float-free ROUND_UP and ROUND_DOWN macros

templates: clean up testmacros

The exclusion set for testmacros is no longer a limited hack, but now
a more general hack covering more use cases. We move this set to
macros.py to be more self-documenting, and update its entries.

templates: remove unused Isabelle macro

templates: remove capdl_sorter

The sorting is now performed in the capDL-tool and capDL allocator.

templates: support hierarchical identifiers in Isabelle output

This mangles hierarchical identifiers e.g. `foo.bar` into valid
Isabelle identifiers. This relies on capDL-tool performing a similar
mangling (which is currently hardcoded) for the Isabelle capDL spec.

We also prefix Isabelle identifiers for different ADL types e.g.
procedures, components, etc. This is to reduce name conflicts within
the ADL names, as well as conflicts with HOL or l4v builtins.

Implements VER-1012.

templates: Added ROUND_DOWN macro

Updated the macros with a ROUND_DOWN macro. This rounds down a
value to the nearest multiple.

templates: Style macros.py

Ran styling over the macros.py file.

templates: Added page align address macro

Added new macro that aligns (down) an address to the page
boundary.

camkes/templates: remove unused TLS region

This region was used for TLS before actual TLS became available. It is
no longer required.

Use new TLS and sel4runtime support

- minimal crt0.S: construct environment in start.c and via the runtime
- update tls init to be compatible with runtime and move initialisation
to after the runtime is initialised
- wait runtime to be initialised in fault handlers

Macros: Add new next_page_size function

This function will be used in the new seL4DTBHardware connector to find
suitable sizes of memory to map hardware registers in.

templates: Change object naming policy

Objects exist in a global namespace and so need to be named in a way
that doesn't cause collisions. Given that instance names are
unique, also using length of instance names and interface names doesn't
really gain anything and so isn't needed.

Filters: Set scheduling properties in templates

These properties can be set when the objects are created.

Filters: Remove set_tcb_info filter

This filter set the following properties on a TCB:
- elf: the name of the ELF file describing the threads address space
- ip: The program counter of the thread when it is started
- sp: The stack pointer of the thread when it is started
- addr: The address of the IPC buffer for the thread
- init: An array of arguments that are given to the thread.
- sc_slot: A cap to the scheduling context of the thread if it is not
'passive'

These properties are all mostly known when the TCB objects are created
in the templates and we don't need to set them in a filter. The only
special cases are the ip, sp, and addr values that need to be set based
on the virtual address of the symbol in the ELF file. We use simpleeval
to allow the template to save a query that calculates an offset of a
virtual address corresponding to a symbol name so that the values can be
easily calculated once the ELF files are built, but the policy for what
offset into the symbol (e.g. to allow for page guards) can still be
controlled by the template. This mechanism is not Camkes specific and
could be moved into the python-capdl-tool library at a future date.

templates: Refactor TCB creation for components

Create thread stacks, ipc buffers, scheduling contexts, and properties
in one place. Previously having this allocation occuring within a switch
statement made it very hard to understand and maintain.

Now macros.threads() returns an array of all the threads for a component
containing properties for each thread:
- name: The name used for creating objects
- interface: If the thread is an interface thread, what interface it is
for
- intra_index: Index of the thread within an interface that has more
than one thread. 0 if not an interface thread.
- stack_symbol: Name of the stack for this thread
- stack_size: Size of the stack
- ipc_symbol: Name of the ipc buffer symbol for this thread.

The template can then create resources for each thread based on the
contents of this array.

templates: fix pylint errors in get_perm macro

- add missing import of TemplateError
- fix string arguments to exception message
- add missing argument to re.match

templates/macros.py: Updated get_perm argument

Updated get_perm macro argument. The configuration variable
was incorrectly named.

templates: add macro to get/sanitise perms

This is pulled from some duplicated code in global-components

generate consistent app identifier for Isabelle templates

The generated Isabelle theories and ROOT file need to refer to each
other by filename. This commit modifies the tool and build system to
generate a consistent identifier (based on the app name) and pass that
to all the Isabelle templates. This avoids having to hardcode
assumptions about the build system inside the templates themselves.

macros.py: get_word_size uses lookup_architecture

Updated the 'get_word_size' macro to use the lookup_architecture
function from capdl.

templates: Removed constant 64-bit words in CakeML

To allow the CakeML templates to be compatible on 32-bit
platforms, assumptions around 64-bit based word sizes have been
removed. This is replaced by a templated value. Updated the
CakeML source and FFI calls to support variable word sizes.

Change Camkes alignment and section linking policy

There are now special sections created by the Camkes linker script that
are aligned to each of the architecture page sizes. Symbols that require
a certain alignment in order to be backed by an underlying seL4 frame of
a certain size should declare to be in the section of that size. The
purpose of this is to drastically simplify the linking policy shared
between Camkes and the capdl python scripts that would create the
address space objects.

The linker script requirement is because a compiler/assembler is not required to
respect the `align` attribute above a certain small size and any
alignment requirements on the order of page sizes needs to be specified
by a linker script.

These changes make it possible to remove some architecture special cases
that exist in Camkes templates, which is why they are removed.

It is assumed that any of the special policy associated with the special
section names: guarded, shared_*, ignore_* and persistent can still be
implemented by using the new section name with the same alignment, eg
align_12bit for all symbols that require 4k guard pages.

templates: Require all dataports to be fixed size

It was possible for dataports to have an unknown size until the ELF file
had been built and for the size to be based on the type of the C object.
We now require the size of the dataport to be specified at template
rendering time. This enables better alignment optimisation and simpler
code for managing shared seL4 objects.

Use AddressSpaceAllocator for creating guard pages

Stacks and ipc buffers have guard pages that were implemented by running
a filter over the address space objects and deleting the frame before
and after the address regions. This way uses the AddressSpaceAllocator
to explicitly create the guarded sections when the C symbols are
defined. This remove the need for the more complex filter.

camkes: Pass default-stack-size through camkes

This makes it possible for camkes to know the default stack size without
having to build the component into an ELF file.

templates: consistent messages for generated-file warnings

restore 'outfile' context as 'outfile_name'

Isabelle theory templates need to know the output filename. Hence, we
provide the filename as 'outfile_name' when running non-code templates.

macros.py: Remove unused macro

macros: Set length to 0 if array is empty

If we haven't assigned anything to a type we have defined, then just
assume any arrays within the struct have length 0.

macros: only use first value of array for printing

We use the values to calculate how long any array elements in the struct
will be. C doesn't support variable length arrays in struct definitions
unless they are the last field. We just assume the length of the first
value given and leave the compiler to throw an error

Use generic Exception in macros

TemplateError is only a valid exception in a jinja2 context, not in the parent python context.

Macro for finding a C type to fit an integer

change capDL sorting order to match the Haskell capDL tool

The label-mapping proofs apparently rely on this.

templates: Remove unused macro function

Header guards were replaced with #pragma once

Use CONFIG_* versions of configuration definitions

The old definitions like ARCH_ARM are deprecated and should not be used

Fix whitespace

- remove trailing whitespace
- remove duplicate blank lines
- remote blank lines at end of file

Add initial Rumprun support to camkes-tool

Fix licenses

Inline functions to pass unit tests

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.

Remove hardcoded min and max untyped size

More robust sizeof macro

Remove unused template macros.

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

Handle targeting x86_64 from an i386 host in macros.sizeof.

Fix macros.sizeof when targeting x86 from an x86_64 host.

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

Pass architecture to macros.sizeof.

This is not used yet.

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

Fix missing parameter to string.

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

Provide a macro for CapDL object sizes.

This commit cherry-picks part of 30d16b14de71cbc76c731e30727d302de2a3773d and
04a9a04cedf30a950654d307b10b4a10d385d3f1 from
ssh://github.inside.nicta.com.au/mfernandez/project.

Add helper function for printing Isabelle sets.

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

Change ARCH_IA32 to ARCH_X86

Refactored parser init commit.

Implement per-thread stack configuration.

Closes JIRA CAMKES-164

Clean up trailing spaces.

Remove legacy template macros.

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.

Fix: Remove 'development' changes that were accidentally transplanted.

This commit removes a relocation of the IPC buffer and thread stacks to a
separate ELF section. This relocation only makes sense in the context of a
dynamic linker script that is not present on the 'master' branch. Whether these
changes should end up on 'master' eventually is an open question, but for now
we just remove this malformed change.

Fix: Missing return value in macros for array marshalling.

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