#
98207e9d |
|
31-Jan-2018 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add checks for unpredictable ARMv7 encodings.
|
#
78f3d14b |
|
30-Jan-2018 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Improve handling of undefined and unpredictable for VFP instructions.
|
#
3a981fec |
|
21-Sep-2017 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add some whitespace to signature files.
|
#
161d7acc |
|
02-Jul-2017 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Floating-point update. • isSignallingNan predicate is added to machine_ieeeTheory. • The RISC-V model is simplified in places (for DIV and REM). • The L3 import is extended to cover more operations.
|
#
27d6cfb0 |
|
27-Jun-2017 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Minor update to some L3 models.
|
#
086cbeb8 |
|
22-Jun-2017 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Minor changes within floating-point theory. • The operations float_negate1985 and float_abs1985 have been removed. • Added a predicate float_is_signalling and renamed float_some_nan to float_some_qnan. • Fixed problem with EQ_tm and GT_tm being swapped in binary_ieeeSyntax.
|
#
fd546f27 |
|
08-May-2017 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Update ARM model for latest L3. Simple bit patterns are now handled better.
|
#
d34415b5 |
|
02-May-2017 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Update for latest L3. Removes some unnecessary bracketing.
|
#
8f9e3151 |
|
11-Apr-2017 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
VFP instruction parsing/printing improvements for ARMv7 model. Fix for VMRS when destination is APSR_nzcv.
|
#
4b08982c |
|
03-Apr-2017 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Update for latest version of L3.
|
#
7e1d02fe |
|
17-Feb-2017 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fix for vmov_double in ARM model. Many of the changes in arm.sml (record type annotations) come from using a newer version of L3.
|
#
e821cde6 |
|
05-Aug-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add vldm and vstm to ARMv7 model. These aren't supported by the "step" or "spec" tools.
|
#
893e1146 |
|
02-Aug-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Extend floating-point support within the ARMv7 model. The model can be configured for VFPv2, VFPv3 or VFPv4. Most VFP instructions are modelled now but some are still missing, i.e.: • VCVT for fixed-point and half-precision. • VSTM and VLDM.
|
#
685f5a80 |
|
22-Jun-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Update ARMv7 model for latest version of L3.
|
#
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.
|
#
f69520e1 |
|
16-Oct-2015 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Update model for latest version of L3.
|
#
8f1ae54e |
|
15-Jul-2015 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Update SML files generated by L3. The BitsN library has been sped up by removing word size checks.
|
#
dcc2c549 |
|
24-Nov-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Some fixes for the L3 ARM model. A number of bugs were detected when validating the L3 model against the tests used to check the old (monadic) ARM model. These can be found here: http://www.cl.cam.ac.uk/~mom22/arm-tests/ The bugs were as follows: 1. Off by one error in definition of SignExtendFrom. 2. Off by one error in definition of SignedSatQ. 3. Error in setting Q flag for QDADD. 4. Error in setting the GE flags for USAX and USUB16. 5. Error in the top-halfword result for SXTB16, UXTB16, SXTAB16 and UXTAB16. 6. Error in handling the C flag for some data-processing instructions (looks to affect immediate value variants only). 7. Incorrectly identifying some STRD instructions as unpredictable. Note that 1-5 relate to instructions that are not supported by the decompiler, and 7 just prevented some valid code from being decompiled. As such, 6 is the most significant error fixed here. The model now passes all of the tests.
|
#
06401b70 |
|
18-Nov-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Update for L3 machine-code examples. Some minor changes come from using the latest version of L3 when generating SML code. The ARMv8 model gains a function for encoding instructions (in the logic). The step tools are updated to support the NOP instruction.
|
#
22ffb16d |
|
16-May-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Merge "_,_" instances in patterns.
|
#
17aa1139 |
|
08-May-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add tool support for working with ARM instructions MRS, MSR and RFE.
|
#
cc9dd295 |
|
21-Feb-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add assembly code parsing/printing support for the M0 and ARMv7 models. There are new entry points to the decompiler. These take a function that maps a quotation (containing machine or assembly code) into a list of strings (typically hex). This facilitate the input of ARM assembly code. For example, the functions: m0_decompLib.m0_decompile_code m0_core_decompLib.m0_core_decompile_code arm_decompLib.arm_decompile_code arm_core_decompLib.arm_core_decompile_code are provided with type : string -> string quotation -> Thm.thm * Thm.thm
|