History log of /seL4-l4v-master/HOL4/examples/machine-code/compiler/compilerLib.sml
Revision Date Author Comments
# 04b1a4d3 03-Jun-2019 Michael Norrish <Michael.Norrish@nicta.com.au>

Fix some examples/machine-code libraries for tight equality

In particular, make sure they are parsing wrt a specific known
grammar. In case of prog_armLib, also make that grammar have loose
equality (a locally visible change).


# 4b814b28 06-Feb-2019 Michael Norrish <Michael.Norrish@nicta.com.au>

Fix code in theorem-prover + machine-code ex's for remove-term-eqtype


# 845531b5 14-Sep-2011 Michael Norrish <Michael.Norrish@nicta.com.au>

Remove trailing whitespace in source files.


# 999d6941 20-Dec-2010 Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk>

Many minor additions/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.


# 79c9c017 10-Jun-2010 Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk>

Register allocator improved.


# 40fc02a8 03-Jun-2010 Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk>

Minor changes.


# 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).


# cdb70f70 03-Dec-2009 Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk>

Minor updates.


# 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?


# 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?


# 0e4ccf01 10-Apr-2009 Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk>

Various minor modifications, also added two files
that were apparently missing from the svn version.


# 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.


# 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.