Assisting Program Analyses with Library Synopses∗

Understanding a program based on its source code is te-dious and error-prone. Unfortunately, such a task is often necessary due to lack of adequate documentation. To assist software engineers in this task, automated analysis tools are often used. Such tools analyze the program source, com-puting information, and present that information to the tool user in a useful way. To compute correct information, the entire program may need to be analyzed; however, most programs written today use libraries extensively, for which source code may not be available. Therefore, tools must somehow model the libraries to summarize their effects. However, such models are hard to construct by hand and are often tool-specific, limiting reuse. We present a general, automatable technique for gen-erating models of libraries given their source. The resulting models are themselves pieces of source code called syn-opses. Synopses are more accurate than hand-generated models and are reusable across tools. Furthermore, the use of synopses can increase precision of subsequent analyses since they allow functions to be expanded inline, thereby gaining one level of precision with respect to calling con-text. Finally, synopses can be extended to entire software layers, improving the efficiency of analysis tools