为约减积域合成抽象转换器
Synthesizing Abstract Transformers for Reduced-Product Domains
AI总结：
本文针对约减积域中抽象转换器合成搜索空间爆炸和组件协作困难的问题，提出基于多 DSL 的合成算法，并在工具 Amurth2 中实现，在 SAFEstr 框架的两个积域上取得了优于手工转换器的精度。
摘要：
最近，我们展示了如何将程序合成技术应用于在用户提供的领域特定语言（DSL）L 中创建抽象转换器（即“L-转换器”）。然而，我们发现 Kalita 等人的算法在应用于约减积域时并不成功：需要同时为所有域合成转换器会使搜索空间急剧膨胀。由于约减积域是提高抽象解释精度的重要手段，本文提出了一种算法，用于为积域 A1 × A2 × … × An 合成约减 L-转换器 ⟨f1#R, f2#R, ..., fn#R⟩，并使用多个 DSL：L = ⟨L1, L2, ..., Ln⟩。约减积转换器的合成相当具有挑战性：首先，合成任务必须应对增大的“特征集”，因为每个组件转换器现在都可以访问积中所有组件域的抽象输入。其次，为了确保积转换器具有最大精度，合成任务需要安排各组件转换器相互协作。我们在工具 Amurth2 中实现了该算法，并使用它为 SAFEstr 框架（用于 JavaScript 程序分析）中可用的两个积域——SAFE 和 JSAI——合成抽象转换器。对于 SAFEstr 支持的六个操作中的四个，Amurth2 合成的抽象转换器比 SAFEstr 中手工编写的转换器更精确。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
