Synthesizing data structure refinements from integrity constraints
Synthesizing data structure refinements from integrity constraints
复制标题
从完整性约束综合数据结构改进
DOI：
10.1145/3453483.3454063
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Dillig, Isil
中科院分区：
文献类型：
--
作者：
Pailoor, Shankara;Wang, Yuepeng;Wang, Xinyu;Dillig, Isil
许多数据结构的实现使用多个相关字段来提高性能;然而，这些字段之间的不一致可能是严重程序错误的来源。为了解决这个问题，我们提出了一种新的技术，自动完善数据结构的完整性约束。特别地，考虑一个数据结构D，它有字段F和方法M，以及一组新的辅助字段F ′，应该添加到D中。给定此输入和与FandF ′相关的完整性约束Φ，我们的方法自动生成满足所提供的完整性约束的D的精化。我们的方法是基于amodularinstantiation的CEGIS范式，并使用一种新的归纳合成器，增强自上而下的搜索与三个关键的想法。首先，它计算部分程序的必要的预条件，以显着修剪其搜索空间。其次，它通过利用计算的前提条件来增强语法，并有希望产生新的结果。第三，通过对完整性检查函数和原始代码库的静态分析，得到了一个概率上下文无关文法，用于指导自顶向下的搜索。我们评估了我们的方法对25个数据结构从流行的Java项目，并表明我们的方法可以成功地完善其中的23个。我们还将我们的方法与两种最先进的合成工具进行了比较，并进行了消融研究，以证明我们的设计选择。我们的评估表明，（1）我们的方法在改进许多数据结构实现方面是成功的，（2）它在综合方面推进了最先进的技术，（3）我们提出的想法对于使这项技术实用化至关重要。
Implementations of many data structures use several correlated fields to improve their performance; however, inconsistencies between these fields can be a source of serious program errors. To address this problem, we propose a new technique for automatically refining data structures from integrity constraints. In particular, consider a data structureDwith fieldsFand methodsM, as well as a new set of auxiliary fieldsF′ that should be added toD. Given this input and an integrity constraint Φ relatingFandF′, our method automatically generates a refinement ofDthat satisfies the provided integrity constraint. Our method is based on amodularinstantiation of the CEGIS paradigm and uses a novel inductive synthesizer that augments top-down search with three key ideas. First, it computesnecessary preconditionsof partial programs to dramatically prune its search space. Second, it augments the grammar with promising new productions by leveraging the computed preconditions. Third, it guides top-down search using aprobabilisticcontext-free grammar obtained by statically analyzing the integrity checking function and the original code base. We evaluated our method on 25 data structures from popular Java projects and show that our method can successfully refine 23 of them. We also compare our method against two state-of-the-art synthesis tools and perform an ablation study to justify our design choices. Our evaluation shows that (1) our method is successful at refining many data structure implementations in the wild, (2) it advances the state-of-the-art in synthesis, and (3) our proposed ideas are crucial for making this technique practical.
登录
查看更多内容
DOI：
--
发表时间：
2018-09
期刊：
--
影响因子：
--
作者：
X. Si;Yuan Yang;H. Dai;M. Naik;Le Song
通讯作者：
X. Si;Yuan Yang;H. Dai;M. Naik;Le Song
DOI：
10.1145/1706299.1706325
发表时间：
2010-01
期刊：
--
影响因子：
--
作者：
Philippe Suter;Mirco Dotta;Viktor Kunčak
通讯作者：
Philippe Suter;Mirco Dotta;Viktor Kunčak
Hob：验证数据结构一致性的工具
DOI：
10.1007/978-3-540-31985-6_16
发表时间：
2005
期刊：
ACM Trans. Program. Lang. Syst.
影响因子：
--
作者：
Patrick Lam;Viktor Kunčak;M. Rinard
通讯作者：
M. Rinard
影响因子：
--
作者：
Yu Feng;R. Martins;O. Bastani;Işıl Dillig
通讯作者：
Yu Feng;R. Martins;O. Bastani;Işıl Dillig
DOI：
--
发表时间：
2017
期刊：
ArXiv
影响因子：
--
作者：
Manos Koukoutos;Mukund Raghothaman;Etienne Kneuss;Viktor Kunčak
通讯作者：
Viktor Kunčak