Typing Tools for Typeless Stack Languages

Abstract. Many low-level runtime engines and virtual machines are stack based- instructions take parameters from the stack and leave their results on the stack. Stack language is a common name for several lan-guages used to program stack based (virtual) machines- like CLR, JVM, Forth, Postscript, etc. We chose the Forth language as an example to represent the class of stack languages, partially because this language is typeless, partially because there exists a big amount of industrial legacy Forth code that needs to be validated. Usually applications that take advantage of stack machines are mini-malistic and designed to run on restricted environments like electronic devices, smartcards, embedded systems, etc. Sometimes these compo-nents are used to build safety critical systems where software errors are inadmissible. Type checking allows to locate possible errors of stack usage that most often occur in stack language programs. Limited resources give preference to a static solution- run-time type information is expensive to manage and quite useless in turnkey applications. Static type checking is based on a type system that is introduced here for originally typeless stack languages. This external type system is flexible enough to perform several tasks. Static program analysis can be used both for finding er-rors and performing useful transformations on programs (optimization, parallelization, etc.). In this paper a type system to perform the so called must-analysis is described that allows to locate the stack language code where the strong stack discipline is violated. Experimental implementation of the analysis framework is written in Java