Semantic Type Qualifiers
ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2005), Chicago, Illinois, June 12-15, 2005.
Brian Chin, Shane Markstrum, Todd Millstein
We present a new approach for supporting user-defined type refinements,
which augment existing types to specify and check
additional invariants of
interest to programmers. We provide an expressive language in
which users define new refinements and associated type rules. These
rules are automatically incorporated by an extensible
typechecker during static typechecking of programs.
Separately, a soundness checker automatically
proves that each refinement's type rules ensure
the intended invariant, for all possible
programs. We have formalized our approach and have instantiated it
as a framework for
adding new type qualifiers to C programs. We have used this
framework to define
and automatically prove sound a host of type
qualifiers of different sorts,
including pos and neg for integers, tainted and
untainted for strings,
and nonnull and unique for pointers,
and we have applied our qualifiers to ensure important
invariants on open-source C programs.