Computing summaries of string loops in C for better testing and refactoring
File(s)
Accepted version
Author(s)
Kapus, Timotej
Ish-Shalom, Oren
Itzhaky, Shachar
Rinetzky, Noam
Cadar, Cristian
Type
Conference Paper
Abstract
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.
Date Issued
2019-06
Date Acceptance
2019-04-03
Citation
2019, pp.874-888
Publisher
ACM
Start Page
874
End Page
888
Copyright Statement
© 2019 Copyright held by the owner/author(s). Publication rights licensed
to ACM.
to ACM.
Sponsor
Engineering & Physical Science Research Council (EPSRC)
Identifier
https://dl.acm.org/doi/10.1145/3314221.3314610
Grant Number
EP/N007166/1
Source
ACM SIGPLAN Conference on Programming Language Design and Implementation
Publication Status
Published
Start Date
2019-06-22
Finish Date
2019-06-26
Coverage Spatial
Phoenix, Arizona, USA
Date Publish Online
2019-06