Add some SSE (streaming SIMD extensions) instructions to the x86-64 model.

Support x86 "bit test" instructions.

Adds BT, BTS, BTR and BTC.

Minor improvements to x86 model and tools.

The parser now checks for inconsistent use of byte registers.

Minor update to x86 model.

Remove reference to old BadMemAccess x86 exception.

Support a few more instruction in the x86-64 model.

Now covers IDIV, IMUL and multi-byte NOPs.

Update for latest version of L3.

Fix for x86 model.

The RAX and RDX were swapped in the dividend.

Improve x86 encoding for SETcc.

Add SETcc instruction to x86-64 model.

Adapt x64 encoder to avoid use of ARB.

Update x86 model for latest version of L3.

Update x86 model to cover CLC, SMC and STC instructions.

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

Fix misspecification for x86 division.

The divisor is register RDX not RAX.

Minor updates for the x64 model.

• The decoder has been tweaked (mainly for use under SML). Previously it would succeed in decoding an instruction even if there were too few bytes.

• x64DisassembleLib has been removed. The function x64_disassemble has been implemented in x64AssemblerLib.

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.

Simplify the x86-64 model under L3 examples.

The instruction cache has been removed, together with the CPUID instruction. Also, the memory now has type ``: word64 -> word8`` instead of ``: word64 -> word8 option``.

Tweak to x86-64 instruction encoder.

Update for x86-64 model and tools.

- x64Theory now includes an instruction encoder.
- The functions in x64_stepLib have been renamed, e.g. x64_step is now x64_step_hex.

Further refinements to x86-64 decoding.

The decoder now fails when an "address override prefix" is present (the model only considers 64-bit addresses).

Also make another attempt to fix the decoding issue addressed in checkin d69c0c9.

Fix for x86 decoding of instructions with a SIB byte when there is no base register.

Need to read a 32-bit displacement in these cases.

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.

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

Add support for x86 instructions LEAVE and LOOP.

Extend L3 x86 model with support for MOVSX instructions (move with sign extend).

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

Updates to l3-machine-code.

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

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