licenses: convert license tags to SPDX

asmrefine: Add support for 64-bit architectures.

asmrefine: arch split CFunDump files

Now that asmrefine targets several arches, it's useful to separate out
any intermediate artefacts by L4V_ARCH. For instance, this lets us use
the same directory to test two arches at once.

asmrefine: update to Isabelle2019; reduce warnings

Isabelle2018: new AsmRefine session + test

Isabelle2018: new "op x" syntax; now is "(x)"

(result of "isabelle update_op -m <dir>")

globally use session-qualified imports; add Lib session

Session-qualified imports will be required for Isabelle2018 and help clarify
the structure of sessions in the build tree.

This commit mainly adds a new set of sessions for lib/, including a Lib
session that includes most theories in lib/ and a few separate sessions for
parts that have dependencies beyond CParser or are separate AFP sessions.
The group "lib" collects all lib/ sessions.

As a consequence, other theories should use lib/ theories by session name,
not by path, which in turns means spec and proof sessions should also refer
to each other by session name, not path, to avoid duplicate theory errors in
theory merges later.

Removes all trailing whitespaces

Support extra specs, ctzl, clzl in SimplExport.

This patch permits the user to supply additional specs for functions
whose bodies were not imported (DONT_TRANSLATE or not present in parsed
C source). Those specs are exported by SimplExport.

The existing apparatus can import builtin functions like ctzl/clzl in C
sources by admitting them without bodies (DONT_TRANSLATE) and giving
them axiomatic Hoare triples (FNSPEC).

Translation validation then requires export of useful semantics. The user
can supply a made-up body, and show that it is a refinement of the body
that the parser created (derived from the FNSPEC and MODIFIES clauses).
The body must export out the graph language correctly. For ctzl/clzl etc
this is easy.

Isabelle2016-1: update references to renamed constants and facts

Handling of AsmStmt in c-parser, more tests.

The C-parser contains a full parser for __asm__ syntax but
up until now hasn't done anything with it. Instead we export
some semantics. It's unspecified exactly what these semantics
are but they are parametrised with the __asm__ semantics that
went in to them, so the translation validation has something
to reason about.

Tweak modifies proofs as a result, and add some more test files.

Isabelle2016: SimplExportAndRefine updated for RC3

Repair SimplExport/GraphRefine.

Improve guard handling in GraphRefine.

Needed for recent changes to how global validity assertions are
generated.

Progress on upgrading GraphRefine.

Needed to handle new concepts being exported from Simpl.

WIP on WCET annotations.

asmrefine: 2015 udpate

more Isabelle2015 update; AInvs up to (excluding) Syscall_AI

also includes some global replacements

Adjustments in GraphLang to support CDSL.

Update graph-refine for StaticFun change, bugfix.

Fix asmrefine stuff for 2014 branch.

some of the global Isabelle2014 renames

option_case -> case_option
sum_case -> case_sum
prod_case -> case_prod
Option.set -> set_option
Option.map -> map_option
option_rel -> rel_option
list_all2_def -> list_all2_iff
map.simps -> list.map
tl.simps -> list.sel(2-3)
the.simps -> option.sel

Import release snapshot.