Improving naming of bit-vector signed division constants.

This renaming introduces incompatibilities:

• words$word_sdiv -> words$word_quot (this is proved to be related to int_quot for a non-zero divisor).
• words$word_srem -> words$word_rem (this is proved to be related to int_rem for a non-zero divisor).
• integer_word$word_sdiv (this is a new constant defined directly in terms of int_div).
• words$word_smod -> integer_word$word_smod (this is now defined directly in terms of int_mod).

Improvements to updateLib. Added some comments describing the various conversions.

Note that the interface has changed a bit. Some conversions now take a compset (and/or a conversion) instead of a list of theorems.

Support for evaluating instructions of the form "ldr pc,[pc,rn,lsl #2]".

Previously this would not work for certain registers "rn". This now works but a
precondition is added, namely: ARM_READ_REG rn state << 2 <> 0xFFFFFFF8w.
This ensures that the branch destination is not the machine-code value of the
instruction.

Adopt ML-style syntax for case expressions and use freed up "||" for bitwise-or. See issue #24.

Move some definitions from arm_opsem to arm_coretypes.

Added word_sign_extend to src/n-bit.

Change the specification wrt interrupt masking. The function arm_next no
longer masks interrupts -- this is instead left to the level above,
e.g. arm_run.

Other changes include more checking of step theorems in selftest. Also made use
of tools in updateLib.

Add simplification for offsets. For example, where arm_step would give

r1 + 4w + 1w

it will now give

r1 + 5w

A few changes:

- Make use of the new zDefine
- Moved some theorems from arm_stepTheory to arm_opsemTheory and
arm_coretypeTheory, e.g. change_processor_state_thm and encode_psr_bit
- Changed some instruction specifications -- moving the call to
current_mode_is_user_or_system.
- Remove unwanted application of WORD_ARITH_ss in arm_stepLib. This was
inadvertently added in a previous check-in.

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

Fix bug with condition test for le/gt.

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

Make arm_stepLib much more robust with regard to possible
constant name clashes.

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

Add a new function "instruction_type" that gives the instruction
type (e.g. "ldr (imm)") for a given op-code.

Also minor tweak to arm_stepLib.

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.

Changes to the memory, to conform with the approach that Magnus explored in
ARM/experimental.

The memory now has type :address -> word8, instead of :address -> word8 option.
Accesses are recorded in a component state.accesses : memory_access list.

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 overflow problem with parser under Mosml.

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>