Computing summaries of string loops in C for better testing and refactoring
Computing summaries of string loops in C for better testing and refactoring
复制标题
DOI：
10.1145/3314221.3314610
复制
发表时间：
2019-06
期刊：
影响因子：
--
通讯作者：
Timotej Kapus;Oren Ish-Shalom;Shachar Itzhaky;N. Rinetzky;Cristian Cadar
中科院分区：
文献类型：
--
作者：
Timotej Kapus;Oren Ish-Shalom;Shachar Itzhaky;N. Rinetzky;Cristian Cadar
分析和理解使用字符串的C程序很难：使用标准库功能来操纵字符串，并未执行，并且程序通常用于相同的目的。我们介绍了无内存循环的概念，该概念捕获了其中一些字符串循环，并提出了反例引导的合成方法，以使用C标准库函数来汇总无内存循环，该库具有测试，优化和重构的应用。我们证明我们的摘要对于任意输入字符串是正确的，并在我们从13个开源程序中收集的循环数据库中进行了评估。我们的方法可以在不到五分钟的每个循环时间内总结三分之二的无内存循环。然后，我们证明这些摘要可用于（1）改善符号执行（2）优化本机代码和（3）重构代码。
Analysing and comprehending C programs that use strings is hard: using standard library functions for manipulating strings is not enforced and programs often use complex loops for the same purpose. We introduce the notion of memoryless loops that capture some of these string loops and present a counterexample-guided synthesis approach to summarise memoryless loops using C standard library functions, which has applications to testing, optimisation and refactoring. We prove our summarisation is correct for arbitrary input strings and evaluate it on a database of loops we gathered from thirteen open-source programs. Our approach can summarise over two thirds of memoryless loops in less than five minutes of computation time per loop. We then show that these summaries can be used to (1) improve symbolic execution (2) optimise native code, and (3) refactor code.