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.

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: support optional interfaces in proofs

This informs the Isabelle ADL spec about interfaces declared as
`maybe uses` and `maybe consumes`. We do not need to check connectivity
for such interfaces.

templates: arch-definitions: tag wellformed proof

This relies on an annotated simpset from CamkesAdlSpec, so it
involves changing the solver from `code_simp` to `simp`.
The downside is that proofs become a few times slower.

templates, include: explicit Isabelle semantics for connectors

To verify capDL refinement, we need to know the intended semantics for
CAmkES connectors. We use a convention of declaring such semantics in
a new attribute, `isabelle_connector_spec`, which should contain
an Isabelle term of type `connector`. This text is inserted verbatim
when emitting the `Arch_Spec` theory for a CAmkES assembly.

We also add semantics for most of the built-in connectors. These are
merely links to the same built-in connectors of CamkesAdlSpec.
However, other connectors can now declare custom semantics if needed.

templates: arch-definitions: emit hardware flag for components

The formal model in l4v now supports specifying this flag.

templates: arch-definitions: omit exported interfaces from model

The parser already resolves exports in `stage7`, but the export
declarations are left untouched in the `Component`s. This commit
detects and removes them to avoid dangling interfaces in the
Isabelle model.

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: update name handling in arch-definitions.thy

arch-definitions: avoid hardcoding C types; better wellformed_* proofs

Instead of hardcoding basic C types, this passes most of them along as
uninterpreted strings. This allows typedefs such as time_t or ssize_t
to be used, without requiring our formal model to recognise them.

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.

Isabelle templates: qualify entity names in arch spec

This is a stop-gap to prevent short entity names in the input from
clobbering names in the Isabelle context. We still need a proper
name mangling scheme in the future.

Isabelle templates: use Isabelle2018-style import syntax

Isabelle templates: support connectors with multiple from/to ends

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.

Provide explicit theory names

This fixes these theories that were broken when `options.outfile` support was removed
from templates. The new theory names should be equivalent to what was being derived
previously from the outfile name, although if the Makefile template is changed to
generate different file names then these need to be manually updated.

Document outfile deprecation in theory files

The 'outfile' is being removed as an option templates can query, as a result these templates
will break. Adding this comment is meant to aid understanding if someone attempts to use
these theories before they can be fixed.

Fix licenses

Remove another deprecated comment.

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

Fix generation of arch theory for systems involving dataports.

Similar changes to the AST for dataports as for events meant that this template
was referencing invalid members.

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

Fix generation of arch theory with events.

In moving to the newer AST, a component instances emits and consumes now have
types that are just basic strings.

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

arch-definitions: Fix wellformed configuration proof.

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

templates: Use `code_simp` in preference to `eval`.

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

templates: Quote filenames when used as Isabelle terms.

This allows for characters in filenames that disrupt Isabelle's outer syntax,
but are OK in its inner syntax; e.g. "-".

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

Refactored parser init commit.

Trivial: Make some checks against `None` more explicit.

Templates: Access `splitext` through `os.path`.

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

This is slightly clearer and safer.

Add some clarifying comments in THY templates.

arch spec: Remove comment that is no longer relevant.

arch spec: Support for 'refin' parameters.

arch spec: Unconditionally generate correctness lemmas.

This template depended on the external variable `LEMMAS`. Unfortunately support
for passing in extenal variables like this was removed in
71d36f6f1f0fe046d75f037cd713cfac96c24b33. Regardless, it makes no sense to
generate these conditionally as they cost us nothing.

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.

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

Release snapshot