Document Open Access Logo

Learning to Accelerate Symbolic Execution via Code Transformation

Authors Junjie Chen, Wenxiang Hu, Lingming Zhang, Dan Hao, Sarfraz Khurshid, Lu Zhang

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2018.6.pdf
  • Filesize: 0.88 MB
  • 27 pages

Document Identifiers

Author Details

Junjie Chen
  • Key Laboratory of High Confidence Software Technologies (Peking University), MoE, Institute of Software, EECS, Peking University, Beijing, 100871, China
Wenxiang Hu
  • Key Laboratory of High Confidence Software Technologies (Peking University), MoE, Institute of Software, EECS, Peking University, Beijing, 100871, China
Lingming Zhang
  • Department of Computer Science, University of Texas at Dallas, 75080, USA
Dan Hao
  • Key Laboratory of High Confidence Software Technologies (Peking University), MoE, Institute of Software, EECS, Peking University, Beijing, 100871, China
Sarfraz Khurshid
  • Department of Electrical and Computer Engineering, University of Texas at Austin, 78712, USA
Lu Zhang
  • Key Laboratory of High Confidence Software Technologies (Peking University), MoE, Institute of Software, EECS, Peking University, Beijing, 100871, China

Funding

This work is partially supported by the National Key Research and Development Program of China (Grant No. 2017YFB1001803), and NSFC 61672047, 61529201, 61522201, 61861130363. This work is also partially supported by NSF Grant No. CCF-1566589, UT Dallas start-up fund, Google, Huawei, and Samsung. This work is also partially supported by NSF Grant No. CCF-1704790.
  • Hao, Dan: corresponding author.

Cite AsGet BibTex

Junjie Chen, Wenxiang Hu, Lingming Zhang, Dan Hao, Sarfraz Khurshid, and Lu Zhang. Learning to Accelerate Symbolic Execution via Code Transformation. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 6:1-6:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.ECOOP.2018.6

Abstract

Symbolic execution is an effective but expensive technique for automated test generation. Over the years, a large number of refined symbolic execution techniques have been proposed to improve its efficiency. However, the symbolic execution efficiency problem remains, and largely limits the application of symbolic execution in practice. Orthogonal to refined symbolic execution, in this paper we propose to accelerate symbolic execution through semantic-preserving code transformation on the target programs. During the initial stage of this direction, we adopt a particular code transformation, compiler optimization, which is initially proposed to accelerate program concrete execution by transforming the source program into another semantic-preserving target program with increased efficiency (e.g., faster or smaller). However, compiler optimizations are mostly designed to accelerate program concrete execution rather than symbolic execution. Recent work also reported that unified settings on compiler optimizations that can accelerate symbolic execution for any program do not exist at all. Therefore, in this work we propose a machine-learning based approach to tuning compiler optimizations to accelerate symbolic execution, whose results may also aid further design of specific code transformations for symbolic execution. In particular, the proposed approach LEO separates source-code functions and libraries through our program-splitter, and predicts individual compiler optimization (i.e., whether a type of code transformation is chosen) separately through analyzing the performance of existing symbolic execution. Finally, LEO applies symbolic execution on the code transformed by compiler optimization (through our local-optimizer). We conduct an empirical study on GNU Coreutils programs using the KLEE symbolic execution engine. The results show that LEO significantly accelerates symbolic execution, outperforming the default KLEE configurations (i.e., turning on/off all compiler optimizations) in various settings, e.g., with the default training/testing time, LEO achieves the highest line coverage in 50/68 programs, and its average improvement rate on all programs is 46.48%/88.92% in terms of line coverage compared with turning on/off all compiler optimizations.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Software testing and debugging
Keywords
  • Symbolic Execution
  • Code Transformation
  • Machine Learning

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. F. Agakov, E. Bonilla, J. Cavazos, B. Franke, G. Fursin, M. F. P. O'Boyle, J. Thomson, M. Toussaint, and C. K. I. Williams. Using machine learning to focus iterative optimization. In CGO, pages 295-305, 2006. Google Scholar
  2. Alfred V Aho, Ravi Sethi, and Jeffrey D Ullman. Compilers, Principles, Techniques. Pearson Education, Inc., 1986. Google Scholar
  3. Aws Albarghouthi, Arie Gurfinkel, Ou Wei, and Marsha Chechik. Abstract analysis of symbolic executions. In CAV, pages 495-510, 2010. Google Scholar
  4. Saswat Anand, Alessandro Orso, and Mary Jean Harrold. Type-dependence analysis and program transformation for symbolic execution. In TACAS, pages 117-133, 2007. Google Scholar
  5. J. H. Andrews, L. C. Briand, and Y. Labiche. Is mutation an appropriate tool for testing experiments? In ICSE, pages 402-411, 2005. Google Scholar
  6. Tien-Duy B Le, David Lo, Claire Le Goues, and Lars Grunske. A learning-to-rank based fault localization approach using likely invariants. In ISSTA, pages 177-188, 2016. Google Scholar
  7. André Baresel, David Binkley, Mark Harman, and Bogdan Korel. Evolutionary testing in the presence of loop-assigned flags: A testability transformation approach. In ISSTA, pages 108-118, 2004. Google Scholar
  8. David W. Binkley, Mark Harman, and Kiran Lakhotia. Flagremover: A testability transformation for transforming loop-assigned flags. TOSEM, 20(3):12:1-12:33, 2011. Google Scholar
  9. François Bodin, Toru Kisuki, Peter Knijnenburg, Mike O'Boyle, and Erven Rohou. Iterative compilation in a non-linear optimisation space. In PFDC, 1998. Google Scholar
  10. Pietro Braione, Giovanni Denaro, and Mauro Pezzè. Enhancing symbolic execution with built-in term rewriting and constrained lazy initialization. In FSE, pages 411-421, 2013. Google Scholar
  11. Pietro Braione, Giovanni Denaro, and Mauro Pezzè. Symbolic execution of programs with heap inputs. In FSE, pages 602-613, 2015. Google Scholar
  12. Leo Breiman. Random forests. Machine learning, 45(1):5-32, 2001. Google Scholar
  13. William R Bush, Jonathan D Pincus, and David J Sielaff. A static analyzer for finding dynamic programming errors. SPE, 30(7):775-802, 2000. Google Scholar
  14. Cristian Cadar. Targeted program transformations for symbolic execution. In FSE, pages 906-909, 2015. Google Scholar
  15. Cristian Cadar, Daniel Dunbar, and Dawson Engler. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In OSDI, pages 209-224, 2008. Google Scholar
  16. Cristian Cadar, Vijay Ganesh, Peter M. Pawlowski, David L. Dill, and Dawson R. Engler. Exe: Automatically generating inputs of death. TISSEC, 12(2):10, 2008. Google Scholar
  17. Cristian Cadar, Patrice Godefroid, Sarfraz Khurshid, Corina S Păsăreanu, Koushik Sen, Nikolai Tillmann, and Willem Visser. Symbolic execution for software testing in practice: preliminary assessment. In ICSE, pages 1066-1071, 2011. Google Scholar
  18. Cristian Cadar and Koushik Sen. Symbolic execution for software testing: three decades later. CACM, 56(2):82-90, 2013. Google Scholar
  19. John Cavazos, Grigori Fursin, Felix Agakov, Edwin Bonilla, Michael F. P. O'Boyle, and Olivier Temam. Rapidly selecting good compiler optimizations using performance counters. In CGO, pages 185-197, 2007. Google Scholar
  20. Gavin C Cawley and Nicola LC Talbot. Efficient leave-one-out cross-validation of kernel fisher discriminant classifiers. Pattern Recognition, 36(11):2585-2592, 2003. Google Scholar
  21. Nitesh V Chawla. Data mining for imbalanced datasets: An overview. In Data Min. Knowl. Discov., pages 853-867. Springer, 2005. Google Scholar
  22. Nitesh V. Chawla, Kevin W. Bowyer, Lawrence O. Hall, and W. Philip Kegelmeyer. Smote: synthetic minority over-sampling technique. JAIR, pages 321-357, 2002. Google Scholar
  23. Nitesh V. Chawla, Nathalie Japkowicz, and Aleksander Kotcz. Editorial: Special issue on learning from imbalanced data sets. SIGKDD Explor, 6(1):1-6, 2004. Google Scholar
  24. Junjie Chen, Yanwei Bai, Dan Hao, Yingfei Xiong, Hongyu Zhang, and Bing Xie. Learning to prioritize test programs for compiler testing. In ICSE, pages 700-711, 2017. Google Scholar
  25. Junjie Chen, Yanwei Bai, Dan Hao, Lingming Zhang, Lu Zhang, and Bing Xie. How do assertions impact coverage-based test-suite reduction? In ICST, pages 418-423, 2017. Google Scholar
  26. Junjie Chen, Yanwei Bai, Dan Hao, Lingming Zhang, Lu Zhang, Bing Xie, and Hong Mei. Supporting oracle construction via static analysis. In ASE, pages 178-189, 2016. Google Scholar
  27. Junjie Chen, Wenxiang Hu, Dan Hao, Yingfei Xiong, Hongyu Zhang, Lu Zhang, and Bing Xie. An empirical comparison of compiler testing techniques. In ICSE, pages 180-190, 2016. Google Scholar
  28. Maria Christakis, Peter Müller, and Valentin Wüstholz. Guiding dynamic symbolic execution toward unverified program executions. In ICSE, pages 144-155, 2016. Google Scholar
  29. Lori A. Clarke. A system to generate test data and symbolically execute programs. TSE, SE-2(3):215-222, 1976. URL: http://dx.doi.org/10.1109/TSE.1976.233817.
  30. Hayes Converse, Oswaldo Olivo, and Sarfraz Khurshid. Non-semantics-preserving transformations for high-coverage test generation using symbolic execution. In ICST, pages 241-252, 2017. Google Scholar
  31. Hayes Elliott Converse, Oswaldo Olivo, and Sarfraz Khurshid. Non-semantics-preserving transformations for higher-coverage test generation using symbolic execution. PhD thesis, The University of Texas at Austin, 2017. Google Scholar
  32. Keith D Cooper, Alexander Grosul, Timothy J Harvey, Steve Reeves, Devika Subramanian, Linda Torczon, and Todd Waterman. Exploring the structure of the space of compilation sequences using randomized search algorithms. J Supercomput, 36(2):135-151, 2006. Google Scholar
  33. Shiyu Dong, Oswaldo Olivo, Lingming Zhang, and Sarfraz Khurshid. Studying the influence of standard compiler optimizations on symbolic execution. In ISSRE, pages 205-215, 2015. Google Scholar
  34. Ikpeme Erete and Alessandro Orso. Optimizing constraint solving to better support symbolic execution. In ICSTW, pages 310-315, 2011. Google Scholar
  35. Antonio Filieri, Corina S. Păsăreanu, Willem Visser, and Jaco Geldenhuys. Statistical symbolic execution with informed sampling. In FSE, pages 437-448, 2014. Google Scholar
  36. Yoav Freund and Llew Mason. The alternating decision tree learning algorithm. In ICML, pages 124-133, 1999. Google Scholar
  37. Jerome Friedman, Trevor Hastie, Robert Tibshirani, et al. Additive logistic regression: a statistical view of boosting (with discussion and a rejoinder by the authors). Ann. Stat., 28(2):337-407, 2000. Google Scholar
  38. Grigori Fursin, Yuriy Kashnikov, Abdul Wahid Memon, Zbigniew Chamski, Olivier Temam, Mircea Namolaru, Elad Yom-Tov, Bilha Mendelson, Ayal Zaks, Eric Courtois, Francois Bodin, Phil Barnard, Elton Ashton, Edwin Bonilla, John Thomson, Christopher K. I. Williams, and Michael O'Boyle. Milepost gcc: Machine learning enabled self-tuning compiler. IJPP, 39(3):296-327, 2011. Google Scholar
  39. Jaco Geldenhuys, Matthew B. Dwyer, and Willem Visser. Probabilistic symbolic execution. In ISSTA, pages 166-176, 2012. Google Scholar
  40. Alexander Genkin, David D Lewis, and David Madigan. Large-scale bayesian logistic regression for text categorization. Technometrics, 49(3):291-304, 2007. Google Scholar
  41. Patrice Godefroid. Compositional dynamic test generation. In POPL, pages 47-54, 2007. Google Scholar
  42. Patrice Godefroid, Nils Klarlund, and Koushik Sen. DART: Directed automated random testing. In PLDI, pages 213-223, 2005. Google Scholar
  43. Patrice Godefroid, Shuvendu K. Lahiri, and Cindy Rubio-González. Statically validating must summaries for incremental compositional dynamic test generation. In Proceedings of the 18th International Conference on Static Analysis, SAS'11, pages 112-128, Berlin, Heidelberg, 2011. Springer-Verlag. URL: http://dl.acm.org/citation.cfm?id=2041552.2041564.
  44. Patrice Godefroid, Aditya V. Nori, Sriram K. Rajamani, and Sai Deep Tetali. Compositional may-must program analysis: Unleashing the power of alternation. In POPL, pages 43-56, 2010. Google Scholar
  45. Shengjian Guo, Markus Kusano, and Chao Wang. Conc-ise: Incremental symbolic execution of concurrent software. In ASE, pages 531-542, 2016. Google Scholar
  46. Mark Harman, André Baresel, David Binkley, Robert Hierons, Lin Hu, Bogdan Korel, Phil McMinn, and Marc Roper. Testability transformation-program transformation to improve testability. In Formal methods and testing, pages 320-344. Springer, 2008. Google Scholar
  47. Kenneth Hoste and Lieven Eeckhout. Cole: Compiler optimization level exploration. In CGO, pages 165-174, 2008. Google Scholar
  48. Y Kumar Jain and Santosh Kumar Bhandare. Min max normalization based data perturbation method for privacy protection. IJRCCT, 2(8):45-50, 2011. Google Scholar
  49. Konrad Jamrozik, Gordon Fraser, Nikolai Tillmann, and Jonathan De Halleux. Augmented dynamic symbolic execution. In ASE, pages 254-257, 2012. Google Scholar
  50. Jinseong Jeon, Xiaokang Qiu, Jonathan Fetter-Degges, Jeffrey S. Foster, and Armando Solar-Lezama. Synthesizing framework models for symbolic execution. In ICSE, pages 156-167, 2016. Google Scholar
  51. René Just, Darioush Jalali, Laura Inozemtseva, Michael D Ernst, Reid Holmes, and Gordon Fraser. Are mutants a valid substitute for real faults in software testing? In FSE, pages 654-665, 2014. Google Scholar
  52. James C King. Symbolic execution and program testing. CACM, 19(7):385-394, 1976. Google Scholar
  53. Bogdan Korel, Mark Harman, S. Chung, P. Apirukvorapinit, R. Gupta, and Q. Zhang. Data dependence based testability transformation in automated test generation. In ISSRE, pages 245-254, 2005. Google Scholar
  54. Tomasz Kuchta, Cristian Cadar, Miguel Castro, and Manuel Costa. Docovery: Toward generic automatic document recovery. In ASE, pages 563-574, 2014. Google Scholar
  55. Chris Lattner and Vikram Adve. Llvm: A compilation framework for lifelong program analysis &transformation. In CGO, pages 75-86, 2004. Google Scholar
  56. Saskia Le Cessie and Johannes C Van Houwelingen. Ridge estimators in logistic regression. Applied statistics, pages 191-201, 1992. Google Scholar
  57. You Li, Zhendong Su, Linzhang Wang, and Xuandong Li. Steering symbolic execution to less traveled paths. In OOPSLA, pages 19-32, 2013. Google Scholar
  58. Daniel Liew, Cristian Cadar, and Alastair F. Donaldson. Symbooglix: A symbolic execution engine for boogie programs. In ICST, 2016. Google Scholar
  59. Kasper Luckow, Corina S. Păsăreanu, Matthew B. Dwyer, Antonio Filieri, and Willem Visser. Exact and approximate probabilistic symbolic execution for nondeterministic programs. In ASE, pages 575-586, 2014. Google Scholar
  60. P. D. Marinescu and Cristian Cadar. KATCH: High-coverage testing of software patches. In FSE, pages 235-245, 2013. Google Scholar
  61. Paul Dan Marinescu and Cristian Cadar. High-coverage symbolic patch testing. In SPIN, pages 7-21, 2012. Google Scholar
  62. Paul Dan Marinescu and Cristian Cadar. Make test-zesti: A symbolic execution solution for improving regression testing. In ICSE, pages 716-726, 2012. Google Scholar
  63. Frank J Massey Jr. The kolmogorov-smirnov test for goodness of fit. JASA, 46(253):68-78, 1951. Google Scholar
  64. Zhelong Pan and Rudolf Eigenmann. Fast and effective orchestration of compiler optimizations for automatic performance tuning. In CGO, pages 319-332, 2006. Google Scholar
  65. Corina S Păsăreanu and Neha Rungta. Symbolic pathfinder: symbolic execution of java bytecode. In ASE, pages 179-180, 2010. Google Scholar
  66. David M Perry, Andrea Mattavelli, Xiangyu Zhang, and Cristian Cadar. Accelerating array constraints in symbolic execution. In ISSTA, pages 68-78, 2017. Google Scholar
  67. Suzette Person, Matthew B. Dwyer, Sebastian Elbaum, and Corina S. Pǎsǎreanu. Differential symbolic execution. In FSE, pages 226-237, 2008. Google Scholar
  68. Suzette Person, Guowei Yang, Neha Rungta, and Sarfraz Khurshid. Directed incremental symbolic execution. In PLDI, pages 504-515, 2011. Google Scholar
  69. John Platt. Sequential minimal optimization: A fast algorithm for training support vector machines. Technical Report MSR-TR-98-14, Microsoft Research, April 1998. Google Scholar
  70. Rui Qiu, Sarfraz Khurshid, Corina S Păsăreanu, Junye Wen, and Guowei Yang. Using test ranges to improve symbolic execution. In NFM, pages 416-434. Springer, 2018. Google Scholar
  71. Rui Qiu, Corina S Păsăreanu, and Sarfraz Khurshid. Certified symbolic execution. In ATVA, pages 495-511. Springer, 2016. Google Scholar
  72. Rui Qiu, Guowei Yang, Corina S. Păsăreanu, and Sarfraz Khurshid. Compositional symbolic execution with memoized replay. In ICSE, pages 632-642, 2015. Google Scholar
  73. Eric F. Rizzi, Mathew B. Dwyer, and Sebastian Elbaum. Safely reducing the cost of unit level symbolic execution through read/write analysis. SEN, 39(1):1-5, 2014. Google Scholar
  74. Koushik Sen, Darko Marinov, and Gul Agha. CUTE: A concolic unit testing engine for C. In FSE, pages 263-272, 2005. Google Scholar
  75. Koushik Sen, George Necula, Liang Gong, and Wontae Choi. Multise: Multi-path symbolic execution using value summaries. In FSE, pages 842-853, 2015. Google Scholar
  76. Junaid Haroon Siddiqui and Sarfraz Khurshid. ParSym: Parallel symbolic execution. In ICSTE, pages V1-405-V1-409, 2010. Google Scholar
  77. Junaid Haroon Siddiqui and Sarfraz Khurshid. Scaling symbolic execution using ranged analysis. In OOPSLA, volume 47, pages 523-536, 2012. Google Scholar
  78. Matt Staats and Corina Pǎsǎreanu. Parallel symbolic execution for structural test generation. In ISSTA, pages 183-194, 2010. Google Scholar
  79. Kunal Taneja, Tao Xie, Nikolai Tillmann, and Jonathan de Halleux. express: guided path exploration for efficient regression test generation. In ISSTA, pages 1-11, 2011. Google Scholar
  80. Hao Tang, Xiaoyin Wang, Lingming Zhang, Bing Xie, Lu Zhang, and Hong Mei. Summary-based context-sensitive data-dependence analysis in presence of callbacks. In POPL, volume 50, pages 83-95, 2015. Google Scholar
  81. Nikolai Tillmann and Jonathan De Halleux. Pex-white box test generation for .net. In TAP, pages 134-153. Springer, 2008. Google Scholar
  82. Lisa Torrey and Jude Shavlik. Transfer learning. Handbook of Research on Machine Learning Applications and Trends: Algorithms, Methods, and Techniques, 1:242, 2009. Google Scholar
  83. Willem Visser, Jaco Geldenhuys, and Matthew B. Dwyer. Green: Reducing, reusing and recycling constraints in program analysis. In FSE, pages 58:1-58:11, 2012. Google Scholar
  84. Jonas Wagner, Volodymyr Kuznetsov, and George Candea. -overify: Optimizing programs for fast verification. In HotOS XIV. EPFL-CONF-186012, 2013. Google Scholar
  85. Tao Wang, Abhik Roychoudhury, Roland HC Yap, and Shishir C Choudhary. Symbolic execution of behavioral requirements. In PADL, pages 178-192. Springer, 2004. Google Scholar
  86. Xiaoyin Wang, Lingming Zhang, and Philip Tanofsky. Experience report: How is dynamic symbolic execution different from manual testing? a study on klee. In ISSTA, pages 199-210, 2015. Google Scholar
  87. Edmund Wong, Lei Zhang, Song Wang, Taiyue Liu, and Lin Tan. Dase: Document-assisted symbolic execution for improving automated software testing. In ICSE, pages 620-631, 2015. Google Scholar
  88. Guowei Yang, Corina S Păsăreanu, and Sarfraz Khurshid. Memoized symbolic execution. In ISSTA, pages 144-154, 2012. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact