Implementation of shape analysis for the byte code of a first-order functional language
This experimental software is based on the paper:
A functional scenario for bytecode verification of resource bounds.
by R.M. Amadio, S. Coupet-Grimal, S. Dal Zilio, L. Jakubiec.
Research Report LIF 17-2004, January 2004.
Extended abstract appeared in Proc. CSL 2004, Springer LNCS.
The paper defines a simple stack machine for a first-order functional
language and shows how to perform size and termination verifications
at the level of the bytecode of the machine.
Usual Java like byte code verification builds for each byte code
instruction an abstract representation of the stack and the information
which is typically computed concerns the types of the values on the
stack. In order to perform size and termination verification, we
refine this abstract representation from types to (typed) first order
expressions and call this analysis `SHAPE ANALYSIS'.
A byte code comes with certain annotations on the function symbols.
The byte code verifier performs a shape analysis and then checks the
validity of the annotations. If this check is positive, it can
conclude that the byte code when executed on the given virtual machine
will terminate and/or run within certain space bounds. This is actually
a THEOREM that we have proved in the quoted paper and that we are currently
formalising in the Coq proof environment.
The software in this distribution includes a compiler from a
first-order functional language to the byte code, an implementation of
the virtual machine, and a program that performs the shape analysis.
It does NOT include the program that checks the validity of
termination and/or size annotations with respect to the shape
analysis, nor tools to synthesize the annotations.
The front-end of the compiler was initially programmed by Roberto Amadio and the virtual
machine by Solange Coupet. Later, a group of undergraduate students
has implemented the shape analysis while structuring and documenting the code.
We have also used the ML code as a `specification' for a
compiler to be realised in C by third year students.
The software can be downloaded
here.