Partial solution based constraint solving cache in symbolic execution
Constraint solving is one of the main challenges for symbolic execution. Caching is an effective mechanism to reduce the number of the solver invocations in symbolic execution and is adopted by many mainstream symbolic execution engines. However, caching can not perform well on all programs. How to...
Saved in:
Main Authors: | , , , , , , |
---|---|
Format: | text |
Language: | English |
Published: |
Institutional Knowledge at Singapore Management University
2024
|
Subjects: | |
Online Access: | https://ink.library.smu.edu.sg/sis_research/9179 https://ink.library.smu.edu.sg/context/sis_research/article/10184/viewcontent/3660817.pdf |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Institution: | Singapore Management University |
Language: | English |
id |
sg-smu-ink.sis_research-10184 |
---|---|
record_format |
dspace |
spelling |
sg-smu-ink.sis_research-101842024-08-13T05:27:55Z Partial solution based constraint solving cache in symbolic execution SHUAI, Ziqi CHEN, Zhenbang MA, Kelin LIU, Kunlin ZHANG, Yufeng SUN, Jun WANG, Ji Constraint solving is one of the main challenges for symbolic execution. Caching is an effective mechanism to reduce the number of the solver invocations in symbolic execution and is adopted by many mainstream symbolic execution engines. However, caching can not perform well on all programs. How to improve caching’s effectiveness is challenging in general. In this work, we propose a partial solution-based caching method for improving caching’s effectiveness. Our key idea is to utilize the partial solutions inside the constraint solving to generate more cache entries. A partial solution may satisfy other constraints of symbolic execution. Hence, our partial solution-based caching method naturally improves the rate of cache hits. We have implemented our method on two mainstream symbolic executors (KLEE and Symbolic PathFinder) and two SMT solvers (STP and Z3). The results of extensive experiments on real-world benchmarks demonstrate that our method effectively increases the number of the explored paths in symbolic execution. Our caching method achieves 1.07x to 2.3x speedups for exploring the same amount of paths on different benchmarks. 2024-07-01T07:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/9179 info:doi/10.1145/3660817 https://ink.library.smu.edu.sg/context/sis_research/article/10184/viewcontent/3660817.pdf http://creativecommons.org/licenses/by-nc-nd/4.0/ Research Collection School Of Computing and Information Systems eng Institutional Knowledge at Singapore Management University Symbolic Execution Constraint Solving Cache Software Engineering |
institution |
Singapore Management University |
building |
SMU Libraries |
continent |
Asia |
country |
Singapore Singapore |
content_provider |
SMU Libraries |
collection |
InK@SMU |
language |
English |
topic |
Symbolic Execution Constraint Solving Cache Software Engineering |
spellingShingle |
Symbolic Execution Constraint Solving Cache Software Engineering SHUAI, Ziqi CHEN, Zhenbang MA, Kelin LIU, Kunlin ZHANG, Yufeng SUN, Jun WANG, Ji Partial solution based constraint solving cache in symbolic execution |
description |
Constraint solving is one of the main challenges for symbolic execution. Caching is an effective mechanism to reduce the number of the solver invocations in symbolic execution and is adopted by many mainstream symbolic execution engines. However, caching can not perform well on all programs. How to improve caching’s effectiveness is challenging in general. In this work, we propose a partial solution-based caching method for improving caching’s effectiveness. Our key idea is to utilize the partial solutions inside the constraint solving to generate more cache entries. A partial solution may satisfy other constraints of symbolic execution. Hence, our partial solution-based caching method naturally improves the rate of cache hits. We have implemented our method on two mainstream symbolic executors (KLEE and Symbolic PathFinder) and two SMT solvers (STP and Z3). The results of extensive experiments on real-world benchmarks demonstrate that our method effectively increases the number of the explored paths in symbolic execution. Our caching method achieves 1.07x to 2.3x speedups for exploring the same amount of paths on different benchmarks. |
format |
text |
author |
SHUAI, Ziqi CHEN, Zhenbang MA, Kelin LIU, Kunlin ZHANG, Yufeng SUN, Jun WANG, Ji |
author_facet |
SHUAI, Ziqi CHEN, Zhenbang MA, Kelin LIU, Kunlin ZHANG, Yufeng SUN, Jun WANG, Ji |
author_sort |
SHUAI, Ziqi |
title |
Partial solution based constraint solving cache in symbolic execution |
title_short |
Partial solution based constraint solving cache in symbolic execution |
title_full |
Partial solution based constraint solving cache in symbolic execution |
title_fullStr |
Partial solution based constraint solving cache in symbolic execution |
title_full_unstemmed |
Partial solution based constraint solving cache in symbolic execution |
title_sort |
partial solution based constraint solving cache in symbolic execution |
publisher |
Institutional Knowledge at Singapore Management University |
publishDate |
2024 |
url |
https://ink.library.smu.edu.sg/sis_research/9179 https://ink.library.smu.edu.sg/context/sis_research/article/10184/viewcontent/3660817.pdf |
_version_ |
1814047783239286784 |