Automatic loop summarization via path dependency analysis

Analyzing loops is very important for various software engineering tasks such as bug detection, test case generation and program optimization. However, loops are very challenging structures for program analysis, especially when (nested) loops contain multiple paths that have complex interleaving rel...

Full description

Saved in:
Bibliographic Details
Main Authors: XIE, Xiaofei, CHEN, Bihuan, ZOU, Liang, LIU, Yang, LE, Wei, LI, Xiaohong
Format: text
Language:English
Published: Institutional Knowledge at Singapore Management University 2019
Subjects:
Online Access:https://ink.library.smu.edu.sg/sis_research/7100
https://ink.library.smu.edu.sg/context/sis_research/article/8103/viewcontent/336ed1cc9c1df91a9ae8b5a4977cc8d93e8f.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-8103
record_format dspace
spelling sg-smu-ink.sis_research-81032022-04-14T11:55:40Z Automatic loop summarization via path dependency analysis XIE, Xiaofei CHEN, Bihuan ZOU, Liang LIU, Yang LE, Wei LI, Xiaohong Analyzing loops is very important for various software engineering tasks such as bug detection, test case generation and program optimization. However, loops are very challenging structures for program analysis, especially when (nested) loops contain multiple paths that have complex interleaving relationships. In this paper, we propose the path dependency automaton (PDA) to capture the dependencies among the multiple paths in a loop. Based on the PDA, we first propose a loop classification to understand the complexity of loop summarization. Then, we propose a loop analysis framework, named Proteus, which takes a loop program and a set of variables of interest as inputs and summarizes path-sensitive loop effects (i.e., disjunctive loop summary) on the variables of interest. An algorithm is proposed to traverse the PDA to summarize the effect for all possible executions in the loop. We have evaluated Proteus using loops from five open-source projects and two well-known benchmarks and applying the disjunctive loop summary to three applications: loop bound analysis, program verification and test case generation. The evaluation results have demonstrated that Proteus can compute a more precise bound than the existing loop bound analysis techniques; Proteus can significantly outperform the state-of-the-art tools for loop program verification; and Proteus can help generate test cases for deep loops within one second, while symbolic execution tools KLEE and Pex either need much more time or fail. 2019-06-01T07:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/7100 info:doi/10.1109/TSE.2017.2788018 https://ink.library.smu.edu.sg/context/sis_research/article/8103/viewcontent/336ed1cc9c1df91a9ae8b5a4977cc8d93e8f.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 Disjunctive loop summary path dependency automaton path interleaving Software Engineering
institution Singapore Management University
building SMU Libraries
continent Asia
country Singapore
Singapore
content_provider SMU Libraries
collection InK@SMU
language English
topic Disjunctive loop summary
path dependency automaton
path interleaving
Software Engineering
spellingShingle Disjunctive loop summary
path dependency automaton
path interleaving
Software Engineering
XIE, Xiaofei
CHEN, Bihuan
ZOU, Liang
LIU, Yang
LE, Wei
LI, Xiaohong
Automatic loop summarization via path dependency analysis
description Analyzing loops is very important for various software engineering tasks such as bug detection, test case generation and program optimization. However, loops are very challenging structures for program analysis, especially when (nested) loops contain multiple paths that have complex interleaving relationships. In this paper, we propose the path dependency automaton (PDA) to capture the dependencies among the multiple paths in a loop. Based on the PDA, we first propose a loop classification to understand the complexity of loop summarization. Then, we propose a loop analysis framework, named Proteus, which takes a loop program and a set of variables of interest as inputs and summarizes path-sensitive loop effects (i.e., disjunctive loop summary) on the variables of interest. An algorithm is proposed to traverse the PDA to summarize the effect for all possible executions in the loop. We have evaluated Proteus using loops from five open-source projects and two well-known benchmarks and applying the disjunctive loop summary to three applications: loop bound analysis, program verification and test case generation. The evaluation results have demonstrated that Proteus can compute a more precise bound than the existing loop bound analysis techniques; Proteus can significantly outperform the state-of-the-art tools for loop program verification; and Proteus can help generate test cases for deep loops within one second, while symbolic execution tools KLEE and Pex either need much more time or fail.
format text
author XIE, Xiaofei
CHEN, Bihuan
ZOU, Liang
LIU, Yang
LE, Wei
LI, Xiaohong
author_facet XIE, Xiaofei
CHEN, Bihuan
ZOU, Liang
LIU, Yang
LE, Wei
LI, Xiaohong
author_sort XIE, Xiaofei
title Automatic loop summarization via path dependency analysis
title_short Automatic loop summarization via path dependency analysis
title_full Automatic loop summarization via path dependency analysis
title_fullStr Automatic loop summarization via path dependency analysis
title_full_unstemmed Automatic loop summarization via path dependency analysis
title_sort automatic loop summarization via path dependency analysis
publisher Institutional Knowledge at Singapore Management University
publishDate 2019
url https://ink.library.smu.edu.sg/sis_research/7100
https://ink.library.smu.edu.sg/context/sis_research/article/8103/viewcontent/336ed1cc9c1df91a9ae8b5a4977cc8d93e8f.pdf
_version_ 1770576212296466432