#
21e53512 |
|
25-Mar-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Get ARM examples to build; v7-step regression fails though
|
#
e6eddd82 |
|
10-Dec-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fix in the printing of BFC and BFI instructions. Similar to the previous commit.
|
#
d62154ce |
|
10-Dec-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fix for printing of SSAT and SSAT16 instructions. The immediate values “#32” and “#16” were printing as “#0”.
|
#
a2328149 |
|
23-Sep-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Adopt ML-style syntax for case expressions and use freed up "||" for bitwise-or. See issue #24.
|
#
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. */
|
#
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.
|
#
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.
|
#
add70cef |
|
18-Sep-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fix bug in the model (relating to encoding of Thumb2 immediate values). Also add more checks to encoding function and fixed a couple of bugs in the parser/encoder/disassembler.
|
#
9241c39a |
|
09-Sep-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
A few refinements. Also added an examples file, which demonstrates how to use armLib.
|
#
9dfee26e |
|
18-Aug-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
A new Monadic ARM instruction set specification. Covers all current ISA versions i.e. ARMv4 to ARMv7. Doesn't cover the ThumbEE, VFP and Advanced SIMD extensions. Also doesn't model hardware interrupts - these will be added at a later date. To use the armLib tools, Moscow ML users will likely have to apply the patch to avoid the Chr exception. <http://hol.sourceforge.net/mosml-chr-instructions.html>
|