bitfield_gen: update proofs to support RISC-V MCS

Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>

bitfield_gen: emit fields in visible order

Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>

bitfield_gen: fixups for MCS

Changes the 'size suffix map' to be useful in more places. In general,
when we use the 'short name' of a variable in these generated proofs, we
run the risk of a change in variable declaration order breaking the
resulting proofs (since declaration order is how the C parser chooses
which variables get the short name). Best practice is to use the long
names whenever possible.

Uses the suffix map for some generated proofs.

Removes an unnecessary simp step.

Signed-off-by: Edward Pierzchalski <ed.pierzchalski@data61.csiro.au>

Convert license tags to SPDX identifiers

This commit also converts our own copyright headers to directly use
SPDX, but leaves all other copyright header intact, only adding the
SPDX ident. As far as possible this commit also merges multiple
Data61 copyright statements/headers into one for consistency.

bitfield_gen: explicit branch predications

gcc8 might get wrong branch predications on these condition checks,
and it could break the code layout.

Add the suffix to the bitfield generation

Clang complains about shifting signed numbers so we need to make sure it
knows it is unsigned

bitfields: Specify iteration order over dicts

In Python 3, dict value iterators aren't deterministic between runs,
which causes nondeterministic definition output order. Some L4V proofs
are sensitive to this order.

Use sorted keys to guarantee order when iterating over values.

python2 --> python3

Update all scripts and build system to call python3, given python2's
upcoming doom. Use sys.maxsize instead of sys.maxint in one script
(maxint does not exist in python3).

style: run autopep8 on python files

bitfield_gen: merge clarsimp/simp in generated proofs

The old generated proofs would fail if a simp set change made
`clarsimp` discharge what `simp` simplified.

bitfield_gen: Improve prune list generation time

Previously this would create a very big regex to parse the input
sources. This didn't scale as well on architectures with more bitfield
objects

Improve generated bitfield proofs

For bitfields requiring sign extension, the generated specs are nicer to
work with in proofs. The proofs also support an updated `sign_extend`
specification (in the l4v repository) which has nicer properties.

This change also speeds up some bitfield proofs.

tools bitfield_gen: proof updates for new base + sign-extension mechanism

tools bitfield_gen: use hex literals in proofs and specs

tools bitfield_gen: simplify theory imports; conform to style

tools bitfield_gen: remove obsolete mask comments

(These masks existed in earlier versions of the bitfield proofs, removed
because the statements were stronger without them.)

tools bitfield_gen: use generic base instead of word32 in proofs

tools: fix licenses

libsel4: fix licenses

- some were incorrectly marked GPL (libsel4 is BSD)
- update NICTA --> DATA61 etc
- fix tags D61 --> DATA61
- update year to 2017

bitfield_gen: generate more efficient *_new and *_ptr_new functions

For blocks and unions, generate only one write for each word, rather
than an update for each bitfield.

For verification, this speeds up some automatically generated proofs.

By not writing a parse.py table, we avoid the parallel build issue of corrupted parse.py files

Import reduce from functools in python scripts

libsel4: Optional public symbols for external interfaces

CONFIG_LIB_SEL4_PUBLIC_SYMBOLS=y will disable inlining for external
interfaces (except deprecated functions), thereby providing public
symbols for easy linkage with other languages.

Bitfields generated with ply rather than yacc

Generated bitfield proofs: use hrs_mem_update.

This is a technical change to the proof mode of the bitfield
generator included in the seL4 source.

The postconditions of the generated specifications of the
*_ptr_set and *_ptr_new functions now describe the entire new
heap via (new_heap = hrs_mem_update (...) old_heap).
Previously they described the contents of various projections
of the heap, which is less precise.

bitfield_gen: write output files atomically

Revert "bf gen: Add a backend for AutoCorres."

This reverts commit 5ee397156373709f58c37f217e9b914017d67e99. This backend was
previously used in an experiment towards libsel4 verification. That project has
since adopted a different strategy and this backend is now unused. Meanwhile
the backend has lagged behind breaking changes to AutoCorres. This commit
removes the backend to avoid confusion from users who believe it to be
functional.

Verification: adjust use of new bf proof features.

Apologies, some final adjustments got lost in the previous pull
request round. This version actually works.

Verification: bf: use new proof features.

The plan here is to move some of the proof script complexity embedded
in the text of the bitfield_gen utility into generic proof helpers in the
l4v repository that bitfield_gen can use more modularly. This is a simple
first step.

tools: bitfield_gen: use six to access range (py3) or xrange (py2)

tools: bitfield_gen: use itertools.chain instead of concatenating lists

This isn't efficient in Python, and moreover in python3 these methods
return iterables, not lists.

tools: bitfield_gen: use integral (//) instead of duck-typed division (/)

tools: bitfield_gen: iterable->list for optparse

tools: bitfield_gen: use '... in ...' instead of dict.has_key

tools: bitfield_gen: use print_function

tools: bitfield_gen: remove trailing whitespace

conversion: fixed bitfield generator, clz spec

bitfield: Correct assertions when using sign extended bases

Streamline libsel4 and remove its libc dependencies.

There are now separate libs for benchmark, assert, printf, putchar
start/stop:

libs/libsel4benchmark
libs/libsel4assert
libs/libsel4printf
libs/libsel4putchar
libs/libsel4startstop

The primary changes are introducing sel4/sel4.h and removing std* types
plus porting assert and IO code from the kernel to libsel4assert,
libsel4printf, libsel4putchar.

This means the code within libsel4 and the newlibs do not overload any
typical libc entities. Instead the libraries use types like
seL4_Uint32 ... instead of uint32_t. And printf is now seL4_Printf and
assert is seL4_Assert ....

Finally, the only file modified that effects kernel code is
kernel/tools/bitfield_gen.py. It needed to be modified as it generates
files for both kernel and user space. And for user space the generated code
(types_gen.h) needed to use the new types and asserts. The changes should
not change what is generated for the kernel and I did a comparison of
kernel_final.{c|s} before and after my change and the only differences
were time stamps.

Bug: #15 Streamline kernel/libsel4 and remove its libc dependencies

bitfield: Allow for controlling how many bits of a word are actually used, and whether the rest of the bits are signed extended or not

bitfield: Allow for using different bases throughout a bitfield file

bitfield: Extend bitfield generator to add a size suffix onto constant mask values

bf gen: Add a backend for AutoCorres.

This commit adds a two new output targets for the bitfield generator,
--autocorres-defs and --autocorres-proofs. These produce, respectively,
abstract definitions of the generated C functions suitable for use in
AutoCorres proofs and WP/simp lemmas suitable for use within AutoCorres proofs
of functions that call the generated C functions. Existing behaviour and
functionality should be unaffected.

bf gen: Fix: Check UMM types is known before generating HOL proofs.

bf gen: Fix: Prevent using stdout when writing HOL defs/proofs.

Stdout is not suitable as an output target for these things.

bf gen: Removed some undefined bit shifts.

The bitfield generator constructs tags as enums. The compiler is free to back
these by any type big enough to cover the enum. The generator emits code that
uses these tag values in mask and shift operations where the target type is
typically a uint32_t. As a result, it can produce code involving undefined
shifts like:

(seL4_CapData_Badge & 0x1) << 31

This commit casts the tag value to the unsigned target type before masking to
ensure everything is done on an appropriate sized unsigned type.

JIRA: SELFOUR-193

bf gen: Fix missing include.

The bitfield generator uses the macros CONST and PURE which, for libsel4, are
defined in macros.h.

bf gen: Fix whitespace in constructors and getters.

Release snapshot