A Theory of Type Qualifiers∗Jeffrey S. [email protected] F¨[email protected] DepartmentUniversity of California, BerkeleyBerkeley, CA 94720-1776Alexander [email protected] describe a framework for adding type qualifiers to a lan-guage. Type qualifiers encode a simple but highly usefulform of subtyping. Our framework extends standard typerules to model the flow of qualifiers through a program,where each qualifier or set of qualifiers comes with addi-tional rules that capture its semantics. Our framework al-lows types to be polymorphic in the type qualifiers. Wepresent a const-inference system for C as an example appli-cation of the framework. We show that for a set of real Cprograms, many more consts can be used than are actuallypresent in the original code.1 IntroductionProgrammers know strong invariants about their programs,and it is widely accepted by practitioners that such invari-ants should be automatically, statically checked to the ex-tent possible [Mag93]. However, except for static type sys-tems, modern programming languages provide little or nosupport for expressing such invariants. In our view, theproblem is not a lack of proposals for expressing invariants;the research community, and especially the verification com-munity, has proposed many mechanisms for specifying andproving properties of programs. Rather, the problem lies ingaining widespread acceptance in practice. A central issueis what sort of invariants programmers would be willing towrite down.In this paper we consciously seek a conservative frame-work that minimizes the unfamiliar machinery programmersmust learn while still allowing interesting program invariantsto be expressed and checked. One kind of programming an-notation that is widely used is a type qualifier.Type qualifiers are easy to understand, yet they can ex-press strong invariants. The type system guarantees that inevery program execution the semantic properties capturedby the qualifier annotations are maintained. This is in con-trast to dynamic invariant checking (e.g., assert macros or∗This research was supported in part by the National ScienceFoundation Young Investigator Award No. CCR-9457812, NASAContract No. NAG2-1210, and an NDSEG fellowship.In Proceedings of the ACM SIGPLAN ’99 Conferenceon Programming Language Design and Implementation(PLDI), Atlanta, Georgia, May 1999.Purify [Pur]), which test for properties in a particular pro-gram execution.A canonical example of a type qualifier from the C worldis the ANSI C qualifier const. A variable with a type an-notated with const can be initialized but not updated.1Aprimary use of const is annotating pointer-valued functionparameters as not being updated by the function. Not onlyis this information useful to a caller of the function, but itis automatically verified by the compiler (up to casting).Another example is Evans’s lclint [Eva96], which intro-duces a large number of additional qualifier-like annotationsto C as an aid to debugging memory usage errors. Onesuch annotation is nonnull, which indicates that a pointervalue must not be null. Evans found that adding such an-notations greatly increased compile-time detection of nullpointer dereferences [Eva96]. Although it is not a type-based system, we believe that annotations like lclint’s canbe expressed naturally as type qualifiers in our framework.Yet another example of type qualifiers comes frombinding-time analysis, which is used in partial evaluationsystems [Hen91, DHM95]. Binding-time analysis inferswhether values are known at compile time (the qualifierstatic) or may not be known until run time (the quali-fier dynamic) by specializing the program with respect to aninitial input.There are also many other examples of type qualifiers inthe literature. Each of the cited examples adds particulartype qualifiers for a specific application. This paper presentsa framework for adding new, user-specified type qualifiers toa language in a general way. Our framework also extends thestandard type system to perform qualifier inference, whichpropagates programmer-supplied annotations through theprogram and checks them. Such a system gives the pro-grammer more complete information about qualifiers andmakes qualifiers more convenient to use than a pure check-ing system.The main contributions of the paper are• We show that it is straightforward to parameterize alanguage by a set of type qualifiers and inference rulesfor checking conditions on those qualifiers. In particu-lar, the changes to the lexing, parsing, and type check-ing (see below) phases of a compiler are minimal. Webelieve it would be realistic to incorporate our proposalinto software engineering tools for any typed language.1C allows type casts to remove constness, but the result is imple-mentation dependent [KR88].1• We show that the handling of type qualifiers can beseparated from the standard type system of the lan-guage. That is, while the augmented type system in-cludes rules for manipulating and checking qualifiers,in fact the computation of qualifiers can be isolated ina separate phase after standard typechecking has beenperformed. This factorization is similar to that of re-gion inference [TT94].• We introduce a natural notion of qualifier polymor-phism that allows types to be polymorphic in theirqualifiers. We present examples from existing C pro-grams to show that qualifier polymorphism is usefuland in fact necessary in some situations.• We present experimental evidence from a prototypequalifier inference system. For this study, we exam-ine the use of the qualifier const on a set of C bench-marks. We show that even in cases where programmershave apparently tried to systematically mark variablesas const, monomorphic qualifier inference is able to in-fer many additional variables as const. Furthermore,polymorphic qualifier inference finds more const vari-ables than monomorphic inference. This study showsboth that qualifier inference is practical and useful,even for existing qualifiers and programs.The technical observation behind our framework is that atype qualifier q introduces a simple form of subtyping: Forall types τ , either τ  q τ or q τ  τ. Here, as throughthe rest of the paper, we write qualifiers in prefix notation,so q τ represents standard type τ qualified by q. We illus-trate the subtyping relationship using the examples givenabove. In C, non-const l-values can be promoted to constl-values,