Some fixes for the ARMv7 step tools.

Fix changing endianness.

Add arm_stepLib tool support for some SUBS PC instructions.

These instructions are used for exception return.

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.

Small improvement to ARM spec tool.

Better treatment of `aligned' under a conditional.

Update L3 examples.

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

Various updates to the L3 examples.

Most changes are brought about by improvements and generalisations within stateLib and utilsLib.

A Holmakefile has been added to a new decompilers sub-directory and some *decomp_demoScript files have also been added. This makes it easier to perform regression testing.

Print out configuration options when an unrecognised option is supplied.

Make use of alignmentTheory in the l3-machine-code examples.

Improve the interface to stateLib.update_frame_state_thm.

Also add some explanatory comments within stateScript.sml.

Modify the type of HolKernel.syntax_fns and add some documentation.

This is in response to issue #247.

The change to the type makes things a little more natural when using partial applications - for example, HolKernel.syntax_fns1 can be used to provide syntax support for regular unary operations.

Towards decompilation of MIPS.

Fails for code with branches.

Contains minor changes elsewhere (e.g. handling of endianness and quotations).

Update ARM tools.

Provides support for a few more instructions.

Update for L3 examples.

Fixes a potential problem with the handling of word replicate.

Moves some shared code into stateLib (the register_combinations function).

Some other minor fixes.

Minor update to ARM tools.

word_memory_introduction now does a bit more simplification.

Refinement to stateLib.introduce_map_definition.

Should do a better job when simplifying reg-map updates.

Add tool support for working with ARM instructions MRS, MSR and RFE.

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

Adapt behaviour of l3_arm_triples (in arm_decompLib),

Provides better handling of load (pc relative) instructions.

Update ISA models.

The new models are generated by the latest version of L3. This mostly results in just a few formatting (pretty-printing) changes. However, bit-patterns are now expanded out in a different manner. Specifically, applications of “word_extract” (over the match word) are replaced with applications of “v2w” (over the bits generated by “boolify”). Some minor updates were needed to accommodate this change.

The ARMv7 tools now support another memory representation.

Memory can now be treated as a map of type ``:word32 -> word32``.

Also reworked the tools with respect to the handling of word endianness.

Updates for machine-code tools.

Added support for introducing SEP_ARRAY predicates for memory operations (applied to the ARM and M0 models).

Tool support for "LDR (literal)" under M0.

Support for generating TEMPORAL triples.

Currently works for ARM, M0 and MIPS models. Yet to update the x86-64 model.

Make the building of SPEC theorems more lazy (when using arm_progLib.arm_spec_hex).

Various updates/improvements to the decompiler tools.

Minor improvements to ARM tools.

Update M0 tools.

Minor updates to other ISA tools.

Updates and improvements to the l3-machine-code decompilation tools.

Further updates to the tools linking the L3 ARM model to the decompiler.

A lot of code has been generalised (making it usable with other models) and the performance has been improved.

Update to ARM tools.

Triples are now generated with a "mode" variable. This is required to satisfy the "GoodMode" predicate. Before concrete modes were used, e.g. "16" for user mode.

In addition, various performance related enhancements have been made in helperLib (especially with regard to AC rewriting for the "*" operator).

The Hoare-triples for PC-relative loads now have immediate values appearing in the code-pool.

This affects the triples that are generated for instruction such as "ldr r1, [pc, #12]".

The tools for the other ISA models need minor updates following changes in stateLib.

Fix for duplicate theorems occurring in the output of arm_progLib.arm_spec_hex.

Support more ARM VFP instructions.

Adds VMOV, VCMP and VMRS.

Missing files from last commit.