Add checks for unpredictable ARMv7 encodings.

Improve handling of undefined and unpredictable for VFP instructions.

Support more than one method of detecting floating-point underflow.

Also update the L3 importer, which can be configured for different underflow detection options.

Minor updates to L3 ARM models.

Minor changes within floating-point theory.

• The operations float_negate1985 and float_abs1985 have been removed.
• Added a predicate float_is_signalling and renamed float_some_nan to float_some_qnan.
• Fixed problem with EQ_tm and GT_tm being swapped in binary_ieeeSyntax.

Update ARM model for latest L3.

Simple bit patterns are now handled better.

Update for latest version of L3.

Fix for vmov_double in ARM model.

Many of the changes in arm.sml (record type annotations) come from using a newer version of L3.

Add vldm and vstm to ARMv7 model.

These aren't supported by the "step" or "spec" tools.

Remove UndefinedVFP from ARMv7 model.

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.

Update ARMv7 model for latest version of L3.

Update the ARMv7, ARM-M0, MIPS and x86-64 models.

Exported from the latest version of L3.

Update for the latest version of L3.

Changes have been made when exporting operations of the form:

`f : args -> state -> value * state`

If the state is not changed then this is now exported as

`f : args -> state -> value`

If the state is changed but the `value` type is `unit` then it this is now exported as

`f : args -> state -> state`.

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.

Update for the latest version of L3, which has additional floating-point support.

Cover IEEE754:1985 behaviour for "abs" and "neg". Also adds support for "compare", "toInt" and "fromInt" at the machine level.

Update model for latest version of L3.

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

Some fixes for the L3 ARM model.

A number of bugs were detected when validating the L3 model against the tests used to check the old (monadic) ARM model. These can be found here:

http://www.cl.cam.ac.uk/~mom22/arm-tests/

The bugs were as follows:

1. Off by one error in definition of SignExtendFrom.
2. Off by one error in definition of SignedSatQ.
3. Error in setting Q flag for QDADD.
4. Error in setting the GE flags for USAX and USUB16.
5. Error in the top-halfword result for SXTB16, UXTB16, SXTAB16 and UXTAB16.
6. Error in handling the C flag for some data-processing instructions (looks to affect immediate value variants only).
7. Incorrectly identifying some STRD instructions as unpredictable.

Note that 1-5 relate to instructions that are not supported by the decompiler, and 7 just prevented some valid code from being decompiled. As such, 6 is the most significant error fixed here.

The model now passes all of the tests.

Update for compatibility with the latest version of L3.

The ARM model now includes an instruction encoder.

Also, expose the function arm_eval in arm_stepLib.

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.

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

Update to ARM model.

Fixes MSR (banked register) and MRS (banked register) instructions, in accordance with corrections made within the ARM ARM.

Minor update to ARMv7-AR model.

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.

Minor change to ISA models.

All ‘rst record fields are now prefixed by the type name.

Fix missing IncPC in specification of VMRS instruction.

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.

Support more ARM VFP instructions.

Adds VMOV, VCMP and VMRS.

Fix for Thumb instructions CBZ/CBNZ.

Some minor formatting (printing) changes in the L3 instruction set models.

Reorganisation of files under examples/l3-machine-code.

Changes to the standard L3 ARM model.

These have been brought about by minor modifications to the L3 export (a little bit more simplification occurs).

Fix for ARM MOVW.

Updates to l3-machine-code.

Includes a monadic version of the ARM model, which includes data aborts.

Minor tweaks for l3-machine-code example.

Update L3 ARM model.

Was missing some fixes.

Add some ARM VFP instruction support (under l3-machine-code).

Tweak to treatment of UNKNOWN flag values for multiplies (e.g. MULS) under ARMv4.

Minor fix to ARM specification.

Test for unpredictability of MUL instructions should be "Rd = Rn" and not "Rd = Rm". (Only applies to ARMv4 through to ARMv6.)

New ARM and x86 instruction set models, with tool support for generating Hoare triples.

The new models are generated using a domain specific language; see ITP 2012 paper: "Directions in ISA Specification" (LNCS 7406).

The tools should be quite a bit faster than those found in examples/ARM/v7 and examples/machine-code. However, they are less extensive (this is work-in-progress).