Type and interval aware array constraint solving for symbolic execution

Array constraints are prevalent in analyzing a program with symbolic execution. Solving array constraints is challenging due to the complexity of the precise encoding for arrays. In this work, we propose to synergize symbolic execution and array constraint solving. Our method addresses the difficult...

Full description

Saved in:
Bibliographic Details
Main Authors: SHUAI, Ziqi, CHEN, Zhenbang, ZHANG, Yufeng, SUN, Jun, WANG, Ji
Format: text
Language:English
Published: Institutional Knowledge at Singapore Management University 2021
Subjects:
Online Access:https://ink.library.smu.edu.sg/sis_research/6236
https://ink.library.smu.edu.sg/context/sis_research/article/7239/viewcontent/type_and_interval_aware.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-7239
record_format dspace
spelling sg-smu-ink.sis_research-72392021-11-05T05:16:27Z Type and interval aware array constraint solving for symbolic execution SHUAI, Ziqi CHEN, Zhenbang ZHANG, Yufeng SUN, Jun WANG, Ji Array constraints are prevalent in analyzing a program with symbolic execution. Solving array constraints is challenging due to the complexity of the precise encoding for arrays. In this work, we propose to synergize symbolic execution and array constraint solving. Our method addresses the difficulties in solving array constraints with novel ideas. First, we propose a lightweight method for pre-checking the unsatisfiability of array constraints based on integer linear programming. Second, observing that encoding arrays at the byte-level introduces many redundant axioms that reduce the effectiveness of constraint solving, we propose type and interval aware axiom generation. Note that the type information of array variables is inferred by symbolic execution, whereas interval information is calculated through the above pre-checking step. We have implemented our methods based on KLEE and its underlying constraint solver STP and conducted large-scale experiments on 75 real-world programs. The experimental results show that our method effectively improves the efficiency of symbolic execution. Our method solves 182.56% more constraints and explores 277.56% more paths on average under the same time threshold. 2021-08-01T07:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/6236 info:doi/10.1145/3460319.3464826 https://ink.library.smu.edu.sg/context/sis_research/article/7239/viewcontent/type_and_interval_aware.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 Software and its engineering Software testing and debugging Software Engineering
institution Singapore Management University
building SMU Libraries
continent Asia
country Singapore
Singapore
content_provider SMU Libraries
collection InK@SMU
language English
topic Software and its engineering
Software testing and debugging
Software Engineering
spellingShingle Software and its engineering
Software testing and debugging
Software Engineering
SHUAI, Ziqi
CHEN, Zhenbang
ZHANG, Yufeng
SUN, Jun
WANG, Ji
Type and interval aware array constraint solving for symbolic execution
description Array constraints are prevalent in analyzing a program with symbolic execution. Solving array constraints is challenging due to the complexity of the precise encoding for arrays. In this work, we propose to synergize symbolic execution and array constraint solving. Our method addresses the difficulties in solving array constraints with novel ideas. First, we propose a lightweight method for pre-checking the unsatisfiability of array constraints based on integer linear programming. Second, observing that encoding arrays at the byte-level introduces many redundant axioms that reduce the effectiveness of constraint solving, we propose type and interval aware axiom generation. Note that the type information of array variables is inferred by symbolic execution, whereas interval information is calculated through the above pre-checking step. We have implemented our methods based on KLEE and its underlying constraint solver STP and conducted large-scale experiments on 75 real-world programs. The experimental results show that our method effectively improves the efficiency of symbolic execution. Our method solves 182.56% more constraints and explores 277.56% more paths on average under the same time threshold.
format text
author SHUAI, Ziqi
CHEN, Zhenbang
ZHANG, Yufeng
SUN, Jun
WANG, Ji
author_facet SHUAI, Ziqi
CHEN, Zhenbang
ZHANG, Yufeng
SUN, Jun
WANG, Ji
author_sort SHUAI, Ziqi
title Type and interval aware array constraint solving for symbolic execution
title_short Type and interval aware array constraint solving for symbolic execution
title_full Type and interval aware array constraint solving for symbolic execution
title_fullStr Type and interval aware array constraint solving for symbolic execution
title_full_unstemmed Type and interval aware array constraint solving for symbolic execution
title_sort type and interval aware array constraint solving for symbolic execution
publisher Institutional Knowledge at Singapore Management University
publishDate 2021
url https://ink.library.smu.edu.sg/sis_research/6236
https://ink.library.smu.edu.sg/context/sis_research/article/7239/viewcontent/type_and_interval_aware.pdf
_version_ 1770575897808601088