1Specialization of Imperative Programs through Analysis of Relational Expressions

An analysis method for specialization of imperative programs is described in this paper. This anal-ysis is an inter-procedural data flow method operating on control flow graphs and collecting infor-mation about program expressions. It applies to various procedural languages. The set of analyzed formulas includes equivalences between program expressions and constants, linear-ordering ine-qualities between program expressions and constants, equalities originating from some program assignments, and atomic constituents of controlling expressions of program branches. Analysis is executed by a worklist-based fixpoint algorithm which interprets conditional branches and ignores some impossible paths. This analysis algorithm incorporates a simple inference procedure that uti-lizes both positive and negative information. The analysis algorithm is shown to be conservative; its asymptotic time complexity is cubic. A polyvariant specialization of imperative programs, that is based on the information collected by the analysis, is also defined at the level of nodes and edges of control flow graphs. The specialization incorporates a further refinement of analysis information through local propagation. Multiple variants are produced by replicating disjoint subgraphs whose in-links are limited to one node