A general class of program analyses area combination of context-free and regular language reachability. We define regularly annotated set constraints, a constraint formalism that captures this class. Our results extend the class of reachability problems expressible naturally in a single constraint formalism, including such diverse applications as interprocedural dataflow analysis, precise type-based flow analysis, and pushdown model checking.

We describe flow-insensitive type qualifiers, a lightweight, practical mechanism for specifying and checking properties not captured by traditional type systems. We present a framework for adding new, user-specified type qualifiers to programming languages with static type systems, such as C and Java. In our system, programmers add a few type qualifier annotations to their program, and automatic type qualifier inference determines the remaining qualifiers and checks the annotations for consistency. We describe a tool CQual for adding type qualifiers to the C programming language. Our tool CQual includes a visualization component for displaying browsable inference results to the programmer. Finally, we present several experiments using our tool, including inferring const qualifiers, finding security vulnerabilities in several popular C programs, and checking initialization data usage in the Linux kernel. Our results suggest that inference and visualization make type qualifiers lightweight, that type qualifier inference scales to large programs, and that type qualifiers are applicable to a wide variety of problems.

Many program analyses can be reduced to graph reachability problems involving a limited form of context-free language reachability called Dyck-CFL reachability. We show a new reduction from Dyck-CFL reachability to set constraints that can be used in practice to solve these problems. Our reduction is much simpler than the general reduction from context-free language reachability to set constraints. We have implemented our reduction on top of a set constraints toolkit and tested its performance on a substantial polymorphic flow analysis application.

In prior work [15] we studied a language construct restrict that allows programmers to specify that certain pointers are not aliased to other pointers used within a lexical scope. Among other applications, programming with these constructs helps program analysis tools locally recover strong updates, which can improve the tracking of state in flow-sensitive analyses. In this paper we continue the study of restrict and introduce the construct confine. We present a type and effect system for checking the correctness of these annotations, and we develop efficient constraint-based algorithms implementing these type checking systems. To make it easier to use restrict and confine in practice, we show how to automatically infer such annotations without programmer assistance. In experiments on locking in 589 Linux device drivers, confine inference can automatically recover strong updates to eliminate 95% of the type errors resulting from weak updates.