template: removed unused symbol

This symbols was used in a xxx_flush_cache() function once, but all this
has been refactored out into libsel4camkes which obtains the information
for the cap from the dataport_frame_t xxx_0 definition.

Co-authored-by: Kent McLeod <kent.mcleod@data61.csiro.au>

seL4HardwareMMIO: Fix cache flushing behavior

For dataports that are mapped cached, in order to perform cache
maintenance operations, the mapping caps need to be copied to the
component. This used to be supported but was broken when camkes next
(3.0.0) was merged as the feature hadn't been correctly reimplemented.

trivial: Suppress compilation warning

trivial: fix another missing bracket

trivial: fix missing bracket

templates: Use large pages for dataports if able

Instead of rounding the dataports to 4K pages all the time, try to use
multiples of larger frames to back the dataports if the size of the
dataports are a multiple of the larger frames.

templates: Update connectors to use new flush code

This commit updates the seL4DTBHardware and seL4HardwareMMIO connectors
to use the new dataport flushing code inside libsel4camkes.

templates: Fix dataport frame vaddr calculation

The original worked fine for small mappings. However, with larger
mappings, there is some weird behaviour with C. I.e. with an offset of
say, 131072 (2^17, 0x20000), 0x30000 + 131072 becomes something like
0x1030000, which is not what we want.

camkes/templates: expose dataport frame details

Adds a symbol array for hardware MMIOs such that connectees can
find caps and details of each mapped frame.

seL4HardwareMMIO: Correctly map phys to virt addrs

/*? me.interface.name ?*/_translate_paddr returns a virtual address for
a physical address within the dataport. Now this correctly translates
for any subrange within the dataport instead of only working for the
first address and whole size of the dataport.

seL4HardwareMMIO: Include aarch64 in cache ops

runner: simplify integrity label handling

This removes set_integrity_label and merges it into alloc, alloc_obj.

We also change register_shared_variable so that it now allocates frames
with a sensible default label. This allows us to drop the manually set
labels from the built-in shared mem templates.

templates: specify connector label when allocating shared memory

This modifies register_shared_variable, etc. to accept a label argument
and updates shared memory templates to pass in the connector label.

As shared frame objects are now allocated under the correct labels,
we no longer need to fix them in object_label_mapping prior to the
integrity verification.

Modify shared regions to use AddrSpaceAllocator

This updates register_shared_variable to use AddrSpaceAllocator instead
of shmem. The relevant filter functions have also been removed.

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.

camkes: Remove kept_symbols from RenderState

This dictionary is unnecessary and forces the generated cmake file to be
run after all other templates.

Keep symbol results in -Wl,-u symbol being passed to the linker, which
is equivalent to attribute((used)) that USED expands to. Note: This
assumes that every generated file is passed to the compiler directly and
not within a library. In this case it may be required for -u to be used.

Refactored hardware dataport frame allocation

When using register_shared_variable only one caller can pass in already allocated frames.
This refactors the frame allocation so that in an N-to-1 scenario only the first template
passes in the frames to register_shared_variable, and the other templates receive the
frame caps through the per template data stash.

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.

Keeping dataport symbols, even if they are unused

Fix licenses

[Fix] Prevent out-of-bound index on dataport flush

When using cached hardware dataports, users could previously specify an
arbitrary size for the region of the dataport to flush, potentially
causing an out-of-bounds array index when searching for the cap to the
frame backing the specified region of the dataport. This change prevents
the out-of-bounds index and returns with an error when an invalid range
is specified.

Print error message when cache flush fails

Including utils/util.h in seL4HardwareMMIO

This file uses the ROUND_UP macro, so explicitly including its definition.

Allow arm_hyp or aarch32 in templates

The checks against the architecture updated here are around pieces
of code that are common for both aarch32 and arm_hyp

[Fix] replaced "arm" with "aarch32" in hardware dataport template

Removed inline from sel4_flush_cache in hardware dataport template

Minor corrections to cached hardware dataports based on code review

Refactored hardware mmio template to remove duplicated code

Treating dataport size as unsigned when computing end address

This is required to prevent a warning for dataports whose size + address
is >= 0x80000000.

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.

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.

Refactored parser init commit.

When translating physical addresses in the hardware MMIO template allow returning a sub range

This allows for a large MMIO region to be defined in a CAmkES specification
and sub ranges of it to be requested through the camkes_io_map interface

HardwareMMIO: Fix: Remove misleading comment.

Both 2M and 4M MMIO region access is supported. The dataport is emitted right
below this comment, so I'm not sure what the rest of it was meant to mean.

Wrap dataport array typedefs in structs to reduce surprises in user code.

Both the `Buf` typedef and the internal area defined for a dataport were byte
arrays. When a user was not consciously aware of these being arrays, it was
possible for them perform casts and pointer operations that had surprising
outcomes. This commit makes both of these structs, and then referenced by
pointers. The in-memory data layout should be unaffected, but this should
reduce surprise misbehaviours in user code.

Closes JIRA CAMKES-369

Optimisation: Use new configuration dictionary interface in the templates.

libsel4camkes: Separate IO functionality from DMA.

Prior to this commit, the DMA allocator functions incorrectly presumed that the
user would want to use ps_io functions to lookup DMA pages by their physical
address. These functions are actually intended to be used to lookup the virtual
addresses of memory-mapped IO devices. This commit separates this functionality
into a separate file and extends IO access functionality to cover IO ports as
well. This is primarily for interaction with libplatsupport. If you are not
using libplatsupport infrastructure, it will probably be simply to directly
invoke CAmkES interface functions.

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

Release snapshot