Update for latest version of L3.

Extend floating-point support within the ARMv7 model.

The model can be configured for VFPv2, VFPv3 or VFPv4.

Most VFP instructions are modelled now but some are still missing, i.e.:

• VCVT for fixed-point and half-precision.
• VSTM and VLDM.

Make sure disassembly occurs for ARMv7-A.

Update L3 examples.

Most changes relate to Poly/ML moving to fixed-width integers.

Update SML files generated by L3.

The BitsN library has been sped up by removing word size checks.

Add support for x86-64 assembly code.

Based on NASM syntax, as opposed to AT&T (which is the default for gas).

Extend m0AssemblerLib and armAssemblerLib to include functions for instruction disassembly.

For example:

> print_m0_disassemble `f3ef 8100`;
mrs r1, apsr ; f3ef 8100
val it = (): unit

Add assembly code parsing/printing support for the M0 and ARMv7 models.

There are new entry points to the decompiler. These take a function that maps a quotation (containing machine or assembly code) into a list of strings (typically hex). This facilitate the input of ARM assembly code. For example, the functions:

m0_decompLib.m0_decompile_code
m0_core_decompLib.m0_core_decompile_code
arm_decompLib.arm_decompile_code
arm_core_decompLib.arm_core_decompile_code

are provided with type

: string -> string quotation -> Thm.thm * Thm.thm