Recently, we 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”). This algorithm does not scale when applied to reduced-product domains: synthesizing transformers for all of the component domains simultaneously blows up the search-space. Because reduced-product domains can significantly improve the precision of abstract interpretation, in this paper, 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 larger “feature set” as 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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Synthesizing Abstract Transformers for Reduced-Product Domains

  • Pankaj Kumar Kalita,
  • Thomas Reps,
  • Subhajit Roy

摘要

Recently, we 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”). This algorithm does not scale when applied to reduced-product domains: synthesizing transformers for all of the component domains simultaneously blows up the search-space. Because reduced-product domains can significantly improve the precision of abstract interpretation, in this paper, 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 larger “feature set” as 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.