Synthesizing Abstract Transformers

This paper addresses the problem of creating abstract transformers automatically. The method we present provides the basis for creating a tool to automate the construction of program analyzers in a fashion similar to the way yacc automates the construction of parsers. Our method treats the problem as a program-synthesis problem. The user provides specifications of (i) the concrete semantics of a given operation O, (ii) the abstract domain A to be used by the analyzer, and (iii) the semantics of a domain-specific language L in which the abstract transformer is to be expressed. As output, our method creates an abstract transformer for O for abstract domain A, expressed in DSL L. We implemented our method, and used it to create a set of replacement abstract transformers for those used in an existing analyzer, and obtained essentially identical performance. However, when we compared the existing transformers with the generated transformers, we discovered that two of the existing transformers were unsound, which demonstrates the risk of using manually created transformers.