Automated Abstract Transformer Synthesis for Reduced Product Domains

Designing abstract transformers for program-analysis tools is a challenging task. In the past, bugs have been discovered in such transformers, showing the difficulty of designing such transformers manually, and providing motivation for automated techniques. Recently, Kalita et al. showed how to apply program-synthesis techniques to create abstract transformers in a user-provided domain-specific language (DSL) \({\mathcal{L}}\) (i.e., “ \({\mathcal{L}}\) -transformers”). Their technique creates provably sound and maximally precise \({\mathcal{L}}\) -transformers for an abstract domain \( A \) —i.e., given specifications of a concrete operation op , DSL \({\mathcal{L}}\) , and abstract domain \( A \) , it finds a best abstract \({\mathcal{L}}\) -transformer for op in \( A \) . However, we found that the algorithm of Kalita et al. does not succeed when applied to reduced-product domains: The need to synthesize transformers for all of the domains simultaneously blows up the search space. Because reduced-product domains are an important device for improving the precision of abstract interpretation, in this article, we propose an algorithm to synthesize reduced \({\mathcal{L}}\) -transformers \(\langle{f}^{\sharp\textsf{R}}_{1},{f}^{\sharp\textsf{R}}_{2},\dots,{f}^{\sharp \textsf{R}}_{n}\rangle\) for a product domain \(A_{1}\times A_{2}\times\dots\times A_{n}\) , using multiple DSLs: \({\mathcal{L}}\) \(=\langle{\mathcal{L}}_{1},{\mathcal{L}}_{2},\ldots,{\mathcal{L}}_{n}\rangle\) . Synthesis of reduced-product transformers is quite challenging: First, the synthesis task has to tackle an increased “feature set” because each component transformer now has access to the abstract inputs from all component domains in the product. Second, to ensure that the product transformer is maximally precise, the synthesis task needs to arrange for the component transformers to cooperate with each other. We implemented our algorithm in a tool, Amurth2 , and used it to synthesize abstract transformers for two product domains—SAFE and JSAI—available within the SAFE str framework for JavaScript program analysis. For four of the six operations supported by SAFE str , Amurth2 synthesizes more precise abstract transformers than the manually written ones available in SAFE str .