|
CMU-CS-98-178
Computer Science Department
School of Computer Science, Carnegie Mellon University
CMU-CS-98-178
Stack-Based Typed Assembly Language
Greg Morrisett, Karl Crary, David Walker, Neal Glew
November 1998
Also appears as Fox Memorandum CMU-CS-FOX-98-05
CMU-CS-98-178.ps
CMU-CS-98-178.pdf
Keywords: Typed compilation, typed assembly language, certified
code, polymorphic recursion, stacks
In previous work, we presented Typed Assembly Language
(TAL). TAL is sufficiently expressive to serve as a target language
for compilers of high-level languages such as ML. That work assumed
such a compiler would perform a continuation-passing style
transform and eliminate the control stack by heap-allocating
activation records. However, most compilers are based on stack
allocation. This paper presents STAL, an extension of TAL with
stack constructs and stack types to support the stack allocation
style. We show that STAL is sufficiently expressive to support
languages such as Java, Pascal, and ML; constructs such as
exceptions and displays; and optimizations such as tail call
elimination and callee-saves registers. This paper also formalizes
the typing connection between CPS-based compilation and stack-based
compilation and illustrates how STAL can formally model calling
conventions by specifying them as formal translations of source
function types to STAL types.
32 pages
|