Loop path reduction by state pruning

Jianxiong Gao, Steven S. Lumetta

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Path explosion has been a problem for symbolic execution for a long time. The key to avoid path explosion is to limit the number of paths generated within loops while maintaining high code coverage. Full symbolic execution creates paths for every possible execution path. Frequently, paths within loops do not contribute to code coverage. Branches within loops may generate new states at every iteration. The path explosion problem created by loops often stops symbolic execution to reach deeper parts of the code. In this paper, we propose a new path exploration method that reduces the number of states needed to achieve high coverage. Our algorithm limits the number of new states created by first prioritizing states, and then pruning the states that do not contribute to code coverage. Our algorithm does not require loop invariant inference/loop summarization, nor does it bound the number of iterations of loop exploration. The proposed algorithm can thus handle a broader set of loops than previous approaches. In fact, our algorithm is orthogonal to loop summarization techniques and search-guide heuristics, so it complements the current methods. We have implemented our algorithm using KLEE and tested with 235 student-generated versions of a classroom assignment. Our results show that our algorithm helps to achieve the same coverage with speedup of 11.8× for 117 out of the 235 programs, while adding 15% max observed and 2% average overhead over the 50% of programs not benefiting from the technique. The maximum speedup for a single program is 52.3×.

Original languageEnglish (US)
Title of host publicationASE 2018 - Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering
EditorsChristian Kastner, Marianne Huchard, Gordon Fraser
PublisherAssociation for Computing Machinery, Inc
Pages838-843
Number of pages6
ISBN (Electronic)9781450359375
DOIs
StatePublished - Sep 3 2018
Event33rd IEEE/ACM International Conference on Automated Software Engineering, ASE 2018 - Montpellier, France
Duration: Sep 3 2018Sep 7 2018

Publication series

NameASE 2018 - Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering

Other

Other33rd IEEE/ACM International Conference on Automated Software Engineering, ASE 2018
CountryFrance
CityMontpellier
Period9/3/189/7/18

Keywords

  • Loop analysis
  • Symbolic execution

ASJC Scopus subject areas

  • Computational Theory and Mathematics
  • Human-Computer Interaction
  • Software

Fingerprint Dive into the research topics of 'Loop path reduction by state pruning'. Together they form a unique fingerprint.

Cite this