Constraint Solver Techniques for Implementing Precise and Scalable Static Program Analysis

As people rely on all kinds of software systems for almost every aspect of their lives, how to ensure the reliability of software is becoming more and more important. Program analysis, therefore, becomes more and more important for the software development process. Static program analysis helps developers to build reliable software systems more quickly and with fewer bugs or security defects. While designing and implementing a program analysis remains a hard work, making it both scalable and precise is even more challenging. In this dissertation, we show that with a general inclusion constraint solver using unification we could make a program analysis easier to design and implement, much more scalable, and still as precise as expected. We present an inclusion constraint language with the explicit equality constructs for specifying program analysis problems, and a parameterized framework for tuning a constraint system. Implementing an analysis is simplified as generating a set of constraints to be complied with. The equality constraints specifies equivalent analysis variables and thereby could be taken advantage of by a constraint solver to reduce a problem space and improve performance. We show a good balance between performance and precision could be achieved with the framework. We also introduce off-line optimizations for a general constraint solver. The optimizations automatically efficiently detect (potential) equivalent classes. With our case studies on a C pointer analysis, and two data flow analyses for C language, we demonstrate a large amount of equivalences could be detected by off-line analyses, and they could then be used by a constraint solver to significantly improve the scalability of an analysis without sacrificing any precision.