#
4a3a6c2b |
|
01-Oct-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Adjust ARM/v7/arm_step tech in light of 44aabdd82 Along the way, make this SML code more independent of the stateful rewriter; previously the code in arm_stepLib could change its behaviour from one invocation to the next if the stateful simpset changed. That's no longer true, but there's currently still a dependency on the state of it when arm_stepLib is loaded.
|
#
8fa159cc |
|
15-May-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix ARM/v7 example for tight equality
|
#
e6364b62 |
|
01-Apr-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Remove the constant bit$LSB, which was simply arithmetic$ODD. This may break some user proofs. Also tidy-up bitScript and numeral_bitScript.
|
#
f6d6a8b2 |
|
09-Dec-2012 |
Michael Norrish <michael.norrish@nicta.com.au> |
Fix a flipped case-constant occurrence in examples/ARM/v7 This is progress with github issue #97.
|
#
0fc75877 |
|
30-Jul-2012 |
Ramana Kumar <ramana.kumar@gmail.com> |
change interface to add_persistent_funs (#73) and fix more calls The new interface takes a list of strings naming theorems. (The old interface took a list of (string * thm) pairs.) The new way better ensures consistency of theory development and theory load behaviour: you can no longer pass a name with a theorem that isn't actually saved under it. Theorems are looked up with DB.theorem, or failing that, DB.definition or DB.axiom. Alas, I found more examples using add_persistent_funs to add theorems in ancestor theories. Rather than modify the ancestor theories, I have opted to make the offending theories save the theorems they want to add to computeLib themselves so they have a name in the current theory to pass to add_persistent_funs. If this behavior was appropriate for patricia too (da47401) change it. Alternatively, if the ancestor theories should have exported those things for computeLib anyway, search this commit for new instances of "save_thm" to see what needs fixing.
|
#
32efb827 |
|
18-Oct-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Support for evaluating instructions of the form "ldr pc,[pc,rn,lsl #2]". Previously this would not work for certain registers "rn". This now works but a precondition is added, namely: ARM_READ_REG rn state << 2 <> 0xFFFFFFF8w. This ensures that the branch destination is not the machine-code value of the instruction.
|
#
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.
|
#
845531b5 |
|
14-Sep-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove trailing whitespace in source files.
|
#
d60adf99 |
|
01-Feb-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Change the specification wrt interrupt masking. The function arm_next no longer masks interrupts -- this is instead left to the level above, e.g. arm_run. Other changes include more checking of step theorems in selftest. Also made use of tools in updateLib.
|
#
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 |||).
|
#
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.
|
#
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.
|
#
29fb3aa5 |
|
26-Mar-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fix a proof.
|
#
eee9a561 |
|
23-Mar-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fixes for EmitML script. Also, get RFE instructions working (albeit very slowly) with arm_step.
|
#
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.
|
#
56fc6a1a |
|
07-Jan-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Change following modification to wordsLib.WORD_BIT_EQ_ss.
|
#
c6842bb3 |
|
02-Dec-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
add_with_carry has moved to wordsTheory. Also made some tweaks to evaluation.
|
#
d74056c8 |
|
27-Nov-2009 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
Added a few cases that were missing.
|
#
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.
|
#
06ca8491 |
|
21-Oct-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Tweak definition of encode_psr and remove some unused code.
|
#
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.
|
#
89c223f3 |
|
01-Oct-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Word slice "<>" has been replaced with "''".
|
#
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>
|