Computing summaries of string loops in C for better testing and refactoring
| Autor: | Oren Ish-Shalom, Noam Rinetzky, Timotej Kapus, Shachar Itzhaky, Cristian Cadar |
|---|---|
| Přispěvatelé: | Engineering & Physical Science Research Council (EPSRC) |
| Rok vydání: | 2019 |
| Předmět: |
Loop (graph theory)
Programming language Computer science Computation String (computer science) 020207 software engineering 02 engineering and technology computer.software_genre Symbolic execution Code refactoring 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing computer Library function Machine code C standard library |
| Zdroj: | PLDI ACM SIGPLAN Conference on Programming Language Design and Implementation |
| Popis: | Analysing and comprehending C programs that use stringsis hard: Using standard library functions for manipulatingstrings is not enforced and programs often use complex loopsfor the same purpose. We introduce the notion of memorylessloops that capture some of these string loops and presenta counterexample-guided inductive synthesis approach tosummarise memoryless string loops using C standard libraryfunctions, which has applications to testing, optimizationand refactoring.We prove our summarization is correct for arbitrary inputstrings and evaluate it on a database of loops we gatheredfrom a set of 13 open-source programs. Our approach cansummarize over two thirds of memoryless loops in less than5 minutes of computation time per loop. We then show thatthese summaries can be used to (1) enhance symbolic ex-ecution testing, where we observed median speedups of79x when employing a string constraint solver, (2) optimizenative code, where certain summarizations led to signifi-cant performance gains, and (3) refactor code, where wehad several patches accepted in the codebases of popularapplications such as patch and wget. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|