Solving Program Sketches with Large Integer Values
Solving Program Sketches with Large Integer Values
复制标题
DOI：
10.1145/3532849
复制
发表时间：
2022-01-01
影响因子：
1.3
通讯作者：
D'Antoni，Loris
中科院分区：
文献类型：
--
作者：
Hu，Qinheping;Singh，Rishabh;D'Antoni，Loris
程序草图是一种程序合成范式，程序员提供带有漏洞和断言的部分程序。合成器的目标是自动找到孔的整数值，以便结果程序满足断言。最流行的草图绘制工具Sketch可以高效地解决复杂的程序草图，但使用整数编码，如果绘制的程序操纵大整数值，这种编码往往性能不佳。在本文中，我们提出了一种新的求解技术，允许Sketch在处理大整数值的同时保持其整数编码。我们的技术使用数论的一个结果，中国剩余定理，重写程序草图，只跟踪某些变量值关于几个质数的余数。我们证明了我们的变换是可靠的，并且结果程序的编码比现有的Sketchending编码要简洁得多。我们在处理大整数值的各种基准测试中评估了我们的技术。我们的技术对现有的SketchSolver都提供了加速，并可以解决现有SketchSolver无法处理的基准测试。
Program sketching is a program synthesis paradigm in which the programmer provides a partial program with holes and assertions. The goal of the synthesizer is to automatically find integer values for the holes so that the resulting program satisfies the assertions. The most popular sketching tool,Sketch, can efficiently solve complex program sketches but uses an integer encoding that often performs poorly if the sketched program manipulates large integer values. In this article, we propose a new solving technique that allowsSketchto handle large integer values while retaining its integer encoding. Our technique uses a result from number theory, the Chinese Remainder Theorem, to rewrite program sketches to only track the remainders of certain variable values with respect to several prime numbers. We prove that our transformation is sound and the encoding of the resulting programs are exponentially more succinct than existingSketchencodings. We evaluate our technique on a variety of benchmarks manipulating large integer values. Our technique provides speedups against both existingSketchsolvers and can solve benchmarks that existingSketchsolvers cannot handle.