Static analysis of multistaged programs via unstaging translation

Static analysis of multi-staged programs is challenging because the basic assumption of conventional static analysis no longer holds: the program text itself is no longer a fixed static entity, but rather a dynamically constructed value. This article presents a semantic-preserving translation of multi-staged call-by-value programs into unstaged programs and a static analysis framework based on this translation. The translation is semantic-preserving in that every small-step reduction of a multi-staged program is simulated by the evaluation of its unstaged version. Thanks to this translation we can analyze multi-staged programs with existing static analy-sis techniques that have been developed for conventional unstaged programs: we first apply the unstaging translation, then we apply conventional static analysis to the unstaged version, and finally we cast the analysis results back in terms of the original staged pro-gram. Our translation handles staging constructs that have been evolved to be useful in practice (typified in Lisp’s quasi-quotation): open code as values, unrestricted operations on references and in-tentional variable-capturing substitutions. This article omits refer-ences for which we refer the reader to our companion technical report