Synthesizing Abstract Transformers for Reduced-Product Domains

TL;DR

This work tackles the challenge of achieving high-precision static analysis by synthesizing reduced-product ${\mathcal{L}}$-transformers for product domains $A_1 \times \dots \times A_n$. It proposes a practical algorithm that synthesizes component transformers ${f}^{\sharp \textsf{R}}_i$ using a DSL tuple ${\mathcal{L}}=\langle {\mathcal{L}}_1, \dots, {\mathcal{L}}_n \rangle$, enabling inter-domain cooperation while avoiding exponential joint search. Implemented as Amurth2, the approach scales better than direct product synthesis and yields more precise transformers than the SAFEstr baselines on real JavaScript analyses, including two product domains (SAFE FOOL:LWJCR12 and JSAI DBLP:conf/sigsoft/KashyapDKWGSWH14). Empirical results show Amurth2 achieving higher precision for four of six concrete operations, illustrating practical impact for improving soundness and precision in static analysis pipelines.

Abstract

Recently, we showed how to apply program-synthesis techniques to create abstract transformers in a user-provided domain-specific language (DSL) L (i.e., ''L-transformers"). 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 paper, we propose an algorithm to synthesize reduced L-transformers $\langle f_1^{\sharp R}, f_2^{\sharp R},..., f_n^{\sharp R}\rangle$ for a product domain $A_1 \times A_2 \times \ldots \times A_n$ , using multiple DSLs: $\mathcal{L} = \langle \mathcal{L}_1 , \mathcal{L}_2, ... , \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 SAFEstr framework for JavaScript program analysis. For four of the six operations supported by SAFEstr, Amurth2 synthesizes more precise abstract transformers than the manually written ones available in SAFEstr.

Figures (2)

• Figure 1: Lattice for the odd-interval domain
• Figure 2: Illustrations of working of direct and reduced-product transformers