Synthesis of loop-free programs
Synthesis of loop-free programs
复制标题
DOI：
10.1145/1993498.1993506
复制
发表时间：
2011-06
期刊：
影响因子：
--
通讯作者：
Sumit Gulwani;Susmit Jha;A. Tiwari;R. Venkatesan
中科院分区：
文献类型：
--
作者：
Sumit Gulwani;Susmit Jha;A. Tiwari;R. Venkatesan
我们考虑使用给定库中的组件来合成实现所需功能的无循环程序的问题。所需功能和库组件的规范被提供为它们各自的输入和输出变量之间的逻辑关系。库组件最多只能使用一次，因此要求库包含所需组件的多个集合的合理过度近似。我们使用一种基于约束的方法来解决上述基于组件的合成问题，该方法首先生成一个合成约束，然后求解该约束。综合约束是一阶∃∀逻辑公式，其大小在组件数量上是二次的。我们提出了一种新的算法来解决这类约束。我们的算法基于反例指导的迭代综合范例，并使用现成的SMT求解器。我们给出的实验结果表明，我们的工具Brahma可以有效地综合高度非平凡的10-20行无循环位向量程序。这些程序代表了大约2010个程序的状态空间，超出了其他基于草图和超级优化的工具的范围。
We consider the problem of synthesizing loop-free programs that implement a desired functionality using components from a given library. Specifications of the desired functionality and the library components are provided as logical relations between their respective input and output variables. The library components can be used at most once, and hence the library is required to contain a reasonable overapproximation of the multiset of the components required. We solve the above component-based synthesis problem using a constraint-based approach that involves first generating a synthesis constraint, and then solving the constraint. The synthesis constraint is a first-order ∃∀ logic formula whose size is quadratic in the number of components. We present a novel algorithm for solving such constraints. Our algorithm is based on counterexample guided iterative synthesis paradigm and uses off-the-shelf SMT solvers. We present experimental results that show that our tool Brahma can efficiently synthesize highly nontrivial 10-20 line loop-free bitvector programs. These programs represent a state space of approximately 2010 programs, and are beyond the reach of the other tools based on sketching and superoptimization.