#
8d83067c |
|
21-Oct-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove TABs from examples
|
#
21e53512 |
|
25-Mar-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Get ARM examples to build; v7-step regression fails though
|
#
4888f523 |
|
15-Oct-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove eqtype declaration for term type
|
#
a59fbbea |
|
22-Oct-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Minor change to the predictability of the CPS instruction, to keep up with the ARM Reference Errata 8. Fix evaluation with regard to LDM/STM instructions with the base register in the register list and write-back enabled. In some places move the position of increment_pc (under operator |||).
|
#
29126407 |
|
23-Jul-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Minor change capturing unpredictable case for LDM -- from latest ARM reference errata 7. Changed the return type for functions provided by arm_parserLib and arm_encoderLib. They now include a symbol table, which identifies the address of labels. Clean up following changes to EmitML. Also, some other tweaks wrt evaluation.
|
#
2d28b95c |
|
24-Jun-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Update that adds support for ThumbEE. /* From the ARM reference... ThumbEE Is a variant of the Thumb instruction set that is designed as a target for dynamically generated code. It is: * a required extension to the ARMv7-A profile * an optional extension to the ARMv7-R profile. */
|
#
1508c7c0 |
|
03-Jun-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fix typo.
|
#
469ce305 |
|
03-Jun-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added support for hardware interrupts: reset, fiq and irq. This adds an extra argument to the next state functions, i.e. we now have arm_next : iiid -> HWInterrupt -> unit M and ARM_NEXT : HWInterrupt -> arm_state -> arm_state option In the absence of an interrupt, the previous behaviour is obtained with ARM_NEXT NoInterrupt : arm_state -> arm_state option The single-step behaviour for interrupts can be obtained with armLib.arm_step "" "reset" (* ARM_NEXT HW_Reset *) armLib.arm_step "" "irq" (* ARM_NEXT HW_Irq *) armLib.arm_step "" "fiq" (* ARM_NEXT HW_Fiq *) There has also been some minor tidying-up to the code.
|
#
a6b4a573 |
|
01-Mar-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Numerous assorted changes, including: - renamed some constants, e.g. sN -> psrN etc. - changed handling of IT state for architecture versions < v6T2. - some fixes to the parser and to the handling of the ADR instruction. - added a couple of functions (arm_parserLib.calc_itstate and arm_random_testingLib.arm_step_updates).
|
#
8f08a545 |
|
22-Jan-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fix to instruction evaluator wrt instructions relying on the theorem condT_set_q. Also, protect occurrences of term_to_string wrt subsequent changes to the term/type grammars.
|
#
1d7ffa1d |
|
22-Dec-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add generate_opcode_nop for testing conditional instructions. Also modify instruction_type to split "msr" into "msr (imm)" and "msr (reg)".
|
#
35063fb3 |
|
13-Dec-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add facility to test specific op-code.
|
#
315a33ff |
|
13-Nov-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fix bug in Thumb2 decoder for ldrsh (imm) and ldrsb (imm). Also made modification to random generator: adds "literal" forms for loads and allows branches to be conditional.
|
#
9b3faefc |
|
12-Nov-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Mask ldm/stm register list for testing.
|
#
838b4cbb |
|
11-Nov-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Remove restrictions on size of load/store immediate offsets for testing.
|
#
2c19e070 |
|
06-Nov-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fix to instruction_type for if-then instruction.
|
#
f81268e5 |
|
03-Nov-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fix bug preventing generation of mov instructions.
|
#
803a6645 |
|
30-Oct-2009 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
Syntax errors fixed.
|
#
e7beb448 |
|
30-Oct-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
instruction_instance was renamed to instruction_type.
|
#
fe82a4e4 |
|
30-Oct-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add a new function "instruction_type" that gives the instruction type (e.g. "ldr (imm)") for a given op-code. Also minor tweak to arm_stepLib.
|
#
f5a5396e |
|
19-Oct-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fix encoding of TBB and TBH. Random testing now avoids store exclusive instructions, which are not supported by arm_stepLib (yet). Random testing now ensures that offsets for branches and loads/stores are fairly small -- this should make it easier to do testing on hardware.
|
#
83dfb4a7 |
|
17-Oct-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
A few changes: 1. Make it clear that the ARMv7-M profile is not properly supported (yet). 2. Fix for EmitML script (following changes to memory). 3. Fixed parsing/encoding for 16-bit Thumb MOV (register) instruction. 4. Fixed bugs in model for BFI, SSAT and SSAT16.
|
#
e152be20 |
|
14-Oct-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Changes to the memory, to conform with the approach that Magnus explored in ARM/experimental. The memory now has type :address -> word8, instead of :address -> word8 option. Accesses are recorded in a component state.accesses : memory_access list.
|
#
632a17bb |
|
12-Oct-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Tweaks to random test generation. Top level function now takes the required encoding type. Also tried to improve the hit rate for Thumb data processing instructions (for ARMv4T and ARMv5T).
|
#
c48cb07f |
|
06-Oct-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Generate a single test case, instead of a list.
|
#
6913e4d7 |
|
29-Sep-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Some fixes to the parser and encoder. Added a new tool "arm_random_testingLib". This randomly generates instructions and derives test vectors (where registers and memory represented as free variables). Magnus will use this to carry out validation checks on hardware.
|