Practical Considerations in a Static Stack Checker

Abstract

One difficulty in applying static checking to existing Forth code (rather than accepting only programs written with the checker in mind) is how to deal with words with statically unknown stack effects, such as \code{execute}. The work described in this paper introduces the concept of an \emph{anchor} to represent the basis of the stack depth for a position in the code. A new anchor is introduced after a word with an unknown stack effect. Two anchors are synchronized (if still unrelated) on control-flow joins (e.g., \code{then}), without reporting a stack imbalance (which would probably be a false positive). For previously synchronized anchors, such control flow words can compare the stack depth and report a stack imbalance (probably a mistake) if they do not match. The introduction of anchors also allows to perform the analysis in a single pass.