#
cd6c9672 |
|
05-Mar-2015 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Towards decompilation of MIPS. Fails for code with branches. Contains minor changes elsewhere (e.g. handling of endianness and quotations).
|
#
be95efdd |
|
20-Jan-2015 |
Michael Norrish <michael.norrish@nicta.com.au> |
Use new Theory.temp_binding to allow "silly" definitions/bindings Previously, bindings made in decompilerLib just got the name "(( step ))"; now the binding machinery rejects this with an exception. So, the code now has to generate a name that the Theory machinery won't reject. As a bonus, this name can't get exported either (though outdating constants will typically serve this purpose as well).
|
#
d2da74b7 |
|
12-Aug-2014 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
ARMv8 model and tools. This model supports AArch64 mode only, i.e. there's no support for the AArch32 mode.
|
#
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
|
#
8d08dc89 |
|
11-Oct-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Various updates/improvements to the decompiler tools.
|
#
c1a3271e |
|
18-Jul-2013 |
Magnus Myreen <magnus.myreen@cl.cam.ac.uk> |
minor bug fix to decompiler
|
#
a5883aa0 |
|
11-Jul-2013 |
Magnus Myreen <magnus.myreen@cl.cam.ac.uk> |
minor clean up under examples/machine-code
|
#
5299625d |
|
11-Jun-2013 |
Magnus Myreen <magnus.myreen@cl.cam.ac.uk> |
x64 for multiword integer division verified
|
#
3ed13bb5 |
|
11-May-2013 |
Magnus Myreen <magnus.myreen@cl.cam.ac.uk> |
bug fix
|
#
4f2e9309 |
|
10-May-2013 |
Magnus Myreen <magnus.myreen@cl.cam.ac.uk> |
rearranging files in examples/machine-code to separate decompiler from ISA models
|
#
c13e8e1d |
|
16-Oct-2012 |
Magnus Myreen <magnus.myreen@gmail.com> |
Fixed another bug due to 632a78
|
#
e83c2008 |
|
16-Oct-2012 |
Magnus Myreen <magnus.myreen@gmail.com> |
Fixed automation that broke due to 632a78 Also did some other tidying up.
|
#
845531b5 |
|
14-Sep-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove trailing whitespace in source files.
|
#
bdcaf18d |
|
28-Feb-2011 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
Minor tweaks.
|
#
999d6941 |
|
20-Dec-2010 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
Many minor additions/changes.
|
#
8f4bb526 |
|
14-Oct-2010 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
Tweaks.
|
#
85e15ca3 |
|
13-Oct-2010 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
More tweaks.
|
#
a10fc67d |
|
07-Sep-2010 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
A minor fixes (and a hack).
|
#
6c11c116 |
|
31-Aug-2010 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
Minor changes.
|
#
36a8973a |
|
24-Aug-2010 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
Minor changes.
|
#
8860e6f7 |
|
22-Jul-2010 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
Minor tweaks.
|
#
415a155c |
|
31-May-2010 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
I've changed the way tail-recursive functions are defined. They are now defined based on a step function: step: 'a -> 'a + 'b Tail-recursive functions loop until their step function returns something in the right component (INR).
|
#
0f547b64 |
|
07-May-2010 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
Multiple minor changes.
|
#
f0eb1065 |
|
12-Apr-2010 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
A few bugs fixed.
|
#
00a8819e |
|
09-Apr-2010 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
Minor update.
|
#
314727fa |
|
01-Mar-2010 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
Many minor changes.
|
#
aaf643a1 |
|
02-Feb-2010 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
A few minor changes.
|
#
90a751a1 |
|
05-Oct-2009 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
Many minor updates.
|
#
4761143b |
|
10-Aug-2009 |
Tjark Weber <Tjark.Weber@cl.cam.ac.uk> |
Removed trailing whitespace from all .sml and .sig files. This affects over 900 files and was done using emacs's delete-trailing-whitespace function in batch mode. Building the system with Poly/ML and Moscow ML seems to work, so I'm hoping these changes don't break anything. Please complain if they do!
|
#
9030ae5a |
|
26-Jun-2009 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
A general update: 1. the decompiler is now slightly faster, due to new code abbreviations (terms smaller in internal proofs); 2. the definition of the machine-code Hoare triple was slightly altered to support instruction caches; 3. the x86 model now includes an instruction cache. Also, I give up on attempting to support MoscowML for examples/machine-code/lisp. Both the standard kernel and the experimental kernel crash while loading files in this directory using the latest patched version of MoscowML. Both kernels exit with an uninformative message: Compiling lisp_equalScript.sml Linking lisp_equalScript.uo to produce theory-builder executable Uncaught exception: Chr Failed to build script file, lisp_equalScript Did they run out of memory? If so, why does the error message not say so?
|
#
8d739bb9 |
|
10-Jun-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove another instance of the illegal SML idiom that I presume Poly/ML accepts.
|
#
8c3fc760 |
|
09-Jun-2009 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
A general update. Now lisp_finalTheory produces assembly files containing the verified LISP interpeteres (in machine code): arm_eval.s x86_eval.s ppc_eval.s Each of these have been successfully run on real hardware, for each respective platform. The proof scripts are likely to only work in the experimental kernel, due to some unfortuante differences between the two kernels. Some of these differences are exposed more frequently now due to recent(ish) changes to the datatype package. Maybe some of the changes made to the datatype package ought to be reconsidered?
|
#
44a6db21 |
|
03-Apr-2009 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
Restructuring and simplification.
|
#
c2f14f37 |
|
05-Mar-2009 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
Improvements to the verified LISP interepreters. The new interpreters have been proved to implement McCarthy's LISP 1.5 as formalise by Mike Gordon for the ACL2 workshop 2007. Warning: lisp_evalScript takes 73 minutes to run using Holmake under PolyML.
|
#
287c084e |
|
21-Jan-2009 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
Updates requested by Lu Zhao.
|
#
7c197d42 |
|
07-Jan-2009 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
A new version of files previously in examples/mc-logic. Eventually examples/mc-logic will be deleted.
|