runner,templates: Fix generate_seL4_SignalRecv

This function was fixed before to resolve the issue where
seL4_SignalRecv did not exist as a seL4 kernel syscall. The result of
that fix was to generate separate seL4_Signal and seL4_Recv calls. This
altered the macro so that the macro also assigns the result of seL4_Recv
to a variable. However, the macro assumes that the variable that
contains the message info to be sent is the same as the variable that
will store the result of the seL4_Recv/seL4NBSendRecv call.

This isn't a good assumption and so this commit adds in an extra
parameter to the macro for the result variable and also fixes the
missing result assignment for the realtime case. Also update the macro
usage in rpc-connector.c.

runner: Fix generate_seL4SignalRecv

seL4SignalRecv does not exist in the normal kernel, this commit splits
the two calls so that the compilable code can be generated.

trivial: refactor context

A number of checks were being performed
differently. Make this pattern the same
for consistency.

seL4HardwareInterrupt: Add 'arm' irq type support

This allows IRQs on Arm to have the trigger mode and target core
configured. By default Arm IRQs are level triggered and delivered on the
first target core.

In the following configuration IRQ 42 is configured to be edge
triggered:
${instance_name}.${interface_name}_irq_type = "arm";
${instance_name}.${interface_name}_irq_trigger = "edge";
${instance_name}.${interface_name}_irq_number = 42;

python3: Replace reduce with functools.reduce

This runction was removed from builtins in python3.

Update camkes-tool to python3

- Fix minor incompatibilities
- Update scripts to call python3 instead of python2

ast,runner: Remove template field from connector

This allows us to more easily extend the mechanisms for constructing
components and connectors.

Context.py: Shared memory should default to cached

This was the historical behavior that regressed in an earlier refactor.

Update FrameFill declarations to match new api

FrameFills in the capDL spec have been updated to always require
destination_offset and size parameters before the FrameFill subtype
specific parameters.

register_shared_mem: Align symbol to page not size

Symbols that are multiples of pages that aren't power-of-2 sized are
still valid but were being rejected.

register_shared_variable: Move mapping caps

Allow a component to have the caps to a shared variable mapping moved
into its own cspace. This will allow it to perform cache maintenance
operations if necessary.

templates: allow adding to integrity policy

This adds a function `add_policy_extra` to the template context,
allowing templates to add extra integrity policy edges in an ad-hoc
fashion. This is used by the `global-endpoint` template.

Implementation note: we extend the capDL `AllocatorState` to store
this extra policy state. However, the new state class is defined in
the capDL library to work around a limitation of the `pickle` module.

templates: cdl-refine: support IRQs and ASIDs

Part of solving VER-986 i.e. proof support for ARM VMs. This adds basic
support for `vm_minimal`, with a single VM and ASID pool.

Many hacks here. For example, the proof currently assumes that there is
at most one ASID pool. This should be generalised when the kernel
supports multiple VMs, as each one will require its own ASID space.

trivial: fix style

camkes: avoid running renderer in config stage

Avoid running the renderer in the configuration stage (when
camkes_gen.cmake is created) as object-sizes are not defined at this
point.

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.

trivial: Style changed files

runner: Add 'size' arg to register_fill_frames

Previously, register_fill_frames() was only able to register a single 4K
page as a 'fill frame'. By adding a size argument,
register_fill_frames() is now able create multiple fill frames for a
'fill frame' block.

context: Pass capdl Arch object to calc_frame_size

Calling arch.capdl_name() was incorrect as some architectures have
the same capdl name but different page table structures. (aarch32 +
arm_hyp -> arm11, riscv32 + riscv64 -> riscv)

camkes: Remove Perspectives

Perspectives and NameMangling.py was mostly needed to enable the
Filters. As Filters are no longer used, Perspectives should be able to
be safely removed. One point of Perspectives were for encoding policy of
how configuration options were named for certain interfaces, but as new
options are added and new templates are added it seems to have been
easier to encode the naming policy directly in the template where the
config value is obtained.

camkes: Remove version() function

This removes the functionality that hashes the camkes sources.

camkes_version: Remove camkes_release symbol

This symbol is statically initialised to a hash of all camkes sources.
It is being removed as it no longer refers to the actual camkes version,
and there isn't a strong need to read the version from every component.

runner: add support for grantreply

grantreply is a new capability access right in seL4

runner: simplify default args

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.

runner: pre-compile regex in object_label_mapping

Allow templates to manually set integrity labels for objects

This is needed by some connector templates because they allocate
private objects for the parent component. We need to inform the
capDL verification template that these objects are owned by the
component's label.

Fixed for seL4Notification's internal lock objects; other connectors
will undoubtedly also need updating.

extract integrity labels for objects

The object allocator tracks “labels” (corresponding to names of
components and connectors) for each object. While this functionality
was neglected for most CAmkES applications, the labels are necessary
if we want to define an integrity policy for the component system.

Remove remaining references to shmem

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.

Use AddressSpaceAllocator for dma_pools

This removes the need for the replace_dma_frames filter. We also remove
the symbol rename in the objcopy phase as the symbol is private and
won't collide with anything else. This also means
we can remove the dma_pool_symbol entry from the filter NameMangling
list.

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.

runner: Add Cap object to context

Templates can get access to the Cap object via alloc_cap, but they need
to be able to instantiate Cap directly for creating Caps that don't end
up in a CNode, IE for threads cap slots.

runner: Replace fill_frames filter with addr_space

End result in the capdl file should be the same

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.

runner: Use RenderState to capture persistent data

camkes/runner: use new ObjectType and ObjectRights from capdl

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.

register_shared_variable takes a cacheability option

Adds an option to register_shared_variable to, if you are also setting a `paddr`,
set the cacheability of the mapping.

Fix licenses

Ability to get sched_ctrl caps from simple

sched_ctrl caps should be added to a configuration
as component.sched_ctrl = core, where core determines which
CPU core the sched_ctrl cap is for.

Add interface for adding fill information to symbols

capDL frame objects can have an optional 'fill' attribute that instructs the loader
with what to initialize the frame with when loading. This change adds an interface
for adding such information to an existing page sized/aligned symbol

Fix incorrect variable name

Add interface for specifying symbols to keep

CAMKES-560: Add support for new-rt APIs to next

Replace instances of seL4_Recv, seL4_SignalRecv, seL4_Send, with
RT-compliant versions that operate on reply object caps.

Added `lookup_template` to template context

This allows templates to determine the existance of other templates
as they are rendered. This is required for templates to determine
whether connectors have header file templates.

ARM SMMU support in simple template

Adds support for getting ARM IOSpace caps through the simple interface

Shared variables can have preallocated frames

This allows templates to allocate frame objects (using `alloc` and
`alloc_obj`), and associate them with a shared variable through an
additional argument to `register_shared_variable`. A shared variable's
associated frames are used to back the shared variable, rather than
allocating new frames when collapsing shared variables. Only one
instance of a given shared variable may declare associated frames.

Add math and enumerate to template context

Expose CAmkES version to the template context.

Replace usage of DeterministicSet with OrderedSet.

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

Primitive support for realtime seL4

This allows camkes systems to be built to run on realtime seL4. If the
realtime kernel is used, scheduling contexts are created for each
thread. This also adds options to the runner for specifying default
scheduling context field values.

Enforce shared memory constraints in register_shared_variable.

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

Omitting SCs from the capdl spec if rt not enabled

Removed redundant "None" from template context

Removed unused alloc_entity from template context

Ensuring argument to parse_bool is a string

Added parse_bool function to template context

Export functools to the template context.

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

Use configuration to find sc in templates

Some templates need to know the value of the sc attribute of an instance
or interface. A custom function was added to the template context for
looking up a given entity's sc. This change uses the configuration
settings, and camkes name mangling to find the sc instead, removing the
need for these custom lookup functions.

Update import usage within the runner for Python changes.

The aim of this commit is compatibility with Python 2.7.11. These changes
effectively make the runner a first class module (relative imports used
internally; __main__.py importing sources as belonging to a module). The intent
is to remain backwards compatible down to Python 2.6 and forwards to Python
3.5.

[Fix] arch variable in templates set from --arguments option

Find and replace seL4_AsyncEndpointObject with seL4_NotificationObject.

Add missing Derivers

JIRA CAMKES-429

Initialise passive threads from a component's control thread.

JIRA CAMKES-429

Added initial support for scheduling contexts.

This assigns an SC to every thread, unless the user requests not to.
It also adds extra priority config settings for threads.

JIRA CAMKES-429

Refactored parser init commit.

Replaced AsyncEndpoint with Notification. Applied "s/AsyncEndpoint/Notification/g" and "s/aep/notification/g" to each file.

Expose 'itertools' to the template context.

Remove `assert_current_goal`.

This helper function is no longer used in any of the Isabelle templates. Its
functionality has largely been superseded by the `subgoal by` support in
Isabelle 2015.

Export all Python builtins to the templates, instead of one-by-one.

This commit drops the manual export of certain builtins to the template context
and just exports all Python builtins. We don't lose any security here, because
the templates have full access to the runner through other mechanisms anyway.
This commit also stops constructing `namedtuple`s to fake modules and just
exports the modules themselves. This should have no noticeable effect on
functionality unless your template is shadowing a builtin.

Remove deprecated Isabelle helpers.

This commit removes some utility functions that were previously used in proof
templates. These have outlived their usefulness and have been replaced with
more flexible mechanisms.

Template context: export `max` and `min`.

Stop hard-coding 32-bit platform assumptions in template context's `sizeof`.

Remove `__WORDSIZE` from the template context and receive it via build system.

Remove `__SIZEOF_POINTER__`.

The only instance where this was being used was to check whether an argument
fitted in a single message register or two message registers. The width of a
message register is `__WORDSIZE` bits, not `__SIZEOF_POINTER__` bytes.

Template context: Export `tuple`.

Template context: Export `any` and `all`.

These can be useful when making type assertions.

Template context: Stop exporting `splitext`.

** BREAKING CHANGE **

This was polluting the template namespace and is unnecessary when it is
accessible via the (already exported) `os.path`.

Template context: Export `basestring`.

Template context: stop exporting `math.pow`.

As far as I can see this is not in use.

Template context: Expose 'capdl' module to templates.

Use a defaultdict to simplify shared memory registration.

Fix: guard shared variable registration with CSpace, instead of entity.

It was fine to guard shared variable registration with either for the
per-component template, but in connection templates the "entity" in the
connection itself. The intention was actually to guard this registration with
something that corresponded to the address space of the local name. Using the
CSpace isn't perfect, but it's the best we can do for now.

JIRA CAMKES-323

Remove `Joiner`.

This can now be replaced by the Jinja built-in `joiner`.

Closes JIRA CAMKES-357

Expose printing functions for template debugging.

Honestly, I thought these were already visible.

Remove functionality for `show` on RPC parameters.

It did not really make sense to call this function from a template context,
because it displayed parameters in a specific way that was only sometimes
relevant to the context you were in. It was easy to invoke this function in an
invalid context and be mystified as to why you ended up with malformed C.

Pass the entire assembly to the template context and allow templates to look through both the configuration and the composition of the assembly

Fix typo(module "Allocation" does not exist in the python-capdl).

Runner: support interoperation with either branch of python-capdl.

Template context: Expose 'bool'.

Context: Expose 'list' type.

Optimisation: Don't deepcopy AST entities when passing them to templates.

As of 1e50795a727c4a473ab31a0c452e8ca9a515585e (and prior, really) we're
trusting user templates and filtering code^1. This commit goes further along
this line, passing them a modifiable version of the current AST entity, though
note that they are expected not to modify it. Empirically, this shaves ~25
seconds off a non-cached build of the VM project.

1. Realistically, it never made sense not to trust these pieces of code as they
can cause all sorts of chaos anyway, but these copies guarded against buggy,
rather than malicious code.

Template context: Export deepcopy.

Template context: Export 'textwrap'

Template context: Add a mechanism to write C-style include guards.

Jinja provides two mechanisms for including content from another template file,
`import` and `include`. Import, by default, does not include your current
context and imports the target as a module. The result is that any raw text in
the file is not directly included. Include includes your current context, but
does not let the included file modify the context.

For AutoCorres proofs, it is desirable to abstract some general proofs into
templates that we include with a C-like #include mechanism. However the design
described above makes neither suitable as-is for this purpose. This commit adds
a global set that can be used to track the included files and be modified in
included contexts using `do` statements.

Whereas a C header guard would look like:
#ifndef _MY_FILE_H_
#define _MY_FILE_H_
...
#endif
One of these Jinja guards could be written as:
/*- if 'my_file.h' not in included -*/
/*- do included.add('my_file.h') -*/
...
/*- endif -*/

Template context: Expose `chr` and `ord`.

Needed in order to work around some idiocy in Isabelle.

Conflicts:
camkes/runner/Context.py

Template context: Add a function for asserting the current Isabelle subgoal.

Expose the camkes.ast module to template authors.

This allows the template context to perform `isinstance` testing on variables
against AST types.

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

Improve the simple template with variable sized mmio regions, irq capabilities and asid pools

Release snapshot