#
086cbeb8 |
|
22-Jun-2017 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
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.
|
#
6accf023 |
|
10-May-2017 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Generalise some MIPS floating-point instructions. The BC1* and C.cond.fmt instructions are no longer specialised to $fcc0 only.
|
#
8116e28b |
|
08-May-2017 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
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.)
|
#
398ba670 |
|
02-May-2017 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fix for MIPS encoder.
|
#
e96ed696 |
|
25-Apr-2017 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add MIPS floating-point instruction encoder.
|
#
40ee118e |
|
19-Apr-2017 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
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).
|
#
6c49cd84 |
|
19-May-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Update the ARMv7, ARM-M0, MIPS and x86-64 models. Exported from the latest version of L3.
|
#
fdeae967 |
|
29-Apr-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
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`.
|
#
d5ee45bd |
|
20-Jan-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
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.
|
#
96edb9f3 |
|
20-Nov-2015 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
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.
|
#
f69520e1 |
|
16-Oct-2015 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Update model for latest version of L3.
|
#
3ba0a168 |
|
06-May-2015 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Update MIPS model and tools. The model now includes an instruction encoder.
|
#
0c2c180e |
|
07-Nov-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Update the MIPS example. The model should detect more instances of branches in the branch delay slot, which is categorised as being unpredictable.
|
#
929272de |
|
17-Sep-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Update the MIPS model to catch more unpredictable cases.
|
#
721f8cf2 |
|
11-Aug-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fix for MIPS SUBU instruction.
|
#
bbe4fa68 |
|
27-Jul-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
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.
|
#
6185d6ad |
|
30-Apr-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Update MIPS model and associated tools.
|
#
301a1603 |
|
19-Feb-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
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.)
|
#
dda2aa5c |
|
10-Feb-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Update to MIPS model. (Just structural changes.)
|
#
6ae8ac7d |
|
27-Jan-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Support for ERET MIPS instruction.
|
#
92710a76 |
|
27-Jan-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fix for MIPS jumps instructions.
|
#
a4c512e2 |
|
23-Jan-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Update MIPS model. Now includes the instructions: MOVN, MOVZ, MUL, MADD, MADDU, MSUB and MSUBU. This extends the model beyond vanilla MIPS III.
|
#
64cf73f2 |
|
27-Nov-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
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.
|
#
28acd234 |
|
15-Nov-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Minor change to ISA models. All ‘rst record fields are now prefixed by the type name.
|
#
1dfd0f84 |
|
16-Aug-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Update to the MIPS model. The decoder is now more strict.
|
#
30e1fe6e |
|
01-Aug-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Extend support for MTC0 and MFC0 instructions (MIPS).
|
#
156fbbfe |
|
23-Jul-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Some minor formatting (printing) changes in the L3 instruction set models.
|
#
db1f8a10 |
|
16-Jul-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add MIPS model (and tools) to examples.
|