Get ARM examples to build; v7-step regression fails though

Minor change capturing unpredictable case for LDM -- from latest ARM reference
errata 7.

Changed the return type for functions provided by arm_parserLib and
arm_encoderLib. They now include a symbol table, which identifies the address
of labels.

Clean up following changes to EmitML. Also, some other tweaks wrt evaluation.

Update that adds support for ThumbEE.

/* From the ARM reference...

ThumbEE

Is a variant of the Thumb instruction set that is designed as a target for
dynamically generated code. It is:
* a required extension to the ARMv7-A profile
* an optional extension to the ARMv7-R profile. */

Added support for hardware interrupts: reset, fiq and irq. This adds an extra
argument to the next state functions, i.e. we now have

arm_next : iiid -> HWInterrupt -> unit M

and

ARM_NEXT : HWInterrupt -> arm_state -> arm_state option

In the absence of an interrupt, the previous behaviour is obtained with

ARM_NEXT NoInterrupt : arm_state -> arm_state option

The single-step behaviour for interrupts can be obtained with

armLib.arm_step "" "reset" (* ARM_NEXT HW_Reset *)
armLib.arm_step "" "irq" (* ARM_NEXT HW_Irq *)
armLib.arm_step "" "fiq" (* ARM_NEXT HW_Fiq *)

There has also been some minor tidying-up to the code.

Some changes to make things up-to-date with the latest ARM Architecture
Reference Manual, i.e. errata version 6. The changes mostly relate to the
specification of Undefined and Unpredictable instruction instances.

Numerous assorted changes, including:

- renamed some constants, e.g. sN -> psrN etc.
- changed handling of IT state for architecture versions < v6T2.
- some fixes to the parser and to the handling of the ADR instruction.
- added a couple of functions (arm_parserLib.calc_itstate and
arm_random_testingLib.arm_step_updates).

Fix to instruction evaluator wrt instructions relying on the
theorem condT_set_q.

Also, protect occurrences of term_to_string wrt subsequent changes
to the term/type grammars.

Support for ground-term evaluation of the ARM model within HOL -- the program
memory is implemented as a Patricia tree.

Fix encoding of TBB and TBH.

Random testing now avoids store exclusive instructions, which are not
supported by arm_stepLib (yet).

Random testing now ensures that offsets for branches and loads/stores
are fairly small -- this should make it easier to do testing on hardware.

A few changes:

1. Make it clear that the ARMv7-M profile is not properly supported (yet).
2. Fix for EmitML script (following changes to memory).
3. Fixed parsing/encoding for 16-bit Thumb MOV (register) instruction.
4. Fixed bugs in model for BFI, SSAT and SSAT16.

Some fixes to the parser and encoder.

Added a new tool "arm_random_testingLib". This randomly generates
instructions and derives test vectors (where registers and memory
represented as free variables). Magnus will use this to carry out
validation checks on hardware.

Fix bug in the model (relating to encoding of Thumb2 immediate values).

Also add more checks to encoding function and fixed a couple of bugs in
the parser/encoder/disassembler.

A few refinements. Also added an examples file, which demonstrates how
to use armLib.

A new Monadic ARM instruction set specification. Covers all current ISA
versions i.e. ARMv4 to ARMv7.

Doesn't cover the ThumbEE, VFP and Advanced SIMD extensions. Also doesn't
model hardware interrupts - these will be added at a later date.

To use the armLib tools, Moscow ML users will likely have to apply the patch to
avoid the Chr exception.
<http://hol.sourceforge.net/mosml-chr-instructions.html>