Context sensitive symbolic pointer analysis

One of the bottlenecks in the recent movement of hardware synthesis from behavioral C programs is the difficulty in reasoning about runtime pointer values at compile time. The pointer analysis problem has been investigated in the compiler community for two decades and has yielded efficient, polynomial time algorithms for context-insensitive (CI) analysis. However, at the accuracy level for which hardware synthesis is desired, namely context and flow sensitive analysis, the time and space complexity of the best algorithms reported grow exponentially with program size. In this paper, we propose a new analysis technology to combat the inefficiency encountered in traditional algorithms. The key idea is to implicitly encode the pointer-to relation in the Boolean domain by Bryant´s binary decision diagram, thereby capturing the procedure transfer function completely, compactly and canonically. With symbolic transfer functions, we can establish a common framework to perform both CI and context-sensitive (CS) pointer analysis efficiently. In addition, we propose a symbolic representation of the invocation graph, which can otherwise be exponentially large. In contrast to the classical frameworks, where CS point-to information of a procedure has to be obtained by the application of its transfer function exponentially many times, our method can obtain point-to information of all contexts in a single application. Our experimental evaluation on a wide range of C benchmarks indicates that our CS pointer analysis can be made almost as fast as its CI counterpart.