Computing summaries of string loops in C for better testing and refactoring

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