Control-Flow Analysis with SAT Solvers

Abstract. Control-flow analyses statically determine the control-flow of programs. This is a nontrivial problem for higher-order programming languages. This work attempts to leverage the power of SAT solvers to answer questions regarding control-flow. A brief overview of a tra-ditional control-flow analysis is presented. Then an encoding is given which has the property that any satisfying assignment will give a con-servative approximation of the true control-flow, along with additional ideas to improve the precision and efficiency of the encoding. The results of the encodings are then compared to those of a traditional implementa-tion on several example programs. This approach is competitive in some instances with hand-optimized implementations. Finally, the paper con-cludes with a discussion of the implications of these results and work that can build upon them.