Update L3 examples.

Most changes relate to Poly/ML moving to fixed-width integers.

Various updates to the L3 examples.

Most changes are brought about by improvements and generalisations within stateLib and utilsLib.

A Holmakefile has been added to a new decompilers sub-directory and some *decomp_demoScript files have also been added. This makes it easier to perform regression testing.

Fix glitch with previous check-in.

Print out configuration options when an unrecognised option is supplied.

Make use of alignmentTheory in the l3-machine-code examples.

Improve the interface to stateLib.update_frame_state_thm.

Also add some explanatory comments within stateScript.sml.

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.

Update for L3 examples.

Fixes a potential problem with the handling of word replicate.

Moves some shared code into stateLib (the register_combinations function).

Some other minor fixes.

Update mk_m0_code_pool.

Required after commit e459571.

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

Update ISA models.

The new models are generated by the latest version of L3. This mostly results in just a few formatting (pretty-printing) changes. However, bit-patterns are now expanded out in a different manner. Specifically, applications of “word_extract” (over the match word) are replaced with applications of “v2w” (over the bits generated by “boolify”). Some minor updates were needed to accommodate this change.

The ARMv7 tools now support another memory representation.

Memory can now be treated as a map of type ``:word32 -> word32``.

Also reworked the tools with respect to the handling of word endianness.

Updates for machine-code tools.

Added support for introducing SEP_ARRAY predicates for memory operations (applied to the ARM and M0 models).

Tool support for "LDR (literal)" under M0.

Support for generating TEMPORAL triples.

Currently works for ARM, M0 and MIPS models. Yet to update the x86-64 model.

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

Various updates/improvements to the decompiler tools.

Update M0 tools.

Minor updates to other ISA tools.

Further updates to the tools linking the L3 ARM model to the decompiler.

A lot of code has been generalised (making it usable with other models) and the performance has been improved.

Support a few more M0 instruction instances.

The Hoare-triples for PC-relative loads now have immediate values appearing in the code-pool.

This affects the triples that are generated for instruction such as "ldr r1, [pc, #12]".

The tools for the other ISA models need minor updates following changes in stateLib.

Add ARM-M0 model (and tools) to examples.