Extending Typestate Checking Using Conditional Liveness Analysis

Abstract

We present a practical extension to typestate checking which is capable of proving programs free of uninitialized variable errors even when these programs contain conditionally initialized variables where the initialization of a variable depends upon the equality of one or more “tag” variables to a constant. The user need not predeclare the relationship between a conditionally initialized variable and its tags, and this relationship may change from one point in the program to another. Our technique generalizes liveness analysis to conditional liveness analysis. Like typestate checking, our technique incorporates a dataflow analysis algorithm in which each point in a program is labeled with a lattice point describing statically tracked information, including the initialization of variables. The labeling is then used to check for programming errors such as referencing a variable which may be uninitialized. Our technique incorporates a more expressive lattice, including predicates of the form: “x is initialized if y equals 2.” Because the number of tags per variable is small, the added complexity of the analysis is usually small. The efficiency of our technique is due, to a large extent to the fact that we use a backwards analysis of the program (instead of the forward analysis used in the original typestate checking algorithm). Our results suggest that backwards analy sis—tracking only those properties which need to hold to make the subsequent statements correct—can be more efficient that forward analysis—tracking all properties which are made true by the preceding statements. We conclude with some additiona applications of our techniques to program checking. © 1993 IEEE