#
e5fc0f36 |
|
11-Sep-2017 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Improving naming of bit-vector signed division constants. This renaming introduces incompatibilities: • words$word_sdiv -> words$word_quot (this is proved to be related to int_quot for a non-zero divisor). • words$word_srem -> words$word_rem (this is proved to be related to int_rem for a non-zero divisor). • integer_word$word_sdiv (this is a new constant defined directly in terms of int_div). • words$word_smod -> integer_word$word_smod (this is now defined directly in terms of int_mod).
|
#
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.)
|
#
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).
|
#
3639e156 |
|
14-Jul-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Small fix.
|
#
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`.
|
#
d7726677 |
|
15-Feb-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Update L3 examples. Most changes relate to Poly/ML moving to fixed-width integers.
|
#
aa23933d |
|
29-Jan-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Opening lcsymtacs is no longer necessary.
|
#
34d6b745 |
|
19-Oct-2015 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
When casting from a bool to a bit-vector use "v2w" instead of a conditional expression.
|
#
e9d0138f |
|
06-Mar-2015 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fix for MIPS decompilation. Basic programs seem to be decompiling now.
|
#
6ac8ba08 |
|
08-Dec-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add tool support for the MIPS instructions LWL, LWR, LDL and LDR.
|
#
b8492ebd |
|
27-Nov-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add support for MIPS instructions SC and SCD.
|
#
37c69151 |
|
19-Nov-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
The MIPS tools were experiencing problems with NOP instructions. Reported by Brian Campbell.
|
#
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.
|
#
62bf91d5 |
|
15-Oct-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add some assembly code support for the MIPS tools.
|
#
7238aa61 |
|
17-Sep-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Update the MIPS step tool to support cases when processor exceptions occur in the branch delay slot.
|
#
929272de |
|
17-Sep-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Update the MIPS model to catch more unpredictable cases.
|
#
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.
|
#
4a32990b |
|
08-Jul-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Move some shared code into utilsLib.
|
#
d228277c |
|
01-Jul-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fix names used in some exceptions.
|
#
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.)
|
#
6ae8ac7d |
|
27-Jan-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Support for ERET MIPS instruction.
|
#
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.
|
#
e5073aed |
|
04-Nov-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Updates for machine-code tools. Added support for introducing SEP_ARRAY predicates for memory operations (applied to the ARM and M0 models).
|
#
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).
|
#
e9ff6165 |
|
31-Jul-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Improvements to MIPS tools.
|
#
db1f8a10 |
|
16-Jul-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add MIPS model (and tools) to examples.
|