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.

Fixes for EmitML script.

Also, get RFE instructions working (albeit very slowly) with arm_step.

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).

Refinements to the ground-term evaluator. To simplify things, the function
update (=+) sorting conversion has been removed. Instead updates are sorted
just prior to printing.

The elf object file loader now includes the "data" and "rodata" sections.

Poly/ML users can now build a stand-alone ARM assembler by using the code at
the end of arm_evalLib.sml.

add_with_carry has moved to wordsTheory. Also made some tweaks to evaluation.

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