History log of /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/core_decompilerLib.sml
Revision Date Author Comments
# ac817518 11-May-2015 Anthony Fox <anthony.fox@cl.cam.ac.uk>

Modify the type of HolKernel.syntax_fns and add some documentation.

This is in response to issue #247.

The change to the type makes things a little more natural when using partial applications - for example, HolKernel.syntax_fns1 can be used to provide syntax support for regular unary operations.


# 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


# e609174b 16-Oct-2013 Anthony Fox <anthony.fox@cl.cam.ac.uk>

The ARM-M0 model is now hooked up to the "core/fast" decompiler.


# 8d08dc89 11-Oct-2013 Anthony Fox <anthony.fox@cl.cam.ac.uk>

Various updates/improvements to the decompiler tools.


# e54aed22 07-Oct-2013 Anthony Fox <anthony.fox@cl.cam.ac.uk>

Reorganisation and improvements for the "fast" decompiler.

Now tentatively called the "core" decompiler.