Generalise some MIPS floating-point instructions.

The BC1* and C.cond.fmt instructions are no longer specialised to $fcc0 only.

Update MIPS tools to support floating-point operations.

This currently omits support for the floating-point memory operations, such as LDC1 and SDC1. (They should be straightforward to support.)

Update MIPS model to include Mike Roe’s floating-point specification.

Also improve treatment of memory operations (so as to be more similar to the CHERI model).

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

Opening lcsymtacs is no longer necessary.

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

Update MIPS model and tools.

The model now includes an instruction encoder.

Towards decompilation of MIPS.

Fails for code with branches.

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

Add tool support for the MIPS instructions LWL, LWR, LDL and LDR.

Add support for MIPS instructions SC and SCD.

Update the MIPS example.

The model should detect more instances of branches in the branch delay slot, which is categorised as being unpredictable.

Update the MIPS step tool to support cases when processor exceptions occur in the branch delay slot.

Update MIPS model and associated tools.

Update for MIPS model and tools.

Simplifies handling of load/stores. (The tools now no longer attempt to accommodate reverse endian mode.)

Fixes modelling of exceptions occurring for an instruction in the branch delay slot. (This has to be properly processed and flagged using the component CP0.Cause.BD.)

Also fixed errors in the specifications of the MADD, MADDU, MSUB, MSUBU, SWR and SDR instructions. (Thanks to Mike Roe for testing the model.)

Update to MIPS model.

(Just structural changes.)

Extend support for MTC0 and MFC0 instructions (MIPS).

Add MIPS model (and tools) to examples.