A Stack-based Typed Assembly Language
Abstract
In previous work, we presented a low-level typed intermediate
language, Typed Assembly Language (TAL), and proved its type system is
sound. TAL is sufficiently expressive to support compilation from
high-level languages such as ML while preserving source level
abstractions. Furthermore, its type system does not impede the use of
traditional low-level optimizations.
The compiler presented was based on a continuation-passing style transform,
which eliminated the need for a control stack by heap allocating stack frames.
However, modern architectures and most compilers are based on stack allocation
of these frames. 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 makes two additional contributions. First, it clarifies the
connection between compilation based on a CPS transform and stack-based
compilation. The latter is seen as a continuation-passing style where
continuation closures are unboxed by the caller and the continuation's
environment is placed on the stack. Second, it illustrates how STAL can
formally model calling conventions by specifying them as formal translations of
source function types to STAL types.
(postscript,
dvi)