Taming the Hydra: Targeted Control-Flow Transformations for Dynamic Symbolic Execution
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2023
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866910079921422336 |
|---|---|
| author | Saumya, Charitha Hassan, Muhammad Gangaraju, Rohan Kulkarni, Milind Sundararajah, Kirshanthan |
| author_facet | Saumya, Charitha Hassan, Muhammad Gangaraju, Rohan Kulkarni, Milind Sundararajah, Kirshanthan |
| contents | Dynamic Symbolic Execution (DSE) suffers from the path explosion problem when the target program has many conditional branches. The classical approach for managing the path explosion problem is dynamic state merging. Dynamic state merging combines similar symbolic program states to avoid the exponential growth in the number of states during DSE. However, state merging still requires solver invocations at each program branch, even when both paths of the branch are feasible. Moreover, the best path search strategy for DSE may not create the best state merging opportunities. Some drawbacks of state merging can be mitigated by compile-time state merging (i.e., branch elimination by converting control-flow into dataflow). In this paper, we propose a non-semantics-preserving but failure-preserving compiler transformation for removing expensive symbolic branches in a program to improve the scalability of DSE. We have developed a framework for detecting spurious bugs that our transformation can insert. Finally, we show that our transformation can significantly improve the performance of DSE on various benchmark programs and help improve the performance of coverage and bug discovery of large real-world programs. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2308_01554 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Taming the Hydra: Targeted Control-Flow Transformations for Dynamic Symbolic Execution Saumya, Charitha Hassan, Muhammad Gangaraju, Rohan Kulkarni, Milind Sundararajah, Kirshanthan Software Engineering Programming Languages Dynamic Symbolic Execution (DSE) suffers from the path explosion problem when the target program has many conditional branches. The classical approach for managing the path explosion problem is dynamic state merging. Dynamic state merging combines similar symbolic program states to avoid the exponential growth in the number of states during DSE. However, state merging still requires solver invocations at each program branch, even when both paths of the branch are feasible. Moreover, the best path search strategy for DSE may not create the best state merging opportunities. Some drawbacks of state merging can be mitigated by compile-time state merging (i.e., branch elimination by converting control-flow into dataflow). In this paper, we propose a non-semantics-preserving but failure-preserving compiler transformation for removing expensive symbolic branches in a program to improve the scalability of DSE. We have developed a framework for detecting spurious bugs that our transformation can insert. Finally, we show that our transformation can significantly improve the performance of DSE on various benchmark programs and help improve the performance of coverage and bug discovery of large real-world programs. |
| title | Taming the Hydra: Targeted Control-Flow Transformations for Dynamic Symbolic Execution |
| topic | Software Engineering Programming Languages |
| url | https://arxiv.org/abs/2308.01554 |