#
4888f523 |
|
15-Oct-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove eqtype declaration for term type
|
#
335c2a01 |
|
23-Jan-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fix for Thumb-2 decoding of "MSR spsr, <Rn>".
|
#
c1e0d4fe |
|
22-Sep-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
A few changes: - Make use of the new zDefine - Moved some theorems from arm_stepTheory to arm_opsemTheory and arm_coretypeTheory, e.g. change_processor_state_thm and encode_psr_bit - Changed some instruction specifications -- moving the call to current_mode_is_user_or_system. - Remove unwanted application of WORD_ARITH_ss in arm_stepLib. This was inadvertently added in a previous check-in.
|
#
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).
|
#
a6edb681 |
|
24-Nov-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Support for ground-term evaluation of the ARM model within HOL -- the program memory is implemented as a Patricia tree.
|
#
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>
|