Add checks for unpredictable ARMv7 encodings.

Improve handling of undefined and unpredictable for VFP instructions.

Floating-point update.

• isSignallingNan predicate is added to machine_ieeeTheory.
• The RISC-V model is simplified in places (for DIV and REM).
• The L3 import is extended to cover more operations.

Minor update to some L3 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 L3.

Removes some unnecessary bracketing.

VFP instruction parsing/printing improvements for ARMv7 model.

Fix for VMRS when destination is APSR_nzcv.

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.

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 L3 examples.

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

Update model for latest version of L3.

Update SML files generated by L3.

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

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 L3 machine-code examples.

Some minor changes come from using the latest version of L3 when generating SML code.

The ARMv8 model gains a function for encoding instructions (in the logic). The step tools are updated to support the NOP instruction.

Merge "_,_" instances in patterns.

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